theory Access_AC

lemma troa_tro_alt[elim!]:
  "integrity_obj_atomic aag activate subjects l ko ko'
   \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'" apply (erule integrity_obj_atomic.cases) text \<open>Single out TCB cases for special handling. We manually simplify
        the TCB updates in the tro_alt rules using @{thm tcb.equality}.\<close> 
    (* somewhat slow 10s *)
                 apply (find_goal \<open>match premises in "ko = Some (TCB _)" \<Rightarrow> succeed\<close>,
                       ((erule(1) integrity_obj_alt.intros[OF tro_tagI],
                         (intro exI tcb.equality; solves \<open>simp\<close>));
                        fastforce simp: reply_cap_deletion_integrity_def direct_reply_def
                                        tcb_bound_notification_reset_integrity_def))+ text \<open>Remaining cases.\<close> apply (fastforce intro: integrity_obj_alt.intros[OF tro_tagI])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_obj_atomic aag activate subjects l ko ko' \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko' proof (prove)
goal (15 subgoals):
 1. l \<in> subjects \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 2. \<And>ntfn ntfn' auth s. \<lbrakk>ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; s \<in> subjects; (s, auth, l) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 3. \<And>ep ep' auth s. \<lbrakk>ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; s \<in> subjects; (s, auth, l) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 4. \<And>ep ep' tcb ntfn. \<lbrakk>ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag; (tcb, Receive, l) \<in> pasPolicy aag; aag_subjects_have_auth_to subjects aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 5. \<And>tcb tcb' ctxt' ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send subjects aag ep tcb \<or> indirect_send subjects aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 6. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs aag caller \<in> subjects; direct_call subjects aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 7. \<And>tcb tcb' new_st ctxt'. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label subjects aag Reply l\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 8. \<And>tcb tcb' new_st ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; new_st = Running \<or> inactive new_st \<and> call_blocked ep (tcb_state tcb) \<or> awaiting_reply new_st \<and> allowed_call_blocked ep (tcb_state tcb); send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to subjects aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 9. \<And>tcb tcb' ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to subjects aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 10. \<And>tcb tcb'. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to subjects aag Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. l \<in> subjects \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 2. \<And>ntfn ntfn' auth s. \<lbrakk>ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; s \<in> subjects; (s, auth, l) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 3. \<And>ep ep' auth s. \<lbrakk>ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; s \<in> subjects; (s, auth, l) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 4. \<And>ep ep' tcb ntfn. \<lbrakk>ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag; (tcb, Receive, l) \<in> pasPolicy aag; aag_subjects_have_auth_to subjects aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 5. \<And>tcb tcb' ctxt' ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send subjects aag ep tcb \<or> indirect_send subjects aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 6. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs aag caller \<in> subjects; direct_call subjects aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 7. \<And>tcb tcb' new_st ctxt'. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label subjects aag Reply l\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 8. \<And>tcb tcb' new_st ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; new_st = Running \<or> inactive new_st \<and> call_blocked ep (tcb_state tcb) \<or> awaiting_reply new_st \<and> allowed_call_blocked ep (tcb_state tcb); send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to subjects aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 9. \<And>tcb tcb' ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to subjects aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 10. \<And>tcb tcb'. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to subjects aag Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. l \<in> subjects \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 2. \<And>ntfn ntfn' auth s. \<lbrakk>ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; s \<in> subjects; (s, auth, l) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 3. \<And>ep ep' auth s. \<lbrakk>ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; s \<in> subjects; (s, auth, l) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 4. \<And>ep ep' tcb ntfn. \<lbrakk>ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag; (tcb, Receive, l) \<in> pasPolicy aag; aag_subjects_have_auth_to subjects aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 5. \<And>tcb tcb' ctxt' ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; direct_send subjects aag ep tcb \<or> indirect_send subjects aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 6. \<And>tcb tcb' caller R ctxt' ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, tcb_caller := ReplyCap caller False R\<rparr>; pasObjectAbs aag caller \<in> subjects; direct_call subjects aag ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 7. \<And>tcb tcb' new_st ctxt'. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb); aag_subjects_have_auth_to_label subjects aag Reply l\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 8. \<And>tcb tcb' new_st ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := new_st\<rparr>; new_st = Running \<or> inactive new_st \<and> call_blocked ep (tcb_state tcb) \<or> awaiting_reply new_st \<and> allowed_call_blocked ep (tcb_state tcb); send_blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to subjects aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 9. \<And>tcb tcb' ep. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; blocked_on ep (tcb_state tcb); aag_subjects_have_auth_to subjects aag Reset ep\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 10. \<And>tcb tcb'. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; aag_subjects_have_auth_to subjects aag Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
A total of 15 subgoals... proof (prove)
goal (6 subgoals):
 1. l \<in> subjects \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 2. \<And>ntfn ntfn' auth s. \<lbrakk>ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; s \<in> subjects; (s, auth, l) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 3. \<And>ep ep' auth s. \<lbrakk>ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; s \<in> subjects; (s, auth, l) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 4. \<And>ep ep' tcb ntfn. \<lbrakk>ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag; (tcb, Receive, l) \<in> pasPolicy aag; aag_subjects_have_auth_to subjects aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 5. \<And>n content content'. \<lbrakk>ko = Some (CNode n content); ko' = Some (CNode n content'); cnode_integrity subjects aag content content'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 6. \<And>ao ao'. \<lbrakk>ko = Some (ArchObj ao); ko' = Some (ArchObj ao'); arch_integrity_obj_atomic aag subjects l ao ao'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko' proof (prove)
goal (6 subgoals):
 1. l \<in> subjects \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 2. \<And>ntfn ntfn' auth s. \<lbrakk>ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); auth \<in> {Receive, Notify, Reset}; s \<in> subjects; (s, auth, l) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 3. \<And>ep ep' auth s. \<lbrakk>ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); auth \<in> {Receive, SyncSend, Reset}; s \<in> subjects; (s, auth, l) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 4. \<And>ep ep' tcb ntfn. \<lbrakk>ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag; (tcb, Receive, l) \<in> pasPolicy aag; aag_subjects_have_auth_to subjects aag Notify ntfn\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 5. \<And>n content content'. \<lbrakk>ko = Some (CNode n content); ko' = Some (CNode n content'); cnode_integrity subjects aag content content'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'
 6. \<And>ao ao'. \<lbrakk>ko = Some (ArchObj ao); ko' = Some (ArchObj ao'); arch_integrity_obj_atomic aag subjects l ao ao'\<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko' proof (prove)
goal:
No subgoals!