theory Ipc_AC

lemma receive_ipc_base_integrity:
  notes do_nbrecv_failed_transfer_def[simp]
  shows "\<lbrace>pas_refined aag and integrity aag X st and invs and ko_at (Endpoint ep) epptr and
          K (is_subject aag receiver \<and> aag_has_auth_to aag Receive epptr \<and>
             (\<forall>auth \<in> cap_rights_to_auth rights True. aag_has_auth_to aag auth epptr))\<rbrace>
         receive_ipc_base aag receiver ep epptr rights is_blocking
         \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp: thread_get_def get_thread_state_def cong: endpoint.case_cong) apply (rule hoare_pre) apply (wpsimp wp: set_endpoint_respects set_thread_state_running_respects
             setup_caller_cap_integrity_recv[where ep = epptr]
             do_ipc_transfer_integrity_autarch
             set_thread_state_integrity_autarch[where param_a=receiver]
             sts_receive_Inactive_respects[where ep = epptr]
             as_user_integrity_autarch) apply (rename_tac list tcb data) apply (rule_tac Q="\<lambda>rv s. integrity aag X st s
                           \<and> valid_mdb s
                           \<and> is_subject aag receiver
                           \<and> (sender_can_call data \<longrightarrow> AllowGrant \<in> rights
                                                   \<longrightarrow> is_subject aag (hd list))
                           \<and> (sender_can_grant data \<longrightarrow> is_subject aag (hd list))
                           \<and> st_tcb_at (send_blocked_on epptr) (hd list) s
                           \<and> st_tcb_at (\<lambda>st. st = BlockedOnSend epptr data) (hd list) s"
                     in hoare_strengthen_post[rotated]) apply (fastforce simp: st_tcb_at_def obj_at_def get_tcb_rev call_blocked_def
                                allowed_call_blocked_def
                         dest!: get_tcb_SomeD
                         elim: pred_tcb_atI) apply (wpsimp wp: do_ipc_transfer_integrity_autarch do_ipc_transfer_pred_tcb
                          set_endpoint_respects get_simple_ko_wp
                          set_thread_state_integrity_autarch[where param_a=receiver]
                          hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1]
                          hoare_vcg_all_lift as_user_integrity_autarch)+ apply (subgoal_tac "ep_at epptr s \<and> (\<exists>auth. aag_has_auth_to aag auth epptr
                                    \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))") prefer 2 apply (fastforce simp: obj_at_def is_ep) apply simp apply (thin_tac "ep_at epptr s \<and> (\<exists>auth. aag_has_auth_to aag auth epptr
                                 \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))") apply (clarsimp simp: st_tcb_def2 a_type_def) apply (frule_tac t="hd x" in sym_ref_endpoint_sendD[OF invs_sym_refs],assumption,force) apply (clarsimp simp: get_tcb_def elim!: pred_tcb_atE) apply (intro conjI; (force elim: receive_ipc_valid_ep_helper receive_ipc_sender_can_grant_helper)?) apply (intro impI) apply (frule_tac x= "hd x" in pas_refined_mem[rotated,where auth=Call]) apply (rule sta_ts) apply (simp add: thread_st_auth_def tcb_states_of_state_def get_tcb_def) apply (simp add: cap_rights_to_auth_def) apply (rule aag_has_Control_iff_owns[THEN iffD1], assumption) apply (erule aag_wellformed_grant_Control_to_send_by_reply[OF _ _ _ pas_refined_wellformed]; force) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and invs and ko_at (Endpoint ep) epptr and K (is_subject aag receiver \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref data \<Rightarrow> return data | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some epptr) (sender_badge data) (sender_can_grant data) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (AllowGrant \<in> rights) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag receiver \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and invs and ko_at (Endpoint ep) epptr\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref data \<Rightarrow> return data | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some epptr) (sender_badge data) (sender_can_grant data) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (AllowGrant \<in> rights) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and invs and ko_at (Endpoint ep) epptr\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | SendEP q \<Rightarrow> do y <- assert (q \<noteq> []);
