theory Ipc_IF

lemma receive_ipc_globals_equiv:
  notes do_nbrecv_failed_transfer_def[simp]
  shows "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
                           and pspace_distinct and pspace_aligned and valid_global_objs
                           and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
         receive_ipc thread cap is_blocking
         \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding receive_ipc_def thread_get_def including no_pre apply (wp) apply (simp add: split_def) apply (wp set_simple_ko_globals_equiv set_thread_state_globals_equiv
             setup_caller_cap_globals_equiv dxo_wp_weak as_user_globals_equiv
          | wpc
          | simp split del: if_split)+ apply (rule hoare_strengthen_post[where Q= "\<lambda>_. globals_equiv st and valid_arch_state
                                                                              and valid_global_objs"]) apply (wp do_ipc_transfer_globals_equiv as_user_globals_equiv) apply clarsimp apply (wp gts_wp get_simple_ko_sp | wpc)+ apply (wp hoare_vcg_all_lift hoare_drop_imps)[1] apply (wp set_simple_ko_globals_equiv | wpc)+ apply (wp set_thread_state_globals_equiv) apply (wp get_simple_ko_wp gbn_wp get_simple_ko_wp as_user_globals_equiv | wpc | simp)+ apply (rule hoare_pre) apply (wpc) apply (rule fail_wp | rule return_wp)+ by (auto intro: valid_ep_send_enqueue simp: neq_Nil_conv cong: case_list_cons_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> receive_ipc thread cap is_blocking \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> do (epptr, rights) <- case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail;
ep <- get_endpoint epptr;
ntfnptr <- get_bound_notification thread;
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) thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | 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) thread;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender thread (AllowGrant \<in> rights) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> do (epptr, rights) <- case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail;
ep <- get_endpoint epptr;
ntfnptr <- get_bound_notification thread;
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) thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | 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) thread;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender thread (AllowGrant \<in> rights) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?B x\<rbrace> case x of (epptr, rights) \<Rightarrow> do ep <- get_endpoint epptr;
ntfnptr <- get_bound_notification thread;
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) thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | 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) thread;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender thread (AllowGrant \<in> rights) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?B x\<rbrace> do ep <- get_endpoint (fst x);
ntfnptr <- get_bound_notification thread;
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) thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive (fst x) \<lparr>receiver_can_grant = AllowGrant \<in> snd x\<rparr>);
set_endpoint (fst x) (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint (fst x) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some (fst x)) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender thread (AllowGrant \<in> snd x) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive (fst x) \<lparr>receiver_can_grant = AllowGrant \<in> snd x\<rparr>);
set_endpoint (fst x) (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>?B\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>x ep ntfnptr ntfn x2 queue sender sender_state data. \<lbrakk>ntfnptr = None \<or> \<not> isActive ntfn; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B66 x (SendEP x2) ntfnptr ntfn x2 () queue sender () sender_state data\<rbrace> do_ipc_transfer sender (Some (fst x)) (sender_badge data) (sender_can_grant data) thread \<lbrace>\<lambda>xc s. (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (sender_can_grant_reply data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s)) \<and> (\<not> sender_is_call data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s)\<rbrace>
 2. \<And>x ep ntfnptr ntfn x2 xa queue sender xb sender_state. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B65 x ep ntfnptr ntfn x2 xa queue sender xb sender_state\<rbrace> case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B66 x ep ntfnptr ntfn x2 xa queue sender xb sender_state\<rbrace>
 3. \<And>x ep ntfnptr ntfn x2 xa queue sender xb. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x ep ntfnptr ntfn x2 xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B65 x ep ntfnptr ntfn x2 xa queue sender xb\<rbrace>
 4. \<And>x ep ntfnptr ntfn x2 xa queue sender. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B62 x ep ntfnptr ntfn x2 xa queue sender\<rbrace> set_endpoint (fst x) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue \<lbrace>?B63 x ep ntfnptr ntfn x2 xa queue sender\<rbrace>
 5. \<And>x ep ntfnptr ntfn x2 xa queue. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x ep ntfnptr ntfn x2 xa queue\<rbrace> return $ hd x2 \<lbrace>?B62 x ep ntfnptr ntfn x2 xa queue\<rbrace>
 6. \<And>x ep ntfnptr ntfn x2 xa. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B59 x ep ntfnptr ntfn x2 xa\<rbrace> return $ tl x2 \<lbrace>?B61 x ep ntfnptr ntfn x2 xa\<rbrace>
 7. \<And>x ep ntfnptr ntfn x2. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x ep ntfnptr ntfn x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B59 x ep ntfnptr ntfn x2\<rbrace>
 8. \<And>x ep ntfnptr ntfn x3. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x ep ntfnptr ntfn x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive (fst x) \<lparr>receiver_can_grant = AllowGrant \<in> snd x\<rparr>);
