theory Ipc_DR

lemma do_reply_transfer_corres:
  notes wp_post_taut [wp]
  shows
  "slot' = transform_cslot_ptr slot \<Longrightarrow>
   dcorres dc \<top>
     (invs and tcb_at recver and tcb_at sender
      and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot
      and (\<lambda>s. not_idle_thread (cur_thread s) s)
      and not_idle_thread recver and not_idle_thread sender and valid_etcbs)
     (Endpoint_D.do_reply_transfer sender recver slot' can_grant)
     (Ipc_A.do_reply_transfer sender recver slot can_grant)" apply (clarsimp simp:do_reply_transfer_def Endpoint_D.do_reply_transfer_def) apply (clarsimp simp:get_thread_state_def thread_get_def get_thread_fault_def) apply (rule dcorres_absorb_gets_the) apply (clarsimp simp:assert_def corres_free_fail bind_assoc) apply (frule(1) valid_etcbs_get_tcb_get_etcb) apply (rule dcorres_gets_the[rotated]) apply (clarsimp simp:not_idle_thread_def
     opt_object_tcb transform_tcb_def | intro conjI impI)+ apply (rule corres_guard_imp) apply (rule corres_split) apply (rule corres_complete_ipc_transfer; simp) apply (rule corres_split[OF delete_cap_simple_corres]) apply (rule corres_split_noop_rhs2[OF set_thread_state_corres
                                               possible_switch_to_dcorres[THEN corres_trivial]]) apply (wp | clarsimp simp:not_idle_thread_def)+ apply (clarsimp simp:invs_def valid_state_def valid_pspace_def not_idle_thread_def) apply (case_tac slot,clarsimp simp:cte_wp_at_caps_of_state) apply (drule valid_idle_has_null_cap) apply simp+ apply (clarsimp simp:bind_assoc) apply (rule corres_guard_imp) apply (rule corres_split[OF delete_cap_simple_corres]) apply (rule corres_symb_exec_r) apply (rule corres_symb_exec_r) apply (rule corres_symb_exec_r) apply (rule corres_split[OF dcorres_handle_fault_reply]) apply (rule corres_split[OF thread_set_fault_corres]) apply (simp add: when_return split del: if_split) apply (simp add: dc_def[symmetric] if_distrib[where f = "set_thread_state recver"]
                         split del: if_split) apply (rule corres_split_noop_rhs2) apply (rule corres_if_rhs) apply (rule corres_alternate2) apply (rule set_thread_state_corres) apply (rule corres_alternate1) apply (rule set_thread_state_corres) apply (rule corres_trivial) apply (clarsimp simp: when_def dc_def[symmetric]) apply (rule possible_switch_to_dcorres) apply wp+ apply simp apply clarsimp+ apply (wp wp_post_taut thread_set_no_change_tcb_state
                   hoare_drop_imps thread_set_cur_thread_idle_thread
                   thread_set_valid_idle
                   | simp add:not_idle_thread_def)+ apply (rule_tac Q = "\<lambda>r s. invs s \<and> not_idle_thread recver s \<and> valid_etcbs s
        \<and> tcb_at recver s "
      in  hoare_strengthen_post) apply (clarsimp simp:not_idle_thread_def) apply (wp cap_delete_one_reply_st_tcb_at)+ apply (clarsimp simp:not_idle_thread_def invs_valid_idle st_tcb_at_tcb_at) apply (wp |clarsimp)+ apply (rule conjI) apply (case_tac slot) apply (clarsimp simp:invs_def not_idle_thread_def valid_state_def) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule valid_idle_has_null_cap) apply assumption+ apply (fastforce simp:valid_state_def) apply (rule emptyable_cte_wp_atD) apply (fastforce simp:is_master_reply_cap_def invs_def
                          valid_state_def valid_pspace_def valid_idle_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slot' = transform_cslot_ptr slot \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at recver and tcb_at sender and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot and (\<lambda>s. not_idle_thread (cur_thread s) s) and not_idle_thread recver and not_idle_thread sender and valid_etcbs) (Endpoint_D.do_reply_transfer sender recver slot' can_grant) (Ipc_A.do_reply_transfer sender recver slot can_grant) proof (prove)
goal (1 subgoal):
 1. slot' = transform_cslot_ptr slot \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at recver and tcb_at sender and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot and (\<lambda>s. not_idle_thread (cur_thread s) s) and not_idle_thread recver and not_idle_thread sender and valid_etcbs) (do has_fault <- get_thread_fault recver;
y <- when (\<not> has_fault) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- when has_fault (do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od);
if \<not> has_fault then KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap else KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do state <- get_thread_state recver;
y <- assert (awaiting_reply state);
thread_get tcb_fault recver >>= case_option (do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od)
od) proof (prove)
goal (1 subgoal):
 1. slot' = transform_cslot_ptr slot \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at recver and tcb_at sender and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot and (\<lambda>s. not_idle_thread (cur_thread s) s) and not_idle_thread recver and not_idle_thread sender and valid_etcbs) (do has_fault <- do t <- KHeap_D.get_object recver;
