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

arm-hyp refine: update for changed corres split rules 

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis 2022-10-05 12:28:12 +11:00 committed by Gerwin Klein
parent e23c379720
commit b614d7ec9c
19 changed files with 2885 additions and 2824 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -153,89 +153,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
@ -527,6 +527,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;
clarsimp simp: master_pde_relation_def pde_relation'_def isSuperSection_def' page_base_def
split: if_split_asm)

22
proof/refine/ARM_HYP/Bits_R.thy
View File

@ -234,14 +234,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:
@ -427,9 +426,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
@ -468,11 +466,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

306
proof/refine/ARM_HYP/CNodeInv_R.thy
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
@ -6792,9 +6789,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)
@ -8765,8 +8762,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)
@ -8794,27 +8791,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)
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)
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)+

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

@ -3927,10 +3927,7 @@ lemma getCTE_get:
done
lemma setUntypedCapAsFull_corres:
"\<lbrakk>cap_relation c c'; src' = cte_map src; dest' = cte_map dest;
cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap;
cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer \<and>
mdbNext (cteMDBNode rv') = nullPointer\<rbrakk>
"\<lbrakk>cap_relation c c'; cap_relation src_cap (cteCap srcCTE)\<rbrakk>
\<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and
pspace_aligned and pspace_distinct)
(cte_wp_at' ((=) srcCTE) (cte_map src) and
@ -5204,193 +5201,148 @@ 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 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: cte_wp_at_ctes_of nullPointer_def
prev_update_modify_mdb_relation)
apply (subgoal_tac "cte_map dest \<noteq> 0")
prefer 2
subgoal by (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
apply (subgoal_tac "cte_map src \<noteq> 0")
prefer 2
subgoal by (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)
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
apply (thin_tac "gsCNodes t = p" for t p)+
apply (thin_tac "ksWorkUnitsCompleted 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)
defer
apply(rule conjI)
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 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 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: cte_wp_at_ctes_of nullPointer_def
prev_update_modify_mdb_relation)
apply (subgoal_tac "cte_map dest \<noteq> 0")
prefer 2
subgoal by (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
apply (subgoal_tac "cte_map src \<noteq> 0")
prefer 2
subgoal by (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)
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
apply (thin_tac "gsCNodes t = p" for t p)+
apply (thin_tac "ksWorkUnitsCompleted 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)
defer
apply(rule conjI)
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)
@ -5398,10 +5350,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)
@ -5413,7 +5365,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)
@ -5423,123 +5375,117 @@ 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')
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)
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)
@ -5550,9 +5496,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)
@ -5560,59 +5506,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 (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 (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)
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 (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)+
@ -5672,12 +5666,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)

265
proof/refine/ARM_HYP/CSpace_R.thy
View File

@ -3493,11 +3493,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
@ -4795,135 +4795,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)+
@ -4939,7 +4937,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

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

@ -654,7 +654,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)+

14
proof/refine/ARM_HYP/Finalise_R.thy
View File

@ -3907,8 +3907,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
@ -3933,8 +3933,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
@ -3996,10 +3996,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

18
proof/refine/ARM_HYP/InterruptAcc_R.thy
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)

396
proof/refine/ARM_HYP/Interrupt_R.thy
View File

