make proofs generic in cacheLineBits

lib/Word_Lib/Word_Lemmas_Internal.thy

@@ -933,6 +933,11 @@ lemma shiftr_not_max_word:
   "0 < n \<Longrightarrow> w >> n \<noteq> max_word"
   by (metis and_mask_eq_iff_shiftr_0 and_mask_not_max_word diff_less len_gt_0 shiftr_le_0 word_shiftr_lt)
 
+lemma shiftr_less_max_mask:
+  "0 < n \<Longrightarrow> x >> n < mask LENGTH('a)" for x :: "'a::len word"
+  using not_max_word_iff_less shiftr_not_max_word
+  by auto
+
 lemma word_sandwich1:
   fixes a b c :: "'a::len word"
   assumes "a < b"

proof/crefine/AARCH64/Arch_C.thy

@@ -92,7 +92,7 @@ lemma clearMemory_PT_setObject_PTE_ccorres:
    apply (clarsimp simp: guard_is_UNIV_def bit_simps split: if_split)
   apply clarsimp
   apply (frule is_aligned_addrFromPPtr_n, simp)
-  apply (simp add: is_aligned_no_overflow' addrFromPPtr_mask_cacheLineSize)
+  apply (simp add: is_aligned_no_overflow' addrFromPPtr_mask_cacheLineBits)
   apply (rule conjI)
    apply (simp add: unat_mask_eq flip: mask_2pm1)
    apply (simp add: mask_eq_exp_minus_1)
@@ -1604,7 +1604,7 @@ definition flushtype_relation :: "flush_type \<Rightarrow> machine_word \<Righta
        label \<in> scast ` {Kernel_C.ARMPageUnify_Instruction, Kernel_C.ARMVSpaceUnify_Instruction}"
 
 lemma doFlush_ccorres:
-  "ccorres dc xfdc (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask cacheLineSize = ps && mask cacheLineSize
+  "ccorres dc xfdc (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask cacheLineBits = ps && mask cacheLineBits
         \<and> ptrFromPAddr ps \<le> ptrFromPAddr ps + (ve - vs)
         \<and> unat (ve - vs) \<le> gsMaxObjectSize s)
      (\<lbrace>flushtype_relation t \<acute>invLabel\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>) []

proof/crefine/AARCH64/Invoke_C.thy

@@ -1685,7 +1685,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_cacheLineSize pptrBaseOffset_alignment_def)
+  apply (simp add: addrFromPPtr_mask_cacheLineBits pptrBaseOffset_alignment_def)
   apply (cases "ptr = 0"; simp)
   apply (drule subsetD, rule intvl_self, simp)
   apply simp

proof/crefine/AARCH64/Machine_C.thy

@@ -156,7 +156,7 @@ assumes cleanByVA_PoU_ccorres:
 
 assumes cleanCacheRange_RAM_ccorres:
   "ccorres dc xfdc (\<lambda>s. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)
-                        \<and> w1 && mask cacheLineSize  = w3 && mask cacheLineSize
+                        \<and> w1 && mask cacheLineBits  = w3 && mask cacheLineBits
                         \<and> unat (w2 - w1) \<le> gsMaxObjectSize s)
                    (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) []
            (doMachineOp (cleanCacheRange_RAM w1 w2 w3))
@@ -165,30 +165,30 @@ assumes cleanCacheRange_RAM_ccorres:
 assumes cleanCacheRange_PoU_ccorres:
   "ccorres dc xfdc (\<lambda>s. unat (w2 - w1) \<le> gsMaxObjectSize s
                         \<and> w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)
-                        \<and> w1 && mask cacheLineSize = w3 && mask cacheLineSize)
+                        \<and> w1 && mask cacheLineBits = w3 && mask cacheLineBits)
                    (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) []
            (doMachineOp (cleanCacheRange_PoU w1 w2 w3))
            (Call cleanCacheRange_PoU_'proc)"
 
 assumes cleanInvalidateCacheRange_RAM_ccorres:
   "ccorres dc xfdc (\<lambda>s. unat (w2 - w1) \<le> gsMaxObjectSize s
                         \<and> w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)
-                        \<and> w1 && mask cacheLineSize = w3 && mask cacheLineSize)
+                        \<and> w1 && mask cacheLineBits = w3 && mask cacheLineBits)
                    (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) []
            (doMachineOp (cleanInvalidateCacheRange_RAM w1 w2 w3))
            (Call cleanInvalidateCacheRange_RAM_'proc)"
 
 assumes invalidateCacheRange_RAM_ccorres:
   "ccorres dc xfdc ((\<lambda>s. unat (w2 - w1) \<le> gsMaxObjectSize s)
                     and (\<lambda>_. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)
-                      \<and> w1 && mask cacheLineSize = w3 && mask cacheLineSize))
+                      \<and> w1 && mask cacheLineBits = w3 && mask cacheLineBits))
                    (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) []
            (doMachineOp (invalidateCacheRange_RAM w1 w2 w3))
            (Call invalidateCacheRange_RAM_'proc)"
 
 assumes invalidateCacheRange_I_ccorres:
   "ccorres dc xfdc (\<lambda>_. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)
-                        \<and> w1 && mask cacheLineSize = w3 && mask cacheLineSize)
+                        \<and> w1 && mask cacheLineBits = w3 && mask cacheLineBits)
                    (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) []
            (doMachineOp (invalidateCacheRange_I w1 w2 w3))
            (Call invalidateCacheRange_I_'proc)"

proof/crefine/AARCH64/Recycle_C.thy

@@ -387,13 +387,7 @@ lemma clearMemory_PageCap_ccorres:
                         capAligned_def word_of_nat_less)
   apply (frule is_aligned_addrFromPPtr_n, simp add: pageBitsForSize_def split: vmpage_size.splits)
   apply (simp add: bit_simps pptrBaseOffset_alignment_def)+
-  apply (simp add: is_aligned_no_overflow')
-  apply (rule conjI)
-  subgoal
-    apply (prop_tac "cacheLineSize \<le> pageBitsForSize sz")
-     apply (simp add: pageBitsForSize_def bit_simps cacheLineSize_def split: vmpage_size.splits)
-    apply (simp add: is_aligned_mask[THEN iffD1] is_aligned_weaken)
-    done
+  apply (simp add: is_aligned_no_overflow' addrFromPPtr_mask_cacheLineBits)
   apply (simp add: pageBitsForSize_def bit_simps split: vmpage_size.splits)
   done
 

proof/crefine/AARCH64/Wellformed_C.thy

@@ -562,6 +562,50 @@ lemma ucast_irq_array_guard[unfolded irq_array_size_val, simplified]:
   done
 
 
+text \<open>cacheLineBits interface\<close>
+
+lemmas cacheLineBits_val =
+  cacheLineBits_def[unfolded Kernel_Config.CONFIG_L1_CACHE_LINE_SIZE_BITS_def]
+
+lemma cacheLineBits_leq_pageBits:
+  "cacheLineBits \<le> pageBits"
+  using cacheLineBits_sanity
+  by (simp add: pageBits_def)
+
+lemma pageBits_leq_pptrBaseOffset_alignment:
+  "pageBits \<le> pptrBaseOffset_alignment"
+  by (simp add: pageBits_def pptrBaseOffset_alignment_def)
+
+lemma cacheLineBits_leq_pptrBaseOffset_alignment:
+  "cacheLineBits \<le> pptrBaseOffset_alignment"
+  by (rule order.trans, rule cacheLineBits_leq_pageBits, rule pageBits_leq_pptrBaseOffset_alignment)
+
+lemma cacheLineBits_leq_pbfs:
+  "cacheLineBits \<le> pageBitsForSize sz"
+  by (rule order.trans, rule cacheLineBits_leq_pageBits, rule pbfs_atleast_pageBits)
+
+lemma addrFromPPtr_mask_pptrBaseOffset_alignment:
+  "n \<le> pptrBaseOffset_alignment
+   \<Longrightarrow> addrFromPPtr ptr && mask n = ptr && mask n"
+  unfolding addrFromPPtr_def
+  by (metis is_aligned_weaken mask_add_aligned pptrBaseOffset_aligned zadd_diff_inverse)
+
+lemma addrFromPPtr_mask_cacheLineBits:
+  "addrFromPPtr ptr && mask cacheLineBits = ptr && mask cacheLineBits"
+  by (rule addrFromPPtr_mask_pptrBaseOffset_alignment,
+      rule cacheLineBits_leq_pptrBaseOffset_alignment)
+
+lemma pptrBaseOffset_cacheLineBits_aligned[simp]:
+  "pptrBaseOffset && mask cacheLineBits = 0"
+  unfolding is_aligned_mask[symmetric]
+  by (rule is_aligned_weaken[OF pptrBaseOffset_aligned cacheLineBits_leq_pptrBaseOffset_alignment])
+
+lemma ptrFromPAddr_mask_cacheLineBits[simp]:
+  "ptrFromPAddr v && mask cacheLineBits = v && mask cacheLineBits"
+  by (simp add: ptrFromPAddr_def add_mask_ignore)
+
+(* end of Kernel_Config interface section *)
+
 (* Input abbreviations for API object types *)
 (* disambiguates names *)
 
@@ -645,26 +689,6 @@ abbreviation(input)
 where
   "prioInvalid == seL4_InvalidPrio"
 
-(* caches *)
-
-definition cacheLineSize :: nat where
-  "cacheLineSize \<equiv> 6"
-
-lemma addrFromPPtr_mask_cacheLineSize:
-  "addrFromPPtr ptr && mask cacheLineSize = ptr && mask cacheLineSize"
-  apply (simp add: addrFromPPtr_def AARCH64.pptrBase_def pptrBaseOffset_def canonical_bit_def
-                   paddrBase_def cacheLineSize_def mask_def)
-  apply word_bitwise
-  done
-
-lemma pptrBaseOffset_cacheLineSize_aligned[simp]:
-  "pptrBaseOffset && mask cacheLineSize = 0"
-  by (simp add: pptrBaseOffset_def paddrBase_def pptrBase_def cacheLineSize_def mask_def)
-
-lemma ptrFromPAddr_mask_cacheLineSize[simp]:
-  "ptrFromPAddr v && mask cacheLineSize = v && mask cacheLineSize"
-  by (simp add: ptrFromPAddr_def add_mask_ignore)
-
 (* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
 lemma ThreadState_Restart_mask[simp]:
   "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"

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

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}"

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)