arm-hyp ainvs+crefine: move masking lemmas for cacheLineBits

addrFromPPtr_mask and ptrFromPAddr_mask are only needed for masking with cacheLineBits in CRefine. Move to CRefine where the rest of the cacheLineBits infrastructure is. Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Sep 24, 2024 · 99286f3 · 99286f3
1 parent 9bcac41
commit 99286f3
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 18 deletions.
diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy
@@ -529,6 +529,29 @@ lemma ucast_irq_array_guard[unfolded irq_array_size_val, simplified]:
   apply simp
   done
 
+
+text \<open>cacheLineBits interface\<close>
+
+lemma addrFromPPtr_mask_SuperSection:
+  "n \<le> pageBitsForSize ARMSuperSection
+   \<Longrightarrow> addrFromPPtr ptr && mask n = ptr && mask n"
+  apply (simp add: addrFromPPtr_def)
+  apply (prop_tac "pptrBaseOffset AND mask n = 0")
+   apply (rule mask_zero[OF is_aligned_weaken[OF pptrBaseOffset_aligned]], simp)
+  apply (simp flip: mask_eqs(8))
+  done
+
+lemma ptrFromPAddr_mask_SuperSection:
+  "n \<le> pageBitsForSize ARMSuperSection
+   \<Longrightarrow> ptrFromPAddr ptr && mask n = ptr && mask n"
+  apply (simp add: ptrFromPAddr_def)
+  apply (prop_tac "pptrBaseOffset AND mask n = 0")
+   apply (rule mask_zero[OF is_aligned_weaken[OF pptrBaseOffset_aligned]], simp)
+  apply (simp flip: mask_eqs(7))
+  done
+
+(* ------------ *)
+
 (* Input abbreviations for API object types *)
 (* disambiguates names *)
 

diff --git a/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
@@ -2624,24 +2624,6 @@ lemma is_aligned_ptrFromPAddrD[simplified pageBitsForSize_simps]:
   by (simp add: ptrFromPAddr_def)
      (erule is_aligned_addD2, erule is_aligned_weaken[OF pptrBaseOffset_aligned])
 
-lemma addrFromPPtr_mask[simplified ARM_HYP.pageBitsForSize_simps]:
-  "n \<le> pageBitsForSize ARMSuperSection
-   \<Longrightarrow> addrFromPPtr ptr && mask n = ptr && mask n"
-  apply (simp add: addrFromPPtr_def)
-  apply (prop_tac "pptrBaseOffset AND mask n = 0")
-   apply (rule mask_zero[OF is_aligned_weaken[OF pptrBaseOffset_aligned]], simp)
-  apply (simp flip: mask_eqs(8))
-  done
-
-lemma ptrFromPAddr_mask[simplified ARM_HYP.pageBitsForSize_simps]:
-  "n \<le> pageBitsForSize ARMSuperSection
-   \<Longrightarrow> ptrFromPAddr ptr && mask n = ptr && mask n"
-  apply (simp add: ptrFromPAddr_def)
-  apply (prop_tac "pptrBaseOffset AND mask n = 0")
-   apply (rule mask_zero[OF is_aligned_weaken[OF pptrBaseOffset_aligned]], simp)
-  apply (simp flip: mask_eqs(7))
-  done
-
 end
 
 declare ARM_HYP.arch_tcb_context_absorbs[simp]