theory KHeap_DR

lemma set_boundntfn_cap_corres:
  "dcorres dc (\<lambda>_. True)
   (not_idle_thread y and ko_at (TCB obj) y and K (cap = infer_tcb_bound_notification ntfn_opt) and
    valid_etcbs)
   (KHeap_D.set_cap (y, tcb_boundntfn_slot) cap)
   (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj)))" apply (simp add: KHeap_D.set_cap_def gets_def gets_the_def bind_assoc not_idle_thread_def) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: obj_at_def) apply (drule(1) valid_etcbs_tcb_etcb, clarsimp) apply (frule opt_object_tcb[rotated, rotated]) apply (fastforce simp: get_tcb_def) apply (fastforce simp: get_etcb_rev) apply (clarsimp simp: assert_opt_def has_slots_def
    transform_tcb_def object_slots_def update_slots_def tcb_slots) apply (clarsimp simp: corres_underlying_def in_monad
    set_object_def KHeap_D.set_object_def get_object_def simpler_modify_def) apply (simp add: transform_def transform_current_thread_def) apply (rule ext) apply (subst transform_objects_update_kheap_same_caps) apply ((simp add: obj_at_def transform_tcb_def
       not_generates_pending_is_null tcb_slots)+)[3] apply (auto simp: obj_at_def not_generates_pending_is_null transform_tcb_def tcb_slots) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread y and ko_at (TCB obj) y and K (cap = infer_tcb_bound_notification ntfn_opt) and valid_etcbs) (KHeap_D.set_cap (y, tcb_boundntfn_slot) cap) (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj))) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) ((\<lambda>s. y \<noteq> idle_thread s) and ko_at (TCB obj) y and (\<lambda>y. cap = infer_tcb_bound_notification ntfn_opt) and valid_etcbs) (do x <- get;
obj <- assert_opt (cdl_objects x y);
ya <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> cap)) obj of Tcb t \<Rightarrow> if tcb_boundntfn_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_boundntfn_slot \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> cap)) obj)) >>= KHeap_D.set_object y
od) (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; ((\<lambda>s. y \<noteq> idle_thread s) and ko_at (TCB obj) y and (\<lambda>y. cap = infer_tcb_bound_notification ntfn_opt) and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') y);
ya <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> cap)) obj of Tcb t \<Rightarrow> if tcb_boundntfn_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_boundntfn_slot \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> cap)) obj)) >>= KHeap_D.set_object y
od) (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); valid_etcbs s'; cap = infer_tcb_bound_notification ntfn_opt\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') y);
ya <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj of Tcb t \<Rightarrow> if tcb_boundntfn_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_boundntfn_slot \<noteq> Some (infer_tcb_bound_notification ntfn_opt) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj)) >>= KHeap_D.set_object y
od) (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj))) proof (prove)
goal (1 subgoal):
 1. \<And>s' etcb. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') y);
ya <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj of Tcb t \<Rightarrow> if tcb_boundntfn_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_boundntfn_slot \<noteq> Some (infer_tcb_bound_notification ntfn_opt) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj)) >>= KHeap_D.set_object y
od) (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj))) proof (prove)
goal (3 subgoals):
 1. \<And>s' etcb. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb\<rbrakk> \<Longrightarrow> get_tcb y s' = Some (?tcb14 s' etcb)
 2. \<And>s' etcb. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb\<rbrakk> \<Longrightarrow> get_etcb y s' = Some (?etcb14 s' etcb)
 3. \<And>s' etcb. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; cdl_objects (transform s') y = Some (transform_tcb (machine_state s') y (?tcb14 s' etcb) (?etcb14 s' etcb))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') y);
ya <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj of Tcb t \<Rightarrow> if tcb_boundntfn_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_boundntfn_slot \<noteq> Some (infer_tcb_bound_notification ntfn_opt) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj)) >>= KHeap_D.set_object y
od) (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj))) proof (prove)
goal (2 subgoals):
 1. \<And>s' etcb. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb\<rbrakk> \<Longrightarrow> get_etcb y s' = Some (?etcb14 s' etcb)
 2. \<And>s' etcb. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; cdl_objects (transform s') y = Some (transform_tcb (machine_state s') y obj (?etcb14 s' etcb))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') y);
