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

access: proof style cleanup (for GrantReply patch) 

As the title says, this commit introduces general formatting and style
cleanup, but only for the parts touched by the recent GrantReply patch.
This commit is contained in:
Japheth Lim 2018-11-02 16:01:02 +11:00
parent 6dfe687ac1
commit 5d1525bb7a
9 changed files with 811 additions and 817 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

119
proof/access-control/Access.thy
View File

@ -141,6 +141,16 @@ abbreviation(input) aag_has_auth_to :: "'a PAS \<Rightarrow> auth \<Rightarrow>
where
"aag_has_auth_to aag auth ptr \<equiv> (pasSubject aag, auth, pasObjectAbs aag ptr) \<in> pasPolicy aag"
abbreviation aag_subjects_have_auth_to_label :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> auth \<Rightarrow> 'a \<Rightarrow> bool"
where
"aag_subjects_have_auth_to_label subs aag auth label
\<equiv> \<exists>s \<in> subs. (s, auth, label) \<in> pasPolicy aag"
abbreviation aag_subjects_have_auth_to :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> auth \<Rightarrow> obj_ref \<Rightarrow> bool"
where
"aag_subjects_have_auth_to subs aag auth oref
\<equiv> aag_subjects_have_auth_to_label subs aag auth (pasObjectAbs aag oref)"
context begin interpretation Arch . (*FIXME: arch_split*)
@ -725,7 +735,7 @@ lemma is_transferable_null_filter[simp]:
lemma sbta_null_filter:
"state_bits_to_policy (null_filter cs) sr bar cd vr = state_bits_to_policy cs sr bar cd vr"
apply rule
apply (rule subset_antisym)
apply clarsimp
apply (erule state_bits_to_policy.induct,
(fastforce intro: state_bits_to_policy.intros
@ -937,16 +947,6 @@ where
"send_is_call (Structures_A.BlockedOnSend _ payl) = sender_is_call payl"
| "send_is_call _ = False"
abbreviation aag_subjects_have_auth_to_label :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> auth \<Rightarrow> 'a \<Rightarrow> bool"
where
"aag_subjects_have_auth_to_label subs aag auth label
\<equiv> \<exists>s \<in> subs. (s, auth, label) \<in> pasPolicy aag"
abbreviation aag_subjects_have_auth_to :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> auth \<Rightarrow> obj_ref \<Rightarrow> bool"
where
"aag_subjects_have_auth_to subs aag auth oref
\<equiv> aag_subjects_have_auth_to_label subs aag auth (pasObjectAbs aag oref)"
definition tcb_bound_notification_reset_integrity
@ -1018,7 +1018,7 @@ lemmas reply_cap_deletion_integrityI1 =
reply_cap_deletion_integrity_def[THEN meta_eq_to_obj_eq,THEN iffD2,OF disjI1]
lemmas reply_cap_deletion_integrityI2 =
reply_cap_deletion_integrity_def[THEN meta_eq_to_obj_eq,THEN iffD2, OF disjI2, OF exI,
OF exI,rule_format]
OF exI, OF conjI [OF _ conjI], rule_format]
lemmas reply_cap_deletion_integrity_intros =
reply_cap_deletion_integrityI1 reply_cap_deletion_integrityI2
@ -1127,7 +1127,9 @@ inductive integrity_obj_atomic for aag activate subjects l ko ko'
| troa_tcb_receive:
"\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb');
tcb' = tcb \<lparr>tcb_state := new_st\<rparr>;
new_st = Running \<or> (((new_st = Inactive \<and> call_blocked ep (tcb_state tcb)) \<or> (new_st = BlockedOnReply \<and> (allowed_call_blocked ep (tcb_state tcb)))));
new_st = Running
\<or> (inactive new_st \<and> call_blocked ep (tcb_state tcb))
\<or> (awaiting_reply new_st \<and> allowed_call_blocked ep (tcb_state tcb));
send_blocked_on ep (tcb_state tcb);
aag_subjects_have_auth_to subjects aag Receive ep \<rbrakk>
\<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'"
@ -1433,17 +1435,21 @@ lemmas disj_cong' = arg_cong2[where f="(\<or>)"]
lemma troa_tro_alt[elim!]:
"integrity_obj_atomic aag activate subjects l ko ko'
\<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'"
(* slow, 10s, but I don't think it's possible to do better without exploding the size *)
by (erule integrity_obj_atomic.cases;
(* TCB handling tactic (filtered by tcb.equality) *)
((erule(1) integrity_obj_alt.intros[OF tro_tagI],
(intro exI tcb.equality; solves\<open>simp\<close>));
fastforce simp: reply_cap_deletion_integrity_def
tcb_bound_notification_reset_integrity_def direct_reply_def
(* non-TCB handling tactic *)
| fastforce intro:integrity_obj_alt.intros[OF tro_tagI]))
apply (erule integrity_obj_atomic.cases)
text \<open>Single out TCB cases for special handling. We manually simplify
the TCB updates in the tro_alt rules using @{thm tcb.equality}.\<close>
(* somewhat slow 10s *)
apply (find_goal \<open>match premises in "ko = Some (TCB _)" \<Rightarrow> succeed\<close>,
((erule(1) integrity_obj_alt.intros[OF tro_tagI],
(intro exI tcb.equality; solves \<open>simp\<close>));
fastforce simp: reply_cap_deletion_integrity_def
tcb_bound_notification_reset_integrity_def
direct_reply_def))+
text \<open>Remaining cases.\<close>
apply (fastforce intro: integrity_obj_alt.intros[OF tro_tagI])+
done
@ -1477,17 +1483,13 @@ where
subsubsection {* generic stuff : FIXME MOVE *}
thm rtranclp_mono[THEN predicate2D]
thm predicate2I
lemma integrity_obj_activate:
"integrity_obj aag False subjects l' ko ko' \<Longrightarrow>
integrity_obj aag activate subjects l' ko ko'"
unfolding integrity_obj_def
apply (erule rtranclp_mono[THEN predicate2D, rotated])
apply (rule predicate2I)
by (erule integrity_obj_atomic.cases ; (intro integrity_obj_atomic.intros ; assumption | simp))
by (erule integrity_obj_atomic.cases; (intro integrity_obj_atomic.intros; assumption | simp))
abbreviation object_integrity
where
@ -1601,9 +1603,6 @@ lemmas integrity_obj_simps [simp] = tro_orefl[OF refl]
subsection {* How the CDT can change *}
text {*
@ -1715,8 +1714,6 @@ lemmas integrity_cdt_direct = cca_direct[THEN integrity_cdt_change_allowed]
text{*
m is the cdt of the initial state
tcbsts are tcb_states_of_state of the initial state
@ -1826,8 +1823,6 @@ where
section {* Integrity transitivity *}
subsection {* Object integrity transitivity *}
@ -1855,7 +1850,7 @@ lemma reply_cap_deletion_integrity_trans[elim]:
by (auto simp: reply_cap_deletion_integrity_def)
lemma cnone_integrity_trans[elim]:
lemma cnode_integrity_trans[elim]:
"\<lbrakk> cnode_integrity subjects aag cont cont';
cnode_integrity subjects aag cont' cont'' \<rbrakk>
\<Longrightarrow> cnode_integrity subjects aag cont cont''"
@ -2107,15 +2102,14 @@ lemma tsos_tro:
lemma can_receive_ipc_backward:
"\<lbrakk>integrity_obj_state aag activate subjects s s'; tcb_states_of_state s' p = Some a;
can_receive_ipc a; pasObjectAbs aag p \<notin> subjects \<rbrakk>
\<Longrightarrow> case_option False can_receive_ipc (tcb_states_of_state s p)"
\<Longrightarrow> case tcb_states_of_state s p of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x"
apply (drule_tac x = p in spec)
apply (erule integrity_objE)
apply(clarsimp simp: tcb_states_of_state_def get_tcb_def call_blocked_def allowed_call_blocked_def
split: option.splits kernel_object.splits;
cases a;
fastforce simp: tcb_states_of_state_def get_tcb_def call_blocked_def allowed_call_blocked_def
split: option.splits kernel_object.splits)+
done
apply (erule integrity_objE;
(fastforce simp: tcb_states_of_state_def get_tcb_def
call_blocked_def allowed_call_blocked_def
split: option.splits kernel_object.splits
| cases a \<comment> \<open>only split when needed\<close>)+)
done
@ -2242,14 +2236,13 @@ proof -
qed
thus ?thesis using tro_trans[OF tro1 tro2] t1 t2 intm
apply (clarsimp simp add: integrity_subjects_def simp del: split_paired_All)
apply (drule(3) trcdtlist_trans) (* needs cdt_integrity before it gets destroyed *)
apply (drule(2) trcdt_trans)
apply (drule(1) trinterrupts_trans[simplified])
apply (drule(1) trasids_trans[simplified])
apply (drule(1) tre_trans[simplified])
apply (drule(1) trrqs_trans)
apply simp
done
apply (frule(2) trcdt_trans)
apply (frule(3) trcdtlist_trans)
apply (frule(1) trinterrupts_trans[simplified])
apply (frule(1) trasids_trans[simplified])
apply (frule(1) tre_trans[simplified])
apply (frule(1) trrqs_trans[simplified])
by blast
qed
lemma integrity_refl [simp]:
@ -2889,29 +2882,29 @@ lemma integrity_mono:
apply (erule integrity_obj_atomic.cases[OF _ integrity_obj_atomic.intros];
auto simp: indirect_send_def direct_send_def direct_call_def direct_reply_def
elim: asid_pool_integrity_mono reply_cap_deletion_integrity_mono
cnode_integrity_mono)[1]
cnode_integrity_mono)
apply (rule conjI)
apply clarsimp
apply (drule_tac x=x in spec)+
apply (erule integrity_eobj.cases, auto intro: integrity_eobj.intros)[1]
apply (erule integrity_eobj.cases; auto intro: integrity_eobj.intros)
apply (rule conjI)
apply clarsimp
apply (drule_tac x=x in spec, erule integrity_mem.cases,
(blast intro: integrity_mem.intros trm_ipc')+)[1]
apply (drule_tac x=x in spec, erule integrity_mem.cases;
blast intro: integrity_mem.intros trm_ipc')
apply (rule conjI)
apply clarsimp
apply (drule_tac x=x in spec, erule integrity_device.cases,
(blast intro: integrity_device.intros)+)[1]
apply (drule_tac x=x in spec, erule integrity_device.cases;
blast intro: integrity_device.intros)
apply (rule conjI)
apply (intro allI)
apply (drule_tac x=x in spec)+
apply (erule integrity_cdtE, auto elim: cdt_change_allowed_mono)[1]
apply (erule integrity_cdtE; auto elim: cdt_change_allowed_mono)
apply (rule conjI)
apply (intro allI)
apply (drule_tac x=x in spec)+
apply (erule integrity_cdt_listE,
auto elim!: weaken_filter_eq' intro: integrity_cdt_list_intros
elim: cdt_change_allowed_mono)[1]
apply (intro allI)
apply (drule_tac x=x in spec)+
apply (erule integrity_cdt_listE;
auto elim!: weaken_filter_eq' intro: integrity_cdt_list_intros
elim: cdt_change_allowed_mono)
apply (rule conjI)
apply (fastforce simp: integrity_interrupts_def)
apply (rule conjI)

358
proof/access-control/Arch_AC.thy
View File

@ -221,7 +221,7 @@ lemma is_transferable_ArchCap[simp]:
lemma is_transferable_is_arc_update:
lemma is_transferable_is_arch_update:
"is_arch_update cap cap' \<Longrightarrow> is_transferable (Some cap) = is_transferable (Some cap')"
using is_transferable.simps is_arch_cap_def is_arch_update_def cap_master_cap_def
by (simp split: cap.splits arch_cap.splits)
@ -236,24 +236,41 @@ lemma perform_page_table_invocation_pas_refined [wp]:
cong: page_table_invocation.case_cong option.case_cong prod.case_cong
cap.case_cong arch_cap.case_cong)
apply (rule hoare_pre)
apply (wp get_cap_wp mapM_wp' store_pte_cte_wp_at do_machine_op_cte_wp_at hoare_vcg_all_lift set_cap_pas_refined_not_transferable
apply (wp get_cap_wp mapM_wp' store_pte_cte_wp_at do_machine_op_cte_wp_at
hoare_vcg_all_lift set_cap_pas_refined_not_transferable
| (wp hoare_vcg_imp_lift, unfold disj_not1)
| wpc
| simp add: mapM_x_mapM authorised_page_table_inv_def imp_conjR
pte_ref_simps | wps | blast)+
pte_ref_simps
| wps
| blast)+
apply (cases page_table_invocation)
apply (fastforce simp: cte_wp_at_caps_of_state Option.is_none_def is_transferable_is_arc_update[symmetric] valid_pti_def is_cap_simps pas_refined_refl auth_graph_map_def2 dest: pde_ref_pde_ref2)
apply (fastforce simp: cte_wp_at_caps_of_state Option.is_none_def
is_transferable_is_arch_update[symmetric]
valid_pti_def is_cap_simps pas_refined_refl auth_graph_map_def2
dest: pde_ref_pde_ref2)
apply (rename_tac s pt_cap page_cslot)
apply (case_tac page_cslot)
apply (rename_tac page_ptr page_slot)
apply (case_tac "\<exists>pt_ptr mapping. pt_cap = ArchObjectCap (PageTableCap pt_ptr mapping)")
prefer 2
apply fastforce
apply (elim exE)
apply clarsimp
apply (subgoal_tac "cte_wp_at ((=) xc) (aa, ba) s \<longrightarrow>
cte_wp_at (\<lambda>c. \<not> is_transferable (Some c)) (aa, ba) s \<and>
pas_cap_cur_auth aag (cap.ArchObjectCap (update_map_data (the_arch_cap xc) None))")
apply (rename_tac page_cap)
apply (subgoal_tac
"cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow>
cte_wp_at (\<lambda>c. \<not> is_transferable (Some c)) (page_ptr, page_slot) s \<and>
pas_cap_cur_auth aag
(cap.ArchObjectCap (update_map_data (the_arch_cap page_cap) None))")
apply simp
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (frule (1) cap_cur_auth_caps_of_state)
apply simp
apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state is_cap_simps is_arch_diminished_def)
apply (clarsimp simp: diminished_def mask_PTCap_eq)
apply (clarsimp simp: cap_auth_conferred_def update_map_data_def is_page_cap_def cap_links_asid_slot_def cap_links_irq_def aag_cap_auth_def)
apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state
is_arch_diminished_def diminished_def mask_PTCap_eq)
apply (clarsimp simp: cap_auth_conferred_def update_map_data_def is_page_cap_def
cap_links_asid_slot_def cap_links_irq_def aag_cap_auth_def)
done
definition
@ -464,9 +481,9 @@ lemma kernel_base_aligned_20:
lemma diminished_PageCapD:
"diminished (ArchObjectCap (PageCap dev p R sz m)) cap
\<Longrightarrow> \<exists>R'. cap = ArchObjectCap (PageCap dev p R' sz m)"
apply (cases cap, auto simp add: diminished_def mask_cap_def cap_rights_update_def)
apply (auto simp: acap_rights_update_def split: arch_cap.splits bool.splits)
\<Longrightarrow> \<exists>R'. cap = ArchObjectCap (PageCap dev p R' sz m)"
apply (clarsimp simp: diminished_def mask_cap_def cap_rights_update_def)
apply (fastforce simp: acap_rights_update_def split: cap.splits arch_cap.splits bool.splits)
done
(* FIXME: CLAG *)
@ -689,18 +706,21 @@ lemma perform_page_invocation_pas_refined [wp]:
| wps
| simp)+
apply (case_tac pgi)
apply ((force simp: valid_slots_def pte_ref_def cte_wp_at_caps_of_state is_transferable_is_arc_update[symmetric]
pde_ref2_def auth_graph_map_mem pas_refined_refl split:sum.splits)+)[2]
apply (clarsimp simp: cte_wp_at_caps_of_state is_transferable_is_arc_update[symmetric]
is_arch_diminished_def pte_ref_def pde_ref2_def
is_cap_simps is_pg_cap_def cap_auth_conferred_def
dest!: diminished_PageCapD)
apply (frule(1) cap_cur_auth_caps_of_state,simp)
apply (((rule conjI, rule impI)+)?, clarsimp,
clarsimp simp: update_map_data_def clas_no_asid aag_cap_auth_def
apply ((force simp: valid_slots_def pte_ref_def cte_wp_at_caps_of_state
is_transferable_is_arch_update[symmetric]
pde_ref2_def auth_graph_map_mem pas_refined_refl
split: sum.splits)+)[2]
apply (clarsimp simp: cte_wp_at_caps_of_state is_transferable_is_arch_update[symmetric]
is_arch_diminished_def pte_ref_def pde_ref2_def
is_cap_simps is_pg_cap_def cap_auth_conferred_def
dest!: diminished_PageCapD)
apply (frule(1) cap_cur_auth_caps_of_state, simp)
apply (intro impI conjI;
clarsimp; (* NB: for speed *)
clarsimp simp: update_map_data_def clas_no_asid aag_cap_auth_def
cap_auth_conferred_def vspace_cap_rights_to_auth_def
cli_no_irqs is_pg_cap_def pte_ref_def
[simplified aag_cap_auth_def])+
cli_no_irqs is_pg_cap_def
pte_ref_def[simplified aag_cap_auth_def])+
done
definition
@ -757,11 +777,6 @@ lemma perform_asid_control_invocation_respects:
apply(simp add: mask_neg_mask_is_zero mask_zero)
done
(* Comment from the reviewers : This lemma was already proven once *)
(* FIXME DELETE *)
lemmas pas_refined_cdt = aag_cdt_link_Control
lemma pas_refined_set_asid_strg:
"pas_refined aag s \<and> is_subject aag pool \<and> (\<forall>asid. asid_high_bits_of asid = base \<longrightarrow> is_subject_asid aag asid)
\<longrightarrow>
@ -863,32 +878,36 @@ lemma perform_asid_control_invocation_pas_refined [wp]:
set_cap_descendants_range_in set_cap_no_overlap get_cap_wp set_cap_caps_no_overlap
hoare_vcg_all_lift static_imp_wp retype_region_invs_extras
set_cap_pas_refined_not_transferable
| simp add: do_machine_op_def split_def cte_wp_at_neg2 region_in_kernel_window_def)+
apply(rename_tac word1 prod1 prod2 word2 cap)
apply(rule_tac Q="\<lambda> rv s. (\<exists> idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) prod2 s) \<and>
(\<forall> x\<in>ptr_range word1 pageBits. is_subject aag x) \<and>
pas_refined aag s \<and>
pas_cur_domain aag s \<and>
pspace_no_overlap_range_cover word1 pageBits s \<and>
invs s \<and>
descendants_range_in
{word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} prod2
s \<and>
range_cover word1 pageBits
(obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and>
is_subject aag (fst prod1) \<and>
is_subject aag (fst prod2) \<and>
pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap word1 word2)) \<and>
is_subject aag word1 \<and>
(\<forall>x. asid_high_bits_of x = asid_high_bits_of word2 \<longrightarrow>
is_subject_asid aag x)" in hoare_strengthen_post)
| simp add: do_machine_op_def split_def cte_wp_at_neg2 region_in_kernel_window_def)+
apply (rename_tac frame slot parent base cap)
apply (case_tac slot, rename_tac slot_ptr slot_idx)
apply (case_tac parent, rename_tac parent_ptr parent_idx)
apply (rule_tac Q="\<lambda>rv s.
(\<exists>idx. cte_wp_at ((=) (UntypedCap False frame pageBits idx)) parent s) \<and>
(\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and>
pas_refined aag s \<and>
pas_cur_domain aag s \<and>
pspace_no_overlap_range_cover frame pageBits s \<and>
invs s \<and>
descendants_range_in
{frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} parent s \<and>
range_cover frame pageBits
(obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and>
is_subject aag slot_ptr \<and>
is_subject aag parent_ptr \<and>
pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and>
is_subject aag frame \<and>
(\<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow>
is_subject_asid aag x)"
in hoare_strengthen_post)
apply (simp add: page_bits_def)
apply (wp add: delete_objects_pspace_no_overlap hoare_vcg_ex_lift
delete_objects_descendants_range_in delete_objects_invs_ex
delete_objects_pas_refined
del: Untyped_AI.delete_objects_pspace_no_overlap
delete_objects_descendants_range_in delete_objects_invs_ex
delete_objects_pas_refined
del: Untyped_AI.delete_objects_pspace_no_overlap
| simp add: page_bits_def)+
apply clarsimp
apply (rename_tac s idx)
apply (frule untyped_cap_aligned, simp add: invs_valid_objs)
apply (clarsimp simp: cte_wp_at_def aag_cap_auth_def ptr_range_def pas_refined_refl
cap_links_asid_slot_def cap_links_irq_def is_aligned_neg_mask_eq
@ -896,38 +915,41 @@ lemma perform_asid_control_invocation_pas_refined [wp]:
apply (rule conjI, force intro: descendants_range_caps_no_overlapI
simp: cte_wp_at_def is_aligned_neg_mask_eq)
apply (rule conjI)
apply (cut_tac s=s and ptr="(aa,ba)" in cap_refs_in_kernel_windowD)
apply (cut_tac s=s and ptr="(parent_ptr, parent_idx)" in cap_refs_in_kernel_windowD)
apply ((fastforce simp add: caps_of_state_def cap_range_def)+)[3]
apply (rule conjI, force simp add:field_simps)
apply (rule conjI, force simp: field_simps)
apply (rule conjI, fastforce)
apply (fastforce dest: caps_of_state_valid simp add: caps_of_state_def free_index_of_def
apply (fastforce dest: caps_of_state_valid
simp: caps_of_state_def free_index_of_def
max_free_index_def valid_cap_def)
apply (clarsimp simp: valid_aci_def authorised_asid_control_inv_def)
apply (subgoal_tac "is_aligned x pageBits")
apply (rename_tac frame slot_ptr slot_idx parent_ptr parent_idx base)
apply (subgoal_tac "is_aligned frame pageBits")
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (rule conjI)
apply(drule untyped_slots_not_in_untyped_range)
apply(erule empty_descendants_range_in)
apply(simp add: cte_wp_at_caps_of_state)
apply (drule untyped_slots_not_in_untyped_range)
apply (erule empty_descendants_range_in)
apply (simp add: cte_wp_at_caps_of_state)
apply simp
apply(rule refl)
apply(rule subset_refl)
apply(simp add: page_bits_def)
apply(clarsimp simp: ptr_range_def invs_psp_aligned invs_valid_objs
descendants_range_def2 empty_descendants_range_in
is_aligned_neg_mask_eq page_bits_def)
apply (rule refl)
apply (rule subset_refl)
apply (simp add: page_bits_def)
apply (clarsimp simp: ptr_range_def invs_psp_aligned invs_valid_objs
descendants_range_def2 empty_descendants_range_in
is_aligned_neg_mask_eq page_bits_def)
apply ((strengthen refl | simp)+)?
apply (rule conjI, fastforce)
apply (rule conjI, fastforce intro: empty_descendants_range_in)
apply(rule conjI)
apply(clarsimp simp: range_cover_def obj_bits_api_def default_arch_object_def)
apply(subst is_aligned_neg_mask_eq[THEN sym], assumption)
apply(simp add: mask_neg_mask_is_zero pageBits_def mask_zero)
apply(clarsimp simp: aag_cap_auth_def pas_refined_refl)
apply(drule_tac x=x in bspec)
apply(simp add: is_aligned_no_overflow)
apply(clarsimp simp: pas_refined_refl cap_links_asid_slot_def label_owns_asid_slot_def cap_links_irq_def)
apply(fastforce dest: cte_wp_at_valid_objs_valid_cap simp: valid_cap_def cap_aligned_def)
apply (rule conjI)
apply (clarsimp simp: range_cover_def obj_bits_api_def default_arch_object_def)
apply (subst is_aligned_neg_mask_eq[THEN sym], assumption)
apply (simp add: mask_neg_mask_is_zero pageBits_def mask_zero)
apply (clarsimp simp: aag_cap_auth_def pas_refined_refl)
apply (drule_tac x=frame in bspec)
apply (simp add: is_aligned_no_overflow)
apply (clarsimp simp: pas_refined_refl cap_links_asid_slot_def
label_owns_asid_slot_def cap_links_irq_def)
apply (fastforce dest: cte_wp_at_valid_objs_valid_cap simp: valid_cap_def cap_aligned_def)
done
lemma set_asid_pool_respects:
@ -994,8 +1016,9 @@ lemma perform_asid_pool_invocation_pas_refined [wp]:
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: perform_asid_pool_invocation_def)
apply (rule hoare_pre)
apply (wp get_cap_auth_wp [where aag = aag] set_cap_pas_refined_not_transferable | wpc)+
apply (clarsimp simp: authorised_asid_pool_inv_def cap_links_asid_slot_def is_subject_asid_into_loas aag_cap_auth_def)
apply (wp get_cap_auth_wp[where aag = aag] set_cap_pas_refined_not_transferable | wpc)+
apply (clarsimp simp: authorised_asid_pool_inv_def cap_links_asid_slot_def
is_subject_asid_into_loas aag_cap_auth_def)
apply (clarsimp simp: cap_auth_conferred_def is_cap_simps is_page_cap_def auth_graph_map_mem
pas_refined_all_auth_is_owns pas_refined_refl cli_no_irqs
cte_wp_at_caps_of_state
@ -1006,7 +1029,7 @@ lemma perform_asid_pool_invocation_pas_refined [wp]:
valid_apinv_def obj_at_def)
apply (drule(2) asid_pool_uniqueness)
apply (simp add: obj_at_def)
apply (case_tac "asid = 0", simp_all add: pas_refined_refl)[1]
apply (case_tac "asid = 0"; simp add: pas_refined_refl)
apply (simp add: asid_low_high_bits[rotated, OF arg_cong[where f=ucast]])
apply (clarsimp simp: obj_at_def)
apply (frule (2) asid_pool_into_aag)
@ -1063,11 +1086,13 @@ lemma invoke_arch_pas_refined:
lemma create_mapping_entries_authorised_slots [wp]:
"\<lbrace>\<exists>\<rhd> pd and invs and pas_refined aag
and K (is_subject aag pd \<and> is_aligned pd pd_bits
\<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base
\<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights.
\<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size).
aag_has_auth_to aag a p))\<rbrace>
and K (is_subject aag pd
\<and> is_aligned pd pd_bits
\<and> vmsz_aligned vptr vmpage_size
\<and> vptr < kernel_base
\<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights.
\<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size).
aag_has_auth_to aag a p))\<rbrace>
create_mapping_entries base vptr vmpage_size rights attrib pd
\<lbrace>\<lambda>rv s. authorised_slots aag rv\<rbrace>, -"
unfolding authorised_slots_def
@ -1132,79 +1157,102 @@ lemma decode_arch_invocation_authorised:
apply (clarsimp simp: authorised_asid_pool_inv_def authorised_page_table_inv_def
neq_Nil_conv invs_psp_aligned invs_vspace_objs cli_no_irqs)
apply (drule diminished_cte_wp_at_valid_cap, clarsimp+)
apply (cases cap, simp_all)
apply (cases cap; simp)
\<comment> \<open>asid pool\<close>
apply ((clarsimp simp: split_def cap_auth_conferred_def is_page_cap_def
pas_refined_all_auth_is_owns asid_high_bits_of_add_ucast
valid_cap_simps cap_links_asid_slot_def
label_owns_asid_slot_def pas_refined_refl )+)[1]
apply (find_goal \<open>match premises in "cap = ASIDPoolCap _ _" \<Rightarrow> succeed\<close>)
subgoal for s obj_ref asid
by (clarsimp simp: cap_auth_conferred_def is_page_cap_def
pas_refined_all_auth_is_owns asid_high_bits_of_add_ucast
valid_cap_simps)
\<comment> \<open>ControlCap\<close>
apply (clarsimp simp: neq_Nil_conv split_def valid_cap_simps)
apply (cases excaps, simp_all)[1]
apply (clarsimp simp: neq_Nil_conv aag_has_auth_to_Control_eq_owns)
apply (drule cte_wp_at_valid_objs_valid_cap, clarsimp)
apply (clarsimp simp: valid_cap_def cap_aligned_def)
apply (clarsimp simp: is_cap_simps cap_auth_conferred_def pas_refined_all_auth_is_owns aag_cap_auth_def)
apply (find_goal \<open>match premises in "cap = ASIDControlCap" \<Rightarrow> succeed\<close>)
subgoal
apply (clarsimp simp: neq_Nil_conv split_def valid_cap_simps)
apply (cases excaps, solves simp)
apply (clarsimp simp: neq_Nil_conv aag_has_auth_to_Control_eq_owns)
apply (drule cte_wp_at_valid_objs_valid_cap, clarsimp)
apply (clarsimp simp: valid_cap_def cap_aligned_def)
apply (clarsimp simp: is_cap_simps cap_auth_conferred_def
pas_refined_all_auth_is_owns aag_cap_auth_def)
done
\<comment> \<open>PageCap\<close>
apply (clarsimp simp: valid_cap_simps cli_no_irqs)
apply (cases "invocation_type label", simp_all)
apply (rename_tac archlabel)
apply (case_tac archlabel, simp_all)
\<comment> \<open>Map\<close>
apply (clarsimp simp: cap_auth_conferred_def is_cap_simps is_page_cap_def pas_refined_all_auth_is_owns)
apply (rule conjI)
apply (clarsimp simp: cap_auth_conferred_def is_page_cap_def pas_refined_all_auth_is_owns aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def)
apply (rule conjI, fastforce)
apply (simp only: linorder_not_le kernel_base_less_observation
vmsz_aligned_t2n_neg_mask simp_thms)
apply (clarsimp simp: cap_auth_conferred_def is_page_cap_def
pas_refined_all_auth_is_owns cli_no_irqs aag_cap_auth_def
exI vspace_cap_rights_to_auth_def mask_vm_rights_def
validate_vm_rights_def vm_read_write_def vm_read_only_def
vm_kernel_only_def)
\<comment> \<open>Remap\<close>
apply (clarsimp simp: cap_auth_conferred_def
is_page_cap_def pas_refined_all_auth_is_owns)
apply (rule conjI, fastforce)
apply clarsimp
apply (drule (1) bspec)
apply (erule bspec)
apply (clarsimp simp: vspace_cap_rights_to_auth_def mask_vm_rights_def
validate_vm_rights_def vm_read_write_def vm_read_only_def
vm_kernel_only_def
split: if_split_asm)
\<comment> \<open>Unmap\<close>
apply (simp add: aag_cap_auth_def cli_no_irqs)
\<comment> \<open>PageTableCap\<close>
apply (cases "invocation_type label", simp_all)
apply (rename_tac archlabel)
apply (case_tac archlabel, simp_all)
\<comment> \<open>PTMap\<close>
apply (clarsimp simp: aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def cap_auth_conferred_def is_page_cap_def
pde_ref2_def pas_refined_all_auth_is_owns pas_refined_refl pd_shifting [folded pd_bits_14] )
\<comment> \<open>Unmap\<close>
apply (rename_tac word option archlabel)
apply (clarsimp simp: aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def cap_auth_conferred_def is_page_cap_def
pde_ref2_def pas_refined_all_auth_is_owns pas_refined_refl )
apply (subgoal_tac "x && ~~ mask pt_bits = word")
apply simp
apply (clarsimp simp: valid_cap_simps cap_aligned_def split: if_split_asm)
apply (subst (asm) upto_enum_step_subtract)
apply (subgoal_tac "is_aligned word pt_bits")
apply (simp add: is_aligned_no_overflow)
apply (simp add: pt_bits_def pageBits_def)
apply (simp add: word_minus_1 minus_one_norm)
apply (subst (asm) upto_enum_step_red [where us = 2, simplified])
apply (simp add: pt_bits_def pageBits_def word_bits_conv)
apply (simp add: pt_bits_def pageBits_def word_bits_conv)
apply clarsimp
apply (subst is_aligned_add_helper)
apply (simp add: pt_bits_def pageBits_def)
apply (erule word_less_power_trans_ofnat [where k = 2, simplified])
apply (simp add: pt_bits_def pageBits_def)
apply (simp add: pt_bits_def pageBits_def word_bits_conv)
apply simp
apply (find_goal \<open>match premises in "cap = PageCap _ _ _ _ _" \<Rightarrow> succeed\<close>)
subgoal for s is_dev obj_ref cap_rights vmpage_size mapping
apply (clarsimp simp: valid_cap_simps cli_no_irqs)
apply (cases "invocation_type label"; (solves \<open>simp\<close>)?)
apply (find_goal \<open>match premises in "_ = ArchInvocationLabel _" \<Rightarrow> succeed\<close>)
apply (rename_tac archlabel)
apply (case_tac archlabel; (solves \<open>simp\<close>)?)
\<comment> \<open>Map\<close>
apply (find_goal \<open>match premises in "_ = ARMPageMap" \<Rightarrow> succeed\<close>)
subgoal
apply (clarsimp simp: cap_auth_conferred_def is_cap_simps is_page_cap_def
pas_refined_all_auth_is_owns)
apply (rule conjI)
apply (clarsimp simp: cap_auth_conferred_def is_page_cap_def pas_refined_all_auth_is_owns
aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def)
apply (simp only: linorder_not_le kernel_base_less_observation
vmsz_aligned_t2n_neg_mask simp_thms)
apply (clarsimp simp: cap_auth_conferred_def vspace_cap_rights_to_auth_def
mask_vm_rights_def validate_vm_rights_def vm_read_only_def
vm_kernel_only_def)
done
\<comment> \<open>Remap\<close>
apply (find_goal \<open>match premises in "_ = ARMPageRemap" \<Rightarrow> succeed\<close>)
subgoal
apply (clarsimp simp: cap_auth_conferred_def
is_page_cap_def pas_refined_all_auth_is_owns)
apply (drule (1) bspec)
apply (erule bspec)
apply (clarsimp simp: vspace_cap_rights_to_auth_def
mask_vm_rights_def validate_vm_rights_def vm_read_only_def
vm_kernel_only_def)
apply (simp only: auth.distinct rights.distinct empty_iff insert_iff simp_thms
split: if_split_asm)
done
apply (find_goal \<open>match premises in "_ = ARMPageUnmap" \<Rightarrow> succeed\<close>)
\<comment> \<open>Unmap\<close>
subgoal by (simp add: aag_cap_auth_def cli_no_irqs)
done
\<comment> \<open>PageTableCap\<close>
apply (find_goal \<open>match premises in "cap = PageTableCap _ _" \<Rightarrow> succeed\<close>)
subgoal for s word option
apply (cases "invocation_type label"; (solves \<open>simp\<close>)?)
apply (find_goal \<open>match premises in "_ = ArchInvocationLabel _" \<Rightarrow> succeed\<close>)
apply (rename_tac archlabel)
apply (case_tac archlabel; (solves \<open>simp\<close>)?)
\<comment> \<open>PTMap\<close>
apply (find_goal \<open>match premises in "_ = ARMPageTableMap" \<Rightarrow> succeed\<close>)
apply (clarsimp simp: aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def
cap_auth_conferred_def is_page_cap_def
pde_ref2_def pas_refined_all_auth_is_owns pas_refined_refl
pd_shifting[folded pd_bits_14])
\<comment> \<open>Unmap\<close>
apply (find_goal \<open>match premises in "_ = ARMPageTableUnmap" \<Rightarrow> succeed\<close>)
subgoal
apply (clarsimp simp: aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def
cap_auth_conferred_def is_page_cap_def
pde_ref2_def pas_refined_all_auth_is_owns pas_refined_refl)
apply (subgoal_tac "x && ~~ mask pt_bits = word")
apply simp
apply (clarsimp simp: valid_cap_simps cap_aligned_def split: if_split_asm)
apply (subst (asm) upto_enum_step_subtract)
apply (subgoal_tac "is_aligned word pt_bits")
apply (simp add: is_aligned_no_overflow)
apply (simp add: pt_bits_def pageBits_def)
apply (simp add: word_minus_1 minus_one_norm)
apply (subst (asm) upto_enum_step_red [where us = 2, simplified])
apply (simp add: pt_bits_def pageBits_def word_bits_conv)
apply (simp add: pt_bits_def pageBits_def word_bits_conv)
apply clarsimp
apply (subst is_aligned_add_helper)
apply (simp add: pt_bits_def pageBits_def)
apply (erule word_less_power_trans_ofnat [where k = 2, simplified])
apply (simp add: pt_bits_def pageBits_def)
apply (simp add: pt_bits_def pageBits_def word_bits_conv)
apply simp
done
done
done
crunch pas_refined[wp]: invalidate_asid_entry "pas_refined aag"
@ -1262,11 +1310,9 @@ lemma pas_refined_asid_mem:
by (auto simp add: pas_refined_def)
(* FIXME: replace precondition by asid_pool_integrity *)
lemma set_asid_pool_respects_clear:
"\<lbrace>(\<lambda>s. \<forall>pool'. ko_at (ArchObj (arch_kernel_obj.ASIDPool pool')) ptr s
\<longrightarrow> (\<forall>x. pool x \<noteq> pool' x \<longrightarrow> pool x = None \<and>
aag_has_auth_to aag Control (the (pool' x))))
\<longrightarrow> asid_pool_integrity {pasSubject aag} aag pool' pool)
and integrity aag X st\<rbrace>
set_asid_pool ptr pool \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def)
@ -1275,7 +1321,7 @@ lemma set_asid_pool_respects_clear:
split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm)
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def)
apply (rule tro_asidpool_clear,(simp add:asid_pool_integrity_def)+)
apply (rule tro_asidpool_clear; simp add: asid_pool_integrity_def)
done
lemma delete_asid_respects:
@ -1283,7 +1329,7 @@ lemma delete_asid_respects:
delete_asid asid pd
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
by (wpsimp wp: set_asid_pool_respects_clear hoare_vcg_all_lift
simp: obj_at_def pas_refined_refl delete_asid_def)
simp: obj_at_def pas_refined_refl delete_asid_def asid_pool_integrity_def)
end

