arm+arm-hyp crefine: make proof generic in cacheLineBits

Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Sep 24, 2024 · 4d502fe · 4d502fe
1 parent 99286f3
commit 4d502fe
Show file tree

Hide file tree

Showing 15 changed files with 315 additions and 212 deletions.
diff --git a/proof/crefine/ARM/ArchMove_C.thy b/proof/crefine/ARM/ArchMove_C.thy
@@ -233,7 +233,7 @@ crunch insertNewCap, Arch_createNewCaps, threadSet, Arch.createObject, setThread
    simp: unless_def updateObject_default_def crunch_simps
    ignore_del: preemptionPoint)
 
-lemma addrFromPPtr_mask[simplified ARM.pageBitsForSize_simps]:
+lemma addrFromPPtr_mask_ARMSuperSection:
   "n \<le> pageBitsForSize ARMSuperSection
    \<Longrightarrow> addrFromPPtr ptr && mask n = ptr && mask n"
   apply (simp add: addrFromPPtr_def)
@@ -242,13 +242,6 @@ lemma addrFromPPtr_mask[simplified ARM.pageBitsForSize_simps]:
   apply (simp flip: mask_eqs(8))
   done
 
-(* this could be done as
-   lemmas addrFromPPtr_mask_5 = addrFromPPtr_mask[where n=5, simplified]
-   but that wouldn't give a sanity check of the n \<le> ... assumption  disappearing *)
-lemma addrFromPPtr_mask_5:
-  "addrFromPPtr ptr && mask 5 = ptr && mask 5"
-  by (rule addrFromPPtr_mask[where n=5, simplified])
-
 end
 
 end
diff --git a/proof/crefine/ARM/Arch_C.thy b/proof/crefine/ARM/Arch_C.thy
@@ -1598,9 +1598,8 @@ lemma performPageInvocationMapPTE_ccorres:
          apply simp
         apply (subst is_aligned_no_wrap', assumption, fastforce)
         apply (subst add_diff_eq [symmetric], subst is_aligned_no_wrap', assumption, fastforce)
-        apply (simp add:addrFromPPtr_mask_5)
-       apply (clarsimp simp:pte_range_relation_def ptr_add_def ptr_range_to_list_def
-                            addrFromPPtr_mask_5)
+        apply simp
+       apply (clarsimp simp: pte_range_relation_def ptr_add_def ptr_range_to_list_def)
        apply (auto simp: valid_pte_slots'2_def upt_conv_Cons[where i=0])[1]
       apply (clarsimp simp: guard_is_UNIV_def hd_conv_nth last_conv_nth ucast_minus)
       apply (clarsimp simp: pte_range_relation_def ptr_range_to_list_def objBits_simps archObjSize_def)
@@ -1848,19 +1847,19 @@ lemma performPageInvocationMapPDE_ccorres:
        apply (simp add: hd_conv_nth last_conv_nth)
        apply (rule conj_assoc[where Q="a \<le> b" for a b, THEN iffD1])+
        apply (rule conjI)
- (* the inequality first *)
-        apply (clarsimp simp:valid_pde_slots'2_def pdeBits_def
-          objBits_simps archObjSize_def hd_conv_nth)
+        (* the inequality first *)
+        apply (clarsimp simp: valid_pde_slots'2_def pdeBits_def
+                              objBits_simps archObjSize_def hd_conv_nth)
         apply (clarsimp simp:pde_range_relation_def ptr_range_to_list_def ptr_add_def)
         apply (frule is_aligned_addrFromPPtr_n,simp)
         apply (cut_tac n = "sz+2" in  power_not_zero[where 'a="32"])
          apply simp
         apply (subst is_aligned_no_wrap', assumption, fastforce)
         apply (subst add_diff_eq [symmetric])
         apply (subst is_aligned_no_wrap', assumption, fastforce)
-        apply (simp add:addrFromPPtr_mask_5)
+        apply simp
        apply (clarsimp simp: pde_range_relation_def ptr_range_to_list_def CTypesDefs.ptr_add_def
-                             valid_pde_slots'2_def addrFromPPtr_mask_5)
+                             valid_pde_slots'2_def)
        apply (auto simp: upt_conv_Cons[where i=0])[1]
       apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem hd_conv_nth last_conv_nth)
       apply (clarsimp simp: pde_range_relation_def ptr_range_to_list_def pdeBits_def)
@@ -2787,10 +2786,9 @@ lemma decodeARMFrameInvocation_ccorres:
                       erule is_aligned_no_wrap', clarsimp\<close>
             | solves \<open>frule vmsz_aligned_addrFromPPtr(3)[THEN iffD2],
                       (subst mask_add_aligned mask_add_aligned_right, erule is_aligned_weaken,
-                       rule order_trans[OF _ pbfs_atleast_pageBits[simplified pageBits_def]], simp)+,
+                       rule cacheLineBits_leq_pbfs)+,
                       simp\<close>)+)[1] (* 20s *)
      done
-
   (* C side *)
   apply (clarsimp simp: rf_sr_ksCurThread ThreadState_defs mask_eq_iff_w2p
                         word_size word_less_nat_alt from_bool_0 excaps_map_def cte_wp_at_ctes_of)
@@ -3146,13 +3144,12 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
               apply (simp add:linorder_not_le)
               apply (erule word_less_sub_1)
              apply (simp add:mask_add_aligned mask_twice)
-            apply (subgoal_tac "5 \<le> pageBitsForSize a")
-             apply (frule(1) is_aligned_weaken)
-             apply (simp add:mask_add_aligned mask_twice)
-             apply (erule order_trans[rotated])
-             apply (erule flush_range_le1, simp add: linorder_not_le)
-             apply (erule word_less_sub_1)
-            apply (case_tac a,simp+)[1]
+            apply (cut_tac cacheLineBits_leq_pbfs)
+            apply (frule(1) is_aligned_weaken)
+            apply (simp add:mask_add_aligned mask_twice)
+            apply (erule order_trans[rotated])
+            apply (erule flush_range_le1, simp add: linorder_not_le)
+            apply (erule word_less_sub_1)
            apply simp
            apply (vcg exspec=resolveVAddr_modifies)
           apply (rule_tac P'="{s. errstate s = find_ret}"

diff --git a/proof/crefine/ARM/Invoke_C.thy b/proof/crefine/ARM/Invoke_C.thy
@@ -1555,7 +1555,7 @@ lemma clearMemory_untyped_ccorres:
                         word_of_nat_less Kernel_Config.resetChunkBits_def
                         word_bits_def unat_2p_sub_1)
   apply (strengthen is_aligned_no_wrap'[where sz=sz] is_aligned_addrFromPPtr_n)+
-  apply (simp add: addrFromPPtr_mask)
+  apply simp
   apply (cases "ptr = 0")
    apply (drule subsetD, rule intvl_self, simp)
    apply (simp split: if_split_asm)