theory Schedule_DR

lemma activate_thread_corres:
  "dcorres dc \<top> (ct_in_state activatable and invs and valid_etcbs)
  (do t \<leftarrow> gets cdl_current_thread;
      case t of Some thread \<Rightarrow> do
       restart \<leftarrow> has_restart_cap thread;
       when restart $  KHeap_D.set_cap (thread,tcb_pending_op_slot) RunningCap
      od | None \<Rightarrow> return ()
  od)
  activate_thread" apply (simp add: activate_thread_def has_restart_cap_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (rule dcorres_absorb_get_l) apply (simp add:get_thread_state_def bind_assoc thread_get_def) apply (rule dcorres_absorb_gets_the) apply (case_tac "cdl_current_thread (transform s'a) = None") apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def
     cdl_current_thread transform_current_thread_def valid_idle_def
     arch_activate_idle_thread_def
     split : if_splits dest!:get_tcb_SomeD invs_valid_idle) apply clarsimp apply (subgoal_tac "not_idle_thread (cur_thread s'b) s'b") prefer 2 apply (clarsimp simp:transform_def transform_current_thread_def) apply (clarsimp simp:not_idle_thread_def)+ apply (frule(1) valid_etcbs_get_tcb_get_etcb, clarsimp) apply (frule opt_object_tcb) apply simp apply simp apply (clarsimp simp:transform_tcb_def gets_def gets_the_def has_restart_cap_def
    get_thread_def bind_assoc cdl_current_thread transform_current_thread_def) apply (rule dcorres_absorb_get_l) apply (simp add:assert_opt_def when_def) apply (case_tac  "tcb_state obj'") apply (clarsimp simp:infer_tcb_pending_op_def tcb_pending_op_slot_def tcb_boundntfn_slot_def
           when_def pred_tcb_at_def ct_in_state_def obj_at_def
           dest!:get_tcb_SomeD)+ apply (rule corres_guard_imp) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (rule set_thread_state_corres[unfolded tcb_pending_op_slot_def]) apply simp apply (wpsimp wp: dcorres_to_wp[OF as_user_setNextPC_corres,simplified])+ apply (simp add:invs_mdb pred_tcb_at_def obj_at_def invs_valid_idle
         generates_pending_def not_idle_thread_def) apply (clarsimp simp:infer_tcb_pending_op_def arch_activate_idle_thread_def
             when_def pred_tcb_at_def ct_in_state_def obj_at_def tcb_pending_op_slot_def tcb_boundntfn_slot_def
             dest!:get_tcb_SomeD)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (ct_in_state activatable and invs and valid_etcbs) (do t <- gets cdl_current_thread;
case t of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart $ KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od
od) activate_thread proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (ct_in_state activatable and invs and valid_etcbs) (do s <- get;
case cdl_current_thread s of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart $ KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od
od) (do s <- get;
get_thread_state (cur_thread s) >>= case_thread_state (return ()) fail (do pc <- as_user (cur_thread s) getRestartPC;
y <- as_user (cur_thread s) (setNextPC pc);
set_thread_state (cur_thread s) Running
od) (\<lambda>word receiver_payload_ext. fail) (\<lambda>word sender_payload_ext. fail) fail (\<lambda>word. fail) (arch_activate_idle_thread (cur_thread s))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (ct_in_state activatable and invs and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
case cdl_current_thread s of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart $ KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od
od) (get_thread_state (cur_thread s') >>= case_thread_state (return ()) fail (do pc <- as_user (cur_thread s') getRestartPC;
y <- as_user (cur_thread s') (setNextPC pc);
set_thread_state (cur_thread s') Running
od) (\<lambda>word receiver_payload_ext. fail) (\<lambda>word sender_payload_ext. fail) fail (\<lambda>word. fail) (arch_activate_idle_thread (cur_thread s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a. \<lbrakk>True; (ct_in_state activatable and invs and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (case cdl_current_thread (transform s'a) of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart $ KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) (get_thread_state (cur_thread s') >>= case_thread_state (return ()) fail (do pc <- as_user (cur_thread s') getRestartPC;
y <- as_user (cur_thread s') (setNextPC pc);
set_thread_state (cur_thread s') Running
od) (\<lambda>word receiver_payload_ext. fail) (\<lambda>word sender_payload_ext. fail) fail (\<lambda>word. fail) (arch_activate_idle_thread (cur_thread s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a. \<lbrakk>ct_in_state activatable s'a \<and> invs s'a \<and> valid_etcbs s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (case cdl_current_thread (transform s'a) of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart $ KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) (do tcb <- gets_the (get_tcb (cur_thread s'a));
case tcb_state tcb of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'a) getRestartPC;
y <- as_user (cur_thread s'a) (setNextPC pc);
set_thread_state (cur_thread s'a) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'a) | _ \<Rightarrow> fail
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a s'b obj'. \<lbrakk>ct_in_state activatable s'a \<and> invs s'a \<and> valid_etcbs s'a; s' = s'a; s'a = s'b; get_tcb (cur_thread s'a) s'b = Some obj'; transform s'a = transform s'b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case cdl_current_thread (transform s'a) of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart $ KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'a) getRestartPC;
y <- as_user (cur_thread s'a) (setNextPC pc);
set_thread_state (cur_thread s'a) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'a) | _ \<Rightarrow> fail) proof (prove)
goal (2 subgoals):
 1. \<And>s' s'a s'b obj'. \<lbrakk>ct_in_state activatable s'a \<and> invs s'a \<and> valid_etcbs s'a; s' = s'a; s'a = s'b; get_tcb (cur_thread s'a) s'b = Some obj'; transform s'a = transform s'b; cdl_current_thread (transform s'a) = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case cdl_current_thread (transform s'a) of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart $ KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'a) getRestartPC;
y <- as_user (cur_thread s'a) (setNextPC pc);
set_thread_state (cur_thread s'a) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'a) | _ \<Rightarrow> fail)
 2. \<And>s' s'a s'b obj'. \<lbrakk>ct_in_state activatable s'a \<and> invs s'a \<and> valid_etcbs s'a; s' = s'a; s'a = s'b; get_tcb (cur_thread s'a) s'b = Some obj'; transform s'a = transform s'b; cdl_current_thread (transform s'a) \<noteq> None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case cdl_current_thread (transform s'a) of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart $ KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'a) getRestartPC;
y <- as_user (cur_thread s'a) (setNextPC pc);
set_thread_state (cur_thread s'a) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'a) | _ \<Rightarrow> fail) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a s'b obj'. \<lbrakk>ct_in_state activatable s'a \<and> invs s'a \<and> valid_etcbs s'a; s' = s'a; s'a = s'b; get_tcb (cur_thread s'a) s'b = Some obj'; transform s'a = transform s'b; cdl_current_thread (transform s'a) \<noteq> None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (case cdl_current_thread (transform s'a) of None \<Rightarrow> return () | Some thread \<Rightarrow> do restart <- has_restart_cap thread;
when restart $ KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'a) getRestartPC;
y <- as_user (cur_thread s'a) (setNextPC pc);
set_thread_state (cur_thread s'a) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'a) | _ \<Rightarrow> fail) proof (prove)
goal (1 subgoal):
 1. \<And>s'b obj' y. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (do restart <- has_restart_cap y;
when restart (KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap)
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail) proof (prove)
goal (2 subgoals):
 1. \<And>s'b obj' y. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; not_idle_thread (cur_thread s'b) s'b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (do restart <- has_restart_cap y;
when restart (KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap)
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)
 2. \<And>s'b obj' y. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b\<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s'b) s'b proof (prove)
goal (2 subgoals):
 1. \<And>s'b obj' y. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b\<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s'b) s'b
 2. \<And>s'b obj' y. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; not_idle_thread (cur_thread s'b) s'b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (do restart <- has_restart_cap y;
when restart (KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap)
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail) proof (prove)
goal (2 subgoals):
 1. \<And>s'b obj' y. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; (if cur_thread s'b \<noteq> idle_thread s'b then Some (cur_thread s'b) else None) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b\<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s'b) s'b
 2. \<And>s'b obj' y. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; not_idle_thread (cur_thread s'b) s'b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (do restart <- has_restart_cap y;
when restart (KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap)
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail) proof (prove)
goal (1 subgoal):
 1. \<And>s'b obj' y. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; cur_thread s'b \<noteq> idle_thread s'b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (do restart <- has_restart_cap y;
when restart (KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap)
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail) proof (prove)
goal (1 subgoal):
 1. \<And>s'b obj' y etcb. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; cur_thread s'b \<noteq> idle_thread s'b; get_etcb (cur_thread s'b) s'b = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (do restart <- has_restart_cap y;
when restart (KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap)
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail) proof (prove)
goal (3 subgoals):
 1. \<And>s'b obj' y etcb. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; cur_thread s'b \<noteq> idle_thread s'b; get_etcb (cur_thread s'b) s'b = Some etcb\<rbrakk> \<Longrightarrow> get_etcb (cur_thread s'b) s'b = Some (?etcb55 s'b obj' y etcb)
 2. \<And>s'b obj' y etcb. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; cur_thread s'b \<noteq> idle_thread s'b; get_etcb (cur_thread s'b) s'b = Some etcb\<rbrakk> \<Longrightarrow> cur_thread s'b \<noteq> idle_thread s'b
 3. \<And>s'b obj' y etcb. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; cur_thread s'b \<noteq> idle_thread s'b; get_etcb (cur_thread s'b) s'b = Some etcb; cdl_objects (transform s'b) (cur_thread s'b) = Some (transform_tcb (machine_state s'b) (cur_thread s'b) obj' (?etcb55 s'b obj' y etcb))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (do restart <- has_restart_cap y;
when restart (KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap)
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail) proof (prove)
goal (2 subgoals):
 1. \<And>s'b obj' y etcb. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; cur_thread s'b \<noteq> idle_thread s'b; get_etcb (cur_thread s'b) s'b = Some etcb\<rbrakk> \<Longrightarrow> cur_thread s'b \<noteq> idle_thread s'b
 2. \<And>s'b obj' y etcb. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; cur_thread s'b \<noteq> idle_thread s'b; get_etcb (cur_thread s'b) s'b = Some etcb; cdl_objects (transform s'b) (cur_thread s'b) = Some (transform_tcb (machine_state s'b) (cur_thread s'b) obj' etcb)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (do restart <- has_restart_cap y;
when restart (KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap)
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail) proof (prove)
goal (1 subgoal):
 1. \<And>s'b obj' y etcb. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; cdl_current_thread (transform s'b) = Some y; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; cur_thread s'b \<noteq> idle_thread s'b; get_etcb (cur_thread s'b) s'b = Some etcb; cdl_objects (transform s'b) (cur_thread s'b) = Some (transform_tcb (machine_state s'b) (cur_thread s'b) obj' etcb)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (do restart <- has_restart_cap y;
when restart (KHeap_D.set_cap (y, tcb_pending_op_slot) RunningCap)
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail) proof (prove)
goal (1 subgoal):
 1. \<And>s'b obj' etcb. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; cur_thread s'b \<noteq> idle_thread s'b; get_etcb (cur_thread s'b) s'b = Some etcb; cdl_objects (transform s'b) (cur_thread s'b) = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s'b) (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s'b) (cur_thread s'b) obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'b)) ((=) s'b) (do x <- get;
x <- assert_opt (cdl_objects x (cur_thread s'b));
t <- case x of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail;
when (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap) (KHeap_D.set_cap (cur_thread s'b, tcb_pending_op_slot) RunningCap)
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail) proof (prove)
goal (1 subgoal):
 1. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s'b) s'b = Some obj'; ct_in_state activatable s'b; invs s'b; valid_etcbs s'b; cur_thread s'b \<noteq> idle_thread s'b; get_etcb (cur_thread s'b) s'b = Some etcb; cdl_objects (transform s'b) (cur_thread s'b) = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s'b) (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s'b) (cur_thread s'b) obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); transform s'b = transform s'; s'b = s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do x <- assert_opt (cdl_objects (transform s') (cur_thread s'b));
t <- case x of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail;
when (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap) (KHeap_D.set_cap (cur_thread s'b, tcb_pending_op_slot) RunningCap)
od) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail) proof (prove)
goal (1 subgoal):
 1. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) proof (prove)
goal (8 subgoals):
 1. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = Running\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 2. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; inactive (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 3. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = Restart\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 4. \<And>s'b obj' etcb s' x41 x42. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 5. \<And>s'b obj' etcb s' x51 x52. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 6. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 7. \<And>s'b obj' etcb s' x7. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 8. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) proof (prove)
goal (6 subgoals):
 1. \<And>obj' etcb s'. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', 5) RunningCap) (do pc <- as_user (cur_thread s') getRestartPC;
y <- as_user (cur_thread s') (setNextPC pc);
set_thread_state (cur_thread s') Running
od)
 2. \<And>s'b obj' etcb s' x41 x42. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 3. \<And>s'b obj' etcb s' x51 x52. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 4. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 5. \<And>s'b obj' etcb s' x7. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 6. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) proof (prove)
goal (8 subgoals):
 1. \<And>obj' etcb s'. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> dcorres dc (?Q91 obj' etcb s') (?Q'91 obj' etcb s') (KHeap_D.set_cap (cur_thread s', 5) RunningCap) (do pc <- as_user (cur_thread s') getRestartPC;
y <- as_user (cur_thread s') (setNextPC pc);
set_thread_state (cur_thread s') Running
od)
 2. \<And>obj' etcb s' s. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj'); transform s' = s\<rbrakk> \<Longrightarrow> ?Q91 obj' etcb s' s
 3. \<And>obj' etcb s' s. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> ?Q'91 obj' etcb s' s
 4. \<And>s'b obj' etcb s' x41 x42. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 5. \<And>s'b obj' etcb s' x51 x52. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 6. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 7. \<And>s'b obj' etcb s' x7. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 8. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) proof (prove)
goal (10 subgoals):
 1. \<And>obj' etcb s' rv. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> dcorres dc (?Q91 obj' etcb s') (?Q'95 obj' etcb s' rv) (KHeap_D.set_cap (cur_thread s', 5) RunningCap) (do y <- as_user (cur_thread s') (setNextPC rv);
set_thread_state (cur_thread s') Running
od)
 2. \<And>obj' etcb s'. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'91 obj' etcb s'\<rbrace> as_user (cur_thread s') getRestartPC \<lbrace>?Q'95 obj' etcb s'\<rbrace>
 3. \<And>obj' etcb s' cs. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> as_user (cur_thread s') getRestartPC \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>obj' etcb s' s. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj'); transform s' = s\<rbrakk> \<Longrightarrow> ?Q91 obj' etcb s' s
 5. \<And>obj' etcb s' s. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> ?Q'91 obj' etcb s' s
 6. \<And>s'b obj' etcb s' x41 x42. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 7. \<And>s'b obj' etcb s' x51 x52. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 8. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 9. \<And>s'b obj' etcb s' x7. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 10. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) proof (prove)
goal (12 subgoals):
 1. \<And>obj' etcb s' rv rva. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> dcorres dc (?Q91 obj' etcb s') (?Q'99 obj' etcb s' rv rva) (KHeap_D.set_cap (cur_thread s', 5) RunningCap) (set_thread_state (cur_thread s') Running)
 2. \<And>obj' etcb s' rv. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'95 obj' etcb s' rv\<rbrace> as_user (cur_thread s') (setNextPC rv) \<lbrace>?Q'99 obj' etcb s' rv\<rbrace>
 3. \<And>obj' etcb s' rv cs. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> as_user (cur_thread s') (setNextPC rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>obj' etcb s'. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'91 obj' etcb s'\<rbrace> as_user (cur_thread s') getRestartPC \<lbrace>?Q'95 obj' etcb s'\<rbrace>
 5. \<And>obj' etcb s' cs. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> as_user (cur_thread s') getRestartPC \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>obj' etcb s' s. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj'); transform s' = s\<rbrakk> \<Longrightarrow> ?Q91 obj' etcb s' s
 7. \<And>obj' etcb s' s. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> ?Q'91 obj' etcb s' s
 8. \<And>s'b obj' etcb s' x41 x42. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 9. \<And>s'b obj' etcb s' x51 x52. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 10. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>obj' etcb s' rv. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'95 obj' etcb s' rv\<rbrace> as_user (cur_thread s') (setNextPC rv) \<lbrace>\<lambda>r. not_idle_thread (cur_thread s') and K (RunningCap = infer_tcb_pending_op (cur_thread s') Running) and valid_etcbs\<rbrace>
 2. \<And>obj' etcb s' rv cs. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> as_user (cur_thread s') (setNextPC rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>obj' etcb s'. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'91 obj' etcb s'\<rbrace> as_user (cur_thread s') getRestartPC \<lbrace>?Q'95 obj' etcb s'\<rbrace>
 4. \<And>obj' etcb s' cs. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> as_user (cur_thread s') getRestartPC \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>obj' etcb s' s. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj'); transform s' = s\<rbrakk> \<Longrightarrow> True
 6. \<And>obj' etcb s' s. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> ?Q'91 obj' etcb s' s
 7. \<And>s'b obj' etcb s' x41 x42. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 8. \<And>s'b obj' etcb s' x51 x52. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 9. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 10. \<And>s'b obj' etcb s' x7. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>obj' etcb s' rv. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'95 obj' etcb s' rv\<rbrace> as_user (cur_thread s') (setNextPC rv) \<lbrace>\<lambda>r. not_idle_thread (cur_thread s') and valid_etcbs\<rbrace>
 2. \<And>obj' etcb s' rv cs. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> as_user (cur_thread s') (setNextPC rv) \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>obj' etcb s'. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'91 obj' etcb s'\<rbrace> as_user (cur_thread s') getRestartPC \<lbrace>?Q'95 obj' etcb s'\<rbrace>
 4. \<And>obj' etcb s' cs. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> as_user (cur_thread s') getRestartPC \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>obj' etcb s' s. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj'); transform s' = s\<rbrakk> \<Longrightarrow> True
 6. \<And>obj' etcb s' s. \<lbrakk>invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s' (cur_thread s') = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> ?Q'91 obj' etcb s' s
 7. \<And>s'b obj' etcb s' x41 x42. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 8. \<And>s'b obj' etcb s' x51 x52. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 9. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 10. \<And>s'b obj' etcb s' x7. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
A total of 11 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>obj' etcb s. \<lbrakk>invs s; valid_etcbs s; cur_thread s \<noteq> idle_thread s; get_etcb (cur_thread s) s = Some etcb; cdl_objects (transform s) (cur_thread s) = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s) (cur_thread s) obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); tcb_state obj' = Restart; kheap s (cur_thread s) = Some (TCB obj')\<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s
 2. \<And>s'b obj' etcb s' x41 x42. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 3. \<And>s'b obj' etcb s' x51 x52. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 4. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 5. \<And>s'b obj' etcb s' x7. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 6. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) proof (prove)
goal (5 subgoals):
 1. \<And>s'b obj' etcb s' x41 x42. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 2. \<And>s'b obj' etcb s' x51 x52. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 3. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; awaiting_reply (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 4. \<And>s'b obj' etcb s' x7. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; tcb_state obj' = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)))
 5. \<And>s'b obj' etcb s'. \<lbrakk>get_tcb (cur_thread s') s' = Some obj'; ct_in_state activatable s'; invs s'; valid_etcbs s'; cur_thread s' \<noteq> idle_thread s'; get_etcb (cur_thread s') s' = Some etcb; cdl_objects (transform s') (cur_thread s') = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op (cur_thread s') (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (cur_thread s') obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>); s'b = s'; idle (tcb_state obj')\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> (infer_tcb_bound_notification (tcb_bound_notification obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_boundntfn_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_bound_notification (tcb_bound_notification obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') = RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) RunningCap) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail)) \<and> (infer_tcb_pending_op (cur_thread s') (tcb_state obj') \<noteq> RestartCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (case tcb_state obj' of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user (cur_thread s'b) getRestartPC;
y <- as_user (cur_thread s'b) (setNextPC pc);
set_thread_state (cur_thread s'b) Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread (cur_thread s'b) | _ \<Rightarrow> fail))) proof (prove)
goal:
No subgoals!