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

Remove valid_arch_objs 

now that we have valid_vspace_objs to express validiy of
vspace objects, we do not need valid_arch_objs: we have
valid_objs to state the validity of non-vspace arch objects.
This commit is contained in:
Miki Tanaka 2017-07-19 22:59:59 +10:00
parent dbd888ad3e
commit 6d8e917087
43 changed files with 223 additions and 951 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
proof/infoflow/Arch_IF.thy
View File

@ -2354,10 +2354,10 @@ lemma valid_arch_arm_asid_table_unmap:
crunch valid_arch_state[wp]: load_hw_asid "valid_arch_state"
lemma valid_arch_objs_arm_asid_table_unmap:
"valid_arch_objs s
"valid_vspace_objs s
\<and> tab = arm_asid_table (arch_state s)
\<longrightarrow> valid_arch_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)"
apply (clarsimp simp: valid_state_def valid_arch_objs_unmap_strg)
\<longrightarrow> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)"
apply (clarsimp simp: valid_state_def valid_vspace_objs_unmap_strg)
done
lemma valid_vspace_objs_arm_asid_table_unmap:
@ -2367,16 +2367,13 @@ lemma valid_vspace_objs_arm_asid_table_unmap:
apply (clarsimp simp: valid_state_def valid_vspace_objs_unmap_strg)
done
crunch valid_arch_objs[wp]: set_vm_root "valid_arch_objs"
crunch valid_arch_objs[wp]: invalidate_asid_entry "valid_arch_objs"
crunch valid_arch_objs[wp]: flush_space "valid_arch_objs"
crunch valid_vspace_objs[wp]: set_vm_root "valid_vspace_objs"
crunch valid_vspace_objs[wp]: invalidate_asid_entry "valid_vspace_objs"
crunch valid_vspace_objs[wp]: flush_space "valid_vspace_objs"
lemma invalidate_hw_asid_vspace_objs [wp]:
"\<lbrace>valid_vspace_objs\<rbrace> invalidate_hw_asid_entry asid \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
apply (wpsimp simp: invalidate_hw_asid_entry_def valid_vspace_objs_arch_update)+
apply assumption
apply wpsimp+
done
by (wpsimp simp: invalidate_hw_asid_entry_def valid_vspace_objs_arch_update)+
crunch vspace_objs[wp]: invalidate_asid valid_vspace_objs
(simp: valid_vspace_objs_arch_update)
@ -2399,12 +2396,12 @@ crunch valid_vspace_objs[wp]: invalidate_asid_entry "valid_vspace_objs"
crunch valid_vspace_objs[wp]: flush_space "valid_vspace_objs"
lemma delete_asid_pool_valid_arch_obsj[wp]:
"\<lbrace>valid_arch_objs\<rbrace>
"\<lbrace>valid_vspace_objs\<rbrace>
delete_asid_pool base pptr
\<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
\<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
unfolding delete_asid_pool_def
apply (wp modify_wp)
apply (strengthen valid_arch_objs_arm_asid_table_unmap)
apply (strengthen valid_vspace_objs_arm_asid_table_unmap)
apply (wpsimp wp: mapM_wp')+
done
@ -2432,10 +2429,10 @@ crunch valid_vspace_objs[wp]: empty_slot "valid_arch_objs"
(wp: crunch_wps simp: crunch_simps ignore: )
*)
lemma set_asid_pool_arch_objs_unmap'':
"\<lbrace>(valid_arch_objs and ko_at (ArchObj (ASIDPool ap)) p) and K(f = (ap |` S))\<rbrace> set_asid_pool p f \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
"\<lbrace>(valid_vspace_objs and ko_at (ArchObj (ASIDPool ap)) p) and K(f = (ap |` S))\<rbrace> set_asid_pool p f \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
apply (rule hoare_gen_asm)
apply simp
apply (rule set_asid_pool_arch_objs_unmap)
apply (rule set_asid_pool_vspace_objs_unmap)
done
lemma set_asid_pool_vspace_objs_unmap'':
@ -2448,7 +2445,7 @@ lemma set_asid_pool_vspace_objs_unmap'':
lemma restrict_eq_asn_none: "f(N := None) = f |` {s. s \<noteq> N}" by auto
lemma delete_asid_valid_arch_objs[wp]:
"\<lbrace>valid_arch_objs and pspace_aligned\<rbrace> delete_asid a b \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
"\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> delete_asid a b \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
unfolding delete_asid_def
apply (wpsimp wp: set_asid_pool_arch_objs_unmap'')
apply (fastforce simp: restrict_eq_asn_none)

4
proof/infoflow/Example_Valid_State.thy
View File