case t of Tcb tcb \<Rightarrow> return (cdl_tcb_has_fault tcb) | _ \<Rightarrow> fail
od;
y <- when (\<not> has_fault) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- when has_fault (do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od);
if \<not> has_fault then KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap else KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do tcb <- gets_the (get_tcb recver);
y <- assert (awaiting_reply (tcb_state tcb));
tcb <- gets_the (get_tcb recver);
case tcb_fault tcb of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>slot' = transform_cslot_ptr slot; (invs and tcb_at recver and tcb_at sender and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot and (\<lambda>s. not_idle_thread (cur_thread s) s) and not_idle_thread recver and not_idle_thread sender and valid_etcbs) s'; get_tcb recver s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do has_fault <- do t <- KHeap_D.get_object recver;
case t of Tcb tcb \<Rightarrow> return (cdl_tcb_has_fault tcb) | _ \<Rightarrow> fail
od;
y <- when (\<not> has_fault) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- when has_fault (do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od);
if \<not> has_fault then KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap else KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do y <- assert (awaiting_reply (tcb_state obj'));
tcb <- gets_the (get_tcb recver);
case tcb_fault tcb of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>slot' = transform_cslot_ptr slot; get_tcb recver s' = Some obj'; invs s'; tcb_at recver s'; tcb_at sender s'; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'; not_idle_thread (cur_thread s') s'; not_idle_thread recver s'; not_idle_thread sender s'; valid_etcbs s'; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do x <- KHeap_D.get_object recver;
has_fault <- case x of Tcb tcb \<Rightarrow> return (cdl_tcb_has_fault tcb) | _ \<Rightarrow> fail;
y <- when (\<not> has_fault) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- when has_fault (do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od);
if \<not> has_fault then KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap else KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do tcb <- gets_the (get_tcb recver);
case tcb_fault tcb of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>slot' = transform_cslot_ptr slot; get_tcb recver s' = Some obj'; invs s'; tcb_at recver s'; tcb_at sender s'; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'; not_idle_thread (cur_thread s') s'; not_idle_thread recver s'; not_idle_thread sender s'; valid_etcbs s'; awaiting_reply (tcb_state obj'); \<exists>etcb. get_etcb recver s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do x <- KHeap_D.get_object recver;
has_fault <- case x of Tcb tcb \<Rightarrow> return (cdl_tcb_has_fault tcb) | _ \<Rightarrow> fail;
y <- when (\<not> has_fault) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- when has_fault (do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od);
if \<not> has_fault then KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap else KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do tcb <- gets_the (get_tcb recver);
case tcb_fault tcb of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od
od) proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' s s'a. \<lbrakk>slot' = transform_cslot_ptr slot; get_tcb recver s' = Some obj'; invs s'; tcb_at recver s'; tcb_at sender s'; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'; not_idle_thread (cur_thread s') s'; not_idle_thread recver s'; not_idle_thread sender s'; valid_etcbs s'; awaiting_reply (tcb_state obj'); \<exists>etcb. get_etcb recver s' = Some etcb; s = transform s'a; transform s' = s; s' = s'a; get_tcb recver s'a \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None
 2. \<And>s' obj' s s'a obj obj'a. \<lbrakk>slot' = transform_cslot_ptr slot; get_tcb recver s' = Some obj'; invs s'; tcb_at recver s'; tcb_at sender s'; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'; not_idle_thread (cur_thread s') s'; not_idle_thread recver s'; not_idle_thread sender s'; valid_etcbs s'; awaiting_reply (tcb_state obj'); \<exists>etcb. get_etcb recver s' = Some etcb; s = transform s'a; transform s' = s; s' = s'a; get_tcb recver s'a = Some obj'a; cdl_objects s recver = Some obj\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s'a) (do has_fault <- case obj of Tcb tcb \<Rightarrow> return (cdl_tcb_has_fault tcb) | _ \<Rightarrow> fail;
y <- when (\<not> has_fault) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- when has_fault (do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od);
if \<not> has_fault then KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap else KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj'a of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (2 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- Endpoint_D.do_ipc_transfer None sender recver can_grant;
y <- delete_cap_simple (transform_cslot_ptr slot);
KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap
od) (do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od)
 2. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; \<exists>y. tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- when (tcb_fault obj' = None) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od;
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj' of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (4 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> dcorres dc (?Q39 obj' s'a etcb) (?Q'39 obj' s'a etcb) (do y <- Endpoint_D.do_ipc_transfer None sender recver can_grant;
y <- delete_cap_simple (transform_cslot_ptr slot);
KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap
od) (do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od)
 2. \<And>obj' s'a etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; transform s'a = s\<rbrakk> \<Longrightarrow> ?Q39 obj' s'a etcb s
 3. \<And>obj' s'a etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; s'a = s\<rbrakk> \<Longrightarrow> ?Q'39 obj' s'a etcb s
 4. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; \<exists>y. tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- when (tcb_fault obj' = None) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od;
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj' of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (7 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> dcorres (?r'43 obj' s'a etcb) (?P43 obj' s'a etcb) (?P'43 obj' s'a etcb) (Endpoint_D.do_ipc_transfer None sender recver can_grant) (Ipc_A.do_ipc_transfer sender None 0 can_grant recver)
 2. \<And>obj' s'a etcb y ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; ?r'43 obj' s'a etcb y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R43 obj' s'a etcb y) (?R'43 obj' s'a etcb ya) (do y <- delete_cap_simple (transform_cslot_ptr slot);
KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap
od) (do y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od)
 3. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 obj' s'a etcb\<rbrace> Endpoint_D.do_ipc_transfer None sender recver can_grant \<lbrace>?R43 obj' s'a etcb\<rbrace>
 4. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 obj' s'a etcb\<rbrace> Ipc_A.do_ipc_transfer sender None 0 can_grant recver \<lbrace>?R'43 obj' s'a etcb\<rbrace>
 5. \<And>obj' s'a etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; transform s'a = s\<rbrakk> \<Longrightarrow> (?P43 obj' s'a etcb and ?Q43 obj' s'a etcb) s
 6. \<And>obj' s'a etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; s'a = s\<rbrakk> \<Longrightarrow> (?P'43 obj' s'a etcb and ?Q'43 obj' s'a etcb) s
 7. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; \<exists>y. tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- when (tcb_fault obj' = None) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od;
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj' of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (6 subgoals):
 1. \<And>obj' s'a etcb y ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R43 obj' s'a etcb y) (?R'43 obj' s'a etcb ya) (do y <- delete_cap_simple (transform_cslot_ptr slot);
KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap
od) (do y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od)
 2. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 obj' s'a etcb\<rbrace> Endpoint_D.do_ipc_transfer None sender recver can_grant \<lbrace>?R43 obj' s'a etcb\<rbrace>
 3. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 obj' s'a etcb\<rbrace> Ipc_A.do_ipc_transfer sender None 0 can_grant recver \<lbrace>?R'43 obj' s'a etcb\<rbrace>
 4. \<And>obj' s'a etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 obj' s'a etcb) s
 5. \<And>obj' s'a etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; s'a = s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and valid_global_refs and pspace_distinct and valid_mdb and (\<lambda>s. not_idle_thread (cur_thread s) s) and valid_irq_node and valid_idle and not_idle_thread recver and not_idle_thread sender and valid_etcbs and ?Q'43 obj' s'a etcb) s
 6. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; \<exists>y. tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- when (tcb_fault obj' = None) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od;
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj' of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (8 subgoals):
 1. \<And>obj' s'a etcb y ya yb yc. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R54 obj' s'a etcb y ya yb) (?R'54 obj' s'a etcb y ya yc) (KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap) (do y <- set_thread_state recver Running;
possible_switch_to recver
od)
 2. \<And>obj' s'a etcb y ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 obj' s'a etcb y\<rbrace> delete_cap_simple (transform_cslot_ptr slot) \<lbrace>?R54 obj' s'a etcb y ya\<rbrace>
 3. \<And>obj' s'a etcb y ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'58 obj' s'a etcb ya\<rbrace> cap_delete_one slot \<lbrace>?R'54 obj' s'a etcb y ya\<rbrace>
 4. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 obj' s'a etcb\<rbrace> Endpoint_D.do_ipc_transfer None sender recver can_grant \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q56 obj' s'a etcb y\<rbrace>
 5. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 obj' s'a etcb\<rbrace> Ipc_A.do_ipc_transfer sender None 0 can_grant recver \<lbrace>\<lambda>ya. invs and not_idle_thread (fst slot) and valid_etcbs and ?Q'58 obj' s'a etcb ya\<rbrace>
 6. \<And>obj' s'a etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 obj' s'a etcb) s
 7. \<And>obj' s'a etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; s'a = s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and valid_global_refs and pspace_distinct and valid_mdb and (\<lambda>s. not_idle_thread (cur_thread s) s) and valid_irq_node and valid_idle and not_idle_thread recver and not_idle_thread sender and valid_etcbs and ?Q'43 obj' s'a etcb) s
 8. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; \<exists>y. tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- when (tcb_fault obj' = None) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od;
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj' of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (9 subgoals):
 1. \<And>obj' s'a etcb y ya yb yc. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q66 obj' s'a etcb y ya yb\<rbrace> KHeap_D.set_cap (recver, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>obj' s'a etcb y ya yb yc. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'71 obj' s'a etcb y ya yc\<rbrace> set_thread_state recver Running \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>obj' s'a etcb y ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 obj' s'a etcb y\<rbrace> delete_cap_simple (transform_cslot_ptr slot) \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q66 obj' s'a etcb y ya yb\<rbrace>
 4. \<And>obj' s'a etcb y ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'58 obj' s'a etcb ya\<rbrace> cap_delete_one slot \<lbrace>\<lambda>yc. not_idle_thread recver and K (RunningCap = infer_tcb_pending_op recver Running) and valid_etcbs and ?Q'71 obj' s'a etcb y ya yc\<rbrace>
 5. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 obj' s'a etcb\<rbrace> Endpoint_D.do_ipc_transfer None sender recver can_grant \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q56 obj' s'a etcb y\<rbrace>
 6. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 obj' s'a etcb\<rbrace> Ipc_A.do_ipc_transfer sender None 0 can_grant recver \<lbrace>\<lambda>ya. invs and not_idle_thread (fst slot) and valid_etcbs and ?Q'58 obj' s'a etcb ya\<rbrace>
 7. \<And>obj' s'a etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 obj' s'a etcb) s
 8. \<And>obj' s'a etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = None; s'a = s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_aligned and valid_global_refs and pspace_distinct and valid_mdb and (\<lambda>s. not_idle_thread (cur_thread s) s) and valid_irq_node and valid_idle and not_idle_thread recver and not_idle_thread sender and valid_etcbs and ?Q'43 obj' s'a etcb) s
 9. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; \<exists>y. tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- when (tcb_fault obj' = None) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od;
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj' of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (2 subgoals):
 1. \<And>obj' etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = None\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_aligned s \<and> valid_global_refs s \<and> pspace_distinct s \<and> valid_mdb s \<and> valid_irq_node s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s
 2. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; \<exists>y. tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- when (tcb_fault obj' = None) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od;
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj' of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (2 subgoals):
 1. \<And>obj' etcb s. \<lbrakk>slot' = transform_cslot_ptr slot; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = None; 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_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; fst slot = idle_thread s\<rbrakk> \<Longrightarrow> False
 2. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; \<exists>y. tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- when (tcb_fault obj' = None) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od;
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj' of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (2 subgoals):
 1. \<And>obj' etcb s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = None; 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_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; slot = (idle_thread s, b); caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; \<exists>y. tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- when (tcb_fault obj' = None) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od;
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj' of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (6 subgoals):
 1. \<And>obj' etcb s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = None; 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; 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_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; slot = (idle_thread s, b); caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R)\<rbrakk> \<Longrightarrow> valid_global_refs s
 2. \<And>obj' etcb s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = None; 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; 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_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; slot = (idle_thread s, b); caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R)\<rbrakk> \<Longrightarrow> valid_idle s
 3. \<And>obj' etcb s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = None; 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; 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_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; slot = (idle_thread s, b); caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R)\<rbrakk> \<Longrightarrow> valid_irq_node s
 4. \<And>obj' etcb s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = None; 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; 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_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; slot = (idle_thread s, b); caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R)\<rbrakk> \<Longrightarrow> caps_of_state s (idle_thread s, ?v173 obj' etcb s b R) = Some (?cap173 obj' etcb s b R)
 5. \<And>obj' etcb s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = None; 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; 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_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; slot = (idle_thread s, b); caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R); ?cap173 obj' etcb s b R = cap.NullCap\<rbrakk> \<Longrightarrow> False
 6. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; \<exists>y. tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- when (tcb_fault obj' = None) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od;
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj' of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (1 subgoal):
 1. \<And>obj' s'a etcb. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; \<exists>y. tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- when (tcb_fault obj' = None) (Endpoint_D.do_ipc_transfer None sender recver can_grant);
y <- delete_cap_simple (transform_cslot_ptr slot);
y <- do y <- corrupt_tcb_intent recver;
update_thread_fault recver (\<lambda>_. False)
od;
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (case tcb_fault obj' of None \<Rightarrow> do y <- Ipc_A.do_ipc_transfer sender None 0 can_grant recver;
y <- cap_delete_one slot;
y <- set_thread_state recver Running;
possible_switch_to recver
od | Some f \<Rightarrow> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (1 subgoal):
 1. \<And>obj' s'a etcb y. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- delete_cap_simple (transform_cslot_ptr slot);
x <- corrupt_tcb_intent recver;
y <- update_thread_fault recver (\<lambda>_. False);
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do ya <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply y recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od) proof (prove)
goal (3 subgoals):
 1. \<And>obj' s'a etcb y. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc (?Q180 obj' s'a etcb y) (?Q'180 obj' s'a etcb y) (do y <- delete_cap_simple (transform_cslot_ptr slot);
x <- corrupt_tcb_intent recver;
y <- update_thread_fault recver (\<lambda>_. False);
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do ya <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply y recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od)
 2. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; transform s'a = s\<rbrakk> \<Longrightarrow> ?Q180 obj' s'a etcb y s
 3. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; s'a = s\<rbrakk> \<Longrightarrow> ?Q'180 obj' s'a etcb y s proof (prove)
goal (5 subgoals):
 1. \<And>obj' s'a etcb y rv ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> dcorres dc (?R184 obj' s'a etcb y rv) (?R'184 obj' s'a etcb y ya) (do x <- corrupt_tcb_intent recver;
y <- update_thread_fault recver (\<lambda>_. False);
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply y recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od)
 2. \<And>obj' s'a etcb y. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q184 obj' s'a etcb y\<rbrace> delete_cap_simple (transform_cslot_ptr slot) \<lbrace>?R184 obj' s'a etcb y\<rbrace>
 3. \<And>obj' s'a etcb y. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'184 obj' s'a etcb y\<rbrace> cap_delete_one slot \<lbrace>?R'184 obj' s'a etcb y\<rbrace>
 4. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q184 obj' s'a etcb y) s
 5. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; s'a = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst slot) and valid_etcbs and ?Q'184 obj' s'a etcb y) s proof (prove)
goal (8 subgoals):
 1. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> dcorres dc (?R184 obj' s'a etcb y rv) (?Q'189 obj' s'a etcb y rv ya mi) (do x <- corrupt_tcb_intent recver;
y <- update_thread_fault recver (\<lambda>_. False);
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply y recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od)
 2. \<And>obj' s'a etcb y rv ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?R'184 obj' s'a etcb y ya\<rbrace> get_message_info sender \<lbrace>?Q'189 obj' s'a etcb y rv ya\<rbrace>
 3. \<And>obj' s'a etcb y rv ya s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?R'184 obj' s'a etcb y ya s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_message_info sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>obj' s'a etcb y rv ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?R'184 obj' s'a etcb y ya) (get_message_info sender)
 5. \<And>obj' s'a etcb y. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q184 obj' s'a etcb y\<rbrace> delete_cap_simple (transform_cslot_ptr slot) \<lbrace>?R184 obj' s'a etcb y\<rbrace>
 6. \<And>obj' s'a etcb y. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'184 obj' s'a etcb y\<rbrace> cap_delete_one slot \<lbrace>?R'184 obj' s'a etcb y\<rbrace>
 7. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q184 obj' s'a etcb y) s
 8. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; s'a = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst slot) and valid_etcbs and ?Q'184 obj' s'a etcb y) s proof (prove)
