theory Ipc_AC

lemma send_ipc_integrity_autarch:
  "\<lbrace>integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and
    obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r \<in> refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr and
    K (is_subject aag sender \<and> aag_has_auth_to aag SyncSend epptr \<and>
       (can_grant_reply \<longrightarrow> aag_has_auth_to aag Call epptr))\<rbrace>
   send_ipc block call badge can_grant can_grant_reply sender epptr
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: send_ipc_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (case_tac ep)
    \<comment> \<open>IdleEP\<close> apply simp apply (rule hoare_pre) apply (wp set_endpoint_respects  set_thread_state_integrity_autarch | wpc | simp)+ apply (fastforce simp: obj_at_def is_ep) \<comment> \<open>ep_at and has_auth\<close>
   \<comment> \<open>SendEP\<close> apply simp apply (rule hoare_pre) apply (wp set_endpoint_respects  set_thread_state_integrity_autarch | wpc | simp)+ apply (fastforce simp: obj_at_def is_ep) \<comment> \<open>ep_at and has_auth\<close>
  \<comment> \<open>WaitingEP\<close> apply (rename_tac list) apply simp apply (case_tac "is_subject aag (hd list)") \<comment> \<open>autarch or not on receiver side\<close> apply clarsimp apply (rule hoare_pre) apply (wp setup_caller_cap_integrity_autarch set_thread_state_integrity_autarch thread_get_wp'
           | wpc)+ apply (rule_tac Q="\<lambda>rv s. integrity aag X st s \<and> (can_grant \<longrightarrow> is_subject aag (hd list))"
                       in hoare_strengthen_post[rotated]) apply simp+ apply (wp set_thread_state_integrity_autarch thread_get_wp'
                    do_ipc_transfer_integrity_autarch
                    hoare_vcg_all_lift hoare_drop_imps set_endpoint_respects
                 | wpc | simp add: get_thread_state_def split del: if_split del: hoare_True_E_R)+ apply (fastforce simp: a_type_def obj_at_def is_ep elim: send_ipc_valid_ep_helper)
  \<comment> \<open>we don't own head of queue\<close> apply clarsimp apply (rule use_spec') \<comment> \<open>Name initial state\<close> apply (simp add: spec_valid_def) \<comment> \<open>no imp rule?\<close> apply (rule hoare_pre) apply (wpc, wp) apply (rename_tac list s receiver queue) apply (rule_tac Q="\<lambda>_ s'. integrity aag X st s \<and>
                             integrity_tcb_in_ipc aag X receiver epptr TRFinal s s'" in hoare_post_imp) apply (fastforce dest!: integrity_tcb_in_ipc_final elim!: integrity_trans) apply (wp setup_caller_cap_respects_in_ipc_reply
             set_thread_state_respects_in_ipc_autarch[where param_b = Inactive]
             hoare_vcg_if_lift hoare_weak_lift_imp possible_switch_to_respects_in_ipc_autarch
             set_thread_state_running_respects_in_ipc do_ipc_transfer_respects_in_ipc thread_get_inv
             set_endpoint_integrity_in_ipc
          | wpc
          | strengthen integrity_tcb_in_ipc_no_call
          | wp hoare_drop_imps
          | simp add:get_thread_state_def)+ apply (clarsimp intro: integrity_tcb_in_ipc_refl) apply (frule_tac t=x in sym_ref_endpoint_recvD[OF invs_sym_refs],assumption,simp) apply (clarsimp simp: st_tcb_at_tcb_states_of_state_eq st_tcb_at_tcb_states_of_state direct_call_def) apply (subgoal_tac "\<not> can_grant") apply (force intro!: integrity_tcb_in_ipc_refl
                  simp: st_tcb_at_tcb_states_of_state
                  elim: send_ipc_valid_ep_helper) apply (force elim: obj_at_ko_atE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr and K (is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag))\<rbrace> send_ipc block call badge can_grant can_grant_reply sender epptr \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr\<rbrace> send_ipc block call badge can_grant can_grant_reply sender epptr \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr\<rbrace> do ep <- get_endpoint epptr;
