Proofs for runtime domain scheduling by lsf37 · Pull Request #969 · seL4/l4v

lsf37 · 2026-02-26T04:23:07Z

This PR adds proofs for seL4 PR seL4/seL4#1511, which implements runtime domains schedules as described in RFC-20.

Most changes are to generic files, architecture-specific proofs are only affected tangentially.

The commits are organised by larger proof package/spec, and can probably be squashed more after review (suggestions for grouping welcome).

Test with: seL4/seL4#1511

lsf37 · 2026-02-26T04:24:04Z

@ryybrr if you could take a look at the infoflow proofs that would be great. Mainly to see if this setup would break anything you are currently working on.

Xaphiosis · 2026-02-26T15:15:50Z

lib/clib/Corres_UL_C.thy


+lemma ccorres_assume_pre_sr:
+  assumes "\<And>s s'. \<lbrakk>P s; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> rrel xf arrel axf P P' hs f g"
+  shows "ccorres_underlying sr \<Gamma> rrel xf arrel axf P P' hs f g"


I can't make sense of how and when I'd use this lemma. Can you enlighten me a bit? The conclusions look identical

The conclusion is identical, but when you apply the lemma you get additional assumptions. Combined with other assumptions in the goal, you can sometimes use these to make progress. This one is exactly like the existing ccorres_assume_pre, but it also gives you the state relation, hence _sr.

lib/ExtraCorres.thy

spec/machine/Kernel_Config_Lemmas.thy

spec/haskell/src/SEL4/API/InvocationLabels.lhs

spec/haskell/src/SEL4/Object/Structures/ARM.lhs

spec/haskell/src/SEL4/Object/Structures.lhs

spec/haskell/src/SEL4/Object/ObjectType.lhs

spec/haskell/src/SEL4/Object/Domain.hs

spec/abstract/ARM/Arch_Structs_A.thy

spec/abstract/X64/Arch_Structs_A.thy

spec/abstract/Schedule_A.thy

proof/invariant-abstract/Tcb_AI.thy

proof/invariant-abstract/DetSchedDomainTime_AI.thy

proof/refine/AARCH64/ArchVSpace_R.thy

proof/crefine/ARM/ADT_C.thy

proof/crefine/ARM/SR_lemmas_C.thy

proof/crefine/AARCH64/Invoke_C.thy

A variation with unat x < 2^LENGTH('b) exists, but is not suitable for direct rewriting in goals where the code checks overflow directly on the word type. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

- add none_top/bot preservation over function updates to the state - add listUpdate in HaskellLib_H as an abbreviation for built-in list_update. - add lemma for rewriting common post condition pair form into fst/snd - add corres lemma for ignoring "whenE P (throwError)" when the abstract can always non-deterministically throw. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

- extension to ccorres_assume_pre that also assumes the state relation - short cut lemma for proving corres_pre_*-style rules Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Abort early in config lemmas if numDomains cannot be stored within the number of bits available in the C domain schedule entries. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Haskell spec for RFC-20: seL4/rfcs#33 Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

- manually define basic time types and functions in Structs_B/Arch_Structs_B so they can be shared with ASpec - flip dependency order of Arch_Structs_B and Structs_B so that there is a generic ancestor that can defined the ticks type before the arch-specific definition of parseTimeArg that needs it - new skeleton files Domain_H and ArchDomain_H corresponding to the new Haskell Domain.hs files - mark domain_schedule_item as known type in the Haskell translator Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Specification for RFC-20: seL4/rfcs#33 Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Minimal changes, mainly noting that domains are not in authorised_invocation because of the already assumed absence of domain caps. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Add an explicit domain schedule to the capDL model. Currently no attempts at arch split or machine word abstraction to keep in line with the current code. Only store schedule and start, not current index or domain time, because scheduling is fully nondeterministic at the capDL level. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Only update the example systems for now. The initialiser explicitly assumes that all TCBs are allocated to domain 0, so there is no point setting a domain schedule. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

No change in the overall property, but the addition of invocations that can change the domain schedule has the following high-level consequences for the infoflow proof and infoflow refinement: - We now explicitly appeal to the (already assumed) absence of domain caps to prove that nothing related to the domain schedule can change. Previously we could trivially prove this property via crunch over the entire kernel without preconditions. - We add the absence of domain caps to the ADT_if invariants so that kernel_entry_if can be shown to preserve domain properties. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

- Before this commit, domain_set_start would correctly set a new start index for the domain schedule, and would end the current domain, but would not end the entire current domain schedule to actually start the new schedule. Reserve the last index in the domain schedule to be an end marker. In domain_set_start set the current domain index to the second to last index, such that after index increment in next_domain, we hit the end marker and therefore start the new schedule. - This change means that the valid_domain_list invariant now also depends on domain_index, which in turn means we need to prove more preservation lemmas. Use the infrastructure for domain field preservation from the InfoFlow session (PasUpdates.thy) in AInvs to reduce the number of lemma statements for this and re-use the setup in InfoFlow. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lsf37 requested review from Xaphiosis, corlewis and ryybrr February 26, 2026 04:23

lsf37 force-pushed the dyn-domains branch from e7c98b7 to 07dd3fb Compare February 26, 2026 04:26