arm refine: update for changed corres split rules

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis 2022-08-29 14:00:04 +10:00 committed by Gerwin Klein
parent f9295d6a97
commit 7289575cc7
20 changed files with 2784 additions and 2743 deletions

View File

@ -154,89 +154,89 @@ lemma performASIDControlInvocation_corres:
apply (erule deleteObjects_corres)
apply (simp add:pageBits_def)
apply (rule corres_split[OF getSlotCap_corres])
apply (rule_tac F = " pcap = (cap.UntypedCap False word1 pageBits idxa)" in corres_gen_asm)
apply (rule corres_split[OF updateFreeIndex_corres])
apply (rule corres_split)
apply (simp add: retype_region2_ext_retype_region_ArchObject )
apply (rule corres_retype [where ty="Inl (KOArch (KOASIDPool F))",
unfolded APIType_map2_def makeObjectKO_def,
THEN createObjects_corres',simplified,
where val = "makeObject::asidpool"])
apply simp
apply (simp add: objBits_simps obj_bits_api_def arch_kobj_size_def
default_arch_object_def archObjSize_def)+
apply (simp add: obj_relation_retype_def default_object_def
default_arch_object_def objBits_simps archObjSize_def)
apply (simp add: other_obj_relation_def asid_pool_relation_def)
apply (simp add: makeObject_asidpool const_def inv_def)
apply (rule range_cover_full)
apply (simp add:obj_bits_api_def arch_kobj_size_def default_arch_object_def)+
apply (rule corres_split)
apply (rule cteInsert_simple_corres, simp, rule refl, rule refl)
apply (rule_tac F="is_aligned word2 asid_low_bits" in corres_gen_asm)
apply (simp add: is_aligned_mask dc_def[symmetric])
apply (rule corres_split[where P=\<top> and P'=\<top> and r'="\<lambda>t t'. t = t' o ucast"])
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule corres_trivial)
apply (rule corres_modify)
apply (thin_tac "x \<in> state_relation" for x)
apply (clarsimp simp: state_relation_def arch_state_relation_def o_def)
apply (rule ext)
apply clarsimp
apply (erule_tac P = "x = asid_high_bits_of word2" in notE)
apply (rule word_eqI[rule_format])
apply (drule_tac x1="ucast x" in bang_eq [THEN iffD1])
apply (erule_tac x=n in allE)
apply (simp add: word_size nth_ucast)
apply wp+
apply (strengthen safe_parent_strg[where idx = "2^pageBits"])
apply (strengthen invs_valid_objs invs_distinct
invs_psp_aligned invs_mdb
| simp cong:conj_cong)+
apply (wp retype_region_plain_invs[where sz = pageBits]
retype_cte_wp_at[where sz = pageBits])+
apply (strengthen vp_strgs'
safe_parent_strg'[where idx = "2^pageBits"])
apply (simp cong: conj_cong)
apply (wp createObjects_valid_pspace'
[where sz = pageBits and ty="Inl (KOArch (KOASIDPool undefined))"])
apply (simp add: makeObjectKO_def)+
apply (simp add:objBits_simps archObjSize_def range_cover_full)+
apply (clarsimp simp:valid_cap'_def)
apply (wp createObject_typ_at'
createObjects_orig_cte_wp_at'[where sz = pageBits])
apply (rule descendants_of'_helper)
apply (wp createObjects_null_filter'
[where sz = pageBits and ty="Inl (KOArch (KOASIDPool undefined))"])
apply simp
apply (rule_tac F = " pcap = (cap.UntypedCap False word1 pageBits idxa)" in corres_gen_asm)
apply (rule corres_split[OF updateFreeIndex_corres])
apply (clarsimp simp:is_cap_simps)
apply (simp add: free_index_of_def)
apply (clarsimp simp: conj_comms obj_bits_api_def arch_kobj_size_def
objBits_simps archObjSize_def default_arch_object_def
pred_conj_def)
apply (clarsimp simp: conj_comms
| strengthen invs_mdb invs_valid_pspace)+
apply (simp add:region_in_kernel_window_def)
apply (wp set_untyped_cap_invs_simple[where sz = pageBits]
set_cap_cte_wp_at
set_cap_caps_no_overlap[where sz = pageBits]
set_cap_no_overlap
set_cap_device_and_range_aligned[where dev = False,simplified]
set_untyped_cap_caps_overlap_reserved[where sz = pageBits])+
apply (rule corres_split)
apply (simp add: retype_region2_ext_retype_region_ArchObject )
apply (rule corres_retype [where ty="Inl (KOArch (KOASIDPool F))",
unfolded APIType_map2_def makeObjectKO_def,
THEN createObjects_corres',simplified,
where val = "makeObject::asidpool"])
apply simp
apply (simp add: objBits_simps obj_bits_api_def arch_kobj_size_def
default_arch_object_def archObjSize_def)+
apply (simp add: obj_relation_retype_def default_object_def
default_arch_object_def objBits_simps archObjSize_def)
apply (simp add: other_obj_relation_def asid_pool_relation_def)
apply (simp add: makeObject_asidpool const_def inv_def)
apply (rule range_cover_full)
apply (simp add:obj_bits_api_def arch_kobj_size_def default_arch_object_def)+
apply (rule corres_split)
apply (rule cteInsert_simple_corres, simp, rule refl, rule refl)
apply (rule_tac F="is_aligned word2 asid_low_bits" in corres_gen_asm)
apply (simp add: is_aligned_mask dc_def[symmetric])
apply (rule corres_split[where P=\<top> and P'=\<top> and r'="\<lambda>t t'. t = t' o ucast"])
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule corres_trivial)
apply (rule corres_modify)
apply (thin_tac "x \<in> state_relation" for x)
apply (clarsimp simp: state_relation_def arch_state_relation_def o_def)
apply (rule ext)
apply clarsimp
apply (erule_tac P = "x = asid_high_bits_of word2" in notE)
apply (rule word_eqI[rule_format])
apply (drule_tac x1="ucast x" in bang_eq [THEN iffD1])
apply (erule_tac x=n in allE)
apply (simp add: word_size nth_ucast)
apply wp+
apply (strengthen safe_parent_strg[where idx = "2^pageBits"])
apply (strengthen invs_valid_objs invs_distinct
invs_psp_aligned invs_mdb
| simp cong:conj_cong)+
apply (wp retype_region_plain_invs[where sz = pageBits]
retype_cte_wp_at[where sz = pageBits])+
apply (strengthen vp_strgs'
safe_parent_strg'[where idx = "2^pageBits"])
apply (simp cong: conj_cong)
apply (wp createObjects_valid_pspace'
[where sz = pageBits and ty="Inl (KOArch (KOASIDPool undefined))"])
apply (simp add: makeObjectKO_def)+
apply (simp add:objBits_simps archObjSize_def range_cover_full)+
apply (clarsimp simp:valid_cap'_def)
apply (wp createObject_typ_at'
createObjects_orig_cte_wp_at'[where sz = pageBits])
apply (rule descendants_of'_helper)
apply (wp createObjects_null_filter'
[where sz = pageBits and ty="Inl (KOArch (KOASIDPool undefined))"])
apply (clarsimp simp: conj_comms obj_bits_api_def arch_kobj_size_def
objBits_simps archObjSize_def default_arch_object_def
makeObjectKO_def range_cover_full
simp del: capFreeIndex_update.simps
| strengthen invs_valid_pspace' invs_pspace_aligned'
invs_pspace_distinct'
exI[where x="makeObject :: asidpool"])+
apply (wp updateFreeIndex_forward_invs'
updateFreeIndex_pspace_no_overlap'
updateFreeIndex_caps_no_overlap''
updateFreeIndex_descendants_of2
updateFreeIndex_cte_wp_at
updateFreeIndex_caps_overlap_reserved
| simp add: descendants_of_null_filter' split del: if_split)+
objBits_simps archObjSize_def default_arch_object_def
pred_conj_def)
apply (clarsimp simp: conj_comms
| strengthen invs_mdb invs_valid_pspace)+
apply (simp add:region_in_kernel_window_def)
apply (wp set_untyped_cap_invs_simple[where sz = pageBits]
set_cap_cte_wp_at
set_cap_caps_no_overlap[where sz = pageBits]
set_cap_no_overlap
set_cap_device_and_range_aligned[where dev = False,simplified]
set_untyped_cap_caps_overlap_reserved[where sz = pageBits])+
apply (clarsimp simp: conj_comms obj_bits_api_def arch_kobj_size_def
objBits_simps archObjSize_def default_arch_object_def
makeObjectKO_def range_cover_full
simp del: capFreeIndex_update.simps
| strengthen invs_valid_pspace' invs_pspace_aligned'
invs_pspace_distinct'
exI[where x="makeObject :: asidpool"])+
apply (wp updateFreeIndex_forward_invs'
updateFreeIndex_pspace_no_overlap'
updateFreeIndex_caps_no_overlap''
updateFreeIndex_descendants_of2
updateFreeIndex_cte_wp_at
updateFreeIndex_caps_overlap_reserved
| simp add: descendants_of_null_filter' split del: if_split)+
apply (wp get_cap_wp)+
apply (subgoal_tac "word1 && ~~ mask pageBits = word1 \<and> pageBits \<le> word_bits \<and> word_size_bits \<le> pageBits")
prefer 2
@ -507,6 +507,7 @@ lemma resolveVAddr_corres:
and R'="\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s
\<and> vs_valid_duplicates' (ksPSpace s)"
in corres_split[OF get_master_pde_corres])
apply simp
apply (case_tac rv, simp_all add: pde_relation'_def)[1]
apply (rule corres_stateAssert_assume_stronger)
apply (rule stronger_corres_guard_imp)
@ -767,14 +768,6 @@ 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]
@ -947,7 +940,7 @@ shows
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 (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)
@ -960,18 +953,18 @@ shows
apply (erule disjE; clarsimp simp: whenE_def kernel_base_def pptrBase_def
split: option.splits)
apply clarsimp
apply (rule corres_splitEE'[where r'=dc and P=\<top> and P'=\<top>])
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 pptrBase_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'[
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 checkVPAlignment_corres])
apply (rule corres_splitEE'[OF createMappingEntries_corres]
apply (rule corres_splitEE[where r'=dc, OF checkVPAlignment_corres])
apply (rule corres_splitEE[OF createMappingEntries_corres]
; simp add: mask_vmrights_corres vm_attributes_corres)
apply (rule corres_splitEE'[OF ensureSafeMapping_corres], assumption)
apply (rule corres_splitEE[OF ensureSafeMapping_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)

View File

@ -232,14 +232,13 @@ lemma corres_injection:
\<Longrightarrow> corres (f \<oplus> r) P P' (t m) (t' m')"
apply (simp add: injection_handler_def handleE'_def x y)
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated)
defer
apply (rule corres_split)
apply assumption
apply (rule wp_post_taut)
apply (case_tac v, (clarsimp simp: z)+)
apply (rule wp_post_taut)
apply simp
apply (rule wp_post_taut)
apply simp
apply (case_tac v, (clarsimp simp: z)+)
apply simp
done
lemma rethrowFailure_injection:
@ -425,9 +424,8 @@ lemma corres_empty_on_failure:
apply (simp add: empty_on_failure_def emptyOnFailure_def)
apply (rule corres_guard_imp)
apply (rule corres_split_catch)
apply (rule corres_trivial, simp)
apply (erule corres_rel_imp)
apply (case_tac x; simp)
apply assumption
apply (rule corres_trivial, simp)
apply wp+
apply simp+
done
@ -466,11 +464,9 @@ lemma corres_const_on_failure:
apply (simp add: const_on_failure_def constOnFailure_def)
apply (rule corres_guard_imp)
apply (rule corres_split_catch)
apply (rule corres_trivial, simp)
apply (erule corres_rel_imp)
apply (case_tac xa)
apply (clarsimp simp: const_def)
apply simp
apply assumption
apply (rule corres_trivial, simp)
apply (clarsimp simp: const_def)
apply wp+
apply simp+
done

View File

@ -172,50 +172,52 @@ lemma decodeCNodeInvocation_corres:
split del: if_split
cong: if_cong list.case_cong)
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rule corres_splitEE[OF ensureEmptySlot_corres])
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (simp(no_asm) add: liftE_bindE del: de_Morgan_conj split del: if_split)
apply (rule corres_split[OF get_cap_corres'])
apply (simp add: split_def)
apply (rule whenE_throwError_corres)
apply (simp add: lookup_failure_map_def)
apply auto[1]
apply (rule_tac r'="\<lambda>a b. fst b = rights_mask_map (fst a)
\<and> snd b = fst (snd a)
\<and> snd (snd a) = (gen_invocation_type (mi_label mi)
\<in> {CNodeMove, CNodeMutate})"
in corres_splitEE)
apply (rule corres_trivial)
subgoal by (auto split: list.split gen_invocation_labels.split,
auto simp: returnOk_def all_rights_def
rightsFromWord_correspondence)
apply (rule_tac r'=cap_relation in corres_splitEE)
apply (simp add: returnOk_def del: imp_disjL)
apply (rule conjI[rotated], rule impI)
apply (rule deriveCap_corres)
apply (clarsimp simp: cap_relation_mask
cap_map_update_data
split: option.split)
apply clarsimp
apply (clarsimp simp: cap_map_update_data
split: option.split)
apply (rule corres_trivial)
subgoal by (auto simp add: whenE_def, auto simp add: returnOk_def)
apply (wp | wpc | simp(no_asm))+
apply (wp hoare_vcg_const_imp_lift_R hoare_vcg_const_imp_lift
hoare_vcg_all_lift_R hoare_vcg_all_lift lsfco_cte_at' hoare_drop_imps
| clarsimp)+
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (rule corres_splitEE)
apply (rule ensureEmptySlot_corres; simp)
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (simp(no_asm) add: liftE_bindE del: de_Morgan_conj split del: if_split)
apply (rule corres_split[OF get_cap_corres'])
apply (simp add: split_def)
apply (rule whenE_throwError_corres)
apply (simp add: lookup_failure_map_def)
apply auto[1]
apply (rule_tac r'="\<lambda>a b. fst b = rights_mask_map (fst a)
\<and> snd b = fst (snd a)
\<and> snd (snd a) = (gen_invocation_type (mi_label mi)
\<in> {CNodeMove, CNodeMutate})"
in corres_splitEE)
apply (rule corres_trivial)
subgoal by (auto split: list.split gen_invocation_labels.split,
auto simp: returnOk_def all_rights_def
rightsFromWord_correspondence)
apply (rule_tac r'=cap_relation in corres_splitEE)
apply (simp add: returnOk_def del: imp_disjL)
apply (rule conjI[rotated], rule impI)
apply (rule deriveCap_corres)
apply (clarsimp simp: cap_relation_mask
cap_map_update_data
split: option.split)
apply clarsimp
apply (clarsimp simp: cap_map_update_data
split: option.split)
apply (rule corres_trivial)
subgoal by (auto simp add: whenE_def, auto simp add: returnOk_def)
apply (wp | wpc | simp(no_asm))+
apply (wp hoare_vcg_const_imp_lift_R hoare_vcg_const_imp_lift
hoare_vcg_all_lift_R hoare_vcg_all_lift lsfco_cte_at' hoare_drop_imps
| clarsimp)+
subgoal by (auto elim!: valid_cnode_capI)
apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def)
\<comment> \<open>Revoke\<close>
apply (simp add: decode_cnode_invocation_def decodeCNodeInvocation_def
isCap_simps Let_def unlessE_whenE del: ser_def split del: if_split)
apply (rule corres_guard_imp, rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (simp add: split_beta)
apply (rule corres_returnOkTT)
apply simp
apply simp
apply (rule corres_guard_imp, rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (simp add: split_beta)
apply (rule corres_returnOkTT)
apply simp
apply wp+
apply (auto elim!: valid_cnode_capI)[1]
@ -224,11 +226,10 @@ lemma decodeCNodeInvocation_corres:
apply (simp add: decode_cnode_invocation_def decodeCNodeInvocation_def
isCap_simps Let_def unlessE_whenE del: ser_def split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (simp add: split_beta)
apply (rule corres_returnOkTT)
apply simp
apply simp
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (simp add: split_beta)
apply (rule corres_returnOkTT)
apply simp
apply wp+
apply (auto elim!: valid_cnode_capI)[1]
@ -237,33 +238,31 @@ lemma decodeCNodeInvocation_corres:
apply (simp add: decode_cnode_invocation_def decodeCNodeInvocation_def
isCap_simps Let_def unlessE_whenE del: ser_def split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (simp add: split_beta)
apply (rule corres_split_norE)
apply (rule corres_returnOkTT)
apply simp
apply (rule ensureEmptySlot_corres)
apply simp
apply wp+
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (simp add: split_beta)
apply (rule corres_split_norE)
apply (rule ensureEmptySlot_corres)
apply simp
apply (rule corres_returnOkTT)
apply simp
apply simp
apply simp
apply (wp hoare_drop_imps)+
apply (wp hoare_drop_imps)+
apply (auto elim!: valid_cnode_capI)[1]
apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def)
\<comment> \<open>CancelBadgedSends\<close>
apply (simp add: decode_cnode_invocation_def decodeCNodeInvocation_def
isCap_simps Let_def unlessE_whenE del: ser_def split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (simp(no_asm) add: split_beta liftE_bindE)
apply (rule corres_split[OF get_cap_corres'])
apply (rule corres_split_norE)
apply (rule corres_trivial)
apply (clarsimp simp add: returnOk_def)
apply (simp add: cancelSendRightsEq)
apply (rule corres_trivial, auto simp add: whenE_def returnOk_def)[1]
apply (wp get_cap_wp getCTE_wp | simp only: whenE_def | clarsimp)+
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (simp(no_asm) add: split_beta liftE_bindE)
apply (rule corres_split[OF get_cap_corres'], simp)
apply (rule corres_split_norE)
apply (simp add: cancelSendRightsEq)
apply (rule corres_trivial, auto simp add: whenE_def returnOk_def)[1]
apply (rule corres_trivial)
apply (clarsimp simp add: returnOk_def)
apply (wp get_cap_wp getCTE_wp | simp only: whenE_def | clarsimp)+
apply (rule hoare_trivE_R[where P="\<top>"])
apply (simp add: cte_wp_at_ctes_of pred_conj_def cong: conj_cong)
apply (fastforce elim!: valid_cnode_capI simp: invs_def valid_state_def valid_pspace_def)
@ -274,64 +273,62 @@ lemma decodeCNodeInvocation_corres:
apply (simp add: le_diff_conv2 split_def decode_cnode_invocation_def decodeCNodeInvocation_def
isCap_simps Let_def unlessE_whenE whenE_whenE_body
del: disj_not1 ser_def split del: if_split)
apply (rule corres_guard_imp, rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rename_tac dest_slot destSlot)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])+
apply (rule_tac R = "\<lambda>s. cte_at pivot_slot s \<and> cte_at dest_slot s
\<and> cte_at src_slot s \<and> invs s" in
whenE_throwError_corres' [where R' = \<top>])
apply simp
apply (elim conjE)
apply rule
apply fastforce
apply (erule disjE)
apply (clarsimp simp add: split_def)
apply (drule (2) cte_map_inj_eq, clarsimp+)[1]
apply (clarsimp simp add: split_def)
apply (drule (2) cte_map_inj_eq, clarsimp+)[1]
apply (rule corres_split_norE)
apply (simp add: liftE_bindE del: de_Morgan_conj disj_not1 split del: if_split)
apply (rule corres_split_liftM2, simp only: split_beta, rule get_cap_corres)
apply (rule whenE_throwError_corres)
apply (simp add: lookup_failure_map_def)
apply (erule cap_relation_NullCapI)
apply (rule corres_split_liftM2, simp only: split_beta, rule get_cap_corres)
apply (rule whenE_throwError_corres)
apply (simp add: lookup_failure_map_def)
apply (erule cap_relation_NullCapI)
apply (rule whenE_throwError_corres)
apply simp
apply (simp add: cap_relation_NullCap)
apply (rule corres_returnOkTT)
apply simp
apply (intro conjI)
apply (erule cap_map_update_data)+
apply (wp hoare_drop_imps)+
apply (rule_tac F = "(src_slot \<noteq> dest_slot) = (srcSlot \<noteq> destSlot)"
and P = "\<lambda>s. cte_at src_slot s \<and> cte_at dest_slot s \<and> invs s" and P' = invs' in corres_req)
apply simp
apply rule
apply clarsimp
apply clarsimp
apply (drule (2) cte_map_inj_eq, clarsimp+)[1]
apply (rule corres_guard_imp)
apply (erule corres_whenE)
apply (rule ensureEmptySlot_corres)
apply clarsimp
apply simp
apply clarsimp
apply clarsimp
apply (wp hoare_whenE_wp)+
apply simp
apply (rule corres_guard_imp, rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (rename_tac dest_slot destSlot)
apply (rule corres_splitEE, (rule lookupSlotForCNodeOp_corres; simp))+
apply (rule_tac R = "\<lambda>s. cte_at pivot_slot s \<and> cte_at dest_slot s
\<and> cte_at src_slot s \<and> invs s" in
whenE_throwError_corres' [where R' = \<top>])
apply simp
apply (elim conjE)
apply rule
apply fastforce
apply (erule disjE)
apply (clarsimp simp add: split_def)
apply (drule (2) cte_map_inj_eq, clarsimp+)[1]
apply (clarsimp simp add: split_def)
apply (drule (2) cte_map_inj_eq, clarsimp+)[1]
apply (rule corres_split_norE)
apply (rule_tac F = "(src_slot \<noteq> dest_slot) = (srcSlot \<noteq> destSlot)"
and P = "\<lambda>s. cte_at src_slot s \<and> cte_at dest_slot s \<and> invs s" and P' = invs' in corres_req)
apply simp
apply (wp lsfco_cte_at' lookup_cap_valid lookup_cap_valid')
apply (simp add: if_apply_def2)
apply (wp hoare_drop_imps)
apply wp
apply simp
apply simp
apply (wp lsfco_cte_at' lookup_cap_valid lookup_cap_valid' hoare_drop_imps
| simp add: if_apply_def2 del: de_Morgan_conj split del: if_split)+
apply rule
apply clarsimp
apply clarsimp
apply (drule (2) cte_map_inj_eq, clarsimp+)[1]
apply (rule corres_guard_imp)
apply (erule corres_whenE)
apply (rule ensureEmptySlot_corres)
apply clarsimp
apply simp
apply clarsimp
apply clarsimp
apply (simp add: liftE_bindE del: de_Morgan_conj disj_not1 split del: if_split)
apply (rule corres_split_liftM2, simp only: split_beta, rule get_cap_corres)
apply (rule whenE_throwError_corres)
apply (simp add: lookup_failure_map_def)
apply (erule cap_relation_NullCapI)
apply (rule corres_split_liftM2, simp only: split_beta, rule get_cap_corres)
apply (rule whenE_throwError_corres)
apply (simp add: lookup_failure_map_def)
apply (erule cap_relation_NullCapI)
apply (rule whenE_throwError_corres)
apply simp
apply (simp add: cap_relation_NullCap)
apply (rule corres_returnOkTT)
apply simp
apply (intro conjI)
apply (erule cap_map_update_data)+
apply (wp hoare_drop_imps)+
apply simp
apply (wp lsfco_cte_at' lookup_cap_valid lookup_cap_valid')
apply (simp add: if_apply_def2)
apply (wp hoare_drop_imps)
apply wp
apply simp
apply (wp lsfco_cte_at' lookup_cap_valid lookup_cap_valid' hoare_drop_imps
| simp add: if_apply_def2 del: de_Morgan_conj split del: if_split)+
apply (auto elim!: valid_cnode_capI)[1]
apply (clarsimp dest!: list_all2_lengthD simp: invs'_def valid_state'_def valid_pspace'_def)
\<comment> \<open>Errors\<close>
@ -350,9 +347,9 @@ lemma decodeCNodeInvocation_corres:
cnode_invok_case_cleanup
split del: if_split cong: if_cong)
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rule corres_trivial, clarsimp split: list.split_asm)
apply simp+
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (rule corres_trivial, clarsimp split: list.split_asm)
apply wp+
apply (auto elim!: valid_cnode_capI)[1]
apply fastforce
@ -360,11 +357,11 @@ lemma decodeCNodeInvocation_corres:
isCNodeCap_CNodeCap split_def unlessE_whenE
split del: if_split cong: if_cong)
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres _ wp_post_tautE wp_post_tautE])
apply (clarsimp simp: list_all2_Cons1 list_all2_Nil
split: list.split_asm split del: if_split)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres _ wp_post_tautE wp_post_tautE])
apply simp
apply simp
apply simp
apply (clarsimp simp: list_all2_Cons1 list_all2_Nil
split: list.split_asm split del: if_split)
apply (auto elim!: valid_cnode_capI)[1]
apply fastforce
done
@ -6714,9 +6711,9 @@ proof -
show ?thesis
unfolding spec_corres_def
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated)
apply (erule w)
apply (rule x[unfolded spec_corres_def])
apply (rule corres_split)
apply (rule x[unfolded spec_corres_def])
apply (erule w)
apply (wp z)
apply (rule univ_wp)
apply (rule z)
@ -8623,8 +8620,8 @@ lemma invokeCNode_corres:
apply simp
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated [OF cteMove_corres])
apply assumption
apply (rule corres_split)
apply (erule cteMove_corres)
apply (erule cteMove_corres)
apply wp
apply (simp add: cte_wp_at_caps_of_state)
@ -8652,27 +8649,28 @@ lemma invokeCNode_corres:
apply (simp add: getThreadCallerSlot_def locateSlot_conv objBits_simps)
apply (rule corres_guard_imp)
apply (rule corres_split[OF getCurThread_corres])
apply (subgoal_tac "thread + 2^cte_level_bits * tcbCallerSlot = cte_map (thread, tcb_cnode_index 3)")
prefer 2
apply (simp add: cte_map_def tcb_cnode_index_def tcbCallerSlot_def cte_level_bits_def objBits_defs)
apply (rule corres_split[OF getSlotCap_corres])
apply (rule_tac P="\<lambda>s. (is_reply_cap cap \<or> cap = cap.NullCap) \<and>
(is_reply_cap cap \<longrightarrow>
(einvs and cte_at (threada, tcb_cnode_index 3) and
cte_wp_at (\<lambda>c. c = cap.NullCap) prod and
real_cte_at prod and valid_cap cap and
K ((threada, tcb_cnode_index 3) \<noteq> prod)) s)" and
P'="\<lambda>s. (isReplyCap rv' \<and> \<not> capReplyMaster rv') \<longrightarrow> (invs' and
cte_wp_at'
(\<lambda>c. weak_derived' rv' (cteCap c) \<and>
cteCap c \<noteq> capability.NullCap)
(cte_map (threada, tcb_cnode_index 3)) and
cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map prod)) s" in corres_inst)
apply (case_tac cap, simp_all add: isCap_simps is_cap_simps split: bool.split)[1]
apply clarsimp
apply (rule corres_guard_imp)
apply (rule cteMove_corres)
apply (simp add: real_cte_tcb_valid)+
apply (subgoal_tac "thread + 2^cte_level_bits * tcbCallerSlot = cte_map (thread, tcb_cnode_index 3)")
prefer 2
apply (simp add: cte_map_def tcb_cnode_index_def tcbCallerSlot_def cte_level_bits_def objBits_defs)
apply (rule corres_split[OF getSlotCap_corres])
apply simp
apply (rule_tac P="\<lambda>s. (is_reply_cap cap \<or> cap = cap.NullCap) \<and>
(is_reply_cap cap \<longrightarrow>
(einvs and cte_at (threada, tcb_cnode_index 3) and
cte_wp_at (\<lambda>c. c = cap.NullCap) prod and
real_cte_at prod and valid_cap cap and
K ((threada, tcb_cnode_index 3) \<noteq> prod)) s)" and
P'="\<lambda>s. (isReplyCap rv' \<and> \<not> capReplyMaster rv') \<longrightarrow> (invs' and
cte_wp_at'
(\<lambda>c. weak_derived' rv' (cteCap c) \<and>
cteCap c \<noteq> capability.NullCap)
(cte_map (threada, tcb_cnode_index 3)) and
cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map prod)) s" in corres_inst)
apply (case_tac cap, simp_all add: isCap_simps is_cap_simps split: bool.split)[1]
apply clarsimp
apply (rule corres_guard_imp)
apply (rule cteMove_corres)
apply (simp add: real_cte_tcb_valid)+
apply (wp get_cap_wp)
apply (simp add: getSlotCap_def)
apply (wp getCTE_wp)+

View File

@ -3759,7 +3759,7 @@ lemma getCTE_get:
done
lemma setUntypedCapAsFull_corres:
"\<lbrakk>cap_relation c c'; src' = cte_map src; dest' = cte_map dest;
"\<lbrakk>cap_relation c c'; src' = cte_map src;
cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap;
cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer \<and>
mdbNext (cteMDBNode rv') = nullPointer\<rbrakk>
@ -5036,175 +5036,128 @@ lemma cteInsert_corres:
R'="\<lambda>r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) and
cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE)))
(cte_map src)"
in corres_split_deprecated[where r'=dc])
apply (rule corres_stronger_no_failI)
apply (rule no_fail_pre)
apply (wp hoare_weak_lift_imp)
apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def)
apply (erule_tac valid_dlistEn[where p = "cte_map src"])
apply (simp+)[3]
apply (clarsimp simp: corres_underlying_def state_relation_def
in_monad valid_mdb'_def valid_mdb_ctes_def)
apply (drule (1) pspace_relationsD)
apply (drule (18) set_cap_not_quite_corres)
apply (rule refl)
apply (elim conjE exE)
apply (rule bind_execI, assumption)
apply (subgoal_tac "mdb_insert_abs (cdt a) src dest")
prefer 2
apply (erule mdb_insert_abs.intro)
in corres_split[where r'=dc])
apply (rule setUntypedCapAsFull_corres; simp)
apply (rule corres_stronger_no_failI)
apply (rule no_fail_pre)
apply (wp hoare_weak_lift_imp)
apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def)
apply (erule_tac valid_dlistEn[where p = "cte_map src"])
apply (simp+)[3]
apply (clarsimp simp: corres_underlying_def state_relation_def
in_monad valid_mdb'_def valid_mdb_ctes_def)
apply (drule (1) pspace_relationsD)
apply (drule (18) set_cap_not_quite_corres)
apply (rule refl)
apply (elim conjE exE)
apply (rule bind_execI, assumption)
apply (subgoal_tac "mdb_insert_abs (cdt a) src dest")
prefer 2
apply (erule mdb_insert_abs.intro)
apply (rule mdb_Null_None)
apply (simp add: op_equal)
apply (simp add: op_equal)
apply simp
apply (rule mdb_Null_descendants)
apply (rule mdb_Null_descendants)
apply (simp add: op_equal)
apply simp
apply (subgoal_tac "no_mloop (cdt a)")
prefer 2
apply (simp add: valid_mdb_def)
apply (clarsimp simp: exec_gets update_cdt_def bind_assoc
set_cdt_def
exec_get exec_put set_original_def modify_def simp del: fun_upd_apply
| (rule bind_execI[where f="cap_insert_ext x y z i p" for x y z i p], clarsimp simp: exec_gets exec_get put_def mdb_insert_abs.cap_insert_ext_det_def2 update_cdt_list_def set_cdt_list_def, rule refl))+
apply (clarsimp simp: put_def state_relation_def)
apply (drule updateCap_stuff)
apply clarsimp
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def
prev_update_modify_mdb_relation)
apply (subgoal_tac "cte_map dest \<noteq> 0")
prefer 2
apply (clarsimp simp: valid_mdb'_def
valid_mdb_ctes_def no_0_def)
apply (subgoal_tac "cte_map src \<noteq> 0")
prefer 2
apply (clarsimp simp: valid_mdb'_def
valid_mdb_ctes_def no_0_def)
apply (thin_tac "ksMachineState t = p" for p t)+
apply (thin_tac "ksCurThread t = p" for p t)+
apply (thin_tac "ksIdleThread t = p" for p t)+
apply (thin_tac "ksReadyQueues t = p" for p t)+
apply (thin_tac "ksSchedulerAction t = p" for p t)+
apply (clarsimp simp: pspace_relations_def)
apply simp
apply (subgoal_tac "no_mloop (cdt a)")
prefer 2
apply (simp add: valid_mdb_def)
apply (clarsimp simp: exec_gets update_cdt_def bind_assoc set_cdt_def
exec_get exec_put set_original_def modify_def
simp del: fun_upd_apply
| (rule bind_execI[where f="cap_insert_ext x y z i p" for x y z i p], clarsimp simp: exec_gets exec_get put_def mdb_insert_abs.cap_insert_ext_det_def2 update_cdt_list_def set_cdt_list_def, rule refl))+
apply (clarsimp simp: put_def state_relation_def)
apply (drule updateCap_stuff)
apply clarsimp
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def
prev_update_modify_mdb_relation)
apply (subgoal_tac "cte_map dest \<noteq> 0")
prefer 2
apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
apply (subgoal_tac "cte_map src \<noteq> 0")
prefer 2
apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
apply (thin_tac "ksMachineState t = p" for p t)+
apply (thin_tac "ksCurThread t = p" for p t)+
apply (thin_tac "ksIdleThread t = p" for p t)+
apply (thin_tac "ksReadyQueues t = p" for p t)+
apply (thin_tac "ksSchedulerAction t = p" for p t)+
apply (clarsimp simp: pspace_relations_def)
apply (rule conjI)
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
apply (rule conjI)
defer
apply(rule conjI)
apply (thin_tac "ctes_of s = t" for s t)+
apply (thin_tac "pspace_relation s t" for s t)+
apply (thin_tac "machine_state t = s" for s t)+
apply (case_tac "srcCTE")
apply (rename_tac src_cap' src_node)
apply (case_tac "rv'")
apply (rename_tac dest_node)
apply (clarsimp simp: in_set_cap_cte_at_swp)
apply (subgoal_tac "cte_at src a \<and> is_derived (cdt a) src c src_cap")
prefer 2
apply (fastforce simp: cte_wp_at_def)
apply (erule conjE)
apply (subgoal_tac "mdb_insert (ctes_of b) (cte_map src) (maskedAsFull src_cap' c') src_node
(cte_map dest) NullCap dest_node")
prefer 2
apply (rule mdb_insert.intro)
apply (rule mdb_ptr.intro)
apply (rule vmdb.intro, simp add: valid_mdb_ctes_def)
apply (erule mdb_ptr_axioms.intro)
apply (rule conjI)
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
apply (rule conjI)
defer
apply(rule conjI)
apply (thin_tac "ctes_of s = t" for s t)+
apply (thin_tac "pspace_relation s t" for s t)+
apply (thin_tac "machine_state t = s" for s t)+
apply (case_tac "srcCTE")
apply (rename_tac src_cap' src_node)
apply (case_tac "rv'")
apply (rename_tac dest_node)
apply (clarsimp simp: in_set_cap_cte_at_swp)
apply (subgoal_tac "cte_at src a \<and> is_derived (cdt a) src c src_cap")
prefer 2
apply (fastforce simp: cte_wp_at_def)
apply (erule conjE)
apply (subgoal_tac "mdb_insert (ctes_of b) (cte_map src) (maskedAsFull src_cap' c') src_node
(cte_map dest) NullCap dest_node")
prefer 2
apply (rule mdb_insert.intro)
apply (rule mdb_ptr.intro)
apply (rule vmdb.intro, simp add: valid_mdb_ctes_def)
apply (erule mdb_ptr_axioms.intro)
apply (rule mdb_insert_axioms.intro)
apply (rule refl)
apply assumption
apply (rule mdb_ptr.intro)
apply (rule vmdb.intro, simp add: valid_mdb_ctes_def)
apply (erule mdb_ptr_axioms.intro)
apply (rule mdb_insert_axioms.intro)
apply (rule refl)
apply assumption
apply assumption
apply assumption
apply (erule (5) cte_map_inj)
apply (frule mdb_insert_der.intro)
apply (rule mdb_insert_der_axioms.intro)
apply (simp add: is_derived_eq)
apply (simp (no_asm_simp) add: cdt_relation_def split: if_split)
apply (subgoal_tac "descendants_of dest (cdt a) = {}")
prefer 2
apply (drule mdb_insert.dest_no_descendants)
apply (fastforce simp add: cdt_relation_def)
apply (subgoal_tac "mdb_insert_abs (cdt a) src dest")
prefer 2
apply (erule mdb_insert_abs.intro)
apply (rule mdb_None)
apply (erule(1) mdb_insert.descendants_not_dest)
apply assumption
apply assumption
apply (erule (5) cte_map_inj)
apply (frule mdb_insert_der.intro)
apply (rule mdb_insert_der_axioms.intro)
apply (simp add: is_derived_eq)
apply (simp (no_asm_simp) add: cdt_relation_def split: if_split)
apply (subgoal_tac "descendants_of dest (cdt a) = {}")
prefer 2
apply (drule mdb_insert.dest_no_descendants)
apply (fastforce simp add: cdt_relation_def)
apply (subgoal_tac "mdb_insert_abs (cdt a) src dest")
prefer 2
apply (erule mdb_insert_abs.intro)
apply (rule mdb_None)
apply (erule(1) mdb_insert.descendants_not_dest)
apply assumption
apply assumption
apply(simp add: cdt_list_relation_def)
apply(subgoal_tac "no_mloop (cdt a) \<and> finite_depth (cdt a)")
apply assumption
apply(simp add: cdt_list_relation_def)
apply(subgoal_tac "no_mloop (cdt a) \<and> finite_depth (cdt a)")
prefer 2
apply(simp add: finite_depth valid_mdb_def)
apply(intro conjI impI allI)
apply(simp cong: option.case_cong)
apply(simp split: option.split)
apply(subgoal_tac "\<forall>aa. cdt a src = Some aa \<longrightarrow> src \<noteq> aa")
prefer 2
apply(simp add: finite_depth valid_mdb_def)
apply(intro conjI impI allI)
apply(simp cong: option.case_cong)
apply(simp split: option.split)
apply(subgoal_tac "\<forall>aa. cdt a src = Some aa \<longrightarrow> src \<noteq> aa")
prefer 2
apply(fastforce simp: no_mloop_weaken)
apply(simp add: fun_upd_twist)
apply(rule allI)
apply(case_tac "next_child src (cdt_list (a))")
apply(frule next_child_NoneD)
apply(subst mdb_insert_abs.next_slot)
apply(simp_all)[5]
apply(case_tac "ca=src")
apply(simp)
apply(clarsimp simp: modify_map_def)
apply(fastforce split: if_split_asm)
apply(case_tac "ca = dest")
apply(simp)
apply(rule impI)
apply(clarsimp simp: modify_map_def const_def)
apply(simp split: if_split_asm)
apply(drule_tac p="cte_map src" in valid_mdbD1')
subgoal by(simp)
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
subgoal by(clarsimp)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(erule_tac x=src in allE)+
subgoal by(fastforce)
apply(simp)
apply(rule impI)
apply(subgoal_tac "cte_at ca a")
prefer 2
apply(rule cte_at_next_slot)
apply(simp_all)[4]
apply(clarsimp simp: modify_map_def const_def)
apply(simp split: if_split_asm)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule_tac p="cte_map src" in valid_mdbD1')
subgoal by(simp)
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
subgoal by(clarsimp)
apply(clarsimp)
apply(case_tac z)
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply(frule(1) next_childD)
apply(simp add: mdb_insert_abs.next_slot)
apply(fastforce simp: no_mloop_weaken)
apply(simp add: fun_upd_twist)
apply(rule allI)
apply(case_tac "next_child src (cdt_list (a))")
apply(frule next_child_NoneD)
apply(subst mdb_insert_abs.next_slot)
apply(simp_all)[5]
apply(case_tac "ca=src")
apply(simp)
apply(clarsimp simp: modify_map_def)
subgoal by(fastforce split: if_split_asm)
apply(fastforce split: if_split_asm)
apply(case_tac "ca = dest")
apply(simp)
apply(rule impI)
@ -5212,10 +5165,10 @@ lemma cteInsert_corres:
apply(simp split: if_split_asm)
apply(drule_tac p="cte_map src" in valid_mdbD1')
subgoal by(simp)
apply(simp add: valid_mdb'_def valid_mdb_ctes_def)
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
subgoal by(clarsimp)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(simp_all)[2]
apply(erule_tac x=src in allE)+
subgoal by(fastforce)
apply(simp)
@ -5227,7 +5180,7 @@ lemma cteInsert_corres:
apply(clarsimp simp: modify_map_def const_def)
apply(simp split: if_split_asm)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(simp_all)[2]
apply(drule_tac p="cte_map src" in valid_mdbD1')
subgoal by(simp)
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
@ -5237,112 +5190,22 @@ lemma cteInsert_corres:
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(simp_all)[2]
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply(subgoal_tac "mdb_insert_sib (ctes_of b) (cte_map src) (maskedAsFull src_cap' c')
src_node (cte_map dest) capability.NullCap dest_node c'")
prefer 2
apply(simp add: mdb_insert_sib_def)
apply(rule mdb_insert_sib_axioms.intro)
apply (subst can_be_is [symmetric])
apply simp
apply (rule cap_relation_masked_as_full)
apply (simp+)[3]
apply simp
apply simp
apply simp
apply (subst (asm) revokable_eq, assumption, assumption)
apply (rule derived_sameRegionAs)
apply (subst is_derived_eq[symmetric], assumption,
assumption, assumption, assumption, assumption)
apply assumption
subgoal by (clarsimp simp: cte_wp_at_def is_derived_def is_cap_simps cap_master_cap_simps
dest!:cap_master_cap_eqDs)
apply (subgoal_tac "is_original_cap a src = mdbRevocable src_node")
apply (frule(4) iffD1[OF is_derived_eq])
apply (drule_tac src_cap' = src_cap' in
maskedAsFull_revokable[where a = c',symmetric])
subgoal by(simp)
apply (simp add: revokable_relation_def)
apply (erule_tac x=src in allE)+
apply simp
apply (erule impE)
apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state split: if_splits)
subgoal by (clarsimp simp: masked_as_full_def is_cap_simps free_index_update_def split: if_splits)
apply(simp)
apply(subgoal_tac "cdt_list (a) src = []")
prefer 2
apply(rule ccontr)
apply(simp add: empty_list_empty_desc)
apply(simp add: no_children_empty_desc[symmetric])
apply(erule exE)
apply(drule_tac p="cte_map caa" in mdb_insert_sib.src_no_parent)
apply(subgoal_tac "cte_map caa\<in>descendants_of' (cte_map src) (ctes_of b)")
subgoal by(simp add: descendants_of'_def)
apply(simp add: cdt_relation_def)
apply(erule_tac x=src in allE)
apply(drule child_descendant)+
apply(drule_tac x=caa and f=cte_map in imageI)
subgoal by(simp)
apply(case_tac "cdt a src")
apply(simp)
apply(subst mdb_insert_abs_sib.next_slot_no_parent')
apply(simp add: mdb_insert_abs_sib_def)
apply(simp_all add: fun_upd_idem)[5]
apply(case_tac "ca=src")
subgoal by(simp add: next_slot_def no_parent_next_not_child_None)
apply(case_tac "ca = dest")
subgoal by(simp add: next_slot_def no_parent_next_not_child_None
mdb_insert_abs.dest empty_list_empty_desc)
apply(case_tac "next_slot ca (cdt_list (a)) (cdt a)")
subgoal by(simp)
apply(simp)
apply(subgoal_tac "cte_at ca a")
prefer 2
apply(rule cte_at_next_slot)
apply(simp_all)[4]
apply(clarsimp simp: modify_map_def const_def)
apply(simp split: if_split_asm)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule_tac p="cte_map src" in valid_mdbD1')
apply(simp)
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
subgoal by(clarsimp)
apply(clarsimp)
apply(case_tac z)
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply(simp add: fun_upd_idem)
apply(subst mdb_insert_abs_sib.next_slot')
subgoal by(simp add: mdb_insert_abs_sib_def)
apply(simp_all)[5]
apply(frule(1) next_childD)
apply(simp add: mdb_insert_abs.next_slot)
apply(case_tac "ca=src")
apply(simp)
apply(clarsimp simp: modify_map_def)
subgoal by(fastforce split: if_split_asm)
apply(case_tac "ca = dest")
apply(simp)
apply(case_tac "next_slot src (cdt_list (a)) (cdt a)")
subgoal by(simp)
apply(simp)
apply(rule impI)
apply(clarsimp simp: modify_map_def const_def)
apply(simp split: if_split_asm)
apply(drule_tac p="cte_map src" in valid_mdbD1')
@ -5350,10 +5213,93 @@ lemma cteInsert_corres:
apply(simp add: valid_mdb'_def valid_mdb_ctes_def)
subgoal by(clarsimp)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(simp_all)[2]
apply(erule_tac x=src in allE)+
subgoal by(fastforce)
apply(simp)
apply(rule impI)
apply(subgoal_tac "cte_at ca a")
prefer 2
apply(rule cte_at_next_slot)
apply(simp_all)[4]
apply(clarsimp simp: modify_map_def const_def)
apply(simp split: if_split_asm)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule_tac p="cte_map src" in valid_mdbD1')
subgoal by(simp)
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
subgoal by(clarsimp)
apply(clarsimp)
apply(case_tac z)
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply(subgoal_tac "mdb_insert_sib (ctes_of b) (cte_map src) (maskedAsFull src_cap' c')
src_node (cte_map dest) capability.NullCap dest_node c'")
prefer 2
apply(simp add: mdb_insert_sib_def)
apply(rule mdb_insert_sib_axioms.intro)
apply (subst can_be_is [symmetric])
apply simp
apply (rule cap_relation_masked_as_full)
apply (simp+)[3]
apply simp
apply simp
apply simp
apply (subst (asm) revokable_eq, assumption, assumption)
apply (rule derived_sameRegionAs)
apply (subst is_derived_eq[symmetric]; assumption)
apply assumption
subgoal by (clarsimp simp: cte_wp_at_def is_derived_def is_cap_simps cap_master_cap_simps
dest!:cap_master_cap_eqDs)
apply (subgoal_tac "is_original_cap a src = mdbRevocable src_node")
apply (frule(4) iffD1[OF is_derived_eq])
apply (drule_tac src_cap' = src_cap' in
maskedAsFull_revokable[where a = c',symmetric])
subgoal by(simp)
apply (simp add: revokable_relation_def)
apply (erule_tac x=src in allE)+
apply simp
apply (erule impE)
apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state split: if_splits)
subgoal by (clarsimp simp: masked_as_full_def is_cap_simps free_index_update_def split: if_splits)
apply(simp)
apply(subgoal_tac "cdt_list (a) src = []")
prefer 2
apply(rule ccontr)
apply(simp add: empty_list_empty_desc)
apply(simp add: no_children_empty_desc[symmetric])
apply(erule exE)
apply(drule_tac p="cte_map caa" in mdb_insert_sib.src_no_parent)
apply(subgoal_tac "cte_map caa\<in>descendants_of' (cte_map src) (ctes_of b)")
subgoal by(simp add: descendants_of'_def)
apply(simp add: cdt_relation_def)
apply(erule_tac x=src in allE)
apply(drule child_descendant)+
apply(drule_tac x=caa and f=cte_map in imageI)
subgoal by(simp)
apply(case_tac "cdt a src")
apply(simp)
apply(subst mdb_insert_abs_sib.next_slot_no_parent')
apply(simp add: mdb_insert_abs_sib_def)
apply(simp_all add: fun_upd_idem)[5]
apply(case_tac "ca=src")
subgoal by(simp add: next_slot_def no_parent_next_not_child_None)
apply(case_tac "ca = dest")
subgoal by(simp add: next_slot_def no_parent_next_not_child_None
mdb_insert_abs.dest empty_list_empty_desc)
apply(case_tac "next_slot ca (cdt_list (a)) (cdt a)")
subgoal by(simp)
apply(simp)
@ -5364,9 +5310,9 @@ lemma cteInsert_corres:
apply(clarsimp simp: modify_map_def const_def)
apply(simp split: if_split_asm)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(simp_all)[2]
apply(drule_tac p="cte_map src" in valid_mdbD1')
subgoal by(simp)
apply(simp)
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
subgoal by(clarsimp)
apply(clarsimp)
@ -5374,60 +5320,107 @@ lemma cteInsert_corres:
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(simp_all)[2]
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply (thin_tac "ctes_of t = t'" for t t')+
apply (clarsimp simp: modify_map_apply)
apply (clarsimp simp: revokable_relation_def split: if_split)
apply (rule conjI)
apply(simp add: fun_upd_idem)
apply(subst mdb_insert_abs_sib.next_slot')
subgoal by(simp add: mdb_insert_abs_sib_def)
apply(simp_all)[5]
apply(case_tac "ca=src")
apply(clarsimp simp: modify_map_def)
subgoal by(fastforce split: if_split_asm)
apply(case_tac "ca = dest")
apply(simp)
apply(case_tac "next_slot src (cdt_list (a)) (cdt a)")
subgoal by(simp)
apply(simp)
apply(clarsimp simp: modify_map_def const_def)
apply(simp split: if_split_asm)
apply(drule_tac p="cte_map src" in valid_mdbD1')
subgoal by(simp)
apply(simp add: valid_mdb'_def valid_mdb_ctes_def)
subgoal by(clarsimp)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(erule_tac x=src in allE)+
subgoal by(fastforce)
apply(simp)
apply(case_tac "next_slot ca (cdt_list (a)) (cdt a)")
subgoal by(simp)
apply(simp)
apply(subgoal_tac "cte_at ca a")
prefer 2
apply(rule cte_at_next_slot)
apply(simp_all)[4]
apply(clarsimp simp: modify_map_def const_def)
apply(simp split: if_split_asm)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule_tac p="cte_map src" in valid_mdbD1')
subgoal by(simp)
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
subgoal by(clarsimp)
apply(clarsimp)
apply(case_tac z)
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(erule_tac x="(aa, bb)" in allE)+
subgoal by(fastforce)
apply (thin_tac "ctes_of t = t'" for t t')+
apply (clarsimp simp: modify_map_apply)
apply (clarsimp simp: revokable_relation_def split: if_split)
apply (rule conjI)
apply clarsimp
apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'")
prefer 2
apply (case_tac rv')
subgoal by (clarsimp simp add: const_def modify_map_def split: if_split_asm)
apply simp
apply (rule revokable_eq, assumption, assumption)
apply (rule derived_sameRegionAs)
apply (drule(3) is_derived_eq[THEN iffD1,rotated -1])
subgoal by (simp add: cte_wp_at_def)
apply assumption
apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'")
prefer 2
apply (case_tac rv')
subgoal by (clarsimp simp add: const_def modify_map_def split: if_split_asm)
apply simp
apply (rule revokable_eq, assumption, assumption)
apply (rule derived_sameRegionAs)
apply (drule(3) is_derived_eq[THEN iffD1,rotated -1])
subgoal by (simp add: cte_wp_at_def)
apply assumption
subgoal by (clarsimp simp: cap_master_cap_simps cte_wp_at_def is_derived_def is_cap_simps
split:if_splits dest!:cap_master_cap_eqDs)
apply clarsimp
apply (case_tac srcCTE)
apply (case_tac rv')
apply clarsimp
apply (subgoal_tac "\<exists>cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')")
prefer 2
apply (clarsimp simp: modify_map_def split: if_split_asm)
apply (case_tac z)
subgoal by clarsimp
apply clarsimp
apply (drule set_cap_caps_of_state_monad)+
apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None")
prefer 2
subgoal by (clarsimp simp: cte_wp_at_caps_of_state null_filter_def split: if_splits)
apply assumption
subgoal by (clarsimp simp: cap_master_cap_simps cte_wp_at_def is_derived_def is_cap_simps
split:if_splits dest!:cap_master_cap_eqDs)
apply clarsimp
apply (case_tac srcCTE)
apply (case_tac rv')
apply clarsimp
apply (subgoal_tac "\<exists>cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')")
prefer 2
apply (clarsimp simp: modify_map_def split: if_split_asm)
apply (case_tac z)
subgoal by clarsimp
apply clarsimp
apply (drule set_cap_caps_of_state_monad)+
apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None")
prefer 2
subgoal by (clarsimp simp: cte_wp_at_caps_of_state null_filter_def split: if_splits)
apply clarsimp
apply (subgoal_tac "cte_at (aa,bb) a")
prefer 2
apply (drule null_filter_caps_of_stateD)
apply (erule cte_wp_at_weakenE, rule TrueI)
apply (subgoal_tac "mdbRevocable node = mdbRevocable node'")
subgoal by clarsimp
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map dest")
subgoal by (clarsimp simp: modify_map_def split: if_split_asm)
apply (erule (5) cte_map_inj)
(* FIXME *)
apply (rule setUntypedCapAsFull_corres)
apply simp+
apply clarsimp
apply (subgoal_tac "cte_at (aa,bb) a")
prefer 2
apply (drule null_filter_caps_of_stateD)
apply (erule cte_wp_at_weakenE, rule TrueI)
apply (subgoal_tac "mdbRevocable node = mdbRevocable node'")
subgoal by clarsimp
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map dest")
subgoal by (clarsimp simp: modify_map_def split: if_split_asm)
apply (erule (5) cte_map_inj)
apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb
set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap
setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+
@ -5490,12 +5483,12 @@ lemma cteInsert_corres:
apply simp
apply (subst mdb_insert_child.descendants)
apply (rule mdb_insert_child.intro)
apply simp
apply simp
apply (rule mdb_insert_child_axioms.intro)
apply (subst can_be_is [symmetric])
apply simp
apply (rule cap_relation_masked_as_full)
apply (simp+)[3]
apply (rule cap_relation_masked_as_full)
apply (simp+)[3]
apply simp
apply simp
apply (subst (asm) revokable_eq, assumption, assumption)

View File

@ -3441,11 +3441,11 @@ lemma lookupSlotForCNodeOp_corres:
word_bits_def toInteger_nat fromIntegral_def fromInteger_nat)
apply (rule corres_lookup_error)
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF rab_corres'])
apply (rule corres_trivial)
apply (clarsimp simp: returnOk_def lookup_failure_map_def
split: list.split)
apply simp+
apply (rule corres_splitEE)
apply (rule rab_corres'; simp)
apply (rule corres_trivial)
apply (clarsimp simp: returnOk_def lookup_failure_map_def
split: list.split)
apply wp+
apply clarsimp
apply clarsimp
@ -4738,135 +4738,133 @@ lemma cteInsert_simple_corres:
R'="\<lambda>r. ?P' and cte_wp_at' ((=) rv') (cte_map dest)
and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src)
and (\<lambda>s. safe_parent_for' (ctes_of s) src' c')"
in corres_split_deprecated[where r'=dc])
apply (rule corres_stronger_no_failI)
apply (rule no_fail_pre, wp hoare_weak_lift_imp)
apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def)
apply (erule_tac valid_dlistEn[where p = "cte_map src"])
apply (simp+)[3]
apply (clarsimp simp: corres_underlying_def state_relation_def
in_monad valid_mdb'_def valid_mdb_ctes_def)
apply (drule (1) pspace_relationsD)
apply (drule (18) set_cap_not_quite_corres)
apply (rule refl)
apply (elim conjE exE)
apply (rule bind_execI, assumption)
apply (subgoal_tac "mdb_insert_abs (cdt a) src dest")
in corres_split[where r'=dc])
apply (rule setUntypedCapAsFull_corres; simp)
apply (rule corres_stronger_no_failI)
apply (rule no_fail_pre, wp hoare_weak_lift_imp)
apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def)
apply (erule_tac valid_dlistEn[where p = "cte_map src"])
apply (simp+)[3]
apply (clarsimp simp: corres_underlying_def state_relation_def
in_monad valid_mdb'_def valid_mdb_ctes_def)
apply (drule (1) pspace_relationsD)
apply (drule (18) set_cap_not_quite_corres)
apply (rule refl)
apply (elim conjE exE)
apply (rule bind_execI, assumption)
apply (subgoal_tac "mdb_insert_abs (cdt a) src dest")
prefer 2
apply (clarsimp simp: cte_wp_at_caps_of_state valid_mdb_def2)
apply (rule mdb_insert_abs.intro)
apply clarsimp
apply (erule (1) mdb_cte_at_Null_None)
apply (erule (1) mdb_cte_at_Null_descendants)
apply (subgoal_tac "no_mloop (cdt a)")
prefer 2
apply (simp add: valid_mdb_def)
apply (clarsimp simp: exec_gets update_cdt_def bind_assoc set_cdt_def
exec_get exec_put set_original_def modify_def
simp del: fun_upd_apply
| (rule bind_execI[where f="cap_insert_ext x y z x' y'" for x y z x' y'], clarsimp simp: mdb_insert_abs.cap_insert_ext_det_def2 update_cdt_list_def set_cdt_list_def put_def simp del: fun_upd_apply) | rule refl)+
apply (clarsimp simp: put_def state_relation_def simp del: fun_upd_apply)
apply (drule updateCap_stuff)
apply clarsimp
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
apply (clarsimp simp: pspace_relations_def)
apply (thin_tac "gsCNodes t = p" for t p)+
apply (thin_tac "ksMachineState t = p" for t p)+
apply (thin_tac "ksCurThread t = p" for t p)+
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
apply (thin_tac "ksIdleThread t = p" for t p)+
apply (thin_tac "ksReadyQueues t = p" for t p)+
apply (thin_tac "ksSchedulerAction t = p" for t p)+
apply (thin_tac "cur_thread t = p" for t p)+
apply (thin_tac "domain_index t = p" for t p)+
apply (thin_tac "domain_time t = p" for t p)+
apply (thin_tac "cur_domain t = p" for t p)+
apply (thin_tac "scheduler_action t = p" for t p)+
apply (thin_tac "ready_queues t = p" for t p)+
apply (thin_tac "idle_thread t = p" for t p)+
apply (thin_tac "machine_state t = p" for t p)+
apply (thin_tac "work_units_completed t = p" for t p)+
apply (thin_tac "ksArchState t = p" for t p)+
apply (thin_tac "gsUserPages t = p" for t p)+
apply (thin_tac "ksCurDomain t = p" for t p)+
apply (thin_tac "ksInterruptState t = p" for t p)+
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
apply (thin_tac "ksDomainTime t = p" for t p)+
apply (thin_tac "ksDomSchedule t = p" for t p)+
apply (thin_tac "ctes_of t = p" for t p)+
apply (thin_tac "ekheap_relation t p" for t p)+
apply (thin_tac "pspace_relation t p" for t p)+
apply (thin_tac "interrupt_state_relation s t p" for s t p)+
apply (thin_tac "sched_act_relation t p" for t p)+
apply (thin_tac "ready_queues_relation t p" for t p)+
apply (rule conjI)
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation)
apply (subgoal_tac "cte_map dest \<noteq> 0")
prefer 2
apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
apply (subgoal_tac "cte_map src \<noteq> 0")
prefer 2
apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
apply (subgoal_tac "should_be_parent_of src_cap (is_original_cap a src) c (revokable src_cap c) = True")
prefer 2
apply (subst should_be_parent_of_masked_as_full[symmetric])
apply (subst safe_parent_is_parent)
apply ((simp add: cte_wp_at_caps_of_state)+)[4]
apply (subst conj_assoc[symmetric])
apply (rule conjI)
defer
apply (clarsimp simp: modify_map_apply)
apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply)
apply (simp split: if_split)
apply (rule conjI)
apply clarsimp
apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'")
prefer 2
apply (case_tac rv')
apply (clarsimp simp add: const_def modify_map_def split: if_split_asm)
apply clarsimp
apply (rule revokable_eq, assumption, assumption)
apply (subst same_region_as_relation [symmetric])
prefer 3
apply (rule safe_parent_same_region)
apply (simp add: cte_wp_at_caps_of_state)
apply assumption
apply assumption
apply (clarsimp simp: cte_wp_at_def is_simple_cap_def)
apply clarsimp
apply (case_tac srcCTE)
apply (case_tac rv')
apply clarsimp
apply (subgoal_tac "\<exists>cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')")
prefer 2
apply (clarsimp simp: cte_wp_at_caps_of_state valid_mdb_def2)
apply (rule mdb_insert_abs.intro)
apply clarsimp
apply (erule (1) mdb_cte_at_Null_None)
apply (erule (1) mdb_cte_at_Null_descendants)
apply (subgoal_tac "no_mloop (cdt a)")
prefer 2
apply (simp add: valid_mdb_def)
apply (clarsimp simp: exec_gets update_cdt_def bind_assoc set_cdt_def
exec_get exec_put set_original_def modify_def
simp del: fun_upd_apply
| (rule bind_execI[where f="cap_insert_ext x y z x' y'" for x y z x' y'], clarsimp simp: mdb_insert_abs.cap_insert_ext_det_def2 update_cdt_list_def set_cdt_list_def put_def simp del: fun_upd_apply) | rule refl)+
apply (clarsimp simp: put_def state_relation_def simp del: fun_upd_apply)
apply (drule updateCap_stuff)
apply clarsimp
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
apply (clarsimp simp: pspace_relations_def)
apply (thin_tac "gsCNodes t = p" for t p)+
apply (thin_tac "ksMachineState t = p" for t p)+
apply (thin_tac "ksCurThread t = p" for t p)+
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
apply (thin_tac "ksIdleThread t = p" for t p)+
apply (thin_tac "ksReadyQueues t = p" for t p)+
apply (thin_tac "ksSchedulerAction t = p" for t p)+
apply (thin_tac "cur_thread t = p" for t p)+
apply (thin_tac "domain_index t = p" for t p)+
apply (thin_tac "domain_time t = p" for t p)+
apply (thin_tac "cur_domain t = p" for t p)+
apply (thin_tac "scheduler_action t = p" for t p)+
apply (thin_tac "ready_queues t = p" for t p)+
apply (thin_tac "idle_thread t = p" for t p)+
apply (thin_tac "machine_state t = p" for t p)+
apply (thin_tac "work_units_completed t = p" for t p)+
apply (thin_tac "ksArchState t = p" for t p)+
apply (thin_tac "gsUserPages t = p" for t p)+
apply (thin_tac "ksCurDomain t = p" for t p)+
apply (thin_tac "ksInterruptState t = p" for t p)+
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
apply (thin_tac "ksDomainTime t = p" for t p)+
apply (thin_tac "ksDomSchedule t = p" for t p)+
apply (thin_tac "ctes_of t = p" for t p)+
apply (thin_tac "ekheap_relation t p" for t p)+
apply (thin_tac "pspace_relation t p" for t p)+
apply (thin_tac "interrupt_state_relation s t p" for s t p)+
apply (thin_tac "sched_act_relation t p" for t p)+
apply (thin_tac "ready_queues_relation t p" for t p)+
apply (rule conjI)
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation)
apply (subgoal_tac "cte_map dest \<noteq> 0")
prefer 2
apply (clarsimp simp: valid_mdb'_def
valid_mdb_ctes_def no_0_def)
apply (subgoal_tac "cte_map src \<noteq> 0")
prefer 2
apply (clarsimp simp: valid_mdb'_def
valid_mdb_ctes_def no_0_def)
apply (subgoal_tac "should_be_parent_of src_cap (is_original_cap a src) c (revokable src_cap c) = True")
prefer 2
apply (subst should_be_parent_of_masked_as_full[symmetric])
apply (subst safe_parent_is_parent)
apply ((simp add: cte_wp_at_caps_of_state)+)[4]
apply (subst conj_assoc[symmetric])
apply (rule conjI)
defer
apply (clarsimp simp: modify_map_apply)
apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply)
apply (simp split: if_split)
apply (rule conjI)
apply clarsimp
apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'")
prefer 2
apply (case_tac rv')
apply (clarsimp simp add: const_def modify_map_def split: if_split_asm)
apply clarsimp
apply (rule revokable_eq, assumption, assumption)
apply (subst same_region_as_relation [symmetric])
prefer 3
apply (rule safe_parent_same_region)
apply (simp add: cte_wp_at_caps_of_state)
apply assumption
apply assumption
apply (clarsimp simp: cte_wp_at_def is_simple_cap_def)
apply clarsimp
apply (case_tac srcCTE)
apply (case_tac rv')
apply clarsimp
apply (subgoal_tac "\<exists>cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')")
prefer 2
subgoal by (clarsimp simp: modify_map_def split: if_split_asm)
apply clarsimp
apply (drule set_cap_caps_of_state_monad)+
apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None")
prefer 2
subgoal by (clarsimp simp: cte_wp_at_caps_of_state null_filter_def split: if_splits)
apply clarsimp
apply (subgoal_tac "cte_at (aa,bb) a")
prefer 2
apply (drule null_filter_caps_of_stateD)
apply (erule cte_wp_at_weakenE, rule TrueI)
apply (subgoal_tac "mdbRevocable node = mdbRevocable node'")
apply clarsimp
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map dest")
subgoal by (clarsimp simp: modify_map_def split: if_split_asm)
apply (erule (5) cte_map_inj)
apply (rule setUntypedCapAsFull_corres)
apply simp+
apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_valid_list
set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap
setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+
subgoal by (clarsimp simp: modify_map_def split: if_split_asm)
apply clarsimp
apply (drule set_cap_caps_of_state_monad)+
apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None")
prefer 2
subgoal by (clarsimp simp: cte_wp_at_caps_of_state null_filter_def split: if_splits)
apply clarsimp
apply (subgoal_tac "cte_at (aa,bb) a")
prefer 2
apply (drule null_filter_caps_of_stateD)
apply (erule cte_wp_at_weakenE, rule TrueI)
apply (subgoal_tac "mdbRevocable node = mdbRevocable node'")
apply clarsimp
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map dest")
subgoal by (clarsimp simp: modify_map_def split: if_split_asm)
apply (erule (5) cte_map_inj)
apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb
set_untyped_cap_as_full_valid_list set_untyped_cap_as_full_cte_wp_at
setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for'
| clarsimp | wps)+
apply (clarsimp simp:cte_wp_at_caps_of_state )
apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def)
apply (wp getCTE_wp' get_cap_wp)+
@ -4882,7 +4880,6 @@ lemma cteInsert_simple_corres:
prefer 2
subgoal by (fastforce simp: cte_wp_at_def)
apply (erule conjE)
apply (subgoal_tac "mdb_insert (ctes_of b) (cte_map src) (maskedAsFull src_cap' c') src_node
(cte_map dest) NullCap dest_node")
prefer 2
@ -4978,9 +4975,9 @@ lemma cteInsert_simple_corres:
apply(drule cte_map_inj_eq)
apply(simp_all)[6]
apply(drule cte_map_inj_eq)
apply(simp_all)[6]
apply(simp_all)[6]
apply(drule cte_map_inj_eq)
apply(simp_all)[6]
apply(simp_all)[6]
by(fastforce)
declare if_split [split]

View File

@ -660,7 +660,7 @@ lemma deleteObjects_corres:
valid_pspace' s" in corres_underlying_split)
apply (rule corres_bind_return)
apply (rule corres_guard_imp[where r=dc])
apply (rule corres_split_deprecated[OF cNodeNoPartialOverlap])
apply (rule corres_split[OF _ cNodeNoPartialOverlap])
apply (rule corres_machine_op[OF corres_Id], simp+)
apply (rule no_fail_freeMemory, simp+)
apply (wp hoare_vcg_ex_lift)+

View File

@ -3450,8 +3450,8 @@ lemma unbindNotification_corres:
apply (rule corres_split[OF getNotification_corres])
apply clarsimp
apply (rule corres_split[OF setNotification_corres])
apply (rule setBoundNotification_corres)
apply (clarsimp simp: ntfn_relation_def split:Structures_A.ntfn.splits)
apply (clarsimp simp: ntfn_relation_def split:Structures_A.ntfn.splits)
apply (rule setBoundNotification_corres)
apply (wp gbn_wp' gbn_wp)+
apply (clarsimp elim!: obj_at_valid_objsE
dest!: bound_tcb_at_state_refs_ofD invs_valid_objs
@ -3476,8 +3476,8 @@ lemma unbindMaybeNotification_corres:
apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits)
apply (rule corres_return_trivial)
apply (rule corres_split[OF setNotification_corres])
apply (rule setBoundNotification_corres)
apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits)
apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits)
apply (rule setBoundNotification_corres)
apply (wp get_simple_ko_wp getNotification_wp)+
apply (clarsimp elim!: obj_at_valid_objsE
dest!: bound_tcb_at_state_refs_ofD invs_valid_objs
@ -3539,10 +3539,10 @@ lemma cap_delete_one_corres:
apply (rule corres_split[OF isFinalCapability_corres[where ptr=ptr]])
apply (simp add: split_def bind_assoc [THEN sym])
apply (rule corres_split[OF fast_finaliseCap_corres[where sl=ptr]])
apply (rule emptySlot_corres)
apply simp+
apply simp+
apply (rule emptySlot_corres, simp)
apply (wp hoare_drop_imps)+
apply (wp isFinalCapability_inv | wp (once) isFinal[where x="cte_map ptr"])+
apply (wp isFinalCapability_inv | wp (once) isFinal[where x="cte_map ptr"])+
apply (rule corres_trivial, simp)
apply (wp get_cap_wp getCTE_wp)+
apply (clarsimp simp: cte_wp_at_caps_of_state can_fast_finalise_Null

View File

@ -31,15 +31,15 @@ lemma setIRQState_corres:
apply (subgoal_tac "(state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)")
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (rule corres_machine_op)
apply (rule corres_Id | simp)+
apply (rule no_fail_maskInterrupt)
apply (simp add: getInterruptState_def setInterruptState_def
simpler_gets_def simpler_modify_def bind_def)
apply (simp add: simpler_modify_def[symmetric])
apply (rule corres_trivial, rule corres_modify)
apply (simp add: state_relation_def swp_def)
apply (clarsimp simp: interrupt_state_relation_def)
apply (simp add: getInterruptState_def setInterruptState_def
simpler_gets_def simpler_modify_def bind_def)
apply (simp add: simpler_modify_def[symmetric])
apply (rule corres_trivial, rule corres_modify)
apply (simp add: state_relation_def swp_def)
apply (clarsimp simp: interrupt_state_relation_def)
apply (rule corres_machine_op)
apply (rule corres_Id | simp)+
apply (rule no_fail_maskInterrupt)
apply (wp | simp)+
apply (clarsimp simp: irq_state_relation_def
split: irq_state.split_asm irqstate.split_asm)

View File

@ -221,15 +221,17 @@ lemma arch_decodeIRQControlInvocation_corres:
apply (clarsimp simp add: minIRQ_def maxIRQ_def ucast_nat_def)
apply (rule corres_split_eqr[OF is_irq_active_corres])
apply (rule whenE_throwError_corres, clarsimp, clarsimp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rule corres_splitEE[OF ensureEmptySlot_corres])
apply (rule corres_returnOkTT)
apply (clarsimp simp: arch_irq_control_inv_relation_def )
apply ((wpsimp wp: isIRQActive_inv arch_check_irq_maxIRQ_valid' checkIRQ_inv
simp: invs_valid_objs invs_psp_aligned invs_valid_objs'
invs_pspace_aligned' invs_pspace_distinct'
| strengthen invs_valid_objs invs_psp_aligned
| wp (once) hoare_drop_imps arch_check_irq_inv)+)
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (rule corres_splitEE)
apply (rule ensureEmptySlot_corres; simp)
apply (rule corres_returnOkTT)
apply (clarsimp simp: arch_irq_control_inv_relation_def )
apply ((wpsimp wp: isIRQActive_inv arch_check_irq_maxIRQ_valid' checkIRQ_inv
simp: invs_valid_objs invs_psp_aligned invs_valid_objs'
invs_pspace_aligned' invs_pspace_distinct'
| strengthen invs_valid_objs invs_psp_aligned
| wp (once) hoare_drop_imps arch_check_irq_inv)+)
apply (auto split: arch_invocation_label.splits invocation_label.splits)
done
@ -273,15 +275,17 @@ lemma decodeIRQControlInvocation_corres:
apply (clarsimp simp add: minIRQ_def maxIRQ_def ucast_nat_def)
apply (rule corres_split_eqr[OF is_irq_active_corres])
apply (rule whenE_throwError_corres, clarsimp, clarsimp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rule corres_splitEE[OF ensureEmptySlot_corres])
apply (rule corres_returnOkTT)
apply (clarsimp simp: arch_irq_control_inv_relation_def )
apply (wpsimp wp: isIRQActive_inv arch_check_irq_maxIRQ_valid' checkIRQ_inv
simp: invs_valid_objs invs_psp_aligned invs_valid_objs'
invs_pspace_aligned' invs_pspace_distinct'
| strengthen invs_valid_objs invs_psp_aligned
| wp (once) hoare_drop_imps arch_check_irq_inv)+
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (rule corres_splitEE)
apply (rule ensureEmptySlot_corres; simp)
apply (rule corres_returnOkTT)
apply (clarsimp simp: arch_irq_control_inv_relation_def )
apply (wpsimp wp: isIRQActive_inv arch_check_irq_maxIRQ_valid' checkIRQ_inv
simp: invs_valid_objs invs_psp_aligned invs_valid_objs'
invs_pspace_aligned' invs_pspace_distinct'
| strengthen invs_valid_objs invs_psp_aligned
| wp (once) hoare_drop_imps arch_check_irq_inv)+
apply (auto split: arch_invocation_label.splits invocation_label.splits
simp: not_less unat_le_helper)
done
@ -492,13 +496,12 @@ lemma arch_performIRQControl_corres:
apply (cases x2; simp add: ARM_H.performIRQControl_def invoke_irq_control.cases IRQ_def)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (rule corres_split_nor)
apply (rule cteInsert_simple_corres; simp)
apply (rule setIRQTrigger_corres)
apply (rule corres_split_nor)
apply (rule setIRQState_corres)
apply (simp add: irq_state_relation_def)
apply (wp | simp add: irq_state_relation_def IRQHandler_valid IRQHandler_valid')+
apply (rule setIRQTrigger_corres)
apply wp+
apply (rule cteInsert_simple_corres; simp)
apply (wp | simp add: irq_state_relation_def IRQHandler_valid IRQHandler_valid')+
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def cte_wp_at_caps_of_state
is_simple_cap_def is_cap_simps arch_irq_control_inv_valid_def
safe_parent_for_def)
@ -519,9 +522,9 @@ lemma performIRQControl_corres:
apply (cases i, simp_all add: performIRQControl_def)
apply (rule corres_guard_imp)
apply (rule corres_split_nor[OF setIRQState_corres])
apply (rule cteInsert_simple_corres)
apply (wp | simp add: irq_state_relation_def
IRQHandler_valid IRQHandler_valid')+
apply (simp add: irq_state_relation_def)
apply (rule cteInsert_simple_corres)
apply (wp | simp add: IRQHandler_valid IRQHandler_valid')+
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def
cte_wp_at_caps_of_state is_simple_cap_def
is_cap_simps safe_parent_for_def)
@ -650,73 +653,73 @@ lemma timerTick_corres:
apply (simp add: timerTick_def timer_tick_def)
apply (simp add:thread_state_case_if threadState_case_if)
apply (rule_tac Q="\<top> and (cur_tcb and valid_sched)" and Q'="\<top> and invs'" in corres_guard_imp)
apply (rule corres_guard_imp)
apply (rule corres_split[OF getCurThread_corres])
apply simp
apply (rule corres_split[OF getThreadState_corres])
apply (rename_tac state state')
apply (rule corres_split_deprecated[where r' = dc ])
apply simp
apply (rule corres_when,simp)
apply (rule corres_split[OF decDomainTime_corres])
apply (rule corres_split[OF getDomainTime_corres])
apply (rule corres_when,simp)
apply (rule rescheduleRequired_corres)
apply (wp hoare_drop_imp)+
apply (simp add:dec_domain_time_def)
apply wp+
apply (simp add:decDomainTime_def)
apply wp
apply (rule corres_if[where Q = \<top> and Q' = \<top>])
apply (case_tac state,simp_all)[1]
apply (simp add: Let_def)
apply (rule_tac r'="(=)" in corres_split[OF ethreadget_corres])
apply (rename_tac ts ts')
apply (rule_tac R="1 < ts" in corres_cases)
apply (simp)
apply (unfold thread_set_time_slice_def)
apply (rule ethread_set_corres, simp+)
apply (clarsimp simp: etcb_relation_def)
apply simp
apply (rule corres_split[OF ethread_set_corres])
apply (rule corres_split[OF tcbSchedAppend_corres])
apply (rule rescheduleRequired_corres)
apply (wp)[1]
apply (rule hoare_strengthen_post)
apply (rule tcbSchedAppend_invs_but_ct_not_inQ', clarsimp simp: sch_act_wf_weak)
apply (simp add: sch_act_wf_weak etcb_relation_def pred_conj_def)+
apply (rule corres_guard_imp)
apply (rule corres_split[OF getCurThread_corres])
apply simp
apply (rule corres_split[OF getThreadState_corres])
apply (rename_tac state state')
apply (rule corres_split[where r' = dc ])
apply (rule corres_if[where Q = \<top> and Q' = \<top>])
apply (case_tac state,simp_all)[1]
apply (simp add: Let_def)
apply (rule_tac r'="(=)" in corres_split[OF ethreadget_corres])
apply (simp add:etcb_relation_def)
apply (rename_tac ts ts')
apply (rule_tac R="1 < ts" in corres_cases)
apply (simp)
apply (unfold thread_set_time_slice_def)
apply (rule ethread_set_corres, simp+)
apply (clarsimp simp: etcb_relation_def)
apply simp
apply (rule corres_split)
apply (rule ethread_set_corres; simp)
apply (simp add: etcb_relation_def)
apply (rule corres_split[OF tcbSchedAppend_corres])
apply (rule rescheduleRequired_corres)
apply (wp)[1]
apply (rule hoare_strengthen_post)
apply (rule tcbSchedAppend_invs_but_ct_not_inQ',
clarsimp simp: sch_act_wf_weak)
apply (wp threadSet_timeslice_invs threadSet_valid_queues
threadSet_valid_queues' threadSet_pred_tcb_at_state)+
apply (simp add:etcb_relation_def)
apply (wp threadSet_timeslice_invs threadSet_valid_queues
threadSet_valid_queues' threadSet_pred_tcb_at_state)
apply simp
apply (wp|wpc|unfold Let_def|simp)+
apply (wp static_imp_wp threadSet_timeslice_invs threadSet_valid_queues threadSet_valid_queues'
threadSet_pred_tcb_at_state threadSet_weak_sch_act_wf tcbSchedAppend_valid_objs'
rescheduleRequired_weak_sch_act_wf tcbSchedAppend_valid_queues| simp)+
apply (strengthen sch_act_wf_weak)
apply (clarsimp simp:conj_comms)
apply (wp tcbSchedAppend_valid_queues tcbSchedAppend_sch_act_wf)
apply simp
apply (wp threadSet_valid_queues threadSet_pred_tcb_at_state threadSet_sch_act
threadSet_tcbDomain_triv threadSet_valid_queues' threadSet_valid_objs'| simp)+
apply (wp threadGet_wp gts_wp gts_wp')+
apply (clarsimp simp: cur_tcb_def tcb_at_is_etcb_at valid_sched_def valid_sched_action_def)
prefer 2
apply clarsimp
apply (clarsimp simp add:cur_tcb_def valid_sched_def
valid_sched_action_def valid_etcbs_def is_tcb_def
is_etcb_at_def st_tcb_at_def obj_at_def
dest!:get_tcb_SomeD)
apply (clarsimp simp: invs'_def valid_state'_def
sch_act_wf_weak
cur_tcb'_def inQ_def
ct_in_state'_def obj_at'_def)
apply (clarsimp simp:st_tcb_at'_def
valid_idle'_def ct_idle_or_in_cur_domain'_def
obj_at'_def projectKO_eq)
apply simp
apply simp
apply (rule corres_when,simp)
apply (rule corres_split[OF decDomainTime_corres])
apply (rule corres_split[OF getDomainTime_corres])
apply (rule corres_when,simp)
apply (rule rescheduleRequired_corres)
apply (wp hoare_drop_imp)+
apply (simp add:dec_domain_time_def)
apply wp+
apply (simp add:decDomainTime_def)
apply wp
apply (wp|wpc|unfold Let_def|simp)+
apply (wp static_imp_wp threadSet_timeslice_invs threadSet_valid_queues threadSet_valid_queues'
threadSet_pred_tcb_at_state threadSet_weak_sch_act_wf tcbSchedAppend_valid_objs'
rescheduleRequired_weak_sch_act_wf tcbSchedAppend_valid_queues| simp)+
apply (strengthen sch_act_wf_weak)
apply (clarsimp simp:conj_comms)
apply (wp tcbSchedAppend_valid_queues tcbSchedAppend_sch_act_wf)
apply simp
apply (wp threadSet_valid_queues threadSet_pred_tcb_at_state threadSet_sch_act
threadSet_tcbDomain_triv threadSet_valid_queues' threadSet_valid_objs'| simp)+
apply (wp threadGet_wp gts_wp gts_wp')+
apply (clarsimp simp: cur_tcb_def tcb_at_is_etcb_at valid_sched_def valid_sched_action_def)
prefer 2
apply clarsimp
apply (clarsimp simp add:cur_tcb_def valid_sched_def
valid_sched_action_def valid_etcbs_def is_tcb_def
is_etcb_at_def st_tcb_at_def obj_at_def
dest!:get_tcb_SomeD)
apply (clarsimp simp: invs'_def valid_state'_def
sch_act_wf_weak
cur_tcb'_def inQ_def
ct_in_state'_def obj_at'_def)
apply (clarsimp simp:st_tcb_at'_def
valid_idle'_def ct_idle_or_in_cur_domain'_def
obj_at'_def projectKO_eq)
apply simp
done
lemmas corres_eq_trivial = corres_Id[where f = h and g = h for h, simplified]
@ -736,7 +739,7 @@ lemma handleInterrupt_corres:
defer
apply (wp getIRQState_prop getIRQState_inv do_machine_op_bind doMachineOp_bind | simp add: do_machine_op_bind doMachineOp_bind )+
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated)
apply (rule corres_split)
apply (rule corres_machine_op, rule corres_eq_trivial ; (simp add: dc_def no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+
apply ((wp | simp)+)[4]
apply (rule corres_gen_asm2)
@ -754,20 +757,20 @@ lemma handleInterrupt_corres:
apply (rule corres_guard_imp, rule sendSignal_corres)
apply (clarsimp simp: valid_cap_def valid_cap'_def do_machine_op_bind doMachineOp_bind
arch_mask_irq_signal_def maskIrqSignal_def)+
apply (rule corres_split_deprecated)
apply (rule corres_split)
apply (rule corres_machine_op, rule corres_eq_trivial
; (simp add: no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+
apply ((wp | simp)+)
apply clarsimp
apply fastforce
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated)
apply simp
apply (rule corres_split[OF timerTick_corres corres_machine_op])
apply (rule corres_eq_trivial, simp+)
apply (rule corres_machine_op)
apply (rule corres_eq_trivial, (simp add: no_fail_ackInterrupt)+)
apply wp+
apply (rule corres_split)
apply (rule corres_split[OF timerTick_corres corres_machine_op])
apply (rule corres_eq_trivial, simp+)
apply wp+
apply (rule corres_machine_op)
apply (rule corres_eq_trivial, (simp add: no_fail_ackInterrupt)+)
apply wp+
apply clarsimp
apply clarsimp
done

View File

@ -199,9 +199,9 @@ lemma blocked_cancelIPC_corres:
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split[OF setEndpoint_corres])
apply (rule setThreadState_corres)
apply simp
apply (simp add: ep_relation_def)
apply (simp add: ep_relation_def)
apply (rule setThreadState_corres)
apply simp
apply (simp add: valid_tcb_state_def pred_conj_def)
apply (wp weak_sch_act_wf_lift)+
apply (clarsimp simp: st_tcb_at_tcb_at)
@ -222,9 +222,9 @@ lemma blocked_cancelIPC_corres:
apply clarsimp
apply (rule corres_guard_imp)
apply (rule corres_split[OF setEndpoint_corres])
apply (rule setThreadState_corres)
apply simp
apply (simp add: ep_relation_def)
apply (simp add: ep_relation_def)
apply (rule setThreadState_corres)
apply simp
apply (wp)+
apply (clarsimp simp: st_tcb_at_tcb_at)
apply (clarsimp simp: st_tcb_at_def obj_at_def)
@ -247,9 +247,9 @@ lemma blocked_cancelIPC_corres:
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split[OF setEndpoint_corres])
apply (rule setThreadState_corres)
apply simp
apply (simp add: ep_relation_def)
apply (simp add: ep_relation_def)
apply (rule setThreadState_corres)
apply simp
apply (simp add: valid_tcb_state_def pred_conj_def)
apply (wp weak_sch_act_wf_lift)+
apply (clarsimp simp: st_tcb_at_tcb_at)
@ -270,9 +270,9 @@ lemma blocked_cancelIPC_corres:
apply clarsimp
apply (rule corres_guard_imp)
apply (rule corres_split[OF setEndpoint_corres])
apply (rule setThreadState_corres)
apply simp
apply (simp add: ep_relation_def)
apply (simp add: ep_relation_def)
apply (rule setThreadState_corres)
apply simp
apply (wp)+
apply (clarsimp simp: st_tcb_at_tcb_at)
apply (clarsimp simp: st_tcb_at_def obj_at_def)
@ -325,15 +325,15 @@ lemma cancelSignal_corres:
apply (rule_tac R="remove1 t list = []" in corres_cases)
apply (simp del: dc_simp)
apply (rule corres_split[OF setNotification_corres])
apply (rule setThreadState_corres)
apply simp
apply (simp add: ntfn_relation_def)
apply (simp add: ntfn_relation_def)
apply (rule setThreadState_corres)
apply simp
apply (wp)+
apply (simp add: list_case_If del: dc_simp)
apply (rule corres_split[OF setNotification_corres])
apply (rule setThreadState_corres)
apply simp
apply (clarsimp simp add: ntfn_relation_def neq_Nil_conv)
apply (clarsimp simp add: ntfn_relation_def neq_Nil_conv)
apply (rule setThreadState_corres)
apply simp
apply (wp)+
apply (simp add: isWaitingNtfn_def ntfn_relation_def)
apply (wp getNotification_wp)+
@ -1244,20 +1244,21 @@ lemma tcbSchedDequeue_corres':
apply (simp add: ready_queues_relation_def)
apply (simp add: unless_def when_def)
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated[where r'="(=)", OF _ ethreadget_corres])
apply (simp split del: if_split)
apply (rule corres_split_eqr[OF ethreadget_corres])
apply (rule corres_split_eqr[OF getQueue_corres])
apply (simp split del: if_split)
apply (subst bind_return_unit, rule corres_split_deprecated[where r'=dc])
apply (rule corres_split_noop_rhs)
apply (simp add: dc_def[symmetric])
apply (rule threadSet_corres_noop, simp_all add: tcb_relation_def exst_same_def)[1]
apply (clarsimp, rule removeFromBitmap_corres_noop)
apply wp
apply (simp add: tcb_sched_dequeue_def)
apply (rule setQueue_corres)
apply (wp | simp add: etcb_relation_def)+
apply (rule corres_split[where r'="(=)"])
apply (rule ethreadget_corres, simp add: etcb_relation_def)
apply (simp split del: if_split)
apply (rule corres_split_eqr)
apply (rule ethreadget_corres, simp add: etcb_relation_def)
apply (rule corres_split_eqr[OF getQueue_corres])
apply (simp split del: if_split)
apply (subst bind_return_unit, rule corres_split[where r'=dc])
apply (simp add: tcb_sched_dequeue_def)
apply (rule setQueue_corres)
apply (rule corres_split_noop_rhs)
apply (clarsimp, rule removeFromBitmap_corres_noop)
apply (simp add: dc_def[symmetric])
apply (rule threadSet_corres_noop, simp_all add: tcb_relation_def exst_same_def)[1]
apply (wp | simp)+
done
lemma setQueue_valid_inQ_queues:
@ -1412,23 +1413,21 @@ lemma (in delete_one) suspend_corres:
apply (rule corres_split_nor[OF cancel_ipc_corres])
apply (rule corres_split[OF getThreadState_corres])
apply (rule corres_split_nor)
apply (rule corres_split_nor[OF setThreadState_corres])
apply (rule tcbSchedDequeue_corres')
apply wpsimp
apply wp
apply wpsimp
apply (rule corres_if)
apply (case_tac state; simp)
apply (simp add: update_restart_pc_def updateRestartPC_def)
apply (rule asUser_corres')
apply (simp add: ARM.nextInstructionRegister_def ARM.faultRegister_def
ARM_H.nextInstructionRegister_def ARM_H.faultRegister_def)
apply (simp add: ARM_H.Register_def)
apply (subst unit_dc_is_eq)
apply (rule corres_underlying_trivial)
apply (wpsimp simp: ARM.setRegister_def ARM.getRegister_def)
apply (rule corres_return_trivial)
apply (wpsimp simp: update_restart_pc_def updateRestartPC_def)+
apply (rule corres_if)
apply (case_tac state; simp)
apply (simp add: update_restart_pc_def updateRestartPC_def)
apply (rule asUser_corres')
apply (simp add: ARM.nextInstructionRegister_def ARM.faultRegister_def
ARM_H.nextInstructionRegister_def ARM_H.faultRegister_def)
apply (simp add: ARM_H.Register_def)
apply (subst unit_dc_is_eq)
apply (rule corres_underlying_trivial)
apply (wpsimp simp: ARM.setRegister_def ARM.getRegister_def)
apply (rule corres_return_trivial)
apply (rule corres_split_nor[OF setThreadState_corres])
apply simp
apply (rule tcbSchedDequeue_corres')
apply (wpsimp simp: update_restart_pc_def updateRestartPC_def)+
apply (rule hoare_post_imp[where Q = "\<lambda>rv s. tcb_at t s \<and> is_etcb_at t s"])
apply simp
apply wp
@ -1904,7 +1903,7 @@ lemma ep_cancel_corres_helper:
in corres_mapM_x)
apply clarsimp
apply (rule corres_guard_imp)
apply (subst bind_return_unit, rule corres_split_deprecated [OF tcbSchedEnqueue_corres])
apply (subst bind_return_unit, rule corres_split[OF _ tcbSchedEnqueue_corres])
apply simp
apply (rule corres_guard_imp [OF setThreadState_corres])
apply simp
@ -1915,10 +1914,10 @@ lemma ep_cancel_corres_helper:
apply (fastforce elim: obj_at'_weakenE)
apply ((wp hoare_vcg_const_Ball_lift | simp)+)[1]
apply (rule hoare_pre)
apply (wp hoare_vcg_const_Ball_lift
weak_sch_act_wf_lift_linear sts_st_tcb' setThreadState_not_st
sts_valid_queues tcbSchedEnqueue_not_st
| simp)+
apply (wp hoare_vcg_const_Ball_lift
weak_sch_act_wf_lift_linear sts_st_tcb' setThreadState_not_st
sts_valid_queues tcbSchedEnqueue_not_st
| simp)+
apply (auto elim: obj_at'_weakenE simp: valid_tcb_state'_def)
done
@ -1950,7 +1949,7 @@ proof -
apply (rule corres_underlying_split)
apply (rule corres_guard_imp [OF setEndpoint_corres])
apply (simp add: ep_relation_def)+
apply (rule corres_split_deprecated [OF rescheduleRequired_corres])
apply (rule corres_split[OF _ rescheduleRequired_corres])
apply (rule ep_cancel_corres_helper)
apply (rule mapM_x_wp')
apply (wp weak_sch_act_wf_lift_linear set_thread_state_runnable_weak_valid_sched_action | simp)+
@ -1962,11 +1961,11 @@ proof -
sts_valid_queues setThreadState_not_st sts_st_tcb' tcbSchedEnqueue_not_st
| clarsimp
| fastforce elim: obj_at'_weakenE simp: valid_tcb_state'_def)+)[2]
apply (rule hoare_name_pre_state)
apply (wp hoare_vcg_const_Ball_lift set_ep_valid_objs'
| (clarsimp simp: valid_ep'_def)
| (drule (1) bspec, clarsimp simp: valid_pspace'_def valid_tcb'_def valid_ep'_def elim!: valid_objs_valid_tcbE))+
done
apply (rule hoare_name_pre_state)
apply (wp hoare_vcg_const_Ball_lift set_ep_valid_objs'
| (clarsimp simp: valid_ep'_def)
| (drule (1) bspec, clarsimp simp: valid_pspace'_def valid_tcb'_def valid_ep'_def elim!: valid_objs_valid_tcbE))+
done
show ?thesis
apply (simp add: cancel_all_ipc_def cancelAllIPC_def)
@ -1990,8 +1989,8 @@ lemma set_ntfn_tcb_obj_at' [wp]:
"\<lbrace>obj_at' (P::tcb \<Rightarrow> bool) t\<rbrace>
setNotification ntfn v
\<lbrace>\<lambda>_. obj_at' P t\<rbrace>"
apply (clarsimp simp: setNotification_def, wp)
done
apply (clarsimp simp: setNotification_def, wp)
done
lemma cancelAllSignals_corres:
"corres dc (invs and valid_sched and ntfn_at ntfn) (invs' and ntfn_at' ntfn)
@ -2003,23 +2002,21 @@ lemma cancelAllSignals_corres:
apply (case_tac "ntfn_obj ntfna", simp_all add: ntfn_relation_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF setNotification_corres])
apply (rule corres_split_deprecated [OF rescheduleRequired_corres])
apply (rule ep_cancel_corres_helper)
apply (wp mapM_x_wp'[where 'b="det_ext state"]
weak_sch_act_wf_lift_linear setThreadState_not_st
set_thread_state_runnable_weak_valid_sched_action
| simp)+
apply (rename_tac list)
apply (rule_tac R="\<lambda>_ s. (\<forall>x\<in>set list. tcb_at' x s) \<and> valid_objs' s"
in hoare_post_add)
apply (rule mapM_x_wp')
apply (rule hoare_name_pre_state)
apply (wp hoare_vcg_const_Ball_lift
sts_st_tcb' sts_valid_queues setThreadState_not_st
tcbSchedEnqueue_not_st
| (clarsimp simp: valid_tcb_state'_def)
| fastforce elim: obj_at'_weakenE)+
apply (simp add: ntfn_relation_def)
apply (simp add: ntfn_relation_def)
apply (rule corres_split[OF _ rescheduleRequired_corres])
apply (rule ep_cancel_corres_helper)
apply (wp mapM_x_wp'[where 'b="det_ext state"]
weak_sch_act_wf_lift_linear setThreadState_not_st
set_thread_state_runnable_weak_valid_sched_action
| simp)+
apply (rename_tac list)
apply (rule_tac R="\<lambda>_ s. (\<forall>x\<in>set list. tcb_at' x s) \<and> valid_objs' s"
in hoare_post_add)
apply (rule mapM_x_wp')
apply (rule hoare_name_pre_state)
apply (wpsimp wp: hoare_vcg_const_Ball_lift
sts_st_tcb' sts_valid_queues setThreadState_not_st
simp: valid_tcb_state'_def)
apply (wp hoare_vcg_const_Ball_lift set_ntfn_aligned' set_ntfn_valid_objs'
weak_sch_act_wf_lift_linear
| simp)+
@ -2600,18 +2597,15 @@ lemma cancelBadgedSends_corres:
(cancel_badged_sends epptr bdg) (cancelBadgedSends epptr bdg)"
apply (simp add: cancel_badged_sends_def cancelBadgedSends_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF getEndpoint_corres get_simple_ko_sp get_ep_sp',
apply (rule corres_split[OF getEndpoint_corres _ get_simple_ko_sp get_ep_sp',
where Q="invs and valid_sched" and Q'=invs'])
apply simp_all
apply (case_tac ep, simp_all add: ep_relation_def)
apply (simp add: filterM_mapM list_case_return cong: list.case_cong)
apply (rule corres_guard_imp)
apply (rule corres_split_nor[OF setEndpoint_corres])
apply (rule corres_split_eqr[OF _ _ _ hoare_post_add[where R="\<lambda>_. valid_objs'"]])
apply (rule corres_split_deprecated [OF rescheduleRequired_corres])
apply (rule setEndpoint_corres)
apply (simp split: list.split add: ep_relation_def)
apply (wp weak_sch_act_wf_lift_linear)+
apply (simp add: ep_relation_def)
apply (rule corres_split_eqr[OF _ _ _ hoare_post_add[where R="\<lambda>_. valid_objs'"]])
apply (rule_tac S="(=)"
and Q="\<lambda>xs s. (\<forall>x \<in> set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s"
and Q'="\<lambda>xs s. (\<forall>x \<in> set xs. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s"
@ -2624,25 +2618,28 @@ lemma cancelBadgedSends_corres:
in corres_gen_asm)
apply (clarsimp simp: o_def dc_def[symmetric] liftM_def)
apply (rule corres_split[OF setThreadState_corres])
apply (rule corres_split[OF tcbSchedEnqueue_corres])
apply (rule corres_trivial)
apply simp
apply wp+
apply simp
apply (wp sts_valid_queues gts_st_tcb_at)+
apply simp
apply (rule corres_split[OF tcbSchedEnqueue_corres])
apply (rule corres_trivial)
apply simp
apply (wp sts_valid_queues gts_st_tcb_at)+
apply (clarsimp simp: valid_tcb_state_def tcb_at_def st_tcb_def2
st_tcb_at_refs_of_rev
dest!: state_refs_of_elemD elim!: tcb_at_is_etcb_at[rotated])
apply (simp add: is_tcb_def)
apply (wp hoare_vcg_const_Ball_lift gts_wp | clarsimp)+
apply (wp gts_st_tcb_at hoare_vcg_const_Ball_lift hoare_vcg_imp_lift
weak_sch_act_wf_lift_linear mapM_wp'
sts_st_tcb' sts_valid_queues setThreadState_valid_objs'
set_thread_state_runnable_weak_valid_sched_action
apply (simp add: is_tcb_def)
apply (wp hoare_vcg_const_Ball_lift gts_wp | clarsimp)+
apply (wp gts_st_tcb_at hoare_vcg_imp_lift
sts_st_tcb' sts_valid_queues
| clarsimp simp: valid_tcb_state'_def)+
apply (simp add: ep_relation_def)
apply (wp hoare_vcg_const_Ball_lift weak_sch_act_wf_lift_linear set_ep_valid_objs'
| simp)+
apply (rule corres_split[OF _ rescheduleRequired_corres])
apply (rule setEndpoint_corres)
apply (simp split: list.split add: ep_relation_def)
apply (wp weak_sch_act_wf_lift_linear)+
apply (wp gts_st_tcb_at hoare_vcg_imp_lift mapM_wp'
sts_st_tcb' sts_valid_queues
set_thread_state_runnable_weak_valid_sched_action
| clarsimp simp: valid_tcb_state'_def)+
apply (wp hoare_vcg_const_Ball_lift set_ep_valid_objs')+
apply (clarsimp simp: conj_comms)
apply (frule sym_refs_ko_atD, clarsimp+)
apply (rule obj_at_valid_objsE, assumption+, clarsimp+)

File diff suppressed because it is too large Load Diff

View File

@ -588,14 +588,14 @@ lemma kernel_corres:
apply (rule corres_guard_imp)
apply (rule corres_add_noop_lhs2)
apply (simp only: bind_assoc[symmetric])
apply (rule corres_split_deprecated[where r'=dc and
apply (rule corres_split[where r'=dc and
R="\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s" and
R'="\<lambda>_. \<top>"])
apply (rule corres_bind_return2, rule corres_stateAssert_assume_stronger)
apply simp
apply (simp add: kernelExitAssertions_def state_relation_def)
apply (simp only: bind_assoc)
apply (rule kernel_corres')
apply (simp only: bind_assoc)
apply (rule kernel_corres')
apply (rule corres_bind_return2, rule corres_stateAssert_assume_stronger)
apply simp
apply (simp add: kernelExitAssertions_def state_relation_def)
apply (wp call_kernel_domain_time_inv_det_ext call_kernel_domain_list_inv_det_ext)
apply wp
apply clarsimp
@ -679,13 +679,14 @@ lemma do_user_op_corres:
apply (rule_tac F = "dom (rvc \<circ> addrFromPPtr) \<subseteq> dom rvd" in corres_gen_asm)
apply simp
apply (rule_tac r'="(=)" in corres_split[OF corres_select])
apply (rule corres_underlying_split[OF corres_machine_op])
apply simp
apply (rule corres_underlying_trivial)
apply (simp add: user_memory_update_def)
apply (wp | simp)+
apply (rule corres_underlying_split[OF corres_machine_op,where Q = dc and Q'=dc])
apply (rule corres_underlying_trivial)
apply simp
apply (rule corres_underlying_split[OF corres_machine_op])
apply simp
apply (rule corres_underlying_trivial)
apply (simp add: user_memory_update_def)
apply (wp | simp)+
apply (rule corres_underlying_split[OF corres_machine_op,where Q = dc and Q'=dc])
apply (rule corres_underlying_trivial)
apply (wp | simp add: dc_def device_memory_update_def)+
apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def)
apply fastforce

View File

@ -1422,16 +1422,20 @@ lemma objBitsKO_gt_0: "0 < objBitsKO ko"
apply (simp_all add:archObjSize_def pageBits_def pteBits_def pdeBits_def)
done
lemma kheap_ekheap_double_gets: "(\<And>rv erv rv'. pspace_relation rv rv' \<Longrightarrow> ekheap_relation erv rv' \<Longrightarrow> corres r (R rv erv) (R' rv') (b rv erv) (d rv')) \<Longrightarrow>
corres r (\<lambda>s. R (kheap s) (ekheap s) s) (\<lambda>s. R' (ksPSpace s) s) (do x \<leftarrow> gets kheap; xa \<leftarrow> gets ekheap; b x xa od) (gets ksPSpace >>= d)"
lemma kheap_ekheap_double_gets:
"(\<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk>
\<Longrightarrow> corres r (R rv erv) (R' rv') (b rv erv) (d rv')) \<Longrightarrow>
corres r (\<lambda>s. R (kheap s) (ekheap s) s) (\<lambda>s. R' (ksPSpace s) s)
(do x \<leftarrow> gets kheap; xa \<leftarrow> gets ekheap; b x xa od) (gets ksPSpace >>= d)"
apply (rule corres_symb_exec_l)
apply (rule corres_guard_imp)
apply (rule_tac r'= "\<lambda>erv rv'. ekheap_relation erv rv' \<and> pspace_relation x rv'" in corres_split_deprecated)
apply (rule_tac r'= "\<lambda>erv rv'. ekheap_relation erv rv' \<and> pspace_relation x rv'"
in corres_split)
apply (subst corres_gets[where P="\<lambda>s. x = kheap s" and P'=\<top>])
apply clarsimp
apply assumption
apply (subst corres_gets[where P="\<lambda>s. x = kheap s" and P'=\<top>])
apply (simp add: state_relation_def)
apply clarsimp
apply (simp add: state_relation_def)
apply assumption
apply (wp gets_exs_valid | simp)+
done
@ -1787,19 +1791,19 @@ proof -
apply (simp add: not_less modify_modify bind_assoc[symmetric]
obj_bits_api[symmetric] shiftl_t2n upto_enum_red'
range_cover.unat_of_nat_n[OF cover])
apply (rule corres_split_nor[OF corres_trivial])
apply (clarsimp simp: retype_addrs_fold[symmetric] ptr_add_def upto_enum_red' not_zero'
range_cover.unat_of_nat_n[OF cover] word_le_sub1
simp del: word_of_nat_eq_0_iff)
apply (rule_tac f=g in arg_cong)
apply clarsimp
apply (rename_tac x eps ps)
apply (rule_tac P="\<lambda>s. x = kheap s \<and> eps = ekheap (s) \<and> ?P s" and
P'="\<lambda>s. ps = ksPSpace s \<and> ?P' s" in corres_modify)
apply (simp add: set_retype_addrs_fold new_caps_adds_fold)
apply (erule retype_state_relation[OF _ _ _ _ _ _ _ _ _ cover _ _ orr],
simp_all add: ko not_zero obj_bits_api
bound[simplified obj_bits_api ko])[1]
apply (rule corres_split_nor[OF _ corres_trivial])
apply (rename_tac x eps ps)
apply (rule_tac P="\<lambda>s. x = kheap s \<and> eps = ekheap (s) \<and> ?P s" and
P'="\<lambda>s. ps = ksPSpace s \<and> ?P' s" in corres_modify)
apply (simp add: set_retype_addrs_fold new_caps_adds_fold)
apply (erule retype_state_relation[OF _ _ _ _ _ _ _ _ _ cover _ _ orr],
simp_all add: ko not_zero obj_bits_api
bound[simplified obj_bits_api ko])[1]
apply (clarsimp simp: retype_addrs_fold[symmetric] ptr_add_def upto_enum_red' not_zero'
range_cover.unat_of_nat_n[OF cover] word_le_sub1
simp del: word_of_nat_eq_0_iff)
apply (rule_tac f=g in arg_cong)
apply clarsimp
apply wp+
apply (clarsimp split: option.splits)
apply (intro conjI impI)
@ -2533,25 +2537,24 @@ lemma copyGlobalMappings_corres:
pd_bits_def pdBits_def mapM_x_mapM)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule_tac F ="is_aligned pd 6 \<and> is_aligned global_pd 6" in corres_gen_asm)
apply (simp add: liftM_def[symmetric])
apply (rule_tac S="(=)" and r'=dc
and Q="\<lambda>xs s. \<forall>x \<in> set xs. pde_at (global_pd + (x << 2)) s
\<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and>
valid_etcbs s"
and Q'="\<lambda>xs s. \<forall>x \<in> set xs. pde_at' (global_pd + (x << 2)) s
\<and> pde_at' (pd + (x << 2)) s"
in corres_mapM_list_all2, (simp add: pdeBits_def)+)
apply (rule corres_guard_imp, rule corres_split_deprecated)
apply (erule storePDE_corres[OF _ refl])
apply (rule corres_rel_imp)
apply (rule_tac getObject_PDE_corres[OF refl])
apply clarsimp
apply (drule(1) pde_relation_aligned_eq)
apply fastforce
apply (wp hoare_vcg_const_Ball_lift | simp)+
apply (simp add: kernel_base_def ARM.pptrBase_def pptrBase_def list_all2_refl pageBits_def)
apply (rule corres_trivial, clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule corres_trivial, clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule_tac F ="is_aligned pd 6 \<and> is_aligned global_pd 6" in corres_gen_asm)
apply (simp add: liftM_def[symmetric])
apply (rule_tac S="(=)" and r'=dc
and Q="\<lambda>xs s. \<forall>x \<in> set xs. pde_at (global_pd + (x << 2)) s
\<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and>
valid_etcbs s"
and Q'="\<lambda>xs s. \<forall>x \<in> set xs. pde_at' (global_pd + (x << 2)) s
\<and> pde_at' (pd + (x << 2)) s"
in corres_mapM_list_all2, (simp add: pdeBits_def)+)
apply (rule corres_guard_imp, rule corres_split)
apply (rule_tac getObject_PDE_corres[OF refl])
apply (rule storePDE_corres[OF _ refl])
apply clarsimp
apply (drule(1) pde_relation_aligned_eq)
apply fastforce
apply (wp hoare_vcg_const_Ball_lift | simp)+
apply (simp add: kernel_base_def ARM.pptrBase_def pptrBase_def list_all2_refl pageBits_def)
apply wp+
apply (clarsimp simp: valid_arch_state_def)
apply (auto elim: page_directory_pde_atI is_aligned_weaken[OF pd_aligned])[1]
@ -5280,19 +5283,19 @@ lemma corres_retype_region_createNewCaps:
split del: if_split)[9] (* not PageDirectoryObject *)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule corres_split_nor)
apply (rule corres_trivial, simp)
apply (clarsimp simp: list_all2_same list_all2_map1 list_all2_map2
objBits_simps APIType_map2_def)
apply (rule corres_retype[where 'a = tcb],
simp_all add: obj_bits_api_def objBits_simps' pageBits_def
APIType_map2_def makeObjectKO_def
other_objs_default_relation)[1]
apply (fastforce simp: range_cover_def)
apply (rule corres_split_nor)
apply (simp add: APIType_map2_def)
apply (rule retype_region2_extra_ext_mapM_x_corres)
apply wp
apply (rule corres_trivial, simp)
apply (clarsimp simp: list_all2_same list_all2_map1 list_all2_map2
objBits_simps APIType_map2_def)
apply wp
apply (rule corres_retype[where 'a = tcb],
simp_all add: obj_bits_api_def objBits_simps' pageBits_def
APIType_map2_def makeObjectKO_def
other_objs_default_relation)[1]
apply (fastforce simp: range_cover_def)
apply wp
apply ((wp retype_region2_obj_at | simp add: APIType_map2_def)+)[1]
apply ((wp createObjects_tcb_at'[where sz=sz] | simp add: APIType_map2_def objBits_simps' obj_bits_api_def)+)[1]
apply simp
@ -5430,36 +5433,6 @@ lemma corres_retype_region_createNewCaps:
\<comment> \<open>PageDirectory\<close>
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (simp add: init_arch_objects_def APIType_map2_def
bind_assoc)
apply (rule corres_split_nor)
apply (simp add: liftM_def[symmetric] o_def list_all2_map1
list_all2_map2 list_all2_same
arch_default_cap_def mapM_x_mapM)
apply (simp add: dc_def[symmetric])
apply (rule corres_machine_op)
apply (rule corres_Id)
apply (simp add: shiftl_t2n shiftL_nat
pdBits_def ptBits_def pageBits_def pt_bits_def)
defer
apply simp
apply (simp add: mapM_discarded[where g = "return ()",simplified,symmetric])
apply (rule no_fail_pre)
apply (wp no_fail_mapM|clarsimp)+
apply (simp add: mapM_x_mapM)
apply (rule corres_underlying_split[where r' = dc])
apply (rule_tac Q="\<lambda>xs s. (\<forall>x \<in> set xs. page_directory_at x s)
\<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_etcbs s"
and Q'="\<lambda>xs s. (\<forall>x \<in> set xs. page_directory_at' x s) \<and> valid_arch_state' s"
in corres_mapM_list_all2[where r'=dc and S="(=)"])
apply simp+
apply (rule corres_guard_imp, rule copyGlobalMappings_corres)
apply simp+
apply (wp hoare_vcg_const_Ball_lift | simp)+
apply (simp add: list_all2_same)
apply (rule corres_return[where P =\<top> and P'=\<top>,THEN iffD2])
apply simp
apply wp+
apply (rule corres_retype[where ty = "Inr PageDirectoryObject" and 'a = pde
, simplified, folded retype_region2_ext_retype_region_ArchObject_PageDirectoryObj],
simp_all add: APIType_map2_def obj_bits_api_def
@ -5469,7 +5442,36 @@ lemma corres_retype_region_createNewCaps:
makeObjectKO_def)[1]
apply (simp add: range_cover_def)+
apply (rule pagedirectory_relation_retype)
apply (wp | simp)+
apply (simp add: init_arch_objects_def APIType_map2_def
bind_assoc)
apply (rule corres_split_nor)
apply (simp add: mapM_x_mapM)
apply (rule corres_underlying_split[where r' = dc])
apply (rule_tac Q="\<lambda>xs s. (\<forall>x \<in> set xs. page_directory_at x s)
\<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_etcbs s"
and Q'="\<lambda>xs s. (\<forall>x \<in> set xs. page_directory_at' x s) \<and> valid_arch_state' s"
in corres_mapM_list_all2[where r'=dc and S="(=)"])
apply simp+
apply (rule corres_guard_imp, rule copyGlobalMappings_corres)
apply simp+
apply (wp hoare_vcg_const_Ball_lift | simp)+
apply (simp add: list_all2_same)
apply (rule corres_return[where P =\<top> and P'=\<top>,THEN iffD2])
apply simp
apply wp+
apply (simp add: liftM_def[symmetric] o_def list_all2_map1
list_all2_map2 list_all2_same
arch_default_cap_def mapM_x_mapM)
apply (simp add: dc_def[symmetric])
apply (rule corres_machine_op)
apply (rule corres_Id)
apply (simp add: shiftl_t2n shiftL_nat
pdBits_def ptBits_def pageBits_def pt_bits_def)
defer
apply simp
apply (simp add: mapM_discarded[where g = "return ()",simplified,symmetric])
apply (rule no_fail_pre)
apply (wp no_fail_mapM|clarsimp)+
apply (rule hoare_vcg_conj_lift)
apply (rule hoare_post_imp)
prefer 2
@ -5521,7 +5523,7 @@ lemma corres_retype_region_createNewCaps:
APIType_map2_def default_arch_object_def default_object_def archObjSize_def
pteBits_def pdeBits_def
pd_bits_def fromIntegral_def toInteger_nat fromInteger_nat)
done
done
end
end

View File

@ -49,15 +49,15 @@ proof -
apply (subst P)
apply (rule corres_guard_imp)
apply (rule corres_split[OF x])
apply (rule corres_if2)
apply (case_tac ra, clarsimp+)[1]
apply (rule corres_trivial, clarsimp)
apply (case_tac ra, simp_all)[1]
apply (erule(1) meta_mp [OF _ suffix_ConsD])
apply assumption
apply assumption
apply (rule corres_if2)
apply (case_tac ra, clarsimp+)[1]
apply (rule corres_trivial, clarsimp)
apply (case_tac ra, simp_all)[1]
apply (erule(1) meta_mp [OF _ suffix_ConsD])
apply (rule Q)
apply (rule hoare_post_imp [OF _ z])
apply simp+
apply simp+
done
qed
@ -118,21 +118,30 @@ lemma tcbSchedAppend_corres:
apply clarsimp
apply (clarsimp simp: unless_def when_def cong: if_cong)
apply (rule stronger_corres_guard_imp)
apply (rule corres_split_deprecated[where r'="(=)", OF _ ethreadget_corres])
apply (rule corres_split_deprecated[where r'="(=)", OF _ ethreadget_corres])
apply (rule corres_split_deprecated[where r'="(=)"])
apply (rule corres_split_noop_rhs2)
apply (rule corres_split_noop_rhs2)
apply (rule threadSet_corres_noop, simp_all add: tcb_relation_def exst_same_def)[1]
apply (rule addToBitmap_if_null_noop_corres)
apply wp+
apply (simp add: tcb_sched_append_def)
apply (intro conjI impI)
apply (rule corres_guard_imp)
apply (rule setQueue_corres)
prefer 3
apply (rule_tac P=\<top> and Q="K (t \<notin> set queuea)" in corres_assume_pre)
apply (wp getQueue_corres getObject_tcb_wp | simp add: etcb_relation_def threadGet_def)+
apply (rule corres_split[where r'="(=)"])
apply (rule ethreadget_corres)
apply (simp add: etcb_relation_def)
apply (rule corres_split[where r'="(=)"])
apply (rule ethreadget_corres)
apply (simp add: etcb_relation_def)
apply (rule corres_split[where r'="(=)"])
apply simp
apply (rule getQueue_corres)
apply (rule corres_split_noop_rhs2)
apply (simp add: tcb_sched_append_def)
apply (intro conjI impI)
apply (rule corres_guard_imp)
apply (rule setQueue_corres)
prefer 3
apply (rule_tac P=\<top> and Q="K (t \<notin> set queuea)" in corres_assume_pre)
apply simp
apply simp
apply simp
apply (rule corres_split_noop_rhs2)
apply (rule addToBitmap_if_null_noop_corres)
apply (rule threadSet_corres_noop, simp_all add: tcb_relation_def exst_same_def)[1]
apply wp+
apply (wp getObject_tcb_wp | simp add: threadGet_def)+
apply (fastforce simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_def inQ_def
projectKO_eq project_inject)
done
@ -1698,11 +1707,11 @@ lemma scheduleChooseNewThread_fragment_corres:
apply (subst bind_dummy_ret_val)
apply (subst bind_dummy_ret_val)
apply (rule corres_guard_imp)
apply (rule corres_split[OF corres_when])
apply simp
apply (rule chooseThread_corres)
apply simp
apply (rule nextDomain_corres)
apply (rule corres_split)
apply (rule corres_when, simp)
apply (rule nextDomain_corres)
apply simp
apply (rule chooseThread_corres)
apply (wp nextDomain_invs_no_cicd')+
apply (clarsimp simp: valid_sched_def invs'_def valid_state'_def all_invs_but_ct_idle_or_in_cur_domain'_def)+
done
@ -1806,80 +1815,83 @@ lemma schedule_corres:
apply (subst schact_bind_inside)
apply (rule corres_guard_imp)
apply (rule corres_split[OF getCurThread_corres[THEN corres_rel_imp[where r="\<lambda>x y. y = x"],simplified]])
apply (rule corres_split[OF getSchedulerAction_corres])
apply (rule corres_split_sched_act,assumption)
apply (rule_tac P="tcb_at ct" in corres_symb_exec_l')
apply (rule_tac corres_symb_exec_l)
apply simp
apply (rule corres_assert_ret)
apply ((wpsimp wp: thread_get_wp' gets_exs_valid)+)
apply (rule corres_split[OF getSchedulerAction_corres])
apply (rule corres_split_sched_act,assumption)
apply (rule_tac P="tcb_at ct" in corres_symb_exec_l')
apply (rule_tac corres_symb_exec_l)
apply simp
apply (rule corres_assert_ret)
apply ((wpsimp wp: thread_get_wp' gets_exs_valid)+)
prefer 2
(* choose thread *)
apply clarsimp
apply (rule corres_split[OF thread_get_isRunnable_corres])
apply (rule corres_split[OF corres_when])
apply (rule corres_split[OF thread_get_isRunnable_corres])
apply (rule corres_split)
apply (rule corres_when, simp)
apply (rule tcbSchedEnqueue_corres)
apply (rule scheduleChooseNewThread_corres, simp)
apply (rule tcbSchedEnqueue_corres, simp)
apply (wp thread_get_wp' tcbSchedEnqueue_invs' hoare_vcg_conj_lift hoare_drop_imps
| clarsimp)+
apply (wp thread_get_wp' tcbSchedEnqueue_invs' hoare_vcg_conj_lift hoare_drop_imps
| clarsimp)+
(* switch to thread *)
apply (rule corres_split[OF thread_get_isRunnable_corres],
rename_tac was_running wasRunning)
apply (rule corres_split[OF corres_when])
apply (rule corres_split[OF getIdleThread_corres], rename_tac it it')
apply (rule_tac F="was_running \<longrightarrow> ct \<noteq> it" in corres_gen_asm)
apply (rule corres_split[OF ethreadget_corres[where r="(=)"]],
rename_tac tp tp')
apply (rule corres_split[OF ethread_get_when_corres[where r="(=)"]],
rename_tac cp cp')
apply (rule corres_split[OF scheduleSwitchThreadFastfail_corres])
apply (rule corres_split[OF curDomain_corres])
apply (rule corres_split[OF isHighestPrio_corres]; simp only:)
apply (rule corres_if, simp)
apply (rule corres_split[OF tcbSchedEnqueue_corres])
apply (simp, fold dc_def)
apply (rule corres_split[OF setSchedulerAction_corres])
apply (rule scheduleChooseNewThread_corres, simp)
apply (rule corres_split)
apply (rule corres_when, simp)
apply (rule tcbSchedEnqueue_corres)
apply (rule corres_split[OF getIdleThread_corres], rename_tac it it')
apply (rule_tac F="was_running \<longrightarrow> ct \<noteq> it" in corres_gen_asm)
apply (rule corres_split)
apply (rule ethreadget_corres[where r="(=)"])
apply (clarsimp simp: etcb_relation_def)
apply (rename_tac tp tp')
apply (rule corres_split)
apply (rule ethread_get_when_corres[where r="(=)"])
apply (clarsimp simp: etcb_relation_def)
apply (rename_tac cp cp')
apply (rule corres_split)
apply (rule scheduleSwitchThreadFastfail_corres; simp)
apply (rule corres_split[OF curDomain_corres])
apply (rule corres_split[OF isHighestPrio_corres]; simp only:)
apply (rule corres_if, simp)
apply (rule corres_split[OF tcbSchedEnqueue_corres])
apply (simp, fold dc_def)
apply (rule corres_split)
apply (rule setSchedulerAction_corres; simp)
apply (rule scheduleChooseNewThread_corres)
apply (wp | simp)+
apply (simp add: valid_sched_def)
apply wp
apply (rule hoare_vcg_conj_lift)
apply (rule_tac t=t in set_scheduler_action_cnt_valid_blocked')
apply (wpsimp wp: setSchedulerAction_invs')+
apply (wp tcb_sched_action_enqueue_valid_blocked hoare_vcg_all_lift enqueue_thread_queued)
apply (wp tcbSchedEnqueue_invs'_not_ResumeCurrentThread)
apply (rule corres_if, fastforce)
apply (rule corres_split[OF tcbSchedAppend_corres])
apply (simp, fold dc_def)
apply (rule corres_split)
apply (rule setSchedulerAction_corres; simp)
apply (rule scheduleChooseNewThread_corres)
apply (wp | simp)+
apply (simp add: valid_sched_def)
apply wp
apply (rule hoare_vcg_conj_lift)
apply (rule_tac t=t in set_scheduler_action_cnt_valid_blocked')
apply (wpsimp wp: setSchedulerAction_invs')+
apply (wp tcb_sched_action_append_valid_blocked hoare_vcg_all_lift append_thread_queued)
apply (wp tcbSchedAppend_invs'_not_ResumeCurrentThread)
apply (wp | simp)+
apply (simp add: valid_sched_def)
apply wp
apply (rule hoare_vcg_conj_lift)
apply (rule_tac t=t in set_scheduler_action_cnt_valid_blocked')
apply (wpsimp wp: setSchedulerAction_invs')+
apply (wp tcb_sched_action_enqueue_valid_blocked hoare_vcg_all_lift enqueue_thread_queued)
apply (wp tcbSchedEnqueue_invs'_not_ResumeCurrentThread)
apply (rule corres_split[OF guarded_switch_to_corres], simp)
apply (rule setSchedulerAction_corres[simplified dc_def])
apply (wp | simp)+
apply (rule corres_if, fastforce)
(* isHighestPrio *)
apply (clarsimp simp: if_apply_def2)
apply ((wp (once) hoare_drop_imp)+)[1]
apply (rule corres_split[OF tcbSchedAppend_corres])
apply (simp, fold dc_def)
apply (rule corres_split[OF setSchedulerAction_corres])
apply (rule scheduleChooseNewThread_corres, simp)
apply (wp | simp)+
apply (simp add: valid_sched_def)
apply wp
apply (rule hoare_vcg_conj_lift)
apply (rule_tac t=t in set_scheduler_action_cnt_valid_blocked')
apply (wpsimp wp: setSchedulerAction_invs')+
apply (wp tcb_sched_action_append_valid_blocked hoare_vcg_all_lift append_thread_queued)
apply (wp tcbSchedAppend_invs'_not_ResumeCurrentThread)
apply (rule corres_split[OF guarded_switch_to_corres], simp)
apply (rule setSchedulerAction_corres[simplified dc_def])
apply (wp | simp)+
(* isHighestPrio *)
apply (clarsimp simp: if_apply_def2)
apply ((wp (once) hoare_drop_imp)+)[1]
apply (simp add: if_apply_def2)
apply ((wp (once) hoare_drop_imp)+)[1]
apply wpsimp+
apply (wpsimp simp: etcb_relation_def)+
apply (rule tcbSchedEnqueue_corres)
apply wpsimp+
apply (simp add: if_apply_def2)
apply ((wp (once) hoare_drop_imp)+)[1]
apply wpsimp+
apply (clarsimp simp: conj_ac cong: conj_cong)
apply wp
@ -2269,18 +2281,20 @@ lemma possibleSwitchTo_corres:
apply (simp add: possible_switch_to_def possibleSwitchTo_def cong: if_cong)
apply (rule corres_guard_imp)
apply (rule corres_split[OF curDomain_corres], simp)
apply (rule corres_split[OF ethreadget_corres[where r="(=)"]])
apply (rule corres_split[OF getSchedulerAction_corres])
apply (rule corres_if, simp)
apply (rule tcbSchedEnqueue_corres)
apply (rule corres_if, simp)
apply (case_tac action; simp)
apply (rule corres_split[OF rescheduleRequired_corres])
apply (rule tcbSchedEnqueue_corres)
apply (wp rescheduleRequired_valid_queues'_weak)+
apply (rule setSchedulerAction_corres, simp)
apply (wpsimp simp: etcb_relation_def if_apply_def2
wp: hoare_drop_imp[where f="ethread_get a b" for a b])+
apply (rule corres_split)
apply (rule ethreadget_corres[where r="(=)"])
apply (clarsimp simp: etcb_relation_def)
apply (rule corres_split[OF getSchedulerAction_corres])
apply (rule corres_if, simp)
apply (rule tcbSchedEnqueue_corres)
apply (rule corres_if, simp)
apply (case_tac action; simp)
apply (rule corres_split[OF rescheduleRequired_corres])
apply (rule tcbSchedEnqueue_corres)
apply (wp rescheduleRequired_valid_queues'_weak)+
apply (rule setSchedulerAction_corres, simp)
apply (wpsimp simp: if_apply_def2
wp: hoare_drop_imp[where f="ethread_get a b" for a b])+
apply (wp hoare_drop_imps)[1]
apply wp+
apply (fastforce simp: valid_sched_def invs_def valid_state_def cur_tcb_def

View File

@ -139,24 +139,25 @@ lemma decodeDomainInvocation_corres:
apply (simp+)[2]
apply (case_tac "args", simp_all)
apply (rule corres_guard_imp)
apply (rule_tac r'="\<lambda>domain domain'. domain = domain'" and R="\<lambda>_. \<top>" and R'="\<lambda>_. \<top>" in corres_splitEE)
apply (rule whenE_throwError_corres_initial)
apply simp
apply (case_tac "cs")
apply ((case_tac "cs'", ((simp add: null_def)+)[2])+)[2]
apply (subgoal_tac "cap_relation (fst (hd cs)) (fst (hd cs'))")
apply (case_tac "fst (hd cs)")
apply (case_tac "fst (hd cs')", simp+, rule corres_returnOkTT)
apply (simp add: inv_relation_def o_def uncurry_def)
apply (case_tac "fst (hd cs')", fastforce+)
apply (case_tac "cs")
apply (case_tac "cs'", ((simp add: list_all2_map2 list_all2_map1)+)[2])
apply (case_tac "cs'", ((simp add: list_all2_map2 list_all2_map1)+)[2])
apply (rule whenE_throwError_corres)
apply (simp+)[2]
apply (rule corres_returnOkTT)
apply (rule_tac r'="\<lambda>domain domain'. domain = domain'" and R="\<lambda>_. \<top>" and R'="\<lambda>_. \<top>"
in corres_splitEE) apply (rule whenE_throwError_corres)
apply (simp+)[2]
apply (rule corres_returnOkTT)
apply simp
apply (rule whenE_throwError_corres_initial)
apply simp
apply (case_tac "cs")
apply ((case_tac "cs'", ((simp add: null_def)+)[2])+)[2]
apply (subgoal_tac "cap_relation (fst (hd cs)) (fst (hd cs'))")
apply (case_tac "fst (hd cs)")
apply (case_tac "fst (hd cs')", simp+, rule corres_returnOkTT)
apply (simp add: inv_relation_def o_def uncurry_def)
apply (case_tac "fst (hd cs')", fastforce+)
apply (case_tac "cs")
apply (case_tac "cs'", ((simp add: list_all2_map2 list_all2_map1)+)[2])
apply (case_tac "cs'", ((simp add: list_all2_map2 list_all2_map1)+)[2])
apply (wp | simp)+
done
done
lemma decodeInvocation_corres:
"\<lbrakk>cptr = to_bl cptr'; mi' = message_info_map mi;
@ -266,10 +267,10 @@ lemma hinv_corres_assist:
\<comment> \<open>switched over to argument of corres_cap_fault\<close>
apply (rule lookupCapAndSlot_corres, simp)
apply (rule corres_split[OF lookupIPCBuffer_corres])
apply (rule corres_splitEE[OF lookupExtraCaps_corres])
apply (rule corres_returnOkTT)
apply simp+
apply (wp | simp)+
apply (rule corres_splitEE)
apply (rule lookupExtraCaps_corres; simp)
apply (rule corres_returnOkTT)
apply (wp | simp)+
apply auto
done
@ -350,17 +351,18 @@ lemma setDomain_corres:
apply (rule corres_guard_imp)
apply (rule corres_split[OF getCurThread_corres])
apply (rule corres_split[OF tcbSchedDequeue_corres])
apply (rule corres_split[OF ethread_set_corres])
apply (rule corres_split[OF isRunnable_corres])
apply simp
apply (rule corres_split_deprecated[OF corres_when[OF refl]])
apply (rule rescheduleRequired_corres)
apply clarsimp
apply (rule corres_when[OF refl])
apply (rule tcbSchedEnqueue_corres)
apply (wp hoare_drop_imps hoare_vcg_conj_lift | clarsimp| assumption)+
apply (clarsimp simp: etcb_relation_def)
apply ((wp hoare_vcg_conj_lift hoare_vcg_disj_lift | clarsimp)+)[1]
apply (rule corres_split)
apply (rule ethread_set_corres; simp)
apply (clarsimp simp: etcb_relation_def)
apply (rule corres_split[OF isRunnable_corres])
apply simp
apply (rule corres_split)
apply clarsimp
apply (rule corres_when[OF refl])
apply (rule tcbSchedEnqueue_corres)
apply (rule corres_when[OF refl])
apply (rule rescheduleRequired_corres)
apply ((wp hoare_drop_imps hoare_vcg_conj_lift | clarsimp| assumption)+)[5]
apply clarsimp
apply (rule_tac Q="\<lambda>_. valid_objs' and valid_queues' and valid_queues and
(\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and tcb_at' tptr"
@ -397,60 +399,61 @@ lemma performInvocation_corres:
apply (case_tac i)
apply (clarsimp simp: o_def liftE_bindE)
apply (rule corres_guard_imp)
apply (rule corres_split_norE[OF corres_returnOkTT])
apply simp
apply (rule corres_rel_imp, rule inv_untyped_corres)
apply simp
apply (case_tac x, simp_all)[1]
apply (rule corres_split_norE)
apply (rule corres_rel_imp, rule inv_untyped_corres)
apply simp
apply (case_tac x, simp_all)[1]
apply (rule corres_returnOkTT)
apply simp
apply wp+
apply simp+
apply (rule corres_guard_imp)
apply (rule corres_split[OF getCurThread_corres])
apply simp
apply (rule corres_split[OF sendIPC_corres])
apply (rule corres_split[OF getCurThread_corres])
apply simp
apply (rule corres_split[OF sendIPC_corres])
apply simp
apply (rule corres_trivial)
apply simp
apply simp
apply wp+
apply (clarsimp simp: ct_in_state_def)
apply (fastforce elim: st_tcb_ex_cap)
apply (clarsimp simp: pred_conj_def invs'_def cur_tcb'_def simple_sane_strg
sch_act_simple_def)
apply (rule corres_guard_imp)
apply (simp add: liftE_bindE)
apply (rule corres_split[OF sendSignal_corres])
apply (rule corres_trivial)
apply (simp add: returnOk_def)
apply wp+
apply (simp+)[2]
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[OF getCurThread_corres])
apply (rule corres_split_nor[OF doReplyTransfer_corres'])
apply (rule corres_trivial, simp)
apply wp+
apply (clarsimp simp: ct_in_state_def)
apply (fastforce elim: st_tcb_ex_cap)
apply (clarsimp simp: pred_conj_def invs'_def cur_tcb'_def simple_sane_strg
sch_act_simple_def)
apply (rule corres_guard_imp)
apply (simp add: liftE_bindE)
apply (rule corres_split[OF sendSignal_corres])
apply (rule corres_trivial)
apply (simp add: returnOk_def)
apply wp+
apply (clarsimp simp: tcb_at_invs)
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def)
apply (simp+)[2]
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[OF getCurThread_corres])
apply (rule corres_split_nor[OF doReplyTransfer_corres'])
apply (rule corres_trivial, simp)
apply wp+
apply (clarsimp simp: tcb_at_invs)
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def)
apply (erule cte_wp_at_weakenE, fastforce simp: is_reply_cap_to_def)
apply (clarsimp simp: tcb_at_invs')
apply (fastforce elim!: cte_wp_at_weakenE')
apply (clarsimp simp: liftME_def)
apply (rule corres_guard_imp)
apply (erule invokeTCB_corres)
apply (simp)+
\<comment> \<open>domain cap\<close>
apply (clarsimp simp: tcb_at_invs')
apply (fastforce elim!: cte_wp_at_weakenE')
apply (clarsimp simp: liftME_def)
apply (rule corres_guard_imp)
apply (erule invokeTCB_corres)
apply (simp)+
\<comment> \<open>domain cap\<close>
apply (clarsimp simp: invoke_domain_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF setDomain_corres])
apply (rule corres_trivial, simp)
apply (wp)+
apply (rule corres_split[OF setDomain_corres])
apply (rule corres_trivial, simp)
apply (wp)+
apply (clarsimp+)[2]
\<comment> \<open>CNodes\<close>
apply clarsimp
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF invokeCNode_corres])
apply (rule corres_trivial, simp add: returnOk_def)
apply assumption
apply assumption
apply (rule corres_trivial, simp add: returnOk_def)
apply wp+
apply (clarsimp+)[2]
apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric])
@ -1231,24 +1234,26 @@ lemma handleInvocation_corres:
apply (clarsimp simp: when_def)
apply (rule replyFromKernel_corres)
apply (rule corres_split[OF setThreadState_corres])
apply (rule corres_splitEE[OF performInvocation_corres])
apply simp
apply (rule corres_split[OF getThreadState_corres])
apply (rename_tac state state')
apply (case_tac state, simp_all)[1]
apply (fold dc_def)[1]
apply (rule corres_split_deprecated [OF setThreadState_corres])
apply simp
apply (rule corres_when [OF refl replyFromKernel_corres])
apply (simp add: when_def)
apply (rule conjI, rule impI)
apply (rule reply_from_kernel_tcb_at)
apply (rule impI, wp+)
apply (simp)+
apply (wp hoare_drop_imps)+
apply (simp)
apply (wp)
apply (simp)
apply simp
apply (rule corres_splitEE)
apply (rule performInvocation_corres; simp)
apply simp
apply (rule corres_split[OF getThreadState_corres])
apply (rename_tac state state')
apply (case_tac state, simp_all)[1]
apply (fold dc_def)[1]
apply (rule corres_split)
apply (rule corres_when [OF refl replyFromKernel_corres])
apply (rule setThreadState_corres)
apply simp
apply (simp add: when_def)
apply (rule conjI, rule impI)
apply (rule reply_from_kernel_tcb_at)
apply (rule impI, wp+)
apply simp+
apply (wp hoare_drop_imps)+
apply simp
apply wp
apply simp
apply (rule_tac Q="\<lambda>rv. einvs and simple_sched_action and valid_invocation rve
and (\<lambda>s. thread = cur_thread s)
@ -1503,17 +1508,16 @@ lemma handleRecv_isBlocking_corres':
apply (rule corres_split_eqr[OF getCurThread_corres])
apply (rule corres_split_eqr[OF asUser_getRegister_corres])
apply (rule corres_split_catch)
apply (erule handleFault_corres)
apply (rule corres_cap_fault)
apply (rule corres_splitEE[OF lookupCap_corres])
apply (rule_tac P="?pre1 and tcb_at thread
and (\<lambda>s. (cur_thread s) = thread )
and valid_cap rv"
and P'="?pre2 and tcb_at' thread and valid_cap' rv'" in corres_inst)
apply (clarsimp split: cap_relation_split_asm arch_cap.split_asm split del: if_split
simp: lookup_failure_map_def whenE_def)
apply (rule corres_guard_imp)
apply (rename_tac rights)
apply (rule corres_cap_fault)
apply (rule corres_splitEE[OF lookupCap_corres])
apply (rule_tac P="?pre1 and tcb_at thread
and (\<lambda>s. (cur_thread s) = thread )
and valid_cap rv"
and P'="?pre2 and tcb_at' thread and valid_cap' rv'" in corres_inst)
apply (clarsimp split: cap_relation_split_asm arch_cap.split_asm split del: if_split
simp: lookup_failure_map_def whenE_def)
apply (rule corres_guard_imp)
apply (rename_tac rights)
apply (case_tac "AllowRead \<in> rights"; simp)
apply (rule corres_split_nor[OF deleteCallerCap_corres])
apply (rule receiveIPC_corres)
@ -1521,31 +1525,35 @@ lemma handleRecv_isBlocking_corres':
apply (wp delete_caller_cap_nonz_cap delete_caller_cap_valid_ep_cap)+
apply (clarsimp)+
apply (clarsimp simp: lookup_failure_map_def)+
apply (clarsimp simp: valid_cap'_def capAligned_def)
apply (rule corres_guard_imp)
apply (rename_tac rights)
apply (case_tac "AllowRead \<in> rights"; simp)
apply (rule_tac r'=ntfn_relation in corres_splitEE)
apply (clarsimp simp: valid_cap'_def capAligned_def)
apply (rule corres_guard_imp)
apply (rename_tac rights)
apply (case_tac "AllowRead \<in> rights"; simp)
apply (rule_tac r'=ntfn_relation in corres_splitEE)
apply clarsimp
apply (rule getNotification_corres)
apply (rule corres_if)
apply (clarsimp simp: ntfn_relation_def)
apply (clarsimp, rule receiveSignal_corres)
prefer 3
apply (rule corres_trivial)
apply (clarsimp simp: lookup_failure_map_def)+
apply (rule getNotification_corres)
apply (wp get_simple_ko_wp getNotification_wp | wpcw | simp)+
apply (clarsimp simp: lookup_failure_map_def)
apply (clarsimp simp: valid_cap_def ct_in_state_def)
apply (clarsimp simp: valid_cap'_def capAligned_def)
apply (wp get_simple_ko_wp | wpcw | simp)+
apply (wp get_simple_ko_wp getNotification_wp | wpcw | simp)+
apply (clarsimp simp: lookup_failure_map_def)
apply (clarsimp simp: valid_cap_def ct_in_state_def)
apply (clarsimp simp: valid_cap'_def capAligned_def)
apply wp+
apply (rule handleFault_corres)
apply simp
apply (wp get_simple_ko_wp | wpcw | simp)+
apply (rule hoare_vcg_E_elim)
apply (simp add: lookup_cap_def lookup_slot_for_thread_def)
apply wp
apply (simp add: split_def)
apply (wp resolve_address_bits_valid_fault2)+
apply (wp getNotification_wp | wpcw | simp add: valid_fault_def whenE_def split del: if_split)+
apply (clarsimp simp add: ct_in_state_def ct_in_state'_def conj_comms invs_valid_tcb_ctable
invs_valid_objs tcb_at_invs invs_psp_aligned invs_cur)
apply (clarsimp simp add: ct_in_state_def ct_in_state'_def conj_comms invs_valid_tcb_ctable
invs_valid_objs tcb_at_invs invs_psp_aligned invs_cur)
apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def
ct_in_state'_def sch_act_sane_not)
done
@ -1996,90 +2004,91 @@ proof -
done
show ?thesis
apply (case_tac event)
apply (simp_all add: handleEvent_def)
apply (simp_all add: handleEvent_def)
apply (rename_tac syscall)
apply (case_tac syscall)
apply (auto intro: corres_guard_imp[OF handleSend_corres]
corres_guard_imp[OF hw]
corres_guard_imp [OF handleReply_corres]
corres_guard_imp[OF handleReply_handleRecv_corres]
corres_guard_imp[OF handleCall_corres]
corres_guard_imp[OF handleYield_corres]
active_from_running active_from_running'
simp: simple_sane_strg)[8]
apply (rename_tac syscall)
apply (case_tac syscall)
apply (auto intro: corres_guard_imp[OF handleSend_corres]
corres_guard_imp[OF hw]
corres_guard_imp [OF handleReply_corres]
corres_guard_imp[OF handleReply_handleRecv_corres]
corres_guard_imp[OF handleCall_corres]
corres_guard_imp[OF handleYield_corres]
active_from_running active_from_running'
simp: simple_sane_strg)[8]
apply (rule corres_underlying_split)
apply (rule corres_guard_imp[OF getCurThread_corres], simp+)
apply (rule handleFault_corres)
apply simp
apply (simp add: valid_fault_def)
apply wp
apply (fastforce elim!: st_tcb_ex_cap st_tcb_weakenE
simp: ct_in_state_def)
apply wp
apply (clarsimp)
apply (frule(1) ct_not_ksQ)
apply (auto simp: ct_in_state'_def sch_act_simple_def
sch_act_sane_def
elim: pred_tcb'_weakenE st_tcb_ex_cap'')[1]
apply (rule corres_underlying_split)
apply (rule corres_guard_imp[OF getCurThread_corres], simp+)
apply (rule corres_guard_imp, rule getCurThread_corres, simp+)
apply (rule handleFault_corres)
apply simp
apply (simp add: valid_fault_def)
apply (simp add: valid_fault_def)
apply wp
apply (fastforce elim!: st_tcb_ex_cap st_tcb_weakenE
simp: ct_in_state_def)
simp: ct_in_state_def valid_fault_def)
apply wp
apply (clarsimp)
apply clarsimp
apply (frule(1) ct_not_ksQ)
apply (auto simp: ct_in_state'_def sch_act_simple_def
sch_act_sane_def
elim: pred_tcb'_weakenE st_tcb_ex_cap'')[1]
apply (rule corres_underlying_split)
apply (rule corres_guard_imp, rule getCurThread_corres, simp+)
apply (rule handleFault_corres)
apply (simp add: valid_fault_def)
apply wp
apply (fastforce elim!: st_tcb_ex_cap st_tcb_weakenE
simp: ct_in_state_def valid_fault_def)
apply wp
apply clarsimp
apply (frule(1) ct_not_ksQ)
apply (auto simp: ct_in_state'_def sch_act_simple_def
sch_act_sane_def
elim: pred_tcb'_weakenE st_tcb_ex_cap'')[1]
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[where R="\<lambda>rv. einvs"
and R'="\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> R'' x s"
for R''])
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[where R="\<lambda>rv. einvs"
and R'="\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> R'' x s"
for R''])
apply (rule corres_machine_op)
apply (rule corres_Id, simp+)
apply wp
apply (case_tac rv, simp_all add: doMachineOp_return)[1]
apply (rule handleInterrupt_corres)
apply (rule corres_machine_op)
apply (rule corres_Id, simp+)
apply (wp hoare_vcg_all_lift
doMachineOp_getActiveIRQ_IRQ_active'
| simp
| simp add: imp_conjR | wp (once) hoare_drop_imps)+
apply force
apply simp
apply (simp add: invs'_def valid_state'_def)
apply (rule_tac corres_underlying_split)
apply (rule corres_guard_imp, rule getCurThread_corres, simp+)
apply (rule corres_split_catch)
apply force
apply simp
apply (simp add: invs'_def valid_state'_def)
apply (rule_tac corres_underlying_split)
apply (rule corres_guard_imp, rule getCurThread_corres, simp+)
apply (rule corres_split_catch)
apply (rule handleVMFault_corres)
apply (erule handleFault_corres)
apply (rule handleVMFault_corres)
apply (rule hoare_elim_pred_conjE2)
apply (rule hoare_vcg_E_conj, rule valid_validE_E, wp)
apply (wp handle_vm_fault_valid_fault)
apply (rule hv_inv_ex')
apply (rule hoare_elim_pred_conjE2)
apply (rule hoare_vcg_E_conj, rule valid_validE_E, wp)
apply (wp handle_vm_fault_valid_fault)
apply (rule hv_inv_ex')
apply wp
apply (clarsimp simp: simple_from_running tcb_at_invs)
apply (fastforce elim!: st_tcb_ex_cap st_tcb_weakenE simp: ct_in_state_def)
apply wp
apply (clarsimp simp: simple_from_running tcb_at_invs)
apply (fastforce elim!: st_tcb_ex_cap st_tcb_weakenE simp: ct_in_state_def)
apply (clarsimp)
apply (frule(1) ct_not_ksQ)
apply (fastforce simp: simple_sane_strg sch_act_simple_def ct_in_state'_def
elim: st_tcb_ex_cap'' pred_tcb'_weakenE)
apply (rule corres_underlying_split)
apply (rule corres_guard_imp[OF getCurThread_corres], simp+)
apply (rule handleHypervisorFault_corres)
apply (simp add: valid_fault_def)
apply wp
apply (fastforce elim!: st_tcb_ex_cap st_tcb_weakenE
simp: ct_in_state_def)
apply wp
apply (clarsimp)
apply (frule(1) ct_not_ksQ)
apply (fastforce simp: simple_sane_strg sch_act_simple_def ct_in_state'_def
elim: st_tcb_ex_cap'' pred_tcb'_weakenE)
apply (rule corres_underlying_split)
apply (rule corres_guard_imp[OF getCurThread_corres], simp+)
apply (rule handleHypervisorFault_corres)
apply (simp add: valid_fault_def)
apply wp
apply (fastforce elim!: st_tcb_ex_cap st_tcb_weakenE
simp: ct_in_state_def)
apply wp
apply (clarsimp)
apply (frule(1) ct_not_ksQ)
apply (auto simp: ct_in_state'_def sch_act_simple_def
sch_act_sane_def
elim: pred_tcb'_weakenE st_tcb_ex_cap'')[1]
apply (auto simp: ct_in_state'_def sch_act_simple_def
sch_act_sane_def
elim: pred_tcb'_weakenE st_tcb_ex_cap'')[1]
done
qed

View File

@ -410,10 +410,10 @@ lemma threadSet_corres_noop_splitT:
apply (rule corres_guard_imp)
apply (subst return_bind[symmetric])
apply (rule corres_split_nor[OF threadSet_corres_noopT])
apply (rule z)
apply (simp add: x)
apply (rule y)
apply (rule e)
apply (simp add: x)
apply (rule y)
apply (rule e)
apply (rule z)
apply (wp w)+
apply simp
apply simp
@ -1345,22 +1345,22 @@ lemma asUser_corres':
show ?thesis
apply (simp add: as_user_def asUser_def)
apply (rule corres_guard_imp)
apply (rule_tac r'="\<lambda>tcb con. (arch_tcb_context_get o tcb_arch) tcb = con" in corres_split_deprecated)
apply (rule corres_split[OF L4])
apply clarsimp
apply (rule corres_split_nor)
apply (rule corres_trivial, simp)
apply (simp add: threadSet_def)
apply (rule corres_symb_exec_r)
prefer 4
apply (rule no_fail_pre_and, wp)
apply (rule L3[simplified])
apply simp
apply simp
apply (wp select_f_inv | simp)+
apply (rule L1[simplified])
apply wp+
apply auto
apply (rule_tac r'="\<lambda>tcb con. (arch_tcb_context_get o tcb_arch) tcb = con"
in corres_split)
apply simp
apply (rule L1[simplified])
apply (rule corres_split)
apply (rule L4; simp)
apply clarsimp
apply (rule corres_split_nor)
apply (simp add: threadSet_def)
apply (rule corres_symb_exec_r)
prefer 4
apply (rule no_fail_pre_and, wp)
apply (rule L3[simplified])
apply simp
apply simp
apply (wp select_f_inv | simp)+
done
qed
@ -1795,21 +1795,27 @@ proof -
apply (rule ready_queues_helper; auto)
apply (clarsimp simp: when_def)
apply (rule stronger_corres_guard_imp)
apply (rule corres_split_deprecated[where r'="(=)", OF _ ethreadget_corres])
apply (rule corres_split_deprecated[where r'="(=)", OF _ ethreadget_corres])
apply (rule corres_split_deprecated[where r'="(=)"])
apply (rule corres_split_noop_rhs2)
apply (rule corres_split_noop_rhs2)
apply (fastforce intro: threadSet_corres_noop simp: tcb_relation_def exst_same_def)
apply (fastforce intro: addToBitmap_noop_corres)
apply wp+
apply (simp add: tcb_sched_enqueue_def split del: if_split)
apply (rule_tac P=\<top> and Q="K (t \<notin> set queuea)" in corres_assume_pre)
apply (wp setQueue_corres[unfolded dc_def] | simp)+
apply (wp getQueue_corres getObject_tcb_wp | simp add: etcb_relation_def threadGet_def)+
apply (fastforce simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_def inQ_def
projectKO_eq project_inject)
done
apply (rule corres_split[where r'="(=)"])
apply (rule ethreadget_corres)
apply (simp add: etcb_relation_def)
apply (rule corres_split[where r'="(=)"])
apply (rule ethreadget_corres)
apply (simp add: etcb_relation_def)
apply (rule corres_split[where r'="(=)"])
apply simp
apply (rule getQueue_corres)
apply (rule corres_split_noop_rhs2)
apply (simp add: tcb_sched_enqueue_def split del: if_split)
apply (rule_tac P=\<top> and Q="K (t \<notin> set queuea)" in corres_assume_pre)
apply simp
apply (rule setQueue_corres[unfolded dc_def])
apply (rule corres_split_noop_rhs2)
apply (fastforce intro: addToBitmap_noop_corres)
apply (fastforce intro: threadSet_corres_noop simp: tcb_relation_def exst_same_def)
apply (wp getObject_tcb_wp | simp add: threadGet_def)+
apply (fastforce simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_def inQ_def
projectKO_eq project_inject)
done
qed
definition
@ -1843,13 +1849,14 @@ lemma rescheduleRequired_corres:
apply (rule corres_guard_imp)
apply (rule corres_split[OF getSchedulerAction_corres])
apply (rule_tac P="case action of switch_thread t \<Rightarrow> P t | _ \<Rightarrow> \<top>"
and P'="case actiona of SwitchToThread t \<Rightarrow> P' t | _ \<Rightarrow> \<top>" for P P' in corres_split_deprecated[where r'=dc])
apply (rule setSchedulerAction_corres)
apply simp
apply (case_tac action)
and P'="case actiona of SwitchToThread t \<Rightarrow> P' t | _ \<Rightarrow> \<top>" for P P'
in corres_split[where r'=dc])
apply (case_tac action)
apply simp
apply simp
apply (rule tcbSchedEnqueue_corres)
apply simp
apply (rule tcbSchedEnqueue_corres)
apply (rule setSchedulerAction_corres)
apply simp
apply (wp | wpc | simp)+
apply (force dest: st_tcb_weakenE simp: in_monad weak_valid_sched_action_def valid_etcbs_def
@ -1996,15 +2003,19 @@ lemma tcbSchedDequeue_corres:
apply (simp add: exec_gets simpler_modify_def get_etcb_def ready_queues_relation_def cong: if_cong get_tcb_queue_def)
apply (simp add: when_def)
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated[where r'="(=)", OF _ ethreadget_corres])
apply (rule corres_split_deprecated[where r'="(=)", OF _ ethreadget_corres])
apply (rule corres_split_deprecated[where r'="(=)"])
apply (rule corres_split_noop_rhs2)
apply (rule corres_split_noop_rhs)
apply (rule threadSet_corres_noop; simp_all add: tcb_relation_def exst_same_def)
apply (clarsimp, rule removeFromBitmap_corres_noop)
apply (rule setQueue_corres | rule getQueue_corres |
wp | simp add: tcb_sched_dequeue_def etcb_relation_def)+
apply (rule corres_split[where r'="(=)"])
apply (rule ethreadget_corres, simp add: etcb_relation_def)
apply (rule corres_split[where r'="(=)"])
apply (rule ethreadget_corres, simp add: etcb_relation_def)
apply (rule corres_split[where r'="(=)"])
apply (simp, rule getQueue_corres)
apply (rule corres_split_noop_rhs2)
apply (simp add: tcb_sched_dequeue_def)
apply (rule setQueue_corres)
apply (rule corres_split_noop_rhs)
apply (clarsimp, rule removeFromBitmap_corres_noop)
apply (rule threadSet_corres_noop; simp_all add: tcb_relation_def exst_same_def)
apply (wp | simp)+
done
lemma thread_get_test: "do cur_ts \<leftarrow> get_thread_state cur; g (test cur_ts) od =
@ -2034,21 +2045,20 @@ lemma setThreadState_corres:
apply (simp add: set_thread_state_ext_def[abs_def])
apply (subst bind_assoc[symmetric], subst thread_set_def[simplified, symmetric])
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated[where r'=dc])
apply simp
apply (subst thread_get_test[where test="runnable"])
apply (rule corres_split[OF thread_get_isRunnable_corres])
apply (rule corres_split[OF getCurThread_corres])
apply (rule corres_split[OF getSchedulerAction_corres])
apply (simp only: when_def)
apply (rule corres_if[where Q=\<top> and Q'=\<top>])
apply (rule iffI)
apply clarsimp+
apply (case_tac rva,simp_all)[1]
apply (wp rescheduleRequired_corres_simple corres_return_trivial | simp)+
apply (rule threadset_corres, (simp add: tcb_relation_def exst_same_def)+)
apply (wp hoare_vcg_conj_lift[where Q'="\<top>\<top>"] | simp add: sch_act_simple_def)+
done
apply (rule corres_split[where r'=dc])
apply (rule threadset_corres, (simp add: tcb_relation_def exst_same_def)+)
apply (subst thread_get_test[where test="runnable"])
apply (rule corres_split[OF thread_get_isRunnable_corres])
apply (rule corres_split[OF getCurThread_corres])
apply (rule corres_split[OF getSchedulerAction_corres])
apply (simp only: when_def)
apply (rule corres_if[where Q=\<top> and Q'=\<top>])
apply (rule iffI)
apply clarsimp+
apply (case_tac rva,simp_all)[1]
apply (wp rescheduleRequired_corres_simple corres_return_trivial | simp)+
apply (wp hoare_vcg_conj_lift[where Q'="\<top>\<top>"] | simp add: sch_act_simple_def)+
done
lemma setBoundNotification_corres:
"corres dc
@ -3157,21 +3167,22 @@ lemma storeWordUser_corres:
apply (rule corres_guard2_imp)
apply (rule_tac F = "is_aligned a msg_align_bits" in corres_gen_asm2)
apply (rule corres_guard1_imp)
apply (rule_tac r'=dc in corres_split_deprecated)
apply (rule corres_machine_op)
apply (rule corres_Id [OF refl])
apply simp
apply (rule no_fail_pre)
apply (wp no_fail_storeWord)
apply (erule_tac n=msg_align_bits in aligned_add_aligned)
apply (rule is_aligned_mult_triv2 [where n = 2, simplified])
apply (simp add: word_bits_conv msg_align_bits)+
apply (simp add: stateAssert_def)
apply (rule_tac r'=dc in corres_split_deprecated)
apply (rule_tac r'=dc in corres_split)
apply (simp add: stateAssert_def)
apply (rule_tac r'=dc in corres_split)
apply (rule corres_trivial)
apply simp
apply (rule corres_assert)
apply (rule corres_trivial)
apply simp
apply wp+
apply wp+
apply (rule corres_machine_op)
apply (rule corres_Id [OF refl])
apply simp
apply (rule no_fail_pre)
apply (wp no_fail_storeWord)
apply (erule_tac n=msg_align_bits in aligned_add_aligned)
apply (rule is_aligned_mult_triv2 [where n = 2, simplified])
apply (simp add: word_bits_conv msg_align_bits)+
apply wp+
apply (simp add: in_user_frame_eq[OF y])
apply simp
apply (rule conjI)
@ -3226,7 +3237,7 @@ lemma getMRs_corres:
apply (case_tac mi, simp add: get_mrs_def getMRs_def split del: if_split)
apply (case_tac buf)
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated [where R = "\<lambda>_. \<top>" and R' = "\<lambda>_. \<top>", OF _ T])
apply (rule corres_split [where R = "\<lambda>_. \<top>" and R' = "\<lambda>_. \<top>", OF T])
apply simp
apply wp+
apply simp
@ -3236,21 +3247,21 @@ lemma getMRs_corres:
apply (simp only: option.simps return_bind fun_app_def
load_word_offs_def doMachineOp_mapM ef_loadWord)
apply (rule corres_split_eqr)
apply (rule corres_trivial, simp)
apply (simp only: mapM_map_simp msgMaxLength_def msgLengthBits_def
msg_max_length_def o_def upto_enum_word)
apply (rule corres_mapM [where r'="(=)" and S="{a. fst a = snd a \<and> fst a < unat max_ipc_words}"])
apply (simp only: mapM_map_simp msgMaxLength_def msgLengthBits_def
msg_max_length_def o_def upto_enum_word)
apply (rule corres_mapM [where r'="(=)" and S="{a. fst a = snd a \<and> fst a < unat max_ipc_words}"])
apply simp
apply simp
apply (simp add: word_size wordSize_def wordBits_def)
apply (rule loadWordUser_corres)
apply simp
apply (simp add: word_size wordSize_def wordBits_def)
apply (rule loadWordUser_corres)
apply simp
apply wp+
apply simp
apply (unfold msgRegisters_unfold)[1]
apply simp
apply (clarsimp simp: set_zip)
apply (simp add: msgRegisters_unfold max_ipc_words nth_append)
apply wp+
apply simp
apply (unfold msgRegisters_unfold)[1]
apply simp
apply (clarsimp simp: set_zip)
apply (simp add: msgRegisters_unfold max_ipc_words nth_append)
apply (rule corres_trivial, simp)
apply (wp hoare_vcg_all_lift | simp add: valid_ipc_buffer_ptr'_def)+
done
qed
@ -3326,11 +3337,11 @@ proof -
apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_Nil zipWithM_x_modify
take_min_len zip_take_triv2 min.commute)
apply (rule corres_guard_imp)
apply (rule corres_split_nor[OF asUser_corres'], rule corres_trivial, simp)
apply (rule corres_modify')
apply (fastforce simp: fold_fun_upd[symmetric] msgRegisters_unfold
cong: if_cong simp del: the_index.simps)
apply ((wp |simp)+)[5]
apply (rule corres_split_nor[OF asUser_corres'])
apply (rule corres_modify')
apply (fastforce simp: fold_fun_upd[symmetric] msgRegisters_unfold
cong: if_cong simp del: the_index.simps)
apply ((wp |simp)+)[6]
\<comment> \<open>buf = Some a\<close>
using if_split[split del]
apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_Nil zipWithM_x_modify
@ -3339,21 +3350,23 @@ proof -
apply (simp add: msg_max_length_def)
apply (rule corres_guard_imp)
apply (rule corres_split_nor[OF asUser_corres'])
apply (rule corres_split_nor, rule corres_trivial, clarsimp simp: min.commute)
apply (rule_tac S="{((x, y), (x', y')). y = y' \<and> x' = (a + (of_nat x * 4)) \<and> x < unat max_ipc_words}"
in zipWithM_x_corres)
apply (fastforce intro: storeWordUser_corres)
apply wp+
apply (clarsimp simp add: S msgMaxLength_def msg_max_length_def set_zip)
apply (simp add: wordSize_def wordBits_def word_size max_ipc_words
upt_Suc_append[symmetric] upto_enum_word)
apply simp
apply wp+
apply (rule corres_modify')
apply (simp only: msgRegisters_unfold cong: if_cong)
apply (fastforce simp: fold_fun_upd[symmetric])
apply (wp | clarsimp simp: valid_ipc_buffer_ptr'_def)+
done
apply clarsimp
apply (rule corres_split_nor)
apply (rule_tac S="{((x, y), (x', y')). y = y' \<and> x' = (a + (of_nat x * 4)) \<and> x < unat max_ipc_words}"
in zipWithM_x_corres)
apply (fastforce intro: storeWordUser_corres)
apply wp+
apply (clarsimp simp add: S msgMaxLength_def msg_max_length_def set_zip)
apply (simp add: wordSize_def wordBits_def word_size max_ipc_words
upt_Suc_append[symmetric] upto_enum_word)
apply simp
apply (rule corres_trivial, clarsimp simp: min.commute)
apply wp+
apply (wp | clarsimp simp: valid_ipc_buffer_ptr'_def)+
done
qed
lemma copyMRs_corres:
@ -3419,23 +3432,24 @@ proof -
apply (rename_tac sb_ptr rb_ptr)
apply (rule corres_split_nor[OF as_user_bit])
apply (rule corres_split_eqr)
apply (rule corres_trivial, simp)
apply (rule_tac S="{(x, y). y = of_nat x \<and> x < unat max_ipc_words}" in corres_mapM, simp+)
apply (rule corres_split_eqr)
apply (rule storeWordUser_corres)
apply simp
apply (rule loadWordUser_corres)
apply simp
apply (wp hoare_vcg_all_lift | simp)+
apply (clarsimp simp: upto_enum_def)
apply arith
apply (subst set_zip)
apply (simp add: upto_enum_def U del: upt.simps)
apply (clarsimp simp del: upt.simps)
apply (clarsimp simp: msg_max_length_def word_le_nat_alt nth_append
max_ipc_words)
apply (erule order_less_trans)
apply simp
apply (rule_tac S="{(x, y). y = of_nat x \<and> x < unat max_ipc_words}"
in corres_mapM, simp+)
apply (rule corres_split_eqr)
apply (rule loadWordUser_corres)
apply simp
apply (rule storeWordUser_corres)
apply simp
apply (wp hoare_vcg_all_lift | simp)+
apply (clarsimp simp: upto_enum_def)
apply arith
apply (subst set_zip)
apply (simp add: upto_enum_def U del: upt.simps)
apply (clarsimp simp del: upt.simps)
apply (clarsimp simp: msg_max_length_def word_le_nat_alt nth_append
max_ipc_words)
apply (erule order_less_trans)
apply simp
apply (rule corres_trivial, simp)
apply (wp hoare_vcg_all_lift mapM_wp'
| simp add: valid_ipc_buffer_ptr'_def)+
done
@ -3522,39 +3536,39 @@ lemma lookupIPCBuffer_corres':
apply (simp add: lookup_ipc_buffer_def ARM_H.lookupIPCBuffer_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[OF threadGet_corres])
apply (simp add: getThreadBufferSlot_def locateSlot_conv)
apply (rule corres_split[OF getSlotCap_corres])
apply (rule_tac F="valid_ipc_buffer_cap rv buffer_ptr"
in corres_gen_asm)
apply (rule_tac P="valid_cap rv" and Q="no_0_obj'"
in corres_assume_pre)
apply (simp add: Let_def split: cap.split arch_cap.split
split del: if_split cong: if_cong)
apply (safe, simp_all add: isCap_simps valid_ipc_buffer_cap_simps split:bool.split_asm)[1]
apply (rename_tac word rights vmpage_size option)
apply (subgoal_tac "word + (buffer_ptr &&
mask (pageBitsForSize vmpage_size)) \<noteq> 0")
apply (simp add: cap_aligned_def
valid_ipc_buffer_cap_def
vmrights_map_def vm_read_only_def vm_read_write_def)
apply auto[1]
apply (subgoal_tac "word \<noteq> 0")
apply (subgoal_tac "word \<le> word + (buffer_ptr &&
mask (pageBitsForSize vmpage_size))")
apply fastforce
apply (rule_tac b="2 ^ (pageBitsForSize vmpage_size) - 1"
in word_plus_mono_right2)
apply (clarsimp simp: valid_cap_def cap_aligned_def
intro!: is_aligned_no_overflow')
apply (clarsimp simp: word_bits_def
intro!: word_less_sub_1 and_mask_less')
apply (case_tac vmpage_size, simp_all)[1]
apply (drule state_relation_pspace_relation)
apply (clarsimp simp: valid_cap_def obj_at_def no_0_obj_kheap
obj_relation_cuts_def3 no_0_obj'_def split:if_split_asm)
apply (simp add: tcb_relation_def)
apply (simp add: getThreadBufferSlot_def locateSlot_conv)
apply (rule corres_split[OF getSlotCap_corres])
apply (simp add: cte_map_def tcb_cnode_index_def cte_level_bits_def tcbIPCBufferSlot_def)
apply (wp get_cap_valid_ipc get_cap_aligned)+
apply (simp add: tcb_relation_def)
apply (rule_tac F="valid_ipc_buffer_cap rv buffer_ptr"
in corres_gen_asm)
apply (rule_tac P="valid_cap rv" and Q="no_0_obj'"
in corres_assume_pre)
apply (simp add: Let_def split: cap.split arch_cap.split
split del: if_split cong: if_cong)
apply (safe, simp_all add: isCap_simps valid_ipc_buffer_cap_simps split:bool.split_asm)[1]
apply (rename_tac word rights vmpage_size option)
apply (subgoal_tac "word + (buffer_ptr &&
mask (pageBitsForSize vmpage_size)) \<noteq> 0")
apply (simp add: cap_aligned_def
valid_ipc_buffer_cap_def
vmrights_map_def vm_read_only_def vm_read_write_def)
apply auto[1]
apply (subgoal_tac "word \<noteq> 0")
apply (subgoal_tac "word \<le> word + (buffer_ptr &&
mask (pageBitsForSize vmpage_size))")
apply fastforce
apply (rule_tac b="2 ^ (pageBitsForSize vmpage_size) - 1"
in word_plus_mono_right2)
apply (clarsimp simp: valid_cap_def cap_aligned_def
intro!: is_aligned_no_overflow')
apply (clarsimp simp: word_bits_def
intro!: word_less_sub_1 and_mask_less')
apply (case_tac vmpage_size, simp_all)[1]
apply (drule state_relation_pspace_relation)
apply (clarsimp simp: valid_cap_def obj_at_def no_0_obj_kheap
obj_relation_cuts_def3 no_0_obj'_def split:if_split_asm)
apply (wp get_cap_valid_ipc get_cap_aligned)+
apply (wp thread_get_obj_at_eq)+
apply (clarsimp elim!: tcb_at_cte_at)
apply clarsimp
@ -4385,11 +4399,10 @@ lemma get_cap_corres_all_rights_P:
apply (subst bind_return [symmetric])
apply (rule corres_guard_imp)
apply (rule corres_split[OF get_cap_corres_P [where P=P]])
defer
apply (wp getCTE_wp')+
apply simp
apply fastforce
apply (insert cap_relation_masks, simp)
apply (insert cap_relation_masks, simp)
apply (wp getCTE_wp')+
apply simp
apply fastforce
done
lemma asUser_irq_handlers':

View File

@ -68,8 +68,8 @@ lemma bindNotification_corres:
apply (rule corres_guard_imp)
apply (rule corres_split[OF getNotification_corres])
apply (rule corres_split[OF setNotification_corres])
apply (rule setBoundNotification_corres)
apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits)
apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits)
apply (rule setBoundNotification_corres)
apply (wp)+
apply auto
done
@ -213,8 +213,10 @@ lemma restart_corres:
apply (rule corres_split_nor[OF cancel_ipc_corres])
apply (rule corres_split_nor[OF setupReplyMaster_corres])
apply (rule corres_split_nor[OF setThreadState_corres])
apply (rule corres_split[OF tcbSchedEnqueue_corres possibleSwitchTo_corres])
apply (wp set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at' sts_valid_queues sts_st_tcb' | clarsimp simp: valid_tcb_state'_def)+
apply clarsimp
apply (rule corres_split[OF tcbSchedEnqueue_corres possibleSwitchTo_corres])
apply (wp set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at' sts_valid_queues sts_st_tcb'
| clarsimp simp: valid_tcb_state'_def)+
apply (rule_tac Q="\<lambda>rv. valid_sched and cur_tcb" in hoare_strengthen_post)
apply wp
apply (simp add: valid_sched_def valid_sched_action_def)
@ -226,7 +228,6 @@ lemma restart_corres:
apply (clarsimp simp add: invs'_def valid_state'_def sch_act_wf_weak)
done
lemma restart_invs':
"\<lbrace>invs' and ex_nonz_cap_to' t and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace>
ThreadDecls_H.restart t \<lbrace>\<lambda>rv. invs'\<rbrace>"
@ -289,18 +290,17 @@ lemma invokeTCB_ReadRegisters_corres:
frameRegisters_def gpRegisters_def)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (rule corres_split[OF getCurThread_corres])
apply (simp add: liftM_def[symmetric])
apply (rule asUser_corres)
apply (rule corres_Id)
apply simp
apply (rule corres_when[OF refl])
apply (rule suspend_corres)
apply (rule corres_split[OF getCurThread_corres])
apply (simp add: liftM_def[symmetric])
apply (rule asUser_corres)
apply (rule corres_Id)
apply simp
apply (rule no_fail_mapM)
apply (simp add: no_fail_getRegister)
apply wp+
apply (rule corres_when [OF refl])
apply (rule suspend_corres)
apply wp+
apply simp
apply (rule no_fail_mapM)
apply (simp add: no_fail_getRegister)
apply wp+
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def
dest!: idle_no_ex_cap)
apply (clarsimp simp: invs'_def valid_state'_def dest!: global'_no_ex_cap)
@ -406,12 +406,12 @@ proof -
apply clarsimp
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule asUser_getRegister_corres)
apply (simp add: setRegister_def)
apply (rule asUser_corres)
apply (rule corres_modify')
apply simp
apply simp
apply (rule asUser_getRegister_corres)
apply (simp | wp)+
done
have R: "\<And>src src' des des' xs ys. \<lbrakk> src = src'; des = des'; xs = ys \<rbrakk> \<Longrightarrow>
@ -443,36 +443,37 @@ proof -
apply (rule corres_split[OF corres_when [OF refl suspend_corres]], simp)
apply (rule corres_split[OF corres_when [OF refl restart_corres]], simp)
apply (rule corres_split_nor)
apply (rule corres_when[OF refl])
apply (rule corres_split_nor)
apply (rule corres_split_eqr[OF getCurThread_corres])
apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
apply (rule corres_split[OF corres_when[OF refl rescheduleRequired_corres]])
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
apply simp
apply (wp static_imp_wp)+
apply (rule R[OF refl refl])
apply (simp add: frame_registers_def frameRegisters_def)
apply (simp add: getRestartPC_def setNextPC_def dc_def[symmetric])
apply (rule Q[OF refl refl])
apply ((wp mapM_x_wp' static_imp_wp | simp)+)[2]
apply (rule corres_split_nor)
apply (rule corres_when[OF refl])
apply (rule R[OF refl refl])
apply (simp add: gpRegisters_def)
apply (rule_tac Q="\<lambda>_. einvs and tcb_at dest" in hoare_strengthen_post[rotated])
apply (clarsimp simp: invs_def valid_sched_weak_strg valid_sched_def)
prefer 2
apply (rule_tac Q="\<lambda>_. invs' and tcb_at' dest" in hoare_strengthen_post[rotated])
apply (clarsimp simp: invs'_def valid_state'_def invs_weak_sch_act_wf)
apply (wp mapM_x_wp' | simp)+
apply (rule corres_when[OF refl])
apply (rule corres_split_nor)
apply (simp add: getRestartPC_def setNextPC_def dc_def[symmetric])
apply (rule Q[OF refl refl])
apply (rule R[OF refl refl])
apply (simp add: frame_registers_def frameRegisters_def)
apply (rule corres_split_eqr[OF getCurThread_corres])
apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
apply (rule corres_split[OF corres_when[OF refl rescheduleRequired_corres]])
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
apply simp
apply ((wp static_imp_wp)+)[6]
apply (rule_tac Q="\<lambda>_. einvs and tcb_at dest" in hoare_strengthen_post[rotated])
apply (clarsimp simp: invs_def valid_sched_weak_strg valid_sched_def)
prefer 2
apply (rule_tac Q="\<lambda>_. invs' and tcb_at' dest" in hoare_strengthen_post[rotated])
apply (clarsimp simp: invs'_def valid_state'_def invs_weak_sch_act_wf)
apply ((wp mapM_x_wp' static_imp_wp | simp)+)[2]
apply (wp mapM_x_wp' static_imp_wp | simp)+
apply ((wp static_imp_wp restart_invs' | wpc | clarsimp simp add: if_apply_def2)+)[2]
apply ((wp mapM_x_wp' static_imp_wp | simp)+)[1]
apply (wp mapM_x_wp' static_imp_wp | simp)+
apply ((wp mapM_x_wp' static_imp_wp restart_invs' | wpc | clarsimp simp add: if_apply_def2)+)[2]
apply (wp suspend_nonz_cap_to_tcb static_imp_wp | simp add: if_apply_def2)+
apply (fastforce simp: invs_def valid_state_def valid_pspace_def
dest!: idle_no_ex_cap)
apply (fastforce simp: invs'_def valid_state'_def dest!: global'_no_ex_cap)
done
done
qed
lemma readreg_invs':
@ -635,15 +636,16 @@ lemma sp_corres2:
apply (rule stronger_corres_guard_imp)
apply (rule corres_split[OF tcbSchedDequeue_corres])
apply (rule corres_split[OF ethread_set_corres], simp_all)[1]
apply (rule corres_split[OF isRunnable_corres])
apply (erule corres_when)
apply(rule corres_split[OF getCurThread_corres])
apply (wp corres_if; clarsimp)
apply (rule rescheduleRequired_corres)
apply (rule possibleSwitchTo_corres)
apply ((clarsimp
| wp static_imp_wp hoare_vcg_if_lift hoare_wp_combs gts_wp isRunnable_wp
| simp add: etcb_relation_def)+)[5]
apply (simp add: etcb_relation_def)
apply (rule corres_split[OF isRunnable_corres])
apply (erule corres_when)
apply(rule corres_split[OF getCurThread_corres])
apply (wp corres_if; clarsimp)
apply (rule rescheduleRequired_corres)
apply (rule possibleSwitchTo_corres)
apply ((clarsimp
| wp static_imp_wp hoare_vcg_if_lift hoare_wp_combs gts_wp
isRunnable_wp)+)[4]
apply (wp hoare_vcg_imp_lift' hoare_vcg_if_lift hoare_vcg_all_lift)
apply clarsimp
apply ((wp hoare_drop_imps hoare_vcg_if_lift hoare_vcg_all_lift
@ -1452,20 +1454,19 @@ proof -
apply (case_tac b, simp_all add: newroot_rel_def)
apply (rule corres_guard_imp)
apply (rule corres_split_norE)
apply (rule_tac F="is_aligned aa msg_align_bits" in corres_gen_asm2)
apply (rule corres_split_nor)
apply (rule corres_split[OF getCurThread_corres], clarsimp)
apply (rule corres_when[OF refl rescheduleRequired_corres])
apply (wpsimp wp: gct_wp)+
apply (rule cteDelete_corres)
apply (rule_tac F="is_aligned aa msg_align_bits" in corres_gen_asm2)
apply (rule corres_split_nor)
apply (rule threadset_corres,
(simp add: tcb_relation_def), (simp add: exst_same_def)+)[1]
apply (wp hoare_drop_imp)
apply (rule threadcontrol_corres_helper1[unfolded pred_conj_def])
apply simp
apply (rule corres_split[OF getCurThread_corres], clarsimp)
apply (rule corres_when[OF refl rescheduleRequired_corres])
apply (wpsimp wp: gct_wp)+
apply (wp hoare_drop_imp)
apply (wp threadcontrol_corres_helper2 | wpc | simp)+
apply (rule cteDelete_corres)
apply wp
apply (rule threadcontrol_corres_helper1[unfolded pred_conj_def])
apply simp
apply (wp hoare_drop_imp)
apply (wp threadcontrol_corres_helper2 | wpc | simp)+
apply (wpsimp wp: cteDelete_invs' hoare_vcg_conj_lift)
apply (fastforce simp: emptyable_def)
apply fastforce
@ -1475,15 +1476,15 @@ proof -
apply (rule_tac F="is_aligned aa msg_align_bits" in corres_gen_asm)
apply (rule_tac F="isArchObjectCap ac" in corres_gen_asm2)
apply (rule corres_split_nor)
apply (rule corres_split_nor)
apply (rule corres_split[OF getCurThread_corres], clarsimp)
apply (rule corres_when[OF refl rescheduleRequired_corres])
apply (wp gct_wp)+
apply (rule threadset_corres,
simp add: tcb_relation_def, (simp add: exst_same_def)+)
apply (rule corres_split_nor)
apply (erule checkCapAt_cteInsert_corres)
apply (wp hoare_drop_imp threadcontrol_corres_helper3)[1]
apply (wp hoare_drop_imp threadcontrol_corres_helper4)[1]
apply (rule threadset_corres,
simp add: tcb_relation_def, (simp add: exst_same_def)+)
apply (rule corres_split[OF getCurThread_corres], clarsimp)
apply (rule corres_when[OF refl rescheduleRequired_corres])
apply (wp gct_wp)+
apply (wp hoare_drop_imp threadcontrol_corres_helper3)[1]
apply (wp hoare_drop_imp threadcontrol_corres_helper4)[1]
apply (wp thread_set_tcb_ipc_buffer_cap_cleared_invs
thread_set_cte_wp_at_trivial thread_set_not_state_valid_sched
| simp add: ran_tcb_cap_cases)+
@ -1558,11 +1559,11 @@ proof -
apply (rule corres_split_norE[OF T [OF x U], simplified])
apply (rule corres_split_norE[OF T [OF y V], simplified])
apply (rule corres_split_norE)
apply (rule corres_split_nor[OF S, simplified])
apply (rule corres_returnOkTT, simp)
apply wp
apply (rule T2[simplified])
apply (rule corres_split_nor[OF S, simplified])
apply (rule corres_returnOkTT, simp)
apply wp
apply (rule T2[simplified])
apply wp
apply (wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_const_imp_lift
hoare_vcg_all_lift_R hoare_vcg_all_lift as_user_invs cap_delete_deletes
thread_set_ipc_tcb_cap_valid thread_set_tcb_ipc_buffer_cap_cleared_invs
@ -1862,9 +1863,9 @@ lemma invokeTCB_corres:
apply (rule corres_split[OF TcbAcc_R.asUser_setRegister_corres])
apply (rule corres_split[OF Bits_R.getCurThread_corres])
apply (rule corres_split[OF Corres_UL.corres_when])
apply (rule corres_trivial, simp)
apply simp
apply (rule TcbAcc_R.rescheduleRequired_corres)
apply simp
apply (rule TcbAcc_R.rescheduleRequired_corres)
apply (rule corres_trivial, simp)
apply (wpsimp wp: hoare_drop_imp)+
apply (clarsimp simp: valid_sched_weak_strg einvs_valid_etcbs)
apply (clarsimp simp: Tcb_R.invs_valid_queues' Invariants_H.invs_queues)
@ -2070,16 +2071,16 @@ lemma checkPrio_corres:
apply (simp add: check_prio_def checkPrio_def)
apply (rule corres_guard_imp)
apply (simp add: liftE_bindE)
apply (rule corres_split[OF threadGet_corres])
apply (rule_tac rvr = dc and
R = \<top> and
R' = \<top> in
whenE_throwError_corres'[where m="returnOk ()" and m'="returnOk ()", simplified])
apply (simp add: minPriority_def)
apply (clarsimp simp: minPriority_def)
apply (rule corres_returnOkTT)
apply (simp add: minPriority_def)
apply (simp add: tcb_relation_def)
apply (rule corres_split[OF threadGet_corres[where r="(=)"]])
apply (clarsimp simp: tcb_relation_def)
apply (rule_tac rvr = dc and
R = \<top> and
R' = \<top> in
whenE_throwError_corres'[where m="returnOk ()" and m'="returnOk ()", simplified])
apply (simp add: minPriority_def)
apply (clarsimp simp: minPriority_def)
apply (rule corres_returnOkTT)
apply (simp add: minPriority_def)
apply (wp gct_wp)+
apply (simp add: cur_tcb_def cur_tcb'_def)+
done
@ -2096,11 +2097,11 @@ lemma decodeSetPriority_corres:
clarsimp simp: decode_set_priority_def decodeSetPriority_def)
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
apply (rule corres_split_eqrE)
apply (rule corres_splitEE[OF checkPrio_corres])
apply (rule corres_returnOkTT)
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
apply wpsimp+
apply (corressimp simp: valid_cap_def valid_cap'_def)+
apply corressimp
apply (rule corres_splitEE[OF checkPrio_corres])
apply (rule corres_returnOkTT)
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
apply (wpsimp simp: valid_cap_def valid_cap'_def)+
done
lemma decodeSetMCPriority_corres:
@ -2115,11 +2116,11 @@ lemma decodeSetMCPriority_corres:
clarsimp simp: decode_set_mcpriority_def decodeSetMCPriority_def)
apply (rename_tac auth_cap auth_slot auth_path rest auth_cap' rest')
apply (rule corres_split_eqrE)
apply (rule corres_splitEE[OF checkPrio_corres])
apply (rule corres_returnOkTT)
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
apply wpsimp+
apply (corressimp simp: valid_cap_def valid_cap'_def)+
apply corressimp
apply (rule corres_splitEE[OF checkPrio_corres])
apply (rule corres_returnOkTT)
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
apply (wpsimp simp: valid_cap_def valid_cap'_def)+
done
lemma getMCP_sp:
@ -2226,12 +2227,13 @@ lemma decodeSetSchedParams_corres:
apply (clarsimp split: list.split simp: list_all2_Cons2)
apply (clarsimp simp: list_all2_Cons1 neq_Nil_conv val_le_length_Cons linorder_not_less)
apply (rule corres_split_eqrE)
apply (rule corres_split_norE[OF checkPrio_corres])
apply (rule corres_splitEE[OF checkPrio_corres])
apply (rule corres_returnOkTT)
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
apply (wpsimp wp: check_prio_inv checkPrio_inv)+
apply (corressimp simp: valid_cap_def valid_cap'_def)+
apply corressimp
apply (rule corres_split_norE[OF checkPrio_corres])
apply (rule corres_splitEE[OF checkPrio_corres])
apply (rule corres_returnOkTT)
apply (clarsimp simp: newroot_rel_def elim!: is_thread_cap.elims(2))
apply (wpsimp wp: check_prio_inv checkPrio_inv
simp: valid_cap_def valid_cap'_def)+
done
lemma checkValidIPCBuffer_corres:
@ -2287,7 +2289,8 @@ lemma decodeSetIPCBuffer_corres:
split del: if_split)
apply (clarsimp simp add: returnOk_def newroot_rel_def)
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF deriveCap_corres])
apply (rule corres_splitEE)
apply (rule deriveCap_corres; simp)
apply (simp add: o_def newroot_rel_def split_def dc_def[symmetric])
apply (erule checkValidIPCBuffer_corres)
apply (wp hoareE_TrueI | simp)+
@ -2372,55 +2375,56 @@ lemma decodeSetSpace_corres:
apply (cases "3 \<le> length args \<and> 2 \<le> length extras'")
apply (clarsimp simp: val_le_length_Cons list_all2_Cons2
split del: if_split)
apply (simp add: liftE_bindE liftM_def
apply (simp add: liftE_bindE liftM_def unlessE_whenE
getThreadCSpaceRoot getThreadVSpaceRoot
split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split[OF slotCapLongRunningDelete_corres])
apply (rule corres_split[OF slotCapLongRunningDelete_corres])
apply (rule corres_split_norE)
apply (simp(no_asm) add: split_def unlessE_throwError_returnOk
bindE_assoc cap_CNode_case_throw
split del: if_split)
apply (rule corres_splitEE[OF deriveCap_corres])
apply (rule corres_split_norE)
apply (rule corres_splitEE[OF deriveCap_corres])
apply (rule corres_split_norE)
apply (rule corres_trivial)
apply (clarsimp simp: returnOk_def newroot_rel_def is_cap_simps
list_all2_conv_all_nth split_def)
apply (unfold unlessE_whenE)
apply (rule corres_whenE)
apply (case_tac vroot_cap', simp_all add:
is_valid_vtable_root_def isValidVTableRoot_def
ARM_H.isValidVTableRoot_def)[1]
apply (rename_tac arch_cap)
apply (clarsimp, case_tac arch_cap, simp_all)[1]
apply (simp split: option.split)
apply (rule corres_trivial, simp)
apply simp
apply wp+
apply (clarsimp simp: cap_map_update_data)
apply simp
apply ((simp only: simp_thms pred_conj_def | wp)+)[2]
apply (clarsimp simp: is_cap_simps get_tcb_ctable_ptr_def cte_map_tcb_0)
apply (rule corres_split[OF slotCapLongRunningDelete_corres])
apply (clarsimp simp: is_cap_simps get_tcb_vtable_ptr_def cte_map_tcb_1[simplified] objBits_defs)
apply (rule corres_split_norE)
apply (rule corres_whenE)
apply simp
apply (rule corres_trivial, simp)
apply simp
apply (simp(no_asm) add: split_def unlessE_throwError_returnOk
bindE_assoc cap_CNode_case_throw unlessE_whenE
split del: if_split)
apply (rule corres_splitEE)
apply (rule deriveCap_corres)
apply (clarsimp simp: cap_map_update_data)
apply simp
apply (rule corres_split_norE)
apply (rule corres_whenE)
apply simp
apply (rule corres_trivial, simp)
apply simp
apply (rule corres_splitEE)
apply (rule deriveCap_corres)
apply (fastforce dest: list_all2_nthD2[where p=0] simp: cap_map_update_data)
apply simp
apply (rule corres_split_norE)
apply (unfold unlessE_whenE)
apply (rule corres_whenE)
apply simp
apply (case_tac vroot_cap', simp_all add:
is_valid_vtable_root_def isValidVTableRoot_def
ARM_H.isValidVTableRoot_def)[1]
apply (rename_tac arch_cap)
apply (clarsimp, case_tac arch_cap, simp_all)[1]
apply (simp split: option.split)
apply (rule corres_trivial, simp)
apply simp
apply (unfold whenE_def, wp+)[2]
apply (fastforce dest: list_all2_nthD2[where p=0] simp: cap_map_update_data)
apply (fastforce dest: list_all2_nthD2[where p=0])
apply ((simp split del: if_split | wp | rule hoare_drop_imps)+)[2]
apply (rule corres_whenE)
apply simp
apply (rule corres_trivial, simp)
apply simp
apply (unfold whenE_def, wp+)[2]
apply (clarsimp simp: is_cap_simps get_tcb_vtable_ptr_def cte_map_tcb_1[simplified] objBits_defs)
apply simp
apply (wp hoare_drop_imps)+
apply (clarsimp simp: is_cap_simps get_tcb_ctable_ptr_def cte_map_tcb_0)
apply wp+
apply (rule corres_trivial)
apply (clarsimp simp: returnOk_def newroot_rel_def is_cap_simps
list_all2_conv_all_nth split_def)
apply wp+
apply ((simp only: simp_thms pred_conj_def | wp)+)[2]
apply (unfold whenE_def, wp+)[2]
apply ((simp split del: if_split | wp | rule hoare_drop_imps)+)[2]
apply (unfold whenE_def, wp+)[2]
apply simp
apply (wp hoare_drop_imps)+
apply (clarsimp simp: get_tcb_ctable_ptr_def get_tcb_vtable_ptr_def
is_cap_simps valid_cap_def tcb_at_cte_at_0
tcb_at_cte_at_1[simplified])
@ -2511,14 +2515,16 @@ lemma decodeTCBConfigure_corres:
apply (clarsimp simp: linorder_not_less val_le_length_Cons list_all2_Cons1
priorityBits_def)
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF decodeSetIPCBuffer_corres])
apply (rule corres_splitEE[OF decodeSetSpace_corres])
apply (rule_tac F="is_thread_control set_params" in corres_gen_asm)
apply (rule_tac F="is_thread_control set_space" in corres_gen_asm)
apply (rule_tac F="tcThreadCapSlot setSpace = cte_map slot" in corres_gen_asm2)
apply (rule corres_trivial)
apply (clarsimp simp: returnOk_def is_thread_control_def2 is_cap_simps)
apply (wp | simp add: invs_def valid_sched_def)+
apply (rule corres_splitEE)
apply (rule decodeSetIPCBuffer_corres; simp)
apply (rule corres_splitEE)
apply (rule decodeSetSpace_corres; simp)
apply (rule_tac F="is_thread_control set_params" in corres_gen_asm)
apply (rule_tac F="is_thread_control set_space" in corres_gen_asm)
apply (rule_tac F="tcThreadCapSlot setSpace = cte_map slot" in corres_gen_asm2)
apply (rule corres_trivial)
apply (clarsimp simp: returnOk_def is_thread_control_def2 is_cap_simps)
apply (wp | simp add: invs_def valid_sched_def)+
done
lemma isThreadControl_def2:
@ -2568,15 +2574,14 @@ lemma tcb_real_cte_16:
by (clarsimp simp: obj_at'_def projectKOs objBitsKO_def ps_clear_16)
lemma corres_splitEE':
assumes x: "corres_underlying sr nf nf' (f \<oplus> r') P P' a c"
assumes y: "\<And>x y x' y'. r' (x, y) (x', y')
\<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (R x y) (R' x' y') (b x y) (d x' y')"
assumes "corres_underlying sr nf nf' (f \<oplus> r') P P' a c"
assumes x: "\<lbrace>Q\<rbrace> a \<lbrace>%(x, y). R x y \<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>%(x, y). R' x y\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>"
assumes z: "\<lbrace>Q\<rbrace> a \<lbrace>%(x, y). R x y \<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>%(x, y). R' x y\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>"
shows "corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a >>=E (\<lambda>(x, y). b x y)) (c >>=E (\<lambda>(x, y). d x y))"
using assms
apply (unfold bindE_def validE_def split_def)
apply (rule corres_split_deprecated)
defer
apply (rule corres_split[rotated 2])
apply assumption+
apply (case_tac rv)
apply (clarsimp simp: lift_def y)+
@ -2594,33 +2599,32 @@ notes if_cong[cong] shows
apply (simp add: null_def returnOk_def)
apply (rule corres_guard_imp)
apply (rule corres_split_norE)
apply (rule_tac F="extras \<noteq> []" in corres_gen_asm)
apply (rule corres_split_eqrE)
apply (rule corres_split_norE)
apply (rule corres_splitEE'[where r'="\<lambda>rv rv'. ((fst rv) = (fst rv')) \<and> ((snd rv') = (AllowRead \<in> (snd rv)))"])
apply (rule corres_split_norE)
apply (clarsimp split del: if_split)
apply (rule corres_splitEE[where r'=ntfn_relation])
apply (rule corres_trivial, simp split del: if_split)
apply (simp add: ntfn_relation_def
split: Structures_A.ntfn.splits Structures_H.ntfn.splits
option.splits)
apply simp
apply (rule getNotification_corres)
apply wp+
apply (rule corres_trivial, clarsimp simp: whenE_def returnOk_def)
apply (wp | simp add: whenE_def split del: if_split)+
apply (rule corres_trivial, simp)
apply (case_tac extras, simp, clarsimp simp: list_all2_Cons1)
apply (fastforce split: cap.splits capability.splits simp: returnOk_def)
apply (wp | wpc | simp)+
apply (rule corres_trivial, simp split: option.splits add: returnOk_def)
apply (wp | wpc | simp)+
apply (rule corres_trivial)
apply (auto simp: returnOk_def whenE_def)[1]
apply (rule_tac F="extras \<noteq> []" in corres_gen_asm)
apply (rule corres_split_eqrE)
apply simp
apply (rule getBoundNotification_corres)
apply (simp | wp gbn_wp gbn_wp')+
apply (rule corres_trivial)
apply (auto simp: returnOk_def whenE_def)[1]
apply (simp add: whenE_def split del: if_split | wp)+
apply (rule corres_split_norE)
apply (rule corres_trivial, simp split: option.splits add: returnOk_def)
apply (rule corres_splitEE'[where r'="\<lambda>rv rv'. ((fst rv) = (fst rv')) \<and> ((snd rv') = (AllowRead \<in> (snd rv)))"])
apply (rule corres_trivial, simp)
apply (case_tac extras, simp, clarsimp simp: list_all2_Cons1)
apply (fastforce split: cap.splits capability.splits simp: returnOk_def)
apply (rule corres_split_norE)
apply (rule corres_trivial, clarsimp simp: whenE_def returnOk_def)
apply (clarsimp split del: if_split)
apply (rule corres_splitEE[where r'=ntfn_relation])
apply simp
apply (rule getNotification_corres)
apply (rule corres_trivial, simp split del: if_split)
apply (simp add: ntfn_relation_def
split: Structures_A.ntfn.splits Structures_H.ntfn.splits
option.splits)
apply wp+
apply (wp | simp add: whenE_def split del: if_split)+
apply (wp | wpc | simp)+
apply (simp | wp gbn_wp gbn_wp')+
apply (fastforce simp: valid_cap_def valid_cap'_def dest: hd_in_set)+
done
@ -2633,11 +2637,11 @@ lemma decodeUnbindNotification_corres:
apply (simp add: decode_unbind_notification_def decodeUnbindNotification_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqrE)
apply (rule corres_trivial)
apply (simp split: option.splits)
apply (simp add: returnOk_def)
apply simp
apply (rule getBoundNotification_corres)
apply simp
apply (rule getBoundNotification_corres)
apply (rule corres_trivial)
apply (simp split: option.splits)
apply (simp add: returnOk_def)
apply wp+
apply auto
done

View File

@ -87,14 +87,13 @@ lemma corres_check_no_children:
apply (clarsimp simp:const_on_failure_def constOnFailure_def)
apply (rule corres_guard_imp)
apply (rule corres_split_catch[where E = dc and E'=dc])
apply simp
apply (rule corres_guard_imp[OF corres_splitEE])
apply (rule corres_returnOkTT)
apply simp
apply (rule ensureNoChildren_corres)
apply simp
apply wp+
apply simp+
apply (rule corres_guard_imp[OF corres_splitEE])
apply (rule ensureNoChildren_corres)
apply simp
apply (rule corres_returnOkTT)
apply simp
apply wp+
apply simp+
apply (clarsimp simp:dc_def,wp)+
apply simp
apply simp
@ -295,109 +294,111 @@ next
apply (clarsimp simp: fromAPIType_def)
apply (rule whenE_throwError_corres, simp)
apply (clarsimp simp: fromAPIType_def)
apply (rule_tac r' = "\<lambda>cap cap'. cap_relation cap cap'" in corres_splitEE[OF corres_if])
apply (rule_tac corres_split_norE)
apply (rule corres_if)
apply simp
apply (rule corres_returnOk,clarsimp)
apply (rule corres_trivial)
apply (clarsimp simp: fromAPIType_def lookup_failure_map_def)
apply (rule_tac F="is_cnode_cap rva \<and> cap_aligned rva" in corres_gen_asm)
apply (subgoal_tac "is_aligned (obj_ref_of rva) (bits_of rva) \<and> bits_of rva < 32")
prefer 2
apply (clarsimp simp: is_cap_simps bits_of_def cap_aligned_def word_bits_def
is_aligned_weaken)
apply (rule whenE_throwError_corres)
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def)+
apply (simp add: unat_arith_simps(2) unat_2p_sub_1 word_bits_def)
apply (rule whenE_throwError_corres)
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def)+
apply (simp add: unat_eq_0 word_less_nat_alt)
apply (rule whenE_throwError_corres)
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def)+
apply (clarsimp simp:toInteger_word unat_arith_simps(2) cap_aligned_def)
apply (subst unat_sub)
apply (simp add: linorder_not_less word_le_nat_alt)
apply (fold neq0_conv)
apply (simp add: unat_eq_0 cap_aligned_def)
apply (clarsimp simp:fromAPIType_def)
apply (clarsimp simp:liftE_bindE mapM_locate_eq)
apply (subgoal_tac "unat (arg4 + arg5) = unat arg4 + unat arg5")
prefer 2
apply (clarsimp simp:not_less)
apply (subst unat_word_ariths(1))
apply (rule mod_less)
apply (unfold word_bits_len_of)[1]
apply (subgoal_tac "2 ^ bits_of rva < (2 :: nat) ^ word_bits")
apply arith
apply (rule power_strict_increasing, simp add: word_bits_conv)
apply simp
apply (rule_tac P'="valid_cap rva" in corres_stateAssert_implied)
apply (frule_tac bits2 = "bits_of rva" in YUCK)
apply (simp)
apply (simp add: word_bits_conv)
apply (simp add: word_le_nat_alt)
apply (simp add: word_le_nat_alt)
apply (simp add:liftE_bindE[symmetric] free_index_of_def)
apply (rule corres_split_norE)
apply (subst liftE_bindE)+
apply (rule corres_split_eqr[OF corres_check_no_children])
apply (simp only: free_index_of_def cap.simps if_res_def[symmetric])
apply (rule_tac F="if_res reset \<le> 2 ^ n" in corres_gen_asm)
apply (rule whenE_throwError_corres)
apply (clarsimp simp:shiftL_nat word_less_nat_alt shiftr_div_2n'
split del: if_split)+
apply (simp add: word_of_nat_le another)
apply (drule_tac x = "if_res reset" in unat_of_nat32[OF le_less_trans])
apply (simp add:ty_size shiftR_nat)+
apply (simp add:unat_of_nat32 le_less_trans[OF div_le_dividend]
le_less_trans[OF diff_le_self])
apply (rule whenE_throwError_corres)
apply (clarsimp)
apply (clarsimp simp: fromAPIType_def)
apply (rule corres_returnOkTT)
apply (clarsimp simp:ty_size getFreeRef_def get_free_ref_def is_cap_simps)
apply simp
apply (strengthen if_res_2n, wp)
apply simp
apply wp
apply (clarsimp simp:is_cap_simps simp del:ser_def)
apply (simp add: mapME_x_map_simp del: ser_def)
apply (rule_tac P = "valid_cap (cap.CNodeCap r bits g) and invs" in corres_guard_imp [where P' = invs'])
apply (rule mapME_x_corres_inv [OF _ _ _ refl])
apply (simp del: ser_def)
apply (rule ensureEmptySlot_corres)
apply (clarsimp simp: is_cap_simps)
apply (simp, wp)
apply (simp, wp)
apply clarsimp
apply (clarsimp simp add: xs is_cap_simps bits_of_def valid_cap_def)
apply (erule cap_table_at_cte_at)
apply (simp add: nat_to_cref_def word_bits_conv)
apply simp
apply (wp mapME_x_inv_wp
validE_R_validE[OF valid_validE_R[OF ensure_empty_inv]]
validE_R_validE[OF valid_validE_R[OF ensureEmpty_inv]])+
apply (clarsimp simp: is_cap_simps valid_cap_simps
cap_table_at_gsCNodes bits_of_def
linorder_not_less)
apply (erule order_le_less_trans)
apply (rule word_leq_le_minus_one)
apply (simp add: word_le_nat_alt)
apply (simp add: unat_arith_simps)
apply wp+
apply simp
apply (rule corres_returnOkTT)
apply (rule crel)
apply simp
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rule_tac r' = "\<lambda>cap cap'. cap_relation cap cap'"
in corres_splitEE)
apply (rule corres_if, simp)
apply (rule corres_returnOkTT)
apply (rule crel)
apply simp
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres)
apply (rule crel)
apply simp
apply (rule getSlotCap_corres,simp)
apply (rule crel)
apply simp
apply (wp lookup_slot_for_cnode_op_inv
hoare_drop_impE_R hoare_vcg_all_lift_R
| clarsimp)+
apply simp
apply (rule getSlotCap_corres,simp)
apply (wp lookup_slot_for_cnode_op_inv
hoare_drop_impE_R hoare_vcg_all_lift_R)+
apply (rule_tac corres_split_norE)
apply (rule corres_if)
apply simp
apply (rule corres_returnOk,clarsimp)
apply (rule corres_trivial)
apply (clarsimp simp: fromAPIType_def lookup_failure_map_def)
apply (rule_tac F="is_cnode_cap rva \<and> cap_aligned rva" in corres_gen_asm)
apply (subgoal_tac "is_aligned (obj_ref_of rva) (bits_of rva) \<and> bits_of rva < 32")
prefer 2
apply (clarsimp simp: is_cap_simps bits_of_def cap_aligned_def word_bits_def
is_aligned_weaken)
apply (rule whenE_throwError_corres)
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def)+
apply (simp add: unat_arith_simps(2) unat_2p_sub_1 word_bits_def)
apply (rule whenE_throwError_corres)
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def)+
apply (simp add: unat_eq_0 word_less_nat_alt)
apply (rule whenE_throwError_corres)
apply (clarsimp simp:Kernel_Config.retypeFanOutLimit_def is_cap_simps bits_of_def)+
apply (clarsimp simp:toInteger_word unat_arith_simps(2) cap_aligned_def)
apply (subst unat_sub)
apply (simp add: linorder_not_less word_le_nat_alt)
apply (fold neq0_conv)
apply (simp add: unat_eq_0 cap_aligned_def)
apply (clarsimp simp:fromAPIType_def)
apply (clarsimp simp:liftE_bindE mapM_locate_eq)
apply (subgoal_tac "unat (arg4 + arg5) = unat arg4 + unat arg5")
prefer 2
apply (clarsimp simp:not_less)
apply (subst unat_word_ariths(1))
apply (rule mod_less)
apply (unfold word_bits_len_of)[1]
apply (subgoal_tac "2 ^ bits_of rva < (2 :: nat) ^ word_bits")
apply arith
apply (rule power_strict_increasing, simp add: word_bits_conv)
apply simp
apply (rule_tac P'="valid_cap rva" in corres_stateAssert_implied)
apply (frule_tac bits2 = "bits_of rva" in YUCK)
apply (simp)
apply (simp add: word_bits_conv)
apply (simp add: word_le_nat_alt)
apply (simp add: word_le_nat_alt)
apply (simp add:liftE_bindE[symmetric] free_index_of_def)
apply (rule corres_split_norE)
apply (clarsimp simp:is_cap_simps simp del:ser_def)
apply (simp add: mapME_x_map_simp del: ser_def)
apply (rule_tac P = "valid_cap (cap.CNodeCap r bits g) and invs" in corres_guard_imp [where P' = invs'])
apply (rule mapME_x_corres_inv [OF _ _ _ refl])
apply (simp del: ser_def)
apply (rule ensureEmptySlot_corres)
apply (clarsimp simp: is_cap_simps)
apply (simp, wp)
apply (simp, wp)
apply clarsimp
apply (clarsimp simp add: xs is_cap_simps bits_of_def valid_cap_def)
apply (erule cap_table_at_cte_at)
apply (simp add: nat_to_cref_def word_bits_conv)
apply simp
apply (subst liftE_bindE)+
apply (rule corres_split_eqr[OF corres_check_no_children])
apply (simp only: free_index_of_def cap.simps if_res_def[symmetric])
apply (rule_tac F="if_res reset \<le> 2 ^ n" in corres_gen_asm)
apply (rule whenE_throwError_corres)
apply (clarsimp simp:shiftL_nat word_less_nat_alt shiftr_div_2n'
split del: if_split)+
apply (simp add: word_of_nat_le another)
apply (drule_tac x = "if_res reset" in unat_of_nat32[OF le_less_trans])
apply (simp add:ty_size shiftR_nat)+
apply (simp add:unat_of_nat32 le_less_trans[OF div_le_dividend]
le_less_trans[OF diff_le_self])
apply (rule whenE_throwError_corres)
apply (clarsimp)
apply (clarsimp simp: fromAPIType_def)
apply (rule corres_returnOkTT)
apply (clarsimp simp:ty_size getFreeRef_def get_free_ref_def is_cap_simps)
apply simp
apply (strengthen if_res_2n, wp)
apply simp
apply wp
apply (wp mapME_x_inv_wp
validE_R_validE[OF valid_validE_R[OF ensure_empty_inv]]
validE_R_validE[OF valid_validE_R[OF ensureEmpty_inv]])+
apply (clarsimp simp: is_cap_simps valid_cap_simps
cap_table_at_gsCNodes bits_of_def
linorder_not_less)
apply (erule order_le_less_trans)
apply (rule word_leq_le_minus_one)
apply (simp add: word_le_nat_alt)
apply (simp add: unat_arith_simps)
apply wp+
apply simp
apply (rule hoare_strengthen_post [where Q = "\<lambda>r. invs and valid_cap r and cte_at slot"])
apply wp+
apply (clarsimp simp: is_cap_simps bits_of_def cap_aligned_def
@ -408,18 +409,18 @@ next
apply wp+
apply (rule hoare_strengthen_post [where Q = "\<lambda>r. invs' and cte_at' (cte_map slot)"])
apply wp+
apply (clarsimp simp:invs_pspace_aligned' invs_pspace_distinct' )
apply (clarsimp simp:invs_pspace_aligned' invs_pspace_distinct')
apply auto[1]
apply (wp whenE_throwError_wp | wp (once) hoare_drop_imps)+
apply (clarsimp simp: invs_valid_objs' invs_pspace_aligned' invs_pspace_distinct'
cte_wp_at_caps_of_state cte_wp_at_ctes_of )
apply (clarsimp simp: invs_valid_objs invs_psp_aligned)
apply (frule caps_of_state_valid_cap, clarsimp+)
apply (strengthen refl[where t=True] refl exI[mk_strg I E] exI[where x=d])+
apply (clarsimp simp: is_cap_simps valid_cap_def bits_of_def cap_aligned_def
cte_level_bits_def word_bits_conv)
apply (clarsimp simp: invs_valid_objs' invs_pspace_aligned' invs_pspace_distinct'
cte_wp_at_caps_of_state cte_wp_at_ctes_of )
apply (wp whenE_throwError_wp | wp (once) hoare_drop_imps)+
apply (clarsimp simp: invs_valid_objs' invs_pspace_aligned' invs_pspace_distinct'
cte_wp_at_caps_of_state cte_wp_at_ctes_of )
apply (clarsimp simp: invs_valid_objs invs_psp_aligned)
apply (frule caps_of_state_valid_cap, clarsimp+)
apply (strengthen refl[where t=True] refl exI[mk_strg I E] exI[where x=d])+
apply (clarsimp simp: is_cap_simps valid_cap_def bits_of_def cap_aligned_def
cte_level_bits_def word_bits_conv)
apply (clarsimp simp: invs_valid_objs' invs_pspace_aligned' invs_pspace_distinct'
cte_wp_at_caps_of_state cte_wp_at_ctes_of )
done
qed
@ -919,11 +920,11 @@ lemma corres_list_all2_mapM_':
apply (clarsimp simp add: mapM_x_def sequence_x_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF y])
apply (clarsimp dest!: suffix_ConsD)
apply (erule meta_allE, (drule(1) meta_mp)+)
apply assumption
apply assumption
apply assumption
apply (clarsimp dest!: suffix_ConsD)
apply (erule meta_allE, (drule(1) meta_mp)+)
apply assumption
apply (erule(1) z)+
apply simp+
@ -1516,16 +1517,17 @@ shows
apply (rule corres_underlying_symb_exec_l [OF set_original_symb_exec_l])
apply (rule corres_cong[OF refl refl _ refl refl, THEN iffD1])
apply (rule bind_return[THEN fun_cong])
apply (rule corres_split[OF setCTE_corres])
apply (subst bind_return[symmetric],
rule corres_split)
apply (simp add: dc_def[symmetric])
apply (rule updateMDB_symb_exec_r)
apply (rule corres_split)
apply (rule setCTE_corres; simp)
apply (subst bind_return[symmetric],
rule corres_split)
apply (simp add: dc_def[symmetric])
apply (rule corres_split_noop_rhs[OF updateMDB_symb_exec_r])
apply (rule updateNewFreeIndex_noop_psp_corres)
apply (wp getCTE_wp set_cdt_valid_objs set_cdt_cte_at
hoare_weak_lift_imp | simp add: o_def)+
apply (rule updateMDB_symb_exec_r)
apply (simp add: dc_def[symmetric])
apply (rule corres_split_noop_rhs[OF updateMDB_symb_exec_r])
apply (rule updateNewFreeIndex_noop_psp_corres)
apply (wp getCTE_wp set_cdt_valid_objs set_cdt_cte_at
hoare_weak_lift_imp | simp add: o_def)+
apply (clarsimp simp: cte_wp_at_cte_at)
apply (clarsimp simp: cte_wp_at_ctes_of no_0_def valid_mdb'_def
valid_mdb_ctes_def)
@ -4182,128 +4184,131 @@ lemma resetUntypedCap_corres:
liftE_bindE)
apply (rule corres_guard_imp)
apply (rule corres_split[OF getSlotCap_corres])
apply (rule_tac F="cap = cap.UntypedCap dev ptr sz idx
\<and> (\<exists>s. s \<turnstile> cap)" in corres_gen_asm)
apply (clarsimp simp: bits_of_def free_index_of_def unlessE_def
split del: if_split)
apply (rule corres_if[OF refl])
apply (rule corres_returnOk[where P=\<top> and P'=\<top>], simp)
apply (simp add: liftE_bindE bits_of_def split del: if_split)
apply (rule corres_split[OF deleteObjects_corres])
apply (rule corres_if)
apply simp
apply (simp add: bits_of_def shiftL_nat)
apply (rule corres_split_nor)
apply (rule updateFreeIndex_corres, simp)
apply (simp add: free_index_of_def)
apply (simp add: unless_def)
apply (rule corres_when, simp)
apply (rule corres_machine_op)
apply (rule corres_Id, simp, simp, wp)
apply (wp | simp only: unless_def)+
apply (rule_tac F="sz < word_bits \<and> idx \<le> 2 ^ sz
\<and> ptr \<noteq> 0 \<and> is_aligned ptr sz
\<and> resetChunkBits \<le> sz" in corres_gen_asm)
apply (simp add: bits_of_def free_index_of_def mapME_x_map_simp liftE_bindE
reset_addrs_same[where ptr=ptr and idx=idx and sz=sz]
o_def rev_map
del: capFreeIndex_update.simps)
apply (rule_tac P="\<lambda>x. valid_objs and pspace_aligned and pspace_distinct
and pspace_no_overlap {ptr .. ptr + 2 ^ sz - 1}
and cte_wp_at (\<lambda>a. is_untyped_cap a \<and> obj_ref_of a = ptr \<and> cap_bits a = sz
\<and> cap_is_device a = dev) slot"
and P'="\<lambda>_. valid_pspace' and (\<lambda>s. descendants_of' (cte_map slot) (ctes_of s) = {})
and pspace_no_overlap' ptr sz
and cte_wp_at' (\<lambda>cte. \<exists>idx. cteCap cte = UntypedCap dev ptr sz idx) (cte_map slot)"
in mapME_x_corres_same_xs)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (rule corres_split_nor[OF updateFreeIndex_corres])
apply (rule preemptionPoint_corres)
apply simp
apply (simp add: getFreeRef_def getFreeIndex_def free_index_of_def)
apply clarify
apply (subst unat_mult_simple)
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply (subst unat_p2)
apply (simp add: Kernel_Config.resetChunkBits_def)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply simp
apply wp+
apply (rule corres_machine_op)
apply (rule corres_Id)
apply (simp add: shiftL_nat getFreeRef_def shiftl_t2n mult.commute)
apply simp
apply (rule_tac F="cap = cap.UntypedCap dev ptr sz idx
\<and> (\<exists>s. s \<turnstile> cap)" in corres_gen_asm)
apply (clarsimp simp: bits_of_def free_index_of_def unlessE_def
split del: if_split)
apply (rule corres_if[OF refl])
apply (rule corres_returnOk[where P=\<top> and P'=\<top>], simp)
apply (simp add: liftE_bindE bits_of_def split del: if_split)
apply (rule corres_split)
apply (rule deleteObjects_corres)
apply (clarsimp simp: valid_cap_def cap_aligned_def)
apply (clarsimp simp: valid_cap_def cap_aligned_def untyped_min_bits_def)
apply (rule corres_if)
apply simp
apply (simp add: bits_of_def shiftL_nat)
apply (rule corres_split_nor)
apply (simp add: unless_def)
apply (rule corres_when, simp)
apply (rule corres_machine_op)
apply (rule corres_Id, simp, simp, wp)
apply (rule updateFreeIndex_corres, simp)
apply (simp add: free_index_of_def)
apply (wp | simp only: unless_def)+
apply (rule_tac F="sz < word_bits \<and> idx \<le> 2 ^ sz
\<and> ptr \<noteq> 0 \<and> is_aligned ptr sz
\<and> resetChunkBits \<le> sz" in corres_gen_asm)
apply (simp add: bits_of_def free_index_of_def mapME_x_map_simp liftE_bindE
reset_addrs_same[where ptr=ptr and idx=idx and sz=sz]
o_def rev_map
del: capFreeIndex_update.simps)
apply (rule_tac P="\<lambda>x. valid_objs and pspace_aligned and pspace_distinct
and pspace_no_overlap {ptr .. ptr + 2 ^ sz - 1}
and cte_wp_at (\<lambda>a. is_untyped_cap a \<and> obj_ref_of a = ptr \<and> cap_bits a = sz
\<and> cap_is_device a = dev) slot"
and P'="\<lambda>_. valid_pspace' and (\<lambda>s. descendants_of' (cte_map slot) (ctes_of s) = {})
and pspace_no_overlap' ptr sz
and cte_wp_at' (\<lambda>cte. \<exists>idx. cteCap cte = UntypedCap dev ptr sz idx) (cte_map slot)"
in mapME_x_corres_same_xs)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (rule corres_machine_op)
apply (rule corres_Id)
apply (simp add: shiftL_nat getFreeRef_def shiftl_t2n mult.commute)
apply simp
apply wp
apply (rule corres_split_nor)
apply (rule updateFreeIndex_corres)
apply simp
apply wp+
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (clarsimp simp: getFreeRef_def valid_pspace'_def cte_wp_at_ctes_of
valid_cap_def cap_aligned_def)
apply (erule aligned_add_aligned)
apply (rule is_aligned_weaken)
apply (rule is_aligned_mult_triv2)
apply (simp add: Kernel_Config.resetChunkBits_def)
apply (simp add: untyped_min_bits_def)
apply (rule hoare_pre)
apply simp
apply (strengthen imp_consequent)
apply (wp preemption_point_inv set_cap_cte_wp_at
update_untyped_cap_valid_objs
set_cap_no_overlap | simp)+
apply (clarsimp simp: exI cte_wp_at_caps_of_state)
apply (drule caps_of_state_valid_cap, simp+)
apply (clarsimp simp: is_cap_simps valid_cap_simps
cap_aligned_def
valid_untyped_pspace_no_overlap)
apply (rule hoare_pre)
apply (simp del: capFreeIndex_update.simps)
apply (strengthen imp_consequent)
apply (wp updateFreeIndex_valid_pspace_no_overlap'
updateFreeIndex_descendants_of2
doMachineOp_psp_no_overlap
updateFreeIndex_cte_wp_at
pspace_no_overlap'_lift
preemptionPoint_inv
hoare_vcg_ex_lift
| simp)+
apply (clarsimp simp add: cte_wp_at_ctes_of exI isCap_simps valid_pspace'_def)
apply (clarsimp simp: getFreeIndex_def getFreeRef_def)
apply (subst is_aligned_weaken[OF is_aligned_mult_triv2])
apply (simp add: Kernel_Config.resetChunkBits_def minUntypedSizeBits_def)
apply (subst unat_mult_simple)
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply (subst unat_p2)
apply (simp add: Kernel_Config.resetChunkBits_def)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply simp
apply (simp add: getFreeRef_def getFreeIndex_def free_index_of_def)
apply clarify
apply (subst unat_mult_simple)
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply (subst unat_p2)
apply (simp add: Kernel_Config.resetChunkBits_def)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply simp
apply (rule preemptionPoint_corres)
apply wp+
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (clarsimp simp: getFreeRef_def valid_pspace'_def cte_wp_at_ctes_of
valid_cap_def cap_aligned_def)
apply (erule aligned_add_aligned)
apply (rule is_aligned_weaken)
apply (rule is_aligned_mult_triv2)
apply (simp add: Kernel_Config.resetChunkBits_def)
apply (simp add: untyped_min_bits_def)
apply (rule hoare_pre)
apply simp
apply (clarsimp simp add: valid_cap_def cap_aligned_def)
apply (clarsimp simp add: valid_cap_def cap_aligned_def untyped_min_bits_def)
apply (simp add: if_apply_def2)
apply (strengthen invs_valid_objs invs_psp_aligned invs_distinct)
apply (wp hoare_vcg_const_imp_lift)
apply (strengthen imp_consequent)
apply (wp preemption_point_inv set_cap_cte_wp_at
update_untyped_cap_valid_objs
set_cap_no_overlap | simp)+
apply (clarsimp simp: exI cte_wp_at_caps_of_state)
apply (drule caps_of_state_valid_cap, simp+)
apply (clarsimp simp: is_cap_simps valid_cap_simps
cap_aligned_def
valid_untyped_pspace_no_overlap)
apply (rule hoare_pre)
apply (simp del: capFreeIndex_update.simps)
apply (strengthen imp_consequent)
apply (wp updateFreeIndex_valid_pspace_no_overlap'
updateFreeIndex_descendants_of2
doMachineOp_psp_no_overlap
updateFreeIndex_cte_wp_at
pspace_no_overlap'_lift
preemptionPoint_inv
hoare_vcg_ex_lift
| simp)+
apply (clarsimp simp add: cte_wp_at_ctes_of exI isCap_simps valid_pspace'_def)
apply (clarsimp simp: getFreeIndex_def getFreeRef_def)
apply (subst is_aligned_weaken[OF is_aligned_mult_triv2])
apply (simp add: Kernel_Config.resetChunkBits_def minUntypedSizeBits_def)
apply (subst unat_mult_simple)
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply (subst unat_p2)
apply (simp add: Kernel_Config.resetChunkBits_def)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (subst unat_of_nat_eq)
apply (rule order_less_trans[rotated],
rule_tac n=sz in power_strict_increasing; simp add: word_bits_def)
apply (erule order_less_le_trans; simp)
apply simp
apply simp
apply (simp add: if_apply_def2)
apply (strengthen invs_pspace_aligned' invs_pspace_distinct'
invs_valid_pspace')
apply (wp hoare_vcg_const_imp_lift deleteObjects_cte_wp_at'[where p="cte_map slot"]
deleteObjects_invs'[where p="cte_map slot"]
deleteObjects_descendants[where p="cte_map slot"]
| simp)+
apply (strengthen invs_valid_objs invs_psp_aligned invs_distinct)
apply (wp hoare_vcg_const_imp_lift)
apply (simp add: if_apply_def2)
apply (strengthen invs_pspace_aligned' invs_pspace_distinct'
invs_valid_pspace')
apply (wp hoare_vcg_const_imp_lift deleteObjects_cte_wp_at'[where p="cte_map slot"]
deleteObjects_invs'[where p="cte_map slot"]
deleteObjects_descendants[where p="cte_map slot"]
| simp)+
apply (wp get_cap_wp getCTE_wp' | simp add: getSlotCap_def)+
apply (clarsimp simp: cte_wp_at_caps_of_state descendants_range_def2)
apply (cases slot)
@ -4839,14 +4844,13 @@ lemma inv_untyped_corres':
sz (if reset then 0 else idx)" in corres_gen_asm)
apply (rule corres_add_noop_lhs)
apply (rule corres_split_nor[OF cNodeNoOverlap _ return_wp stateAssert_wp])
apply (rule corres_split[OF updateFreeIndex_corres,rotated])
apply (rule corres_split[OF updateFreeIndex_corres])
apply (simp add:isCap_simps)+
apply (clarsimp simp:getFreeIndex_def bits_of_def shiftL_nat shiftl_t2n
free_index_of_def)
prefer 3
apply (insert range_cover.range_cover_n_less[OF cover] vslot)
apply (rule createNewObjects_corres_helper)
apply simp+
apply simp+
apply (simp add: insertNewCaps_def)
apply (rule corres_split_retype_createNewCaps[where sz = sz,OF corres_rel_imp])
apply (rule inv_untyped_corres_helper1)

View File

@ -185,60 +185,61 @@ lemma findPDForASIDAssert_corres:
findPDForASIDAssert_def liftM_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule_tac F="is_aligned pda pdBits
\<and> pda = pd" in corres_gen_asm)
apply (clarsimp simp add: is_aligned_mask[symmetric])
apply (rule_tac P="pde_at pd and pd_at_uniq asid pd
and pspace_aligned and pspace_distinct
and vspace_at_asid asid pd and valid_asid_map"
and P'="pspace_aligned' and pspace_distinct'"
in stronger_corres_guard_imp)
apply (rule corres_split_catch[OF find_pd_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 (rule_tac F="is_aligned pda pdBits
\<and> pda = pd" in corres_gen_asm)
apply (clarsimp simp add: is_aligned_mask[symmetric])
apply (rule_tac P="pde_at pd and pd_at_uniq asid pd
and pspace_aligned and pspace_distinct
and vspace_at_asid asid pd and valid_asid_map"
and P'="pspace_aligned' and pspace_distinct'"
in stronger_corres_guard_imp)
apply (rule corres_symb_exec_l[where P="pde_at pd and pd_at_uniq asid pd
and valid_asid_map and vspace_at_asid asid pd"])
apply (rule corres_symb_exec_r[where P'="page_directory_at' pd"])
apply (simp add: checkPDUniqueToASID_def ran_option_map
checkPDASIDMapMembership_def)
apply (rule_tac P'="pd_at_uniq asid pd" in corres_stateAssert_implied)
apply (simp add: gets_def bind_assoc[symmetric]
stateAssert_def[symmetric, where L="[]"])
apply (rule_tac P'="valid_asid_map and vspace_at_asid asid pd"
in corres_stateAssert_implied)
apply (rule corres_trivial, simp)
apply (clarsimp simp: state_relation_def arch_state_relation_def
valid_asid_map_def
split: option.split)
apply (drule bspec, erule graph_ofI)
apply clarsimp
apply (drule(1) pd_at_asid_unique2)
apply simp
apply (rule corres_symb_exec_r[where P'="page_directory_at' pd"])
apply (simp add: checkPDUniqueToASID_def ran_option_map
checkPDASIDMapMembership_def)
apply (rule_tac P'="pd_at_uniq asid pd" in corres_stateAssert_implied)
apply (simp add: gets_def bind_assoc[symmetric]
stateAssert_def[symmetric, where L="[]"])
apply (rule_tac P'="valid_asid_map and vspace_at_asid asid pd"
in corres_stateAssert_implied)
apply (rule corres_trivial, simp)
apply (clarsimp simp: state_relation_def arch_state_relation_def
pd_at_uniq_def ran_option_map)
apply wp+
apply (simp add: checkPDAt_def stateAssert_def)
apply (rule no_fail_pre, wp)
apply simp
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
apply (clarsimp split: Structures_A.kernel_object.splits
arch_kernel_obj.splits if_split_asm)
apply (simp add: get_pde_def exs_valid_def bind_def return_def
get_pd_def get_object_def simpler_gets_def)
apply wp
apply simp
apply (simp add: get_pde_def get_pd_def)
apply (rule no_fail_pre)
apply (wp get_object_wp | wpc)+
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
apply (clarsimp split: Structures_A.kernel_object.splits
arch_kernel_obj.splits if_split_asm)
apply simp
apply (clarsimp simp: state_relation_def)
apply (erule(3) pspace_relation_pd)
apply (simp add: pde_at_def pd_bits_def pdBits_def
is_aligned_neg_mask_eq pdeBits_def pageBits_def)
apply (rule corres_split_catch[OF find_pd_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])+
valid_asid_map_def
split: option.split)
apply (drule bspec, erule graph_ofI)
apply clarsimp
apply (drule(1) pd_at_asid_unique2)
apply simp
apply (clarsimp simp: state_relation_def arch_state_relation_def
pd_at_uniq_def ran_option_map)
apply wp+
apply (simp add: checkPDAt_def stateAssert_def)
apply (rule no_fail_pre, wp)
apply simp
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
apply (clarsimp split: Structures_A.kernel_object.splits
arch_kernel_obj.splits if_split_asm)
apply (simp add: get_pde_def exs_valid_def bind_def return_def
get_pd_def get_object_def simpler_gets_def)
apply wp
apply simp
apply (simp add: get_pde_def get_pd_def)
apply (rule no_fail_pre)
apply (wp get_object_wp | wpc)+
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
apply (clarsimp split: Structures_A.kernel_object.splits
arch_kernel_obj.splits if_split_asm)
apply simp
apply (clarsimp simp: state_relation_def)
apply (erule(3) pspace_relation_pd)
apply (simp add: pde_at_def pd_bits_def pdBits_def
is_aligned_neg_mask_eq pdeBits_def pageBits_def)
apply (wp find_pd_for_asid_valids[where pd=pd])+
apply (clarsimp simp: word_neq_0_conv valid_vspace_objs_def)
apply simp
done
@ -309,23 +310,22 @@ lemma storeHWASID_corres:
apply (rule corres_guard_imp)
apply (rule corres_split[OF findPDForASIDAssert_corres[where pd=pd]])
apply (rule corres_split_eqr)
apply (rule corres_split)
apply (rule corres_trivial, rule corres_modify)
apply (clarsimp simp: state_relation_def)
apply (simp add: arch_state_relation_def)
apply (rule ext)
apply simp
apply (rule corres_split_eqr)
apply (rule corres_trivial, rule corres_modify)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule ext)
apply simp
apply (rule corres_trivial)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule corres_split)
apply (rule corres_trivial, rule corres_modify)
apply (clarsimp simp: state_relation_def)
apply (simp add: arch_state_relation_def)
apply (rule ext)
apply simp
apply (rule corres_split_eqr)
apply (rule corres_trivial)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply ((wp | simp)+)[4]
apply (rule corres_trivial)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (wp | simp)+
apply (rule corres_trivial, rule corres_modify)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule ext)
apply simp
apply (wp | simp)+
done
lemma invalidateASID_corres:
@ -368,12 +368,12 @@ lemma invalidateHWASIDEntry_corres:
apply (simp add: invalidate_hw_asid_entry_def invalidateHWASIDEntry_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule corres_trivial, rule corres_modify)
defer
apply (rule corres_trivial)
apply (wp | clarsimp simp: state_relation_def arch_state_relation_def)+
apply (rule ext)
apply simp
apply (rule corres_trivial)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule corres_trivial, rule corres_modify)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule ext)
apply (wp | clarsimp)+
done
lemma findFreeHWASID_corres:
@ -388,38 +388,40 @@ lemma findFreeHWASID_corres:
apply (simp add: find_free_hw_asid_def findFreeHWASID_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[OF corres_trivial])
apply (rule corres_split_eqr[OF corres_trivial])
apply (subgoal_tac "take (length [minBound .e. maxBound :: hardware_asid])
([next_asid .e. maxBound] @ [minBound .e. next_asid])
= [next_asid .e. maxBound] @ init [minBound .e. next_asid]")
apply (cut_tac option="find (\<lambda>a. hw_asid_table a = None)
([next_asid .e. maxBound] @ init [minBound .e. next_asid])"
in option.nchotomy[rule_format])
apply (erule corres_disj_division)
apply (clarsimp split del: if_split)
apply (rule corres_split[OF invalidate_asid_ext_corres])
apply (rule corres_underlying_split [where r'=dc])
apply (rule corres_trivial, rule corres_machine_op)
apply (rule corres_no_failI)
apply (rule no_fail_invalidateLocalTLB_ASID)
apply fastforce
apply (clarsimp simp: arch_state_relation_def state_relation_def)
apply (rule corres_split_eqr[OF corres_trivial])
apply (clarsimp simp: arch_state_relation_def state_relation_def)
apply (subgoal_tac "take (length [minBound .e. maxBound :: hardware_asid])
([next_asid .e. maxBound] @ [minBound .e. next_asid])
= [next_asid .e. maxBound] @ init [minBound .e. next_asid]")
apply (cut_tac option="find (\<lambda>a. hw_asid_table a = None)
([next_asid .e. maxBound] @ init [minBound .e. next_asid])"
in option.nchotomy[rule_format])
apply (erule corres_disj_division)
apply (clarsimp split del: if_split)
apply (rule corres_split[OF invalidate_asid_ext_corres])
apply (rule corres_underlying_split [where r'=dc])
apply (rule corres_trivial, rule corres_machine_op)
apply (rule corres_no_failI)
apply (rule no_fail_invalidateLocalTLB_ASID)
apply fastforce
apply (rule corres_split)
apply (rule invalidateHWASIDEntry_corres)
apply (rule corres_split)
apply (rule invalidateHWASIDEntry_corres)
apply (rule corres_split_deprecated)
apply (rule corres_trivial)
apply simp
apply (rule corres_trivial)
apply (rule corres_modify)
apply (simp add: minBound_word maxBound_word
state_relation_def arch_state_relation_def)
apply (wp | simp split del: if_split)+
apply (rule corres_trivial, clarsimp)
apply (cut_tac x=next_asid in leq_maxBound)
apply (simp only: word_le_nat_alt)
apply (simp add: init_def upto_enum_word
minBound_word
del: upt.simps)
apply (wp | clarsimp simp: arch_state_relation_def state_relation_def)+
apply (rule corres_trivial)
apply (rule corres_modify)
apply (simp add: minBound_word maxBound_word
state_relation_def arch_state_relation_def)
apply (rule corres_trivial)
apply simp
apply (wp | simp split del: if_split)+
apply (rule corres_trivial, clarsimp)
apply (cut_tac x=next_asid in leq_maxBound)
apply (simp only: word_le_nat_alt)
apply (simp add: init_def upto_enum_word
minBound_word
del: upt.simps)
apply wp+
apply (clarsimp dest!: findNoneD)
apply (drule bspec, rule UnI1, simp, rule order_refl)
apply (clarsimp simp: valid_arch_state_def)
@ -428,8 +430,8 @@ lemma findFreeHWASID_corres:
apply (frule bspec, erule graph_ofI, clarsimp)
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_vspace_objs_def)
apply simp
apply (simp add: valid_vspace_objs_def)
apply fastforce
apply clarsimp
done
@ -635,13 +637,15 @@ lemma setCurrentPD_corres:
apply (rule corres_machine_op)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule corres_split_eqr)
apply (rule corres_rel_imp)
apply (wp
| rule corres_underlying_trivial
| rule setCurrentPD_no_fails
| rule setCurrentPD_no_irqs
| simp add: dc_def)+
apply (rule corres_underlying_trivial)
apply (wp setCurrentPD_no_fails)
apply (rule corres_split_eqr)
apply (rule corres_underlying_trivial)
apply (wp setCurrentPD_no_fails)
apply (rule corres_rel_imp)
apply (rule corres_underlying_trivial)
apply (wp setCurrentPD_no_fails)
apply wpsimp+
done
lemma setVMRoot_corres:
@ -662,9 +666,9 @@ proof -
od)"
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule setCurrentPD_corres)
apply (subst corres_gets)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (subst corres_gets)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule setCurrentPD_corres)
apply (wp | simp)+
done
have Q: "\<And>P P'. corres dc P P'
@ -678,8 +682,8 @@ proof -
od))"
apply (rule corres_guard_imp)
apply (rule corres_split_catch [where f=lfr])
apply (simp, rule P)
apply (subst corres_throwError, simp add: lookup_failure_map_def)
apply (subst corres_throwError, simp add: lookup_failure_map_def)
apply (simp, rule P)
apply (wp | simp)+
done
show ?thesis
@ -696,49 +700,51 @@ proof -
pspace_aligned and pspace_distinct and
cte_wp_at ((=) thread_root) thread_root_slot"
and R'="\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'"
in corres_split[OF getSlotCap_corres])
apply (insert Q)
apply (case_tac rv, simp_all add: isCap_simps Q[simplified])[1]
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all add: isCap_simps Q[simplified])[1]
apply (rename_tac word option)
apply (case_tac option, simp_all add: Q[simplified])[1]
apply (clarsimp simp: cap_asid_def)
apply (rule corres_guard_imp)
apply (rule corres_split_catch [where f=lfr])
apply (simp add: checkPDNotInASIDMap_def
checkPDASIDMapMembership_def)
apply (rule_tac P'="(Not \<circ> vspace_at_asid aa word) and K (aa \<le> mask asid_bits)
and pd_at_uniq aa word
and valid_asid_map and valid_vs_lookup
and (unique_table_refs o caps_of_state)
and valid_vspace_objs and valid_global_objs
and valid_arch_state"
in corres_stateAssert_implied)
apply (rule P)
apply (clarsimp simp: restrict_map_def state_relation_asid_map
elim!: ranE)
apply (frule(1) valid_asid_mapD)
apply (case_tac "x = aa")
apply clarsimp
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])
in corres_split)
apply (rule getSlotCap_corres; simp)
apply (insert Q)
apply (case_tac rv, simp_all add: isCap_simps Q[simplified])[1]
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all add: isCap_simps Q[simplified])[1]
apply (rename_tac word option)
apply (case_tac option, simp_all add: Q[simplified])[1]
apply (clarsimp simp: cap_asid_def)
apply (rule corres_guard_imp)
apply (rule corres_split_catch [where f=lfr])
apply (rule corres_split_eqrE)
apply (rule find_pd_for_asid_corres; simp)
apply (rule whenE_throwError_corres)
apply (simp add: lookup_failure_map_def)
apply simp
apply simp
apply (rule armv_contextSwitch_corres)
apply ((wp find_pd_for_asid_pd_at_asid_again
| simp add: if_apply_def2 | wp (once) hoare_drop_imps)+)
apply clarsimp
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)
apply (drule(1) pd_at_asid_unique2, simp)
apply simp+
apply (wp hoare_drop_imps)+
apply (simp add: checkPDNotInASIDMap_def
checkPDASIDMapMembership_def)
apply (rule_tac P'="(Not \<circ> vspace_at_asid aa word) and K (aa \<le> mask asid_bits)
and pd_at_uniq aa word
and valid_asid_map and valid_vs_lookup
and (unique_table_refs o caps_of_state)
and valid_vspace_objs and valid_global_objs
and valid_arch_state"
in corres_stateAssert_implied)
apply (rule P)
apply (clarsimp simp: restrict_map_def state_relation_asid_map
elim!: ranE)
apply (frule(1) valid_asid_mapD)
apply (case_tac "x = aa")
apply clarsimp
apply (clarsimp simp: pd_at_uniq_def restrict_map_def)
apply (erule notE, rule_tac a=x in ranI)
apply simp
apply (wp find_pd_for_asid_pd_at_asid_again)+
apply clarsimp
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)
apply (drule(1) pd_at_asid_unique2, simp)
apply simp+
apply (wp get_cap_wp | simp)+
apply (clarsimp simp: tcb_at_cte_at_1 [simplified])
apply simp
@ -790,14 +796,14 @@ lemma invalidateASIDEntry_corres:
(invalidate_asid_entry asid) (invalidateASIDEntry asid)"
apply (simp add: invalidate_asid_entry_def invalidateASIDEntry_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF loadHWASID_corres[where pd=pd]])
apply (rule corres_split[OF corres_when])
apply (rule invalidateASID_corres[where pd=pd])
apply simp
apply simp
apply (rule invalidateHWASIDEntry_corres)
apply (wp load_hw_asid_wp
| clarsimp cong: if_cong)+
apply (rule corres_split[OF loadHWASID_corres[where pd=pd]])
apply (rule corres_split[OF corres_when])
apply simp
apply simp
apply (rule invalidateHWASIDEntry_corres)
apply (rule invalidateASID_corres[where pd=pd])
apply (wp load_hw_asid_wp
| clarsimp cong: if_cong)+
apply (simp add: pd_at_asid_uniq)
apply simp
done
@ -1087,26 +1093,25 @@ proof -
apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv)
apply (rule corres_guard_imp)
apply (rule corres_split[OF getCurThread_corres])
apply (rule corres_split_deprecated [where R="\<lambda>_. vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
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_vspace_objs and valid_global_objs
and unique_table_refs o caps_of_state
and valid_arch_state
and pspace_aligned and pspace_distinct"
and R'="\<lambda>_. pspace_aligned' and pspace_distinct' and no_0_obj'",
OF _ getSlotCap_corres])
apply (case_tac "isArchObjectCap rv' \<and>
isPageDirectoryCap (capCap rv') \<and>
capPDMappedASID (capCap rv') \<noteq> None \<and>
capPDBasePtr (capCap rv') = pd")
apply (case_tac rv, simp_all add: isCap_simps)[1]
apply (rename_tac arch_cap)
apply (case_tac arch_cap, auto)[1]
apply (case_tac rv, simp_all add: isCap_simps[simplified] X[simplified])[1]
and R'="\<lambda>_. pspace_aligned' and pspace_distinct' and no_0_obj'"])
apply (rule getSlotCap_corres)
apply (simp add: cte_map_def tcb_cnode_index_def tcbVTableSlot_def to_bl_1)
apply (case_tac "isArchObjectCap rv' \<and>
isPageDirectoryCap (capCap rv') \<and>
capPDMappedASID (capCap rv') \<noteq> None \<and>
capPDBasePtr (capCap rv') = pd")
apply (case_tac rv, simp_all add: isCap_simps)[1]
apply (rename_tac arch_cap)
apply (case_tac arch_cap, auto simp: X[simplified] split: option.splits)[1]
apply (simp add: cte_map_def objBits_simps tcb_cnode_index_def
tcbVTableSlot_def to_bl_1 cte_level_bits_def)
apply (case_tac arch_cap, auto)[1]
apply (case_tac rv, simp_all add: isCap_simps[simplified] X[simplified])[1]
apply (rename_tac arch_cap)
apply (case_tac arch_cap, auto simp: X[simplified] split: option.splits)[1]
apply wp+
apply (clarsimp simp: cur_tcb_def)
apply (erule tcb_at_cte_at)
@ -1288,16 +1293,16 @@ lemma flushTable_corres:
apply (rule corres_split[OF load_hw_asid_corres2[where pd=pd]])
apply (clarsimp cong: corres_weak_cong)
apply (rule corres_when, rule refl)
apply (rule corres_split_deprecated[where r' = dc, OF corres_when corres_machine_op])
apply simp
apply (rule corres_split[OF getCurThread_corres])
apply (simp, rule setVMRoot_corres)
apply ((wp mapM_wp' hoare_vcg_const_imp_lift get_pte_wp getPTE_wp|
wpc|simp|fold cur_tcb_def cur_tcb'_def)+)[4]
apply (rule corres_Id[OF refl])
apply (rule corres_split[where r' = dc, OF corres_machine_op corres_when])
apply (rule corres_Id[OF refl])
apply simp
apply (rule no_fail_invalidateLocalTLB_ASID)
apply simp
apply (rule no_fail_invalidateLocalTLB_ASID)
apply (wp hoare_drop_imps | simp)+
apply (rule corres_split[OF getCurThread_corres])
apply (simp, rule setVMRoot_corres)
apply ((wp mapM_wp' hoare_vcg_const_imp_lift get_pte_wp getPTE_wp|
wpc|simp|fold cur_tcb_def cur_tcb'_def)+)[4]
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] )+
done
@ -1324,14 +1329,14 @@ lemma flushPage_corres:
apply (clarsimp cong: corres_weak_cong)
apply (rule corres_when, rule refl)
apply (rule corres_split[OF corres_machine_op [where r=dc]])
apply (rule corres_when, rule refl)
apply (rule corres_split[OF getCurThread_corres])
apply simp
apply (rule setVMRoot_corres)
apply wp+
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_pre, wp no_fail_invalidateLocalTLB_VAASID)
apply simp
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_pre, wp no_fail_invalidateLocalTLB_VAASID)
apply simp
apply (rule corres_when, rule refl)
apply (rule corres_split[OF getCurThread_corres])
apply simp
apply (rule setVMRoot_corres)
apply wp+
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
@ -1360,16 +1365,16 @@ lemma pageTableMapped_corres:
(pageTableMapped asid vaddr pt)"
apply (simp add: page_table_mapped_def pageTableMapped_def)
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 (simp add: liftE_bindE)
apply (rule corres_split[OF getObject_PDE_corres'])
apply (rule corres_trivial)
apply (case_tac rv,
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 (rule corres_split_catch)
apply (rule corres_split_eqrE[OF find_pd_for_asid_corres])
apply simp
apply (simp add: liftE_bindE)
apply (rule corres_split[OF getObject_PDE_corres'])
apply (rule corres_trivial)
apply (case_tac rv,
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)
apply simp
done
@ -1395,14 +1400,14 @@ lemma unmapPageTable_corres:
apply (rule corres_split_eqr[OF pageTableMapped_corres])
apply (simp add: case_option_If2 split del: if_split)
apply (rule corres_if2[OF refl])
apply (rule corres_split[OF storePDE_corres'])
apply (rule corres_split[OF corres_machine_op])
apply (rule flushTable_corres)
apply (rule corres_split)
apply (rule storePDE_corres')
apply (simp add:pde_relation_aligned_def)
apply (rule corres_split[OF corres_machine_op])
apply (rule corres_Id, rule refl, simp)
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_vspace_objs_invalid)
apply (wp no_fail_cleanByVA_PoU)
apply (rule flushTable_corres)
apply (wpsimp 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)+
@ -1439,9 +1444,9 @@ lemma corres_split_strengthen_ftE:
\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,-; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>,- \<rbrakk>
\<Longrightarrow> corres (dc \<oplus> r) (P and Q) (P' and Q') (f >>=E (\<lambda>rv. g rv)) (j >>=E (\<lambda>rv'. k rv'))"
apply (rule_tac r'=r' in corres_splitEE)
apply (rule corres_rel_imp, assumption)
apply (erule corres_rel_imp)
apply (case_tac x, auto)[1]
apply (erule corres_rel_imp)
apply (rule corres_rel_imp, assumption)
apply (case_tac x, auto)[1]
apply (simp add: validE_R_def)+
done
@ -1501,130 +1506,137 @@ lemma unmapPage_corres:
(unmapPage sz asid vptr pptr)"
apply (clarsimp simp: unmap_page_def unmapPage_def ignoreFailure_def const_def largePagePTEOffsets_def)
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,simp)
apply (rule corres_splitEE)
apply (rule corres_split_catch [where E="\<lambda>_. \<top>" and E'="\<lambda>_. \<top>"])
apply (rule corres_split_strengthen_ftE[where ftr'=dc],
rule find_pd_for_asid_corres,simp)
apply (rule corres_splitEE)
prefer 2
apply clarsimp
apply (rule flushPage_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_vspace_objs
and equal_kernel_mappings
and pspace_aligned and valid_global_objs and valid_etcbs and
K (valid_unmap sz (asid,vptr) )" and
P'="pspace_aligned' and pspace_distinct'" in corres_inst)
apply clarsimp
apply (rule flushPage_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_vspace_objs
and equal_kernel_mappings
and pspace_aligned and valid_global_objs and valid_etcbs and
K (valid_unmap sz (asid,vptr) )" and
P'="pspace_aligned' and pspace_distinct'" in corres_inst)
apply clarsimp
apply (rename_tac pd)
apply (cases sz, simp_all)[1]
apply (rule corres_guard_imp)
apply (rule_tac F = "vptr < kernel_base" in corres_gen_asm)
apply (rule corres_split_strengthen_ftE[OF lookupPTSlot_corres[OF refl refl]])
apply simp
apply (rule corres_splitEE[OF checkMappingPPtr_corres])
apply simp
apply (rule corres_split[OF storePTE_corres'])
apply (rename_tac pd)
apply (cases sz, simp_all)[1]
apply (rule corres_guard_imp)
apply (rule_tac F = "vptr < kernel_base" in corres_gen_asm)
apply (rule corres_split_strengthen_ftE[OF lookupPTSlot_corres[OF refl refl]])
apply simp
apply (rule corres_splitEE[OF checkMappingPPtr_corres])
apply simp
apply (rule corres_split)
apply (rule storePTE_corres')
apply (simp add: pte_relation_aligned_def)
apply (rule corres_machine_op)
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_cleanByVA_PoU)
apply (wp hoare_drop_imps lookup_pt_slot_inv
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)
apply (simp add:valid_unmap_def pageBits_def)
apply (erule less_kernel_base_mapping_slots)
apply (simp add:page_directory_at_aligned_pd_bits)
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split_strengthen_ftE[OF lookupPTSlot_corres[OF refl refl]])
apply (rule_tac F="is_aligned p 6" in corres_gen_asm)
apply (simp add: is_aligned_mask[symmetric])
apply (rule corres_split_strengthen_ftE[OF checkMappingPPtr_corres])
apply (simp add: largePagePTEOffsets_def pteBits_def)
apply (rule corres_split[OF corres_mapM])
prefer 8
apply (rule order_refl)
apply (rule corres_machine_op)
apply (clarsimp simp: last_byte_pte_def objBits_simps archObjSize_def)
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_cleanCacheRange_PoU)
apply simp
apply simp
apply clarsimp
apply (rule_tac P="(\<lambda>s. \<forall>x\<in>set [0, 4 .e. 0x3C]. pte_at (x + pa) s) and pspace_aligned and valid_etcbs"
and P'="pspace_aligned' and pspace_distinct'"
in corres_guard_imp)
apply (rule storePTE_corres', simp add:pte_relation_aligned_def)
apply clarsimp
apply clarsimp
apply (wp store_pte_typ_at hoare_vcg_const_Ball_lift | simp | wp (once) hoare_drop_imps)+
apply (wp lookup_pt_slot_ptes lookup_pt_slot_inv lookupPTSlot_inv
lookup_pt_slot_is_aligned lookup_pt_slot_is_aligned_6)+
apply (clarsimp simp: page_directory_pde_at_lookupI vmsz_aligned_def pd_aligned
pd_bits_def pageBits_def valid_unmap_def)
apply (drule(1) less_kernel_base_mapping_slots[OF _ page_directory_at_aligned_pd_bits])
apply (wpsimp wp: hoare_drop_imps lookup_pt_slot_inv
lookupPTSlot_inv lookup_pt_slot_is_aligned)+
apply (clarsimp simp: page_directory_pde_at_lookupI
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)
apply simp
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 checkMappingPPtr_corres])
apply (rule corres_guard_imp)
apply (rule corres_split_strengthen_ftE[OF lookupPTSlot_corres[OF refl refl]])
apply (rule_tac F="is_aligned p 6" in corres_gen_asm)
apply (simp add: is_aligned_mask[symmetric])
apply (rule corres_split_strengthen_ftE[OF checkMappingPPtr_corres])
apply (simp add: largePagePTEOffsets_def pteBits_def)
apply (rule corres_split)
apply (rule corres_mapM)
prefer 7
apply (rule order_refl)
apply simp
apply simp
apply clarsimp
apply (rule_tac P="(\<lambda>s. \<forall>x\<in>set [0, 4 .e. 0x3C]. pte_at (x + pa) s) and pspace_aligned and valid_etcbs"
and P'="pspace_aligned' and pspace_distinct'"
in corres_guard_imp)
apply (rule storePTE_corres', simp add:pte_relation_aligned_def)
apply clarsimp
apply clarsimp
apply (wpsimp wp: store_pte_typ_at hoare_vcg_const_Ball_lift)+
apply (rule corres_machine_op)
apply (clarsimp simp: last_byte_pte_def objBits_simps archObjSize_def)
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_cleanCacheRange_PoU)
apply (wp hoare_drop_imps | simp)+
apply (wp lookup_pt_slot_ptes lookup_pt_slot_inv lookupPTSlot_inv
lookup_pt_slot_is_aligned lookup_pt_slot_is_aligned_6)+
apply (clarsimp simp: page_directory_pde_at_lookupI vmsz_aligned_def pd_aligned
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 (rule corres_split[OF storePDE_corres'])
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 checkMappingPPtr_corres])
apply simp
apply (rule corres_split)
apply (rule storePDE_corres')
apply (simp add:pde_relation_aligned_def)
apply (rule corres_machine_op)
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_cleanByVA_PoU)
apply (wp | simp add:pde_relation_aligned_def
| wp (once) hoare_drop_imps)+
apply (clarsimp simp: page_directory_pde_at_lookupI
pg_entry_align_def)
apply (clarsimp simp:lookup_pd_slot_def)
apply (erule(1) aligned_add_aligned[OF page_directory_at_aligned_pd_bits])
apply (simp add:is_aligned_shiftl_self)
apply (simp add:pd_bits_def pageBits_def word_bits_conv)
apply (simp add:pd_bits_def pageBits_def)
apply (rule corres_guard_imp)
apply (rule corres_split_strengthen_ftE[OF checkMappingPPtr_corres])
apply (rule_tac F="is_aligned (lookup_pd_slot pd vptr) 6"
in corres_gen_asm)
apply (simp add: is_aligned_mask[symmetric])
apply (rule corres_split_deprecated)
apply (wp | simp | wp (once) hoare_drop_imps)+
apply (clarsimp simp: page_directory_pde_at_lookupI
pg_entry_align_def)
apply (clarsimp simp:lookup_pd_slot_def)
apply (erule(1) aligned_add_aligned[OF page_directory_at_aligned_pd_bits])
apply (simp add:is_aligned_shiftl_self)
apply (simp add:pd_bits_def pageBits_def word_bits_conv)
apply (simp add:pd_bits_def pageBits_def)
apply (rule corres_guard_imp)
apply (rule corres_split_strengthen_ftE[OF checkMappingPPtr_corres])
apply (rule_tac F="is_aligned (lookup_pd_slot pd vptr) 6"
in corres_gen_asm)
apply (simp add: is_aligned_mask[symmetric])
apply (rule corres_split)
apply (rule_tac P="page_directory_at pd and pspace_aligned and valid_etcbs
and K (valid_unmap sz (asid, vptr))"
in corres_mapM [where r=dc], simp, simp)
prefer 5
apply (rule order_refl)
apply (clarsimp simp: superSectionPDEOffsets_def pdeBits_def)
apply (rule corres_guard_imp, rule storePDE_corres')
apply (simp add:pde_relation_aligned_def)+
apply clarsimp
apply (erule (2) pde_at_aligned_vptr)
apply (simp add: valid_unmap_def)
apply assumption
apply (wp | simp add: superSectionPDEOffsets_def pdeBits_def)+
apply (rule corres_machine_op)
apply (clarsimp simp: last_byte_pde_def objBits_simps archObjSize_def
superSectionPDEOffsets_def pdeBits_def)
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_cleanCacheRange_PoU)
apply (rule_tac P="page_directory_at pd and pspace_aligned and valid_etcbs
and K (valid_unmap sz (asid, vptr))"
in corres_mapM [where r=dc], simp, simp)
prefer 5
apply (rule order_refl)
apply (clarsimp simp: superSectionPDEOffsets_def pdeBits_def)
apply (rule corres_guard_imp, rule storePDE_corres')
apply (simp add:pde_relation_aligned_def)+
apply clarsimp
apply (erule (2) pde_at_aligned_vptr)
apply (simp add: valid_unmap_def)
apply assumption
apply (wp | simp add: superSectionPDEOffsets_def pdeBits_def | wp (once) hoare_drop_imps)+
apply (clarsimp simp: valid_unmap_def page_directory_pde_at_lookupI
lookup_pd_slot_aligned_6 pg_entry_align_def
pd_aligned vmsz_aligned_def)
apply simp
apply wp
apply (rule_tac Q'="\<lambda>_. invs and vspace_at_asid asid pda" in hoare_post_imp_R)
apply (wp lookup_pt_slot_inv lookup_pt_slot_cap_to2' lookup_pt_slot_cap_to_multiple2
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])[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
page_directory_at_lookup_mask_aligned_strg lookup_pd_slot_kernel_mappings_set_strg
page_directory_at_lookup_mask_add_aligned_strg
| wp hoare_vcg_const_Ball_lift_R)+
apply (wp hoare_drop_imps)+
apply (clarsimp simp: valid_unmap_def page_directory_pde_at_lookupI
lookup_pd_slot_aligned_6 pg_entry_align_def
pd_aligned vmsz_aligned_def)
apply simp
apply wp
apply (rule_tac Q'="\<lambda>_. invs and vspace_at_asid asid pda" in hoare_post_imp_R)
apply (wp lookup_pt_slot_inv lookup_pt_slot_cap_to2' lookup_pt_slot_cap_to_multiple2
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 (fastforce simp: invs_vspace_objs[simplified])
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
page_directory_at_lookup_mask_aligned_strg lookup_pd_slot_kernel_mappings_set_strg
page_directory_at_lookup_mask_add_aligned_strg
| wp hoare_vcg_const_Ball_lift_R
| simp)+
apply (clarsimp simp add: valid_unmap_def valid_asid_def)
apply (case_tac sz)
apply (auto simp: invs_def valid_state_def
@ -2123,29 +2135,30 @@ proof -
apply (clarsimp simp: mapM_Cons bind_assoc split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split[OF pteCheckIfMapped_corres])
apply (rule corres_split[OF storePTE_corres'])
apply (rule corres_split_deprecated[where r' = dc, OF _ corres_store_pte_with_invalid_tail])
apply (rule corres_split_deprecated[where r'=dc, OF _ corres_machine_op[OF corres_Id]])
apply (rule corres_split[where r'=dc, OF _ corres_return_eq_same[OF refl]])
apply (clarsimp simp add: when_def)
apply (rule invalidate_tlb_by_asid_corres_ex)
apply wp
apply wp
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 (rule corres_split)
apply (rule storePTE_corres')
apply (clarsimp simp: pte_relation_aligned_def
dest!: valid_slots_duplicated_pteD')
apply (rule corres_split[where r' = dc])
apply (rule corres_store_pte_with_invalid_tail)
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 (rule corres_split[where r'=dc])
apply (rule corres_machine_op[OF corres_Id])
apply (simp add: last_byte_pte_def objBits_simps archObjSize_def pteBits_def)
apply simp
apply (rule no_fail_cleanCacheRange_PoU)
apply (rule corres_split[where r'=dc, OF _ corres_return_eq_same[OF refl]])
apply (clarsimp simp add: when_def)
apply (rule invalidate_tlb_by_asid_corres_ex)
apply (wp hoare_vcg_ex_lift)+
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 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)+
@ -2174,29 +2187,29 @@ proof -
apply (clarsimp simp: mapM_Cons bind_assoc split del:if_split)
apply (rule corres_guard_imp)
apply (rule corres_split[OF pdeCheckIfMapped_corres])
apply (rule corres_split[OF storePDE_corres'])
apply (rule corres_split_deprecated[where r'=dc, OF _ corres_store_pde_with_invalid_tail])
apply (rule corres_split_deprecated[where r'=dc,OF _ corres_machine_op[OF corres_Id]])
apply (rule corres_split[where r'=dc, OF _ corres_return_eq_same[OF refl]])
apply (clarsimp simp: when_def)
apply (rule invalidate_tlb_by_asid_corres_ex)
apply wp
apply wp
apply (simp add: last_byte_pde_def objBits_simps archObjSize_def pdeBits_def)
apply simp
apply (rule no_fail_cleanCacheRange_PoU)
apply (rule corres_split)
apply (rule storePDE_corres')
apply (clarsimp simp: pde_relation_aligned_def
dest!: valid_slots_duplicated_pdeD')
apply (rule corres_split[where r'=dc])
apply (rule corres_store_pde_with_invalid_tail)
apply (clarsimp dest!: valid_slots_duplicated_pdeD')
apply (rule corres_split[where r'=dc])
apply (rule corres_machine_op[OF corres_Id])
apply (simp add: last_byte_pde_def objBits_simps archObjSize_def pdeBits_def)
apply simp
apply (rule no_fail_cleanCacheRange_PoU)
apply (rule corres_split[where r'=dc, OF _ corres_return_eq_same[OF refl]])
apply (clarsimp simp: when_def)
apply (rule invalidate_tlb_by_asid_corres_ex)
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 (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 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)
@ -2386,12 +2399,13 @@ lemma performPageTableInvocation_corres:
apply (rule corres_guard_imp)
apply (rule corres_split[OF updateCap_same_master])
apply assumption
apply (rule corres_split[OF storePDE_corres'])
apply (rule corres_machine_op)
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_cleanByVA_PoU)
apply (rule corres_split)
apply (rule storePDE_corres')
apply (simp add: pde_relation_aligned_def)
apply (wp set_cap_typ_at)+
apply (rule corres_machine_op)
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_cleanByVA_PoU)
apply (wp set_cap_typ_at)+
apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state is_arch_update_def)
apply (clarsimp simp: is_cap_simps cap_master_cap_simps
dest!: cap_master_cap_eqDs)
@ -2409,20 +2423,20 @@ lemma performPageTableInvocation_corres:
apply (simp add: case_option_If2 getSlotCap_def split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (simp add: liftM_def)
apply (rule corres_split[OF get_cap_corres])
apply (rule_tac F="is_pt_cap x" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_pt_cap_def update_map_data_def)
apply (wp get_cap_wp)+
apply (rule corres_if[OF refl])
apply (rule corres_split[OF unmapPageTable_corres])
apply (rule corres_split_nor)
apply (rule corres_if[OF refl _ corres_trivial])
apply (rule corres_split[OF unmapPageTable_corres])
apply (rule corres_split_nor)
apply (simp add: pteBits_def)+
apply (rule clear_page_table_corres)
apply (rule corres_machine_op, rule corres_Id)
apply (simp add: pteBits_def)+
apply (rule clear_page_table_corres)
apply wp+
apply (rule corres_trivial, simp)
apply wpsimp+
apply (simp add: liftM_def)
apply (rule corres_split[OF get_cap_corres])
apply (rule_tac F="is_pt_cap x" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_pt_cap_def update_map_data_def)
apply (wp get_cap_wp)
apply wp
apply (simp add: cte_wp_at_caps_of_state pred_conj_def
split del: if_split)
apply (rule hoare_lift_Pf2[where f=caps_of_state])
@ -2436,7 +2450,7 @@ lemma performPageTableInvocation_corres:
apply (auto simp: valid_cap_def mask_def cap_master_cap_def
cap_rights_update_def acap_rights_update_def
split: option.split_asm)[1]
apply (auto simp: valid_pti'_def cte_wp_at_ctes_of)
apply (auto simp: valid_pti'_def cte_wp_at_ctes_of)
done
definition
@ -2463,6 +2477,7 @@ lemma performASIDPoolInvocation_corres:
apply (rename_tac word1 word2 prod)
apply (rule corres_guard_imp)
apply (rule corres_split[OF getSlotCap_corres])
apply simp
apply (rule_tac F="\<exists>p asid. rv = Structures_A.ArchObjectCap (ARM_A.PageDirectoryCap p asid)" in corres_gen_asm)
apply clarsimp
apply (rule_tac Q="valid_objs and pspace_aligned and pspace_distinct and asid_pool_at word2 and valid_etcbs and
@ -2487,8 +2502,7 @@ lemma performASIDPoolInvocation_corres:
apply (erule cte_wp_at_weakenE)
apply (clarsimp simp: is_cap_simps cap_master_cap_simps dest!: cap_master_cap_eqDs)
apply (wp getASID_wp)
apply (rule refl)
apply (wp get_cap_wp getCTE_wp)+
apply (wp get_cap_wp getCTE_wp)+
apply (clarsimp simp: valid_apinv_def cte_wp_at_def cap_master_cap_def is_pd_cap_def obj_at_def)
apply (clarsimp simp: a_type_def)
apply (clarsimp simp: cte_wp_at_ctes_of valid_apinv'_def)

View File

@ -118,12 +118,12 @@ lemma corres_symb_exec_l':
assumes y: "\<lbrace>Q\<rbrace> m \<lbrace>Q'\<rbrace>"
shows "corres_underlying sr nf nf' r (P and Q) P' (m >>= (\<lambda>rv. x rv)) y"
apply (rule corres_guard_imp)
apply (subst gets_bind_ign[symmetric], rule corres_split_deprecated)
apply (rule z)
apply (rule corres_noop3)
apply (erule x)
apply (rule gets_wp)
apply (rule non_fail_gets)
apply (subst gets_bind_ign[symmetric], rule corres_split)
apply (rule corres_noop3)
apply (erule x)
apply (rule gets_wp)
apply (rule non_fail_gets)
apply (rule z)
apply (rule y)
apply (rule gets_wp)
apply simp+
@ -136,16 +136,16 @@ lemma corres_symb_exec_r':
assumes nf: "nf' \<Longrightarrow> no_fail R' m"
shows "corres_underlying sr nf nf' r P (P' and Q' and R') x (m >>= (\<lambda>rv. y rv))"
apply (rule corres_guard_imp)
apply (subst gets_bind_ign[symmetric], rule corres_split_deprecated)
apply (rule z)
apply (rule_tac P'="a' and a''" for a' a'' in corres_noop3)
apply (simp add: simpler_gets_def exs_valid_def)
apply (subst gets_bind_ign[symmetric], rule corres_split)
apply (rule_tac P'="a' and a''" for a' a'' in corres_noop3)
apply (simp add: simpler_gets_def exs_valid_def)
apply clarsimp
apply (erule x)
apply (rule no_fail_pre)
apply (erule nf)
apply clarsimp
apply (erule x)
apply (rule no_fail_pre)
apply (erule nf)
apply clarsimp
apply assumption
apply assumption
apply (rule z)
apply (rule gets_wp)
apply (rule y)
apply simp+