arch-split Init_R and InterruptAcc_R by Xaphiosis · Pull Request #985 · seL4/l4v

Xaphiosis · 2026-03-31T03:24:32Z

These are small files, was able to get through them relatively quickly.

🦆🦆🦆 Init_R is mainly taking out the arch states into their own file with two wrapped lemmas, so I didn't bother with the whole PR diff-minimisation setup for it, but did the setup for InterruptAcc_R.

Instructions:

In real life, I did the usual addition of InterruptAcc_R, hierarchy update, arch-split and then update. However, since the arch-split part first splits AARCH64, then takes the AARCH64 version of InterruptAcc_R and only fixes what broke, we ended up with a small(er) diff there (again).

Please review commit-by commit with the following notes:

single-commit split of Init_R due to its small size
[squash] PR: copy AARCH64 version into ..._R - same as last time: stop ..._R looking like a wall of green (no need to review)
aarch64 refine: arch-split ..._R` - this is the main bulk of the arch-split, dealing with AARCH64, as well as updates
[squash] copy AARCH64 Arch..._R to other arches - wipes the body (not the header!) of other arches' Arch..._R with a copy of the AARCH64 version with AARCH64 appropriately substituted - (mostly pointless to review)
`[squash][fake] refine: arch-split ..._R (other arches) - result of fixing up the ArchSchedule_R of other architectures - shows diff to AARCH64

Reminder: DO NOT MERGE squashed version if it still says aarch64 refine: arch-split or AARCH64

Stats: 31 files changed, 386 insertions(+), 1243 deletions(-)
Total: 857 lines removed

Xaphiosis · 2026-03-31T03:25:12Z

Still checking the builds on my side, but not expecting CRefine to be affected.

corlewis · 2026-03-31T04:51:01Z

proof/refine/InterruptAcc_R.thy

+  assumes preemptionPoint_corres:
+    "corres (dc \<oplus> dc) \<top> \<top> preemption_point preemptionPoint"


It might not be worth it since the current proof just unfolds everything, but it feels like this should be able to be a generic lemma. I think the only arch-specific part of preemptionPoint is the doMachineOp (getActiveIRQ True), so it should be possible to have an interface lemma just for that.

Done now, see new commit and comment below.

proof/refine/X64/ArchInterruptAcc_R.thy

corlewis

It's a bit confusing that AARCH64 had so much more in InterruptAcc_R that could be removed, but this looks very good!

Xaphiosis · 2026-04-01T00:03:27Z

Followed @corlewis's advice and tried to make preemptionPoint_corres generic. There was a lot of friction fighting OR_choice_E and get/select_f, and the proof is more hand-holdy. It does clear out the locale though, since there are no longer any arch assumptions.

Please look over the extra commit, also @lsf37

Xaphiosis · 2026-04-01T03:24:32Z

It's a bit confusing that AARCH64 had so much more in InterruptAcc_R that could be removed, but this looks very good!

Thinking more about this: if we were to move those somewhere else then there wouldn't be a need for ArchInterruptAcc_R since for non-AARCH64 they are empty now.

lsf37 · 2026-04-01T03:39:00Z

proof/refine/InterruptAcc_R.thy

+lemma exec_liftE_get:
+  "(liftE get >>=E f) x = f x x"


This is worth a FIXME move

Will add. This is worth a moment of discussion of where to while we're here. exec_get is in NonDet_Lemmas.thy which don't see monad_eq yet. The earliest I think that does see monad_eq is ... uh... NonDetMonadLemmaBucket?

Nondet_Monad_Equations is a good place, I think

OK, added those FIXMEs

lsf37 · 2026-04-01T03:40:50Z

It's a bit confusing that AARCH64 had so much more in InterruptAcc_R that could be removed, but this looks very good!

Thinking more about this: if we were to move those somewhere else then there wouldn't be a need for ArchInterruptAcc_R since for non-AARCH64 they are empty now.

That would be quite nice. What is left in AArch64 ArchInterruptAcc_R at this point? (hard to see in the diff)

lsf37 · 2026-04-01T03:42:22Z

Followed @corlewis's advice and tried to make preemptionPoint_corres generic. There was a lot of friction fighting OR_choice_E and get/select_f, and the proof is more hand-holdy.

