theory Syscall_AI

lemma (in Systemcall_AI_Pre2) do_reply_invs[wp]:
  "\<lbrace>tcb_at t and tcb_at t' and cte_wp_at (is_reply_cap_to t) slot and
    invs\<rbrace>
     do_reply_transfer t' t slot grant
   \<lbrace>\<lambda>rv. invs :: 'state_ext state \<Rightarrow> _\<rbrace>" apply (simp add: do_reply_transfer_def is_reply_cap_to_def) apply (wp | wpc |simp)+ apply (wp sts_invs_minor) apply (clarsimp) apply (wp cap_delete_one_st_tcb_at) apply (rule_tac Q = "\<lambda>_. invs and if_live_then_nonz_cap and
                                st_tcb_at awaiting_reply t and
                                (\<lambda>s. \<not>has_reply_cap t s)" in
              hoare_strengthen_post[rotated]) apply (clarsimp) apply (rule conjI, erule(1) st_tcb_ex_cap, clarsimp) apply (rule conjI) apply (clarsimp simp add: invs_def valid_state_def valid_idle_def) apply (drule st_tcb_at_eq, erule pred_tcb_weaken_strongerE, simp) apply (clarsimp) apply (rule disjI1) apply (erule pred_tcb_weakenE) apply (clarsimp) apply (rule_tac Q = "\<lambda>_. invs and st_tcb_at awaiting_reply t and
                           (\<lambda>s. \<not>has_reply_cap t s)" in
              hoare_strengthen_post[rotated], clarsimp) apply (wp cap_delete_one_reply_st_tcb_at cap_delete_one_deletes_reply | simp)+ apply (rule_tac Q = "\<lambda>_. valid_reply_caps and
                          cte_wp_at (is_reply_cap_to t) slot" in
             hoare_strengthen_post[rotated], clarsimp) apply (erule cte_wp_at_weakenE, simp) apply (wp) apply (rule do_ipc_transfer_non_null_cte_wp_at2, clarsimp simp add: is_reply_cap_to_def) apply (clarsimp simp: is_cap_simps is_reply_cap_to_def) apply (wp sts_invs_minor | simp split del: if_split)+ apply (wp sts_invs_minor thread_set_no_change_tcb_state) apply (clarsimp) apply (clarsimp) apply (rule conjI) apply (clarsimp) apply (wp thread_set_cap_to thread_set_it |
                  clarsimp simp add: tcb_cap_cases_def)+ apply (rule_tac Q = "\<lambda>_. invs and st_tcb_at awaiting_reply t and
                               (\<lambda>s. \<not>has_reply_cap t s)" in
                  hoare_strengthen_post[rotated]) apply (clarsimp) apply (erule pred_tcb_weakenE) apply (clarsimp) apply (wp thread_set_invs_trivial thread_set_no_change_tcb_state
                     thread_set_has_no_reply_cap | clarsimp simp add: tcb_cap_cases_def)+ apply (rule_tac Q = "\<lambda>_. st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t and invs and
                             st_tcb_at awaiting_reply t and (\<lambda>s. \<not>has_reply_cap t s)" in
                hoare_strengthen_post[rotated]) apply (clarsimp) apply (rule conjI) apply (erule(1) st_tcb_ex_cap'[where P=awaiting_reply]) apply (clarsimp) apply (clarsimp simp add: invs_def valid_state_def valid_idle_def) apply (drule st_tcb_at_eq, erule pred_tcb_weaken_strongerE, simp) apply clarsimp apply (wp handle_fault_reply_has_no_reply_cap) apply (rule_tac Q = "\<lambda>_. st_tcb_at awaiting_reply t and invs and
                         (\<lambda>s. \<not>has_reply_cap t s)" in hoare_strengthen_post[rotated]) apply (clarsimp) apply (erule pred_tcb_weakenE) apply (clarsimp) apply (wp cap_delete_one_deletes_reply cap_delete_one_reply_st_tcb_at)+ apply (clarsimp) apply (wp hoare_drop_imp hoare_allI)[1] apply (wp assert_wp) apply (clarsimp) apply (rule_tac Q = "\<lambda>rv. st_tcb_at ((=) rv) t and tcb_at t' and invs and
                      emptyable slot and
                      cte_wp_at (is_reply_cap_to t) slot" in
         hoare_strengthen_post[rotated]) apply (clarsimp simp add: st_tcb_at_tcb_at) apply (rule conjI, erule pred_tcb_weakenE, clarsimp)+ apply (clarsimp simp add: invs_def valid_state_def valid_pspace_def) apply (rule conjI, erule pred_tcb_weakenE, clarsimp) apply (assumption) apply (wp gts_sp) apply (clarsimp simp add:is_reply_cap_to_def)+ apply (erule emptyable_cte_wp_atD) apply (clarsimp simp add: invs_def valid_state_def is_master_reply_cap_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t and tcb_at t' and cte_wp_at (is_reply_cap_to t) slot and invs\<rbrace> do_reply_transfer t' t slot grant \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs\<rbrace> do state <- get_thread_state t;
y <- assert (awaiting_reply state);
thread_get tcb_fault t >>= case_option (do y <- do_ipc_transfer t' None 0 grant t;
y <- cap_delete_one slot;
y <- set_thread_state t Running;
do_extended_op (possible_switch_to t)
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply f t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od)
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>state. \<lbrace>?B21 state () None () ()\<rbrace> set_thread_state t Running \<lbrace>\<lambda>yc. invs\<rbrace>
 2. \<And>state y x ya. x = None \<Longrightarrow> \<lbrace>?B20 state y x ya\<rbrace> cap_delete_one slot \<lbrace>?B21 state y x ya\<rbrace>
 3. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>?B20 state y x\<rbrace>
 4. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 6. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 8. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>state y x ya. x = None \<Longrightarrow> \<lbrace>?B20 state y x ya\<rbrace> cap_delete_one slot \<lbrace>\<lambda>a. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of Running) t and (\<lambda>s. \<not> halted Running \<longrightarrow> ex_nonz_cap_to t s) and (\<lambda>s. \<forall>a data. Running = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) and (\<lambda>s. t \<noteq> idle_thread s) and (\<lambda>s. st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted Running \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) and (\<lambda>s. \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of Running) and (\<lambda>s. Running \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s) and K (Running \<noteq> IdleThreadState) and invs\<rbrace>
 2. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>?B20 state y x\<rbrace>
 3. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 5. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 6. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 7. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>state. \<lbrace>?B20 state () None ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t b \<and> ex_nonz_cap_to t b \<and> t \<noteq> idle_thread b \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t b \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) b) \<and> \<not> has_reply_cap t b \<and> invs b\<rbrace>
 2. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>?B20 state y x\<rbrace>
 3. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 5. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 6. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 7. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>rv s. ex_nonz_cap_to t s \<and> t \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>
 2. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 3. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 5. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 6. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 7. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>state rv s. (invs and if_live_then_nonz_cap and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)) s \<Longrightarrow> ex_nonz_cap_to t s \<and> t \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> \<not> has_reply_cap t s \<and> invs s
 2. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. invs and if_live_then_nonz_cap and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 4. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 6. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 8. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>s. \<lbrakk>invs s; if_live_then_nonz_cap s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s \<and> t \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s)
 2. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. invs and if_live_then_nonz_cap and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 4. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 6. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 8. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>s. \<lbrakk>invs s; if_live_then_nonz_cap s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s)
 2. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. invs and if_live_then_nonz_cap and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 4. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 6. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 8. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>invs s; if_live_then_nonz_cap s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread s
 2. \<And>s. \<lbrakk>invs s; if_live_then_nonz_cap s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s
 3. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. invs and if_live_then_nonz_cap and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 4. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 5. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 7. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 8. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 9. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>if_live_then_nonz_cap s; st_tcb_at awaiting_reply idle_thread_ptr s; \<not> has_reply_cap idle_thread_ptr s; valid_pspace s; valid_mdb s; valid_ioc s; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s; idle_thread s = idle_thread_ptr; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; t = idle_thread_ptr\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>invs s; if_live_then_nonz_cap s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s
 3. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. invs and if_live_then_nonz_cap and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 4. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 5. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 7. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 8. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 9. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>if_live_then_nonz_cap s; \<not> has_reply_cap idle_thread_ptr s; valid_pspace s; valid_mdb s; valid_ioc s; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s; idle_thread s = idle_thread_ptr; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; t = idle_thread_ptr; idle BlockedOnReply\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>invs s; if_live_then_nonz_cap s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s
 3. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. invs and if_live_then_nonz_cap and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 4. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 5. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 7. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 8. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 9. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>s. \<lbrakk>invs s; if_live_then_nonz_cap s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s
 2. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. invs and if_live_then_nonz_cap and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 4. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 6. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 8. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>s. \<lbrakk>invs s; if_live_then_nonz_cap s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. \<not> halted st) t s
 2. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. invs and if_live_then_nonz_cap and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 4. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 6. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 8. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>s tcb. \<lbrakk>invs s; if_live_then_nonz_cap s; \<not> has_reply_cap t s; awaiting_reply (itcb_state tcb)\<rbrakk> \<Longrightarrow> \<not> halted (itcb_state tcb)
 2. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. invs and if_live_then_nonz_cap and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 4. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 6. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 8. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. invs and if_live_then_nonz_cap and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 2. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 3. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 5. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 6. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 7. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>state. \<lbrace>?P'32 state () (ds_id None) ()\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 2. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t and K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {})) b \<and> ?P'32 state y x a b\<rbrace>
 3. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 5. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 6. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 7. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (6 subgoals):
 1. \<And>state. \<lbrace>?P'128 state () None\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>rv s. cte_wp_at (is_reply_cap_to (?t'127 state () None ())) slot s \<and> cte_wp_at (is_reply_cap_to t) slot s \<and> valid_reply_caps s\<rbrace>
 2. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> ?P'128 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 4. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 5. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 6. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>state s. \<lbrakk>valid_reply_caps s; cte_wp_at (is_reply_cap_to t) slot s\<rbrakk> \<Longrightarrow> cte_wp_at (is_reply_cap_to (?t'127 state () None ())) slot s
 2. \<And>state. \<lbrace>?P'128 state () None\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>_. valid_reply_caps and cte_wp_at (is_reply_cap_to t) slot\<rbrace>
 3. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> ?P'128 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 5. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 6. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 7. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (6 subgoals):
 1. \<And>state. \<lbrace>?P'128 state () None\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>_. valid_reply_caps and cte_wp_at (is_reply_cap_to t) slot\<rbrace>
 2. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> ?P'128 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 4. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 5. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 6. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (6 subgoals):
 1. \<And>state. \<lbrace>?P'141 state () (ds_id None)\<rbrace> do_ipc_transfer t' None 0 grant t \<lbrace>\<lambda>rv. cte_wp_at (is_reply_cap_to t) slot\<rbrace>
 2. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> ?P'141 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 4. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 5. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 6. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (6 subgoals):
 1. \<And>state cap. is_reply_cap_to t cap \<Longrightarrow> \<not> is_untyped_cap cap
 2. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 4. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 5. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 6. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (5 subgoals):
 1. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info t';