goal (11 subgoals):
 1. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> dcorres dc (?R184 obj' s'a etcb y rv) (?Q'194 obj' s'a etcb y rv ya mi buf) (do x <- corrupt_tcb_intent recver;
y <- update_thread_fault recver (\<lambda>_. False);
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply y recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od)
 2. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'189 obj' s'a etcb y rv ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?Q'194 obj' s'a etcb y rv ya mi\<rbrace>
 3. \<And>obj' s'a etcb y rv ya mi s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'189 obj' s'a etcb y rv ya mi s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookup_ipc_buffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'189 obj' s'a etcb y rv ya mi) (lookup_ipc_buffer False sender)
 5. \<And>obj' s'a etcb y rv ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?R'184 obj' s'a etcb y ya\<rbrace> get_message_info sender \<lbrace>?Q'189 obj' s'a etcb y rv ya\<rbrace>
 6. \<And>obj' s'a etcb y rv ya s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?R'184 obj' s'a etcb y ya s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_message_info sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>obj' s'a etcb y rv ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?R'184 obj' s'a etcb y ya) (get_message_info sender)
 8. \<And>obj' s'a etcb y. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q184 obj' s'a etcb y\<rbrace> delete_cap_simple (transform_cslot_ptr slot) \<lbrace>?R184 obj' s'a etcb y\<rbrace>
 9. \<And>obj' s'a etcb y. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'184 obj' s'a etcb y\<rbrace> cap_delete_one slot \<lbrace>?R'184 obj' s'a etcb y\<rbrace>
 10. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q184 obj' s'a etcb y) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> dcorres dc (?R184 obj' s'a etcb y rv) (?Q'199 obj' s'a etcb y rv ya mi buf mrs) (do x <- corrupt_tcb_intent recver;
y <- update_thread_fault recver (\<lambda>_. False);
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do restart <- handle_fault_reply y recver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od)
 2. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?Q'199 obj' s'a etcb y rv ya mi buf\<rbrace>
 3. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
 5. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'189 obj' s'a etcb y rv ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?Q'194 obj' s'a etcb y rv ya mi\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'189 obj' s'a etcb y rv ya mi s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookup_ipc_buffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'189 obj' s'a etcb y rv ya mi) (lookup_ipc_buffer False sender)
 8. \<And>obj' s'a etcb y rv ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?R'184 obj' s'a etcb y ya\<rbrace> get_message_info sender \<lbrace>?Q'189 obj' s'a etcb y rv ya\<rbrace>
 9. \<And>obj' s'a etcb y rv ya s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?R'184 obj' s'a etcb y ya s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_message_info sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<And>obj' s'a etcb y rv ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?R'184 obj' s'a etcb y ya) (get_message_info sender)
