Make proof generic over current seL4 RISC-V platforms by lsf37 · Pull Request #1024 · seL4/l4v

lsf37 · 2026-07-02T03:13:54Z

This PR mostly makes the treatment of maxIRQ generic in the proofs, which is the only not-yet-generic parameter that still varies between RISC-V platforms. This means, after this PR is merged, all seL4 RISC-V platforms are supported by the full RISC-V proof stack.

Part of this update is fixing the machine interface definition getActiveIRQ for RISC-V. It was suppressing IRQ 0xFF, which was an invalid IRQ for a previous architecture, not for RISC-V. There is no effect on the proof, since this is an assumption that was not made use of anywhere (invalidIRQ = 0 on RISC-V).

PR for verified configs here: seL4/seL4#1698. I'm planning to make a separate PR for adding some of these to CI one both PRs are merged.

- add machine declarations for maxIRQ - remove old manual maxIRQ definition - add interface lemmas for maxIRQ Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Fix the definition of getActiveIRQ in RSICV64 to not suppress 0xFF, which was an invalid IRQ of some previous platform. Instead check for symbolic irqInvalid. From the proof perspective, even this check is not necessary, but it models actual hardware behaviour where irqInvalid (= irq 0) is reserved to mean "no IRQ". Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

- make sure we are referring to Kernel_Config.maxIRQ - increase alignment of IRQ node in example init state and add alignment check lemma (also used later in AInvs). We need to increase alignment, because some platforms have a much larger number of IRQs (>512). Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Use properties from Arch_Kernel_Config_Lemmas instead of unfolding, which also simplifies most proofs that are involved. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Xaphiosis · 2026-07-02T05:05:38Z

  unfolding kernelELFBase_def kernelELFPAddrBase_def pptrTop_def
  by (simp add: mask_def Kernel_Config.physBase_def)

+(* maxIRQ lemmas *)


when we use (* *) comments for a grouping, typically we have an empty line after... if there's no empty line, we assume the comment is only for the thing it's attached to

Xaphiosis · 2026-07-02T05:09:11Z

+  "x \<le> Kernel_Config.maxIRQ \<Longrightarrow> toEnum (unat x) = x" for x::machine_word
+  by (simp add: word_le_nat_alt Kernel_Config.maxIRQ_def)
+
+(* The following are derived and no longer need to unfold, but are small enough to include here *)


Same comment as above on needing an extra line after if this applies to more than just the next lemma.
Also I don't really understand what this comment says. The following [...] no longer need to unfold?

None of the lemmas that follow unfold any Kernel_Config.*dev. This means they don't really have to be in this theory. (But they are similar enough to the other ones and small enough that we want to keep them together).

Ah, then you might also want to add something to the comment, at least something after the "unfold", otherwise it's a complete mystery when reading it.

Xaphiosis · 2026-07-02T05:10:45Z

+
+lemma ucast_irq_bounded_machine_word:
+  "(ucast irq :: machine_word) < 2 ^ irq_len" for irq::irq
+  by (simp add: word_less_nat_alt unat_ucast_upcast is_up unat_2p_irq_len_machine unat_irq_bounded)


aside: how close are these Kernel_Config lemmas to the other Arms'?

many are just copies of the Arm ones

Xaphiosis · 2026-07-02T05:16:44Z

-     if is_masked active_irq \<or> active_irq = 0xFF \<or> (in_kernel \<and> active_irq \<in> non_kernel_IRQs)
+     if is_masked active_irq \<or> active_irq = irqInvalid \<or> (in_kernel \<and> active_irq \<in> non_kernel_IRQs)
     then return None
-     else return ((Some active_irq) :: irq option)


For this commit (riscv machine: fix getActiveIRQ) I have an irrational bias towards a non-fix title. Something like riscv machine: use irqInvalid in getActiveIRQ maybe? I have traumatic experiences where saying something was "fixed" was like taunting the gods. Saying it was updated to use irqInvalid instead of the incorrect 0xFF feels less drastic.

