theory Ipc_AC

lemma cancel_ipc_receive_blocked_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and st_tcb_at (receive_blocked) t and
    (sym_refs o state_refs_of) and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and
    K (abs_has_auth_to aag Receive t ntfnptr \<and> aag_has_auth_to aag Notify ntfnptr)\<rbrace>
   cancel_ipc t
   \<lbrace>\<lambda>_. integrity_once_ts_upd t Running aag X st\<rbrace>" apply (clarsimp simp: cancel_ipc_def bind_assoc) apply (rule hoare_seq_ext[OF _ gts_sp]) apply (rule hoare_name_pre_state) apply (subgoal_tac "case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False") apply (simp add: blocked_cancel_ipc_def bind_assoc set_simple_ko_def set_object_def
                    get_ep_queue_def get_blocking_object_def
             split: thread_state.splits) apply (rule hoare_pre) apply (wp set_thread_state_integrity_once_ts_upd get_object_wp get_simple_ko_wp
          | wpc)+ apply (clarsimp simp: st_tcb_at_def2 obj_at_def) apply (rename_tac ep payload s tcb ntfn) apply (drule_tac t="tcb_state tcb" in sym) apply (subgoal_tac "st_tcb_at ((=) (tcb_state tcb)) t s") apply (drule(1) sym_refs_st_tcb_atD) apply (clarsimp simp: obj_at_def ep_q_refs_of_def fun_upd_def get_tcb_def
                   split: endpoint.splits cong: if_cong) apply (intro impI conjI, simp_all)[1] apply (erule integrity_trans) apply (simp add: integrity_def) apply (intro impI conjI allI) apply clarsimp apply (rule tro_ep_unblock; simp?) apply (erule get_tcb_recv_blocked_implies_receive, erule get_tcb_rev; solves\<open>simp\<close>) apply (rule_tac ep=ep in tro_tcb_send[OF refl refl];
           fastforce intro!: tcb.equality arch_tcb_context_set_eq[symmetric]
                       simp: indirect_send_def pred_tcb_at_def obj_at_def) apply (fastforce simp: integrity_asids_kh_upds) apply (fastforce simp: indirect_send_def pred_tcb_at_def obj_at_def) apply (fastforce simp: pred_tcb_at_def obj_at_def receive_blocked_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)\<rbrace> cancel_ipc t \<lbrace>\<lambda>_. integrity_once_ts_upd t Running aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)\<rbrace> do state <- get_thread_state t;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. integrity_once_ts_upd t Running aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))\<rbrace> case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return () \<lbrace>\<lambda>_. integrity_once_ts_upd t Running aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return () \<lbrace>\<lambda>_. integrity_once_ts_upd t Running aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state s. \<lbrakk>(st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return () \<lbrace>\<lambda>_. integrity_once_ts_upd t Running aag X st\<rbrace>
 2. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>state s x41 x42. \<lbrakk>st_tcb_at ((=) (BlockedOnReceive x41 x42)) t s; integrity aag X st s; pas_refined aag s; st_tcb_at receive_blocked t s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; state = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do ep <- get_endpoint x41;
queue <- case ep of IdleEP \<Rightarrow> fail | SendEP x \<Rightarrow> return x | RecvEP x \<Rightarrow> return x;
x <- get_object x41;
xa <- assert (a_type x = AEndpoint \<or> a_type x = ANTFN);
x <- assert (\<exists>y. Endpoint y = x);
x <- get_object x41;
x <- assert (a_type x = AEndpoint);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(x41 \<mapsto> Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue)))\<rparr>);
set_thread_state t Inactive
od \<lbrace>\<lambda>_. integrity_once_ts_upd t Running aag X st\<rbrace>
 2. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>state s x41 x42. \<lbrakk>st_tcb_at ((=) (BlockedOnReceive x41 x42)) t s; integrity aag X st s; pas_refined aag s; st_tcb_at receive_blocked t s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; state = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 state s x41 x42\<rbrace> do ep <- get_endpoint x41;
