theory Noninterference

lemma partitionIntegrity_subjectAffects_mem:
  assumes par_inte: "partitionIntegrity aag s s'"
  assumes pas_ref: "pas_refined aag s"
  assumes invs: "invs s"
  assumes um_diff:
    "underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x"
  notes inte_mem =
    par_inte[THEN partitionIntegrity_integrity, THEN integrity_subjects_mem, THEN spec[where x=x]]
  shows
  "pasObjectAbs aag x \<in> subjectAffects (pasPolicy aag) (pasSubject aag)" using inte_mem proof (cases rule: integrity_mem.cases) case trm_lrefl thus ?thesis by (fastforce intro: affects_lrefl) next case trm_orefl thus ?thesis using um_diff by blast next case trm_write thus ?thesis by (fastforce intro: affects_write) next case trm_globals thus ?thesis by blast next case (trm_ipc p) note trm_ipc_hyps = this then obtain tcbst where "tcb_states_of_state s p = Some tcbst" "can_receive_ipc tcbst" by (force split:option.splits) note hyps = this trm_ipc_hyps(2-)[simplified] pas_ref invs um_diff from par_inte[THEN partitionIntegrity_integrity, THEN integrity_subjects_obj,
                  THEN spec[where x=p], THEN tro_tro_alt] show ?thesis proof (cases rule: integrity_obj_alt.cases) case (tro_alt_tcb_send tcb tcb' ccap' cap' ntfn' 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 auth_ipc_buffers_mem_Write') apply clarsimp apply (rule affects_send[rotated 2]) apply (fastforce intro!: affects_send bound_tcb_at_implies_receive pred_tcb_atI
                              dest: sym) apply (fastforce intro!: auth_ipc_buffers_mem_Write') apply assumption apply blast done next case (tro_alt_tcb_call tcb tcb' ccap' cap' ntfn' caller R 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!: auth_ipc_buffers_mem_Write') apply assumption apply blast done next case (tro_alt_tcb_reply tcb tcb' ccap' cap' ntfn' new_st) thus ?thesis using hyps apply (clarsimp simp: direct_reply_def) apply (erule affects_reply) by (force intro: auth_ipc_buffers_mem_Write') next case (tro_alt_tcb_receive tcb tcb' ccap' cap' ntfn' new_st ep) thus ?thesis using hyps apply (clarsimp elim!: tcb_states_of_state_kheapE send_blocked_on.elims
                               can_receive_ipc.elims) apply (frule (1) pas_refined_tcb_st_to_auth[rotated 2,where auth=Call and ep =ep]) apply force apply (rule affects_reply) apply (erule (1) aag_wellformed_reply, force) apply (fastforce intro!: auth_ipc_buffers_mem_Write') done next case (tro_alt_tcb_restart tcb tcb' ccap' cap' ntfn' 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!: auth_ipc_buffers_mem_Write') qed (insert hyps, force elim: tcb_states_of_state_kheapE)+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
memory_integrity {} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (5 subgoals):
 1. pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) x \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. x \<in> {} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) x \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}