A total of 14 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> dcorres dc (?R204 obj' s'a etcb y rv ya mi buf mrs x) (?R'204 obj' s'a etcb y rv ya mi buf mrs restart) (do y <- update_thread_fault recver (\<lambda>_. False);
KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. None)) recver;
y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od)
 2. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>?R204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 3. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>?R'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
 7. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'189 obj' s'a etcb y rv ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?Q'194 obj' s'a etcb y rv ya mi\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'189 obj' s'a etcb y rv ya mi s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookup_ipc_buffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'189 obj' s'a etcb y rv ya mi) (lookup_ipc_buffer False sender)
 10. \<And>obj' s'a etcb y rv ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?R'184 obj' s'a etcb y ya\<rbrace> get_message_info sender \<lbrace>?Q'189 obj' s'a etcb y rv ya\<rbrace>
A total of 16 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>obj' s'a etcb y rv ya mi buf mrs x restart t. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> False = (case None of None \<Rightarrow> False | Some a \<Rightarrow> True)
 2. \<And>obj' s'a etcb y rv ya mi buf mrs x restart yb yc. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R210 obj' s'a etcb y rv ya mi buf mrs x restart yb) (?R'210 obj' s'a etcb y rv ya mi buf mrs x restart yc) (KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap) (do y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od)
 3. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>?R210 obj' s'a etcb y rv ya mi buf mrs x restart\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>?R'210 obj' s'a etcb y rv ya mi buf mrs x restart\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
 10. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'189 obj' s'a etcb y rv ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?Q'194 obj' s'a etcb y rv ya mi\<rbrace>
A total of 19 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>obj' s'a etcb y rv ya mi buf mrs x restart yb yc. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R210 obj' s'a etcb y rv ya mi buf mrs x restart yb) (?R'210 obj' s'a etcb y rv ya mi buf mrs x restart yc) (KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap) (do y <- set_thread_state recver (if restart then Restart else Inactive);
when restart (possible_switch_to recver)
od)
 2. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>?R210 obj' s'a etcb y rv ya mi buf mrs x restart\<rbrace>
 3. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>?R'210 obj' s'a etcb y rv ya mi buf mrs x restart\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
 9. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'189 obj' s'a etcb y rv ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?Q'194 obj' s'a etcb y rv ya mi\<rbrace>
 10. \<And>obj' s'a etcb y rv ya mi s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'189 obj' s'a etcb y rv ya mi s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookup_ipc_buffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc (?R210 obj' s'a etcb y () () mi buf mrs () restart ()) (?R'210 obj' s'a etcb y () () mi buf mrs () restart ()) (KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap) (do y <- if restart then set_thread_state recver Restart else set_thread_state recver Inactive;
when restart (possible_switch_to recver)
od)
 2. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>?R210 obj' s'a etcb y rv ya mi buf mrs x restart\<rbrace>
 3. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>?R'210 obj' s'a etcb y rv ya mi buf mrs x restart\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
 9. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'189 obj' s'a etcb y rv ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?Q'194 obj' s'a etcb y rv ya mi\<rbrace>
 10. \<And>obj' s'a etcb y rv ya mi s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'189 obj' s'a etcb y rv ya mi s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookup_ipc_buffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