I like the new generic proof better than the old unfold+hammer proofs. At least there is now chance of figuring out what is going on.

lsf37

Nice, I don't think we split the init proofs in AInvs, and there is really no reason not to. Also great that preemption point is generic now, I think that was worth it.

If we can eliminate ArchInterruptAcc entirely by moving AARCH64 lemmas I'm all for it (unless it's completely messy, but maybe we're in luck of a change).

Xaphiosis · 2026-04-01T04:57:19Z

If we can eliminate ArchInterruptAcc entirely by moving AARCH64 lemmas I'm all for it (unless it's completely messy, but maybe we're in luck of a change).

This is done in latest commit, please check if it's acceptable. It undoes some of the earlier work (rename and update hierarch), which means when I squash it'll also end up as a single commit.

lsf37 · 2026-04-01T05:07:32Z

This is done in latest commit, please check if it's acceptable. It undoes some of the earlier work (rename and update hierarch), which means when I squash it'll also end up as a single commit.

Looks all good, ready to go from my side!

corlewis · 2026-04-01T05:13:10Z

This is done in latest commit, please check if it's acceptable. It undoes some of the earlier work (rename and update hierarch), which means when I squash it'll also end up as a single commit.

Looks good to me as well!

Mainly to split off the zeroed arch state definitions. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Make InterruptAcc_R generic-only, including: * make preemptionPoint_corres generic at the cost of being a bit longer than the unfold-everything approach * migrate AARCH64 VCPU lemmas to Interrupt_R and Arch_R as needed and, since these theories don't depend on each other, move the common dependency virqType_eq to ArchStateRelationLemmas. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Xaphiosis · 2026-04-01T06:21:43Z

Squashed and rebased. Ready to merge once tests pass.

Xaphiosis requested review from corlewis, lsf37 and michaelmcinerney March 31, 2026 03:24

Xaphiosis added the arch-split splitting proofs into generic and architecture dependent label Mar 31, 2026

corlewis reviewed Mar 31, 2026

View reviewed changes

proof/refine/X64/ArchInterruptAcc_R.thy Outdated Show resolved Hide resolved

corlewis approved these changes Mar 31, 2026

View reviewed changes

Xaphiosis force-pushed the arch-split branch from 9149be8 to 1bb334c Compare April 1, 2026 02:31

lsf37 reviewed Apr 1, 2026

View reviewed changes

lsf37 approved these changes Apr 1, 2026

View reviewed changes

Xaphiosis added 2 commits April 1, 2026 17:04

refine: arch-split Init_R

62bb771

Mainly to split off the zeroed arch state definitions. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Xaphiosis force-pushed the arch-split branch from 63a193a to 5c86733 Compare April 1, 2026 06:11

Xaphiosis merged commit 88b6421 into master Apr 1, 2026
14 checks passed

Xaphiosis deleted the arch-split branch April 1, 2026 22:14

		assumes preemptionPoint_corres:
		"corres (dc \<oplus> dc) \<top> \<top> preemption_point preemptionPoint"

Conversation

Xaphiosis commented Mar 31, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Xaphiosis commented Mar 31, 2026

Uh oh!

corlewis Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Xaphiosis Apr 1, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

corlewis left a comment

Choose a reason for hiding this comment

Uh oh!

Xaphiosis commented Apr 1, 2026

Uh oh!

Xaphiosis commented Apr 1, 2026

Uh oh!

lsf37 Apr 1, 2026

Choose a reason for hiding this comment

Uh oh!

Xaphiosis Apr 1, 2026

Choose a reason for hiding this comment

Uh oh!

lsf37 Apr 1, 2026

Choose a reason for hiding this comment

Uh oh!

Xaphiosis Apr 1, 2026

Choose a reason for hiding this comment

Uh oh!

lsf37 commented Apr 1, 2026

Uh oh!

lsf37 commented Apr 1, 2026

Uh oh!

lsf37 left a comment

Choose a reason for hiding this comment

Uh oh!

Xaphiosis commented Apr 1, 2026

Uh oh!

lsf37 commented Apr 1, 2026

Uh oh!

corlewis commented Apr 1, 2026

Uh oh!

Xaphiosis commented Apr 1, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Xaphiosis commented Mar 31, 2026 •

edited

Loading