theory Access_AC

lemma tro_alt_trans_spec: (* this takes a long time to process *)
  "\<lbrakk> integrity_obj_alt aag activate es subjects ko ko';
     integrity_obj_alt aag activate es subjects ko' ko'' \<rbrakk>
     \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''" 
  (* We need to consider nearly 200 cases, one for each possible pair
     of integrity steps. We use the tro_tags to select subsets of goals
     that can be solved by the same method. *)

  (* Expand the first integrity step *)
   apply (erule integrity_obj_alt.cases[where ko=ko and ko'=ko']) 

  (* LRefl and ORefl trivially collapse into the second integrity step *)
   apply (find_goal \<open>match premises in "tro_tag LRefl" \<Rightarrow> -\<close>) subgoal by (rule tro_alt_lrefl, simp) apply (find_goal \<open>match premises in "tro_tag ORefl" \<Rightarrow> -\<close>) subgoal by simp 

  (* Now re-tag the first step with tro_tag' *)
   apply (all \<open>simp only:tro_tag_to_prime\<close>) 
  (* Expand the second integrity step, which will be tagged with tro_tag *)
   apply (all \<open>erule integrity_obj_alt.cases\<close>) 

  (* There are some special cases that would be too slow or unsolvable by the bulk tactics.
     We move them up here and solve manually *)
   apply (find_goal \<open>match premises in "tro_tag' TCBReply" and "tro_tag TCBActivate" \<Rightarrow> -\<close>) apply (clarsimp, rule tro_alt_tcb_reply[OF tro_tagI refl refl],
         (rule exI; rule tcb.equality; simp); fastforce) apply (find_goal \<open>match premises in "tro_tag' TCBReceive" and "tro_tag TCBReply" \<Rightarrow> -\<close>) apply (clarsimp, rule tro_alt_tcb_reply[OF tro_tagI refl refl],
         (rule exI; rule tcb.equality; simp);
          fastforce simp: direct_reply_def allowed_call_blocked_def) apply (find_goal \<open>match premises in "tro_tag TCBGeneric" and "tro_tag' TCBRestart" \<Rightarrow> -\<close>) subgoal apply (erule integrity_obj_alt.intros[simplified tro_tag_to_prime]) apply (simp | rule tcb.equality | fastforce)+ done apply (find_goal \<open>match premises in "tro_tag TCBActivate" and "tro_tag' TCBRestart" \<Rightarrow> -\<close>) apply (rule tro_alt_tcb_restart[OF tro_tagI], (fastforce simp: tcb.splits fun_upd_def)+)[1] apply (find_goal \<open>match premises in "tro_tag REp" and "tro_tag' REp" \<Rightarrow> -\<close>) subgoal by (erule integrity_obj_alt.intros, (rule refl | assumption)+) 

  (* Select groups of subgoals by tag, then solve with the given methods *)
   apply (all \<open>fails \<open>erule thin_rl[of "tro_tag LRefl"]\<close>
             | time_methods \<open>fastforce intro: tro_alt_lrefl\<close>\<close>) apply (all \<open>fails \<open>erule thin_rl[of "tro_tag ORefl"]\<close>
             | time_methods \<open>solves \<open>
                   drule sym[where t="ko''"];
                   erule integrity_obj_alt.intros[simplified tro_tag_to_prime];
                   solves \<open>simp\<close>\<close>\<close>\<close>) apply (all \<open>fails \<open>erule thin_rl[of "tro_tag RNtfn"] thin_rl[of "tro_tag' RNtfn"]\<close>
             | time_methods \<open>fastforce intro: tro_alt_ntfn\<close>\<close>) apply (all \<open>fails \<open>erule thin_rl[of "tro_tag REp"]
                    | erule thin_rl[of "tro_tag' REp"]
                    | erule thin_rl[of "tro_tag RArch"]
                    | erule thin_rl[of "tro_tag' RArch"]
                    | erule thin_rl[of "tro_tag EpUnblock"]
                    | erule thin_rl[of "tro_tag' EpUnblock"]
                    | erule thin_rl[of "tro_tag RCNode"]
                    | erule thin_rl[of "tro_tag' RCNode"]\<close>
             | time_methods \<open>fastforce intro: integrity_obj_alt.intros
                                        simp: arch_tro_alt_trans_spec\<close>\<close>) 

  (* TCB-TCB steps, somewhat slow *)
   apply (all \<open>fails \<open>erule thin_rl[of "tro_tag TCBGeneric"]\<close>
             | time_methods \<open>solves \<open>
                    erule integrity_obj_alt.intros[simplified tro_tag_to_prime],
                    (assumption | rule refl
                    | ((erule exE)+)?, (rule exI)?, force intro: tcb.equality)+\<close>\<close>\<close>) apply (all \<open>fails \<open>erule thin_rl[of "tro_tag' TCBGeneric"]\<close>
             | time_methods \<open>solves \<open>
                    erule integrity_obj_alt.intros,
                    (assumption | rule refl
                    | (elim exE)?, (intro exI)?, fastforce intro: tcb.equality
                    | fastforce simp: indirect_send_def direct_send_def direct_call_def direct_reply_def
                                dest: tcb_bound_notification_reset_eq_or_none)+\<close>\<close>\<close>) apply (time_methods \<open>
           succeeds \<open>match premises in T: "tro_tag _" and T': "tro_tag' _" \<Rightarrow>
                                       \<open>print_fact T, print_fact T'\<close>\<close>,
           fastforce intro: integrity_obj_alt.intros tcb.equality
                     simp: indirect_send_def direct_send_def direct_call_def direct_reply_def
                           call_blocked_def allowed_call_blocked_def\<close>)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_obj_alt aag activate es subjects ko ko'; integrity_obj_alt aag activate es subjects ko' ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_obj_alt aag activate es subjects ko ko'; integrity_obj_alt aag activate es subjects ko' ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko'' proof (prove)
goal (14 subgoals):
 1. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 2. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag ORefl; ko = ko'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 3. \<And>ntfn ntfn' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 4. \<And>ep ep' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 5. \<And>ep ep'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag EpUnblock; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReply; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 9. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReceive; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 10. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBRestart; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 2. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag ORefl; ko = ko'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 3. \<And>ntfn ntfn' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 4. \<And>ep ep' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 5. \<And>ep ep'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag EpUnblock; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReply; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 9. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReceive; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 10. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBRestart; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 2. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag ORefl; ko = ko'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 3. \<And>ntfn ntfn' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 4. \<And>ep ep' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 5. \<And>ep ep'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag EpUnblock; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReply; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 9. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReceive; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 10. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBRestart; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
A total of 14 subgoals... proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko'' proof (prove)
goal (13 subgoals):
 1. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag ORefl; ko = ko'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 3. \<And>ep ep' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 4. \<And>ep ep'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag EpUnblock; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 5. \<And>tcb tcb' ccap' cap' ntfn' ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReply; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReceive; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 9. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBRestart; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 10. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBGeneric; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag ORefl; ko = ko'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 3. \<And>ep ep' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 4. \<And>ep ep'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag EpUnblock; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 5. \<And>tcb tcb' ccap' cap' ntfn' ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReply; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReceive; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 9. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBRestart; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 10. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBGeneric; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
A total of 13 subgoals... proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag ORefl; ko = ko'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko'' proof (prove)
goal (12 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 2. \<And>ep ep' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 3. \<And>ep ep'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag EpUnblock; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 4. \<And>tcb tcb' ccap' cap' ntfn' ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 5. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReply; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReceive; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBRestart; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 9. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBGeneric; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 10. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBActivate; ko = Some (TCB tcb); ko' = 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 es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 2. \<And>ep ep' auth. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 3. \<And>ep ep'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag EpUnblock; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 4. \<And>tcb tcb' ccap' cap' ntfn' ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 5. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReply; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBReceive; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBRestart; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 9. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBGeneric; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
 10. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>integrity_obj_alt aag activate es subjects ko' ko''; tro_tag TCBActivate; ko = Some (TCB tcb); ko' = 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 es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (Notification ntfn')) ko''; tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ep ep' auth. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (Endpoint ep')) ko''; tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 3. \<And>ep ep'. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (Endpoint ep')) ko''; tro_tag' EpUnblock; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 4. \<And>tcb tcb' ccap' cap' ntfn' ep. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB tcb')) ko''; tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 5. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB tcb')) ko''; tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB tcb')) ko''; tro_tag' TCBReply; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB (tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) ko''; tro_tag' TCBReceive; ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB tcb')) ko''; tro_tag' TCBRestart; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 9. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) ko''; tro_tag' TCBGeneric; ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 10. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>integrity_obj_alt aag True es subjects (Some (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>))) ko''; tro_tag' TCBActivate; ko = Some (TCB tcb); ko' = Some (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' = 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 es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag True es subjects (Some (TCB tcb)) ko''
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (Notification ntfn')) ko''; tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ep ep' auth. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (Endpoint ep')) ko''; tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 3. \<And>ep ep'. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (Endpoint ep')) ko''; tro_tag' EpUnblock; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 4. \<And>tcb tcb' ccap' cap' ntfn' ep. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB tcb')) ko''; tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 5. \<And>tcb tcb' ccap' cap' ntfn' caller R ep. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB tcb')) ko''; tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB tcb')) ko''; tro_tag' TCBReply; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' new_st ep. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB (tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) ko''; tro_tag' TCBReceive; ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB tcb')) ko''; tro_tag' TCBRestart; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 9. \<And>tcb tcb' ccap' cap' ntfn'. \<lbrakk>integrity_obj_alt aag activate es subjects (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) ko''; tro_tag' TCBGeneric; ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 10. \<And>tcb tcb' ntfn' ccap' cap'. \<lbrakk>integrity_obj_alt aag True es subjects (Some (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>))) ko''; tro_tag' TCBActivate; ko = Some (TCB tcb); ko' = Some (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' = 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 es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag True es subjects (Some (TCB tcb)) ko''
A total of 12 subgoals... proof (prove)
goal (168 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_arch ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBRestart; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 168 subgoals... proof (prove)
goal (168 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_arch ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBRestart; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 168 subgoals... proof (prove)
goal (168 subgoals):
 1. \<And>tcb tcb' ccap' cap' ntfn' new_st tcba tcb'a ntfn'a ccap'a cap'a. \<lbrakk>tro_tag' TCBReply; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb; tro_tag TCBActivate; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcba))) (tcb_arch tcba), tcb_caller := cap'a, tcb_ctable := ccap'a, tcb_state := Running, tcb_bound_notification := ntfn'a\<rparr>; tcb_state tcba = Restart; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 168 subgoals... proof (prove)
goal (167 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_arch ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBRestart; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 167 subgoals... proof (prove)
goal (167 subgoals):
 1. \<And>tcb tcb' ccap' cap' ntfn' new_st ep tcba tcb'a ccap'a cap'a ntfn'a new_sta. \<lbrakk>tro_tag' TCBReceive; ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep; tro_tag TCBReply; Some (TCB (tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)) = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := new_sta, tcb_fault := None, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_sta = Running \<or> tcb_fault tcba \<noteq> None \<and> (new_sta = Restart \<or> inactive new_sta); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_reply es aag subjects tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 167 subgoals... proof (prove)
goal (166 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_arch ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBRestart; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 166 subgoals... proof (prove)
goal (166 subgoals):
 1. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep tcba tcb'a ccap'a cap'a ntfn'a. \<lbrakk>tro_tag' TCBRestart; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep; tro_tag TCBGeneric; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 166 subgoals... proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tro_tag' TCBRestart; ko = Some (TCB tcb_); ko' = 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'_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb_) cap'_; reply_cap_deletion_integrity es aag (tcb_ctable tcb_) ccap'_; blocked_on ep_ (tcb_state tcb_); aag_subjects_have_auth_to es aag Reset ep_; tro_tag TCBGeneric; Some (TCB tcb'_) = Some (TCB tcba_); ko'' = Some (TCB tcb'a_); tcb'a_ = tcba_\<lparr>tcb_bound_notification := ntfn'a_, tcb_caller := cap'a_, tcb_ctable := ccap'a_\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba_) ntfn'a_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba_) cap'a_; reply_cap_deletion_integrity es aag (tcb_ctable tcba_) ccap'a_\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb_)) ko'' proof (prove)
goal (9 subgoals):
 1. \<lbrakk>ko = Some (TCB tcb_); ko' = 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'_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb_) cap'_; reply_cap_deletion_integrity es aag (tcb_ctable tcb_) ccap'_; blocked_on ep_ (tcb_state tcb_); aag_subjects_have_auth_to es aag Reset ep_; tro_tag TCBGeneric; Some (TCB tcb'_) = Some (TCB tcba_); ko'' = Some (TCB tcb'a_); tcb'a_ = tcba_\<lparr>tcb_bound_notification := ntfn'a_, tcb_caller := cap'a_, tcb_ctable := ccap'a_\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba_) ntfn'a_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba_) cap'a_; reply_cap_deletion_integrity es aag (tcb_ctable tcba_) ccap'a_\<rbrakk> \<Longrightarrow> Some (TCB tcb_) = Some (TCB ?tcb)
 2. \<lbrakk>ko = Some (TCB tcb_); ko' = 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'_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb_) cap'_; reply_cap_deletion_integrity es aag (tcb_ctable tcb_) ccap'_; blocked_on ep_ (tcb_state tcb_); aag_subjects_have_auth_to es aag Reset ep_; tro_tag TCBGeneric; Some (TCB tcb'_) = Some (TCB tcba_); ko'' = Some (TCB tcb'a_); tcb'a_ = tcba_\<lparr>tcb_bound_notification := ntfn'a_, tcb_caller := cap'a_, tcb_ctable := ccap'a_\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba_) ntfn'a_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba_) cap'a_; reply_cap_deletion_integrity es aag (tcb_ctable tcba_) ccap'a_\<rbrakk> \<Longrightarrow> ko'' = Some (TCB ?tcb')
 3. \<lbrakk>ko = Some (TCB tcb_); ko' = 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'_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb_) cap'_; reply_cap_deletion_integrity es aag (tcb_ctable tcb_) ccap'_; blocked_on ep_ (tcb_state tcb_); aag_subjects_have_auth_to es aag Reset ep_; tro_tag TCBGeneric; Some (TCB tcb'_) = Some (TCB tcba_); ko'' = Some (TCB tcb'a_); tcb'a_ = tcba_\<lparr>tcb_bound_notification := ntfn'a_, tcb_caller := cap'a_, tcb_ctable := ccap'a_\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba_) ntfn'a_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba_) cap'a_; reply_cap_deletion_integrity es aag (tcb_ctable tcba_) ccap'a_\<rbrakk> \<Longrightarrow> ?tcb' = ?tcb\<lparr>tcb_arch := ?new_arch, tcb_state := tcb_state ?tcb', tcb_bound_notification := ?ntfn', tcb_caller := ?cap', tcb_ctable := ?ccap'\<rparr>
 4. \<lbrakk>ko = Some (TCB tcb_); ko' = 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'_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb_) cap'_; reply_cap_deletion_integrity es aag (tcb_ctable tcb_) ccap'_; blocked_on ep_ (tcb_state tcb_); aag_subjects_have_auth_to es aag Reset ep_; tro_tag TCBGeneric; Some (TCB tcb'_) = Some (TCB tcba_); ko'' = Some (TCB tcb'a_); tcb'a_ = tcba_\<lparr>tcb_bound_notification := ntfn'a_, tcb_caller := cap'a_, tcb_ctable := ccap'a_\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba_) ntfn'a_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba_) cap'a_; reply_cap_deletion_integrity es aag (tcb_ctable tcba_) ccap'a_\<rbrakk> \<Longrightarrow> 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)
 5. \<lbrakk>ko = Some (TCB tcb_); ko' = 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'_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb_) cap'_; reply_cap_deletion_integrity es aag (tcb_ctable tcb_) ccap'_; blocked_on ep_ (tcb_state tcb_); aag_subjects_have_auth_to es aag Reset ep_; tro_tag TCBGeneric; Some (TCB tcb'_) = Some (TCB tcba_); ko'' = Some (TCB tcb'a_); tcb'a_ = tcba_\<lparr>tcb_bound_notification := ntfn'a_, tcb_caller := cap'a_, tcb_ctable := ccap'a_\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba_) ntfn'a_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba_) cap'a_; reply_cap_deletion_integrity es aag (tcb_ctable tcba_) ccap'a_\<rbrakk> \<Longrightarrow> tcb_bound_notification_reset_integrity (tcb_bound_notification ?tcb) ?ntfn' es aag
 6. \<lbrakk>ko = Some (TCB tcb_); ko' = 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'_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb_) cap'_; reply_cap_deletion_integrity es aag (tcb_ctable tcb_) ccap'_; blocked_on ep_ (tcb_state tcb_); aag_subjects_have_auth_to es aag Reset ep_; tro_tag TCBGeneric; Some (TCB tcb'_) = Some (TCB tcba_); ko'' = Some (TCB tcb'a_); tcb'a_ = tcba_\<lparr>tcb_bound_notification := ntfn'a_, tcb_caller := cap'a_, tcb_ctable := ccap'a_\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba_) ntfn'a_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba_) cap'a_; reply_cap_deletion_integrity es aag (tcb_ctable tcba_) ccap'a_\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity es aag (tcb_caller ?tcb) ?cap'
 7. \<lbrakk>ko = Some (TCB tcb_); ko' = 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'_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb_) cap'_; reply_cap_deletion_integrity es aag (tcb_ctable tcb_) ccap'_; blocked_on ep_ (tcb_state tcb_); aag_subjects_have_auth_to es aag Reset ep_; tro_tag TCBGeneric; Some (TCB tcb'_) = Some (TCB tcba_); ko'' = Some (TCB tcb'a_); tcb'a_ = tcba_\<lparr>tcb_bound_notification := ntfn'a_, tcb_caller := cap'a_, tcb_ctable := ccap'a_\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba_) ntfn'a_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba_) cap'a_; reply_cap_deletion_integrity es aag (tcb_ctable tcba_) ccap'a_\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity es aag (tcb_ctable ?tcb) ?ccap'
 8. \<lbrakk>ko = Some (TCB tcb_); ko' = 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'_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb_) cap'_; reply_cap_deletion_integrity es aag (tcb_ctable tcb_) ccap'_; blocked_on ep_ (tcb_state tcb_); aag_subjects_have_auth_to es aag Reset ep_; tro_tag TCBGeneric; Some (TCB tcb'_) = Some (TCB tcba_); ko'' = Some (TCB tcb'a_); tcb'a_ = tcba_\<lparr>tcb_bound_notification := ntfn'a_, tcb_caller := cap'a_, tcb_ctable := ccap'a_\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba_) ntfn'a_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba_) cap'a_; reply_cap_deletion_integrity es aag (tcb_ctable tcba_) ccap'a_\<rbrakk> \<Longrightarrow> blocked_on ?ep (tcb_state ?tcb)
 9. \<lbrakk>ko = Some (TCB tcb_); ko' = 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'_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb_) cap'_; reply_cap_deletion_integrity es aag (tcb_ctable tcb_) ccap'_; blocked_on ep_ (tcb_state tcb_); aag_subjects_have_auth_to es aag Reset ep_; tro_tag TCBGeneric; Some (TCB tcb'_) = Some (TCB tcba_); ko'' = Some (TCB tcb'a_); tcb'a_ = tcba_\<lparr>tcb_bound_notification := ntfn'a_, tcb_caller := cap'a_, tcb_ctable := ccap'a_\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba_) ntfn'a_ es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba_) cap'a_; reply_cap_deletion_integrity es aag (tcb_ctable tcba_) ccap'a_\<rbrakk> \<Longrightarrow> aag_subjects_have_auth_to es aag Reset ?ep proof (prove)
