theory Ipc_AC

lemma send_ipc_pas_refined:
  "\<lbrace>pas_refined aag and invs and
    K (is_subject aag thread \<and> aag_has_auth_to aag SyncSend epptr
                             \<and> (can_grant_reply \<longrightarrow> aag_has_auth_to aag Call epptr)
                             \<and> (can_grant \<longrightarrow> aag_has_auth_to aag Grant epptr
                                            \<and> aag_has_auth_to aag Call epptr))\<rbrace>
   send_ipc block call badge can_grant can_grant_reply thread epptr
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: send_ipc_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wpc | wp set_thread_state_pas_refined)+ apply (simp add: hoare_if_r_and split del:if_split) apply (wp setup_caller_cap_pas_refined set_thread_state_pas_refined)+ apply (simp split del:if_split) apply (rule_tac Q="\<lambda>rv. pas_refined aag and pspace_aligned and valid_vspace_objs and
                               valid_arch_state and valid_mdb and
                               K (can_grant \<or> can_grant_reply
                                  \<longrightarrow> (reply_can_grant \<longrightarrow> is_subject aag x21) \<and>
                                      (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag)"
                    in hoare_strengthen_post[rotated]) apply simp apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined hoare_weak_lift_imp gts_wp
              | wpc
              | simp add: hoare_if_r_and)+ apply (wp hoare_vcg_all_lift hoare_imp_lift_something | simp add: st_tcb_at_tcb_states_of_state_eq)+ subgoal for ep s  (* post-wp proof *)
     apply (intro conjI impI; clarsimp;
           frule(2) pas_refined_ep_recv[OF _ _ _ head_in_set]) subgoal  (* can_grant *)
       apply (frule(2) aag_wellformed_grant_Control_to_recv[OF _ _ pas_refined_wellformed]) apply (frule(2) aag_wellformed_reply[OF _ _ pas_refined_wellformed]) apply (force elim: send_ipc_valid_ep_helper simp:aag_has_Control_iff_owns) done subgoal  (* can_grant_reply and not can_grant*)
       apply (frule(2) aag_wellformed_reply[OF _ _ pas_refined_wellformed]) apply (frule(1) tcb_states_of_state_to_auth) 
      (* Make the blockedOnReceive state point to epptr *)
       apply (frule(1) sym_ref_endpoint_recvD[OF invs_sym_refs _ head_in_set],
             clarsimp simp:st_tcb_at_tcb_states_of_state_eq) apply (fastforce elim: send_ipc_valid_ep_helper
                       simp: aag_has_Control_iff_owns
                       dest: aag_wellformed_grant_Control_to_recv_by_reply
                               [OF _ _ _ pas_refined_wellformed]) done subgoal  (* not can_grant_reply and not can_grant*)
       by (force elim: send_ipc_valid_ep_helper) done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag))\<rbrace> send_ipc block call badge can_grant can_grant_reply thread epptr \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> send_ipc block call badge can_grant can_grant_reply thread epptr \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> do ep <- get_endpoint epptr;
