theory Ipc_IF

lemma receive_ipc_base_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  notes do_nbrecv_failed_transfer_def[simp]
  shows "reads_respects aag (l :: 'a subject_label)
     (invs and pas_refined aag and pas_cur_domain aag
      and ko_at (Endpoint ep) epptr
      and is_subject aag \<circ> cur_thread
      and K (is_subject aag receiver
           \<and> aag_has_auth_to aag Receive epptr
           \<and> (\<forall>auth \<in> cap_rights_to_auth rights True . aag_has_auth_to aag auth epptr)))
     (receive_ipc_base aag receiver ep epptr rights is_blocking)" apply (rule gen_asm_ev) apply (simp add: thread_get_def split: endpoint.split) apply (intro conjI impI) prefer 2 defer apply ((wp set_thread_state_reads_respects set_simple_ko_reads_respects
               as_user_set_register_reads_respects'
        | simp | intro allI impI | rule pre_ev, wpc)+)[2] apply (intro allI impI) apply (wp hoare_weak_lift_imp set_simple_ko_reads_respects set_thread_state_reads_respects
            setup_caller_cap_reads_respects do_ipc_transfer_reads_respects
            possible_switch_to_reads_respects gets_cur_thread_ev set_thread_state_pas_refined
            set_simple_ko_reads_respects hoare_vcg_all_lift
            hoare_vcg_imp_lift[OF set_simple_ko_get_tcb, unfolded disj_not1]
            set_thread_state_reads_respects get_simple_ko_reads_respects
            get_simple_ko_wp do_ipc_transfer_pas_refined
        | wpc | simp add: get_thread_state_def thread_get_def)+ apply (clarsimp simp:neq_Nil_conv) subgoal for s sender queue apply (frule(1) receive_ipc_valid_ep_helper) apply (frule(1) sym_ref_endpoint_sendD[OF invs_sym_refs,where t= "sender"], force) apply (clarsimp simp:st_tcb_at_def elim!:obj_atE dest!:sym[where t = "tcb_state _"]) apply (subgoal_tac "aag_can_read aag sender") apply (fastforce simp: get_tcb_def
                      elim: receive_ipc_sender_can_grant_helper
                     intro: requiv_get_tcb_eq') apply (frule(2) receive_ipc_sender_helper) apply (solves \<open>auto intro:reads_ep read_sync_ep_read_senders\<close>) done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint ep) epptr and is_subject aag \<circ> cur_thread 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))) (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) proof (prove)
goal (1 subgoal):
 1. 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> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint ep) epptr and is_subject aag \<circ> cur_thread) (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) proof (prove)
goal (1 subgoal):
 1. 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> (ep = IdleEP \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint IdleEP) epptr and is_subject aag \<circ> cur_thread) (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)) \<and> (\<forall>x2. ep = SendEP x2 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint (SendEP x2)) epptr and is_subject aag \<circ> cur_thread) (do y <- assert (x2 \<noteq> []);
y <- set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (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 x2) receiver (AllowGrant \<in> rights) else set_thread_state (hd x2) Inactive else do set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od)) \<and> (\<forall>x3. ep = RecvEP x3 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint (RecvEP x3)) epptr and is_subject aag \<circ> cur_thread) (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)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>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); ep = IdleEP\<rbrakk> \<Longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint IdleEP) epptr and is_subject aag \<circ> cur_thread) (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)
 2. 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>x2. ep = SendEP x2 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint (SendEP x2)) epptr and is_subject aag \<circ> cur_thread) (do y <- assert (x2 \<noteq> []);
y <- set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (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 x2) receiver (AllowGrant \<in> rights) else set_thread_state (hd x2) Inactive else do set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od)
 3. 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>x3. ep = RecvEP x3 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint (RecvEP x3)) epptr and is_subject aag \<circ> cur_thread) (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) proof (prove)