goal:
No subgoals! proof (prove)
goal (165 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_arch ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBRestart; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 165 subgoals... proof (prove)
goal (165 subgoals):
 1. \<And>tcb tcb' ccap' cap' ntfn' new_arch ep tcba tcb'a ntfn'a ccap'a cap'a. \<lbrakk>tro_tag' TCBRestart; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep; tro_tag TCBActivate; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcba))) (tcb_arch tcba), tcb_caller := cap'a, tcb_ctable := ccap'a, tcb_state := Running, tcb_bound_notification := ntfn'a\<rparr>; tcb_state tcba = Restart; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 165 subgoals... proof (prove)
goal (164 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_arch ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBRestart; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 164 subgoals... proof (prove)
goal (164 subgoals):
 1. \<And>ep ep' auth epa ep'a autha. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Endpoint ep') = Some (Endpoint epa); ko'' = Some (Endpoint ep'a); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 164 subgoals... proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep_); ko' = Some (Endpoint ep'_); auth_ \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth_ subjects; tro_tag REp; Some (Endpoint ep'_) = Some (Endpoint epa_); ko'' = Some (Endpoint ep'a_); autha_ \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha_ subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep_)) ko'' proof (prove)
goal (163 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_arch ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBRestart; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 163 subgoals... proof (prove)
goal (163 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag LRefl; subjects \<in> es\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_arch ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBRestart; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 163 subgoals... proof (prove)
goal (151 subgoals):
 1. \<And>ntfn ntfn' auth. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag ORefl; Some (Notification ntfn') = ko''\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_arch ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBRestart; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBGeneric; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 151 subgoals... proof (prove)
goal (139 subgoals):
 1. \<And>ntfn ntfn' auth ntfna ntfn'a autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RNtfn; Some (Notification ntfn') = Some (Notification ntfna); ko'' = Some (Notification ntfn'a); autha \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 2. \<And>ntfn ntfn' auth ep ep' autha. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag REp; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); autha \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag autha subjects\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 3. \<And>ntfn ntfn' auth ep ep'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Notification ntfn') = Some (Endpoint ep); ko'' = Some (Endpoint ep'); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 4. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 5. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a caller R ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 6. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 7. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_st ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 8. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a new_arch ep. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBRestart; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb', tcb_bound_notification := ntfn'a, 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'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to es aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 9. \<And>ntfn ntfn' auth tcb tcb' ccap' cap' ntfn'a. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBGeneric; Some (Notification ntfn') = Some (TCB tcb); ko'' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn'a, tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
 10. \<And>ntfn ntfn' auth tcb tcb' ntfn'a ccap' cap'. \<lbrakk>tro_tag' RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBActivate; Some (Notification ntfn') = Some (TCB tcb); ko'' = 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'a\<rparr>; tcb_state tcb = Restart; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn'a es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Notification ntfn)) ko''
A total of 139 subgoals... proof (prove)
goal (116 subgoals):
 1. \<And>ep ep' auth epa ep'a. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag EpUnblock; Some (Endpoint ep') = Some (Endpoint epa); ko'' = Some (Endpoint ep'a); \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> (tcb, Receive, subjects) \<in> pasPolicy aag \<and> aag_subjects_have_auth_to es aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 2. \<And>ep ep' auth tcb tcb' ccap' cap' ntfn' epa. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBSend; Some (Endpoint ep') = Some (TCB tcb); ko'' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag epa tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) epa tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 3. \<And>ep ep' auth tcb tcb' ccap' cap' ntfn' caller R epa. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBCall; Some (Endpoint ep') = Some (TCB tcb); ko'' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag epa (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 4. \<And>ep ep' auth tcb tcb' ccap' cap' ntfn' new_st. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReply; Some (Endpoint ep') = Some (TCB tcb); ko'' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_reply es aag subjects tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 5. \<And>ep ep' auth tcb tcb' ccap' cap' ntfn' new_st epa. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBReceive; Some (Endpoint ep') = Some (TCB tcb); ko'' = 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 epa (tcb_state tcb) \<or> awaiting_reply new_st \<and> allowed_call_blocked epa (tcb_state tcb); tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; send_blocked_on epa (tcb_state tcb); aag_subjects_have_auth_to es aag Receive epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 6. \<And>ep ep' auth tcb tcb' ccap' cap' ntfn' new_arch epa. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBRestart; Some (Endpoint ep') = Some (TCB tcb); ko'' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; blocked_on epa (tcb_state tcb); aag_subjects_have_auth_to es aag Reset epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 7. \<And>ep ep' auth tcb tcb' ccap' cap' ntfn'. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBGeneric; Some (Endpoint ep') = Some (TCB tcb); ko'' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 8. \<And>ep ep' auth tcb tcb' ntfn' ccap' cap'. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag TCBActivate; Some (Endpoint ep') = Some (TCB tcb); ko'' = 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 es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 9. \<And>ep ep' auth n content content'. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RCNode; Some (Endpoint ep') = Some (CNode n content); ko'' = Some (CNode n content'); cnode_integrity es aag content content'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
 10. \<And>ep ep' auth ao ao'. \<lbrakk>tro_tag' REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; aag_subjects_have_auth_to_label es aag auth subjects; tro_tag RArch; Some (Endpoint ep') = Some (ArchObj ao); ko'' = Some (ArchObj ao'); arch_integrity_obj_alt aag es subjects ao ao'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (Endpoint ep)) ko''