set_endpoint (fst x) (RecvEP (x3 @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 9. \<And>x ep ntfnptr. \<lbrace>?B16 x 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> (globals_equiv st and (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s))) s) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (is_blocking = False \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)) s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R33 x ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R34 x ep ntfnptr ntfn xa s))\<rbrace>
 10. \<And>x ep. \<lbrace>?B15 x ep\<rbrace> get_bound_notification thread \<lbrace>?B16 x ep\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>x ep ntfnptr ntfn x2 queue sender sender_state data. \<lbrakk>ntfnptr = None \<or> \<not> isActive ntfn; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B66 x (SendEP x2) ntfnptr ntfn x2 () queue sender () sender_state data\<rbrace> do_ipc_transfer sender (Some (fst x)) (sender_badge data) (sender_can_grant data) thread \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
 2. \<And>x ep ntfnptr ntfn x2 queue sender sender_state data rv s. \<lbrakk>ntfnptr = None \<or> \<not> isActive ntfn; ep = SendEP x2; (globals_equiv st and valid_arch_state and valid_global_objs) s\<rbrakk> \<Longrightarrow> (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (sender_can_grant_reply data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s)) \<and> (\<not> sender_is_call data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s)
 3. \<And>x ep ntfnptr ntfn x2 xa queue sender xb sender_state. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B65 x ep ntfnptr ntfn x2 xa queue sender xb sender_state\<rbrace> case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>?B66 x ep ntfnptr ntfn x2 xa queue sender xb sender_state\<rbrace>
 4. \<And>x ep ntfnptr ntfn x2 xa queue sender xb. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x ep ntfnptr ntfn x2 xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B65 x ep ntfnptr ntfn x2 xa queue sender xb\<rbrace>
 5. \<And>x ep ntfnptr ntfn x2 xa queue sender. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B62 x ep ntfnptr ntfn x2 xa queue sender\<rbrace> set_endpoint (fst x) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue \<lbrace>?B63 x ep ntfnptr ntfn x2 xa queue sender\<rbrace>
 6. \<And>x ep ntfnptr ntfn x2 xa queue. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x ep ntfnptr ntfn x2 xa queue\<rbrace> return $ hd x2 \<lbrace>?B62 x ep ntfnptr ntfn x2 xa queue\<rbrace>
 7. \<And>x ep ntfnptr ntfn x2 xa. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B59 x ep ntfnptr ntfn x2 xa\<rbrace> return $ tl x2 \<lbrace>?B61 x ep ntfnptr ntfn x2 xa\<rbrace>
 8. \<And>x ep ntfnptr ntfn x2. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x ep ntfnptr ntfn x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B59 x ep ntfnptr ntfn x2\<rbrace>
 9. \<And>x ep ntfnptr ntfn x3. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x ep ntfnptr ntfn x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive (fst x) \<lparr>receiver_can_grant = AllowGrant \<in> snd x\<rparr>);
set_endpoint (fst x) (RecvEP (x3 @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 10. \<And>x ep ntfnptr. \<lbrace>?B16 x 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> (globals_equiv st and (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s))) s) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (is_blocking = False \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)) s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R33 x ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R34 x ep ntfnptr ntfn xa s))\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>x ep ntfnptr ntfn x2 queue sender sender_state data rv s. \<lbrakk>ntfnptr = None \<or> \<not> isActive ntfn; ep = SendEP x2; (globals_equiv st and valid_arch_state and valid_global_objs) s\<rbrakk> \<Longrightarrow> (sender_is_call data \<longrightarrow> (sender_can_grant data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (sender_can_grant_reply data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (\<not> sender_can_grant data \<and> \<not> sender_can_grant_reply data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s)) \<and> (\<not> sender_is_call data \<longrightarrow> globals_equiv st s \<and> valid_arch_state s)
 2. \<And>x ep ntfnptr ntfn x2 xa queue sender xb sender_state. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B65 x ep ntfnptr ntfn x2 xa queue sender xb sender_state\<rbrace> case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>\<lambda>a b. (globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)) b \<and> valid_arch_state b \<and> valid_global_objs b\<rbrace>
 3. \<And>x ep ntfnptr ntfn x2 xa queue sender xb. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x ep ntfnptr ntfn x2 xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B65 x ep ntfnptr ntfn x2 xa queue sender xb\<rbrace>
 4. \<And>x ep ntfnptr ntfn x2 xa queue sender. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B62 x ep ntfnptr ntfn x2 xa queue sender\<rbrace> set_endpoint (fst x) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue \<lbrace>?B63 x ep ntfnptr ntfn x2 xa queue sender\<rbrace>
 5. \<And>x ep ntfnptr ntfn x2 xa queue. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x ep ntfnptr ntfn x2 xa queue\<rbrace> return $ hd x2 \<lbrace>?B62 x ep ntfnptr ntfn x2 xa queue\<rbrace>
 6. \<And>x ep ntfnptr ntfn x2 xa. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B59 x ep ntfnptr ntfn x2 xa\<rbrace> return $ tl x2 \<lbrace>?B61 x ep ntfnptr ntfn x2 xa\<rbrace>
 7. \<And>x ep ntfnptr ntfn x2. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x ep ntfnptr ntfn x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B59 x ep ntfnptr ntfn x2\<rbrace>
 8. \<And>x ep ntfnptr ntfn x3. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x ep ntfnptr ntfn x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive (fst x) \<lparr>receiver_can_grant = AllowGrant \<in> snd x\<rparr>);
