theory Syscall_DR

lemma dcorres_reply_from_syscall:
  "dcorres (dc \<oplus> dc) \<top> (invs and not_idle_thread thread and valid_idle and valid_etcbs)
    (do restart \<leftarrow> has_restart_cap thread;
      if restart then liftE (
      (do y \<leftarrow> corrupt_ipc_buffer thread True;
          y \<leftarrow>when call (mark_tcb_intent_error thread False);
          KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
      od ))
      else returnOk ()
    od)
    (liftE (do x \<leftarrow> get_thread_state thread;
      (case x of
        Structures_A.thread_state.Restart \<Rightarrow>
        do y \<leftarrow> when call (reply_from_kernel thread (0, reply));
           set_thread_state thread Structures_A.thread_state.Running
        od
      | _ \<Rightarrow> return ()) od))" apply (clarsimp simp:get_thread_state_def thread_get_def liftE_distrib' liftE_bindE) apply (rule dcorres_absorb_gets_the) apply (simp add:has_restart_cap_def get_thread_def gets_the_def
    gets_def bind_assoc liftE_distrib') apply (rule dcorres_absorb_get_l) apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb) apply (clarsimp simp:opt_object_tcb not_idle_thread_def
    liftE_bindE liftE_distrib' infer_tcb_pending_op_def tcb_slots
    transform_tcb_def assert_opt_def when_def returnOk_liftE[symmetric]
    split: Structures_A.thread_state.splits) apply (intro conjI impI) apply (rule dcorres_returnOk',simp)+ apply (rule corres_guard_imp) apply (rule corres_split[OF dcorres_reply_from_kernel]) apply (rule corres_dummy_return_pr) apply (rule corres_split[OF dcorres_set_intent_error]) apply (simp add:liftE_bindE returnOk_liftE) apply (rule set_thread_state_corres[unfolded tcb_slots]) apply (wp rfk_invs reply_from_kernel_error)+ apply (simp add:not_idle_thread_def) apply (wp rfk_invs) apply simp apply (clarsimp simp: tcb_at_def st_tcb_at_def obj_at_def not_idle_thread_def
                       dest!: get_tcb_SomeD) apply (rule corres_dummy_return_pr) apply (rule corres_guard_imp[OF corres_split[where r' = "dc"]]) apply (rule dcorres_dummy_corrupt_ipc_buffer) apply (simp add: returnOk_liftE) apply (rule set_thread_state_corres[unfolded tcb_slots]) apply wp+ apply simp apply (clarsimp simp: tcb_at_def invs_mdb st_tcb_at_def not_idle_thread_def obj_at_def
                      dest!: get_tcb_SomeD) apply (rule dcorres_returnOk', simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and not_idle_thread thread and valid_idle and valid_etcbs) (do restart <- has_restart_cap thread;
if restart then liftE (do y <- corrupt_ipc_buffer thread True;
y <- when call (mark_tcb_intent_error thread False);
KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) else returnOk ()
od) (liftE (do x <- get_thread_state thread;
case x of Restart \<Rightarrow> do y <- when call (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od | _ \<Rightarrow> return ()
od)) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and not_idle_thread thread and valid_idle and valid_etcbs) (do restart <- has_restart_cap thread;
if restart then liftE (do y <- corrupt_ipc_buffer thread True;
y <- when call (mark_tcb_intent_error thread False);
KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) else returnOk ()
od) (do tcb <- gets_the (get_tcb thread);
liftE (case tcb_state tcb of Restart \<Rightarrow> do y <- when call (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od | _ \<Rightarrow> return ())
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>(invs and not_idle_thread thread and valid_idle and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (do restart <- has_restart_cap thread;
if restart then liftE (do y <- corrupt_ipc_buffer thread True;
y <- when call (mark_tcb_intent_error thread False);
KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) else returnOk ()
od) (liftE (case tcb_state obj' of Restart \<Rightarrow> do y <- when call (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od | _ \<Rightarrow> return ())) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>invs s' \<and> not_idle_thread thread s' \<and> valid_idle s' \<and> valid_etcbs s'; get_tcb thread s' = Some obj'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (do x <- get;
x <- assert_opt (cdl_objects x thread);
t <- case x of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail;
if cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap then liftE (do y <- corrupt_ipc_buffer thread True;
y <- when call (mark_tcb_intent_error thread False);
KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) else returnOk ()
od) (liftE (case tcb_state obj' of Restart \<Rightarrow> do y <- when call (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od | _ \<Rightarrow> return ())) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj' s'a. \<lbrakk>invs s' \<and> not_idle_thread thread s' \<and> valid_idle s' \<and> valid_etcbs s'; get_tcb thread s' = Some obj'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do x <- assert_opt (cdl_objects (transform s'a) thread);
t <- case x of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail;
if cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap then liftE (do y <- corrupt_ipc_buffer thread True;
y <- when call (mark_tcb_intent_error thread False);
KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) else returnOk ()
od) (liftE (case tcb_state obj' of Restart \<Rightarrow> do y <- when call (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od | _ \<Rightarrow> return ())) proof (prove)
goal (1 subgoal):
 1. \<And>obj' s'a. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; not_idle_thread thread s'a; valid_idle s'a; valid_etcbs s'a; \<exists>etcb. get_etcb thread s'a = Some etcb\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do x <- assert_opt (cdl_objects (transform s'a) thread);
t <- case x of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail;
if cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap then liftE (do y <- corrupt_ipc_buffer thread True;
y <- when call (mark_tcb_intent_error thread False);
KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) else returnOk ()
od) (liftE (case tcb_state obj' of Restart \<Rightarrow> do y <- when call (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od | _ \<Rightarrow> return ())) proof (prove)
goal (1 subgoal):
 1. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb\<rbrakk> \<Longrightarrow> (tcb_state obj' = Running \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())) \<and> (inactive (tcb_state obj') \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())) \<and> (tcb_state obj' = Restart \<longrightarrow> (call \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
y <- mark_tcb_intent_error thread False;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (do y <- reply_from_kernel thread (0, reply);
liftE (set_thread_state thread Running)
od)) \<and> (\<not> call \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running)))) \<and> ((\<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42) \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())) \<and> ((\<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52) \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())) \<and> (awaiting_reply (tcb_state obj') \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())) \<and> ((\<exists>x7. tcb_state obj' = BlockedOnNotification x7) \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())) \<and> (idle (tcb_state obj') \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())) proof (prove)
goal (9 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Running\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; inactive (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
y <- mark_tcb_intent_error thread False;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (do y <- reply_from_kernel thread (0, reply);
liftE (set_thread_state thread Running)
od)
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (7 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
y <- mark_tcb_intent_error thread False;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (do y <- reply_from_kernel thread (0, reply);
liftE (set_thread_state thread Running)
od)
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (9 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?Q52 obj' s'a etcb) (?Q'52 obj' s'a etcb) (do y <- corrupt_ipc_buffer thread True;
y <- mark_tcb_intent_error thread False;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (do y <- reply_from_kernel thread (0, reply);
liftE (set_thread_state thread Running)
od)
 2. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; transform s'a = s\<rbrakk> \<Longrightarrow> ?Q52 obj' s'a etcb s
 3. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; s'a = s\<rbrakk> \<Longrightarrow> ?Q'52 obj' s'a etcb s
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (11 subgoals):
 1. \<And>obj' s'a etcb y ya. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; dc y ya\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R56 obj' s'a etcb y) (?R'56 obj' s'a etcb ya) (do y <- mark_tcb_intent_error thread False;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 obj' s'a etcb\<rbrace> corrupt_ipc_buffer thread True \<lbrace>?R56 obj' s'a etcb\<rbrace>
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?Q'56 obj' s'a etcb\<rbrace> reply_from_kernel thread (0, reply) \<lbrace>?R'56 obj' s'a etcb\<rbrace>
 4. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q56 obj' s'a etcb) s
 5. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; s'a = s\<rbrakk> \<Longrightarrow> (invs and tcb_at thread and not_idle_thread thread and valid_etcbs and ?Q'56 obj' s'a etcb) s
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 10. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>obj' s'a etcb y ya. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; dc y ya\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R56 obj' s'a etcb y) (?R'56 obj' s'a etcb ya) (do y <- mark_tcb_intent_error thread False;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (do return (?b61 obj' s'a etcb y ya);
liftE (set_thread_state thread Running)
od)
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 obj' s'a etcb\<rbrace> corrupt_ipc_buffer thread True \<lbrace>?R56 obj' s'a etcb\<rbrace>
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?Q'56 obj' s'a etcb\<rbrace> reply_from_kernel thread (0, reply) \<lbrace>?R'56 obj' s'a etcb\<rbrace>
 4. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q56 obj' s'a etcb) s
 5. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; s'a = s\<rbrakk> \<Longrightarrow> (invs and tcb_at thread and not_idle_thread thread and valid_etcbs and ?Q'56 obj' s'a etcb) s
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 10. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>obj' s'a etcb y ya yb rv'. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; dc y ya; dc yb rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R63 obj' s'a etcb y ya yb) (?R'63 obj' s'a etcb y ya rv') (liftE (KHeap_D.set_cap (thread, 5) RunningCap)) (K_bind (liftE (set_thread_state thread Running)) rv')
 2. \<And>obj' s'a etcb y ya. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 obj' s'a etcb y\<rbrace> mark_tcb_intent_error thread False \<lbrace>?R63 obj' s'a etcb y ya\<rbrace>
 3. \<And>obj' s'a etcb y ya. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'69 obj' s'a etcb ya\<rbrace> return (?b61 obj' s'a etcb y ya) \<lbrace>?R'63 obj' s'a etcb y ya\<rbrace>
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 obj' s'a etcb\<rbrace> corrupt_ipc_buffer thread True \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q65 obj' s'a etcb y\<rbrace>
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?Q'56 obj' s'a etcb\<rbrace> reply_from_kernel thread (0, reply) \<lbrace>\<lambda>ya. invs and valid_etcbs and (\<lambda>s. \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = False \<and> ko_at (TCB tcb) thread s) and not_idle_thread thread and ?Q'69 obj' s'a etcb ya\<rbrace>
 6. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q56 obj' s'a etcb) s
 7. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; s'a = s\<rbrakk> \<Longrightarrow> (invs and tcb_at thread and not_idle_thread thread and valid_etcbs and ?Q'56 obj' s'a etcb) s
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 10. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>obj' s'a etcb rv'. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> dcorres dc (?R63 obj' s'a etcb () () ()) (?R'63 obj' s'a etcb () () rv') (KHeap_D.set_cap (thread, 5) RunningCap) (set_thread_state thread Running)
 2. \<And>obj' s'a etcb y ya. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 obj' s'a etcb y\<rbrace> mark_tcb_intent_error thread False \<lbrace>?R63 obj' s'a etcb y ya\<rbrace>
 3. \<And>obj' s'a etcb y ya. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'69 obj' s'a etcb ya\<rbrace> return (?b61 obj' s'a etcb y ya) \<lbrace>?R'63 obj' s'a etcb y ya\<rbrace>
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 obj' s'a etcb\<rbrace> corrupt_ipc_buffer thread True \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q65 obj' s'a etcb y\<rbrace>
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?Q'56 obj' s'a etcb\<rbrace> reply_from_kernel thread (0, reply) \<lbrace>\<lambda>ya. invs and valid_etcbs and (\<lambda>s. \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = False \<and> ko_at (TCB tcb) thread s) and not_idle_thread thread and ?Q'69 obj' s'a etcb ya\<rbrace>
 6. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q56 obj' s'a etcb) s
 7. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; s'a = s\<rbrakk> \<Longrightarrow> (invs and tcb_at thread and not_idle_thread thread and valid_etcbs and ?Q'56 obj' s'a etcb) s
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 10. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>obj' s'a etcb y ya. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q65 obj' s'a etcb y\<rbrace> mark_tcb_intent_error thread False \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>obj' s'a etcb y ya. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'69 obj' s'a etcb ya\<rbrace> return (?b61 obj' s'a etcb y ya) \<lbrace>\<lambda>a. not_idle_thread thread and K (RunningCap = infer_tcb_pending_op thread Running) and valid_etcbs\<rbrace>
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 obj' s'a etcb\<rbrace> corrupt_ipc_buffer thread True \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q65 obj' s'a etcb y\<rbrace>
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?Q'56 obj' s'a etcb\<rbrace> reply_from_kernel thread (0, reply) \<lbrace>\<lambda>ya. invs and valid_etcbs and (\<lambda>s. \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = False \<and> ko_at (TCB tcb) thread s) and not_idle_thread thread and ?Q'69 obj' s'a etcb ya\<rbrace>
 5. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q56 obj' s'a etcb) s
 6. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; s'a = s\<rbrakk> \<Longrightarrow> (invs and tcb_at thread and not_idle_thread thread and valid_etcbs and ?Q'56 obj' s'a etcb) s
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 10. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
A total of 12 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?P'95 obj' s'a etcb\<rbrace> reply_from_kernel thread (0, reply) \<lbrace>\<lambda>rv s. not_idle_thread thread s \<and> (not_idle_thread thread and K (RunningCap = infer_tcb_pending_op thread Running) and valid_etcbs) s\<rbrace>
 2. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; s'a = s\<rbrakk> \<Longrightarrow> (invs and tcb_at thread and not_idle_thread thread and valid_etcbs and (\<lambda>s. (invs and tcb_at thread) s \<and> valid_etcbs s \<and> (tcb_at thread and K (fst (0, reply) \<le> mask 19 \<and> (0 < fst (0, reply)) = False)) s \<and> ?P'95 obj' s'a etcb s)) s
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (9 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call\<rbrakk> \<Longrightarrow> \<lbrace>?P'95 obj' s'a etcb\<rbrace> reply_from_kernel thread (0, reply) \<lbrace>\<lambda>rv s. thread \<noteq> idle_thread s \<and> valid_etcbs s\<rbrace>
 2. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; s'a = s\<rbrakk> \<Longrightarrow> (invs and tcb_at thread and not_idle_thread thread and valid_etcbs and (\<lambda>s. (invs and tcb_at thread) s \<and> valid_etcbs s \<and> (tcb_at thread and K (fst (0, reply) \<le> mask 19 \<and> (0 < fst (0, reply)) = False)) s \<and> ?P'95 obj' s'a etcb s)) s
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (8 subgoals):
 1. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; s'a = s\<rbrakk> \<Longrightarrow> (invs and tcb_at thread and not_idle_thread thread and valid_etcbs and (\<lambda>s. (invs and tcb_at thread) s \<and> valid_etcbs s \<and> (tcb_at thread and K (fst (0, reply) \<le> mask 19 \<and> (0 < fst (0, reply)) = False)) s \<and> thread \<noteq> idle_thread s \<and> valid_etcbs s)) s
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (7 subgoals):
 1. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; call; s'a = s\<rbrakk> \<Longrightarrow> (invs and tcb_at thread and not_idle_thread thread and valid_etcbs and (\<lambda>s. (invs and tcb_at thread) s \<and> valid_etcbs s \<and> (tcb_at thread and K (fst (0, reply) \<le> mask 19 \<and> (0 < fst (0, reply)) = False)) s \<and> thread \<noteq> idle_thread s \<and> valid_etcbs s)) s
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (6 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (liftE (set_thread_state thread Running))
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (6 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (do y <- corrupt_ipc_buffer thread True;
liftE (KHeap_D.set_cap (thread, 5) RunningCap)
od) (do return (?b107 obj' s'a etcb);
liftE (set_thread_state thread Running)
od)
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (11 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres dc (?P110 obj' s'a etcb) (?P'110 obj' s'a etcb) (corrupt_ipc_buffer thread True) (return (?b107 obj' s'a etcb))
 2. \<And>obj' s'a etcb y rv'. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; dc y rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R110 obj' s'a etcb y) (?R'110 obj' s'a etcb rv') (liftE (KHeap_D.set_cap (thread, 5) RunningCap)) (K_bind (liftE (set_thread_state thread Running)) rv')
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> \<lbrace>?Q110 obj' s'a etcb\<rbrace> corrupt_ipc_buffer thread True \<lbrace>?R110 obj' s'a etcb\<rbrace>
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> \<lbrace>?Q'110 obj' s'a etcb\<rbrace> return (?b107 obj' s'a etcb) \<lbrace>?R'110 obj' s'a etcb\<rbrace>
 5. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; transform s'a = s\<rbrakk> \<Longrightarrow> (?P110 obj' s'a etcb and ?Q110 obj' s'a etcb) s
 6. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; s'a = s\<rbrakk> \<Longrightarrow> (?P'110 obj' s'a etcb and ?Q'110 obj' s'a etcb) s
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 10. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>obj' s'a etcb y rv'. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; dc y rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R110 obj' s'a etcb y) (?R'110 obj' s'a etcb rv') (liftE (KHeap_D.set_cap (thread, 5) RunningCap)) (K_bind (liftE (set_thread_state thread Running)) rv')
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> \<lbrace>?Q110 obj' s'a etcb\<rbrace> corrupt_ipc_buffer thread True \<lbrace>?R110 obj' s'a etcb\<rbrace>
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> \<lbrace>?Q'110 obj' s'a etcb\<rbrace> return (?b107 obj' s'a etcb) \<lbrace>?R'110 obj' s'a etcb\<rbrace>
 4. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q110 obj' s'a etcb) s
 5. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'110 obj' s'a etcb) s
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 10. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (10 subgoals):
 1. \<And>obj' s'a etcb rv'. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> dcorres dc (?R110 obj' s'a etcb ()) (?R'110 obj' s'a etcb rv') (KHeap_D.set_cap (thread, 5) RunningCap) (set_thread_state thread Running)
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> \<lbrace>?Q110 obj' s'a etcb\<rbrace> corrupt_ipc_buffer thread True \<lbrace>?R110 obj' s'a etcb\<rbrace>
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> \<lbrace>?Q'110 obj' s'a etcb\<rbrace> return (?b107 obj' s'a etcb) \<lbrace>?R'110 obj' s'a etcb\<rbrace>
 4. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q110 obj' s'a etcb) s
 5. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'110 obj' s'a etcb) s
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 10. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (9 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> \<lbrace>?Q110 obj' s'a etcb\<rbrace> corrupt_ipc_buffer thread True \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call\<rbrakk> \<Longrightarrow> \<lbrace>?Q'110 obj' s'a etcb\<rbrace> return (?b107 obj' s'a etcb) \<lbrace>\<lambda>rv'. not_idle_thread thread and K (RunningCap = infer_tcb_pending_op thread Running) and valid_etcbs\<rbrace>
 3. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q110 obj' s'a etcb) s
 4. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'110 obj' s'a etcb) s
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 8. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 9. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (7 subgoals):
 1. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
 2. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and valid_idle and not_idle_thread thread and valid_etcbs and (not_idle_thread thread and K (RunningCap = infer_tcb_pending_op thread Running) and valid_etcbs)) s
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 7. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (6 subgoals):
 1. \<And>obj' s'a etcb s. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; tcb_state obj' = Restart; \<not> call; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and valid_idle and not_idle_thread thread and valid_etcbs and (not_idle_thread thread and K (RunningCap = infer_tcb_pending_op thread Running) and valid_etcbs)) s
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 6. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal (5 subgoals):
 1. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x41 x42. tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 2. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x51 x52. tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 3. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 4. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; \<exists>x7. tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ())
 5. \<And>obj' s'a etcb. \<lbrakk>get_tcb thread s'a = Some obj'; invs s'a; thread \<noteq> idle_thread s'a; valid_idle s'a; valid_etcbs s'a; get_etcb thread s'a = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (returnOk ()) (returnOk ()) proof (prove)
goal:
No subgoals!