175
proof/access-control/CNode_AC.thy
View File

@ -27,13 +27,9 @@ lemma tcb_domain_map_wellformed_ekheap[intro!, simp]:
"ekheap (P s) = ekheap s \<Longrightarrow> tcb_domain_map_wellformed aag (P s) = tcb_domain_map_wellformed aag s"
by (simp add: tcb_domain_map_wellformed_aux_def get_etcb_def)
section{* CNode-specific AC. *}
lemma set_original_integrity_autarch:
"\<lbrace>integrity aag X st and K (is_subject aag (fst slot))\<rbrace>
set_original slot orig \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
@ -43,10 +39,6 @@ lemma set_original_integrity_autarch:
apply (clarsimp intro!: integrity_cdt_direct)
done
lemma set_original_integrity:
"\<lbrace>integrity aag X st and cdt_change_allowed' aag slot\<rbrace>
set_original slot orig
@ -391,9 +383,6 @@ lemma set_cap_pas_refined_not_transferable:
(* FIXME MOVE *)
lemma parent_ofI[intro!]: "m x = Some src \<Longrightarrow> m \<Turnstile> src \<leadsto> x"
by (simp add: cdt_parent_rel_def is_cdt_parent_def)
@ -426,7 +415,7 @@ lemma cap_swap_respects[wp]:
K (is_subject aag (fst slot) \<and> is_subject aag (fst slot'))\<rbrace>
cap_swap cap slot cap' slot' \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: cap_swap_def) apply (elim conjE)
apply (simp add: cap_swap_def)
apply (wp get_cap_wp set_cap_integrity_autarch
cap_swap_ext_extended.list_integ_lift[where Q="\<top>"] cap_swap_list_integrity
set_original_integrity_autarch[unfolded pred_conj_def K_def]
@ -466,7 +455,7 @@ lemma dmo_no_mem_respects:
apply (erule (1) use_valid [OF _ q])
done
(* MOVE *)
(* FIXME: MOVE *)
(* Only works after a hoare_pre! *)
lemma dmo_wp:
assumes mopv: "\<And>s. \<lbrace>P s\<rbrace> mop \<lbrace>\<lambda>a b. R a (s\<lparr>machine_state := b\<rparr>)\<rbrace>"
@ -503,6 +492,7 @@ abbreviation cleanup_info_wf :: "cap \<Rightarrow> 'a PAS \<Rightarrow> bool"
where
"cleanup_info_wf c aag \<equiv> c \<noteq> NullCap \<longrightarrow> (\<exists>irq. c = (IRQHandlerCap irq) \<and> is_subject_irq aag irq)"
(* FIXME: MOVE *)
named_theorems wp_transferable
named_theorems wp_not_transferable
@ -520,8 +510,10 @@ lemma empty_slot_integrity_spec:
empty_slot_extended.list_integ_lift empty_slot_list_integrity[where m="cdt s"] |
simp add: set_cdt_def |
wpc)+
apply safe
by (clarsimp simp add: integrity_def, blast intro: cca_owned cdt_change_allowed_all_children)+
apply (safe; \<comment> \<open>for speedup\<close>
clarsimp simp add: integrity_def,
blast intro: cca_owned cdt_change_allowed_all_children)
done
lemma empty_slot_integrity[wp,wp_not_transferable]:
"\<lbrace>integrity aag X st and valid_list and valid_objs and valid_mdb and pas_refined aag and
@ -591,8 +583,8 @@ lemma set_cap_integrity_deletion_aux:
apply clarsimp
apply (erule is_transferable.cases, blast)
apply (fastforce intro: reply_cap_deletion_integrity_intros)
apply (intro reply_cap_deletion_integrityI2)
apply (clarsimp) apply (rule conjI,rule refl)+
apply clarsimp
apply (rule reply_cap_deletion_integrityI2[OF refl refl])
apply (elim cdt_change_allowedE cdt_direct_change_allowed.cases)
apply (drule reply_cap_no_grand_parent[where cs="caps_of_state s"]; fastforce?)
apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
@ -607,8 +599,8 @@ lemma set_cap_integrity_deletion_aux:
apply clarsimp
apply (elim is_transferable.cases, simp)
apply (fastforce intro: reply_cap_deletion_integrity_intros)
apply (intro reply_cap_deletion_integrityI2)
apply (clarsimp) apply (rule conjI, rule refl)+
apply clarsimp
apply (rule reply_cap_deletion_integrityI2[OF refl refl])
apply (elim cdt_change_allowedE cdt_direct_change_allowed.cases)
apply (force simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
dest: reply_cap_no_grand_parent cap_auth_caps_of_state pas_refined_Control)
@ -634,8 +626,8 @@ lemma set_cap_integrity_deletion_aux:
apply clarsimp
apply (elim is_transferable.cases, simp)
apply (fastforce intro: reply_cap_deletion_integrity_intros)
apply (intro reply_cap_deletion_integrityI2)
apply (clarsimp) apply (rule conjI, rule refl)+
apply clarsimp
apply (rule reply_cap_deletion_integrityI2[OF refl refl])
apply (elim cdt_change_allowedE cdt_direct_change_allowed.cases)
apply (force simp:aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
dest: reply_cap_no_grand_parent cap_auth_caps_of_state pas_refined_Control)
@ -774,20 +766,21 @@ lemma empty_slot_integrity_transferable[wp_transferable]:
empty_slot slot c \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply integrity_trans_start
apply (rule hoare_pre)
apply (simp add:empty_slot_def)
apply (simp add: empty_slot_def)
apply (simp add: empty_slot_commute_ugly[simplified])
apply (simp add:set_cdt_def)
apply (simp add: set_cdt_def)
apply (wp set_original_wp)
apply (rename_tac cdtv x)
apply (rule_tac Q = "\<lambda>_ s'. integrity aag X s s'\<and> cdtv = cdt s \<and>
is_original_cap s = is_original_cap s'"
in hoare_post_imp)
apply (clarsimp simp add:integrity_def)
apply (clarsimp simp add: integrity_def)
apply (frule all_childrenD[OF cdt_change_allowed_all_children];fastforce)
apply (wp empty_slot_extended.list_integ_lift)
apply (rule hoare_pre)
apply (rule_tac m = "cdt s" in empty_slot_list_integrity)
apply simp apply wp+
apply (rule_tac m = "cdt s" in empty_slot_list_integrity)
apply simp
apply wp+
apply (wp set_cap_integrity_deletion gets_wp get_cap_wp)+
by (fastforce intro: cdt_change_allowed_all_children)
@ -804,10 +797,11 @@ lemma set_cdt_pas_refined:
apply (simp add: pas_refined_def state_objs_to_policy_def set_cdt_def)
apply (wp | simp | simp_all)+
apply (clarsimp dest!: auth_graph_map_memD)
apply (subgoal_tac "\<forall>x y. c x = Some y \<longrightarrow>
(is_transferable (caps_of_state s x) \<or>
(pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag)
\<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag")
apply (subgoal_tac
"\<forall>x y. c x = Some y \<longrightarrow>
(is_transferable (caps_of_state s x)
\<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag)
\<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag")
defer
apply (intro allI, case_tac "cdt s x = Some y")
apply (solves\<open>auto intro: auth_graph_map_memI state_bits_to_policy.intros\<close>)
@ -871,13 +865,6 @@ lemma state_objs_to_policy_more_update[simp]:
state_objs_to_policy s"
by (simp add: state_objs_to_policy_def)
(*lemma tcb_domain_map_wellformed_lift:
assumes ekh: "\<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>"
shows "\<lbrace>tcb_domain_map_wellformed aag\<rbrace> f \<lbrace>\<lambda>_. tcb_domain_map_wellformed aag\<rbrace>"
apply (simp add: tcb_domain_map_wellformed_aux_def get_etcb_def)
apply (wp ekh)
done*)
end
context is_extended begin
@ -905,24 +892,24 @@ lemma untyped_not_transferable:
(* FIXME MOVE *)
lemma is_transferable_max_free_index_update[simp]:
"is_transferable (Some (max_free_index_update cap)) = is_transferable (Some cap)"
by (simp add: is_transferable.simps free_index_update_def split: cap.splits)
by (simp add: is_transferable.simps free_index_update_def split: cap.splits)
lemma set_untyped_cap_as_full_is_transferable[wp]:
"\<lbrace>\<lambda>s.\<not> is_transferable (caps_of_state s other_slot)\<rbrace>
set_untyped_cap_as_full src_cap new_cap slot
\<lbrace>\<lambda>rv s. \<not> is_transferable (caps_of_state s other_slot)\<rbrace>"
apply (clarsimp simp: set_untyped_cap_as_full_def)
apply wp
using untyped_not_transferable max_free_index_update_preserve_untyped by simp
apply (clarsimp simp: set_untyped_cap_as_full_def)
apply wp
using untyped_not_transferable max_free_index_update_preserve_untyped by simp
lemma set_untyped_cap_as_full_is_transferable':
"\<lbrace>\<lambda>s. is_transferable ((caps_of_state s(slot2 \<mapsto> new_cap)) slot3) \<and> Some src_cap = (caps_of_state s slot)\<rbrace>
set_untyped_cap_as_full src_cap new_cap slot
\<lbrace>\<lambda>rv s. is_transferable ((caps_of_state s(slot2 \<mapsto> new_cap)) slot3)\<rbrace>"
apply (clarsimp simp: set_untyped_cap_as_full_def)
apply safe
apply (wp,fastforce)+
done
apply (clarsimp simp: set_untyped_cap_as_full_def)
apply safe
apply (wp,fastforce)+
done
lemma cap_insert_pas_refined:
"\<lbrace>pas_refined aag and valid_mdb and
@ -1007,9 +994,8 @@ lemma cap_move_pas_refined[wp]:
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: cap_move_def)
apply (rule hoare_pre)
apply (wp set_cap_pas_refined set_cdt_pas_refined tcb_domain_map_wellformed_lift
set_cap_caps_of_state2
| simp)+
apply (wpsimp wp: set_cap_pas_refined set_cdt_pas_refined tcb_domain_map_wellformed_lift
set_cap_caps_of_state2)
by (fastforce simp: is_transferable_weak_derived valid_mdb_def2 mdb_cte_at_def
Option.is_none_def cte_wp_at_caps_of_state
simp del: split_paired_All
@ -1025,10 +1011,8 @@ lemma empty_slot_pas_refined[wp, wp_not_transferable]:
empty_slot slot irqopt
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: empty_slot_def)
apply (wp set_cap_pas_refined get_cap_wp set_cdt_pas_refined
tcb_domain_map_wellformed_lift hoare_drop_imps
| simp | wpc)+
apply clarsimp
apply (wpsimp wp: set_cap_pas_refined get_cap_wp set_cdt_pas_refined
tcb_domain_map_wellformed_lift hoare_drop_imps)
apply (strengthen aag_wellformed_delete_derived_trans[OF _ _ pas_refined_wellformed,
mk_strg I _ _ A])
by (fastforce dest: all_childrenD is_transferable_all_children
@ -1053,10 +1037,10 @@ lemma empty_slot_pas_refined_transferable[wp_transferable]:
lemma obj_ref_weak_derived:
"weak_derived cap cap' \<Longrightarrow> obj_refs cap = obj_refs cap'"
unfolding obj_refs_def aobj_ref'_def weak_derived_def copy_of_def same_object_as_def
apply (cases cap)
prefer 12 (* Should be Arch Cap *)
apply (case_tac x12)
by (fastforce simp: is_cap_simps split:cap.splits arch_cap.splits)+
by (cases cap;
(* also split arch caps *)
(match premises in "cap = ArchObjectCap acap" for acap \<Rightarrow> \<open>cases acap\<close>)?;
fastforce simp: is_cap_simps split: cap.splits arch_cap.splits)
crunch thread_states[wp]: set_cdt "\<lambda>s. P (thread_states s)"
@ -1082,12 +1066,15 @@ lemma cap_swap_pas_refined[wp]:
split del: if_split)
apply (rename_tac old_cap old_cap')
apply (intro conjI)
defer
apply (find_goal \<open>match conclusion in "state_asids_to_policy_aux _ _ _ _ \<subseteq> _" \<Rightarrow> succeed\<close>)
apply (erule(1) sata_update2[unfolded fun_upd_def]; fastforce)
apply (find_goal \<open>match conclusion in "state_irqs_to_policy_aux _ _ \<subseteq> _" \<Rightarrow> succeed\<close>)
apply (erule sita_caps_update2[unfolded fun_upd_def]; fastforce)
apply (find_goal \<open>match conclusion in "auth_graph_map _ _ \<subseteq> _" \<Rightarrow> succeed\<close>)
apply (rule subsetI)
apply clarsimp
apply (erule auth_graph_map_memE)
apply (simp only: eq_commute[where b=slot'] eq_commute[where b=slot])
apply (erule state_bits_to_policy.cases)
apply (simp split: if_splits, blast intro: sbta_caps auth_graph_map_memI)
apply (simp split: if_splits, blast intro: state_bits_to_policy.intros auth_graph_map_memI)
@ -1095,18 +1082,15 @@ lemma cap_swap_pas_refined[wp]:
apply (blast intro: state_bits_to_policy.intros auth_graph_map_memI)
apply clarsimp
subgoal for s old_cap old_cap' child_obj child_index parent_obj parent_index
apply (simp split: if_splits
add: eq_commute[where b=slot'] eq_commute[where b=slot] aag_wellformed_refl)
apply (simp split: if_splits add: aag_wellformed_refl)
by (erule subsetD;
force simp: is_transferable_weak_derived intro!: sbta_cdt auth_graph_map_memI)+
apply clarsimp
subgoal for s old_cap old_cap' child_obj child_index parent_obj parent_index
apply (simp split: if_splits
add: eq_commute[where b=slot'] eq_commute[where b=slot] aag_wellformed_refl)
apply (simp split: if_splits add: aag_wellformed_refl)
by (erule subsetD;
force simp: is_transferable_weak_derived intro!: sbta_cdt_transferable auth_graph_map_memI)+
by (blast intro: state_bits_to_policy.intros auth_graph_map_memI)+
by (blast intro: state_bits_to_policy.intros auth_graph_map_memI)
lemma cap_swap_for_delete_pas_refined[wp]:
@ -1130,9 +1114,9 @@ lemma sts_respects_restart_ep:
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def obj_at_def st_tcb_at_def get_tcb_def)
apply (rule_tac tro_tcb_restart [OF refl refl])
apply (fastforce dest!: get_tcb_SomeD)
apply (fastforce dest!: get_tcb_SomeD)
apply simp
apply (fastforce dest!: get_tcb_SomeD)
apply (fastforce dest!: get_tcb_SomeD)
apply simp
done
lemma set_endpoinintegrity:
@ -1191,9 +1175,9 @@ lemma sbn_thread_bound_ntfns[wp]:
(* FIXME move to AInvs *)
lemma set_thread_state_ekheap[wp]:
"\<lbrace>\<lambda>s. P (ekheap s)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>"
apply (simp add: set_thread_state_def)
apply (wp set_scheduler_action_wp | simp add: set_thread_state_ext_def)+
done
apply (simp add: set_thread_state_def)
apply (wpsimp wp: set_scheduler_action_wp simp: set_thread_state_ext_def)
done
lemma set_thread_state_pas_refined:
"\<lbrace>pas_refined aag and
@ -1204,57 +1188,61 @@ lemma set_thread_state_pas_refined:
apply (rule hoare_pre)
apply (wp tcb_domain_map_wellformed_lift | wps)+
apply (clarsimp dest!: auth_graph_map_memD)
apply (erule state_bits_to_policy.cases)
apply (auto intro: state_bits_to_policy.intros auth_graph_map_memI
apply (erule state_bits_to_policy.cases;
auto intro: state_bits_to_policy.intros auth_graph_map_memI
split: if_split_asm)
done
lemma set_simple_ko_vrefs[wp]:
"\<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> set_simple_ko f ptr val \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace>"
apply (simp add: set_simple_ko_def set_object_def)
apply (wp get_object_wp; clarsimp; rule conjI)
apply (wp get_object_wp)
apply clarify
apply (clarsimp simp: state_vrefs_def vs_refs_no_global_pts_def obj_at_def
partial_inv_def a_type_def
elim!: rsubst[where P=P, OF _ ext]
split: Structures_A.kernel_object.split_asm)+
split: Structures_A.kernel_object.split_asm if_splits)
done
lemma set_simple_ko_tcb_states_of_state[wp]:
"\<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> set_simple_ko f ptr val \<lbrace>\<lambda>rv s. P (tcb_states_of_state s)\<rbrace>"
apply (simp add: set_simple_ko_def set_object_def)
apply (wp get_object_wp; clarsimp; rule conjI)
apply (wp get_object_wp)
apply clarify
apply (clarsimp simp: thread_states_def obj_at_def get_tcb_def tcb_states_of_state_def
partial_inv_def a_type_def
elim!: rsubst[where P=P, OF _ ext]
split: Structures_A.kernel_object.split_asm option.split)+
split: Structures_A.kernel_object.split_asm if_splits)
done
lemma set_simple_ko_thread_states[wp]:
"\<lbrace>\<lambda>s. P (thread_states s)\<rbrace> set_simple_ko f ptr val \<lbrace>\<lambda>rv s. P (thread_states s)\<rbrace>"
apply (simp add: set_simple_ko_def set_object_def)
apply (wp get_object_wp; clarsimp; rule conjI)
apply (wp get_object_wp)
apply clarify
apply (clarsimp simp: thread_states_def obj_at_def get_tcb_def tcb_states_of_state_def
partial_inv_def a_type_def
elim!: rsubst[where P=P, OF _ ext]
split: Structures_A.kernel_object.split_asm option.split)+
split: Structures_A.kernel_object.split_asm if_splits)
done
lemma set_simple_ko_thread_bound_ntfns[wp]:
"\<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> set_simple_ko f ptr val \<lbrace>\<lambda>rv s. P (thread_bound_ntfns s)\<rbrace>"
apply (simp add: set_simple_ko_def set_object_def)
apply (wp get_object_wp; clarsimp; rule conjI)
apply (wp get_object_wp)
apply clarify
apply (clarsimp simp: thread_bound_ntfns_def obj_at_def get_tcb_def tcb_states_of_state_def
partial_inv_def a_type_def
elim!: rsubst[where P=P, OF _ ext]
split: Structures_A.kernel_object.split_asm option.split)+
split: Structures_A.kernel_object.split_asm if_splits)
done
(* FIXME move to AInvs *)
lemma set_simple_ko_ekheap[wp]:
"\<lbrace>\<lambda>s. P (ekheap s)\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>"
apply (simp add: set_simple_ko_def)
apply (wp get_object_wp | simp)+
done
apply (simp add: set_simple_ko_def)
apply (wpsimp wp: get_object_wp)
done
lemma set_simple_ko_pas_refined[wp]:
"\<lbrace>pas_refined aag\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
@ -1313,16 +1301,12 @@ lemma aag_owned_cdt_link:
\<not> is_transferable (caps_of_state s x) \<rbrakk> \<Longrightarrow> is_subject aag (fst x)"
by (fastforce dest: sta_cdt pas_refined_mem pas_refined_Control)
(*FIXME RENAME descendants_of_owned in descendants_of_owned_or_transferable + MOVE *)
lemma descendants_of_owned:
"\<lbrakk> valid_mdb s ; pas_refined aag s; p \<in> descendants_of q (cdt s); is_subject aag (fst q) \<rbrakk>
(* FIXME: MOVE *)
lemma descendants_of_owned_or_transferable:
"\<lbrakk> valid_mdb s; pas_refined aag s; p \<in> descendants_of q (cdt s); is_subject aag (fst q) \<rbrakk>
\<Longrightarrow> is_subject aag (fst p) \<or> is_transferable (caps_of_state s p)"
using all_children_descendants_of pas_refined_all_children by blast
lemma pas_refined_arch_state_update_not_asids[simp]:
"(arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s)) \<Longrightarrow> pas_refined aag (arch_state_update f s) = pas_refined aag s"
by (simp add: pas_refined_def state_objs_to_policy_def)
@ -1781,7 +1765,7 @@ lemma arch_derive_cap_obj_refs_auth:
\<lbrace>(\<lambda>x s. \<forall>r\<in>obj_refs x. \<forall>auth\<in>cap_auth_conferred x. aag_has_auth_to aag auth r)\<rbrace>, -"
unfolding arch_derive_cap_def
apply (rule hoare_pre)
apply (wp | wpc)+
apply (wp | wpc)+
apply (clarsimp simp: cap_auth_conferred_def is_page_cap_def)
done
@ -1791,7 +1775,7 @@ lemma derive_cap_obj_refs_auth:
\<lbrace>\<lambda>x s. (\<forall>r\<in>obj_refs x. \<forall>auth\<in>cap_auth_conferred x. aag_has_auth_to aag auth r) \<rbrace>, -"
unfolding derive_cap_def
apply (rule hoare_pre)
apply (wp arch_derive_cap_obj_refs_auth | wpc | simp)+
apply (wp arch_derive_cap_obj_refs_auth | wpc | simp)+
done
lemma arch_derive_cap_cli:
@ -1846,8 +1830,11 @@ lemma update_cap_untyped_range_subset:
split: if_split_asm)
done
lemmas derive_cap_aag_caps = derive_cap_obj_refs_auth derive_cap_untyped_range_subset
derive_cap_clas derive_cap_cli
lemmas derive_cap_aag_caps =
derive_cap_obj_refs_auth
derive_cap_untyped_range_subset
derive_cap_clas
derive_cap_cli
lemma derive_cap_cap_cur_auth [wp]:
"\<lbrace>\<lambda>s. pas_cap_cur_auth aag cap\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. pas_cap_cur_auth aag rv\<rbrace>, -"

179
proof/access-control/Finalise_AC.thy
View File

@ -41,27 +41,27 @@ lemma tcb_sched_action_dequeue_integrity[wp]:
"\<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag thread)\<rbrace>
tcb_sched_action tcb_sched_dequeue thread
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def
split: option.splits)
apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE)
apply (auto intro: domtcbs)
done
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def
split: option.splits)
apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE)
apply (auto intro: domtcbs)
done
lemma tcb_sched_action_enqueue_integrity[wp]:
"\<lbrace>integrity aag X st\<rbrace>
tcb_sched_action tcb_sched_enqueue thread
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
tcb_domain_map_wellformed_aux_def tcb_at_def get_etcb_def
tcb_sched_enqueue_def etcb_at_def
split: option.splits)
apply (metis append.simps(2))
done
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
tcb_domain_map_wellformed_aux_def tcb_at_def get_etcb_def
tcb_sched_enqueue_def etcb_at_def
split: option.splits)
apply (metis append.simps(2))
done
text {* See comment for @{thm tcb_sched_action_dequeue_integrity'} *}
lemma tcb_sched_action_append_integrity':
@ -79,14 +79,14 @@ lemma tcb_sched_action_append_integrity[wp]:
"\<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag thread)\<rbrace>
tcb_sched_action tcb_sched_append thread
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def
split: option.splits)
apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE)
apply (auto intro: domtcbs)
done
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def
tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def
split: option.splits)
apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE)
apply (auto intro: domtcbs)
done
lemma tcb_sched_action_append_integrity_pasMayEditReadyQueues:
"\<lbrace>integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag)\<rbrace>
@ -99,10 +99,10 @@ lemma tcb_sched_action_append_integrity_pasMayEditReadyQueues:
lemma reschedule_required_integrity[wp]:
"\<lbrace>integrity aag X st\<rbrace> reschedule_required \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: integrity_def reschedule_required_def)
apply (wp | wpc)+
apply simp
done
apply (simp add: integrity_def reschedule_required_def)
apply (wp | wpc)+
apply simp
done
lemma cancel_badged_sends_respects[wp]:
"\<lbrace>integrity aag X st and einvs
@ -123,7 +123,7 @@ lemma cancel_badged_sends_respects[wp]:
apply (simp add: bind_assoc)
apply (rule hoare_seq_ext[OF _ gts_sp])
apply (rule hoare_pre)
apply (wp add:sts_respects_restart_ep hoare_vcg_const_Ball_lift sts_st_tcb_at_neq)+
apply (wp sts_respects_restart_ep hoare_vcg_const_Ball_lift sts_st_tcb_at_neq)
apply clarsimp
apply fastforce
apply (wp set_endpoinintegrity hoare_vcg_const_Ball_lift get_simple_ko_wp)+
@ -285,12 +285,10 @@ lemma reply_cap_descends_from_master0:
done
(*declare empty_slot_pas_refined[wp del]*)
lemma reply_cancel_ipc_pas_refined[wp]:
"\<lbrace>pas_refined aag and invs and tcb_at t and K (is_subject aag t)\<rbrace>
reply_cancel_ipc t
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
supply empty_slot_pas_refined[wp del]
apply (rule hoare_gen_asm)
apply (simp add: reply_cancel_ipc_def)
apply (wp add: select_wp wp_transferable del: wp_not_transferable)
@ -316,12 +314,11 @@ lemma finalise_cap_pas_refined[wp]:
finalise_cap cap fin
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)
apply (cases cap, simp_all, safe)
apply (cases cap; simp only: finalise_cap.simps)
(* 12 subgoals *)
apply (wp unbind_notification_invs
| simp add: aag_cap_auth_def cap_auth_conferred_def
pas_refined_all_auth_is_owns valid_cap_simps
cap_links_irq_def pas_refined_Control[symmetric]
| elim conjE pas_refined_Control[symmetric], assumption)+
| clarsimp simp: aag_cap_auth_def cap_auth_conferred_def valid_cap_simps
cap_links_irq_def pas_refined_Control[symmetric])+
done
lemma cancel_all_signals_respects [wp]:
@ -442,13 +439,13 @@ lemma fast_finalise_respects[wp]:
K (pas_cap_cur_auth aag cap)\<rbrace>
fast_finalise cap fin
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (cases cap, simp_all)
apply (wp_trace unbind_maybe_notification_valid_objs get_simple_ko_wp
apply (cases cap; simp)
apply (wp unbind_maybe_notification_valid_objs get_simple_ko_wp
unbind_maybe_notification_respects
| wpc
| simp add: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def when_def
split: if_split_asm
| fastforce)+
| wpc
| simp add: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def when_def
split: if_split_asm
| fastforce)+
apply (clarsimp simp: obj_at_def valid_cap_def is_ntfn invs_def valid_state_def
valid_pspace_def
split: option.splits)+
@ -469,7 +466,7 @@ lemma fast_finalise_is_transferable[wp_transferable]:
"\<lbrace> P and K(is_transferable (Some cap)) \<rbrace>
fast_finalise cap final
\<lbrace>\<lambda>_. P \<rbrace>"
by (rule hoare_gen_asm) (erule is_transferable.cases;simp)
by (rule hoare_gen_asm) (erule is_transferable.cases; simp)
lemma cap_delete_one_respects_transferable[wp_transferable]:
"\<lbrace>integrity aag X st and pas_refined aag and einvs and
@ -483,12 +480,12 @@ lemma cap_delete_one_respects_transferable[wp_transferable]:
done
lemma thread_set_tcb_state_trivial:
" (\<And> tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow>
\<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (tcb_states_of_state s)\<rbrace>"
apply (simp add: thread_set_def set_object_def)
apply wp
apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD)
by (auto simp add:tcb_states_of_state_def get_tcb_def)
"(\<And> tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow>
\<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (tcb_states_of_state s)\<rbrace>"
apply (simp add: thread_set_def set_object_def)
apply wp
apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD)
by (auto simp: tcb_states_of_state_def get_tcb_def)
lemma reply_cancel_ipc_respects[wp]:
@ -502,17 +499,17 @@ lemma reply_cancel_ipc_respects[wp]:
apply (wp add: select_wp wp_transferable del:wp_not_transferable)
apply simp
apply (rule hoare_lift_Pf2[where f="cdt"])
apply (wp hoare_vcg_const_Ball_lift thread_set_integrity_autarch
thread_set_invs_trivial[OF ball_tcb_cap_casesI] thread_set_tcb_state_trivial
thread_set_not_state_valid_sched static_imp_wp thread_set_cte_wp_at_trivial
thread_set_pas_refined | simp add: ran_tcb_cap_cases)+
apply clarsimp
apply (wpsimp wp: hoare_vcg_const_Ball_lift thread_set_integrity_autarch
thread_set_invs_trivial[OF ball_tcb_cap_casesI] thread_set_tcb_state_trivial
thread_set_not_state_valid_sched static_imp_wp thread_set_cte_wp_at_trivial
thread_set_pas_refined
simp: ran_tcb_cap_cases)+
apply (rule conjI)
apply (fastforce simp:cte_wp_at_caps_of_state intro:is_transferable.intros
dest!:reply_cap_descends_from_master0)
apply (rule cdt_change_allowed_all_children[where aag=aag,
THEN all_children_descendants_of])
by force+
apply (fastforce simp: cte_wp_at_caps_of_state intro:is_transferable.intros
dest!: reply_cap_descends_from_master0)
apply (rule cdt_change_allowed_all_children
[where aag=aag, THEN all_children_descendants_of])
by fastforce+
lemma cancel_signal_respects[wp]:
"\<lbrace>integrity aag X st and K (is_subject aag t \<and>
@ -546,10 +543,10 @@ lemma suspend_respects[wp]:
"\<lbrace>integrity aag X st and pas_refined aag and einvs and tcb_at t and
K (is_subject aag t)\<rbrace>
suspend t \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: suspend_def)
apply (wp set_thread_state_integrity_autarch set_thread_state_pas_refined)
apply simp_all
done
apply (simp add: suspend_def)
apply (wp set_thread_state_integrity_autarch set_thread_state_pas_refined)
apply simp_all
done
lemma finalise_is_fast_finalise:
"can_fast_finalise cap \<Longrightarrow>
@ -608,12 +605,13 @@ lemma finalise_cap_respects[wp]:
(*NTFN Cap*)
apply ((wp unbind_maybe_notification_valid_objs get_simple_ko_wp
unbind_maybe_notification_respects
| wpc
| simp add: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def split: if_split_asm
| fastforce)+;
(clarsimp simp: obj_at_def valid_cap_def is_ntfn invs_def
valid_state_def valid_pspace_def
split: option.splits)+)
| wpc
| simp add: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def
split: if_split_asm
| fastforce)+;
clarsimp simp: obj_at_def valid_cap_def is_ntfn invs_def
valid_state_def valid_pspace_def
split: option.splits)
(* tcb cap *)
apply (wp unbind_notification_respects unbind_notification_invs
| clarsimp simp: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def
@ -833,9 +831,6 @@ next
apply auto
done
next
have replicate_helper:
"\<And>x n. True \<in> set x \<Longrightarrow> replicate n False \<noteq> x"
by (clarsimp simp: replicate_not_True)
case (3 ptr bits n slot s)
show ?case
apply (simp add: spec_validE_def)
@ -844,9 +839,6 @@ next
done
next
have nat_helper:
"\<And>x n. \<lbrakk> x < Suc n; x \<noteq> n \<rbrakk> \<Longrightarrow> x < n"
by (simp add: le_simps)
case (4 ptr bits n slot s)
show ?case
apply (rule hoare_spec_gen_asm)+
@ -947,18 +939,6 @@ lemmas rec_del_respects_CTEDelete_transferable =
(* TODO section change *)
(* FIXME these two clagged from arch, also should be crunchable *)
lemma store_pde_respects:
"\<lbrace>integrity aag X st and K (is_subject aag (p && ~~ mask pd_bits)) \<rbrace>
store_pde p pde
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: store_pde_def set_pd_def)
apply (wp get_object_wp set_object_integrity_autarch)
apply simp
done
(* FIXME: CLAG *)
lemmas dmo_valid_cap[wp] = valid_cap_typ [OF do_machine_op_obj_at]
@ -1241,11 +1221,11 @@ next
done
qed
lemma nullcap_not_pg_cap :
lemma nullcap_not_pg_cap:
"is_pg_cap NullCap \<longrightarrow> has_cancel_send_rights NullCap"
by (clarsimp simp: is_pg_cap_def)
lemma zombie_not_pg_cap :
lemma zombie_not_pg_cap:
"is_pg_cap (Zombie word x y) \<longrightarrow> has_cancel_send_rights (Zombie word x y)"
by (clarsimp simp: is_pg_cap_def)
@ -1331,7 +1311,7 @@ lemma cap_move_cte_wp_at_separation:
(* FIXME MOVE *)
lemma cap_move_empty_src_slot:
"\<lbrace> K(src \<noteq> dest) \<rbrace>
"\<lbrace> K(src \<noteq> dest) \<rbrace>
cap_move cap src dest
\<lbrace>\<lambda>_. cte_wp_at ((=) NullCap) src \<rbrace>"
apply (simp add:cap_move_def)
@ -1339,15 +1319,15 @@ lemma cap_move_empty_src_slot:
apply simp
apply (wp dxo_wp_weak set_cdt_cte_wp_at set_cap_sets_wp)+
apply simp
done
done
lemma is_derived_is_transferable:
"\<lbrakk> is_derived m slot child_cap parent_cap; is_transferable_cap parent_cap \<rbrakk> \<Longrightarrow>
is_transferable_cap child_cap"
is_transferable_cap child_cap"
apply (erule is_transferable_capE)
apply simp
apply (simp add:is_derived_def is_cap_simps)
done
done
lemma invoke_cnode_pas_refined:
"\<lbrace>pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action
@ -1362,12 +1342,13 @@ lemma invoke_cnode_pas_refined:
| wpc
| simp split del: if_split
| wp_once cap_move_cte_wp_at_separation)+
apply (cases ci, simp_all add: authorised_cnode_inv_def
cnode_inv_auth_derivations_def integrity_def)
by (clarsimp simp: cte_wp_at_caps_of_state pas_refined_refl cap_links_irq_def
real_cte_emptyable_strg
| drule auth_derived_caps_of_state_impls
| fastforce intro: cap_cur_auth_caps_of_state dest:is_derived_is_transferable)+
by (cases ci;
simp add: authorised_cnode_inv_def
cnode_inv_auth_derivations_def integrity_def;
(clarsimp simp: cte_wp_at_caps_of_state pas_refined_refl cap_links_irq_def
real_cte_emptyable_strg
| drule auth_derived_caps_of_state_impls
| fastforce intro: cap_cur_auth_caps_of_state dest: is_derived_is_transferable)+)
end