Also typo in commit message: RSICV64

Xaphiosis · 2026-07-02T05:23:03Z


-(* Sufficiently aligned for irq type + cte_level_bits *)
+(* Sufficiently aligned for irq type + cte_level_bits. irq_len can be up to 10, depending on
+   platform, so we need alignment to at least 15 bits. *)


alignment to at least 15 bits -> an alignment of at least 15 bits?
If you want "to at least", then I think it would fit in a "we need X to be aligned to at least ..." style sentence

Xaphiosis · 2026-07-02T05:29:06Z

           apply (clarsimp simp: up_ucast_inj_eq c_valid_cap_def ucast_eq_mask
                                 cl_valid_cap_def mask_twice from_bool_0
+                           simp flip: LENGTH_irq_len_irqBits
                          split: if_split bool.split


indentation edge case: alignment is now to argument start for first two args (simp, simp flip), but : for third (split)

Xaphiosis · 2026-07-02T05:29:58Z

 lemma array_assertion_abs_irq:
  "\<forall>s s'. (s, s') \<in> rf_sr \<and> True
-        \<and> (n s' \<le> 64 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
+        \<and> (n s' \<le> 2^irqBits \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))


did we ever decide if we prefer 2 ^ n over 2^n? I feel like we talked about this at some point, but completely forgot what the outcome was

yeah we did, and I think you won :)

Ahh, if I won then 2 ^ n please (also elsewhere in PR)

Xaphiosis · 2026-07-02T05:30:44Z

+  apply (rule mask_eq_ucast_eq[where 'a="irq_len" and 'b="machine_word_len" and 'c="machine_word_len",
+                               symmetric, simplified])
+  apply (simp flip: LENGTH_irq_len_irqBits)
+  done


waaay nicer now; do the Arms use this nicer tech too?

yes, most of that is from Arm :-)

Xaphiosis · 2026-07-02T05:32:59Z

  apply (cinit lift: irq_')
   apply (simp add: getIRQState_def getInterruptState_def)
-   apply (rule_tac P="irq \<le> ucast Kernel_C.maxIRQ \<and> unat irq < (126::nat)" in ccorres_gen_asm)
+   apply (rule_tac P="irq \<le> ucast Kernel_C.maxIRQ \<and> unat irq < Kernel_Config.maxIRQ+1" in ccorres_gen_asm)


would prefer + 1

Xaphiosis · 2026-07-02T05:35:16Z

  for x::machine_word
-  by (simp add: word_le_nat_alt maxIRQ_def Kernel_C.maxIRQ_def ucast_nat_def unat_ucast)
+  unfolding maxIRQ_def
+  by (simp add: Kernel_C_maxIRQ maxIRQ_ucast_toEnum_eq_irq irq_machine_le_maxIRQ_irq)


I'm a little confused by this block. unfolding maxIRQ_def will take it from the Platform one to the Kernel_Config one, and then maxIRQ_ucast_toEnum_eq_irq and irq_machine_le_maxIRQ_irq are Kernel_Config lemmas? If so, why don't they need the Kernel_Config. prefix here?

The lemmas are fine to use, that's why we make them. They never need the Kernel_Config prefix (unless the name is ambiguous somehow)

Right, so it's a case of "we don't have all the same theorems on Platform.maxIRQ because that would be duplication, and we can't just have everyone use the Kernel_Config ones uniformly because x86"

Correct, yes. This is CRefine, so everything is fully arch specific, and going via Platform.maxIRQ wouldn't really help anything.

Xaphiosis · 2026-07-02T05:40:39Z

-value_type irq_array_size = "Suc (unat Kernel_C.maxIRQ)"
+lemma Kernel_C_maxIRQ:
+  "Kernel_C.maxIRQ = Kernel_Config.maxIRQ"
+  by (simp add: Kernel_C.maxIRQ_def Kernel_Config.maxIRQ_def)


I'm wondering... this equation bypasses the Platform maxIRQ, which means it can only be applied after unfolding maxIRQ. Is this related to only having some properties on Platform maxIRQ, and the rest on Kernel_Config.maxIRQ, and so we end up in this strange land where we have to unfold to use the Kernel_Config lemmas, but if we unfolded we now need to relate the Kernel_C maxIRQ to Kernel_Config.maxIRQ?

Xaphiosis · 2026-07-02T05:43:42Z

   apply (rule equiv_valid_guard_imp, rule invoke_untyped_reads_respects_g_wcap)
   apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state valid_untyped_inv_wcap)
-   apply auto[1]
+   (* resolve schematics first, auto and fastforce only take forever *)


I first read this as (only take forever), which seemed very deep and poetic... on second read, I realised it's auto and (fastforce only) :P

Xaphiosis · 2026-07-02T05:50:40Z

+                                                  pt_offs_range_def cnode_offs_range_def
+                                                  page_offs_range_def irq_len_val
+                                                  s0_ptr_defs mask_def is_aligned_def,
+                                   unat_arith?\<close>\<close>)


