Partially merge master into rt by corlewis · Pull Request #951 · seL4/l4v

corlewis · 2026-01-22T01:46:49Z

Significant changes merged in that are visible to rt proofs:

refine: arch-split KHeap_R
refine: unify SubMonad_R
refine: arch-split ArchAcc_R
spec+proof: pptrBase, haveSetTrigger, numSGIs
spec+proof: maybe_handle_interrupt
refine: arch-split CSpace_I
refine: arch-split CSpace1_R
refine: arch-split CSpace_R
spec+proof: update for vcpu_flush
ainvs: add new AInvsToplevel_AI to AInvs session
refine: add IRQReserved to state relation
refine: arch-split TcbAcc_R
arm spec+proof: GICv3 now allows 32 bit targets
refine: arch-split VSpace_R
refine+crefine: make valid_arch_obj' stateless
refine: arch-split Retype_R

In preparation for arch-split. Create KHeap_R.thy and update import hierarchy. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Notable observations: * X64 had pulled in a number of cross and related lemmas into KHeap_R that show up later for other arches. Isolating these shows they are not critical in ArchKHeap_R, but moving them will happen later in arch-split. * setObject_other_corres is requalified since it contains a free type variable, and locale interfaces cannot quantify over those * same goes for setObject and pspace_in_kernel_mappings' * drop diff_neg_mask[simp del] * drop if_cong[cong] * unify is_other_obj_relation_type_* assumptions, move to StateRelation * move a bunch of objBits lemmas to Bits_R * standardise a[a]_type_simps[simp] (on AARCH64/RISCV64 these are already in [simp]) Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

Auto-complete session names and options for the main run_tests script. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Currently any vcg invocation produces a warning about a duplicate simp rule that is used internally. Set the context that is passed to the VCG tactic to internal so that such warnings about internal rules are suppressed. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Document the existing options of the install_C_file command. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Make a syntax bundle for the C separation logic notation and remove the notation in the top-level C parser file so that it is not exported. Users can re-enable the syntax with "unbundle C_seplog_syntax". Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

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

Add an option no_modifies to the install_C_file command that will skip the generation of modifies proofs. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Skip the generation of modifies proofs in the original kernel_all locale. This locale is not used for the C proofs, and we are proving a set of new modifies theorems anyway later in the CSpec session. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

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

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

Show that the current FPU owner is always in the current domain. Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

Also add placeholder files for architectures that do not enable the FPU. Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

This theory was short and mostly generic. The arch-specific atcbContextSet proofs got interfaced in Bits_R. Unifying SubMonad_R in this manner uncovered issues with objBits_less_word_bits and objBits_pos_power2. These needed to be exported into the generic context, but contained free type variables so could not be placed in a locale. By using objBitsKO instead of objBits, we could avoid the free type variable, also migrating the resulting setup into Bits_R. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

In preparation for arch-split. Create ArchAcc_R.thy and update import hierarchy. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Notes: * During X64 verification, a number of lemmas were moved to KHeap_R relative to other architectures and ended up in ArchKHeap_R during arch-split. To sync up the architectures, we pulled them back into ArchArchAcc_R Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

After discussion, `proof` block after [global_]interpretation should be indented as per autoindenter, as per style guide. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Describes disabiguation of fact names using `global./Arch.` prefix, and `named_theorems` caveat to fact name ordering. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Add example of disambiguating a constant that has the same name both within Arch and in the global context. Add examples of named_theorems causing an internal fact name reordering, resulting in the unqualified fact name being the arch-specific one despite the `global_naming global` requalification. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Add missing Isabelle update in debug ML code. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Using requalify_types (in Arch) inside the Arch locale has unexpected side effects such as switching global naming from AARCH64_H to Arch. Use outside the locale as intended. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

FNSPEC comments were re-using the C identifier spec for theorem names, which is too restrictive. For function specs where the function name starts with an underscore, the lemma name will need to contain the ' character, e.g. StrictC'_f_spec. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

