theory Noninterference

lemma partitionIntegrity_subjectAffects_obj:
  assumes par_inte: "partitionIntegrity (aag :: 'a subject_label PAS) s s'"
  assumes pas_ref: "pas_refined aag s"
  assumes invs: "invs s"
  assumes pwni: "pas_wellformed_noninterference aag"
  assumes silc_inv: "silc_inv aag st s"
  assumes kh_diff: "kheap s x \<noteq> kheap s' x"
  notes inte_obj = par_inte[THEN partitionIntegrity_integrity, THEN integrity_subjects_obj,
                            THEN spec[where x=x], simplified integrity_obj_def, simplified]
  shows "pasObjectAbs aag x \<in> subjectAffects (pasPolicy aag) (pasSubject aag)" proof - show ?thesis using inte_obj proof (induct "kheap s x" rule: converse_rtranclp_induct) case base thus ?case using kh_diff by force next case (step z) note troa = step.hyps(1) show ?case proof (cases "z = kheap s x") case True thus ?thesis using step.hyps by blast next case False note hyps = this pwni pas_ref invs silc_inv kh_diff hence sym_helper: "\<And>auth tcb. kheap s x = Some (TCB tcb) \<Longrightarrow>
                                    (pasObjectAbs aag x, auth, pasObjectAbs aag x) \<in> pasPolicy aag" by (fastforce elim!: pas_wellformed_noninterference_policy_refl
                             silc_inv_cnode_onlyE obj_atE
                       simp: is_cap_table_def) show ?thesis using troa proof (cases rule: integrity_obj_atomic.cases) case troa_lrefl thus ?thesis by (fastforce intro: subjectAffects.intros) next case (troa_ntfn ntfn ntfn' auth s) thus ?thesis by (fastforce intro: affects_ep) next case (troa_ep ep ep' auth s) thus ?thesis by (fastforce intro: affects_ep) next case (troa_ep_unblock ep ep' tcb ntfn) thus ?thesis by (fastforce intro: affects_ep_bound_trans) next case (troa_tcb_send tcb tcb' ctxt' ep) thus ?thesis using hyps apply (clarsimp simp: direct_send_def indirect_send_def) apply (erule disjE) apply (clarsimp simp: receive_blocked_on_def2) apply (frule (2) pas_refined_tcb_st_to_auth) apply (fastforce intro!: affects_send sym_helper) apply (fastforce intro!: affects_send bound_tcb_at_implies_receive
                                   pred_tcb_atI sym_helper) done next case (troa_tcb_call tcb tcb' caller R ctxt' ep) thus ?thesis using hyps apply (clarsimp simp add: direct_call_def ep_recv_blocked_def) apply (rule affects_send[rotated 2]) apply (erule (1) pas_refined_tcb_st_to_auth[rotated 2]; force) apply (fastforce intro: sym_helper) apply assumption apply blast done next case (troa_tcb_reply tcb tcb' new_st ctxt') thus ?thesis using hyps apply clarsimp apply (erule affects_reply) by (rule sym_helper) next case (troa_tcb_receive tcb tcb' new_st ep) thus ?thesis using hyps by (auto intro: affects_recv pas_refined_tcb_st_to_auth simp: send_blocked_on_def2) next case (troa_tcb_restart tcb tcb' ep) thus ?thesis using hyps by (fastforce intro: affects_reset[where auth=Receive] affects_reset[where auth=SyncSend]
                         elim: blocked_on.elims pas_refined_tcb_st_to_auth[rotated 2]
                       intro!: sym_helper) next case (troa_tcb_unbind tcb tcb') thus ?thesis using hyps apply - by (cases "tcb_bound_notification tcb" ;
              fastforce intro: affects_reset[where auth=Receive] bound_tcb_at_implies_receive
                               pred_tcb_atI sym_helper) next case (troa_tcb_empty_ctable tcb tcb' cap') thus ?thesis using hyps apply (clarsimp simp:reply_cap_deletion_integrity_def; elim disjE; clarsimp) apply (rule affects_delete_derived) apply (rule aag_wellformed_delete_derived[rotated -1, OF pas_refined_wellformed],
                 assumption) apply (frule cap_auth_caps_of_state[rotated,where p ="(x,tcb_cnode_index 0)"],
                 force simp: caps_of_state_def') by (fastforce simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
                       split: if_splits) next case (troa_tcb_empty_caller tcb tcb' cap') thus ?thesis using hyps apply (clarsimp simp:reply_cap_deletion_integrity_def) apply (elim disjE; clarsimp) apply (rule affects_delete_derived) apply (rule aag_wellformed_delete_derived[rotated -1, OF pas_refined_wellformed],
                 assumption) apply (frule cap_auth_caps_of_state[rotated,where p ="(x,tcb_cnode_index 3)"],
                 force simp: caps_of_state_def') by (fastforce simp: aag_cap_auth_def cap_auth_conferred_def
                              reply_cap_rights_to_auth_def
                       split: if_splits) next case (troa_tcb_activate tcb tcb') thus ?thesis by blast next case (troa_arch ao ao') thus ?thesis using assms by (fastforce dest: partitionIntegrity_subjectAffects_aobj) next case (troa_cnode n content content') thus ?thesis using hyps unfolding cnode_integrity_def apply clarsimp apply (drule fun_noteqD) apply (erule exE, rename_tac l) apply (drule_tac x=l in spec) apply (clarsimp dest!:not_sym[where t=None]) apply (clarsimp simp:reply_cap_deletion_integrity_def) apply (rule affects_delete_derived) apply (rule aag_wellformed_delete_derived[rotated -1, OF pas_refined_wellformed],
                 assumption) apply (frule_tac p="(x,l)" in cap_auth_caps_of_state[rotated]) apply (force simp: caps_of_state_def' intro:well_formed_cnode_invsI) by (fastforce simp: aag_cap_auth_def cap_auth_conferred_def
                              reply_cap_rights_to_auth_def
                       split: if_splits) qed qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
(integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s x) (kheap s' x)

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (2 subgoals):
 1. kheap s' x = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>z. \<lbrakk>integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) z; (integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x))\<^sup>*\<^sup>* z (kheap s' x); z = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
kheap s' x = kheap s x

goal (2 subgoals):
 1. kheap s' x = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>z. \<lbrakk>integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) z; (integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x))\<^sup>*\<^sup>* z (kheap s' x); z = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s' x = kheap s x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s' x = kheap s x
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (1 subgoal):
 1. \<And>z. \<lbrakk>integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) z; (integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x))\<^sup>*\<^sup>* z (kheap s' x); z = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) z; (integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x))\<^sup>*\<^sup>* z (kheap s' x); z = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) z
(integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x))\<^sup>*\<^sup>* z (kheap s' x)
z = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (1 subgoal):
 1. \<And>z. \<lbrakk>integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) z; (integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x))\<^sup>*\<^sup>* z (kheap s' x); z = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) z

goal (1 subgoal):
 1. \<And>z. \<lbrakk>integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) z; (integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x))\<^sup>*\<^sup>* z (kheap s' x); z = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (2 subgoals):
 1. z = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. z \<noteq> kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
z = kheap s x

goal (2 subgoals):
 1. z = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. z \<noteq> kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
z = kheap s x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
z = kheap s x
integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) z
(integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x))\<^sup>*\<^sup>* z (kheap s' x)
z = kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (1 subgoal):
 1. z \<noteq> kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (1 subgoal):
 1. z \<noteq> kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
z \<noteq> kheap s x

goal (1 subgoal):
 1. z \<noteq> kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. z \<noteq> kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. \<And>auth tcb. kheap s x = Some (TCB tcb) \<Longrightarrow> (pasObjectAbs aag x, auth, pasObjectAbs aag x) \<in> pasPolicy aag proof (state)
this:
kheap s x = Some (TCB ?tcb) \<Longrightarrow> (pasObjectAbs aag x, ?auth, pasObjectAbs aag x) \<in> pasPolicy aag

goal (1 subgoal):
 1. z \<noteq> kheap s x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {pasSubject aag} (pasObjectAbs aag x) (kheap s x) z

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (15 subgoals):
 1. pasObjectAbs aag x \<in> {pasSubject aag} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ntfn ntfn' auth sa. \<lbrakk>kheap s x = Some (Notification ntfn); z = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ep ep' auth sa. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' tcb ntfn. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); (tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 15 subgoals... proof (state)
this:
pasObjectAbs aag x \<in> {pasSubject aag}

goal (15 subgoals):
 1. pasObjectAbs aag x \<in> {pasSubject aag} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ntfn ntfn' auth sa. \<lbrakk>kheap s x = Some (Notification ntfn); z = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ep ep' auth sa. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' tcb ntfn. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); (tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 15 subgoals... proof (prove)
using this:
pasObjectAbs aag x \<in> {pasSubject aag}

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (14 subgoals):
 1. \<And>ntfn ntfn' auth sa. \<lbrakk>kheap s x = Some (Notification ntfn); z = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ep ep' auth sa. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ep ep' tcb ntfn. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); (tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 14 subgoals... proof (state)
goal (14 subgoals):
 1. \<And>ntfn ntfn' auth sa. \<lbrakk>kheap s x = Some (Notification ntfn); z = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ep ep' auth sa. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ep ep' tcb ntfn. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); (tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 14 subgoals... proof (state)
this:
kheap s x = Some (Notification ntfn)
z = Some (Notification ntfn')
auth \<in> {Receive, Notify, Reset}
s \<in> {pasSubject aag}
(s, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)

goal (14 subgoals):
 1. \<And>ntfn ntfn' auth sa. \<lbrakk>kheap s x = Some (Notification ntfn); z = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ep ep' auth sa. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ep ep' tcb ntfn. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); (tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 14 subgoals... proof (prove)
using this:
kheap s x = Some (Notification ntfn)
z = Some (Notification ntfn')
auth \<in> {Receive, Notify, Reset}
s \<in> {pasSubject aag}
(s, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (13 subgoals):
 1. \<And>ep ep' auth sa. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ep ep' tcb ntfn. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); (tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 13 subgoals... proof (state)
goal (13 subgoals):
 1. \<And>ep ep' auth sa. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ep ep' tcb ntfn. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); (tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 13 subgoals... proof (state)
this:
kheap s x = Some (Endpoint ep)
z = Some (Endpoint ep')
auth \<in> {Receive, SyncSend, Reset}
s \<in> {pasSubject aag}
(s, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)

goal (13 subgoals):
 1. \<And>ep ep' auth sa. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; sa \<in> {pasSubject aag}; (sa, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ep ep' tcb ntfn. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); (tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 13 subgoals... proof (prove)
using this:
kheap s x = Some (Endpoint ep)
z = Some (Endpoint ep')
auth \<in> {Receive, SyncSend, Reset}
s \<in> {pasSubject aag}
(s, auth, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (12 subgoals):
 1. \<And>ep ep' tcb ntfn. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); (tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 12 subgoals... proof (state)
goal (12 subgoals):
 1. \<And>ep ep' tcb ntfn. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); (tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 12 subgoals... proof (state)
this:
kheap s x = Some (Endpoint ep)
z = Some (Endpoint ep')
(tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
(tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn

goal (12 subgoals):
 1. \<And>ep ep' tcb ntfn. \<lbrakk>kheap s x = Some (Endpoint ep); z = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); (tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 12 subgoals... proof (prove)
using this:
kheap s x = Some (Endpoint ep)
z = Some (Endpoint ep')
(tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
(tcb, Receive, pasObjectAbs aag x) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (11 subgoals):
 1. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 11 subgoals... proof (state)
goal (11 subgoals):
 1. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 11 subgoals... proof (state)
this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>
direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb

goal (11 subgoals):
 1. \<And>tcb tcb' ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 11 subgoals... proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>
direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>
direct_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; receive_blocked_on ep (tcb_state tcb) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<in> pasPolicy aag) \<or> ep_recv_blocked ep (tcb_state tcb) \<and> (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag \<and> tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb)); tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; receive_blocked_on ep (tcb_state tcb) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; ep_recv_blocked ep (tcb_state tcb) \<and> (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag \<and> tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (ep, Receive) \<in> tcb_st_to_auth (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; ep_recv_blocked ep (tcb_state tcb) \<and> (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag \<and> tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (ep, Receive) \<in> tcb_st_to_auth (tcb_state tcb); (pasSubject aag, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ep) \<in> pasPolicy aag; (pasObjectAbs aag x, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; ep_recv_blocked ep (tcb_state tcb) \<and> (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag \<and> tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; ep_recv_blocked ep (tcb_state tcb) \<and> (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag \<and> tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal:
No subgoals! proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (10 subgoals):
 1. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (10 subgoals):
 1. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}
direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)

goal (10 subgoals):
 1. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}; direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}
direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject aag}
direct_call {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>pl. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (4 subgoals):
 1. \<And>pl. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (?l'13 pl, Receive, ?ep13 pl) \<in> pasPolicy aag
 2. \<And>pl. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (?l'13 pl, Write, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<And>pl. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (pasSubject aag, ?auth13 pl, ?ep13 pl) \<in> pasPolicy aag
 4. \<And>pl. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> ?auth13 pl \<in> {SyncSend, Notify, Call} proof (prove)
goal (3 subgoals):
 1. \<And>pl. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Write, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>pl. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (pasSubject aag, ?auth13 pl, pasObjectAbs aag ep) \<in> pasPolicy aag
 3. \<And>pl. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> ?auth13 pl \<in> {SyncSend, Notify, Call} proof (prove)
goal (2 subgoals):
 1. \<And>pl. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (pasSubject aag, ?auth13 pl, pasObjectAbs aag ep) \<in> pasPolicy aag
 2. \<And>pl. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> ?auth13 pl \<in> {SyncSend, Notify, Call} proof (prove)
goal (1 subgoal):
 1. \<And>pl. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; is_subject aag caller; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> Call \<in> {SyncSend, Notify, Call} proof (prove)
goal:
No subgoals! proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (9 subgoals):
 1. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (9 subgoals):
 1. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>
new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st)
awaiting_reply (tcb_state tcb)
aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)

goal (9 subgoals):
 1. \<And>tcb tcb' new_st ctxt'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>
new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st)
awaiting_reply (tcb_state tcb)
aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>
new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st)
awaiting_reply (tcb_state tcb)
aag_subjects_have_auth_to_label {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reply (pasObjectAbs aag x)
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> (\<exists>y. tcb_fault tcb = Some y) \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); (pasSubject aag, Reply, pasObjectAbs aag x) \<in> pasPolicy aag; tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> (\<exists>y. tcb_fault tcb = Some y) \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (8 subgoals):
 1. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (8 subgoals):
 1. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_state := new_st\<rparr>
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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep

goal (8 subgoals):
 1. \<And>tcb tcb' new_st ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; 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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_state := new_st\<rparr>
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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_state := new_st\<rparr>
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 {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (7 subgoals):
 1. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (7 subgoals):
 1. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_state := Restart\<rparr>
blocked_on ep (tcb_state tcb)
aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep

goal (7 subgoals):
 1. \<And>tcb tcb' ep. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_state := Restart\<rparr>
blocked_on ep (tcb_state tcb)
aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_state := Restart\<rparr>
blocked_on ep (tcb_state tcb)
aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (6 subgoals):
 1. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (6 subgoals):
 1. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>
aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))

goal (6 subgoals):
 1. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>
aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>
aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb))
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset (the (tcb_bound_notification tcb)); z \<noteq> kheap s x; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; kheap s x \<noteq> kheap s' x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (5 subgoals):
 1. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (5 subgoals):
 1. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>
reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'

goal (5 subgoals):
 1. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>
reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>
reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) cap'
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>caller R. \<lbrakk>tcb\<lparr>tcb_ctable := NullCap\<rparr> \<noteq> tcb; Some (TCB tcb) \<noteq> kheap s' x; kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_ctable := NullCap\<rparr>)); tcb' = tcb\<lparr>tcb_ctable := NullCap\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) NullCap; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; tcb_ctable tcb = ReplyCap caller False R; is_subject aag caller; cap' = NullCap\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>caller R. \<lbrakk>tcb\<lparr>tcb_ctable := NullCap\<rparr> \<noteq> tcb; Some (TCB tcb) \<noteq> kheap s' x; kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_ctable := NullCap\<rparr>)); tcb' = tcb\<lparr>tcb_ctable := NullCap\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) NullCap; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; tcb_ctable tcb = ReplyCap caller False R; is_subject aag caller; cap' = NullCap\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>caller R. \<lbrakk>tcb\<lparr>tcb_ctable := NullCap\<rparr> \<noteq> tcb; Some (TCB tcb) \<noteq> kheap s' x; kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_ctable := NullCap\<rparr>)); tcb' = tcb\<lparr>tcb_ctable := NullCap\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) NullCap; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; tcb_ctable tcb = ReplyCap caller False R; is_subject aag caller; cap' = NullCap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>caller R. \<lbrakk>tcb\<lparr>tcb_ctable := NullCap\<rparr> \<noteq> tcb; Some (TCB tcb) \<noteq> kheap s' x; kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_ctable := NullCap\<rparr>)); tcb' = tcb\<lparr>tcb_ctable := NullCap\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) NullCap; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; tcb_ctable tcb = ReplyCap caller False R; is_subject aag caller; cap' = NullCap; aag_cap_auth aag (pasObjectAbs aag (fst (x, tcb_cnode_index 0))) (ReplyCap caller False R)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Reply, pasSubject aag) \<in> pasPolicy aag proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (4 subgoals):
 1. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (4 subgoals):
 1. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>
reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'

goal (4 subgoals):
 1. \<And>tcb tcb' cap'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>
reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>
reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_caller := cap'\<rparr>)); tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; tcb_caller tcb = cap' \<or> (\<exists>caller. (\<exists>R. tcb_caller tcb = ReplyCap caller False R) \<and> cap' = NullCap \<and> is_subject aag caller); tcb\<lparr>tcb_caller := cap'\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>caller R. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_caller := NullCap\<rparr>)); tcb' = tcb\<lparr>tcb_caller := NullCap\<rparr>; tcb\<lparr>tcb_caller := NullCap\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; tcb_caller tcb = ReplyCap caller False R; is_subject aag caller; cap' = NullCap\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>caller R. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_caller := NullCap\<rparr>)); tcb' = tcb\<lparr>tcb_caller := NullCap\<rparr>; tcb\<lparr>tcb_caller := NullCap\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; tcb_caller tcb = ReplyCap caller False R; is_subject aag caller; cap' = NullCap\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>caller R. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_caller := NullCap\<rparr>)); tcb' = tcb\<lparr>tcb_caller := NullCap\<rparr>; tcb\<lparr>tcb_caller := NullCap\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; tcb_caller tcb = ReplyCap caller False R; is_subject aag caller; cap' = NullCap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>caller R. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB (tcb\<lparr>tcb_caller := NullCap\<rparr>)); tcb' = tcb\<lparr>tcb_caller := NullCap\<rparr>; tcb\<lparr>tcb_caller := NullCap\<rparr> \<noteq> tcb; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (TCB tcb) \<noteq> kheap s' x; tcb_caller tcb = ReplyCap caller False R; is_subject aag caller; cap' = NullCap; aag_cap_auth aag (pasObjectAbs aag (fst (x, tcb_cnode_index 3))) (ReplyCap caller False R)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Reply, pasSubject aag) \<in> pasPolicy aag proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (3 subgoals):
 1. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (3 subgoals):
 1. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>
