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

corlewis · 2026-07-26T03:04:19Z

Significant changes merged in that are visible to rt proofs:

refine+crefine: arch-split Detype_R
refine: expose threadSet_invs_trivialT as generic interface
refine: arch-split IpcCancel_R
cspec/c: extract maxIRQ for RISCV64
refine: arch-split Init_R
refine: arch-split InterruptAcc_R
refine+crefine: arch-split Finalise_R
refine: improve TcbAcc_R arch-split
refine+crefine: arch-split Ipc_R
refine+crefine: arch-split CNodeInv_R
refine+crefine: arch-split Tcb_R
spec+proofs: consolidate maxIRQ definition in Platform.thy
aarch64: remove plic_complete_claim
refine: arch-split Interrupt_R
monads: introduce opt_filter projection
aarch64 aspec+ainvs: introduce asid_map
refine+crefine: update proofs for asid_map addition
aarch64: CONFIG_VTIMER_UPDATE_VOFFSET=OFF

As always with these merges, the main commit to review is the 'update after merge' one. Quite a lot of work went into the merge commit itself, trying to resolve conflicts in a way that minimised the overall effort, but I don't know how feasible that is to review. The final crefine commit has already been reviewed elsewhere and is only cherry-picked here to try to avoid merge-related git complications.

corlewis · 2026-07-26T03:20:18Z

-lemma tcb_cte_cases_simps[simp]:
-  "tcb_cte_cases 0  = Some (tcbCTable, tcbCTable_update)"
-  "tcb_cte_cases (1 << cteSizeBits) = Some (tcbVTable, tcbVTable_update)"
-  "tcb_cte_cases (2 << cteSizeBits) = Some (tcbIPCBufferFrame, tcbIPCBufferFrame_update)"
-  "tcb_cte_cases (3 << cteSizeBits) = Some (tcbFaultHandler, tcbFaultHandler_update)"
-  "tcb_cte_cases (4 << cteSizeBits) = Some (tcbTimeoutHandler, tcbTimeoutHandler_update)"
-  by (simp add: tcb_cte_cases_neqs_n tcb_cte_cases_def)+
-
 lemmas tcbSlot_defs = tcbCTableSlot_def tcbVTableSlot_def tcbIPCBufferSlot_def
                      tcbFaultHandlerSlot_def tcbTimeoutHandlerSlot_def

+lemma tcb_cte_cases_simps[simp]:
+  "tcb_cte_cases (tcbCTableSlot << cteSizeBits) = Some (tcbCTable, tcbCTable_update)"
+  "tcb_cte_cases (tcbVTableSlot << cteSizeBits) = Some (tcbVTable, tcbVTable_update)"
+  "tcb_cte_cases (tcbIPCBufferSlot << cteSizeBits) = Some (tcbIPCBufferFrame, tcbIPCBufferFrame_update)"
+  "tcb_cte_cases (tcbFaultHandlerSlot << cteSizeBits) = Some (tcbFaultHandler, tcbFaultHandler_update)"
+  "tcb_cte_cases (tcbTimeoutHandlerSlot << cteSizeBits) = Some (tcbTimeoutHandler, tcbTimeoutHandler_update)"
+  by (simp add: tcb_cte_cases_neqs_n tcb_cte_cases_def tcbSlot_defs)+
+
+lemmas tcb_cte_cases_simps'[simp] = tcb_cte_cases_simps[simplified tcbSlot_defs shiftl_0]


This change is a bit unrelated to the rest of the merge but it's something that I found made some of the proofs I needed to update bit nicer and easier to keep symbolic. I didn't include it here but I was also tempted to add a version that uses _ * 2 ^ cteSizeBits instead of _ << cteSizeBits, as that form seems to be produced by the simplifier quite often.

Assuming that none of this is contentious, I might copy this specific change back to master, to see if it makes any proofs nicer there and to keep the branches more in sync.

I like the symbolic form, but I'd keep << -- we should usually not automatically simplify to 2^n, it's just that a lot of the existing proofs do that. Better to remove the latter than the former.

I didn't investigate too hard but some of the 2^n seemed to come out of the specification, which is why I was thinking to duplicate these lemmas to handle it as well. That way we would at least not have to do things like shiftl_t2n[symmetric] for easy cases.

yes, that would be perfectly fine, especially if we can do a lemmas ... = ...[simplified ...] thing

