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