theory Ipc_DR

lemma set_thread_state_block_on_notification_corres:
    "dcorres dc \<top>
     (not_idle_thread thread and tcb_at thread and valid_etcbs)
     (block_thread_on_ipc thread (PendingNtfnRecvCap w))
     (set_thread_state thread (Structures_A.thread_state.BlockedOnNotification w))" apply (simp add: block_thread_on_ipc_def) apply (clarsimp simp: KHeap_D.set_cap_def set_thread_state_def) apply (rule dcorres_dc_rhs_noop_below_2_True[OF allI[OF set_thread_state_ext_dcorres]]) apply (rule dcorres_gets_the) apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb, clarsimp) apply (clarsimp simp: not_idle_thread_def opt_object_tcb assert_def transform_tcb_def has_slots_def) apply (clarsimp simp: update_slots_def object_slots_def) apply (clarsimp simp: set_object_def get_object_def in_monad simpler_modify_def KHeap_D.set_object_def
                         get_def put_def bind_def corres_underlying_def return_def) apply (clarsimp simp: transform_def transform_current_thread_def) apply (intro ext conjI) apply (case_tac x) apply (clarsimp simp: |rule conjI)+ apply (clarsimp simp: transform_tcb_def transform_objects_def infer_tcb_pending_op_def) apply ((fastforce simp: transform_objects_def restrict_map_def map_add_def tcb_at_def
                               transform_tcb_def tcb_slot_defs
                       dest!: get_tcb_SomeD get_etcb_SomeD)+)[2] apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb, clarsimp) apply (fastforce simp: not_idle_thread_def dest!:opt_object_tcb get_tcb_rev get_etcb_rev) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread thread and tcb_at thread and valid_etcbs) (block_thread_on_ipc thread (PendingNtfnRecvCap w)) (set_thread_state thread (BlockedOnNotification w)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread thread and tcb_at thread and valid_etcbs) (KHeap_D.set_cap (thread, tcb_pending_op_slot) (PendingNtfnRecvCap w)) (set_thread_state thread (BlockedOnNotification w)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread thread and tcb_at thread and valid_etcbs) (do obj <- KHeap_D.get_object thread;
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some (PendingNtfnRecvCap w) 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> PendingNtfnRecvCap w)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w)) obj)) >>= KHeap_D.set_object thread
od) (do tcb <- gets_the (get_tcb thread);
y <- KHeap_A.set_object thread (TCB (update_tcb_state (BlockedOnNotification w) tcb));
set_thread_state_ext thread
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread thread and tcb_at thread and valid_etcbs) (do obj <- KHeap_D.get_object thread;
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some (PendingNtfnRecvCap w) 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> PendingNtfnRecvCap w)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w)) obj)) >>= KHeap_D.set_object thread
od) (do x <- gets_the (get_tcb thread);
KHeap_A.set_object thread (TCB (update_tcb_state (BlockedOnNotification w) x))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s' obj obj'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; cdl_objects s thread = 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> PendingNtfnRecvCap w)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some (PendingNtfnRecvCap w) 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> PendingNtfnRecvCap w)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w)) obj)) >>= KHeap_D.set_object thread
od) (KHeap_A.set_object thread (TCB (update_tcb_state (BlockedOnNotification w) obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; cdl_objects (transform s') thread = Some obj; not_idle_thread thread s'; tcb_at thread s'; valid_etcbs s'; get_etcb thread 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> PendingNtfnRecvCap w)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some (PendingNtfnRecvCap w) 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> PendingNtfnRecvCap w)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w)) obj)) >>= KHeap_D.set_object thread
od) (KHeap_A.set_object thread (TCB (update_tcb_state (BlockedOnNotification w) obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; thread \<noteq> idle_thread s'; tcb_at thread s'; valid_etcbs s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') ((case update_slots ((object_slots (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 thread (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') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>))(tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w)) (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 thread (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') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots (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 thread (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') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) tcb_pending_op_slot \<noteq> Some (PendingNtfnRecvCap w) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots (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 thread (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') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>))(tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w)) (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 thread (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') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) | _ \<Rightarrow> return (update_slots ((object_slots (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 thread (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') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>))(tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w)) (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 thread (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') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>))) >>= KHeap_D.set_object thread) (KHeap_A.set_object thread (TCB (update_tcb_state (BlockedOnNotification w) obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>get_tcb thread s' = Some obj'; thread \<noteq> idle_thread s'; tcb_at thread s'; valid_etcbs s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_object thread (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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj'), tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) (KHeap_A.set_object thread (TCB (update_tcb_state (BlockedOnNotification w) obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' etcb tcb. \<lbrakk>get_tcb thread s' = Some obj'; thread \<noteq> idle_thread s'; tcb_at thread s'; valid_etcbs s'; get_etcb thread s' = Some etcb; kheap s' thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s')(thread \<mapsto> TCB (update_tcb_state (BlockedOnNotification w) obj'))) s') = dupdate_cdl_object thread (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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj'), tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) (transform s')
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' etcb tcb. \<lbrakk>get_tcb thread s' = Some obj'; thread \<noteq> idle_thread s'; tcb_at thread s'; valid_etcbs s'; get_etcb thread s' = Some etcb; kheap s' thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(thread \<mapsto> TCB (update_tcb_state (BlockedOnNotification w) obj'))) s') = (transform_objects s')(thread \<mapsto> 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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj'), tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' etcb tcb x. \<lbrakk>get_tcb thread s' = Some obj'; thread \<noteq> idle_thread s'; tcb_at thread s'; valid_etcbs s'; get_etcb thread s' = Some etcb; kheap s' thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(thread \<mapsto> TCB (update_tcb_state (BlockedOnNotification w) obj'))) s') x = ((transform_objects s')(thread \<mapsto> 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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj'), tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) x
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' etcb tcb x n. \<lbrakk>get_tcb thread s' = Some obj'; thread \<noteq> idle_thread s'; tcb_at thread s'; valid_etcbs s'; get_etcb thread s' = Some etcb; kheap s' thread = Some (TCB tcb); x = word_of_nat n; n < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(thread \<mapsto> TCB (update_tcb_state (BlockedOnNotification w) obj'))) s') x = ((transform_objects s')(thread \<mapsto> 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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj'), tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') thread obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) x
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s' obj' etcb tcb n. \<lbrakk>get_tcb (word_of_nat n) s' = Some obj'; word_of_nat n \<noteq> idle_thread s'; tcb_at (word_of_nat n) s'; valid_etcbs s'; get_etcb (word_of_nat n) s' = Some etcb; kheap s' (word_of_nat n) = Some (TCB tcb); n < 4294967296; thread = word_of_nat n\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(word_of_nat n \<mapsto> TCB (update_tcb_state (BlockedOnNotification w) obj'))) s') (word_of_nat n) = 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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj'), tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (word_of_nat n) obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)
 2. \<And>s' obj' etcb tcb n. \<lbrakk>get_tcb thread s' = Some obj'; thread \<noteq> idle_thread s'; tcb_at thread s'; valid_etcbs s'; get_etcb thread s' = Some etcb; kheap s' thread = Some (TCB tcb); n < 4294967296\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> thread \<longrightarrow> transform_objects (update_kheap ((kheap s')(thread \<mapsto> TCB (update_tcb_state (BlockedOnNotification w) obj'))) s') (word_of_nat n) = transform_objects s' (word_of_nat n)
 3. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s' obj' etcb tcb n. \<lbrakk>get_tcb (word_of_nat n) s' = Some obj'; word_of_nat n \<noteq> idle_thread s'; tcb_at (word_of_nat n) s'; valid_etcbs s'; get_etcb (word_of_nat n) s' = Some etcb; kheap s' (word_of_nat n) = Some (TCB tcb); n < 4294967296; thread = word_of_nat n\<rbrakk> \<Longrightarrow> (case ekheap s' (word_of_nat n) of Some x \<Rightarrow> transform_tcb (machine_state s') (word_of_nat n) (update_tcb_state (BlockedOnNotification w) obj') x) = 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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj'), tcb_pending_op_slot \<mapsto> PendingNtfnRecvCap w], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj'), cdl_tcb_intent = transform_full_intent (machine_state s') (word_of_nat n) obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>
 2. \<And>s' obj' etcb tcb n. \<lbrakk>get_tcb thread s' = Some obj'; thread \<noteq> idle_thread s'; tcb_at thread s'; valid_etcbs s'; get_etcb thread s' = Some etcb; kheap s' thread = Some (TCB tcb); n < 4294967296\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> thread \<longrightarrow> transform_objects (update_kheap ((kheap s')(thread \<mapsto> TCB (update_tcb_state (BlockedOnNotification w) obj'))) s') (word_of_nat n) = transform_objects s' (word_of_nat n)
 3. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread thread and tcb_at thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s thread \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>s' y etcb. \<lbrakk>get_tcb thread s' = Some y; not_idle_thread thread s'; tcb_at thread s'; valid_etcbs s'; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') thread = Some y proof (prove)
goal:
No subgoals!