theory Ipc_DR

lemma block_thread_on_send_corres:
  "dcorres dc \<top> (not_idle_thread thread and valid_etcbs)
           (KHeap_D.set_cap (thread, tcb_pending_op_slot)
             (PendingSyncSendCap epptr badge call can_grant can_grant_reply
               False))
           (set_thread_state thread
             (Structures_A.thread_state.BlockedOnSend epptr
               \<lparr>sender_badge = badge, sender_can_grant = can_grant,
                sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))" apply (clarsimp simp:KHeap_D.set_cap_def set_thread_state_def) apply (rule dcorres_gets_the, clarsimp) apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres]) apply (frule(1) valid_etcbs_get_tcb_get_etcb, clarsimp) apply (clarsimp simp: obj_at_def not_idle_thread_def opt_object_tcb assert_def
                         transform_tcb_def has_slots_def split: option.splits) 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_objects_def transform_current_thread_def) apply (rule ext) apply (clarsimp simp: |rule conjI)+ apply (fastforce dest!: get_tcb_SomeD get_etcb_SomeD
                      simp: transform_tcb_def infer_tcb_pending_op_def tcb_slot_defs) apply (clarsimp simp:restrict_map_def map_add_def) 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) (not_idle_thread thread and valid_etcbs) (KHeap_D.set_cap (thread, tcb_pending_op_slot) (PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) (set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread 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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some (PendingSyncSendCap epptr badge call can_grant can_grant_reply False) 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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj)) >>= KHeap_D.set_object thread
od) (do tcb <- gets_the (get_tcb thread);
y <- KHeap_A.set_object thread (TCB (update_tcb_state (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) tcb));
set_thread_state_ext thread
od) proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>get_tcb thread s' = Some obj'; cdl_objects (transform s') thread = Some obj; not_idle_thread thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some (PendingSyncSendCap epptr badge call can_grant can_grant_reply False) 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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj)) >>= KHeap_D.set_object thread
od) (do y <- KHeap_A.set_object thread (TCB (update_tcb_state (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) obj'));
set_thread_state_ext thread
od)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread 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'. \<lbrakk>get_tcb thread s' = Some obj'; cdl_objects (transform s') thread = Some obj; not_idle_thread thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some (PendingSyncSendCap epptr badge call can_grant can_grant_reply False) 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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj)) >>= KHeap_D.set_object thread
od) (KHeap_A.set_object thread (TCB (update_tcb_state (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread 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'; 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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some (PendingSyncSendCap epptr badge call can_grant can_grant_reply False) 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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) obj)) >>= KHeap_D.set_object thread
od) (KHeap_A.set_object thread (TCB (update_tcb_state (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread 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'; 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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) (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 (PendingSyncSendCap epptr badge call can_grant can_grant_reply False) 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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) (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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) (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 (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread 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'; 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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False], 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 (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) obj')))
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread 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'; 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 (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) 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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False], 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 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'; valid_etcbs s'; get_etcb thread s' = Some etcb; kheap s' thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) (if ptr = thread then Some (TCB (update_tcb_state (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) obj')) else (kheap s' |` (- {idle_thread s'} - {thread})) ptr)) = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) ((kheap s' |` (- {idle_thread s'})) ptr)))(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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False], 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 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'; valid_etcbs s'; get_etcb thread s' = Some etcb; kheap s' thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) (if ptr = thread then Some (TCB (update_tcb_state (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) obj')) else (kheap s' |` (- {idle_thread s'} - {thread})) ptr))) x = (((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) ((kheap s' |` (- {idle_thread s'})) ptr)))(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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False], 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 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. \<lbrakk>get_tcb thread s' = Some obj'; thread \<noteq> idle_thread s'; valid_etcbs s'; get_etcb thread s' = Some etcb; kheap s' thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (case ekheap s' thread of Some x \<Rightarrow> transform_tcb (machine_state s') thread (update_tcb_state (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) 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> PendingSyncSendCap epptr badge call can_grant can_grant_reply False], 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' obj' etcb tcb x. \<lbrakk>get_tcb thread s' = Some obj'; thread \<noteq> idle_thread s'; valid_etcbs s'; get_etcb thread s' = Some etcb; kheap s' thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> x \<noteq> thread \<longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) (if ptr = thread then Some (TCB (update_tcb_state (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) obj')) else (kheap s' |` (- {idle_thread s'} - {thread})) ptr))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) ((kheap s' |` (- {idle_thread s'})) ptr))) x
 3. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread 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'; valid_etcbs s'; get_etcb thread s' = Some etcb; kheap s' thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> x \<noteq> thread \<longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) (if ptr = thread then Some (TCB (update_tcb_state (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>) obj')) else (kheap s' |` (- {idle_thread s'} - {thread})) ptr))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) ((kheap s' |` (- {idle_thread s'})) ptr))) x
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (not_idle_thread 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 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. \<lbrakk>get_tcb thread s' = Some y; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') thread = Some y proof (prove)
goal:
No subgoals!