case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP [thread]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP (queue @ [thread])
od | False \<Rightarrow> return () | RecvEP [] \<Rightarrow> fail | RecvEP (dest # queue) \<Rightarrow> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap thread dest reply_can_grant else set_thread_state thread Inactive
od
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep. is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) epptr and (pas_refined aag and invs)\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP [thread]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP (queue @ [thread])
od | False \<Rightarrow> return () | RecvEP [] \<Rightarrow> fail | RecvEP (dest # queue) \<Rightarrow> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap thread dest reply_can_grant else set_thread_state thread Inactive
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep. is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>?Q6 ep\<rbrace> case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP [thread]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP (queue @ [thread])
od | False \<Rightarrow> return () | RecvEP [] \<Rightarrow> fail | RecvEP (dest # queue) \<Rightarrow> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap thread dest reply_can_grant else set_thread_state thread Inactive
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>ep s. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); (ko_at (Endpoint ep) epptr and (pas_refined aag and invs)) s\<rbrakk> \<Longrightarrow> ?Q6 ep s proof (prove)
goal (8 subgoals):
 1. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa xb. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22; call; can_grant \<or> can_grant_reply\<rbrakk> \<Longrightarrow> \<lbrace>?Q105 ep x3 x21 x22 x recv_state reply_can_grant xa xb\<rbrace> setup_caller_cap thread x21 reply_can_grant \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa xb. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22; call; \<not> (can_grant \<or> can_grant_reply)\<rbrakk> \<Longrightarrow> \<lbrace>?R105 ep x3 x21 x22 x recv_state reply_can_grant xa xb\<rbrace> set_thread_state thread Inactive \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B99 ep x3 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> ?Q105 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) \<and> (\<not> (can_grant \<or> can_grant_reply) \<longrightarrow> ?R105 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) else pas_refined aag\<rbrace>
 4. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B98 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B99 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 5. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B97 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B98 ep x3 x21 x22 x recv_state\<rbrace>
 6. \<And>ep x3 x21 x22 x. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B95 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B97 ep x3 x21 x22 x\<rbrace>
 7. \<And>ep x3 x21 x22. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R89 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B95 ep x3 x21 x22\<rbrace>
 8. \<And>ep s. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); (ko_at (Endpoint ep) epptr and (pas_refined aag and invs)) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R89 ep x xa xb s)) proof (prove)
goal (8 subgoals):
 1. \<And>ep x3 x21 x22 recv_state reply_can_grant. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP (x21 # x22); x3 = x21 # x22; call; can_grant \<or> can_grant_reply\<rbrakk> \<Longrightarrow> \<lbrace>?Q105 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state reply_can_grant () ()\<rbrace> setup_caller_cap thread x21 reply_can_grant \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa xb. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22; call; \<not> (can_grant \<or> can_grant_reply)\<rbrakk> \<Longrightarrow> \<lbrace>?R105 ep x3 x21 x22 x recv_state reply_can_grant xa xb\<rbrace> set_thread_state thread Inactive \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B99 ep x3 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> ?Q105 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) \<and> (\<not> (can_grant \<or> can_grant_reply) \<longrightarrow> ?R105 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) else pas_refined aag\<rbrace>
 4. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B98 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B99 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 5. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B97 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B98 ep x3 x21 x22 x recv_state\<rbrace>
 6. \<And>ep x3 x21 x22 x. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B95 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B97 ep x3 x21 x22 x\<rbrace>
 7. \<And>ep x3 x21 x22. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R89 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B95 ep x3 x21 x22\<rbrace>
 8. \<And>ep s. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); (ko_at (Endpoint ep) epptr and (pas_refined aag and invs)) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R89 ep x xa xb s)) proof (prove)
goal (6 subgoals):
 1. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B99 ep x3 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> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and K ((reply_can_grant \<longrightarrow> is_subject aag thread \<and> is_subject aag x21) \<and> (pasObjectAbs aag x21, Reply, pasObjectAbs aag thread) \<in> pasPolicy aag)) s) \<and> (\<not> (can_grant \<or> can_grant_reply) \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth Inactive. (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s) else pas_refined aag\<rbrace>
 2. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B98 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B99 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B97 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B98 ep x3 x21 x22 x recv_state\<rbrace>
 4. \<And>ep x3 x21 x22 x. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B95 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B97 ep x3 x21 x22 x\<rbrace>
 5. \<And>ep x3 x21 x22. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R89 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B95 ep x3 x21 x22\<rbrace>
 6. \<And>ep s. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); (ko_at (Endpoint ep) epptr and (pas_refined aag and invs)) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R89 ep x xa xb s)) proof (prove)
goal (6 subgoals):
 1. \<And>ep x3 x21 x22 recv_state reply_can_grant. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP (x21 # x22); x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B99 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state reply_can_grant ()\<rbrace> possible_switch_to x21 \<lbrace>\<lambda>xb. if call then \<lambda>s. (can_grant \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (reply_can_grant \<longrightarrow> is_subject aag x21) \<and> (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag) \<and> (can_grant_reply \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (reply_can_grant \<longrightarrow> is_subject aag x21) \<and> (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) else pas_refined aag\<rbrace>
 2. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B98 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B99 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B97 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B98 ep x3 x21 x22 x recv_state\<rbrace>
 4. \<And>ep x3 x21 x22 x. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B95 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B97 ep x3 x21 x22 x\<rbrace>
 5. \<And>ep x3 x21 x22. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R89 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B95 ep x3 x21 x22\<rbrace>
 6. \<And>ep s. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); (ko_at (Endpoint ep) epptr and (pas_refined aag and invs)) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R89 ep x xa xb s)) proof (prove)
