theory Access_AC

lemma tro_tcb_reply':
  "\<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> new_st = Inactive));
     direct_reply subjects aag l' tcb \<rbrakk>
     \<Longrightarrow> integrity_obj aag activate subjects l' ko ko'" apply (clarsimp simp:direct_reply_def simp del:not_None_eq) apply (erule disjE, (rule tro_tcb_reply[OF refl refl], force; force))  (* Warning: schematics *)
   apply (clarsimp simp del:not_None_eq) apply (rule tro_trans_spec) apply (frule allowed_call_blocked_def[THEN meta_eq_to_obj_eq,THEN iffD1],clarsimp) apply (rule tro_tcb_receive[OF refl refl refl, where new_st=BlockedOnReply];force) apply (rule tro_trans_spec) apply (rule tro_tcb_reply[OF refl refl refl, where new_st=new_st];force) by (fastforce intro!: tro_orefl tcb.equality)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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); direct_reply subjects aag l' tcb\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' ko ko' proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); awaiting_reply (tcb_state tcb) \<or> (\<exists>ep. allowed_call_blocked ep (tcb_state tcb) \<and> aag_subjects_have_auth_to subjects aag Receive ep); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag; \<exists>ep. allowed_call_blocked ep (tcb_state tcb) \<and> aag_subjects_have_auth_to subjects aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag; \<exists>ep. allowed_call_blocked ep (tcb_state tcb) \<and> aag_subjects_have_auth_to subjects aag Receive ep\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s ep sa. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag; allowed_call_blocked ep (tcb_state tcb); sa \<in> subjects; (sa, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>s ep sa. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag; allowed_call_blocked ep (tcb_state tcb); sa \<in> subjects; (sa, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) (?y40 s ep sa)
 2. \<And>s ep sa. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag; allowed_call_blocked ep (tcb_state tcb); sa \<in> subjects; (sa, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (?y40 s ep sa) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>s ep sa pl. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> (\<exists>y. tcb_fault tcb = Some y) \<and> (new_st = Restart \<or> inactive new_st); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag; allowed_call_blocked ep (BlockedOnSend ep pl); sa \<in> subjects; (sa, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; tcb_state tcb = BlockedOnSend ep pl; sender_is_call pl; sender_can_grant pl \<or> sender_can_grant_reply pl\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) (?y40 s ep sa)
 2. \<And>s ep sa. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag; allowed_call_blocked ep (tcb_state tcb); sa \<in> subjects; (sa, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (?y40 s ep sa) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s ep sa. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag; allowed_call_blocked ep (tcb_state tcb); sa \<in> subjects; (sa, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB (tcb\<lparr>tcb_state := BlockedOnReply\<rparr>))) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>s ep sa. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag; allowed_call_blocked ep (tcb_state tcb); sa \<in> subjects; (sa, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB (tcb\<lparr>tcb_state := BlockedOnReply\<rparr>))) (?y88 s ep sa)
 2. \<And>s ep sa. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag; allowed_call_blocked ep (tcb_state tcb); sa \<in> subjects; (sa, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (?y88 s ep sa) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s ep sa. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)); tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>; new_st = Running \<or> tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> inactive new_st); s \<in> subjects; (s, Reply, l') \<in> pasPolicy aag; allowed_call_blocked ep (tcb_state tcb); sa \<in> subjects; (sa, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB (tcb\<lparr>tcb_state := BlockedOnReply, tcb_arch := arch_tcb_context_set (?ctxt'92 s ep sa) (tcb_arch (tcb\<lparr>tcb_state := BlockedOnReply\<rparr>)), tcb_state := new_st, tcb_fault := None\<rparr>))) (Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := new_st, tcb_fault := None\<rparr>)))