From 1c2f1d84db73aca727f9dfbdb9ecc3f39001df9d Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 21 Dec 2022 17:13:19 +1100 Subject: [PATCH] ainvs: remove proof method "prove" The method is mostly unused and easily replaced by prop_tac. Signed-off-by: Gerwin Klein --- proof/invariant-abstract/ARM/ArchAcc_AI.thy | 16 ++++++++-------- proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy | 16 ++++++++-------- proof/invariant-abstract/LevityCatch_AI.thy | 1 - proof/refine/ARM/CSpace1_R.thy | 6 +++--- proof/refine/ARM_HYP/CSpace1_R.thy | 6 +++--- 5 files changed, 22 insertions(+), 23 deletions(-) diff --git a/proof/invariant-abstract/ARM/ArchAcc_AI.thy b/proof/invariant-abstract/ARM/ArchAcc_AI.thy index a6f80af24..5a711f8fc 100644 --- a/proof/invariant-abstract/ARM/ArchAcc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchAcc_AI.thy @@ -344,13 +344,13 @@ lemma pde_at_aligned_vptr: split: kernel_object.split_asm arch_kernel_obj.split_asm if_split_asm cong: kernel_object.case_cong) - apply (prove "is_aligned x 2") + apply (prop_tac "is_aligned x 2") subgoal apply (clarsimp simp: upto_enum_step_def word_shift_by_2) by (rule is_aligned_shiftl_self) apply (simp add: aligned_add_aligned word_bits_conv is_aligned_shiftl_self)+ - apply (prove "pd = (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits)") + apply (prop_tac "pd = (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits)") subgoal supply bit_simps[simp del] apply (subst mask_lower_twice[symmetric, where n=6]) @@ -547,7 +547,7 @@ lemma lookup_pt_slot_ptes_aligned_valid: apply (frule (2) valid_vspace_objsD) apply (clarsimp simp: ) subgoal for s _ _ x - apply (prove "page_table_at (ptrFromPAddr x) s") + apply (prop_tac "page_table_at (ptrFromPAddr x) s") subgoal apply (bspec "(ucast (pd + (vptr >> 20 << 2) && mask pd_bits >> 2))";clarsimp) apply (frule kernel_mapping_slots_empty_pdeI) @@ -667,7 +667,7 @@ lemma create_mapping_entries_valid [wp]: apply (clarsimp simp add: valid_mapping_entries_def) apply wp apply (simp add: lookup_pd_slot_def Let_def) - apply (prove "is_aligned pd 14") + apply (prop_tac "is_aligned pd 14") apply (clarsimp simp: obj_at_def add.commute invs_def valid_state_def valid_pspace_def pspace_aligned_def) apply (drule bspec, blast) apply (clarsimp simp: a_type_def split: kernel_object.splits arch_kernel_obj.splits if_split_asm) @@ -1244,14 +1244,14 @@ lemma set_pt_valid_vspace_objs[wp]: apply (clarsimp simp: valid_vspace_objs_def) subgoal for s opt pa rs ao apply (spec pa) - apply (prove "(\\ pa) s") + apply (prop_tac "(\\ pa) s") apply (rule exI[where x=rs]) apply (erule vs_lookupE) apply clarsimp apply (erule vs_lookupI) apply (erule rtrancl.induct, simp) subgoal for \ b c - apply (prove "(b \1 c) s") + apply (prop_tac "(b \1 c) s") apply (thin_tac "_ : rtrancl _")+ apply (clarsimp simp add: vs_lookup1_def obj_at_def vs_refs_def split: if_split_asm) @@ -2096,8 +2096,8 @@ lemma lookup_pt_slot_looks_up [wp]: apply (clarsimp simp: vs_lookup1_def lookup_pd_slot_def Let_def pd_shifting pd_shifting_dual) apply (rule exI, rule conjI, assumption) subgoal for s _ x - apply (prove "ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x") - apply (prove "is_aligned (ptrFromPAddr x) 10") + apply (prop_tac "ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x") + apply (prop_tac "is_aligned (ptrFromPAddr x) 10") apply (drule (2) valid_vspace_objsD) apply clarsimp apply (erule_tac x="ucast (vptr >> 20 << 2 >> 2)" in ballE) diff --git a/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy index e7b944c71..38832e9d7 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy @@ -376,13 +376,13 @@ lemma pde_at_aligned_vptr: (* ARMHYP *) (* 0x3C \ 0x78?, 24 \> pageBits + pt_bits - pte_bits << pde_bits)) && ~~ mask pd_bits)") + apply (prop_tac "pd = (x + (pd + (vptr >> pageBits + pt_bits - pte_bits << pde_bits)) && ~~ mask pd_bits)") subgoal apply (subst mask_lower_twice[symmetric, where n=7]) apply (simp add: pd_bits_def pageBits_def) @@ -561,7 +561,7 @@ lemma lookup_pt_slot_ptes_aligned_valid: (* ARMHYP *) apply (frule (2) valid_vspace_objsD) apply clarsimp subgoal for s _ _ x - apply (prove "page_table_at (ptrFromPAddr x) s") + apply (prop_tac "page_table_at (ptrFromPAddr x) s") subgoal by (spec "(ucast (pd + (vptr >> (pageBits + pt_bits - pte_bits) << pde_bits) && mask pd_bits >> pde_bits))";clarsimp) apply (rule conjI) @@ -702,7 +702,7 @@ lemma create_mapping_entries_valid [wp]: apply (erule (1) page_directory_pde_at_lookupI) apply (wpsimp simp: valid_mapping_entries_def superSectionPDE_offsets_def vspace_bits_defs lookup_pd_slot_def) - apply (prove "is_aligned pd 14") + apply (prop_tac "is_aligned pd 14") apply (clarsimp simp: obj_at_def add.commute invs_def valid_state_def valid_pspace_def pspace_aligned_def) apply (drule bspec, blast) apply (clarsimp simp: a_type_def vspace_bits_defs split: kernel_object.splits arch_kernel_obj.splits if_split_asm) @@ -1340,14 +1340,14 @@ lemma set_pt_valid_vspace_objs[wp]: apply (clarsimp simp: valid_vspace_objs_def) subgoal for s opt pa rs ao apply (spec pa) - apply (prove "(\\ pa) s") + apply (prop_tac "(\\ pa) s") apply (rule exI[where x=rs]) apply (erule vs_lookupE) apply clarsimp apply (erule vs_lookupI) apply (erule rtrancl.induct, simp) subgoal for \ b c - apply (prove "(b \1 c) s") + apply (prop_tac "(b \1 c) s") apply (thin_tac "_ : rtrancl _")+ apply (clarsimp simp add: vs_lookup1_def obj_at_def vs_refs_def split: if_split_asm) @@ -2212,8 +2212,8 @@ lemma lookup_pt_slot_looks_up [wp]: (* ARMHYP *) apply (clarsimp simp: vs_lookup1_def lookup_pd_slot_def Let_def pd_shifting pd_shifting_dual) apply (rule exI, rule conjI, assumption) subgoal for s _ x - apply (prove "ptrFromPAddr x + ((vptr >> 12) && 0x1FF << 3) && ~~ mask pt_bits = ptrFromPAddr x") - apply (prove "is_aligned (ptrFromPAddr x) 12") + apply (prop_tac "ptrFromPAddr x + ((vptr >> 12) && 0x1FF << 3) && ~~ mask pt_bits = ptrFromPAddr x") + apply (prop_tac "is_aligned (ptrFromPAddr x) 12") apply (drule (2) valid_vspace_objsD) apply clarsimp apply (erule_tac x="ucast (vptr >> pageBits + pt_bits - pte_bits << pde_bits >> pde_bits)" in allE) diff --git a/proof/invariant-abstract/LevityCatch_AI.thy b/proof/invariant-abstract/LevityCatch_AI.thy index 44303e073..b0744193e 100644 --- a/proof/invariant-abstract/LevityCatch_AI.thy +++ b/proof/invariant-abstract/LevityCatch_AI.thy @@ -23,7 +23,6 @@ end method spec for x :: "_ :: type" = (erule allE[of _ x]) method bspec for x :: "_ :: type" = (erule ballE[of _ _ x]) -method prove for x :: "prop" = (rule revcut_rl[of "PROP x"]) lemmas aobj_ref_arch_cap_simps[simp] = aobj_ref_arch_cap diff --git a/proof/refine/ARM/CSpace1_R.thy b/proof/refine/ARM/CSpace1_R.thy index 9afc11fd6..3eadbd312 100644 --- a/proof/refine/ARM/CSpace1_R.thy +++ b/proof/refine/ARM/CSpace1_R.thy @@ -609,7 +609,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct) simp: locateSlot_conv) apply (simp add: drop_postfix_eq) apply clarsimp - apply (prove "is_aligned ptr (cte_level_bits + cbits) \ cbits \ word_bits - cte_level_bits") + apply (prop_tac "is_aligned ptr (cte_level_bits + cbits) \ cbits \ word_bits - cte_level_bits") apply (erule valid_CNodeCapE; fastforce simp: cte_level_bits_def) subgoal premises prems for s s' x apply (insert prems) @@ -622,8 +622,8 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct) apply (subst \to_bl _ = _\[symmetric]) apply (drule postfix_dropD) apply clarsimp - apply (prove "32 + (cbits + length guard) - length cref = - (cbits + length guard) + (32 - length cref)") + apply (prop_tac "32 + (cbits + length guard) - length cref = + (cbits + length guard) + (32 - length cref)") apply (drule len_drop_lemma, simp, arith) apply simp apply (subst drop_drop [symmetric]) diff --git a/proof/refine/ARM_HYP/CSpace1_R.thy b/proof/refine/ARM_HYP/CSpace1_R.thy index 6ded3048f..ed35a6609 100644 --- a/proof/refine/ARM_HYP/CSpace1_R.thy +++ b/proof/refine/ARM_HYP/CSpace1_R.thy @@ -612,7 +612,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct) simp: locateSlot_conv) apply (simp add: drop_postfix_eq) apply clarsimp - apply (prove "is_aligned ptr (4 + cbits) \ cbits \ word_bits - cte_level_bits") + apply (prop_tac "is_aligned ptr (4 + cbits) \ cbits \ word_bits - cte_level_bits") apply (erule valid_CNodeCapE; fastforce simp: cte_level_bits_def) subgoal premises prems for s s' x apply (insert prems) @@ -625,8 +625,8 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct) apply (subst \to_bl _ = _\[symmetric]) apply (drule postfix_dropD) apply clarsimp - apply (prove "32 + (cbits + length guard) - length cref = - (cbits + length guard) + (32 - length cref)") + apply (prop_tac "32 + (cbits + length guard) - length cref = + (cbits + length guard) + (32 - length cref)") apply (drule len_drop_lemma, simp, arith) apply simp apply (subst drop_drop [symmetric])