While this is bravery award territory, there's also a lot of repetition, and the differences appear to only be 16 vs 17. Would it make sense here to deploy supply_local_method technology here?

We could, and maybe I'm wrong, but I somewhat wanted to keep this ugly so that it doesn't look like this needs no cleanup. The current approach in these lemmas is "unfold everything to raw numbers, then use unat_arith to solve". Previously it was "unfold most of everything to raw numbers, do some word rules on magic numbers, then try to solve with big hammers". Neither of them is good. Ideally this would be mostly symbolic, which would make the whole theory a lot faster and hopefully easier to understand. It's a bit of a project, though.

Xaphiosis · 2026-07-02T05:52:19Z

Commits:

riscv aspec: adjustments for generic maxIRQ has the following in the comment:
- make sure we are referring to Kernel_Config.maxIRQ however the contents of the commit does not have anything related to Kernel_Config. Removing that reduces the bullet point list to one point, and so it can stop being a list.
riscv proofs: update for generic maxIRQ: the phrase which also simplifies most proofs that are involved. could use some clarification... do you maybe mean "proofs involving them" (where them = the properties?)

irq_cnode is unused, the real IRQ node is at init_irq_node_ptr. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Replace quadratic number of long-running arithmetic goals (with unat_arith) for pspace_distinct' with linear check on sorted list of addresses. This should generalise to abstract-level pspace_distinct as well in the future. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lsf37 requested review from Xaphiosis and corlewis July 2, 2026 03:13

lsf37 mentioned this pull request Jul 2, 2026

configs: proofs now generic in RISC-V config; add stm32mp2 for AArch64 seL4/seL4#1698

Merged

lsf37 added 4 commits July 2, 2026 13:20

riscv machine+m-skel: maxIRQ declaration + lemmas

f172107

- add machine declarations for maxIRQ - remove old manual maxIRQ definition - add interface lemmas for maxIRQ Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

riscv proofs: update for generic maxIRQ

1edc961

Use properties from Arch_Kernel_Config_Lemmas instead of unfolding, which also simplifies most proofs that are involved. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lsf37 force-pushed the riscv-maxIRQ branch from 426836a to 1edc961 Compare July 2, 2026 03:20

Xaphiosis reviewed Jul 2, 2026

View reviewed changes

lsf37 added 2 commits July 10, 2026 18:57

[squash] infoflow: remove obsolete irq_cnode

7eb97f4

irq_cnode is unused, the real IRQ node is at init_irq_node_ptr. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Uh oh!

Conversation

lsf37 commented Jul 2, 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!

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!

Xaphiosis Jul 2, 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!

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!

Xaphiosis commented Jul 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

lsf37 commented Jul 2, 2026 •

edited

Loading

Xaphiosis Jul 2, 2026 •

edited

Loading