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

riscv refine: update for changed corres split rules 

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

6
proof/refine/RISCV64/ArchAcc_R.thy
View File

@ -628,7 +628,8 @@ next
apply (subst pt_lookup_slot_from_level_rec)
apply (simp add: lookupPTSlotFromLevel.simps Let_def obind_comp_dist if_comp_dist
gets_the_if_distrib checkPTAt_def)
apply (rule corres_guard_imp, rule corres_split_deprecated[where r'=pte_relation'])
apply (rule corres_guard_imp, rule corres_split[where r'=pte_relation'])
apply (rule pteAtIndex_corres, simp)
apply (rule corres_if3)
apply (rename_tac pte pte', case_tac pte; (simp add: isPageTablePTE_def))
apply (rule corres_stateAssert_implied)
@ -646,7 +647,6 @@ next
apply (rule corres_inst[where P=\<top> and P'=\<top>])
apply (clarsimp simp: ptSlotIndex_def pt_slot_offset_def pt_index_def pt_bits_left_def
ptIndex_def ptBitsLeft_def)
apply (rule pteAtIndex_corres, simp)
apply wpsimp+
apply (frule (5) vs_lookup_table_is_aligned)
apply (rule conjI)
@ -757,6 +757,7 @@ next
apply (rule corres_initial_splitE[where r'=dc])
apply (corressimp simp: lookup_failure_map_def)
apply (rule corres_splitEE[where r'=pte_relation'])
apply (simp, rule getObject_PTE_corres)
apply (rule whenE_throwError_corres)
apply (simp add: lookup_failure_map_def)
apply (rename_tac pte pte', case_tac pte; simp add: isPageTablePTE_def)
@ -776,7 +777,6 @@ next
apply (clarsimp simp: RISCV64_A.is_PageTablePTE_def pptr_from_pte_def getPPtrFromHWPTE_def
addr_from_ppn_def)
apply (simp add: state_relation_def)
apply (simp, rule getObject_PTE_corres)
apply wpsimp+
apply (simp add: bit0.neq_0_conv)
apply (frule (5) vs_lookup_table_is_aligned)

17
proof/refine/RISCV64/Arch_R.thy
View File

@ -158,9 +158,11 @@ lemma performASIDControlInvocation_corres:
apply (rule corres_split)
apply (erule deleteObjects_corres)
apply (simp add:pageBits_def)
apply (rule corres_split[OF getSlotCap_corres])
apply (rule corres_split[OF getSlotCap_corres], 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,
@ -210,8 +212,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 default_arch_object_def pred_conj_def)
apply (clarsimp simp: conj_comms
@ -624,9 +624,9 @@ lemma maybeVSpaceForASID_corres:
apply (simp add: maybeVSpaceForASID_def gets_vspace_for_asid_is_catch)
apply (rule corres_guard_imp)
apply (rule corres_split_catch)
apply (rule corres_trivial, simp)
apply (simp add: o_def)
apply (rule findVSpaceForASID_corres, simp)
apply (rule corres_trivial, simp)
apply wpsimp+
done
@ -930,8 +930,9 @@ lemma arch_performInvocation_corres:
apply (clarsimp simp: archinv_relation_def)
apply (cases ai)
apply (clarsimp simp: archinv_relation_def performRISCVMMUInvocation_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)
@ -942,14 +943,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/RISCV64/Bits_R.thy
View File

@ -219,14 +219,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:
@ -406,9 +405,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
@ -446,11 +444,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

91
proof/refine/RISCV64/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
@ -6723,9 +6720,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)
@ -8703,8 +8700,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)
@ -8735,7 +8732,7 @@ lemma invokeCNode_corres:
apply (subgoal_tac "thread + 2^cte_level_bits * tcbCallerSlot = cte_map (thread, tcb_cnode_index 3)")
prefer 2
apply (simp add: cte_map_def tcb_cnode_index_def tcbCallerSlot_def cte_level_bits_def)
apply (rule corres_split[OF getSlotCap_corres])
apply (rule corres_split[OF getSlotCap_corres], 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

27
proof/refine/RISCV64/CSpace1_R.thy
View File

@ -3886,10 +3886,7 @@ lemma getCTE_get:
done
lemma setUntypedCapAsFull_corres:
"\<lbrakk>cap_relation c c'; src' = cte_map src; dest' = cte_map dest;
cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap;
cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer \<and>
mdbNext (cteMDBNode rv') = nullPointer\<rbrakk>
"\<lbrakk>cap_relation c c'; cap_relation src_cap (cteCap srcCTE)\<rbrakk>
\<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and
pspace_aligned and pspace_distinct)
(cte_wp_at' ((=) srcCTE) (cte_map src) and
@ -5165,7 +5162,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)
@ -5191,9 +5189,9 @@ lemma cteInsert_corres:
apply (subgoal_tac "no_mloop (cdt a)")
prefer 2
apply (simp add: valid_mdb_def)
apply (clarsimp simp: exec_gets update_cdt_def bind_assoc
set_cdt_def
exec_get exec_put set_original_def modify_def simp del: fun_upd_apply
apply (clarsimp simp: exec_gets update_cdt_def bind_assoc set_cdt_def
exec_get exec_put set_original_def modify_def
simp del: fun_upd_apply
| (rule bind_execI[where f="cap_insert_ext x y z i p" for x y z i p], clarsimp simp: exec_gets exec_get put_def mdb_insert_abs.cap_insert_ext_det_def2 update_cdt_list_def set_cdt_list_def, rule refl))+
apply (clarsimp simp: put_def state_relation_def)
apply (drule updateCap_stuff)
@ -5205,12 +5203,10 @@ lemma cteInsert_corres:
prev_update_modify_mdb_relation)
apply (subgoal_tac "cte_map dest \<noteq> 0")
prefer 2
apply (clarsimp simp: valid_mdb'_def
valid_mdb_ctes_def no_0_def)
apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
apply (subgoal_tac "cte_map src \<noteq> 0")
prefer 2
apply (clarsimp simp: valid_mdb'_def
valid_mdb_ctes_def no_0_def)
apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
apply (thin_tac "ksMachineState t = p" for p t)+
apply (thin_tac "ksCurThread t = p" for p t)+
apply (thin_tac "ksIdleThread t = p" for p t)+
@ -5388,8 +5384,7 @@ lemma cteInsert_corres:
apply simp
apply (subst (asm) is_cap_revocable_eq, assumption, assumption)
apply (rule derived_sameRegionAs)
apply (subst is_derived_eq[symmetric], assumption,
assumption, assumption, assumption, assumption)
apply (subst is_derived_eq[symmetric]; assumption)
apply assumption
subgoal by (clarsimp simp: cte_wp_at_def is_derived_def is_cap_simps cap_master_cap_simps
dest!:cap_master_cap_eqDs)
@ -5444,7 +5439,7 @@ lemma cteInsert_corres:
apply(drule cte_map_inj_eq')
apply(simp_all)[2]
apply(drule_tac p="cte_map src" in valid_mdbD1')
apply(simp)
subgoal by(simp)
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
subgoal by(clarsimp)
apply(clarsimp)
@ -5555,8 +5550,6 @@ lemma cteInsert_corres:
apply (erule (5) cte_map_inj)
(* FIXME *)
apply (rule setUntypedCapAsFull_corres)
apply simp+
apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb
set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap
setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+

10
proof/refine/RISCV64/CSpace_R.thy
View File

@ -3450,11 +3450,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
@ -4754,7 +4754,8 @@ 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; 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)
@ -4878,8 +4879,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)+
@ -4898,7 +4897,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/RISCV64/Detype_R.thy
View File

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

9
proof/refine/RISCV64/Finalise_R.thy
View File

@ -3444,7 +3444,6 @@ lemma arch_finaliseCap_corres:
elim: is_aligned_weaken)[2]
apply (rule corres_guard_imp)
apply (rule corres_split_catch[where f=dc])
apply (rule unmapPageTable_corres; simp)
apply (rule corres_splitEE)
apply (rule corres_rel_imp[where r="dc \<oplus> (=)"], rule findVSpaceForASID_corres; simp)
apply (case_tac x; simp)
@ -3454,6 +3453,8 @@ lemma arch_finaliseCap_corres:
apply (rule deleteASID_corres; rule refl)
apply simp
apply (wpsimp wp: hoare_vcg_if_lift_ER hoare_drop_imps)+
apply (rule unmapPageTable_corres; simp)
apply (wpsimp wp: hoare_drop_imps)+
apply (clarsimp simp: invs_psp_aligned invs_distinct invs_vspace_objs invs_valid_asid_table)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (drule (1) caps_of_state_valid)
@ -3477,8 +3478,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
@ -3503,8 +3504,8 @@ lemma unbindMaybeNotification_corres:
apply (rule corres_return_trivial)
apply simp
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
@ -3566,8 +3567,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/RISCV64/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)

71
proof/refine/RISCV64/Interrupt_R.thy
View File

@ -220,8 +220,9 @@ lemma arch_decodeIRQControlInvocation_corres:
apply (clarsimp simp add: minIRQ_def maxIRQ_def ucast_nat_def)
apply (rule corres_split_eqr[OF is_irq_active_corres])
apply (rule whenE_throwError_corres, clarsimp, clarsimp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rule corres_splitEE[OF ensureEmptySlot_corres])
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; clarsimp)
apply (rule corres_splitEE[OF ensureEmptySlot_corres], simp)
apply (rule corres_returnOkTT)
apply (clarsimp simp: arch_irq_control_inv_relation_def)
apply (wpsimp wp: isIRQActive_inv arch_check_irq_valid' checkIRQ_inv
@ -268,8 +269,9 @@ lemma decodeIRQControlInvocation_corres:
apply (clarsimp simp add: minIRQ_def maxIRQ_def ucast_nat_def)
apply (rule corres_split_eqr[OF is_irq_active_corres])
apply (rule whenE_throwError_corres, clarsimp, clarsimp)
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply (rule corres_splitEE[OF ensureEmptySlot_corres])
apply (rule corres_splitEE)
apply (rule lookupSlotForCNodeOp_corres; clarsimp)
apply (rule corres_splitEE[OF ensureEmptySlot_corres], simp)
apply (rule corres_returnOkTT)
apply (clarsimp simp: arch_irq_control_inv_relation_def)
apply (wpsimp wp: isIRQActive_inv arch_check_irq_valid' checkIRQ_inv
@ -466,7 +468,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 no_fail_setIRQTrigger: "no_fail \<top> (setIRQTrigger irq trig)"
by (simp add: setIRQTrigger_def)
@ -491,13 +493,12 @@ lemma arch_performIRQControl_corres:
apply (cases x2; simp add: RISCV64_H.performIRQControl_def invoke_irq_control.cases IRQ_def)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (rule setIRQTrigger_corres)
apply (rule corres_split_nor)
apply (rule cteInsert_simple_corres; simp)
apply (rule setIRQState_corres)
apply (simp add: irq_state_relation_def)
apply (rule cteInsert_simple_corres; simp)
apply (wp | simp add: irq_state_relation_def IRQHandler_valid IRQHandler_valid')+
apply (rule setIRQTrigger_corres)
apply wp+
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 is_simple_cap_arch_def)
@ -518,9 +519,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_simple_cap_arch_def
is_cap_simps safe_parent_for_def)
@ -650,7 +651,27 @@ 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 (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[OF ethread_set_corres])
apply (simp add: sch_act_wf_weak etcb_relation_def pred_conj_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 (rule corres_when,simp)
apply (rule corres_split[OF decDomainTime_corres])
@ -662,26 +683,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 (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 (wpsimp wp: static_imp_wp threadSet_timeslice_invs threadSet_valid_queues
threadSet_valid_queues' tcbSchedAppend_valid_objs'
threadSet_pred_tcb_at_state threadSet_weak_sch_act_wf
@ -718,11 +719,11 @@ 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)
apply (rule corres_gen_asm2)
apply (case_tac st, simp_all add: irq_state_relation_def split: irqstate.split_asm)
apply (simp add: getSlotCap_def bind_assoc)
apply (rule corres_guard_imp)
@ -743,10 +744,10 @@ apply (rule corres_split_deprecated)
apply clarsimp
apply fastforce
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated)
apply (rule corres_split)
apply simp
apply (rule corres_split[OF timerTick_corres corres_machine_op])
apply (rule corres_eq_trivial, simp+)
apply (rule corres_eq_trivial, wpsimp+)
apply (rule corres_machine_op)
apply (rule corres_eq_trivial, (simp add: no_fail_ackInterrupt)+)
apply wp+

75
proof/refine/RISCV64/IpcCancel_R.thy
View File

@ -187,9 +187,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)
@ -210,9 +210,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)
@ -235,9 +235,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)
@ -258,9 +258,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)
@ -313,15 +313,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)+
@ -1194,20 +1194,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:
@ -1379,11 +1380,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)
@ -1395,6 +1391,11 @@ lemma (in delete_one) suspend_corres:
apply (rule corres_underlying_trivial)
apply (wpsimp simp: RISCV64.setRegister_def RISCV64.getRegister_def)
apply (rule corres_return_trivial)
apply (rule corres_split_nor[OF setThreadState_corres])
apply wpsimp
apply (rule tcbSchedDequeue_corres')
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 \<and> pspace_aligned s \<and> pspace_distinct s"])
apply simp
@ -1883,7 +1884,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
@ -1929,7 +1930,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)+
@ -1982,7 +1983,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
@ -1993,12 +1995,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)+
@ -2566,18 +2565,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> pspace_aligned s \<and> pspace_distinct s"
@ -2591,6 +2587,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
@ -2603,12 +2600,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)

