Make proof generic over current seL4 RISC-V platforms

lib/Lib.thy

@@ -22,6 +22,7 @@ imports
   Monads.Monad_Lib
   Basics.CLib
   NICTATools
+  Sorted_Addrs
   "Word_Lib.WordSetup"
 begin
 

lib/ROOT

@@ -71,6 +71,7 @@ session Lib (lib) = Word_Lib +
     Rules_Tac
     Heap_List
     None_Top_Bot
+    Sorted_Addrs
 
     (* should move to Monads: *)
     NonDetMonadLemmaBucket

lib/Sorted_Addrs.thy

@@ -0,0 +1,253 @@
+(*
+ * Copyright 2026, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+theory Sorted_Addrs
+imports
+  Word_Lib.WordSetup
+  Eisbach_Tools.Eisbach_Methods
+begin
+
+(* Proving pspace_distinct' produces quadratically many slow arithmetic proof obligations when
+   done directly. If we instead provide a sorted list of addresses of non-overlapping objects,
+   pspace_distinct' follows abstractly. Proving that a list of addresses is sorted and
+   non-overlapping produces only linearly many proof obligations.
+
+   The local sorted_addrs below defines sorted lists of addresses for non-overlapping objects
+   and derives and unfolded version of pspace_distinct'. because pspace_distinct' itself is not
+   yet available. See lemma obj_spaced_distinct.
+
+   The locale can be instantiated to the abstract and design levels by providing either obj_bits
+   or objBitsKO as a parameter at interpretation.
+
+   In addition to a plain list of object addresses, there are also helper functions for defining
+   lists of aligned offsets within a larger region, for instance for CNodes or page tables, and
+   for appending these into the global sorted list of objects.
+
+   See proof/infoflow/refine/RISCV64/Example_Valid_StateH.thy for an example of how this is used.
+*)
+
+
+(* Addresses of objects inside CNodes or page tables. p is the start of the encompassing object
+   region, sz its size in bits, and `align` the homogeneous alignment (and size) of the smaller
+   objects within. These will automatically be sorted and non-overlapping. *)
+definition aligned_offsets :: "'a::len word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a word list" where
+  "aligned_offsets p sz align = [p, p + 2^align .e. p + mask sz]"
+
+locale sorted_addrs =
+  fixes bits_of :: "'o \<Rightarrow> nat" (* this is for obj_bits or objBitsKO *)
+begin
+
+(* get alignment of an object at specific address *)
+definition align_of :: "('a::len word \<rightharpoonup> 'o) \<Rightarrow> 'a word \<Rightarrow> nat" where
+  "align_of kh p \<equiv> case kh p of Some obj \<Rightarrow> bits_of obj | None \<Rightarrow> 0"
+
+(* the objects in the list are ordered by address and non-overlapping *)
+fun obj_spaced :: "('a::len word \<rightharpoonup> 'o) \<Rightarrow> 'a word list \<Rightarrow> bool" where
+  "obj_spaced kh []        = True"
+| "obj_spaced kh [p]       = True"
+| "obj_spaced kh (p#p'#ps) = (p + mask (align_of kh p) < p' \<and> obj_spaced kh (p'#ps))"
+
+(* pspace_aligned' in a more convenient form. The following is expected to hold when instantiated
+   to the design spec level:
+   "\<lbrakk> pspace_aligned' s; set addrs = dom (ksPSpace s) \<rbrakk> \<Longrightarrow> obj_aligned (ksPSpace s) addrs" *)
+definition obj_aligned :: "('a::len word \<rightharpoonup> 'o) \<Rightarrow> 'a word list \<Rightarrow> bool" where
+  "obj_aligned kh addrs \<equiv> \<forall>p \<in> set addrs. is_aligned p (align_of kh p)"
+
+(* all objects in the set have the given alignment *)
+definition offsets_align :: "('a::len word \<rightharpoonup> 'o) \<Rightarrow> 'a word set \<Rightarrow> nat \<Rightarrow> bool" where
+  "offsets_align kh addrs n \<equiv> \<forall>p \<in> addrs. align_of kh p = n"
+
+
+(* Lemmas *)
+
+lemma obj_spaced_nth:
+  "obj_spaced kh xs = (\<forall>i. Suc i < length xs \<longrightarrow>
+                           xs ! i + mask (align_of kh (xs ! i)) < xs ! Suc i)"
+  by (induct xs rule: obj_spaced.induct; fastforce simp: nth_Cons split: nat.split)
+
+lemma sorted_imp_obj_spaced:
+  "sorted_wrt (\<lambda>p p'. p + mask (align_of kh p) < p') xs \<Longrightarrow> obj_spaced kh xs"
+  by (induct xs rule: obj_spaced.induct) auto
+
+lemma obj_spaced_imp_sorted:
+  "\<lbrakk> obj_aligned kh addrs; set xs \<subseteq> set addrs; obj_spaced kh xs \<rbrakk> \<Longrightarrow>
+   sorted_wrt (\<lambda>p p'. p + mask (align_of kh p) < p') xs"
+  apply (induct xs rule: obj_spaced.induct; clarsimp)
+  apply (meson aligned_add_mask_lessD basic_trans_rules(19) obj_aligned_def)
+  done
+
+lemma obj_spaced_sorted:
+  "obj_aligned kh ps \<Longrightarrow> obj_spaced kh ps = sorted_wrt (\<lambda>p p'. p + mask (align_of kh p) < p') ps"
+  by (auto intro!: obj_spaced_imp_sorted sorted_imp_obj_spaced)
+
+lemma obj_spaced_append:
+  "obj_spaced kh (xs @ ys) =
+   (obj_spaced kh xs \<and> obj_spaced kh ys \<and>
+    (xs \<noteq> [] \<longrightarrow> ys \<noteq> [] \<longrightarrow> last xs + mask (align_of kh (last xs)) < hd ys))"
+  apply (induct xs rule: obj_spaced.induct; simp)
+  apply (case_tac ys, auto)
+  done
+
+lemma obj_spaced_distinct:
+  "\<lbrakk> obj_spaced kh addrs; obj_aligned kh addrs; dom kh = set addrs; kh p = Some ko \<rbrakk> \<Longrightarrow>
+   (mask_range p (bits_of ko) - {p}) \<inter> dom kh = {}"
+  apply (simp add: obj_spaced_sorted sorted_wrt_iff_nth_less)
+  apply (clarsimp simp: obj_aligned_def)
+  apply (prop_tac "p \<in> set addrs", fastforce)
+  apply (frule (1) bspec)
+  apply (simp add: align_of_def)
+  apply (rule Int_emptyI)
+  apply (rename_tac p')
+  apply clarsimp
+  apply (drule_tac x=p' in bspec, assumption)
+  apply (prop_tac "\<exists>ko'. kh p' = Some ko'", fastforce)
+  apply (clarsimp simp: in_set_conv_nth)
+  apply (rename_tac i j ko')
+  apply (case_tac "i < j"; clarsimp)
+   apply (erule allE)+
+   apply (erule (1) impE, erule (1) impE)
+   apply simp
+  apply (clarsimp simp: not_less le_less)
+  apply (prop_tac "i \<noteq> j", fastforce)
+  apply simp
+  apply (erule allE)+
+  apply (erule (1) impE, erule (1) impE)
+  apply simp
+  apply (drule is_aligned_no_overflow_mask)+
+  apply fastforce
+  done
+
+
+(* Arrays of small objects: aligned_offsets *)
+
+lemma length_aligned_offsets:
+  "is_aligned p sz \<Longrightarrow>
+   length (aligned_offsets p sz align) = Suc (unat ((mask sz :: 'a word) div 2 ^ align))"
+  for p::"'a::len word"
+  unfolding aligned_offsets_def
+  apply (subst length_upto_enum_step)
+   apply (erule is_aligned_no_overflow_mask)
+  apply simp
+  done
+
+lemma aligned_offsets_nth:
+  "\<lbrakk> is_aligned p sz; n < length (aligned_offsets p sz align) \<rbrakk> \<Longrightarrow>
+   aligned_offsets p sz align ! n = p + of_nat n * 2^align"
+  apply (simp add: aligned_offsets_def)
+  apply (subst upto_enum_step_nth)
+    apply (erule is_aligned_no_overflow_mask)
+   apply simp
+   apply (subst (asm) length_upto_enum_step)
+    apply (erule is_aligned_no_overflow_mask)
+   apply simp
+  apply simp
+  done
+
+lemma aligned_offsets_obj_spaced:
+  "\<lbrakk> offsets_align kh (set (aligned_offsets p sz align)) align; is_aligned p sz \<rbrakk> \<Longrightarrow>
+   obj_spaced kh (aligned_offsets p sz align)"
+  apply (clarsimp simp: obj_spaced_nth offsets_align_def)
+  apply (simp add: aligned_offsets_nth length_aligned_offsets ring_distribs add_ac)
+  apply (erule (1) nth_aligned_offset_no_overflow)
+  done
+
+lemma set_aligned_offsets:
+  "is_aligned p n \<Longrightarrow>
+   set (aligned_offsets p sz n) = {p'. p \<le> p' \<and> p' \<le> p + mask sz} \<inter> {p. is_aligned p n}"
+  apply (clarsimp simp: aligned_offsets_def upto_enum_step_def)
+  apply (rule conjI)
+   apply fastforce
+  apply (clarsimp simp: not_less)
+  apply (rule equalityI; clarsimp)
+   apply (rule conjI; clarsimp)
+    apply (meson div_to_mult_word_lt word_plus_mono_right word_plus_mono_right2)
+   apply (erule is_aligned_add)
+   apply (rule is_aligned_mult_triv2)
+  apply (clarsimp simp: image_iff)
+  apply (simp flip: shiftr_div_2n_w shiftl_eq_mult)
+  apply (rule_tac x="(x - p) >> n" in exI)
+  apply (rule conjI)
+   apply (simp add: add.commute le_shiftr word_diff_ls')
+  apply (prop_tac "is_aligned (x - p) n")
+   apply (erule (1) aligned_sub_aligned_simple)
+  apply (simp add: is_aligned_shiftr_shiftl)
+  done
+
+lemma aligned_offsets_neq_Nil:
+  "is_aligned p sz \<Longrightarrow> aligned_offsets p sz n \<noteq> []"
+  apply (prop_tac "length (aligned_offsets p sz n) \<noteq> 0")
+   apply (simp add: length_aligned_offsets)
+  apply clarsimp
+  done
+
+lemma hd_aligned_offsets:
+  "\<lbrakk> is_aligned p sz; sz < LENGTH('a) \<rbrakk> \<Longrightarrow> hd (aligned_offsets p sz n) = p" for p::"'a::len word"
+  apply (prop_tac "length (aligned_offsets p sz n) \<noteq> 0")
+   apply (simp add: length_aligned_offsets)
+  apply clarsimp
+  apply (frule is_aligned_no_overflow_mask)
+  apply (simp add: upto_enum_step_def not_less aligned_offsets_def split: if_splits)
+  apply (rule conjI, fastforce)
+  apply (simp add: hd_map)
+  apply (simp flip: shiftr_div_2n_w shiftl_eq_mult add: shiftr_mask2)
+  apply (clarsimp simp: upto_enum_def hd_append hd_map)
+  apply (simp add: unat_eq_zero)
+  done
+
+lemma hd_aligned_offsets_append:
+  "\<lbrakk> is_aligned p sz; sz < LENGTH('a) \<rbrakk> \<Longrightarrow> hd (aligned_offsets p sz n @ xs) = p"
+  for p::"'a::len word"
+  by (simp add: aligned_offsets_neq_Nil hd_aligned_offsets)
+
+lemma obj_spaced_cons_aligned_offsets:
+  "\<lbrakk> is_aligned p' sz; sz < LENGTH('a) \<rbrakk> \<Longrightarrow>
+   obj_spaced kh (p # aligned_offsets p' sz n @ xs) =
+   (p + mask (align_of kh p) < p' \<and> obj_spaced kh (aligned_offsets p' sz n @ xs))"
+  for p::"'a::len word"
+  apply (frule (1) hd_aligned_offsets[where n=n])
+  apply (drule aligned_offsets_neq_Nil[where n=n])
+  apply (clarsimp simp: neq_Nil_conv)
+  done
+
+lemma last_aligned_offsets:
+  "is_aligned p sz \<Longrightarrow> last (aligned_offsets p sz n) = p + (mask sz >> n << n)"
+  apply (frule aligned_offsets_neq_Nil[where n=n])
+  apply (simp add: last_conv_nth aligned_offsets_nth length_aligned_offsets)
+  apply (simp flip: shiftr_div_2n_w shiftl_t2n')
+  done
+
+lemma last_aligned_offests_plus_mask:
+  "\<lbrakk> offsets_align kh (set (aligned_offsets p sz n)) n; is_aligned p sz; n \<le> sz \<rbrakk> \<Longrightarrow>
+   last (aligned_offsets p sz n) + mask (align_of kh (last (aligned_offsets p sz n))) =
+   p + mask sz"
+proof -
+  assume sz: "n \<le> sz"
+  assume [simp]: "is_aligned p sz"
+  hence "aligned_offsets p sz n \<noteq> []"
+    by (rule aligned_offsets_neq_Nil)
+  moreover
+  assume "offsets_align kh (set (aligned_offsets p sz n)) n"
+  ultimately
+  have [simp]: "align_of kh (last (aligned_offsets p sz n)) = n"
+    by (simp add: offsets_align_def)
+  have "last (aligned_offsets p sz n) = p + (mask sz >> n << n)"
+    by (simp add: last_aligned_offsets)
+  also
+  have "... + mask n = p + (mask sz && ~~mask n) + mask n"
+    by (simp add: and_not_mask)
+  also
+  from mask_and_neg_mask_compose[OF sz]
+  have "...  = p + mask sz"
+    by simp
+  finally
+  have "last (aligned_offsets p sz n) + mask n = p + mask sz" .
+  thus ?thesis
+    by simp
+qed
+
+end (* locale sorted_addrs *)
+
+end

lib/Word_Lib/Word_Lemmas_Internal.thy

@@ -1130,4 +1130,56 @@ lemma ucast_0_eq_right:
 
 lemmas ucast_0_eq = ucast_0_eq_left ucast_0_eq_right
 
+lemma nth_aligned_offset_no_overflow:
+  fixes p :: "'a::len word"
+  assumes aligned: "is_aligned p sz"
+  assumes i: "i < unat (mask sz div 2 ^ n :: 'a word)"
+  shows "p + (mask n + word_of_nat i * 2 ^ n) < p + (2 ^ n + word_of_nat i * 2 ^ n)"
+proof -
+  from i
+  have n: "n < LENGTH('a)"
+    by (metis div_by_0 gr_implies_not0 unat_2tp_if unsigned_eq_0_iff)
+
+  from i
+  have i_len: "i < 2^LENGTH('a)"
+    by (auto intro: order_less_trans)
+
+  let ?i = "word_of_nat i :: 'a::len word"
+  from i
+  have i_shift: "?i < mask sz >> n"
+    by (simp add: word_less_nat_alt shiftr_div_2n_w i_len unat_of_nat_eq)
+
+  have Suc_i: "Suc i * 2 ^ n \<le> unat (mask sz :: 'a word)"
+    by (metis Suc_leI bot_nat_0.extremum_strict div_by_0 i th2 unat_2tp_if unat_div)
+
+  from aligned
+  have p_mask: "p \<le> p + mask sz"
+    by (simp add: is_aligned_no_overflow_mask)
+
+  have less_mask: "2 ^ n + (?i << n) \<le> mask sz"
+    by (metis Suc_i of_nat_Suc of_nat_shiftl shiftl_1 word_of_nat_le word_shiftl_add_distrib)
+
+  have mask_less: "mask n < (2 ^n :: 'a word)"
+    by (simp add: mask_lt_2pn n)
+  hence "mask n + (?i << n) < 2 ^ n + (?i << n)"
+    by (smt (verit, ccfv_SIG) Suc_i add.commute add_right_cancel bot_nat_0.extremum_strict
+                              is_aligned_and_not_zero is_aligned_shift le_unat_uoi mult_Suc
+                              n_less_equal_power_2 of_nat_add of_nat_numeral of_nat_shiftl
+                              olen_add_eqv order_less_le semiring_1_class.of_nat_power
+                              trans_less_add1 unsigned_eq_0_iff word_plus_mono_right)
+  moreover
+  have "p \<le> p + (2 ^ n + (?i << n))"
+    using less_mask p_mask order_less_imp_le word_random
+    by blast
+  ultimately
+  have "p + (mask n + (?i << n)) < p + (2 ^ n + (?i << n))"
+    by (rule word_plus_strict_mono_right)
+  thus ?thesis
+    by (simp add: shiftl_t2n')
+qed
+
+lemma mask_and_neg_mask_compose:
+  "n \<le> sz \<Longrightarrow> (mask sz && ~~mask n) + mask n = mask sz"
+  by (metis diff_add_cancel mask_sub)
+
 end

proof/crefine/RISCV64/ADT_C.thy

@@ -294,21 +294,23 @@ lemma cirqstate_cancel:
 
 definition
   "cint_state_to_H cnode cirqs \<equiv>
-   InterruptState (ptr_val cnode)
-     (\<lambda>i::6 word. if i \<le> maxIRQ then cirqstate_to_H (index cirqs (unat i))
-                else irqstate.IRQInactive)"
+     InterruptState (ptr_val cnode)
+       (\<lambda>i::irq. if i \<le> maxIRQ then cirqstate_to_H (index cirqs (unat i))
+                 else irqstate.IRQInactive)"
 
-lemma cint_rel_to_H:
+end
+
+lemma (in kernel_m) cint_rel_to_H:
   "irqs_masked' s \<Longrightarrow>
    cinterrupt_relation (ksInterruptState s) n t \<Longrightarrow>
    cint_state_to_H n t = (ksInterruptState s)"
   apply (simp add: irqs_masked'_def)
   apply (cases "ksInterruptState s")
   apply (rename_tac "fun")
   apply (clarsimp simp: cinterrupt_relation_def cint_state_to_H_def
-                        maxIRQ_def Kernel_C.maxIRQ_def)
+                        maxIRQ_def Kernel_C_maxIRQ)
   apply (rule ext)
-  apply clarsimp
+  apply (clarsimp split: if_split)
   apply (drule spec, erule impE, assumption)
   apply (drule_tac s="irqstate_to_C (fun i)" in sym,
          simp add: cirqstate_cancel[THEN fun_cong, simplified])
@@ -322,6 +324,8 @@ lemma projectKO_opt_UserData [simp]:
   "projectKO_opt KOUserData = Some UserData"
   by (simp add: projectKO_opts_defs)
 
+context begin interpretation Arch . (*FIXME: arch-split*)
+
 lemma ucast_ucast_mask_pageBits_shift:
   "ucast (ucast (p && mask pageBits >> 3) :: 9 word) = p && mask pageBits >> 3"
   apply (rule word_eqI)

proof/crefine/RISCV64/ArchMove_C.thy

@@ -337,18 +337,6 @@ lemma asid_shiftr_low_bits_less[simplified]:
   apply simp
   done
 
-lemma getActiveIRQ_neq_Some0x3FF':
-  "\<lbrace>\<top>\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>"
-  apply (simp add: getActiveIRQ_def)
-  apply wpsimp
-  done
-
-lemma getActiveIRQ_neq_Some0x3FF:
-  "\<lbrace>\<top>\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>"
-  apply (wpsimp simp: doMachineOp_def split_def)
-  apply (auto dest: use_valid intro: getActiveIRQ_neq_Some0x3FF')
-  done
-
 (* We don't have access to n_msgRegisters from C here, but the number of msg registers in C should
    be equivalent to what we have in the abstract/design specs. We want a number for this definition
    that automatically updates if the number of registers changes, and we sanity check it later