set_endpoint (fst x) (RecvEP (x3 @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 9. \<And>x ep ntfnptr. \<lbrace>?B16 x 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> (globals_equiv st and (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s))) s) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (is_blocking = False \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)) s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R33 x ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R34 x ep ntfnptr ntfn xa s))\<rbrace>
 10. \<And>x ep. \<lbrace>?B15 x ep\<rbrace> get_bound_notification thread \<lbrace>?B16 x ep\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x ep ntfnptr ntfn x2 xa queue sender xb sender_state. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B65 x ep ntfnptr ntfn x2 xa queue sender xb sender_state\<rbrace> case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail \<lbrace>\<lambda>a b. (globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)) b \<and> valid_arch_state b \<and> valid_global_objs b\<rbrace>
 2. \<And>x ep ntfnptr ntfn x2 xa queue sender xb. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B63 x ep ntfnptr ntfn x2 xa queue sender xb\<rbrace> get_thread_state sender \<lbrace>?B65 x ep ntfnptr ntfn x2 xa queue sender xb\<rbrace>
 3. \<And>x ep ntfnptr ntfn x2 xa queue sender. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B62 x ep ntfnptr ntfn x2 xa queue sender\<rbrace> set_endpoint (fst x) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue \<lbrace>?B63 x ep ntfnptr ntfn x2 xa queue sender\<rbrace>
 4. \<And>x ep ntfnptr ntfn x2 xa queue. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x ep ntfnptr ntfn x2 xa queue\<rbrace> return $ hd x2 \<lbrace>?B62 x ep ntfnptr ntfn x2 xa queue\<rbrace>
 5. \<And>x ep ntfnptr ntfn x2 xa. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B59 x ep ntfnptr ntfn x2 xa\<rbrace> return $ tl x2 \<lbrace>?B61 x ep ntfnptr ntfn x2 xa\<rbrace>
 6. \<And>x ep ntfnptr ntfn x2. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x ep ntfnptr ntfn x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B59 x ep ntfnptr ntfn x2\<rbrace>
 7. \<And>x ep ntfnptr ntfn x3. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x ep ntfnptr ntfn x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive (fst x) \<lparr>receiver_can_grant = AllowGrant \<in> snd x\<rparr>);
set_endpoint (fst x) (RecvEP (x3 @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 8. \<And>x ep ntfnptr. \<lbrace>?B16 x 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> (globals_equiv st and (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s))) s) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (is_blocking = False \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)) s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R33 x ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R34 x ep ntfnptr ntfn xa s))\<rbrace>
 9. \<And>x ep. \<lbrace>?B15 x ep\<rbrace> get_bound_notification thread \<lbrace>?B16 x ep\<rbrace>
 10. \<And>x. \<lbrace>?B x\<rbrace> get_endpoint (fst x) \<lbrace>?B15 x\<rbrace>
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>x ep ntfnptr ntfn x2 xa queue sender. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B62 x ep ntfnptr ntfn x2 xa queue sender\<rbrace> set_endpoint (fst x) (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue) \<lbrace>\<lambda>xb s. \<forall>sta. st_tcb_at ((=) sta) sender s \<longrightarrow> (sta = Running \<longrightarrow> True) \<and> (inactive sta \<longrightarrow> True) \<and> (sta = Restart \<longrightarrow> True) \<and> (\<forall>x xa. sta = BlockedOnReceive x xa \<longrightarrow> True) \<and> (\<forall>x xa. sta = BlockedOnSend x xa \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (awaiting_reply sta \<longrightarrow> True) \<and> (\<forall>x. sta = BlockedOnNotification x \<longrightarrow> True) \<and> (idle sta \<longrightarrow> True)\<rbrace>
 2. \<And>x ep ntfnptr ntfn x2 xa queue. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x ep ntfnptr ntfn x2 xa queue\<rbrace> return $ hd x2 \<lbrace>?B62 x ep ntfnptr ntfn x2 xa queue\<rbrace>
 3. \<And>x ep ntfnptr ntfn x2 xa. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B59 x ep ntfnptr ntfn x2 xa\<rbrace> return $ tl x2 \<lbrace>?B61 x ep ntfnptr ntfn x2 xa\<rbrace>
 4. \<And>x ep ntfnptr ntfn x2. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x ep ntfnptr ntfn x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B59 x ep ntfnptr ntfn x2\<rbrace>
 5. \<And>x ep ntfnptr ntfn x3. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x ep ntfnptr ntfn x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive (fst x) \<lparr>receiver_can_grant = AllowGrant \<in> snd x\<rparr>);
