theory Ipc_IF

lemma do_reply_transfer_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects_f aag l
       (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver
                        and tcb_at sender and emptyable slot  and is_subject aag \<circ> cur_thread
                        and K (grant \<longrightarrow> is_subject aag receiver)
                        and K (is_subject aag sender \<and> aag_can_read aag receiver
                                                     \<and> is_subject aag (fst slot)))
       (do_reply_transfer sender receiver slot grant)" unfolding do_reply_transfer_def apply (rule gen_asm_ev)+ apply (wp gets_cur_thread_ev[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]]
            set_thread_state_reads_respects cap_delete_one_reads_respects_f
            do_ipc_transfer_reads_respects do_ipc_transfer_pas_refined
            thread_set_reads_respects handle_fault_reply_reads_respects
            get_mrs_rev lookup_ipc_buffer_reads_respects
            lookup_ipc_buffer_has_read_auth' get_message_info_rev
            get_mi_length
            cap_delete_one_silc_inv do_ipc_transfer_silc_inv
            set_thread_state_pas_refined thread_set_fault_pas_refined'
            possible_switch_to_reads_respects[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]]
            when_ev
         | wpc
         | simp split del: if_split
         | wp (once) reads_respects_f[where aag=aag and st=st]
         | elim conjE
         | wp (once) hoare_drop_imps)+ apply (rule_tac Q="\<lambda> rv s. pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s
                                 \<and> is_subject aag (cur_thread s)
                                 \<and> silc_inv aag st s"
                     in hoare_strengthen_post[rotated]) apply ((wp (once) hoare_drop_imps
                  | wp cap_delete_one_invs  hoare_vcg_all_lift
                       cap_delete_one_silc_inv reads_respects_f[OF thread_get_reads_respects]
                       reads_respects_f[OF get_thread_state_rev]
                  | simp add: invs_valid_objs invs_psp_aligned invs_valid_global_refs
                              invs_distinct invs_arch_state
                              invs_psp_aligned invs_vspace_objs invs_arch_state
                  | rule conjI
                  | elim conjE
                  | assumption)+)[8] by (fastforce dest: silc_inv_not_subject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread and K (grant \<longrightarrow> is_subject aag receiver) and K (is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot))) (do_reply_transfer sender receiver slot grant) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread and K (grant \<longrightarrow> is_subject aag receiver) and K (is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot))) (do state <- get_thread_state receiver;
assert (awaiting_reply state);
fault <- thread_get tcb_fault receiver;
case fault of None \<Rightarrow> do do_ipc_transfer sender None 0 grant receiver;
cap_delete_one slot;
set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver)
od | Some f \<Rightarrow> do cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
set_thread_state receiver (if restart then Restart else Inactive);
when restart $ do_extended_op (possible_switch_to receiver);
return ()
od
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread) (do state <- get_thread_state receiver;
assert (awaiting_reply state);
fault <- thread_get tcb_fault receiver;
case fault of None \<Rightarrow> do do_ipc_transfer sender None 0 grant receiver;
cap_delete_one slot;
set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver)
od | Some f \<Rightarrow> do cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
set_thread_state receiver (if restart then Restart else Inactive);
when restart $ do_extended_op (possible_switch_to receiver);
return ()
od
od) proof (prove)
goal (8 subgoals):
 1. \<And>rv rvb x2. \<lbrakk>grant \<longrightarrow> is_subject aag receiver; rvb = Some x2; is_subject aag sender; aag_can_read aag receiver; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> \<lbrace>?P'604 rv () (Some x2) x2\<rbrace> cap_delete_one slot \<lbrace>\<lambda>rva s. valid_objs s \<and> silc_inv aag st s \<and> is_subject aag (cur_thread s) \<and> pas_refined (?aag577 rv () (Some x2) x2 ()) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> silc_inv aag st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s)\<rbrace>
 2. \<And>rv rva. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> reads_respects_f aag l (?P'7 rv rva) (thread_get tcb_fault receiver)
 3. \<And>rv rva. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> \<lbrace>?P''7 rv rva\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>rvb s. (rvb = None \<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 ((grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) \<and> aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect aag l receiver)) and (\<lambda>a. pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a \<and> valid_objs a \<and> valid_mdb a \<and> pas_refined aag a)) s \<and> (silc_inv aag (?st129 rv rva rvb) and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> K (is_subject aag (fst slot)) s \<and> (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 (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)) s \<and> K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel) s \<and> is_subject aag (cur_thread s) \<and> (silc_inv (?aag153 rv rva rvb) (?st150 rv rva rvb) and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined (?aag153 rv rva rvb) and K (grant \<longrightarrow> is_subject (?aag153 rv rva rvb) sender \<and> is_subject (?aag153 rv rva rvb) receiver)) s \<and> K (pasObjectAbs (?aag153 rv rva rvb) (fst slot) \<noteq> SilcLabel) s \<and> (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 (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)) s \<and> K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (valid_mdb and (valid_objs and pspace_aligned and pspace_distinct)) s \<and> K (is_subject aag (fst slot)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> K (\<forall>r\<in>tcb_st_to_auth Running. (pasObjectAbs aag receiver, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag) s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> True) \<and> (\<forall>x. rvb = Some x \<longrightarrow> (silc_inv aag (?st581 rv rva rvb x) and invs and pas_refined aag and K (is_subject aag (fst slot))) s \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> K (is_subject aag sender) s \<and> (silc_inv (?aag591 rv rva rvb x) (?st591 rv rva rvb x) and K (pasObjectAbs (?aag591 rv rva rvb x) (fst slot) \<noteq> SilcLabel)) s \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> K (aag_can_read_or_affect aag l sender) s \<and> (silc_inv (?aag599 rv rva rvb x) (?st599 rv rva rvb x) and K (pasObjectAbs (?aag599 rv rva rvb x) (fst slot) \<noteq> SilcLabel)) s \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (valid_mdb and K (is_subject aag (fst slot)))) s \<and> ?P'604 rv rva rvb x s)\<rbrace>
 4. \<And>rv. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> reads_respects_f aag l (?P'5 rv) (assert (awaiting_reply rv))
 5. \<And>rv. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> \<lbrace>?P''5 rv\<rbrace> assert (awaiting_reply rv) \<lbrace>\<lambda>rva s. ?P'7 rv rva s \<and> ?P''7 rv rva s\<rbrace>
 6. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> reads_respects_f aag l ?P'4 (get_thread_state receiver)
 7. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> \<lbrace>?P''4\<rbrace> get_thread_state receiver \<lbrace>\<lambda>rv s. ?P'5 rv s \<and> ?P''5 rv s\<rbrace>
 8. \<And>s. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver; (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?P'4 s \<and> ?P''4 s
flex-flex pairs:
\<lambda>x xb. ?aag579 x () (Some xb) xb () \<equiv>\<^sup>? \<lambda>x xb. ?aag577 x () (Some xb) xb () proof (prove)
goal (9 subgoals):
 1. \<And>rv rvb x2 rva s. \<lbrakk>grant \<longrightarrow> is_subject aag receiver; rvb = Some x2; is_subject aag sender; aag_can_read aag receiver; is_subject aag (fst slot); pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> silc_inv aag st s\<rbrakk> \<Longrightarrow> valid_objs s \<and> silc_inv aag st s \<and> is_subject aag (cur_thread s) \<and> pas_refined (?aag577 rv () (Some x2) x2 ()) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> silc_inv aag st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s)
 2. \<And>rv rvb x2. \<lbrakk>grant \<longrightarrow> is_subject aag receiver; rvb = Some x2; is_subject aag sender; aag_can_read aag receiver; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> \<lbrace>?P'604 rv () (Some x2) x2\<rbrace> cap_delete_one slot \<lbrace>\<lambda>rv s. pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> silc_inv aag st s\<rbrace>
 3. \<And>rv rva. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> reads_respects_f aag l (?P'7 rv rva) (thread_get tcb_fault receiver)
 4. \<And>rv rva. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> \<lbrace>?P''7 rv rva\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>rvb s. (rvb = None \<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 ((grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) \<and> aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect aag l receiver)) and (\<lambda>a. pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a \<and> valid_objs a \<and> valid_mdb a \<and> pas_refined aag a)) s \<and> (silc_inv aag (?st129 rv rva rvb) and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> K (is_subject aag (fst slot)) s \<and> (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 (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)) s \<and> K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel) s \<and> is_subject aag (cur_thread s) \<and> (silc_inv (?aag153 rv rva rvb) (?st150 rv rva rvb) and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined (?aag153 rv rva rvb) and K (grant \<longrightarrow> is_subject (?aag153 rv rva rvb) sender \<and> is_subject (?aag153 rv rva rvb) receiver)) s \<and> K (pasObjectAbs (?aag153 rv rva rvb) (fst slot) \<noteq> SilcLabel) s \<and> (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 (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)) s \<and> K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (valid_mdb and (valid_objs and pspace_aligned and pspace_distinct)) s \<and> K (is_subject aag (fst slot)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> K (\<forall>r\<in>tcb_st_to_auth Running. (pasObjectAbs aag receiver, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag) s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> True) \<and> (\<forall>x. rvb = Some x \<longrightarrow> (silc_inv aag (?st581 rv rva rvb x) and invs and pas_refined aag and K (is_subject aag (fst slot))) s \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> K (is_subject aag sender) s \<and> (silc_inv (?aag591 rv rva rvb x) (?st591 rv rva rvb x) and K (pasObjectAbs (?aag591 rv rva rvb x) (fst slot) \<noteq> SilcLabel)) s \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> K (aag_can_read_or_affect aag l sender) s \<and> (silc_inv (?aag599 rv rva rvb x) (?st599 rv rva rvb x) and K (pasObjectAbs (?aag599 rv rva rvb x) (fst slot) \<noteq> SilcLabel)) s \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (valid_mdb and K (is_subject aag (fst slot)))) s \<and> ?P'604 rv rva rvb x s)\<rbrace>
 5. \<And>rv. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> reads_respects_f aag l (?P'5 rv) (assert (awaiting_reply rv))
 6. \<And>rv. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> \<lbrace>?P''5 rv\<rbrace> assert (awaiting_reply rv) \<lbrace>\<lambda>rva s. ?P'7 rv rva s \<and> ?P''7 rv rva s\<rbrace>
 7. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> reads_respects_f aag l ?P'4 (get_thread_state receiver)
 8. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver\<rbrakk> \<Longrightarrow> \<lbrace>?P''4\<rbrace> get_thread_state receiver \<lbrace>\<lambda>rv s. ?P'5 rv s \<and> ?P''5 rv s\<rbrace>
 9. \<And>s. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver; (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?P'4 s \<and> ?P''4 s
flex-flex pairs:
\<lambda>x xb. ?aag579 x () (Some xb) xb () \<equiv>\<^sup>? \<lambda>x xb. ?aag577 x () (Some xb) xb () proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot); grant \<longrightarrow> is_subject aag receiver; (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> (silc_inv aag ?st1005 and K (aag_can_read aag receiver) and ?Q1001) s \<and> True \<and> (silc_inv aag (?st1059 ()) and K (aag_can_read_or_affect aag l receiver) and ?Q1057 ()) s \<and> ((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 ((grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) \<and> aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect aag l receiver)) and (\<lambda>a. pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a \<and> valid_objs a \<and> valid_mdb a \<and> pas_refined aag a)) s \<and> (silc_inv aag (?st1055 ()) and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> K (is_subject aag (fst slot)) s \<and> (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 (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)) s \<and> K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel) s \<and> is_subject aag (cur_thread s) \<and> (silc_inv (?aag1045 ()) (?st1052 ()) and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined (?aag1045 ()) and K (grant \<longrightarrow> is_subject (?aag1045 ()) sender \<and> is_subject (?aag1045 ()) receiver)) s \<and> K (pasObjectAbs (?aag1045 ()) (fst slot) \<noteq> SilcLabel) s \<and> (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 (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)) s \<and> K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (valid_mdb and (valid_objs and pspace_aligned and pspace_distinct)) s \<and> K (is_subject aag (fst slot)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> K (\<forall>r\<in>tcb_st_to_auth Running. (pasObjectAbs aag receiver, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag) s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> True) \<and> (\<forall>x. (silc_inv aag (?st1043 () x) and invs and pas_refined aag and K (is_subject aag (fst slot))) s \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> K (is_subject aag sender) s \<and> (silc_inv (?aag1038 () x) (?st1040 () x) and K (pasObjectAbs (?aag1038 () x) (fst slot) \<noteq> SilcLabel)) s \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> K (aag_can_read_or_affect aag l sender) s \<and> (silc_inv (?aag1033 () x) (?st1035 () x) and K (pasObjectAbs (?aag1033 () x) (fst slot) \<noteq> SilcLabel)) s \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (valid_mdb and K (is_subject aag (fst slot)))) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (valid_mdb and K (is_subject aag (fst slot)))) s \<and> pas_cur_domain aag s \<and> (invs and emptyable slot) s \<and> is_subject aag (cur_thread s) \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s)