A total of 18 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc (?P228 obj' s'a etcb y () () mi buf mrs () restart ()) (?P'226 obj' s'a etcb y () () mi buf mrs () restart ()) (KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap) (if restart then set_thread_state recver Restart else set_thread_state recver Inactive)
 2. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc (?R220 obj' s'a etcb y mi buf mrs restart) (?R'220 obj' s'a etcb y mi buf mrs restart) (return ()) (when restart (possible_switch_to recver))
 3. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q227 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>x. ?R220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 4. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'225 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> if restart then set_thread_state recver Restart else set_thread_state recver Inactive \<lbrace>\<lambda>x. ?R'220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>\<lambda>a. ?P228 obj' s'a etcb y rv ya mi buf mrs x restart a and ?Q227 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a. ?P'226 obj' s'a etcb y rv ya mi buf mrs x restart a and ?Q'225 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 10. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
A total of 21 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; restart\<rbrakk> \<Longrightarrow> dcorres dc (?P237 obj' s'a etcb y () () mi buf mrs () restart ()) (?Q235 obj' s'a etcb y () () mi buf mrs () restart ()) (KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap) (set_thread_state recver Restart)
 2. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; \<not> restart\<rbrakk> \<Longrightarrow> dcorres dc (?P'236 obj' s'a etcb y () () mi buf mrs () restart ()) (?Q'234 obj' s'a etcb y () () mi buf mrs () restart ()) (KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap) (set_thread_state recver Inactive)
 3. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc (?R220 obj' s'a etcb y mi buf mrs restart) (?R'220 obj' s'a etcb y mi buf mrs restart) (return ()) (when restart (possible_switch_to recver))
 4. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q227 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>x. ?R220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 5. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'225 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> if restart then set_thread_state recver Restart else set_thread_state recver Inactive \<lbrace>\<lambda>x. ?R'220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>\<lambda>a. (\<lambda>b. (restart \<longrightarrow> ?P237 obj' s'a etcb y rv ya mi buf mrs x restart a b) \<and> (\<not> restart \<longrightarrow> ?P'236 obj' s'a etcb y rv ya mi buf mrs x restart a b)) and ?Q227 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a. (\<lambda>b. (restart \<longrightarrow> ?Q235 obj' s'a etcb y rv ya mi buf mrs x restart a b) \<and> (\<not> restart \<longrightarrow> ?Q'234 obj' s'a etcb y rv ya mi buf mrs x restart a b)) and ?Q'225 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 10. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
A total of 22 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; restart\<rbrakk> \<Longrightarrow> dcorres dc (?P237 obj' s'a etcb y () () mi buf mrs () restart ()) (?Q235 obj' s'a etcb y () () mi buf mrs () restart ()) (KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap) (set_thread_state recver Restart)
 2. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; \<not> restart\<rbrakk> \<Longrightarrow> dcorres dc (?P'236 obj' s'a etcb y () () mi buf mrs () restart ()) (?Q'234 obj' s'a etcb y () () mi buf mrs () restart ()) (KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap) (set_thread_state recver Inactive)
 3. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc (?R220 obj' s'a etcb y mi buf mrs restart) (?R'220 obj' s'a etcb y mi buf mrs restart) (return ()) (when restart (possible_switch_to recver))
 4. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q227 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>x. ?R220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 5. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'225 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> if restart then set_thread_state recver Restart else set_thread_state recver Inactive \<lbrace>\<lambda>x. ?R'220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>\<lambda>a. (\<lambda>b. (restart \<longrightarrow> ?P237 obj' s'a etcb y rv ya mi buf mrs x restart a b) \<and> (\<not> restart \<longrightarrow> ?P'236 obj' s'a etcb y rv ya mi buf mrs x restart a b)) and ?Q227 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a. (\<lambda>b. (restart \<longrightarrow> ?Q235 obj' s'a etcb y rv ya mi buf mrs x restart a b) \<and> (\<not> restart \<longrightarrow> ?Q'234 obj' s'a etcb y rv ya mi buf mrs x restart a b)) and ?Q'225 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 10. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
A total of 22 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; \<not> restart\<rbrakk> \<Longrightarrow> dcorres dc (?P'236 obj' s'a etcb y () () mi buf mrs () restart ()) (?Q'234 obj' s'a etcb y () () mi buf mrs () restart ()) (KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap) (set_thread_state recver Inactive)
 2. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc (?R220 obj' s'a etcb y mi buf mrs restart) (?R'220 obj' s'a etcb y mi buf mrs restart) (return ()) (when restart (possible_switch_to recver))
 3. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q227 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>x. ?R220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 4. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'225 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> if restart then set_thread_state recver Restart else set_thread_state recver Inactive \<lbrace>\<lambda>x. ?R'220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>\<lambda>a. (\<lambda>b. (restart \<longrightarrow> True) \<and> (\<not> restart \<longrightarrow> ?P'236 obj' s'a etcb y rv ya mi buf mrs x restart a b)) and ?Q227 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a. (\<lambda>b. (restart \<longrightarrow> (not_idle_thread recver and K (RestartCap = infer_tcb_pending_op recver Restart) and valid_etcbs) b) \<and> (\<not> restart \<longrightarrow> ?Q'234 obj' s'a etcb y rv ya mi buf mrs x restart a b)) and ?Q'225 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 10. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
A total of 21 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; \<not> restart\<rbrakk> \<Longrightarrow> dcorres dc (?P'236 obj' s'a etcb y () () mi buf mrs () restart ()) (?Q'234 obj' s'a etcb y () () mi buf mrs () restart ()) (KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap) (set_thread_state recver Inactive)
 2. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc (?R220 obj' s'a etcb y mi buf mrs restart) (?R'220 obj' s'a etcb y mi buf mrs restart) (return ()) (when restart (possible_switch_to recver))
 3. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q227 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>x. ?R220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 4. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'225 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> if restart then set_thread_state recver Restart else set_thread_state recver Inactive \<lbrace>\<lambda>x. ?R'220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>\<lambda>a. (\<lambda>b. (restart \<longrightarrow> True) \<and> (\<not> restart \<longrightarrow> ?P'236 obj' s'a etcb y rv ya mi buf mrs x restart a b)) and ?Q227 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a. (\<lambda>b. (restart \<longrightarrow> (not_idle_thread recver and K (RestartCap = infer_tcb_pending_op recver Restart) and valid_etcbs) b) \<and> (\<not> restart \<longrightarrow> ?Q'234 obj' s'a etcb y rv ya mi buf mrs x restart a b)) and ?Q'225 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 10. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
A total of 21 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc (?R220 obj' s'a etcb y mi buf mrs restart) (?R'220 obj' s'a etcb y mi buf mrs restart) (return ()) (when restart (possible_switch_to recver))
 2. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q227 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>x. ?R220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 3. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'225 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> if restart then set_thread_state recver Restart else set_thread_state recver Inactive \<lbrace>\<lambda>x. ?R'220 obj' s'a etcb y mi buf mrs restart\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>\<lambda>a. (\<lambda>a. (restart \<longrightarrow> True) \<and> (\<not> restart \<longrightarrow> True)) and ?Q227 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a. (\<lambda>a. (restart \<longrightarrow> (not_idle_thread recver and K (RestartCap = infer_tcb_pending_op recver Restart) and valid_etcbs) a) \<and> (\<not> restart \<longrightarrow> (not_idle_thread recver and K (cdl_cap.NullCap = infer_tcb_pending_op recver Inactive) and valid_etcbs) a)) and ?Q'225 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
A total of 20 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (when restart (possible_switch_to recver))
 2. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q227 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'225 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> if restart then set_thread_state recver Restart else set_thread_state recver Inactive \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>\<lambda>a. (\<lambda>a. (restart \<longrightarrow> True) \<and> (\<not> restart \<longrightarrow> True)) and ?Q227 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a. (\<lambda>a. (restart \<longrightarrow> (not_idle_thread recver and K (RestartCap = infer_tcb_pending_op recver Restart) and valid_etcbs) a) \<and> (\<not> restart \<longrightarrow> (not_idle_thread recver and K (cdl_cap.NullCap = infer_tcb_pending_op recver Inactive) and valid_etcbs) a)) and ?Q'225 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
A total of 20 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>obj' s'a etcb y restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; restart\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (possible_switch_to recver)
 2. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q227 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'225 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> if restart then set_thread_state recver Restart else set_thread_state recver Inactive \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>\<lambda>a. (\<lambda>a. (restart \<longrightarrow> True) \<and> (\<not> restart \<longrightarrow> True)) and ?Q227 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a. (\<lambda>a. (restart \<longrightarrow> (not_idle_thread recver and K (RestartCap = infer_tcb_pending_op recver Restart) and valid_etcbs) a) \<and> (\<not> restart \<longrightarrow> (not_idle_thread recver and K (cdl_cap.NullCap = infer_tcb_pending_op recver Inactive) and valid_etcbs) a)) and ?Q'225 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
A total of 20 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q227 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> KHeap_D.set_cap (recver, tcb_pending_op_slot) cdl_cap.NullCap \<sqinter> KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'225 obj' s'a etcb y () () mi buf mrs () restart ()\<rbrace> if restart then set_thread_state recver Restart else set_thread_state recver Inactive \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace> update_thread_fault recver (\<lambda>_. False) \<lbrace>\<lambda>a. (\<lambda>a. (restart \<longrightarrow> True) \<and> (\<not> restart \<longrightarrow> True)) and ?Q227 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a. (\<lambda>a. (restart \<longrightarrow> (not_idle_thread recver and K (RestartCap = infer_tcb_pending_op recver Restart) and valid_etcbs) a) \<and> (\<not> restart \<longrightarrow> (not_idle_thread recver and K (cdl_cap.NullCap = infer_tcb_pending_op recver Inactive) and valid_etcbs) a)) and ?Q'225 obj' s'a etcb y rv ya mi buf mrs x restart a\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
 10. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'189 obj' s'a etcb y rv ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?Q'194 obj' s'a etcb y rv ya mi\<rbrace>
A total of 19 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>obj' s'a etcb y rv ya mi buf mrs x restart s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart; ?Q212 obj' s'a etcb y rv ya mi buf mrs x s\<rbrakk> \<Longrightarrow> (restart \<longrightarrow> True) \<and> (\<not> restart \<longrightarrow> True)
 2. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a. (\<lambda>a. (restart \<longrightarrow> (not_idle_thread recver and K (RestartCap = infer_tcb_pending_op recver Restart) and valid_etcbs) a) \<and> (\<not> restart \<longrightarrow> (not_idle_thread recver and K (cdl_cap.NullCap = infer_tcb_pending_op recver Inactive) and valid_etcbs) a)) and (\<lambda>a. True)\<rbrace>
 3. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
 8. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'189 obj' s'a etcb y rv ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?Q'194 obj' s'a etcb y rv ya mi\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'189 obj' s'a etcb y rv ya mi s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookup_ipc_buffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'189 obj' s'a etcb y rv ya mi) (lookup_ipc_buffer False sender)
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>obj' s'a etcb y rv ya mi buf mrs x restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; dc x restart\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a. (\<lambda>a. (restart \<longrightarrow> (not_idle_thread recver and K (RestartCap = infer_tcb_pending_op recver Restart) and valid_etcbs) a) \<and> (\<not> restart \<longrightarrow> (not_idle_thread recver and K (cdl_cap.NullCap = infer_tcb_pending_op recver Inactive) and valid_etcbs) a)) and (\<lambda>a. True)\<rbrace>
 2. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 3. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
 7. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'189 obj' s'a etcb y rv ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?Q'194 obj' s'a etcb y rv ya mi\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'189 obj' s'a etcb y rv ya mi s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookup_ipc_buffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'189 obj' s'a etcb y rv ya mi) (lookup_ipc_buffer False sender)
 10. \<And>obj' s'a etcb y rv ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?R'184 obj' s'a etcb y ya\<rbrace> get_message_info sender \<lbrace>?Q'189 obj' s'a etcb y rv ya\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>obj' s'a etcb y mi buf mrs restart. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'215 obj' s'a etcb y () () mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) recver \<lbrace>\<lambda>a b. not_idle_thread recver b \<and> valid_etcbs b\<rbrace>
 2. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q206 obj' s'a etcb y rv\<rbrace> corrupt_tcb_intent recver \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q212 obj' s'a etcb y rv ya mi buf mrs x\<rbrace>
 3. \<And>obj' s'a etcb y rv ya mi buf mrs. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace> handle_fault_reply y recver (mi_label mi) mrs \<lbrace>\<lambda>restart. tcb_at recver and not_idle_thread recver and valid_etcbs and ?Q'215 obj' s'a etcb y rv ya mi buf mrs restart\<rbrace>
 4. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'194 obj' s'a etcb y rv ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>mrs. tcb_at recver and valid_idle and not_idle_thread recver and valid_etcbs and ?Q'204 obj' s'a etcb y rv ya mi buf mrs\<rbrace>
 5. \<And>obj' s'a etcb y rv ya mi buf s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'194 obj' s'a etcb y rv ya mi buf s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs sender buf mi \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>obj' s'a etcb y rv ya mi buf. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'194 obj' s'a etcb y rv ya mi buf) (get_mrs sender buf mi)
 7. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'189 obj' s'a etcb y rv ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?Q'194 obj' s'a etcb y rv ya mi\<rbrace>
 8. \<And>obj' s'a etcb y rv ya mi s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; ?Q'189 obj' s'a etcb y rv ya mi s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookup_ipc_buffer False sender \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>obj' s'a etcb y rv ya mi. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya; False\<rbrakk> \<Longrightarrow> no_fail (?Q'189 obj' s'a etcb y rv ya mi) (lookup_ipc_buffer False sender)
 10. \<And>obj' s'a etcb y rv ya. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; dc rv ya\<rbrakk> \<Longrightarrow> \<lbrace>?R'184 obj' s'a etcb y ya\<rbrace> get_message_info sender \<lbrace>?Q'189 obj' s'a etcb y rv ya\<rbrace>
A total of 16 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>obj' s'a etcb y. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?P'342 obj' s'a etcb y\<rbrace> cap_delete_one slot \<lbrace>\<lambda>rv s. valid_idle s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s \<and> tcb_at recver s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s\<rbrace>
 2. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) s
 3. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; s'a = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst slot) and valid_etcbs and (\<lambda>s. tcb_at recver s \<and> ?P'342 obj' s'a etcb y s)) s proof (prove)