124
proof/refine/RISCV64/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)
@ -1325,12 +1325,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
@ -1424,28 +1424,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
@ -1620,15 +1620,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
@ -1838,8 +1838,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)+
@ -2144,8 +2143,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)
@ -2180,7 +2179,11 @@ 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 simp
apply (rule corres_split)
apply (rule threadset_corresT;
clarsimp simp add: tcb_relation_def fault_rel_optionation_def cteSizeBits_def
tcb_cap_cases_def tcb_cte_cases_def exst_same_def)
apply (rule_tac Q="valid_sched and cur_tcb and tcb_at receiver and pspace_aligned and pspace_distinct"
and Q'="tcb_at' receiver and cur_tcb'
and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
@ -2189,15 +2192,15 @@ lemma doReplyTransfer_corres:
apply (case_tac rvb, simp_all)[1]
apply (rule corres_guard_imp)
apply (rule corres_split[OF setThreadState_corres])
apply (clarsimp simp: tcb_relation_def)
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)+
sts_st_tcb' sts_valid_queues
| 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 cteSizeBits_def
tcb_cap_cases_def tcb_cte_cases_def exst_same_def)+
apply (clarsimp simp: tcb_relation_def)
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'
@ -2279,6 +2282,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"
@ -2305,8 +2310,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
@ -2421,9 +2424,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 invs_distinct)
apply clarsimp
@ -2431,9 +2434,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 invs_distinct)
apply clarsimp
@ -2447,6 +2450,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
@ -2456,9 +2460,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)
@ -2484,7 +2488,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)
@ -2528,6 +2531,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"
@ -2536,10 +2540,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
@ -2551,7 +2554,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
@ -2615,11 +2617,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
@ -2647,7 +2649,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)
@ -2663,7 +2667,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)+
@ -2678,7 +2681,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)
@ -2688,7 +2693,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)+
@ -3100,6 +3104,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 clarsimp
apply (rule setMessageInfo_corres)
apply (wp hoare_case_option_wp hoare_valid_ipc_buffer_ptr_typ_at'
| clarsimp simp: invs_distinct invs_psp_aligned)+
@ -3163,7 +3168,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)
@ -3183,9 +3193,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
@ -3200,6 +3210,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.
@ -3234,8 +3245,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'
@ -3248,7 +3259,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
@ -3264,19 +3274,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 invs_distinct)
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)+
@ -3315,9 +3320,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)
apply (clarsimp simp: invs_distinct)
@ -3327,9 +3332,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)
@ -3373,7 +3378,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)
@ -3406,9 +3413,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
@ -3432,6 +3436,7 @@ lemma handleDoubleFault_corres:
apply (rule corres_guard_imp)
apply (subst bind_return [symmetric],
rule corres_split[OF setThreadState_corres])
apply simp
apply (rule corres_noop2)
apply (simp add: exs_valid_def return_def)
apply (rule hoare_eq_P)
@ -4177,16 +4182,15 @@ 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 wpsimp+
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)
apply auto
done

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