buf <- lookup_ipc_buffer False t';
mrs <- get_mrs t' buf mi;
restart <- handle_fault_reply x2 t (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
y <- set_thread_state t (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 3. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 4. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 5. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (10 subgoals):
 1. \<And>state x x2 mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?B169 state () (Some x2) x2 () mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of (if restart then Restart else Inactive)) t s \<and> (\<not> halted (if restart then Restart else Inactive) \<longrightarrow> ex_nonz_cap_to t s) \<and> ((\<exists>a data. (if restart then Restart else Inactive) = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) \<and> t \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted (if restart then Restart else Inactive) \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> (\<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of (if restart then Restart else Inactive)) \<and> ((if restart then Restart else Inactive) \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s) \<and> (if restart then Restart else Inactive) \<noteq> IdleThreadState \<and> invs s\<rbrace>
 2. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B168 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>?B169 state y x x2 ya mi buf mrs\<rbrace>
 3. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 4. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 5. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 6. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 7. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 8. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 9. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 10. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (11 subgoals):
 1. \<And>state x x2 mi buf mrs restart tcb. x = Some x2 \<Longrightarrow> tcb_state (tcb\<lparr>tcb_fault := None\<rparr>) = tcb_state tcb
 2. \<And>state x x2 mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?P'190 state () (Some x2) x2 () mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. (\<not> halted (if restart then Restart else Inactive) \<longrightarrow> ex_nonz_cap_to t s) \<and> ((\<exists>a data. (if restart then Restart else Inactive) = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) \<and> t \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted (if restart then Restart else Inactive) \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> (\<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of (if restart then Restart else Inactive)) \<and> ((if restart then Restart else Inactive) \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s) \<and> (if restart then Restart else Inactive) \<noteq> IdleThreadState \<and> invs s\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B168 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>b. tcb_st_refs_of b = tcb_st_refs_of (if a then Restart else Inactive)) t b \<and> ?P'190 state y x x2 ya mi buf mrs a b\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>state x x2 mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?P'190 state () (Some x2) x2 () mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. (\<not> halted (if restart then Restart else Inactive) \<longrightarrow> ex_nonz_cap_to t s) \<and> ((\<exists>a data. (if restart then Restart else Inactive) = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) \<and> t \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted (if restart then Restart else Inactive) \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> (\<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of (if restart then Restart else Inactive)) \<and> ((if restart then Restart else Inactive) \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s) \<and> (if restart then Restart else Inactive) \<noteq> IdleThreadState \<and> invs s\<rbrace>
 2. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B168 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>b. tcb_st_refs_of b = tcb_st_refs_of (if a then Restart else Inactive)) t b \<and> ?P'190 state y x x2 ya mi buf mrs a b\<rbrace>
 3. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 4. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 5. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 6. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 7. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 8. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 9. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 10. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (10 subgoals):
 1. \<And>state x2 mi buf mrs restart. (restart \<longrightarrow> \<lbrace>?P'190 state () (Some x2) x2 () mi buf mrs True\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. ex_nonz_cap_to t s \<and> t \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>) \<and> (\<not> restart \<longrightarrow> \<lbrace>?P'190 state () (Some x2) x2 () mi buf mrs False\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>)
 2. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B168 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>b. tcb_st_refs_of b = tcb_st_refs_of (if a then Restart else Inactive)) t b \<and> ?P'190 state y x x2 ya mi buf mrs a b\<rbrace>
 3. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 4. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 5. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 6. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 7. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 8. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 9. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 10. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (11 subgoals):
 1. \<And>state x2 mi buf mrs restart. restart \<longrightarrow> \<lbrace>?P'190 state () (Some x2) x2 () mi buf mrs True\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. ex_nonz_cap_to t s \<and> t \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>
 2. \<And>state x2 mi buf mrs restart. \<not> restart \<longrightarrow> \<lbrace>?P'190 state () (Some x2) x2 () mi buf mrs False\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B168 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>b. tcb_st_refs_of b = tcb_st_refs_of (if a then Restart else Inactive)) t b \<and> ?P'190 state y x x2 ya mi buf mrs a b\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state x2 mi buf mrs restart. restart \<Longrightarrow> \<lbrace>?P'190 state () (Some x2) x2 () mi buf mrs True\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. ex_nonz_cap_to t s \<and> t \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>
 2. \<And>state x2 mi buf mrs restart. \<not> restart \<longrightarrow> \<lbrace>?P'190 state () (Some x2) x2 () mi buf mrs False\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B168 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>b. tcb_st_refs_of b = tcb_st_refs_of (if a then Restart else Inactive)) t b \<and> ?P'190 state y x x2 ya mi buf mrs a b\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state x2 mi buf mrs restart. restart \<Longrightarrow> \<lbrace>?P'219 state () (Some x2) x2 () mi buf mrs (ds_id True)\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>
 2. \<And>state x2 mi buf mrs restart. \<not> restart \<longrightarrow> \<lbrace>\<lambda>a. ex_nonz_cap_to t a \<and> t \<noteq> idle_thread a \<and> ?P'219 state () (Some x2) x2 () mi buf mrs False a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B168 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>b. tcb_st_refs_of b = tcb_st_refs_of (if a then Restart else Inactive)) t b \<and> ex_nonz_cap_to t b \<and> t \<noteq> idle_thread b \<and> ?P'219 state y x x2 ya mi buf mrs a b\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>state x2 mi buf mrs restart rv s. \<lbrakk>restart; (invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)) s\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> \<not> has_reply_cap t s \<and> invs s
 2. \<And>state x2 mi buf mrs restart. restart \<Longrightarrow> \<lbrace>?P'219 state () (Some x2) x2 () mi buf mrs (ds_id True)\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state x2 mi buf mrs restart. \<not> restart \<longrightarrow> \<lbrace>\<lambda>a. ex_nonz_cap_to t a \<and> t \<noteq> idle_thread a \<and> ?P'219 state () (Some x2) x2 () mi buf mrs False a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>
 4. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B168 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>b. tcb_st_refs_of b = tcb_st_refs_of (if a then Restart else Inactive)) t b \<and> ex_nonz_cap_to t b \<and> t \<noteq> idle_thread b \<and> ?P'219 state y x x2 ya mi buf mrs a b\<rbrace>
 5. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 6. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 7. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 8. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 9. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 10. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>restart s. \<lbrakk>restart; invs s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s; \<not> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. \<not> halted st) t s
 2. \<And>state x2 mi buf mrs restart. restart \<Longrightarrow> \<lbrace>?P'219 state () (Some x2) x2 () mi buf mrs (ds_id True)\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state x2 mi buf mrs restart. \<not> restart \<longrightarrow> \<lbrace>\<lambda>a. ex_nonz_cap_to t a \<and> t \<noteq> idle_thread a \<and> ?P'219 state () (Some x2) x2 () mi buf mrs False a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>
 4. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B168 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>b. tcb_st_refs_of b = tcb_st_refs_of (if a then Restart else Inactive)) t b \<and> ex_nonz_cap_to t b \<and> t \<noteq> idle_thread b \<and> ?P'219 state y x x2 ya mi buf mrs a b\<rbrace>
 5. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 6. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 7. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 8. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 9. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 10. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>restart s tcb. \<lbrakk>restart; invs s; \<not> has_reply_cap t s; \<not> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; awaiting_reply (itcb_state tcb)\<rbrakk> \<Longrightarrow> \<not> halted (itcb_state tcb)
 2. \<And>state x2 mi buf mrs restart. restart \<Longrightarrow> \<lbrace>?P'219 state () (Some x2) x2 () mi buf mrs (ds_id True)\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state x2 mi buf mrs restart. \<not> restart \<longrightarrow> \<lbrace>\<lambda>a. ex_nonz_cap_to t a \<and> t \<noteq> idle_thread a \<and> ?P'219 state () (Some x2) x2 () mi buf mrs False a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>
 4. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B168 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>b. tcb_st_refs_of b = tcb_st_refs_of (if a then Restart else Inactive)) t b \<and> ex_nonz_cap_to t b \<and> t \<noteq> idle_thread b \<and> ?P'219 state y x x2 ya mi buf mrs a b\<rbrace>
 5. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 6. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 7. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 8. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 9. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 10. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state x2 mi buf mrs restart. restart \<Longrightarrow> \<lbrace>?P'219 state () (Some x2) x2 () mi buf mrs (ds_id True)\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 2. \<And>state x2 mi buf mrs restart. \<not> restart \<longrightarrow> \<lbrace>\<lambda>a. ex_nonz_cap_to t a \<and> t \<noteq> idle_thread a \<and> ?P'219 state () (Some x2) x2 () mi buf mrs False a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B168 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>b. tcb_st_refs_of b = tcb_st_refs_of (if a then Restart else Inactive)) t b \<and> ex_nonz_cap_to t b \<and> t \<noteq> idle_thread b \<and> ?P'219 state y x x2 ya mi buf mrs a b\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>state x2 mi buf mrs. \<lbrace>?B168 state () (Some x2) x2 () mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>b. tcb_st_refs_of b = tcb_st_refs_of (if a then Restart else Inactive)) t b \<and> ex_nonz_cap_to t b \<and> t \<noteq> idle_thread b \<and> invs b \<and> st_tcb_at awaiting_reply t b \<and> \<not> has_reply_cap t b\<rbrace>
 2. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 3. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 4. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 5. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 6. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 7. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 8. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 9. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (10 subgoals):
 1. \<And>state x2 mi buf mrs rv s. (st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t and invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)) s \<Longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = tcb_st_refs_of (if rv then Restart else Inactive)) t s \<and> ex_nonz_cap_to t s \<and> t \<noteq> idle_thread s \<and> invs s \<and> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 2. \<And>state x2 mi buf mrs. \<lbrace>?B168 state () (Some x2) x2 () mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>_. st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t and invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 4. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 5. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 6. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 7. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 8. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 9. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 10. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (10 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t s; invs s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s \<and> t \<noteq> idle_thread s
 2. \<And>state x2 mi buf mrs. \<lbrace>?B168 state () (Some x2) x2 () mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>_. st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t and invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 4. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 5. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 6. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 7. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 8. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 9. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 10. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (11 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t s; invs s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s
 2. \<And>s. \<lbrakk>st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t s; invs s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread s
 3. \<And>state x2 mi buf mrs. \<lbrace>?B168 state () (Some x2) x2 () mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>_. st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t and invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s st. \<lbrakk>st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t s; invs s; \<not> has_reply_cap t s; awaiting_reply st\<rbrakk> \<Longrightarrow> \<not> halted st
 2. \<And>s. \<lbrakk>st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t s; invs s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread s
 3. \<And>state x2 mi buf mrs. \<lbrace>?B168 state () (Some x2) x2 () mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>_. st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t and invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t s; invs s; st_tcb_at awaiting_reply t s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread s
 2. \<And>state x2 mi buf mrs. \<lbrace>?B168 state () (Some x2) x2 () mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>_. st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t and invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 4. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 5. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 6. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 7. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 8. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 9. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 10. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (10 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) idle_thread_ptr s; st_tcb_at awaiting_reply idle_thread_ptr s; \<not> has_reply_cap idle_thread_ptr s; valid_pspace s; valid_mdb s; valid_ioc s; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s; idle_thread s = idle_thread_ptr; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; t = idle_thread_ptr\<rbrakk> \<Longrightarrow> False
 2. \<And>state x2 mi buf mrs. \<lbrace>?B168 state () (Some x2) x2 () mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>_. st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t and invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 4. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 5. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 6. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 7. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 8. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 9. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 10. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (10 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) idle_thread_ptr s; \<not> has_reply_cap idle_thread_ptr s; valid_pspace s; valid_mdb s; valid_ioc s; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s; idle_thread s = idle_thread_ptr; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; t = idle_thread_ptr; idle BlockedOnReply\<rbrakk> \<Longrightarrow> False
 2. \<And>state x2 mi buf mrs. \<lbrace>?B168 state () (Some x2) x2 () mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>_. st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t and invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 4. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 5. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 6. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 7. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 8. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 9. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 10. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>state x2 mi buf mrs. \<lbrace>?B168 state () (Some x2) x2 () mi buf mrs\<rbrace> handle_fault_reply x2 t (mi_label mi) mrs \<lbrace>\<lambda>_. st_tcb_at (\<lambda>s. tcb_st_refs_of s = {}) t and invs and st_tcb_at awaiting_reply t and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 2. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>?B168 state y x x2 ya mi buf\<rbrace>
 3. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 4. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 5. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 6. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 7. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 8. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 9. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>\<lambda>a b. st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t b \<and> invs b \<and> st_tcb_at awaiting_reply t b \<and> \<not> has_reply_cap t b\<rbrace>
 2. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 3. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 4. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 5. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 6. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 8. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>state y x x2 ya mi buf rv s. \<lbrakk>x = Some x2; (st_tcb_at awaiting_reply t and invs and (\<lambda>s. \<not> has_reply_cap t s)) s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> invs s \<and> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 2. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>\<lambda>_. st_tcb_at awaiting_reply t and invs and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 4. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 5. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 6. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 7. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 8. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 9. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at awaiting_reply t s; invs s; \<not> has_reply_cap t s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s
 2. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>\<lambda>_. st_tcb_at awaiting_reply t and invs and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 4. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 5. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 6. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 7. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 8. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 9. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>s tcb. \<lbrakk>invs s; \<not> has_reply_cap t s; awaiting_reply (itcb_state tcb)\<rbrakk> \<Longrightarrow> tcb_st_refs_of (itcb_state tcb) = {}
 2. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>\<lambda>_. st_tcb_at awaiting_reply t and invs and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 3. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 4. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 5. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 6. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 7. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 8. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 9. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B167 state y x x2 ya mi buf\<rbrace> get_mrs t' buf mi \<lbrace>\<lambda>_. st_tcb_at awaiting_reply t and invs and (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 2. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B166 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False t' \<lbrace>?B167 state y x x2 ya mi\<rbrace>
 3. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B165 state y x x2 ya\<rbrace> get_message_info t' \<lbrace>?B166 state y x x2 ya\<rbrace>
 4. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B165 state y x x2\<rbrace>
 5. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 6. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 8. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> K (\<forall>st. active st \<longrightarrow> tcb_st_refs_of st = {}) s \<and> (invs and tcb_at t and tcb_at t') s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> (valid_reply_caps and (valid_reply_masters and valid_objs and valid_mdb)) s \<and> (valid_objs and cte_wp_at (is_reply_cap_to t) slot) s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (st_tcb_at awaiting_reply t and cte_wp_at (is_reply_cap_to (?t'369 state y x xa)) slot) s \<and> (invs and emptyable slot) s \<and> (cte_wp_at (is_reply_cap_to t) slot and valid_reply_caps) s)\<rbrace>
 2. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 3. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 4. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>state. \<lbrace>?B6 state ()\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>x s. (x = None \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> invs s \<and> tcb_at t s \<and> tcb_at t' s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_objs s \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (is_reply_cap_to t) slot s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> st_tcb_at awaiting_reply t s \<and> cte_wp_at (is_reply_cap_to (?t'369 state () (Some xa) xa)) slot s \<and> invs s \<and> emptyable slot s \<and> cte_wp_at (is_reply_cap_to t) slot s \<and> valid_reply_caps s)\<rbrace>
 2. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 3. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 4. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>\<lambda>a b. (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t b \<and> invs b \<and> tcb_at t b \<and> tcb_at t' b \<and> emptyable slot b \<and> st_tcb_at awaiting_reply t b \<and> valid_reply_caps b \<and> valid_reply_masters b \<and> valid_objs b \<and> valid_mdb b \<and> valid_objs b \<and> cte_wp_at (is_reply_cap_to t) slot b) \<and> st_tcb_at awaiting_reply t b \<and> cte_wp_at (is_reply_cap_to (?t'392 state a)) slot b \<and> invs b \<and> emptyable slot b \<and> cte_wp_at (is_reply_cap_to t) slot b \<and> valid_reply_caps b\<rbrace>
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?B5\<rbrace>
 3. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s