goal (4 subgoals):
 1. \<And>obj' s'a etcb y. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?P'342 obj' s'a etcb y\<rbrace> cap_delete_one slot \<lbrace>\<lambda>r s. invs s \<and> not_idle_thread recver s \<and> valid_etcbs s \<and> tcb_at recver s\<rbrace>
 2. \<And>obj' s'a etcb y rv s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; invs s \<and> not_idle_thread recver s \<and> valid_etcbs s \<and> tcb_at recver s\<rbrakk> \<Longrightarrow> valid_idle s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s \<and> tcb_at recver s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s
 3. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) s
 4. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; s'a = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst slot) and valid_etcbs and (\<lambda>s. tcb_at recver s \<and> ?P'342 obj' s'a etcb y s)) s proof (prove)
goal (4 subgoals):
 1. \<And>obj' s'a etcb y. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?P'342 obj' s'a etcb y\<rbrace> cap_delete_one slot \<lbrace>\<lambda>r s. invs s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s \<and> tcb_at recver s\<rbrace>
 2. \<And>obj' s'a etcb y rv s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; invs s \<and> not_idle_thread recver s \<and> valid_etcbs s \<and> tcb_at recver s\<rbrakk> \<Longrightarrow> valid_idle s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s \<and> tcb_at recver s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s
 3. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) s
 4. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; s'a = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst slot) and valid_etcbs and (\<lambda>s. tcb_at recver s \<and> ?P'342 obj' s'a etcb y s)) s proof (prove)
