theory Access_AC

lemma tsos_tro:
  "\<lbrakk> integrity_obj_state aag activate subjects s s'; tcb_states_of_state s' p = Some a;
     receive_blocked_on ep a; pasObjectAbs aag p \<notin> subjects \<rbrakk>
     \<Longrightarrow> tcb_states_of_state s p = Some a" apply (drule_tac x = p in spec) apply (erule integrity_objE, simp_all add: tcb_states_of_state_def get_tcb_def) by fastforce+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_obj_state aag activate subjects s s'; tcb_states_of_state s' p = Some a; receive_blocked_on ep a; pasObjectAbs aag p \<notin> subjects\<rbrakk> \<Longrightarrow> tcb_states_of_state s p = Some a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_states_of_state s' p = Some a; receive_blocked_on ep a; pasObjectAbs aag p \<notin> subjects; integrity_obj aag activate subjects (pasObjectAbs aag p) (kheap s p) (kheap s' p)\<rbrakk> \<Longrightarrow> tcb_states_of_state s p = Some a proof (prove)
goal (5 subgoals):
 1. \<And>tcb tcb' ccap' cap' ntfn' epa. \<lbrakk>tcb_state tcb' = a; receive_blocked_on ep a; pasObjectAbs aag p \<notin> subjects; 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' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'; direct_send subjects aag epa tcb \<or> indirect_send subjects aag (the (tcb_bound_notification tcb)) epa tcb\<rbrakk> \<Longrightarrow> tcb_state tcb = a
 2. \<And>tcb tcb' ccap' cap' ntfn' caller R epa. \<lbrakk>tcb_state tcb' = a; receive_blocked_on ep a; pasObjectAbs aag p \<notin> subjects; 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 caller \<in> subjects; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'; direct_call subjects aag epa (tcb_state tcb)\<rbrakk> \<Longrightarrow> tcb_state tcb = a
 3. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>tcb_state tcb' = a; receive_blocked_on ep a; pasObjectAbs aag p \<notin> subjects; 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> (\<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' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'; direct_reply subjects aag (pasObjectAbs aag p) tcb\<rbrakk> \<Longrightarrow> tcb_state tcb = a
 4. \<And>tcb tcb' ccap' cap' ntfn' new_st epa. \<lbrakk>new_st = a; receive_blocked_on ep a; pasObjectAbs aag p \<notin> subjects; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_state := a, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_state := a, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; a = Running \<or> inactive a \<and> call_blocked epa (tcb_state tcb) \<or> awaiting_reply a \<and> allowed_call_blocked epa (tcb_state tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'; send_blocked_on epa (tcb_state tcb); aag_subjects_have_auth_to subjects aag Receive epa\<rbrakk> \<Longrightarrow> tcb_state tcb = a
 5. \<And>tcb tcb' ccap' cap' ntfn' new_arch epa. \<lbrakk>receive_blocked_on ep a; pasObjectAbs aag p \<notin> subjects; kheap s p = Some (TCB tcb); kheap s' p = Some (TCB (tcb\<lparr>tcb_arch := new_arch, tcb_state := a, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := a, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; a = Restart \<and> new_arch = tcb_arch tcb \<or> a = 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' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'; blocked_on epa (tcb_state tcb); aag_subjects_have_auth_to subjects aag Reset epa\<rbrakk> \<Longrightarrow> tcb_state tcb = a