theory FinalCaps

lemma send_ipc_silc_inv:
  "\<lbrace>silc_inv aag st and invs and pas_refined aag
       and K (is_subject aag thread \<and> aag_has_auth_to aag SyncSend epptr \<and>
            (can_grant_reply \<longrightarrow> aag_has_auth_to aag Call epptr) \<and>
            (can_grant \<longrightarrow> aag_has_auth_to aag Grant epptr))\<rbrace>
     send_ipc block call badge can_grant can_grant_reply thread epptr
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding send_ipc_def apply (wp setup_caller_cap_silc_inv hoare_weak_lift_imp do_ipc_transfer_silc_inv gts_wp
        | wpc
        | simp add:st_tcb_at_tcb_states_of_state_eq
        | rule conjI impI
        | blast)+ apply (wp hoare_vcg_all_lift hoare_imp_lift_something get_simple_ko_wp
           | simp add:st_tcb_at_tcb_states_of_state_eq)+ apply clarsimp subgoal for s receiver t apply (frule silc_inv_not_subject) apply (cases can_grant) subgoal  (* grant case *)
       apply clarsimp apply (rule context_conjI; clarsimp) apply (thin_tac "can_grant_reply \<longrightarrow> _")+ apply (frule(1) tcb_states_of_state_to_auth, simp) apply (subgoal_tac "is_subject aag receiver") apply (force dest!: ko_atD elim: send_ipc_valid_ep_helper[simplified obj_at_def]) 
      (* Make the blockedOnReceive state point to epptr *)
       apply (frule(1) sym_ref_endpoint_recvD[OF invs_sym_refs _ head_in_set],
             clarsimp simp: st_tcb_at_tcb_states_of_state_eq) apply (frule(2) aag_wellformed_grant_Control_to_recv[OF _ _ pas_refined_wellformed]) by (simp add: aag_has_Control_iff_owns) apply clarsimp apply (intro conjI[rotated] impI) subgoal  (* no grant or grant reply case *)
       by (force elim: send_ipc_valid_ep_helper) subgoal  (* grant reply case *)
       apply clarsimp 
      (* Make the blockedOnReceive state point to epptr *)
       apply (frule(1) sym_ref_endpoint_recvD[OF invs_sym_refs _ head_in_set],
             clarsimp simp: st_tcb_at_tcb_states_of_state_eq) apply (frule(1) tcb_states_of_state_to_auth) by (auto elim: send_ipc_valid_ep_helper
          simp: aag_has_Control_iff_owns
          dest: tcb_states_of_state_to_auth
          aag_wellformed_grant_Control_to_recv_by_reply[OF _ _ _ pas_refined_wellformed];
          force dest: tcb_states_of_state_kheapD
          simp: obj_at_def is_cap_table
          elim: silc_inv_cnode_onlyE) done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and invs and pas_refined aag and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag))\<rbrace> send_ipc block call badge can_grant can_grant_reply thread epptr \<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 K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag))\<rbrace> do ep <- get_endpoint epptr;