It's annoying when jumping between --l4v-arch-all and --l4v-arches when re-using command history. Introduce an --l4v-arch= option to make things more consistent, i.e.: run_tests --l4v-arch=X64,RISCV64 run_tests --l4v-arch-all Keep the old --l4v-arches as an alias for --l4v-arch for compatibility: run_tests --l4v-arches=X64,RISCV64 Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

When using the skip_proofs checkbox in our version of the JEdit Isabelle plugin and closing/killing JEdit, sometimes the skip_proofs setting is persistently set in ~/.isabelle/etc/preferences Running run_tests after that makes it look like everything worked when no proofs were checked. Caveat: Isabelle internally respects ISABELLE_BUILD_OPTIONS, which can contain skip_proofs, but `isabelle options -g skip_proofs` will ignore that and only print the etc/preferences setting. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

corlewis · 2026-01-22T01:51:55Z

For reviewing purposes, the merge commit has been split into two, one with the merge conflicts left in and the second resolving them.

I'm not sure how helpful it will be in this case, a lot of the conflicts were very large and difficult to resolve, but let me know if it makes reviewing any easier.

These two commits will need to be squashed before this PR is merged.

corlewis · 2026-01-22T01:54:44Z

proof/refine/RISCV64/ArchInvsLemmas_H.thy


 lemmas objBits_defs =
  tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def cteSizeBits_def replySizeBits_def
+  minSchedContextBits_def


I am unsure whether moving minSchedContextBits_def out of bit_simps' and into objBits_defs was a good idea. It feels like it's more consistent with the other definitions and it made some proofs simpler, but it also made others more complicated when they expected minSchedContextBits to not be unfolded.

See faffd13#diff-d8509b2fca55c1719ec4ad344c91ff883c66772f66f50932b3e28ec23f0de945R1749 as an example of this making a proof worse.

I don't have strong feelings either way. Conceptually, it does make more sense to include in objBits_defs than in bit_simps' and I don't think the proof fixups are problematic. A mild preference for leaving it as you have it now.

corlewis · 2026-01-22T04:17:39Z

Proof tests aren't working here due to what we suspect is a GitHub problem, but I can confirm that all relevant tests pass.

lsf37

Wow, that proof fixup was a massive amount of work, I am impressed. Also about 100k lines removed with importing the arch split is nice to see in this accumulated form.

I've reviewed the fixup commit closely and the conflict resolution a bit faster. I found the conflict resolution part useful to get an impression of what is going on and where the problem areas were, but if it is a huge hassle to produce/squash I can live without it (if it is easy, it is nice to have, though).

Overall looks good, I did not spot any problems.

corlewis · 2026-01-27T02:47:17Z

Wow, that proof fixup was a massive amount of work, I am impressed. Also about 100k lines removed with importing the arch split is nice to see in this accumulated form.

Yeah, I was maybe a bit ambitious doing all of this in one merge. The changes are mostly orthogonal which is why I thought it was ok, but it ended up a lot bigger than I expected.

corlewis · 2026-01-27T02:50:01Z

I've reviewed the fixup commit closely and the conflict resolution a bit faster. I found the conflict resolution part useful to get an impression of what is going on and where the problem areas were, but if it is a huge hassle to produce/squash I can live without it (if it is easy, it is nice to have, though).

Good to hear that it helps. It was easy to produce and I'm confident that it will be just as easy to squash, so shouldn't be any problem for future merges. I guess it's particularly useful in cases like this, where there was actually a fair bit of work involved in resolving the conflicts themselves.

michaelmcinerney

Looks great! Goodness me that must have been a difficult process

michaelmcinerney · 2026-01-29T00:16:06Z

proof/refine/RISCV64/ArchKHeap_R.thy

+                         is_sc_obj_def)
+  done
+
+lemmas sc_inv_state_eq' = getObject_sc_inv[THEN use_valid[rotated], rotated


Maybe we don't want to fix this now, but this has the highly illegal comma on a new line

Good spotting, fixed

Xaphiosis · 2026-02-03T00:54:16Z

proof/crefine/RISCV64/Refine_C.thy