tcb_state tcb = Restart
False

goal (3 subgoals):
 1. \<And>tcb tcb'. \<lbrakk>kheap s x = Some (TCB tcb); z = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>; tcb_state tcb = Restart; False\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (TCB tcb)
z = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb), tcb_state := Running\<rparr>
tcb_state tcb = Restart
False

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (2 subgoals):
 1. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (2 subgoals):
 1. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
kheap s x = Some (ArchObj ao)
z = Some (ArchObj ao')
arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'

goal (2 subgoals):
 1. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ao ao'. \<lbrakk>kheap s x = Some (ArchObj ao); z = Some (ArchObj ao'); arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (ArchObj ao)
z = Some (ArchObj ao')
arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (ArchObj ao)
z = Some (ArchObj ao')
arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'
partitionIntegrity aag s s'
pas_refined aag s
invs s
pas_wellformed_noninterference aag
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (1 subgoal):
 1. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (1 subgoal):
 1. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
kheap s x = Some (CNode n content)
z = Some (CNode n content')
cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'

goal (1 subgoal):
 1. \<And>n content content'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (CNode n content)
z = Some (CNode n content')
cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (CNode n content)
z = Some (CNode n content')
cnode_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) content content'
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
kheap s x = Some (CNode n content)
z = Some (CNode n content')
\<forall>l. content l = content' l \<or> (\<exists>cap cap'. content l = Some cap \<and> content' l = Some cap' \<and> reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) cap cap')
z \<noteq> kheap s x
pas_wellformed_noninterference aag
pas_refined aag s
invs s
silc_inv aag st s
kheap s x \<noteq> kheap s' x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); \<forall>l. content l = content' l \<or> (\<exists>cap. content l = Some cap \<and> (\<exists>cap'. content' l = Some cap' \<and> reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) cap cap')); content' \<noteq> content; pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (CNode n content) \<noteq> kheap s' x\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); \<forall>l. content l = content' l \<or> (\<exists>cap. content l = Some cap \<and> (\<exists>cap'. content' l = Some cap' \<and> reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) cap cap')); pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (CNode n content) \<noteq> kheap s' x; \<exists>a. content' a \<noteq> content a\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); \<forall>l. content l = content' l \<or> (\<exists>cap. content l = Some cap \<and> (\<exists>cap'. content' l = Some cap' \<and> reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) cap cap')); pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (CNode n content) \<noteq> kheap s' x; content' l \<noteq> content l\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (CNode n content) \<noteq> kheap s' x; content' l \<noteq> content l; content l = content' l \<or> (\<exists>cap. content l = Some cap \<and> (\<exists>cap'. content' l = Some cap' \<and> reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) cap cap'))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>l cap cap'. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (CNode n content) \<noteq> kheap s' x; cap' \<noteq> cap; content l = Some cap; content' l = Some cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) cap cap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>l caller R. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (CNode n content) \<noteq> kheap s' x; content l = Some (ReplyCap caller False R); content' l = Some NullCap; is_subject aag caller\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>l caller R. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (CNode n content) \<noteq> kheap s' x; content l = Some (ReplyCap caller False R); content' l = Some NullCap; is_subject aag caller\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>l caller R. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (CNode n content) \<noteq> kheap s' x; content l = Some (ReplyCap caller False R); content' l = Some NullCap; is_subject aag caller\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>l caller R. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (CNode n content) \<noteq> kheap s' x; content l = Some (ReplyCap caller False R); content' l = Some NullCap; is_subject aag caller\<rbrakk> \<Longrightarrow> caps_of_state s (x, l) = Some (?cap31 l caller R)
 2. \<And>l caller R. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (CNode n content) \<noteq> kheap s' x; content l = Some (ReplyCap caller False R); content' l = Some NullCap; is_subject aag caller; aag_cap_auth aag (pasObjectAbs aag (fst (x, l))) (?cap31 l caller R)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>l caller R. \<lbrakk>kheap s x = Some (CNode n content); z = Some (CNode n content'); pas_wellformed_noninterference aag; pas_refined aag s; invs s; silc_inv aag st s; Some (CNode n content) \<noteq> kheap s' x; content l = Some (ReplyCap caller False R); content' l = Some NullCap; is_subject aag caller; aag_cap_auth aag (pasObjectAbs aag (fst (x, l))) (ReplyCap caller False R)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Reply, pasSubject aag) \<in> pasPolicy aag proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal:
No subgoals! proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal:
No subgoals! proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal:
No subgoals! proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal:
No subgoals!