theory Ipc_AC

lemma receive_ipc_base_pas_refined:
  "\<lbrace>pas_refined aag and invs and ko_at (Endpoint ep) epptr and
    K (is_subject aag thread \<and> aag_has_auth_to aag Receive epptr \<and>
       (\<forall>auth \<in> cap_rights_to_auth rights True . aag_has_auth_to aag auth epptr))\<rbrace>
   receive_ipc_base aag thread ep epptr rights is_blocking
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 
  (* FIXME: proof structure *)
   apply (rule hoare_gen_asm) apply (clarsimp simp: thread_get_def cong: endpoint.case_cong) apply (rule hoare_pre) apply (wp set_thread_state_pas_refined get_simple_ko_wp setup_caller_cap_pas_refined
          | wpc | simp add: thread_get_def do_nbrecv_failed_transfer_def split del: if_split)+ apply (rename_tac list sss data) apply (rule_tac Q="\<lambda>rv s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and>
                                  valid_arch_state s \<and> valid_mdb s \<and>
                                  (sender_can_grant data \<longrightarrow> is_subject aag (hd list)) \<and>
                                  (sender_can_grant_reply data \<longrightarrow>
                                  (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and>
                                  aag_has_auth_to aag Reply (hd list))"
                     in hoare_strengthen_post[rotated]) apply (fastforce simp: pas_refined_refl) apply (wp hoare_weak_lift_imp do_ipc_transfer_pas_refined set_simple_ko_pas_refined
                  set_thread_state_pas_refined get_simple_ko_wp hoare_vcg_all_lift
                  hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1]
               | wpc
               | simp add: thread_get_def  get_thread_state_def do_nbrecv_failed_transfer_def)+ apply (clarsimp simp: tcb_at_def [symmetric] tcb_at_st_tcb_at) apply (simp only: invs_psp_aligned invs_vspace_objs invs_arch_state simp_thms) subgoal premises prems for s proof - have "\<And>P Q R. \<lbrakk> R ; P \<Longrightarrow> R \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> (\<not>P \<longrightarrow> R)" by blast thus ?thesis apply this using prems apply clarsimp subgoal premises prems for list ep' pl proof - have "sender_can_grant pl \<Longrightarrow> is_subject aag (hd list)" using prems apply (clarsimp elim!: tcb_atE simp:tcb_at_st_tcb_at[symmetric] get_tcb_def) apply (frule(1) sym_ref_endpoint_sendD[OF invs_sym_refs,where t= "hd list"],force) apply (clarsimp simp:st_tcb_at_def elim!:obj_atE) by (rule receive_ipc_sender_can_grant_helper) moreover have
          "sender_can_grant_reply pl \<Longrightarrow> aag_has_auth_to aag Reply (hd list)" using prems apply (clarsimp elim!: tcb_atE simp:tcb_at_st_tcb_at[symmetric] get_tcb_def) apply (frule(1) sym_ref_endpoint_sendD[OF invs_sym_refs,where t= "hd list"],force) apply (clarsimp simp:st_tcb_at_def elim!:obj_atE) apply (frule pas_refined_mem[rotated,where x = "(hd list)" and auth=Call]) apply (rule sta_ts) apply (simp add:thread_st_auth_def tcb_states_of_state_def get_tcb_def) by (erule(2) aag_wellformed_reply[OF _ _ pas_refined_wellformed]) ultimately show ?thesis using prems by (force dest:receive_ipc_valid_ep_helper) qed apply clarsimp using prems apply (intro conjI;clarsimp simp add:cap_rights_to_auth_def) apply (clarsimp elim!: tcb_atE simp:tcb_at_st_tcb_at[symmetric] get_tcb_def
                             cap_rights_to_auth_def) apply (frule_tac t="hd x" in sym_ref_endpoint_sendD[OF invs_sym_refs],assumption,force) apply (clarsimp simp:st_tcb_at_def elim!:obj_atE) apply (frule_tac x="hd x" in pas_refined_mem[rotated,where auth=Call]) apply (rule sta_ts) apply (simp add:thread_st_auth_def tcb_states_of_state_def get_tcb_def) apply (frule aag_wellformed_grant_Control_to_send_by_reply[OF _ _ _ pas_refined_wellformed]) by (force simp:aag_has_Control_iff_owns)+ qed done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and ko_at (Endpoint ep) epptr and K (is_subject aag thread \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref data \<Rightarrow> return data | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some epptr) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> rights) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and ko_at (Endpoint ep) epptr and K (is_subject aag thread \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref data \<Rightarrow> return data | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some epptr) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> rights) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>pas_refined aag and invs and ko_at (Endpoint ep) epptr\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref data \<Rightarrow> return data | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some epptr) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> rights) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and ko_at (Endpoint ep) epptr\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do y <- assert (q \<noteq> []);
