theory Syscall_DR

lemma receive_ipc_cur_thread:
  notes do_nbrecv_failed_transfer_def[simp]
        if_split[split del]
  shows
  " \<lbrace>\<lambda>s. valid_objs s \<and>  P (cur_thread (s :: det_ext state))\<rbrace> receive_ipc a b c \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>" apply (simp add:receive_ipc_def bind_assoc) apply (wp|wpc|clarsimp)+ apply (simp add:setup_caller_cap_def) apply (wp dxo_wp_weak | simp)+ apply (rule_tac Q="\<lambda>r s. P (cur_thread s)" in hoare_strengthen_post) apply clarsimp apply (wp|wpc)+ apply clarsimp apply (clarsimp simp:neq_Nil_conv) apply (rename_tac list queue sender) apply (rule_tac Q="\<lambda>r s. P (cur_thread s) \<and> tcb_at (hd list) s" in hoare_strengthen_post) apply wp apply (clarsimp simp:st_tcb_at_def tcb_at_def) apply (wp get_simple_ko_wp[where f=Notification] gbn_wp | wpc | simp add: Ipc_A.isActive_def)+ apply (rule_tac Q="\<lambda>r s. valid_ep r s \<and> P (cur_thread s)" in hoare_strengthen_post) apply (wp get_simple_ko_valid[where f=Endpoint, simplified valid_ep_def2[symmetric]]) apply (clarsimp simp:valid_ep_def) apply auto[1] apply (rule hoare_pre) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs s \<and> P (cur_thread s)\<rbrace> Ipc_A.receive_ipc a b c \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs s \<and> P (cur_thread s)\<rbrace> do (epptr, rights) <- case b of cap.EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail;