goal (7 subgoals):
 1. \<And>ep x3 x21 x22 recv_state reply_can_grant rv s. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP (x21 # x22); x3 = x21 # x22; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and K (can_grant \<or> can_grant_reply \<longrightarrow> (reply_can_grant \<longrightarrow> is_subject aag x21) \<and> (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag)) s\<rbrakk> \<Longrightarrow> (if call then \<lambda>s. (can_grant \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (reply_can_grant \<longrightarrow> is_subject aag x21) \<and> (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag) \<and> (can_grant_reply \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (reply_can_grant \<longrightarrow> is_subject aag x21) \<and> (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) else pas_refined aag) s
 2. \<And>ep x3 x21 x22 recv_state reply_can_grant. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP (x21 # x22); x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B99 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state reply_can_grant ()\<rbrace> possible_switch_to x21 \<lbrace>\<lambda>rv. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and K (can_grant \<or> can_grant_reply \<longrightarrow> (reply_can_grant \<longrightarrow> is_subject aag x21) \<and> (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag)\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B98 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B99 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 4. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B97 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B98 ep x3 x21 x22 x recv_state\<rbrace>
 5. \<And>ep x3 x21 x22 x. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B95 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B97 ep x3 x21 x22 x\<rbrace>
 6. \<And>ep x3 x21 x22. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R89 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B95 ep x3 x21 x22\<rbrace>
 7. \<And>ep s. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); (ko_at (Endpoint ep) epptr and (pas_refined aag and invs)) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R89 ep x xa xb s)) proof (prove)
goal (6 subgoals):
 1. \<And>ep x3 x21 x22 recv_state reply_can_grant. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP (x21 # x22); x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B99 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state reply_can_grant ()\<rbrace> possible_switch_to x21 \<lbrace>\<lambda>rv. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and K (can_grant \<or> can_grant_reply \<longrightarrow> (reply_can_grant \<longrightarrow> is_subject aag x21) \<and> (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag)\<rbrace>
 2. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B98 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B99 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B97 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B98 ep x3 x21 x22 x recv_state\<rbrace>
 4. \<And>ep x3 x21 x22 x. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B95 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B97 ep x3 x21 x22 x\<rbrace>
 5. \<And>ep x3 x21 x22. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R89 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B95 ep x3 x21 x22\<rbrace>
 6. \<And>ep s. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); (ko_at (Endpoint ep) epptr and (pas_refined aag and invs)) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R89 ep x xa xb s)) proof (prove)
goal (2 subgoals):
 1. \<And>ep x3 x21 x22. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ep = RecvEP (x21 # x22); x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R89 (RecvEP (x21 # x22)) (x21 # x22) x21 x22\<rbrace> set_endpoint epptr (case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22) \<lbrace>\<lambda>x s. \<forall>st. st_tcb_at ((=) st) x21 s \<longrightarrow> (\<forall>x xa. st = BlockedOnReceive x xa \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (can_grant \<longrightarrow> is_subject aag x21) \<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_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (can_grant \<longrightarrow> (receiver_can_grant xa \<longrightarrow> is_subject aag x21) \<and> (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag) \<and> (can_grant_reply \<longrightarrow> (receiver_can_grant xa \<longrightarrow> is_subject aag x21) \<and> (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag))\<rbrace>
 2. \<And>ep s. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); (ko_at (Endpoint ep) epptr and (pas_refined aag and invs)) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>). (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> pas_refined aag s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R89 ep x xa xb s)) proof (prove)
