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

x64 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-04 11:20:19 +11:00 committed by Gerwin Klein
parent 7289575cc7
commit e23c379720
20 changed files with 2634 additions and 2577 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
proof/refine/X64/ArchAcc_R.thy
View File

@ -1296,7 +1296,6 @@ lemma lookupPDSlot_corres:
apply (rule corres_split_eqrE[OF lookupPDPTSlot_corres])
apply (rule corres_splitEE
[where R'="\<lambda>_. pspace_distinct'" and R="\<lambda>r. valid_pdpte r and pspace_aligned"])
prefer 2
apply (simp, rule getObject_PDPTE_corres')
apply (case_tac pdpte; simp add: lookup_failure_map_def bit_simps lookupPDSlotFromPD_def
split: pdpte.splits)
@ -1342,7 +1341,6 @@ lemma lookupPTSlot_corres:
apply (rule corres_split_eqrE[OF lookupPDSlot_corres])
apply (rule corres_splitEE
[where R'="\<lambda>_. pspace_distinct'" and R="\<lambda>r. valid_pde r and pspace_aligned"])
prefer 2
apply (simp, rule getObject_PDE_corres')
apply (case_tac pde; simp add: lookup_failure_map_def bit_simps lookupPTSlotFromPT_def
split: pde.splits)
@ -1513,28 +1511,28 @@ lemma createMappingEntries_corres:
apply (cases pgsz, simp_all add: createMappingEntries_def mapping_map_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqrE)
apply (rule corres_returnOkTT)
apply (clarsimp simp: vmattributes_map_def mapping_map_simps)
apply (rule corres_lookup_error)
apply (rule lookupPTSlot_corres)
apply (rule corres_returnOkTT)
apply (clarsimp simp: vmattributes_map_def mapping_map_simps)
apply wp+
apply clarsimp
apply simp+
apply (rule corres_guard_imp)
apply (rule corres_split_eqrE)
apply (rule corres_returnOkTT)
apply (clarsimp simp: vmattributes_map_def mapping_map_simps)
apply (rule corres_lookup_error)
apply (rule lookupPDSlot_corres)
apply (rule corres_returnOkTT)
apply (clarsimp simp: vmattributes_map_def mapping_map_simps)
apply wp+
apply clarsimp
apply simp+
apply (rule corres_guard_imp)
apply (rule corres_split_eqrE)
apply (rule corres_returnOkTT)
apply (clarsimp simp: vmattributes_map_def mapping_map_simps)
apply (rule corres_lookup_error)
apply (rule lookupPDPTSlot_corres)
apply (rule corres_returnOkTT)
apply (clarsimp simp: vmattributes_map_def mapping_map_simps)
apply wp+
apply clarsimp
apply simp

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

@ -156,8 +156,12 @@ 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 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 (rule corres_split)
apply (simp add: retype_region2_ext_retype_region_ArchObject )
apply (rule corres_retype [where ty="Inl (KOArch (KOASIDPool F))" for F,
@ -212,9 +216,6 @@ lemma performASIDControlInvocation_corres:
apply (rule descendants_of'_helper)
apply (wp createObjects_null_filter'
[where sz = pageBits and ty="Inl (KOArch (KOASIDPool undefined))"])
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)
@ -924,14 +925,13 @@ lemma ensurePortOperationAllowed_corres:
apply (rule corres_gen_asm)
apply (rule corres_guard_imp)
apply (rule corres_split_eqrE)
apply (rule corres_assertE_assume; (rule impI, assumption))
apply (rule corres_split_eqrE)
apply (rule corres_assertE_assume)
apply (rule impI, assumption)+
apply (rule corres_whenE, simp)
apply clarsimp
apply clarsimp
apply (rule corres_assertE_assume)
apply (rule impI, assumption)+
apply wp+
apply (rule corres_assertE_assume; (rule impI, assumption))
apply wp+
apply (clarsimp simp: valid_cap_def; elim disjE; clarsimp)
apply (subst add.commute, subst no_olen_add, simp add: word_le_def)+
@ -957,9 +957,9 @@ lemma decode_port_inv_corres:
apply (clarsimp simp: neq_Nil_conv)
apply (rule corres_guard_imp)
apply (rule corres_split_norE)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply (rule corres_returnOkTT)
apply (clarsimp simp: archinv_relation_def ioport_invocation_map_def ioport_data_relation_def)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply wpsimp+
apply (cases "invocation_type label = ArchInvocationLabel X64IOPortIn16")
apply (simp add: Let_def isCap_simps whenE_def)
@ -967,9 +967,9 @@ lemma decode_port_inv_corres:
apply (clarsimp simp: neq_Nil_conv)
apply (rule corres_guard_imp)
apply (rule corres_split_norE)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply (rule corres_returnOkTT)
apply (clarsimp simp: archinv_relation_def ioport_invocation_map_def ioport_data_relation_def)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply wpsimp+
apply (cases "invocation_type label = ArchInvocationLabel X64IOPortIn32")
apply (simp add: Let_def isCap_simps whenE_def)
@ -977,36 +977,36 @@ lemma decode_port_inv_corres:
apply (clarsimp simp: neq_Nil_conv)
apply (rule corres_guard_imp)
apply (rule corres_split_norE)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply (rule corres_returnOkTT)
apply (clarsimp simp: archinv_relation_def ioport_invocation_map_def ioport_data_relation_def)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply wpsimp+
apply (cases "invocation_type label = ArchInvocationLabel X64IOPortOut8")
apply (simp add: Let_def isCap_simps whenE_def)
apply (clarsimp simp: neq_Nil_conv split: list.splits)+
apply (rule corres_guard_imp)
apply (rule corres_split_norE)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply (rule corres_returnOkTT)
apply (clarsimp simp: archinv_relation_def ioport_invocation_map_def ioport_data_relation_def)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply wpsimp+
apply (cases "invocation_type label = ArchInvocationLabel X64IOPortOut16")
apply (simp add: Let_def isCap_simps whenE_def)
apply (clarsimp simp: neq_Nil_conv split: list.splits)+
apply (rule corres_guard_imp)
apply (rule corres_split_norE)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply (rule corres_returnOkTT)
apply (clarsimp simp: archinv_relation_def ioport_invocation_map_def ioport_data_relation_def)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply wpsimp+
apply (cases "invocation_type label = ArchInvocationLabel X64IOPortOut32")
apply (simp add: Let_def isCap_simps whenE_def)
apply (clarsimp simp: neq_Nil_conv split: list.splits)+
apply (rule corres_guard_imp)
apply (rule corres_split_norE)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply (rule corres_returnOkTT)
apply (clarsimp simp: archinv_relation_def ioport_invocation_map_def ioport_data_relation_def)
apply (rule ensurePortOperationAllowed_corres, simp, simp)
apply wpsimp+
apply (clarsimp simp: isCap_simps Let_def split: arch_invocation_label.splits invocation_label.splits)
done
@ -1064,23 +1064,23 @@ lemma decodeX64PortInvocation_corres:
apply clarsimp
apply clarsimp
apply (rule corres_split_eqr[OF isIOPortRangeFree_corres])
apply (clarsimp simp: word_le_not_less)
apply (clarsimp simp: unlessE_whenE)
apply (rule whenE_throwError_corres)
apply clarsimp
apply clarsimp
apply (clarsimp simp: lookupTargetSlot_def)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rule corres_splitEE[OF ensureEmptySlot_corres])
apply (rule corres_returnOkTT)
apply (clarsimp simp: archinv_relation_def ioport_control_inv_relation_def)
apply clarsimp
apply wp
apply wp
apply (clarsimp simp: cap_relation_def)
apply clarsimp
apply (rule corres_splitEE[OF ensureEmptySlot_corres])
apply clarsimp
apply (rule corres_returnOkTT)
apply (clarsimp simp: archinv_relation_def ioport_control_inv_relation_def)
apply wp
apply wp
apply wpsimp
apply wpsimp
apply (clarsimp simp: word_le_not_less)
apply clarsimp
apply (wpsimp wp: is_ioport_range_free_wp)
apply clarsimp
@ -1299,7 +1299,6 @@ lemma port_in_corres[corres]:
apply (clarsimp simp: port_in_def portIn_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply wpsimp
apply (rule corres_machine_op[OF corres_Id], simp+)
by wpsimp+
@ -1308,7 +1307,6 @@ lemma port_out_corres[@lift_corres_args, corres]:
apply (clarsimp simp: port_out_def portOut_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply wpsimp
apply (rule corres_machine_op[OF corres_Id], simp+)
apply wpsimp+
done
@ -1360,10 +1358,10 @@ lemma performX64PortInvocation_corres:
apply (rule corres_guard_imp)
apply (rule corres_split_nor[OF set_ioport_mask_corres])
apply (rule corres_split_nor[OF cteInsert_simple_corres])
apply (rule corres_return_eq_same, simp)
apply (clarsimp simp: cap_relation_def)
apply simp
apply simp
apply (rule corres_return_eq_same, simp)
apply wpsimp
apply wpsimp
apply (clarsimp simp: is_simple_cap_def is_cap_simps)
@ -1421,20 +1419,23 @@ lemma arch_performInvocation_corres:
apply (clarsimp simp: performX64MMUInvocation_def)
apply (cases ai)
apply (clarsimp simp: archinv_relation_def performX64MMUInvocation_def)
apply (rule corres_guard_imp, rule corres_split_nor, rule corres_trivial, simp)
apply (rule corres_guard_imp, rule corres_split_nor)
apply (rule performPageTableInvocation_corres; wpsimp)
apply (rule corres_trivial, simp)
apply wpsimp+
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_guard_imp, rule corres_split_nor, rule corres_trivial, simp)
apply (rule corres_guard_imp, rule corres_split_nor)
apply (rule performPageDirectoryInvocation_corres; wpsimp)
apply (rule corres_trivial, simp)
apply wpsimp+
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_guard_imp, rule corres_split_nor, rule corres_trivial, simp)
apply (rule corres_guard_imp, rule corres_split_nor)
apply (rule performPDPTInvocation_corres; wpsimp)
apply (rule corres_trivial, simp)
apply wpsimp+
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
@ -1445,14 +1446,16 @@ lemma arch_performInvocation_corres:
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_guard_imp, rule corres_split_nor, rule corres_trivial, simp)
apply (rule corres_guard_imp, rule corres_split_nor)
apply (rule performASIDControlInvocation_corres; wpsimp)
apply (rule corres_trivial, simp)
apply wpsimp+
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_guard_imp, rule corres_split_nor, rule corres_trivial, simp)
apply (rule corres_guard_imp, rule corres_split_nor)
apply (rule performASIDPoolInvocation_corres; wpsimp)
apply (rule corres_trivial, simp)
apply wpsimp+
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)

18
proof/refine/X64/Bits_R.thy
View File

@ -242,14 +242,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 (rule wp_post_taut)
apply simp
apply simp
apply (case_tac v, (clarsimp simp: z)+)
apply (rule wp_post_taut)
apply (rule wp_post_taut)
apply simp
apply simp
done
lemma rethrowFailure_injection:
@ -430,9 +429,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 assumption
apply (rule corres_trivial, simp)
apply (erule corres_rel_imp)
apply (case_tac x; simp)
apply wp+
apply simp+
done
@ -470,11 +468,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 assumption
apply (rule corres_trivial, simp)
apply (erule corres_rel_imp)
apply (case_tac xa)
apply (clarsimp simp: const_def)
apply simp
apply wp+
apply simp+
done

90
proof/refine/X64/CNodeInv_R.thy
View File

@ -173,9 +173,12 @@ 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 (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)
@ -212,12 +215,11 @@ lemma decodeCNodeInvocation_corres:
\<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 (rule corres_guard_imp, rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (simp add: split_beta)
apply (rule corres_returnOkTT)
apply simp
apply simp
apply simp
apply wp+
apply (auto elim!: valid_cnode_capI)[1]
apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def)
@ -225,12 +227,11 @@ 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 (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (simp add: split_beta)
apply (rule corres_returnOkTT)
apply simp
apply simp
apply simp
apply wp+
apply (auto elim!: valid_cnode_capI)[1]
apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def)
@ -238,16 +239,13 @@ 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 (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
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 simp
apply simp
apply (rule corres_returnOkTT)
apply simp
apply (wp hoare_drop_imps)+
apply (auto elim!: valid_cnode_capI)[1]
@ -256,14 +254,15 @@ 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 (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'])
apply (rule corres_split[OF get_cap_corres'], simp)
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 (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)
@ -275,9 +274,10 @@ 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 (rule corres_guard_imp, rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (rename_tac dest_slot destSlot)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])+
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>])
@ -291,6 +291,20 @@ lemma decodeCNodeInvocation_corres:
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 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)
@ -308,29 +322,12 @@ lemma decodeCNodeInvocation_corres:
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 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 (auto elim!: valid_cnode_capI)[1]
@ -351,9 +348,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_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (rule corres_trivial, clarsimp split: list.split_asm)
apply simp+
apply wp+
apply (auto elim!: valid_cnode_capI)[1]
apply fastforce
@ -362,10 +359,10 @@ lemma decodeCNodeInvocation_corres:
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 simp
apply simp
apply (clarsimp simp: list_all2_Cons1 list_all2_Nil
split: list.split_asm split del: if_split)
apply simp
apply simp
apply (auto elim!: valid_cnode_capI)[1]
apply fastforce
done
@ -6865,9 +6862,9 @@ proof -
show ?thesis
unfolding spec_corres_def
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated)
apply (erule w)
apply (rule corres_split)
apply (rule x[unfolded spec_corres_def])
apply (erule w)
apply (wp z)
apply (rule univ_wp)
apply (rule z)
@ -8892,8 +8889,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)
@ -8925,6 +8922,7 @@ lemma invokeCNode_corres:
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

9
proof/refine/X64/CSpace1_R.thy
View File

@ -3926,7 +3926,7 @@ lemma getCTE_get:
done
lemma setUntypedCapAsFull_corres:
"\<lbrakk>cap_relation c c'; src' = cte_map src; dest' = cte_map dest;
"\<lbrakk>cap_relation c c'; src' = cte_map src;
cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap;
cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer \<and>
mdbNext (cteMDBNode rv') = nullPointer\<rbrakk>
@ -5274,7 +5274,8 @@ 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])
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)
@ -5576,12 +5577,12 @@ lemma cteInsert_corres:
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(case_tac "ca=src")
apply(simp)
apply(clarsimp simp: modify_map_def)
subgoal by(fastforce split: if_split_asm)
apply(case_tac "ca = dest")
@ -5665,8 +5666,6 @@ lemma cteInsert_corres:
subgoal by (clarsimp simp: modify_map_def split: if_split_asm)
apply (erule (5) cte_map_inj)
(* FIXME *)
apply (rule setUntypedCapAsFull_corres; 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)+