13
proof/access-control/Interrupt_AC.thy
View File

@ -11,7 +11,6 @@
theory Interrupt_AC
imports
Finalise_AC
(* cap_delete_one *)
begin
context begin interpretation Arch . (*FIXME: arch_split*)
@ -94,14 +93,14 @@ lemma invoke_irq_handler_pas_refined:
and cte_wp_at can_fast_finalise irq_slot
and not cte_wp_at is_transferable_cap slot
and K(is_subject aag (fst irq_slot))" in hoare_post_imp)
apply (force simp :cte_wp_at_caps_of_state)
apply (simp)
apply (force simp: cte_wp_at_caps_of_state)
apply simp
apply (wp get_irq_slot_different)
apply (clarsimp simp:emptyable_irq_node cte_wp_at_caps_of_state )
apply (fastforce simp:interrupt_derived_def is_cap_simps cap_master_cap_def split:cap.splits)
apply (clarsimp simp: emptyable_irq_node cte_wp_at_caps_of_state)
apply (fastforce simp: interrupt_derived_def is_cap_simps cap_master_cap_def split: cap.splits)
apply (wp delete_one_caps_of_state | simp add: get_irq_slot_def)+
apply (fastforce dest:pas_refined_is_subject_irqD)
apply (fastforce dest: pas_refined_is_subject_irqD)
done
@ -126,7 +125,7 @@ lemma invoke_irq_control_respects:
lemma integrity_irq_masks [iff]:
"integrity aag X st (s\<lparr>machine_state := machine_state s \<lparr>irq_masks := v \<rparr>\<rparr>) = integrity aag X st s"
unfolding integrity_def
by (simp )
by simp
lemma invoke_irq_handler_respects:
"\<lbrace>integrity aag X st and pas_refined aag and einvs and