A total of 116 subgoals... proof (prove)
goal (45 subgoals):
 1. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBSend; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_send es aag epa tcba \<or> indirect_send es aag (the (tcb_bound_notification tcba)) epa tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 2. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a caller R epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBCall; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_call es aag epa (tcb_state tcba)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 3. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_st. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBReply; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> tcb_fault tcba \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_reply es aag subjects tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 4. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_st epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBReceive; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> inactive new_st \<and> call_blocked epa (tcb_state tcba) \<or> awaiting_reply new_st \<and> allowed_call_blocked epa (tcb_state tcba); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; send_blocked_on epa (tcb_state tcba); aag_subjects_have_auth_to es aag Receive epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 5. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_arch epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBRestart; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb'a, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_state tcb'a = Restart \<and> new_arch = tcb_arch tcba \<or> tcb_state tcb'a = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcba))) (tcb_arch tcba); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; blocked_on epa (tcb_state tcba); aag_subjects_have_auth_to es aag Reset epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBGeneric; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ntfn'a ccap'a cap'a. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBActivate; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcba))) (tcb_arch tcba), tcb_caller := cap'a, tcb_ctable := ccap'a, tcb_state := Running, tcb_bound_notification := ntfn'a\<rparr>; tcb_state tcba = Restart; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a epa. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBSend; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_send es aag epa tcba \<or> indirect_send es aag (the (tcb_bound_notification tcba)) epa tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 9. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a callera Ra epa. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBCall; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; pasObjectAbs aag callera \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap callera False Ra) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_call es aag epa (tcb_state tcba)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 10. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a new_st. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBReply; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> tcb_fault tcba \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_reply es aag subjects tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