y <- set_endpoint epptr (case tl q of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl q));
sender_state <- get_thread_state (hd q);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd q) (Some epptr) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap (hd q) thread (AllowGrant \<in> rights) else set_thread_state (hd q) Inactive else do y <- set_thread_state (hd q) Running;
possible_switch_to (hd q)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>?Q9\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do y <- assert (q \<noteq> []);
y <- set_endpoint epptr (case tl q of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl q));
sender_state <- get_thread_state (hd q);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd q) (Some epptr) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap (hd q) thread (AllowGrant \<in> rights) else set_thread_state (hd q) Inactive else do y <- set_thread_state (hd q) Running;
possible_switch_to (hd q)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pas_refined aag and invs and ko_at (Endpoint ep) epptr) s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (7 subgoals):
 1. \<And>x2 sender_state data. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B58 x2 () () sender_state data\<rbrace> do_ipc_transfer (hd x2) (Some epptr) (sender_badge data) (sender_can_grant data) thread \<lbrace>\<lambda>yb s. (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x2)) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x2)) \<in> pasPolicy aag) \<and> (sender_can_grant_reply data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x2)) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x2)) \<in> pasPolicy aag) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (\<not> sender_is_call data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)\<rbrace>
 2. \<And>x2 y ya sender_state. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x2 y ya sender_state\<rbrace> case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B58 x2 y ya sender_state\<rbrace>
 3. \<And>x2 y ya. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x2 y ya\<rbrace> get_thread_state (hd x2) \<lbrace>?B57 x2 y ya\<rbrace>
 4. \<And>x2 y. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B55 x2 y\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>?B56 x2 y\<rbrace>
 5. \<And>x2. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R24 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B55 x2\<rbrace>
 6. \<And>x3. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R25 x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (x3 @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 7. \<And>s. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pas_refined aag and invs and ko_at (Endpoint ep) epptr) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = 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 (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<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> (is_blocking = False \<longrightarrow> (pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag) s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R24 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R25 x s) proof (prove)
goal (7 subgoals):
 1. \<And>list sss data. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP list\<rbrakk> \<Longrightarrow> \<lbrace>?B58 list () () sss data\<rbrace> do_ipc_transfer (hd list) (Some epptr) (sender_badge data) (sender_can_grant data) thread \<lbrace>\<lambda>yb s. (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag) \<and> (sender_can_grant_reply data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (\<not> sender_is_call data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)\<rbrace>
 2. \<And>x2 y ya sender_state. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x2 y ya sender_state\<rbrace> case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B58 x2 y ya sender_state\<rbrace>
 3. \<And>x2 y ya. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x2 y ya\<rbrace> get_thread_state (hd x2) \<lbrace>?B57 x2 y ya\<rbrace>
 4. \<And>x2 y. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B55 x2 y\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>?B56 x2 y\<rbrace>
 5. \<And>x2. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R24 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B55 x2\<rbrace>
 6. \<And>x3. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R25 x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (x3 @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 7. \<And>s. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pas_refined aag and invs and ko_at (Endpoint ep) epptr) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = 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 (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<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> (is_blocking = False \<longrightarrow> (pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag) s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R24 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R25 x s) proof (prove)
goal (8 subgoals):
 1. \<And>list sss data rv s. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP list; pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (sender_can_grant data \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant_reply data \<longrightarrow> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag) \<and> (sender_can_grant_reply data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (\<not> sender_is_call data \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)
 2. \<And>list sss data. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP list\<rbrakk> \<Longrightarrow> \<lbrace>?B58 list () () sss data\<rbrace> do_ipc_transfer (hd list) (Some epptr) (sender_badge data) (sender_can_grant data) thread \<lbrace>\<lambda>rv s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (sender_can_grant data \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant_reply data \<longrightarrow> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag)\<rbrace>
 3. \<And>x2 y ya sender_state. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x2 y ya sender_state\<rbrace> case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B58 x2 y ya sender_state\<rbrace>
 4. \<And>x2 y ya. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x2 y ya\<rbrace> get_thread_state (hd x2) \<lbrace>?B57 x2 y ya\<rbrace>
 5. \<And>x2 y. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B55 x2 y\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>?B56 x2 y\<rbrace>
 6. \<And>x2. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R24 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B55 x2\<rbrace>
 7. \<And>x3. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R25 x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (x3 @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 8. \<And>s. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pas_refined aag and invs and ko_at (Endpoint ep) epptr) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = 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 (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<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> (is_blocking = False \<longrightarrow> (pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag) s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R24 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R25 x s) proof (prove)
goal (7 subgoals):
 1. \<And>list sss data. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP list\<rbrakk> \<Longrightarrow> \<lbrace>?B58 list () () sss data\<rbrace> do_ipc_transfer (hd list) (Some epptr) (sender_badge data) (sender_can_grant data) thread \<lbrace>\<lambda>rv s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (sender_can_grant data \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant_reply data \<longrightarrow> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag)\<rbrace>
 2. \<And>x2 y ya sender_state. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x2 y ya sender_state\<rbrace> case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B58 x2 y ya sender_state\<rbrace>
 3. \<And>x2 y ya. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x2 y ya\<rbrace> get_thread_state (hd x2) \<lbrace>?B57 x2 y ya\<rbrace>
 4. \<And>x2 y. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B55 x2 y\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>?B56 x2 y\<rbrace>
 5. \<And>x2. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R24 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B55 x2\<rbrace>
 6. \<And>x3. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R25 x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (x3 @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 7. \<And>s. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pas_refined aag and invs and ko_at (Endpoint ep) epptr) s\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = 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 (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<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> (is_blocking = False \<longrightarrow> (pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag) s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R24 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R25 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s \<and> invs s \<and> ko_at (Endpoint ep) epptr s\<rbrakk> \<Longrightarrow> (AllowGrant \<in> rights \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<exists>y. get_tcb (hd x) s = Some y) \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> 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 tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s))) \<and> (AllowGrant \<notin> rights \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking \<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> (\<not> is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<exists>y. get_tcb (hd x) s = Some y) \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> 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 tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> (is_blocking \<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> (\<not> is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ko_at (Endpoint ep) epptr s\<rbrakk> \<Longrightarrow> (AllowGrant \<in> rights \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> 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 tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s))) \<and> (AllowGrant \<notin> rights \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking \<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> (\<not> is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> 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 tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> (is_blocking \<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> (\<not> is_blocking \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ko_at (Endpoint ep) epptr s\<rbrakk> \<Longrightarrow> (AllowGrant \<in> rights \<longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)) \<and> (AllowGrant \<notin> rights \<longrightarrow> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag)))) proof (prove)
goal (1 subgoal):
 1. (AllowGrant \<in> rights \<longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)) \<and> (AllowGrant \<notin> rights \<longrightarrow> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag)))) proof (state)
goal (1 subgoal):
 1. (AllowGrant \<in> rights \<longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)) \<and> (AllowGrant \<notin> rights \<longrightarrow> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag)))) proof (prove)
