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

x64: CnodeInv_AI, ArchCNodeInv_AI now process

This commit is contained in:
Joel Beeren 2017-02-15 14:11:32 +11:00
parent 5ea1d903ae
commit 6723b58cb7
2 changed files with 86 additions and 114 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
proof/invariant-abstract/CNodeInv_AI.thy
View File

@ -181,7 +181,7 @@ locale CNodeInv_AI =
\<lbrace>\<lambda>rv. valid_machine_state\<rbrace>"
assumes unat_of_bl_nat_to_cref:
"\<And>n ln. \<lbrakk> n < 2 ^ ln; ln < word_bits \<rbrakk>
\<Longrightarrow> unat (of_bl (nat_to_cref ln n) :: word32) = n"
\<Longrightarrow> unat (of_bl (nat_to_cref ln n) :: machine_word) = n"
assumes zombie_is_cap_toE_pre:
"\<And>(s::'state_ext state) ptr zbits n m irqn.
\<lbrakk> s \<turnstile> Zombie ptr zbits n; invs s; m < n \<rbrakk>
@ -2203,13 +2203,13 @@ lemma word_same_bl_memo_unify_word_type:
lemma word_and_bl_proof:
"\<lbrakk> invs s; kheap s x = Some (CNode sz cs);
unat (of_bl y :: word32) = 0; unat (of_bl z :: word32) = 0;
unat (of_bl y :: machine_word) = 0; unat (of_bl z :: machine_word) = 0;
y \<in> dom cs; z \<in> dom cs \<rbrakk> \<Longrightarrow> y = z"
apply (simp add: unat_eq_0)
apply (frule invs_valid_objs, erule(1) valid_objsE)
apply (clarsimp simp: valid_obj_def valid_cs_def
valid_cs_size_def well_formed_cnode_n_def)
apply (rule word_same_bl_memo_unify_word_type[where 'a=32])
apply (rule word_same_bl_memo_unify_word_type[where 'a=machine_word_len])
apply simp
apply simp
apply (simp add: word_bits_def)

194
proof/invariant-abstract/X64/ArchCNodeInv_AI.thy
View File

@ -24,22 +24,7 @@ lemma derive_cap_objrefs [CNodeInv_AI_assms]:
apply ((wp ensure_no_children_inv | simp add: o_def | rule hoare_pre)+)[11]
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all add: arch_derive_cap_def)
apply (wp | simp add: o_def)+
apply (rename_tac word option)
apply (case_tac option)
apply simp
apply (rule hoare_pre, wp)
apply simp
apply (rule hoare_pre, wp)
apply (simp add: aobj_ref_cases)
apply (rename_tac word option)
apply (case_tac option, simp)
apply (rule hoare_pre, wp)
apply simp
apply (rule hoare_pre, wp)
apply clarsimp
done
by (wp | wpc | simp add: o_def)+
lemma derive_cap_zobjrefs [CNodeInv_AI_assms]:
"\<lbrace>\<lambda>s. P (zobj_refs cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (zobj_refs rv)\<rbrace>,-"
@ -47,45 +32,30 @@ lemma derive_cap_zobjrefs [CNodeInv_AI_assms]:
apply ((wp ensure_no_children_inv | simp add: o_def | rule hoare_pre)+)[11]
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all add: arch_derive_cap_def)
apply (wp | simp add: o_def)+
apply (rename_tac option)
apply (case_tac option)
apply simp
apply (rule hoare_pre, wp)
apply simp
apply (rule hoare_pre, wp)
apply (simp add: aobj_ref_cases)
apply (rename_tac option)
apply (case_tac option, simp)
apply (rule hoare_pre, wp)
apply simp
apply (rule hoare_pre, wp)
apply clarsimp
done
by (wp | wpc |simp add: o_def)+
lemma update_cap_objrefs [CNodeInv_AI_assms]:
"\<lbrakk> update_cap_data P dt cap \<noteq> NullCap \<rbrakk> \<Longrightarrow>
obj_refs (update_cap_data P dt cap) = obj_refs cap"
by (case_tac cap,
simp_all add: update_cap_data_closedform
split: if_split_asm)
simp_all add: update_cap_data_closedform Let_def
split: if_split_asm arch_cap.splits)
lemma update_cap_zobjrefs [CNodeInv_AI_assms]:
"\<lbrakk> update_cap_data P dt cap \<noteq> cap.NullCap \<rbrakk> \<Longrightarrow>
zobj_refs (update_cap_data P dt cap) = zobj_refs cap"
apply (case_tac cap,
simp_all add: update_cap_data_closedform arch_update_cap_data_def
split: if_split_asm)
simp_all add: update_cap_data_closedform arch_update_cap_data_def Let_def
split: if_split_asm arch_cap.splits)
done
lemma copy_mask [simp, CNodeInv_AI_assms]:
"copy_of (mask_cap R c) = copy_of c"
apply (rule ext)
apply (auto simp: copy_of_def is_cap_simps mask_cap_def
cap_rights_update_def same_object_as_def
apply (auto simp: copy_of_def is_cap_simps mask_cap_def
cap_rights_update_def same_object_as_def
bits_of_def acap_rights_update_def
split: cap.splits arch_cap.splits)
done
@ -94,8 +64,10 @@ lemma update_cap_data_mask_Null [simp, CNodeInv_AI_assms]:
"(update_cap_data P x (mask_cap m c) = NullCap) = (update_cap_data P x c = NullCap)"
unfolding update_cap_data_def mask_cap_def
apply (cases c)
by (auto simp add: the_cnode_cap_def Let_def is_cap_simps cap_rights_update_def badge_update_def
arch_update_cap_data_def)
apply (clarsimp simp: is_cap_simps cap_rights_update_def badge_update_def split: if_splits)+
apply (rename_tac arch_cap)
apply (case_tac arch_cap; clarsimp simp: arch_update_cap_data_def acap_rights_update_def split: if_splits)
done
lemma cap_master_update_cap_data [CNodeInv_AI_assms]:
"\<lbrakk> update_cap_data P x c \<noteq> NullCap \<rbrakk>
@ -112,21 +84,29 @@ lemma same_object_as_def2:
\<and> \<not> cp = NullCap \<and> \<not> is_untyped_cap cp
\<and> \<not> is_zombie cp
\<and> (is_arch_cap cp \<longrightarrow>
(case the_arch_cap cp of PageCap d x rs tp sz v
\<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1
(case the_arch_cap cp of
PageCap d x rs tp sz v \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1
| IOPortCap f l \<Rightarrow> (is_arch_cap cp' \<longrightarrow>
(case the_arch_cap cp' of
IOPortCap f' l' \<Rightarrow> f\<le>f'\<and>l'\<le>l
| _ \<Rightarrow> False))
| _ \<Rightarrow> True)))"
apply (simp add: same_object_as_def is_cap_simps split: cap.split)
apply (auto simp: cap_master_cap_def bits_of_def
split: arch_cap.split_asm)
apply (auto split: arch_cap.split)
apply (auto simp: cap_master_cap_def bits_of_def is_cap_simps
split: arch_cap.splits)
done
lemma same_object_as_cap_master [CNodeInv_AI_assms]:
"same_object_as cap cap' \<Longrightarrow> cap_master_cap cap = cap_master_cap cap'"
by (simp add: same_object_as_def2)
lemma weak_derived_cap_is_device[CNodeInv_AI_assms]:
"\<lbrakk>weak_derived c' c\<rbrakk> \<Longrightarrow> cap_is_device c = cap_is_device c'"
apply (auto simp: weak_derived_def copy_of_def is_cap_simps
same_object_as_def2
split: if_split_asm
dest!: master_cap_eq_is_device_cap_eq)
done
lemma cap_asid_update_cap_data [CNodeInv_AI_assms]:
"update_cap_data P x c \<noteq> NullCap
@ -156,19 +136,22 @@ lemma cap_asid_base_update_cap_data [CNodeInv_AI_assms]:
done
lemma same_object_as_update_cap_data [CNodeInv_AI_assms]:
"\<lbrakk> update_cap_data P x c \<noteq> NullCap; same_object_as c' c \<rbrakk> \<Longrightarrow>
"\<lbrakk> update_cap_data P x c \<noteq> NullCap; same_object_as c' c \<rbrakk> \<Longrightarrow>
same_object_as c' (update_cap_data P x c)"
apply (clarsimp simp: same_object_as_def is_cap_simps
thm same_object_as_def same_aobject_as_def arch_same_region_as.simps arch_update_cap_data_def
apply (clarsimp simp: same_object_as_def is_cap_simps
split: cap.split_asm arch_cap.splits if_split_asm)
apply (simp add: update_cap_data_def badge_update_def cap_rights_update_def is_cap_simps arch_update_cap_data_def
Let_def split_def the_cnode_cap_def bits_of_def split: if_split_asm cap.splits)+
apply (auto simp: update_cap_data_def badge_update_def cap_rights_update_def is_cap_simps
arch_update_cap_data_def
Let_def split_def the_cnode_cap_def bits_of_def
split: if_split_asm cap.splits)
done
lemma weak_derived_update_cap_data [CNodeInv_AI_assms]:
"\<lbrakk>update_cap_data P x c \<noteq> NullCap; weak_derived c c'\<rbrakk>
\<Longrightarrow> weak_derived (update_cap_data P x c) c'"
apply (simp add: weak_derived_def copy_of_def
cap_master_update_cap_data cap_asid_update_cap_data
"\<lbrakk>update_cap_data P x c \<noteq> NullCap; weak_derived c c'\<rbrakk>
\<Longrightarrow> weak_derived (update_cap_data P x c) c'"
apply (simp add: weak_derived_def copy_of_def
cap_master_update_cap_data cap_asid_update_cap_data
cap_asid_base_update_cap_data
cap_vptr_update_cap_data
split del: if_split cong: if_cong)
@ -186,10 +169,11 @@ lemma weak_derived_update_cap_data [CNodeInv_AI_assms]:
apply clarsimp
apply (rule conjI, clarsimp simp: is_cap_simps update_cap_data_def split del: if_split)+
apply clarsimp
apply (clarsimp simp: same_object_as_def is_cap_simps
apply (clarsimp simp: same_object_as_def is_cap_simps
split: cap.split_asm arch_cap.splits if_split_asm)
apply (simp add: update_cap_data_def badge_update_def cap_rights_update_def is_cap_simps arch_update_cap_data_def
Let_def split_def the_cnode_cap_def bits_of_def split: if_split_asm cap.splits)+
apply (auto simp: update_cap_data_def badge_update_def cap_rights_update_def is_cap_simps arch_update_cap_data_def
Let_def split_def the_cnode_cap_def bits_of_def
split: if_split_asm cap.splits arch_cap.splits)
done
lemma cap_badge_update_cap_data [CNodeInv_AI_assms]:
@ -206,7 +190,7 @@ lemma cap_badge_update_cap_data [CNodeInv_AI_assms]:
lemma cap_vptr_rights_update[simp, CNodeInv_AI_assms]:
"cap_vptr (cap_rights_update f c) = cap_vptr c"
by (simp add: cap_vptr_def cap_rights_update_def acap_rights_update_def
by (simp add: cap_vptr_def cap_rights_update_def acap_rights_update_def
split: cap.splits arch_cap.splits)
lemma cap_vptr_mask[simp, CNodeInv_AI_assms]:
@ -215,7 +199,7 @@ lemma cap_vptr_mask[simp, CNodeInv_AI_assms]:
lemma cap_asid_base_rights [simp, CNodeInv_AI_assms]:
"cap_asid_base (cap_rights_update R c) = cap_asid_base c"
by (simp add: cap_rights_update_def acap_rights_update_def
by (simp add: cap_rights_update_def acap_rights_update_def
split: cap.splits arch_cap.splits)
lemma cap_asid_base_mask[simp, CNodeInv_AI_assms]:
@ -240,23 +224,23 @@ lemma weak_derived_mask [CNodeInv_AI_assms]:
lemma vs_cap_ref_update_cap_data[simp, CNodeInv_AI_assms]:
"vs_cap_ref (update_cap_data P d cap) = vs_cap_ref cap"
by (simp add: vs_cap_ref_def update_cap_data_closedform
arch_update_cap_data_def
split: cap.split)
arch_update_cap_data_def Let_def
split: arch_cap.splits cap.split if_splits)
lemma in_preempt[simp, intro, CNodeInv_AI_assms]:
"(Inr rv, s') \<in> fst (preemption_point s) \<Longrightarrow>
(\<exists>f es. s' = s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>, exst := es\<rparr>)"
apply (clarsimp simp: preemption_point_def in_monad do_machine_op_def
(\<exists>f es. s' = s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>, exst := es\<rparr>)"
apply (clarsimp simp: preemption_point_def in_monad do_machine_op_def
return_def returnOk_def throwError_def o_def
select_f_def select_def getActiveIRQ_def)
select_f_def select_def getActiveIRQ_def)
done
lemma invs_irq_state_independent[intro!, simp, CNodeInv_AI_assms]:
"invs (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>)
= invs s"
by (clarsimp simp: irq_state_independent_A_def invs_def
by (clarsimp simp: irq_state_independent_A_def invs_def
valid_state_def valid_pspace_def valid_mdb_def valid_ioc_def valid_idle_def
only_idle_def if_unsafe_then_cap_def valid_reply_caps_def
valid_reply_masters_def valid_global_refs_def valid_arch_state_def
@ -265,7 +249,7 @@ lemma invs_irq_state_independent[intro!, simp, CNodeInv_AI_assms]:
valid_kernel_mappings_def equal_kernel_mappings_def
valid_asid_map_def valid_global_vspace_mappings_def
pspace_in_kernel_window_def cap_refs_in_kernel_window_def
cur_tcb_def sym_refs_def state_refs_of_def vspace_at_asid_def
cur_tcb_def sym_refs_def state_refs_of_def vspace_at_asid_def
swp_def valid_irq_states_def)
@ -328,7 +312,7 @@ lemma weak_derived_vs_cap_ref [CNodeInv_AI_assms]:
lemma weak_derived_table_cap_ref [CNodeInv_AI_assms]:
"weak_derived c c' \<Longrightarrow> table_cap_ref c = table_cap_ref c'"
apply (clarsimp simp: weak_derived_def copy_of_def
same_object_as_def2
same_object_as_def2
split: if_split_asm)
apply (elim disjE,simp_all add:is_cap_simps)
apply (elim disjE,simp_all)
@ -340,10 +324,12 @@ lemma weak_derived_table_cap_ref [CNodeInv_AI_assms]:
done
lemma weak_derived_pd_pt_asid:
lemma weak_derived_vspace_asid:
"weak_derived c c' \<Longrightarrow> cap_asid c = cap_asid c'
\<and> is_pt_cap c = is_pt_cap c'
\<and> is_pd_cap c = is_pd_cap c'"
\<and> is_pd_cap c = is_pd_cap c'
\<and> is_pdpt_cap c = is_pdpt_cap c'
\<and> is_pml4_cap c = is_pml4_cap c'"
by (auto simp: weak_derived_def copy_of_def is_cap_simps
same_object_as_def2 is_pt_cap_def
cap_master_cap_simps
@ -359,7 +345,7 @@ lemma weak_derived_ASIDPool1:
apply (clarsimp simp: weak_derived_def copy_of_def split: if_split_asm)
apply (clarsimp simp: same_object_as_def2 cap_master_cap_simps dest!: cap_master_cap_eqDs)
done
lemma weak_derived_ASIDPool2:
"weak_derived cap (ArchObjectCap (ASIDPoolCap ap asid)) =
(cap = ArchObjectCap (ASIDPoolCap ap asid))"
@ -370,14 +356,14 @@ lemma weak_derived_ASIDPool2:
apply (auto simp: same_object_as_def2 cap_master_cap_simps dest!: cap_master_cap_eqDs)
done
lemmas weak_derived_ASIDPool [simp] =
lemmas weak_derived_ASIDPool [simp] =
weak_derived_ASIDPool1 weak_derived_ASIDPool2
lemma swap_of_caps_valid_arch_caps [CNodeInv_AI_assms]:
"\<lbrace>valid_arch_caps and
cte_wp_at (weak_derived c) a and
cte_wp_at (weak_derived c') b\<rbrace>
cte_wp_at (weak_derived c') b\<rbrace>
do
y \<leftarrow> set_cap c b;
set_cap c' a
@ -394,8 +380,8 @@ lemma swap_of_caps_valid_arch_caps [CNodeInv_AI_assms]:
simp del: split_paired_Ex split_paired_All imp_disjL)
apply (frule weak_derived_obj_refs[where dcap=c])
apply (frule weak_derived_obj_refs[where dcap=c'])
apply (frule weak_derived_pd_pt_asid[where c=c])
apply (frule weak_derived_pd_pt_asid[where c=c'])
apply (frule weak_derived_vspace_asid[where c=c])
apply (frule weak_derived_vspace_asid[where c=c'])
apply (intro conjI)
apply (simp add: valid_vs_lookup_def del: split_paired_Ex split_paired_All)
apply (elim allEI)
@ -403,7 +389,7 @@ lemma swap_of_caps_valid_arch_caps [CNodeInv_AI_assms]:
apply (simp del: split_paired_Ex split_paired_All)
apply (elim conjE)
apply (erule exfEI[where f="id (a := b, b := a)"])
apply (auto dest!: weak_derived_vs_cap_ref)[1]
subgoal by (clarsimp dest!: weak_derived_vs_cap_ref, intro conjI; clarsimp)
apply (simp add: valid_table_caps_def empty_table_caps_of
del: split_paired_Ex split_paired_All imp_disjL)
apply (simp add: unique_table_caps_def
@ -424,7 +410,7 @@ lemma swap_of_caps_valid_arch_caps [CNodeInv_AI_assms]:
lemma cap_swap_asid_map[wp, CNodeInv_AI_assms]:
"\<lbrace>valid_asid_map and
cte_wp_at (weak_derived c) a and
cte_wp_at (weak_derived c') b\<rbrace>
cte_wp_at (weak_derived c') b\<rbrace>
cap_swap c a c' b \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>"
apply (simp add: cap_swap_def set_cdt_def valid_asid_map_def vspace_at_asid_def)
apply (rule hoare_pre)
@ -436,7 +422,7 @@ lemma cap_swap_asid_map[wp, CNodeInv_AI_assms]:
lemma cap_swap_cap_refs_in_kernel_window[wp, CNodeInv_AI_assms]:
"\<lbrace>cap_refs_in_kernel_window and
cte_wp_at (weak_derived c) a and
cte_wp_at (weak_derived c') b\<rbrace>
cte_wp_at (weak_derived c') b\<rbrace>
cap_swap c a c' b \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>"
apply (simp add: cap_swap_def)
apply (rule hoare_pre)
@ -453,10 +439,10 @@ lemma cap_swap_vms[wp, CNodeInv_AI_assms]:
hoare_vcg_all_lift hoare_vcg_ex_lift hoare_vcg_disj_lift)
done
(* FIXME x64: this could probably be generic *)
lemma unat_of_bl_nat_to_cref[CNodeInv_AI_assms]:
"\<lbrakk> n < 2 ^ ln; ln < word_bits \<rbrakk>
\<Longrightarrow> unat (of_bl (nat_to_cref ln n) :: word32) = n"
"\<lbrakk> n < 2 ^ len; len < word_bits \<rbrakk>
\<Longrightarrow> unat (of_bl (nat_to_cref len n) :: machine_word) = n"
apply (simp add: nat_to_cref_def word_bits_conv of_drop_to_bl
word_size)
apply (subst less_mask_eq)
@ -466,7 +452,7 @@ lemma unat_of_bl_nat_to_cref[CNodeInv_AI_assms]:
apply simp
apply simp
apply simp
apply (rule unat_of_nat32)
apply (rule unat_of_nat_eq[where 'a=machine_word_len, unfolded word_bits_len_of])
apply (erule order_less_trans)
apply (rule power_strict_increasing)
apply (simp add: word_bits_conv)
@ -493,7 +479,7 @@ lemma finalise_cap_makes_halted_proof[CNodeInv_AI_assms]:
apply (case_tac cap, simp_all)
apply (wp unbind_notification_valid_objs
| clarsimp simp: o_def valid_cap_def cap_table_at_typ
is_tcb obj_at_def
is_tcb obj_at_def
| clarsimp simp: halted_if_tcb_def
split: option.split
| intro impI conjI
@ -508,15 +494,15 @@ lemma finalise_cap_makes_halted_proof[CNodeInv_AI_assms]:
done
crunch emptyable[wp, CNodeInv_AI_assms]: finalise_cap "emptyable sl"
(simp: crunch_simps lift: emptyable_lift
crunch emptyable[wp,CNodeInv_AI_assms]: finalise_cap "\<lambda>s. emptyable sl s"
(simp: crunch_simps rule: emptyable_lift
wp: crunch_wps suspend_emptyable unbind_notification_invs unbind_maybe_notification_invs)
lemma finalise_cap_not_reply_master_unlifted [CNodeInv_AI_assms]:
"(rv, s') \<in> fst (finalise_cap cap sl s) \<Longrightarrow>
\<not> is_master_reply_cap (fst rv)"
by (case_tac cap, auto simp: is_cap_simps in_monad liftM_def
by (case_tac cap, auto simp: is_cap_simps in_monad liftM_def
arch_finalise_cap_def
split: if_split_asm arch_cap.split_asm bool.split_asm option.split_asm)
@ -602,11 +588,11 @@ next
apply (rule hoare_pre_spec_validE)
apply (wp replace_cap_invs | simp)+
apply (erule finalise_cap_not_reply_master)
apply (wp "2.hyps", assumption+)
apply (wp "2.hyps")
apply (wp preemption_point_Q | simp)+
apply (wp preemption_point_inv, simp+)
apply (wp preemption_point_Q)
apply ((wp preemption_point_inv irq_state_independent_A_conjI irq_state_independent_AI
apply ((wp preemption_point_inv irq_state_independent_A_conjI irq_state_independent_AI
emptyable_irq_state_independent invs_irq_state_independent
| simp add: valid_rec_del_call_def irq_state_independent_A_def)+)[1]
apply (simp(no_asm))
@ -616,7 +602,7 @@ next
| wp replace_cap_invs set_cap_sets final_cap_same_objrefs
set_cap_cte_cap_wp_to static_imp_wp
| erule finalise_cap_not_reply_master)+
apply (wp hoare_vcg_const_Ball_lift)
apply (wp hoare_vcg_const_Ball_lift)+
apply (rule hoare_strengthen_post)
apply (rule_tac Q="\<lambda>fin s. Q s \<and> invs s \<and> replaceable s slot (fst fin) rv
\<and> cte_wp_at (op = rv) slot s \<and> s \<turnstile> (fst fin)
@ -769,7 +755,7 @@ next
apply (clarsimp simp: valid_cap_def cap_aligned_def is_cap_simps
cte_wp_at_cte_at appropriate_Zombie
split: option.split_asm)
apply (wp get_cap_cte_wp_at)[1]
apply (wp get_cap_cte_wp_at)[1]
apply simp
apply (subst conj_assoc[symmetric])
apply (rule spec_valid_conj_liftE2)
@ -803,7 +789,7 @@ context Arch begin global_naming X64
lemma finalise_cap_rvk_prog [CNodeInv_AI_assms]:
"\<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>
finalise_cap a b
finalise_cap a b
\<lbrace>\<lambda>_ s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>"
apply (case_tac a,simp_all add:liftM_def)
apply (wp cancel_all_ipc_rvk_prog cancel_all_signals_rvk_prog
@ -841,7 +827,7 @@ next
apply (rule hoare_pre_spec_validE)
apply wp
apply ((wp | simp)+)[1]
apply (wp wp, assumption+)
apply (wp wp)
apply ((wp preemption_point_inv | simp)+)[1]
apply (simp(no_asm))
apply (rule wp, assumption+)
@ -913,7 +899,7 @@ declare cap_revoke.simps[simp del]
context Arch begin global_naming X64
crunch typ_at[wp, CNodeInv_AI_assms]: cap_recycle "\<lambda>s. P (typ_at T p s)"
crunch typ_at[wp, CNodeInv_AI_assms]: finalise_slot "\<lambda>s. P (typ_at T p s)"
(wp: crunch_wps simp: crunch_simps filterM_mapM unless_def
ignore: without_preemption filterM set_object clearMemory)
@ -946,6 +932,7 @@ lemma cap_move_invs[wp, CNodeInv_AI_assms]:
and K (\<not> is_master_reply_cap cap)\<rbrace>
cap_move cap ptr ptr'
\<lbrace>\<lambda>rv. invs\<rbrace>"
including no_pre
unfolding invs_def valid_state_def valid_pspace_def
apply (simp add: pred_conj_def conj_comms [where Q = "valid_mdb S" for S])
apply wp
@ -980,6 +967,8 @@ lemma cap_move_invs[wp, CNodeInv_AI_assms]:
apply (wp set_cap_valid_objs set_cap_idle set_cap_typ_at
cap_table_at_lift_irq tcb_at_typ_at
hoare_vcg_disj_lift hoare_vcg_all_lift
set_cap_cap_refs_respects_device_region_NullCap
| wp set_cap_cap_refs_respects_device_region_spec[where ptr=ptr]
| simp del: split_paired_Ex split_paired_All
| simp add: valid_irq_node_def valid_machine_state_def
del: split_paired_All split_paired_Ex)+
@ -991,30 +980,13 @@ lemma cap_move_invs[wp, CNodeInv_AI_assms]:
apply (simp add: cap_range_NullCap valid_ipc_buffer_cap_def[where c=cap.NullCap])
apply (simp add: is_cap_simps)
apply (subgoal_tac "tcb_cap_valid cap.NullCap ptr s")
apply (simp add: tcb_cap_valid_def)
apply (simp add: tcb_cap_valid_def weak_derived_cap_is_device)
apply (rule tcb_cap_valid_NullCapD)
apply (erule(1) tcb_cap_valid_caps_of_stateD)
apply (simp add: is_cap_simps)
apply (clarsimp simp: cte_wp_at_caps_of_state)
done
lemma recycle_cap_appropriateness [CNodeInv_AI_assms]:
"\<lbrace>valid_cap cap\<rbrace> recycle_cap is_final cap \<lbrace>\<lambda>rv s. appropriate_cte_cap rv = appropriate_cte_cap cap\<rbrace>"
apply (simp add: recycle_cap_def)
apply (rule hoare_pre)
apply (wp thread_get_wp gts_wp | wpc | simp add: get_bound_notification_def)+
apply (simp add: arch_recycle_cap_def o_def split del: if_split)
apply (wp | wpc | simp add: | wp_once hoare_drop_imps)+
apply (auto simp: appropriate_cte_cap_def fun_eq_iff valid_cap_def tcb_at_st_tcb_at pred_tcb_at_def)
done
lemma reset_mem_mapping_master:
"cap_master_cap (ArchObjectCap (arch_reset_mem_mapping arch_cap)) = cap_master_cap (ArchObjectCap arch_cap)"
unfolding cap_master_cap_def
by (cases arch_cap, simp_all)
end