A total of 45 subgoals... proof (prove)
goal (45 subgoals):
 1. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBSend; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_send es aag epa tcba \<or> indirect_send es aag (the (tcb_bound_notification tcba)) epa tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 2. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a caller R epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBCall; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_call es aag epa (tcb_state tcba)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 3. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_st. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBReply; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> tcb_fault tcba \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_reply es aag subjects tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 4. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_st epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBReceive; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> inactive new_st \<and> call_blocked epa (tcb_state tcba) \<or> awaiting_reply new_st \<and> allowed_call_blocked epa (tcb_state tcba); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; send_blocked_on epa (tcb_state tcba); aag_subjects_have_auth_to es aag Receive epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 5. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_arch epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBRestart; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb'a, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_state tcb'a = Restart \<and> new_arch = tcb_arch tcba \<or> tcb_state tcb'a = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcba))) (tcb_arch tcba); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; blocked_on epa (tcb_state tcba); aag_subjects_have_auth_to es aag Reset epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBGeneric; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ntfn'a ccap'a cap'a. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBActivate; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcba))) (tcb_arch tcba), tcb_caller := cap'a, tcb_ctable := ccap'a, tcb_state := Running, tcb_bound_notification := ntfn'a\<rparr>; tcb_state tcba = Restart; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a epa. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBSend; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_send es aag epa tcba \<or> indirect_send es aag (the (tcb_bound_notification tcba)) epa tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 9. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a callera Ra epa. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBCall; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; pasObjectAbs aag callera \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap callera False Ra) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_call es aag epa (tcb_state tcba)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 10. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a new_st. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBReply; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> tcb_fault tcba \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_reply es aag subjects tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