goal (1 subgoal):
 1. \<And>P Q R. \<lbrakk>R; \<lbrakk>P; R\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R) proof (state)
this:
\<lbrakk>?R; \<lbrakk>?P; ?R\<rbrakk> \<Longrightarrow> ?Q\<rbrakk> \<Longrightarrow> (?P \<longrightarrow> ?Q) \<and> (\<not> ?P \<longrightarrow> ?R)

goal (1 subgoal):
 1. (AllowGrant \<in> rights \<longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)) \<and> (AllowGrant \<notin> rights \<longrightarrow> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag)))) proof (prove)
using this:
\<lbrakk>?R; \<lbrakk>?P; ?R\<rbrakk> \<Longrightarrow> ?Q\<rbrakk> \<Longrightarrow> (?P \<longrightarrow> ?Q) \<and> (\<not> ?P \<longrightarrow> ?R)

goal (1 subgoal):
 1. (AllowGrant \<in> rights \<longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)) \<and> (AllowGrant \<notin> rights \<longrightarrow> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag)))) proof (prove)
goal (2 subgoals):
 1. \<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))
 2. \<lbrakk>AllowGrant \<in> rights; \<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) proof (prove)
using this:
is_subject aag thread
(pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag
\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag
pas_refined aag s
invs s
ko_at (Endpoint ep) epptr s

goal (2 subgoals):
 1. \<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))
 2. \<lbrakk>AllowGrant \<in> rights; \<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; st_tcb_at (\<lambda>_. True) (hd x) s; tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb\<rbrakk> \<Longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag)
 2. \<lbrakk>AllowGrant \<in> rights; \<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> valid_mdb s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> pspace_distinct s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant_reply pl \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag) proof (state)