set_endpoint (fst x) (RecvEP (x3 @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>x ep ntfnptr. \<lbrace>?B16 x 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> (globals_equiv st and (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s))) s) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (is_blocking = False \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)) s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R33 x ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R34 x ep ntfnptr ntfn xa s))\<rbrace>
 7. \<And>x ep. \<lbrace>?B15 x ep\<rbrace> get_bound_notification thread \<lbrace>?B16 x ep\<rbrace>
 8. \<And>x. \<lbrace>?B x\<rbrace> get_endpoint (fst x) \<lbrace>?B15 x\<rbrace>
 9. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>?B\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>x ep ntfnptr ntfn x2 xa queue sender sta xb xc. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?P193 x ep ntfnptr ntfn x2 xa queue sender sta xb xc\<rbrace> set_endpoint (fst x) (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue) \<lbrace>\<lambda>rv s. globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrace>
 2. \<And>x ep ntfnptr ntfn x2 xa queue sender st. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?P'191 x ep ntfnptr ntfn x2 xa queue sender st\<rbrace> set_endpoint (fst x) (case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue) \<lbrace>\<lambda>rv s. (awaiting_reply st \<longrightarrow> True) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> True) \<and> (idle st \<longrightarrow> True)\<rbrace>
 3. \<And>x ep ntfnptr ntfn x2 xa queue. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B61 x ep ntfnptr ntfn x2 xa queue\<rbrace> return $ hd x2 \<lbrace>\<lambda>sender s. \<forall>xb. True \<and> True \<and> True \<and> (\<forall>x xa. True) \<and> (\<forall>xc xd. ?P193 x ep ntfnptr ntfn x2 xa queue sender xb xc xd s) \<and> ?P'191 x ep ntfnptr ntfn x2 xa queue sender xb s\<rbrace>
 4. \<And>x ep ntfnptr ntfn x2 xa. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B59 x ep ntfnptr ntfn x2 xa\<rbrace> return $ tl x2 \<lbrace>?B61 x ep ntfnptr ntfn x2 xa\<rbrace>
 5. \<And>x ep ntfnptr ntfn x2. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x ep ntfnptr ntfn x2\<rbrace> assert (x2 \<noteq> []) \<lbrace>?B59 x ep ntfnptr ntfn x2\<rbrace>
 6. \<And>x ep ntfnptr ntfn x3. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x ep ntfnptr ntfn x3\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive (fst x) \<lparr>receiver_can_grant = AllowGrant \<in> snd x\<rparr>);