y <- set_endpoint epptr (case tl q of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl q));
tcb <- gets_the (get_tcb (hd q));
data <- case tcb_state tcb of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd q) (Some epptr) (sender_badge data) (sender_can_grant data) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap (hd q) receiver (AllowGrant \<in> rights) else set_thread_state (hd q) Inactive else do y <- set_thread_state (hd q) Running;
possible_switch_to (hd q)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>?Q10\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | SendEP q \<Rightarrow> do y <- assert (q \<noteq> []);
y <- set_endpoint epptr (case tl q of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl q));
tcb <- gets_the (get_tcb (hd q));
data <- case tcb_state tcb of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd q) (Some epptr) (sender_badge data) (sender_can_grant data) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap (hd q) receiver (AllowGrant \<in> rights) else set_thread_state (hd q) Inactive else do y <- set_thread_state (hd q) Running;
possible_switch_to (hd q)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pas_refined aag and integrity aag X st and invs and ko_at (Endpoint ep) epptr) s\<rbrakk> \<Longrightarrow> ?Q10 s proof (prove)
goal (7 subgoals):
 1. \<And>x2 tcb data. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B59 x2 () () tcb data\<rbrace> do_ipc_transfer (hd x2) (Some epptr) (sender_badge data) (sender_can_grant data) receiver \<lbrace>\<lambda>yb s. (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> integrity aag X st s \<and> valid_mdb s \<and> st_tcb_at (send_blocked_on epptr) (hd x2) s \<and> pred_tcb_at id (\<lambda>itcb. allowed_call_blocked epptr (itcb_state itcb)) (hd x2) s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x2))) \<and> (sender_can_grant_reply data \<longrightarrow> integrity aag X st s \<and> valid_mdb s \<and> st_tcb_at (send_blocked_on epptr) (hd x2) s \<and> pred_tcb_at id (\<lambda>itcb. allowed_call_blocked epptr (itcb_state itcb)) (hd x2) s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x2))) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> integrity aag X st s \<and> st_tcb_at (send_blocked_on epptr) (hd x2) s \<and> (\<forall>tcb. get_tcb (hd x2) s = Some tcb \<longrightarrow> call_blocked epptr (tcb_state tcb)))) \<and> (\<not> sender_is_call data \<longrightarrow> integrity aag X st s \<and> (\<exists>ep. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> st_tcb_at (send_blocked_on ep) (hd x2) s))\<rbrace>
 2. \<And>x2 y ya tcb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B58 x2 y ya tcb\<rbrace> case tcb_state tcb of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B59 x2 y ya tcb\<rbrace>
 3. \<And>x2 y ya. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x2 y ya\<rbrace> gets_the (get_tcb (hd x2)) \<lbrace>?B58 x2 y ya\<rbrace>
 4. \<And>x2 y. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x2 y\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>?B57 x2 y\<rbrace>
 5. \<And>x2. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R26 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B56 x2\<rbrace>
 6. \<And>x3. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R27 x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (x3 @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pas_refined aag and integrity aag X st and invs and ko_at (Endpoint ep) epptr) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (integrity aag X st and K (is_subject aag receiver)) s \<and> ep_at epptr s \<and> K (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> auth \<in> {Receive, SyncSend, Reset}) s) \<and> (is_blocking = False \<longrightarrow> (integrity aag X st and K (is_subject aag receiver)) s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R26 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R27 x s) proof (prove)