flex-flex pairs:
\<lambda>state. ?t'393 state () \<equiv>\<^sup>? \<lambda>state. ?t'392 state () proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. awaiting_reply state \<longrightarrow> (st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> invs s \<and> tcb_at t s \<and> tcb_at t' s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_objs s \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (is_reply_cap_to t) slot s) \<and> st_tcb_at awaiting_reply t s \<and> cte_wp_at (is_reply_cap_to (?t'392 state ())) slot s \<and> invs s \<and> emptyable slot s \<and> cte_wp_at (is_reply_cap_to t) slot s \<and> valid_reply_caps s\<rbrace>
 2. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s
flex-flex pairs:
\<lambda>state. ?t'393 state () \<equiv>\<^sup>? \<lambda>state. ?t'392 state () proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. awaiting_reply state \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> invs s \<and> tcb_at t s \<and> tcb_at t' s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_objs s \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (is_reply_cap_to t) slot s \<and> st_tcb_at awaiting_reply t s \<and> cte_wp_at (is_reply_cap_to (?t'392 BlockedOnReply ())) slot s \<and> invs s \<and> emptyable slot s \<and> cte_wp_at (is_reply_cap_to t) slot s \<and> valid_reply_caps s\<rbrace>
 2. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s
flex-flex pairs:
\<lambda>state. ?t'393 state () \<equiv>\<^sup>? \<lambda>state. ?t'392 state () proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (st_tcb_at ((=) rv) t and tcb_at t' and invs and emptyable slot and cte_wp_at (is_reply_cap_to t) slot) s \<Longrightarrow> awaiting_reply rv \<longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> invs s \<and> tcb_at t s \<and> tcb_at t' s \<and> emptyable slot s \<and> st_tcb_at awaiting_reply t s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_objs s \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (is_reply_cap_to t) slot s \<and> st_tcb_at awaiting_reply t s \<and> cte_wp_at (is_reply_cap_to (?t'392 BlockedOnReply ())) slot s \<and> invs s \<and> emptyable slot s \<and> cte_wp_at (is_reply_cap_to t) slot s \<and> valid_reply_caps s
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) t and tcb_at t' and invs and emptyable slot and cte_wp_at (is_reply_cap_to t) slot\<rbrace>
 3. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s
flex-flex pairs:
\<lambda>state. ?t'393 state () \<equiv>\<^sup>? \<lambda>state. ?t'392 state () proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at ((=) BlockedOnReply) t s; tcb_at t' s; invs s; emptyable slot s; cte_wp_at (is_reply_cap_to t) slot s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>a. tcb_st_refs_of a = {}) t s \<and> st_tcb_at awaiting_reply t s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_objs s \<and> valid_mdb s \<and> valid_objs s \<and> st_tcb_at awaiting_reply t s \<and> cte_wp_at (is_reply_cap_to (?t'392 BlockedOnReply ())) slot s \<and> valid_reply_caps s
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) t and tcb_at t' and invs and emptyable slot and cte_wp_at (is_reply_cap_to t) slot\<rbrace>
 3. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s
