theory Finalise_IF

lemma owns_thread_blocked_reads_endpoint:
  "\<lbrakk> pas_refined aag s; invs s; st_tcb_at (\<lambda> y. y = state) tptr s; is_subject aag tptr;
     state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x \<rbrakk>
     \<Longrightarrow> aag_can_read aag x" apply (rule_tac auth="tcb_st_to_auth' state" in reads_ep) apply (drule sym, simp, rule pas_refined_mem) apply (rule_tac s=s in sta_ts) apply (clarsimp simp: thread_st_auth_def tcb_states_of_state_def
                          st_tcb_at_def get_tcb_def obj_at_def) apply fastforce apply assumption apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; is_subject aag tptr; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x\<rbrakk> \<Longrightarrow> aag_can_read aag x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; is_subject aag tptr; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x\<rbrakk> \<Longrightarrow> (pasSubject aag, tcb_st_to_auth' state, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; is_subject aag tptr; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x\<rbrakk> \<Longrightarrow> tcb_st_to_auth' state \<in> {SyncSend, Receive} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x; pasSubject aag = pasObjectAbs aag tptr\<rbrakk> \<Longrightarrow> (tptr, tcb_st_to_auth' state, x) \<in> state_objs_to_policy ?s3
 2. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x; pasSubject aag = pasObjectAbs aag tptr\<rbrakk> \<Longrightarrow> pas_refined aag ?s3
 3. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; is_subject aag tptr; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x\<rbrakk> \<Longrightarrow> tcb_st_to_auth' state \<in> {SyncSend, Receive} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x; pasSubject aag = pasObjectAbs aag tptr\<rbrakk> \<Longrightarrow> (x, tcb_st_to_auth' state) \<in> thread_st_auth s tptr
 2. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x; pasSubject aag = pasObjectAbs aag tptr\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; is_subject aag tptr; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x\<rbrakk> \<Longrightarrow> tcb_st_to_auth' state \<in> {SyncSend, Receive} proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>pas_refined aag s; invs s; tcb_state tcb = BlockedOnReceive x pl \<or> tcb_state tcb = BlockedOnSend x xb \<or> tcb_state tcb = BlockedOnNotification x; pasSubject aag = pasObjectAbs aag tptr; kheap s tptr = Some (TCB tcb); state = tcb_state tcb\<rbrakk> \<Longrightarrow> (x, tcb_st_to_auth' (tcb_state tcb)) \<in> tcb_st_to_auth (tcb_state tcb)
 2. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x; pasSubject aag = pasObjectAbs aag tptr\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; is_subject aag tptr; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x\<rbrakk> \<Longrightarrow> tcb_st_to_auth' state \<in> {SyncSend, Receive} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x; pasSubject aag = pasObjectAbs aag tptr\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; is_subject aag tptr; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x\<rbrakk> \<Longrightarrow> tcb_st_to_auth' state \<in> {SyncSend, Receive} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; invs s; st_tcb_at (\<lambda>y. y = state) tptr s; is_subject aag tptr; state = BlockedOnReceive x pl \<or> state = BlockedOnSend x xb \<or> state = BlockedOnNotification x\<rbrakk> \<Longrightarrow> tcb_st_to_auth' state \<in> {SyncSend, Receive} proof (prove)
goal:
No subgoals!