ya <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj of Tcb t \<Rightarrow> if tcb_boundntfn_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_boundntfn_slot \<noteq> Some (infer_tcb_bound_notification ntfn_opt) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj)) >>= KHeap_D.set_object y
od) (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj))) proof (prove)
goal (1 subgoal):
 1. \<And>s' etcb. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; cdl_objects (transform s') y = Some (transform_tcb (machine_state s') y obj etcb)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') y);
ya <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj of Tcb t \<Rightarrow> if tcb_boundntfn_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_boundntfn_slot \<noteq> Some (infer_tcb_bound_notification ntfn_opt) then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification ntfn_opt)) obj)) >>= KHeap_D.set_object y
od) (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj))) proof (prove)
goal (1 subgoal):
 1. \<And>s' etcb. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; cdl_objects (transform s') y = 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 y (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') y 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 y (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 y (tcb_state obj), 6 \<mapsto> infer_tcb_bound_notification ntfn_opt], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj), cdl_tcb_intent = transform_full_intent (machine_state s') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) (KHeap_A.set_object y (TCB (update_tcb_boundntfn ntfn_opt obj))) proof (prove)
goal (1 subgoal):
 1. \<And>s' etcb. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; cdl_objects (transform s') y = 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 y (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') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s')(y \<mapsto> TCB (update_tcb_boundntfn ntfn_opt obj))) s') = dupdate_cdl_object y (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 y (tcb_state obj), 6 \<mapsto> infer_tcb_bound_notification ntfn_opt], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj), cdl_tcb_intent = transform_full_intent (machine_state s') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) (transform s') proof (prove)
goal (1 subgoal):
 1. \<And>s' etcb. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; transform_objects s' y = 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 y (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') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(y \<mapsto> TCB (update_tcb_boundntfn ntfn_opt obj))) s') = (transform_objects s')(y \<mapsto> 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 y (tcb_state obj), 6 \<mapsto> infer_tcb_bound_notification ntfn_opt], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj), cdl_tcb_intent = transform_full_intent (machine_state s') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s' etcb x. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; transform_objects s' y = 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 y (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') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(y \<mapsto> TCB (update_tcb_boundntfn ntfn_opt obj))) s') x = ((transform_objects s')(y \<mapsto> 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 y (tcb_state obj), 6 \<mapsto> infer_tcb_bound_notification ntfn_opt], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj), cdl_tcb_intent = transform_full_intent (machine_state s') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) x proof (prove)
goal (4 subgoals):
 1. \<And>s' etcb x. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; transform_objects s' y = 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 y (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') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> kheap s' y = Some (?ko45 s' etcb x)
 2. \<And>s' etcb x. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; transform_objects s' y = 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 y (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') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> caps_of_object (TCB (update_tcb_boundntfn ntfn_opt obj)) = caps_of_object (?ko45 s' etcb x)
 3. \<And>s' etcb x. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; transform_objects s' y = 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 y (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') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> a_type (TCB (update_tcb_boundntfn ntfn_opt obj)) = a_type (?ko45 s' etcb x)
 4. \<And>s' etcb x. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; transform_objects s' y = 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 y (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') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> (if y = idle_thread s' then transform_objects (update_kheap (kheap s') s') else (transform_objects (update_kheap (kheap s') s'))(y \<mapsto> transform_object (machine_state s') y (ekheap s' y) (TCB (update_tcb_boundntfn ntfn_opt obj)))) x = ((transform_objects s')(y \<mapsto> 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 y (tcb_state obj), 6 \<mapsto> infer_tcb_bound_notification ntfn_opt], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj), cdl_tcb_intent = transform_full_intent (machine_state s') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) x proof (prove)
goal (1 subgoal):
 1. \<And>s' etcb x. \<lbrakk>y \<noteq> idle_thread s'; kheap s' y = Some (TCB obj); cap = infer_tcb_bound_notification ntfn_opt; ekheap s' y = Some etcb; transform_objects s' y = 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 y (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') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> (if y = idle_thread s' then transform_objects (update_kheap (kheap s') s') else (transform_objects (update_kheap (kheap s') s'))(y \<mapsto> transform_object (machine_state s') y (ekheap s' y) (TCB (update_tcb_boundntfn ntfn_opt obj)))) x = ((transform_objects s')(y \<mapsto> 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 y (tcb_state obj), 6 \<mapsto> infer_tcb_bound_notification ntfn_opt], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler obj), cdl_tcb_intent = transform_full_intent (machine_state s') y obj, cdl_tcb_has_fault = \<exists>y. tcb_fault obj = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) x proof (prove)
goal:
No subgoals!