goal (3 subgoals):
 1. \<And>obj' s'a etcb y rv s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; invs s \<and> not_idle_thread recver s \<and> valid_etcbs s \<and> tcb_at recver s\<rbrakk> \<Longrightarrow> valid_idle s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s \<and> tcb_at recver s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s
 2. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) s
 3. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; s'a = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst slot) and valid_etcbs and (\<lambda>s. tcb_at recver s \<and> (invs and emptyable slot) s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s \<and> tcb_at recver s)) s proof (prove)
goal (2 subgoals):
 1. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True)) s
 2. \<And>obj' s'a etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s'a; tcb_at recver s'a; tcb_at sender s'a; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s'a; cur_thread s'a \<noteq> idle_thread s'a; recver \<noteq> idle_thread s'a; sender \<noteq> idle_thread s'a; valid_etcbs s'a; awaiting_reply (tcb_state obj'); get_tcb recver s'a = Some obj'; get_etcb recver s'a = Some etcb; tcb_fault obj' = Some y; s'a = s\<rbrakk> \<Longrightarrow> (invs and not_idle_thread (fst slot) and valid_etcbs and (\<lambda>s. tcb_at recver s \<and> (invs and emptyable slot) s \<and> recver \<noteq> idle_thread s \<and> valid_etcbs s \<and> tcb_at recver s)) s proof (prove)