11
proof/refine/X64/CSpace_R.thy
View File

@ -3638,11 +3638,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_splitEE)
apply (rule rab_corres'; simp)
apply (rule corres_trivial)
apply (clarsimp simp: returnOk_def lookup_failure_map_def
split: list.split)
apply simp+
apply wp+
apply clarsimp
apply clarsimp
@ -4987,7 +4987,9 @@ 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])
in corres_split[where r'=dc])
apply (rule setUntypedCapAsFull_corres)
apply 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)
@ -5110,8 +5112,6 @@ lemma cteInsert_simple_corres:
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)+
@ -5130,7 +5130,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/X64/Detype_R.thy
View File

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

6
proof/refine/X64/Finalise_R.thy
View File

@ -3652,8 +3652,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 (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
@ -3678,8 +3678,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 (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
@ -3741,8 +3741,8 @@ 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 (rule emptySlot_corres, simp)
apply (wp hoare_drop_imps)+
apply (wp isFinalCapability_inv | wp (once) isFinal[where x="cte_map ptr"])+
apply (rule corres_trivial, simp)

6
proof/refine/X64/InterruptAcc_R.thy
View File

@ -28,15 +28,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 (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)

109
proof/refine/X64/Interrupt_R.thy
View File

@ -226,18 +226,21 @@ lemma arch_decodeIRQControlInvocation_corres:
apply (simp add: irq_const_defs)
apply (simp add: irq_const_defs)
apply (simp add: linorder_not_less )
apply (simp add: irq_const_defs word_le_nat_alt ucast_id)
apply (simp add: irq_const_defs word_le_nat_alt)
apply (simp add: ucast_nat_def Groups.ab_semigroup_add_class.add.commute toEnum_unat_ucast_helper_64_8)
apply (rule corres_split_eqr[OF is_irq_active_corres])
apply (rule whenE_throwError_corres, simp, simp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (rule corres_splitEE[OF ensureEmptySlot_corres])
apply simp
apply (rule whenE_throwError_corres, ((simp add: maxPCIBus_def maxPCIDev_def maxPCIFunc_def)+)[2])+
apply (rule corres_returnOkTT)
apply (clarsimp simp: arch_irq_control_inv_relation_def )
apply ((wpsimp wp: isIRQActive_inv
simp: invs_valid_objs invs_psp_aligned invs_valid_objs' invs_pspace_aligned' invs_pspace_distinct'
| wp (once) hoare_drop_imps)+)
apply (wpsimp wp: isIRQActive_inv
simp: invs_valid_objs invs_psp_aligned invs_valid_objs'
invs_pspace_aligned' invs_pspace_distinct'
| wp (once) hoare_drop_imps)+
\<comment> \<open>IOAPIC\<close>
apply (rule conjI, clarsimp)
apply (rule corres_guard_imp)
@ -245,22 +248,23 @@ lemma arch_decodeIRQControlInvocation_corres:
apply (simp add: irq_const_defs)
apply (simp add: irq_const_defs)
apply (simp add: linorder_not_less )
apply (simp add: irq_const_defs word_le_nat_alt ucast_id)
apply (simp add: irq_const_defs word_le_nat_alt)
apply (simp add: ucast_nat_def add.commute toEnum_unat_ucast_helper_64_8)
apply (rule corres_split_eqr[OF is_irq_active_corres])
apply (rule whenE_throwError_corres, simp, simp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; simp)
apply (rule corres_splitEE[OF ensureEmptySlot_corres])
apply simp
apply (rule corres_split[OF corres_gets_num_ioapics])
apply (rule whenE_throwError_corres, ((simp add: ucast_id ioapicIRQLines_def)+)[2])+
apply (rule whenE_throwError_corres, ((simp add: ioapicIRQLines_def)+)[2])+
apply (rule corres_returnOkTT)
apply (clarsimp simp: arch_irq_control_inv_relation_def )
apply ((wpsimp wp: isIRQActive_inv
apply (wpsimp wp: isIRQActive_inv
simp: invs_valid_objs invs_psp_aligned invs_valid_objs' invs_pspace_aligned' invs_pspace_distinct'
| wp (once) hoare_drop_imps)+)
| wp (once) hoare_drop_imps)+
by (auto split: arch_invocation_label.splits invocation_label.splits)
lemma irqhandler_simp[simp]:
"gen_invocation_type label \<noteq> IRQIssueIRQHandler \<Longrightarrow>
(case gen_invocation_type label of IRQIssueIRQHandler \<Rightarrow> b | _ \<Rightarrow> c) = c"
@ -460,7 +464,7 @@ lemma IRQHandler_valid':
crunch valid_mdb'[wp]: setIRQState "valid_mdb'"
method do_machine_op_corres
= (rule corres_machine_op, rule corres_Id, rule refl, simp)
= (rule corres_machine_op, rule corres_Id, rule refl, simp, wp)
lemma updateIRQState_corres[wp]:
"state = x64irqstate_to_abstract state' \<Longrightarrow>
@ -497,12 +501,14 @@ lemma arch_performIRQControl_corres:
apply (cases x2; simp add: X64_H.performIRQControl_def arch_invoke_irq_control_def)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply do_machine_op_corres
apply (rule corres_split_nor)
apply (rule corres_split_nor[OF setIRQState_corres])
apply (wpsimp simp: IRQ_def)
apply (rule corres_split_nor)
apply (rule setIRQState_corres)
apply (simp add: irq_state_relation_def)
apply (rule cteInsert_simple_corres)
apply (wp | simp add: irq_state_relation_def
IRQHandler_valid IRQHandler_valid')+
apply (do_machine_op_corres | wpsimp simp: IRQ_def | wps)+
apply (wpsimp simp: IRQHandler_valid IRQHandler_valid' | wps)+
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)
@ -514,11 +520,12 @@ lemma arch_performIRQControl_corres:
apply (auto dest: valid_irq_handlers_ctes_ofD)[1]
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (rule corres_split_nor[OF setIRQState_corres])
apply (wpsimp simp: IRQ_def)
apply (rule corres_split_nor)
apply (rule setIRQState_corres)
apply (simp add: irq_state_relation_def)
apply (rule cteInsert_simple_corres)
apply (wp | simp add: irq_state_relation_def
IRQHandler_valid IRQHandler_valid')+
apply (do_machine_op_corres | wpsimp simp: IRQ_def | wps)+
apply (wpsimp simp: IRQHandler_valid IRQHandler_valid' | wps)+
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)
@ -539,9 +546,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 (simp add: irq_state_relation_def)
apply (rule cteInsert_simple_corres)
apply (wp | simp add: irq_state_relation_def
IRQHandler_valid IRQHandler_valid')+
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)
@ -699,7 +706,31 @@ lemma timerTick_corres:
apply simp
apply (rule corres_split[OF getThreadState_corres])
apply (rename_tac state state')
apply (rule corres_split_deprecated[where r' = dc ])
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
apply simp
apply (rule corres_when,simp)
apply (rule corres_split[OF decDomainTime_corres])
@ -711,30 +742,6 @@ lemma timerTick_corres:
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 (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'
@ -780,7 +787,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)
@ -798,16 +805,16 @@ lemma handleInterrupt_corres:
apply (rule corres_guard_imp, rule sendSignal_corres)
apply (clarsimp simp: valid_cap_def valid_cap'_def do_machine_op_bind doMachineOp_bind
arch_mask_irq_signal_def maskIrqSignal_def)+
apply ( rule corres_split_deprecated)
apply (rule corres_split)
apply (rule corres_machine_op, rule corres_eq_trivial ; (simp add: no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+
apply ((wp |simp)+)
apply clarsimp
apply fastforce
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated)
apply simp
apply (rule corres_split)
apply (rule corres_split[OF timerTick_corres corres_machine_op])
apply (rule corres_eq_trivial, simp+)
apply wp+
apply (rule corres_machine_op)
apply (rule corres_eq_trivial, (simp add: no_fail_ackInterrupt)+)
apply wp+

84
proof/refine/X64/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 (simp add: ep_relation_def)
apply (rule setThreadState_corres)
apply simp
apply (simp add: ep_relation_def)
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 (simp add: ep_relation_def)
apply (rule setThreadState_corres)
apply simp
apply (simp add: ep_relation_def)
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 (simp add: ep_relation_def)
apply (rule setThreadState_corres)
apply simp
apply (simp add: ep_relation_def)
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 (simp add: ep_relation_def)
apply (rule setThreadState_corres)
apply simp
apply (simp add: ep_relation_def)
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 (simp add: ntfn_relation_def)
apply (rule setThreadState_corres)
apply simp
apply (simp add: ntfn_relation_def)
apply (wp)+
apply (simp add: list_case_If del: dc_simp)
apply (rule corres_split[OF setNotification_corres])
apply (clarsimp simp add: ntfn_relation_def neq_Nil_conv)
apply (rule setThreadState_corres)
apply simp
apply (clarsimp simp add: ntfn_relation_def neq_Nil_conv)
apply (wp)+
apply (simp add: isWaitingNtfn_def ntfn_relation_def)
apply (wp getNotification_wp)+
@ -1237,20 +1237,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 (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[OF ethreadget_corres])
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_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 (subst bind_return_unit, rule corres_split[where r'=dc])
apply (simp add: tcb_sched_dequeue_def)
apply (rule setQueue_corres)
apply (wp | simp add: etcb_relation_def)+
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:
@ -1410,11 +1411,6 @@ 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)
@ -1426,6 +1422,12 @@ lemma (in delete_one) suspend_corres:
apply (rule corres_underlying_trivial)
apply (wpsimp simp: X64.setRegister_def X64.getRegister_def)
apply (rule corres_return_trivial)
apply (rule corres_split_nor[OF setThreadState_corres])
apply simp
apply (rule tcbSchedDequeue_corres')
apply wpsimp
apply wp
apply wpsimp
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
@ -1458,13 +1460,13 @@ lemma (in delete_one) prepareThreadDelete_corres:
ArchVSpace_A.X64_A.fpu_thread_delete_def ArchRetype_H.X64_H.fpuThreadDelete_def
X64_H.fromPPtr_def)
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated[where r'="(=)"])
apply clarsimp
apply (rule corres_when)
apply clarsimp
apply (rule corres_split[where r'="(=)"])
apply (rule corres_machine_op)
apply (rule corres_Id, rule refl, simp)
apply wpsimp
apply clarsimp
apply (rule corres_when)
apply clarsimp
apply (rule corres_machine_op)
apply (rule corres_Id, rule refl, simp)
apply wpsimp
@ -1955,7 +1957,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
@ -2001,7 +2003,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)+
@ -2054,7 +2056,8 @@ 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 (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
@ -2065,12 +2068,9 @@ lemma cancelAllSignals_corres:
in hoare_post_add)
apply (rule mapM_x_wp')
apply (rule hoare_name_pre_state)
apply (wp hoare_vcg_const_Ball_lift
apply (wpsimp 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)
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)+
@ -2651,18 +2651,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 (simp add: ep_relation_def)
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 (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"
@ -2675,6 +2672,7 @@ 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 simp
apply (rule corres_split[OF tcbSchedEnqueue_corres])
apply (rule corres_trivial)
apply simp
@ -2687,12 +2685,16 @@ lemma cancelBadgedSends_corres:
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'
apply (wp hoare_vcg_imp_lift sts_st_tcb' sts_valid_queues
| clarsimp simp: valid_tcb_state'_def)+
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 (simp add: ep_relation_def)
apply (wp hoare_vcg_const_Ball_lift weak_sch_act_wf_lift_linear set_ep_valid_objs'
| simp)+
apply (clarsimp simp: conj_comms)

125
proof/refine/X64/Ipc_R.thy
View File

@ -154,11 +154,11 @@ lemma getReceiveSlots_corres:
apply (simp add: split_def liftE_bindE unlessE_whenE)
apply (rule corres_split[OF get_cap_corres])
apply (rule corres_split_norE)
apply (rule corres_trivial, simp add: returnOk_def)
apply (rule corres_whenE)
apply (case_tac cap, auto)[1]
apply (rule corres_trivial, simp)
apply simp
apply (rule corres_trivial, simp add: returnOk_def)
apply (wp lookup_cap_valid lookup_cap_valid' lsfco_cte_at | simp)+
done
@ -436,11 +436,11 @@ next
apply (rule corres_if2)
apply (case_tac "fst x", auto simp add: isCap_simps)[1]
apply (rule corres_split[OF corres_set_extra_badge])
apply (clarsimp simp: is_cap_simps)
apply (drule conjunct1)
apply simp
apply (rule corres_rel_imp, rule Cons.hyps, simp_all)[1]
apply (case_tac mi, simp)
apply (clarsimp simp: is_cap_simps)
apply (simp add: split_def)
apply (wp hoare_vcg_const_Ball_lift)
apply (subgoal_tac "obj_ref_of (fst x) = capEPPtr (fst y)")
@ -460,6 +460,11 @@ next
apply (simp add: remove_rights_def)
apply clarsimp
apply (rule corres_split_norE)
apply (rule corres_whenE)
apply (case_tac cap', auto)[1]
apply (rule corres_trivial, simp)
apply (case_tac mi, simp)
apply simp
apply (simp add: liftE_bindE)
apply (rule corres_split_nor)
apply (rule cteInsert_corres, simp_all add: hd_map)[1]
@ -473,13 +478,8 @@ next
cteInsert_valid_pspace
| simp add: split_def)+
apply (wp cteInsert_weak_cte_wp_at hoare_valid_ipc_buffer_ptr_typ_at')+
apply (wp hoare_vcg_const_Ball_lift cteInsert_cte_wp_at valid_case_option_post_wp
| simp add:split_def)+
apply (rule corres_whenE)
apply (case_tac cap', auto)[1]
apply (rule corres_trivial, simp)
apply (case_tac mi, simp)
apply simp
apply (wpsimp wp: hoare_vcg_const_Ball_lift cteInsert_cte_wp_at valid_case_option_post_wp
simp: split_def)
apply (unfold whenE_def)
apply wp+
apply (clarsimp simp: conj_comms ball_conj_distrib split del: if_split)
@ -1374,12 +1374,12 @@ lemma lookupCapAndSlot_corres:
apply (rule corres_guard_imp)
apply (rule_tac r'="\<lambda>rv rv'. rv' = cte_map (fst rv)"
in corres_splitEE)
apply (rule corres_split[OF getSlotCap_corres])
apply (rule corres_returnOkTT, simp)
apply simp
apply wp+
apply (rule corres_rel_imp, rule lookupSlotForThread_corres)
apply (simp add: split_def)
apply (rule corres_split[OF getSlotCap_corres])
apply simp
apply (rule corres_returnOkTT, simp)
apply wp+
apply (wp | simp add: liftE_bindE[symmetric])+
done
@ -1473,28 +1473,28 @@ lemma doNormalTransfer_corres:
(doNormalTransfer sender send_buf ep badge can_grant receiver recv_buf)"
apply (simp add: do_normal_transfer_def doNormalTransfer_def)
apply (rule corres_guard_imp)
apply (rule corres_split_mapr[OF getMessageInfo_corres])
apply (rule_tac F="valid_message_info mi" in corres_gen_asm)
apply (rule_tac r'="list_all2 (\<lambda>x y. cap_relation (fst x) (fst y) \<and> snd y = cte_map (snd x))"
in corres_split)
apply (rule corres_if[OF refl])
apply (rule corres_split_catch)
apply (rule lookupExtraCaps_corres; simp)
apply (rule corres_trivial, simp)
apply (rule lookupExtraCaps_corres, simp+)
apply wp+
apply (rule corres_trivial, simp)
apply simp
apply (rule corres_split_eqr[OF copyMRs_corres])
apply (rule corres_split[OF transferCaps_corres])
apply (rule corres_split)
apply (rule transferCaps_corres; simp)
apply (rename_tac mi' mi'')
apply (rule_tac F="mi_label mi' = mi_label mi"
in corres_gen_asm)
apply (rule corres_split_nor[OF setMessageInfo_corres])
apply (case_tac mi', clarsimp)
apply (simp add: badge_register_def badgeRegister_def)
apply (fold dc_def)
apply (rule asUser_setRegister_corres)
apply (case_tac mi', clarsimp)
apply wp
apply simp+
apply ((wp valid_case_option_post_wp hoare_vcg_const_Ball_lift
@ -1662,15 +1662,15 @@ lemma doFaultTransfer_corres:
apply (rule corres_split_eqr[OF makeFaultMessage_corres])
apply (rule corres_split_eqr[OF setMRs_corres [OF refl]])
apply (rule corres_split_nor[OF setMessageInfo_corres])
apply (rule asUser_setRegister_corres)
apply simp
apply (rule asUser_setRegister_corres)
apply (wp | simp)+
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[OF makeFaultMessage_corres])
apply (rule corres_split_eqr[OF setMRs_corres [OF refl]])
apply (rule corres_split_nor[OF setMessageInfo_corres])
apply (rule asUser_setRegister_corres)
apply simp
apply (rule asUser_setRegister_corres)
apply (wp | simp)+
done
@ -1888,8 +1888,7 @@ lemma handle_fault_reply_registers_corres:
od)"
apply (rule corres_guard_imp)
apply (clarsimp simp: arch_get_sanitise_register_info_def getSanitiseRegisterInfo_def)
apply (rule corres_split_deprecated)
apply (rule corres_trivial, simp)
apply (rule corres_split)
apply (rule asUser_corres')
apply(simp add: setRegister_def syscallMessage_def)
apply(subst zipWithM_x_modify)+
@ -2193,8 +2192,8 @@ lemma doReplyTransfer_corres:
apply (rule corres_split[OF doIPCTransfer_corres])
apply (rule corres_split[OF cap_delete_one_corres])
apply (rule corres_split[OF setThreadState_corres])
apply (rule possibleSwitchTo_corres)
apply simp
apply (rule possibleSwitchTo_corres)
apply (wp set_thread_state_runnable_valid_sched set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at' sts_st_tcb' sts_valid_queues sts_valid_objs' delete_one_tcbDomain_obj_at'
| simp add: valid_tcb_state'_def)+
apply (strengthen cte_wp_at_reply_cap_can_fast_finalise)
@ -2229,24 +2228,27 @@ lemma doReplyTransfer_corres:
apply (rule corres_split_eqr[OF getMRs_corres])
apply (simp(no_asm) del: dc_simp)
apply (rule corres_split_eqr[OF handleFaultReply_corres])
apply (rule corres_split[OF threadset_corresT])
apply (rule_tac Q="valid_sched and cur_tcb and tcb_at receiver"
and Q'="tcb_at' receiver and cur_tcb'
apply simp
apply (rule corres_split)
apply (rule threadset_corresT;
clarsimp simp add: tcb_relation_def fault_rel_optionation_def
tcb_cap_cases_def tcb_cte_cases_def exst_same_def)
apply (rule_tac P="valid_sched and cur_tcb and tcb_at receiver"
and P'="tcb_at' receiver and cur_tcb'
and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
and Invariants_H.valid_queues and valid_queues' and valid_objs'"
in corres_guard_imp)
in corres_inst)
apply (case_tac rvb, simp_all)[1]
apply (rule corres_guard_imp)
apply (rule corres_split[OF setThreadState_corres])
apply simp
apply (fold dc_def, rule possibleSwitchTo_corres)
apply simp
apply (wp static_imp_wp static_imp_conj_wp set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at'
sts_st_tcb' sts_valid_queues | simp | force simp: valid_sched_def valid_sched_action_def valid_tcb_state'_def)+
apply (rule corres_guard_imp)
apply (rule setThreadState_corres)
apply (simp_all)[20]
apply (clarsimp simp add: tcb_relation_def fault_rel_optionation_def
tcb_cap_cases_def tcb_cte_cases_def exst_same_def)+
apply clarsimp+
apply (wp threadSet_cur weak_sch_act_wf_lift_linear threadSet_pred_tcb_no_state
thread_set_not_state_valid_sched threadSet_valid_queues threadSet_valid_queues'
threadSet_tcbDomain_triv threadSet_valid_objs'
@ -2327,6 +2329,8 @@ lemma setupCallerCap_corres:
getThreadCallerSlot_def)
apply (rule stronger_corres_guard_imp)
apply (rule corres_split_nor)
apply (rule setThreadState_corres)
apply (simp split: option.split)
apply (rule corres_symb_exec_r)
apply (rule_tac F="\<exists>r. cteCap masterCTE = capability.ReplyCap sender True r
\<and> mdbNext (cteMDBNode masterCTE) = nullPointer"
@ -2353,8 +2357,6 @@ lemma setupCallerCap_corres:
apply blast
apply (rule no_fail_pre, wp)
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (rule setThreadState_corres)
apply (simp split: option.split)
apply (wp sts_valid_pspace_hangers
| simp add: cte_wp_at_ctes_of)+
apply (clarsimp simp: valid_tcb_state_def st_tcb_at_reply_cap_valid
@ -2467,9 +2469,9 @@ proof -
apply (simp add: ep_relation_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF setThreadState_corres])
apply simp
apply (rule setEndpoint_corres)
apply (simp add: ep_relation_def)
apply (simp add: fault_rel_optionation_def)
apply wp+
apply (clarsimp simp: st_tcb_at_tcb_at valid_tcb_state_def)
apply clarsimp
@ -2477,9 +2479,9 @@ proof -
apply (simp add: ep_relation_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF setThreadState_corres])
apply simp
apply (rule setEndpoint_corres)
apply (simp add: ep_relation_def)
apply (simp add: fault_rel_optionation_def)
apply wp+
apply (clarsimp simp: st_tcb_at_tcb_at valid_tcb_state_def)
apply clarsimp
@ -2493,6 +2495,7 @@ proof -
apply (clarsimp split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split[OF setEndpoint_corres])
apply (simp add: ep_relation_def split: list.split)
apply (simp add: isReceive_def split del:if_split)
apply (rule corres_split[OF getThreadState_corres])
apply (rule_tac
@ -2502,9 +2505,9 @@ proof -
simp del: dc_simp split del: if_split cong: if_cong)
apply (rule corres_split[OF doIPCTransfer_corres])
apply (rule corres_split[OF setThreadState_corres])
apply simp
apply (rule corres_split[OF possibleSwitchTo_corres])
apply (fold when_def)[1]
apply (rule_tac P="call" and P'="call"
in corres_symmetric_bool_cases, blast)
apply (simp add: when_def dc_def[symmetric] split del: if_split)
@ -2530,7 +2533,6 @@ proof -
apply (simp add: valid_tcb_state'_def)
apply (wp weak_sch_act_wf_lift_linear tcb_in_cur_domain'_lift hoare_drop_imps)[1]
apply (wp gts_st_tcb_at)+
apply (simp add: ep_relation_def split: list.split)
apply (simp add: pred_conj_def cong: conj_cong)
apply (wp hoare_post_taut)
apply (simp)
@ -2574,6 +2576,7 @@ proof -
apply (clarsimp split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split[OF setEndpoint_corres])
apply (simp add: ep_relation_def split: list.split)
apply (rule corres_split[OF getThreadState_corres])
apply (rule_tac
F="\<exists>data. recv_state = Structures_A.BlockedOnReceive ep data"
@ -2582,10 +2585,9 @@ proof -
split del: if_split cong: if_cong)
apply (rule corres_split[OF doIPCTransfer_corres])
apply (rule corres_split[OF setThreadState_corres])
apply simp
apply (rule possibleSwitchTo_corres)
apply (simp add: if_apply_def2)
apply (wp hoare_drop_imps)
apply (simp add: if_apply_def2)
apply ((wp sts_cur_tcb set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at_cases |
simp add: if_apply_def2 split del: if_split)+)[1]
apply (wp setThreadState_valid_queues' sts_valid_queues sts_weak_sch_act_wf
@ -2597,7 +2599,6 @@ proof -
apply (strengthen sch_act_wf_weak)
apply (wp weak_sch_act_wf_lift_linear hoare_drop_imps)
apply (wp gts_st_tcb_at)+
apply (simp add: ep_relation_def split: list.split)
apply (simp add: pred_conj_def cong: conj_cong)
apply (wp hoare_post_taut)
apply simp
@ -2668,11 +2669,11 @@ lemma sendSignal_corres:
Structures_H.thread_state.splits)
apply (rule corres_split[OF cancel_ipc_corres])
apply (rule corres_split[OF setThreadState_corres])
apply (clarsimp simp: thread_state_relation_def)
apply (simp add: badgeRegister_def badge_register_def)
apply (rule corres_split[OF asUser_setRegister_corres])
apply (rule possibleSwitchTo_corres)
apply wp
apply (clarsimp simp: thread_state_relation_def)
apply (wp set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at'
sts_valid_queues sts_st_tcb' hoare_disjI2
cancel_ipc_cte_wp_at_not_reply_state
@ -2700,7 +2701,9 @@ lemma sendSignal_corres:
apply (rule_tac F="list \<noteq> []" in corres_gen_asm)
apply (simp add: list_case_helper split del: if_split)
apply (rule corres_split[OF setNotification_corres])
apply (simp add: ntfn_relation_def)
apply (rule corres_split[OF setThreadState_corres])
apply simp
apply (simp add: badgeRegister_def badge_register_def)
apply (rule corres_split[OF asUser_setRegister_corres])
apply (rule possibleSwitchTo_corres)
@ -2716,7 +2719,6 @@ lemma sendSignal_corres:
apply (wp sts_st_tcb_at'_cases sts_valid_queues setThreadState_valid_queues'
setThreadState_st_tcb
| simp)+
apply (simp add: ntfn_relation_def)
apply (wp set_simple_ko_valid_objs set_ntfn_aligned' set_ntfn_valid_objs'
hoare_vcg_disj_lift weak_sch_act_wf_lift_linear
| simp add: valid_tcb_state_def valid_tcb_state'_def)+
@ -2731,7 +2733,9 @@ lemma sendSignal_corres:
apply (rule_tac F="list \<noteq> []" in corres_gen_asm)
apply (simp add: list_case_helper)
apply (rule corres_split[OF setNotification_corres])
apply (simp add: ntfn_relation_def split:list.splits)
apply (rule corres_split[OF setThreadState_corres])
apply simp
apply (simp add: badgeRegister_def badge_register_def)
apply (rule corres_split[OF asUser_setRegister_corres])
apply (rule possibleSwitchTo_corres)
@ -2741,7 +2745,6 @@ lemma sendSignal_corres:
apply (wp sts_st_tcb_at'_cases sts_valid_queues setThreadState_valid_queues'
setThreadState_st_tcb
| simp)+
apply (simp add: ntfn_relation_def split:list.splits)
apply (wp set_ntfn_aligned' set_simple_ko_valid_objs set_ntfn_valid_objs'
hoare_vcg_disj_lift weak_sch_act_wf_lift_linear
| simp add: valid_tcb_state_def valid_tcb_state'_def)+
@ -3146,6 +3149,7 @@ lemma replyFromKernel_corres:
apply (rule corres_split_eqr[OF lookupIPCBuffer_corres])
apply (rule corres_split[OF asUser_setRegister_corres])
apply (rule corres_split_eqr[OF setMRs_corres])
apply simp
apply (rule setMessageInfo_corres)
apply (wp hoare_case_option_wp hoare_valid_ipc_buffer_ptr_typ_at'
| clarsimp)+
@ -3210,7 +3214,12 @@ lemma receiveIPC_corres:
apply (rule corres_split[OF getEndpoint_corres])
apply (rule corres_guard_imp)
apply (rule corres_split[OF getBoundNotification_corres])
apply (rule_tac r'="ntfn_relation" in corres_split_deprecated)
apply (rule_tac r'="ntfn_relation" in corres_split)
apply (rule corres_option_split[rotated 2])
apply (rule getNotification_corres)
apply clarsimp
apply (rule corres_trivial, simp add: ntfn_relation_def default_notification_def
default_ntfn_def)
apply (rule corres_if)
apply (clarsimp simp: ntfn_relation_def Ipc_A.isActive_def Endpoint_H.isActive_def
split: Structures_A.ntfn.splits Structures_H.notification.splits)
@ -3230,9 +3239,9 @@ lemma receiveIPC_corres:
apply (rule corres_guard_imp)
apply (case_tac isBlocking; simp)
apply (rule corres_split[OF setThreadState_corres])
apply simp
apply (rule setEndpoint_corres)
apply (simp add: ep_relation_def)
apply simp
apply wp+
apply (rule corres_guard_imp, rule doNBRecvFailedTransfer_corres, simp)
apply simp
@ -3247,6 +3256,7 @@ lemma receiveIPC_corres:
apply (case_tac list, simp_all split del: if_split)[1]
apply (rule corres_guard_imp)
apply (rule corres_split[OF setEndpoint_corres])
apply (case_tac lista, simp_all add: ep_relation_def)[1]
apply (rule corres_split[OF getThreadState_corres])
apply (rule_tac
F="\<exists>data.
@ -3281,8 +3291,8 @@ lemma receiveIPC_corres:
apply simp
apply simp
apply (rule corres_split[OF setThreadState_corres])
apply (rule possibleSwitchTo_corres)
apply simp
apply (rule possibleSwitchTo_corres)
apply (wp sts_st_tcb_at' set_thread_state_runnable_weak_valid_sched_action
| simp)+
apply (wp sts_st_tcb_at'_cases sts_valid_queues setThreadState_valid_queues'
@ -3295,7 +3305,6 @@ lemma receiveIPC_corres:
apply (rule_tac Q="\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s"
in hoare_post_imp, erule sch_act_wf_weak)
apply (wp sts_st_tcb' gts_st_tcb_at | simp)+
apply (case_tac lista, simp_all add: ep_relation_def)[1]
apply (simp cong: list.case_cong)
apply wp
apply simp
@ -3311,19 +3320,14 @@ lemma receiveIPC_corres:
apply (rule_tac corres_guard_imp)
apply (case_tac isBlocking; simp)
apply (rule corres_split[OF setThreadState_corres])
apply simp
apply (rule setEndpoint_corres)
apply (simp add: ep_relation_def)
apply simp
apply wp+
apply (rule corres_guard_imp, rule doNBRecvFailedTransfer_corres, simp)
apply simp
apply (clarsimp simp: valid_tcb_state_def)
apply (clarsimp simp add: valid_tcb_state'_def)
apply (rule corres_option_split[rotated 2])
apply (rule getNotification_corres)
apply clarsimp
apply (rule corres_trivial, simp add: ntfn_relation_def default_notification_def
default_ntfn_def)
apply (wp get_simple_ko_wp[where f=Notification] getNotification_wp gbn_wp gbn_wp'
hoare_vcg_all_lift hoare_vcg_imp_lift hoare_vcg_if_lift
| wpc | simp add: ep_at_def2[symmetric, simplified] | clarsimp)+
@ -3361,9 +3365,9 @@ lemma receiveSignal_corres:
apply (rule corres_guard_imp)
apply (case_tac isBlocking; simp)
apply (rule corres_split[OF setThreadState_corres])
apply simp
apply (rule setNotification_corres)
apply (simp add: ntfn_relation_def)
apply simp
apply wp+
apply (rule corres_guard_imp, rule doNBRecvFailedTransfer_corres, simp+)
\<comment> \<open>WaitingNtfn\<close>
@ -3371,9 +3375,9 @@ lemma receiveSignal_corres:
apply (rule corres_guard_imp)
apply (case_tac isBlocking; simp)
apply (rule corres_split[OF setThreadState_corres])
apply simp
apply (rule setNotification_corres)
apply (simp add: ntfn_relation_def)
apply simp
apply wp+
apply (rule corres_guard_imp)
apply (rule doNBRecvFailedTransfer_corres, simp+)
@ -3416,7 +3420,9 @@ lemma sendFaultIPC_corres:
apply (simp add: send_fault_ipc_def sendFaultIPC_def
liftE_bindE Let_def)
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated [where r'="\<lambda>fh fh'. fh = to_bl fh'"])
apply (rule corres_split [where r'="\<lambda>fh fh'. fh = to_bl fh'"])
apply (rule threadGet_corres)
apply (simp add: tcb_relation_def)
apply simp
apply (rule corres_splitEE)
apply (rule corres_cap_fault)
@ -3449,9 +3455,6 @@ lemma sendFaultIPC_corres:
apply auto[1]
apply (clarsimp simp: lookup_failure_map_def)
apply wp+
apply (rule threadGet_corres)
apply (simp add: tcb_relation_def)
apply wp+
apply (fastforce elim: st_tcb_at_tcb_at)
apply fastforce
done
@ -4246,17 +4249,17 @@ lemma handleFault_corres:
apply (simp add: handle_fault_def handleFault_def)
apply (rule corres_guard_imp)
apply (subst return_bind [symmetric],
rule corres_split_deprecated [where P="tcb_at thread",
OF _ gets_the_noop_corres [where x="()"]])
rule corres_split[where P="tcb_at thread",
OF gets_the_noop_corres [where x="()"]])
apply (simp add: tcb_at_def)
apply (rule corres_split_catch)
apply (rule handleDoubleFault_corres)
apply (rule_tac F="valid_fault f" in corres_gen_asm)
apply (rule sendFaultIPC_corres, assumption)
apply simp
apply (rule handleDoubleFault_corres)
apply wp+
apply (rule hoare_post_impErr, rule sfi_invs_plus', simp_all)[1]
apply clarsimp
apply (simp add: tcb_at_def)
apply wp+
apply (clarsimp simp: st_tcb_at_tcb_at st_tcb_def2 invs_def
valid_state_def valid_idle_def)

7
proof/refine/X64/Refine.thy
View File

@ -588,14 +588,14 @@ lemma kernel_corres:
apply (rule corres_guard_imp)
apply (rule corres_add_noop_lhs2)
apply (simp only: bind_assoc[symmetric])
apply (rule corres_split_deprecated[where r'=dc and
apply (rule corres_split[where r'=dc and
R="\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s" and
R'="\<lambda>_. \<top>"])
apply (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 (simp only: bind_assoc)
apply (rule kernel_corres')
apply (wp call_kernel_domain_time_inv_det_ext call_kernel_domain_list_inv_det_ext)
apply wp
apply clarsimp
@ -667,6 +667,7 @@ 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 simp
apply (rule corres_underlying_split[OF corres_machine_op])
apply simp
apply (rule corres_underlying_trivial)

42
proof/refine/X64/Retype_R.thy
View File

@ -1429,16 +1429,20 @@ lemma objBitsKO_gt_0: "0 < objBitsKO ko"
apply (simp_all add:archObjSize_def pageBits_def)
done
lemma kheap_ekheap_double_gets: "(\<And>rv erv rv'. pspace_relation rv rv' \<Longrightarrow> ekheap_relation erv rv' \<Longrightarrow> corres r (R rv erv) (R' rv') (b rv erv) (d rv')) \<Longrightarrow>
corres r (\<lambda>s. R (kheap s) (ekheap s) s) (\<lambda>s. R' (ksPSpace s) s) (do x \<leftarrow> gets kheap; xa \<leftarrow> gets ekheap; b x xa od) (gets ksPSpace >>= d)"
lemma kheap_ekheap_double_gets:
"(\<And>rv erv rv'. \<lbrakk>pspace_relation rv rv'; ekheap_relation erv rv'\<rbrakk>
\<Longrightarrow> corres r (R rv erv) (R' rv') (b rv erv) (d rv')) \<Longrightarrow>
corres r (\<lambda>s. R (kheap s) (ekheap s) s) (\<lambda>s. R' (ksPSpace s) s)
(do x \<leftarrow> gets kheap; xa \<leftarrow> gets ekheap; b x xa od) (gets ksPSpace >>= d)"
apply (rule corres_symb_exec_l)
apply (rule corres_guard_imp)
apply (rule_tac r'= "\<lambda>erv rv'. ekheap_relation erv rv' \<and> pspace_relation x rv'" in corres_split_deprecated)
apply clarsimp
apply assumption
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 (simp add: state_relation_def)
apply clarsimp
apply assumption
apply (wp gets_exs_valid | simp)+
done
@ -1792,12 +1796,7 @@ 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 (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)
@ -1805,6 +1804,11 @@ proof -
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)
@ -5387,19 +5391,19 @@ lemma corres_retype_region_createNewCaps:
split del: if_split)[10] (* not PML4Object *)
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 (simp add: APIType_map2_def)
apply (rule retype_region2_extra_ext_mapM_x_corres)
apply wp
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 (rule corres_split_nor)
apply (simp add: APIType_map2_def)
apply (rule retype_region2_extra_ext_mapM_x_corres)
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 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]

80
proof/refine/X64/Schedule_R.thy
View File

@ -49,12 +49,12 @@ proof -
apply (subst P)
apply (rule corres_guard_imp)
apply (rule corres_split[OF x])
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 assumption
apply (rule Q)
apply (rule hoare_post_imp [OF _ z])
apply simp+
@ -114,21 +114,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[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 (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 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
@ -1688,11 +1697,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 (rule corres_split)
apply (rule corres_when, simp)
apply (rule nextDomain_corres)
apply simp
apply (rule chooseThread_corres)
apply simp
apply (rule nextDomain_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
@ -1808,30 +1817,38 @@ lemma schedule_corres:
(* choose thread *)
apply clarsimp
apply (rule corres_split[OF thread_get_isRunnable_corres])
apply (rule corres_split[OF corres_when])
apply (rule corres_split)
apply (rule corres_when, simp)
apply (rule tcbSchedEnqueue_corres)
apply (rule scheduleChooseNewThread_corres, simp)
apply (rule tcbSchedEnqueue_corres, simp)
apply (wp thread_get_wp' tcbSchedEnqueue_invs' hoare_vcg_conj_lift hoare_drop_imps
| clarsimp)+
(* 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)
apply (rule corres_when, simp)
apply (rule tcbSchedEnqueue_corres)
apply (rule corres_split[OF getIdleThread_corres], rename_tac it it')
apply (rule_tac F="was_running \<longrightarrow> ct \<noteq> it" in corres_gen_asm)
apply (rule corres_split[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)
apply (rule ethreadget_corres[where r="(=)"])
apply (clarsimp simp: etcb_relation_def)
apply (rename_tac tp tp')
apply (rule corres_split)
apply (rule ethread_get_when_corres[where r="(=)"])
apply (clarsimp simp: etcb_relation_def)
apply (rename_tac cp cp')
apply (rule corres_split)
apply (rule scheduleSwitchThreadFastfail_corres; simp)
apply (rule corres_split[OF curDomain_corres])
apply (rule corres_split[OF isHighestPrio_corres]; simp only:)
apply (rule corres_if, simp)
apply (rule corres_split[OF tcbSchedEnqueue_corres])
apply (simp, fold dc_def)
apply (rule corres_split[OF setSchedulerAction_corres])
apply (rule scheduleChooseNewThread_corres, simp)
apply (rule corres_split)
apply (rule setSchedulerAction_corres; simp)
apply (rule scheduleChooseNewThread_corres)
apply (wp | simp)+
apply (simp add: valid_sched_def)
apply wp
@ -1840,14 +1857,12 @@ lemma schedule_corres:
apply (wpsimp wp: setSchedulerAction_invs')+
apply (wp tcb_sched_action_enqueue_valid_blocked hoare_vcg_all_lift enqueue_thread_queued)
apply (wp tcbSchedEnqueue_invs'_not_ResumeCurrentThread)
apply (rule corres_if, fastforce)
apply (rule corres_split[OF tcbSchedAppend_corres])
apply (simp, fold dc_def)
apply (rule corres_split[OF setSchedulerAction_corres])
apply (rule scheduleChooseNewThread_corres, simp)
apply (rule corres_split)
apply (rule setSchedulerAction_corres; simp)
apply (rule scheduleChooseNewThread_corres)
apply (wp | simp)+
apply (simp add: valid_sched_def)
apply wp
@ -1868,9 +1883,6 @@ lemma schedule_corres:
apply (simp add: if_apply_def2)
apply ((wp (once) hoare_drop_imp)+)[1]
apply wpsimp+
apply (wpsimp simp: etcb_relation_def)+
apply (rule tcbSchedEnqueue_corres)
apply wpsimp+
apply (clarsimp simp: conj_ac cong: conj_cong)
apply wp
@ -2259,7 +2271,9 @@ 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)
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)
@ -2269,7 +2283,7 @@ lemma possibleSwitchTo_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
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+

65
proof/refine/X64/Syscall_R.thy
View File

@ -139,7 +139,11 @@ 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_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")
@ -152,9 +156,6 @@ lemma decodeDomainInvocation_corres:
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 (wp | simp)+
done
@ -265,9 +266,9 @@ 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_splitEE)
apply (rule lookupExtraCaps_corres; simp)
apply (rule corres_returnOkTT)
apply simp+
apply (wp | simp)+
apply auto
done
@ -359,17 +360,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)
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_deprecated[OF corres_when[OF refl]])
apply (rule rescheduleRequired_corres)
apply (rule corres_split)
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_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,19 +409,20 @@ 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_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_trivial)
apply simp
apply (rule corres_trivial)
apply simp
apply wp+
apply (clarsimp simp: ct_in_state_def)
@ -459,8 +462,8 @@ lemma performInvocation_corres:
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 (rule corres_trivial, simp add: returnOk_def)
apply wp+
apply (clarsimp+)[2]
apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric])
@ -1212,24 +1215,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_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_deprecated [OF setThreadState_corres])
apply simp
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 simp+
apply (wp hoare_drop_imps)+
apply (simp)
apply (wp)
apply (simp)
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)
@ -1481,7 +1486,6 @@ 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
@ -1504,17 +1508,21 @@ lemma handleRecv_isBlocking_corres':
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+
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)
@ -2007,10 +2015,11 @@ 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
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
@ -2021,8 +2030,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 (erule handleFault_corres)
apply (rule hoare_elim_pred_conjE2)
apply (rule hoare_vcg_E_conj, rule valid_validE_E, wp)
apply (wp handle_vm_fault_valid_fault)

115
proof/refine/X64/TcbAcc_R.thy
View File

@ -441,10 +441,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 (rule z)
apply (wp w)+
apply simp
apply simp
@ -1370,11 +1370,14 @@ 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 (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 (rule corres_trivial, simp)
apply (simp add: threadSet_def)
apply (rule corres_symb_exec_r)
prefer 4
@ -1383,9 +1386,6 @@ lemma asUser_corres':
apply simp
apply simp
apply (wp select_f_inv | simp)+
apply (rule L1[simplified])
apply wp+
apply auto
done
qed
@ -1826,18 +1826,24 @@ 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[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 (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 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
@ -1874,14 +1880,15 @@ 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
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 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
split: Deterministic_A.scheduler_action.split)
@ -2027,15 +2034,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[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 (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 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 =
@ -2065,8 +2076,8 @@ 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 (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])
@ -2077,7 +2088,6 @@ lemma setThreadState_corres:
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
@ -3196,7 +3206,13 @@ 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_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 wp+
apply (rule corres_machine_op)
apply (rule corres_Id [OF refl])
apply simp
@ -3205,11 +3221,6 @@ lemma storeWordUser_corres:
apply (erule_tac n=msg_align_bits in aligned_add_aligned)
apply (rule is_aligned_mult_triv2 [where n = 3, 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 corres_assert)
apply (rule corres_trivial)
apply simp
apply wp+
apply (simp add: in_user_frame_eq[OF y])
apply simp
@ -3273,7 +3284,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
@ -3283,7 +3294,6 @@ 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}"])
@ -3298,6 +3308,7 @@ lemma getMRs_corres:
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
@ -3390,12 +3401,14 @@ 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_split_nor[OF asUser_corres'])
apply (rule corres_modify')
apply (fastforce simp: fold_fun_upd[symmetric] msgRegisters_unfold UserContext_fold
modify_registers_def
cong: if_cong simp del: the_index.simps)
apply ((wp |simp)+)[5]
apply simp
apply (rule corres_trivial, simp)
apply ((wp |simp)+)[4]
\<comment> \<open>buf = Some a\<close>
using if_split[split del]
apply (clarsimp simp: msgRegisters_unfold setRegister_def2 zipWithM_x_Nil zipWithM_x_modify
@ -3404,7 +3417,11 @@ 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 corres_modify')
apply (simp only: msgRegisters_unfold cong: if_cong)
apply (fastforce simp: fold_fun_upd[symmetric] modify_registers_def UserContext_fold)
apply simp
apply (rule corres_split_nor)
apply (rule_tac S="{((x, y), (x', y')). y = y' \<and> x' = (a + (of_nat x * 8)) \<and> x < unat max_ipc_words}"
in zipWithM_x_corres)
apply (fastforce intro: storeWordUser_corres)
@ -3413,10 +3430,8 @@ proof -
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 (rule corres_modify')
apply (simp only: msgRegisters_unfold cong: if_cong)
apply (fastforce simp: fold_fun_upd[symmetric] modify_registers_def UserContext_fold)
apply (wp | clarsimp simp: valid_ipc_buffer_ptr'_def)+
done
qed
@ -3484,13 +3499,13 @@ 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_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 (rule storeWordUser_corres)
apply simp
apply (wp hoare_vcg_all_lift | simp)+
apply (clarsimp simp: upto_enum_def)
apply arith
@ -3501,6 +3516,7 @@ proof -
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
@ -3587,8 +3603,10 @@ lemma lookupIPCBuffer_corres':
apply (simp add: lookup_ipc_buffer_def X64_H.lookupIPCBuffer_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[OF threadGet_corres])
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 (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'"
@ -3618,9 +3636,7 @@ lemma lookupIPCBuffer_corres':
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: 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 (wp thread_get_obj_at_eq)+
apply (clarsimp elim!: tcb_at_cte_at)
apply clarsimp
@ -4506,11 +4522,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 (insert cap_relation_masks, simp)
apply (wp getCTE_wp')+
apply simp
apply fastforce
apply (insert cap_relation_masks, simp)
done
lemma asUser_irq_handlers':

163
proof/refine/X64/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 (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 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 (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>"
@ -284,6 +285,8 @@ lemma invokeTCB_ReadRegisters_corres:
frameRegisters_def gpRegisters_def)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
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)
@ -293,9 +296,6 @@ lemma invokeTCB_ReadRegisters_corres:
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 (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)
@ -409,12 +409,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>
@ -446,29 +446,29 @@ proof -
apply (rule corres_split[OF corres_when [OF refl suspend_corres]], simp)
apply (rule corres_split[OF corres_when [OF refl restart_corres]], simp)
apply (rule corres_split_nor)
apply (rule corres_when[OF refl])
apply (rule corres_split_nor)
apply (rule 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 (wpsimp wp: mapM_x_wp' static_imp_wp)+
apply (rule corres_split_nor)
apply (rule corres_when[OF refl])
apply (rule R[OF refl refl])
apply (simp add: gpRegisters_def)
apply (rule corres_split_eqr[OF getCurThread_corres])
apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
apply (rule corres_split[OF corres_when[OF refl rescheduleRequired_corres]])
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
apply simp
apply (wp static_imp_wp)+
apply (rule corres_when[OF refl])
apply (rule R[OF refl refl])
apply (simp add: gpRegisters_def)
apply ((solves \<open>wp static_imp_wp\<close>)+)
apply (rule_tac Q="\<lambda>_. einvs and tcb_at dest" in hoare_post_imp)
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_post_imp)
apply (clarsimp simp: invs'_def valid_state'_def invs_weak_sch_act_wf cur_tcb'_def)
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 ((wp mapM_x_wp' static_imp_wp | simp+)+)[4]
apply (wp mapM_x_wp' static_imp_wp | simp)+
apply ((wp static_imp_wp restart_invs' | wpc | clarsimp simp: 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
@ -632,6 +632,7 @@ 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 (simp add: etcb_relation_def)
apply (rule corres_split[OF isRunnable_corres])
apply (erule corres_when)
apply(rule corres_split[OF getCurThread_corres])
@ -639,8 +640,8 @@ lemma sp_corres2:
apply (rule rescheduleRequired_corres)
apply (rule possibleSwitchTo_corres)
apply ((clarsimp
| wp static_imp_wp hoare_vcg_if_lift hoare_wp_combs gts_wp isRunnable_wp
| simp add: etcb_relation_def)+)[5]
| wp static_imp_wp hoare_vcg_if_lift hoare_wp_combs gts_wp
isRunnable_wp)+)[4]
apply (wp hoare_vcg_imp_lift' hoare_vcg_if_lift hoare_vcg_all_lift)
apply clarsimp
apply ((wp hoare_drop_imps hoare_vcg_if_lift hoare_vcg_all_lift
@ -1386,19 +1387,18 @@ proof -
apply (case_tac b, simp_all add: newroot_rel_def)
apply (rule corres_guard_imp)
apply (rule corres_split_norE)
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 (rule corres_split[OF getCurThread_corres], clarsimp)
apply (rule corres_when[OF refl rescheduleRequired_corres])
apply (wpsimp wp: gct_wp)+
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 (wp hoare_drop_imp)
apply (wp threadcontrol_corres_helper2 | wpc | simp)+
apply (rule cteDelete_corres)
apply wp
apply (wpsimp wp: cteDelete_invs' hoare_vcg_conj_lift)
apply (fastforce simp: emptyable_def)
apply fastforce
@ -1409,15 +1409,15 @@ proof -
in corres_gen_asm)
apply (rule_tac F="isArchObjectCap ac" in corres_gen_asm2)
apply (rule corres_split_nor)
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 (rule corres_split[OF getCurThread_corres], clarsimp)
apply (rule corres_when[OF refl rescheduleRequired_corres])
apply (wp gct_wp)+
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 (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)+
@ -1492,11 +1492,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 T2[simplified])
apply (rule corres_split_nor[OF S, simplified])
apply (rule corres_returnOkTT, simp)
apply wp
apply wp
apply (rule T2[simplified])
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 thread_set_ipc_tcb_cap_valid
@ -1801,9 +1801,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 (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)
@ -2009,7 +2009,8 @@ 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 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
@ -2018,7 +2019,6 @@ lemma checkPrio_corres:
apply (clarsimp simp: minPriority_def)
apply (rule corres_returnOkTT)
apply (simp add: minPriority_def)
apply (simp add: tcb_relation_def)
apply (wp gct_wp)+
apply (simp add: cur_tcb_def cur_tcb'_def)+
done
@ -2035,11 +2035,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 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+
apply (corressimp simp: valid_cap_def valid_cap'_def)+
apply (wpsimp simp: valid_cap_def valid_cap'_def)+
done
lemma decodeSetMCPriority_corres:
@ -2054,11 +2054,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 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+
apply (corressimp simp: valid_cap_def valid_cap'_def)+
apply (wpsimp simp: valid_cap_def valid_cap'_def)+
done
lemma valid_objs'_maxPriority':
@ -2171,12 +2171,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 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)+
apply (corressimp simp: valid_cap_def valid_cap'_def)+
apply (wpsimp wp: check_prio_inv checkPrio_inv
simp: valid_cap_def valid_cap'_def)+
done
lemma checkValidIPCBuffer_corres:
@ -2232,7 +2233,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)+
@ -2331,24 +2333,33 @@ 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
getThreadCSpaceRoot getThreadVSpaceRoot
apply (simp add: liftE_bindE liftM_def getThreadCSpaceRoot getThreadVSpaceRoot
cap_CNode_case_throw unlessE_throwError_returnOk unlessE_whenE
split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split[OF slotCapLongRunningDelete_corres])
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])
apply (rule corres_split_norE)
apply (simp(no_asm) add: split_def unlessE_throwError_returnOk
bindE_assoc cap_CNode_case_throw
apply (rule corres_whenE)
apply simp
apply (rule corres_trivial, simp)
apply simp
apply (simp(no_asm) add: split_def bindE_assoc
split del: if_split)
apply (rule corres_splitEE[OF deriveCap_corres])
apply (fastforce dest: list_all2_nthD2[where p=0] simp: cap_map_update_data)
apply (fastforce dest: list_all2_nthD2[where p=0])
apply (rule corres_split_norE)
apply (rule corres_whenE)
apply simp
apply (rule corres_trivial, simp)
apply simp
apply (rule corres_splitEE[OF deriveCap_corres])
apply (clarsimp simp: cap_map_update_data)
apply simp
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
@ -2358,28 +2369,16 @@ lemma decodeSetSpace_corres:
apply (simp split: option.split)
apply (rule corres_trivial, simp)
apply simp
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 (clarsimp simp: cap_map_update_data)
apply simp
apply ((simp only: simp_thms pred_conj_def | wp)+)[2]
apply (rule corres_whenE)
apply simp
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])
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 (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])
@ -2470,8 +2469,10 @@ 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 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)
@ -2527,15 +2528,14 @@ lemma tcb_real_cte_32:
by (clarsimp simp: obj_at'_def projectKOs objBitsKO_def ps_clear_32)
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)+
@ -2553,33 +2553,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 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 (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 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 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 (fastforce simp: valid_cap_def valid_cap'_def dest: hd_in_set)+
done
@ -2592,11 +2591,11 @@ lemma decodeUnbindNotification_corres:
apply (simp add: decode_unbind_notification_def decodeUnbindNotification_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqrE)
apply simp
apply (rule getBoundNotification_corres)
apply (rule corres_trivial)
apply (simp split: option.splits)
apply (simp add: returnOk_def)
apply simp
apply (rule getBoundNotification_corres)
apply wp+
apply auto
done

95
proof/refine/X64/Untyped_R.thy
View File

@ -87,12 +87,11 @@ 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 (rule corres_returnOkTT)
apply simp
apply wp+
apply simp+
apply (clarsimp simp:dc_def,wp)+
@ -295,11 +294,22 @@ next
apply (clarsimp simp: fromAPIType_def X64_H.fromAPIType_def)
apply (rule whenE_throwError_corres, simp)
apply (clarsimp simp: fromAPIType_def X64_H.fromAPIType_def)
apply (rule_tac r' = "\<lambda>cap cap'. cap_relation cap cap'" in corres_splitEE[OF corres_if])
apply (rule_tac r' = "\<lambda>cap cap'. cap_relation cap cap'"
in corres_splitEE[OF corres_if])
apply simp
apply (rule corres_returnOkTT)
apply (rule crel)
apply simp
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rule crel)
apply simp
apply simp
apply (rule getSlotCap_corres,simp)
apply wp+
apply (rule_tac corres_split_norE)
apply (rule corres_if)
apply simp
apply (rule corres_returnOk,clarsimp)
apply (rule corres_returnOkTT, simp)
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)
@ -340,6 +350,20 @@ next
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])
@ -361,20 +385,6 @@ next
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]])+
@ -386,18 +396,7 @@ next
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 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 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
@ -409,7 +408,6 @@ next
apply (rule hoare_strengthen_post [where Q = "\<lambda>r. invs' and cte_at' (cte_map slot)"])
apply wp+
apply (clarsimp simp:invs_pspace_aligned' invs_pspace_distinct')
apply 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 )
@ -961,12 +959,12 @@ 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 assumption
apply assumption
apply assumption
apply (clarsimp dest!: suffix_ConsD)
apply (erule meta_allE, (drule(1) meta_mp)+)
apply assumption
apply assumption
apply assumption
apply assumption
apply (erule(1) z)+
apply simp+
done
@ -1562,7 +1560,8 @@ 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 (rule corres_split)
apply (rule setCTE_corres; simp)
apply (subst bind_return[symmetric],
rule corres_split)
apply (simp add: dc_def[symmetric])
@ -4317,6 +4316,7 @@ lemma resetUntypedCap_corres:
liftE_bindE)
apply (rule corres_guard_imp)
apply (rule corres_split[OF getSlotCap_corres])
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
@ -4325,16 +4325,18 @@ lemma resetUntypedCap_corres:
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 (clarsimp simp add: valid_cap_def cap_aligned_def)
apply (clarsimp simp add: valid_cap_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 (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 (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
@ -4353,8 +4355,12 @@ lemma resetUntypedCap_corres:
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[OF updateFreeIndex_corres])
apply (rule preemptionPoint_corres)
apply simp
apply (simp add: getFreeRef_def getFreeIndex_def free_index_of_def)
apply clarify
@ -4372,11 +4378,7 @@ lemma resetUntypedCap_corres:
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 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
@ -4427,8 +4429,6 @@ lemma resetUntypedCap_corres:
apply (erule order_less_le_trans; simp)
apply simp
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)
@ -4986,11 +4986,10 @@ 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+

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

@ -116,21 +116,19 @@ lemma handleVMFault_corres:
apply (simp add: X64_H.handleVMFault_def handle_vm_fault_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqrE)
apply (rule corres_split_eqrE)
apply (cases fault; simp)
apply simp
apply (rule asUser_getRegister_corres)
apply (simp, wp as_user_typ_at)
apply (simp, wp asUser_typ_ats)
apply simp
apply (rule corres_machine_op [where r="(=)"])
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_getFaultAddress)
apply (rule corres_split_eqrE)
apply simp
apply (rule asUser_getRegister_corres)
apply (cases fault; simp)
apply (simp, wp as_user_typ_at)
apply (simp, wp asUser_typ_ats)
apply wpsimp+
done
crunch valid_global_objs[wp]: do_machine_op "valid_global_objs"
lemma set_current_cr3_corres [corres]:
"cr3_relation c c' \<Longrightarrow> corres dc \<top> \<top> (set_current_cr3 c) (setCurrentUserCR3 c')"
apply (clarsimp simp add: set_current_cr3_def setCurrentUserCR3_def cr3_relation_def)
@ -165,10 +163,10 @@ proof -
make_cr3_def makeCR3_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule set_current_cr3_corres,
simp add: cr3_relation_def cr3_addr_mask_def addrFromKPPtr_def bit_simps)
apply (subst corres_gets)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (rule set_current_cr3_corres,
simp add: cr3_relation_def cr3_addr_mask_def addrFromKPPtr_def bit_simps)
apply (wp | simp)+
done
have Q: "\<And>P P'. corres dc P P'
@ -182,8 +180,8 @@ proof -
od))"
apply (rule corres_guard_imp)
apply (rule corres_split_catch [where f=lfr])
apply (simp, rule P)
apply (subst corres_throwError, simp add: lookup_failure_map_def)
apply (simp, rule P)
apply (wp | simp)+
done
show ?thesis
@ -202,6 +200,7 @@ proof -
cte_wp_at ((=) thread_root) thread_root_slot"
and R'="\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'"
in corres_split[OF getSlotCap_corres])
apply simp
apply (case_tac rv; simp add: isCap_simps Q[simplified])
apply (rename_tac arch_cap)
apply (case_tac arch_cap; simp add: isCap_simps Q[simplified])
@ -209,7 +208,7 @@ proof -
apply (case_tac pm_mapped; simp add: Q[simplified])
apply (clarsimp simp: cap_asid_def)
apply (rule corres_guard_imp)
apply (rule corres_split_catch [where f=lfr, OF P _ wp_post_tautE wp_post_tautE])
apply (rule corres_split_catch [where f=lfr, OF _ P wp_post_tautE wp_post_tautE])
apply (rule corres_split_eqrE[OF findVSpaceForASID_corres[OF refl]])
apply (rule whenE_throwError_corres; simp add: lookup_failure_map_def)
apply (simp only: liftE_bindE)
@ -228,7 +227,6 @@ proof -
apply (frule (1) cte_wp_at_valid_objs_valid_cap)
apply (clarsimp simp: valid_cap_def mask_def word_neq_0_conv asid_wf_def asid_bits_def)
apply (fastforce simp: valid_cap_def mask_def word_neq_0_conv)
apply simp
apply wpsimp
apply (wpsimp wp: get_cap_wp)
apply wp
@ -312,7 +310,8 @@ lemma deleteASID_corres [corres]:
apply (simp add: dom_def)
apply (rule get_asid_pool_corres_inv'[OF refl])
apply (rule corres_when, simp add: mask_asid_low_bits_ucast_ucast asid_low_bits_of_def)
apply (rule corres_split[OF hwASIDInvalidate_corres[where pm=pm]])
apply (rule corres_split)
apply (rule hwASIDInvalidate_corres[where pm=pm]; simp)
apply (rule_tac P="asid_pool_at (the (asidTable (ucast (asid_high_bits_of asid))))
and valid_etcbs"
and P'="pspace_aligned' and pspace_distinct'"
@ -500,12 +499,12 @@ lemma flushTable_corres:
apply (simp add: upto_enum_def bit_simps take_bit_nat_eq_self unsigned_of_nat)
apply (rule corres_guard_imp)
apply (rule corres_split[OF getObject_PTE_corres''])
apply (simp add: bit_simps objBits_simps archObjSize_def)
apply (case_tac rv; case_tac rv'; simp)
apply (rule corres_machine_op)
apply (subgoal_tac "ucast x = y"; simp)
apply (rule corres_rel_imp[OF corres_underlying_trivial]; simp)
apply (wpsimp simp: invalidateTranslationSingleASID_def)
apply (simp add: bit_simps objBits_simps archObjSize_def)
apply (wpsimp)+
apply (rule page_table_pte_atI; simp add: bit_simps ucast_less[where 'b=9, simplified])
apply simp
@ -572,7 +571,7 @@ lemma unmapPageTable_corres:
(unmapPageTable asid' vptr' pt')"
apply (clarsimp simp: assms unmap_page_table_def unmapPageTable_def ignoreFailure_def const_def)
apply (rule corres_guard_imp)
apply (rule corres_split_catch[where E="\<top>\<top>" and E'="\<top>\<top>"], simp)
apply (rule corres_split_catch[where E="\<top>\<top>" and E'="\<top>\<top>", OF _ corres_return_trivial])
apply (rule corres_split_eqrE[OF findVSpaceForASID_corres[OF refl]])
apply (rule corres_split_eqrE[OF lookupPDSlot_corres])
apply (rule corres_splitEE[OF liftE_get_pde_corres])
@ -584,8 +583,8 @@ lemma unmapPageTable_corres:
apply simp
apply (rule corres_split[OF flushTable_corres[OF refl refl refl refl]])
apply (rule corres_split[OF storePDE_corres'])
apply (rule invalidatePageStructureCacheASID_corres)
apply simp
apply (rule invalidatePageStructureCacheASID_corres)
apply ((wpsimp wp: hoare_if get_pde_wp getPDE_wp)+)[8]
apply ((wpsimp wp: lookup_pd_slot_wp hoare_vcg_all_lift_R | wp (once) hoare_drop_imps)+)[2]
apply ((wp find_vspace_for_asid_wp)+)[4]
@ -607,10 +606,10 @@ lemma corres_split_strengthen_ftE:
\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,-; \<lbrace>Q'\<rbrace> j \<lbrace>R'\<rbrace>,- \<rbrakk>
\<Longrightarrow> corres (dc \<oplus> r) (P and Q) (P' and Q') (f >>=E (\<lambda>rv. g rv)) (j >>=E (\<lambda>rv'. k rv'))"
apply (rule_tac r'=r' in corres_splitEE)
apply (rule corres_rel_imp, assumption)
apply (case_tac x, auto)[1]
apply (erule corres_rel_imp)
apply (case_tac x, auto)[1]
apply (rule corres_rel_imp, assumption)
apply (case_tac x, auto)[1]
apply (simp add: validE_R_def)+
done
@ -655,13 +654,10 @@ lemma unmapPage_corres:
(unmapPage sz' asid' vptr' pptr')"
apply (clarsimp simp: assms unmap_page_def unmapPage_def ignoreFailure_def const_def)
apply (rule corres_guard_imp)
apply (rule corres_split_catch[where E="\<top>\<top>" and E'="\<top>\<top>"], simp)
apply (rule corres_split_catch[where E="\<top>\<top>" and E'="\<top>\<top>", OF _ corres_return_trivial])
apply (rule corres_split_strengthen_ftE[where ftr'=dc])
apply (rule findVSpaceForASID_corres[OF refl])
apply (rule corres_splitEE)
apply (clarsimp simp: ucast_id)
apply (rule corres_machine_op, rule corres_Id, rule refl, simp)
apply (rule no_fail_invalidateTranslationSingleASID)
apply (rule_tac F = "vptr < pptr_base" in corres_gen_asm)
apply (rule_tac P="\<exists>\<rhd> vspace and page_map_l4_at vspace and vspace_at_asid asid vspace
and (\<exists>\<rhd> vspace)
@ -680,38 +676,44 @@ lemma unmapPage_corres:
apply (rule corres_splitEE[OF liftE_get_pte_corres])
apply simp
apply (rule corres_split_norE[OF checkMappingPPtr_corres, where r=dc, simplified])
apply (simp add: page_entry_map_def)
apply simp
apply (rule storePTE_corres')
apply (((wpsimp wp: hoare_vcg_all_lift_R get_pte_wp getPTE_wp lookup_pt_slot_wp
simp: page_entry_map_def unlessE_def is_aligned_pml4 if_apply_def2
simp: unlessE_def is_aligned_pml4 if_apply_def2
split_del: if_split
simp_del: dc_simp)+
| wp (once) hoare_drop_imps)+)[10]
| wp (once) hoare_drop_imps)+)[9]
apply (rule corres_guard_imp)
apply (rule corres_split_strengthen_ftE[OF lookupPDSlot_corres])
apply (simp del: dc_simp)
apply (rule corres_splitEE[OF liftE_get_pde_corres])
apply (rule corres_split_norE[OF checkMappingPPtr_corres, where r=dc, simplified])
apply (simp add: page_entry_map_def)
apply simp
apply (rule storePDE_corres')
apply (((wpsimp wp: hoare_vcg_all_lift_R get_pde_wp getPDE_wp lookup_pd_slot_wp
simp: page_entry_map_def unlessE_def is_aligned_pml4 if_apply_def2
simp: unlessE_def is_aligned_pml4 if_apply_def2
split_del: if_split
simp_del: dc_simp)+
| wp (once) hoare_drop_imps)+)[10]
| wp (once) hoare_drop_imps)+)[9]
apply (rule corres_guard_imp)
apply (rule corres_split_strengthen_ftE[OF lookupPDPTSlot_corres])
apply (simp del: dc_simp)
apply (rule corres_splitEE[OF liftE_get_pdpte_corres])
apply (rule corres_split_norE[OF checkMappingPPtr_corres, where r=dc, simplified])
apply (simp add: page_entry_map_def)
apply simp
apply (rule storePDPTE_corres')
apply (((wpsimp wp: hoare_vcg_all_lift_R get_pdpte_wp getPDPTE_wp
lookup_pdpt_slot_wp
simp: page_entry_map_def unlessE_def is_aligned_pml4 if_apply_def2
simp: unlessE_def is_aligned_pml4 if_apply_def2
split_del: if_split
simp_del: dc_simp)+
| wp (once) hoare_drop_imps)+)
apply (rule corres_machine_op, rule corres_Id, rule refl, simp)
apply (rule no_fail_invalidateTranslationSingleASID)
apply wpsimp+
apply (rule conjI[OF disjI1], clarsimp)
apply (clarsimp simp: invs_vspace_objs invs_psp_aligned valid_unmap_def invs_arch_state
invs_equal_kernel_mappings)
@ -883,15 +885,16 @@ proof -
apply (clarsimp simp: mapM_Cons bind_assoc split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split[OF storePTE_corres'])
apply (rule corres_split_deprecated[where r'="(=)"])
apply (rule corres_underlying_split[where r'=dc, OF _ corres_return_eq_same[OF refl]
hoare_post_taut hoare_post_taut])
apply simp
apply (rule invalidatePageStructureCacheASID_corres)
apply (rule corres_split[where r'="(=)"])
apply (case_tac cap; clarsimp simp add: is_pg_cap_def)
apply (case_tac m; clarsimp)
apply (rule corres_fail[where P=\<top> and P'=\<top>])
apply (simp add: same_refs_def)
apply (rule corres_underlying_split[where r'=dc, OF _ corres_return_eq_same[OF refl]
hoare_post_taut hoare_post_taut])
apply simp
apply (rule invalidatePageStructureCacheASID_corres)
apply (wpsimp simp: invs_psp_aligned)+
apply (frule (1) mapping_map_pde, clarsimp)
apply (clarsimp simp: mapping_map_simps valid_slots'_def valid_slots_def valid_page_inv_def
@ -900,15 +903,16 @@ proof -
apply (clarsimp simp: mapM_Cons bind_assoc split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split[OF storePDE_corres'])
apply (rule corres_split_deprecated[where r'="(=)"])
apply simp
apply (rule corres_underlying_split[where r'=dc, OF _ corres_return_eq_same[OF refl]
hoare_post_taut hoare_post_taut])
apply (rule invalidatePageStructureCacheASID_corres)
apply (rule corres_split[where r'="(=)"])
apply (case_tac cap; clarsimp simp add: is_pg_cap_def)
apply (case_tac m; clarsimp)
apply (rule corres_fail[where P=\<top> and P'=\<top>])
apply (simp add: same_refs_def)
apply simp
apply (rule corres_underlying_split[where r'=dc, OF _ corres_return_eq_same[OF refl]
hoare_post_taut hoare_post_taut])
apply (rule invalidatePageStructureCacheASID_corres)
apply (wpsimp simp: invs_psp_aligned)+
apply (frule (1) mapping_map_pdpte, clarsimp)
apply (clarsimp simp: mapping_map_simps valid_slots'_def valid_slots_def valid_page_inv_def
@ -917,15 +921,16 @@ proof -
apply (clarsimp simp: mapM_Cons bind_assoc split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split[OF storePDPTE_corres'])
apply (rule corres_split_deprecated[where r'="(=)"])
apply simp
apply (rule corres_underlying_split[where r'=dc, OF _ corres_return_eq_same[OF refl]
hoare_post_taut hoare_post_taut])
apply (rule invalidatePageStructureCacheASID_corres)
apply (rule corres_split[where r'="(=)"])
apply (case_tac cap; clarsimp simp add: is_pg_cap_def)
apply (case_tac m; clarsimp)
apply (rule corres_fail[where P=\<top> and P'=\<top>])
apply (simp add: same_refs_def)
apply simp
apply (rule corres_underlying_split[where r'=dc, OF _ corres_return_eq_same[OF refl]
hoare_post_taut hoare_post_taut])
apply (rule invalidatePageStructureCacheASID_corres)
apply (wpsimp simp: invs_psp_aligned)+
apply (wp arch_update_cap_invs_map set_cap_valid_page_map_inv)
apply (wp arch_update_updateCap_invs)
@ -1122,11 +1127,12 @@ lemma performPageTableInvocation_corres:
apply (rule corres_split[OF updateCap_same_master])
apply assumption
apply (rule corres_split[OF storePDE_corres'])
apply (rule corres_split_deprecated[where r'="(=)" and P="\<top>" and P'="\<top>"])
apply simp
apply (rule invalidatePageStructureCacheASID_corres)
apply (rule corres_split[where r'="(=)" and P="\<top>" and P'="\<top>"])
apply (case_tac cap; clarsimp simp add: is_pt_cap_def)
apply (solves \<open>clarsimp split: option.splits\<close>)
apply simp
apply (rule invalidatePageStructureCacheASID_corres)
apply (wpsimp wp: set_cap_typ_at)+
apply (clarsimp simp: invs_valid_objs invs_psp_aligned invs_distinct is_arch_update_def
cte_wp_at_caps_of_state )
@ -1145,17 +1151,18 @@ lemma performPageTableInvocation_corres:
apply (simp add: case_option_If2 getSlotCap_def split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (simp add: liftM_def)
apply (rule corres_split[OF get_cap_corres])
apply (rule_tac F="is_pt_cap x" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_pt_cap_def update_map_data_def)
apply (wp get_cap_wp)+
apply (rule corres_if[OF refl])
apply (rule corres_split[OF unmapPageTable_corres[OF refl refl refl]])
apply (rule clear_page_table_corres[simplified bit_simps bitSimps, simplified])
apply wp+
apply (rule corres_trivial, simp)
apply (simp add: liftM_def)
apply (rule corres_split[OF get_cap_corres])
apply (rule_tac F="is_pt_cap x" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_pt_cap_def update_map_data_def)
apply (wp get_cap_wp)
apply wp
apply (simp add: cte_wp_at_caps_of_state pred_conj_def
split del: if_split)
apply (rule hoare_lift_Pf2[where f=caps_of_state])
@ -1205,7 +1212,7 @@ lemma unmapPageDirectory_corres:
apply (clarsimp simp: assms unmap_pd_def unmapPageDirectory_def flushPD_def
ignoreFailure_def const_def)
apply (rule corres_guard_imp)
apply (rule corres_split_catch[where E="\<top>\<top>" and E'="\<top>\<top>"], simp)
apply (rule corres_split_catch[where E="\<top>\<top>" and E'="\<top>\<top>", OF _ corres_return_trivial])
apply (rule corres_split_eqrE[OF findVSpaceForASID_corres[OF refl]])
apply (rule corres_split_eqrE[OF lookupPDPTSlot_corres])
apply (rule corres_splitEE[OF liftE_get_pdpte_corres])
@ -1216,8 +1223,8 @@ lemma unmapPageDirectory_corres:
split: X64_A.pdpte.splits)
apply simp
apply (rule corres_split_nor[OF flush_all_corres[OF refl refl]])
apply (rule corres_split_deprecated[OF invalidatePageStructureCacheASID_corres
storePDPTE_corres'])
apply (rule corres_split[OF storePDPTE_corres'
invalidatePageStructureCacheASID_corres])
apply ((wpsimp wp: get_pdpte_wp simp: pdpte_at_def)+)[8]
apply (wpsimp wp: hoare_drop_imps)
apply ((wp lookup_pdpt_slot_wp find_vspace_for_asid_wp)+)[6]
@ -1251,11 +1258,12 @@ lemma performPageDirectoryInvocation_corres:
apply (rule corres_split[OF updateCap_same_master])
apply assumption
apply (rule corres_split[OF storePDPTE_corres'])
apply (rule corres_split_deprecated[where r'="(=)" and P="\<top>" and P'="\<top>"])
apply simp
apply (rule invalidatePageStructureCacheASID_corres)
apply (rule corres_split[where r'="(=)" and P="\<top>" and P'="\<top>"])
apply (case_tac cap; clarsimp simp add: is_pd_cap_def)
apply (solves \<open>clarsimp split: option.splits\<close>)
apply simp
apply (rule invalidatePageStructureCacheASID_corres)
apply (wpsimp wp: set_cap_typ_at)+
apply (clarsimp simp: invs_valid_objs invs_psp_aligned invs_distinct is_arch_update_def
cte_wp_at_caps_of_state )
@ -1274,17 +1282,18 @@ lemma performPageDirectoryInvocation_corres:
apply (simp add: case_option_If2 getSlotCap_def split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (simp add: liftM_def)
apply (rule corres_split[OF get_cap_corres])
apply (rule_tac F="is_pd_cap x" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_pd_cap_def update_map_data_def)
apply (wp get_cap_wp)+
apply (rule corres_if[OF refl])
apply (rule corres_split[OF unmapPageDirectory_corres[OF refl refl refl]])
apply (rule clear_page_directory_corres[simplified bit_simps bitSimps, simplified])
apply wp+
apply (rule corres_trivial, simp)
apply (simp add: liftM_def)
apply (rule corres_split[OF get_cap_corres])
apply (rule_tac F="is_pd_cap x" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_pd_cap_def update_map_data_def)
apply (wp get_cap_wp)
apply wp
apply (simp add: cte_wp_at_caps_of_state pred_conj_def
split del: if_split)
apply (rule hoare_lift_Pf2[where f=caps_of_state])
@ -1326,7 +1335,7 @@ lemma unmapPDPT_corres:
invalidatePageStructureCacheASID_def
ignoreFailure_def const_def)
apply (rule corres_guard_imp)
apply (rule corres_split_catch[where E="\<top>\<top>" and E'="\<top>\<top>"], simp)
apply (rule corres_split_catch[where E="\<top>\<top>" and E'="\<top>\<top>", OF _ corres_return_trivial])
apply (rule corres_split_eqrE[OF findVSpaceForASID_corres[OF refl]])
apply (rule corres_splitEE[OF liftE_get_pml4e_corres])
apply (rule corres_splitEE[where r'=dc])
@ -1375,12 +1384,13 @@ lemma performPDPTInvocation_corres:
apply (rule corres_guard_imp)
apply (rule corres_split[OF updateCap_same_master])
apply assumption
apply (rule corres_split[OF store_pml4e_corres'])
apply (rule corres_split_deprecated[where r'="(=)" and P="\<top>" and P'="\<top>"])
apply simp
apply (rule invalidatePageStructureCacheASID_corres)
apply (rule corres_split)
apply (rule store_pml4e_corres'; simp)
apply (rule corres_split[where r'="(=)" and P="\<top>" and P'="\<top>"])
apply (case_tac cap; clarsimp simp add: is_pdpt_cap_def)
apply (solves \<open>clarsimp split: option.splits\<close>)
apply simp
apply (rule invalidatePageStructureCacheASID_corres)
apply (wpsimp wp: set_cap_typ_at)+
apply (clarsimp simp: invs_valid_objs invs_psp_aligned invs_distinct is_arch_update_def
cte_wp_at_caps_of_state )
@ -1399,17 +1409,18 @@ lemma performPDPTInvocation_corres:
apply (simp add: case_option_If2 getSlotCap_def split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (simp add: liftM_def)
apply (rule corres_split[OF get_cap_corres])
apply (rule_tac F="is_pdpt_cap x" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_pdpt_cap_def update_map_data_def)
apply (wp get_cap_wp)+
apply (rule corres_if[OF refl])
apply (rule corres_split[OF unmapPDPT_corres[OF refl refl refl]])
apply (rule clear_pdpt_corres[simplified bit_simps bitSimps, simplified])
apply wp+
apply (rule corres_trivial, simp)
apply (simp add: liftM_def)
apply (rule corres_split[OF get_cap_corres])
apply (rule_tac F="is_pdpt_cap x" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_pdpt_cap_def update_map_data_def)
apply (wp get_cap_wp)
apply wp
apply (simp add: cte_wp_at_caps_of_state pred_conj_def
split del: if_split)
apply (rule hoare_lift_Pf2[where f=caps_of_state])
@ -1459,12 +1470,13 @@ lemma performASIDPoolInvocation_corres:
apply (cases ap, simp add: asid_pool_invocation_map_def)
apply (rename_tac word1 word2 prod)
apply (rule corres_guard_imp)
apply (rule corres_split[OF getSlotCap_corres[OF refl] get_cap_wp getSlotCap_wp])
apply (rule corres_split[OF getSlotCap_corres[OF refl] _ get_cap_wp getSlotCap_wp])
apply (rule_tac F="\<exists>p asid. rv = Structures_A.ArchObjectCap (X64_A.PML4Cap p asid)"
in corres_gen_asm; elim exE)
apply (simp cong: corres_weak_cong)
apply (rule subst[OF helper], assumption)
apply (rule corres_split[OF updateCap_same_master])
apply simp
unfolding store_asid_pool_entry_def
apply (rule corres_split[where r'="\<lambda>pool pool'. pool = pool' \<circ> ucast"])
apply (simp cong: corres_weak_cong)
@ -1475,7 +1487,6 @@ lemma performASIDPoolInvocation_corres:
apply (rule setObject_ASIDPool_corres')
apply (rule ext; clarsimp simp: inv_def mask_asid_low_bits_ucast_ucast)
apply (wp getASID_wp)+
apply simp
apply (wpsimp wp: set_cap_typ_at hoare_drop_imps)
apply (wpsimp wp: hoare_drop_imps)
by (auto simp: valid_apinv_def cte_wp_at_def is_pml4_cap_def