case (ep, block) of (IdleEP, True) \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP [thread]
od | (IdleEP, False) \<Rightarrow> return () | (SendEP queue, True) \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP (queue @ [thread])
od | (SendEP queue, False) \<Rightarrow> return () | (RecvEP [], x) \<Rightarrow> fail | (RecvEP (dest # queue), x) \<Rightarrow> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap thread dest reply_can_grant else set_thread_state thread Inactive
od
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'402 (RecvEP (x21 # x22)) (x21 # x22) x21 x22\<rbrace> set_endpoint epptr (case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22) \<lbrace>\<lambda>rv s. \<forall>sta. tcb_states_of_state s x21 = Some sta \<longrightarrow> (\<forall>x xa. sta = BlockedOnReceive x 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> (can_grant \<longrightarrow> is_subject aag thread \<and> is_subject aag x21) \<and> (receiver_can_grant xa \<longrightarrow> is_subject aag thread \<and> is_subject aag x21) \<and> pasObjectAbs aag thread \<noteq> SilcLabel \<and> pasObjectAbs aag x21 \<noteq> SilcLabel)\<rbrace>
 2. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'401 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>\<lambda>rv s. (can_grant_reply \<longrightarrow> (\<forall>sta. st_tcb_at ((=) sta) x21 s \<longrightarrow> (sta = Running \<longrightarrow> True) \<and> (inactive sta \<longrightarrow> True) \<and> (sta = Restart \<longrightarrow> True) \<and> (\<forall>x xa. sta = BlockedOnReceive x xa \<longrightarrow> (silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (can_grant \<longrightarrow> is_subject aag thread \<and> is_subject aag x21)) s \<and> (receiver_can_grant xa \<longrightarrow> is_subject aag thread \<and> is_subject aag x21) \<and> pasObjectAbs aag thread \<noteq> SilcLabel \<and> pasObjectAbs aag x21 \<noteq> SilcLabel) \<and> (\<forall>x xa. sta = BlockedOnSend x xa \<longrightarrow> True) \<and> (awaiting_reply sta \<longrightarrow> True) \<and> (\<forall>x. sta = BlockedOnNotification x \<longrightarrow> True) \<and> (idle sta \<longrightarrow> True))) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> (\<forall>sta. st_tcb_at ((=) sta) x21 s \<longrightarrow> (sta = Running \<longrightarrow> True) \<and> (inactive sta \<longrightarrow> True) \<and> (sta = Restart \<longrightarrow> True) \<and> (\<forall>x xa. sta = BlockedOnReceive x xa \<longrightarrow> (silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (can_grant \<longrightarrow> is_subject aag thread \<and> is_subject aag x21)) s) \<and> (\<forall>x xa. sta = BlockedOnSend x xa \<longrightarrow> True) \<and> (awaiting_reply sta \<longrightarrow> True) \<and> (\<forall>x. sta = BlockedOnNotification x \<longrightarrow> True) \<and> (idle sta \<longrightarrow> True)))\<rbrace>
 3. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> silc_inv aag st s) \<and> (block = False \<longrightarrow> silc_inv aag st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> silc_inv aag st s) \<and> (block = False \<longrightarrow> silc_inv aag st s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> (can_grant \<longrightarrow> ?P'402 ep x xa xb s) \<and> ?P'401 ep x xa xb s))\<rbrace>
 4. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<Longrightarrow> \<forall>ntfn. ko_at (Endpoint ntfn) epptr s \<longrightarrow> (\<forall>x. ntfn = RecvEP x \<longrightarrow> (\<forall>xa xb. x = xa # xb \<longrightarrow> (can_grant \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<forall>xc xd. x = BlockedOnReceive xc xd \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag xa \<and> (receiver_can_grant xd \<longrightarrow> is_subject aag xa) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag xa \<noteq> SilcLabel))) \<and> (can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<forall>xc xd. x = BlockedOnReceive xc xd \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag xa) \<and> (receiver_can_grant xd \<longrightarrow> is_subject aag xa) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag xa \<noteq> SilcLabel))) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (xa # xb))) epptr s\<rbrakk> \<Longrightarrow> (can_grant \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<forall>xc xd. x = BlockedOnReceive xc xd \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag xa \<and> (receiver_can_grant xd \<longrightarrow> is_subject aag xa) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag xa \<noteq> SilcLabel))) \<and> (can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<forall>xc xd. x = BlockedOnReceive xc xd \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag xa) \<and> (receiver_can_grant xd \<longrightarrow> is_subject aag xa) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag xa \<noteq> SilcLabel))) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s xa = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s\<rbrakk> \<Longrightarrow> (can_grant \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> (can_grant \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant\<rbrakk> \<Longrightarrow> (can_grant \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s))
 2. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant\<rbrakk> \<Longrightarrow> (can_grant \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant\<rbrakk> \<Longrightarrow> (can_grant \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant\<rbrakk> \<Longrightarrow> (can_grant \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant\<rbrakk> \<Longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel)) \<and> (can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant; tcb_states_of_state s receiver = Some (BlockedOnReceive xa xb)\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant; tcb_states_of_state s receiver = Some (BlockedOnReceive xa xb)\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant; tcb_states_of_state s receiver = Some (BlockedOnReceive xa xb); (pasObjectAbs aag receiver, Receive, pasObjectAbs aag xa) \<in> pasPolicy aag \<and> (\<forall>x\<in>if receiver_can_grant xb then {(xa, Grant)} else {}. case x of (obj, auth) \<Rightarrow> (pasObjectAbs aag receiver, auth, pasObjectAbs aag obj) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant; tcb_states_of_state s receiver = Some (BlockedOnReceive xa xb); (pasObjectAbs aag receiver, Receive, pasObjectAbs aag xa) \<in> pasPolicy aag \<and> (\<forall>x\<in>if receiver_can_grant xb then {(xa, Grant)} else {}. case x of (obj, auth) \<Rightarrow> (pasObjectAbs aag receiver, auth, pasObjectAbs aag obj) \<in> pasPolicy aag); is_subject aag receiver\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel
 2. \<And>xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant; tcb_states_of_state s receiver = Some (BlockedOnReceive xa xb); (pasObjectAbs aag receiver, Receive, pasObjectAbs aag xa) \<in> pasPolicy aag \<and> (\<forall>x\<in>if receiver_can_grant xb then {(xa, Grant)} else {}. case x of (obj, auth) \<Rightarrow> (pasObjectAbs aag receiver, auth, pasObjectAbs aag obj) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> is_subject aag receiver proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant; tcb_states_of_state s receiver = Some (BlockedOnReceive xa xb); (pasObjectAbs aag receiver, Receive, pasObjectAbs aag xa) \<in> pasPolicy aag \<and> (\<forall>x\<in>if receiver_can_grant xb then {(xa, Grant)} else {}. case x of (obj, auth) \<Rightarrow> (pasObjectAbs aag receiver, auth, pasObjectAbs aag obj) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> is_subject aag receiver proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant; tcb_states_of_state s receiver = Some (BlockedOnReceive xa xb); (pasObjectAbs aag receiver, Receive, pasObjectAbs aag xa) \<in> pasPolicy aag \<and> (\<forall>x\<in>if receiver_can_grant xb then {(xa, Grant)} else {}. case x of (obj, auth) \<Rightarrow> (pasObjectAbs aag receiver, auth, pasObjectAbs aag obj) \<in> pasPolicy aag)\<rbrakk> \<Longrightarrow> is_subject aag receiver proof (prove)
goal (1 subgoal):
 1. \<And>xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant; tcb_states_of_state s receiver = Some (BlockedOnReceive epptr xb); (pasObjectAbs aag receiver, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>x\<in>if receiver_can_grant xb then {(epptr, Grant)} else {}. case x of (obj, auth) \<Rightarrow> (pasObjectAbs aag receiver, auth, pasObjectAbs aag obj) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag receiver proof (prove)
goal (1 subgoal):
 1. \<And>xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; can_grant; tcb_states_of_state s receiver = Some (BlockedOnReceive epptr xb); (pasObjectAbs aag receiver, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>x\<in>if receiver_can_grant xb then {(epptr, Grant)} else {}. case x of (obj, auth) \<Rightarrow> (pasObjectAbs aag receiver, auth, pasObjectAbs aag obj) \<in> pasPolicy aag; (pasSubject aag, Control, pasObjectAbs aag receiver) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag receiver proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant\<rbrakk> \<Longrightarrow> (can_grant \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag receiver \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (can_grant \<longrightarrow> is_subject aag receiver) \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasSubject aag \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (\<not> can_grant \<and> \<not> can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant\<rbrakk> \<Longrightarrow> (can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel))) \<and> (\<not> can_grant_reply \<longrightarrow> (\<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant; \<not> can_grant_reply\<rbrakk> \<Longrightarrow> \<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s
 2. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant; can_grant_reply\<rbrakk> \<Longrightarrow> \<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant; \<not> can_grant_reply\<rbrakk> \<Longrightarrow> \<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant; \<not> can_grant_reply\<rbrakk> \<Longrightarrow> \<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<exists>xa xb. x = BlockedOnReceive xa xb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant; can_grant_reply\<rbrakk> \<Longrightarrow> \<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant; can_grant_reply\<rbrakk> \<Longrightarrow> \<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; can_grant_reply \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant; can_grant_reply\<rbrakk> \<Longrightarrow> \<forall>x. tcb_states_of_state s receiver = Some x \<longrightarrow> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel) proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant; can_grant_reply; tcb_states_of_state s receiver = Some (BlockedOnReceive xa xb)\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant; can_grant_reply; tcb_states_of_state s receiver = Some (BlockedOnReceive xa xb)\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant; can_grant_reply; tcb_states_of_state s receiver = Some (BlockedOnReceive epptr xb)\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>xb. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; is_subject aag thread; (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint (RecvEP (receiver # t))) epptr s; SilcLabel \<noteq> pasSubject aag; \<not> can_grant; can_grant_reply; tcb_states_of_state s receiver = Some (BlockedOnReceive epptr xb); \<forall>(obj, auth)\<in>tcb_st_to_auth (BlockedOnReceive epptr xb). (pasObjectAbs aag receiver, auth, pasObjectAbs aag obj) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case t of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP t) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (receiver_can_grant xb \<longrightarrow> is_subject aag receiver) \<and> pasObjectAbs aag receiver \<noteq> SilcLabel proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!