queue <- case ep of IdleEP \<Rightarrow> fail | SendEP x \<Rightarrow> return x | RecvEP x \<Rightarrow> return x;
x <- get_object x41;
xa <- assert (a_type x = AEndpoint \<or> a_type x = ANTFN);
x <- assert (\<exists>y. Endpoint y = x);
x <- get_object x41;
x <- assert (a_type x = AEndpoint);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(x41 \<mapsto> Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue)))\<rparr>);
set_thread_state t Inactive
od \<lbrace>\<lambda>_. integrity_once_ts_upd t Running aag X st\<rbrace>
 2. \<And>state s x41 x42 sa. \<lbrakk>st_tcb_at ((=) (BlockedOnReceive x41 x42)) t s; integrity aag X st s; pas_refined aag s; st_tcb_at receive_blocked t s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; state = BlockedOnReceive x41 x42; s = sa\<rbrakk> \<Longrightarrow> ?Q101 state s x41 x42 sa
 3. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>state s x41 x42 sa. \<lbrakk>st_tcb_at ((=) (BlockedOnReceive x41 x42)) t s; integrity aag X st s; pas_refined aag s; st_tcb_at receive_blocked t s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; state = BlockedOnReceive x41 x42; s = sa\<rbrakk> \<Longrightarrow> \<forall>ntfn. ko_at (Endpoint ntfn) x41 sa \<longrightarrow> (ntfn = IdleEP \<longrightarrow> True) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> (\<forall>ko. ko_at ko x41 sa \<longrightarrow> a_type ko = AEndpoint \<or> a_type ko = ANTFN \<longrightarrow> (\<exists>y. Endpoint y = ko) \<longrightarrow> (\<forall>ko. ko_at ko x41 sa \<longrightarrow> a_type ko = AEndpoint \<longrightarrow> integrity_once_ts_upd t Running aag X st (sa\<lparr>kheap := (kheap sa)(x41 \<mapsto> Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x)))\<rparr>)))) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> (\<forall>ko. ko_at ko x41 sa \<longrightarrow> a_type ko = AEndpoint \<or> a_type ko = ANTFN \<longrightarrow> (\<exists>y. Endpoint y = ko) \<longrightarrow> (\<forall>ko. ko_at ko x41 sa \<longrightarrow> a_type ko = AEndpoint \<longrightarrow> integrity_once_ts_upd t Running aag X st (sa\<lparr>kheap := (kheap sa)(x41 \<mapsto> Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x)))\<rparr>))))
 2. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 sa tcb ntfn. \<lbrakk>integrity aag X st sa; pas_refined aag sa; sym_refs (state_refs_of sa); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t sa; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; BlockedOnReceive x41 x42 = tcb_state tcb; kheap sa t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap sa x41 = Some (Endpoint ntfn)\<rbrakk> \<Longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> integrity aag X st (sa\<lparr>kheap := (\<lambda>a. if a = x41 then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap sa a)(t \<mapsto> TCB (the (get_tcb t (sa\<lparr>kheap := \<lambda>a. if a = x41 then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap sa a\<rparr>))\<lparr>tcb_state := Running\<rparr>))\<rparr>)) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> integrity aag X st (sa\<lparr>kheap := (\<lambda>a. if a = x41 then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap sa a)(t \<mapsto> TCB (the (get_tcb t (sa\<lparr>kheap := \<lambda>a. if a = x41 then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap sa a\<rparr>))\<lparr>tcb_state := Running\<rparr>))\<rparr>))
 2. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; BlockedOnReceive ep payload = tcb_state tcb; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn)\<rbrakk> \<Longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a)(t \<mapsto> TCB (the (get_tcb t (s\<lparr>kheap := \<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a\<rparr>))\<lparr>tcb_state := Running\<rparr>))\<rparr>)) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a)(t \<mapsto> TCB (the (get_tcb t (s\<lparr>kheap := \<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a\<rparr>))\<lparr>tcb_state := Running\<rparr>))\<rparr>))
 2. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a)(t \<mapsto> TCB (the (get_tcb t (s\<lparr>kheap := \<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a\<rparr>))\<lparr>tcb_state := Running\<rparr>))\<rparr>)) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a)(t \<mapsto> TCB (the (get_tcb t (s\<lparr>kheap := \<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a\<rparr>))\<lparr>tcb_state := Running\<rparr>))\<rparr>))
 2. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload; st_tcb_at ((=) (tcb_state tcb)) t s\<rbrakk> \<Longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a)(t \<mapsto> TCB (the (get_tcb t (s\<lparr>kheap := \<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a\<rparr>))\<lparr>tcb_state := Running\<rparr>))\<rparr>)) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a)(t \<mapsto> TCB (the (get_tcb t (s\<lparr>kheap := \<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a\<rparr>))\<lparr>tcb_state := Running\<rparr>))\<rparr>))
 2. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 3. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload; \<exists>ts ntfn. tcb_state tcb = ts \<and> obj_at (tcb_ntfn_is_bound ntfn) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfn \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfn. obj_at (\<lambda>ko. (t, symreftype tp) \<in> refs_of ko) x s)\<rbrakk> \<Longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a)(t \<mapsto> TCB (the (get_tcb t (s\<lparr>kheap := \<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a\<rparr>))\<lparr>tcb_state := Running\<rparr>))\<rparr>)) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a)(t \<mapsto> TCB (the (get_tcb t (s\<lparr>kheap := \<lambda>a. if a = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ntfn (remove1 t x))) else kheap s a\<rparr>))\<lparr>tcb_state := Running\<rparr>))\<rparr>))
 2. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 3. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ep payload s tcb x3 ntfna x. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x3)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x3; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko\<rbrakk> \<Longrightarrow> (t = ep \<longrightarrow> x3 = x \<longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>x. if x = ep then Some (TCB (the None\<lparr>tcb_state := Running\<rparr>)) else kheap s x\<rparr>)) \<and> (t \<noteq> ep \<longrightarrow> x3 = x \<longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>xa. if xa = t then Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)) else if xa = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x3) (remove1 t x))) else kheap s xa\<rparr>))
 2. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 3. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ep payload s tcb x3 ntfna x. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>xa. if xa = t then Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)) else if xa = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x3) (remove1 t x))) else kheap s xa\<rparr>)
 2. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 3. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ep payload s tcb x3 ntfna x. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>kheap := \<lambda>xa. if xa = t then Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)) else if xa = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x3) (remove1 t x))) else kheap s xa\<rparr>)
 2. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 3. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ep payload s tcb x3 ntfna x. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x\<rbrakk> \<Longrightarrow> (\<forall>xa. (xa = ep \<longrightarrow> object_integrity aag (pasObjectAbs aag ep) (Some (Endpoint (RecvEP x))) (Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x3) (remove1 t x))))) \<and> (xa \<noteq> ep \<longrightarrow> xa = t \<longrightarrow> object_integrity aag (pasObjectAbs aag t) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>))))) \<and> (\<forall>xa a. integrity_asids aag {pasSubject aag} xa a s (s\<lparr>kheap := \<lambda>xa. if xa = t then Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)) else if xa = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x3) (remove1 t x))) else kheap s xa\<rparr>))
 2. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 3. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>ep payload s tcb x3 ntfna x xa. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x; xa = ep\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag ep) (Some (Endpoint (RecvEP x))) (Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x3) (remove1 t x))))
 2. \<And>ep payload s tcb x3 ntfna x xa. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x; xa \<noteq> ep; xa = t\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag t) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)))
 3. \<And>ep payload s tcb x3 ntfna x xa a. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x\<rbrakk> \<Longrightarrow> integrity_asids aag {pasSubject aag} xa a s (s\<lparr>kheap := \<lambda>xa. if xa = t then Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)) else if xa = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x3) (remove1 t x))) else kheap s xa\<rparr>)
 4. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 5. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>ep payload s tcb ntfna x. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag ep) (Some (Endpoint (RecvEP x))) (Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x) (remove1 t x))))
 2. \<And>ep payload s tcb x3 ntfna x xa. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x; xa \<noteq> ep; xa = t\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag t) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)))
 3. \<And>ep payload s tcb x3 ntfna x xa a. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x\<rbrakk> \<Longrightarrow> integrity_asids aag {pasSubject aag} xa a s (s\<lparr>kheap := \<lambda>xa. if xa = t then Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)) else if xa = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x3) (remove1 t x))) else kheap s xa\<rparr>)
 4. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 5. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>ep payload s tcb ntfna x. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep\<rbrakk> \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag
 2. \<And>ep payload s tcb x3 ntfna x xa. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x; xa \<noteq> ep; xa = t\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag t) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)))
 3. \<And>ep payload s tcb x3 ntfna x xa a. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x\<rbrakk> \<Longrightarrow> integrity_asids aag {pasSubject aag} xa a s (s\<lparr>kheap := \<lambda>xa. if xa = t then Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)) else if xa = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x3) (remove1 t x))) else kheap s xa\<rparr>)
 4. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 5. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>ep payload s tcb x3 ntfna x xa. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x; xa \<noteq> ep; xa = t\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag t) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)))
 2. \<And>ep payload s tcb x3 ntfna x xa a. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x\<rbrakk> \<Longrightarrow> integrity_asids aag {pasSubject aag} xa a s (s\<lparr>kheap := \<lambda>xa. if xa = t then Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)) else if xa = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x3) (remove1 t x))) else kheap s xa\<rparr>)
 3. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 4. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ep payload s tcb x3 ntfna x xa a. \<lbrakk>pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (BlockedOnReceive ep payload); kheap s ep = Some (Endpoint (RecvEP x)); tcb_state tcb = BlockedOnReceive ep payload; tcb_ntfn_is_bound ntfna (TCB tcb); state_refs_of s t = insert (ep, TCBBlockedRecv) (tcb_bound_refs ntfna); t \<in> set x; \<forall>x\<in>tcb_bound_refs ntfna. case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (t, symreftype tp) \<in> refs_of ko; t \<noteq> ep; x3 = x\<rbrakk> \<Longrightarrow> integrity_asids aag {pasSubject aag} xa a s (s\<lparr>kheap := \<lambda>xa. if xa = t then Some (TCB (tcb\<lparr>tcb_state := Running\<rparr>)) else if xa = ep then Some (Endpoint (case remove1 t x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue (RecvEP x3) (remove1 t x))) else kheap s xa\<rparr>)
 2. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 3. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ep payload s tcb ntfn. \<lbrakk>integrity aag X st s; pas_refined aag s; sym_refs (state_refs_of s); bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t s; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); receive_blocked (tcb_state tcb); kheap s ep = Some (Endpoint ntfn); tcb_state tcb = BlockedOnReceive ep payload\<rbrakk> \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s
 2. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and pas_refined aag and st_tcb_at receive_blocked t and sym_refs \<circ> state_refs_of and bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and (\<lambda>y. (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!