goal (1 subgoal):
 1. valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> valid_mdb s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> pspace_distinct s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant_reply pl \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. sender_can_grant pl \<Longrightarrow> is_subject aag (hd list) proof (prove)
using this:
is_subject aag thread
(pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag
\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag
pas_refined aag s
invs s
ko_at (Endpoint (SendEP list)) epptr s
ep = SendEP list
list \<noteq> []
st_tcb_at (\<lambda>_. True) (hd list) s
tcb_state (the (get_tcb (hd list) s)) = BlockedOnSend ep' pl

goal (1 subgoal):
 1. sender_can_grant pl \<Longrightarrow> is_subject aag (hd list) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>sender_can_grant pl; is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ko_at (Endpoint (SendEP list)) epptr s; ep = SendEP list; list \<noteq> []; tcb_state tcb = BlockedOnSend ep' pl; kheap s (hd list) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> is_subject aag (hd list) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>sender_can_grant pl; is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ko_at (Endpoint (SendEP list)) epptr s; ep = SendEP list; list \<noteq> []; tcb_state tcb = BlockedOnSend ep' pl; kheap s (hd list) = Some (TCB tcb); \<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) (hd list) s\<rbrakk> \<Longrightarrow> is_subject aag (hd list) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>sender_can_grant pl; is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag ep') \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag ep') \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP list; list \<noteq> []; tcb_state tcb = BlockedOnSend ep' pl; kheap s ep' = Some (Endpoint (SendEP list)); kheap s (hd list) = Some (TCB tcb); epptr = ep'\<rbrakk> \<Longrightarrow> is_subject aag (hd list) proof (state)
this:
sender_can_grant pl \<Longrightarrow> is_subject aag (hd list)

goal (1 subgoal):
 1. valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> valid_mdb s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> pspace_distinct s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant_reply pl \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag) proof (state)
this:
sender_can_grant pl \<Longrightarrow> is_subject aag (hd list)

goal (1 subgoal):
 1. valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> valid_mdb s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> pspace_distinct s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant_reply pl \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. sender_can_grant_reply pl \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag proof (prove)
