theory Ipc_IF

lemma send_ipc_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects aag (l :: 'a subject_label)
        (pas_refined aag and invs and pas_cur_domain aag
          and is_subject aag \<circ> cur_thread
          and K (can_grant \<longrightarrow> (aag_has_auth_to aag Grant epptr))
          and K (is_subject aag thread \<and> aag_has_auth_to aag SyncSend epptr))
     (send_ipc block call badge can_grant can_grant_reply thread epptr)" apply (rule gen_asm_ev) apply (subgoal_tac "aag_can_read aag epptr") prefer 2 apply (fastforce intro: reads_ep) apply (simp add: send_ipc_def) apply (wp set_simple_ko_reads_respects set_thread_state_reads_respects
            when_ev setup_caller_cap_reads_respects thread_get_reads_respects
            set_thread_state_reads_respects
            do_ipc_transfer_reads_respects
            set_simple_ko_reads_respects
            hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1] hoare_vcg_all_lift
            get_simple_ko_reads_respects get_simple_ko_wp
            possible_switch_to_reads_respects
            gets_cur_thread_ev set_thread_state_pas_refined
            do_ipc_transfer_pas_refined
        | wpc
        | simp add: get_thread_state_def thread_get_def split del: if_split)+ apply clarsimp apply (rename_tac receiver queue) apply (subgoal_tac "aag_can_read aag receiver \<and> (can_grant \<longrightarrow> is_subject aag receiver)") prefer 2 apply (frule(2) pas_refined_ep_recv, rule head_in_set) apply (rule conjI) subgoal by (rule read_sync_ep_read_receivers) apply (fastforce dest: aag_wellformed_grant_Control_to_recv[OF _ _ pas_refined_wellformed]
                    simp: aag_has_Control_iff_owns) by (fastforce elim: send_ipc_valid_ep_helper reads_equivE equiv_forD
      intro: kheap_get_tcb_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and invs and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (send_ipc block call badge can_grant can_grant_reply thread epptr) proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> reads_respects aag l (pas_refined aag and invs and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (send_ipc block call badge can_grant can_grant_reply thread epptr) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; aag_can_read aag epptr\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and invs and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (send_ipc block call badge can_grant can_grant_reply thread epptr)
 2. is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> aag_can_read aag epptr proof (prove)
goal (2 subgoals):
 1. is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> aag_can_read aag epptr
 2. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; aag_can_read aag epptr\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and invs and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (send_ipc block call badge can_grant can_grant_reply thread epptr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; aag_can_read aag epptr\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and invs and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (send_ipc block call badge can_grant can_grant_reply thread epptr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; aag_can_read aag epptr\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and invs and pas_cur_domain aag and is_subject aag \<circ> cur_thread and (\<lambda>y. can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (do ep <- get_endpoint epptr;
case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP [thread]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP (queue @ [thread])
od | False \<Rightarrow> return () | RecvEP [] \<Rightarrow> fail | RecvEP (dest # queue) \<Rightarrow> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap thread dest reply_can_grant else set_thread_state thread Inactive
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; aag_can_read aag epptr; pas_refined aag s \<and> invs s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> \<forall>ntfn. ko_at (Endpoint ntfn) epptr s \<longrightarrow> (\<forall>x. ntfn = RecvEP x \<longrightarrow> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb xa s = get_tcb xa t) \<and> ((\<exists>y. get_tcb xa s = Some y) \<longrightarrow> ((\<exists>x xb. tcb_state (the (get_tcb xa s)) = BlockedOnReceive x xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag xa) \<and> aag_can_read_or_affect aag l xa) \<and> ((\<exists>x xb. tcb_state (the (get_tcb xa s)) = BlockedOnReceive x xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> (can_grant \<longrightarrow> is_subject aag xa) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (call \<longrightarrow> (can_grant \<longrightarrow> aag_can_read aag xa) \<and> (can_grant_reply \<longrightarrow> aag_can_read aag xa)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s xa xb. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (xa # xb))) epptr s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb xa s = get_tcb xa t) \<and> ((\<exists>y. get_tcb xa s = Some y) \<longrightarrow> ((\<exists>x xb. tcb_state (the (get_tcb xa s)) = BlockedOnReceive x xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag xa) \<and> aag_can_read_or_affect aag l xa) \<and> ((\<exists>x xb. tcb_state (the (get_tcb xa s)) = BlockedOnReceive x xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> (can_grant \<longrightarrow> is_subject aag xa) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (call \<longrightarrow> (can_grant \<longrightarrow> aag_can_read aag xa) \<and> (can_grant_reply \<longrightarrow> aag_can_read aag xa)))) proof (prove)
goal (1 subgoal):
 1. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb receiver s = get_tcb receiver t) \<and> ((\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> aag_can_read_or_affect aag l receiver) \<and> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (call \<longrightarrow> (can_grant \<longrightarrow> aag_can_read aag receiver) \<and> (can_grant_reply \<longrightarrow> aag_can_read aag receiver)))) proof (prove)
goal (2 subgoals):
 1. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s; aag_can_read aag receiver \<and> (can_grant \<longrightarrow> is_subject aag receiver)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb receiver s = get_tcb receiver t) \<and> ((\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> aag_can_read_or_affect aag l receiver) \<and> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (call \<longrightarrow> (can_grant \<longrightarrow> aag_can_read aag receiver) \<and> (can_grant_reply \<longrightarrow> aag_can_read aag receiver))))
 2. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s\<rbrakk> \<Longrightarrow> aag_can_read aag receiver \<and> (can_grant \<longrightarrow> is_subject aag receiver) proof (prove)
goal (2 subgoals):
 1. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s\<rbrakk> \<Longrightarrow> aag_can_read aag receiver \<and> (can_grant \<longrightarrow> is_subject aag receiver)
 2. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s; aag_can_read aag receiver \<and> (can_grant \<longrightarrow> is_subject aag receiver)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb receiver s = get_tcb receiver t) \<and> ((\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> aag_can_read_or_affect aag l receiver) \<and> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (call \<longrightarrow> (can_grant \<longrightarrow> aag_can_read aag receiver) \<and> (can_grant_reply \<longrightarrow> aag_can_read aag receiver)))) proof (prove)
goal (2 subgoals):
 1. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s; (pasObjectAbs aag receiver, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read aag receiver \<and> (can_grant \<longrightarrow> is_subject aag receiver)
 2. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s; aag_can_read aag receiver \<and> (can_grant \<longrightarrow> is_subject aag receiver)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb receiver s = get_tcb receiver t) \<and> ((\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> aag_can_read_or_affect aag l receiver) \<and> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (call \<longrightarrow> (can_grant \<longrightarrow> aag_can_read aag receiver) \<and> (can_grant_reply \<longrightarrow> aag_can_read aag receiver)))) proof (prove)
goal (3 subgoals):
 1. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s; (pasObjectAbs aag receiver, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read aag receiver
 2. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s; (pasObjectAbs aag receiver, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> can_grant \<longrightarrow> is_subject aag receiver
 3. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s; aag_can_read aag receiver \<and> (can_grant \<longrightarrow> is_subject aag receiver)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb receiver s = get_tcb receiver t) \<and> ((\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> aag_can_read_or_affect aag l receiver) \<and> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (call \<longrightarrow> (can_grant \<longrightarrow> aag_can_read aag receiver) \<and> (can_grant_reply \<longrightarrow> aag_can_read aag receiver)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s_; invs s_; pas_cur_domain aag s_; is_subject aag (cur_thread s_); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver_ # queue_))) epptr s_; (pasObjectAbs aag receiver_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read aag receiver_ proof (prove)
goal (2 subgoals):
 1. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s; (pasObjectAbs aag receiver, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> can_grant \<longrightarrow> is_subject aag receiver
 2. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s; aag_can_read aag receiver \<and> (can_grant \<longrightarrow> is_subject aag receiver)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb receiver s = get_tcb receiver t) \<and> ((\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> aag_can_read_or_affect aag l receiver) \<and> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (call \<longrightarrow> (can_grant \<longrightarrow> aag_can_read aag receiver) \<and> (can_grant_reply \<longrightarrow> aag_can_read aag receiver)))) proof (prove)
goal (1 subgoal):
 1. \<And>s receiver queue. \<lbrakk>aag_can_read aag epptr; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; pas_cur_domain aag s; is_subject aag (cur_thread s); can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # queue))) epptr s; aag_can_read aag receiver \<and> (can_grant \<longrightarrow> is_subject aag receiver)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb receiver s = get_tcb receiver t) \<and> ((\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> aag_can_read_or_affect aag l receiver) \<and> ((\<exists>x xa. tcb_state (the (get_tcb receiver s)) = BlockedOnReceive x xa) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue) s \<and> valid_mdb s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (call \<longrightarrow> (can_grant \<longrightarrow> aag_can_read aag receiver) \<and> (can_grant_reply \<longrightarrow> aag_can_read aag receiver))))