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
