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

x64: refine: s/find_pd_for_asid/find_vspace_for_asid/g

This commit is contained in:
Joel Beeren 2017-03-23 15:32:01 +11:00
parent 178b95a6d3
commit 62fb7c8ae8
4 changed files with 79 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
proof/refine/X64/Arch_R.thy
View File

@ -569,7 +569,7 @@ lemma dec_arch_inv_page_flush_corres:
case option of
None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation
| Some x \<Rightarrow> returnOk x;
pd \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid;
pd \<leftarrow> lookup_error_on_failure False $ find_vspace_for_asid asid;
whenE (end \<le> start) $
throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1;
page_size \<leftarrow> returnOk $ 1 << pageBitsForSize vmpage_size;
@ -597,7 +597,7 @@ lemma dec_arch_inv_page_flush_corres:
apply (rule corres_splitEE)
prefer 2
apply (rule corres_lookup_error)
apply (rule find_pd_for_asid_corres)
apply (rule find_vspace_for_asid_corres)
apply (rule whenE_throwError_corres, simp)
apply simp
apply (rule whenE_throwError_corres, simp)
@ -1000,7 +1000,7 @@ shows
valid_cap (cap.ArchObjectCap
(arch_cap.PageDirectoryCap wd (Some optv)))"
in corres_guard_imp)
apply (rule find_pd_for_asid_corres)
apply (rule find_vspace_for_asid_corres)
apply (clarsimp simp: valid_cap_def)
apply (simp add: mask_def)
apply assumption
@ -1078,7 +1078,7 @@ shows
apply (rule corres_splitEE)
prefer 2
apply (rule corres_lookup_error)
apply (rule find_pd_for_asid_corres)
apply (rule find_vspace_for_asid_corres)
apply (rule whenE_throwError_corres)
apply simp
apply simp
@ -1150,7 +1150,7 @@ shows
apply (rule corres_splitEE)
prefer 2
apply (rule corres_lookup_error)
apply (rule find_pd_for_asid_corres)
apply (rule find_vspace_for_asid_corres)
apply (rule whenE_throwError_corres, simp, simp)
apply (rule corres_splitEE)
prefer 2
@ -1172,7 +1172,7 @@ shows
apply (clarsimp simp: archinv_relation_def page_table_invocation_map_def)
apply (clarsimp simp: attribs_from_word_def attribsFromWord_def Let_def)
apply (simp add: shiftr_shiftl1)
apply (wp hoare_whenE_wp get_master_pde_wp getPDE_wp find_pd_for_asid_inv
apply (wp hoare_whenE_wp get_master_pde_wp getPDE_wp find_vspace_for_asid_inv
| wp_once hoare_drop_imps)+
apply (fastforce simp: valid_cap_def mask_def)
apply (clarsimp simp: valid_cap'_def)
@ -1228,7 +1228,7 @@ shows
apply (rule corres_splitEE)
prefer 2
apply (rule corres_lookup_error)
apply (rule find_pd_for_asid_corres)
apply (rule find_vspace_for_asid_corres)
apply (rule whenE_throwError_corres, simp)
apply clarsimp
apply (simp add: liftE_bindE)
@ -1526,9 +1526,9 @@ lemma inv_ASIDPool: "inv ASIDPool = (\<lambda>v. case v of ASIDPool a \<Rightarr
apply simp
done
lemma findPDForASID_aligned[wp]:
"\<lbrace>valid_objs'\<rbrace> findPDForASID p \<lbrace>\<lambda>rv s. is_aligned rv pdBits\<rbrace>,-"
apply (simp add: findPDForASID_def assertE_def cong: option.case_cong
lemma findVSpaceForASID_aligned[wp]:
"\<lbrace>valid_objs'\<rbrace> findVSpaceForASID p \<lbrace>\<lambda>rv s. is_aligned rv pdBits\<rbrace>,-"
apply (simp add: findVSpaceForASID_def assertE_def cong: option.case_cong
split del: if_split)
apply (rule hoare_pre)
apply (wp getASID_wp | wpc)+
@ -1538,11 +1538,11 @@ lemma findPDForASID_aligned[wp]:
split: asidpool.split_asm)
done
lemma findPDForASID_valid_offset'[wp]:
"\<lbrace>valid_objs' and K (vptr < kernelBase)\<rbrace> findPDForASID p
lemma findVSpaceForASID_valid_offset'[wp]:
"\<lbrace>valid_objs' and K (vptr < kernelBase)\<rbrace> findVSpaceForASID p
\<lbrace>\<lambda>rv s. valid_pde_mapping_offset' (rv + (vptr >> 20 << 2) && mask pdBits)\<rbrace>,-"
apply (rule hoare_gen_asmE)
apply (rule hoare_post_imp_R, rule findPDForASID_aligned)
apply (rule hoare_post_imp_R, rule findVSpaceForASID_aligned)
apply (simp add: mask_add_aligned)
apply (erule less_kernelBase_valid_pde_offset'')
done
@ -1563,11 +1563,11 @@ lemma lookupPTSlot_page_table_at':
apply simp
done
lemma findPDForASID_page_directory_at':
lemma findVSpaceForASID_page_directory_at':
notes checkPDAt_inv[wp del]
shows "\<lbrace>\<top>\<rbrace> findPDForASID asiv
shows "\<lbrace>\<top>\<rbrace> findVSpaceForASID asiv
\<lbrace>\<lambda>rv s. page_directory_at' (lookup_pd_slot rv vptr && ~~ mask pdBits) s\<rbrace>,-"
apply (simp add:findPDForASID_def)
apply (simp add:findVSpaceForASID_def)
apply (wp getASID_wp|simp add:checkPDAt_def | wpc)+
apply (clarsimp simp:lookup_pd_slot_def pdBits_def)
apply (subst vaddr_segment_nonsense[unfolded pd_bits_def,simplified])
@ -1825,7 +1825,7 @@ lemma arch_decodeInvocation_wf[wp]:
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'
createMappingEntries_valid_pde_slots' findVSpaceForASID_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]
@ -1856,7 +1856,7 @@ lemma arch_decodeInvocation_wf[wp]:
| 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'
hoare_drop_impE_R findVSpaceForASID_page_directory_at'
createMappingEntries_valid_pde_slots'
| wpc
| simp add: valid_arch_inv'_def valid_page_inv'_def)+)[3]