ep <- get_endpoint epptr;
ntfnptr <- get_bound_notification a;
ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if (\<exists>y. ntfnptr = Some y) \<and> isActive ntfn then complete_signal (the ntfnptr) a else case ep of IdleEP \<Rightarrow> case c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [a])
od | False \<Rightarrow> do_nbrecv_failed_transfer a | 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (sender_badge data) (sender_can_grant data) a;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender a (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 c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [a]))
od | False \<Rightarrow> do_nbrecv_failed_transfer a
od \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace> proof (prove)
goal (16 subgoals):
 1. \<And>x1 x2 ntfnptr ntfn x2a queue sender sender_state data. \<lbrakk>ntfnptr = None \<or> \<not> isActive ntfn; sender_is_call data; sender_can_grant data \<or> sender_can_grant_reply data\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 (x1, x2) x1 x2 (SendEP x2a) ntfnptr ntfn x2a () queue sender () sender_state data ()\<rbrace> setup_caller_cap sender a (AllowGrant \<in> x2) \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a; sender_is_call data; \<not> (sender_can_grant data \<or> sender_can_grant_reply data)\<rbrakk> \<Longrightarrow> \<lbrace>?R72 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc\<rbrace> set_thread_state sender Inactive \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a; \<not> sender_is_call data\<rbrakk> \<Longrightarrow> \<lbrace>?R71 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc\<rbrace> do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B68 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data\<rbrace> Ipc_A.do_ipc_transfer sender (Some x1) (sender_badge data) (sender_can_grant data) a \<lbrace>\<lambda>xc s. (sender_is_call data \<longrightarrow> (sender_can_grant data \<or> sender_can_grant_reply data \<longrightarrow> ?Q72 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc s) \<and> (\<not> (sender_can_grant data \<or> sender_can_grant_reply data) \<longrightarrow> ?R72 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc s)) \<and> (\<not> sender_is_call data \<longrightarrow> ?R71 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc s)\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B67 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>?B68 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B67 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 8. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 9. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 10. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>x1 x2 ntfnptr ntfn x2a queue sender sender_state data. \<lbrakk>ntfnptr = None \<or> \<not> isActive ntfn; sender_is_call data; sender_can_grant data \<or> sender_can_grant_reply data\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 (x1, x2) x1 x2 (SendEP x2a) ntfnptr ntfn x2a () queue sender () sender_state data ()\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (cap.ReplyCap sender False (if AllowGrant \<in> x2 then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (a, tcb_cnode_index 3)
od \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a; sender_is_call data; \<not> (sender_can_grant data \<or> sender_can_grant_reply data)\<rbrakk> \<Longrightarrow> \<lbrace>?R72 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc\<rbrace> set_thread_state sender Inactive \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a; \<not> sender_is_call data\<rbrakk> \<Longrightarrow> \<lbrace>?R71 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc\<rbrace> do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B68 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data\<rbrace> Ipc_A.do_ipc_transfer sender (Some x1) (sender_badge data) (sender_can_grant data) a \<lbrace>\<lambda>xc s. (sender_is_call data \<longrightarrow> (sender_can_grant data \<or> sender_can_grant_reply data \<longrightarrow> ?Q72 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc s) \<and> (\<not> (sender_can_grant data \<or> sender_can_grant_reply data) \<longrightarrow> ?R72 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc s)) \<and> (\<not> sender_is_call data \<longrightarrow> ?R71 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state data xc s)\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B67 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>?B68 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb sender_state\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B67 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 8. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 9. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 10. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
A total of 16 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>x x1 x2 ep ntfnptr ntfn x2a queue sender sender_state. \<lbrakk>x = (x1, x2); ntfnptr = None \<or> \<not> isActive ntfn; ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B67 (x1, x2) x1 x2 (SendEP x2a) ntfnptr ntfn x2a () queue sender () sender_state\<rbrace> case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>\<lambda>data s. (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> P (cur_thread s)) \<and> (sender_can_grant_reply data \<longrightarrow> P (cur_thread s)) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> P (cur_thread s))) \<and> (\<not> sender_is_call data \<longrightarrow> P (cur_thread s))\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B67 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>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [a]))
od | False \<Rightarrow> do_nbrecv_failed_transfer a \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 8. \<And>x x1 x2 ep ntfnptr. x = (x1, x2) \<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. ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn \<longrightarrow> P (cur_thread s)) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (c = True \<longrightarrow> P (cur_thread s)) \<and> (c = False \<longrightarrow> P (cur_thread 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. x = (x1, x2) \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification a \<lbrace>?B14 x x1 x2 ep\<rbrace>
 10. \<And>x x1 x2. x = (x1, x2) \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>x x1 x2 ep ntfnptr ntfn x2a queue sender sender_state. \<lbrakk>x = (x1, x2); ntfnptr = None \<or> \<not> isActive ntfn; ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B67 (x1, x2) x1 x2 (SendEP x2a) ntfnptr ntfn x2a () queue sender () sender_state\<rbrace> case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a queue sender sender_state rv s. \<lbrakk>x = (x1, x2); ntfnptr = None \<or> \<not> isActive ntfn; ep = SendEP x2a; P (cur_thread s)\<rbrakk> \<Longrightarrow> (sender_is_call rv \<longrightarrow> (sender_can_grant rv \<longrightarrow> P (cur_thread s)) \<and> (sender_can_grant_reply rv \<longrightarrow> P (cur_thread s)) \<and> (\<not> sender_can_grant rv \<and> \<not> sender_can_grant_reply rv \<longrightarrow> P (cur_thread s))) \<and> (\<not> sender_is_call rv \<longrightarrow> P (cur_thread s))
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B67 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>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 8. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [a]))
od | False \<Rightarrow> do_nbrecv_failed_transfer a \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 9. \<And>x x1 x2 ep ntfnptr. x = (x1, x2) \<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. ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn \<longrightarrow> P (cur_thread s)) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (c = True \<longrightarrow> P (cur_thread s)) \<and> (c = False \<longrightarrow> P (cur_thread 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. x = (x1, x2) \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification a \<lbrace>?B14 x x1 x2 ep\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>x1 x2 ntfnptr ntfn x2a queue sender sender_state. ntfnptr = None \<or> \<not> isActive ntfn \<Longrightarrow> \<lbrace>?B67 (x1, x2) x1 x2 (SendEP x2a) ntfnptr ntfn x2a () queue sender () sender_state\<rbrace> case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a queue sender sender_state rv s. \<lbrakk>x = (x1, x2); ntfnptr = None \<or> \<not> isActive ntfn; ep = SendEP x2a; P (cur_thread s)\<rbrakk> \<Longrightarrow> (sender_is_call rv \<longrightarrow> (sender_can_grant rv \<longrightarrow> P (cur_thread s)) \<and> (sender_can_grant_reply rv \<longrightarrow> P (cur_thread s)) \<and> (\<not> sender_can_grant rv \<and> \<not> sender_can_grant_reply rv \<longrightarrow> P (cur_thread s))) \<and> (\<not> sender_is_call rv \<longrightarrow> P (cur_thread s))
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B67 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>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 8. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [a]))
od | False \<Rightarrow> do_nbrecv_failed_transfer a \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 9. \<And>x x1 x2 ep ntfnptr. x = (x1, x2) \<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. ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn \<longrightarrow> P (cur_thread s)) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (c = True \<longrightarrow> P (cur_thread s)) \<and> (c = False \<longrightarrow> P (cur_thread 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. x = (x1, x2) \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification a \<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 queue sender sender_state rv s. \<lbrakk>x = (x1, x2); ntfnptr = None \<or> \<not> isActive ntfn; ep = SendEP x2a; P (cur_thread s)\<rbrakk> \<Longrightarrow> (sender_is_call rv \<longrightarrow> (sender_can_grant rv \<longrightarrow> P (cur_thread s)) \<and> (sender_can_grant_reply rv \<longrightarrow> P (cur_thread s)) \<and> (\<not> sender_can_grant rv \<and> \<not> sender_can_grant_reply rv \<longrightarrow> P (cur_thread s))) \<and> (\<not> sender_is_call rv \<longrightarrow> P (cur_thread s))
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>\<lambda>a b. (a = Running \<longrightarrow> True) \<and> (inactive a \<longrightarrow> True) \<and> (a = Restart \<longrightarrow> True) \<and> (\<forall>x xa. a = BlockedOnReceive x xa \<longrightarrow> True) \<and> (\<forall>x xa. a = BlockedOnSend x xa \<longrightarrow> P (cur_thread b)) \<and> (awaiting_reply a \<longrightarrow> True) \<and> (\<forall>x. a = BlockedOnNotification x \<longrightarrow> True) \<and> (idle a \<longrightarrow> True)\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [a]))
od | False \<Rightarrow> do_nbrecv_failed_transfer a \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 8. \<And>x x1 x2 ep ntfnptr. x = (x1, x2) \<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. ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn \<longrightarrow> P (cur_thread s)) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (c = True \<longrightarrow> P (cur_thread s)) \<and> (c = False \<longrightarrow> P (cur_thread 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. x = (x1, x2) \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification a \<lbrace>?B14 x x1 x2 ep\<rbrace>
 10. \<And>x x1 x2. x = (x1, x2) \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>\<lambda>a b. (a = Running \<longrightarrow> True) \<and> (inactive a \<longrightarrow> True) \<and> (a = Restart \<longrightarrow> True) \<and> (\<forall>x xa. a = BlockedOnReceive x xa \<longrightarrow> True) \<and> (\<forall>x xa. a = BlockedOnSend x xa \<longrightarrow> P (cur_thread b)) \<and> (awaiting_reply a \<longrightarrow> True) \<and> (\<forall>x. a = BlockedOnNotification x \<longrightarrow> True) \<and> (idle a \<longrightarrow> True)\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [a]))