-  "ccorres dc xfdc invs' UNIV []
-           (liftE (maybeHandleInterrupt inKernel)) (Call checkInterrupt_'proc)"
+  "ccorres dc xfdc (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) UNIV []
+           ((maybeHandleInterrupt inKernel)) (Call checkInterrupt_'proc)"


(( )) -> ( )?

Xaphiosis · 2026-02-03T00:56:25Z

proof/refine/CSpace1_R.thy

@@ -3061,7 +3053,7 @@ lemma setCTE_UntypedCap_corres:
  apply (rename_tac abs conc conc' abs')

  (* FIXME RT: replace this with whatever comes out of VER-1248. *)


BTW: is this FIXME still relevant?

I think so, it's not related to arch-split or anything that has been changed in master. It's to do with the extract_conjunct these proofs use: https://sel4.atlassian.net/browse/VER-1248.

Xaphiosis · 2026-02-03T00:57:54Z

proof/invariant-abstract/DetSchedAux_AI.thy

  apply wp
  apply (clarsimp simp add: pred_tcb_at_def obj_at_def simp del: fun_upd_apply)
-  apply (clarsimp simp: etcbs_of'_def etcb_at'_def etcb_of_def)
+  apply (clarsimp simp:  etcb_at'_def etcb_of_def pred_map_simps vs_heap_simps)


now double space after :

Xaphiosis · 2026-02-03T01:01:08Z

proof/refine/RISCV64/ArchTcbAcc_R.thy

+  apply (wpsimp wp: threadSet_iflive'T)
+   apply (fastforce simp: update_tcb_cte_cases)
+  apply fastforce
+  done


does this not work with only wpsimp like for tcbInReleaseQueue_update_iflive'? It should still work with one-lining these with wpsimp wp: threadSet_iflive'T; fastforce simp: update_tcb_cte_cases

Funnily enough, if_live_then_nonz_cap' is about to be unceremoniously ripped out of rt. It wouldn't be hard to do the same thing to master.

Xaphiosis · 2026-02-03T01:03:52Z

proof/refine/RISCV64/IpcCancel_R.thy

  "valid_pspace' s \<Longrightarrow> pspace_bounded' s"
  by fastforce

+context Arch begin arch_global_naming


no FIXME on this one?

This arch locale actually already existed on master, it must have been removed from rt at some point. In my mind that meant it didn't need an additional FIXME, it should be handled properly once the arch-split process reaches this file.

Xaphiosis · 2026-02-03T01:04:58Z

proof/refine/RISCV64/IpcCancel_R.thy

+  unfolding valid_pspace'_def
+  by wpsimp
+
+end


I picked up the habit of commenting on which locale the ends are for. Here it's rather short, but something to consider.

Significant changes merged in that are visible to rt proofs: * refine: arch-split KHeap_R * refine: unify SubMonad_R * refine: arch-split ArchAcc_R * spec+proof: pptrBase, haveSetTrigger, numSGIs * spec+proof: maybe_handle_interrupt * refine: arch-split CSpace_I * refine: arch-split CSpace1_R * refine: arch-split CSpace_R * spec+proof: update for vcpu_flush * ainvs: add new AInvsToplevel_AI to AInvs session * refine: add IRQReserved to state relation * refine: arch-split TcbAcc_R * arm spec+proof: GICv3 now allows 32 bit targets * refine: arch-split VSpace_R * refine+crefine: make valid_arch_obj' stateless * refine: arch-split Retype_R

This mostly involves updates for arch-splitting InvariantUpdates_H and StateRelation. Note: new rt content has not been completely arch-split. Simple parts that easily follow patterns from master have been, but the rest has just been updated to continue working. They will be arch-split in a separate pass later. Some additional changes were also needed for maybe_handle_interrupt. Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

Xaphiosis and others added 30 commits July 30, 2025 10:11

refine: KHeap_R given Arch prefix

e2c7f56

In preparation for arch-split. Create KHeap_R.thy and update import hierarchy. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

refine: update for KHeap_R arch-split

450762c

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

crefine: update for KHeap_R arch-split

1102853

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

monads: add no_fail_whileLoop to Nondet_While_Loop_Rules

b06393d

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

lib: use no_fail_whileLoop in corres_whileLoop_ret

512192d

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

lib: add det_wp_whileLoop to DetWPLib

1bee128

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

lib: make det_wp_pre [wp_pre]

48482a1

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

misc: bash completion for run_tests

8005b22

Auto-complete session names and options for the main run_tests script. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

c-parser: document options in README

cef9c1e

Document the existing options of the install_C_file command. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

clib: use syntax bundle for seplog notation

bef3022

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

c-parser: make modifies proofs optional

01fd24a

Add an option no_modifies to the install_C_file command that will skip the generation of modifies proofs. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

gitignore: ignore tex generated files in c-parser

1c5df66

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

lib: add valid_none_top_post_wp

0a0597b

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

x64+aarch64 ainvs: prove cur_fpu_in_cur_domain

951771f

Show that the current FPU owner is always in the current domain. Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

ainvs: add ArchFPU_AI to AInvs session

4806a49

Also add placeholder files for architectures that do not enable the FPU. Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

refine: ArchAcc_R given Arch prefix

8c5740d

In preparation for arch-split. Create ArchAcc_R.thy and update import hierarchy. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

refine: update for ArchAcc_R arch-split

2022a02

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

crefine: update for ArchAcc_R arch-split

001cdd1

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

docs: arch-split: indentation for interpretations

5ce23db

After discussion, `proof` block after [global_]interpretation should be indented as per autoindenter, as per style guide. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

docs: arch-split: global fact name disambiguation

47d2a9c

Describes disabiguation of fact names using `global./Arch.` prefix, and `named_theorems` caveat to fact name ordering. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

SimplExport: fix debug theory

1ab23d6

Add missing Isabelle update in debug ML code. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

aarch64 design: use requalify_types correctly

d5463a9

Using requalify_types (in Arch) inside the Arch locale has unexpected side effects such as switching global naming from AARCH64_H to Arch. Use outside the locale as intended. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Xaphiosis added 2 commits December 8, 2025 17:59

corlewis requested review from Xaphiosis, lsf37 and michaelmcinerney January 22, 2026 01:46

corlewis self-assigned this Jan 22, 2026

corlewis added the MCS related to `rt` branch and mixed-criticality systems label Jan 22, 2026

corlewis commented Jan 22, 2026

View reviewed changes

corlewis force-pushed the rt-merge branch 2 times, most recently from d37a612 to 61c2e20 Compare January 22, 2026 04:15

corlewis force-pushed the rt-merge branch 2 times, most recently from 2065cba to 3d160c9 Compare January 27, 2026 01:12

lsf37 approved these changes Jan 27, 2026

View reviewed changes

michaelmcinerney approved these changes Jan 29, 2026

View reviewed changes

Xaphiosis reviewed Feb 3, 2026

View reviewed changes

corlewis mentioned this pull request Feb 5, 2026

Backport minor cleanup from rt #956

Merged

corlewis added 2 commits February 9, 2026 14:10

corlewis force-pushed the rt-merge branch from 2412b63 to 6d75119 Compare February 9, 2026 03:11

corlewis merged commit 6d75119 into rt Feb 9, 2026
8 of 14 checks passed

corlewis deleted the rt-merge branch February 9, 2026 03:15

		@@ -3061,7 +3053,7 @@ lemma setCTE_UntypedCap_corres:
		apply (rename_tac abs conc conc' abs')

		(* FIXME RT: replace this with whatever comes out of VER-1248. *)

Comments

Conversation

corlewis commented Jan 22, 2026

Uh oh!

corlewis commented Jan 22, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

corlewis commented Jan 22, 2026

Uh oh!

lsf37 left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

corlewis commented Jan 27, 2026

Uh oh!

corlewis commented Jan 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

michaelmcinerney left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

lsf37 left a comment •

edited

Loading

corlewis commented Jan 27, 2026 •

edited

Loading