theory Syscall_AI

lemma receive_ipc_st_tcb_at_runnable:
  "\<lbrace>st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s)) and K (t' \<noteq> t) \<rbrace>
   receive_ipc t' a b
   \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>" unfolding receive_ipc_def apply (rule hoare_gen_asm) apply (wpc | wp sts_st_tcb_at_other
        | clarsimp simp: do_nbrecv_failed_transfer_def setup_caller_cap_def | rule conjI)+ apply (wp hoare_drop_imps) apply (wp hoare_drop_imps) apply wpc apply ((wp gts_wp gbn_wp  hoare_vcg_all_lift sts_st_tcb_at_other | wpc
                           | simp add: do_nbrecv_failed_transfer_def | wp (once) hoare_drop_imps)+)[8] apply clarsimp apply (wp gts_wp) apply (wp hoare_drop_imps hoare_vcg_all_lift)[1] apply ((wp sts_st_tcb_at_other get_simple_ko_wp gbn_wp get_simple_ko_wp | wpc)+)[8] apply clarsimp apply (rule conjI) apply clarsimp apply (rename_tac sendq) apply (frule list.collapse[symmetric]) apply (drule st_tcb_at_state_refs_ofD) apply (frule (1) sym_refs_ko_atD) apply clarsimp apply (drule_tac x="hd sendq" in bspec, clarsimp) apply (case_tac ts; clarsimp simp: obj_at_def state_refs_of_def dest!: refs_in_tcb_bound_refs) apply clarsimp apply (rename_tac sendq) apply (frule list.collapse[symmetric]) apply (drule st_tcb_at_state_refs_ofD) apply (frule (1) sym_refs_ko_atD) apply clarsimp apply (drule_tac x="hd sendq" in bspec, clarsimp) apply (case_tac ts; clarsimp simp: obj_at_def state_refs_of_def dest!: refs_in_tcb_bound_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s)) and K (t' \<noteq> t)\<rbrace> receive_ipc t' a b \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s)) and K (t' \<noteq> t)\<rbrace> do (epptr, rights) <- case a of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail;
ep <- get_endpoint epptr;
ntfnptr <- get_bound_notification t';
ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if ntfnptr \<noteq> None \<and> isActive ntfn then complete_signal (the ntfnptr) t' else case ep of IdleEP \<Rightarrow> case b of True \<Rightarrow> do set_thread_state t' (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [t'])
od | False \<Rightarrow> do_nbrecv_failed_transfer t' | 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) t';
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender t' (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 b of True \<Rightarrow> do set_thread_state t' (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [t']))
od | False \<Rightarrow> do_nbrecv_failed_transfer t'
od \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (1 subgoal):
 1. t' \<noteq> t \<Longrightarrow> \<lbrace>st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace> do (epptr, rights) <- case a of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail;
ep <- get_endpoint epptr;
ntfnptr <- get_bound_notification t';
ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if ntfnptr \<noteq> None \<and> isActive ntfn then complete_signal (the ntfnptr) t' else case ep of IdleEP \<Rightarrow> case b of True \<Rightarrow> do set_thread_state t' (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [t'])
od | False \<Rightarrow> do_nbrecv_failed_transfer t' | 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) t';
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender t' (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 b of True \<Rightarrow> do set_thread_state t' (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [t']))
od | False \<Rightarrow> do_nbrecv_failed_transfer t'
od \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (13 subgoals):
 1. \<And>x1 x2 ntfnptr ntfn x2a queue sender sender_state data. \<lbrakk>t' \<noteq> t; ntfnptr = None \<or> \<not> isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>?B60 (x1, x2) x1 x2 (SendEP x2a) ntfnptr ntfn x2a () queue sender () sender_state data\<rbrace> do_ipc_transfer sender (Some x1) (sender_badge data) (sender_can_grant data) t' \<lbrace>\<lambda>xc s. (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> (sender_can_grant_reply data \<longrightarrow> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> st_tcb_at runnable t s \<and> t \<noteq> sender)) \<and> (\<not> sender_is_call data \<longrightarrow> st_tcb_at runnable t s \<and> t \<noteq> sender)\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B59 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state\<rbrace> case sender_state of BlockedOnSend ref data \<Rightarrow> return data | _ \<Rightarrow> fail \<lbrace>?B60 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B59 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace> set_endpoint x1 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue \<lbrace>?B57 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 8. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case b of True \<Rightarrow> do set_thread_state t' (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [t']))
od | False \<Rightarrow> do_nbrecv_failed_transfer t' \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 9. \<And>x x1 x2 ep ntfnptr. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B14 x x1 x2 ep ntfnptr\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>ntfn s. (ntfnptr \<noteq> None \<and> isActive ntfn \<longrightarrow> st_tcb_at runnable t s) \<and> (\<not> (ntfnptr \<noteq> None \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (b = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (b = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R31 x x1 x2 ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R32 x x1 x2 ep ntfnptr ntfn xa s))\<rbrace>
 10. \<And>x x1 x2 ep. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification t' \<lbrace>?B14 x x1 x2 ep\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B59 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state\<rbrace> case sender_state of BlockedOnSend ref data \<Rightarrow> return data | _ \<Rightarrow> fail \<lbrace>\<lambda>a b. ((st_tcb_at runnable t b \<and> t \<noteq> sender) \<and> (st_tcb_at runnable t b \<and> t \<noteq> sender) \<and> st_tcb_at runnable t b \<and> t \<noteq> sender) \<and> st_tcb_at runnable t b \<and> t \<noteq> sender\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B59 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace> set_endpoint x1 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue \<lbrace>?B57 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case b of True \<Rightarrow> do set_thread_state t' (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [t']))
od | False \<Rightarrow> do_nbrecv_failed_transfer t' \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 8. \<And>x x1 x2 ep ntfnptr. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B14 x x1 x2 ep ntfnptr\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>ntfn s. (ntfnptr \<noteq> None \<and> isActive ntfn \<longrightarrow> st_tcb_at runnable t s) \<and> (\<not> (ntfnptr \<noteq> None \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (b = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (b = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R31 x x1 x2 ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R32 x x1 x2 ep ntfnptr ntfn xa s))\<rbrace>
 9. \<And>x x1 x2 ep. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification t' \<lbrace>?B14 x x1 x2 ep\<rbrace>
 10. \<And>x x1 x2. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B59 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state\<rbrace> case sender_state of BlockedOnSend ref data \<Rightarrow> return data | _ \<Rightarrow> fail \<lbrace>\<lambda>rv s. st_tcb_at runnable t s \<and> t \<noteq> sender \<and> ((st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B59 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace> set_endpoint x1 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue \<lbrace>?B57 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case b of True \<Rightarrow> do set_thread_state t' (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [t']))
od | False \<Rightarrow> do_nbrecv_failed_transfer t' \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 8. \<And>x x1 x2 ep ntfnptr. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B14 x x1 x2 ep ntfnptr\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>ntfn s. (ntfnptr \<noteq> None \<and> isActive ntfn \<longrightarrow> st_tcb_at runnable t s) \<and> (\<not> (ntfnptr \<noteq> None \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (b = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (b = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R31 x x1 x2 ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R32 x x1 x2 ep ntfnptr ntfn xa s))\<rbrace>
 9. \<And>x x1 x2 ep. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification t' \<lbrace>?B14 x x1 x2 ep\<rbrace>
 10. \<And>x x1 x2. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
A total of 12 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a; sender_state = Running\<rbrakk> \<Longrightarrow> \<lbrace>?R177 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state\<rbrace> fail \<lbrace>\<lambda>rv s. st_tcb_at runnable t s \<and> t \<noteq> sender \<and> ((st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a; inactive sender_state\<rbrakk> \<Longrightarrow> \<lbrace>?R176 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state\<rbrace> fail \<lbrace>\<lambda>rv s. st_tcb_at runnable t s \<and> t \<noteq> sender \<and> ((st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a; sender_state = Restart\<rbrakk> \<Longrightarrow> \<lbrace>?R175 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state\<rbrace> fail \<lbrace>\<lambda>rv s. st_tcb_at runnable t s \<and> t \<noteq> sender \<and> ((st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state x41 x42. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a; sender_state = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>?R174 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state x41 x42\<rbrace> fail \<lbrace>\<lambda>rv s. st_tcb_at runnable t s \<and> t \<noteq> sender \<and> ((st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state x51 x52. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a; sender_state = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>?R171 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state x51 x52\<rbrace> return x52 \<lbrace>\<lambda>rv s. st_tcb_at runnable t s \<and> t \<noteq> sender \<and> ((st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a; awaiting_reply sender_state\<rbrakk> \<Longrightarrow> \<lbrace>?R168 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state\<rbrace> fail \<lbrace>\<lambda>rv s. st_tcb_at runnable t s \<and> t \<noteq> sender \<and> ((st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state x7. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a; sender_state = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> \<lbrace>?R167 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state x7\<rbrace> fail \<lbrace>\<lambda>rv s. st_tcb_at runnable t s \<and> t \<noteq> sender \<and> ((st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender\<rbrace>
 8. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a; idle sender_state\<rbrakk> \<Longrightarrow> \<lbrace>?R165 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state\<rbrace> fail \<lbrace>\<lambda>rv s. st_tcb_at runnable t s \<and> t \<noteq> sender \<and> ((st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender\<rbrace>
 9. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>\<lambda>sender_state s. (sender_state = Running \<longrightarrow> ?R177 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state s) \<and> (inactive sender_state \<longrightarrow> ?R176 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state s) \<and> (sender_state = Restart \<longrightarrow> ?R175 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state s) \<and> (\<forall>xc xd. sender_state = BlockedOnReceive xc xd \<longrightarrow> ?R174 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state xc xd s) \<and> (\<forall>xc xd. sender_state = BlockedOnSend xc xd \<longrightarrow> ?R171 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state xc xd s) \<and> (awaiting_reply sender_state \<longrightarrow> ?R168 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state s) \<and> (\<forall>xc. sender_state = BlockedOnNotification xc \<longrightarrow> ?R167 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state xc s) \<and> (idle sender_state \<longrightarrow> ?R165 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state s)\<rbrace>
 10. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace> set_endpoint x1 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue \<lbrace>?B57 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
A total of 19 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B57 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>\<lambda>sender_state s. (sender_state = Running \<longrightarrow> True) \<and> (inactive sender_state \<longrightarrow> True) \<and> (sender_state = Restart \<longrightarrow> True) \<and> (\<forall>x xa. sender_state = BlockedOnReceive x xa \<longrightarrow> True) \<and> (\<forall>x xa. sender_state = BlockedOnSend x xa \<longrightarrow> st_tcb_at runnable t s \<and> t \<noteq> sender \<and> ((st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> st_tcb_at runnable t s \<and> t \<noteq> sender) \<and> (awaiting_reply sender_state \<longrightarrow> True) \<and> (\<forall>x. sender_state = BlockedOnNotification x \<longrightarrow> True) \<and> (idle sender_state \<longrightarrow> True)\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace> set_endpoint x1 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue \<lbrace>?B57 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case b of True \<Rightarrow> do set_thread_state t' (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [t']))
od | False \<Rightarrow> do_nbrecv_failed_transfer t' \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B14 x x1 x2 ep ntfnptr\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>ntfn s. (ntfnptr \<noteq> None \<and> isActive ntfn \<longrightarrow> st_tcb_at runnable t s) \<and> (\<not> (ntfnptr \<noteq> None \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (b = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (b = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R31 x x1 x2 ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R32 x x1 x2 ep ntfnptr ntfn xa s))\<rbrace>
 8. \<And>x x1 x2 ep. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification t' \<lbrace>?B14 x x1 x2 ep\<rbrace>
 9. \<And>x x1 x2. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
 10. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q2\<rbrace> case a of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> ?R11 x xa xb s\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x1 x2 ntfnptr ntfn x2a queue sender. \<lbrakk>t' \<noteq> t; ntfnptr = None \<or> \<not> isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>?B57 (x1, x2) x1 x2 (SendEP x2a) ntfnptr ntfn x2a () queue sender ()\<rbrace> get_thread_state sender \<lbrace>\<lambda>sender_state s. (\<exists>x xa. sender_state = BlockedOnSend x xa) \<longrightarrow> st_tcb_at runnable t s \<and> t \<noteq> sender \<and> st_tcb_at runnable t s \<and> t \<noteq> sender\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace> set_endpoint x1 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue \<lbrace>?B57 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case b of True \<Rightarrow> do set_thread_state t' (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [t']))
od | False \<Rightarrow> do_nbrecv_failed_transfer t' \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B14 x x1 x2 ep ntfnptr\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>ntfn s. (ntfnptr \<noteq> None \<and> isActive ntfn \<longrightarrow> st_tcb_at runnable t s) \<and> (\<not> (ntfnptr \<noteq> None \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (b = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (b = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R31 x x1 x2 ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R32 x x1 x2 ep ntfnptr ntfn xa s))\<rbrace>
 8. \<And>x x1 x2 ep. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification t' \<lbrace>?B14 x x1 x2 ep\<rbrace>
 9. \<And>x x1 x2. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
 10. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q2\<rbrace> case a of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> ?R11 x xa xb s\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace> set_endpoint x1 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue \<lbrace>\<lambda>a b. \<forall>st. st_tcb_at ((=) st) sender b \<longrightarrow> (\<exists>x xa. st = BlockedOnSend x xa) \<longrightarrow> st_tcb_at runnable t b \<and> t \<noteq> sender \<and> st_tcb_at runnable t b \<and> t \<noteq> sender\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B56 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case b of True \<Rightarrow> do set_thread_state t' (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [t']))
od | False \<Rightarrow> do_nbrecv_failed_transfer t' \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B14 x x1 x2 ep ntfnptr\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>ntfn s. (ntfnptr \<noteq> None \<and> isActive ntfn \<longrightarrow> st_tcb_at runnable t s) \<and> (\<not> (ntfnptr \<noteq> None \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (b = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (b = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R31 x x1 x2 ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R32 x x1 x2 ep ntfnptr ntfn xa s))\<rbrace>
 7. \<And>x x1 x2 ep. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification t' \<lbrace>?B14 x x1 x2 ep\<rbrace>
 8. \<And>x x1 x2. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
 9. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q2\<rbrace> case a of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> ?R11 x xa xb s\<rbrace>
 10. \<And>s. \<lbrakk>t' \<noteq> t; (st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (9 subgoals):
 1. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>\<lambda>sender s. \<forall>x. st_tcb_at runnable t s \<and> t \<noteq> sender \<and> st_tcb_at runnable t s \<and> t \<noteq> sender\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B55 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B53 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>t' \<noteq> t; x = (x1, x2); \<not> (ntfnptr \<noteq> None \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case b of True \<Rightarrow> do set_thread_state t' (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [t']))
od | False \<Rightarrow> do_nbrecv_failed_transfer t' \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B14 x x1 x2 ep ntfnptr\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>ntfn s. (ntfnptr \<noteq> None \<and> isActive ntfn \<longrightarrow> st_tcb_at runnable t s) \<and> (\<not> (ntfnptr \<noteq> None \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (b = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (b = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R31 x x1 x2 ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R32 x x1 x2 ep ntfnptr ntfn xa s))\<rbrace>
 6. \<And>x x1 x2 ep. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification t' \<lbrace>?B14 x x1 x2 ep\<rbrace>
 7. \<And>x x1 x2. \<lbrakk>t' \<noteq> t; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
 8. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q2\<rbrace> case a of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> ?R11 x xa xb s\<rbrace>
 9. \<And>s. \<lbrakk>t' \<noteq> t; (st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>t' \<noteq> t; (st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s))) s\<rbrakk> \<Longrightarrow> (a = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. a = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. a = EndpointCap x xa xb \<longrightarrow> (\<forall>xa xc. (x, xb) = (xa, xc) \<longrightarrow> (\<forall>ntfn. ko_at (Endpoint ntfn) xa s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) t' s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfna \<noteq> None \<and> isActive default_notification \<longrightarrow> st_tcb_at runnable t s) \<and> (\<not> (ntfna \<noteq> None \<and> isActive default_notification) \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (b = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (b = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<forall>xa. st_tcb_at runnable t s \<and> t \<noteq> hd x \<and> st_tcb_at runnable t s \<and> t \<noteq> hd x)) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> (b = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (b = False \<longrightarrow> st_tcb_at runnable t s)))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfnb. ko_at (Notification ntfnb) x s \<longrightarrow> (ntfna \<noteq> None \<and> isActive ntfnb \<longrightarrow> st_tcb_at runnable t s) \<and> (\<not> (ntfna \<noteq> None \<and> isActive ntfnb) \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (b = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (b = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<forall>xa. st_tcb_at runnable t s \<and> t \<noteq> hd x \<and> st_tcb_at runnable t s \<and> t \<noteq> hd x)) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> (b = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (b = False \<longrightarrow> st_tcb_at runnable t s))))))))) \<and> (\<forall>x xa xb. a = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. a = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. a = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. a = ThreadCap x \<longrightarrow> True) \<and> (a = DomainCap \<longrightarrow> True) \<and> (a = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. a = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. a = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. a = ArchObjectCap x \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb ntfn ntfna. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint ntfn) x s; bound_tcb_at ((=) ntfna) t' s\<rbrakk> \<Longrightarrow> (ntfna = None \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x)) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> \<not> isActive ntfna \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x))) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb ntfn ntfna. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint ntfn) x s; bound_tcb_at ((=) ntfna) t' s\<rbrakk> \<Longrightarrow> ntfna = None \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x)
 2. \<And>s x xa xb ntfn ntfna. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint ntfn) x s; bound_tcb_at ((=) ntfna) t' s\<rbrakk> \<Longrightarrow> \<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> \<not> isActive ntfna \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb xc. \<lbrakk>t' \<noteq> hd xc; st_tcb_at runnable (hd xc) s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP xc)) x s; bound_tcb_at ((=) None) t' s; xc \<noteq> []; t = hd xc\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa xb ntfn ntfna. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint ntfn) x s; bound_tcb_at ((=) ntfna) t' s\<rbrakk> \<Longrightarrow> \<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> \<not> isActive ntfna \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb sendq. \<lbrakk>t' \<noteq> hd sendq; st_tcb_at runnable (hd sendq) s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) None) t' s; sendq \<noteq> []; t = hd sendq\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa xb ntfn ntfna. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint ntfn) x s; bound_tcb_at ((=) ntfna) t' s\<rbrakk> \<Longrightarrow> \<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> \<not> isActive ntfna \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb sendq. \<lbrakk>t' \<noteq> hd sendq; st_tcb_at runnable (hd sendq) s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) None) t' s; sendq \<noteq> []; t = hd sendq; sendq = hd sendq # tl sendq\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa xb ntfn ntfna. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint ntfn) x s; bound_tcb_at ((=) ntfna) t' s\<rbrakk> \<Longrightarrow> \<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> \<not> isActive ntfna \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb sendq. \<lbrakk>t' \<noteq> hd sendq; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) None) t' s; sendq \<noteq> []; t = hd sendq; sendq = hd sendq # tl sendq; \<exists>ts ntfnptr. runnable ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) (hd sendq) s \<and> state_refs_of s (hd sendq) = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa xb ntfn ntfna. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint ntfn) x s; bound_tcb_at ((=) ntfna) t' s\<rbrakk> \<Longrightarrow> \<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> \<not> isActive ntfna \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb sendq. \<lbrakk>t' \<noteq> hd sendq; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) None) t' s; sendq \<noteq> []; t = hd sendq; sendq = hd sendq # tl sendq; \<exists>ts ntfnptr. runnable ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) (hd sendq) s \<and> state_refs_of s (hd sendq) = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr; state_refs_of s x = refs_of (Endpoint (SendEP sendq)) \<and> (\<forall>(xa, tp)\<in>refs_of (Endpoint (SendEP sendq)). obj_at (\<lambda>ko. (x, symreftype tp) \<in> refs_of ko) xa s)\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa xb ntfn ntfna. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint ntfn) x s; bound_tcb_at ((=) ntfna) t' s\<rbrakk> \<Longrightarrow> \<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> \<not> isActive ntfna \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb sendq ts ntfnptr. \<lbrakk>t' \<noteq> hd sendq; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) None) t' s; sendq \<noteq> []; t = hd sendq; state_refs_of s x = set sendq \<times> {EPSend}; \<forall>xa\<in>set sendq. obj_at (\<lambda>ko. (x, TCBBlockedSend) \<in> refs_of ko) xa s; runnable ts; obj_at (tcb_ntfn_is_bound ntfnptr) (hd sendq) s; state_refs_of s (hd sendq) = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa xb ntfn ntfna. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint ntfn) x s; bound_tcb_at ((=) ntfna) t' s\<rbrakk> \<Longrightarrow> \<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> \<not> isActive ntfna \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb sendq ts ntfnptr. \<lbrakk>t' \<noteq> hd sendq; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) None) t' s; sendq \<noteq> []; t = hd sendq; state_refs_of s x = set sendq \<times> {EPSend}; runnable ts; obj_at (tcb_ntfn_is_bound ntfnptr) (hd sendq) s; state_refs_of s (hd sendq) = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr; obj_at (\<lambda>ko. (x, TCBBlockedSend) \<in> refs_of ko) (hd sendq) s\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa xb ntfn ntfna. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint ntfn) x s; bound_tcb_at ((=) ntfna) t' s\<rbrakk> \<Longrightarrow> \<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> \<not> isActive ntfna \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb ntfn ntfna. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint ntfn) x s; bound_tcb_at ((=) ntfna) t' s\<rbrakk> \<Longrightarrow> \<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> \<not> isActive ntfna \<longrightarrow> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> t \<noteq> hd x)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb xc ntfnb xd. \<lbrakk>t' \<noteq> hd xd; st_tcb_at runnable (hd xd) s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP xd)) x s; bound_tcb_at ((=) (Some xc)) t' s; ko_at (Notification ntfnb) xc s; \<not> isActive ntfnb; xd \<noteq> []; t = hd xd\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb xc ntfnb sendq. \<lbrakk>t' \<noteq> hd sendq; st_tcb_at runnable (hd sendq) s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) (Some xc)) t' s; ko_at (Notification ntfnb) xc s; \<not> isActive ntfnb; sendq \<noteq> []; t = hd sendq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb xc ntfnb sendq. \<lbrakk>t' \<noteq> hd sendq; st_tcb_at runnable (hd sendq) s; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) (Some xc)) t' s; ko_at (Notification ntfnb) xc s; \<not> isActive ntfnb; sendq \<noteq> []; t = hd sendq; sendq = hd sendq # tl sendq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb xc ntfnb sendq. \<lbrakk>t' \<noteq> hd sendq; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) (Some xc)) t' s; ko_at (Notification ntfnb) xc s; \<not> isActive ntfnb; sendq \<noteq> []; t = hd sendq; sendq = hd sendq # tl sendq; \<exists>ts ntfnptr. runnable ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) (hd sendq) s \<and> state_refs_of s (hd sendq) = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb xc ntfnb sendq. \<lbrakk>t' \<noteq> hd sendq; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) (Some xc)) t' s; ko_at (Notification ntfnb) xc s; \<not> isActive ntfnb; sendq \<noteq> []; t = hd sendq; sendq = hd sendq # tl sendq; \<exists>ts ntfnptr. runnable ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) (hd sendq) s \<and> state_refs_of s (hd sendq) = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr; state_refs_of s x = refs_of (Endpoint (SendEP sendq)) \<and> (\<forall>(xa, tp)\<in>refs_of (Endpoint (SendEP sendq)). obj_at (\<lambda>ko. (x, symreftype tp) \<in> refs_of ko) xa s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb xc ntfnb sendq ts ntfnptr. \<lbrakk>t' \<noteq> hd sendq; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) (Some xc)) t' s; ko_at (Notification ntfnb) xc s; \<not> isActive ntfnb; sendq \<noteq> []; t = hd sendq; state_refs_of s x = set sendq \<times> {EPSend}; \<forall>xa\<in>set sendq. obj_at (\<lambda>ko. (x, TCBBlockedSend) \<in> refs_of ko) xa s; runnable ts; obj_at (tcb_ntfn_is_bound ntfnptr) (hd sendq) s; state_refs_of s (hd sendq) = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb xc ntfnb sendq ts ntfnptr. \<lbrakk>t' \<noteq> hd sendq; sym_refs (state_refs_of s); a = EndpointCap x xa xb; ko_at (Endpoint (SendEP sendq)) x s; bound_tcb_at ((=) (Some xc)) t' s; ko_at (Notification ntfnb) xc s; \<not> isActive ntfnb; sendq \<noteq> []; t = hd sendq; state_refs_of s x = set sendq \<times> {EPSend}; runnable ts; obj_at (tcb_ntfn_is_bound ntfnptr) (hd sendq) s; state_refs_of s (hd sendq) = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr; obj_at (\<lambda>ko. (x, TCBBlockedSend) \<in> refs_of ko) (hd sendq) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!