adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

ainvs: remove proof method "prove" 

The method is mostly unused and easily replaced by prop_tac.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-12-21 17:13:19 +11:00
parent 8f6373c7ef
commit 1c2f1d84db
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
5 changed files with 22 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
proof/invariant-abstract/ARM/ArchAcc_AI.thy
View File

@ -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 "(\<exists>\<rhd> pa) s")
apply (prop_tac "(\<exists>\<rhd> 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 \<dots> b c
apply (prove "(b \<rhd>1 c) s")
apply (prop_tac "(b \<rhd>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)

16
proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy
View File

@ -376,13 +376,13 @@ lemma pde_at_aligned_vptr: (* ARMHYP *) (* 0x3C \<rightarrow> 0x78?, 24 \<right
split: kernel_object.split_asm
arch_kernel_obj.split_asm if_split_asm
cong: kernel_object.case_cong)
apply (prove "is_aligned x 3")
apply (prop_tac "is_aligned x 3")
subgoal
apply (clarsimp simp: upto_enum_step_def word_shift_by_n[of _ 3, simplified])
by (rule is_aligned_shiftl_self)
apply (simp add: vspace_bits_defs aligned_add_aligned word_bits_conv
is_aligned_shiftl_self)+
apply (prove "pd = (x + (pd + (vptr >> 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 "(\<exists>\<rhd> pa) s")
apply (prop_tac "(\<exists>\<rhd> 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 \<dots> b c
apply (prove "(b \<rhd>1 c) s")
apply (prop_tac "(b \<rhd>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)

1
proof/invariant-abstract/LevityCatch_AI.thy
View File

@ -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

6
proof/refine/ARM/CSpace1_R.thy
View File

@ -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) \<and> cbits \<le> word_bits - cte_level_bits")
apply (prop_tac "is_aligned ptr (cte_level_bits + cbits) \<and> cbits \<le> 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 \<open>to_bl _ = _\<close>[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])

6
proof/refine/ARM_HYP/CSpace1_R.thy
View File

@ -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) \<and> cbits \<le> word_bits - cte_level_bits")
apply (prop_tac "is_aligned ptr (4 + cbits) \<and> cbits \<le> 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 \<open>to_bl _ = _\<close>[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])