goal (3 subgoals):
 1. 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>x2. ep = SendEP x2 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint (SendEP x2)) epptr and is_subject aag \<circ> cur_thread) (do y <- assert (x2 \<noteq> []);
y <- set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (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 x2) receiver (AllowGrant \<in> rights) else set_thread_state (hd x2) Inactive else do set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od)
 2. \<lbrakk>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); ep = IdleEP\<rbrakk> \<Longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint IdleEP) epptr and is_subject aag \<circ> cur_thread) (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)
 3. 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>x3. ep = RecvEP x3 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint (RecvEP x3)) epptr and is_subject aag \<circ> cur_thread) (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) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>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); ep = IdleEP\<rbrakk> \<Longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint IdleEP) epptr and is_subject aag \<circ> cur_thread) (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)
 2. 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>x3. ep = RecvEP x3 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint (RecvEP x3)) epptr and is_subject aag \<circ> cur_thread) (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)
 3. 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>x2. ep = SendEP x2 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint (SendEP x2)) epptr and is_subject aag \<circ> cur_thread) (do y <- assert (x2 \<noteq> []);
y <- set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (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 x2) receiver (AllowGrant \<in> rights) else set_thread_state (hd x2) Inactive else do set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od) proof (prove)
goal (1 subgoal):
 1. 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>x2. ep = SendEP x2 \<longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint (SendEP x2)) epptr and is_subject aag \<circ> cur_thread) (do y <- assert (x2 \<noteq> []);
y <- set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (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 x2) receiver (AllowGrant \<in> rights) else set_thread_state (hd x2) Inactive else do set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>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); ep = SendEP x2\<rbrakk> \<Longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and ko_at (Endpoint (SendEP x2)) epptr and is_subject aag \<circ> cur_thread) (do y <- assert (x2 \<noteq> []);
y <- set_endpoint epptr (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (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 x2) receiver (AllowGrant \<in> rights) else set_thread_state (hd x2) Inactive else do set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>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); ep = SendEP x2; invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> ko_at (Endpoint (SendEP x2)) epptr s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> x2 \<noteq> [] \<longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb (hd x2) s = get_tcb (hd x2) t) \<and> ((\<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> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag (hd x2)) \<and> aag_can_read_or_affect aag l (hd x2) \<and> (sender_is_call xa \<longrightarrow> (sender_can_grant xa \<longrightarrow> aag_can_read aag (hd x2)) \<and> (sender_can_grant_reply xa \<longrightarrow> aag_can_read aag (hd x2))) \<and> (\<not> sender_is_call xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) s \<and> valid_mdb s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag (hd x2)) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>s y ys. \<lbrakk>ep = SendEP (y # ys); is_subject aag receiver; invs s; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; pas_cur_domain aag s; ko_at (Endpoint (SendEP (y # ys))) epptr s; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb y s = get_tcb y t) \<and> ((\<exists>ya. get_tcb y s = Some ya) \<longrightarrow> (\<forall>x xa. tcb_state (the (get_tcb y s)) = BlockedOnSend x xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case ys of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl (y # ys))) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag y) \<and> aag_can_read_or_affect aag l y \<and> (sender_is_call xa \<longrightarrow> (sender_can_grant xa \<longrightarrow> aag_can_read aag y) \<and> (sender_can_grant_reply xa \<longrightarrow> aag_can_read aag y)) \<and> (\<not> sender_is_call xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case ys of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl (y # ys))) s \<and> valid_mdb s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag y) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ep = SendEP (sender # queue); is_subject aag receiver; invs s; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; pas_cur_domain aag s; ko_at (Endpoint (SendEP (sender # queue))) epptr s; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb sender s = get_tcb sender t) \<and> ((\<exists>y. get_tcb sender s = Some y) \<longrightarrow> (\<forall>x xa. tcb_state (the (get_tcb sender s)) = BlockedOnSend x xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl (sender # queue))) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag sender) \<and> aag_can_read_or_affect aag l sender \<and> (sender_is_call xa \<longrightarrow> (sender_can_grant xa \<longrightarrow> aag_can_read aag sender) \<and> (sender_can_grant_reply xa \<longrightarrow> aag_can_read aag sender)) \<and> (\<not> sender_is_call xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl (sender # queue))) s \<and> valid_mdb s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag sender) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ep = SendEP (sender # queue); is_subject aag receiver; invs s; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; pas_cur_domain aag s; ko_at (Endpoint (SendEP (sender # queue))) epptr s; is_subject aag (cur_thread s); valid_ep (case tl (sender # queue) of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl (sender # queue))) s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb sender s = get_tcb sender t) \<and> ((\<exists>y. get_tcb sender s = Some y) \<longrightarrow> (\<forall>x xa. tcb_state (the (get_tcb sender s)) = BlockedOnSend x xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl (sender # queue))) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag sender) \<and> aag_can_read_or_affect aag l sender \<and> (sender_is_call xa \<longrightarrow> (sender_can_grant xa \<longrightarrow> aag_can_read aag sender) \<and> (sender_can_grant_reply xa \<longrightarrow> aag_can_read aag sender)) \<and> (\<not> sender_is_call xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl (sender # queue))) s \<and> valid_mdb s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag sender) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ep = SendEP (sender # queue); is_subject aag receiver; invs s; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; pas_cur_domain aag s; ko_at (Endpoint (SendEP (sender # queue))) epptr s; is_subject aag (cur_thread s); valid_ep (case tl (sender # queue) of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl (sender # queue))) s; \<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) sender s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb sender s = get_tcb sender t) \<and> ((\<exists>y. get_tcb sender s = Some y) \<longrightarrow> (\<forall>x xa. tcb_state (the (get_tcb sender s)) = BlockedOnSend x xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl (sender # queue))) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag sender) \<and> aag_can_read_or_affect aag l sender \<and> (sender_is_call xa \<longrightarrow> (sender_can_grant xa \<longrightarrow> aag_can_read aag sender) \<and> (sender_can_grant_reply xa \<longrightarrow> aag_can_read aag sender)) \<and> (\<not> sender_is_call xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl (sender # queue))) s \<and> valid_mdb s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag sender) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>pl tcb. \<lbrakk>ep = SendEP (sender # queue); is_subject aag receiver; invs s; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); valid_ep (case queue of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl (sender # queue))) s; kheap s epptr = Some (Endpoint (SendEP (sender # queue))); kheap s sender = Some (TCB tcb); tcb_state tcb = BlockedOnSend epptr pl\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb sender s = get_tcb sender t) \<and> ((\<exists>y. get_tcb sender s = Some y) \<longrightarrow> (\<forall>x xa. tcb_state (the (get_tcb sender s)) = BlockedOnSend x xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag sender) \<and> aag_can_read_or_affect aag l sender \<and> (sender_is_call xa \<longrightarrow> (sender_can_grant xa \<longrightarrow> aag_can_read aag sender) \<and> (sender_can_grant_reply xa \<longrightarrow> aag_can_read aag sender)) \<and> (\<not> sender_is_call xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag sender) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s))) proof (prove)
goal (2 subgoals):
 1. \<And>pl tcb. \<lbrakk>ep = SendEP (sender # queue); is_subject aag receiver; invs s; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); valid_ep (case queue of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl (sender # queue))) s; kheap s epptr = Some (Endpoint (SendEP (sender # queue))); kheap s sender = Some (TCB tcb); tcb_state tcb = BlockedOnSend epptr pl; aag_can_read aag sender\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> get_tcb sender s = get_tcb sender t) \<and> ((\<exists>y. get_tcb sender s = Some y) \<longrightarrow> (\<forall>x xa. tcb_state (the (get_tcb sender s)) = BlockedOnSend x xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag sender) \<and> aag_can_read_or_affect aag l sender \<and> (sender_is_call xa \<longrightarrow> (sender_can_grant xa \<longrightarrow> aag_can_read aag sender) \<and> (sender_can_grant_reply xa \<longrightarrow> aag_can_read aag sender)) \<and> (\<not> sender_is_call xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (sender_can_grant xa \<longrightarrow> is_subject aag sender) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)))
 2. \<And>pl tcb. \<lbrakk>ep = SendEP (sender # queue); is_subject aag receiver; invs s; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); valid_ep (case queue of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl (sender # queue))) s; kheap s epptr = Some (Endpoint (SendEP (sender # queue))); kheap s sender = Some (TCB tcb); tcb_state tcb = BlockedOnSend epptr pl\<rbrakk> \<Longrightarrow> aag_can_read aag sender proof (prove)
goal (1 subgoal):
 1. \<And>pl tcb. \<lbrakk>ep = SendEP (sender # queue); is_subject aag receiver; invs s; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); valid_ep (case queue of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl (sender # queue))) s; kheap s epptr = Some (Endpoint (SendEP (sender # queue))); kheap s sender = Some (TCB tcb); tcb_state tcb = BlockedOnSend epptr pl\<rbrakk> \<Longrightarrow> aag_can_read aag sender proof (prove)
goal (1 subgoal):
 1. \<And>pl tcb. \<lbrakk>ep = SendEP (sender # queue); is_subject aag receiver; invs s; (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; \<forall>auth\<in>cap_rights_to_auth rights True. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); valid_ep (case queue of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl (sender # queue))) s; kheap s epptr = Some (Endpoint (SendEP (sender # queue))); kheap s sender = Some (TCB tcb); tcb_state tcb = BlockedOnSend epptr pl; (pasObjectAbs aag sender, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read aag sender proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!