using this:
is_subject aag thread
(pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag
\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag
pas_refined aag s
invs s
ko_at (Endpoint (SendEP list)) epptr s
ep = SendEP list
list \<noteq> []
st_tcb_at (\<lambda>_. True) (hd list) s
tcb_state (the (get_tcb (hd list) s)) = BlockedOnSend ep' pl

goal (1 subgoal):
 1. sender_can_grant_reply pl \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>sender_can_grant_reply pl; is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ko_at (Endpoint (SendEP list)) epptr s; ep = SendEP list; list \<noteq> []; tcb_state tcb = BlockedOnSend ep' pl; kheap s (hd list) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>sender_can_grant_reply pl; is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ko_at (Endpoint (SendEP list)) epptr s; ep = SendEP list; list \<noteq> []; tcb_state tcb = BlockedOnSend ep' pl; kheap s (hd list) = Some (TCB tcb); \<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) (hd list) s\<rbrakk> \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>sender_can_grant_reply pl; is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag ep') \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag ep') \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP list; list \<noteq> []; tcb_state tcb = BlockedOnSend ep' pl; kheap s ep' = Some (Endpoint (SendEP list)); kheap s (hd list) = Some (TCB tcb); epptr = ep'\<rbrakk> \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>sender_can_grant_reply pl; is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag ep') \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag ep') \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP list; list \<noteq> []; tcb_state tcb = BlockedOnSend ep' pl; kheap s ep' = Some (Endpoint (SendEP list)); kheap s (hd list) = Some (TCB tcb); epptr = ep'\<rbrakk> \<Longrightarrow> (hd list, Call, ?y25 tcb) \<in> state_objs_to_policy s
 2. \<And>tcb. \<lbrakk>sender_can_grant_reply pl; is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag ep') \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag ep') \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP list; list \<noteq> []; tcb_state tcb = BlockedOnSend ep' pl; kheap s ep' = Some (Endpoint (SendEP list)); kheap s (hd list) = Some (TCB tcb); epptr = ep'; (pasObjectAbs aag (hd list), Call, pasObjectAbs aag (?y25 tcb)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>sender_can_grant_reply pl; is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag ep') \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag ep') \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP list; list \<noteq> []; tcb_state tcb = BlockedOnSend ep' pl; kheap s ep' = Some (Endpoint (SendEP list)); kheap s (hd list) = Some (TCB tcb); epptr = ep'\<rbrakk> \<Longrightarrow> (?y25 tcb, Call) \<in> thread_st_auth s (hd list)
 2. \<And>tcb. \<lbrakk>sender_can_grant_reply pl; is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag ep') \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag ep') \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP list; list \<noteq> []; tcb_state tcb = BlockedOnSend ep' pl; kheap s ep' = Some (Endpoint (SendEP list)); kheap s (hd list) = Some (TCB tcb); epptr = ep'; (pasObjectAbs aag (hd list), Call, pasObjectAbs aag (?y25 tcb)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>sender_can_grant_reply pl; is_subject aag thread; (pasSubject aag, Receive, pasObjectAbs aag ep') \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag ep') \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP list; list \<noteq> []; tcb_state tcb = BlockedOnSend ep' pl; kheap s ep' = Some (Endpoint (SendEP list)); kheap s (hd list) = Some (TCB tcb); epptr = ep'; (pasObjectAbs aag (hd list), Call, pasObjectAbs aag ep') \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag proof (state)
this:
sender_can_grant_reply pl \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag

goal (1 subgoal):
 1. valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> valid_mdb s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> pspace_distinct s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant_reply pl \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag) proof (chain)
picking this:
sender_can_grant pl \<Longrightarrow> is_subject aag (hd list)
sender_can_grant_reply pl \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag proof (prove)
using this:
sender_can_grant pl \<Longrightarrow> is_subject aag (hd list)
sender_can_grant_reply pl \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag

goal (1 subgoal):
 1. valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> valid_mdb s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> pspace_distinct s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant_reply pl \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag) proof (prove)
using this:
sender_can_grant pl \<Longrightarrow> is_subject aag (hd list)
sender_can_grant_reply pl \<Longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag
is_subject aag thread
(pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag
\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag
pas_refined aag s
invs s
ko_at (Endpoint (SendEP list)) epptr s
ep = SendEP list
list \<noteq> []
st_tcb_at (\<lambda>_. True) (hd list) s
tcb_state (the (get_tcb (hd list) s)) = BlockedOnSend ep' pl

goal (1 subgoal):
 1. valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> valid_mdb s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> pspace_distinct s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant_reply pl \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag) proof (state)