goal (7 subgoals):
 1. \<And>list tcb data. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP list\<rbrakk> \<Longrightarrow> \<lbrace>?B59 list () () tcb data\<rbrace> do_ipc_transfer (hd list) (Some epptr) (sender_badge data) (sender_can_grant data) receiver \<lbrace>\<lambda>yb s. (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> integrity aag X st s \<and> valid_mdb s \<and> st_tcb_at (send_blocked_on epptr) (hd list) s \<and> pred_tcb_at id (\<lambda>itcb. allowed_call_blocked epptr (itcb_state itcb)) (hd list) s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list))) \<and> (sender_can_grant_reply data \<longrightarrow> integrity aag X st s \<and> valid_mdb s \<and> st_tcb_at (send_blocked_on epptr) (hd list) s \<and> pred_tcb_at id (\<lambda>itcb. allowed_call_blocked epptr (itcb_state itcb)) (hd list) s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list))) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> integrity aag X st s \<and> st_tcb_at (send_blocked_on epptr) (hd list) s \<and> (\<forall>tcb. get_tcb (hd list) s = Some tcb \<longrightarrow> call_blocked epptr (tcb_state tcb)))) \<and> (\<not> sender_is_call data \<longrightarrow> integrity aag X st s \<and> (\<exists>ep. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> st_tcb_at (send_blocked_on ep) (hd list) s))\<rbrace>
 2. \<And>x2 y ya tcb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B58 x2 y ya tcb\<rbrace> case tcb_state tcb of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B59 x2 y ya tcb\<rbrace>
 3. \<And>x2 y ya. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x2 y ya\<rbrace> gets_the (get_tcb (hd x2)) \<lbrace>?B58 x2 y ya\<rbrace>
 4. \<And>x2 y. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x2 y\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>?B57 x2 y\<rbrace>
 5. \<And>x2. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R26 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B56 x2\<rbrace>
 6. \<And>x3. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R27 x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (x3 @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pas_refined aag and integrity aag X st and invs and ko_at (Endpoint ep) epptr) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (integrity aag X st and K (is_subject aag receiver)) s \<and> ep_at epptr s \<and> K (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> auth \<in> {Receive, SyncSend, Reset}) s) \<and> (is_blocking = False \<longrightarrow> (integrity aag X st and K (is_subject aag receiver)) s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R26 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R27 x s) proof (prove)
goal (8 subgoals):
 1. \<And>list tcb data rv s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP list; integrity aag X st s \<and> valid_mdb s \<and> is_subject aag receiver \<and> (sender_can_call data \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant data \<longrightarrow> is_subject aag (hd list)) \<and> st_tcb_at (send_blocked_on epptr) (hd list) s \<and> st_tcb_at (\<lambda>st. st = BlockedOnSend epptr data) (hd list) s\<rbrakk> \<Longrightarrow> (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> integrity aag X st s \<and> valid_mdb s \<and> st_tcb_at (send_blocked_on epptr) (hd list) s \<and> pred_tcb_at id (\<lambda>itcb. allowed_call_blocked epptr (itcb_state itcb)) (hd list) s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list))) \<and> (sender_can_grant_reply data \<longrightarrow> integrity aag X st s \<and> valid_mdb s \<and> st_tcb_at (send_blocked_on epptr) (hd list) s \<and> pred_tcb_at id (\<lambda>itcb. allowed_call_blocked epptr (itcb_state itcb)) (hd list) s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list))) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> integrity aag X st s \<and> st_tcb_at (send_blocked_on epptr) (hd list) s \<and> (\<forall>tcb. get_tcb (hd list) s = Some tcb \<longrightarrow> call_blocked epptr (tcb_state tcb)))) \<and> (\<not> sender_is_call data \<longrightarrow> integrity aag X st s \<and> (\<exists>ep. (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> st_tcb_at (send_blocked_on ep) (hd list) s))
 2. \<And>list tcb data. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP list\<rbrakk> \<Longrightarrow> \<lbrace>?B59 list () () tcb data\<rbrace> do_ipc_transfer (hd list) (Some epptr) (sender_badge data) (sender_can_grant data) receiver \<lbrace>\<lambda>rv s. integrity aag X st s \<and> valid_mdb s \<and> is_subject aag receiver \<and> (sender_can_call data \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant data \<longrightarrow> is_subject aag (hd list)) \<and> st_tcb_at (send_blocked_on epptr) (hd list) s \<and> st_tcb_at (\<lambda>st. st = BlockedOnSend epptr data) (hd list) s\<rbrace>
 3. \<And>x2 y ya tcb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B58 x2 y ya tcb\<rbrace> case tcb_state tcb of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B59 x2 y ya tcb\<rbrace>
 4. \<And>x2 y ya. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x2 y ya\<rbrace> gets_the (get_tcb (hd x2)) \<lbrace>?B58 x2 y ya\<rbrace>
 5. \<And>x2 y. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x2 y\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>?B57 x2 y\<rbrace>
 6. \<And>x2. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R26 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B56 x2\<rbrace>
 7. \<And>x3. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R27 x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (x3 @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 8. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pas_refined aag and integrity aag X st and invs and ko_at (Endpoint ep) epptr) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (integrity aag X st and K (is_subject aag receiver)) s \<and> ep_at epptr s \<and> K (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> auth \<in> {Receive, SyncSend, Reset}) s) \<and> (is_blocking = False \<longrightarrow> (integrity aag X st and K (is_subject aag receiver)) s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R26 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R27 x s) proof (prove)