flex-flex pairs:
\<lambda>state. ?t'393 state () \<equiv>\<^sup>? \<lambda>state. ?t'392 state () proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at ((=) BlockedOnReply) t s; tcb_at t' s; invs s; emptyable slot s; cte_wp_at (is_reply_cap_to t) slot s\<rbrakk> \<Longrightarrow> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_objs s \<and> valid_mdb s \<and> valid_objs s \<and> st_tcb_at awaiting_reply t s \<and> cte_wp_at (is_reply_cap_to (?t'392 BlockedOnReply ())) slot s \<and> valid_reply_caps s
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) t and tcb_at t' and invs and emptyable slot and cte_wp_at (is_reply_cap_to t) slot\<rbrace>
 3. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s
flex-flex pairs:
\<lambda>state. ?t'393 state () \<equiv>\<^sup>? \<lambda>state. ?t'392 state () proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at ((=) BlockedOnReply) t s; tcb_at t' s; emptyable slot s; cte_wp_at (is_reply_cap_to t) slot s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> st_tcb_at awaiting_reply t s \<and> cte_wp_at (is_reply_cap_to (?t'392 BlockedOnReply ())) slot s
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) t and tcb_at t' and invs and emptyable slot and cte_wp_at (is_reply_cap_to t) slot\<rbrace>
 3. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s