@ -577,14 +577,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
@ -668,6 +668,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/RISCV64/Retype_R.thy
View File

@ -1415,16 +1415,20 @@ lemma objBitsKO_gt_0: "0 < objBitsKO ko"
apply (simp_all add:archObjSize_def bit_simps)
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
@ -1778,12 +1782,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)
@ -1791,6 +1790,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)
@ -5113,19 +5117,19 @@ lemma corres_retype_region_createNewCaps:
split del: if_split)[8]
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/RISCV64/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+
@ -121,21 +121,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
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
@ -1805,30 +1814,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
@ -1837,14 +1854,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
@ -1865,9 +1880,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
@ -2261,7 +2273,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)
@ -2271,7 +2285,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+

58
proof/refine/RISCV64/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,19 @@ 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, 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 +461,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])
@ -1208,21 +1210,21 @@ lemma handleInvocation_corres:
apply wp[1]
apply (clarsimp simp: when_def)
apply (rule replyFromKernel_corres)
apply (rule corres_split[OF setThreadState_corres])
apply (rule corres_split[OF setThreadState_corres], simp)
apply (rule corres_splitEE[OF performInvocation_corres])
apply 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 (wp reply_from_kernel_tcb_at)
apply (rule impI, wp+)
apply (simp)+
apply (wpsimp wp: hoare_drop_imps|strengthen invs_distinct invs_psp_aligned)+
apply (rule_tac Q="\<lambda>rv. einvs and simple_sched_action and valid_invocation rve
and (\<lambda>s. thread = cur_thread s)
@ -1475,7 +1477,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
@ -1498,17 +1499,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)
@ -2001,10 +2006,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
@ -2015,8 +2021,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)