2
proof/refine/X64/Detype_R.thy
View File

@ -548,7 +548,7 @@ lemma ksASIDMapSafeI:
apply (erule allE)+
apply (erule (1) impE)
apply clarsimp
apply (drule find_pd_for_asid_eq_helper)
apply (drule find_vspace_for_asid_eq_helper)
apply fastforce
apply assumption
apply fastforce

4
proof/refine/X64/PageTableDuplicates.thy
View File

@ -1661,7 +1661,7 @@ crunch valid_duplicates'[wp]:
ignore:getObject updateObject setObject)
crunch valid_duplicates'[wp]:
findPDForASID "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"
findVSpaceForASID "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"
(wp: crunch_wps simp: crunch_simps unless_def
ignore:getObject updateObject setObject)
@ -1745,7 +1745,7 @@ lemma unmapPage_valid_duplicates'[wp]:
(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
K(vmsz_aligned' vptr vmpage_size \<and> is_aligned r pdBits)
and page_directory_at' (lookup_pd_slot r vptr && ~~ mask pdBits)"])
apply (wp findPDForASID_page_directory_at' | simp)+
apply (wp findVSpaceForASID_page_directory_at' | simp)+
apply (clarsimp simp add:pdBits_def pageBits_def vmsz_aligned'_def)
apply (drule is_aligned_lookup_pd_slot)
apply (erule is_aligned_weaken,simp)

116
proof/refine/X64/VSpace_R.thy
View File

@ -38,10 +38,10 @@ defs checkPDASIDMapMembership_def:
crunch inv[wp]:checkPDAt P
lemma findPDForASID_pd_at_wp:
lemma findVSpaceForASID_pd_at_wp:
"\<lbrace>\<lambda>s. \<forall>pd. (page_directory_at' pd s \<longrightarrow> pd_at_asid' pd asid s)
\<longrightarrow> P pd s\<rbrace> findPDForASID asid \<lbrace>P\<rbrace>,-"
apply (simp add: findPDForASID_def assertE_def
\<longrightarrow> P pd s\<rbrace> findVSpaceForASID asid \<lbrace>P\<rbrace>,-"
apply (simp add: findVSpaceForASID_def assertE_def
cong: option.case_cong
split del: if_split)
apply (rule hoare_pre)
@ -53,19 +53,19 @@ lemma findPDForASID_pd_at_wp:
apply fastforce
done
lemma findPDForASIDAssert_pd_at_wp:
lemma findVSpaceForASIDAssert_pd_at_wp:
"\<lbrace>(\<lambda>s. \<forall>pd. pd_at_asid' pd asid s
\<and> pd \<notin> ran ((option_map snd o x64KSASIDMap (ksArchState s) |` (- {asid})))
\<longrightarrow> P pd s)\<rbrace>
findPDForASIDAssert asid \<lbrace>P\<rbrace>"
apply (simp add: findPDForASIDAssert_def const_def
findVSpaceForASIDAssert asid \<lbrace>P\<rbrace>"
apply (simp add: findVSpaceForASIDAssert_def const_def
checkPDAt_def checkPDUniqueToASID_def
checkPDASIDMapMembership_def)
apply (rule hoare_pre, wp getPDE_wp findPDForASID_pd_at_wp)
apply (rule hoare_pre, wp getPDE_wp findVSpaceForASID_pd_at_wp)
apply simp
done
crunch inv[wp]: findPDForASIDAssert "P"
crunch inv[wp]: findVSpaceForASIDAssert "P"
(simp: const_def crunch_simps wp: loadObject_default_inv crunch_wps)
lemma pspace_relation_pd:
@ -89,10 +89,10 @@ lemma pspace_relation_pd:
apply simp
done
lemma find_pd_for_asid_eq_helper:
lemma find_vspace_for_asid_eq_helper:
"\<lbrakk> vspace_at_asid asid pd s; valid_arch_objs s;
asid \<noteq> 0; pspace_aligned s \<rbrakk>
\<Longrightarrow> find_pd_for_asid asid s = returnOk pd s
\<Longrightarrow> find_vspace_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_arch_objs_def)
apply (frule spec, drule mp, erule exI)
@ -119,7 +119,7 @@ lemma find_pd_for_asid_eq_helper:
apply (drule bspec, erule ranI)
apply clarsimp
apply (drule ucast_up_inj, simp)
apply (simp add: find_pd_for_asid_def bind_assoc
apply (simp add: find_vspace_for_asid_def bind_assoc
word_neq_0_conv[symmetric] liftE_bindE)
apply (simp add: exec_gets liftE_bindE bind_assoc
get_asid_pool_def get_object_def)
@ -132,12 +132,12 @@ lemma find_pd_for_asid_eq_helper:
apply (simp add: pdBits_def pageBits_def)
done
lemma find_pd_for_asid_assert_eq:
lemma find_vspace_for_asid_assert_eq:
"\<lbrakk> vspace_at_asid asid pd s; valid_arch_objs s;
asid \<noteq> 0; pspace_aligned s \<rbrakk>
\<Longrightarrow> find_pd_for_asid_assert asid s = return pd s"
apply (drule(3) find_pd_for_asid_eq_helper)
apply (simp add: find_pd_for_asid_assert_def
\<Longrightarrow> find_vspace_for_asid_assert asid s = return pd s"
apply (drule(3) find_vspace_for_asid_eq_helper)
apply (simp add: find_vspace_for_asid_assert_def
catch_def bind_assoc)
apply (clarsimp simp: returnOk_def obj_at_def
a_type_def
@ -150,27 +150,27 @@ lemma find_pd_for_asid_assert_eq:
apply (simp add: exec_gets)
done
lemma find_pd_for_asid_valids:
lemma find_vspace_for_asid_valids:
"\<lbrace> vspace_at_asid asid pd and valid_arch_objs
and pspace_aligned and K (asid \<noteq> 0) \<rbrace>
find_pd_for_asid asid \<lbrace>\<lambda>rv s. pde_at rv s\<rbrace>,-"
find_vspace_for_asid asid \<lbrace>\<lambda>rv s. pde_at rv s\<rbrace>,-"
"\<lbrace> vspace_at_asid asid pd and valid_arch_objs
and pspace_aligned and K (asid \<noteq> 0)
and K (is_aligned pd pdBits \<longrightarrow> P pd) \<rbrace>
find_pd_for_asid asid \<lbrace>\<lambda>rv s. P rv\<rbrace>,-"
find_vspace_for_asid asid \<lbrace>\<lambda>rv s. P rv\<rbrace>,-"
"\<lbrace> vspace_at_asid asid pd and valid_arch_objs
and pspace_aligned and K (asid \<noteq> 0)
and pd_at_uniq asid pd \<rbrace>
find_pd_for_asid asid \<lbrace>\<lambda>rv s. pd_at_uniq asid rv s\<rbrace>,-"
find_vspace_for_asid asid \<lbrace>\<lambda>rv s. pd_at_uniq asid rv s\<rbrace>,-"
"\<lbrace> vspace_at_asid asid pd and valid_arch_objs
and pspace_aligned and K (asid \<noteq> 0) \<rbrace>
find_pd_for_asid asid -,\<lbrace>\<bottom>\<bottom>\<rbrace>"
find_vspace_for_asid asid -,\<lbrace>\<bottom>\<bottom>\<rbrace>"
apply (simp_all add: validE_def validE_R_def validE_E_def
valid_def split: sum.split)
apply (auto simp: returnOk_def return_def
pde_at_def pd_bits_def pdBits_def
pageBits_def is_aligned_neg_mask_eq
dest!: find_pd_for_asid_eq_helper
dest!: find_vspace_for_asid_eq_helper
elim!: is_aligned_weaken)
done
@ -197,17 +197,17 @@ lemma asidBits_asid_bits[simp]:
by (simp add: asid_bits_def asidBits_def
asidHighBits_def asid_low_bits_def)
lemma find_pd_for_asid_assert_corres:
lemma find_vspace_for_asid_assert_corres:
"corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd)
(K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
and pspace_aligned and pspace_distinct
and valid_arch_objs and valid_asid_map
and vspace_at_asid asid pd and pd_at_uniq asid pd)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(find_pd_for_asid_assert asid)
(findPDForASIDAssert asid)"
apply (simp add: find_pd_for_asid_assert_def const_def
findPDForASIDAssert_def liftM_def)
(find_vspace_for_asid_assert asid)
(findVSpaceForASIDAssert asid)"
apply (simp add: find_vspace_for_asid_assert_def const_def
findVSpaceForASIDAssert_def liftM_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule_tac F="is_aligned pda pdBits
@ -260,29 +260,29 @@ lemma find_pd_for_asid_assert_corres:
apply (erule(3) pspace_relation_pd)
apply (simp add: pde_at_def pd_bits_def pdBits_def
is_aligned_neg_mask_eq)
apply (rule corres_split_catch [OF _ find_pd_for_asid_corres'[where pd=pd]])
apply (rule corres_split_catch [OF _ find_vspace_for_asid_corres'[where pd=pd]])
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 (wp find_vspace_for_asid_valids[where pd=pd])+
apply (clarsimp simp: word_neq_0_conv)
apply simp
done
lemma findPDForASIDAssert_known_corres:
lemma findVSpaceForASIDAssert_known_corres:
"corres r P P' f (g pd) \<Longrightarrow>
corres r (vspace_at_asid asid pd and pd_at_uniq asid pd
and valid_arch_objs and valid_asid_map
and pspace_aligned and pspace_distinct
and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits) and P)
(P' and pspace_aligned' and pspace_distinct' and no_0_obj')
f (findPDForASIDAssert asid >>= g)"
f (findVSpaceForASIDAssert asid >>= g)"
apply (subst return_bind[symmetric])
apply (subst corres_cong [OF refl refl _ refl refl])
apply (rule bind_apply_cong [OF _ refl])
apply clarsimp
apply (erule(3) find_pd_for_asid_assert_eq[symmetric])
apply (erule(3) find_vspace_for_asid_assert_eq[symmetric])
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ find_pd_for_asid_assert_corres[where pd=pd]])
apply (rule corres_split [OF _ find_vspace_for_asid_assert_corres[where pd=pd]])
apply simp
apply wp+
apply clarsimp
@ -304,13 +304,13 @@ lemma load_hw_asid_corres:
apply (case_tac "rv' a")
apply simp
apply (rule corres_guard_imp)
apply (rule_tac pd=pd in findPDForASIDAssert_known_corres)
apply (rule_tac pd=pd in findVSpaceForASIDAssert_known_corres)
apply (rule corres_trivial, simp)
apply clarsimp
apply clarsimp
apply clarsimp
apply (rule corres_guard_imp)
apply (rule_tac pd=b in findPDForASIDAssert_known_corres)
apply (rule_tac pd=b in findVSpaceForASIDAssert_known_corres)
apply (rule corres_trivial, simp)
apply (clarsimp simp: valid_arch_state_def valid_asid_map_def)
apply (drule subsetD, erule domI)
@ -332,7 +332,7 @@ lemma store_hw_asid_corres:
(store_hw_asid a h) (storeHWASID a h)"
apply (simp add: store_hw_asid_def storeHWASID_def)
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ find_pd_for_asid_assert_corres[where pd=pd]])
apply (rule corres_split [OF _ find_vspace_for_asid_assert_corres[where pd=pd]])
apply (rule corres_split_eqr)
apply (rule corres_split)
prefer 2
@ -365,7 +365,7 @@ lemma invalidate_asid_corres:
(is "corres dc ?P ?P' ?f ?f'")
apply (simp add: invalidate_asid_def invalidateASID_def)
apply (rule corres_guard_imp)
apply (rule_tac pd=pd in findPDForASIDAssert_known_corres)
apply (rule_tac pd=pd in findVSpaceForASIDAssert_known_corres)
apply (rule_tac P="?P" and P'="?P'" in corres_inst)
apply (rule_tac r'="op =" in corres_split' [OF _ _ gets_sp gets_sp])
apply (clarsimp simp: state_relation_def arch_state_relation_def)
@ -632,17 +632,17 @@ lemma state_relation_asid_map:
"(s, s') \<in> state_relation \<Longrightarrow> x64KSASIDMap (ksArchState s') = x64_asid_map (arch_state s)"
by (simp add: state_relation_def arch_state_relation_def)
lemma find_pd_for_asid_pd_at_asid_again:
lemma find_vspace_for_asid_pd_at_asid_again:
"\<lbrace>\<lambda>s. (\<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s)
\<and> (\<forall>ex. (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> Q ex s)
\<and> valid_arch_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0\<rbrace>
find_pd_for_asid asid
find_vspace_for_asid asid
\<lbrace>P\<rbrace>,\<lbrace>Q\<rbrace>"
apply (unfold validE_def, rule hoare_name_pre_state, fold validE_def)
apply (case_tac "\<exists>pd. vspace_at_asid asid pd s")
apply clarsimp
apply (rule_tac Q="\<lambda>rv s'. s' = s \<and> rv = pd" and E="\<bottom>\<bottom>" in hoare_post_impErr)
apply (rule hoare_pre, wp find_pd_for_asid_valids)
apply (rule hoare_pre, wp find_vspace_for_asid_valids)
apply fastforce
apply simp+
apply (rule_tac Q="\<lambda>rv s'. s' = s \<and> vspace_at_asid asid rv s'"
@ -750,7 +750,7 @@ proof -
apply (clarsimp simp: pd_at_uniq_def restrict_map_def)
apply (erule notE, rule_tac a=x in ranI)
apply simp
apply (rule corres_split_eqrE [OF _ find_pd_for_asid_corres])
apply (rule corres_split_eqrE [OF _ find_vspace_for_asid_corres])
apply (rule whenE_throwError_corres)
apply (simp add: lookup_failure_map_def)
apply simp
@ -758,7 +758,7 @@ proof -
apply (rule x64_context_switch_corres)
apply (wp | simp | wp_once hoare_drop_imps)+
apply (simp add: whenE_def split del: if_split, wp)[1]
apply (rule find_pd_for_asid_pd_at_asid_again)
apply (rule find_vspace_for_asid_pd_at_asid_again)
apply wp
apply clarsimp
apply (frule page_directory_cap_pd_at_uniq, simp+)
@ -801,7 +801,7 @@ lemma loadHWASID_wp [wp]:
"\<lbrace>\<lambda>s. P (option_map fst (x64KSASIDMap (ksArchState s) asid)) s\<rbrace>
loadHWASID asid \<lbrace>P\<rbrace>"
apply (simp add: loadHWASID_def)
apply (wp findPDForASIDAssert_pd_at_wp
apply (wp findVSpaceForASIDAssert_pd_at_wp
| wpc | simp | wp_once hoare_drop_imps)+
apply (auto split: option.split)
done
@ -1152,7 +1152,7 @@ qed
crunch typ_at' [wp]: armv_contextSwitch "\<lambda>s. P (typ_at' T p s)"
(simp: crunch_simps)
crunch typ_at' [wp]: findPDForASID "\<lambda>s. P (typ_at' T p s)"
crunch typ_at' [wp]: findVSpaceForASID "\<lambda>s. P (typ_at' T p s)"
(wp: crunch_wps getObject_inv simp: crunch_simps loadObject_default_def ignore: getObject)
crunch typ_at' [wp]: setVMRoot "\<lambda>s. P (typ_at' T p s)"
@ -1175,11 +1175,11 @@ crunch distinct' [wp]: setVMRootForFlush pspace_distinct'
crunch cur' [wp]: setVMRootForFlush cur_tcb'
(wp: hoare_drop_imps)
lemma findPDForASID_inv2:
"\<lbrace>\<lambda>s. asid \<noteq> 0 \<and> asid \<le> mask asid_bits \<longrightarrow> P s\<rbrace> findPDForASID asid \<lbrace>\<lambda>rv. P\<rbrace>"
lemma findVSpaceForASID_inv2:
"\<lbrace>\<lambda>s. asid \<noteq> 0 \<and> asid \<le> mask asid_bits \<longrightarrow> P s\<rbrace> findVSpaceForASID asid \<lbrace>\<lambda>rv. P\<rbrace>"
apply (cases "asid \<noteq> 0 \<and> asid \<le> mask asid_bits")
apply (simp add: findPDForASID_inv)
apply (simp add: findPDForASID_def assertE_def asidRange_def mask_def)
apply (simp add: findVSpaceForASID_inv)
apply (simp add: findVSpaceForASID_def assertE_def asidRange_def mask_def)
apply clarsimp
done
@ -1195,13 +1195,13 @@ lemma storeHWASID_valid_arch' [wp]:
apply assumption
apply (simp add: valid_arch_state'_def comp_upd_simp fun_upd_def[symmetric])
apply wp
apply (simp add: findPDForASIDAssert_def const_def
apply (simp add: findVSpaceForASIDAssert_def const_def
checkPDUniqueToASID_def checkPDASIDMapMembership_def)
apply wp
apply (rule_tac Q'="\<lambda>rv s. valid_asid_map' (x64KSASIDMap (ksArchState s))
\<and> asid \<noteq> 0 \<and> asid \<le> mask asid_bits"
in hoare_post_imp_R)
apply (wp findPDForASID_inv2)+
apply (wp findVSpaceForASID_inv2)+
apply (clarsimp simp: valid_asid_map'_def)
apply (subst conj_commute, rule context_conjI)
apply clarsimp
@ -1378,9 +1378,9 @@ crunch typ_at' [wp]: flushTable "\<lambda>s. P (typ_at' T p s)"
lemmas flushTable_typ_ats' [wp] = typ_at_lifts [OF flushTable_typ_at']
lemmas findPDForASID_typ_ats' [wp] = typ_at_lifts [OF findPDForASID_typ_at']
lemmas findVSpaceForASID_typ_ats' [wp] = typ_at_lifts [OF findVSpaceForASID_typ_at']
crunch inv [wp]: findPDForASID P
crunch inv [wp]: findVSpaceForASID P
(simp: assertE_def whenE_def loadObject_default_def
wp: crunch_wps getObject_inv ignore: getObject)
@ -1401,7 +1401,7 @@ lemma page_table_mapped_corres:
apply (rule corres_guard_imp)
apply (rule corres_split_catch)
apply (rule corres_trivial, simp)
apply (rule corres_split_eqrE [OF _ find_pd_for_asid_corres])
apply (rule corres_split_eqrE [OF _ find_vspace_for_asid_corres])
apply (simp add: liftE_bindE)
apply (rule corres_split [OF _ get_pde_corres'])
apply (rule corres_trivial)
@ -1544,7 +1544,7 @@ lemma unmap_page_corres:
apply (rule corres_guard_imp)
apply (rule corres_split_catch [where E="\<lambda>_. \<top>" and E'="\<lambda>_. \<top>"], simp)
apply (rule corres_split_strengthen_ftE[where ftr'=dc],
rule find_pd_for_asid_corres)
rule find_vspace_for_asid_corres)
apply (rule corres_splitEE)
apply clarsimp
apply (rule flush_page_corres)
@ -2668,7 +2668,7 @@ lemma storeHWASID_invs:
apply (rule storeHWASID_valid_arch')
apply fastforce
apply (simp add: storeHWASID_def)
apply (wp findPDForASIDAssert_pd_at_wp)
apply (wp findVSpaceForASIDAssert_pd_at_wp)
apply (clarsimp simp: invs'_def valid_state'_def valid_arch_state'_def
valid_global_refs'_def global_refs'_def valid_machine_state'_def
ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
@ -2684,7 +2684,7 @@ lemma storeHWASID_invs_no_cicd':
apply (rule storeHWASID_valid_arch')
apply (fastforce simp: all_invs_but_ct_idle_or_in_cur_domain'_def)
apply (simp add: storeHWASID_def)
apply (wp findPDForASIDAssert_pd_at_wp)
apply (wp findVSpaceForASIDAssert_pd_at_wp)
apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_arch_state'_def
valid_global_refs'_def global_refs'_def valid_machine_state'_def
ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
@ -2698,7 +2698,7 @@ lemma findFreeHWASID_invs:
apply (simp add: findFreeHWASID_def invalidateHWASIDEntry_def invalidateASID_def
doMachineOp_def split_def
cong: option.case_cong)
apply (wp findPDForASIDAssert_pd_at_wp | wpc)+
apply (wp findVSpaceForASIDAssert_pd_at_wp | wpc)+
apply (clarsimp simp: invs'_def valid_state'_def valid_arch_state'_def
valid_global_refs'_def global_refs'_def valid_machine_state'_def
ct_not_inQ_def
@ -2722,7 +2722,7 @@ lemma findFreeHWASID_invs_no_cicd':
apply (simp add: findFreeHWASID_def invalidateHWASIDEntry_def invalidateASID_def
doMachineOp_def split_def
cong: option.case_cong)
apply (wp findPDForASIDAssert_pd_at_wp | wpc)+
apply (wp findVSpaceForASIDAssert_pd_at_wp | wpc)+
apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_arch_state'_def
valid_global_refs'_def global_refs'_def valid_machine_state'_def
ct_not_inQ_def
@ -2850,7 +2850,7 @@ crunch nosch [wp]: setVMRoot "\<lambda>s. P (ksSchedulerAction s)"
(wp: crunch_wps getObject_inv simp: crunch_simps
loadObject_default_def ignore: getObject)
crunch it' [wp]: findPDForASID "\<lambda>s. P (ksIdleThread s)"
crunch it' [wp]: findVSpaceForASID "\<lambda>s. P (ksIdleThread s)"
(simp: crunch_simps loadObject_default_def wp: getObject_inv ignore: getObject)
crunch it' [wp]: deleteASIDPool "\<lambda>s. P (ksIdleThread s)"