set_endpoint (fst x) (RecvEP (x3 @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 7. \<And>x ep ntfnptr. \<lbrace>?B16 x 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> (globals_equiv st and (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s))) s) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (is_blocking = False \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)) s)) \<and> (\<forall>xa. ep = SendEP xa \<longrightarrow> ?R33 x ep ntfnptr ntfn xa s) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> ?R34 x ep ntfnptr ntfn xa s))\<rbrace>
 8. \<And>x ep. \<lbrace>?B15 x ep\<rbrace> get_bound_notification thread \<lbrace>?B16 x ep\<rbrace>
 9. \<And>x. \<lbrace>?B x\<rbrace> get_endpoint (fst x) \<lbrace>?B15 x\<rbrace>
 10. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>?B\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x ep ntfnptr ntfn x3. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3; is_blocking = True\<rbrakk> \<Longrightarrow> \<lbrace>?R238 x ep ntfnptr ntfn x3\<rbrace> set_thread_state thread (BlockedOnReceive (fst x) \<lparr>receiver_can_grant = AllowGrant \<in> snd x\<rparr>) \<lbrace>\<lambda>xa s. globals_equiv st s \<and> valid_arch_state s\<rbrace>
 2. \<And>x ep ntfnptr ntfn x3. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3; is_blocking = False\<rbrakk> \<Longrightarrow> \<lbrace>?R237 x ep ntfnptr ntfn x3\<rbrace> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>x ep ntfnptr. \<lbrace>?B16 x 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> (globals_equiv st and (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s))) s) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (is_blocking = False \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)) s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<forall>xa. True \<and> True \<and> True \<and> (\<forall>x xa. True) \<and> (\<forall>xa xaa. (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s \<and> (valid_objs and valid_simple_obj (Endpoint (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x))) and K (is_simple_type (Endpoint (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x))))) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (awaiting_reply xa \<longrightarrow> True) \<and> (\<forall>x. xa = BlockedOnNotification x \<longrightarrow> True) \<and> (idle xa \<longrightarrow> True))) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> (is_blocking = True \<longrightarrow> ?R238 x ep ntfnptr ntfn xa s) \<and> (is_blocking = False \<longrightarrow> ?R237 x ep ntfnptr ntfn xa s)))\<rbrace>
 4. \<And>x ep. \<lbrace>?B15 x ep\<rbrace> get_bound_notification thread \<lbrace>?B16 x ep\<rbrace>
 5. \<And>x. \<lbrace>?B x\<rbrace> get_endpoint (fst x) \<lbrace>?B15 x\<rbrace>
 6. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>?B\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x ep ntfnptr ntfn x3. \<lbrakk>\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn); ep = RecvEP x3; is_blocking = False\<rbrakk> \<Longrightarrow> \<lbrace>?R237 x ep ntfnptr ntfn x3\<rbrace> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>x ep ntfnptr. \<lbrace>?B16 x 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> (globals_equiv st and (valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s))) s) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive ntfn) \<longrightarrow> (ep = IdleEP \<longrightarrow> (is_blocking = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (is_blocking = False \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)) s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> (\<forall>xa. True \<and> True \<and> True \<and> (\<forall>x xa. True) \<and> (\<forall>xa xaa. (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s \<and> (valid_objs and valid_simple_obj (Endpoint (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x))) and K (is_simple_type (Endpoint (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x))))) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> (awaiting_reply xa \<longrightarrow> True) \<and> (\<forall>x. xa = BlockedOnNotification x \<longrightarrow> True) \<and> (idle xa \<longrightarrow> True))) \<and> (\<forall>xa. ep = RecvEP xa \<longrightarrow> (is_blocking = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (is_blocking = False \<longrightarrow> ?R237 x ep ntfnptr ntfn xa s)))\<rbrace>
 3. \<And>x ep. \<lbrace>?B15 x ep\<rbrace> get_bound_notification thread \<lbrace>?B16 x ep\<rbrace>
 4. \<And>x. \<lbrace>?B x\<rbrace> get_endpoint (fst x) \<lbrace>?B15 x\<rbrace>
 5. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>?B\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q279\<rbrace> case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace>
 2. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)) s \<Longrightarrow> ?Q279 s proof (prove)
goal (13 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>?R331\<rbrace> fail \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>?R332 x21 x22 x23 x24\<rbrace> fail \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>?R333 x31 x32 x33\<rbrace> return (x31, x33) \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>?R334 x41 x42 x43\<rbrace> fail \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>?R335 x51 x52 x53\<rbrace> fail \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace>
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>?R336 x61 x62 x63\<rbrace> fail \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace>
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>?R337 x7\<rbrace> fail \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace>
 8. cap = DomainCap \<Longrightarrow> \<lbrace>?R338\<rbrace> fail \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>?R339\<rbrace> fail \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R340 x10\<rbrace> fail \<lbrace>\<lambda>x s. \<forall>ntfn. ko_at (Endpoint ntfn) (fst x) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))))))\<rbrace>
A total of 13 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)) s \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (\<forall>ntfn. ko_at (Endpoint ntfn) (fst (x, xb)) s \<longrightarrow> (\<forall>ntfna. bound_tcb_at ((=) ntfna) thread s \<longrightarrow> (ntfna = None \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s))) \<and> (\<forall>x. ntfna = Some x \<longrightarrow> (\<forall>ntfna. ko_at (Notification ntfna) x s \<longrightarrow> (isActive ntfna \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s) \<and> (\<not> isActive ntfna \<longrightarrow> (ntfn = IdleEP \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> x \<noteq> [] \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_ep (case tl x of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x)) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> thread \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> (is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s) \<and> (\<not> is_blocking \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> thread \<noteq> idle_thread s)))))))) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> True)