@ -220,16 +220,18 @@ 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
wp_del: arch_check_irq_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[OF ensureEmptySlot_corres])
apply 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
wp_del: arch_check_irq_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
@ -272,15 +274,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
@ -479,13 +483,12 @@ lemma arch_performIRQControl_corres:
apply (cases x2; simp add: ARM_HYP_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)
@ -506,9 +509,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)
@ -637,73 +640,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
lemma corres_return_VGICMaintenance [corres]:
@ -823,65 +826,69 @@ proof -
apply (rule corres_trivial, simp)
apply clarsimp
apply (rule corres_split_eqr[OF corres_machine_op])+
apply (rename_tac eisr0 eisr1 flags)
apply (rule corres_split[OF corres_gets_numlistregs])
apply (rule corres_split_deprecated[where r'="\<lambda>rv rv'. rv' = arch_fault_map rv"])
apply (rule corres_split_eqr[OF getCurThread_corres])
apply (rule corres_split[OF getThreadState_corres])
apply (fold dc_def)
apply (rule corres_when)
apply clarsimp
apply (rename_tac threadState threadState')
apply (case_tac threadState; simp)
apply (rule handleFault_corres)
apply clarsimp
apply clarsimp
apply (wp gts_wp)
apply (wp gts_wp')
apply (rule corres_split_eqr[OF corres_machine_op],
(rule corres_Id; wpsimp simp: get_gic_vcpu_ctrl_misr_def
get_gic_vcpu_ctrl_eisr1_def
get_gic_vcpu_ctrl_eisr0_def))+
apply (rename_tac eisr0 eisr1 flags)
apply (rule corres_split[OF corres_gets_numlistregs])
apply (rule corres_split[where r'="\<lambda>rv rv'. rv' = arch_fault_map rv"])
apply (rule corres_if[rotated -1])
apply (rule corres_trivial, simp)
apply clarsimp
apply (rule corres_if, simp)
apply (rule corres_trivial, simp)
supply if_split[split del]
apply (clarsimp simp: bind_assoc cong: if_cong)
apply (rule corres_split_eqr[OF corres_machine_op])
apply (rule corres_Id; wpsimp)
apply (rule corres_split_dc[OF corres_machine_op])
apply (rule corres_Id; wpsimp)
apply clarsimp
apply (rule_tac
Q="\<lambda>rv. tcb_at rv and einvs
and (\<lambda>_. valid_fault (ExceptionTypes_A.fault.ArchFault rva))"
in hoare_post_imp)
apply (clarsimp cong: imp_cong conj_cong simp: not_pred_tcb runnable_eq pred_conj_def)
apply (strengthen st_tcb_ex_cap'[where P=active], clarsimp)
apply (clarsimp simp: pred_tcb_at_def obj_at_def)
apply wp
apply clarsimp
apply (rule_tac Q="\<lambda>rv x. tcb_at' rv x
\<and> invs' x
\<and> sch_act_not rv x
\<and> (\<forall>d p. rv \<notin> set (ksReadyQueues x (d, p)))"
in hoare_post_imp)
apply (rule corres_split_dc[OF vgicUpdateLR_corres])
apply (rule corres_trivial, simp)
apply wpsimp+
apply (rule corres_split_eqr[OF getCurThread_corres])
apply (rule corres_split[OF getThreadState_corres])
apply (fold dc_def)
apply (rule corres_when)
apply clarsimp
apply (strengthen st_tcb_ex_cap''[where P=active'])
apply (strengthen invs_iflive')
apply (clarsimp cong: imp_cong conj_cong simp: not_pred_tcb')
apply (clarsimp simp: pred_tcb_at'_def)
apply (rule conjI, erule_tac p=r in obj_at'_weakenE
, fastforce split: thread_state.splits)
apply (erule_tac p=r in obj_at'_weakenE, fastforce split: thread_state.splits)
apply wp
apply (rule corres_if[rotated -1])
apply (rule corres_trivial, simp)
apply (rename_tac threadState threadState')
apply (case_tac threadState; simp)
apply (rule handleFault_corres)
apply clarsimp
apply (rule corres_if, simp)
apply (rule corres_trivial, simp)
supply if_split[split del]
apply (clarsimp simp: bind_assoc cong: if_cong)
apply (rule corres_split_eqr[OF corres_machine_op])
apply (rule corres_split_dc[OF corres_machine_op])
apply clarsimp
apply (rule corres_split_dc[OF vgicUpdateLR_corres])
apply (rule corres_trivial, simp)
supply corres_return[simp del]
apply (wpsimp wp: corres_Id wplr wplr' hoare_vcg_all_lift
hoare_vcg_imp_lift' dmo_gets_wp dmo'_gets_wp
simp: get_gic_vcpu_ctrl_misr_def if_apply_def2
get_gic_vcpu_ctrl_eisr1_def
get_gic_vcpu_ctrl_eisr0_def
| strengthen tcb_at_invs tcb_at_invs')+
apply clarsimp
apply (wp gts_wp)
apply (wp gts_wp')
apply (rule_tac
Q="\<lambda>rv. tcb_at rv and einvs
and (\<lambda>_. valid_fault (ExceptionTypes_A.fault.ArchFault rva))"
in hoare_post_imp)
apply (clarsimp cong: imp_cong conj_cong simp: not_pred_tcb runnable_eq pred_conj_def)
apply (strengthen st_tcb_ex_cap'[where P=active], clarsimp)
apply (clarsimp simp: pred_tcb_at_def obj_at_def)
apply wp
apply clarsimp
apply (rule_tac Q="\<lambda>rv x. tcb_at' rv x
\<and> invs' x
\<and> sch_act_not rv x
\<and> (\<forall>d p. rv \<notin> set (ksReadyQueues x (d, p)))"
in hoare_post_imp)
apply clarsimp
apply (strengthen st_tcb_ex_cap''[where P=active'])
apply (strengthen invs_iflive')
apply (clarsimp cong: imp_cong conj_cong simp: not_pred_tcb')
apply (clarsimp simp: pred_tcb_at'_def)
apply (rule conjI, erule_tac p=r in obj_at'_weakenE
, fastforce split: thread_state.splits)
apply (erule_tac p=r in obj_at'_weakenE, fastforce split: thread_state.splits)
apply wp
apply (wpsimp wp: wplr wplr' hoare_vcg_all_lift
hoare_vcg_imp_lift' dmo_gets_wp dmo'_gets_wp
simp: get_gic_vcpu_ctrl_misr_def if_apply_def2
get_gic_vcpu_ctrl_eisr1_def
get_gic_vcpu_ctrl_eisr0_def
| strengthen tcb_at_invs tcb_at_invs')+
apply (frule invs_arch_state)
apply (clarsimp simp: valid_arch_state_def valid_fault_def tcb_at_invs obj_at_def is_vcpu_def)
@ -911,47 +918,47 @@ lemma vppiEvent_corres:
apply clarsimp
apply (rule corres_split_dc[OF corres_machine_op])
apply (rule corres_split_dc[OF vcpuUpdate_corres])
apply (rule corres_split_eqr[OF getCurThread_corres])
apply (rule corres_split[OF getThreadState_corres], rename_tac gts gts')
apply (fold dc_def)
apply (rule corres_when)
apply (case_tac gts; fastforce)
apply (rule handleFault_corres, simp)
apply (wp gts_st_tcb_at hoare_vcg_imp_lift')
apply (wp gts_st_tcb_at' hoare_vcg_imp_lift')
(* on both sides, we check that the current thread is runnable, then have to know it
is runnable directly afterwards, which is obvious and should not propagate further;
clean up the postconditions of the thread_get and threadGet *)
apply (rule_tac
Q="\<lambda>rv. tcb_at rv and einvs
and (\<lambda>_. valid_fault (ExceptionTypes_A.fault.ArchFault
(ARM_A.VPPIEvent irq)))"
in hoare_post_imp)
apply (clarsimp cong: imp_cong conj_cong simp: not_pred_tcb runnable_eq pred_conj_def)
apply (strengthen st_tcb_ex_cap'[where P=active], clarsimp)
apply wp
apply (clarsimp cong: imp_cong conj_cong simp: pred_conj_def)
apply (rule_tac Q="\<lambda>rv x. tcb_at' rv x
\<and> invs' x
\<and> sch_act_not rv x
\<and> (\<forall>d p. rv \<notin> set (ksReadyQueues x (d, p)))" in hoare_post_imp)
apply (strengthen st_tcb_ex_cap''[where P=active'])
apply (strengthen invs_iflive')
apply (clarsimp cong: imp_cong conj_cong simp: not_pred_tcb')
apply (clarsimp simp: pred_tcb_at'_def)
apply (rule conjI, erule_tac p=r in obj_at'_weakenE, fastforce split: thread_state.splits)
apply (erule_tac p=r in obj_at'_weakenE, fastforce split: thread_state.splits)
apply wp
apply (rule corres_Id; wpsimp)
apply (rule corres_split_dc[OF vcpuUpdate_corres])
apply (fastforce simp: vcpu_relation_def irq_vppi_event_index_def
irqVPPIEventIndex_def IRQ_def)
apply (wpsimp wp: vcpu_update_tcb_at hoare_vcg_all_lift hoare_vcg_imp_lift'
cong: vcpu.fold_congs)+
apply (strengthen tcb_at_invs)
apply (wpsimp wp: dmo_maskInterrupt_True maskInterrupt_invs corres_Id
setVCPU_VPPIMasked_invs' simp: vcpuUpdate_def
| wps)+
apply (rule corres_split_eqr[OF getCurThread_corres])
apply (rule corres_split[OF getThreadState_corres], rename_tac gts gts')
apply (fold dc_def)
apply (rule corres_when)
apply (case_tac gts; fastforce)
apply (rule handleFault_corres, simp)
apply (wp gts_st_tcb_at hoare_vcg_imp_lift')
apply (wp gts_st_tcb_at' hoare_vcg_imp_lift')
(* on both sides, we check that the current thread is runnable, then have to know it
is runnable directly afterwards, which is obvious and should not propagate further;
clean up the postconditions of the thread_get and threadGet *)
apply (rule_tac
Q="\<lambda>rv. tcb_at rv and einvs
and (\<lambda>_. valid_fault (ExceptionTypes_A.fault.ArchFault
(ARM_A.VPPIEvent irq)))"
in hoare_post_imp)
apply (clarsimp cong: imp_cong conj_cong simp: not_pred_tcb runnable_eq pred_conj_def)
apply (strengthen st_tcb_ex_cap'[where P=active], clarsimp)
apply wp
apply (clarsimp cong: imp_cong conj_cong simp: pred_conj_def)
apply (rule_tac Q="\<lambda>rv x. tcb_at' rv x
\<and> invs' x
\<and> sch_act_not rv x
\<and> (\<forall>d p. rv \<notin> set (ksReadyQueues x (d, p)))" in hoare_post_imp)
apply (strengthen st_tcb_ex_cap''[where P=active'])
apply (strengthen invs_iflive')
apply (clarsimp cong: imp_cong conj_cong simp: not_pred_tcb')
apply (clarsimp simp: pred_tcb_at'_def)
apply (rule conjI, erule_tac p=r in obj_at'_weakenE, fastforce split: thread_state.splits)
apply (erule_tac p=r in obj_at'_weakenE, fastforce split: thread_state.splits)
apply wp
apply (wpsimp wp: vcpu_update_tcb_at hoare_vcg_all_lift hoare_vcg_imp_lift'
cong: vcpu.fold_congs)+
apply (strengthen tcb_at_invs)
apply (wpsimp wp: dmo_maskInterrupt_True maskInterrupt_invs
setVCPU_VPPIMasked_invs' simp: vcpuUpdate_def
| wps)+
apply (frule invs_arch_state)
apply (simp add: valid_arch_state_def valid_fault_def tcb_at_invs)
apply (clarsimp simp: obj_at_def is_vcpu_def)
@ -996,7 +1003,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)
@ -1015,7 +1022,7 @@ 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)+
apply (clarsimp simp: 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+
@ -1026,13 +1033,12 @@ lemma handleInterrupt_corres:
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, wpsimp+)
apply (rule corres_machine_op)
apply (rule corres_eq_trivial, (simp add: no_fail_ackInterrupt)+)
apply wp+
apply clarsimp
apply clarsimp
apply corressimp

195
proof/refine/ARM_HYP/IpcCancel_R.thy
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)+
@ -1253,20 +1253,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:
@ -1424,23 +1425,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_HYP.nextInstructionRegister_def ARM_HYP.faultRegister_def
ARM_HYP_H.nextInstructionRegister_def ARM_HYP_H.faultRegister_def)
apply (simp add: ARM_HYP_H.Register_def)
apply (subst unit_dc_is_eq)
apply (rule corres_underlying_trivial)
apply (wpsimp simp: ARM_HYP.setRegister_def ARM_HYP.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_HYP.nextInstructionRegister_def ARM_HYP.faultRegister_def
ARM_HYP_H.nextInstructionRegister_def ARM_HYP_H.faultRegister_def)
apply (simp add: ARM_HYP_H.Register_def)
apply (subst unit_dc_is_eq)
apply (rule corres_underlying_trivial)
apply (wpsimp simp: ARM_HYP.setRegister_def ARM_HYP.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
@ -2082,7 +2081,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
@ -2093,10 +2092,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
@ -2128,7 +2127,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)+
@ -2140,11 +2139,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)
@ -2168,8 +2167,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)
@ -2181,23 +2180,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)+
@ -2778,18 +2775,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"
@ -2802,26 +2796,31 @@ 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+
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 simp
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 (wp 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 weak_sch_act_wf_lift_linear set_ep_valid_objs'
| simp)+
apply (clarsimp simp: conj_comms)
apply (frule sym_refs_ko_atD, clarsimp+)
apply (rule obj_at_valid_objsE, assumption+, clarsimp+)

893
proof/refine/ARM_HYP/Ipc_R.thy
View File

File diff suppressed because it is too large Load Diff

27
proof/refine/ARM_HYP/Refine.thy
View File

@ -601,14 +601,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
@ -695,13 +695,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

107
proof/refine/ARM_HYP/Retype_R.thy
View File

@ -1435,16 +1435,20 @@ lemma objBitsKO_gt_0: "0 < objBitsKO ko"
apply (simp_all add:archObjSize_def vcpu_bits_def vspace_bits_defs)
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
@ -1800,19 +1804,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)
@ -5331,19 +5335,19 @@ lemma corres_retype_region_createNewCaps:
split del: if_split)[10] (* 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
@ -5479,23 +5483,19 @@ lemma corres_retype_region_createNewCaps:
apply simp+
defer
\<comment> \<open>PageDirectory\<close>
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
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
default_arch_object_def objBits_simps
archObjSize_def vspace_bits_defs
makeObjectKO_def)[1]
apply (simp add: range_cover_def)+
apply (rule pagedirectory_relation_retype)
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
vspace_bits_defs)
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)
@ -5510,15 +5510,18 @@ lemma corres_retype_region_createNewCaps:
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
default_arch_object_def objBits_simps
archObjSize_def vspace_bits_defs
makeObjectKO_def)[1]
apply (simp add: range_cover_def)+
apply (rule pagedirectory_relation_retype)
apply (wp | simp)+
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
vspace_bits_defs)
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

209
proof/refine/ARM_HYP/Schedule_R.thy
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
@ -140,15 +140,14 @@ lemma arch_switchToThread_corres:
apply (rule corres_guard_imp)
apply (rule corres_split[OF get_tcb_corres])
apply (rule corres_split[OF vcpuSwitch_corres'])
apply (simp add: tcb_relation_def arch_tcb_relation_def)
apply (rule corres_split[OF setVMRoot_corres])
apply (rule corres_machine_op[OF corres_rel_imp])
apply (rule corres_underlying_trivial)
apply wpsimp
apply (clarsimp simp: ARM_HYP.clearExMonitor_def)+
apply wpsimp
apply (clarsimp simp: tcb_relation_def arch_tcb_relation_def)
apply (rule corres_split[OF setVMRoot_corres])
apply (rule corres_machine_op[OF corres_rel_imp])
apply (rule corres_underlying_trivial)
apply wpsimp
apply (clarsimp simp: ARM_HYP.clearExMonitor_def)+
apply wpsimp
apply (clarsimp simp: tcb_relation_def arch_tcb_relation_def)
apply wpsimp
apply (wpsimp wp: tcb_at_typ_at simp:)
apply (wpsimp simp: ARM_HYP.clearExMonitor_def wp: tcb_at_typ_at)+
apply (wp getObject_tcb_hyp_sym_refs)
@ -199,21 +198,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
@ -1821,11 +1829,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
@ -1945,69 +1953,72 @@ lemma schedule_corres:
apply clarsimp
apply (rule corres_split[OF thread_get_isRunnable_corres])
apply (rule corres_split[OF corres_when])
apply (rule scheduleChooseNewThread_corres, simp)
apply (rule tcbSchedEnqueue_corres, simp)
apply simp
apply (rule tcbSchedEnqueue_corres)
apply (rule scheduleChooseNewThread_corres, simp)
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 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[OF ethreadget_corres[where r="(=)"]])
apply (simp add: etcb_relation_def)
apply (rename_tac tp tp')
apply (rule corres_split[OF ethread_get_when_corres[where r="(=)"]])
apply (simp add: 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[OF setSchedulerAction_corres])
apply 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 (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_if, fastforce)
apply (rule corres_split[OF tcbSchedAppend_corres])
apply (simp, fold dc_def)
apply (rule corres_split[OF setSchedulerAction_corres])
apply simp
apply (rule scheduleChooseNewThread_corres)
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 (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)+
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+
(* 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 (clarsimp simp: conj_ac cong: conj_cong)
apply wp
apply (rule_tac Q="\<lambda>_ s. valid_blocked_except t s \<and> scheduler_action s = switch_thread t"
@ -2395,18 +2406,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

256
proof/refine/ARM_HYP/Syscall_R.thy
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
@ -360,17 +361,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"
@ -407,60 +409,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])
@ -1248,24 +1251,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)
@ -1518,17 +1523,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)
@ -1536,31 +1540,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
@ -2066,14 +2074,14 @@ proof -
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 (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 (rule corres_machine_op)
apply (rule corres_Id; wpsimp)
apply (case_tac rv, simp_all add: doMachineOp_return)[1]
apply (rule handleInterrupt_corres)
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 (clarsimp simp: invs'_def valid_state'_def ct_not_inQ_def valid_queues_def
@ -2084,8 +2092,8 @@ proof -
apply (rule_tac corres_underlying_split)
apply (rule corres_guard_imp, rule getCurThread_corres, simp+)
apply (rule corres_split_catch)
apply (erule handleFault_corres)
apply (rule handleVMFault_corres)
apply (rule handleVMFault_corres)
apply (erule handleFault_corres)
apply (wp handle_vm_fault_valid_fault)
apply (wp hvmf_invs_etc)
apply wp

339
proof/refine/ARM_HYP/TcbAcc_R.thy
View File

@ -423,10 +423,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
@ -1381,22 +1381,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
@ -1874,21 +1874,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
@ -1922,13 +1928,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
@ -2075,15 +2082,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 =
@ -2113,21 +2124,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
@ -3241,21 +3251,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)
@ -3310,7 +3321,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
@ -3320,21 +3331,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
@ -3410,11 +3421,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
@ -3423,21 +3434,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:
@ -3503,23 +3516,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
@ -3606,39 +3620,39 @@ lemma lookupIPCBuffer_corres':
apply (simp add: lookup_ipc_buffer_def ARM_HYP_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
@ -4536,11 +4550,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':

378
proof/refine/ARM_HYP/Tcb_R.thy
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>"
@ -282,18 +283,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)
@ -403,12 +403,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>
@ -439,36 +439,36 @@ proof -
apply (rule corres_guard_imp)
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_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)+
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 (solves \<open>wp static_imp_wp\<close>)+
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)+)[4]
apply ((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
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
qed
lemma readreg_invs':
@ -626,19 +626,19 @@ 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 wp
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 wp
apply clarsimp
apply (wp static_imp_wp hoare_vcg_if_lift hoare_wp_combs gts_wp)
apply wp
apply clarsimp
apply (wp hoare_vcg_if_lift static_imp_wp hoare_wp_combs isRunnable_wp)
apply (simp add: etcb_relation_def)
apply (wp static_imp_wp hoare_vcg_if_lift hoare_wp_combs gts_wp)
apply clarsimp
apply (wp hoare_vcg_if_lift static_imp_wp hoare_wp_combs isRunnable_wp)
apply (wp hoare_vcg_imp_lift' hoare_vcg_if_lift hoare_vcg_all_lift)
apply clarsimp
apply (wp hoare_drop_imps)
@ -1428,19 +1428,18 @@ 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 (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 (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
@ -1450,15 +1449,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)+
@ -1533,11 +1532,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
@ -1842,9 +1841,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)
@ -2050,16 +2049,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
@ -2076,11 +2075,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:
@ -2095,11 +2094,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 valid_objs'_maxPriority':
@ -2212,12 +2211,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:
@ -2273,7 +2273,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 +2373,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_HYP_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_HYP_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 +2513,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 +2572,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 +2597,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 +2635,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

508
proof/refine/ARM_HYP/Untyped_R.thy
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
@ -297,108 +296,108 @@ next
apply (rule whenE_throwError_corres, simp)
apply (clarsimp simp: fromAPIType_def ARM_HYP_H.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 simp
apply (rule corres_returnOkTT)
apply (rule crel)
apply simp
apply (rule corres_splitEE[OF 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)+
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 (wp hoare_drop_impE_R hoare_vcg_all_lift_R
| clarsimp)+
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
@ -411,17 +410,17 @@ next
apply wp+
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 )
done
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
lemma decodeUntyped_inv[wp]:
@ -932,11 +931,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+
@ -1533,16 +1532,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)
@ -4233,128 +4233,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)
@ -4892,14 +4895,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)

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

File diff suppressed because it is too large Load Diff