theory Access_AC

lemma owns_ep_owns_receivers:
  "\<lbrakk> \<forall>auth. aag_has_auth_to aag auth epptr; pas_refined aag s; invs s;
     ko_at (Endpoint ep) epptr s; (t, EPRecv) \<in> ep_q_refs_of ep \<rbrakk>
     \<Longrightarrow> is_subject aag t" apply (drule (1) ep_rcv_queued_st_tcb_at[where P = "receive_blocked_on epptr"]) apply clarsimp apply clarsimp apply clarsimp apply (rule refl) apply (drule st_tcb_at_to_thread_st_auth) apply (clarsimp simp: receive_blocked_on_def2) apply (drule spec[where x = Grant]) apply (frule aag_wellformed_grant_Control_to_recv[OF _ _ pas_refined_wellformed]) apply (rule pas_refined_mem[OF sta_ts]) apply (case_tac st; fastforce) apply assumption+ apply (erule (1) aag_Control_into_owns) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ko_at (Endpoint ep) epptr s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 3. \<And>pl. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> receive_blocked_on epptr (BlockedOnReceive epptr pl)
 4. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> kheap ?s' t = kheap s t
 5. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; st_tcb_at (receive_blocked_on epptr) t ?s'\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 2. \<And>pl. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> receive_blocked_on epptr (BlockedOnReceive epptr pl)
 3. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> kheap ?s' t = kheap s t
 4. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; st_tcb_at (receive_blocked_on epptr) t ?s'\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (3 subgoals):
 1. \<And>pl. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> receive_blocked_on epptr (BlockedOnReceive epptr pl)
 2. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> kheap ?s' t = kheap s t
 3. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; st_tcb_at (receive_blocked_on epptr) t ?s'\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> kheap ?s' t = kheap s t
 2. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; st_tcb_at (receive_blocked_on epptr) t ?s'\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; st_tcb_at (receive_blocked_on epptr) t s\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; \<exists>st. receive_blocked_on epptr st \<and> thread_st_auth s t = tcb_st_to_auth st\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>\<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (3 subgoals):
 1. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (?r20 st, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag
 2. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pas_refined aag (?sa20 st)
 3. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Control, ?r20 st) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (4 subgoals):
 1. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (epptr, Receive) \<in> thread_st_auth (?s24 st) (?x24 st)
 2. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pas_refined aag (?s24 st)
 3. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pas_refined aag (?sa20 st)
 4. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Control, pasObjectAbs aag (?x24 st)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (3 subgoals):
 1. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pas_refined aag (?sa20 st)
 3. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Control, pasObjectAbs aag t) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>pas_refined aag s; invs s; (t, EPRecv) \<in> ep_q_refs_of ep; (epptr, Receive) \<in> tcb_st_to_auth st; thread_st_auth s t = tcb_st_to_auth st; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Control, pasObjectAbs aag t) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag t proof (prove)
goal:
No subgoals!