goal (1 subgoal):
 1. \<And>ep s. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ko_at (Endpoint ep) epptr s \<and> pas_refined aag s \<and> invs s\<rbrakk> \<Longrightarrow> (can_grant \<longrightarrow> (ep = IdleEP \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. ep = SendEP x) \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<forall>xc xd. x = BlockedOnReceive xc xd \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> is_subject aag xa \<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_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xd \<longrightarrow> is_subject aag xa) \<and> (pasObjectAbs aag xa, Reply, pasSubject aag) \<in> pasPolicy aag))))) \<and> (\<not> can_grant \<longrightarrow> (can_grant_reply \<longrightarrow> (ep = IdleEP \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. ep = SendEP x) \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<forall>xc xd. x = BlockedOnReceive xc xd \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> 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_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xd \<longrightarrow> is_subject aag xa) \<and> (pasObjectAbs aag xa, Reply, pasSubject aag) \<in> pasPolicy aag))))) \<and> (\<not> can_grant_reply \<longrightarrow> (ep = IdleEP \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. ep = SendEP x) \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ko_at (Endpoint ep) epptr s \<and> pas_refined aag s \<and> invs s\<rbrakk> \<Longrightarrow> (can_grant \<longrightarrow> (ep = IdleEP \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. ep = SendEP x) \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<forall>xc xd. x = BlockedOnReceive xc xd \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> is_subject aag xa \<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_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xd \<longrightarrow> is_subject aag xa) \<and> (pasObjectAbs aag xa, Reply, pasSubject aag) \<in> pasPolicy aag))))) \<and> (\<not> can_grant \<longrightarrow> (can_grant_reply \<longrightarrow> (ep = IdleEP \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. ep = SendEP x) \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<forall>xc xd. x = BlockedOnReceive xc xd \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> 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_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xd \<longrightarrow> is_subject aag xa) \<and> (pasObjectAbs aag xa, Reply, pasSubject aag) \<in> pasPolicy aag))))) \<and> (\<not> can_grant_reply \<longrightarrow> (ep = IdleEP \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. ep = SendEP x) \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag); ko_at (Endpoint ep) epptr s \<and> pas_refined aag s \<and> invs s\<rbrakk> \<Longrightarrow> (can_grant \<longrightarrow> (ep = IdleEP \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. ep = SendEP x) \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<forall>xc xd. x = BlockedOnReceive xc xd \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> is_subject aag xa \<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_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xd \<longrightarrow> is_subject aag xa) \<and> (pasObjectAbs aag xa, Reply, pasSubject aag) \<in> pasPolicy aag))))) \<and> (\<not> can_grant \<longrightarrow> (can_grant_reply \<longrightarrow> (ep = IdleEP \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. ep = SendEP x) \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<forall>xc xd. x = BlockedOnReceive xc xd \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> 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_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xd \<longrightarrow> is_subject aag xa) \<and> (pasObjectAbs aag xa, Reply, pasSubject aag) \<in> pasPolicy aag))))) \<and> (\<not> can_grant_reply \<longrightarrow> (ep = IdleEP \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. ep = SendEP x) \<longrightarrow> block \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s))))) proof (prove)
