diff --git a/proof/crefine/AARCH64/Arch_C.thy b/proof/crefine/AARCH64/Arch_C.thy index e3481189f9..8b7b1c02da 100644 --- a/proof/crefine/AARCH64/Arch_C.thy +++ 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 \ machine_word \ scast ` {Kernel_C.ARMPageUnify_Instruction, Kernel_C.ARMVSpaceUnify_Instruction}" lemma doFlush_ccorres: - "ccorres dc xfdc (\s. vs \ ve \ ps \ ps + (ve - vs) \ vs && mask cacheLineSize = ps && mask cacheLineSize + "ccorres dc xfdc (\s. vs \ ve \ ps \ ps + (ve - vs) \ vs && mask cacheLineBits = ps && mask cacheLineBits \ ptrFromPAddr ps \ ptrFromPAddr ps + (ve - vs) \ unat (ve - vs) \ gsMaxObjectSize s) (\flushtype_relation t \invLabel\ \ \\start = vs\ \ \\end = ve\ \ \\pstart = ps\) [] diff --git a/proof/crefine/AARCH64/Invoke_C.thy b/proof/crefine/AARCH64/Invoke_C.thy index e74e29273c..c688ea43f9 100644 --- a/proof/crefine/AARCH64/Invoke_C.thy +++ b/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 diff --git a/proof/crefine/AARCH64/Machine_C.thy b/proof/crefine/AARCH64/Machine_C.thy index 1e02ad82ad..f741dc55f6 100644 --- a/proof/crefine/AARCH64/Machine_C.thy +++ b/proof/crefine/AARCH64/Machine_C.thy @@ -156,7 +156,7 @@ assumes cleanByVA_PoU_ccorres: assumes cleanCacheRange_RAM_ccorres: "ccorres dc xfdc (\s. w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask cacheLineSize = w3 && mask cacheLineSize + \ w1 && mask cacheLineBits = w3 && mask cacheLineBits \ unat (w2 - w1) \ gsMaxObjectSize s) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (cleanCacheRange_RAM w1 w2 w3)) @@ -165,7 +165,7 @@ assumes cleanCacheRange_RAM_ccorres: assumes cleanCacheRange_PoU_ccorres: "ccorres dc xfdc (\s. unat (w2 - w1) \ gsMaxObjectSize s \ w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask cacheLineSize = w3 && mask cacheLineSize) + \ w1 && mask cacheLineBits = w3 && mask cacheLineBits) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (cleanCacheRange_PoU w1 w2 w3)) (Call cleanCacheRange_PoU_'proc)" @@ -173,7 +173,7 @@ assumes cleanCacheRange_PoU_ccorres: assumes cleanInvalidateCacheRange_RAM_ccorres: "ccorres dc xfdc (\s. unat (w2 - w1) \ gsMaxObjectSize s \ w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask cacheLineSize = w3 && mask cacheLineSize) + \ w1 && mask cacheLineBits = w3 && mask cacheLineBits) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (cleanInvalidateCacheRange_RAM w1 w2 w3)) (Call cleanInvalidateCacheRange_RAM_'proc)" @@ -181,14 +181,14 @@ assumes cleanInvalidateCacheRange_RAM_ccorres: assumes invalidateCacheRange_RAM_ccorres: "ccorres dc xfdc ((\s. unat (w2 - w1) \ gsMaxObjectSize s) and (\_. w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask cacheLineSize = w3 && mask cacheLineSize)) + \ w1 && mask cacheLineBits = w3 && mask cacheLineBits)) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (invalidateCacheRange_RAM w1 w2 w3)) (Call invalidateCacheRange_RAM_'proc)" assumes invalidateCacheRange_I_ccorres: "ccorres dc xfdc (\_. w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask cacheLineSize = w3 && mask cacheLineSize) + \ w1 && mask cacheLineBits = w3 && mask cacheLineBits) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (invalidateCacheRange_I w1 w2 w3)) (Call invalidateCacheRange_I_'proc)" diff --git a/proof/crefine/AARCH64/Recycle_C.thy b/proof/crefine/AARCH64/Recycle_C.thy index 98055bab5b..d2fbd95eb2 100644 --- a/proof/crefine/AARCH64/Recycle_C.thy +++ b/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 \ 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 diff --git a/proof/crefine/AARCH64/Wellformed_C.thy b/proof/crefine/AARCH64/Wellformed_C.thy index 76e236b963..53c9fa726d 100644 --- a/proof/crefine/AARCH64/Wellformed_C.thy +++ b/proof/crefine/AARCH64/Wellformed_C.thy @@ -562,6 +562,50 @@ lemma ucast_irq_array_guard[unfolded irq_array_size_val, simplified]: done +text \cacheLineBits interface\ + +lemmas cacheLineBits_val = + cacheLineBits_def[unfolded Kernel_Config.CONFIG_L1_CACHE_LINE_SIZE_BITS_def] + +lemma cacheLineBits_leq_pageBits: + "cacheLineBits \ pageBits" + using cacheLineBits_sanity + by (simp add: pageBits_def) + +lemma pageBits_leq_pptrBaseOffset_alignment: + "pageBits \ pptrBaseOffset_alignment" + by (simp add: pageBits_def pptrBaseOffset_alignment_def) + +lemma cacheLineBits_leq_pptrBaseOffset_alignment: + "cacheLineBits \ pptrBaseOffset_alignment" + by (rule order.trans, rule cacheLineBits_leq_pageBits, rule pageBits_leq_pptrBaseOffset_alignment) + +lemma cacheLineBits_leq_pbfs: + "cacheLineBits \ pageBitsForSize sz" + by (rule order.trans, rule cacheLineBits_leq_pageBits, rule pbfs_atleast_pageBits) + +lemma addrFromPPtr_mask_pptrBaseOffset_alignment: + "n \ pptrBaseOffset_alignment + \ 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) + +(* ----- *) + (* Input abbreviations for API object types *) (* disambiguates names *) @@ -645,26 +689,6 @@ abbreviation(input) where "prioInvalid == seL4_InvalidPrio" -(* caches *) - -definition cacheLineSize :: nat where - "cacheLineSize \ 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"