theory Ipc_IF

lemma read_queued_thread_reads_ntfn:
  "\<lbrakk> ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s;
     sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue;
     (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<rbrakk>
     \<Longrightarrow> aag_can_read aag ntfnptr" apply (frule_tac P="receive_blocked_on ntfnptr" and t=t in ntfn_queued_st_tcb_at') apply (fastforce) apply assumption apply assumption apply simp apply (rule_tac t="pasObjectAbs aag t" and auth="Receive" and auth'="Notify"
               in reads_read_queued_thread_read_ep) apply assumption apply simp apply (erule pas_refined_mem[rotated]) apply (rule sta_ts) apply (clarsimp simp: thread_st_auth_def tcb_states_of_state_def st_tcb_def2) apply (case_tac "tcb_state tcb", simp_all)[1] apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read aag ntfnptr proof (prove)
goal (5 subgoals):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (t, ?rt) \<in> ntfn_q_refs_of (ntfn_obj ntfn)
 2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 4. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> receive_blocked_on ntfnptr (BlockedOnNotification ntfnptr)
 5. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag ntfnptr proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 3. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> receive_blocked_on ntfnptr (BlockedOnNotification ntfnptr)
 4. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag ntfnptr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> receive_blocked_on ntfnptr (BlockedOnNotification ntfnptr)
 3. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag ntfnptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> receive_blocked_on ntfnptr (BlockedOnNotification ntfnptr)
 2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag ntfnptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag ntfnptr proof (prove)
goal (5 subgoals):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (?a5, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
 2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> Notify \<in> {Notify, SyncSend, Reset}
 3. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
 4. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 5. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> Notify \<in> {Notify, SyncSend, Reset}
 2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
 3. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 4. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
 2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (t, Receive, ntfnptr) \<in> state_objs_to_policy s
 2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (ntfnptr, Receive) \<in> thread_st_auth s t
 2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; get_tcb t s = Some tcb; receive_blocked_on ntfnptr (tcb_state tcb)\<rbrakk> \<Longrightarrow> (ntfnptr, Receive) \<in> tcb_st_to_auth (tcb_state tcb)
 2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (prove)
goal:
No subgoals!