458
proof/access-control/Ipc_AC.thy
View File

@ -121,18 +121,11 @@ subsection{* integrity *}
subsubsection{* autarchy *}
text{*
For the case when the currently-running thread owns the receiver
(i.e. receiver last to the notification rendezvous or sender owns
receiver).
*}
lemma st_tcb_at_tcb_states_of_state:
"(st_tcb_at stf p s) = (\<exists>st. tcb_states_of_state s p = Some st \<and> stf st)"
unfolding tcb_states_of_state_def st_tcb_def2 by auto
@ -242,8 +235,6 @@ lemma cap_auth_caps_of_state:
apply simp
done
lemma lookup_ipc_buffer_has_auth [wp]:
"\<lbrace>pas_refined aag and valid_objs\<rbrace>
lookup_ipc_buffer True receiver
@ -323,7 +314,8 @@ lemma send_upd_ctxintegrity:
apply (drule spec[where x=thread], simp)
apply (cases "is_subject aag thread")
apply (rule tro_lrefl, solves\<open>simp\<close>)
(* very slow > 1min *)
(* slow 5s *)
by (erule integrity_objE;
(* eliminate all TCB unrelated cases and simplifies the other *)
clarsimp;
@ -339,8 +331,6 @@ lemma send_upd_ctxintegrity:
(rule tro_tcb_generic'[OF refl refl refl]; simp),
rule tro_orefl, simp, rule tcb.equality; solves\<open>simp add:arch_tcb_context_set_def\<close>))
lemma set_mrs_respects_in_signalling':
"\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and
K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st
@ -373,7 +363,6 @@ lemma set_mrs_respects_in_signalling':
apply (rule send_upd_ctxintegrity[OF disjI1], auto simp: st_tcb_def2 direct_send_def)
done
lemma as_user_set_register_respects:
"\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and
K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st) \<and> (aag_has_auth_to aag SyncSend ep \<or> aag_has_auth_to aag Notify ep)) \<rbrace>
@ -452,7 +441,9 @@ lemma drop_Suc0_iff:
by (auto simp: neq_Nil_conv)
lemma receive_blocked_on_def3:
"receive_blocked_on ref ts = ((\<exists> pl. ts = Structures_A.BlockedOnReceive ref pl) \<or> ts = (Structures_A.BlockedOnNotification ref))"
"receive_blocked_on ref ts =
((\<exists>pl. ts = Structures_A.BlockedOnReceive ref pl)
\<or> ts = Structures_A.BlockedOnNotification ref)"
by (cases ts, auto)
@ -519,10 +510,11 @@ lemma cancel_ipc_receive_blocked_respects:
split: thread_state.splits)
apply (rule hoare_pre)
apply (wp set_thread_state_integrity_once_ts_upd get_object_wp get_simple_ko_wp
| wpc)+
| wpc)+
apply (clarsimp simp: st_tcb_at_def2 obj_at_def)
apply (rename_tac ep payload s tcb ntfn)
apply (drule_tac t="tcb_state tcb" in sym)
apply (subgoal_tac "st_tcb_at ((=) (tcb_state tcb)) t sa")
apply (subgoal_tac "st_tcb_at ((=) (tcb_state tcb)) t s")
apply (drule(1) sym_refs_st_tcb_atD)
apply (clarsimp simp: obj_at_def ep_q_refs_of_def fun_upd_def get_tcb_def
split: endpoint.splits cong: if_cong)
@ -532,9 +524,8 @@ lemma cancel_ipc_receive_blocked_respects:
apply (intro impI conjI allI)
apply clarsimp
apply (rule tro_ep_unblock; simp?)
apply (erule get_tcb_recv_blocked_implies_receive, erule get_tcb_rev; solves\<open>simp\<close>)
apply (rename_tac word pl careful tcb your dogs finaly one)
apply (rule_tac recv=word in tro_tcb_send;
apply (erule get_tcb_recv_blocked_implies_receive, erule get_tcb_rev; solves\<open>simp\<close>)
apply (rule_tac ep=ep in tro_tcb_send[OF refl refl];
fastforce intro!: tcb.equality arch_tcb_context_set_eq[symmetric]
simp: indirect_send_def pred_tcb_at_def obj_at_def)
apply (fastforce simp: indirect_send_def pred_tcb_at_def obj_at_def)
@ -588,7 +579,8 @@ lemma tsos_tro':
apply (drule_tac x=p in spec)
apply (erule integrity_objE;
simp?;
fastforce simp add: thread_bound_ntfns_def get_tcb_def tcb_bound_notification_reset_integrity_def)
fastforce simp: thread_bound_ntfns_def get_tcb_def
tcb_bound_notification_reset_integrity_def)
done
lemma integrity_receive_blocked_chain_bound:
@ -639,10 +631,10 @@ lemma send_signal_respects:
apply (rule hoare_pre)
apply clarsimp
apply (wpc, clarsimp)
apply (wp set_notification_respects[where auth=Notify] sts_st_tcb_at' as_user_set_register_respects
apply (wp set_notification_respects[where auth=Notify]
sts_st_tcb_at' as_user_set_register_respects
set_thread_state_pas_refined set_simple_ko_pas_refined
set_thread_state_respects_in_signalling [where ntfnptr = ntfnptr]
set_notification_respects[where auth=Send]
set_ntfn_valid_objs_at hoare_vcg_disj_lift static_imp_wp
| wpc
| simp add: update_waiting_ntfn_def)+
@ -919,6 +911,7 @@ lemma derive_cap_is_derived_foo':
apply simp
done
(* FIXME: cleanup *)
lemma transfer_caps_loop_presM_extended:
fixes P vo em ex buffer slots caps n mi
assumes x: "\<And>cap src dest.
@ -955,19 +948,19 @@ lemma transfer_caps_loop_presM_extended:
| assumption | simp split del: if_split)+
apply (rule cap_insert_assume_null)
apply (wp x hoare_vcg_const_Ball_lift cap_insert_cte_wp_at static_imp_wp)+
apply (rule hoare_vcg_conj_liftE_R)
apply (rule derive_cap_is_derived_foo')
apply (rule_tac Q' ="\<lambda>cap' s. (vo \<longrightarrow> cap'\<noteq> cap.NullCap \<longrightarrow>
cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s)
\<and> (cap'\<noteq> cap.NullCap \<longrightarrow> QM s cap')" for QM
in hoare_post_imp_R)
prefer 2
apply clarsimp
apply assumption
apply (rule hoare_vcg_conj_liftE_R)
apply (rule hoare_vcg_const_imp_lift_R)
apply (rule derive_cap_is_derived)
apply (wp derive_cap_is_derived_foo')+
apply (rule hoare_vcg_conj_liftE_R)
apply (rule derive_cap_is_derived_foo')
apply (rule_tac Q' ="\<lambda>cap' s. (vo \<longrightarrow> cap'\<noteq> cap.NullCap \<longrightarrow>
cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s)
\<and> (cap'\<noteq> cap.NullCap \<longrightarrow> QM s cap')" for QM
in hoare_post_imp_R)
prefer 2
apply clarsimp
apply assumption
apply (rule hoare_vcg_conj_liftE_R)
apply (rule hoare_vcg_const_imp_lift_R)
apply (rule derive_cap_is_derived)
apply (wp derive_cap_is_derived_foo')+
apply (clarsimp simp: cte_wp_at_caps_of_state
ex_cte_cap_to_cnode_always_appropriate_strg
real_cte_tcb_valid caps_of_state_valid
@ -975,12 +968,12 @@ lemma transfer_caps_loop_presM_extended:
apply (clarsimp simp: remove_rights_def caps_of_state_valid
neq_Nil_conv cte_wp_at_caps_of_state
imp_conjR[symmetric] conj_comms
split del: if_split)
apply (intro conjI)
split del: if_split)
apply (rule conjI)
apply clarsimp
apply (case_tac "cap = a",clarsimp)
apply (clarsimp simp:masked_as_full_def is_cap_simps)
apply (fastforce simp: cap_master_cap_simps split:if_splits)
apply (fastforce simp: cap_master_cap_simps split: if_splits)
apply (clarsimp split del: if_split)
apply (intro conjI)
apply (fastforce split: if_split elim!: pcap_auth_derived)
@ -992,7 +985,7 @@ lemma transfer_caps_loop_presM_extended:
apply (intro conjI)
apply (case_tac "capa = ac",clarsimp+)
apply (case_tac "capa = ac")
by (clarsimp simp:masked_as_full_def is_cap_simps split:if_splits)+
by (clarsimp simp: masked_as_full_def is_cap_simps split: if_splits)+
lemma transfer_caps_loop_pas_refined:
"\<lbrace>pas_refined aag and valid_objs and valid_mdb
@ -1012,13 +1005,11 @@ lemma transfer_caps_loop_pas_refined:
Pcap="pas_cap_cur_auth aag" and
Pdest="\<lambda>slot . is_subject aag (fst slot)"])
apply (wp cap_insert_pas_refined)
apply (fastforce simp:cte_wp_at_caps_of_state elim!:is_derived_is_transferable)
apply (fastforce simp: cte_wp_at_caps_of_state elim!: is_derived_is_transferable)
apply (rule set_extra_badge_pas_refined)
apply (erule(1) auth_derived_pas_cur_auth)
apply (fastforce elim:cte_wp_at_weakenE)
done
lemma ball_conj: "\<forall>x \<in> S . P \<and> Q \<longleftrightarrow> (\<forall>x \<in> S. P) \<and> (\<forall>x \<in> S . Q)" by blast
apply (fastforce elim: cte_wp_at_weakenE)
done
lemma transfer_caps_pas_refined:
@ -1033,7 +1024,7 @@ lemma transfer_caps_pas_refined:
apply (rule hoare_pre)
by (wp transfer_caps_loop_pas_refined get_receive_slots_authorised get_recv_slot_inv
hoare_vcg_const_imp_lift hoare_vcg_all_lift grs_distinct
| wpc | simp del: get_receive_slots.simps add:ball_conj_distrib)+
| wpc | simp del: get_receive_slots.simps add: ball_conj_distrib)+
@ -1097,6 +1088,7 @@ lemma lec_valid_cap':
unfolding lookup_extra_caps_def
by (wpsimp wp: mapME_set lcs_valid')
(* FIXME: MOVE *)
lemma hoare_conjDR1:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
by (simp add:validE_def validE_R_def valid_def) blast
@ -1201,6 +1193,7 @@ lemma setup_caller_cap_pas_refined:
cap_auth_conferred_def reply_cap_rights_to_auth_def
intro: aag_wellformed_delete_derived[OF _ pas_refined_wellformed])
(* FIXME: MOVE *)
lemma sym_ref_endpoint_recvD:
assumes sym: "sym_refs (state_refs_of s)"
and ep: "ko_at (Endpoint (RecvEP l)) epptr s"
@ -1231,7 +1224,7 @@ lemma pas_refined_ep_recv:
apply (rule pas_refined_mem[OF _ policy])
apply (rule sta_ts[of epptr Receive])
apply (simp add:thread_states_def)
done
done
lemma send_ipc_valid_ep_helper:
"\<lbrakk>invs s ; ko_at (Endpoint (RecvEP (h # t))) epptr s \<rbrakk> \<Longrightarrow>
@ -1239,18 +1232,18 @@ lemma send_ipc_valid_ep_helper:
apply (drule invs_valid_objs)
apply (drule ko_atD)
apply (erule(1) valid_objsE)
by (cases t; simp add:valid_obj_def valid_ep_def)
by (cases t; simp add: valid_obj_def valid_ep_def)
lemmas head_in_set = list.set_intros(1)[of h t for h t]
lemma send_ipc_pas_refined:
"\<lbrace>pas_refined aag
and invs
and K (is_subject aag thread
\<and> aag_has_auth_to aag SyncSend epptr \<and>
(can_grant_reply \<longrightarrow> aag_has_auth_to aag Call epptr) \<and>
(can_grant \<longrightarrow> aag_has_auth_to aag Grant epptr \<and> aag_has_auth_to aag Call epptr))\<rbrace>
and invs
and K (is_subject aag thread
\<and> aag_has_auth_to aag SyncSend epptr
\<and> (can_grant_reply \<longrightarrow> aag_has_auth_to aag Call epptr)
\<and> (can_grant \<longrightarrow> aag_has_auth_to aag Grant epptr \<and> aag_has_auth_to aag Call epptr))\<rbrace>
send_ipc block call badge can_grant can_grant_reply thread epptr
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)
@ -1288,12 +1281,12 @@ lemma send_ipc_pas_refined:
clarsimp simp:st_tcb_at_tcb_states_of_state_eq)
apply (fastforce elim: send_ipc_valid_ep_helper
simp: aag_has_auth_to_Control_eq_owns
dest:
aag_wellformed_grant_Control_to_recv_by_reply[OF _ _ _ pas_refined_wellformed])
dest: aag_wellformed_grant_Control_to_recv_by_reply
[OF _ _ _ pas_refined_wellformed])
done
subgoal (* not can_grant_reply and not can_grant*)
by (force elim: send_ipc_valid_ep_helper)
done
done
done
lemma set_simple_ko_get_tcb:
@ -1341,7 +1334,6 @@ where
\<equiv> receive_ipc_base2 thread is_blocking epptr rights ep"
lemma sym_ref_endpoint_sendD:
assumes sym: "sym_refs (state_refs_of s)"
and ep: "ko_at (Endpoint (SendEP l)) epptr s"
@ -1361,20 +1353,20 @@ proof -
qed
lemma receive_ipc_valid_ep_helper:
"\<lbrakk> invs s; ko_at (Endpoint (SendEP list)) epptr s \<rbrakk> \<Longrightarrow>
valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl list)) s"
apply (drule_tac invs_valid_objs)
apply (drule ko_atD)
apply (erule(1) valid_objsE)
apply (cases list, solves \<open>simp add:valid_obj_def valid_ep_def\<close>)
by (cases "tl list" ;clarsimp simp add:valid_obj_def valid_ep_def)
"\<lbrakk> invs s; ko_at (Endpoint (SendEP list)) epptr s \<rbrakk> \<Longrightarrow>
valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl list)) s"
apply (drule_tac invs_valid_objs)
apply (drule ko_atD)
apply (erule(1) valid_objsE)
apply (cases list, solves \<open>simp add: valid_obj_def valid_ep_def\<close>)
by (cases "tl list"; clarsimp simp:valid_obj_def valid_ep_def)
lemma receive_ipc_sender_helper:
"\<lbrakk>pas_refined aag s ; kheap s thread = Some (TCB tcb) ; tcb_state tcb = BlockedOnSend ep pl\<rbrakk>
\<Longrightarrow> (pasObjectAbs aag thread, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag"
apply (erule pas_refined_mem[rotated])
apply (rule sta_ts)
apply (simp add:thread_states_def tcb_states_of_state_def get_tcb_def)
apply (simp add: thread_states_def tcb_states_of_state_def get_tcb_def)
done
lemma receive_ipc_sender_can_grant_helper:
@ -1397,6 +1389,7 @@ lemma receive_ipc_base_pas_refined:
(\<forall> auth \<in> cap_rights_to_auth rights True . aag_has_auth_to aag auth epptr))\<rbrace>
receive_ipc_base aag thread ep epptr rights is_blocking
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
(* FIXME: proof structure *)
apply (rule hoare_gen_asm)
apply (clarsimp simp: thread_get_def cong: endpoint.case_cong)
apply (rule hoare_pre)
@ -1489,7 +1482,7 @@ lemma receive_ipc_pas_refined:
(* old receive_ipc stuff *)
apply (rule hoare_pre)
apply (wp receive_ipc_base_pas_refined)[1]
apply (fastforce simp:aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)
apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)
(* ntfn-binding case *)
apply clarsimp
apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
@ -1497,7 +1490,7 @@ lemma receive_ipc_pas_refined:
apply (wp complete_signal_pas_refined, clarsimp)
(* regular case again *)
apply (rule hoare_pre, wp receive_ipc_base_pas_refined)
apply (fastforce simp:aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)
apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)
done
@ -1691,11 +1684,11 @@ lemma set_untyped_cap_as_full_not_untyped:
"\<lbrace> P and K(\<not> is_untyped_cap cap') \<rbrace>
set_untyped_cap_as_full cap cap' slot
\<lbrace> \<lambda>rv. P\<rbrace>"
unfolding set_untyped_cap_as_full_def
apply wp
apply (rule hoare_pre_cont)
unfolding set_untyped_cap_as_full_def
apply wp
apply (rule hoare_pre_cont)
apply wpsimp+
done
done
lemma cap_insert_integrity_autarch_not_untyped:
@ -1734,8 +1727,6 @@ lemma set_thread_state_blocked_on_reply_respects:
apply (rule tro_tcb_receive[where new_st=BlockedOnReply])
by fastforce+
lemma setup_caller_cap_integrity_recv:
"\<lbrace>integrity aag X st and valid_mdb
and st_tcb_at (send_blocked_on ep) sender and
@ -1763,12 +1754,12 @@ where
lemma receive_ipc_base_integrity:
notes do_nbrecv_failed_transfer_def[simp]
shows "\<lbrace>pas_refined aag and integrity aag X st and invs
and ko_at (Endpoint ep) epptr
and K (is_subject aag receiver
\<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag
\<and> (\<forall>auth \<in> cap_rights_to_auth rights True. aag_has_auth_to aag auth epptr))\<rbrace>
receive_ipc_base aag receiver ep epptr rights is_blocking
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
and ko_at (Endpoint ep) epptr
and K (is_subject aag receiver
\<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag
\<and> (\<forall>auth \<in> cap_rights_to_auth rights True. aag_has_auth_to aag auth epptr))\<rbrace>
receive_ipc_base aag receiver ep epptr rights is_blocking
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (clarsimp simp: thread_get_def get_thread_state_def cong: endpoint.case_cong)
apply (rule hoare_pre)
@ -1779,16 +1770,16 @@ lemma receive_ipc_base_integrity:
sts_receive_Inactive_respects[where ep = epptr]
as_user_integrity_autarch
| wpc | simp)+
apply (rename_tac list tcb data)
apply (rule_tac Q="\<lambda>rv s. integrity aag X st s
\<and> valid_mdb s
\<and> is_subject aag receiver
\<and> (sender_can_call data \<longrightarrow> AllowGrant \<in> rights
\<longrightarrow> is_subject aag (hd list))
\<and> (sender_can_grant data \<longrightarrow> is_subject aag (hd list))
\<and> st_tcb_at (send_blocked_on epptr) (hd list) s
\<and> st_tcb_at (\<lambda>st. st = BlockedOnSend epptr data) (hd list) s"
in hoare_strengthen_post[rotated])
apply (rename_tac list tcb data)
apply (rule_tac Q="\<lambda>rv s. integrity aag X st s
\<and> valid_mdb s
\<and> is_subject aag receiver
\<and> (sender_can_call data \<longrightarrow> AllowGrant \<in> rights
\<longrightarrow> is_subject aag (hd list))
\<and> (sender_can_grant data \<longrightarrow> is_subject aag (hd list))
\<and> st_tcb_at (send_blocked_on epptr) (hd list) s
\<and> st_tcb_at (\<lambda>st. st = BlockedOnSend epptr data) (hd list) s"
in hoare_strengthen_post[rotated])
apply (fastforce simp: st_tcb_at_def obj_at_def get_tcb_rev call_blocked_def
allowed_call_blocked_def
dest!: get_tcb_SomeD
@ -1809,12 +1800,13 @@ lemma receive_ipc_base_integrity:
\<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))")
apply (clarsimp simp: st_tcb_def2 a_type_def)
apply (frule_tac t="hd x" in sym_ref_endpoint_sendD[OF invs_sym_refs],assumption,force)
apply (clarsimp simp:get_tcb_def elim!: pred_tcb_atE)
apply (intro conjI;(force elim:receive_ipc_valid_ep_helper receive_ipc_sender_can_grant_helper)?)
apply (clarsimp simp: get_tcb_def elim!: pred_tcb_atE)
apply (intro conjI;
(force elim: receive_ipc_valid_ep_helper receive_ipc_sender_can_grant_helper)?)
apply (intro impI)
apply (frule_tac x= "hd x" in pas_refined_mem[rotated,where auth=Call])
apply (rule sta_ts)
apply (simp add:thread_states_def tcb_states_of_state_def get_tcb_def)
apply (simp add: thread_states_def tcb_states_of_state_def get_tcb_def)
apply (simp add: cap_rights_to_auth_def)
apply (rule aag_has_auth_to_Control_eq_owns[THEN iffD1],assumption)
apply (erule aag_wellformed_grant_Control_to_send_by_reply[OF _ _ _ pas_refined_wellformed];force)
@ -1841,7 +1833,7 @@ lemma receive_ipc_integrity_autarch:
apply (rule hoare_pre, wp complete_signal_integrity, clarsimp)
(* old receive case, bound ntfn not active *)
apply (rule hoare_pre, wp receive_ipc_base_integrity)
apply (fastforce simp:aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)
apply (fastforce simp:aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)
done
subsubsection{* Non-autarchy: the sender is running *}
@ -1973,9 +1965,9 @@ lemma integrity_tcb_in_ipc_final:
apply (rule trm_ipc [where p' = thread])
apply (simp add: tcb_states_of_state_def get_tcb_def split:thread_state.splits)
apply (simp add: tcb_states_of_state_def get_tcb_def)
apply (simp add: auth_ipc_buffers_def get_tcb_def
split: option.split_asm cap.split_asm arch_cap.split_asm if_split_asm split del: if_split)
apply simp
apply (simp add: auth_ipc_buffers_def get_tcb_def
split: option.split_asm cap.split_asm arch_cap.split_asm if_split_asm split del: if_split)
apply simp
done
lemma update_tcb_context_in_ipc:
@ -2006,7 +1998,7 @@ lemma update_tcb_state_in_ipc:
unfolding integrity_tcb_in_ipc_def
apply (elim conjE)
apply (intro conjI)
apply assumption+
apply assumption+
apply (erule integrity_trans)
apply (simp cong: if_cong)
apply clarsimp
@ -2019,8 +2011,6 @@ lemma update_tcb_state_in_ipc:
apply fastforce
done
(*subsection{* integrity *}*)
lemma as_user_respects_in_ipc:
"\<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>
as_user thread m
@ -2040,7 +2030,6 @@ lemma set_message_info_respects_in_ipc:
unfolding set_message_info_def
by (wp as_user_respects_in_ipc)
lemma mul_add_word_size_lt_msg_align_bits_ofnat:
"\<lbrakk> p < 2 ^ (msg_align_bits - 2); k < 4 \<rbrakk>
\<Longrightarrow> of_nat p * of_nat word_size + k < (2 :: word32) ^ msg_align_bits"
@ -2444,7 +2433,7 @@ lemma ep_queued_st_tcb_at'':
apply (frule (1) sym_refs_ko_atD, fastforce simp: st_tcb_at_def obj_at_def refs_of_rev)+
done
(* REPLY STUFF *)
subsubsection \<open>Inserting the reply cap\<close>
lemma integrity_tcb_in_ipc_no_call:
"integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st s
@ -2471,36 +2460,36 @@ lemma cap_insert_ext_integrity_in_ipc_reply:
and K(is_subject aag (fst src_slot)
\<and> st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st)\<rbrace>
cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
apply (rule hoare_gen_asm)+
apply (simp add: integrity_tcb_in_ipc_def split del: if_split)
apply (unfold integrity_def)
apply (simp only: integrity_cdt_list_as_list_integ)
apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def
tcb_states_of_state_def get_tcb_def
split del: if_split cong: if_cong)
apply wp
apply (simp add: list_integ_def del: split_paired_All)
apply (fold list_integ_def get_tcb_def tcb_states_of_state_def)
apply (wp cap_insert_list_integrity)
apply simp
apply (simp add: list_integ_def del: split_paired_All)
apply (fold list_integ_def get_tcb_def tcb_states_of_state_def)
apply (clarsimp simp:st_tcb_at_tcb_states_of_state)
apply (rule cca_reply;force)
apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def
tcb_states_of_state_def get_tcb_def
split del: if_split cong: if_cong)
apply wp
apply (simp add: list_integ_def del: split_paired_All)
apply (fold list_integ_def get_tcb_def tcb_states_of_state_def)
apply (wp cap_insert_list_integrity)
apply simp
apply (simp add: list_integ_def del: split_paired_All)
apply (fold list_integ_def get_tcb_def tcb_states_of_state_def)
apply (clarsimp simp: st_tcb_at_tcb_states_of_state)
apply (rule cca_reply; force)
done
lemma update_cdt_wp:
"\<lbrace>\<lambda>s. P (s\<lparr> cdt := f (cdt s) \<rparr>)\<rbrace>
update_cdt f
\<lbrace>\<lambda>_. P \<rbrace>"
by (wpsimp simp: update_cdt_def set_cdt_def)
by (wpsimp simp: update_cdt_def set_cdt_def)
lemma update_cdt_reply_in_ipc:
"\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st
and K(st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st)\<rbrace>
update_cdt (\<lambda>cdt. cdt ((receiver, tcb_cnode_index 3) := val cdt))
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
update_cdt (\<lambda>cdt. cdt ((receiver, tcb_cnode_index 3) := val cdt))
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
apply (wp update_cdt_wp)
apply (clarsimp simp: integrity_tcb_in_ipc_def)
apply (simp add: integrity_def tcb_states_of_state_def get_tcb_def
@ -2513,11 +2502,12 @@ lemma update_cdt_reply_in_ipc:
lemma spec_valid_direct:
"( P s \<Longrightarrow> s \<turnstile> \<lbrace> \<top> \<rbrace> f \<lbrace> Q \<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace> Q \<rbrace>"
by (simp add:spec_valid_def valid_def)
by (simp add: spec_valid_def valid_def)
lemma set_cap_respects_in_ipc_reply:
"\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st
and K(st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st \<and> is_subject aag caller)\<rbrace>
and K(st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st
\<and> is_subject aag caller)\<rbrace>
set_cap (ReplyCap caller False R) (receiver, tcb_cnode_index 3)
\<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>"
unfolding set_cap_def
@ -2542,7 +2532,7 @@ lemma cap_insert_reply_cap_respects_in_ipc:
cap_insert
(ReplyCap caller False R)
master_slot (receiver, tcb_cnode_index 3)
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>"
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>"
unfolding cap_insert_def
apply (rule hoare_pre)
apply (wp add:set_original_respects_in_ipc_reply)
@ -2558,18 +2548,22 @@ lemma set_scheduler_action_respects_in_ipc_autarch:
unfolding set_scheduler_action_def
by (wpsimp simp: integrity_tcb_in_ipc_def integrity_def tcb_states_of_state_def get_tcb_def)
lemma exists_cons_append:
"\<exists>xs. xs @ ys = zs \<Longrightarrow> \<exists>xs. xs @ ys = z # zs"
by auto
lemma tcb_sched_action_respects_in_ipc_autarch:
"\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>
tcb_sched_action tcb_sched_enqueue target
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
apply (simp add: tcb_sched_action_def)
apply wp
apply (clarsimp simp: integrity_def integrity_tcb_in_ipc_def tcb_states_of_state_def get_tcb_def integrity_ready_queues_def pas_refined_def tcb_domain_map_wellformed_aux_def tcb_at_def get_etcb_def tcb_sched_enqueue_def etcb_at_def
split: option.splits)
apply (fold get_tcb_def tcb_states_of_state_def)
apply (thin_tac "tcb_in_ipc _ _ _ _ _ _")
apply (thin_tac "\<forall> x \<in> _ . _ x ")
by (metis append.simps(2)) (* it says append.simps is unused, but refuses to prove the goal without. it also take 30 sec *)
apply (clarsimp simp: integrity_def integrity_tcb_in_ipc_def tcb_states_of_state_def get_tcb_def
integrity_ready_queues_def pas_refined_def tcb_domain_map_wellformed_aux_def
tcb_at_def get_etcb_def tcb_sched_enqueue_def etcb_at_def
split: option.splits)
apply (fastforce intro: exists_cons_append)
done
crunches possible_switch_to, set_thread_state for respects_in_ipc_autarch: "integrity_tcb_in_ipc aag X receiver epptr ctxt st"
@ -2584,8 +2578,6 @@ lemma setup_caller_cap_respects_in_ipc_reply:
by (wpsimp wp: cap_insert_reply_cap_respects_in_ipc set_thread_state_respects_in_ipc_autarch)
lemma send_ipc_integrity_autarch:
"\<lbrace>integrity aag X st and pas_refined aag
and invs
@ -2648,14 +2640,14 @@ lemma send_ipc_integrity_autarch:
| wp hoare_drop_imps
| simp add:get_thread_state_def)+
apply (clarsimp intro:integrity_tcb_in_ipc_refl)
apply (frule_tac t=x in sym_ref_endpoint_recvD[OF invs_sym_refs],assumption,simp)
apply (clarsimp simp:st_tcb_at_tcb_states_of_state_eq st_tcb_at_tcb_states_of_state direct_call_def)
apply (subgoal_tac "\<not> can_grant")
apply (force intro!: integrity_tcb_in_ipc_refl
simp: st_tcb_at_tcb_states_of_state
elim: send_ipc_valid_ep_helper)
apply (force elim:obj_at_ko_atE)
apply (clarsimp intro:integrity_tcb_in_ipc_refl)
apply (frule_tac t=x in sym_ref_endpoint_recvD[OF invs_sym_refs],assumption,simp)
apply (clarsimp simp:st_tcb_at_tcb_states_of_state_eq st_tcb_at_tcb_states_of_state direct_call_def)
apply (subgoal_tac "\<not> can_grant")
apply (force intro!: integrity_tcb_in_ipc_refl
simp: st_tcb_at_tcb_states_of_state
elim: send_ipc_valid_ep_helper)
apply (force elim:obj_at_ko_atE)
done
section{* Faults *}
@ -2711,17 +2703,17 @@ lemma send_fault_ipc_pas_refined:
| wpc
| rule hoare_drop_imps
| simp add: split_def split del: if_split)+
apply (rule_tac Q'="\<lambda>rv s. pas_refined aag s
\<and> is_subject aag (cur_thread s)
\<and> invs s
\<and> valid_fault fault
\<and> is_subject aag (fst (fst rv))"
in hoare_post_imp_R[rotated])
apply (fastforce dest!: cap_auth_caps_of_state
simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state aag_cap_auth_def
cap_auth_conferred_def cap_rights_to_auth_def AllowSend_def)
apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised
| simp add: lookup_cap_def split_def)+
apply (rule_tac Q'="\<lambda>rv s. pas_refined aag s
\<and> is_subject aag (cur_thread s)
\<and> invs s
\<and> valid_fault fault
\<and> is_subject aag (fst (fst rv))"
in hoare_post_imp_R[rotated])
apply (fastforce dest!: cap_auth_caps_of_state
simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state aag_cap_auth_def
cap_auth_conferred_def cap_rights_to_auth_def AllowSend_def)
apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised
| simp add: lookup_cap_def split_def)+
done
lemma handle_fault_pas_refined:
@ -2734,7 +2726,7 @@ lemma handle_fault_pas_refined:
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: handle_fault_def)
apply (wp set_thread_state_pas_refined send_fault_ipc_pas_refined
| simp add: handle_double_fault_def)+
| simp add: handle_double_fault_def)+
done
@ -2749,6 +2741,11 @@ lemma thread_set_tcb_fault_update_valid_mdb:
done
(* FIXME: MOVE *)
lemma obj_at_conj_distrib:
"obj_at (\<lambda>ko. P ko \<and> Q ko) p s = (obj_at (\<lambda>ko. P ko) p s \<and> obj_at (\<lambda>ko. Q ko) p s)"
by (auto simp: obj_at_def)
lemma send_fault_ipc_integrity_autarch:
"\<lbrace>pas_refined aag
and invs
@ -2764,18 +2761,16 @@ lemma send_fault_ipc_integrity_autarch:
thread_set_integrity_autarch thread_set_fault_pas_refined
thread_set_valid_objs'' thread_set_refs_trivial
thread_set_tcb_fault_update_valid_mdb
| wpc
| simp add: is_obj_defs)+
thread_set_tcb_fault_set_invs
| wpc
| simp add: is_obj_defs)+
(* 14 subgoals *)
apply (rename_tac word1 word2 set)
apply (rule_tac Q="\<lambda>rv s. obj_at (\<lambda>ep. is_ep ep \<and> (AllowGrant \<in> set \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)))) word1 s
\<and> is_subject aag (cur_thread s) \<and> invs s
\<and> aag_has_auth_to aag SyncSend word1 \<and> aag_has_auth_to aag Call word1"
in hoare_strengthen_post[rotated])
apply (fastforce simp: obj_at_def)
apply (rule_tac R="\<lambda>rv s. ep_at word1 s" in hoare_post_add)
apply (simp only: obj_at_conj_distrib[symmetric] flip: conj_assoc)
apply (wp thread_set_obj_at_impossible thread_set_tcb_fault_set_invs
get_cap_auth_wp[where aag=aag]
| simp add: lookup_cap_def is_obj_defs split_def)+
| simp add: lookup_cap_def is_obj_defs split_def)+
(* down to 3 : normal indentation *)
apply (rule_tac Q'="\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s
\<and> invs s
@ -2855,8 +2850,10 @@ lemma do_reply_transfer_pas_refined:
lemma update_tcb_state_in_ipc_reply:
"\<lbrakk> integrity_tcb_in_ipc aag X thread epptr TRContext st s;
tcb_state tcb = BlockedOnReply; aag_has_auth_to aag Reply thread; tcb_fault tcb = None;
get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Structures_A.thread_state.Running\<rparr> \<rbrakk>
\<Longrightarrow> integrity_tcb_in_ipc aag X thread epptr TRFinal st (s \<lparr> kheap := (kheap s)(thread \<mapsto> TCB tcb') \<rparr>)"
get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Structures_A.thread_state.Running\<rparr>
\<rbrakk> \<Longrightarrow>
integrity_tcb_in_ipc aag X thread epptr TRFinal st
(s \<lparr> kheap := (kheap s)(thread \<mapsto> TCB tcb') \<rparr>)"
unfolding integrity_tcb_in_ipc_def
apply (elim conjE)
apply (intro conjI)
@ -2865,12 +2862,10 @@ lemma update_tcb_state_in_ipc_reply:
apply (simp cong: if_cong)
apply clarsimp
apply (erule tcb_in_ipc.cases, simp_all)
apply (drule get_tcb_SomeD)
apply (rule tii_reply[OF refl refl])
apply (elim exE, intro exI tcb.equality;solves \<open>simp\<close>)
apply fastforce
apply fastforce
apply (auto intro!: tii_reply[OF refl refl] tii_lrefl[OF refl] dest!: get_tcb_SomeD)
apply (drule get_tcb_SomeD)
apply (rule tii_reply[OF refl refl])
apply (elim exE, intro exI tcb.equality; solves \<open>simp\<close>)
apply auto
done
@ -2886,7 +2881,8 @@ lemma fault_tcb_atE:
using hyp by (fastforce simp:pred_tcb_at_def elim: obj_atE)
lemma set_thread_state_running_respects_in_ipc_reply:
"\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and st_tcb_at awaiting_reply receiver
"\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st
and st_tcb_at awaiting_reply receiver
and fault_tcb_at ((=) None) receiver
and K (aag_has_auth_to aag Reply receiver)\<rbrace>
set_thread_state receiver Structures_A.thread_state.Running
@ -2898,9 +2894,6 @@ lemma set_thread_state_running_respects_in_ipc_reply:
elim!: fault_tcb_atE elim: update_tcb_state_in_ipc_reply[unfolded fun_upd_def])
done
end
context is_extended begin
@ -2936,13 +2929,6 @@ lemma fast_finalise_reply_respects_in_ipc_autarch:
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>"
by (rule hoare_gen_asm) (fastforce simp: is_cap_simps)
(*lemma empty_slot_ext_in_ipc_autarch:
"\<lbrace> integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>
empty_slot_ext slot slot_p
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>"
unfolding empty_slot_def apply simp
apply (wp add: set_cap_respects_in_ipc_autarch set_original_respects_in_ipc_autarch)*)
lemma empty_slot_list_integrity':
notes split_paired_All[simp del]
shows
@ -2953,7 +2939,6 @@ lemma empty_slot_list_integrity':
done
lemma tcb_state_of_states_cdt_update_behind_kheap[simp]:
"tcb_states_of_state (kheap_update g (cdt_update f s)) = tcb_states_of_state (kheap_update g s)"
by (simp add:tcb_states_of_state_def get_tcb_def)
@ -2963,11 +2948,11 @@ lemma set_cdt_empty_slot_respects_in_ipc_autarch:
and (\<lambda>s. descendants_of slot m = {}) and K(is_subject aag (fst slot))\<rbrace>
set_cdt ((\<lambda>p. if m p = Some slot then m slot else m p)(slot := None))
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>"
unfolding set_cdt_def
apply (wp)
apply (simp add: integrity_tcb_in_ipc_def integrity_def)
apply (force simp:no_children_empty_desc[symmetric])
done
unfolding set_cdt_def
apply wp
apply (simp add: integrity_tcb_in_ipc_def integrity_def)
apply (force simp:no_children_empty_desc[symmetric])
done
lemma reply_cap_no_children':
"\<lbrakk> valid_mdb s; caps_of_state s p = Some (ReplyCap t False r) \<rbrakk> \<Longrightarrow> \<forall>p' .cdt s p' \<noteq> Some p"
@ -2981,46 +2966,44 @@ lemma valid_list_empty:
by (fastforce simp del:split_paired_All split_paired_Ex simp add:neq_Nil_conv)
lemma empty_slot_respects_in_ipc_autarch:
"\<lbrace> integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot))\<rbrace>
"\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list
and cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot))\<rbrace>
empty_slot slot NullCap
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>"
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
unfolding empty_slot_def apply simp
apply (wp add: set_cap_respects_in_ipc_autarch set_original_respects_in_ipc_autarch)
apply (wp empty_slot_extended.list_integ_lift_in_ipc empty_slot_list_integrity')
apply (simp)
apply wp+
apply (wp set_cdt_empty_slot_respects_in_ipc_autarch)
apply (simp add:set_cdt_def)
apply (wp)
apply (wp)
apply (wp)
apply (wp add: set_cap_respects_in_ipc_autarch set_original_respects_in_ipc_autarch)
apply (wp empty_slot_extended.list_integ_lift_in_ipc empty_slot_list_integrity')
apply simp
apply wp+
apply (wp set_cdt_empty_slot_respects_in_ipc_autarch)
apply (simp add: set_cdt_def)
apply wp
apply wp
apply wp
apply (wp get_cap_wp)
apply (clarsimp simp:integrity_tcb_in_ipc_def cte_wp_at_caps_of_state is_cap_simps)
apply (drule(1) reply_cap_no_children')
by (force dest:valid_list_empty simp:no_children_empty_desc simp del:split_paired_All)
apply (clarsimp simp: integrity_tcb_in_ipc_def cte_wp_at_caps_of_state is_cap_simps)
apply (drule(1) reply_cap_no_children')
by (force dest: valid_list_empty simp: no_children_empty_desc simp del: split_paired_All)
lemma cte_delete_one_respects_in_ipc_autharch:
"\<lbrace> integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and
cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot)) \<rbrace>
"\<lbrace> integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and
cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot)) \<rbrace>
cap_delete_one slot
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>"
unfolding cap_delete_one_def
apply (wp empty_slot_respects_in_ipc_autarch fast_finalise_reply_respects_in_ipc_autarch get_cap_wp)
by (fastforce simp:cte_wp_at_caps_of_state is_cap_simps)
unfolding cap_delete_one_def
apply (wp empty_slot_respects_in_ipc_autarch
fast_finalise_reply_respects_in_ipc_autarch get_cap_wp)
by (fastforce simp:cte_wp_at_caps_of_state is_cap_simps)
text {* The special case of fault reply need a different machinery than *_in_ipc stuff because,
there is non @{term underlying_memory} modification *}
there is no @{term underlying_memory} modification *}
datatype tcb_respects_fault_state = TRFContext | TRFRemoveFault | TRFFinal
inductive
tcb_in_fault_reply for aag tst l' ko ko'
inductive tcb_in_fault_reply for aag tst l' ko ko'
where
tifr_lrefl: "\<lbrakk> l' = pasSubject aag \<rbrakk> \<Longrightarrow> tcb_in_fault_reply aag tst l' ko ko'"
| tifr_context: "\<lbrakk> ko = Some (TCB tcb);
@ -3069,14 +3052,15 @@ lemma integrity_tcb_in_fault_reply_final:
apply (clarsimp simp: integrity_def)
apply (erule tcb_in_fault_reply.cases; clarsimp)
apply (fastforce intro!:tcb.equality tro_tcb_reply)
done
done
lemma set_scheduler_action_respects_in_fault_reply:
"\<lbrace>integrity_tcb_in_fault_reply aag X receiver ctxt st\<rbrace>
set_scheduler_action action
\<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X receiver ctxt st\<rbrace>"
unfolding set_scheduler_action_def
by (wpsimp simp: integrity_tcb_in_fault_reply_def integrity_def tcb_states_of_state_def get_tcb_def)
unfolding set_scheduler_action_def
by (wpsimp simp: integrity_tcb_in_fault_reply_def integrity_def
tcb_states_of_state_def get_tcb_def)
crunches set_thread_state_ext
for respects_in_fault_reply:"integrity_tcb_in_fault_reply aag X receiver ctxt st"
@ -3090,18 +3074,19 @@ lemma as_user_respects_in_fault_reply:
| wpc
| simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def)+
apply (clarsimp simp: st_tcb_def2 tcb_at_def fun_upd_def[symmetric])
apply (clarsimp simp add: integrity_tcb_in_fault_reply_def)
apply (erule tcb_in_fault_reply.cases; clarsimp dest!:get_tcb_SomeD)
apply (clarsimp simp: integrity_tcb_in_fault_reply_def)
apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD)
apply (rule tifr_context[OF refl refl])
apply (intro exI tcb.equality ; simp add: arch_tcb_context_set_def)
apply (intro exI tcb.equality; simp add: arch_tcb_context_set_def)
by fastforce+
lemma handle_fault_reply_respects_in_fault_reply:
"\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>
handle_fault_reply f thread label mrs
\<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>"
by (cases f;wpsimp simp: handle_arch_fault_reply_def arch_get_sanitise_register_info_def
wp: as_user_respects_in_fault_reply)
by (cases f;
wpsimp simp: handle_arch_fault_reply_def arch_get_sanitise_register_info_def
wp: as_user_respects_in_fault_reply)
lemma thread_set_no_fault_respects_in_fault_reply:
"\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>
@ -3109,44 +3094,45 @@ lemma thread_set_no_fault_respects_in_fault_reply:
\<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\<rbrace>"
apply (simp add: thread_set_def)
apply (wp set_thread_state_ext_respects_in_fault_reply set_object_wp)
apply (clarsimp simp add: integrity_tcb_in_fault_reply_def)
apply (erule tcb_in_fault_reply.cases; clarsimp dest!:get_tcb_SomeD)
apply (clarsimp simp: integrity_tcb_in_fault_reply_def)
apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD)
apply (rule tifr_remove_fault[OF refl refl])
apply (intro exI tcb.equality ; simp add: arch_tcb_context_set_def)
apply (intro exI tcb.equality ; simp add: arch_tcb_context_set_def)
by fastforce+
lemma set_thread_state_respects_in_fault_reply:
"tst = Restart \<or> tst = Inactive \<Longrightarrow>\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\<rbrace>
"tst = Restart \<or> tst = Inactive \<Longrightarrow>
\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\<rbrace>
set_thread_state thread tst
\<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFFinal st\<rbrace>"
apply (simp add: set_thread_state_def)
apply (wp set_thread_state_ext_respects_in_fault_reply set_object_wp)
apply (clarsimp simp add: integrity_tcb_in_fault_reply_def)
apply (erule tcb_in_fault_reply.cases; clarsimp dest!:get_tcb_SomeD)
apply (clarsimp simp: integrity_tcb_in_fault_reply_def)
apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD)
apply (rule tifr_reply[OF refl refl])
apply (intro exI tcb.equality ; simp add: arch_tcb_context_set_def)
apply (intro exI tcb.equality; simp add: arch_tcb_context_set_def)
by fastforce+
lemma integrity_tcb_in_fault_reply_refl:
"\<lbrakk> st_tcb_at awaiting_reply receiver s; fault_tcb_at (flip (\<noteq>) None) receiver s;
aag_has_auth_to aag Reply receiver;
\<not> is_subject aag receiver; pas_refined aag s\<rbrakk>
\<not> is_subject aag receiver; pas_refined aag s \<rbrakk>
\<Longrightarrow> integrity_tcb_in_fault_reply aag X receiver TRFContext s s"
unfolding integrity_tcb_in_fault_reply_def
apply (clarsimp elim!:pred_tcb_atE)
apply (clarsimp elim!: pred_tcb_atE)
apply (rule tifr_context[OF refl refl])
apply (rule tcb_context_no_change)
apply fastforce+
apply (rule tcb_context_no_change)
apply fastforce+
done
thm cte_wp_at_emptyableD[simplified cte_wp_at_caps_of_state]
lemma emptyable_not_master:
"\<lbrakk> valid_objs s ; caps_of_state s slot = Some cap; \<not> is_master_reply_cap cap\<rbrakk>
"\<lbrakk> valid_objs s; caps_of_state s slot = Some cap; \<not> is_master_reply_cap cap\<rbrakk>
\<Longrightarrow> emptyable slot s"
apply (rule emptyable_cte_wp_atD[rotated 2])
apply (intro allI impI,assumption)
by (fastforce simp:is_cap_simps cte_wp_at_caps_of_state)+
apply (intro allI impI, assumption)
by (fastforce simp:is_cap_simps cte_wp_at_caps_of_state)+
lemma do_reply_transfer_respects:
"\<lbrace>pas_refined aag
@ -3165,15 +3151,15 @@ lemma do_reply_transfer_respects:
apply (rule hoare_seq_ext[OF _ assert_sp])
apply (rule hoare_seq_ext[OF _ assert_get_tcb_sp];force?)
apply wpc
\<comment> \<open>No fault case\<close>
\<comment> \<open>No fault case\<close>
apply (rule hoare_vcg_if_split[where P= "is_subject aag receiver" and f=f and g=f for f,
simplified if_cancel])
\<comment> \<open>receiver is a subject\<close>
apply ((wp set_thread_state_integrity_autarch thread_set_integrity_autarch
handle_fault_reply_respects do_ipc_transfer_integrity_autarch
do_ipc_transfer_pas_refined
| simp
| intro conjI impI)+)[1]
\<comment> \<open>receiver is a subject\<close>
apply ((wp set_thread_state_integrity_autarch thread_set_integrity_autarch
handle_fault_reply_respects do_ipc_transfer_integrity_autarch
do_ipc_transfer_pas_refined
| simp
| intro conjI impI)+)[1]
\<comment> \<open>receiver is not a subject\<close>
apply (rule use_spec') \<comment> \<open>Name initial state\<close>
apply (simp add: spec_valid_def) \<comment> \<open>no imp rule?\<close>
@ -3210,8 +3196,8 @@ lemma do_reply_transfer_respects:
handle_fault_reply_respects_in_fault_reply
| simp)+
apply force
apply (strengthen integrity_tcb_in_fault_reply_refl)+
apply (wp cap_delete_one_reply_st_tcb_at)
apply (strengthen integrity_tcb_in_fault_reply_refl)+
apply (wp cap_delete_one_reply_st_tcb_at)
\<comment> \<open>the end\<close>
by (force simp: st_tcb_at_tcb_states_of_state cte_wp_at_caps_of_state is_cap_simps

150
proof/access-control/Retype_AC.thy
View File

@ -407,10 +407,14 @@ lemma delete_objects_respects[wp]:
by (fastforce simp: ptr_range_def intro!: detype_integrity)
lemma storeWord_respects:
"\<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and> (\<forall>p' \<in> ptr_range p 2. aag_has_auth_to aag Write p')\<rbrace> storeWord p v \<lbrace>\<lambda>a b. integrity aag X st (s\<lparr>machine_state := b\<rparr>)\<rbrace>"
"\<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)
\<and> (\<forall>p' \<in> ptr_range p 2. aag_has_auth_to aag Write p')\<rbrace>
storeWord p v
\<lbrace>\<lambda>a b. integrity aag X st (s\<lparr>machine_state := b\<rparr>)\<rbrace>"
unfolding storeWord_def
apply wp
apply (auto simp: integrity_def is_aligned_mask [symmetric] intro!: trm_write ptr_range_memI ptr_range_add_memI)
apply (auto simp: integrity_def is_aligned_mask [symmetric]
intro!: trm_write ptr_range_memI ptr_range_add_memI)
done
lemma dmo_clearMemory_respects':
@ -502,15 +506,17 @@ lemma invoke_untyped_integrity:
retype_region_ret_is_subject retype_region_ret_pd_aligned
set_cap_integrity_autarch hoare_vcg_if_lift
hoare_whenE_wp reset_untyped_cap_integrity
| clarsimp simp: split_paired_Ball
| erule in_set_zipE | blast)+
apply(clarsimp simp: is_aligned_neg_mask_eq
ptr_range_def p_assoc_help bits_of_def
cte_wp_at_caps_of_state)
| clarsimp simp: split_paired_Ball
| erule in_set_zipE
| blast)+
apply (clarsimp simp: is_aligned_neg_mask_eq
ptr_range_def p_assoc_help bits_of_def
cte_wp_at_caps_of_state)
apply (frule(1) cap_cur_auth_caps_of_state, simp+)
apply (clarsimp simp: aag_cap_auth_def pas_refined_all_auth_is_owns)
apply (intro conjI impI, (simp add: word_and_le2 field_simps
| erule ball_subset[where A="{a && c .. b}" for a b c])+)
apply (simp add: word_and_le2 field_simps
| erule ball_subset[where A="{a && c .. b}" for a b c]
| rule conjI impI)+
done
lemma clas_default_cap:
@ -542,16 +548,16 @@ lemma create_cap_pas_refined:
\<and> is_aligned (snd ref) (obj_bits_api tp sz))\<rbrace>
create_cap tp sz p dev ref
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply(simp add: create_cap_def split_def)
apply(wps | wp set_cdt_pas_refined set_cap_pas_refined set_original_wp | clarsimp)+
apply (simp add: create_cap_def split_def)
apply (wps | wp set_cdt_pas_refined set_cap_pas_refined set_original_wp | clarsimp)+
apply (rule conjI)
apply (cases "fst ref", clarsimp simp: pas_refined_refl)
apply (cases "tp = Untyped")
apply (simp add: cap_links_asid_slot_def pas_refined_refl cap_links_irq_def aag_cap_auth_def ptr_range_def obj_bits_api_def)
apply (clarsimp simp add: obj_refs_default_nut clas_default_cap pas_refined_refl cli_default_cap aag_cap_auth_def)
apply(drule obj_refs_default')
apply(case_tac tp, simp_all)
apply(auto intro: pas_refined_refl dest!: subsetD)
apply (drule obj_refs_default')
apply (case_tac tp, simp_all)
apply (auto intro: pas_refined_refl dest!: subsetD)
done
lemma pd_shifting_dual':
@ -559,7 +565,7 @@ lemma pd_shifting_dual':
pd + (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2"
apply (subst (asm) pd_bits_def)
apply (subst (asm) pageBits_def)
apply( simp add: pd_shifting_dual)
apply (simp add: pd_shifting_dual)
done
@ -694,7 +700,7 @@ lemma bas_eq[simp]: "thread_bound_ntfns s' = thread_bound_ntfns s"
end
lemma invs_mdb_cte':
" invs s \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)"
"invs s \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)"
by (drule invs_mdb) (simp add: valid_mdb_def2)
context retype_region_proofs'
@ -705,9 +711,9 @@ interpretation Arch . (*FIXME; arch_split*)
lemma domains_of_state: "domains_of_state s' \<subseteq> domains_of_state s"
unfolding s'_def by simp
(* FIXME MOVE next to cte_at_pres *)
lemma cte_wp_at_pres: "cte_wp_at P p s \<Longrightarrow> cte_wp_at P p s'"
lemma cte_wp_at_pres:
"cte_wp_at P p s \<Longrightarrow> cte_wp_at P p s'"
unfolding cte_wp_at_cases s'_def ps_def
apply (erule disjE)
apply (clarsimp simp: well_formed_cnode_n_def orthr)+
@ -716,26 +722,28 @@ lemma cte_wp_at_pres: "cte_wp_at P p s \<Longrightarrow> cte_wp_at P p s'"
(* FIXME MOVE next to cte_at_pres *)
lemma caps_of_state_pres:
"caps_of_state s p = Some cap \<Longrightarrow> caps_of_state s' p = Some cap"
using cte_wp_at_pres by (simp add: F)
using cte_wp_at_pres by (simp add: F)
lemma pas_refined: "invs s \<Longrightarrow> pas_refined aag s \<Longrightarrow> pas_refined aag s'"
apply(erule pas_refined_state_objs_to_policy_subset)
apply(simp add: state_objs_to_policy_def refs_eq vrefs_eq mdb_and_revokable)
apply(rule subsetI, rename_tac x, case_tac x, simp)
apply(erule state_bits_to_policy.cases)
apply (solves\<open>auto intro!: sbta_caps intro: caps_retype split: cap.split\<close>)
apply (solves\<open>auto intro!: sbta_untyped intro: caps_retype split: cap.split\<close>)
apply (solves \<open>auto intro!: sbta_caps intro: caps_retype split: cap.split\<close>)
apply (solves \<open>auto intro!: sbta_untyped intro: caps_retype split: cap.split\<close>)
apply (blast intro: state_bits_to_policy.intros)
apply (blast intro: state_bits_to_policy.intros)
apply (force intro!: sbta_cdt dest: caps_of_state_pres invs_mdb_cte'[THEN mdb_cte_atD[rotated]])
apply (force intro!: sbta_cdt_transferable dest: caps_of_state_pres invs_mdb_cte'[THEN mdb_cte_atD[rotated]])
apply (force intro!: sbta_cdt
dest: caps_of_state_pres invs_mdb_cte'[THEN mdb_cte_atD[rotated]])
apply (force intro!: sbta_cdt_transferable
dest: caps_of_state_pres invs_mdb_cte'[THEN mdb_cte_atD[rotated]])
apply (simp add: vrefs_eq)
apply(blast intro: state_bits_to_policy.intros)
apply (blast intro: state_bits_to_policy.intros)
apply (simp add: vrefs_eq)
apply(force elim!: state_asids_to_policy_aux.cases
intro: state_asids_to_policy_aux.intros caps_retype
split: cap.split
dest: sata_asid[OF caps_retype, rotated])
apply (force elim!: state_asids_to_policy_aux.cases
intro: state_asids_to_policy_aux.intros caps_retype
split: cap.split
dest: sata_asid[OF caps_retype, rotated])
apply clarsimp
apply (erule state_irqs_to_policy_aux.cases)
apply (solves\<open>auto intro!: sita_controlled intro: caps_retype split: cap.split\<close>)
@ -814,7 +822,6 @@ lemma retype_region_ext_pas_refined:
apply (force intro: domtcbs)
done
lemma retype_region_pas_refined:
"\<lbrace>pas_refined aag and invs and pas_cur_domain aag and
caps_overlap_reserved
@ -829,11 +836,12 @@ lemma retype_region_pas_refined:
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)
apply (rule hoare_pre)
apply(rule use_retype_region_proofs_ext'[where P = "invs and pas_refined aag"])
apply(erule retype_region_proofs'.pas_refined[OF retype_region_proofs'.intro],blast,blast)
apply (wp retype_region_ext_pas_refined)
apply simp
apply auto
apply (rule use_retype_region_proofs_ext'[where P = "invs and pas_refined aag"])
apply clarsimp
apply (erule (2) retype_region_proofs'.pas_refined[OF retype_region_proofs'.intro])
apply (wp retype_region_ext_pas_refined)
apply simp
apply auto
done
(* FIXME MOVE *)
@ -1252,10 +1260,11 @@ lemma retype_region_pas_refined':
K ((type = CapTableObject \<longrightarrow> 0 < o_bits))\<rbrace>
retype_region ptr num_objects o_bits type dev
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply(rule hoare_gen_asm)+
apply(rule hoare_weaken_pre)
apply(rule use_retype_region_proofs_ext'[where P="invs and pas_refined aag"])
apply(erule retype_region_proofs'.pas_refined[OF retype_region_proofs'.intro],blast,blast)
apply (rule hoare_gen_asm)+
apply (rule hoare_weaken_pre)
apply (rule use_retype_region_proofs_ext'[where P="invs and pas_refined aag"])
apply clarsimp
apply (erule (2) retype_region_proofs'.pas_refined[OF retype_region_proofs'.intro])
apply (wp retype_region_ext_pas_refined)
apply simp
apply fastforce
@ -1266,7 +1275,8 @@ lemma retype_region_pas_refined':
apply (fastforce simp: cte_wp_at_caps_of_state)
apply (cases slot)
apply (auto intro: cte_wp_at_caps_no_overlapI descendants_range_caps_no_overlapI
cte_wp_at_pspace_no_overlapI simp: cte_wp_at_sym)
cte_wp_at_pspace_no_overlapI
simp: cte_wp_at_sym)
done
@ -1316,7 +1326,8 @@ lemma pas_refined_work_units_complete[simp]:
(*FIXME MOVE *)
lemma set_cap_sets_direct:
"P cap \<Longrightarrow>\<lbrace>\<top>\<rbrace>
"P cap \<Longrightarrow>
\<lbrace>\<top>\<rbrace>
set_cap cap slot
\<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace>"
apply (rule hoare_strengthen_post)
@ -1324,17 +1335,12 @@ lemma set_cap_sets_direct:
apply (erule cte_wp_at_lift)
by blast
(*FIXME MOVE *)
lemma hoare_gen_asm0:
"(P \<Longrightarrow> \<lbrace>\<top>\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>K P\<rbrace> f \<lbrace>Q\<rbrace>"
by (fastforce simp add: valid_def)
(*FIXME MOVE *)
lemma set_cap_sets_wp:
"\<lbrace>\<lambda>_. P cap\<rbrace>
set_cap cap slot
\<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace>"
by (rule hoare_gen_asm0[simplified]) (erule set_cap_sets_direct)
by (rule hoare_gen_asm2[simplified]) (erule set_cap_sets_direct)
lemma reset_untyped_cap_pas_refined[wp]:
"\<lbrace>pas_refined aag and cte_wp_at is_untyped_cap slot
@ -1344,23 +1350,22 @@ lemma reset_untyped_cap_pas_refined[wp]:
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)
apply (clarsimp simp: reset_untyped_cap_def)
(*
apply (simp add:liftE_bindE)
apply (rule hoare_seq_ext[OF _ get_cap_sp]) *)
apply (rule hoare_pre)
apply (wps | wp set_cap_pas_refined_not_transferable | simp add: unless_def)+
apply (rule valid_validE) apply (rule_tac P="is_untyped_cap cap
\<and> pas_cap_cur_auth aag cap" in hoare_gen_asm)
apply (rule_tac Q= "\<lambda>_.cte_wp_at (\<lambda> c. \<not> is_transferable (Some c)) slot and pas_refined aag" in hoare_strengthen_post)
apply (rule validE_valid, rule mapME_x_inv_wp)
apply (rule hoare_pre)
apply (wps | wp preemption_point_inv' set_cap_pas_refined_not_transferable set_cap_sets_direct | simp)+
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (fastforce simp: is_cap_simps aag_cap_auth_UntypedCap_idx_dev bits_of_def)
apply (rule valid_validE)
apply (rule_tac P="is_untyped_cap cap \<and> pas_cap_cur_auth aag cap" in hoare_gen_asm)
apply (rule_tac Q= "\<lambda>_.cte_wp_at (\<lambda> c. \<not> is_transferable (Some c)) slot and pas_refined aag"
in hoare_strengthen_post)
apply (rule validE_valid, rule mapME_x_inv_wp)
apply (rule hoare_pre)
apply (wps
| wp preemption_point_inv' set_cap_pas_refined_not_transferable set_cap_sets_direct
| simp)+
apply (fastforce simp: is_cap_simps aag_cap_auth_UntypedCap_idx_dev bits_of_def)
apply blast
apply (wps | wp hoare_vcg_const_imp_lift get_cap_wp
delete_objects_pas_refined hoare_drop_imp | simp add: if_apply_def2)+
apply (wps
| wp hoare_vcg_const_imp_lift get_cap_wp delete_objects_pas_refined hoare_drop_imp
| simp)+
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
apply (auto elim: caps_pas_cap_cur_auth_UntypedCap_idx_dev)
done
@ -1377,8 +1382,7 @@ lemma retype_region_post_retype_invs_spec:
apply (wp retype_region_post_retype_invs)
apply (clarsimp simp del: split_paired_Ex)
apply (frule valid_cap_range_untyped[OF invs_valid_objs],simp)
apply (intro conjI)
apply fastforce+
apply fastforce
done
lemma invoke_untyped_pas_refined:
@ -1417,23 +1421,27 @@ lemma invoke_untyped_pas_refined:
apply (rule hoare_pre, wp retype_region_pas_refined)
apply (clarsimp simp: authorised_untyped_inv_def)
apply (strengthen range_cover_le[mk_strg I E], simp)
apply (intro conjI exI; (erule cte_wp_at_weakenE)?,
clarsimp simp: field_simps word_and_le2)
apply (intro conjI exI;
(erule cte_wp_at_weakenE)?,
clarsimp simp: field_simps word_and_le2)
apply (rule hoare_pre, wp set_cap_pas_refined)
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps)
apply (cases ui, clarsimp simp: authorised_untyped_inv_def
caps_pas_cap_cur_auth_UntypedCap_idx_dev)
apply (cases ui,
clarsimp simp: authorised_untyped_inv_def caps_pas_cap_cur_auth_UntypedCap_idx_dev)
apply wp
apply (clarsimp)
apply clarsimp
apply (cases ui, clarsimp)
(* FIXME CLEAN UP ? *)
apply (intro conjI)
prefer 2
apply (simp add:cte_wp_at_caps_of_state del: untyped_range.simps)
apply (rule cte_map_not_null_outside'[where p="(a, b)" and p'="(a, b)" for a b,
simplified fst_conv, OF caps_of_state_cteD], assumption)
apply(force simp: descendants_range_def cte_wp_at_caps_of_state authorised_untyped_inv_def)+
apply (simp add: cte_wp_at_caps_of_state del: untyped_range.simps)
apply (rule cte_map_not_null_outside'
[where p="(a, b)" and p'="(a, b)" for a b,
simplified fst_conv, OF caps_of_state_cteD],
assumption)
apply (force simp: descendants_range_def
cte_wp_at_caps_of_state authorised_untyped_inv_def)+
done
subsection{* decode *}

149
proof/access-control/Syscall_AC.thy
View File

@ -57,15 +57,16 @@ lemma perform_invocation_pas_refined:
done
lemma ntfn_gives_obj_at:
"invs s \<Longrightarrow> (\<exists>ntfn. ko_at (Notification ntfn) ntfnptr s
\<and> (\<forall>x\<in>ntfn_q_refs_of (ntfn_obj ntfn).
(\<lambda>(t, rt). obj_at (\<lambda>tcb. ko_at tcb t s) t s) x)) = ntfn_at ntfnptr s"
"invs s \<Longrightarrow>
(\<exists>ntfn. ko_at (Notification ntfn) ntfnptr s
\<and> (\<forall>x\<in>ntfn_q_refs_of (ntfn_obj ntfn).
(\<lambda>(t, rt). obj_at (\<lambda>tcb. ko_at tcb t s) t s) x)) = ntfn_at ntfnptr s"
apply (rule iffI)
apply (clarsimp simp: obj_at_def is_ntfn)
apply (clarsimp simp: obj_at_def is_ntfn)
apply (drule (1) ntfn_queued_st_tcb_at [where P = \<top>, unfolded obj_at_def, simplified])
apply clarsimp
apply clarsimp
apply clarsimp
apply clarsimp
apply (clarsimp simp: st_tcb_def2 dest!: get_tcb_SomeD)
done
@ -217,7 +218,7 @@ lemma set_thread_state_authorised[wp]:
apply (rename_tac cnode_invocation)
apply (case_tac cnode_invocation,
simp_all add: cnode_inv_auth_derivations_def authorised_cnode_inv_def)[1]
apply (wp set_thread_state_cte_wp_at | simp)+
apply (wp set_thread_state_cte_wp_at | simp)+
apply (rename_tac arch_invocation)
apply (case_tac arch_invocation, simp_all add: valid_arch_inv_def)[1]
apply (rename_tac page_table_invocation)
@ -227,7 +228,7 @@ lemma set_thread_state_authorised[wp]:
| simp add: valid_pdi_def)+
apply (rename_tac asid_control_invocation)
apply (case_tac asid_control_invocation, simp_all add: valid_aci_def)
apply (wp ct_in_state_set | simp)+
apply (wp ct_in_state_set | simp)+
apply (rename_tac asid_pool_invocation)
apply (case_tac asid_pool_invocation; simp add: valid_apinv_def)
apply (wp sts_obj_at_impossible ct_in_state_set
@ -250,12 +251,12 @@ lemma lcs_reply_owns:
lookup_cap_and_slot thread ptr
\<lbrace>\<lambda>rv s. \<forall>ep. (\<exists>m R. fst rv = cap.ReplyCap ep m R \<and> AllowGrant \<in> R) \<longrightarrow> is_subject aag ep\<rbrace>, -"
apply (rule hoare_post_imp_R)
apply (rule hoare_pre)
apply (rule hoare_vcg_conj_lift_R [where S = "K (pas_refined aag)"])
apply (rule lookup_cap_and_slot_cur_auth)
apply (simp | wp lookup_cap_and_slot_inv)+
apply (rule hoare_pre)
apply (rule hoare_vcg_conj_lift_R [where S = "K (pas_refined aag)"])
apply (rule lookup_cap_and_slot_cur_auth)
apply (simp | wp lookup_cap_and_slot_inv)+
apply (force simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
dest:aag_Control_into_owns[rotated])
dest: aag_Control_into_owns)
done
crunch pas_refined[wp]: reply_from_kernel "pas_refined aag"
@ -295,7 +296,7 @@ lemma guarded_to_cur_domain:
is_subject aag (cur_thread s)\<rbrakk>
\<Longrightarrow> pas_cur_domain aag s"
by (auto simp: invs_def valid_state_def valid_idle_def pred_tcb_at_def obj_at_def
ct_in_state_def guarded_pas_domain_def)
ct_in_state_def guarded_pas_domain_def)
lemma handle_invocation_pas_refined:
@ -307,25 +308,25 @@ lemma handle_invocation_pas_refined:
apply (simp add: handle_invocation_def split_def)
apply (cases blocking, simp)
apply (rule hoare_pre)
by (((wp syscall_valid without_preemption_wp
handle_fault_pas_refined set_thread_state_pas_refined
set_thread_state_runnable_valid_sched
perform_invocation_pas_refined
hoare_vcg_conj_lift hoare_vcg_all_lift
| wpc
| rule hoare_drop_imps
| simp add: if_apply_def2 conj_comms split del: if_split
del: hoare_True_E_R)+),
((wp lookup_extra_caps_auth lookup_extra_caps_authorised
decode_invocation_authorised
lookup_cap_and_slot_authorised
lookup_cap_and_slot_cur_auth
as_user_pas_refined
lookup_cap_and_slot_valid_fault3
| simp add: comp_def runnable_eq_active)+),
(auto intro: guarded_to_cur_domain
simp: ct_in_state_def st_tcb_at_def live_def hyp_live_def
intro: if_live_then_nonz_capD)[1])+
by (((wp syscall_valid without_preemption_wp
handle_fault_pas_refined set_thread_state_pas_refined
set_thread_state_runnable_valid_sched
perform_invocation_pas_refined
hoare_vcg_conj_lift hoare_vcg_all_lift
| wpc
| rule hoare_drop_imps
| simp add: if_apply_def2 conj_comms split del: if_split
del: hoare_True_E_R)+),
((wp lookup_extra_caps_auth lookup_extra_caps_authorised
decode_invocation_authorised
lookup_cap_and_slot_authorised
lookup_cap_and_slot_cur_auth
as_user_pas_refined
lookup_cap_and_slot_valid_fault3
| simp add: comp_def runnable_eq_active)+),
(auto intro: guarded_to_cur_domain
simp: ct_in_state_def st_tcb_at_def live_def hyp_live_def
intro: if_live_then_nonz_capD)[1])+
lemma handle_invocation_respects:
"\<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'
@ -344,22 +345,22 @@ lemma handle_invocation_respects:
| wpc
| simp add: if_apply_def2
split del: if_split)+
apply (simp add: conj_comms pred_conj_def comp_def if_apply_def2 split del: if_split
| wp perform_invocation_respects set_thread_state_pas_refined
set_thread_state_authorised
set_thread_state_runnable_valid_sched
set_thread_state_integrity_autarch
sts_first_restart
decode_invocation_authorised
lookup_extra_caps_auth lookup_extra_caps_authorised
set_thread_state_integrity_autarch
lookup_cap_and_slot_cur_auth lookup_cap_and_slot_authorised
hoare_vcg_const_imp_lift perform_invocation_pas_refined
set_thread_state_ct_st hoare_vcg_const_imp_lift_R
lookup_cap_and_slot_valid_fault3
| (rule valid_validE, strengthen invs_vobjs_strgs))+
apply (simp add: conj_comms pred_conj_def comp_def if_apply_def2 split del: if_split
| wp perform_invocation_respects set_thread_state_pas_refined
set_thread_state_authorised
set_thread_state_runnable_valid_sched
set_thread_state_integrity_autarch
sts_first_restart
decode_invocation_authorised
lookup_extra_caps_auth lookup_extra_caps_authorised
set_thread_state_integrity_autarch
lookup_cap_and_slot_cur_auth lookup_cap_and_slot_authorised
hoare_vcg_const_imp_lift perform_invocation_pas_refined
set_thread_state_ct_st hoare_vcg_const_imp_lift_R
lookup_cap_and_slot_valid_fault3
| (rule valid_validE, strengthen invs_vobjs_strgs))+
by (fastforce intro: st_tcb_ex_cap' guarded_to_cur_domain
simp: ct_in_state_def runnable_eq_active)+
simp: ct_in_state_def runnable_eq_active)
crunch pas_refined[wp]: delete_caller_cap "pas_refined aag"
@ -376,21 +377,23 @@ lemma handle_recv_pas_refined:
lookup_slot_for_thread_authorised lookup_slot_for_thread_cap_fault
hoare_vcg_all_lift_R get_simple_ko_wp
| wpc | simp
| rename_tac word1 word2 word3, rule_tac Q="\<lambda>rv s. invs s \<and> is_subject aag thread
\<and> (pasSubject aag, Receive, pasObjectAbs aag word1) \<in> pasPolicy aag"
in hoare_strengthen_post, wp, clarsimp simp: invs_valid_objs invs_sym_refs)+
apply (rule_tac Q' = "\<lambda>rv s. pas_refined aag s \<and> invs s \<and> tcb_at thread s
\<and> cur_thread s = thread \<and> is_subject aag (cur_thread s)
\<and> is_subject aag thread" in hoare_post_imp_R [rotated])
apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def valid_fault_def)
apply (wp user_getreg_inv | strengthen invs_vobjs_strgs invs_sym_refs_strg | simp)+
| (rule_tac Q="\<lambda>rv s. invs s \<and> is_subject aag thread
\<and> (pasSubject aag, Receive, pasObjectAbs aag thread) \<in> pasPolicy aag"
in hoare_strengthen_post,
wp, clarsimp simp: invs_valid_objs invs_sym_refs))+
apply (rule_tac Q' = "\<lambda>rv s. pas_refined aag s \<and> invs s \<and> tcb_at thread s
\<and> cur_thread s = thread \<and> is_subject aag (cur_thread s)
\<and> is_subject aag thread" in hoare_post_imp_R [rotated])
apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def
cap_rights_to_auth_def valid_fault_def)
apply (wp user_getreg_inv | strengthen invs_vobjs_strgs invs_sym_refs_strg | simp)+
apply clarsimp
done
crunch respects[wp]: delete_caller_cap "integrity aag X st"
lemma invs_mdb_strgs: "invs s \<longrightarrow> valid_mdb s"
by(auto)
by auto
lemma handle_recv_integrity:
"\<lbrace>integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread
@ -405,14 +408,16 @@ lemma handle_recv_integrity:
| wpc
| simp
| rule_tac Q="\<lambda>rv s. invs s \<and> is_subject aag thread
\<and> (pasSubject aag, Receive, pasObjectAbs aag _) \<in> pasPolicy aag"
\<and> (pasSubject aag, Receive, pasObjectAbs aag thread) \<in> pasPolicy aag"
in hoare_strengthen_post, wp, clarsimp simp: invs_valid_objs invs_sym_refs)+
apply (rule_tac Q' = "\<lambda>rv s. pas_refined aag s \<and> einvs s \<and> is_subject aag (cur_thread s)
apply (rule_tac Q' = "\<lambda>rv s. pas_refined aag s \<and> einvs s \<and> is_subject aag (cur_thread s)
\<and> tcb_at thread s \<and> cur_thread s = thread
\<and> is_subject aag thread \<and> integrity aag X st s" in hoare_post_imp_R [rotated])
apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def
cap_rights_to_auth_def valid_fault_def)
apply (wp user_getreg_inv | strengthen invs_vobjs_strgs invs_sym_refs_strg invs_mdb_strgs | simp)+
apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def
cap_rights_to_auth_def valid_fault_def)
apply (wp user_getreg_inv
| strengthen invs_vobjs_strgs invs_sym_refs_strg invs_mdb_strgs
| simp)+
apply clarsimp
done
@ -422,7 +427,7 @@ lemma handle_reply_pas_refined[wp]:
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
unfolding handle_reply_def
apply (rule hoare_pre)
apply (wp do_reply_transfer_pas_refined get_cap_auth_wp [where aag = aag]| wpc)+
apply (wp do_reply_transfer_pas_refined get_cap_auth_wp [where aag = aag]| wpc)+
by (force simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
intro: aag_Control_into_owns)
@ -671,23 +676,11 @@ lemma handle_event_integrity:
| fastforce)+
done
(*lemma integrity_restart_context:
"\<lbrakk> integrity aag X st s; pasMayActivate aag;
st_tcb_at ((=) Structures_A.Restart) thread s; \<not> is_subject aag thread \<rbrakk>
\<Longrightarrow> \<exists>tcb tcb'. get_tcb thread st = Some tcb \<and>
get_tcb thread s = Some tcb' \<and>
(arch_tcb_context_get (tcb_arch tcb') = arch_tcb_context_get (tcb_arch tcb) \<or>
arch_tcb_context_get (tcb_arch tcb') =
(arch_tcb_context_get (tcb_arch tcb))(TPIDRURW := (arch_tcb_context_get (tcb_arch tcb)) FaultInstruction))"
apply (clarsimp simp: integrity_def)
apply (drule_tac x = thread in spec)
apply (erule integrity_obj.cases, auto simp add: tcb_states_of_state_def get_tcb_def st_tcb_def2)
done*)
definition consistent_tpidrurw_at
where
where
"consistent_tpidrurw_at \<equiv>
obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> arch_tcb_context_get (tcb_arch tcb) TPIDRURW = tcb_ipc_buffer tcb)"
obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb
\<and> arch_tcb_context_get (tcb_arch tcb) TPIDRURW = tcb_ipc_buffer tcb)"
lemma set_thread_state_restart_to_running_respects:
"\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Restart) thread
@ -706,7 +699,7 @@ lemma set_thread_state_restart_to_running_respects:
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def obj_at_def st_tcb_at_def)
apply (clarsimp dest!: get_tcb_SomeD)
apply (rule_tac tro_tcb_activate [OF refl refl])
apply (rule_tac tro_tcb_activate[OF refl refl])
apply (simp add: tcb_bound_notification_reset_integrity_def)+
done