goal (3 subgoals):
 1. \<And>xa xb xd xe. \<lbrakk>can_grant; is_subject aag thread; ko_at (Endpoint (RecvEP (xa # xb))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP (xa # xb); tcb_states_of_state s xa = Some (BlockedOnReceive xd xe); (pasObjectAbs aag xa, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> is_subject aag xa \<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_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe \<longrightarrow> is_subject aag xa) \<and> (pasObjectAbs aag xa, Reply, pasSubject aag) \<in> pasPolicy aag
 2. \<And>xa xb xd xe. \<lbrakk>\<not> can_grant; can_grant_reply; is_subject aag thread; ko_at (Endpoint (RecvEP (xa # xb))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = RecvEP (xa # xb); tcb_states_of_state s xa = Some (BlockedOnReceive xd xe); (pasObjectAbs aag xa, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe \<longrightarrow> is_subject aag xa) \<and> (pasObjectAbs aag xa, Reply, pasSubject aag) \<in> pasPolicy aag
 3. \<And>xa xb xd xe. \<lbrakk>\<not> can_grant; \<not> can_grant_reply; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (xa # xb))) epptr s; pas_refined aag s; invs s; ep = RecvEP (xa # xb); tcb_states_of_state s xa = Some (BlockedOnReceive xd xe); (pasObjectAbs aag xa, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>can_grant; is_subject aag thread; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive xd_ xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> is_subject aag xa_ \<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_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe_ \<longrightarrow> is_subject aag xa_) \<and> (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>can_grant; is_subject aag thread; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive xd_ xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> is_subject aag xa_ \<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_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe_ \<longrightarrow> is_subject aag xa_) \<and> (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>can_grant; is_subject aag thread; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive xd_ xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Control, pasObjectAbs aag xa_) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> is_subject aag xa_ \<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_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe_ \<longrightarrow> is_subject aag xa_) \<and> (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>can_grant; is_subject aag thread; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive xd_ xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Control, pasObjectAbs aag xa_) \<in> pasPolicy aag; (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> is_subject aag xa_ \<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_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe_ \<longrightarrow> is_subject aag xa_) \<and> (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal:
No subgoals! proof (prove)
goal (2 subgoals):
 1. \<And>xa xb xd xe. \<lbrakk>\<not> can_grant; can_grant_reply; is_subject aag thread; ko_at (Endpoint (RecvEP (xa # xb))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = RecvEP (xa # xb); tcb_states_of_state s xa = Some (BlockedOnReceive xd xe); (pasObjectAbs aag xa, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe \<longrightarrow> is_subject aag xa) \<and> (pasObjectAbs aag xa, Reply, pasSubject aag) \<in> pasPolicy aag
 2. \<And>xa xb xd xe. \<lbrakk>\<not> can_grant; \<not> can_grant_reply; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (xa # xb))) epptr s; pas_refined aag s; invs s; ep = RecvEP (xa # xb); tcb_states_of_state s xa = Some (BlockedOnReceive xd xe); (pasObjectAbs aag xa, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> can_grant; can_grant_reply; is_subject aag thread; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive xd_ xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe_ \<longrightarrow> is_subject aag xa_) \<and> (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> can_grant; can_grant_reply; is_subject aag thread; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive xd_ xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe_ \<longrightarrow> is_subject aag xa_) \<and> (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> can_grant; can_grant_reply; is_subject aag thread; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive xd_ xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe_ \<longrightarrow> is_subject aag xa_) \<and> (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> can_grant; can_grant_reply; is_subject aag thread; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive xd_ xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag; \<forall>(obj, auth)\<in>tcb_st_to_auth (BlockedOnReceive xd_ xe_). (pasObjectAbs aag xa_, auth, pasObjectAbs aag obj) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe_ \<longrightarrow> is_subject aag xa_) \<and> (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> can_grant; can_grant_reply; is_subject aag thread; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive xd_ xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag; \<forall>(obj, auth)\<in>tcb_st_to_auth (BlockedOnReceive xd_ xe_). (pasObjectAbs aag xa_, auth, pasObjectAbs aag obj) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe_ \<longrightarrow> is_subject aag xa_) \<and> (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> can_grant; can_grant_reply; is_subject aag thread; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive epptr xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasObjectAbs aag xa_, Reply, pasSubject aag) \<in> pasPolicy aag; \<forall>x\<in>if receiver_can_grant xe_ then {(epptr, Grant)} else {}. case x of (obj, auth) \<Rightarrow> (pasObjectAbs aag xa_, auth, pasObjectAbs aag obj) \<in> pasPolicy aag; xd_ = epptr\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (receiver_can_grant xe_ \<longrightarrow> is_subject aag xa_) proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<And>xa xb xd xe. \<lbrakk>\<not> can_grant; \<not> can_grant_reply; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (xa # xb))) epptr s; pas_refined aag s; invs s; ep = RecvEP (xa # xb); tcb_states_of_state s xa = Some (BlockedOnReceive xd xe); (pasObjectAbs aag xa, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> pspace_aligned s \<and> pspace_distinct s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> can_grant; \<not> can_grant_reply; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; pas_refined aag s; invs s; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive xd_ xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> can_grant; \<not> can_grant_reply; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (xa_ # xb_))) epptr s; pas_refined aag s; invs s; ep = RecvEP (xa_ # xb_); tcb_states_of_state s xa_ = Some (BlockedOnReceive xd_ xe_); (pasObjectAbs aag xa_, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case xb_ of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb_) s \<and> pspace_aligned s \<and> pspace_distinct s proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!