theory Tcb_DR

lemma restart_corres:
  "dcorres dc \<top>
  (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs)
  (Tcb_D.restart obj_id) (Tcb_A.restart obj_id)" apply (clarsimp simp: Tcb_D.restart_def Tcb_A.restart_def
    when_def get_cap_def) apply (clarsimp simp: thread_get_def get_thread_state_def ) apply (rule dcorres_gets_the) apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb) apply (clarsimp simp:opt_cap_tcb not_idle_thread_def tcb_vspace_slot_def
    tcb_pending_op_slot_def tcb_caller_slot_def tcb_ipcbuffer_slot_def
    tcb_cspace_slot_def tcb_replycap_slot_def) apply (intro conjI impI) apply (rule corres_guard_imp) apply (rule corres_split[OF finalise_cancel_ipc]) apply (rule corres_split[OF dcorres_setup_reply_master[unfolded tcb_replycap_slot_def] ]) apply (rule dcorres_rhs_noop_below_True[OF dcorres_rhs_noop_below_True]) apply (rule possible_switch_to_dcorres) apply (rule tcb_sched_action_dcorres) apply (rule dcorres_set_thread_state_Restart2[unfolded tcb_pending_op_slot_def]) apply wp apply (simp add:not_idle_thread_def) apply ((wp|wps)+)[2] apply (rule_tac Q="(=) s' and invs" in  hoare_vcg_precond_imp) apply (rule hoare_strengthen_post
             [where Q="\<lambda>r. invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs"]) apply (simp add:not_idle_thread_def) apply (wp) apply (clarsimp simp:invs_def valid_state_def valid_pspace_def
                tcb_at_def not_idle_thread_def)+ apply (clarsimp simp:valid_idle_def pred_tcb_at_def obj_at_def) apply assumption apply (clarsimp simp:not_idle_thread_def)+ apply (clarsimp dest!:runnable_imply[where obj_id = obj_id])+ apply (clarsimp simp:invs_def valid_state_def) apply (drule only_idleD[rotated]) apply (fastforce simp:st_tcb_at_def obj_at_def dest!:get_tcb_SomeD) apply simp apply (clarsimp simp: runnable_def infer_tcb_pending_op_def
      split:Structures_A.thread_state.split_asm)+ apply (frule(1) valid_etcbs_get_tcb_get_etcb) apply (fastforce simp:opt_cap_tcb not_idle_thread_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.restart obj_id) (Tcb_A.restart obj_id) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (do cap <- KHeap_D.get_cap (obj_id, tcb_pending_op_slot);
if cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap then do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, tcb_pending_op_slot) RestartCap
od else return ()
od) (do state <- get_thread_state obj_id;
if \<not> runnable state \<and> state \<noteq> IdleThreadState then do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od else return ()
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (do cap <- KHeap_D.get_cap (obj_id, tcb_pending_op_slot);
if cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap then do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, tcb_pending_op_slot) RestartCap
od else return ()
od) (do tcb <- gets_the (get_tcb obj_id);
if \<not> runnable (tcb_state tcb) \<and> tcb_state tcb \<noteq> IdleThreadState then do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od else return ()
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s' obj obj'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' = Some obj'; opt_cap (obj_id, tcb_pending_op_slot) s = Some obj\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (if obj \<noteq> RestartCap \<and> obj \<noteq> RunningCap then do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, tcb_pending_op_slot) RestartCap
od else return ()) (if \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState then do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od else return ())
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>get_tcb obj_id s' = Some obj'; opt_cap (obj_id, tcb_pending_op_slot) (transform s') = Some obj; invs s'; tcb_at obj_id s'; not_idle_thread obj_id s'; valid_etcbs s'; \<exists>etcb. get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> (obj \<noteq> RestartCap \<and> obj \<noteq> RunningCap \<longrightarrow> (\<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, tcb_pending_op_slot) RestartCap
od) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)) \<and> (runnable (tcb_state obj') \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, tcb_pending_op_slot) RestartCap
od) (return ())) \<and> (idle (tcb_state obj') \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, tcb_pending_op_slot) RestartCap
od) (return ()))) \<and> (obj = RestartCap \<longrightarrow> \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)) \<and> (obj = RunningCap \<longrightarrow> \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> (infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap \<longrightarrow> (\<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)) \<and> (runnable (tcb_state obj') \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())) \<and> (idle (tcb_state obj') \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ()))) \<and> (infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap \<longrightarrow> \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)) \<and> (infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap \<longrightarrow> \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (6 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 5. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 6. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (8 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc (?Q38 s' obj' etcb) (?Q'38 s' obj' etcb) (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 2. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ?Q38 s' obj' etcb s
 3. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> ?Q'38 s' obj' etcb s
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 5. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 8. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (10 subgoals):
 1. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R42 s' obj' etcb y) (?R'42 s' obj' etcb ya) (do y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (do y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 s' obj' etcb\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>?R42 s' obj' etcb\<rbrace>
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' obj' etcb\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'42 s' obj' etcb\<rbrace>
 4. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q42 s' obj' etcb) s
 5. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 8. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 9. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 10. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (12 subgoals):
 1. \<And>s' obj' etcb y ya yb yc. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R47 s' obj' etcb y ya yb) (?R'47 s' obj' etcb y ya yc) (KHeap_D.set_cap (obj_id, 5) RestartCap) (do y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 2. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q49 s' obj' etcb y\<rbrace> KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id) \<lbrace>?R47 s' obj' etcb y ya\<rbrace>
 3. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 s' obj' etcb ya\<rbrace> setup_reply_master obj_id \<lbrace>?R'47 s' obj' etcb y ya\<rbrace>
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 s' obj' etcb\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q49 s' obj' etcb y\<rbrace>
 5. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' obj' etcb\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>\<lambda>ya. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and ?Q'52 s' obj' etcb ya\<rbrace>
 6. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q42 s' obj' etcb) s
 7. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 8. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 9. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 10. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
A total of 12 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>s' obj' etcb y ya yb yc. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>y. True) (\<lambda>y. True) (return ()) (possible_switch_to obj_id)
 2. \<And>s' obj' etcb y ya yb yc. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>y. True) (\<lambda>y. True) (return ()) (tcb_sched_action tcb_sched_enqueue obj_id)
 3. \<And>s' obj' etcb y ya yb yc. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R47 s' obj' etcb y ya yb) (?R'47 s' obj' etcb y ya yc) (KHeap_D.set_cap (obj_id, 5) RestartCap) (set_thread_state obj_id Restart)
 4. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q49 s' obj' etcb y\<rbrace> KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id) \<lbrace>?R47 s' obj' etcb y ya\<rbrace>
 5. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 s' obj' etcb ya\<rbrace> setup_reply_master obj_id \<lbrace>?R'47 s' obj' etcb y ya\<rbrace>
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 s' obj' etcb\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q49 s' obj' etcb y\<rbrace>
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' obj' etcb\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>\<lambda>ya. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and ?Q'52 s' obj' etcb ya\<rbrace>
 8. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q42 s' obj' etcb) s
 9. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 10. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s' obj' etcb y ya yb yc. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>y. True) (\<lambda>y. True) (return ()) (tcb_sched_action tcb_sched_enqueue obj_id)
 2. \<And>s' obj' etcb y ya yb yc. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R47 s' obj' etcb y ya yb) (?R'47 s' obj' etcb y ya yc) (KHeap_D.set_cap (obj_id, 5) RestartCap) (set_thread_state obj_id Restart)
 3. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q49 s' obj' etcb y\<rbrace> KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id) \<lbrace>?R47 s' obj' etcb y ya\<rbrace>
 4. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 s' obj' etcb ya\<rbrace> setup_reply_master obj_id \<lbrace>?R'47 s' obj' etcb y ya\<rbrace>
 5. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 s' obj' etcb\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q49 s' obj' etcb y\<rbrace>
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' obj' etcb\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>\<lambda>ya. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and ?Q'52 s' obj' etcb ya\<rbrace>
 7. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q42 s' obj' etcb) s
 8. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 9. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 10. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>s' obj' etcb y ya yb yc. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R47 s' obj' etcb y ya yb) (?R'47 s' obj' etcb y ya yc) (KHeap_D.set_cap (obj_id, 5) RestartCap) (set_thread_state obj_id Restart)
 2. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q49 s' obj' etcb y\<rbrace> KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id) \<lbrace>?R47 s' obj' etcb y ya\<rbrace>
 3. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 s' obj' etcb ya\<rbrace> setup_reply_master obj_id \<lbrace>?R'47 s' obj' etcb y ya\<rbrace>
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 s' obj' etcb\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q49 s' obj' etcb y\<rbrace>
 5. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' obj' etcb\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>\<lambda>ya. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and ?Q'52 s' obj' etcb ya\<rbrace>
 6. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q42 s' obj' etcb) s
 7. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 8. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 9. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 10. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q49 s' obj' etcb y\<rbrace> KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id) \<lbrace>\<lambda>yb _. True\<rbrace>
 2. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 s' obj' etcb ya\<rbrace> setup_reply_master obj_id \<lbrace>\<lambda>yc a. valid_mdb a \<and> not_idle_thread obj_id a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a\<rbrace>
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 s' obj' etcb\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q49 s' obj' etcb y\<rbrace>
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' obj' etcb\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>\<lambda>ya. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and ?Q'52 s' obj' etcb ya\<rbrace>
 5. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q42 s' obj' etcb) s
 6. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 8. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 9. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 10. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s' obj' etcb y ya. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 s' obj' etcb ya\<rbrace> setup_reply_master obj_id \<lbrace>\<lambda>yc a. valid_mdb a \<and> not_idle_thread obj_id a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a\<rbrace>
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 s' obj' etcb\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>\<lambda>y. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' obj' etcb\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>\<lambda>ya. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and ?Q'52 s' obj' etcb ya\<rbrace>
 4. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q42 s' obj' etcb) s
 5. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 8. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 9. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 10. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (10 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 s' obj' etcb ()\<rbrace> setup_reply_master obj_id \<lbrace>\<lambda>yc a. valid_mdb a \<and> obj_id \<noteq> idle_thread a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a\<rbrace>
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q42 s' obj' etcb\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>\<lambda>y. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' obj' etcb\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>\<lambda>ya. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and ?Q'52 s' obj' etcb ya\<rbrace>
 4. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q42 s' obj' etcb) s
 5. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 8. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 9. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 10. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (8 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' obj' etcb\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>\<lambda>ya. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and (\<lambda>a. valid_mdb a \<and> obj_id \<noteq> idle_thread a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a)\<rbrace>
 2. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 5. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 8. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (9 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>(=) s' and invs\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>\<lambda>ya. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and (\<lambda>a. valid_mdb a \<and> obj_id \<noteq> idle_thread a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a)\<rbrace>
 2. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; ?Q'42 s' obj' etcb s\<rbrakk> \<Longrightarrow> ((=) s' and invs) s
 3. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 4. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 5. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 8. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 9. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (10 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>(=) s' and invs\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>\<lambda>r. invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs\<rbrace>
 2. \<And>s' obj' etcb rv s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and (\<lambda>a. valid_mdb a \<and> obj_id \<noteq> idle_thread a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a)) s
 3. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; ?Q'42 s' obj' etcb s\<rbrakk> \<Longrightarrow> ((=) s' and invs) s
 4. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 5. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 8. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 9. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 10. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (10 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>(=) s' and invs\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>\<lambda>r. invs and tcb_at obj_id and (\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs\<rbrace>
 2. \<And>s' obj' etcb rv s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and (\<lambda>a. valid_mdb a \<and> obj_id \<noteq> idle_thread a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a)) s
 3. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; ?Q'42 s' obj' etcb s\<rbrakk> \<Longrightarrow> ((=) s' and invs) s
 4. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 5. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 8. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 9. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 10. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (10 subgoals):
 1. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; ((=) s' and invs) s\<rbrakk> \<Longrightarrow> invs s \<and> tcb_at obj_id s \<and> obj_id \<noteq> idle_thread s \<and> valid_etcbs s
 2. \<And>s' obj' etcb rv s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and (\<lambda>a. valid_mdb a \<and> obj_id \<noteq> idle_thread a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a)) s
 3. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; ?Q'42 s' obj' etcb s\<rbrakk> \<Longrightarrow> ((=) s' and invs) s
 4. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 5. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 8. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 9. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 10. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (9 subgoals):
 1. \<And>s' obj' etcb s tcb. \<lbrakk>get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; valid_objs s'; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj'); tcb_state obj' \<noteq> IdleThreadState; valid_objs s; pspace_aligned s'; pspace_aligned s; pspace_distinct s'; pspace_distinct s; if_live_then_nonz_cap s'; if_live_then_nonz_cap s; zombies_final s'; zombies_final s; sym_refs (state_refs_of s'); sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s'); sym_refs (state_hyp_refs_of s); valid_mdb s'; valid_mdb s; valid_ioc s'; valid_ioc s; valid_idle s'; valid_idle s; only_idle s'; only_idle s; if_unsafe_then_cap s'; if_unsafe_then_cap s; valid_reply_caps s'; valid_reply_caps s; valid_reply_masters s'; valid_reply_masters s; valid_global_refs s'; valid_global_refs s; valid_arch_state s'; valid_arch_state s; valid_irq_node s'; valid_irq_node s; valid_irq_handlers s'; valid_irq_handlers s; valid_irq_states s'; valid_irq_states s; valid_machine_state s'; valid_machine_state s; valid_vspace_objs s'; valid_vspace_objs s; valid_arch_caps s'; valid_arch_caps s; valid_global_objs s'; valid_global_objs s; valid_kernel_mappings s'; valid_kernel_mappings s; equal_kernel_mappings s'; equal_kernel_mappings s; valid_asid_map s'; valid_asid_map s; valid_global_vspace_mappings s'; valid_global_vspace_mappings s; pspace_in_kernel_window s'; pspace_in_kernel_window s; cap_refs_in_kernel_window s'; cap_refs_in_kernel_window s; pspace_respects_device_region s'; pspace_respects_device_region s; cap_refs_respects_device_region s'; cur_tcb s'; cap_refs_respects_device_region s; cur_tcb s; get_tcb obj_id s = Some tcb; obj_id \<noteq> idle_thread s; valid_etcbs s\<rbrakk> \<Longrightarrow> st_tcb_at idle (idle_thread s) s
 2. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; ?Q'42 s' obj' etcb s\<rbrakk> \<Longrightarrow> ((=) s' and invs) s
 3. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 4. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 5. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 8. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 9. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (8 subgoals):
 1. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; ?Q'42 s' obj' etcb s\<rbrakk> \<Longrightarrow> ((=) s' and invs) s
 2. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'42 s' obj' etcb) s
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 5. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 7. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 8. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (7 subgoals):
 1. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>s' obj' etcb s. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ((=) s' and invs)) s
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; runnable (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 5. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 6. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 7. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; runnable (tcb_state obj'); infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RestartCap \<and> infer_tcb_pending_op obj_id (tcb_state obj') \<noteq> RunningCap; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 5. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 4. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; idle (tcb_state obj'); 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> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 4. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; idle (tcb_state obj'); valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_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> st_tcb_at idle (?t240 s' obj' etcb) s'
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; idle (tcb_state obj'); valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_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'; ?t240 s' obj' etcb = idle_thread s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 5. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; idle (tcb_state obj'); valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_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'; obj_id = idle_thread s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- CSpace_D.cancel_ipc obj_id;
y <- KHeap_D.set_cap (obj_id, 2) (MasterReplyCap obj_id);
KHeap_D.set_cap (obj_id, 5) RestartCap
od) (return ())
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 4. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RestartCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb obj_id s' = Some obj'; invs s'; tcb_at obj_id s'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb; infer_tcb_pending_op obj_id (tcb_state obj') = RunningCap; \<not> runnable (tcb_state obj') \<and> tcb_state obj' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- IpcCancel_A.cancel_ipc obj_id;
y <- setup_reply_master obj_id;
y <- set_thread_state obj_id Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id;
possible_switch_to obj_id
od)
 3. \<And>s s'. \<lbrakk>s = transform s'; True; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) s \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>s' y. \<lbrakk>get_tcb obj_id s' = Some y; invs s'; tcb_at obj_id s'; not_idle_thread obj_id s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (obj_id, tcb_pending_op_slot) (transform s') = Some y proof (prove)
goal (1 subgoal):
 1. \<And>s' y. \<lbrakk>get_tcb obj_id s' = Some y; invs s'; tcb_at obj_id s'; not_idle_thread obj_id s'; valid_etcbs s'; \<exists>etcb. get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (obj_id, tcb_pending_op_slot) (transform s') = Some y proof (prove)
goal:
No subgoals!