theory FinalCaps

lemma receive_ipc_base_silc_inv:
  notes do_nbrecv_failed_transfer_def[simp]
  shows
  "\<lbrace>silc_inv aag st and invs and pas_refined aag and ko_at (Endpoint ep) epptr
       and K (is_subject aag receiver \<and>
           (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and>
            (\<forall>auth \<in> cap_rights_to_auth rights True.
                        (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag))\<rbrace>
     receive_ipc_base aag receiver ep epptr rights is_blocking
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (clarsimp simp: thread_get_def get_thread_state_def cong: endpoint.case_cong) apply (rule hoare_pre) apply (wp setup_caller_cap_silc_inv hoare_weak_lift_imp do_ipc_transfer_silc_inv
         | wpc | simp split del: if_split)+ apply (wp  hoare_vcg_all_lift hoare_vcg_imp_lift  set_simple_ko_get_tcb
           | wpc | simp split del: if_split)+ apply (clarsimp) apply (frule tcb_states_of_state_to_auth[rotated]) apply (simp add: tcb_states_of_state_def,blast) apply (clarsimp simp: get_tcb_Some) apply (frule(2) sym_ref_endpoint_sendD[OF invs_sym_refs _ hd_in_set]) apply (clarsimp simp:st_tcb_at_tcb_states_of_state dest!:tcb_states_of_state_kheapD) apply (frule silc_inv_not_subject) by (safe;
       (clarsimp simp: cap_rights_to_auth_def)?;
       (erule(1) receive_ipc_valid_ep_helper
       | (erule(1) silc_inv_cnode_onlyE,simp add: obj_at_def is_cap_table)
       | (drule(2) aag_wellformed_grant_Control_to_send[OF _ _ pas_refined_wellformed],
          (simp add: aag_has_Control_iff_owns | force dest: pas_refined_Control))
       | (drule aag_wellformed_grant_Control_to_send_by_reply[OF _ _ _ pas_refined_wellformed],
          blast, blast, blast, simp add: aag_has_Control_iff_owns)))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and invs and pas_refined aag and ko_at (Endpoint ep) epptr and K (is_subject aag receiver \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref data \<Rightarrow> return data | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some epptr) (sender_badge data) (sender_can_grant data) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (AllowGrant \<in> rights) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and invs and pas_refined aag and ko_at (Endpoint ep) epptr and (\<lambda>y. is_subject aag receiver \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | SendEP q \<Rightarrow> do y <- assert (q \<noteq> []);
y <- set_endpoint epptr (case tl q of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl q));
tcb <- gets_the (get_tcb (hd q));
data <- case tcb_state tcb of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd q) (Some epptr) (sender_badge data) (sender_can_grant data) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap (hd q) receiver (AllowGrant \<in> rights) else set_thread_state (hd q) Inactive else do set_thread_state (hd q) Running;
do_extended_op (possible_switch_to (hd q))
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q5\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | SendEP q \<Rightarrow> do y <- assert (q \<noteq> []);
y <- set_endpoint epptr (case tl q of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl q));
tcb <- gets_the (get_tcb (hd q));
data <- case tcb_state tcb of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd q) (Some epptr) (sender_badge data) (sender_can_grant data) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap (hd q) receiver (AllowGrant \<in> rights) else set_thread_state (hd q) Inactive else do set_thread_state (hd q) Running;
do_extended_op (possible_switch_to (hd q))
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. (silc_inv aag st and invs and pas_refined aag and ko_at (Endpoint ep) epptr and (\<lambda>y. is_subject aag receiver \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag))) s \<Longrightarrow> ?Q5 s proof (prove)
goal (4 subgoals):
 1. \<And>x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B42 x2 ()\<rbrace> set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>\<lambda>ya s. (\<exists>y. get_tcb (hd x2) s = Some y) \<longrightarrow> (\<forall>x xa. tcb_state (the (get_tcb (hd x2) s)) = BlockedOnSend x xa \<longrightarrow> (sender_is_call xa \<longrightarrow> (sender_can_grant xa \<longrightarrow> silc_inv aag st s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> is_subject aag (hd x2) \<and> is_subject aag receiver \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x2) \<and> is_subject aag receiver) \<and> pasObjectAbs aag (hd x2) \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel) \<and> (sender_can_grant_reply xa \<longrightarrow> silc_inv aag st s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag (hd x2) \<and> is_subject aag receiver) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x2) \<and> is_subject aag receiver) \<and> pasObjectAbs aag (hd x2) \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel) \<and> (\<not> sender_can_grant xa \<and> \<not> sender_can_grant_reply xa \<longrightarrow> silc_inv aag st s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s)) \<and> (\<not> sender_is_call xa \<longrightarrow> silc_inv aag st s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag (hd x2) \<and> is_subject aag receiver)))\<rbrace>
 2. \<And>x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R20 x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B42 x2\<rbrace>
 3. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R21 x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (x3 @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>s. (silc_inv aag st and invs and pas_refined aag and ko_at (Endpoint ep) epptr and (\<lambda>y. is_subject aag receiver \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag))) s \<Longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> silc_inv aag st s) \<and> (is_blocking = False \<longrightarrow> silc_inv aag st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R20 x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R21 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> ko_at (Endpoint ep) epptr s \<and> is_subject aag receiver \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<Longrightarrow> \<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> get_tcb (hd x) s = None \<or> (\<forall>xa xb. tcb_state (the (get_tcb (hd x) s)) = BlockedOnSend xa xb \<longrightarrow> (sender_is_call xb \<longrightarrow> (sender_can_grant xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (hd x) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant_reply xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant xb \<or> sender_can_grant_reply xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (sender_is_call xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; ko_at (Endpoint (SendEP x)) epptr s; is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x; x \<noteq> []; get_tcb (hd x) s = Some y; tcb_state y = BlockedOnSend xa xb\<rbrakk> \<Longrightarrow> (sender_is_call xb \<longrightarrow> (sender_can_grant xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (hd x) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant_reply xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant xb \<or> sender_can_grant_reply xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (sender_is_call xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x))) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa y xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; ko_at (Endpoint (SendEP x)) epptr s; is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x; x \<noteq> []; get_tcb (hd x) s = Some y; tcb_state y = BlockedOnSend xa xb\<rbrakk> \<Longrightarrow> tcb_states_of_state s (?thread355 s x xa y xb) = Some (?tcbst355 s x xa y xb)
 2. \<And>s x xa y xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; ko_at (Endpoint (SendEP x)) epptr s; is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x; x \<noteq> []; get_tcb (hd x) s = Some y; tcb_state y = BlockedOnSend xa xb; \<forall>(obj, auth)\<in>tcb_st_to_auth (?tcbst355 s x xa y xb). (pasObjectAbs aag (?thread355 s x xa y xb), auth, pasObjectAbs aag obj) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (sender_is_call xb \<longrightarrow> (sender_can_grant xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (hd x) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant_reply xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant xb \<or> sender_can_grant_reply xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (sender_is_call xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; ko_at (Endpoint (SendEP x)) epptr s; is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x; x \<noteq> []; get_tcb (hd x) s = Some y; tcb_state y = BlockedOnSend xa xb; \<forall>(obj, auth)\<in>tcb_st_to_auth (BlockedOnSend xa xb). (pasObjectAbs aag (hd x), auth, pasObjectAbs aag obj) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (sender_is_call xb \<longrightarrow> (sender_can_grant xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (hd x) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant_reply xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant xb \<or> sender_can_grant_reply xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (sender_is_call xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; ko_at (Endpoint (SendEP x)) epptr s; is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x; x \<noteq> []; kheap s (hd x) = Some (TCB y); tcb_state y = BlockedOnSend xa xb; (pasObjectAbs aag (hd x), SyncSend, pasObjectAbs aag xa) \<in> pasPolicy aag; \<forall>xa\<in>(if sender_can_grant xb then {(xa, Grant), (xa, Call)} else {}) \<union> (if sender_can_grant_reply xb then {(xa, Call)} else {}). case xa of (obj, auth) \<Rightarrow> (pasObjectAbs aag (hd x), auth, pasObjectAbs aag obj) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (sender_is_call xb \<longrightarrow> (sender_can_grant xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (hd x) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant_reply xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant xb \<or> sender_can_grant_reply xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (sender_is_call xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; ko_at (Endpoint (SendEP x)) epptr s; is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x; x \<noteq> []; kheap s (hd x) = Some (TCB y); tcb_state y = BlockedOnSend xa xb; (pasObjectAbs aag (hd x), SyncSend, pasObjectAbs aag xa) \<in> pasPolicy aag; \<forall>xa\<in>(if sender_can_grant xb then {(xa, Grant), (xa, Call)} else {}) \<union> (if sender_can_grant_reply xb then {(xa, Call)} else {}). case xa of (obj, auth) \<Rightarrow> (pasObjectAbs aag (hd x), auth, pasObjectAbs aag obj) \<in> pasPolicy aag; \<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) (hd x) s\<rbrakk> \<Longrightarrow> (sender_is_call xb \<longrightarrow> (sender_can_grant xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (hd x) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant_reply xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant xb \<or> sender_can_grant_reply xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (sender_is_call xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x))) proof (prove)
goal (1 subgoal):
 1. \<And>s x y xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; ko_at (Endpoint (SendEP x)) epptr s; is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; (pasObjectAbs aag (hd x), SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>xa\<in>(if sender_can_grant xb then {(epptr, Grant), (epptr, Call)} else {}) \<union> (if sender_can_grant_reply xb then {(epptr, Call)} else {}). case xa of (obj, auth) \<Rightarrow> (pasObjectAbs aag (hd x), auth, pasObjectAbs aag obj) \<in> pasPolicy aag; kheap s (hd x) = Some (TCB y)\<rbrakk> \<Longrightarrow> (sender_is_call xb \<longrightarrow> (sender_can_grant xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (hd x) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant_reply xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant xb \<or> sender_can_grant_reply xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (sender_is_call xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x))) proof (prove)
goal (1 subgoal):
 1. \<And>s x y xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; ko_at (Endpoint (SendEP x)) epptr s; is_subject aag receiver; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x; x \<noteq> []; tcb_state y = BlockedOnSend epptr xb; (pasObjectAbs aag (hd x), SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>xa\<in>(if sender_can_grant xb then {(epptr, Grant), (epptr, Call)} else {}) \<union> (if sender_can_grant_reply xb then {(epptr, Call)} else {}). case xa of (obj, auth) \<Rightarrow> (pasObjectAbs aag (hd x), auth, pasObjectAbs aag obj) \<in> pasPolicy aag; kheap s (hd x) = Some (TCB y); SilcLabel \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> (sender_is_call xb \<longrightarrow> (sender_can_grant xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (hd x) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant_reply xb \<longrightarrow> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)) \<and> (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd x)) \<and> pasObjectAbs aag (hd x) \<noteq> SilcLabel \<and> pasSubject aag \<noteq> SilcLabel) \<and> (sender_can_grant xb \<or> sender_can_grant_reply xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (sender_is_call xb \<or> 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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xb \<longrightarrow> is_subject aag (hd x)))