I approve of this change and backporting. One thing to check for is to make sure it doesn't introduce more warnings for duplicate simplification rules. It looks like it'll be fine, but keep an eye out.

For the 2^cteSizeBits, I'm ok if you make a rule for this case, but I would prefer that it not end up in [simp]. A long-term strategy is to get rid of the powers of two in favour of shifts and masks when they related to transforms like this, and when that happens seeing the explicit rule being added would be better than mystery failures or successes.

lsf37 · 2026-07-27T00:36:49Z

-   apply (rule delete_locale.deletionIsSafe_holds;
-          fastforce simp: delete_locale_def valid_cap_simps sch_act_simple_def state_relation_def
+   apply (rule detype_locale'.deletionIsSafe_holds;
+          fastforce simp: detype_locale'_def delete_locale_def invs_valid_pspace valid_cap_simps sch_act_simple_def state_relation_def


Does this fit on a line? (hard to see in the diff)

Good spotting, that line is too long. I'll change it to

apply (rule detype_locale'.deletionIsSafe_holds; fastforce simp: detype_locale'_def delete_locale_def invs_valid_pspace valid_cap_simps sch_act_simple_def state_relation_def sched_act_relation_def)

corlewis · 2026-07-27T00:48:04Z

I forgot to mention, while doing this update I did come across a lot of proofs and crunches that broke due to if_cong no longer being added to cong in Refine. I probably should have investigated more to see if they could be reworked not to need it, but for now I just added it back in as needed.

lsf37 · 2026-07-27T00:51:24Z

       apply (rule hoare_strengthen_post)
        apply (rule hoare_vcg_conj_lift[where Q="\<lambda>rv. cte_at' slot"])
-         apply (wp gen_typ_at_lifts [OF finaliseCap_typ_at'])[1]
+         apply (wp RISCV64.typ_at_lifts [OF finaliseCap_typ_at'])[1] (* FIXME: rt arch-split *)


Now that we've done the typ_at_lifts in master, do you remember if there is anything left that needs thinking for this in rt or can we just apply what we did on master?

(not for this PR, I'm just looking ahead to the rt arch split)

Just apply what we did on master, that was one of my goals with doing it there first.

lsf37 · 2026-07-27T01:10:09Z

I forgot to mention, while doing this update I did come across a lot of proofs and crunches that broke due to if_cong no longer being added to cong in Refine. I probably should have investigated more to see if they could be reworked not to need it, but for now I just added it back in as needed.

From my side, that's Ok. if_cong is easy to find if we want to reduce its use later, and locally it's not like using if_cong is a problem, it's just having it [cong] globally that it becomes slow and/or termination dangerous.

lsf37

A massive amount of work again (just the overall diff 36k+/134k- is gigantic), thank you for doing these. Our main problem with these merges is that we are so productive :-)

I have reviewed the post-merge commits closely and skimmed the merge commit. Looks all good from my side.

michaelmcinerney

Looks great! Just a few minor nitpicks and a few questions that we can discuss elsewhere, if you'd like to merge this soon.

michaelmcinerney · 2026-07-27T01:14:28Z

 context Finalise_R begin

+crunch finaliseCap
+  for aligned'[wp]: pspace_aligned'


Not for this PR, but this reminds me of the constant battle with shortened names and abbreviations we have for a lot of invariants and functions. I really dislike them, but maybe it's more of a personal bias than anything else. Though for crunch, I know that the naming is involved somehow. Remembering the abbreviations is like an extra burden and some of them are not really all that easy to figure out, either. For pspace_aligned', or maybe pspace_aligned in AInvs, we have at least psp_aligned, but there are probably several others floating around.

You are right, we should really standardise these, it's always a drag to try to remember which one is used in which context. I'm not sure we want to always have the full long form, but if there is some kind of abbreviating going on, it should always be the same and should be used consistently over different proofs.

It's been a plague for ages, with just about every person that tried to do an abbreviation coming up with a different way to abbreviate. I've seen many flavours of just about everything in crunches when arch-splitting. I'm actually fine for writing out the long name for crunches, and especially crunches that go straight into [wp].

michaelmcinerney · 2026-07-27T01:23:37Z

 lemmas asUser_st_tcb_at'[wp] = asUser_obj_at [folded st_tcb_at'_def]

-end
+end


Maybe not for this PR, but what's the convention with having an empty line at the end of a file? Do we have one? I just checked and Style.thy itself does not have an empty line at the end of the file.

I thought gitlint would be complaining about this (whatever we decided we wanted), but apparently not.

Edit: sorry, not gitlint, but the trailing whitespace check

michaelmcinerney · 2026-07-27T01:29:53Z

     (Tcb_A.restart t) (ThreadDecls_H.restart t)"
  apply (simp add: Tcb_A.restart_def Thread_H.restart_def test_possible_switch_to_def
                   get_tcb_obj_ref_def)
-  apply (rule corres_stateAssert_ignore, simp add: sch_act_wf_asrt_def)+


Thanks for removing these assert definitions.

Xaphiosis · 2026-07-28T03:19:38Z

       wp: crunch_wps undefined_valid finaliseSlot_preservation)

-global_interpretation invokeCNode: typ_at_all_props' "invokeCNode i"
+sublocale invokeCNode: typ_at_all_props' "invokeCNode i"


Is this an example of how the typ_all_at_props' shifting into an arch-splitted theory? I'm expecting that in the generic theory this is what drops the Arch interpretation?

This is actually an example of one shifting into an interface locale, and needing to do a sublocale for that reason.

The rt version of typ_at_all_props' is in a bit of a weird state where it hasn't been arch-split yet. Once I get back to and finish the master version and the merges into rt catch up to that then this should all be consistent.

In this case, this would still be a sublocale but as this is a generic file, it would be the generic version of typ_at_all_props'.

Xaphiosis · 2026-07-28T03:21:41Z


 abbreviation aobjs_of' :: "kernel_state \<Rightarrow> obj_ref \<rightharpoonup> arch_kernel_object" where
-  "aobjs_of' s \<equiv> ksPSpace s |> aobj_of'"
+  "aobjs_of' \<equiv> \<lambda>s. ksPSpace s |> aobj_of'"


interesting, where did this change originate? something backportable to master?

This projection was done on rt as part of the IPC queues work. We could backport the projections to master either separately, or certainly if/when we did the IPC queues work on master.

There's nothing to back port, the change makes the definition equal to the one in master.

This projection has actually already been added to master, as part of Gerwin's changes for the asid_map addition. During the merge I took master's version of the projection with the λ but kept it in the location that rt had it. In master, the abbreviation is instead in StateRelationPre.

Xaphiosis · 2026-07-28T03:34:26Z

-       pspace_distinct' s'; st_tcb_at (Not \<circ> halted) t s;
-       ctes_of s' (t + 2*2^cte_level_bits) = Some cte \<rbrakk>
-     \<Longrightarrow> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {})
-        = (mdbNext (cteMDBNode cte) = nullPointer)"


interesting, where did this one go?

Reply caps don't exist in rt in the same way as they do in master, so this and many other lemmas to do with them have been removed.

Xaphiosis · 2026-07-28T03:38:30Z

+  unfolding setSchedContext_def
+  apply (rule setObject_gen_obj_at, simp)
+  apply (wp setObject_state_hyp_refs_of'; simp add: gen_objBits_simps state_hyp_refs_of'_sc)
+  done


looks collapsible via rule ... ; wpsimp, same for set_reply_state_hyp_refs_of' below

Unfortunately doesn't work out nicely, something goes wrong with the application of state_hyp_refs_of'_sc.

Xaphiosis · 2026-07-28T03:39:26Z

   simp: crunch_simps o_def pteAtIndex_def
   rule: RISCV64_H.finaliseCap_def)

+declare prepareThreadDelete_nosch[CNodeInv_R_assms]


what's happening here?

Xaphiosis · 2026-07-28T03:41:54Z

-  by unfold_locales
-     (fact emptySlot_st_tcb_at')
-
-end (* delete_one_conc_pre *)


interesting that this is disappearing. did it move elsewhere during the merge? no longer necessary on rt?

I'm actually not sure what happened here. Looking at my different versions of the repository, it looks like I was able to remove delete_one_conc_pre_gen completely from rt?

I'm guessing that I might have noticed that all the lemmas in maser that needed to be proved inside of it had been deleted in rt, and then decided that there was no reason to keep the locale.

My guess is that cancelIPC doesn't have the cteDeleteOne in rt, so a lot of the deletion lemmas weren't necessary in the IPC cancel files.

Xaphiosis · 2026-07-28T03:44:03Z

  unfolding makeArchFaultMessage_def
  by (wpsimp wp: asUser_inv getRestartPC_inv split: arch_fault.split)

+declare lookupIPCBuffer_valid_ipc_buffer[Ipc_R_assms]


another one of these declares... not sure why you need to do them like this; also aside: for arch-split I never use declare, but lemmas [Ipc_R_assms] = ... because then they're easier to combine. And furthermore, it's much more convenient to put them as late as possible, right in front of the actual locale interpretation. Scattering them in the middle like this makes it hard to clean up. (same comment goes for any other declares like this)

They are from crunches, no? (collecting them at the end with lemmas is good, though, that's a nice method to settle on)

In master there are interface lemmas that are produced here by crunches, while in rt the crunches aren't doing anything because it finds preexisting lemmas that can be used instead. I didn't want to adjust the interface because some of those earlier lemmas won't exist for other architectures, and then without thinking too hard about it just put the declare where each crunch used to be.

I'll consolidate them and change to lemmas.

Xaphiosis · 2026-07-28T03:44:40Z

-  for pspace_aligned[Tcb_R_assms, wp]: pspace_aligned
-  and pspace_distinct[Tcb_R_assms, wp]: pspace_distinct
-  (wp: crunch_wps simp: crunch_simps)
+declare arch_post_modify_registers_inv[Tcb_R_assms]


another one of these declares

Xaphiosis · 2026-07-28T03:44:52Z

-  (simp: crunch_simps preemption_point_def wp: crunch_wps OR_choiceE_weak_wp)
+  (simp: crunch_simps wp: crunch_wps)
+
+declare prepare_thread_delete_inv[Tcb_R_assms]


and another one

Xaphiosis · 2026-07-28T03:58:24Z

+    done
+qed
+
+end (* detype_locale'_gen *)


is this identical to what is on master? did it move or something? it seems very familiar

The same locale structure as master, but moved and the deletionIsSafe lemma is a bit different on rt.

This one almost caused a whole bunch of problems but I was able to move some other lemmas that the rt version depends on into locales that let me keep the same overall structure.

Xaphiosis

Well done on getting through all that.
I have mainly questions, and one gripe: those declares make some sense being where they are in the diff, but the style and location approach is differing from what I was trying to do on master during arch-split. It would be nice if we were on the same frequency for those.

Xaphiosis · 2026-07-28T06:27:47Z

I think my comments are all answered or updated. Thanks!

corlewis requested review from Xaphiosis, lsf37 and michaelmcinerney July 26, 2026 03:04

corlewis self-assigned this Jul 26, 2026

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

corlewis force-pushed the rt-merge branch 2 times, most recently from baf8005 to 65c2b75 Compare July 26, 2026 03:19

corlewis commented Jul 26, 2026

View reviewed changes

corlewis force-pushed the rt-merge branch from 65c2b75 to d9db250 Compare July 26, 2026 03:26

lsf37 reviewed Jul 27, 2026

View reviewed changes

lsf37 approved these changes Jul 27, 2026

View reviewed changes

michaelmcinerney approved these changes Jul 27, 2026

View reviewed changes

Xaphiosis reviewed Jul 28, 2026

View reviewed changes

Comment thread proof/refine/KHeap_R.thy

Xaphiosis reviewed Jul 28, 2026

View reviewed changes

Comment thread proof/refine/Tcb_R.thy Outdated

Xaphiosis reviewed Jul 28, 2026

View reviewed changes

Xaphiosis approved these changes Jul 28, 2026

View reviewed changes

corlewis force-pushed the rt-merge branch from bb1e076 to 8a4a98a Compare July 28, 2026 06:32

corlewis force-pushed the rt-merge branch from 8a4a98a to 952a97c Compare July 28, 2026 09:00

corlewis merged commit 952a97c into rt Jul 28, 2026
11 of 12 checks passed

corlewis force-pushed the rt branch from 8b61de7 to 952a97c Compare July 28, 2026 12:09

corlewis deleted the rt-merge branch July 28, 2026 12:09

Uh oh!

Conversation

corlewis commented Jul 26, 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!

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!

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

Uh oh!

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!

lsf37 commented Jul 27, 2026

Uh oh!

lsf37 left a comment

Choose a reason for hiding this comment

Uh oh!

michaelmcinerney left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

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!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lsf37 Jul 27, 2026 • 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!

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!

lsf37 Jul 28, 2026 • 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!

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!

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

corlewis commented Jul 27, 2026 •

edited

Loading

lsf37 Jul 27, 2026 •

edited

Loading

lsf37 Jul 28, 2026 •

edited

Loading

lsf37 Jul 28, 2026 •

edited

Loading