case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep. is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ep. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = IdleEP\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ep x2. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>ep x3. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ep. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = IdleEP\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint IdleEP) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ep x2. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>ep x3. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ep. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = IdleEP\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 ep\<rbrace> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ep s. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = IdleEP; (ko_at (Endpoint IdleEP) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)) s\<rbrakk> \<Longrightarrow> ?Q7 ep s
 3. \<And>ep x2. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>ep x3. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ep s. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = IdleEP; ko_at (Endpoint IdleEP) epptr s \<and> integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr s\<rbrakk> \<Longrightarrow> block \<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>ep x2. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>ep x3. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep x2. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ep x3. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep x2. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case block of True \<Rightarrow> do set_thread_state sender (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 (x2 @ [sender])
od | False \<Rightarrow> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ep x3. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ep x2. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q60 ep x2\<rbrace> case block of True \<Rightarrow> do set_thread_state sender (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 (x2 @ [sender])
od | False \<Rightarrow> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ep x2 s. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = SendEP x2; (ko_at (Endpoint (SendEP x2)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)) s\<rbrakk> \<Longrightarrow> ?Q60 ep x2 s
 3. \<And>ep x3. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep x2 s. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = SendEP x2; ko_at (Endpoint (SendEP x2)) epptr s \<and> integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr s\<rbrakk> \<Longrightarrow> block \<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>ep x3. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep x3. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep list. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP list\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 [sender]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state sender (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 @ [sender])
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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep list. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP list\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep list. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP list; is_subject aag (hd list)\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ep list. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP list; pasObjectAbs aag (hd list) \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>list. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ep list. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP list; pasObjectAbs aag (hd list) \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>list. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>?Q119 list\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>list s. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; (ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)) s\<rbrakk> \<Longrightarrow> ?Q119 list s
 3. \<And>ep list. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP list; pasObjectAbs aag (hd list) \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>list x21 x22 x recv_state reply_can_grant xa. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B142 list x21 x22 x recv_state reply_can_grant xa\<rbrace> do_extended_op (possible_switch_to x21) \<lbrace>\<lambda>xb. if call then \<lambda>s. (can_grant \<or> can_grant_reply \<longrightarrow> (integrity aag X st and K (is_subject aag sender) and K (is_subject aag (fst (sender, tcb_cnode_index 2)) \<and> is_subject aag (fst (x21, tcb_cnode_index 3)))) s) \<and> (\<not> (can_grant \<or> can_grant_reply) \<longrightarrow> (integrity aag X st and K (is_subject aag sender)) s) else integrity aag X st\<rbrace>
 2. \<And>list x21 x22 x recv_state reply_can_grant. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B141 list x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B142 list x21 x22 x recv_state reply_can_grant\<rbrace>
 3. \<And>list x21 x22 x recv_state. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B140 list x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer sender (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B141 list x21 x22 x recv_state\<rbrace>
 4. \<And>list x21 x22 x. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B138 list x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B140 list x21 x22 x\<rbrace>
 5. \<And>list x21 x22. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R132 list x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B138 list x21 x22\<rbrace>
 6. \<And>list s. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; (ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)) s\<rbrakk> \<Longrightarrow> (list = [] \<longrightarrow> True) \<and> (\<forall>x xa. list = x # xa \<longrightarrow> ?R132 list x xa s)
 7. \<And>ep list. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP list; pasObjectAbs aag (hd list) \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>list x21 x22 x recv_state reply_can_grant xa rv s. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22; integrity aag X st s \<and> (can_grant \<longrightarrow> is_subject aag (hd list))\<rbrakk> \<Longrightarrow> (if call then \<lambda>s. (can_grant \<or> can_grant_reply \<longrightarrow> (integrity aag X st and K (is_subject aag sender) and K (is_subject aag (fst (sender, tcb_cnode_index 2)) \<and> is_subject aag (fst (x21, tcb_cnode_index 3)))) s) \<and> (\<not> (can_grant \<or> can_grant_reply) \<longrightarrow> (integrity aag X st and K (is_subject aag sender)) s) else integrity aag X st) s
 2. \<And>list x21 x22 x recv_state reply_can_grant xa. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B142 list x21 x22 x recv_state reply_can_grant xa\<rbrace> do_extended_op (possible_switch_to x21) \<lbrace>\<lambda>rv s. integrity aag X st s \<and> (can_grant \<longrightarrow> is_subject aag (hd list))\<rbrace>
 3. \<And>list x21 x22 x recv_state reply_can_grant. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B141 list x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B142 list x21 x22 x recv_state reply_can_grant\<rbrace>
 4. \<And>list x21 x22 x recv_state. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B140 list x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer sender (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B141 list x21 x22 x recv_state\<rbrace>
 5. \<And>list x21 x22 x. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B138 list x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B140 list x21 x22 x\<rbrace>
 6. \<And>list x21 x22. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R132 list x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B138 list x21 x22\<rbrace>
 7. \<And>list s. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; (ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)) s\<rbrakk> \<Longrightarrow> (list = [] \<longrightarrow> True) \<and> (\<forall>x xa. list = x # xa \<longrightarrow> ?R132 list x xa s)
 8. \<And>ep list. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP list; pasObjectAbs aag (hd list) \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>list x21 x22 recv_state reply_can_grant. \<lbrakk>is_subject aag x21; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B142 (x21 # x22) x21 x22 () recv_state reply_can_grant ()\<rbrace> possible_switch_to x21 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>list x21 x22 x recv_state reply_can_grant. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B141 list x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B142 list x21 x22 x recv_state reply_can_grant\<rbrace>
 3. \<And>list x21 x22 x recv_state. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B140 list x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer sender (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B141 list x21 x22 x recv_state\<rbrace>
 4. \<And>list x21 x22 x. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B138 list x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B140 list x21 x22 x\<rbrace>
 5. \<And>list x21 x22. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R132 list x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B138 list x21 x22\<rbrace>
 6. \<And>list s. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; (ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)) s\<rbrakk> \<Longrightarrow> (list = [] \<longrightarrow> True) \<and> (\<forall>x xa. list = x # xa \<longrightarrow> ?R132 list x xa s)
 7. \<And>ep list. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP list; pasObjectAbs aag (hd list) \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>list s. \<lbrakk>is_subject aag (hd list); is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP list)) epptr s \<and> integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr s\<rbrakk> \<Longrightarrow> \<forall>x xa. list = x # xa \<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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> is_subject aag x
 2. \<And>ep list. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP list; pasObjectAbs aag (hd list) \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep list. \<lbrakk>is_subject aag sender \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP list; pasObjectAbs aag (hd list) \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>list. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>list s. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>ko_at (Endpoint (RecvEP list)) epptr and (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr)\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>list s. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> ko_at (Endpoint (RecvEP list)) epptr sa \<and> integrity aag X st sa \<and> pas_refined aag sa \<and> invs sa \<and> is_subject aag (cur_thread sa) \<and> obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr sa\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>list s. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>?Q385 list s\<rbrace> case list of [] \<Rightarrow> fail | 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 sender (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 sender dest reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>list s sa. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; sa = s \<and> ko_at (Endpoint (RecvEP list)) epptr sa \<and> integrity aag X st sa \<and> pas_refined aag sa \<and> invs sa \<and> is_subject aag (cur_thread sa) \<and> obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr sa\<rbrakk> \<Longrightarrow> ?Q385 list s sa proof (prove)
goal (2 subgoals):
 1. \<And>list s x21 x22. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R398 list s x21 x22\<rbrace> do set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22;
recv_state <- get_thread_state x21;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer sender (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state x21 Running;
do_extended_op (possible_switch_to x21);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap sender x21 reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>list s sa. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; sa = s \<and> ko_at (Endpoint (RecvEP list)) epptr sa \<and> integrity aag X st sa \<and> pas_refined aag sa \<and> invs sa \<and> is_subject aag (cur_thread sa) \<and> obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr sa\<rbrakk> \<Longrightarrow> (list = [] \<longrightarrow> True) \<and> (\<forall>x xa. list = x # xa \<longrightarrow> ?R398 list s x xa sa) proof (prove)
goal (2 subgoals):
 1. \<And>list s receiver queue. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = receiver # queue\<rbrakk> \<Longrightarrow> \<lbrace>?R398 list s receiver queue\<rbrace> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state receiver;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer sender (Some epptr) badge can_grant receiver;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap sender receiver reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>list s sa. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; sa = s \<and> ko_at (Endpoint (RecvEP list)) epptr sa \<and> integrity aag X st sa \<and> pas_refined aag sa \<and> invs sa \<and> is_subject aag (cur_thread sa) \<and> obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr sa\<rbrakk> \<Longrightarrow> (list = [] \<longrightarrow> True) \<and> (\<forall>x xa. list = x # xa \<longrightarrow> ?R398 list s x xa sa) proof (prove)
goal (3 subgoals):
 1. \<And>list s receiver queue rv sa. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = receiver # queue; integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver epptr TRFinal s sa\<rbrakk> \<Longrightarrow> integrity aag X st sa
 2. \<And>list s receiver queue. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = receiver # queue\<rbrakk> \<Longrightarrow> \<lbrace>?R398 list s receiver queue\<rbrace> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state receiver;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer sender (Some epptr) badge can_grant receiver;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap sender receiver reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_ s'. integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver epptr TRFinal s s'\<rbrace>
 3. \<And>list s sa. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; sa = s \<and> ko_at (Endpoint (RecvEP list)) epptr sa \<and> integrity aag X st sa \<and> pas_refined aag sa \<and> invs sa \<and> is_subject aag (cur_thread sa) \<and> obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr sa\<rbrakk> \<Longrightarrow> (list = [] \<longrightarrow> True) \<and> (\<forall>x xa. list = x # xa \<longrightarrow> ?R398 list s x xa sa) proof (prove)
goal (2 subgoals):
 1. \<And>list s receiver queue. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; list = receiver # queue\<rbrakk> \<Longrightarrow> \<lbrace>?R398 list s receiver queue\<rbrace> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state receiver;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer sender (Some epptr) badge can_grant receiver;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap sender receiver reply_can_grant else set_thread_state sender Inactive
od \<lbrace>\<lambda>_ s'. integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver epptr TRFinal s s'\<rbrace>
 2. \<And>list s sa. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; sa = s \<and> ko_at (Endpoint (RecvEP list)) epptr sa \<and> integrity aag X st sa \<and> pas_refined aag sa \<and> invs sa \<and> is_subject aag (cur_thread sa) \<and> obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr sa\<rbrakk> \<Longrightarrow> (list = [] \<longrightarrow> True) \<and> (\<forall>x xa. list = x # xa \<longrightarrow> ?R398 list s x xa sa) proof (prove)
goal (1 subgoal):
 1. \<And>list s. \<lbrakk>pasObjectAbs aag (hd list) \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP list)) epptr s \<and> integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr s\<rbrakk> \<Longrightarrow> \<forall>x xa. list = x # xa \<longrightarrow> (call \<longrightarrow> \<not> can_grant \<and> (can_grant_reply \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> st_tcb_at can_receive_ipc x s \<and> \<not> can_grant \<and> st_tcb_at (receive_blocked_on epptr) x s \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) x s) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> st_tcb_at can_receive_ipc x s \<and> st_tcb_at (receive_blocked_on epptr) x s)) \<and> (\<not> call \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> st_tcb_at can_receive_ipc x s \<and> \<not> can_grant \<and> st_tcb_at (receive_blocked_on epptr) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>pasObjectAbs aag x \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (x # xa))) epptr s; integrity aag X st s; pas_refined aag s; invs s; is_subject aag (cur_thread s); obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr s\<rbrakk> \<Longrightarrow> (call \<longrightarrow> \<not> can_grant \<and> (can_grant_reply \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> st_tcb_at can_receive_ipc x s \<and> \<not> can_grant \<and> st_tcb_at (receive_blocked_on epptr) x s \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) x s) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> st_tcb_at can_receive_ipc x s \<and> st_tcb_at (receive_blocked_on epptr) x s)) \<and> (\<not> call \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> st_tcb_at can_receive_ipc x s \<and> \<not> can_grant \<and> st_tcb_at (receive_blocked_on epptr) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>pasObjectAbs aag x \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (x # xa))) epptr s; integrity aag X st s; pas_refined aag s; invs s; is_subject aag (cur_thread s); obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr s; \<exists>pl. st_tcb_at ((=) (BlockedOnReceive epptr pl)) x s\<rbrakk> \<Longrightarrow> (call \<longrightarrow> \<not> can_grant \<and> (can_grant_reply \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> st_tcb_at can_receive_ipc x s \<and> \<not> can_grant \<and> st_tcb_at (receive_blocked_on epptr) x s \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) x s) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> st_tcb_at can_receive_ipc x s \<and> st_tcb_at (receive_blocked_on epptr) x s)) \<and> (\<not> call \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> st_tcb_at can_receive_ipc x s \<and> \<not> can_grant \<and> st_tcb_at (receive_blocked_on epptr) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa pl. \<lbrakk>pasObjectAbs aag x \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (x # xa))) epptr s; integrity aag X st s; pas_refined aag s; invs s; is_subject aag (cur_thread s); obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr s; tcb_states_of_state s x = Some (BlockedOnReceive epptr pl)\<rbrakk> \<Longrightarrow> (call \<longrightarrow> \<not> can_grant \<and> (can_grant_reply \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> \<not> can_grant) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s)) \<and> (\<not> call \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> \<not> can_grant) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa pl. \<lbrakk>pasObjectAbs aag x \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (x # xa))) epptr s; integrity aag X st s; pas_refined aag s; invs s; is_subject aag (cur_thread s); obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr s; tcb_states_of_state s x = Some (BlockedOnReceive epptr pl); \<not> can_grant\<rbrakk> \<Longrightarrow> (call \<longrightarrow> \<not> can_grant \<and> (can_grant_reply \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> \<not> can_grant) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s)) \<and> (\<not> call \<longrightarrow> integrity_tcb_in_ipc aag X x epptr TRContext s s \<and> 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 xa of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xa) s \<and> valid_mdb s \<and> \<not> can_grant)
 2. \<And>s x xa pl. \<lbrakk>pasObjectAbs aag x \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (x # xa))) epptr s; integrity aag X st s; pas_refined aag s; invs s; is_subject aag (cur_thread s); obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr s; tcb_states_of_state s x = Some (BlockedOnReceive epptr pl)\<rbrakk> \<Longrightarrow> \<not> can_grant proof (prove)
goal (1 subgoal):
 1. \<And>s x xa pl. \<lbrakk>pasObjectAbs aag x \<noteq> pasSubject aag; is_subject aag sender; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (x # xa))) epptr s; integrity aag X st s; pas_refined aag s; invs s; is_subject aag (cur_thread s); obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr s; tcb_states_of_state s x = Some (BlockedOnReceive epptr pl)\<rbrakk> \<Longrightarrow> \<not> can_grant proof (prove)
goal:
No subgoals!