od | False \<Rightarrow> do_nbrecv_failed_transfer a \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr. x = (x1, x2) \<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. ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn \<longrightarrow> P (cur_thread s)) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (c = True \<longrightarrow> P (cur_thread s)) \<and> (c = False \<longrightarrow> P (cur_thread 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. x = (x1, x2) \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification a \<lbrace>?B14 x x1 x2 ep\<rbrace>
 9. \<And>x x1 x2. x = (x1, x2) \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
 10. \<lbrace>?Q2\<rbrace> case b of cap.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. ntfnptr = None \<or> \<not> isActive ntfn \<Longrightarrow> \<lbrace>?B65 (x1, x2) x1 x2 (SendEP x2a) ntfnptr ntfn x2a () queue sender ()\<rbrace> get_thread_state sender \<lbrace>\<lambda>a b. (\<exists>x xa. a = BlockedOnSend x xa) \<longrightarrow> P (cur_thread b)\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [a]))
od | False \<Rightarrow> do_nbrecv_failed_transfer a \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr. x = (x1, x2) \<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. ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn \<longrightarrow> P (cur_thread s)) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (c = True \<longrightarrow> P (cur_thread s)) \<and> (c = False \<longrightarrow> P (cur_thread 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. x = (x1, x2) \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification a \<lbrace>?B14 x x1 x2 ep\<rbrace>
 9. \<And>x x1 x2. x = (x1, x2) \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
 10. \<lbrace>?Q2\<rbrace> case b of cap.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 list queue sender. ntfnptr = None \<or> \<not> isActive ntfn \<Longrightarrow> \<lbrace>?B65 (x1, x2) x1 x2 (SendEP list) ntfnptr ntfn list () queue sender ()\<rbrace> get_thread_state sender \<lbrace>\<lambda>a b. (\<exists>x xa. a = BlockedOnSend x xa) \<longrightarrow> P (cur_thread b)\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [a]))