A total of 45 subgoals... proof (prove)
goal (39 subgoals):
 1. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBSend; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_send es aag epa tcba \<or> indirect_send es aag (the (tcb_bound_notification tcba)) epa tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 2. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a caller R epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBCall; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_call es aag epa (tcb_state tcba)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 3. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_st. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBReply; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> tcb_fault tcba \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_reply es aag subjects tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 4. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_st epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBReceive; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> inactive new_st \<and> call_blocked epa (tcb_state tcba) \<or> awaiting_reply new_st \<and> allowed_call_blocked epa (tcb_state tcba); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; send_blocked_on epa (tcb_state tcba); aag_subjects_have_auth_to es aag Receive epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 5. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_arch epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBRestart; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb'a, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_state tcb'a = Restart \<and> new_arch = tcb_arch tcba \<or> tcb_state tcb'a = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcba))) (tcb_arch tcba); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; blocked_on epa (tcb_state tcba); aag_subjects_have_auth_to es aag Reset epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ntfn'a ccap'a cap'a. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBActivate; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcba))) (tcb_arch tcba), tcb_caller := cap'a, tcb_ctable := ccap'a, tcb_state := Running, tcb_bound_notification := ntfn'a\<rparr>; tcb_state tcba = Restart; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a epa. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBSend; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_send es aag epa tcba \<or> indirect_send es aag (the (tcb_bound_notification tcba)) epa tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a callera Ra epa. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBCall; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; pasObjectAbs aag callera \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap callera False Ra) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_call es aag epa (tcb_state tcba)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 9. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a new_st. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBReply; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> tcb_fault tcba \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_reply es aag subjects tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 10. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a new_st epa. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBReceive; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> inactive new_st \<and> call_blocked epa (tcb_state tcba) \<or> awaiting_reply new_st \<and> allowed_call_blocked epa (tcb_state tcba); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; send_blocked_on epa (tcb_state tcba); aag_subjects_have_auth_to es aag Receive epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
