From 99286f3cd4f28d49060dd0652f488161ada62af5 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 1 Sep 2024 18:07:50 +0100 Subject: [PATCH] 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 --- proof/crefine/ARM_HYP/Wellformed_C.thy | 23 +++++++++++++++++++ .../ARM_HYP/ArchInvariants_AI.thy | 18 --------------- 2 files changed, 23 insertions(+), 18 deletions(-) diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy index c5dae8cd44..b65fde118e 100644 --- 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 \cacheLineBits interface\ + +lemma addrFromPPtr_mask_SuperSection: + "n \ pageBitsForSize ARMSuperSection + \ 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 \ pageBitsForSize ARMSuperSection + \ 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 index 175dcedbac..e44be22bd9 100644 --- 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 \ pageBitsForSize ARMSuperSection - \ 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 \ pageBitsForSize ARMSuperSection - \ 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]