flex-flex pairs:
\<lambda>state. ?t'393 state () \<equiv>\<^sup>? \<lambda>state. ?t'392 state () proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at ((=) BlockedOnReply) t s; tcb_at t' s; emptyable slot s; cte_wp_at (is_reply_cap_to t) slot s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> cte_wp_at (is_reply_cap_to (?t'392 BlockedOnReply ())) slot s
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) t and tcb_at t' and invs and emptyable slot and cte_wp_at (is_reply_cap_to t) slot\<rbrace>
 3. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s
flex-flex pairs:
\<lambda>state. ?t'393 state () \<equiv>\<^sup>? \<lambda>state. ?t'392 state () proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) t and tcb_at t' and invs and emptyable slot and cte_wp_at (is_reply_cap_to t) slot\<rbrace>
 2. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at t and tcb_at t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot and invs) s \<Longrightarrow> tcb_at t' s \<and> invs s \<and> emptyable slot s \<and> cte_wp_at (is_reply_cap_to t) slot s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tcb_at t s; tcb_at t' s; cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) slot s; invs s\<rbrakk> \<Longrightarrow> emptyable slot s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_at t s; tcb_at t' s; invs s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s. \<lbrakk>tcb_at t s; tcb_at t' s; invs s\<rbrakk> \<Longrightarrow> \<forall>cap. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> \<not> is_master_reply_cap cap proof (prove)
goal:
No subgoals!