goal (7 subgoals):
 1. \<And>list tcb data. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP list\<rbrakk> \<Longrightarrow> \<lbrace>?B59 list () () tcb data\<rbrace> do_ipc_transfer (hd list) (Some epptr) (sender_badge data) (sender_can_grant data) receiver \<lbrace>\<lambda>rv s. integrity aag X st s \<and> valid_mdb s \<and> is_subject aag receiver \<and> (sender_can_call data \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant data \<longrightarrow> is_subject aag (hd list)) \<and> st_tcb_at (send_blocked_on epptr) (hd list) s \<and> st_tcb_at (\<lambda>st. st = BlockedOnSend epptr data) (hd list) s\<rbrace>
 2. \<And>x2 y ya tcb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B58 x2 y ya tcb\<rbrace> case tcb_state tcb of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B59 x2 y ya tcb\<rbrace>
 3. \<And>x2 y ya. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x2 y ya\<rbrace> gets_the (get_tcb (hd x2)) \<lbrace>?B58 x2 y ya\<rbrace>
 4. \<And>x2 y. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x2 y\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>?B57 x2 y\<rbrace>
 5. \<And>x2. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R26 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B56 x2\<rbrace>
 6. \<And>x3. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R27 x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (x3 @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pas_refined aag and integrity aag X st and invs and ko_at (Endpoint ep) epptr) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (integrity aag X st and K (is_subject aag receiver)) s \<and> ep_at epptr s \<and> K (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> auth \<in> {Receive, SyncSend, Reset}) s) \<and> (is_blocking = False \<longrightarrow> (integrity aag X st and K (is_subject aag receiver)) s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R26 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R27 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint ep) epptr s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<exists>y. get_tcb (hd x) s = Some y) \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> st_tcb_at (send_blocked_on epptr) (hd x) s \<and> st_tcb_at (\<lambda>a. a = BlockedOnSend epptr xb) (hd x) s)) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint ep) epptr s; ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<exists>y. get_tcb (hd x) s = Some y) \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> st_tcb_at (send_blocked_on epptr) (hd x) s \<and> st_tcb_at (\<lambda>a. a = BlockedOnSend epptr xb) (hd x) s)) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)))
 2. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint ep) epptr s\<rbrakk> \<Longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint ep) epptr s\<rbrakk> \<Longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))
 2. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint ep) epptr s; ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<exists>y. get_tcb (hd x) s = Some y) \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> st_tcb_at (send_blocked_on epptr) (hd x) s \<and> st_tcb_at (\<lambda>a. a = BlockedOnSend epptr xb) (hd x) s)) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint ep) epptr s; ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<exists>y. get_tcb (hd x) s = Some y) \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> st_tcb_at (send_blocked_on epptr) (hd x) s \<and> st_tcb_at (\<lambda>a. a = BlockedOnSend epptr xb) (hd x) s)) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint ep) epptr s; ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))\<rbrakk> \<Longrightarrow> \<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<exists>y. get_tcb (hd x) s = Some y) \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa 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 tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> st_tcb_at (send_blocked_on epptr) (hd x) s \<and> st_tcb_at (\<lambda>a. a = BlockedOnSend epptr xb) (hd x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint ep) epptr s\<rbrakk> \<Longrightarrow> \<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<exists>y. get_tcb (hd x) s = Some y) \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa 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 tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> st_tcb_at (send_blocked_on epptr) (hd x) s \<and> st_tcb_at (\<lambda>a. a = BlockedOnSend epptr xb) (hd x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x y xa xb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; get_tcb (hd x) s = Some y; tcb_state y = BlockedOnSend xa xb\<rbrakk> \<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 tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> epptr = xa \<and> xa = epptr proof (prove)
goal (1 subgoal):
 1. \<And>s x y xa xb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; get_tcb (hd x) s = Some y; tcb_state y = BlockedOnSend xa xb; \<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) (hd x) s\<rbrakk> \<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 tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> epptr = xa \<and> xa = epptr proof (prove)
