theory Tcb_DR

lemma dcorres_set_thread_state_Restart2:
  "dcorres dc (\<lambda>_. True)
   (\<lambda>a. valid_mdb a \<and> not_idle_thread recver a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a)
   (KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap)
   (set_thread_state recver Structures_A.thread_state.Restart)" apply (simp add:KHeap_D.set_cap_def set_thread_state_def) apply (rule dcorres_gets_the) apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb, clarsimp) apply (frule opt_object_tcb, simp) apply (clarsimp simp:not_idle_thread_def) apply (clarsimp simp:transform_tcb_def has_slots_def update_slots_def object_slots_def tcb_slots) apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres]) apply (rule dcorres_set_object_tcb) apply (clarsimp simp:transform_tcb_def infer_tcb_pending_op_def tcb_slots) apply (rule conjI, fastforce) apply (clarsimp simp:get_etcb_SomeD) apply (simp add:not_idle_thread_def) apply (clarsimp simp:get_tcb_SomeD) apply (clarsimp simp:get_etcb_SomeD) apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb) apply (fastforce simp:not_idle_thread_def dest!:opt_object_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>a. valid_mdb a \<and> not_idle_thread recver a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a) (KHeap_D.set_cap (recver, tcb_pending_op_slot) RestartCap) (set_thread_state recver Restart) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>a. valid_mdb a \<and> not_idle_thread recver a \<and> st_tcb_at idle (idle_thread a) a \<and> valid_etcbs a) (do obj <- KHeap_D.get_object recver;
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some RestartCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj)) >>= KHeap_D.set_object recver
od) (do tcb <- gets_the (get_tcb recver);
y <- KHeap_A.set_object recver (TCB (update_tcb_state Restart tcb));
set_thread_state_ext recver
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s' obj obj'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' = Some obj'; cdl_objects s recver = Some obj\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (do y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some RestartCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj)) >>= KHeap_D.set_object recver
od) (do y <- KHeap_A.set_object recver (TCB (update_tcb_state Restart obj'));
set_thread_state_ext recver
od)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; cdl_objects (transform s') recver = Some obj; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some RestartCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj)) >>= KHeap_D.set_object recver
od) (do y <- KHeap_A.set_object recver (TCB (update_tcb_state Restart obj'));
set_thread_state_ext recver
od)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; cdl_objects (transform s') recver = Some obj; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb\<rbrakk> \<Longrightarrow> recver \<noteq> idle_thread s'
 2. \<And>s' obj obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; cdl_objects (transform s') recver = Some obj; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (transform_tcb (machine_state s') recver obj' etcb)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some RestartCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj)) >>= KHeap_D.set_object recver
od) (do y <- KHeap_A.set_object recver (TCB (update_tcb_state Restart obj'));
set_thread_state_ext recver
od)
 3. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; cdl_objects (transform s') recver = Some obj; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (transform_tcb (machine_state s') recver obj' etcb)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some RestartCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj)) >>= KHeap_D.set_object recver
od) (do y <- KHeap_A.set_object recver (TCB (update_tcb_state Restart obj'));
set_thread_state_ext recver
od)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver 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')) ((=) s') (KHeap_D.set_object recver (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj'), 5 \<mapsto> RestartCap], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) (do y <- KHeap_A.set_object recver (TCB (update_tcb_state Restart obj'));
set_thread_state_ext recver
od)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver 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')) ((=) s') (KHeap_D.set_object recver (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj'), 5 \<mapsto> RestartCap], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) (KHeap_A.set_object recver (TCB (update_tcb_state Restart obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>etcb'. transform_tcb (machine_state s') recver (update_tcb_state Restart obj') etcb' = Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj'), 5 \<mapsto> RestartCap], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr> \<and> ekheap s' recver = Some etcb'
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> recver \<noteq> idle_thread s'
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> kheap s' recver \<noteq> None
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> ekheap s' recver \<noteq> None
 5. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> case tcb_state obj' of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap recver True False | BlockedOnNotification ptr \<Rightarrow> PendingNtfnRecvCap ptr | _ \<Rightarrow> cdl_cap.NullCap, 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> RestartCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')] = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj'), 5 \<mapsto> RestartCap] \<and> (\<exists>etcb'. tcb_domain etcb' = tcb_domain etcb \<and> ekheap s' recver = Some etcb')
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> recver \<noteq> idle_thread s'
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> kheap s' recver \<noteq> None
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> ekheap s' recver \<noteq> None
 5. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> case tcb_state obj' of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap recver True False | BlockedOnNotification ptr \<Rightarrow> PendingNtfnRecvCap ptr | _ \<Rightarrow> cdl_cap.NullCap, 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>etcb'. tcb_domain etcb' = tcb_domain etcb \<and> ekheap s' recver = Some etcb'
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> recver \<noteq> idle_thread s'
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> kheap s' recver \<noteq> None
 4. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> ekheap s' recver \<noteq> None
 5. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> recver \<noteq> idle_thread s'
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> kheap s' recver \<noteq> None
 3. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> ekheap s' recver \<noteq> None
 4. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> kheap s' recver \<noteq> None
 2. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> ekheap s' recver \<noteq> None
 3. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb recver s' = Some obj'; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; get_etcb recver s' = Some etcb; cdl_objects (transform s') recver = Some (Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable obj'), Suc 0 \<mapsto> transform_cap (tcb_vtable obj'), 2 \<mapsto> transform_cap (tcb_reply obj'), 3 \<mapsto> transform_cap (tcb_caller obj'), 4 \<mapsto> transform_cap (tcb_ipcframe obj'), 5 \<mapsto> infer_tcb_pending_op recver (tcb_state obj'), 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') recver obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> ekheap s' recver \<noteq> None
 2. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; valid_mdb s' \<and> not_idle_thread recver s' \<and> st_tcb_at idle (idle_thread s') s' \<and> valid_etcbs s'; get_tcb recver s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s recver \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>s' y. \<lbrakk>get_tcb recver s' = Some y; valid_mdb s'; not_idle_thread recver s'; st_tcb_at idle (idle_thread s') s'; valid_etcbs s'; \<exists>etcb. get_etcb recver s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') recver = Some y proof (prove)
goal:
No subgoals!