Hi Li-Jun, usually I would not reply to a clearly LLM-generated email, but since you are a student and seem to want to learn, I will make an exception.
The short version is: you should not believe everything Claude tells you. > [..] this means any Haskell prototype edit transitively invalidates ASpec > and AInvs builds this is incorrect > because sessions ExecSpec causes ExecSpec's whole content to be > source-re-executed inside ASpec's ML state. and this makes no sense. ML state is irrelevant here. ASpec does build on ExecSpec as its base session, it only includes specific ExecSpec theories. ASpec will only be rebuilt if the content hash of those theories changes. You can try it out: build ASpec, then change something in e.g. CSpace.lhs in Haskell, and rebuild ASpec. The Makefile will regenerate all ExecSpec theories, and Isabelle will recognise that no relevant content has changed and not rebuild ASpec. Ignoring this, there is still the question why is there no shared base image? The answer is that it has no strong advantages, but a few small disadvantages such as increasing the overall build time because it would produce yet another session image with associated heap export, etc. I’ve been tempted a few times to propose a similar refactor, just because it would look neater, but I have so far decided against it each time. I find that the cognitive dissonance (why does ASpec include ExecSpec theories?) is useful. It serves as a strong marker that some parts are shared and that to get changes in ASpec one might have to edit Haskell source. As you can see, even an LLM can figure out easily which theories these are, so it’s not like they are hard to find. With a common base image, you would be able to gloss over this fact for fairly long if you are new to the proofs and are likely to make plans for changes that do not take into account that Haskell code is relevant for ASpec. Cheers, Gerwin > On 16 May 2026, at 13:29, li-jun zhang via Devel <[email protected]> wrote: > > shared-types design choice Hi seL4 verification team, my name is Li-Jun > Zhang, a PDH student form Nanjing University. I'm studying the structure of > spec/ROOT and have a question about a design choice I'd like to understand > before considering whether it's worth trying to change. The observation > ASpec is declared in spec/ROOT as session ASpec in "abstract" = Word_Lib + > sessions "HOL-Library" Lib ExecSpec ... Across the codebase there are nine > direct imports "ExecSpec.X" from spec-side files, through five targets: > > | Imported ExecSpec theory | Importing spec-side theory | | --- | --- | | > ExecSpec.MachineTypes | CKernel.Kernel_C, CSpec.Kernel_C, > ExecSpec.MachineMonad | | ExecSpec.InvocationLabels_H | ASpec.ArchDecode_A, > ASpec.Decode_A | | ExecSpec.Event_H | ASpec.Syscall_A, DSpec.Syscall_D | | > ExecSpec.Arch_Structs_B | ASpec.Arch_Structs_A | | ExecSpec.ArchLabelFuns_H > | ASpec.InvocationLabels_A | > Combined with the sessions ExecSpec declaration, this means any Haskell > prototype edit transitively invalidates ASpec and AInvs builds — even when > the edit doesn't touch any of the five shared targets, because sessions > ExecSpec causes ExecSpec's whole content to be source-re-executed inside > ASpec's ML state. The skeleton file spec/design/skel/ARM/Arch_Structs_B.thy > carries the comment (* Architecture-specific data types shared by spec and > abstract. *) which suggests these targets are understood as cross-pillar > shared, yet they physically live inside the Haskell-derived ExecSpec > session. The comment dates back to commit 2a03e81 (the initial open-source > release in 2014), and the sessions ExecSpec line has survived multiple > subsequent ROOT reorganizations (e.g. the 2018 session-qualified-imports > work and the 2020-10 new ROOT requirements reorg), so I assume the > structure is intentional rather than incidental. The hypothetical change > Suppose the closure of the five shared targets within ExecSpec (12 theories > total: MachineTypes, MachineMonad, MachineOps, MachineExports, Platform, > Kernel_Config, Setup_Locale, Event_H, ArchInvocationLabels_H, > InvocationLabels_H, ArchLabelFuns_H, Arch_Structs_B) were moved into a base > KernelTypes session, with ASpec and ExecSpec both reparented to + > KernelTypes. Then: sessions ExecSpec could be removed from ASpec's ROOT > entry. A Haskell-side edit that doesn't touch the 12 shared theories would > no longer invalidate ASpec / AInvs. Type identity is preserved as long as > the moved files keep global_naming ARM_H — the fully qualified names > (ARM_H.arm_vspace_region_use, etc.) referenced by downstream are unchanged. > My question Was an extraction of this kind considered when the current > structure was designed (presumably pre-2014, given the comment dates from > the initial release)? Are there constraints — generation-pipeline output > paths, type-equality concerns beyond the global_naming trick, > methodological coupling between Haskell-as-canonical-source and the > abstract spec, downstream tooling that references the ExecSpec.X FQNs, or > anything else — that make the current sessions ExecSpec structure the > deliberate choice? I'd rather not pursue a refactor that's already been > considered and rejected for a reason I'm not seeing. Pointers to prior > discussion (mailing-list threads, design notes, PRs) would be very helpful. > Thanks Li-Jun Zhang > _______________________________________________ > Devel mailing list -- [email protected] > To unsubscribe send an email to [email protected] _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