od | False \<Rightarrow> do_nbrecv_failed_transfer a \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr. x = (x1, x2) \<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. ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn \<longrightarrow> P (cur_thread s)) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (c = True \<longrightarrow> P (cur_thread s)) \<and> (c = False \<longrightarrow> P (cur_thread 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. x = (x1, x2) \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification a \<lbrace>?B14 x x1 x2 ep\<rbrace>
 9. \<And>x x1 x2. x = (x1, x2) \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
 10. \<lbrace>?Q2\<rbrace> case b of cap.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 (12 subgoals):
 1. \<And>x1 x2 ntfnptr ntfn list queue sender. ntfnptr = None \<or> \<not> isActive ntfn \<Longrightarrow> \<lbrace>?B65 (x1, x2) x1 x2 (SendEP list) ntfnptr ntfn list () queue sender ()\<rbrace> get_thread_state sender \<lbrace>\<lambda>r s. P (cur_thread s) \<and> tcb_at (hd list) s\<rbrace>
 2. \<And>x1 x2 ntfnptr ntfn list queue sender rv s. \<lbrakk>ntfnptr = None \<or> \<not> isActive ntfn; P (cur_thread s) \<and> tcb_at (hd list) s\<rbrakk> \<Longrightarrow> (\<exists>x xa. rv = BlockedOnSend x xa) \<longrightarrow> P (cur_thread s)
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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>?B65 x x1 x2 ep ntfnptr ntfn x2a xa queue sender\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [a]))
od | False \<Rightarrow> do_nbrecv_failed_transfer a \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 8. \<And>x x1 x2 ep ntfnptr. x = (x1, x2) \<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. ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn \<longrightarrow> P (cur_thread s)) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (c = True \<longrightarrow> P (cur_thread s)) \<and> (c = False \<longrightarrow> P (cur_thread 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. x = (x1, x2) \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification a \<lbrace>?B14 x x1 x2 ep\<rbrace>
 10. \<And>x x1 x2. x = (x1, x2) \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x1 x2 ntfnptr ntfn list queue sender rv s. \<lbrakk>ntfnptr = None \<or> \<not> isActive ntfn; P (cur_thread s) \<and> tcb_at (hd list) s\<rbrakk> \<Longrightarrow> (\<exists>x xa. rv = BlockedOnSend x xa) \<longrightarrow> P (cur_thread s)
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue sender. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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. P (cur_thread b) \<and> tcb_at (hd x2a) b\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [a]))
od | False \<Rightarrow> do_nbrecv_failed_transfer a \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 7. \<And>x x1 x2 ep ntfnptr. x = (x1, x2) \<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. ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn \<longrightarrow> P (cur_thread s)) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (c = True \<longrightarrow> P (cur_thread s)) \<and> (c = False \<longrightarrow> P (cur_thread 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. x = (x1, x2) \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification a \<lbrace>?B14 x x1 x2 ep\<rbrace>
 9. \<And>x x1 x2. x = (x1, x2) \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
 10. \<lbrace>?Q2\<rbrace> case b of cap.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>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B64 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. P (cur_thread b) \<and> tcb_at (hd x2a) b\<rbrace>
 2. \<And>x x1 x2 ep ntfnptr ntfn x2a xa queue. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace> return $ hd x2a \<lbrace>?B64 x x1 x2 ep ntfnptr ntfn x2a xa queue\<rbrace>
 3. \<And>x x1 x2 ep ntfnptr ntfn x2a xa. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace> return $ tl x2a \<lbrace>?B63 x x1 x2 ep ntfnptr ntfn x2a xa\<rbrace>
 4. \<And>x x1 x2 ep ntfnptr ntfn x2a. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 x x1 x2 ep ntfnptr ntfn x2a\<rbrace> assert (x2a \<noteq> []) \<lbrace>?B61 x x1 x2 ep ntfnptr ntfn x2a\<rbrace>
 5. \<And>x x1 x2 ep ntfnptr ntfn x3. \<lbrakk>x = (x1, x2); \<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x x1 x2 ep ntfnptr ntfn x3\<rbrace> case c of True \<Rightarrow> do set_thread_state a (BlockedOnReceive x1 \<lparr>receiver_can_grant = AllowGrant \<in> x2\<rparr>);
set_endpoint x1 (RecvEP (x3 @ [a]))
od | False \<Rightarrow> do_nbrecv_failed_transfer a \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>
 6. \<And>x x1 x2 ep ntfnptr. x = (x1, x2) \<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. ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn \<longrightarrow> P (cur_thread s)) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (c = True \<longrightarrow> P (cur_thread s)) \<and> (c = False \<longrightarrow> P (cur_thread 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. x = (x1, x2) \<Longrightarrow> \<lbrace>?B13 x x1 x2 ep\<rbrace> get_bound_notification a \<lbrace>?B14 x x1 x2 ep\<rbrace>
 8. \<And>x x1 x2. x = (x1, x2) \<Longrightarrow> \<lbrace>?R11 x x1 x2\<rbrace> get_endpoint x1 \<lbrace>?B13 x x1 x2\<rbrace>
 9. \<lbrace>?Q2\<rbrace> case b of cap.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. valid_objs s \<and> P (cur_thread s) \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>x x1 x2. x = (x1, x2) \<Longrightarrow> \<lbrace>?R11 (x1, x2) x1 x2\<rbrace> get_endpoint x1 \<lbrace>\<lambda>ep s. \<forall>ntfn. bound_tcb_at ((=) ntfn) a s \<longrightarrow> (ntfn = None \<longrightarrow> (ep = IdleEP \<longrightarrow> P (cur_thread s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> P (cur_thread s) \<and> tcb_at (hd x) s) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> P (cur_thread s))) \<and> (\<forall>x. ntfn = Some x \<longrightarrow> (\<forall>ntfn. ko_at (kernel_object.Notification ntfn) x s \<longrightarrow> ((case ntfn_obj ntfn of ActiveNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> P (cur_thread s)) \<and> (\<not> (case ntfn_obj ntfn of ActiveNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (ep = IdleEP \<longrightarrow> P (cur_thread s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> P (cur_thread s) \<and> tcb_at (hd x) s) \<and> ((\<exists>x. ep = RecvEP x) \<longrightarrow> P (cur_thread s)))))\<rbrace>
 2. \<lbrace>?Q2\<rbrace> case b of cap.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>
 3. \<And>s. valid_objs s \<and> P (cur_thread s) \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>x x1 x2. x = (x1, x2) \<Longrightarrow> \<lbrace>?R11 (x1, x2) x1 x2\<rbrace> get_endpoint x1 \<lbrace>\<lambda>r s. valid_ep r s \<and> P (cur_thread s)\<rbrace>
 2. \<And>x x1 x2 rv s. \<lbrakk>x = (x1, x2); valid_ep rv s \<and> P (cur_thread s)\<rbrakk> \<Longrightarrow> \<forall>ntfn. bound_tcb_at ((=) ntfn) a s \<longrightarrow> (ntfn = None \<longrightarrow> (rv = IdleEP \<longrightarrow> P (cur_thread s)) \<and> (\<forall>x. rv = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> P (cur_thread s) \<and> tcb_at (hd x) s) \<and> ((\<exists>x. rv = RecvEP x) \<longrightarrow> P (cur_thread s))) \<and> (\<forall>x. ntfn = Some x \<longrightarrow> (\<forall>ntfn. ko_at (kernel_object.Notification ntfn) x s \<longrightarrow> ((case ntfn_obj ntfn of ActiveNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> P (cur_thread s)) \<and> (\<not> (case ntfn_obj ntfn of ActiveNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (rv = IdleEP \<longrightarrow> P (cur_thread s)) \<and> (\<forall>x. rv = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> P (cur_thread s) \<and> tcb_at (hd x) s) \<and> ((\<exists>x. rv = RecvEP x) \<longrightarrow> P (cur_thread s)))))
 3. \<lbrace>?Q2\<rbrace> case b of cap.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>
 4. \<And>s. valid_objs s \<and> P (cur_thread s) \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>x x1 x2 rv s. \<lbrakk>x = (x1, x2); valid_ep rv s \<and> P (cur_thread s)\<rbrakk> \<Longrightarrow> \<forall>ntfn. bound_tcb_at ((=) ntfn) a s \<longrightarrow> (ntfn = None \<longrightarrow> (rv = IdleEP \<longrightarrow> P (cur_thread s)) \<and> (\<forall>x. rv = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> P (cur_thread s) \<and> tcb_at (hd x) s) \<and> ((\<exists>x. rv = RecvEP x) \<longrightarrow> P (cur_thread s))) \<and> (\<forall>x. ntfn = Some x \<longrightarrow> (\<forall>ntfn. ko_at (kernel_object.Notification ntfn) x s \<longrightarrow> ((case ntfn_obj ntfn of ActiveNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> P (cur_thread s)) \<and> (\<not> (case ntfn_obj ntfn of ActiveNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (rv = IdleEP \<longrightarrow> P (cur_thread s)) \<and> (\<forall>x. rv = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> P (cur_thread s) \<and> tcb_at (hd x) s) \<and> ((\<exists>x. rv = RecvEP x) \<longrightarrow> P (cur_thread s)))))
 2. \<lbrace>?Q2\<rbrace> case b of cap.EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> valid_objs s \<and> P (cur_thread s)\<rbrace>
 3. \<And>s. valid_objs s \<and> P (cur_thread s) \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s ntfn. \<lbrakk>case rv of IdleEP \<Rightarrow> True | SendEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at t s) \<and> distinct ts | RecvEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at t s) \<and> distinct ts; P (cur_thread s); bound_tcb_at ((=) ntfn) a s\<rbrakk> \<Longrightarrow> (ntfn = None \<longrightarrow> (\<forall>x. rv = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> tcb_at (hd x) s)) \<and> (\<forall>x. ntfn = Some x \<longrightarrow> (\<forall>ntfn. ko_at (kernel_object.Notification ntfn) x s \<longrightarrow> \<not> (case ntfn_obj ntfn of ActiveNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (\<forall>x. rv = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> tcb_at (hd x) s)))
 2. \<lbrace>?Q2\<rbrace> case b of cap.EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> valid_objs s \<and> P (cur_thread s)\<rbrace>
 3. \<And>s. valid_objs s \<and> P (cur_thread s) \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> case b of cap.EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> valid_objs s \<and> P (cur_thread s)\<rbrace>
 2. \<And>s. valid_objs s \<and> P (cur_thread s) \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q288\<rbrace> case b of cap.EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> valid_objs s \<and> P (cur_thread s)\<rbrace>
 2. \<And>s. ?Q2 s \<Longrightarrow> ?Q288 s
 3. \<And>s. valid_objs s \<and> P (cur_thread s) \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!