goal (1 subgoal):
 1. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> not_idle_thread (fst slot) s \<and> emptyable slot s proof (prove)
goal (2 subgoals):
 1. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> not_idle_thread (fst slot) s
 2. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> emptyable slot s proof (prove)
goal (2 subgoals):
 1. \<And>obj' etcb y s a b. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y; slot = (a, b)\<rbrakk> \<Longrightarrow> not_idle_thread (fst slot) s
 2. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> emptyable slot s proof (prove)
goal (2 subgoals):
 1. \<And>obj' etcb y s b. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) (idle_thread s, b) s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y; slot = (idle_thread s, b); valid_pspace 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_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> False
 2. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> emptyable slot s proof (prove)
goal (2 subgoals):
 1. \<And>obj' etcb y s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y; slot = (idle_thread s, b); valid_pspace 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_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; caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R)\<rbrakk> \<Longrightarrow> False
 2. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> emptyable slot s proof (prove)
goal (6 subgoals):
 1. \<And>obj' etcb y s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y; slot = (idle_thread s, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle 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_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; caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R)\<rbrakk> \<Longrightarrow> valid_global_refs s
 2. \<And>obj' etcb y s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y; slot = (idle_thread s, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle 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_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; caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R)\<rbrakk> \<Longrightarrow> valid_idle s
 3. \<And>obj' etcb y s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y; slot = (idle_thread s, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle 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_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; caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R)\<rbrakk> \<Longrightarrow> valid_irq_node s
 4. \<And>obj' etcb y s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y; slot = (idle_thread s, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle 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_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; caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R)\<rbrakk> \<Longrightarrow> caps_of_state s (idle_thread s, ?v398 obj' etcb y s b R) = Some (?cap398 obj' etcb y s b R)
 5. \<And>obj' etcb y s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y; slot = (idle_thread s, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle 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_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; caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R); ?cap398 obj' etcb y s b R = cap.NullCap\<rbrakk> \<Longrightarrow> False
 6. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> emptyable slot s proof (prove)
goal (2 subgoals):
 1. \<And>obj' etcb y s b R. \<lbrakk>slot' = transform_cslot_ptr (idle_thread s, b); tcb_at recver s; tcb_at sender s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y; slot = (idle_thread s, b); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle 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_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; caps_of_state s (idle_thread s, b) = Some (cap.ReplyCap recver False R); cap.ReplyCap recver False R = cap.NullCap\<rbrakk> \<Longrightarrow> False
 2. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> emptyable slot s proof (prove)
goal (1 subgoal):
 1. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> emptyable slot s proof (prove)
goal (3 subgoals):
 1. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> cte_wp_at (?P407 obj' etcb y s) slot s
 2. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>obj' etcb y s. \<lbrakk>slot' = transform_cslot_ptr slot; invs s; tcb_at recver s; tcb_at sender s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot s; cur_thread s \<noteq> idle_thread s; recver \<noteq> idle_thread s; sender \<noteq> idle_thread s; valid_etcbs s; awaiting_reply (tcb_state obj'); get_tcb recver s = Some obj'; get_etcb recver s = Some etcb; tcb_fault obj' = Some y\<rbrakk> \<Longrightarrow> \<forall>cap. ?P407 obj' etcb y s cap \<longrightarrow> \<not> is_master_reply_cap cap proof (prove)
goal:
No subgoals!