this:
valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> valid_mdb s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # lista \<Rightarrow> SendEP (tl list)) s \<and> pspace_distinct s \<and> (sender_can_grant pl \<longrightarrow> is_subject aag (hd list)) \<and> (sender_can_grant_reply pl \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag)

goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<lbrakk>AllowGrant \<in> rights; \<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>AllowGrant \<in> rights; \<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) proof (prove)
using this:
is_subject aag thread
(pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag
\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag
pas_refined aag s
invs s
ko_at (Endpoint ep) epptr s

goal (1 subgoal):
 1. \<lbrakk>AllowGrant \<in> rights; \<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))\<rbrakk> \<Longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; st_tcb_at (\<lambda>_. True) (hd x) s; tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend xa xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s (hd x) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ko_at (Endpoint (SendEP x)) epptr s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend xa xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s (hd x) = Some (TCB tcb); \<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) (hd x) s\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (1 subgoal):
 1. \<And>x xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend epptr xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s epptr = Some (Endpoint (SendEP x)); kheap s (hd x) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (2 subgoals):
 1. \<And>x xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend epptr xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s epptr = Some (Endpoint (SendEP x)); kheap s (hd x) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (hd x, Call, ?y133 x xb tcb) \<in> state_objs_to_policy s
 2. \<And>x xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend epptr xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s epptr = Some (Endpoint (SendEP x)); kheap s (hd x) = Some (TCB tcb); (pasObjectAbs aag (hd x), Call, pasObjectAbs aag (?y133 x xb tcb)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (2 subgoals):
 1. \<And>x xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend epptr xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s epptr = Some (Endpoint (SendEP x)); kheap s (hd x) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (?y133 x xb tcb, Call) \<in> thread_st_auth s (hd x)
 2. \<And>x xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend epptr xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s epptr = Some (Endpoint (SendEP x)); kheap s (hd x) = Some (TCB tcb); (pasObjectAbs aag (hd x), Call, pasObjectAbs aag (?y133 x xb tcb)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (1 subgoal):
 1. \<And>x xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend epptr xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s epptr = Some (Endpoint (SendEP x)); kheap s (hd x) = Some (TCB tcb); (pasObjectAbs aag (hd x), Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (prove)
goal (4 subgoals):
 1. \<And>x xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend epptr xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s epptr = Some (Endpoint (SendEP x)); kheap s (hd x) = Some (TCB tcb); (pasObjectAbs aag (hd x), Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (?r146 x xb tcb, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag
 2. \<And>x xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend epptr xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s epptr = Some (Endpoint (SendEP x)); kheap s (hd x) = Some (TCB tcb); (pasObjectAbs aag (hd x), Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (?r146 x xb tcb, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag
 3. \<And>x xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend epptr xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s epptr = Some (Endpoint (SendEP x)); kheap s (hd x) = Some (TCB tcb); (pasObjectAbs aag (hd x), Call, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pas_refined aag (?sa146 x xb tcb)
 4. \<And>x xb tcb. \<lbrakk>AllowGrant \<in> rights; is_subject aag thread; \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; invs s; ep = SendEP x; x \<noteq> []; tcb_state tcb = BlockedOnSend epptr xb; sender_can_grant_reply xb; valid_mdb s; valid_objs s; valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s; pspace_distinct s; (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag; \<not> sender_can_grant xb; kheap s epptr = Some (Endpoint (SendEP x)); kheap s (hd x) = Some (TCB tcb); (pasObjectAbs aag (hd x), Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; (?r146 x xb tcb, Control, pasObjectAbs aag (hd x)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (hd x) proof (state)
this:
(AllowGrant \<in> rights \<longrightarrow> (ep = IdleEP \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> is_subject aag (hd x) \<and> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> is_blocking \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag)) \<and> (AllowGrant \<notin> rights \<longrightarrow> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> st_tcb_at (\<lambda>_. True) (hd x) s \<longrightarrow> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_mdb s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> pspace_distinct s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (sender_can_grant_reply xb \<longrightarrow> (pasSubject aag, Reply, pasObjectAbs aag (hd x)) \<in> pasPolicy aag))))

goal:
No subgoals! proof (prove)
goal:
No subgoals!