goal (5 subgoals):
 1. pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) x \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. x \<in> {} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) x \<in> {pasSubject (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 (4 subgoals):
 1. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. x \<in> {} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (4 subgoals):
 1. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. x \<in> {} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
underlying_memory (machine_state s) x = underlying_memory (machine_state s') x

goal (4 subgoals):
 1. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. x \<in> {} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
underlying_memory (machine_state s) x = underlying_memory (machine_state s') x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
underlying_memory (machine_state s) x = underlying_memory (machine_state s') x
underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state 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 (3 subgoals):
 1. aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. x \<in> {} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (3 subgoals):
 1. aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. x \<in> {} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x

goal (3 subgoals):
 1. aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write x \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. x \<in> {} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Write 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 (2 subgoals):
 1. x \<in> {} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (2 subgoals):
 1. x \<in> {} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
x \<in> {}

goal (2 subgoals):
 1. x \<in> {} \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
x \<in> {}

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>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
case tcb_states_of_state s p of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s' p = Some Running
x \<in> auth_ipc_buffers s p
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}

goal (1 subgoal):
 1. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
case tcb_states_of_state s p of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s' p = Some Running
x \<in> auth_ipc_buffers s p
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}

goal (1 subgoal):
 1. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (chain)
picking this:
case tcb_states_of_state s p of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s' p = Some Running
x \<in> auth_ipc_buffers s p
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} proof (prove)
using this:
case tcb_states_of_state s p of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s' p = Some Running
x \<in> auth_ipc_buffers s p
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}

goal (1 subgoal):
 1. (\<And>tcbst. \<lbrakk>tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
tcb_states_of_state s p = Some tcbst
can_receive_ipc tcbst

goal (1 subgoal):
 1. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
tcb_states_of_state s p = Some tcbst
can_receive_ipc tcbst
tcb_states_of_state s' p = Some Running
x \<in> auth_ipc_buffers s p
pasObjectAbs aag p \<noteq> pasSubject aag
pas_refined aag s
invs s
underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x

goal (1 subgoal):
 1. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p' \<notin> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (chain)
picking this:
integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) (kheap s p) (kheap s' p) proof (prove)
using this:
integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) (kheap s p) (kheap s' p)

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (14 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' ep. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_send {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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)
 7. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_call {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>tro_tag TCBReply; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_reply {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>tro_tag TCBReceive; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 14 subgoals... proof (state)
this:
tro_tag TCBSend
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
direct_send {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb

goal (14 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' ep. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_send {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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)
 7. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_call {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>tro_tag TCBReply; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_reply {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>tro_tag TCBReceive; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 14 subgoals... proof (prove)
using this:
tro_tag TCBSend
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
direct_send {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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:
tro_tag TCBSend
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
direct_send {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep tcb \<or> indirect_send {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (the (tcb_bound_notification tcb)) ep tcb
tcb_states_of_state s p = Some tcbst
can_receive_ipc tcbst
tcb_states_of_state s' p = Some Running
x \<in> auth_ipc_buffers s p
pasObjectAbs aag p \<noteq> pasSubject aag
pas_refined aag s
invs s
underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; 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_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; 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. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (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. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; 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. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (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 p, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; 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. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; 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. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; ep_recv_blocked ep (tcb_state tcb); (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag; tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (4 subgoals):
 1. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; ep_recv_blocked ep (tcb_state tcb); (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag; tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> (?l'54 ctxt', Receive, ?ep54 ctxt') \<in> pasPolicy aag
 2. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; ep_recv_blocked ep (tcb_state tcb); (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag; tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> (?l'54 ctxt', Write, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; ep_recv_blocked ep (tcb_state tcb); (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag; tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> (pasSubject aag, ?auth54 ctxt', ?ep54 ctxt') \<in> pasPolicy aag
 4. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; ep_recv_blocked ep (tcb_state tcb); (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag; tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> ?auth54 ctxt' \<in> {SyncSend, Notify, Call} proof (prove)
goal (3 subgoals):
 1. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; ep_recv_blocked ep (tcb_state tcb); (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag; tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, Write, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; ep_recv_blocked ep (tcb_state tcb); (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag; tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> (pasSubject aag, ?auth54 ctxt', pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag
 3. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; ep_recv_blocked ep (tcb_state tcb); (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag; tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> ?auth54 ctxt' \<in> {SyncSend, Notify, Call} proof (prove)
goal (2 subgoals):
 1. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; ep_recv_blocked ep (tcb_state tcb); (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag; tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> (pasSubject aag, ?auth54 ctxt', pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag
 2. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; ep_recv_blocked ep (tcb_state tcb); (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag; tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> ?auth54 ctxt' \<in> {SyncSend, Notify, Call} proof (prove)
goal (1 subgoal):
 1. \<And>ctxt'. \<lbrakk>tro_tag TCBSend; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; ep_recv_blocked ep (tcb_state tcb); (pasSubject aag, Notify, pasObjectAbs aag (the (tcb_bound_notification tcb))) \<in> pasPolicy aag; tcb_bound_notification tcb = Some (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> Notify \<in> {SyncSend, Notify, Call} proof (prove)
goal:
No subgoals! proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (13 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_call {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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' ccap' cap' ntfn' new_st. \<lbrakk>tro_tag TCBReply; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_reply {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>tro_tag TCBReceive; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 13 subgoals... proof (state)
goal (13 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_call {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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' ccap' cap' ntfn' new_st. \<lbrakk>tro_tag TCBReply; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_reply {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>tro_tag TCBReceive; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 13 subgoals... proof (state)
this:
tro_tag TCBCall
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
direct_call {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)

goal (13 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_call {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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' ccap' cap' ntfn' new_st. \<lbrakk>tro_tag TCBReply; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_reply {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>tro_tag TCBReceive; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 13 subgoals... proof (prove)
using this:
tro_tag TCBCall
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
direct_call {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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:
tro_tag TCBCall
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) caller \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
direct_call {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ep (tcb_state tcb)
tcb_states_of_state s p = Some tcbst
can_receive_ipc tcbst
tcb_states_of_state s' p = Some Running
x \<in> auth_ipc_buffers s p
pasObjectAbs aag p \<noteq> pasSubject aag
pas_refined aag s
invs s
underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>ctxt' pl. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); is_subject aag caller; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (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>ctxt' pl. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); is_subject aag caller; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (?l'22 ctxt' pl, Receive, ?ep22 ctxt' pl) \<in> pasPolicy aag
 2. \<And>ctxt' pl. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); is_subject aag caller; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (?l'22 ctxt' pl, Write, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<And>ctxt' pl. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); is_subject aag caller; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (pasSubject aag, ?auth22 ctxt' pl, ?ep22 ctxt' pl) \<in> pasPolicy aag
 4. \<And>ctxt' pl. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); is_subject aag caller; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> ?auth22 ctxt' pl \<in> {SyncSend, Notify, Call} proof (prove)
goal (3 subgoals):
 1. \<And>ctxt' pl. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); is_subject aag caller; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, Write, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>ctxt' pl. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); is_subject aag caller; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (pasSubject aag, ?auth22 ctxt' pl, pasObjectAbs aag ep) \<in> pasPolicy aag
 3. \<And>ctxt' pl. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); is_subject aag caller; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> ?auth22 ctxt' pl \<in> {SyncSend, Notify, Call} proof (prove)
goal (2 subgoals):
 1. \<And>ctxt' pl. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); is_subject aag caller; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (pasSubject aag, ?auth22 ctxt' pl, pasObjectAbs aag ep) \<in> pasPolicy aag
 2. \<And>ctxt' pl. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); is_subject aag caller; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> ?auth22 ctxt' pl \<in> {SyncSend, Notify, Call} proof (prove)
goal (1 subgoal):
 1. \<And>ctxt' pl. \<lbrakk>tro_tag TCBCall; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); is_subject aag caller; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (ReplyCap caller False R) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; (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 (12 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>tro_tag TCBReply; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_reply {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>tro_tag TCBReceive; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>tro_tag TCBActivate; kheap s p = Some (TCB tcb); kheap s' p = 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_caller := cap', tcb_ctable := ccap', tcb_state := Running, tcb_bound_notification := ntfn'\<rparr>; tcb_state tcb = Restart; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 12 subgoals... proof (state)
goal (12 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>tro_tag TCBReply; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_reply {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>tro_tag TCBReceive; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>tro_tag TCBActivate; kheap s p = Some (TCB tcb); kheap s' p = 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_caller := cap', tcb_ctable := ccap', tcb_state := Running, tcb_bound_notification := ntfn'\<rparr>; tcb_state tcb = Restart; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 12 subgoals... proof (state)
this:
tro_tag TCBReply
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st)
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
direct_reply {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) tcb

goal (12 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>tro_tag TCBReply; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); \<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; direct_reply {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) tcb\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>tro_tag TCBReceive; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>tro_tag TCBActivate; kheap s p = Some (TCB tcb); kheap s' p = 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_caller := cap', tcb_ctable := ccap', tcb_state := Running, tcb_bound_notification := ntfn'\<rparr>; tcb_state tcb = Restart; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
A total of 12 subgoals... proof (prove)
using this:
tro_tag TCBReply
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st)
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
direct_reply {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) tcb

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
tro_tag TCBReply
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
\<exists>ctxt'. tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st)
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
direct_reply {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) tcb
tcb_states_of_state s p = Some tcbst
can_receive_ipc tcbst
tcb_states_of_state s' p = Some Running
x \<in> auth_ipc_buffers s p
pasObjectAbs aag p \<noteq> pasSubject aag
pas_refined aag s
invs s
underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>ctxt'. \<lbrakk>tro_tag TCBReply; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); new_st = Running \<or> (\<exists>y. tcb_fault tcb = Some y) \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; awaiting_reply (tcb_state tcb) \<or> (\<exists>ep. allowed_call_blocked ep (tcb_state tcb) \<and> (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag); (pasSubject aag, Reply, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>ctxt'. \<lbrakk>tro_tag TCBReply; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); new_st = Running \<or> (\<exists>y. tcb_fault tcb = Some y) \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_states_of_state s p = Some tcbst; can_receive_ipc tcbst; tcb_states_of_state s' p = Some Running; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; awaiting_reply (tcb_state tcb) \<or> (\<exists>ep. allowed_call_blocked ep (tcb_state tcb) \<and> (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (11 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>tro_tag TCBReceive; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>tro_tag TCBActivate; kheap s p = Some (TCB tcb); kheap s' p = 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_caller := cap', tcb_ctable := ccap', tcb_state := Running, tcb_bound_notification := ntfn'\<rparr>; tcb_state tcb = Restart; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>n content content'. \<lbrakk>tro_tag RCNode; kheap s p = Some (CNode n content); kheap s' p = Some (CNode n content'); cnode_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>tro_tag TCBReceive; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>tro_tag TCBActivate; kheap s p = Some (TCB tcb); kheap s' p = 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_caller := cap', tcb_ctable := ccap', tcb_state := Running, tcb_bound_notification := ntfn'\<rparr>; tcb_state tcb = Restart; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>n content content'. \<lbrakk>tro_tag RCNode; kheap s p = Some (CNode n content); kheap s' p = Some (CNode n content'); cnode_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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:
tro_tag TCBReceive
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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)
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
send_blocked_on ep (tcb_state tcb)
aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep

goal (11 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>tro_tag TCBReceive; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>tro_tag TCBActivate; kheap s p = Some (TCB tcb); kheap s' p = 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_caller := cap', tcb_ctable := ccap', tcb_state := Running, tcb_bound_notification := ntfn'\<rparr>; tcb_state tcb = Restart; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 10. \<And>n content content'. \<lbrakk>tro_tag RCNode; kheap s p = Some (CNode n content); kheap s' p = Some (CNode n content'); cnode_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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:
tro_tag TCBReceive
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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)
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
send_blocked_on ep (tcb_state tcb)
aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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:
tro_tag TCBReceive
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<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)
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
send_blocked_on ep (tcb_state tcb)
aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Receive ep
tcb_states_of_state s p = Some tcbst
can_receive_ipc tcbst
tcb_states_of_state s' p = Some Running
x \<in> auth_ipc_buffers s p
pasObjectAbs aag p \<noteq> pasSubject aag
pas_refined aag s
invs s
underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x

goal (1 subgoal):
 1. subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>uu_. \<lbrakk>tro_tag TCBReceive; tcb' = tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb_state tcb = BlockedOnSend ep uu_; kheap s p = Some (TCB tcb); tcbst = BlockedOnSend ep uu_; kheap s' p = Some (TCB (tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); new_st = Running; sender_is_call uu_; sender_can_call uu_\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<And>uu_. \<lbrakk>tro_tag TCBReceive; tcb' = tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb_state tcb = BlockedOnSend ep uu_; kheap s p = Some (TCB tcb); tcbst = BlockedOnSend ep uu_; kheap s' p = Some (TCB (tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); new_st = Running; sender_is_call uu_; sender_can_call uu_\<rbrakk> \<Longrightarrow> (ep, Call) \<in> tcb_st_to_auth (tcb_state tcb)
 2. \<And>uu_. \<lbrakk>tro_tag TCBReceive; tcb' = tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb_state tcb = BlockedOnSend ep uu_; kheap s p = Some (TCB tcb); tcbst = BlockedOnSend ep uu_; kheap s' p = Some (TCB (tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); new_st = Running; sender_is_call uu_; sender_can_call uu_; (pasObjectAbs aag p, Call, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>uu_. \<lbrakk>tro_tag TCBReceive; tcb' = tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb_state tcb = BlockedOnSend ep uu_; kheap s p = Some (TCB tcb); tcbst = BlockedOnSend ep uu_; kheap s' p = Some (TCB (tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); new_st = Running; sender_is_call uu_; sender_can_call uu_; (pasObjectAbs aag p, Call, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (2 subgoals):
 1. \<And>uu_. \<lbrakk>tro_tag TCBReceive; tcb' = tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb_state tcb = BlockedOnSend ep uu_; kheap s p = Some (TCB tcb); tcbst = BlockedOnSend ep uu_; kheap s' p = Some (TCB (tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); new_st = Running; sender_is_call uu_; sender_can_call uu_; (pasObjectAbs aag p, Call, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Reply, ?l'46 uu_) \<in> pasPolicy aag
 2. \<And>uu_. \<lbrakk>tro_tag TCBReceive; tcb' = tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb_state tcb = BlockedOnSend ep uu_; kheap s p = Some (TCB tcb); tcbst = BlockedOnSend ep uu_; kheap s' p = Some (TCB (tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); new_st = Running; sender_is_call uu_; sender_can_call uu_; (pasObjectAbs aag p, Call, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (?l'46 uu_, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>uu_. \<lbrakk>tro_tag TCBReceive; tcb' = tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; x \<in> auth_ipc_buffers s p; pasObjectAbs aag p \<noteq> pasSubject aag; pas_refined aag s; invs s; underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state s') x; tcb_state tcb = BlockedOnSend ep uu_; kheap s p = Some (TCB tcb); tcbst = BlockedOnSend ep uu_; kheap s' p = Some (TCB (tcb\<lparr>tcb_state := Running, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); new_st = Running; sender_is_call uu_; sender_can_call uu_; (pasObjectAbs aag p, Call, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, Write, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal:
No subgoals! proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal (10 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>tro_tag TCBActivate; kheap s p = Some (TCB tcb); kheap s' p = 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_caller := cap', tcb_ctable := ccap', tcb_state := Running, tcb_bound_notification := ntfn'\<rparr>; tcb_state tcb = Restart; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>n content content'. \<lbrakk>tro_tag RCNode; kheap s p = Some (CNode n content); kheap s' p = Some (CNode n content'); cnode_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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>tro_tag RArch; kheap s p = Some (ArchObj ao); kheap s' p = Some (ArchObj ao'); arch_integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
goal (10 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>tro_tag TCBActivate; kheap s p = Some (TCB tcb); kheap s' p = 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_caller := cap', tcb_ctable := ccap', tcb_state := Running, tcb_bound_notification := ntfn'\<rparr>; tcb_state tcb = Restart; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>n content content'. \<lbrakk>tro_tag RCNode; kheap s p = Some (CNode n content); kheap s' p = Some (CNode n content'); cnode_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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>tro_tag RArch; kheap s p = Some (ArchObj ao); kheap s' p = Some (ArchObj ao'); arch_integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
tro_tag TCBRestart
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := ep, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
tcb_state tcb' = Restart \<and> ep = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> ep = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb)
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
blocked_on ep_ (tcb_state tcb)
aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep_

goal (10 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>tro_tag TCBRestart; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_state tcb' = Restart \<and> new_arch = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>tro_tag TCBActivate; kheap s p = Some (TCB tcb); kheap s' p = 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_caller := cap', tcb_ctable := ccap', tcb_state := Running, tcb_bound_notification := ntfn'\<rparr>; tcb_state tcb = Restart; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 9. \<And>n content content'. \<lbrakk>tro_tag RCNode; kheap s p = Some (CNode n content); kheap s' p = Some (CNode n content'); cnode_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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>tro_tag RArch; kheap s p = Some (ArchObj ao); kheap s' p = Some (ArchObj ao'); arch_integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
using this:
tro_tag TCBRestart
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := ep, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
tcb_state tcb' = Restart \<and> ep = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> ep = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb)
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
blocked_on ep_ (tcb_state tcb)
aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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:
tro_tag TCBRestart
kheap s p = Some (TCB tcb)
kheap s' p = Some (TCB tcb')
tcb' = tcb\<lparr>tcb_arch := ep, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>
tcb_state tcb' = Restart \<and> ep = tcb_arch tcb \<or> tcb_state tcb' = Running \<and> ep = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb)
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'
reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'
blocked_on ep_ (tcb_state tcb)
aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Reset ep_
tcb_states_of_state s p = Some tcbst
can_receive_ipc tcbst
tcb_states_of_state s' p = Some Running
x \<in> auth_ipc_buffers s p
pasObjectAbs aag p \<noteq> pasSubject aag
pas_refined aag s
invs s
underlying_memory (machine_state s) x \<noteq> underlying_memory (machine_state 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 (9 subgoals):
 1. \<lbrakk>tro_tag LRefl; pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p \<in> {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)}\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 2. \<lbrakk>tro_tag ORefl; kheap s p = kheap s' p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag RNtfn; kheap s p = Some (Notification ntfn); kheap s' p = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 4. \<And>ep ep' auth. \<lbrakk>tro_tag REp; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) auth p\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 5. \<And>ep ep'. \<lbrakk>tro_tag EpUnblock; kheap s p = Some (Endpoint ep); kheap s' p = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) ntfn) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> (tcb, Receive, pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) \<in> pasPolicy (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) \<and> aag_subjects_have_auth_to {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Notify ntfn\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 6. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag TCBGeneric; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 7. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>tro_tag TCBActivate; kheap s p = Some (TCB tcb); kheap s' p = 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_caller := cap', tcb_ctable := ccap', tcb_state := Running, tcb_bound_notification := ntfn'\<rparr>; tcb_state tcb = Restart; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_caller tcb) cap'; reply_cap_deletion_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>); pasMayActivate (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)
 8. \<And>n content content'. \<lbrakk>tro_tag RCNode; kheap s p = Some (CNode n content); kheap s' p = Some (CNode n content'); cnode_integrity {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (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>tro_tag RArch; kheap s p = Some (ArchObj ao); kheap s' p = Some (ArchObj ao'); arch_integrity_obj_alt (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)} (pasObjectAbs (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) p) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (state)
this:
subject_can_affect_label_directly aag (pasObjectAbs aag x)

goal:
No subgoals!