goal (1 subgoal):
 1. \<And>s x y xb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; kheap s (hd x) = Some (TCB y)\<rbrakk> \<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 tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) proof (prove)
goal (1 subgoal):
 1. \<And>s x y xb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; kheap s (hd x) = Some (TCB y)\<rbrakk> \<Longrightarrow> sender_can_grant_reply xb \<longrightarrow> AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x) proof (prove)
goal (1 subgoal):
 1. \<And>s x y xb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; kheap s (hd x) = Some (TCB y); sender_can_grant_reply xb; AllowGrant \<in> rights\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (2 subgoals):
 1. \<And>s x y xb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; kheap s (hd x) = Some (TCB y); sender_can_grant_reply xb; AllowGrant \<in> rights\<rbrakk> \<Longrightarrow> (hd x, Call, ?y699 s x y xb) \<in> state_objs_to_policy s
 2. \<And>s x y xb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; kheap s (hd x) = Some (TCB y); sender_can_grant_reply xb; AllowGrant \<in> rights; (pasObjectAbs aag (hd x), Call, pasObjectAbs aag (?y699 s x y xb)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (2 subgoals):
 1. \<And>s x y xb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; kheap s (hd x) = Some (TCB y); sender_can_grant_reply xb; AllowGrant \<in> rights\<rbrakk> \<Longrightarrow> (?y699 s x y xb, Call) \<in> thread_st_auth s (hd x)
 2. \<And>s x y xb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; kheap s (hd x) = Some (TCB y); sender_can_grant_reply xb; AllowGrant \<in> rights; (pasObjectAbs aag (hd x), Call, pasObjectAbs aag (?y699 s x y xb)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (1 subgoal):
 1. \<And>s x y xb. \<lbrakk>is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; kheap s (hd x) = Some (TCB y); sender_can_grant_reply xb; AllowGrant \<in> rights; (pasObjectAbs aag (hd x), Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (1 subgoal):
 1. \<And>s x y xb. \<lbrakk>is_subject aag receiver; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; kheap s (hd x) = Some (TCB y); sender_can_grant_reply xb; AllowGrant \<in> rights; (pasObjectAbs aag (hd x), Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (1 subgoal):
 1. \<And>s x y xb. \<lbrakk>is_subject aag receiver; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; integrity aag X st s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; kheap s (hd x) = Some (TCB y); sender_can_grant_reply xb; AllowGrant \<in> rights; (pasObjectAbs aag (hd x), Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Control, pasObjectAbs aag (hd x)) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!