118
proof/refine/RISCV64/TcbAcc_R.thy
View File

@ -460,10 +460,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
@ -1379,22 +1379,20 @@ proof -
apply (fastforce simp: tcb_at_cross state_relation_def)
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_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[OF L4])
apply 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
apply (rule no_fail_pre_and, wp)
apply (rule L3[simplified])
apply simp
apply simp
prefer 5
apply (rule no_fail_pre_and, wp)
apply (wp select_f_inv | simp)+
apply (rule L1[simplified])
apply wp+
apply auto
done
qed
@ -1837,18 +1835,23 @@ 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'="(=)", OF ethreadget_corres])
apply (simp add: etcb_relation_def)
apply (rule corres_split[where r'="(=)", OF 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
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
project_inject)
done
@ -1886,14 +1889,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 st_tcb_at_def obj_at_def is_tcb
split: Deterministic_A.scheduler_action.split)
@ -2041,15 +2045,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 =
@ -2081,8 +2089,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])
@ -2093,7 +2101,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
@ -3212,7 +3219,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
@ -3221,11 +3234,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
@ -3291,7 +3299,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
@ -3301,7 +3309,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}"])
@ -3316,6 +3323,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
@ -3408,12 +3416,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
@ -3422,7 +3432,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)
@ -3431,10 +3445,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
@ -3503,13 +3515,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
@ -3520,6 +3532,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
@ -3608,8 +3621,10 @@ lemma lookupIPCBuffer_corres':
apply (simp add: lookup_ipc_buffer_def RISCV64_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'"
@ -3639,9 +3654,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
@ -4521,11 +4534,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':

151
proof/refine/RISCV64/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
@ -211,7 +211,7 @@ lemma restart_corres:
apply (clarsimp simp add: runnable_tsr idle_tsr when_def)
apply (rule corres_split_nor[OF cancel_ipc_corres])
apply (rule corres_split_nor[OF setupReplyMaster_corres])
apply (rule corres_split_nor[OF setThreadState_corres])
apply (rule corres_split_nor[OF setThreadState_corres], simp)
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'
@ -228,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>"
@ -286,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)
@ -295,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)
@ -393,12 +391,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 add: invs_distinct invs_psp_aligned| wp)+
done
have R: "\<And>src src' des des' xs ys. \<lbrakk> src = src'; des = des'; xs = ys \<rbrakk> \<Longrightarrow>
@ -430,28 +428,28 @@ 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 (wp mapM_x_wp' | simp)+
apply (rule corres_split_nor)
apply (rule corres_when[OF refl])
apply (rule R[OF refl refl])
apply (simp add: gpRegisters_def)
apply (rule 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_state_def valid_pspace_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 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)+
@ -621,6 +619,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])
@ -628,8 +627,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
@ -1363,17 +1362,17 @@ 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 thread_set_ipc_weak_valid_sched_action|wp (once) hoare_drop_imp)+
apply simp
apply (wp threadcontrol_corres_helper2 | wpc | simp)+
apply (rule cteDelete_corres)
apply (wp|strengthen einvs_valid_etcbs)+
apply (wpsimp wp: cteDelete_invs' hoare_vcg_conj_lift)
apply (fastforce simp: emptyable_def)
@ -1467,11 +1466,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
@ -1776,9 +1775,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 invs_distinct)
apply (clarsimp simp: invs_valid_queues' invs_queues)
@ -1984,7 +1983,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
@ -1993,7 +1993,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
@ -2010,11 +2009,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+
by (corressimp simp: valid_cap_def valid_cap'_def)+
by (wpsimp simp: valid_cap_def valid_cap'_def)+
lemma decodeSetMCPriority_corres:
"\<lbrakk> cap_relation cap cap'; is_thread_cap cap;
@ -2028,11 +2027,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+
by (corressimp simp: valid_cap_def valid_cap'_def)+
by (wpsimp simp: valid_cap_def valid_cap'_def)+
lemma valid_objs'_maxPriority':
"\<And>s t. \<lbrakk> valid_objs' s; tcb_at' t s \<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbMCP tcb \<le> maxPriority) t s"
@ -2143,12 +2142,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:
@ -2202,7 +2202,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)+
@ -2301,24 +2302,32 @@ lemma decodeSetSpace_corres:
apply (cases "3 \<le> length args \<and> 2 \<le> length extras'")
apply (clarsimp simp: val_le_length_Cons list_all2_Cons2
split del: if_split)
apply (simp add: liftE_bindE liftM_def
apply (simp add: liftE_bindE liftM_def unlessE_throwError_returnOk unlessE_whenE
bindE_assoc cap_CNode_case_throw
getThreadCSpaceRoot getThreadVSpaceRoot
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
split del: if_split)
apply (rule corres_whenE)
apply simp
apply (rule corres_trivial, simp)
apply simp
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)[1]
@ -2327,28 +2336,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])
@ -2439,8 +2436,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)
@ -2496,15 +2495,14 @@ lemma tcb_real_cte_32:
by (clarsimp simp: obj_at'_def 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)+
@ -2522,33 +2520,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
@ -2561,11 +2558,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

90
proof/refine/RISCV64/Untyped_R.thy
View File

@ -90,12 +90,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)+
@ -297,11 +296,22 @@ next
apply (clarsimp simp: fromAPIType_def)
apply (rule whenE_throwError_corres, simp)
apply (clarsimp simp: fromAPIType_def)
apply (rule_tac r' = "\<lambda>cap cap'. cap_relation cap cap'" in corres_splitEE[OF corres_if])
apply (rule_tac 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,clarsimp)
apply (rule corres_trivial)
apply (clarsimp simp: fromAPIType_def lookup_failure_map_def)
apply (rule_tac F="is_cnode_cap rva \<and> cap_aligned rva" in corres_gen_asm)
@ -342,6 +352,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])
@ -363,20 +387,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]])+
@ -387,19 +397,7 @@ next
apply (rule word_leq_le_minus_one)
apply (simp add: word_le_nat_alt)
apply (simp add: unat_arith_simps)
apply wp+
apply simp
apply (rule corres_returnOkTT)
apply (rule crel)
apply simp
apply (rule corres_splitEE[OF lookupSlotForCNodeOp_corres])
apply simp
apply (rule 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 wpsimp+
apply (rule hoare_strengthen_post [where Q = "\<lambda>r. invs and valid_cap r and cte_at slot"])
apply wp+
apply (clarsimp simp: is_cap_simps bits_of_def cap_aligned_def
@ -411,7 +409,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 )
@ -1498,7 +1495,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])
@ -4215,22 +4213,25 @@ lemma resetUntypedCap_corres:
apply (simp add: reset_untyped_cap_def resetUntypedCap_def liftE_bindE cong: if_cong)
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
split del: if_split cong: if_cong)
apply (rule corres_if[OF refl])
apply (rule corres_returnOk[where P=\<top> and P'=\<top>], simp)
apply (rule corres_split[OF deleteObjects_corres])
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 (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
@ -4249,8 +4250,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
@ -4268,11 +4273,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
@ -4322,8 +4323,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)
@ -4890,11 +4889,10 @@ lemma inv_untyped_corres':
apply (rule corres_add_noop_lhs)
apply (rule corres_split_nor[OF cNodeNoOverlap _ return_wp stateAssert_wp])
apply (clarsimp simp: canonicalAddressAssert_def)
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+

59
proof/refine/RISCV64/VSpace_R.thy
View File

@ -54,11 +54,11 @@ lemma handleVMFault_corres:
apply (simp add: RISCV64_H.handleVMFault_def handle_vm_fault_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqrE)
apply (cases fault; simp)
apply simp
apply (rule corres_machine_op[where r="(=)"])
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_read_stval)
apply (cases fault; simp)
apply wpsimp+
done
@ -134,7 +134,6 @@ proof -
apply (case_tac m; clarsimp simp: isCap_simps catch_throwError intro!: global)
apply (rule corres_guard_imp)
apply (rule corres_split_catch [where f=lfr and E'="\<lambda>_. \<top>"])
apply (rule global, assumption)
apply (rule corres_split_eqrE[OF findVSpaceForASID_corres[OF refl]])
apply (rule whenE_throwError_corres; simp add: lookup_failure_map_def)
apply (rule corres_machine_op)
@ -142,6 +141,8 @@ proof -
apply fastforce
apply simp
apply wpsimp+
apply (rule global, assumption)
apply wpsimp+
apply (frule (1) cte_wp_at_valid_objs_valid_cap)
apply (clarsimp simp: valid_cap_def mask_def wellformed_mapdata_def)
apply (wpsimp wp: get_cap_wp simp: getThreadVSpaceRoot_def)+
@ -347,12 +348,14 @@ 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 lookupPTFromLevel_corres[OF _ refl]])
apply simp
apply (simp add: liftE_bindE)
apply (rule corres_split[OF storePTE_corres])
apply simp
apply simp
apply (rule corres_machine_op)
apply (rule corres_Id; simp)
apply (wpsimp wp: pt_lookup_from_level_wp)+
@ -370,10 +373,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
@ -399,7 +402,7 @@ 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>"])
apply (rule corres_split_strengthen_ftE[where ftr'=dc])
apply (rule findVSpaceForASID_corres[OF refl])
apply (rule corres_splitEE)
@ -416,8 +419,8 @@ lemma unmapPage_corres:
apply (simp add: liftE_bindE)
apply (rule corres_split[OF storePTE_corres])
apply simp
apply (rule corres_machine_op, rule corres_Id, rule refl; simp)
apply simp
apply (rule corres_machine_op, rule corres_Id, rule refl; simp)
apply wpsimp+
apply (clarsimp simp: invs_psp_aligned invs_distinct invs_vspace_objs valid_unmap_def
invs_valid_asid_table)
@ -524,9 +527,10 @@ lemma performPageInvocation_corres:
apply (rule corres_guard_imp)
apply (simp add: perform_pg_inv_map_def)
apply (rule corres_split[OF updateCap_same_master])
apply simp
apply (rule corres_split[OF storePTE_corres])
apply (rule corres_machine_op, rule corres_Id; simp)
apply assumption
apply (rule corres_machine_op, rule corres_Id; simp)
apply wpsimp+
apply (clarsimp simp: invs_valid_objs invs_distinct invs_psp_aligned)
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def is_cap_simps)
@ -542,12 +546,7 @@ lemma performPageInvocation_corres:
apply (rule_tac F="RISCV64_A.is_FrameCap cap" in corres_req; clarsimp)
apply (clarsimp simp: RISCV64_A.is_FrameCap_def)
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated[where r'=dc])
apply (rule corres_split[OF getSlotCap_corres[OF refl]])
apply (rule_tac F="is_frame_cap old_cap" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: update_map_data_def is_cap_simps)
apply (wpsimp wp: get_cap_wp)+
apply (rule corres_split[where r'=dc])
apply (rename_tac m)
apply (rule option_corres[where P=\<top> and P'=\<top>])
prefer 3
@ -557,6 +556,11 @@ lemma performPageInvocation_corres:
apply datatype_schem
apply (fold dc_def)[1]
apply (rule unmapPage_corres; simp)
apply (rule corres_split[OF getSlotCap_corres[OF refl]])
apply (rule_tac F="is_frame_cap old_cap" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: update_map_data_def is_cap_simps)
apply (wpsimp wp: get_cap_wp)+
apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_imp_lift')+
apply (clarsimp simp: invs_valid_objs invs_psp_aligned invs_distinct)
apply (clarsimp simp: cte_wp_at_caps_of_state wellformed_pte_def
@ -641,8 +645,8 @@ lemma performPageTableInvocation_corres:
apply (rule corres_split[OF updateCap_same_master])
apply simp
apply (rule corres_split[OF storePTE_corres])
apply (rule corres_machine_op, rule corres_Id; simp)
apply assumption
apply (rule corres_machine_op, rule corres_Id; simp)
apply wpsimp+
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def
invs_valid_objs invs_psp_aligned invs_distinct)
@ -656,22 +660,21 @@ lemma performPageTableInvocation_corres:
apply (simp add: case_option_If2 split del: if_split)
apply (rule corres_guard_imp)
apply (rule corres_split_nor)
apply (rule corres_if3)
apply (fastforce simp: acap_map_data_def mdata_map_def is_PageTableCap_def)
apply (rule corres_split[OF unmapPageTable_corres])
apply (clarsimp simp: mdata_map_def)
apply (clarsimp simp: mdata_map_def)
apply (rule refl)
apply (rule clear_page_table_corres)
apply wp+
apply (rule corres_trivial, simp)
apply (simp add: liftM_def)
apply (rule corres_split[OF getSlotCap_corres[OF refl]])
apply (rule_tac F="is_pt_cap x" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_cap_simps update_map_data_def)
apply (wp get_cap_wp)+
apply (rule corres_if3)
apply (fastforce simp: acap_map_data_def mdata_map_def is_PageTableCap_def)
apply (rule corres_split[OF unmapPageTable_corres])
apply (rule clear_page_table_corres)
apply (clarsimp simp: mdata_map_def)
apply (clarsimp simp: mdata_map_def)
apply (rule refl)
apply wp+
apply (rule corres_trivial, simp)
apply (wpsimp wp: mapM_x_wp' hoare_vcg_all_lift hoare_vcg_imp_lift'
apply (wpsimp wp: get_cap_wp mapM_x_wp' hoare_vcg_all_lift hoare_vcg_imp_lift'
simp: wellformed_pte_def)+
apply (clarsimp simp: valid_pti_def valid_arch_cap_def cte_wp_at_caps_of_state
invs_valid_objs invs_psp_aligned invs_distinct
@ -707,12 +710,13 @@ lemma performASIDPoolInvocation_corres:
apply (clarsimp simp: perform_asid_pool_invocation_def performASIDPoolInvocation_def)
apply (cases ap, simp add: asid_pool_invocation_map_def)
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 corres_assert_gen_asm_l, rule corres_assert_gen_asm_l)
apply (rule_tac F="is_pt_cap pt_cap" in corres_gen_asm)
apply (rule corres_split[OF updateCap_same_master])
apply (clarsimp simp: is_cap_simps update_map_data_def)
apply (rule corres_split[OF copy_global_mappings_corres])
apply (clarsimp simp: is_cap_simps)
apply (unfold store_asid_pool_entry_def)[1]
apply (rule corres_split[where r'="\<lambda>pool pool'. pool = pool' \<circ> ucast"])
apply (simp cong: corres_weak_cong)
@ -724,7 +728,6 @@ lemma performASIDPoolInvocation_corres:
apply (rule ext)
apply (clarsimp simp: inv_def is_cap_simps ucast_up_inj)
apply (wp getASID_wp)+
apply (clarsimp simp: is_cap_simps)
apply (wpsimp wp: set_cap_typ_at hoare_drop_imps|strengthen valid_arch_state_global_arch_objs)+
apply (clarsimp simp: valid_apinv_def cte_wp_at_caps_of_state is_cap_simps cap_master_cap_simps
update_map_data_def)