arm refine: update for PageMap replacing PageRemap (SELFOUR-161)
This commit is contained in:
Victor Phan
parent
dede199780
commit
67d37f8025
|
|
@ -777,6 +777,17 @@ lemma resolve_vaddr_valid_mapping_size:
|
|||
split: if_split_asm)
|
||||
done
|
||||
|
||||
lemma corres_splitEE':
|
||||
assumes "corres_underlying sr nf nf' (f \<oplus> r') P P' a c"
|
||||
assumes "\<And>rv rv'. r' rv rv'
|
||||
\<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (R rv) (R' rv') (b rv) (d rv')"
|
||||
assumes "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>"
|
||||
shows "corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a >>=E (\<lambda>rv. b rv)) (c >>=E (\<lambda>rv'. d rv'))"
|
||||
by (rule corres_splitEE; rule assms)
|
||||
|
||||
lemmas whenE_throwError_corres_terminal =
|
||||
whenE_throwError_corres[where m="returnOk ()" and m'="returnOk ()", OF _ _ corres_returnOkTT, simplified]
|
||||
|
||||
lemma dec_arch_inv_corres:
|
||||
notes check_vp_inv[wp del] check_vp_wpR[wp]
|
||||
(* FIXME: check_vp_inv shadowed check_vp_wpR. Instead,
|
||||
|
|
@ -797,9 +808,7 @@ shows
|
|||
arch_cap excaps)
|
||||
(Arch.decodeInvocation (mi_label mi) args cptr'
|
||||
(cte_map slot) arch_cap' excaps')"
|
||||
apply (simp add: arch_decode_invocation_def
|
||||
ARM_H.decodeInvocation_def
|
||||
decodeARMMMUInvocation_def
|
||||
apply (simp add: arch_decode_invocation_def ARM_H.decodeInvocation_def decodeARMMMUInvocation_def
|
||||
split del: if_split)
|
||||
apply (cases arch_cap)
|
||||
apply (simp add: isCap_simps split del: if_split)
|
||||
|
|
@ -851,7 +860,7 @@ shows
|
|||
apply (simp add: archinv_relation_def asid_pool_invocation_map_def)
|
||||
apply (rule hoare_pre, wp hoare_whenE_wp)
|
||||
apply (clarsimp simp: ucast_fst_hd_assocs)
|
||||
apply (wp hoareE_TrueI hoare_whenE_wp getASID_wp | simp)+
|
||||
apply (wp hoareE_TrueI hoare_whenE_wp getASID_wp | simp)+
|
||||
apply ((clarsimp simp: p2_low_bits_max | rule TrueI impI)+)[2]
|
||||
apply (wp hoare_whenE_wp getASID_wp)+
|
||||
apply (clarsimp simp: valid_cap_def)
|
||||
|
|
@ -894,18 +903,20 @@ shows
|
|||
apply (rule dom_ucast_eq_7)
|
||||
apply (rule corres_trivial, simp, simp)
|
||||
apply (simp split del: if_split)
|
||||
apply (rule_tac F="- dom (asidTable \<circ> ucast) \<inter> {x. x \<le> 2 ^ asid_high_bits - 1} \<noteq> {}" in corres_gen_asm)
|
||||
apply (rule_tac F="- dom (asidTable \<circ> ucast) \<inter> {x. x \<le> 2 ^ asid_high_bits - 1} \<noteq> {}"
|
||||
in corres_gen_asm)
|
||||
apply (drule dom_hd_assocsD)
|
||||
apply (simp add: select_ext_fa[simplified free_asid_select_def]
|
||||
free_asid_select_def o_def returnOk_liftE[symmetric] split del: if_split)
|
||||
free_asid_select_def o_def returnOk_liftE[symmetric]
|
||||
split del: if_split)
|
||||
apply (thin_tac "fst a \<notin> b \<and> P" for a b P)
|
||||
apply (case_tac "isUntypedCap a \<and> capBlockSize a = objBits (makeObject::asidpool) \<and> \<not> capIsDevice a")
|
||||
apply (case_tac "isUntypedCap a \<and> capBlockSize a = objBits (makeObject::asidpool)
|
||||
\<and> \<not> capIsDevice a")
|
||||
prefer 2
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_trivial)
|
||||
apply (case_tac ad, simp_all add: isCap_simps
|
||||
split del: if_split)[1]
|
||||
apply (case_tac x21, simp_all split del: if_split)[1]
|
||||
apply (case_tac ad, simp_all add: isCap_simps split del: if_split)[1]
|
||||
apply (case_tac x21, simp_all split del: if_split)[1]
|
||||
apply (clarsimp simp: objBits_simps archObjSize_def
|
||||
split del: if_split)
|
||||
apply clarsimp
|
||||
|
|
@ -933,160 +944,71 @@ shows
|
|||
apply (wp hoare_whenE_wp)+
|
||||
apply fastforce
|
||||
apply clarsimp
|
||||
apply (simp add: null_def split_def asid_high_bits_def
|
||||
word_le_make_less)
|
||||
apply (simp add: null_def split_def asid_high_bits_def word_le_make_less)
|
||||
apply (subst hd_map, assumption)
|
||||
(* need abstract guard to show list nonempty *)
|
||||
\<comment> \<open>need abstract guard to show list nonempty\<close>
|
||||
apply (simp add: word_le_make_less)
|
||||
apply (subst ucast_ucast_len)
|
||||
apply (drule hd_in_set)
|
||||
apply simp
|
||||
apply fastforce
|
||||
apply (rename_tac word cap_rights vmpage_size option)
|
||||
apply (simp add: isCap_simps split del: if_split)
|
||||
apply (cases "invocation_type (mi_label mi) = ArchInvocationLabel ARMPageMap")
|
||||
apply (case_tac "\<not>(2 < length args \<and> excaps \<noteq> [])")
|
||||
apply (auto split: list.split)[1]
|
||||
apply (rename_tac dev frame_ptr cap_rights vmpage_size map_data)
|
||||
apply (case_tac "\<not>(2 < length args \<and> excaps \<noteq> [])", clarsimp split: list.splits)
|
||||
apply (simp add: Let_def neq_Nil_conv)
|
||||
apply (elim exE conjE)
|
||||
apply (simp split: list.split, intro conjI impI allI, simp_all)[1]
|
||||
apply (rename_tac pd_cap pd_cap_cnode pd_cap_slot excaps_rest)
|
||||
apply (clarsimp split: list.split, intro conjI impI allI; clarsimp)
|
||||
apply (rename_tac vaddr rights_mask attr pd_cap' excaps'_rest args_rest)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule whenE_throwError_corres)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (simp split: cap.split,
|
||||
intro conjI impI allI, simp_all)[1]
|
||||
apply (rename_tac arch_capa)
|
||||
apply (case_tac arch_capa, simp_all)[1]
|
||||
apply (rename_tac wd opt)
|
||||
apply (case_tac opt, simp_all)[1]
|
||||
apply (rename_tac optv)
|
||||
apply (rule corres_splitEE)
|
||||
prefer 2
|
||||
apply (rule corres_lookup_error)
|
||||
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)))"
|
||||
in corres_guard_imp)
|
||||
apply (rule find_pd_for_asid_corres[OF refl])
|
||||
apply (clarsimp simp: valid_cap_def)
|
||||
apply (simp add: mask_def)
|
||||
apply assumption
|
||||
apply (rule whenE_throwError_corres, simp, simp)
|
||||
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>
|
||||
(\<exists>\<rhd> rv') s \<and> page_directory_at rv' s"
|
||||
and R'="\<lambda>_ s. s \<turnstile>' (fst (hd excaps')) \<and> valid_objs' s \<and>
|
||||
pspace_aligned' s \<and> pspace_distinct' s \<and>
|
||||
valid_arch_state' s \<and> vs_valid_duplicates' (ksPSpace s)"
|
||||
in corres_splitEE)
|
||||
prefer 2
|
||||
apply (rule corres_whenE)
|
||||
apply (simp add: kernel_base_def ARM.kernelBase_def kernelBase_def shiftl_t2n)
|
||||
apply (rule corres_trivial, simp)
|
||||
apply simp
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_splitEE)
|
||||
prefer 2
|
||||
apply (rule check_vp_corres)
|
||||
apply (rule corres_splitEE)
|
||||
prefer 2
|
||||
apply (simp only: addrFromPPtr_def)
|
||||
apply (rule create_mapping_entries_corres[OF _ _ refl refl refl refl])
|
||||
apply (simp add: mask_vmrights_corres)
|
||||
apply (simp add: vm_attributes_corres)
|
||||
apply (rule corres_splitEE)
|
||||
prefer 2
|
||||
apply (erule ensure_safe_mapping_corres)
|
||||
apply (rule corres_trivial)
|
||||
apply (rule corres_returnOk)
|
||||
apply (clarsimp simp: archinv_relation_def page_invocation_map_def)
|
||||
apply (wp hoare_whenE_wp check_vp_wpR)+
|
||||
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
|
||||
split: vmpage_size.splits)
|
||||
apply (clarsimp simp: valid_cap'_def)
|
||||
apply simp
|
||||
apply (rule whenE_throwError_wp[unfolded validE_R_def])
|
||||
apply (wp hoare_whenE_wp)+
|
||||
apply (rule hoare_drop_imps)+
|
||||
apply (simp add:not_le)
|
||||
apply (wp hoare_drop_imps)+
|
||||
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> [])")
|
||||
subgoal by (auto split: list.split)
|
||||
apply (simp add: Let_def split: list.split)
|
||||
apply (case_tac args, simp)
|
||||
apply (clarsimp simp: split_def)
|
||||
apply (rename_tac w1 w2 w3)
|
||||
apply (case_tac excaps', simp)
|
||||
apply clarsimp
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_splitEE [where r' = "(=)"])
|
||||
prefer 2
|
||||
apply (clarsimp simp: list_all2_Cons2)
|
||||
apply (case_tac "fst (hd excaps)", simp_all)[1]
|
||||
apply clarsimp
|
||||
apply (rename_tac arch_capa arch_capb)
|
||||
apply (case_tac arch_capa, simp_all)[1]
|
||||
apply (rename_tac opt)
|
||||
apply (case_tac opt, simp_all)[1]
|
||||
apply (rule corres_returnOkTT)
|
||||
apply simp
|
||||
apply (simp add: Let_def split: list.split)
|
||||
apply (rule case_option_corresE)
|
||||
apply (rule corres_trivial)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (rule corres_splitEE)
|
||||
prefer 2
|
||||
apply (rule corres_lookup_error)
|
||||
apply (rule find_pd_for_asid_corres[OF refl])
|
||||
apply (rule whenE_throwError_corres)
|
||||
apply simp
|
||||
apply simp
|
||||
apply simp
|
||||
apply (rule corres_splitEE)
|
||||
prefer 2
|
||||
apply (rule check_vp_corres)
|
||||
apply (rule corres_splitEE)
|
||||
prefer 2
|
||||
apply (simp only: addrFromPPtr_def)
|
||||
apply (rule create_mapping_entries_corres[OF _ _ refl refl refl refl])
|
||||
apply (simp add: mask_vmrights_corres)
|
||||
apply (simp add: vm_attributes_corres)
|
||||
apply (rule corres_splitEE)
|
||||
prefer 2
|
||||
apply (erule ensure_safe_mapping_corres)
|
||||
apply (rule corres_trivial)
|
||||
apply (rule corres_returnOk)
|
||||
apply (clarsimp simp: archinv_relation_def page_invocation_map_def)
|
||||
apply wp+
|
||||
apply (rule_tac P="\<lambda>s. 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>
|
||||
page_directory_at (fst pa) s \<and> (\<exists>\<rhd> (fst pa)) s" in hoare_pre(3))
|
||||
apply wp
|
||||
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
|
||||
page_directory_at_aligned_pd_bits
|
||||
split:vmpage_size.splits)
|
||||
apply wp
|
||||
apply (wpc | wp throwE_R | wp_once hoare_drop_imps)+
|
||||
apply clarsimp
|
||||
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)
|
||||
apply (clarsimp split: option.split)
|
||||
apply (rule_tac P="\<nexists>pd asid. pd_cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid))"
|
||||
in corres_symmetric_bool_cases[where Q=\<top> and Q'=\<top>, OF refl])
|
||||
apply (case_tac pd_cap; clarsimp; rename_tac pd_acap pd_acap'; case_tac pd_acap; clarsimp)
|
||||
apply (rule corres_splitEE'[where r'="(=)" and P=\<top> and P'=\<top>])
|
||||
apply (clarsimp simp: corres_returnOkTT)
|
||||
apply (rule_tac F="pd_cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap (fst rv) (Some (snd rv)))"
|
||||
in corres_gen_asm)
|
||||
apply (clarsimp cong: option.case_cong)
|
||||
apply (rename_tac vspace asid)
|
||||
apply wpfix \<comment> \<open>get asid and vspace parameters in schematic preconditions\<close>
|
||||
apply (rule_tac P="map_data = None \<and> kernel_base \<le> vaddr + 2 ^ pageBitsForSize vmpage_size - 1
|
||||
\<or> (\<exists>asid' vaddr'. map_data = Some (asid', vaddr') \<and> (asid',vaddr') \<noteq> (asid,vaddr))"
|
||||
in corres_symmetric_bool_cases[where Q=\<top> and Q'=\<top>, OF refl])
|
||||
apply (erule disjE; clarsimp simp: whenE_def kernel_base_def kernelBase_def ARM.kernelBase_def
|
||||
split: option.splits)
|
||||
apply clarsimp
|
||||
apply (rule corres_splitEE'[where r'=dc and P=\<top> and P'=\<top>])
|
||||
apply (case_tac map_data
|
||||
; clarsimp simp: whenE_def kernel_base_def kernelBase_def ARM.kernelBase_def
|
||||
corres_returnOkTT)
|
||||
\<comment> \<open>pd=undefined as vspace_at_asid not used in find_pd_for_asid_corres and avoid unresolved schematics\<close>
|
||||
apply (rule corres_splitEE'[
|
||||
OF corres_lookup_error[OF find_pd_for_asid_corres[where pd=undefined, OF refl]]])
|
||||
apply (rule whenE_throwError_corres; simp)
|
||||
apply (rule corres_splitEE'[where r'=dc, OF check_vp_corres])
|
||||
apply (rule corres_splitEE'[OF create_mapping_entries_corres]
|
||||
; simp add: mask_vmrights_corres vm_attributes_corres)
|
||||
apply (rule corres_splitEE'[OF ensure_safe_mapping_corres], assumption)
|
||||
apply (rule corres_returnOkTT)
|
||||
\<comment> \<open>program split done, now prove resulting preconditions and Hoare triples\<close>
|
||||
apply (simp add: archinv_relation_def page_invocation_map_def)
|
||||
apply wpsimp+
|
||||
apply (wp find_pd_for_asid_pd_at_asid_again)
|
||||
apply (wp findPDForASID_pd_at_wp)
|
||||
apply wpsimp
|
||||
apply wpsimp
|
||||
apply wpsimp
|
||||
apply wpsimp
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state cong: conj_cong)
|
||||
apply (rename_tac pd_ptr asid')
|
||||
apply (prop_tac "is_aligned pd_ptr pd_bits")
|
||||
apply (clarsimp simp: valid_cap_simps cap_aligned_def pd_bits)
|
||||
apply (prop_tac "\<forall>vaddr. lookup_pd_slot pd_ptr vaddr && ~~ mask pd_bits = pd_ptr")
|
||||
apply (clarsimp simp: lookup_pd_slot_eq)
|
||||
apply (fastforce simp: valid_cap_simps mask_def aligned_sum_less_kernel_base word_not_le
|
||||
vmsz_aligned_def vspace_at_asid_def
|
||||
intro!: page_directory_pde_at_lookupI page_directory_at_aligned_pd_bits)
|
||||
apply fastforce
|
||||
|
||||
apply (simp split del: if_split)
|
||||
|
|
@ -1124,7 +1046,6 @@ shows
|
|||
apply (rule corres_splitEE)
|
||||
prefer 2
|
||||
apply (simp add: pageBits_def ptBits_def pdeBits_def)
|
||||
(* apply (rule get_pde_corres') *)
|
||||
apply (rule get_master_pde_corres')
|
||||
apply (simp add: unlessE_whenE)
|
||||
apply (rule corres_splitEE)
|
||||
|
|
@ -1782,59 +1703,41 @@ lemma arch_decodeInvocation_wf[wp]:
|
|||
apply (simp add: decodeARMMMUInvocation_def ARM_H.decodeInvocation_def
|
||||
Let_def split_def isCap_simps
|
||||
cong: if_cong split del: if_split)
|
||||
|
||||
apply (cases "invocation_type label = ArchInvocationLabel ARMPageMap")
|
||||
apply (rename_tac word vmrights vmpage_size option)
|
||||
apply (simp add: split_def split del: if_split
|
||||
cong: list.case_cong prod.case_cong)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp|wpc|simp add:valid_arch_inv'_def valid_page_inv'_def)+
|
||||
apply (wpsimp simp: valid_arch_inv'_def valid_page_inv'_def)
|
||||
apply (rule hoare_vcg_conj_lift_R,(wp ensureSafeMapping_inv)[1])+
|
||||
apply ((wp whenE_throwError_wp checkVP_wpR hoare_vcg_const_imp_lift_R
|
||||
ensureSafeMapping_valid_slots_duplicated'
|
||||
createMappingEntries_valid_pde_slots' findPDForASID_page_directory_at'
|
||||
| wpc
|
||||
| simp add: valid_arch_inv'_def valid_page_inv'_def
|
||||
| rule_tac x="fst p" in hoare_imp_eq_substR)+)[8]
|
||||
apply (wpsimp wp: whenE_throwError_wp checkVP_wpR hoare_vcg_const_imp_lift_R
|
||||
hoare_drop_impE_R ensureSafeMapping_valid_slots_duplicated'
|
||||
createMappingEntries_valid_pde_slots' findPDForASID_page_directory_at'
|
||||
simp: valid_arch_inv'_def valid_page_inv'_def)+
|
||||
apply (clarsimp simp: neq_Nil_conv invs_valid_objs' linorder_not_le
|
||||
cte_wp_at_ctes_of)
|
||||
apply (drule ctes_of_valid', fastforce)+
|
||||
apply (clarsimp simp: diminished_valid' [symmetric])
|
||||
apply (clarsimp simp: valid_cap'_def ptBits_def pageBits_def)
|
||||
apply (clarsimp simp: is_arch_update'_def isCap_simps capAligned_def
|
||||
vmsz_aligned'_def
|
||||
dest!: diminished_capMaster)
|
||||
apply (case_tac option; clarsimp)
|
||||
apply (clarsimp simp: diminished_valid' [symmetric] valid_cap'_def ptBits_def pageBits_def
|
||||
is_arch_update'_def isCap_simps capAligned_def vmsz_aligned'_def
|
||||
dest!: diminished_capMaster cong: conj_cong)
|
||||
apply (rule conjI)
|
||||
apply (erule is_aligned_addrFromPPtr_n, case_tac vmpage_size, simp_all)[1]
|
||||
apply (simp add: vmsz_aligned_def)
|
||||
apply (rule conjI)
|
||||
apply (erule order_le_less_trans[rotated])
|
||||
apply (erule is_aligned_no_overflow'[simplified field_simps])
|
||||
apply (clarsimp simp: page_directory_at'_def pdBits_eq lookup_pd_slot_eq)+
|
||||
apply (clarsimp simp: diminished_valid' [symmetric] valid_cap'_def ptBits_def pageBits_def
|
||||
is_arch_update'_def isCap_simps capAligned_def vmsz_aligned'_def
|
||||
dest!: diminished_capMaster cong: conj_cong)
|
||||
|
||||
apply (rule conjI)
|
||||
apply (erule is_aligned_addrFromPPtr_n, case_tac vmpage_size, simp_all)[1]
|
||||
apply (simp add:vmsz_aligned_def)
|
||||
apply (erule order_le_less_trans[rotated])
|
||||
apply (erule is_aligned_no_overflow'[simplified field_simps])
|
||||
apply (cases "invocation_type label = ArchInvocationLabel ARMPageRemap")
|
||||
apply (rename_tac word vmrights vmpage_size option)
|
||||
apply (simp add: split_def invs_valid_objs' split del: if_split
|
||||
cong: list.case_cong prod.case_cong)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp|wpc|simp add:valid_arch_inv'_def valid_page_inv'_def)+
|
||||
apply (rule hoare_vcg_conj_lift_R,(wp ensureSafeMapping_inv)[1])+
|
||||
apply ((wp whenE_throwError_wp checkVP_wpR hoare_vcg_const_imp_lift_R
|
||||
ensureSafeMapping_valid_slots_duplicated'
|
||||
createMappingEntries_valid_pde_slots'
|
||||
| wpc
|
||||
| simp add: valid_arch_inv'_def valid_page_inv'_def)+)[6]
|
||||
apply (simp add: eq_commute[where b="fst x" for x])
|
||||
apply ((wp whenE_throwError_wp checkVP_wpR hoare_vcg_const_imp_lift_R
|
||||
hoare_drop_impE_R findPDForASID_page_directory_at'
|
||||
createMappingEntries_valid_pde_slots'
|
||||
| wpc
|
||||
| simp add: valid_arch_inv'_def valid_page_inv'_def)+)[3]
|
||||
apply (clarsimp simp: invs_valid_objs' linorder_not_le
|
||||
cte_wp_at_ctes_of)
|
||||
apply (drule ctes_of_valid', fastforce)+
|
||||
apply (clarsimp simp: diminished_valid' [symmetric])
|
||||
apply (clarsimp simp: valid_cap'_def ptBits_def pageBits_def)
|
||||
apply (clarsimp simp: is_arch_update'_def isCap_simps capAligned_def
|
||||
vmsz_aligned'_def pdBits_def pageBits_def vmsz_aligned_def
|
||||
dest!: diminished_capMaster)
|
||||
apply (erule is_aligned_addrFromPPtr_n, case_tac vmpage_size, simp_all)[1]
|
||||
apply (simp add: vmsz_aligned_def pd_bits)
|
||||
apply (clarsimp simp: page_directory_at'_def lookup_pd_slot_eq[simplified pd_bits])
|
||||
|
||||
apply (cases "invocation_type label = ArchInvocationLabel ARMPageUnmap")
|
||||
apply (simp split del: if_split)
|
||||
apply (rule hoare_pre, wp)
|
||||
|
|
|
|||
|
|
@ -3311,6 +3311,18 @@ lemma valid_bitmap_valid_bitmapQ_exceptI[intro]:
|
|||
unfolding valid_bitmapQ_except_def valid_bitmapQ_def
|
||||
by simp
|
||||
|
||||
lemma pdBits_eq: "pdBits = pd_bits"
|
||||
by (simp add: pd_bits_def pdBits_def pdeBits_def pageBits_def)
|
||||
|
||||
lemma ptBits_eq: "ptBits = pt_bits"
|
||||
by (simp add: pt_bits_def ptBits_def pteBits_def pageBits_def)
|
||||
|
||||
lemma largePagePTE_offset_eq: "largePagePTE_offsets = largePagePTEOffsets"
|
||||
by (simp add: largePagePTE_offsets_def largePagePTEOffsets_def pteBits_def)
|
||||
|
||||
lemma superSectionPDE_offsets_eq: "superSectionPDE_offsets = superSectionPDEOffsets"
|
||||
by (simp add: superSectionPDE_offsets_def superSectionPDEOffsets_def pdeBits_def)
|
||||
|
||||
lemma mask_wordRadix_less_wordBits:
|
||||
assumes sz: "wordRadix \<le> size w"
|
||||
shows "unat ((w::'a::len word) && mask wordRadix) < wordBits"
|
||||
|
|
|
|||
|
|
@ -1900,64 +1900,6 @@ lemma performPageInvocation_valid_duplicates'[wp]:
|
|||
\<comment> \<open>PageFlush\<close>
|
||||
apply (simp_all add:performPageInvocation_def pteCheckIfMapped_def pdeCheckIfMapped_def)
|
||||
apply ((wp|simp|wpc)+)[2]
|
||||
\<comment> \<open>PageRemap\<close>
|
||||
apply (rename_tac word sum)
|
||||
apply (case_tac sum)
|
||||
apply (case_tac a)
|
||||
apply (case_tac aa)
|
||||
apply (clarsimp simp:valid_arch_inv'_def
|
||||
valid_page_inv'_def valid_slots'_def
|
||||
valid_slots_duplicated'_def mapM_singleton)
|
||||
apply (wp PageTableDuplicates.storePTE_no_duplicates' getPTE_wp | simp)+
|
||||
apply (simp add:vs_entry_align_def)
|
||||
apply (subst mapM_discarded)
|
||||
apply clarsimp
|
||||
apply (rule hoare_seq_ext[OF _ getObject_pte_sp])
|
||||
apply (clarsimp simp:valid_arch_inv'_def valid_page_inv'_def valid_slots'_def
|
||||
valid_slots_duplicated'_def)
|
||||
apply (wp|simp)+
|
||||
apply (rule_tac sz = 6 and ptr = "p && ~~ mask ptBits" and word = p
|
||||
in mapM_x_storePTE_update_helper)
|
||||
apply (simp add:invs_pspace_aligned' pageBits_def ptBits_def)
|
||||
apply (subst mapM_discarded)
|
||||
apply (clarsimp simp:valid_arch_inv'_def
|
||||
valid_page_inv'_def valid_slots'_def
|
||||
valid_slots_duplicated'_def mapM_x_singleton)
|
||||
apply (rule hoare_seq_ext[OF _ getObject_pte_sp])
|
||||
apply (wp PageTableDuplicates.storePTE_no_duplicates' | simp)+
|
||||
apply (simp add:vs_entry_align_def)
|
||||
apply (subst mapM_discarded)+
|
||||
apply (case_tac b)
|
||||
apply (case_tac a)
|
||||
apply (clarsimp simp:valid_arch_inv'_def
|
||||
valid_page_inv'_def valid_slots'_def
|
||||
valid_slots_duplicated'_def mapM_x_singleton)
|
||||
apply (rule hoare_seq_ext[OF _ getObject_pde_sp])
|
||||
apply (wp PageTableDuplicates.storePDE_no_duplicates' | simp add: when_def)+
|
||||
apply (simp add: vs_entry_align_def)+
|
||||
apply (rule hoare_seq_ext[OF _ getObject_pde_sp])
|
||||
apply (clarsimp simp:valid_arch_inv'_def vs_entry_align_def
|
||||
valid_page_inv'_def valid_slots'_def
|
||||
valid_slots_duplicated'_def mapM_x_singleton)
|
||||
apply (wp|wpc|simp add:vs_entry_align_def)+
|
||||
apply ((wp PageTableDuplicates.storePDE_no_duplicates' | wpc | simp)+)[1]
|
||||
apply (simp add: vs_entry_align_def)+
|
||||
apply (rule hoare_seq_ext[OF _ getObject_pde_sp])
|
||||
apply (clarsimp simp:valid_arch_inv'_def
|
||||
valid_page_inv'_def valid_slots'_def
|
||||
valid_slots_duplicated'_def mapM_x_singleton)
|
||||
apply (wp|wpc|simp add:vs_entry_align_def)+
|
||||
apply (wp PageTableDuplicates.storePDE_no_duplicates')
|
||||
apply (simp add: vs_entry_align_def)+
|
||||
apply (rule hoare_seq_ext[OF _ getObject_pde_sp])
|
||||
apply (clarsimp simp:valid_arch_inv'_def
|
||||
valid_page_inv'_def valid_slots'_def
|
||||
valid_slots_duplicated'_def mapM_x_singleton)
|
||||
apply (wp|wpc|simp add:vs_entry_align_def)+
|
||||
apply (rule_tac sz = 6 and ptr = "p && ~~ mask pdBits" and word = p
|
||||
in mapM_x_storePDE_update_helper)
|
||||
apply (simp add:invs_pspace_aligned' ptBits_def
|
||||
pdBits_def field_simps pageBits_def)+
|
||||
\<comment> \<open>PageMap\<close>
|
||||
apply (clarsimp simp: pteCheckIfMapped_def pdeCheckIfMapped_def)
|
||||
apply (clarsimp simp:valid_pde_slots'_def valid_page_inv'_def
|
||||
|
|
|
|||
|
|
@ -1719,9 +1719,6 @@ definition
|
|||
\<exists>c' m'. pgi' = PageMap a c' (cte_map ptr) m' \<and>
|
||||
cap_relation c c' \<and>
|
||||
mapping_map m m'
|
||||
|
||||
| ARM_A.PageRemap a m \<Rightarrow>
|
||||
\<exists>m'. pgi' = PageRemap a m' \<and> mapping_map m m'
|
||||
| ARM_A.PageUnmap c ptr \<Rightarrow>
|
||||
\<exists>c'. pgi' = PageUnmap c' (cte_map ptr) \<and>
|
||||
acap_relation c c'
|
||||
|
|
@ -1887,7 +1884,6 @@ definition
|
|||
PageMap asid cap ptr m \<Rightarrow>
|
||||
cte_wp_at' (is_arch_update' cap) ptr and valid_slots' m and valid_cap' cap
|
||||
and K (valid_pde_slots' m) and (valid_slots_duplicated' m)
|
||||
| PageRemap asid m \<Rightarrow> valid_slots' m and K (valid_pde_slots' m) and (valid_slots_duplicated' m)
|
||||
| PageUnmap cap ptr \<Rightarrow>
|
||||
\<lambda>s. \<exists>d r R sz m. cap = PageCap d r R sz m \<and>
|
||||
cte_wp_at' (is_arch_update' (ArchObjectCap cap)) ptr s \<and>
|
||||
|
|
@ -2109,6 +2105,16 @@ lemma set_mrs_invs'[wp]:
|
|||
simp add: zipWithM_x_mapM split_def)+
|
||||
done
|
||||
|
||||
lemma same_refs_vs_cap_ref_eq:
|
||||
assumes "valid_slots entries s"
|
||||
assumes "same_refs entries cap s"
|
||||
assumes "same_refs entries cap' s"
|
||||
shows "vs_cap_ref cap = vs_cap_ref cap'"
|
||||
using assms
|
||||
apply (cases entries; clarsimp simp: same_refs_def valid_slots_def)
|
||||
apply (all \<open>rename_tac pte slots p; case_tac slots; clarsimp\<close>)
|
||||
done
|
||||
|
||||
lemma perform_page_corres:
|
||||
assumes "page_invocation_map pgi pgi'"
|
||||
shows "corres dc (invs and valid_etcbs and valid_page_inv pgi)
|
||||
|
|
@ -2116,245 +2122,172 @@ lemma perform_page_corres:
|
|||
(perform_page_invocation pgi) (performPageInvocation pgi')"
|
||||
proof -
|
||||
have pull_out_P:
|
||||
"\<And>P s Q c p. P s \<and> (\<forall>c. caps_of_state s p = Some c \<longrightarrow> Q s c) \<longrightarrow> (\<forall>c. caps_of_state s p = Some c \<longrightarrow> P s \<and> Q s c)"
|
||||
"\<And>P s Q c p. P s \<and> (\<forall>c. caps_of_state s p = Some c \<longrightarrow> Q s c) \<longrightarrow>
|
||||
(\<forall>c. caps_of_state s p = Some c \<longrightarrow> P s \<and> Q s c)"
|
||||
by blast
|
||||
show ?thesis
|
||||
using assms
|
||||
apply (cases pgi)
|
||||
apply (rename_tac word cap prod sum)
|
||||
apply (clarsimp simp: perform_page_invocation_def performPageInvocation_def
|
||||
page_invocation_map_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule_tac R="\<lambda>_. invs and (valid_page_map_inv word cap (a,b) sum) and valid_etcbs and (\<lambda>s. caps_of_state s (a,b) = Some cap)"
|
||||
and R'="\<lambda>_. invs' and valid_slots' m' and pspace_aligned' and valid_slots_duplicated' m'
|
||||
and pspace_distinct' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))" in corres_split)
|
||||
prefer 2
|
||||
apply (erule updateCap_same_master)
|
||||
apply (case_tac sum, case_tac aa)
|
||||
apply (clarsimp simp: mapping_map_def valid_slots'_def valid_slots_def valid_page_inv_def neq_Nil_conv valid_page_map_inv_def)
|
||||
apply (rule corres_name_pre)
|
||||
apply (clarsimp simp:mapM_Cons bind_assoc split del: if_split)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF _ pte_check_if_mapped_corres])
|
||||
apply (rule corres_split[OF _ store_pte_corres'])
|
||||
apply (rule corres_split[where r' = dc, OF _ corres_store_pte_with_invalid_tail])
|
||||
apply (rule corres_split[where r'=dc, OF _ corres_machine_op[OF corres_Id]])
|
||||
apply (clarsimp simp add: when_def)
|
||||
apply (rule invalidate_tlb_by_asid_corres_ex)
|
||||
apply (simp add: last_byte_pte_def objBits_simps archObjSize_def pteBits_def)
|
||||
apply simp
|
||||
apply (rule no_fail_cleanCacheRange_PoU)
|
||||
apply (wp hoare_vcg_ex_lift)+
|
||||
apply (clarsimp simp:pte_relation_aligned_def)
|
||||
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])[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)
|
||||
apply (clarsimp dest!:valid_slots_duplicated_pteD')
|
||||
apply (clarsimp simp del: fun_upd_apply simp add: cte_wp_at_caps_of_state)
|
||||
apply (wp add: hoare_vcg_const_Ball_lift store_pte_typ_at store_pte_cte_wp_at hoare_vcg_ex_lift)+
|
||||
apply (wp | simp add: pteCheckIfMapped_def)+
|
||||
apply (clarsimp simp add: cte_wp_at_caps_of_state valid_slots_def parent_for_refs_def empty_refs_def invs_psp_aligned simp del: fun_upd_apply)
|
||||
apply (rule conjI)
|
||||
apply (rule_tac x=aa in exI, rule_tac x=ba in exI)
|
||||
apply (clarsimp simp: is_pt_cap_def cap_asid_def image_def neq_Nil_conv Collect_disj_eq split: Structures_A.cap.splits arch_cap.splits option.splits)
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (drule same_refs_lD)
|
||||
apply (rule_tac x=a in exI, rule_tac x=b in exI)
|
||||
apply clarify
|
||||
apply (drule_tac x=refa in spec)
|
||||
apply clarsimp
|
||||
apply (rule conjI[rotated], fastforce)
|
||||
apply auto[1]
|
||||
apply clarsimp
|
||||
apply (case_tac ba)
|
||||
apply (clarsimp simp: mapping_map_def valid_slots_def valid_slots'_def neq_Nil_conv valid_page_inv_def valid_page_map_inv_def)
|
||||
apply (rule corres_name_pre)
|
||||
apply (clarsimp simp:mapM_Cons bind_assoc split del:if_split)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF _ pde_check_if_mapped_corres])
|
||||
apply (rule corres_split[OF _ store_pde_corres'])
|
||||
apply (rule corres_split[where r'=dc, OF _ corres_store_pde_with_invalid_tail])
|
||||
apply (rule corres_split[where r'=dc,OF _ corres_machine_op[OF corres_Id]])
|
||||
apply (clarsimp simp: when_def)
|
||||
apply (rule invalidate_tlb_by_asid_corres_ex)
|
||||
apply (simp add: last_byte_pde_def objBits_simps archObjSize_def pdeBits_def)
|
||||
apply simp
|
||||
apply (rule no_fail_cleanCacheRange_PoU)
|
||||
apply (wp hoare_vcg_ex_lift)+
|
||||
apply (clarsimp simp: pde_relation_aligned_def)
|
||||
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])[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)
|
||||
apply (clarsimp dest!:valid_slots_duplicated_pdeD')
|
||||
apply (clarsimp simp add: cte_wp_at_caps_of_state simp del: fun_upd_apply)
|
||||
apply (wp_trace hoare_vcg_const_Ball_lift store_pde_typ_at hoare_vcg_ex_lift store_pde_pd_at_asid)
|
||||
apply (rule hoare_vcg_conj_lift)
|
||||
apply (rule_tac slots="y # ys" in store_pde_invs_unmap')
|
||||
apply (wp hoare_vcg_const_Ball_lift store_pde_pd_at_asid hoare_vcg_ex_lift)
|
||||
apply (wp | simp add: pdeCheckIfMapped_def)+
|
||||
apply (clarsimp simp add: cte_wp_at_caps_of_state valid_slots_def parent_for_refs_def empty_refs_def invs_psp_aligned simp del: fun_upd_apply)
|
||||
apply (rule conjI, rule_tac x=ref in exI, clarsimp)
|
||||
apply (rule conjI)
|
||||
apply (rule_tac x=aa in exI, rule_tac x=ba in exI)
|
||||
apply auto[1]
|
||||
apply (rule conjI)
|
||||
apply (rule_tac x=a in exI, rule_tac x=b in exI, auto simp: same_refs_def)[1]
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: pde_at_def obj_at_def
|
||||
caps_of_state_cteD'[where P=\<top>, simplified])
|
||||
apply (drule_tac cap=capa and ptr="(aa,ba)"
|
||||
in valid_global_refsD[OF invs_valid_global_refs])
|
||||
apply assumption+
|
||||
apply (clarsimp simp: cap_range_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
|
||||
apply (clarsimp split: Structures_A.kernel_object.split_asm if_split_asm ARM_A.arch_kernel_obj.splits)
|
||||
apply (rule conjI[rotated], fastforce)
|
||||
apply (erule ballEI)
|
||||
apply (clarsimp simp: pde_at_def obj_at_def
|
||||
caps_of_state_cteD'[where P=\<top>, simplified])
|
||||
apply (drule_tac cap=capa and ptr="(aa,ba)"
|
||||
in valid_global_refsD[OF invs_valid_global_refs])
|
||||
apply assumption+
|
||||
apply (drule_tac x=x in imageI[where f="\<lambda>x. x && ~~ mask pd_bits"])
|
||||
apply (drule (1) subsetD)
|
||||
apply (clarsimp simp: cap_range_def)
|
||||
apply clarsimp
|
||||
apply (wp_trace arch_update_cap_invs_map set_cap_valid_page_map_inv)
|
||||
apply (wp arch_update_updateCap_invs)
|
||||
apply (clarsimp simp: invs_valid_objs invs_psp_aligned invs_distinct valid_page_inv_def cte_wp_at_caps_of_state is_arch_update_def is_cap_simps)
|
||||
apply (simp add: cap_master_cap_def split: cap.splits arch_cap.splits)
|
||||
apply (auto simp: cte_wp_at_ctes_of valid_page_inv'_def)[1]
|
||||
\<comment> \<open>PageRemap\<close>
|
||||
apply (rename_tac word sum)
|
||||
apply (clarsimp simp: perform_page_invocation_def performPageInvocation_def
|
||||
page_invocation_map_def)
|
||||
apply (case_tac sum)
|
||||
apply simp
|
||||
apply (case_tac a, simp)
|
||||
apply (clarsimp simp: mapping_map_def)
|
||||
apply (rule corres_name_pre)
|
||||
apply (clarsimp simp:mapM_Cons mapM_x_mapM bind_assoc valid_slots_def valid_page_inv_def
|
||||
neq_Nil_conv split del: if_split)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF _ pte_check_if_mapped_corres])
|
||||
apply (rule corres_split[OF _ store_pte_corres'])
|
||||
apply (rule corres_split[OF _ corres_store_pte_with_invalid_tail])
|
||||
apply (rule corres_split[where r' = dc,OF _ corres_machine_op[OF corres_Id]])
|
||||
apply (clarsimp simp: when_def)
|
||||
apply (rule invalidate_tlb_by_asid_corres_ex)
|
||||
apply (simp add: last_byte_pte_def objBits_simps archObjSize_def pteBits_def)
|
||||
apply simp
|
||||
apply (rule no_fail_cleanCacheRange_PoU)
|
||||
apply (wp hoare_vcg_ex_lift)+
|
||||
apply (clarsimp simp:valid_page_inv'_def)
|
||||
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])[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)
|
||||
apply (clarsimp dest!:valid_slots_duplicated_pteD')
|
||||
apply (clarsimp simp del: fun_upd_apply simp add: cte_wp_at_caps_of_state)
|
||||
apply (wp_trace add: hoare_vcg_const_Ball_lift store_pte_typ_at store_pte_cte_wp_at hoare_vcg_ex_lift)
|
||||
apply (wp | simp add: pteCheckIfMapped_def)+
|
||||
apply (clarsimp simp add: cte_wp_at_caps_of_state valid_slots_def parent_for_refs_def empty_refs_def invs_psp_aligned is_cap_simps simp del: fun_upd_apply)
|
||||
apply (rule conjI)
|
||||
apply fastforce
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (rule_tac x=ac in exI, rule_tac x=bb in exI, rule_tac x=capa in exI)
|
||||
apply (drule same_refs_lD)
|
||||
apply clarsimp
|
||||
apply (erule (2) ref_is_unique[OF _ _ reachable_page_table_not_global])
|
||||
apply (simp_all add: invs_def valid_state_def valid_arch_state_def valid_arch_caps_def valid_pspace_def valid_objs_caps)[9]
|
||||
apply fastforce
|
||||
apply auto[1]
|
||||
apply simp
|
||||
apply (case_tac b)
|
||||
apply (rule corres_name_pre)
|
||||
apply (clarsimp simp: mapping_map_def valid_page_inv_def
|
||||
mapM_x_mapM mapM_Cons bind_assoc
|
||||
valid_slots_def neq_Nil_conv split del:if_split)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF _ pde_check_if_mapped_corres])
|
||||
apply (rule corres_split[OF _ store_pde_corres'])
|
||||
apply (rule corres_split[where r'=dc, OF _ corres_store_pde_with_invalid_tail])
|
||||
apply (rule corres_split[where r'=dc,OF _ corres_machine_op[OF corres_Id]])
|
||||
apply (clarsimp simp: when_def)
|
||||
apply (rule invalidate_tlb_by_asid_corres_ex)
|
||||
apply (simp add: last_byte_pde_def objBits_simps archObjSize_def
|
||||
pd_bits_def mask_def pdeBits_def)
|
||||
apply simp
|
||||
apply (rule no_fail_cleanCacheRange_PoU)
|
||||
apply (wp hoare_vcg_ex_lift)+
|
||||
apply (clarsimp simp: pde_relation_aligned_def valid_page_inv'_def)
|
||||
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])[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)
|
||||
apply (clarsimp dest!:valid_slots_duplicated_pdeD')
|
||||
apply (clarsimp simp add: cte_wp_at_caps_of_state simp del: fun_upd_apply)
|
||||
apply (wp_trace hoare_vcg_const_Ball_lift store_pde_typ_at hoare_vcg_ex_lift store_pde_pd_at_asid)
|
||||
apply (rule hoare_vcg_conj_lift)
|
||||
apply (rule_tac slots="y # ys" in store_pde_invs_unmap')
|
||||
apply (wp hoare_vcg_const_Ball_lift store_pde_pd_at_asid hoare_vcg_ex_lift)
|
||||
apply (wp | simp add: pdeCheckIfMapped_def)+
|
||||
apply (clarsimp simp add: cte_wp_at_caps_of_state valid_slots_def parent_for_refs_def empty_refs_def invs_psp_aligned simp del: fun_upd_apply)
|
||||
apply (rule conjI, rule_tac x=ref in exI, clarsimp)
|
||||
apply (frule valid_global_refsD2)
|
||||
apply (clarsimp simp: cap_range_def)+
|
||||
apply (rule conjI)
|
||||
apply (rule_tac x=ac in exI, rule_tac x=bb in exI, rule_tac x=cap in exI)
|
||||
apply (erule conjI)
|
||||
apply clarsimp
|
||||
apply (rule conjI)
|
||||
apply (rule_tac x=ad in exI, rule_tac x=bc in exI, rule_tac x=capa in exI)
|
||||
apply (clarsimp simp: same_refs_def pde_ref_def pde_ref_pages_def
|
||||
valid_pde_def invs_def valid_state_def valid_pspace_def)
|
||||
apply (drule valid_objs_caps)
|
||||
apply (clarsimp simp: valid_caps_def)
|
||||
apply (drule spec, drule spec, drule_tac x=capa in spec, drule (1) mp)
|
||||
apply (case_tac aa, simp_all)
|
||||
apply (erule(1) data_at_pg_cap[rotated],fastforce)+
|
||||
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
|
||||
apply (case_tac ko, simp_all split: if_split_asm)[1]
|
||||
apply (rename_tac arch_kernel_obj)
|
||||
apply (case_tac arch_kernel_obj, simp_all)
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (drule_tac ptr="(ac,bb)" in
|
||||
valid_global_refsD[OF invs_valid_global_refs caps_of_state_cteD])
|
||||
apply (simp split: if_split_asm)+
|
||||
apply force
|
||||
apply (rule conjI[rotated], fastforce)
|
||||
apply (erule ballEI)
|
||||
apply clarsimp
|
||||
apply (drule_tac ptr="(ac,bb)" in
|
||||
valid_global_refsD[OF invs_valid_global_refs caps_of_state_cteD])
|
||||
apply (force split: if_split_asm)+
|
||||
apply (auto split: if_split_asm)[1]
|
||||
apply (clarsimp simp: performPageInvocation_def perform_page_invocation_def
|
||||
apply (rename_tac word cap prod sum)
|
||||
\<comment> \<open>PageMap\<close>
|
||||
apply (clarsimp simp: perform_page_invocation_def performPageInvocation_def
|
||||
page_invocation_map_def)
|
||||
apply (rule corres_assume_pre)
|
||||
apply (clarsimp simp: valid_page_inv_def valid_page_inv'_def isCap_simps is_page_cap_def cong: option.case_cong prod.case_cong)
|
||||
apply (case_tac m)
|
||||
apply simp
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split [where r'="acap_relation"])
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule_tac R="\<lambda>_. invs and (valid_page_map_inv word cap (a,b) sum)
|
||||
and valid_etcbs and (\<lambda>s. caps_of_state s (a,b) = Some cap)"
|
||||
and R'="\<lambda>_. invs' and valid_slots' m' and pspace_aligned' and valid_slots_duplicated' m'
|
||||
and pspace_distinct' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))" in corres_split)
|
||||
prefer 2
|
||||
apply (erule updateCap_same_master)
|
||||
apply (case_tac sum, case_tac aa)
|
||||
apply (clarsimp simp: mapping_map_def valid_slots'_def valid_slots_def valid_page_inv_def
|
||||
neq_Nil_conv valid_page_map_inv_def)
|
||||
apply (rule corres_name_pre)
|
||||
apply (clarsimp simp: mapM_Cons bind_assoc split del: if_split)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF _ pte_check_if_mapped_corres])
|
||||
apply (rule corres_split[OF _ store_pte_corres'])
|
||||
apply (rule corres_split[where r' = dc, OF _ corres_store_pte_with_invalid_tail])
|
||||
apply (rule corres_split[where r'=dc, OF _ corres_machine_op[OF corres_Id]])
|
||||
apply (clarsimp simp add: when_def)
|
||||
apply (rule invalidate_tlb_by_asid_corres_ex)
|
||||
apply (simp add: last_byte_pte_def objBits_simps archObjSize_def pteBits_def)
|
||||
apply simp
|
||||
apply (rule no_fail_cleanCacheRange_PoU)
|
||||
apply (wp hoare_vcg_ex_lift)+
|
||||
apply (clarsimp simp: pte_relation_aligned_def)
|
||||
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])[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)
|
||||
apply (clarsimp dest!:valid_slots_duplicated_pteD')
|
||||
apply (clarsimp simp del: fun_upd_apply simp add: cte_wp_at_caps_of_state)
|
||||
apply (wp hoare_vcg_const_Ball_lift store_pte_typ_at store_pte_cte_wp_at
|
||||
hoare_vcg_ex_lift)+
|
||||
apply (wpsimp simp: pteCheckIfMapped_def)
|
||||
apply (clarsimp simp add: cte_wp_at_caps_of_state valid_slots_def parent_for_refs_def
|
||||
empty_refs_def invs_psp_aligned
|
||||
simp del: fun_upd_apply)
|
||||
apply (rule conjI)
|
||||
apply (rule_tac x=aa in exI, rule_tac x=ba in exI)
|
||||
apply (clarsimp simp: is_pt_cap_def cap_asid_def image_def neq_Nil_conv Collect_disj_eq
|
||||
split: Structures_A.cap.splits arch_cap.splits option.splits)
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (drule same_refs_lD)
|
||||
apply (rule_tac x=a in exI, rule_tac x=b in exI)
|
||||
apply clarify
|
||||
apply (drule_tac x=refa in spec)
|
||||
apply clarsimp
|
||||
apply (rule conjI[rotated], fastforce)
|
||||
apply auto[1]
|
||||
apply clarsimp
|
||||
apply (case_tac ba)
|
||||
apply (clarsimp simp: mapping_map_def valid_slots_def valid_slots'_def neq_Nil_conv
|
||||
valid_page_inv_def valid_page_map_inv_def)
|
||||
apply (rule corres_name_pre)
|
||||
apply (clarsimp simp: mapM_Cons bind_assoc split del:if_split)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF _ pde_check_if_mapped_corres])
|
||||
apply (rule corres_split[OF _ store_pde_corres'])
|
||||
apply (rule corres_split[where r'=dc, OF _ corres_store_pde_with_invalid_tail])
|
||||
apply (rule corres_split[where r'=dc,OF _ corres_machine_op[OF corres_Id]])
|
||||
apply (clarsimp simp: when_def)
|
||||
apply (rule invalidate_tlb_by_asid_corres_ex)
|
||||
apply (simp add: last_byte_pde_def objBits_simps archObjSize_def pdeBits_def)
|
||||
apply simp
|
||||
apply (rule no_fail_cleanCacheRange_PoU)
|
||||
apply (wp hoare_vcg_ex_lift)+
|
||||
apply (clarsimp simp: pde_relation_aligned_def)
|
||||
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])[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)
|
||||
apply (clarsimp dest!:valid_slots_duplicated_pdeD')
|
||||
apply (clarsimp simp add: cte_wp_at_caps_of_state simp del: fun_upd_apply)
|
||||
apply (wp hoare_vcg_const_Ball_lift store_pde_typ_at hoare_vcg_ex_lift
|
||||
store_pde_pd_at_asid)
|
||||
apply (rule hoare_vcg_conj_lift)
|
||||
apply (rule_tac slots="y # ys" in store_pde_invs_unmap')
|
||||
apply (wp hoare_vcg_const_Ball_lift store_pde_pd_at_asid hoare_vcg_ex_lift)
|
||||
apply (wp | simp add: pdeCheckIfMapped_def)+
|
||||
apply (clarsimp simp add: cte_wp_at_caps_of_state valid_slots_def parent_for_refs_def
|
||||
empty_refs_def invs_psp_aligned
|
||||
simp del: fun_upd_apply)
|
||||
apply (rule conjI, rule_tac x=ref in exI, clarsimp)
|
||||
apply (rule conjI)
|
||||
apply (rule_tac x=aa in exI, rule_tac x=ba in exI)
|
||||
apply auto[1]
|
||||
apply (rule conjI)
|
||||
apply (rule_tac x=a in exI, rule_tac x=b in exI, auto simp: same_refs_def)[1]
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: pde_at_def obj_at_def
|
||||
caps_of_state_cteD'[where P=\<top>, simplified])
|
||||
apply (drule_tac cap=capa and ptr="(aa,ba)"
|
||||
in valid_global_refsD[OF invs_valid_global_refs])
|
||||
apply assumption+
|
||||
apply (clarsimp simp: cap_range_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
|
||||
apply (clarsimp split: Structures_A.kernel_object.split_asm if_split_asm
|
||||
ARM_A.arch_kernel_obj.splits)
|
||||
apply (rule conjI[rotated], fastforce)
|
||||
apply (erule ballEI)
|
||||
apply (clarsimp simp: pde_at_def obj_at_def
|
||||
caps_of_state_cteD'[where P=\<top>, simplified])
|
||||
apply (drule_tac cap=capa and ptr="(aa,ba)"
|
||||
in valid_global_refsD[OF invs_valid_global_refs])
|
||||
apply assumption+
|
||||
apply (drule_tac x=x in imageI[where f="\<lambda>x. x && ~~ mask pd_bits"])
|
||||
apply (drule (1) subsetD)
|
||||
apply (clarsimp simp: cap_range_def)
|
||||
apply clarsimp
|
||||
apply (wp_trace arch_update_cap_invs_map set_cap_valid_page_map_inv)
|
||||
apply (wp arch_update_updateCap_invs)
|
||||
apply (clarsimp simp: invs_valid_objs invs_psp_aligned invs_distinct valid_page_inv_def
|
||||
cte_wp_at_caps_of_state is_arch_update_def is_cap_simps)
|
||||
apply (erule (3) subst[OF same_refs_vs_cap_ref_eq, rotated 2])
|
||||
apply (clarsimp simp: invs_pspace_aligned' invs_pspace_distinct' valid_page_inv'_def cte_wp_at'_def)
|
||||
\<comment> \<open>PageUnmap\<close>
|
||||
apply (clarsimp simp: performPageInvocation_def perform_page_invocation_def
|
||||
page_invocation_map_def)
|
||||
apply (rule corres_assume_pre)
|
||||
apply (clarsimp simp: valid_page_inv_def valid_page_inv'_def isCap_simps is_page_cap_def
|
||||
cong: option.case_cong prod.case_cong)
|
||||
apply (case_tac m)
|
||||
apply simp
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split [where r'="acap_relation"])
|
||||
prefer 2
|
||||
apply simp
|
||||
apply (rule corres_rel_imp)
|
||||
apply (rule get_cap_corres_all_rights_P[where P=is_arch_cap], rule refl)
|
||||
apply (clarsimp simp: is_cap_simps)
|
||||
apply (rule_tac F="is_page_cap cap" in corres_gen_asm)
|
||||
apply (rule updateCap_same_master)
|
||||
apply (clarsimp simp: is_page_cap_def update_map_data_def)
|
||||
apply (wp get_cap_wp getSlotCap_wp)+
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_diminished_def)
|
||||
apply (drule (2) diminished_is_update')+
|
||||
apply (clarsimp simp: cap_rights_update_def acap_rights_update_def update_map_data_def is_cap_simps)
|
||||
apply auto[1]
|
||||
apply (auto simp: cte_wp_at_ctes_of)[1]
|
||||
apply clarsimp
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split)
|
||||
prefer 2
|
||||
apply (rule unmap_page_corres)
|
||||
apply (rule corres_split [where r'=acap_relation])
|
||||
prefer 2
|
||||
apply simp
|
||||
apply (rule corres_rel_imp)
|
||||
|
|
@ -2364,56 +2297,38 @@ proof -
|
|||
apply (rule updateCap_same_master)
|
||||
apply (clarsimp simp: is_page_cap_def update_map_data_def)
|
||||
apply (wp get_cap_wp getSlotCap_wp)+
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_diminished_def)
|
||||
apply (drule (2) diminished_is_update')+
|
||||
apply (clarsimp simp: cap_rights_update_def acap_rights_update_def update_map_data_def is_cap_simps)
|
||||
apply auto[1]
|
||||
apply (auto simp: cte_wp_at_ctes_of)[1]
|
||||
apply clarsimp
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split)
|
||||
prefer 2
|
||||
apply (rule unmap_page_corres)
|
||||
apply (rule corres_split [where r'=acap_relation])
|
||||
prefer 2
|
||||
apply simp
|
||||
apply (rule corres_rel_imp)
|
||||
apply (rule get_cap_corres_all_rights_P[where P=is_arch_cap], rule refl)
|
||||
apply (clarsimp simp: is_cap_simps)
|
||||
apply (rule_tac F="is_page_cap cap" in corres_gen_asm)
|
||||
apply (rule updateCap_same_master)
|
||||
apply (clarsimp simp: is_page_cap_def update_map_data_def)
|
||||
apply (wp get_cap_wp getSlotCap_wp)+
|
||||
apply (simp add: cte_wp_at_caps_of_state)
|
||||
apply (strengthen pull_out_P)+
|
||||
apply wp
|
||||
apply (simp add: cte_wp_at_ctes_of)
|
||||
apply (simp add: cte_wp_at_caps_of_state)
|
||||
apply (strengthen pull_out_P)+
|
||||
apply wp
|
||||
apply (clarsimp simp: valid_unmap_def cte_wp_at_caps_of_state)
|
||||
apply (clarsimp simp: is_arch_diminished_def is_cap_simps split: cap.splits arch_cap.splits)
|
||||
apply (drule (2) diminished_is_update')+
|
||||
apply (clarsimp simp: cap_rights_update_def is_page_cap_def cap_master_cap_simps update_map_data_def acap_rights_update_def)
|
||||
apply (clarsimp simp add: valid_cap_def mask_def)
|
||||
apply auto[1]
|
||||
apply (auto simp: cte_wp_at_ctes_of)[1]
|
||||
apply (clarsimp simp: performPageInvocation_def perform_page_invocation_def
|
||||
page_invocation_map_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_when, simp)
|
||||
apply (rule corres_split [OF _ set_vm_root_for_flush_corres])
|
||||
apply (rule corres_split [OF _ corres_machine_op])
|
||||
prefer 2
|
||||
apply (rule do_flush_corres)
|
||||
apply (rule corres_when, simp)
|
||||
apply (rule corres_split [OF _ gct_corres])
|
||||
apply simp
|
||||
apply (rule set_vm_root_corres)
|
||||
apply wp+
|
||||
apply (simp add: cur_tcb_def [symmetric] cur_tcb'_def [symmetric])
|
||||
apply (wp hoare_drop_imps)
|
||||
apply (simp add: cte_wp_at_ctes_of)
|
||||
apply wp
|
||||
apply (clarsimp simp: valid_unmap_def cte_wp_at_caps_of_state)
|
||||
apply (clarsimp simp: is_arch_diminished_def is_cap_simps split: cap.splits arch_cap.splits)
|
||||
apply (drule (2) diminished_is_update')+
|
||||
apply (clarsimp simp: cap_rights_update_def is_page_cap_def cap_master_cap_simps
|
||||
update_map_data_def acap_rights_update_def)
|
||||
apply (clarsimp simp add: valid_cap_def mask_def)
|
||||
apply auto[1]
|
||||
apply (auto simp: cte_wp_at_ctes_of)[1]
|
||||
\<comment> \<open>PageFlush\<close>
|
||||
apply (clarsimp simp: performPageInvocation_def perform_page_invocation_def
|
||||
page_invocation_map_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_when, simp)
|
||||
apply (rule corres_split [OF _ set_vm_root_for_flush_corres])
|
||||
apply (rule corres_split [OF _ corres_machine_op])
|
||||
prefer 2
|
||||
apply (rule do_flush_corres)
|
||||
apply (rule corres_when, simp)
|
||||
apply (rule corres_split [OF _ gct_corres])
|
||||
apply simp
|
||||
apply (rule set_vm_root_corres)
|
||||
apply wp+
|
||||
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])[2]
|
||||
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])[2]
|
||||
\<comment> \<open>PageGetAddr\<close>
|
||||
apply (clarsimp simp: perform_page_invocation_def performPageInvocation_def page_invocation_map_def fromPAddr_def)
|
||||
apply (rule corres_guard_imp)
|
||||
|
|
|
|||
Loading…
Reference in New Issue