@ -1574,8 +1574,8 @@ lemma valid_machine_state_s0[simp]:
done
lemma valid_arch_objs_s0[simp]:
"valid_arch_objs s0_internal"
apply (clarsimp simp: valid_arch_objs_def obj_at_def s0_internal_def)
"valid_vspace_objs s0_internal"
apply (clarsimp simp: valid_vspace_objs_def obj_at_def s0_internal_def)
apply (drule kh0_SomeD)
apply (erule disjE | clarsimp simp: pageBits_def addrFromPPtr_def
physMappingOffset_def kernelBase_addr_def physBase_def is_aligned_def

25
proof/infoflow/UserOp_IF.thy
View File

@ -374,13 +374,6 @@ lemma requiv_ptable_xn_eq:
\<Longrightarrow> ptable_xn_s s x = ptable_xn_s s' x"
by (simp add: ptable_xn_s_def requiv_ptable_attrs_eq)
lemma valid_arch_objsD2:
"\<lbrakk>(\<exists>\<rhd> p) s; ko_at (ArchObj ao) p s;
valid_arch_objs s\<rbrakk>
\<Longrightarrow> valid_arch_obj ao s"
by (clarsimp simp: valid_arch_objsD)
lemma mask_shift_le:
"z \<le> y \<Longrightarrow> (x::'a:: len word) && ~~ mask z >> y = x >> y"
proof -
@ -584,7 +577,7 @@ lemma ptable_lift_data_consistant:
apply (rule bang_big[simplified])
apply (simp add: word_size)
apply (frule(1) valid_pdpt_align_ptD[OF _ vpdpt])
apply (simp add: valid_arch_obj_def)
apply (simp add: )
apply (drule_tac x = "(ucast ((x >> 12) && mask 8))" in spec)
apply (frule data_at_same_size[where sz = sz and sz' = ARMLargePage,rotated,simplified],
clarsimp+)
@ -606,7 +599,7 @@ lemma ptable_lift_data_consistant:
apply (rule bang_big[simplified])
apply (simp add: word_size)
apply (frule(1) valid_pdpt_align_ptD[OF _ vpdpt])
apply (simp add: valid_arch_obj_def)
apply (simp add: )
apply (drule_tac x = "(ucast ((x >> 12) && mask 8))" in spec)
apply (frule data_at_same_size[where sz = sz and sz' = ARMSmallPage,rotated,simplified],
clarsimp+)
@ -620,7 +613,7 @@ lemma ptable_lift_data_consistant:
apply (rename_tac pd_base vmattr mw pd caprights)
apply (cut_tac get_pd_of_thread_reachable[OF misc(1)])
apply (frule(1) valid_vspace_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add: valid_arch_obj_def)
apply (simp add: )
apply (drule bspec)
apply (rule Compl_iff[THEN iffD2])
apply (rule kernel_mappings_kernel_mapping_slots[OF misc(2)])
@ -638,7 +631,7 @@ lemma ptable_lift_data_consistant:
apply (rename_tac pd_base vmattr rights pd)
apply (cut_tac get_pd_of_thread_reachable[OF misc(1)])
apply (frule(1) valid_vspace_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add: valid_arch_obj_def)
apply (simp add: )
apply (drule bspec)
apply (rule Compl_iff[THEN iffD2])
apply (rule kernel_mappings_kernel_mapping_slots[OF misc(2)])
@ -695,7 +688,7 @@ lemma ptable_rights_data_consistant:
apply (rename_tac pd_base vmattr mw pd pt)
apply (cut_tac get_pd_of_thread_reachable[OF misc(1)])
apply (frule(1) valid_vspace_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add: valid_arch_obj_def)
apply (simp add: )
apply (drule bspec)
apply (rule Compl_iff[THEN iffD2])
apply (rule kernel_mappings_kernel_mapping_slots[OF misc(2)])
@ -715,7 +708,7 @@ lemma ptable_rights_data_consistant:
apply (rule bang_big[simplified])
apply (simp add: word_size)
apply (frule(1) valid_pdpt_align_ptD[OF _ vpdpt])
apply (simp add: valid_arch_obj_def)
apply (simp add: )
apply (drule_tac x = "(ucast ((x >> 12) && mask 8))" in spec)
apply (frule data_at_same_size[where sz = sz and sz' = ARMLargePage,rotated,simplified],
clarsimp+)
@ -736,7 +729,7 @@ lemma ptable_rights_data_consistant:
apply (rule bang_big[simplified])
apply (simp add: word_size)
apply (frule(1) valid_pdpt_align_ptD[OF _ vpdpt])
apply (simp add: valid_arch_obj_def)
apply (simp add: )
apply (drule_tac x = "(ucast ((x >> 12) && mask 8))" in spec)
apply (frule data_at_same_size[where sz = sz and sz' = ARMSmallPage,rotated,simplified],
clarsimp+)
@ -750,7 +743,7 @@ lemma ptable_rights_data_consistant:
apply (rename_tac pd_base vmattr mw pd caprights)
apply (cut_tac get_pd_of_thread_reachable[OF misc(1)])
apply (frule(1) valid_vspace_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add: valid_arch_obj_def)
apply (simp add: )
apply (drule bspec)
apply (rule Compl_iff[THEN iffD2])
apply (rule kernel_mappings_kernel_mapping_slots[OF misc(2)])
@ -765,7 +758,7 @@ lemma ptable_rights_data_consistant:
apply (rename_tac pd_base vmattr rights pd)
apply (cut_tac get_pd_of_thread_reachable[OF misc(1)])
apply (frule(1) valid_vspace_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add: valid_arch_obj_def)
apply (simp add: )
apply (drule bspec)
apply (rule Compl_iff[THEN iffD2])
apply (rule kernel_mappings_kernel_mapping_slots[OF misc(2)])

2
proof/invariant-abstract/ARM/ArchAInvsPre.thy
View File

@ -153,7 +153,7 @@ lemma some_get_page_info_umapsD:
apply (case_tac ao, simp_all add: a_type_simps obj_at_def )[1]
apply (simp add: get_pt_info_def get_pt_entry_def)
apply (drule_tac x="(ucast ((p >> 12) && mask 8))" in spec)
apply (clarsimp simp: obj_at_def valid_arch_obj_def
apply (clarsimp simp: obj_at_def
split: pte.splits,intro exI conjI,simp_all)[1]
apply (frule obj_bits_data_at)
apply (clarsimp simp: pspace_aligned_def data_at_def)

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

@ -996,15 +996,6 @@ crunch interrupt_states[wp]: set_pd "\<lambda>s. P (interrupt_states s)"
(wp: crunch_wps)
lemma set_pd_arch_objs_unmap:
"\<lbrace>valid_arch_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (PageDirectory pd') s) and
obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd')) \<subseteq> vs_refs ko) p\<rbrace>
set_pd p pd' \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (simp add: set_pd_def)
apply (wp set_object_arch_objs get_object_wp)
including unfold_objects
by (fastforce simp: a_type_def)
lemma set_pd_vspace_objs_unmap:
"\<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd') s) and
obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd')) \<subseteq> vs_refs ko) p\<rbrace>
@ -1177,21 +1168,6 @@ lemma set_pt_vspace_objs [wp]:
done
lemma set_pt_arch_objs [wp]:
"\<lbrace>valid_arch_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (PageTable pt) s)\<rbrace>
set_pt p pt
\<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (simp add: set_pt_def)
apply (wp set_object_arch_objs get_object_wp)
apply (clarsimp simp: obj_at_def)
apply (rule conjI)
apply (clarsimp simp: a_type_def
split: kernel_object.splits arch_kernel_obj.splits)
apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits)
apply (simp add: vs_refs_def)
done
lemma set_pt_vs_lookup [wp]:
"\<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> set_pt p pt \<lbrace>\<lambda>x s. P (vs_lookup s)\<rbrace>"
unfolding set_pt_def set_object_def
@ -1913,16 +1889,6 @@ lemma set_asid_pool_valid_global [wp]:
crunch interrupt_states[wp]: set_asid_pool "\<lambda>s. P (interrupt_states s)"
(wp: crunch_wps)
lemma set_asid_pool_arch_objs_unmap':
"\<lbrace>valid_arch_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (ASIDPool ap) s) and
obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace>
set_asid_pool p ap \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
unfolding set_asid_pool_def including unfold_objects
apply (wpsimp wp: set_object_arch_objs)
apply (fastforce simp: a_type_def vs_refs_def)
done
lemma set_asid_pool_vspace_objs_unmap':
"\<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (ASIDPool ap) s) and
obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace>
@ -1932,16 +1898,6 @@ lemma set_asid_pool_vspace_objs_unmap':
apply (fastforce simp: a_type_def vs_refs_def)
done
lemma set_asid_pool_arch_objs_unmap:
"\<lbrace>valid_arch_objs and ko_at (ArchObj (ASIDPool ap)) p\<rbrace>
set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (wp set_asid_pool_arch_objs_unmap')
apply (clarsimp simp: obj_at_def graph_of_restrict_map)
apply (drule valid_arch_objsD, simp add: obj_at_def, assumption)
apply simp
by (auto simp: obj_at_def valid_arch_obj_def dest!: ran_restrictD)
lemma set_asid_pool_vspace_objs_unmap:
"\<lbrace>valid_vspace_objs and ko_at (ArchObj (ASIDPool ap)) p\<rbrace>
set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
@ -1949,7 +1905,7 @@ lemma set_asid_pool_vspace_objs_unmap:
apply (clarsimp simp: obj_at_def graph_of_restrict_map)
apply (drule valid_vspace_objsD, simp add: obj_at_def, assumption)
apply simp
by (auto simp: obj_at_def valid_arch_obj_def dest!: ran_restrictD)
by (auto simp: obj_at_def dest!: ran_restrictD)
lemma set_asid_pool_table_caps [wp]:
"\<lbrace>valid_table_caps\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_table_caps\<rbrace>"
@ -2093,13 +2049,6 @@ lemma set_asid_pool_asid_map_unmap:
by (simp add: restrict_map_def fun_upd_def if_flip)
lemma set_asid_pool_arch_objs_unmap_single:
"\<lbrace>valid_arch_objs and ko_at (ArchObj (ASIDPool ap)) p\<rbrace>
set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
using set_asid_pool_arch_objs_unmap[where S="- {x}"]
by (simp add: restrict_map_def fun_upd_def if_flip)
lemma set_asid_pool_vspace_objs_unmap_single:
"\<lbrace>valid_vspace_objs and ko_at (ArchObj (ASIDPool ap)) p\<rbrace>
set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
@ -2621,7 +2570,7 @@ lemma lookup_pt_slot_non_empty:
apply fastforce
apply (drule spec)
apply (erule(1) impE)
apply (clarsimp simp:valid_arch_obj_def)
apply (clarsimp simp:)
apply (drule_tac x = "(ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2))" in bspec)
apply (drule less_kernel_base_mapping_slots)
apply (clarsimp simp: obj_at_def)
@ -2812,23 +2761,6 @@ lemma store_pde_lookup_pd:
apply (clarsimp simp: vs_refs_def graph_of_def)
done
lemma store_pde_arch_objs_unmap:
"\<lbrace>valid_arch_objs
and valid_pde pde
and K (pde_ref pde = None)\<rbrace>
store_pde p pde \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (simp add: store_pde_def)
apply (wp set_pd_arch_objs_unmap)
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (drule (1) valid_arch_objsD, fastforce)
apply (simp add: valid_arch_obj_def)
apply (clarsimp simp add: obj_at_def vs_refs_def)
apply (rule pair_imageI)
apply (simp add: graph_of_def split: if_split_asm)
done
lemma store_pde_vspace_objs_unmap:
"\<lbrace>valid_vspace_objs
and valid_pde pde
@ -2840,7 +2772,7 @@ lemma store_pde_vspace_objs_unmap:
apply (rule conjI)
apply clarsimp
apply (drule (1) valid_vspace_objsD, fastforce)
apply (simp add: valid_arch_obj_def)
apply (simp add:)
apply (clarsimp simp add: obj_at_def vs_refs_def)
apply (rule pair_imageI)
apply (simp add: graph_of_def split: if_split_asm)
@ -2968,31 +2900,30 @@ lemma vs_lookup_pages_next_asid[iff]:
vs_lookup_pages s"
by (simp add: vs_lookup_pages_arch_update)
lemma valid_arch_objs_arch_update:
lemma valid_vspace_objs_arch_update:
"arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s) \<Longrightarrow>
valid_arch_objs (arch_state_update f s) = valid_arch_objs s"
valid_vspace_objs (arch_state_update f s) = valid_vspace_objs s"
apply (rule iffI)
apply (erule valid_arch_objs_stateI)
apply (erule valid_vspace_objs_stateI)
apply (clarsimp simp: obj_at_def)
apply simp
apply simp
apply (erule valid_arch_objs_stateI)
apply (erule valid_vspace_objs_stateI)
apply (clarsimp simp: obj_at_def)
apply simp
apply simp
done
lemma store_pte_valid_arch_objs[wp]:
"\<lbrace>valid_arch_objs and valid_pte pte\<rbrace>
lemma store_pte_valid_vspace_objs[wp]:
"\<lbrace>valid_vspace_objs and valid_pte pte\<rbrace>
store_pte p pte
\<lbrace>\<lambda>_. (valid_arch_objs)\<rbrace>"
\<lbrace>\<lambda>_. (valid_vspace_objs)\<rbrace>"
unfolding store_pte_def
apply wp
apply clarsimp
apply (unfold valid_arch_objs_def)
apply (unfold valid_vspace_objs_def)
apply (erule_tac x="p && ~~ mask pt_bits" in allE)
apply (auto simp: valid_arch_obj_def)
apply auto
done
crunch valid_arch [wp]: store_pte valid_arch_state

9
proof/invariant-abstract/ARM/ArchArch_AI.thy
View File

@ -324,11 +324,6 @@ lemma vs_lookup_pages':
done
lemma arch_obj [simp]:
"valid_arch_obj ao s' = valid_arch_obj ao s"
by (cases ao, simp_all add: s'_def)
lemma obj_at [simp]:
"obj_at P p s' = obj_at P p s"
by (simp add: s'_def)
@ -1088,7 +1083,7 @@ lemma find_pd_for_asid_ref_offset_voodoo:
mask_asid_low_bits_ucast_ucast)
apply (fold asid_low_bits_def)
apply (rule hoare_pre, wp find_pd_for_asid_lookup_ref)
apply (simp add: valid_arch_imp_valid_vspace_objs)
apply (simp add: )
apply (simp add: pd_shifting)
done
@ -1550,7 +1545,7 @@ lemma arch_decode_inv_wf[wp]:
apply (drule (1) diminished_is_update)
apply (clarsimp simp: cap_rights_update_def acap_rights_update_def valid_cap_def)
apply (drule (2) valid_table_caps_ptD)
apply (rule conjI, fastforce simp: valid_arch_obj_def)+
apply (rule conjI, fastforce simp:)+
apply (clarsimp simp: kernel_vsrefs_def)
apply (simp add: linorder_not_le, drule minus_one_helper3)
apply (drule le_shiftr[where n=20], drule(1) order_trans)

2
proof/invariant-abstract/ARM/ArchCNodeInv_AI.thy
View File

@ -246,7 +246,7 @@ lemma invs_irq_state_independent[intro!, simp, CNodeInv_AI_assms]:
only_idle_def if_unsafe_then_cap_def valid_reply_caps_def
valid_reply_masters_def valid_global_refs_def valid_arch_state_def
valid_irq_node_def valid_irq_handlers_def valid_machine_state_def
valid_arch_objs_def valid_arch_caps_def valid_global_objs_def
valid_arch_caps_def valid_global_objs_def
valid_kernel_mappings_def equal_kernel_mappings_def
valid_asid_map_def valid_global_vspace_mappings_def
pspace_in_kernel_window_def cap_refs_in_kernel_window_def

9
proof/invariant-abstract/ARM/ArchFinalise_AI.thy
View File

@ -705,9 +705,6 @@ lemma invalidate_tlb_by_asid_pspace_aligned:
apply (simp add: invalidate_tlb_by_asid_def load_hw_asid_def | wp | wpc)+
done
crunch valid_arch_objs[wp]: invalidate_tlb_by_asid, page_table_mapped
"valid_arch_objs"
crunch cte_wp_at[wp]: invalidate_tlb_by_asid, page_table_mapped
"\<lambda>s. P (cte_wp_at P' p s)"
@ -1225,9 +1222,9 @@ lemma replaceable_or_arch_update_pg:
apply (auto simp: is_cap_simps is_arch_update_def cap_master_cap_simps)
done
lemma store_pde_arch_objs_invalid:
"\<lbrace>valid_arch_objs\<rbrace> store_pde p InvalidPDE \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (wp store_pde_arch_objs_unmap)
lemma store_pde_vspace_objs_invalid:
"\<lbrace>valid_vspace_objs\<rbrace> store_pde p ARM_A.InvalidPDE \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
apply (wp store_pde_vspace_objs_unmap)
apply (simp add: pde_ref_def)
done

181
proof/invariant-abstract/ARM/ArchInvariants_AI.thy
View File

@ -268,8 +268,6 @@ where
| "valid_vspace_obj (PageTable pt) = (\<lambda>s. \<forall>x. valid_pte (pt x) s)"
| "valid_vspace_obj (DataPage dev sz) = \<top>"
definition "valid_arch_obj \<equiv> valid_vspace_obj"
definition
wellformed_pte :: "pte \<Rightarrow> bool"
where
@ -416,18 +414,6 @@ where
"valid_vspace_objs \<equiv>
\<lambda>s. \<forall>p rs ao. (rs \<rhd> p) s \<longrightarrow> ko_at (ArchObj ao) p s \<longrightarrow> valid_vspace_obj ao s"
definition
valid_arch_objs :: "'z::state_ext state \<Rightarrow> bool"
where
"valid_arch_objs \<equiv>
\<lambda>s. \<forall>p rs ao. (rs \<rhd> p) s \<longrightarrow> ko_at (ArchObj ao) p s \<longrightarrow> valid_arch_obj ao s"
lemma valid_arch_imp_valid_vspace_obj: "valid_arch_obj ko s \<Longrightarrow> valid_vspace_obj ko s"
by (clarsimp simp: valid_arch_obj_def valid_vspace_obj_def)
lemma valid_arch_imp_valid_vspace_objs: "valid_arch_objs s \<Longrightarrow> valid_vspace_objs s"
by (clarsimp simp: valid_arch_objs_def valid_vspace_objs_def valid_arch_imp_valid_vspace_obj)
definition
pde_ref_pages :: "pde \<Rightarrow> obj_ref option"
where
@ -626,7 +612,7 @@ where
definition
valid_ao_at :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"valid_ao_at p \<equiv> \<lambda>s. \<exists>ao. ko_at (ArchObj ao) p s \<and> valid_arch_obj ao s"
"valid_ao_at p \<equiv> \<lambda>s. \<exists>ao. ko_at (ArchObj ao) p s \<and> valid_vspace_obj ao s"
definition
"valid_pde_mappings pde \<equiv> case pde of
@ -1028,32 +1014,10 @@ lemma vs_lookup_stateI:
shows "(ref \<rhd> p) s'"
using 1 vs_lookup_sub [OF ko table] by blast
lemma valid_arch_objsD:
"\<lbrakk> (ref \<rhd> p) s; ko_at (ArchObj ao) p s; valid_arch_objs s \<rbrakk> \<Longrightarrow> valid_arch_obj ao s"
by (fastforce simp add: valid_arch_objs_def)
lemma valid_vspace_objsD:
"\<lbrakk> (ref \<rhd> p) s; ko_at (ArchObj ao) p s; valid_vspace_objs s \<rbrakk> \<Longrightarrow> valid_vspace_obj ao s"
by (fastforce simp add: valid_vspace_objs_def)
(* should work for unmap and non-arch ops *)
lemma valid_arch_objs_stateI:
assumes 1: "valid_arch_objs s"
assumes ko: "\<And>ko p. ko_at ko p s' \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s"
assumes arch: "graph_of (arm_asid_table (arch_state s')) \<subseteq> graph_of (arm_asid_table (arch_state s))"
assumes vao: "\<And>p ref ao'.
\<lbrakk> (ref \<rhd> p) s; (ref \<rhd> p) s'; \<forall>ao. ko_at (ArchObj ao) p s \<longrightarrow> valid_arch_obj ao s;
ko_at (ArchObj ao') p s' \<rbrakk> \<Longrightarrow> valid_arch_obj ao' s'"
shows "valid_arch_objs s'"
using 1 unfolding valid_arch_objs_def
apply clarsimp
apply (frule vs_lookup_stateI)
apply (erule ko)
apply (rule arch)
apply (erule allE, erule impE, fastforce)
apply (erule (3) vao)
done
lemma valid_arch_cap_typ:
assumes P: "\<And>T p. \<lbrace>\<lambda>s. (typ_at (AArch T) p s )\<rbrace> f \<lbrace>\<lambda>rv s. (typ_at (AArch T) p s)\<rbrace>"
shows "\<lbrace>\<lambda>s. valid_arch_cap c s\<rbrace> f \<lbrace>\<lambda>rv s. valid_arch_cap c s\<rbrace>"
@ -1077,13 +1041,6 @@ lemma valid_vspace_obj_typ:
apply (wp hoare_vcg_disj_lift P)+
done
lemma valid_arch_obj_typ:
assumes P: "\<And>p T. \<lbrace>\<lambda>s. (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. (typ_at (AArch T) p s)\<rbrace>"
shows "\<lbrace>\<lambda>s. valid_arch_obj ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_arch_obj ob s\<rbrace>"
by (wpsimp simp: valid_arch_obj_def wp: valid_vspace_obj_typ P)
lemmas valid_arch_obj_typ_gen = valid_arch_obj_typ
lemma atyp_at_eq_kheap_obj:
"typ_at (AArch AASIDPool) p s \<longleftrightarrow> (\<exists>f. kheap s p = Some (ArchObj (ASIDPool f)))"
"typ_at (AArch APageTable) p s \<longleftrightarrow> (\<exists>pt. kheap s p = Some (ArchObj (PageTable pt)))"
@ -1128,16 +1085,21 @@ lemma wellformed_arch_typ:
shows "\<lbrace>\<lambda>s. wellformed_arch_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. wellformed_arch_obj ao s\<rbrace>"
by (cases ao; clarsimp; wp)
lemma valid_arch_obj_pspaceI:
"\<lbrakk> valid_arch_obj obj s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_arch_obj obj s'"
apply (cases obj, simp_all add: valid_arch_obj_def)
apply (simp add: obj_at_def)
apply (erule allEI)
apply (rename_tac "fun" x)
apply (case_tac "fun x", simp_all add: obj_at_def data_at_def)
apply (erule ballEI)
apply (rename_tac "fun" x)
apply (case_tac "fun x", simp_all add: obj_at_def data_at_def)
lemma valid_vspace_objs_stateI:
assumes 1: "valid_vspace_objs s"
assumes ko: "\<And>ko p. ko_at ko p s' \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s"
assumes arch: "graph_of (arm_asid_table (arch_state s')) \<subseteq> graph_of (arm_asid_table (arch_state s))"
assumes vao: "\<And>p ref ao'.
\<lbrakk> (ref \<rhd> p) s; (ref \<rhd> p) s'; \<forall>ao. ko_at (ArchObj ao) p s \<longrightarrow> valid_vspace_obj ao s;
ko_at (ArchObj ao') p s' \<rbrakk> \<Longrightarrow> valid_vspace_obj ao' s'"
shows "valid_vspace_objs s'"
using 1 unfolding valid_vspace_objs_def
apply clarsimp
apply (frule vs_lookup_stateI)
apply (erule ko)
apply (rule arch)
apply (erule allE, erule impE, fastforce)
apply (erule (3) vao)
done
lemmas pageBitsForSize_simps[simp] =
@ -1208,10 +1170,6 @@ lemma valid_vspace_obj_update [iff]:
"valid_vspace_obj ao (f s) = valid_vspace_obj ao s"
by (cases ao) auto
lemma valid_arch_obj_update [iff]:
"valid_arch_obj ao (f s) = valid_arch_obj ao s"
by (auto simp: valid_arch_obj_def)
lemma valid_ao_at_update [iff]:
"valid_ao_at p (f s) = valid_ao_at p s"
by (simp add: valid_ao_at_def)
@ -1302,10 +1260,6 @@ lemma valid_vspace_objs_update' [iff]:
"valid_vspace_objs (f s) = valid_vspace_objs s"
by (simp add: valid_vspace_objs_def)
lemma valid_arch_objs_update' [iff]:
"valid_arch_objs (f s) = valid_arch_objs s"
by (simp add: valid_arch_objs_def)
end
@ -1429,12 +1383,12 @@ lemma physical_arch_cap_has_ref:
subsection "vs_lookup"
lemma vs_lookup1_ko_at_dest:
"\<lbrakk> ((ref, p) \<rhd>1 (ref', p')) s; ko_at (ArchObj ao) p s; valid_arch_obj ao s \<rbrakk> \<Longrightarrow>
"\<lbrakk> ((ref, p) \<rhd>1 (ref', p')) s; ko_at (ArchObj ao) p s; valid_vspace_obj ao s \<rbrakk> \<Longrightarrow>
\<exists>ao'. ko_at (ArchObj ao') p' s \<and> (\<exists>tp. vs_ref_aatype (hd ref') = Some tp
\<and> aa_type ao = tp)"
apply (drule vs_lookup1D)
apply (clarsimp simp: obj_at_def vs_refs_def)
apply (cases ao, simp_all add: graph_of_def valid_arch_obj_def)
apply (cases ao, simp_all add: graph_of_def)
apply clarsimp
apply (drule bspec, fastforce simp: ran_def)
apply (clarsimp simp add: aa_type_def obj_at_def)
@ -1596,20 +1550,18 @@ lemma stronger_vspace_objsD_lemma:
apply (cases r)
apply clarsimp
apply (frule (2) valid_vspace_objsD)
apply (simp only: valid_arch_obj_def[symmetric])
apply (drule (1) vs_lookup_step)
apply (drule (2) vs_lookup1_ko_at_dest)
apply clarsimp
apply (drule (2) valid_vspace_objsD)
apply (fastforce simp: valid_arch_obj_def)
apply (fastforce simp: valid_vspace_obj_def)
apply clarsimp
apply (simp only: valid_arch_obj_def[symmetric])
apply (frule (2) vs_lookup1_ko_at_dest)
apply (drule (1) vs_lookup_trancl_step)
apply (drule (1) vs_lookup_step)
apply clarsimp
apply (drule (2) valid_vspace_objsD)
apply (fastforce simp: valid_arch_obj_def)
apply (fastforce simp: valid_vspace_obj_def)
done
lemma stronger_vspace_objsD:
@ -1638,55 +1590,6 @@ lemma stronger_vspace_objsD:
apply (clarsimp simp: obj_at_def)
done
lemma stronger_arch_objsD_lemma:
"\<lbrakk>valid_arch_objs s; r \<in> vs_lookup s; (r,r') \<in> (vs_lookup1 s)\<^sup>+ \<rbrakk>
\<Longrightarrow> \<exists>ao. ko_at (ArchObj ao) (snd r') s \<and>
valid_arch_obj ao s"
apply (erule trancl_induct)
apply (frule vs_lookup1_is_arch)
apply (cases r)
apply clarsimp
apply (frule (2) valid_arch_objsD)
apply (drule (1) vs_lookup_step)
apply (drule (2) vs_lookup1_ko_at_dest)
apply clarsimp
apply (drule (2) valid_arch_objsD)
apply fastforce
apply clarsimp
apply (frule (2) vs_lookup1_ko_at_dest)
apply (drule (1) vs_lookup_trancl_step)
apply (drule (1) vs_lookup_step)
apply clarsimp
apply (drule (2) valid_arch_objsD)
apply fastforce
done
lemma stronger_arch_objsD:
"\<lbrakk> (ref \<rhd> p) s;
valid_arch_objs s;
valid_asid_table (arm_asid_table (arch_state s)) s \<rbrakk> \<Longrightarrow>
\<exists>ao. ko_at (ArchObj ao) p s \<and>
valid_arch_obj ao s"
apply (clarsimp simp: vs_lookup_def vs_asid_refs_def graph_of_def)
apply (clarsimp simp: valid_asid_table_def)
apply (drule bspec, fastforce simp: ran_def)
apply (drule rtranclD)
apply (erule disjE)
prefer 2
apply clarsimp
apply (drule stronger_arch_objsD_lemma)
apply (erule vs_lookup_atI)
apply assumption
apply clarsimp
apply clarsimp
apply (simp add: valid_arch_objs_def)
apply (erule_tac x=p in allE)
apply (erule impE)
apply (rule exI)
apply (erule vs_lookup_atI)
apply (clarsimp simp: obj_at_def)
done
(* An alternative definition for valid_vspace_objs.
The predicates valid_asid_table and valid_vspace_objs are very compact
@ -1746,10 +1649,10 @@ lemma valid_vspace_objs_alt:
apply (erule converse_rtranclE)
apply (clarsimp simp: vs_asid_refs_def graph_of_def)
apply (drule spec, drule spec, erule impE, assumption)
apply (clarsimp simp: obj_at_def ran_def valid_arch_obj_def)
apply (clarsimp simp: obj_at_def ran_def)
apply (erule converse_rtranclE)
apply (drule vs_lookup1D)
apply (clarsimp simp: vs_asid_refs_def graph_of_def valid_arch_obj_def)
apply (clarsimp simp: vs_asid_refs_def graph_of_def)
apply (drule spec, drule spec, erule impE, assumption)
apply (drule spec, drule spec, erule impE, assumption)
apply (drule spec, drule spec, erule impE, assumption)
@ -1760,7 +1663,7 @@ lemma valid_vspace_objs_alt:
apply fastforce
apply (erule converse_rtranclE)
apply (clarsimp dest!: vs_lookup1D)
apply (clarsimp simp: vs_asid_refs_def graph_of_def valid_arch_obj_def)
apply (clarsimp simp: vs_asid_refs_def graph_of_def)
apply (drule spec, drule spec, erule impE, assumption)
apply (drule spec, drule spec, erule impE, assumption)
apply (drule spec, drule spec, erule impE, assumption)
@ -1964,7 +1867,7 @@ lemma empty_table_is_valid:
"\<lbrakk>empty_table (set (arm_global_pts (arch_state s))) (ArchObj ao);
valid_arch_state s\<rbrakk>
\<Longrightarrow> valid_vspace_obj ao s"
by (cases ao, simp_all add: empty_table_def valid_arch_obj_def)
by (cases ao, simp_all add: empty_table_def)
lemma empty_table_pde_refD:
"\<lbrakk> pde_ref (pd x) = Some r; empty_table S (ArchObj (PageDirectory pd)) \<rbrakk> \<Longrightarrow>
@ -2030,7 +1933,7 @@ lemma vs_lookup_pages_induct:
done
lemma vs_ref_order:
"\<lbrakk> (r \<rhd> p) s; valid_arch_objs s; valid_arch_state s \<rbrakk>
"\<lbrakk> (r \<rhd> p) s; valid_vspace_objs s; valid_arch_state s \<rbrakk>
\<Longrightarrow> \<exists>tp. r \<noteq> [] \<and> typ_at (AArch tp) p s \<and>
rev (Some tp # map vs_ref_aatype r)
\<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]"
@ -2040,13 +1943,13 @@ lemma vs_ref_order:
apply (clarsimp simp: vs_refs_def a_type_simps
split: kernel_object.split_asm arch_kernel_obj.split_asm
dest!: graph_ofD)
apply (drule valid_arch_objsD) apply (simp add: obj_at_def) apply (assumption)
apply (drule valid_vspace_objsD) apply (simp add: obj_at_def) apply (assumption)
apply (case_tac rs; simp)
apply (case_tac list; simp add: ranI valid_arch_obj_def)
apply (case_tac list; simp add: ranI)
apply (case_tac lista; simp)
apply (frule prefix_length_le, clarsimp)
apply (drule valid_arch_objsD, simp add: obj_at_def, assumption)
apply (clarsimp simp: pde_ref_def valid_arch_obj_def
apply (drule valid_vspace_objsD, simp add: obj_at_def, assumption)
apply (clarsimp simp: pde_ref_def
split: pde.split_asm if_split_asm)
apply (drule_tac x=a in bspec, simp)
apply (case_tac rs; simp)
@ -2073,7 +1976,7 @@ lemma valid_pde_lift2:
lemma valid_vspace_obj_typ2:
assumes P: "\<And>P p T. \<lbrace>\<lambda>s. Q s \<and> P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
shows "\<lbrace>\<lambda>s. Q s \<and> valid_vspace_obj ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_vspace_obj ob s\<rbrace>"
apply (cases ob, simp_all add: valid_arch_obj_def)
apply (cases ob, simp_all add:)
apply (wp hoare_vcg_const_Ball_lift [OF P], simp)
apply (rule hoare_pre, wp hoare_vcg_all_lift valid_pte_lift2 P)
apply clarsimp
@ -2086,15 +1989,6 @@ lemma valid_vspace_obj_typ2:
apply wp
done
lemma valid_arch_obj_typ2:
assumes P: "\<And>P p T. \<lbrace>\<lambda>s. Q s \<and> P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
shows "\<lbrace>\<lambda>s. Q s \<and> valid_arch_obj ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_arch_obj ob s\<rbrace>"
using assms unfolding valid_arch_obj_def by (rule valid_vspace_obj_typ2)
lemma valid_arch_objsI [intro?]:
"(\<And>p ao. \<lbrakk> (\<exists>\<rhd> p) s; ko_at (ArchObj ao) p s \<rbrakk> \<Longrightarrow> valid_arch_obj ao s) \<Longrightarrow> valid_arch_objs s"
by (simp add: valid_arch_objs_def)
lemma valid_vspace_objsI [intro?]:
"(\<And>p ao. \<lbrakk> (\<exists>\<rhd> p) s; ko_at (ArchObj ao) p s \<rbrakk> \<Longrightarrow> valid_vspace_obj ao s) \<Longrightarrow> valid_vspace_objs s"
by (simp add: valid_vspace_objs_def)
@ -2196,16 +2090,6 @@ lemma vs_cap_ref_eq_imp_table_cap_ref_eq:
split: cap.splits arch_cap.splits vmpage_size.splits option.splits)
lemma valid_arch_objs_lift:
assumes x: "\<And>P. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>"
assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
and y: "\<And>ao p. \<lbrace>\<lambda>s. \<not> ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> ko_at (ArchObj ao) p s\<rbrace>"
shows "\<lbrace>valid_arch_objs\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_objs\<rbrace>"
apply (simp add: valid_arch_objs_def)
apply (wp hoare_vcg_all_lift hoare_convert_imp [OF x]
hoare_convert_imp [OF y] valid_arch_obj_typ z)
done
lemma valid_validate_vm_rights[simp]:
"validate_vm_rights rs \<in> valid_vm_rights"
and validate_vm_rights_subseteq[simp]:
@ -2275,11 +2159,6 @@ lemma wellformed_arch_default:
unfolding wellformed_arch_obj_def default_arch_object_def
by (cases aobject_type; simp)
lemma valid_arch_obj_default':
"valid_arch_obj (default_arch_object aobject_type dev us) s"
unfolding default_arch_object_def
by (cases aobject_type; simp add: valid_arch_obj_def)
lemma valid_vspace_obj_default':
"valid_vspace_obj (default_arch_object aobject_type dev us) s"
unfolding default_arch_object_def

9
proof/invariant-abstract/ARM/ArchIpc_AI.thy
View File

@ -389,15 +389,6 @@ lemma transfer_caps_non_null_cte_wp_at:
crunch cte_wp_at[wp,Ipc_AI_assms]: do_fault_transfer "cte_wp_at P p"
lemma set_cap_valid_arch_objs [wp, Ipc_AI_assms]:
"\<lbrace>valid_arch_objs\<rbrace> set_cap a b \<lbrace>\<lambda>_. valid_arch_objs \<rbrace>"
apply (rule valid_arch_objs_lift)
apply (wp set_cap_typ_at)+
apply (rule set_cap.aobj_at)
apply (fastforce simp: arch_obj_pred_def non_arch_obj_def
split: kernel_object.split arch_kernel_obj.splits)
done
lemma do_normal_transfer_non_null_cte_wp_at [Ipc_AI_assms]:
assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c"
shows "\<lbrace>valid_objs and cte_wp_at (P and (op \<noteq> cap.NullCap)) ptr\<rbrace>

55
proof/invariant-abstract/ARM/ArchKHeap_AI.thy
View File

@ -20,9 +20,6 @@ where
"non_vspace_obj (ArchObj _) = False"
| "non_vspace_obj _ = True"
lemma valid_arch_objs_lift2: "valid_pspace s \<Longrightarrow> valid_vspace_objs s \<Longrightarrow> valid_arch_objs s"
by (clarsimp simp add: valid_pspace_def valid_objs_def valid_vspace_objs_def valid_arch_objs_def valid_arch_obj_def obj_at_def)
lemma obj_at_split: "(obj_at (P xo) p s \<and> (Q xo)) = obj_at (\<lambda>ko. P xo ko \<and> Q xo) p s"
by (auto simp: obj_at_def)
@ -268,16 +265,6 @@ lemma valid_vspace_objs_lift_weak:
apply (rule obj_at arch_state vspace_pred_imp; simp)+
done
lemma valid_arch_objs_lift_weak:
assumes obj_at: "\<And>P P' p. arch_obj_pred P' \<Longrightarrow>
\<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
shows "\<lbrace>valid_arch_objs\<rbrace> f \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (rule valid_arch_objs_lift)
apply (rule vs_lookup_arch_obj_at_lift)
apply (rule obj_at arch_state; simp)+
done
lemma set_object_neg_lookup:
"\<lbrace>\<lambda>s. \<not> (\<exists>rs. (rs \<rhd> p') s) \<and> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s \<rbrace>
set_object p ko
@ -392,23 +379,6 @@ lemma set_object_atyp_at:
apply (clarsimp simp: obj_at_def a_type_aa_type)
done
lemma set_object_arch_objs:
"\<lbrace>valid_arch_objs and typ_at (a_type ko) p and
obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p and
(\<lambda>s. case ko of ArchObj ao \<Rightarrow>
(\<exists>\<rhd>p)s \<longrightarrow> valid_arch_obj ao s
| _ \<Rightarrow> True)\<rbrace>
set_object p ko
\<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (simp add: valid_arch_objs_def)
apply (subst imp_conv_disj)+
apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift set_object_neg_lookup set_object_neg_ko
valid_arch_obj_typ2 [where Q="typ_at (a_type ko) p"] set_object_typ_at
| simp)+
apply (clarsimp simp: pred_neg_def obj_at_def)
apply fastforce
done
lemma set_object_vspace_objs:
"\<lbrace>valid_vspace_objs and typ_at (a_type ko) p and
obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p and
@ -627,13 +597,13 @@ lemma valid_ao_at_lift:
and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>"
shows "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>"
unfolding valid_ao_at_def
by (wp hoare_vcg_ex_lift y valid_arch_obj_typ z)
by (wp hoare_vcg_ex_lift y valid_vspace_obj_typ z)
lemma valid_ao_at_lift_aobj_at:
assumes aobj_at: "\<And>P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>"
shows "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>"
unfolding valid_ao_at_def
by (wp hoare_vcg_ex_lift valid_arch_obj_typ aobj_at | clarsimp)+
by (wp hoare_vcg_ex_lift valid_vspace_obj_typ aobj_at | clarsimp)+
lemma valid_vso_at_lift:
assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
@ -743,11 +713,11 @@ lemma set_object_global_vspace_mappings:
lemma valid_table_caps_ptD:
"\<lbrakk> (caps_of_state s) p = Some (ArchObjectCap (arch_cap.PageTableCap p' None));
page_table_at p' s; valid_table_caps s \<rbrakk> \<Longrightarrow>
\<exists>pt. ko_at (ArchObj (PageTable pt)) p' s \<and> valid_arch_obj (PageTable pt) s"
\<exists>pt. ko_at (ArchObj (PageTable pt)) p' s \<and> valid_vspace_obj (PageTable pt) s"
apply (clarsimp simp: valid_table_caps_def simp del: split_paired_All)
apply (erule allE)+
apply (erule (1) impE)
apply (clarsimp simp add: valid_arch_obj_def is_pt_cap_def cap_asid_def)
apply (clarsimp simp add: is_pt_cap_def cap_asid_def)
apply (erule impE, rule refl)
apply (clarsimp simp: obj_at_def empty_table_def)
done
@ -871,26 +841,11 @@ lemma state_hyp_refs_of_tcb_state_update:
apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
done
lemma valid_arch_obj_same_type:
"\<lbrakk>valid_arch_obj ao s; kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
\<Longrightarrow> valid_arch_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> ko')\<rparr>)"
apply (induction ao rule: arch_kernel_obj.induct;
clarsimp simp: valid_arch_obj_def typ_at_same_type)
apply (rule hoare_to_pure_kheap_upd; assumption?)
apply (rule valid_pte_lift, assumption)
apply blast
apply (simp add: obj_at_def)
apply (rule hoare_to_pure_kheap_upd; assumption?)
apply (rule valid_pde_lift, assumption)
apply blast
apply (simp add: obj_at_def)
done
lemma wellformed_arch_obj_same_type:
"\<lbrakk> wellformed_arch_obj ao s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
\<Longrightarrow> wellformed_arch_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
by (induction ao rule: arch_kernel_obj.induct;
clarsimp simp: valid_arch_obj_def typ_at_same_type)
clarsimp simp: typ_at_same_type)
lemma default_arch_object_not_live: "\<not> live (ArchObj (default_arch_object aty dev us))"

2
proof/invariant-abstract/ARM/ArchKernelInit_AI.thy
View File

@ -337,7 +337,7 @@ lemma invs_A:
apply (clarsimp simp: valid_machine_state_def init_A_st_def
init_machine_state_def init_underlying_memory_def)
apply (rule conjI)
apply (clarsimp simp: valid_arch_objs_def obj_at_def state_defs valid_vspace_objs_def)
apply (clarsimp simp: obj_at_def state_defs valid_vspace_objs_def)
apply (clarsimp simp: vs_lookup_def vs_asid_refs_def)
apply (rule conjI)
apply (clarsimp simp: valid_arch_caps_def)

35
proof/invariant-abstract/ARM/ArchRetype_AI.thy
View File

@ -835,12 +835,6 @@ end
context retype_region_proofs_arch begin
lemma valid_arch_obj_pres:
"valid_arch_obj ao s \<Longrightarrow> valid_arch_obj ao s'"
apply (cases ao; simp add: valid_arch_obj_def obj_at_pres)
apply (erule allEI ballEI; rename_tac t i; case_tac "t i"; fastforce simp: data_at_def obj_at_pres)+
done
lemma valid_vspace_obj_pres:
"valid_vspace_obj ao s \<Longrightarrow> valid_vspace_obj ao s'"
apply (cases ao; simp add: valid_vspace_obj_def obj_at_pres)
@ -880,31 +874,6 @@ proof
qed
lemma valid_arch_objs':
assumes va: "valid_arch_objs s"
shows "valid_arch_objs s'"
proof
fix p ao
assume p: "(\<exists>\<rhd> p) s'"
assume "ko_at (ArchObj ao) p s'"
hence "ko_at (ArchObj ao) p s \<or> ArchObj ao = default_object ty dev us"
by (simp add: ps_def obj_at_def s'_def split: if_split_asm)
moreover
{ assume "ArchObj ao = default_object ty dev us" with tyunt
have "valid_arch_obj ao s'" by (rule valid_arch_obj_default)
}
moreover
{ assume "ko_at (ArchObj ao) p s"
with va p
have "valid_arch_obj ao s"
by (auto simp: vs_lookup' elim: valid_arch_objsD)
hence "valid_arch_obj ao s'"
by (rule valid_arch_obj_pres)
}
ultimately
show "valid_arch_obj ao s'" by blast
qed
(* ML \<open>val pre_ctxt_0 = @{context}\<close> *)
sublocale retype_region_proofs_gen?: retype_region_proofs_gen
by (unfold_locales,
@ -1079,7 +1048,7 @@ lemma valid_global_objs:
apply (simp add: obj_at_pres valid_vspace_obj_pres)
apply (simp add: obj_at_pres)
apply (rule exEI, erule(1) bspec)
apply (simp add: obj_at_pres valid_arch_obj_pres)
apply (simp add: obj_at_pres)
done
lemma valid_kernel_mappings:
@ -1336,7 +1305,7 @@ lemma invs_irq_state_independent:
only_idle_def if_unsafe_then_cap_def valid_reply_caps_def
valid_reply_masters_def valid_global_refs_def valid_arch_state_def
valid_irq_node_def valid_irq_handlers_def valid_machine_state_def
valid_arch_objs_def valid_arch_caps_def valid_global_objs_def
valid_arch_caps_def valid_global_objs_def
valid_kernel_mappings_def equal_kernel_mappings_def
valid_asid_map_def vspace_at_asid_def
pspace_in_kernel_window_def cap_refs_in_kernel_window_def

2
proof/invariant-abstract/ARM/ArchUntyped_AI.thy
View File

@ -461,7 +461,7 @@ proof -
by (case_tac pte, auto simp add: typ_at data_at_def)
have valid_ao_at: "\<And>p. valid_ao_at p s \<Longrightarrow> valid_ao_at p ?s'"
using pd uc
apply (clarsimp simp: valid_ao_at_def obj_at_def valid_arch_obj_def)
apply (clarsimp simp: valid_ao_at_def obj_at_def)
apply (intro conjI impI allI)
apply (clarsimp simp: valid_pde vp)
apply (case_tac ao, simp_all add: typ_at valid_pde valid_pte)

4
proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy
View File

@ -1495,7 +1495,7 @@ lemma arch_decode_invocation_valid_pdpt[wp]:
and f="find_pd_for_asid p" for p
in hoare_post_imp_R)
apply (wp| simp)+
apply (fastforce simp:pd_bits_def pageBits_def intro: valid_arch_imp_valid_vspace_objs)
apply (fastforce simp:pd_bits_def pageBits_def)
apply ((wp get_pde_wp
ensure_safe_mapping_ensures[THEN hoare_post_imp_R]
create_mapping_entries_safe check_vp_wpR
@ -1516,7 +1516,7 @@ lemma arch_decode_invocation_valid_pdpt[wp]:
and f="find_pd_for_asid p" for p
in hoare_post_imp_R)
apply (wp| simp)+
apply (auto simp:pd_bits_def pageBits_def intro: valid_arch_imp_valid_vspace_objs)[1]
apply (auto simp:pd_bits_def pageBits_def)[1]
apply ((wp get_pde_wp
ensure_safe_mapping_ensures[THEN hoare_post_imp_R]
create_mapping_entries_safe check_vp_wpR

88
proof/invariant-abstract/ARM/ArchVSpace_AI.thy
View File

@ -112,7 +112,7 @@ lemma table_cap_ref_ap_eq:
lemma pd_at_asid_unique:
"\<lbrakk> vspace_at_asid asid pd s; vspace_at_asid asid' pd s;
unique_table_refs (caps_of_state s);
valid_vs_lookup s; valid_arch_objs s; valid_global_objs s;
valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s;
valid_arch_state s; asid < 2 ^ asid_bits; asid' < 2 ^ asid_bits \<rbrakk>
\<Longrightarrow> asid = asid'"
apply (clarsimp simp: vspace_at_asid_def)
@ -143,7 +143,7 @@ lemma pd_at_asid_unique2:
lemma pd_at_asid_uniq:
"\<lbrakk> vspace_at_asid asid pd s; asid \<le> mask asid_bits; valid_asid_map s;
unique_table_refs (caps_of_state s); valid_vs_lookup s;
valid_arch_objs s; valid_global_objs s; valid_arch_state s \<rbrakk>
valid_vspace_objs s; valid_global_objs s; valid_arch_state s \<rbrakk>
\<Longrightarrow> pd_at_uniq asid pd s"
apply (clarsimp simp: pd_at_uniq_def ran_option_map
dest!: ran_restrictD)
@ -186,13 +186,13 @@ lemma valid_vs_lookupE:
by (simp add: valid_vs_lookup_def, blast)
lemma find_free_hw_asid_arch_objs [wp]:
"\<lbrace>valid_arch_objs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>asid. valid_arch_objs\<rbrace>"
lemma find_free_hw_asid_vspace_objs [wp]:
"\<lbrace>valid_vspace_objs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>asid. valid_vspace_objs\<rbrace>"
apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def invalidate_asid_def
do_machine_op_def split_def
cong: option.case_cong)
apply (wp|wpc)+
apply (simp add: valid_arch_objs_arch_update)
apply (simp add: valid_vspace_objs_arch_update)
done
lemma find_free_hw_asid_pd_at_asid [wp]:
@ -383,11 +383,11 @@ crunch valid_arch [wp]: flush_space valid_arch_state
crunch valid_objs [wp]: flush_space valid_objs
lemma invalidate_hw_asid_arch_objs [wp]:
"\<lbrace>valid_arch_objs\<rbrace> invalidate_hw_asid_entry asid \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
lemma invalidate_hw_asid_vspace_objs [wp]:
"\<lbrace>valid_vspace_objs\<rbrace> invalidate_hw_asid_entry asid \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
apply (simp add: invalidate_hw_asid_entry_def)
apply wp
apply (simp add: valid_arch_objs_arch_update)
apply (simp add: valid_vspace_objs_arch_update)
done
@ -432,9 +432,9 @@ lemma flush_space_asid_map[wp]:
lemma flush_space_arch_objs[wp]:
"\<lbrace>valid_arch_objs\<rbrace> flush_space space \<lbrace>\<lambda>rv. valid_arch_objs\<rbrace>"
"\<lbrace>valid_vspace_objs\<rbrace> flush_space space \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>"
apply (simp add: flush_space_def)
apply (wp load_hw_asid_wp | wpc | simp | rule_tac Q="\<lambda>_. valid_arch_objs" in hoare_strengthen_post)+
apply (wp load_hw_asid_wp | wpc | simp | rule_tac Q="\<lambda>_. valid_vspace_objs" in hoare_strengthen_post)+
done
@ -491,8 +491,8 @@ lemma invalidate_asid_entry_invalidates:
done
crunch arch_objs [wp]: invalidate_asid_entry valid_arch_objs
(simp: valid_arch_objs_arch_update)
crunch vspace_objs [wp]: invalidate_asid_entry valid_vspace_objs
(simp: valid_vspace_objs_arch_update)
lemma flush_space_pd_at_asid [wp]:
@ -671,14 +671,6 @@ lemma valid_arch_state_unmap_strg:
done
lemma valid_arch_objs_unmap_strg:
"valid_arch_objs s \<longrightarrow>
valid_arch_objs(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(ptr := None)\<rparr>\<rparr>)"
apply (clarsimp simp: valid_arch_objs_def)
apply (drule vs_lookup_clear_asid_table [rule_format])
apply blast
done
lemma valid_vspace_objs_unmap_strg:
"valid_vspace_objs s \<longrightarrow>
valid_vspace_objs(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(ptr := None)\<rparr>\<rparr>)"
@ -1045,9 +1037,8 @@ crunch valid_vs_lookup[wp]: set_vm_root_for_flush "valid_vs_lookup"
crunch valid_global_objs[wp]: set_vm_root_for_flush "valid_global_objs"
(simp: valid_global_objs_arch_update)
crunch arch_objs [wp]: set_vm_root_for_flush valid_arch_objs
(simp: valid_arch_objs_arch_update)
crunch vspace_objs [wp]: set_vm_root_for_flush valid_vspace_objs
(simp: valid_vspace_objs_arch_update)
crunch typ_at [wp]: flush_table "\<lambda>s. P (typ_at T p s)"
(simp: assertE_def whenE_def when_def wp: crunch_wps)
@ -1373,8 +1364,8 @@ lemma lookup_pd_slot_pd:
apply (simp add: pd_bits_def pageBits_def)
done
crunch arch_objs [wp]: flush_page valid_arch_objs
(simp: crunch_simps valid_arch_objs_arch_update)
crunch vspace_objs [wp]: flush_page valid_vspace_objs
(simp: crunch_simps valid_vspace_objs_arch_update)
crunch equal_mappings [wp]: flush_page equal_kernel_mappings
(simp: crunch_simps)
@ -1439,8 +1430,8 @@ lemma page_directory_at_aligned_pd_bits:
apply (simp add:pd_bits_def pageBits_def)
done
crunch arch_objs [wp]: flush_page valid_arch_objs
(simp: crunch_simps valid_arch_objs_arch_update)
crunch vspace_objs [wp]: flush_page valid_vspace_objs
(simp: crunch_simps valid_vspace_objs_arch_update)
definition
@ -1590,39 +1581,6 @@ definition
and K (0 < asid \<and> asid \<le> 2^asid_bits - 1)
and ([VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> p)"
(* FIXME Move to ArchInvariants *)
lemma valid_vspace_objs_stateI:
assumes 1: "valid_vspace_objs s"
assumes ko: "\<And>ko p. ko_at ko p s' \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s"
assumes arch: "graph_of (arm_asid_table (arch_state s')) \<subseteq> graph_of (arm_asid_table (arch_state s))"
assumes vao: "\<And>p ref ao'.
\<lbrakk> (ref \<rhd> p) s; (ref \<rhd> p) s'; \<forall>ao. ko_at (ArchObj ao) p s \<longrightarrow> valid_vspace_obj ao s;
ko_at (ArchObj ao') p s' \<rbrakk> \<Longrightarrow> valid_vspace_obj ao' s'"
shows "valid_vspace_objs s'"
using 1 unfolding valid_vspace_objs_def
apply clarsimp
apply (frule vs_lookup_stateI)
apply (erule ko)
apply (rule arch)
apply (erule allE, erule impE, fastforce)
apply (erule (3) vao)
done
(* FIXME Move to ArchAcc_AI *)
lemma valid_vspace_objs_arch_update:
"arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s) \<Longrightarrow>
valid_vspace_objs (arch_state_update f s) = valid_vspace_objs s"
apply (rule iffI)
apply (erule valid_vspace_objs_stateI)
apply (clarsimp simp: obj_at_def)
apply simp
apply simp
apply (erule valid_vspace_objs_stateI)
apply (clarsimp simp: obj_at_def)
apply simp
apply simp
done
lemma store_hw_asid_invs:
"\<lbrace>invs and
(\<lambda>s. arm_asid_map (arch_state s) asid = None \<and>
@ -2893,11 +2851,11 @@ lemma simpler_store_pde_def:
split: Structures_A.kernel_object.splits option.splits arch_kernel_obj.splits if_split_asm)
done
lemma pde_update_valid_arch_objs:
"[|valid_arch_objs s; valid_pde pde s; pde_ref pde = None; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))|]
==> valid_arch_objs
lemma pde_update_valid_vspace_objs:
"[|valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))|]
==> valid_vspace_objs
(s\<lparr>kheap := kheap s(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(ucast (p && mask pd_bits >> 2) := pde))))\<rparr>)"
apply (cut_tac pde=pde and p=p in store_pde_arch_objs_unmap)
apply (cut_tac pde=pde and p=p in store_pde_vspace_objs_unmap)
apply (clarsimp simp: valid_def)
apply (erule allE[where x=s])
apply (clarsimp simp: split_def simpler_store_pde_def obj_at_def a_type_def
@ -4569,7 +4527,7 @@ lemma unmap_page_unmapped:
apply ((simp add: obj_at_def a_type_def)+)[3]
apply (frule_tac p="rv" in valid_vspace_objsD)
apply ((simp add: obj_at_def)+)[2]
apply (fastforce simp: valid_arch_obj_def data_at_def)
apply (fastforce simp: data_at_def)
apply (fastforce simp: obj_at_def a_type_def pd_bits_def pageBits_def data_at_def
split: pde.splits)
apply (fastforce simp: obj_at_def a_type_def data_at_def)

2
proof/invariant-abstract/ARM_HYP/ArchAInvsPre.thy
View File

@ -73,7 +73,7 @@ lemma some_get_page_info_umapsD:
apply (case_tac ao, simp_all add: a_type_simps obj_at_def)[1]
apply (simp add: get_pt_info_def get_pt_entry_def)
apply (drule_tac x="(ucast ((p >> 12) && mask 9))" in spec)
apply (clarsimp simp: obj_at_def valid_arch_obj_def
apply (clarsimp simp: obj_at_def
split: pte.splits,intro exI conjI,simp_all)[1]
apply (frule obj_bits_data_at)
apply (clarsimp simp: pspace_aligned_def data_at_def)

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

@ -711,8 +711,7 @@ lemma create_mapping_entries_valid [wp]:
apply (cases sz)
apply (rule hoare_pre)
apply (wpsimp simp: valid_mapping_entries_def largePagePTE_offsets_def vspace_bits_defs
superSectionPDE_offsets_def
valid_arch_imp_valid_vspace_objs add.commute)+
superSectionPDE_offsets_def add.commute)+
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)
@ -1025,13 +1024,13 @@ crunch interrupt_states[wp]: set_pd "\<lambda>s. P (interrupt_states s)"
(wp: crunch_wps)
lemma set_pd_vspace_objs_unmap:
"\<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (PageDirectory pd') s) and
"\<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd') s) and
obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd')) \<subseteq> vs_refs ko) p\<rbrace>
set_pd p pd' \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
apply (simp add: set_pd_def)
apply (wp set_object_vspace_objs get_object_wp)
including unfold_objects
by (fastforce simp: a_type_def valid_arch_obj_def)
by (fastforce simp: a_type_def valid_vspace_obj_def)
declare graph_of_None_update[simp]
declare graph_of_Some_update[simp]
@ -2695,7 +2694,7 @@ lemma store_pde_arch_objs_unmap: (* ARMHYP *)
and K (pde_ref pde = None)\<rbrace>
store_pde p pde \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
apply (simp add: store_pde_def)
apply (wpsimp wp: set_pd_vspace_objs_unmap simp: valid_arch_obj_def)
apply (wpsimp wp: set_pd_vspace_objs_unmap)
apply (rule conjI)
apply clarsimp
apply (drule (1) valid_vspace_objsD, fastforce)
@ -3074,8 +3073,8 @@ lemma vs_refs_pages_subset: "vs_refs ko \<subseteq> vs_refs_pages ko"
lemma vs_refs_pages_subset2:
"\<lbrakk>vs_refs_pages ko \<subseteq> vs_refs_pages ko';
(\<forall>ao. (ko = ArchObj ao) \<longrightarrow> valid_arch_obj ao s);
(\<forall>ao'. (ko' = ArchObj ao') \<longrightarrow> valid_arch_obj ao' s)\<rbrakk>
(\<forall>ao. (ko = ArchObj ao) \<longrightarrow> valid_vspace_obj ao s);
(\<forall>ao'. (ko' = ArchObj ao') \<longrightarrow> valid_vspace_obj ao' s)\<rbrakk>
\<Longrightarrow> vs_refs ko \<subseteq> vs_refs ko'"
apply clarsimp
apply (drule (1) subsetD[OF _ subsetD[OF vs_refs_pages_subset]])
@ -3096,7 +3095,7 @@ lemma vs_refs_pages_subset2:
A="{(x, y). (pde_ref (fun x)) = Some y}"
and f="(\<lambda>(r, y). (VSRef (ucast r) (Some APageDirectory), y))" and x="(a,b)"])
apply simp
apply (clarsimp simp: pde_ref_def pde_ref_pages_def valid_arch_obj_def
apply (clarsimp simp: pde_ref_def pde_ref_pages_def
split: pde.splits)
apply (drule_tac x=a in spec)+
apply (simp add: valid_pde_def)
@ -3132,7 +3131,7 @@ lemma set_pd_global_mappings[wp]:
lemma set_pd_invs_unmap: (* ARMHYP *)
"\<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and
(\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (PageDirectory pd) s) and
(\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and
obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p and
obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and
(* obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd')
@ -3169,7 +3168,7 @@ lemma store_pde_invs_unmap:
apply (drule invs_valid_objs)
apply (fastforce simp: valid_objs_def dom_def obj_at_def valid_obj_def)
apply (rule conjI)
apply (clarsimp simp: valid_arch_obj_def)
apply (clarsimp)
apply (drule (1) valid_vspace_objsD, fastforce)
apply simp
apply (rule conjI)

28
proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy
View File

@ -347,12 +347,6 @@ lemma vs_lookup_pages':
apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def)
done
lemma arch_obj [simp]:
"valid_arch_obj ao s' = valid_arch_obj ao s"
by (cases ao, simp_all add: s'_def)
lemma obj_at [simp]:
"obj_at P p s' = obj_at P p s"
by (simp add: s'_def)
@ -371,14 +365,6 @@ lemma vspace_objs':
intro: vs_lookup_neq)
done
lemma arch_objs':
"valid_arch_objs s \<Longrightarrow> valid_arch_objs s'"
by (fastforce simp: valid_arch_objs_def
valid_vcpu_def
vspace_objs'
vs_lookup'
split: option.split)
lemma caps_of_state_s':
"caps_of_state s' = caps_of_state s"
by (rule caps_of_state_pspace, simp add: s'_def)
@ -591,20 +577,6 @@ lemma valid_asid_map_asid_upd_strg:
apply (erule (1) asid_update.valid_asid_map')
done
lemma valid_arch_objs_asid_upd_strg:
"valid_arch_objs s \<and>
ko_at (ArchObj (ASIDPool empty)) ap s \<and>
arm_asid_table (arch_state s) asid = None \<longrightarrow>
valid_arch_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
apply clarsimp
apply (subgoal_tac "asid_update ap asid s")
prefer 2
apply unfold_locales[1]
apply assumption+
apply (erule (1) asid_update.arch_objs')
done
lemma valid_vspace_objs_asid_upd_strg:
"valid_vspace_objs s \<and>
ko_at (ArchObj (ASIDPool empty)) ap s \<and>

2
proof/invariant-abstract/ARM_HYP/ArchCNodeInv_AI.thy
View File

@ -259,7 +259,7 @@ lemma invs_irq_state_independent[intro!, simp, CNodeInv_AI_assms]:
only_idle_def if_unsafe_then_cap_def valid_reply_caps_def
valid_reply_masters_def valid_global_refs_def valid_arch_state_def
valid_irq_node_def valid_irq_handlers_def valid_machine_state_def
valid_arch_objs_def valid_arch_caps_def
valid_arch_caps_def
valid_kernel_mappings_def equal_kernel_mappings_def
valid_asid_map_def
pspace_in_kernel_window_def cap_refs_in_kernel_window_def

3
proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy
View File

@ -316,9 +316,6 @@ lemma vs_lookup_pages_preserved:
(* FIXME: This is really horrible but I can't get the automated methods
to "get it". *)
(* lemma valid_arch_obj:
"\<And>ao p. \<lbrakk> valid_arch_obj ao s; ko_at (ArchObj ao) p s; (\<exists>\<rhd>p) s \<rbrakk> \<Longrightarrow>
valid_arch_obj ao (detype (untyped_range cap) s)" *)
lemma valid_vspace_obj:
"\<And>ao p. \<lbrakk> valid_vspace_obj ao s; ko_at (ArchObj ao) p s; (\<exists>\<rhd>p) s \<rbrakk> \<Longrightarrow>
valid_vspace_obj ao (detype (untyped_range cap) s)"

9
proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy
View File

@ -1465,9 +1465,6 @@ lemma invalidate_tlb_by_asid_pspace_aligned:
apply (simp add: invalidate_tlb_by_asid_def load_hw_asid_def | wp | wpc)+
done
crunch valid_arch_objs[wp]: invalidate_tlb_by_asid, page_table_mapped
"valid_arch_objs"
crunch cte_wp_at[wp]: invalidate_tlb_by_asid, page_table_mapped
"\<lambda>s. P (cte_wp_at P' p s)"
@ -1966,12 +1963,6 @@ lemma replaceable_or_arch_update_pg:
apply (auto simp: is_cap_simps is_arch_update_def cap_master_cap_simps)
done
(*lemma store_pde_arch_objs_invalid: (* ARMHYP do we need this? *)
"\<lbrace>valid_arch_objs\<rbrace> store_pde p InvalidPDE \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (wp store_pde_arch_objs_unmap)
apply (simp add: pde_ref_def)
done *)
lemma store_pde_vspace_objs_invalid:
"\<lbrace>valid_vspace_objs\<rbrace> store_pde p InvalidPDE \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
apply (wp store_pde_arch_objs_unmap)

206
proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
View File

@ -286,16 +286,6 @@ where
| "valid_vspace_obj (DataPage dev sz) = \<top>"
| "valid_vspace_obj (VCPU v) = \<top>"
definition
valid_arch_obj :: "arch_kernel_obj \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"valid_arch_obj ao \<equiv> case ao of
VCPU v \<Rightarrow> valid_vcpu v
| _ \<Rightarrow> valid_vspace_obj ao"
lemma valid_arch_imp_valid_vspace_obj: "valid_arch_obj ko s \<Longrightarrow> valid_vspace_obj ko s"
by (case_tac ko; clarsimp simp: valid_arch_obj_def valid_vspace_obj_def)
definition
wellformed_pte :: "pte \<Rightarrow> bool"
where
@ -452,27 +442,6 @@ where
"valid_vspace_objs \<equiv>
\<lambda>s. \<forall>p rs ao. (rs \<rhd> p) s \<longrightarrow> ko_at (ArchObj ao) p s \<longrightarrow> valid_vspace_obj ao s"
definition
valid_arch_objs :: "'z::state_ext state \<Rightarrow> bool" (* ARMHYP *)
where
"valid_arch_objs \<equiv> \<lambda>s. (\<forall>p v. ko_at (ArchObj (VCPU v)) p s \<longrightarrow> valid_vcpu v s) \<and> valid_vspace_objs s"
lemma valid_arch_imp_valid_vspace_objs: "valid_arch_objs s \<Longrightarrow> valid_vspace_objs s"
by (clarsimp simp: valid_arch_objs_def valid_vspace_objs_def valid_arch_imp_valid_vspace_obj)
lemma valid_arch_objs_lift:
"\<lbrace> valid_vspace_objs \<rbrace> f \<lbrace> \<lambda>_. valid_vspace_objs \<rbrace> \<Longrightarrow>
\<lbrace> \<lambda>s. \<forall>p v. ko_at (ArchObj (VCPU v)) p s \<longrightarrow> valid_vcpu v s \<rbrace> f
\<lbrace> \<lambda>_ s. \<forall>p v. ko_at (ArchObj (VCPU v)) p s \<longrightarrow> valid_vcpu v s \<rbrace>
\<Longrightarrow> \<lbrace> valid_arch_objs \<rbrace> f \<lbrace> \<lambda>_. valid_arch_objs \<rbrace>"
apply (clarsimp simp: valid_arch_objs_def)
apply (rule hoare_vcg_conj_lift; assumption?)
done
(**)
definition
pde_ref_pages :: "pde \<Rightarrow> obj_ref option"
where
@ -644,7 +613,9 @@ where
definition
valid_ao_at :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"valid_ao_at p \<equiv> \<lambda>s. \<exists>ao. ko_at (ArchObj ao) p s \<and> valid_arch_obj ao s"
"valid_ao_at p \<equiv> \<lambda>s. \<exists>ao. ko_at (ArchObj ao) p s \<and> (case ao of
VCPU v \<Rightarrow> valid_vcpu v
| _ \<Rightarrow> valid_vspace_obj ao) s"
fun
is_vspace_typ :: "a_type \<Rightarrow> bool"
@ -1043,25 +1014,6 @@ lemma valid_vspace_objsD:
"\<lbrakk> (ref \<rhd> p) s; ko_at (ArchObj ao) p s; valid_vspace_objs s \<rbrakk> \<Longrightarrow> valid_vspace_obj ao s"
by (fastforce simp add: valid_vspace_objs_def)
(* should work for unmap and non-arch ops *)
(*
lemma valid_arch_objs_stateI:
assumes 1: "valid_arch_objs s"
assumes ko: "\<And>ko p. ko_at ko p s' \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s"
assumes arch: "graph_of (arm_asid_table (arch_state s')) \<subseteq> graph_of (arm_asid_table (arch_state s))"
assumes vao: "\<And>p ref ao'.
\<lbrakk> (ref \<rhd> p) s; (ref \<rhd> p) s'; \<forall>ao. ko_at (ArchObj ao) p s \<longrightarrow> valid_arch_obj ao s;
ko_at (ArchObj ao') p s' \<rbrakk> \<Longrightarrow> valid_arch_obj ao' s'"
shows "valid_arch_objs s'"
using 1 unfolding valid_arch_objs_def valid_vspace_objs_def
apply clarsimp
apply (frule vs_lookup_stateI)
apply (erule ko)
apply (rule arch)
apply (erule allE, erule impE, fastforce)
apply (erule (3) vao)
done *)
lemma valid_vspace_objs_stateI:
assumes 1: "valid_vspace_objs s"
assumes ko: "\<And>ko p. ko_at ko p s' \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s"
@ -1090,22 +1042,6 @@ lemma valid_arch_cap_typ:
definition is_avcpu_aatyp :: "arch_kernel_obj \<Rightarrow> bool"
where "is_avcpu_aatyp ob \<equiv> aa_type ob = AVCPU"
lemma valid_arch_obj_typ:
assumes P: "\<And>p T. \<lbrace>\<lambda>s. (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. (typ_at (AArch T) p s)\<rbrace>"
shows "\<lbrace>\<lambda>s. aa_type ob \<noteq> AVCPU \<longrightarrow> valid_arch_obj ob s\<rbrace> f \<lbrace>\<lambda>rv s. aa_type ob \<noteq> AVCPU \<longrightarrow> valid_arch_obj ob s\<rbrace>"
apply (cases ob, simp_all add: aa_type_def valid_arch_obj_def)
apply (rule hoare_vcg_const_Ball_lift [OF P])
apply (rule hoare_vcg_all_lift)
apply (rename_tac "fun" x)
apply (case_tac "fun x"; simp_all add: data_at_def hoare_vcg_prop P)
apply (wp hoare_vcg_disj_lift P)+
apply (rule hoare_vcg_all_lift)
apply (rename_tac "fun" x)
apply (case_tac "fun x";simp_all add: data_at_def hoare_vcg_prop P)
apply (wp hoare_vcg_disj_lift P)+
done
lemma valid_vspace_obj_typ:
assumes P: "\<And>p T. \<lbrace>\<lambda>s. (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. (typ_at (AArch T) p s)\<rbrace>"
shows "\<lbrace>\<lambda>s. valid_vspace_obj ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_vspace_obj ob s\<rbrace>"
@ -1121,24 +1057,6 @@ lemma valid_vspace_obj_typ:
apply (wp hoare_vcg_disj_lift P)+
done
lemma valid_arch_obj_typ_gen: (* ARMHYP *)
assumes P: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
and t: "\<And>P p. \<lbrace>\<lambda>s. P (typ_at ATCB p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at ATCB p s)\<rbrace>"
shows "\<lbrace>\<lambda>s. valid_arch_obj ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_arch_obj ob s\<rbrace>"
apply (cases ob, simp_all add: valid_arch_obj_def)
apply (rule hoare_vcg_const_Ball_lift [OF P])
apply (rule hoare_vcg_all_lift)
apply (rename_tac "fun" x)
apply (case_tac "fun x"; simp_all add: data_at_def hoare_vcg_prop P)
apply (wp hoare_vcg_disj_lift P)+
apply (rule hoare_vcg_all_lift)
apply (rename_tac "fun" x)
apply (case_tac "fun x";simp_all add: data_at_def hoare_vcg_prop P)
apply (wp hoare_vcg_disj_lift P)+
apply (rename_tac v)
apply (case_tac "vcpu_tcb v"; simp add: valid_vcpu_def; wp t)
done
lemma atyp_at_eq_kheap_obj:
"typ_at (AArch AASIDPool) p s \<longleftrightarrow> (\<exists>f. kheap s p = Some (ArchObj (ASIDPool f)))"
"typ_at (AArch APageTable) p s \<longleftrightarrow> (\<exists>pt. kheap s p = Some (ArchObj (PageTable pt)))"
@ -1185,20 +1103,6 @@ lemma wellformed_arch_typ:
apply (rule conjI; clarsimp; wp P)
done
lemma valid_arch_obj_pspaceI:
"\<lbrakk> valid_arch_obj obj s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_arch_obj obj s'"
apply (cases obj, simp_all add: valid_arch_obj_def)
apply (simp add: obj_at_def)
apply (erule allEI)
apply (rename_tac "fun" x)
apply (case_tac "fun x", simp_all add: obj_at_def data_at_def)
apply (erule allEI)
apply (rename_tac "fun" x)
apply (case_tac "fun x", simp_all add: obj_at_def data_at_def)
apply (rename_tac v)
apply (case_tac "vcpu_tcb v"; simp add: valid_vcpu_def obj_at_def)
done
lemma valid_vspace_obj_pspaceI:
"\<lbrakk> valid_vspace_obj obj s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_vspace_obj obj s'"
apply (cases obj, simp_all)
@ -1278,13 +1182,9 @@ lemma valid_vspace_obj_update [iff]:
"valid_vspace_obj ao (f s) = valid_vspace_obj ao s"
by (cases ao) auto
lemma valid_arch_obj_update [iff]:
"valid_arch_obj ao (f s) = valid_arch_obj ao s"
by (cases ao) (auto simp: valid_arch_obj_def)
lemma valid_ao_at_update [iff]:
"valid_ao_at p (f s) = valid_ao_at p s"
by (simp add: valid_ao_at_def)
by (simp add: valid_ao_at_def split: arch_kernel_obj.split)
lemma valid_vso_at_update [iff]:
"valid_vso_at p (f s) = valid_vso_at p s"
@ -1371,10 +1271,6 @@ lemma valid_table_caps_update [iff]:
"valid_table_caps (f s) = valid_table_caps s"
by (simp add: valid_table_caps_def arch)
lemma valid_arch_objs_update' [iff]:
"valid_arch_objs (f s) = valid_arch_objs s"
by (simp add: valid_arch_objs_def valid_vspace_objs_def)
lemma valid_vspace_objs_update' [iff]:
"valid_vspace_objs (f s) = valid_vspace_objs s"
by (simp add: valid_vspace_objs_def)
@ -1496,12 +1392,7 @@ lemma physical_arch_cap_has_ref:
subsection "vs_lookup"
(*
lemma vs_lookup1_ko_at_dest:
"\<lbrakk> ((ref, p) \<rhd>1 (ref', p')) s; ko_at (ArchObj ao) p s; valid_arch_obj ao s \<rbrakk> \<Longrightarrow>
\<exists>ao'. ko_at (ArchObj ao') p' s \<and> (\<exists>tp. vs_ref_aatype (hd ref') = Some tp
\<and> aa_type ao = tp)"
*)
lemma vs_lookup1_ko_at_dest: (* ARMHYP *)
"\<lbrakk> ((ref, p) \<rhd>1 (ref', p')) s; ko_at (ArchObj ao) p s; valid_vspace_obj ao s \<rbrakk> \<Longrightarrow>
\<exists>ao'. ko_at (ArchObj ao') p' s \<and> (\<exists>tp. vs_ref_aatype (hd ref') = Some tp
@ -1662,16 +1553,7 @@ lemma vs_lookup_pages_ptI:
vs_refs_pages_def graph_of_def image_def
split: if_split_asm)
(* ARMHYP: add VCPU? *)
(*
lemma stronger_arch_objsD_lemma:
"\<lbrakk>valid_arch_objs s; r \<in> vs_lookup s; (r,r') \<in> (vs_lookup1 s)\<^sup>+ \<rbrakk>
\<Longrightarrow> \<exists>ao. ko_at (ArchObj ao) (snd r') s \<and>
valid_arch_obj ao s"
*)
lemma stronger_vspace_objsD_lemma: (* ARMHYP *)
lemma stronger_vspace_objsD_lemma:
"\<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r,r') \<in> (vs_lookup1 s)\<^sup>+ \<rbrakk>
\<Longrightarrow> \<exists>ao. ko_at (ArchObj ao) (snd r') s \<and>
valid_vspace_obj ao s"
@ -1693,13 +1575,6 @@ lemma stronger_vspace_objsD_lemma: (* ARMHYP *)
apply (drule (2) valid_vspace_objsD)
apply fastforce
done
(*
lemma stronger_arch_objsD:
"\<lbrakk> (ref \<rhd> p) s;
valid_arch_objs s;
valid_asid_table (arm_asid_table (arch_state s)) s \<rbrakk> \<Longrightarrow>
\<exists>ao. ko_at (ArchObj ao) p s \<and>
valid_arch_obj ao s" *)
lemma stronger_vspace_objsD:
"\<lbrakk> (ref \<rhd> p) s;
@ -1996,12 +1871,6 @@ lemma aa_type_pdD:
by (clarsimp simp: aa_type_def
split: arch_kernel_obj.splits if_split_asm)
lemma empty_table_is_valid: (* ARMHYP? *)
"\<lbrakk>empty_table {} (ArchObj ao);
valid_arch_state s\<rbrakk>
\<Longrightarrow> valid_arch_obj ao s"
by (cases ao, simp_all add: empty_table_def valid_arch_obj_def)
lemma empty_table_pde_refD:
"\<lbrakk> pde_ref (pd x) = Some r; empty_table S (ArchObj (PageDirectory pd)) \<rbrakk> \<Longrightarrow>
r \<in> S"
@ -2060,14 +1929,8 @@ lemma vs_lookup_pages_induct:
apply (drule (1) vs_lookup_pages_trancl_step)
apply (erule (2) s)
done
(*
lemma vs_ref_order:
"\<lbrakk> (r \<rhd> p) s; valid_arch_objs s; valid_arch_state s \<rbrakk>
\<Longrightarrow> \<exists>tp. r \<noteq> [] \<and> typ_at (AArch tp) p s \<and>
rev (Some tp # map vs_ref_aatype r)
\<le> [None, Some AASIDPool, Some APageDirectory, Some APageTable]"
*)
lemma vs_ref_order: (* ARMHYP *)
"\<lbrakk> (r \<rhd> p) s; valid_vspace_objs s; valid_arch_state s \<rbrakk>
\<Longrightarrow> \<exists>tp. r \<noteq> [] \<and> typ_at (AArch tp) p s \<and>
rev (Some tp # map vs_ref_aatype r)
@ -2108,36 +1971,6 @@ lemma valid_pde_lift2:
shows "\<lbrace>\<lambda>s. Q s \<and> valid_pde pde s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pde pde s\<rbrace>"
by (cases pde) (simp add: data_at_def | wp x hoare_vcg_disj_lift)+
(* ARMHYP do we need this?
lemma vcpu_not_vspace_obj: "\<And>s p rs ao. (rs \<rhd> p) s \<Longrightarrow> ko_at (ArchObj ao) p s \<Longrightarrow> \<not> vcpu_at p s"
apply (simp add: vs_lookup_def Image_iff)
apply (clarsimp simp: obj_at_def vs_asid_refs_def graph_of_def vs_lookup1_def)
apply (drule_tac Collect_case_prodD)
apply (simp add: mem_Collect_eq)
apply (drule rtranclpD)
apply clarsimp
apply (erule vs_lookup_induct)
apply (drule_tac vs_lookup_apI)
apply (clarsimp simp: obj_at_def)
apply (simp add: vs_lookup_def obj_at_def)
*)
lemma valid_arch_obj_typ2:
assumes P: "\<And>P p T. \<lbrace>\<lambda>s. Q s \<and> P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
shows "\<lbrace>\<lambda>s. Q s \<and> (aa_type ob \<noteq> AVCPU \<longrightarrow> valid_arch_obj ob s)\<rbrace> f \<lbrace>\<lambda>rv s. aa_type ob \<noteq> AVCPU \<longrightarrow> valid_arch_obj ob s\<rbrace>"
apply (cases ob, simp_all add: aa_type_def valid_arch_obj_def)
apply (wp hoare_vcg_const_Ball_lift [OF P], simp)
apply (rule hoare_pre, wp hoare_vcg_all_lift valid_pte_lift2 P)
apply clarsimp
apply assumption
apply clarsimp
apply (wp hoare_vcg_all_lift valid_pde_lift2 P)
apply clarsimp
apply assumption
apply clarsimp
apply wp+
done
lemma valid_vspace_obj_typ2:
assumes P: "\<And>P p T. \<lbrace>\<lambda>s. Q s \<and> P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
@ -2155,11 +1988,7 @@ lemma valid_vspace_obj_typ2:
apply wp+
done
(*
lemma valid_arch_objsI [intro?]:
"(\<And>p ao. \<lbrakk> (\<exists>\<rhd> p) s; ko_at (ArchObj ao) p s \<rbrakk> \<Longrightarrow> valid_arch_obj ao s) \<Longrightarrow> valid_arch_objs s"
by (simp add: valid_arch_objs_def)
*)
lemma valid_vspace_objsI [intro?]:
"(\<And>p ao. \<lbrakk> (\<exists>\<rhd> p) s; ko_at (ArchObj ao) p s \<rbrakk> \<Longrightarrow> valid_vspace_obj ao s) \<Longrightarrow> valid_vspace_objs s"
by (simp add: valid_vspace_objs_def)
@ -2282,20 +2111,6 @@ lemma valid_vspace_objs_lift:
apply (rule valid_vspace_obj_typ [OF z], auto)
done
(* ARMHYP unnecessary? *)
lemma valid_arch_objs_typ_at_lift:
assumes x: "\<And>P. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>"
assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
and t: "\<And>P p. \<lbrace>\<lambda>s. P (typ_at ATCB p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at ATCB p s)\<rbrace>"
and y: "\<And>ao p. \<lbrace>\<lambda>s. \<not> ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> ko_at (ArchObj ao) p s\<rbrace>"
shows "\<lbrace>valid_arch_objs\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_objs\<rbrace>"
apply (rule valid_arch_objs_lift)
apply (rule valid_vspace_objs_lift; wp x z y)
apply (rule hoare_vcg_all_lift)+
apply (rule hoare_convert_imp[OF y])
apply (case_tac "vcpu_tcb v"; simp add: valid_vcpu_def; (wp t)+)
done
lemma valid_validate_vm_rights[simp]:
"validate_vm_rights rs \<in> valid_vm_rights"
and validate_vm_rights_subseteq[simp]:
@ -2371,11 +2186,6 @@ lemma wellformed_arch_default:
unfolding wellformed_arch_obj_def default_arch_object_def
by (cases aobject_type; simp add: default_vcpu_def valid_vcpu_def)
lemma valid_arch_obj_default':
"valid_arch_obj (default_arch_object aobject_type dev us) s"
unfolding default_arch_object_def
by (cases aobject_type; simp add: default_vcpu_def valid_vcpu_def valid_arch_obj_def)
lemma valid_vspace_obj_default':
"valid_vspace_obj (default_arch_object aobject_type dev us) s"
unfolding default_arch_object_def

9
proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy
View File

@ -391,15 +391,6 @@ lemma transfer_caps_non_null_cte_wp_at:
crunch cte_wp_at[wp,Ipc_AI_assms]: do_fault_transfer "cte_wp_at P p"
lemma set_cap_valid_arch_objs [wp, Ipc_AI_assms]:
"\<lbrace>valid_arch_objs\<rbrace> set_cap a b \<lbrace>\<lambda>_. valid_arch_objs \<rbrace>"
apply (rule valid_arch_objs_typ_at_lift)
apply (wp set_cap_typ_at)+
apply (rule set_cap.aobj_at)
apply (fastforce simp: arch_obj_pred_def non_arch_obj_def
split: kernel_object.split arch_kernel_obj.splits)
done
lemma do_normal_transfer_non_null_cte_wp_at [Ipc_AI_assms]:
assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c"
shows "\<lbrace>valid_objs and cte_wp_at (P and (op \<noteq> cap.NullCap)) ptr\<rbrace>

26
proof/invariant-abstract/ARM_HYP/ArchKHeap_AI.thy
View File

@ -37,11 +37,6 @@ lemma valid_vspace_is_vspace_lift:
apply (rule hoare_vcg_conj_lift hoare_vcg_disj_lift | wp P | simp )+
done
lemma valid_arch_objs_lift: "valid_pspace s \<Longrightarrow> valid_vspace_objs s \<Longrightarrow> valid_arch_objs s"
apply (clarsimp simp add: valid_pspace_def valid_objs_def valid_arch_objs_def obj_at_def)
apply (erule_tac x=p in ballE; clarsimp simp add: valid_obj_def)
done
lemma obj_at_split: "(obj_at (P xo) p s \<and> (Q xo)) = obj_at (\<lambda>ko. P xo ko \<and> Q xo) p s"
by (auto simp: obj_at_def)
@ -374,7 +369,7 @@ lemma set_object_atyp_at:
lemma hoare_post_imp_conj_disj: "(\<lbrace> \<lambda>s. R \<rbrace> f \<lbrace> \<lambda>_ s. P \<longrightarrow> Q \<rbrace>) = (\<lbrace> \<lambda>s. R \<rbrace> f \<lbrace> \<lambda>_ s. \<not> P \<or> Q \<rbrace>)"
by (subst imp_conv_disj, auto)
lemma set_object_vspace_objs:
lemma set_object_vspace_objs: (* used in set_pd_arch_objs_unmap in ArchAcc_AI *) (* ARMHYP *)
"\<lbrace>valid_vspace_objs and typ_at (a_type ko) p and
obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p and
(\<lambda>s. case ko of ArchObj ao \<Rightarrow> (\<exists>\<rhd>p)s \<longrightarrow> valid_vspace_obj ao s
@ -731,23 +726,6 @@ lemma state_hyp_refs_of_tcb_state_update:
apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
done
lemma valid_arch_obj_same_type:
"\<lbrakk>valid_arch_obj ao s; kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
\<Longrightarrow> valid_arch_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> ko')\<rparr>)"
apply (induction ao rule: arch_kernel_obj.induct;
clarsimp simp: valid_arch_obj_def typ_at_same_type)
apply (rule hoare_to_pure_kheap_upd; assumption?)
apply (rule valid_pte_lift, assumption)
apply blast
apply (simp add: obj_at_def)
apply (rule hoare_to_pure_kheap_upd; assumption?)
apply (rule valid_pde_lift, assumption)
apply blast
apply (simp add: obj_at_def)
apply (simp add: valid_vcpu_def split: option.splits)
apply (drule typ_at_same_type[rotated]; assumption)
done
lemma valid_vcpu_lift:
assumes x: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
assumes t: "\<And>p. \<lbrace>typ_at ATCB p\<rbrace> f \<lbrace>\<lambda>rv. typ_at ATCB p\<rbrace>"
@ -773,7 +751,7 @@ lemma wellformed_arch_obj_same_type:
"\<lbrakk> wellformed_arch_obj ao s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
\<Longrightarrow> wellformed_arch_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
by (induction ao rule: arch_kernel_obj.induct;
clarsimp simp: valid_arch_obj_def typ_at_same_type valid_vcpu_same_type)
clarsimp simp: typ_at_same_type valid_vcpu_same_type)
lemma default_arch_object_not_live: "\<not> live (ArchObj (default_arch_object aty dev us))"

2
proof/invariant-abstract/ARM_HYP/ArchKernelInit_AI.thy
View File

@ -331,7 +331,7 @@ lemma invs_A:
apply (clarsimp simp: valid_machine_state_def init_A_st_def
init_machine_state_def init_underlying_memory_def)
apply (rule conjI)
apply (clarsimp simp: valid_arch_objs_def obj_at_def state_defs valid_vspace_objs_def)
apply (clarsimp simp: obj_at_def state_defs valid_vspace_objs_def)
apply (rule conjI)
apply (clarsimp simp: valid_arch_caps_def)
apply (rule conjI)

11
proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy
View File

@ -1461,12 +1461,11 @@ lemma decode_mmu_invocation_valid_pdpt[wp]:
| simp only: obj_at_def)+)
apply (rule_tac Q'="\<lambda>rv. \<exists>\<rhd> rv and K (is_aligned rv pd_bits) and
(\<exists>\<rhd> (lookup_pd_slot rv (args ! 0) && ~~ mask pd_bits)) and
valid_arch_objs and pspace_aligned and valid_pdpt_objs"
valid_vspace_objs and pspace_aligned and valid_pdpt_objs"
and f="find_pd_for_asid p" for p
in hoare_post_imp_R)
apply (wp| simp)+
apply (fastforce simp:pd_bits_def pageBits_def pde_bits_def
intro: valid_arch_imp_valid_vspace_objs)
apply (fastforce simp:pd_bits_def pageBits_def pde_bits_def)
apply ((wp get_pde_wp
ensure_safe_mapping_ensures[THEN hoare_post_imp_R]
create_mapping_entries_safe check_vp_wpR
@ -1482,12 +1481,12 @@ lemma decode_mmu_invocation_valid_pdpt[wp]:
| simp only: obj_at_def)+)
apply (rule_tac Q'="\<lambda>rv. \<exists>\<rhd> rv and K (is_aligned rv pd_bits) and
(\<exists>\<rhd> (lookup_pd_slot rv (snd pa) && ~~ mask pd_bits)) and
valid_arch_objs and pspace_aligned and valid_pdpt_objs and
valid_vspace_objs and pspace_aligned and valid_pdpt_objs and
K ((snd pa) < kernel_base)"
and f="find_pd_for_asid p" for p
in hoare_post_imp_R)
apply (wp| simp)+
apply (auto simp:pd_bits_def pageBits_def intro: valid_arch_imp_valid_vspace_objs)[1]
apply (auto simp:pd_bits_def pageBits_def)[1]
apply ((wp get_pde_wp
ensure_safe_mapping_ensures[THEN hoare_post_imp_R]
create_mapping_entries_safe check_vp_wpR
@ -1512,7 +1511,7 @@ lemma decode_mmu_invocation_valid_pdpt[wp]:
del: hoare_True_E_R
split del: if_split
| simp only: obj_at_def)+)
apply (auto simp:valid_cap_simps intro: valid_arch_objs_lift)
apply (auto simp:valid_cap_simps)
done
qed

61
proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy
View File

@ -293,10 +293,6 @@ lemma valid_vs_lookupE:
\<Longrightarrow> valid_vs_lookup s'"
by (simp add: valid_vs_lookup_def, blast)
(*
lemma find_free_hw_asid_arch_objs [wp]:
"\<lbrace>valid_arch_objs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>asid. valid_arch_objs\<rbrace>" *)
lemma find_free_hw_asid_arch_objs [wp]:
"\<lbrace>valid_vspace_objs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>asid. valid_vspace_objs\<rbrace>"
apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def invalidate_asid_def
@ -498,14 +494,6 @@ crunch valid_arch [wp]: flush_space valid_arch_state
crunch valid_objs [wp]: flush_space valid_objs
(*
lemma invalidate_hw_asid_arch_objs [wp]:
"\<lbrace>valid_arch_objs\<rbrace> invalidate_hw_asid_entry asid \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (simp add: invalidate_hw_asid_entry_def)
apply wp
apply (simp add: valid_arch_objs_arch_update)
done
*)
lemma invalidate_hw_asid_vspace_objs [wp]:
"\<lbrace>valid_vspace_objs\<rbrace> invalidate_hw_asid_entry asid \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
@ -555,13 +543,6 @@ lemma flush_space_asid_map[wp]:
done
lemma flush_space_arch_objs[wp]:
"\<lbrace>valid_arch_objs\<rbrace> flush_space space \<lbrace>\<lambda>rv. valid_arch_objs\<rbrace>"
apply (simp add: flush_space_def)
apply (wp load_hw_asid_wp | wpc | simp | rule_tac Q="\<lambda>_. valid_arch_objs" in hoare_strengthen_post)+
done
crunch typ_at [wp]: invalidate_asid_entry "\<lambda>s. P (typ_at T p s)"
@ -614,10 +595,6 @@ lemma invalidate_asid_entry_invalidates:
apply (erule (1) notE)
done
(*
crunch arch_objs [wp]: invalidate_asid_entry valid_arch_objs
(simp: valid_arch_objs_arch_update)
*)
crunch vspace_objs [wp]: invalidate_asid_entry valid_vspace_objs
(simp: valid_vspace_objs_arch_update)
@ -801,12 +778,6 @@ lemma valid_arch_state_unmap_strg:
apply (clarsimp simp: inj_on_def split: option.split)
done
(*
lemma valid_arch_objs_unmap_strg:
"valid_arch_objs s \<longrightarrow>
valid_arch_objs(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(ptr := None)\<rparr>\<rparr>)"
*)
lemma valid_vspace_objs_unmap_strg:
"valid_vspace_objs s \<longrightarrow>
valid_vspace_objs(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(ptr := None)\<rparr>\<rparr>)"
@ -1165,10 +1136,6 @@ lemma valid_vs_lookup_arch_update:
crunch valid_vs_lookup[wp]: set_vm_root_for_flush "valid_vs_lookup"
(simp: valid_vs_lookup_arch_update)
(*
crunch arch_objs [wp]: set_vm_root_for_flush valid_arch_objs
(simp: valid_arch_objs_arch_update) *)
crunch vspace_objs [wp]: set_vm_root_for_flush valid_vspace_objs
(simp: valid_vspace_objs_arch_update)
@ -1208,13 +1175,6 @@ crunch aligned [wp]: set_vm_root pspace_aligned
crunch aligned [wp]: flush_table pspace_aligned
(simp: crunch_simps whenE_def when_def wp: crunch_wps)
(*
lemma find_pd_for_asid_page_directory [wp]:
"\<lbrace>valid_arch_objs\<rbrace>
find_pd_for_asid asid
\<lbrace>\<lambda>pd. page_directory_at pd\<rbrace>, -"
*)
lemma find_pd_for_asid_page_directory [wp]:
"\<lbrace>valid_vspace_objs\<rbrace>
find_pd_for_asid asid
@ -1249,13 +1209,6 @@ lemma find_pd_for_asid_lookup[wp]:
apply auto
done
(*
lemma find_pd_for_asid_pde [wp]:
"\<lbrace>valid_arch_objs and pspace_aligned\<rbrace>
find_pd_for_asid asid
\<lbrace>\<lambda>pd. pde_at (pd + (vptr >> pageBits + pt_bits - pte_bits << pde_bits))\<rbrace>, -"
*)
lemma find_pd_for_asid_pde [wp]:
"\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace>
find_pd_for_asid asid
@ -1899,11 +1852,6 @@ lemma lookup_pd_slot_pd:
apply (simp add: vspace_bits_defs)
done
(*
crunch arch_objs [wp]: flush_page valid_arch_objs
(simp: crunch_simps valid_arch_objs_arch_update)
*)
lemma vcpu_switch_valid_vspace_objs[wp]:
"\<lbrace>valid_vspace_objs\<rbrace> vcpu_switch vcpu \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
apply (simp add: vcpu_switch_def)
@ -1989,10 +1937,7 @@ lemma page_directory_at_aligned_pd_bits:
apply (drule(1) pspace_alignedD)
apply (simp add:pd_bits_def pageBits_def)
done
(*
crunch arch_objs [wp]: flush_page valid_arch_objs
(simp: crunch_simps valid_arch_objs_arch_update)
*)
crunch vspace_objs [wp]: flush_page valid_vspace_objs
(simp: crunch_simps valid_vspace_objs_arch_update)
@ -3862,7 +3807,7 @@ lemma set_pd_invs_unmap':
set_pd_vspace_objs_unmap set_pd_valid_vs_lookup_map[where T=T and S="{}" and T'=T' and S'=S']
valid_irq_handlers_lift
set_pd_unmap_mappings set_pd_equal_kernel_mappings_triv)
apply (clarsimp simp: valid_arch_obj_def cte_wp_at_caps_of_state valid_arch_caps_def valid_objs_caps obj_at_def
apply (clarsimp simp: cte_wp_at_caps_of_state valid_arch_caps_def valid_objs_caps obj_at_def
del: disjCI)
apply (rule conjI, clarsimp)
apply (rule conjI)
@ -4055,7 +4000,7 @@ lemma simpler_store_pde_def:
split: Structures_A.kernel_object.splits option.splits arch_kernel_obj.splits if_split_asm)
done
lemma pde_update_valid_arch_objs:
lemma pde_update_valid_vspace_objs:
"[|valid_vspace_objs s; valid_pde pde s; pde_ref pde = None;
kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))|]
==> valid_vspace_objs

2
proof/invariant-abstract/BCorres2_AI.thy
View File

@ -166,8 +166,6 @@ lemma valid_irq_handlers[wp]: "I valid_irq_handlers" by (rule lift_inv,simp)
lemma valid_machine_state[wp]: "I valid_machine_state" by (rule lift_inv,simp)
lemma valid_arch_objs[wp]: "I valid_arch_objs" by (rule lift_inv,simp)
lemma valid_vspace_objs[wp]: "I valid_vspace_objs" by (rule lift_inv,simp)
lemma valid_arch_caps[wp]: "I valid_arch_caps" by (rule lift_inv,simp)

3
proof/invariant-abstract/CNodeInv_AI.thy
View File

@ -1843,9 +1843,6 @@ crunch vspace_objs [wp]: cap_swap "valid_vspace_objs"
crunch valid_global_objs [wp]: cap_swap "valid_global_objs"
crunch valid_global_vspace_mappings [wp]: cap_swap "valid_global_vspace_mappings"
(*
crunch arch_objs [wp]: empty_slot "valid_arch_objs"
*)
context CNodeInv_AI begin

2
proof/invariant-abstract/Detype_AI.thy
View File

@ -816,7 +816,7 @@ lemma invariants:
shows "(invs and untyped_children_in_mdb)
(detype (untyped_range cap) (clear_um (untyped_range cap) s))"
using detype_invs_lemmas detype_invs_assms ct_act
by (simp add: invs_def valid_state_def valid_pspace_def valid_arch_imp_valid_vspace_objs
by (simp add: invs_def valid_state_def valid_pspace_def
detype_clear_um_independent clear_um.state_refs_update clear_um.state_hyp_refs_update)
end

21
proof/invariant-abstract/Invariants_AI.thy
View File

@ -36,12 +36,10 @@ requalify_consts
wellformed_vspace_obj
wellformed_arch_obj
valid_asid_map
valid_arch_obj
valid_vspace_obj
valid_arch_tcb
valid_arch_state
valid_arch_objs
valid_vspace_objs
valid_arch_caps
valid_global_objs
@ -71,11 +69,7 @@ requalify_facts
idle_global
valid_ipc_buffer_cap_null
valid_arch_cap_typ
valid_arch_obj_typ
valid_vspace_obj_typ
valid_arch_obj_typ_gen
valid_arch_imp_valid_vspace_obj
valid_arch_imp_valid_vspace_objs
arch_kobj_size_bounded
global_refs_lift
valid_arch_state_lift
@ -84,7 +78,6 @@ requalify_facts
acap_rights_update_id
physical_arch_cap_has_ref
wellformed_arch_default
valid_arch_obj_default'
valid_vspace_obj_default'
vs_lookup1_stateI2
vs_lookup_pages1_stateI2
@ -905,7 +898,6 @@ where
and valid_irq_handlers
and valid_irq_states
and valid_machine_state
(* and valid_arch_objs *)
and valid_vspace_objs
and valid_arch_caps
and valid_global_objs
@ -989,7 +981,7 @@ abbreviation(input)
and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap
and valid_reply_caps and valid_reply_masters and valid_global_refs
and valid_arch_state and valid_machine_state and valid_irq_states
and valid_irq_node and valid_irq_handlers and valid_vspace_objs (* and valid_arch_objs *)
and valid_irq_node and valid_irq_handlers and valid_vspace_objs
and valid_arch_caps and valid_global_objs and valid_kernel_mappings
and equal_kernel_mappings and valid_asid_map
and valid_global_vspace_mappings
@ -1610,7 +1602,6 @@ end
context begin interpretation Arch .
requalify_facts
valid_arch_cap_pspaceI
valid_arch_obj_pspaceI
end
lemma valid_cap_pspaceI:
@ -1629,7 +1620,7 @@ lemma valid_obj_pspaceI:
apply (auto simp add: valid_ntfn_def valid_cs_def valid_tcb_def valid_ep_def
valid_tcb_state_def pred_tcb_at_def valid_bound_ntfn_def
valid_bound_tcb_def wellformed_arch_pspace
intro: obj_at_pspaceI valid_cap_pspaceI valid_arch_obj_pspaceI valid_arch_tcb_pspaceI
intro: obj_at_pspaceI valid_cap_pspaceI valid_arch_tcb_pspaceI
split: ntfn.splits endpoint.splits
thread_state.splits option.split
| auto split: kernel_object.split)+
@ -2249,7 +2240,7 @@ lemma valid_obj_typ:
shows "\<lbrace>\<lambda>s. valid_obj p ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_obj p ob s\<rbrace>"
apply (case_tac ob, simp_all add: valid_obj_def P P [where P=id, simplified]
wellformed_arch_typ
valid_cs_typ valid_tcb_typ valid_ep_typ valid_ntfn_typ valid_arch_obj_typ_gen)
valid_cs_typ valid_tcb_typ valid_ep_typ valid_ntfn_typ)
done
lemma valid_irq_node_typ:
@ -2537,10 +2528,6 @@ context p_arch_update_eq begin
interpretation Arch_p_arch_update_eq f ..
lemma valid_arch_objs_update [iff]:
"valid_arch_objs (f s) = valid_arch_objs s"
by (simp add: valid_arch_objs_def valid_vspace_objs_def)
lemma valid_vspace_objs_update [iff]:
"valid_vspace_objs (f s) = valid_vspace_objs s"
by (simp add: valid_vspace_objs_def)
@ -2825,7 +2812,7 @@ lemmas abs_typ_at_lifts =
ep_at_typ_at ntfn_at_typ_at tcb_at_typ_at
cap_table_at_typ_at
valid_tcb_state_typ valid_cte_at_typ valid_ntfn_typ
valid_ep_typ valid_cs_typ valid_arch_obj_typ valid_untyped_typ
valid_ep_typ valid_cs_typ valid_untyped_typ
valid_tcb_typ valid_obj_typ valid_cap_typ valid_vspace_obj_typ
lemma valid_idle_lift:

16
proof/invariant-abstract/Ipc_AI.thy
View File

@ -297,8 +297,6 @@ locale Ipc_AI =
\<lbrace>valid_vspace_objs::'state_ext state \<Rightarrow> bool\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>"
assumes set_cap_valid_arch_objs[wp]:
"\<And> cap p. \<lbrace>valid_arch_objs ::'state_ext state \<Rightarrow> bool \<rbrace> set_cap cap p \<lbrace>\<lambda>_. valid_arch_objs \<rbrace>"
assumes arch_get_sanitise_register_info_typ_at[wp]:
"\<And> P T p t.
\<lbrace>\<lambda>s::'state_ext state. P (typ_at T p s)\<rbrace>
@ -943,20 +941,6 @@ lemma transfer_caps_loop_irq_handlers[wp]:
apply clarsimp
done
crunch valid_arch_objs [wp]: set_extra_badge valid_arch_objs
crunch arch_objs [wp]: set_untyped_cap_as_full "valid_arch_objs :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps simp: crunch_simps ignore: set_object set_cap)
crunch arch_objs [wp]: cap_insert "valid_arch_objs :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps simp: crunch_simps ignore: set_object set_cap)
lemma transfer_caps_loop_arch_objs[wp]:
"\<lbrace>valid_arch_objs :: 'state_ext state \<Rightarrow> bool\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>rv. valid_arch_objs\<rbrace>"
by (rule transfer_caps_loop_pres; wp)
crunch valid_arch_caps [wp]: set_extra_badge valid_arch_caps

8
proof/invariant-abstract/KHeap_AI.thy
View File

@ -1748,14 +1748,6 @@ lemma dom_objs [wp]:
done
lemma do_machine_op_arch_objs [wp]:
"\<lbrace>valid_arch_objs\<rbrace> do_machine_op f \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (simp add: do_machine_op_def split_def)
apply wp
apply simp
done
lemma tcb_cap_wp_at:
"\<lbrakk>tcb_at t s; valid_objs s; ref \<in> dom tcb_cap_cases;
\<forall>cap st getF setF restr.

8
proof/invariant-abstract/Retype_AI.thy
View File

@ -1632,14 +1632,6 @@ lemma valid_vspace_obj_default:
apply (simp add: valid_vspace_obj_default')
done
lemma valid_arch_obj_default:
assumes tyunt: "ty \<noteq> Structures_A.apiobject_type.Untyped"
shows "ArchObj ao = default_object ty dev us \<Longrightarrow> valid_arch_obj ao s'"
apply (cases ty, simp_all add: default_object_def tyunt)
apply (simp add: valid_arch_obj_default')
done
lemma usable_range_subseteq:
"\<lbrakk>cap_aligned cap;is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<subseteq> untyped_range cap"
apply (clarsimp simp:is_cap_simps cap_aligned_def split:if_splits)

13
proof/refine/ARM/ArchAcc_R.thy
View File

@ -52,9 +52,6 @@ lemmas valid_arch_state_elims[rule_format, elim!] = conjuncts
lemmas valid_vspace_obj_elims [rule_format, elim!] =
valid_vspace_obj.simps[@simp_to_elim, @ \<open>(drule bspec)?\<close>]
lemmas valid_arch_obj_elims[rule_format, elim!] =
valid_vspace_obj_elims [unfolded valid_arch_obj_def[symmetric]]
end
context begin interpretation Arch . (*FIXME: arch_split*)
@ -1342,7 +1339,7 @@ lemma ko_at_typ_at_asidpool:
lemma find_pd_for_asid_corres [corres]:
"asid = asid' \<Longrightarrow> corres (lfr \<oplus> op =) ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid pd s)
and valid_arch_objs and pspace_aligned
and valid_vspace_objs and pspace_aligned
and K (0 < asid \<and> asid \<le> mask asidBits))
(pspace_aligned' and pspace_distinct' and no_0_obj')
(find_pd_for_asid asid) (findPDForASID asid')"
@ -1357,7 +1354,7 @@ lemma find_pd_for_asid_corres [corres]:
apply (insert prems)
apply (elim conjE disjE)
apply (fastforce dest: valid_asid_tableD)
apply (clarsimp simp: vspace_at_asid_def valid_arch_objs_def)
apply (clarsimp simp: vspace_at_asid_def)
apply (clarsimp simp: vs_asid_refs_def graph_of_def elim!: vs_lookupE)
apply (erule rtranclE)
subgoal by simp
@ -1373,8 +1370,8 @@ lemma find_pd_for_asid_corres [corres]:
by (clarsimp dest!: vs_lookup1D)
subgoal pd_at for x pool xa
apply (insert prems)
apply (rule valid_arch_obj_elims)
apply (rule valid_arch_objsD)
apply (rule valid_vspace_obj_elims)
apply (rule valid_vspace_objsD)
apply (rule vs_lookupI)
apply (rule vs_asid_refsI)
apply fastforce
@ -1397,7 +1394,7 @@ lemma find_pd_for_asid_corres [corres]:
done
lemma find_pd_for_asid_corres':
"corres (lfr \<oplus> op =) (vspace_at_asid asid pd and valid_arch_objs
"corres (lfr \<oplus> op =) (vspace_at_asid asid pd and valid_vspace_objs
and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits))
(pspace_aligned' and pspace_distinct' and no_0_obj')
(find_pd_for_asid asid) (findPDForASID asid)"

37
proof/refine/ARM/Arch_R.thy
View File

@ -522,7 +522,7 @@ lemma flush_type_map:
lemma resolve_vaddr_corres:
"\<lbrakk> is_aligned pd pd_bits; vaddr < kernel_base \<rbrakk> \<Longrightarrow>
corres (op =) (pspace_aligned and valid_arch_objs and page_directory_at pd
corres (op =) (pspace_aligned and valid_vspace_objs and page_directory_at pd
and (\<exists>\<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)))
(\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> vs_valid_duplicates' (ksPSpace s))
(resolve_vaddr pd vaddr) (resolveVAddr pd vaddr)"
@ -544,8 +544,7 @@ lemma resolve_vaddr_corres:
apply clarsimp
apply (erule(3) page_table_at_state_relation)
apply wpsimp+
apply (clarsimp simp: page_directory_pde_at_lookupI less_kernel_base_mapping_slots
valid_vspace_objs_def')
apply (clarsimp simp: page_directory_pde_at_lookupI less_kernel_base_mapping_slots)
apply (clarsimp simp: page_directory_pde_at_lookupI' page_directory_at_state_relation)
done
@ -612,8 +611,8 @@ lemma dec_arch_inv_page_flush_corres:
split: flush_type.splits invocation_label.splits arch_invocation_label.splits)
apply wp+
apply (fastforce simp: valid_cap_def mask_def
invs_vspace_objs[simplified valid_vspace_objs_def'])
apply (auto simp: valid_vspace_objs_def')
invs_vspace_objs[simplified])
apply (auto)
done
lemma lookup_pd_slot_mask_6_gumpf:
@ -713,7 +712,7 @@ lemma get_master_pte_wp:
done
lemma resolve_vaddr_valid_mapping_size:
"\<lbrace> valid_vs_lookup and pspace_aligned and valid_arch_objs and page_directory_at pd
"\<lbrace> valid_vs_lookup and pspace_aligned and valid_vspace_objs and page_directory_at pd
and (\<exists>\<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits))
and valid_objs and K (vaddr < kernel_base) \<rbrace>
resolve_vaddr pd vaddr \<lbrace> \<lambda>rv s. case rv of None \<Rightarrow> True
@ -728,8 +727,8 @@ lemma resolve_vaddr_valid_mapping_size:
apply (clarsimp simp: obj_at_def)
apply (frule(1) pspace_alignedD, simp)
apply (drule_tac y=pd_bits in is_aligned_weaken, simp add: pd_bits_def pageBits_def)
apply (frule valid_arch_objsD, simp add: obj_at_def lookup_pd_slot_eq, simp)
apply (simp add: lookup_pd_slot_eq less_kernel_base_mapping_slots valid_arch_obj_def)
apply (frule valid_vspace_objsD, simp add: obj_at_def lookup_pd_slot_eq, simp)
apply (simp add: lookup_pd_slot_eq less_kernel_base_mapping_slots)
apply (drule bspec, simp)
apply (rule conjI)
apply clarsimp
@ -743,10 +742,10 @@ lemma resolve_vaddr_valid_mapping_size:
apply (frule is_aligned_weaken[where x=pt_bits and y=10])
apply (simp add: pt_bits_def pageBits_def)
apply (simp add: vaddr_segment_nonsense3)
apply (frule valid_arch_objsD, simp add: obj_at_def, simp)
apply (frule valid_vspace_objsD, simp add: obj_at_def, simp)
apply (drule vs_lookup_pages_vs_lookupI)
apply (rule conjI)
apply (clarsimp simp: valid_arch_obj_def)
apply (clarsimp simp:)
apply (drule_tac x="ucast (pt_slot' && mask pt_bits >> 2)" in spec)
apply (drule vs_lookup_pages_step)
apply (rule vs_lookup_pages1I, simp add: obj_at_def)
@ -760,7 +759,7 @@ lemma resolve_vaddr_valid_mapping_size:
apply (frule(1) caps_of_state_valid_cap)
apply (clarsimp simp: valid_cap_def obj_at_def data_at_def a_type_simps
split: if_split_asm)
apply (clarsimp simp: vaddr_segment_nonsense4 valid_arch_obj_def)
apply (clarsimp simp: vaddr_segment_nonsense4)
apply (drule_tac x="ucast (pt_slot' && mask pt_bits >> 2)" in spec)
apply (drule vs_lookup_pages_step)
apply (rule vs_lookup_pages1I, simp add: obj_at_def)
@ -998,7 +997,7 @@ shows
apply (rule corres_splitEE)
prefer 2
apply (rule corres_lookup_error)
apply (rule_tac P="valid_arch_state and valid_arch_objs and
apply (rule_tac P="valid_arch_state and valid_vspace_objs and
pspace_aligned and equal_kernel_mappings and valid_global_objs and
valid_cap (cap.ArchObjectCap
(arch_cap.PageDirectoryCap wd (Some optv)))"
@ -1008,7 +1007,7 @@ shows
apply (simp add: mask_def)
apply assumption
apply (rule whenE_throwError_corres, simp, simp)
apply (rule_tac R="\<lambda>_ s. valid_arch_objs s \<and> pspace_aligned s
apply (rule_tac R="\<lambda>_ s. valid_vspace_objs s \<and> pspace_aligned s
\<and> hd args + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base \<and>
valid_arch_state s \<and> equal_kernel_mappings s \<and> valid_global_objs s \<and>
s \<turnstile> (fst (hd excaps)) \<and> (\<exists>\<rhd> (lookup_pd_slot (obj_ref_of (fst (hd excaps))) (hd args) && ~~ mask pd_bits)) s \<and>
@ -1042,7 +1041,6 @@ shows
apply (clarsimp simp: valid_cap_def dest!: vmsz_aligned_less_kernel_base_eq)
apply (frule_tac vptr="hd args" in page_directory_pde_at_lookupI, assumption)
apply (clarsimp simp: vmsz_aligned_def pageBitsForSize_def page_directory_at_aligned_pd_bits
valid_vspace_objs_def'
split: vmpage_size.splits)
apply (clarsimp simp: valid_cap'_def)
apply simp
@ -1051,7 +1049,7 @@ shows
apply (rule hoare_drop_imps)+
apply (simp add:not_le)
apply (wp hoare_drop_imps)+
apply (clarsimp simp: invs_def valid_state_def valid_vspace_objs_def')
apply (clarsimp simp: invs_def valid_state_def)
apply fastforce
apply (cases "invocation_type (mi_label mi) = ArchInvocationLabel ARMPageRemap")
apply (case_tac "\<not>(1 < length args \<and> excaps \<noteq> [])")
@ -1103,7 +1101,7 @@ shows
apply (rule corres_returnOk)
apply (clarsimp simp: archinv_relation_def page_invocation_map_def)
apply wp+
apply (subgoal_tac "valid_arch_objs s \<and> pspace_aligned s \<and>
apply (subgoal_tac "valid_vspace_objs s \<and> pspace_aligned s \<and>
(snd v') < kernel_base \<and>
equal_kernel_mappings s \<and> valid_global_objs s \<and> valid_arch_state s \<and>
(\<exists>\<rhd> (lookup_pd_slot (fst pa) (snd v') && ~~ mask pd_bits)) s \<and>
@ -1113,7 +1111,6 @@ shows
apply clarsimp
apply (frule_tac pd = aa and vptr = bc in page_directory_pde_at_lookupI,assumption)
apply (clarsimp simp: vmsz_aligned_def pageBitsForSize_def
valid_vspace_objs_def'
page_directory_at_aligned_pd_bits
split:vmpage_size.splits)
apply wp
@ -1122,7 +1119,7 @@ shows
apply (drule bspec [where x = "excaps ! 0"])
apply simp
apply (clarsimp simp: valid_cap_def mask_def split: option.split)
apply (fastforce simp: invs_def valid_state_def valid_pspace_def valid_vspace_objs_def')
apply (fastforce simp: invs_def valid_state_def valid_pspace_def)
apply (clarsimp split: option.split)
apply fastforce
@ -1181,7 +1178,7 @@ shows
apply (wp hoare_whenE_wp get_master_pde_wp getPDE_wp find_pd_for_asid_inv
| wp_once hoare_drop_imps)+
apply (fastforce simp: valid_cap_def mask_def
invs_vspace_objs[simplified valid_vspace_objs_def'])
invs_vspace_objs[simplified])
apply (clarsimp simp: valid_cap'_def)
apply fastforce
apply (clarsimp simp: unlessE_whenE liftE_bindE)
@ -1270,7 +1267,7 @@ shows
apply (wp hoare_drop_imps)+
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def valid_cap_simps mask_2pm1
valid_arch_state_def valid_arch_caps_def linorder_not_le
invs_vspace_objs[simplified valid_vspace_objs_def']
invs_vspace_objs[simplified]
split: option.splits)
apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def
split: option.splits)

4
proof/refine/ARM/CNodeInv_R.thy
View File

@ -610,7 +610,7 @@ declare word_unat_power [symmetric, simp del]
(* FIXME: move *)
lemma finalise_cap_not_reachable_pg_cap:
"\<lbrace>pspace_aligned and
valid_arch_objs and
valid_vspace_objs and
valid_objs and
cte_wp_at (op = cap) slot and
(\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s)
@ -624,7 +624,7 @@ lemma finalise_cap_not_reachable_pg_cap:
apply (clarsimp simp:reachable_pg_cap_def is_cap_simps|wp|intro conjI)+
apply (wp arch_finalise_case_no_lookup)
apply (clarsimp dest!: caps_of_state_valid_cap
simp: cte_wp_at_caps_of_state valid_vspace_objs_def')
simp: cte_wp_at_caps_of_state)
apply (clarsimp simp:reachable_pg_cap_def is_cap_simps|wp|intro conjI)+
done

18
proof/refine/ARM/Schedule_R.thy
View File

@ -218,7 +218,7 @@ declare objBitsT_koTypeOf [simp]
lemma arch_switch_thread_corres:
"corres dc (valid_arch_state and valid_objs and valid_asid_map
and valid_arch_objs and pspace_aligned and pspace_distinct
and valid_vspace_objs and pspace_aligned and pspace_distinct
and valid_vs_lookup and valid_global_objs
and unique_table_refs o caps_of_state
and st_tcb_at runnable t)
@ -955,7 +955,7 @@ crunch valid_queues[wp]: "Arch.switchToThread" "Invariants_H.valid_queues"
lemma switch_thread_corres:
"corres dc (valid_arch_state and valid_objs and valid_asid_map
and valid_arch_objs and pspace_aligned and pspace_distinct
and valid_vspace_objs and pspace_aligned and pspace_distinct
and valid_vs_lookup and valid_global_objs
and unique_table_refs o caps_of_state
and st_tcb_at runnable t and valid_etcbs)
@ -1010,7 +1010,7 @@ lemma typ_at'_typ_at'_mask: "\<And>s. \<lbrakk> typ_at' t (P s) s \<rbrakk> \<Lo
lemma arch_switch_idle_thread_corres:
"corres dc (valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and
valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_arch_objs and valid_idle)
valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_idle)
(valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle')
arch_switch_to_idle_thread
Arch.switchToIdleThread"
@ -1020,9 +1020,6 @@ lemma arch_switch_idle_thread_corres:
apply (clarsimp simp: valid_idle_def valid_idle'_def pred_tcb_at_def obj_at_def is_tcb)
done
lemma invs_arch_objs[simp]: "invs s \<Longrightarrow> valid_arch_objs s"
by (drule invs_vspace_objs, simp add: valid_vspace_objs_def')
lemma switch_idle_thread_corres:
"corres dc invs invs_no_cicd' switch_to_idle_thread switchToIdleThread"
apply (simp add: switch_to_idle_thread_def Thread_H.switchToIdleThread_def)
@ -1035,7 +1032,7 @@ lemma switch_idle_thread_corres:
apply (wp+, simp+)
apply (simp add: invs_unique_refs invs_valid_vs_lookup invs_valid_objs invs_valid_asid_map
invs_arch_state invs_valid_global_objs invs_psp_aligned invs_distinct
invs_valid_idle)
invs_valid_idle invs_vspace_objs)
apply (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_pspace'_def)
done
@ -2262,7 +2259,7 @@ lemma gts_exs_valid[wp]:
lemma guarded_switch_to_corres:
"corres dc (valid_arch_state and valid_objs and valid_asid_map
and valid_arch_objs and pspace_aligned and pspace_distinct
and valid_vspace_objs and pspace_aligned and pspace_distinct
and valid_vs_lookup and valid_global_objs
and unique_table_refs o caps_of_state
and st_tcb_at runnable t and valid_etcbs)
@ -2415,8 +2412,7 @@ lemma guarded_switch_to_chooseThread_fragment_corres:
apply (clarsimp simp: st_tcb_at_tcb_at invs_def valid_state_def valid_pspace_def valid_sched_def
invs_valid_vs_lookup invs_unique_refs)
apply (auto elim!: pred_tcb'_weakenE split: thread_state.splits
simp: pred_tcb_at' runnable'_def all_invs_but_ct_idle_or_in_cur_domain'_def
valid_vspace_objs_def')
simp: pred_tcb_at' runnable'_def all_invs_but_ct_idle_or_in_cur_domain'_def)
done
lemma bitmap_lookup_queue_is_max_non_empty:
@ -2674,7 +2670,7 @@ lemma schedule_corres:
apply (rule conjI,simp)
apply (clarsimp split: Deterministic_A.scheduler_action.splits
simp: invs_psp_aligned invs_distinct invs_valid_objs invs_arch_state
invs_vspace_objs[simplified valid_vspace_objs_def'])
invs_vspace_objs[simplified])
apply (intro impI conjI allI tcb_at_invs |
(fastforce simp: invs_def cur_tcb_def valid_arch_caps_def valid_etcbs_def
valid_sched_def valid_sched_action_def is_activatable_def

101
proof/refine/ARM/VSpace_R.thy
View File

@ -177,7 +177,7 @@ lemma find_pd_for_asid_valids:
lemma valid_asid_map_inj_map:
"\<lbrakk> valid_asid_map s; (s, s') \<in> state_relation;
unique_table_refs (caps_of_state s);
valid_vs_lookup s; valid_arch_objs s;
valid_vs_lookup s; valid_vspace_objs s;
valid_arch_state s; valid_global_objs s \<rbrakk>
\<Longrightarrow> inj_on (option_map snd \<circ> armKSASIDMap (ksArchState s'))
(dom (armKSASIDMap (ksArchState s')))"
@ -264,9 +264,7 @@ lemma find_pd_for_asid_assert_corres:
apply (rule_tac P="\<bottom>" and P'="\<top>" in corres_inst)
apply (simp add: corres_fail)
apply (wp find_pd_for_asid_valids[where pd=pd])+
apply (clarsimp simp: word_neq_0_conv valid_arch_objs_def
valid_arch_obj_def
valid_vspace_objs_def)
apply (clarsimp simp: word_neq_0_conv valid_vspace_objs_def)
apply simp
done
@ -458,7 +456,7 @@ lemma find_free_hw_asid_corres:
apply (frule pd_at_asid_uniq, simp_all add: valid_asid_map_def valid_arch_state_def)[1]
apply (drule subsetD, erule domI)
apply simp
apply (simp add: valid_arch_objs_def valid_arch_obj_def valid_vspace_objs_def)
apply (simp add: valid_vspace_objs_def)
apply fastforce
apply clarsimp
done
@ -471,16 +469,13 @@ crunch distinct'[wp]: findFreeHWASID "pspace_distinct'"
crunch no_0_obj'[wp]: getHWASID "no_0_obj'"
(* FIXME: questionable practice *)
lemma valid_vspace_objs_def' : "valid_vspace_objs s = valid_arch_objs s"
by (simp add: valid_arch_objs_def valid_arch_obj_def valid_vspace_objs_def)
lemma get_hw_asid_corres:
"corres op =
(vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask asid_bits)
and unique_table_refs o caps_of_state
and valid_global_objs and valid_vs_lookup
and valid_asid_map and valid_arch_objs
and valid_asid_map and valid_vspace_objs
and pspace_aligned and pspace_distinct
and valid_arch_state)
(pspace_aligned' and pspace_distinct' and no_0_obj')
@ -493,7 +488,7 @@ lemma get_hw_asid_corres:
apply (rule corres_split_eqr [OF _ find_free_hw_asid_corres])
apply (rule corres_split [OF _ store_hw_asid_corres[where pd=pd]])
apply (rule corres_trivial, simp )
apply (wpsimp wp: load_hw_asid_wp simp: valid_vspace_objs_def')+
apply (wpsimp wp: load_hw_asid_wp)+
apply (simp add: pd_at_asid_uniq)
apply simp
done
@ -503,7 +498,7 @@ lemma arm_context_switch_corres:
(vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask asid_bits)
and unique_table_refs o caps_of_state
and valid_global_objs and valid_vs_lookup
and valid_asid_map and valid_arch_objs
and valid_asid_map and valid_vspace_objs
and pspace_aligned and pspace_distinct
and valid_arch_state)
(pspace_aligned' and pspace_distinct' and no_0_obj')
@ -562,7 +557,7 @@ lemma hv_corres:
lemma flush_space_corres:
"corres dc
(K (asid \<le> mask asid_bits \<and> asid \<noteq> 0)
and valid_asid_map and valid_arch_objs
and valid_asid_map and valid_vspace_objs
and pspace_aligned and pspace_distinct
and unique_table_refs o caps_of_state
and valid_global_objs and valid_vs_lookup
@ -587,14 +582,14 @@ lemma flush_space_corres:
apply (rule no_fail_invalidateLocalTLB_ASID)
apply wp+
apply clarsimp
apply (simp add: pd_at_asid_uniq valid_vspace_objs_def')
apply (simp add: pd_at_asid_uniq)
apply simp
done
lemma invalidate_tlb_by_asid_corres:
"corres dc
(K (asid \<le> mask asid_bits \<and> asid \<noteq> 0)
and valid_asid_map and valid_arch_objs
and valid_asid_map and valid_vspace_objs
and pspace_aligned and pspace_distinct
and unique_table_refs o caps_of_state
and valid_global_objs and valid_vs_lookup
@ -614,14 +609,14 @@ lemma invalidate_tlb_by_asid_corres:
apply (rule no_fail_invalidateLocalTLB_ASID)
apply wp+
apply clarsimp
apply (simp add: pd_at_asid_uniq valid_vspace_objs_def')
apply (simp add: pd_at_asid_uniq)
apply simp
done
lemma invalidate_tlb_by_asid_corres_ex:
"corres dc
(\<lambda>s. asid \<le> mask asid_bits \<and> asid \<noteq> 0
\<and> valid_asid_map s \<and> valid_arch_objs s
\<and> valid_asid_map s \<and> valid_vspace_objs s
\<and> pspace_aligned s \<and> pspace_distinct s
\<and> unique_table_refs (caps_of_state s)
\<and> valid_global_objs s \<and> valid_vs_lookup s
@ -681,7 +676,7 @@ lemma set_vm_root_corres:
"corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map
and unique_table_refs o caps_of_state and valid_vs_lookup
and valid_global_objs and pspace_aligned and pspace_distinct
and valid_arch_objs)
and valid_vspace_objs)
(pspace_aligned' and pspace_distinct'
and valid_arch_state' and tcb_at' t and no_0_obj')
(set_vm_root t) (setVMRoot t)"
@ -723,7 +718,7 @@ proof -
apply (simp add: tcbVTableSlot_def cte_map_def objBits_def cte_level_bits_def
objBitsKO_def tcb_cnode_index_def to_bl_1)
apply (rule_tac R="\<lambda>thread_root. valid_arch_state and valid_asid_map and
valid_arch_objs and valid_vs_lookup and
valid_vspace_objs and valid_vs_lookup and
unique_table_refs o caps_of_state and
valid_global_objs and valid_objs and
pspace_aligned and pspace_distinct and
@ -745,7 +740,7 @@ proof -
and pd_at_uniq aa word
and valid_asid_map and valid_vs_lookup
and (unique_table_refs o caps_of_state)
and valid_arch_objs and valid_global_objs
and valid_vspace_objs and valid_global_objs
and valid_arch_state"
in corres_stateAssert_implied)
apply (rule P)
@ -771,8 +766,7 @@ proof -
apply (frule page_directory_cap_pd_at_uniq, simp+)
apply (frule(1) cte_wp_at_valid_objs_valid_cap)
apply (clarsimp simp: valid_cap_def mask_def
word_neq_0_conv
valid_vspace_objs_def')
word_neq_0_conv)
apply (drule(1) pd_at_asid_unique2, simp)
apply simp+
apply (wp get_cap_wp | simp)+
@ -832,8 +826,7 @@ lemma invalidate_asid_entry_corres:
apply simp
apply (rule invalidate_hw_asid_entry_corres)
apply (wp load_hw_asid_wp
| clarsimp simp: valid_vspace_objs_def'
cong: if_cong)+
| clarsimp cong: if_cong)+
apply (simp add: pd_at_asid_uniq)
apply simp
done
@ -909,15 +902,15 @@ lemma delete_asid_corres:
apply (simp del: fun_upd_apply)
apply (fold cur_tcb_def)
apply (wp set_asid_pool_asid_map_unmap
set_asid_pool_arch_objs_unmap_single
set_asid_pool_vspace_objs_unmap_single
set_asid_pool_vs_lookup_unmap')+
apply simp
apply (fold cur_tcb'_def)
apply (wp invalidate_asid_entry_invalidates)+
apply (wp | clarsimp simp: o_def valid_vspace_objs_def')+
apply (wp | clarsimp simp: o_def)+
apply (subgoal_tac "vspace_at_asid asid pd s")
apply (auto simp: obj_at_def a_type_def graph_of_def
invs_vspace_objs[simplified valid_vspace_objs_def']
invs_vspace_objs[simplified]
split: if_split_asm)[1]
apply (simp add: vspace_at_asid_def)
apply (rule vs_lookupI)
@ -997,7 +990,7 @@ lemma delete_asid_pool_corres:
in invalidate_asid_entry_corres)
apply wp
apply clarsimp
apply (wpsimp simp: valid_vspace_objs_def')+
apply (wpsimp)+
apply (clarsimp simp: invs_def valid_state_def
valid_arch_caps_def valid_pspace_def
vspace_at_asid_def cong: conj_cong)
@ -1019,7 +1012,7 @@ lemma delete_asid_pool_corres:
apply (simp add: asid_bits_def word_bits_def)
apply (simp add: asid_low_bits_def word_bits_def)
apply (simp add: asid_bits_def asid_low_bits_def asid_high_bits_def)
apply (subst conj_commute, rule context_conjI, simp add: valid_vspace_objs_def')
apply (subst conj_commute, rule context_conjI, simp add: valid_vspace_objs_def)
apply (erule vs_lookup_trancl_step)
apply (rule r_into_trancl)
apply (erule vs_lookup1I)
@ -1073,7 +1066,7 @@ lemma delete_asid_pool_corres:
apply simp
apply (fold cur_tcb_def)
apply (strengthen valid_arch_state_unmap_strg
valid_arch_objs_unmap_strg
valid_vspace_objs_unmap_strg
valid_asid_map_unmap
valid_vs_lookup_unmap_strg)
apply (simp add: valid_global_objs_arch_update)
@ -1092,7 +1085,7 @@ lemma delete_asid_pool_corres:
apply wp
apply (wp getASID_wp)+
apply (clarsimp simp: conj_comms)
apply (auto simp: vs_lookup_def invs_vspace_objs[simplified valid_vspace_objs_def']
apply (auto simp: vs_lookup_def invs_vspace_objs[simplified]
intro: vs_asid_refsI)[1]
apply clarsimp
done
@ -1112,7 +1105,7 @@ lemma set_vm_root_for_flush_corres:
proof -
have X: "corres op = (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
and valid_asid_map and valid_vs_lookup
and valid_arch_objs and valid_global_objs
and valid_vspace_objs and valid_global_objs
and unique_table_refs o caps_of_state
and valid_arch_state
and pspace_aligned and pspace_distinct)
@ -1134,7 +1127,7 @@ proof -
apply (rule corres_split [OF _ gct_corres])
apply (rule corres_split [where R="\<lambda>_. vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
and valid_asid_map and valid_vs_lookup
and valid_arch_objs and valid_global_objs
and valid_vspace_objs and valid_global_objs
and unique_table_refs o caps_of_state
and valid_arch_state
and pspace_aligned and pspace_distinct"
@ -1153,7 +1146,7 @@ proof -
apply (simp add: cte_map_def objBits_simps tcb_cnode_index_def
tcbVTableSlot_def to_bl_1 cte_level_bits_def)
apply wp+
apply (clarsimp simp: cur_tcb_def valid_vspace_objs_def')
apply (clarsimp simp: cur_tcb_def)
apply (erule tcb_at_cte_at)
apply (simp add: tcb_cap_cases_def)
apply clarsimp
@ -1299,7 +1292,7 @@ crunch valid_arch' [wp]: setVMRootForFlush "valid_arch_state'"
lemma load_hw_asid_corres2:
"corres op =
(valid_arch_objs and pspace_distinct and pspace_aligned
(valid_vspace_objs and pspace_distinct and pspace_aligned
and valid_asid_map and vspace_at_asid a pd
and valid_vs_lookup and valid_global_objs
and unique_table_refs o caps_of_state
@ -1308,7 +1301,7 @@ lemma load_hw_asid_corres2:
(load_hw_asid a) (loadHWASID a)"
apply (rule stronger_corres_guard_imp)
apply (rule load_hw_asid_corres[where pd=pd])
apply (clarsimp simp: pd_at_asid_uniq valid_vspace_objs_def')
apply (clarsimp simp: pd_at_asid_uniq)
apply simp
done
@ -1318,7 +1311,7 @@ crunch no_0_obj'[wp]: flushTable "no_0_obj'"
lemma flush_table_corres:
"corres dc
(pspace_aligned and valid_objs and valid_arch_state and
cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_arch_objs and
cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and
pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs
and unique_table_refs o caps_of_state and
K (is_aligned vptr (pageBitsForSize ARMSection) \<and> asid \<le> mask asid_bits \<and> asid \<noteq> 0))
@ -1346,14 +1339,14 @@ lemma flush_table_corres:
apply (rule no_fail_invalidateLocalTLB_ASID)
apply (wp hoare_drop_imps | simp)+
apply (wp load_hw_asid_wp hoare_drop_imps |
simp add: cur_tcb'_def [symmetric] cur_tcb_def [symmetric] valid_vspace_objs_def')+
simp add: cur_tcb'_def [symmetric] cur_tcb_def [symmetric] )+
done
lemma flush_page_corres:
"corres dc
(K (is_aligned vptr pageBits \<and> asid \<le> mask asid_bits \<and> asid \<noteq> 0) and
cur_tcb and valid_arch_state and valid_objs and
vspace_at_asid asid pd and valid_asid_map and valid_arch_objs and
vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and
valid_vs_lookup and valid_global_objs and
unique_table_refs o caps_of_state and
pspace_aligned and pspace_distinct)
@ -1382,8 +1375,7 @@ lemma flush_page_corres:
apply (simp add: cur_tcb_def [symmetric] cur_tcb'_def [symmetric])
apply (wp hoare_drop_imps)[1]
apply (assumption | wp hoare_drop_imps load_hw_asid_wp
| clarsimp simp: valid_vspace_objs_def'
cur_tcb_def [symmetric] cur_tcb'_def [symmetric])+
| clarsimp simp: cur_tcb_def [symmetric] cur_tcb'_def [symmetric])+
done
crunch typ_at' [wp]: flushTable "\<lambda>s. P (typ_at' T p s)"
@ -1405,7 +1397,7 @@ crunch distinct'[wp]: unmapPageTable "pspace_distinct'"
wp: crunch_wps getObject_inv loadObject_default_inv)
lemma page_table_mapped_corres:
"corres (op =) (valid_arch_state and valid_arch_objs and pspace_aligned
"corres (op =) (valid_arch_state and valid_vspace_objs and pspace_aligned
and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits))
(pspace_aligned' and pspace_distinct' and no_0_obj')
(page_table_mapped asid vaddr pt)
@ -1422,7 +1414,7 @@ lemma page_table_mapped_corres:
simp_all add: returnOk_def pde_relation_aligned_def
split:if_splits ARM_H.pde.splits)[1]
apply (wp | simp add: lookup_pd_slot_def Let_def)+
apply (simp add: word_neq_0_conv valid_vspace_objs_def')
apply (simp add: word_neq_0_conv)
apply simp
done
@ -1457,7 +1449,7 @@ lemma unmap_page_table_corres:
apply (wp no_fail_cleanByVA_PoU)+
apply (simp, wp+)
apply (simp add:pde_relation_aligned_def)+
apply (wp store_pde_pd_at_asid store_pde_arch_objs_invalid)
apply (wp store_pde_pd_at_asid store_pde_vspace_objs_invalid)
apply (rule hoare_vcg_conj_lift)
apply (simp add: store_pde_def)
apply (wp set_pd_vs_lookup_unmap)+
@ -1465,7 +1457,6 @@ lemma unmap_page_table_corres:
apply (wp page_table_mapped_wp)
apply (wp hoare_drop_imps)[1]
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def
valid_vspace_objs_def'
valid_arch_caps_def word_gt_0)
apply (frule (1) page_directory_pde_at_lookupI)
apply (auto elim: simp: empty_table_def valid_pde_mappings_def pde_ref_def obj_at_def
@ -1566,7 +1557,7 @@ lemma unmap_page_corres:
apply (rule_tac F = "vptr < kernel_base" in corres_gen_asm)
apply (rule_tac P="\<exists>\<rhd> pd and page_directory_at pd and vspace_at_asid asid pd
and (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits))
and valid_arch_state and valid_arch_objs
and valid_arch_state and valid_vspace_objs
and equal_kernel_mappings
and pspace_aligned and valid_global_objs and valid_etcbs and
K (valid_unmap sz (asid,vptr) )" and
@ -1588,8 +1579,7 @@ lemma unmap_page_corres:
lookupPTSlot_inv lookup_pt_slot_is_aligned
| simp add: pte_relation_aligned_def)+
apply (clarsimp simp: page_directory_pde_at_lookupI
page_directory_at_aligned_pd_bits vmsz_aligned_def
valid_vspace_objs_def')
page_directory_at_aligned_pd_bits vmsz_aligned_def)
apply (simp add:valid_unmap_def pageBits_def)
apply (erule less_kernel_base_mapping_slots)
apply (simp add:page_directory_at_aligned_pd_bits)
@ -1623,7 +1613,7 @@ lemma unmap_page_corres:
pd_bits_def pageBits_def valid_unmap_def)
apply (drule(1) less_kernel_base_mapping_slots[OF _ page_directory_at_aligned_pd_bits])
apply simp
apply (simp add:pd_bits_def pageBits_def valid_vspace_objs_def')
apply (simp add:pd_bits_def pageBits_def)
apply (clarsimp simp: pd_aligned page_directory_pde_at_lookupI)
apply (rule corres_guard_imp)
apply (rule corres_split_strengthen_ftE[OF check_mapping_corres])
@ -1675,7 +1665,7 @@ lemma unmap_page_corres:
store_pde_invs_unmap store_pde_pd_at_asid mapM_swp_store_pde_invs_unmap
| wpc | simp | wp hoare_drop_imps
| wp mapM_wp')+
apply (auto simp: invs_vspace_objs[simplified valid_vspace_objs_def'])[1]
apply (auto simp: invs_vspace_objs[simplified])[1]
apply (wp lookupPTSlot_inv mapM_wp' | wpc | clarsimp)+
apply (wp hoare_vcg_const_imp_lift_R
| strengthen lookup_pd_slot_kernel_mappings_strg not_in_global_refs_vs_lookup
@ -1686,7 +1676,6 @@ lemma unmap_page_corres:
apply (case_tac sz)
apply (auto simp: invs_def valid_state_def
valid_arch_state_def pageBits_def
valid_vspace_objs_def'
valid_arch_caps_def vmsz_aligned_def)
done
@ -1745,7 +1734,7 @@ lemma perform_page_directory_corres:
apply (simp add: cur_tcb'_def[symmetric])
apply (wp hoare_drop_imps)+
apply clarsimp
apply (auto simp: valid_pdi_def invs_vspace_objs[simplified valid_vspace_objs_def'])[2]
apply (auto simp: valid_pdi_def invs_vspace_objs[simplified])[2]
apply (clarsimp simp: page_directory_invocation_map_def)
done
@ -2203,7 +2192,7 @@ proof -
apply (clarsimp dest!:valid_slots_duplicated_pteD')
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. vspace_at_asid word pd s)" in hoare_strengthen_post)
prefer 2
apply (auto simp: invs_vspace_objs[simplified valid_vspace_objs_def'])[1]
apply (auto simp: invs_vspace_objs[simplified])[1]
apply (wp mapM_swp_store_pte_invs[where pte="ARM_A.pte.InvalidPTE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_UNIV_wp | simp add: swp_def del: fun_upd_apply)+
apply (clarsimp simp:pte_relation_aligned_def)
@ -2244,7 +2233,7 @@ proof -
apply (clarsimp dest!:valid_slots_duplicated_pdeD' )
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. vspace_at_asid word pd s)" in hoare_strengthen_post)
prefer 2
apply (auto simp: invs_vspace_objs[simplified valid_vspace_objs_def'])[1]
apply (auto simp: invs_vspace_objs[simplified])[1]
apply (wp mapM_swp_store_pde_invs_unmap[where pde="ARM_A.pde.InvalidPDE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_UNIV_wp store_pde_pd_at_asid | clarsimp simp add: swp_def)+
apply (clarsimp simp: pde_relation_aligned_def)
@ -2314,7 +2303,7 @@ proof -
apply (clarsimp dest!:valid_slots_duplicated_pteD')
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. vspace_at_asid word pd s)" in hoare_strengthen_post)
prefer 2
apply (auto simp: invs_vspace_objs[simplified valid_vspace_objs_def'])[1]
apply (auto simp: invs_vspace_objs[simplified])[1]
apply (wp mapM_swp_store_pte_invs[where pte="ARM_A.pte.InvalidPTE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_UNIV_wp | simp add: swp_def del: fun_upd_apply)+
apply (clarsimp simp:pte_relation_aligned_def valid_page_inv'_def)
@ -2356,7 +2345,7 @@ proof -
apply (clarsimp dest!:valid_slots_duplicated_pdeD' )
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. vspace_at_asid word pd s)" in hoare_strengthen_post)
prefer 2
apply (auto simp: invs_vspace_objs[simplified valid_vspace_objs_def'])[1]
apply (auto simp: invs_vspace_objs[simplified])[1]
apply (wp mapM_swp_store_pde_invs_unmap[where pde="ARM_A.pde.InvalidPDE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_UNIV_wp store_pde_pd_at_asid | clarsimp simp add: swp_def)+
apply (clarsimp simp: pde_relation_aligned_def valid_page_inv'_def)
@ -2467,7 +2456,7 @@ proof -
apply (wp hoare_drop_imps)
apply (simp add: cur_tcb_def [symmetric] cur_tcb'_def [symmetric])
apply (wp hoare_drop_imps)+
apply (auto simp: valid_page_inv_def invs_vspace_objs[simplified valid_vspace_objs_def'])[2]
apply (auto simp: valid_page_inv_def invs_vspace_objs[simplified])[2]
-- "PageGetAddr"
apply (clarsimp simp: perform_page_invocation_def performPageInvocation_def page_invocation_map_def fromPAddr_def)
apply (rule corres_guard_imp)

4
proof/refine/ARM_HYP/ArchAcc_R.thy
View File

@ -49,8 +49,6 @@ declare valid_arch_state_def[@def_to_elim, conjuncts]
lemmas valid_arch_state_elims[rule_format, elim!] = conjuncts
declare valid_arch_obj_def[simp]
lemmas valid_vspace_obj_elims[rule_format, elim!] =
valid_vspace_obj.simps[@simp_to_elim, @ \<open>(drule bspec)?\<close>]
@ -1513,7 +1511,7 @@ lemma find_pd_for_asid_corres [@lift_corres_args, corres]:
apply (insert prems)
apply (elim conjE disjE)
apply (fastforce dest: valid_asid_tableD)
apply (clarsimp simp: vspace_at_asid_def valid_arch_objs_def)
apply (clarsimp simp: vspace_at_asid_def)
apply (clarsimp simp: vs_asid_refs_def graph_of_def elim!: vs_lookupE)
apply (erule rtranclE)
subgoal by simp

8
proof/refine/ARM_HYP/Arch_R.thy
View File

@ -930,8 +930,6 @@ lemma dec_arch_inv_corres:
notes check_vp_inv[wp del] check_vp_wpR[wp] [[goals_limit = 1]]
(* FIXME: check_vp_inv shadowed check_vp_wpR. Instead,
check_vp_wpR should probably be generalised to replace check_vp_inv. *)
notes valid_arch_imp_valid_vspace_objs[simp add]
notes valid_arch_objs_lift[simp add]
shows
"\<lbrakk> acap_relation arch_cap arch_cap';
list_all2 cap_relation (map fst excaps) (map fst excaps');
@ -1113,7 +1111,7 @@ shows
apply (rule corres_splitEE)
prefer 2
apply (rule corres_lookup_error)
apply (rule_tac P="valid_arch_state and valid_arch_objs and
apply (rule_tac P="valid_arch_state and valid_vspace_objs and
pspace_aligned and equal_kernel_mappings and
valid_cap (cap.ArchObjectCap
(arch_cap.PageDirectoryCap wd (Some optv)))"
@ -1123,7 +1121,7 @@ shows
apply (simp add: mask_def)
apply assumption
apply (rule whenE_throwError_corres, simp, simp)
apply (rule_tac R="\<lambda>_ s. valid_arch_objs s \<and> pspace_aligned s
apply (rule_tac R="\<lambda>_ s. valid_vspace_objs s \<and> pspace_aligned s
\<and> hd args + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base \<and>
valid_arch_state s \<and> equal_kernel_mappings s \<and>
s \<turnstile> (fst (hd excaps)) \<and> (\<exists>\<rhd> (lookup_pd_slot (obj_ref_of (fst (hd excaps))) (hd args) && ~~ mask pd_bits)) s \<and>
@ -1218,7 +1216,7 @@ shows
apply (rule corres_returnOk)
apply (clarsimp simp: archinv_relation_def page_invocation_map_def)
apply wp+
apply (subgoal_tac "valid_arch_objs s \<and> pspace_aligned s \<and>
apply (subgoal_tac "valid_vspace_objs s \<and> pspace_aligned s \<and>
(snd v') < kernel_base \<and>
equal_kernel_mappings s \<and> valid_arch_state s \<and>
(\<exists>\<rhd> (lookup_pd_slot (fst pa) (snd v') && ~~ mask pd_bits)) s \<and>

2
proof/refine/ARM_HYP/VSpace_R.thy
View File

@ -96,7 +96,7 @@ lemma find_pd_for_asid_eq_helper:
asid \<noteq> 0; pspace_aligned s \<rbrakk>
\<Longrightarrow> find_pd_for_asid asid s = returnOk pd s
\<and> page_directory_at pd s \<and> is_aligned pd pdBits"
apply (clarsimp simp: vspace_at_asid_def valid_vspace_objs_def valid_arch_objs_def)
apply (clarsimp simp: vspace_at_asid_def valid_vspace_objs_def)
apply (frule spec, drule mp, erule exI)
apply (clarsimp simp: vs_asid_refs_def graph_of_def
elim!: vs_lookupE)