27
proof/access-control/Tcb_AC.thy
View File

@ -29,7 +29,7 @@ where
pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot))
| tcb_invocation.NotificationControl t ntfn \<Rightarrow> is_subject aag t \<and>
case_option True (\<lambda>a. \<forall>auth \<in> {Receive, Reset}.
(pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag) ntfn
(pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag) ntfn
| tcb_invocation.ReadRegisters src susp n arch \<Rightarrow> is_subject aag src
| tcb_invocation.WriteRegisters dest res values arch \<Rightarrow> is_subject aag dest
| tcb_invocation.CopyRegisters dest src susp res frame int_regs arch \<Rightarrow>
@ -60,7 +60,7 @@ lemma restart_integrity_autarch:
apply (simp add: restart_def)
apply (wp set_thread_state_integrity_autarch setup_reply_master_respects
hoare_drop_imps
| simp add: if_apply_def2)+
| simp add: if_apply_def2)+
done
crunch integrity_autarch: option_update_thread "integrity aag X st"
@ -73,6 +73,7 @@ lemma schematic_lift_tuple3_l:
lemma schematic_lift_tuple3_r:
"Q \<and> P (fst (a, b, c)) (fst (snd (a, b, c))) (snd (snd (a, b, c))) \<Longrightarrow> P a b c" by simp
(* FIXME: MOVE *)
lemma invoke_tcb_cases:
"invoke_tcb ti = (case ti of
tcb_invocation.Suspend t \<Rightarrow> invoke_tcb (tcb_invocation.Suspend t)
@ -125,7 +126,7 @@ lemma aag_cap_auth_master_Reply:
(* FIXME MOVE *)
lemma cdt_NullCap:
"valid_mdb s \<Longrightarrow> caps_of_state s src = Some NullCap \<Longrightarrow> cdt s src = None"
by (rule classical) (force dest:mdb_cte_atD simp:valid_mdb_def2)
by (rule ccontr) (force dest: mdb_cte_atD simp: valid_mdb_def2)
lemma setup_reply_master_pas_refined:
@ -134,7 +135,7 @@ lemma setup_reply_master_pas_refined:
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: setup_reply_master_def)
apply (wp get_cap_wp set_cap_pas_refined set_original_wp)+
by (force dest:cdt_NullCap simp add: aag_cap_auth_master_Reply cte_wp_at_caps_of_state)
by (force dest: cdt_NullCap simp: aag_cap_auth_master_Reply cte_wp_at_caps_of_state)
crunches possible_switch_to
for tcb_domain_map_wellformed[wp]: " tcb_domain_map_wellformed aag"
@ -278,7 +279,7 @@ lemma cap_insert_cdt_change_allowed[wp]:
apply (intro allI notI)
apply (drule(1) mdb_cte_atD[rotated])
apply (simp add:cte_wp_at_caps_of_state)
done
done
lemma invoke_tcb_tc_respects_aag:
@ -350,7 +351,7 @@ lemma invoke_tcb_tc_respects_aag:
clas_no_asid cli_no_irqs
emptyable_def
| rule conjI | erule pas_refined_refl)+
done
done
lemma invoke_tcb_unbind_notification_respects:
"\<lbrace>integrity aag X st and pas_refined aag and simple_sched_action
@ -480,13 +481,13 @@ lemma invoke_tcb_pas_refined:
apply assumption
apply (rule hoare_gen_asm)
apply (cases ti, simp_all add: authorised_tcb_inv_def)
apply (wp ita_wps hoare_drop_imps mapM_x_wp'
| simp add: emptyable_def if_apply_def2 authorised_tcb_inv_def
arch_get_sanitise_register_info_def
| rule ball_tcb_cap_casesI
| wpc
| (fastforce intro: notE[rotated,OF idle_no_ex_cap,simplified]
simp: invs_valid_global_refs invs_valid_objs))+
apply (wp ita_wps hoare_drop_imps mapM_x_wp'
| simp add: emptyable_def if_apply_def2 authorised_tcb_inv_def
arch_get_sanitise_register_info_def
| rule ball_tcb_cap_casesI
| wpc
| fastforce intro: notE[rotated,OF idle_no_ex_cap,simplified]
simp: invs_valid_global_refs invs_valid_objs)+
done
subsection{* TCB / decode *}