arm-hyp crefine: VCPUReg_VMPIDR updates

Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Feb 26, 2024 · dcc6055 · dcc6055
1 parent 12c6edf
commit dcc6055
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 3 deletions.
diff --git a/proof/crefine/ARM_HYP/ArchMove_C.thy b/proof/crefine/ARM_HYP/ArchMove_C.thy
@@ -139,7 +139,7 @@ lemma addToBitmap_sets_L1Bitmap_same_dom:
        \<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrace>"
   unfolding addToBitmap_def bitmap_fun_defs
   apply wpsimp
-  by (metis nth_0 of_nat_numeral prioToL1Index_bit_set word_neq_0_conv word_or_zero)
+  by (metis nth_0 prioToL1Index_bit_set word_or_zero)
 
 context begin interpretation Arch .
 
@@ -457,8 +457,9 @@ crunch pred_tcb_at'[wp]: readVCPUReg "\<lambda>s. P (pred_tcb_at' a b p s)"
 
 crunch ksCurThread[wp]: readVCPUReg "\<lambda>s. P (ksCurThread s)"
 
+(* schematic_goal leads to Suc (Suc ..) form only *)
 lemma fromEnum_maxBound_vcpureg_def:
-  "fromEnum (maxBound :: vcpureg) = 41"
+  "fromEnum (maxBound :: vcpureg) = 42"
   by (clarsimp simp: fromEnum_def maxBound_def enum_vcpureg)
 
 lemma unat_of_nat_mword_fromEnum_vcpureg[simp]:

diff --git a/proof/crefine/ARM_HYP/SR_lemmas_C.thy b/proof/crefine/ARM_HYP/SR_lemmas_C.thy
@@ -2324,6 +2324,7 @@ lemmas seL4_VCPUReg_defs =
     seL4_VCPUReg_R10fiq_def
     seL4_VCPUReg_R11fiq_def
     seL4_VCPUReg_R12fiq_def
+    seL4_VCPUReg_VMPIDR_def
     seL4_VCPUReg_SPSRsvc_def
     seL4_VCPUReg_SPSRabt_def
     seL4_VCPUReg_SPSRund_def

diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy
@@ -42,8 +42,9 @@ abbreviation
   pt_Ptr :: "32 word \<Rightarrow> (pte_C[512]) ptr" where "pt_Ptr == Ptr"
 abbreviation
   pd_Ptr :: "32 word \<Rightarrow> (pde_C[2048]) ptr" where "pd_Ptr == Ptr"
+type_synonym vcpu_regs_array_len = 43
 abbreviation
-  regs_C_Ptr :: "addr \<Rightarrow> (machine_word_len word[42]) ptr" where "regs_C_Ptr \<equiv> Ptr"
+  regs_C_Ptr :: "addr \<Rightarrow> (machine_word_len word[vcpu_regs_array_len]) ptr" where"regs_C_Ptr \<equiv> Ptr"
 abbreviation
   vgic_lr_C_Ptr :: "addr \<Rightarrow> (virq_C[64]) ptr" where "vgic_lr_C_Ptr \<equiv> Ptr"
 abbreviation
@@ -54,6 +55,11 @@ abbreviation
 abbreviation
   word_Ptr :: "addr \<Rightarrow> machine_word ptr" where "word_Ptr \<equiv> Ptr"
 
+(* Avoid repeated str representation computation for VCPU reg array type in typ_heap_simps *)
+schematic_goal nat_to_bin_string_vcpu_regs[simp]:
+  "nat_to_bin_string LENGTH(vcpu_regs_array_len) = ?str"
+  by (simp add: ntbs)
+
 lemma halt_spec:
   "Gamma \<turnstile> {} Call halt_'proc {}"
   apply (rule hoare_complete)