A total of 39 subgoals... proof (prove)
goal (33 subgoals):
 1. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBSend; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_send es aag epa tcba \<or> indirect_send es aag (the (tcb_bound_notification tcba)) epa tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 2. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a caller R epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBCall; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; pasObjectAbs aag caller \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_call es aag epa (tcb_state tcba)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 3. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_st. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBReply; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> tcb_fault tcba \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_reply es aag subjects tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 4. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_st epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBReceive; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> inactive new_st \<and> call_blocked epa (tcb_state tcba) \<or> awaiting_reply new_st \<and> allowed_call_blocked epa (tcb_state tcba); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; send_blocked_on epa (tcb_state tcba); aag_subjects_have_auth_to es aag Receive epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 5. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ccap'a cap'a ntfn'a new_arch epa. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBRestart; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_arch := new_arch, tcb_state := tcb_state tcb'a, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_state tcb'a = Restart \<and> new_arch = tcb_arch tcba \<or> tcb_state tcb'a = Running \<and> new_arch = arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcba))) (tcb_arch tcba); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; blocked_on epa (tcb_state tcba); aag_subjects_have_auth_to es aag Reset epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 6. \<And>tcb tcb' ccap' cap' ntfn' ep tcba tcb'a ntfn'a ccap'a cap'a. \<lbrakk>tro_tag' TCBSend; ko = Some (TCB tcb); ko' = 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' es aag; reply_cap_deletion_integrity es aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_send es aag ep tcb \<or> indirect_send es aag (the (tcb_bound_notification tcb)) ep tcb; tro_tag TCBActivate; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get (tcb_arch tcba))) (tcb_arch tcba), tcb_caller := cap'a, tcb_ctable := ccap'a, tcb_state := Running, tcb_bound_notification := ntfn'a\<rparr>; tcb_state tcba = Restart; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; activate\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 7. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a epa. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBSend; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_send es aag epa tcba \<or> indirect_send es aag (the (tcb_bound_notification tcba)) epa tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 8. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a callera Ra epa. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBCall; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := Running, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; pasObjectAbs aag callera \<in> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (ReplyCap callera False Ra) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_call es aag epa (tcb_state tcba)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 9. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a new_st. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBReply; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); \<exists>ctxt'. tcb'a = tcba\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcba), tcb_state := new_st, tcb_fault := None, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> tcb_fault tcba \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; direct_reply es aag subjects tcba\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
 10. \<And>tcb tcb' ccap' cap' ntfn' caller R ep tcba tcb'a ccap'a cap'a ntfn'a new_st epa. \<lbrakk>tro_tag' TCBCall; ko = Some (TCB tcb); ko' = 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> es; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' es aag; reply_cap_deletion_integrity es aag (ReplyCap caller False R) cap'; reply_cap_deletion_integrity es aag (tcb_ctable tcb) ccap'; direct_call es aag ep (tcb_state tcb); tro_tag TCBReceive; Some (TCB tcb') = Some (TCB tcba); ko'' = Some (TCB tcb'a); tcb'a = tcba\<lparr>tcb_state := new_st, tcb_bound_notification := ntfn'a, tcb_caller := cap'a, tcb_ctable := ccap'a\<rparr>; new_st = Running \<or> inactive new_st \<and> call_blocked epa (tcb_state tcba) \<or> awaiting_reply new_st \<and> allowed_call_blocked epa (tcb_state tcba); tcb_bound_notification_reset_integrity (tcb_bound_notification tcba) ntfn'a es aag; reply_cap_deletion_integrity es aag (tcb_caller tcba) cap'a; reply_cap_deletion_integrity es aag (tcb_ctable tcba) ccap'a; send_blocked_on epa (tcb_state tcba); aag_subjects_have_auth_to es aag Receive epa\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate es subjects (Some (TCB tcb)) ko''
A total of 33 subgoals... proof (prove)
goal:
No subgoals!