theory Intent_DR

lemma corrupt_frame_include_self':
assumes corres:"dcorres dc \<top> P (do corrupt_frame buf; corrupt_tcb_intent y od) g"
assumes imp:"\<And>s. P s\<Longrightarrow> ipc_frame_ptr_at buf y s \<and> not_idle_thread y s \<and> valid_etcbs s"
shows "dcorres dc \<top> P (corrupt_frame buf) g" using corres apply (clarsimp simp:corres_underlying_def bind_def) apply (frule imp) apply (erule allE, erule (1) impE) apply (drule_tac x = "(a,ba)" in bspec) apply simp+ apply (clarsimp) apply (rule_tac x = "((),transform ba)" in bexI) apply simp+ apply (clarsimp simp:corrupt_frame_def select_def bind_def simpler_modify_def) apply (clarsimp simp:corrupt_tcb_intent_def update_thread_def
    select_def gets_the_def KHeap_D.set_object_def
    bind_def gets_def get_def return_def assert_opt_def
    fail_def simpler_modify_def split:option.splits) apply (rule_tac x = "\<lambda>t. if t = y then T else x t" for T in exI) apply (clarsimp simp:corrupt_intents_def transform_def not_idle_thread_def
                       restrict_map_def map_add_def ipc_frame_wp_at_def obj_at_def
                  split:option.split_asm cdl_object.split_asm) apply (rule ext) apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def tcb_ipcframe_id_def tcb_pending_op_slot_def
                        transform_object_def not_idle_thread_def transform_tcb_def tcb_ipcbuffer_slot_def) apply (clarsimp simp: transform_objects_def) apply (clarsimp split:cap.splits arch_cap.splits) apply (drule(1) valid_etcbs_tcb_etcb) by (fastforce simp: transform_tcb_def tcb_ipcframe_id_def tcb_pending_op_slot_def
                      tcb_ipcbuffer_slot_def tcb_boundntfn_slot_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) P (corrupt_frame buf) g proof (prove)
using this:
dcorres dc (\<lambda>_. True) P (do corrupt_frame buf;
corrupt_tcb_intent y
od) g

goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) P (corrupt_frame buf) g proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>\<forall>b. P b \<longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> \<exists>ya\<in>fst (corrupt_frame buf (transform b)). \<exists>x\<in>fst (case ya of (ya, x) \<Rightarrow> corrupt_tcb_intent y x). case x of (r, x) \<Rightarrow> transform t' = x); P b; (a, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (corrupt_frame buf (transform b)). case x of (r, x) \<Rightarrow> transform ba = x proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>\<forall>b. P b \<longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> \<exists>ya\<in>fst (corrupt_frame buf (transform b)). \<exists>x\<in>fst (case ya of (ya, x) \<Rightarrow> corrupt_tcb_intent y x). case x of (r, x) \<Rightarrow> transform t' = x); P b; (a, ba) \<in> fst (g b); ipc_frame_ptr_at buf y b \<and> not_idle_thread y b \<and> valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (corrupt_frame buf (transform b)). case x of (r, x) \<Rightarrow> transform ba = x proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>P b; (a, ba) \<in> fst (g b); ipc_frame_ptr_at buf y b \<and> not_idle_thread y b \<and> valid_etcbs b; \<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> \<exists>ya\<in>fst (corrupt_frame buf (transform b)). \<exists>x\<in>fst (case ya of (ya, x) \<Rightarrow> corrupt_tcb_intent y x). case x of (r, x) \<Rightarrow> transform t' = x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (corrupt_frame buf (transform b)). case x of (r, x) \<Rightarrow> transform ba = x proof (prove)
goal (2 subgoals):
 1. \<And>b a ba. \<lbrakk>P b; (a, ba) \<in> fst (g b); ipc_frame_ptr_at buf y b \<and> not_idle_thread y b \<and> valid_etcbs b\<rbrakk> \<Longrightarrow> (a, ba) \<in> fst (g b)
 2. \<And>b a ba. \<lbrakk>P b; (a, ba) \<in> fst (g b); ipc_frame_ptr_at buf y b \<and> not_idle_thread y b \<and> valid_etcbs b; case (a, ba) of (r', t') \<Rightarrow> \<exists>ya\<in>fst (corrupt_frame buf (transform b)). \<exists>x\<in>fst (case ya of (ya, x) \<Rightarrow> corrupt_tcb_intent y x). case x of (r, x) \<Rightarrow> transform t' = x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (corrupt_frame buf (transform b)). case x of (r, x) \<Rightarrow> transform ba = x proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>P b; (a, ba) \<in> fst (g b); ipc_frame_ptr_at buf y b \<and> not_idle_thread y b \<and> valid_etcbs b; \<exists>ya\<in>fst (corrupt_frame buf (transform b)). \<exists>x\<in>fst (case ya of (ya, x) \<Rightarrow> corrupt_tcb_intent y x). case x of (r, x) \<Rightarrow> transform ba = x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (corrupt_frame buf (transform b)). case x of (r, x) \<Rightarrow> transform ba = x proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb. \<lbrakk>P b; (a, ba) \<in> fst (g b); ((), bb) \<in> fst (corrupt_frame buf (transform b)); ((), transform ba) \<in> fst (corrupt_tcb_intent y bb); ipc_frame_ptr_at buf y b; not_idle_thread y b; valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (corrupt_frame buf (transform b)). case x of (r, x) \<Rightarrow> transform ba = x proof (prove)
goal (2 subgoals):
 1. \<And>b a ba bb. \<lbrakk>P b; (a, ba) \<in> fst (g b); ((), bb) \<in> fst (corrupt_frame buf (transform b)); ((), transform ba) \<in> fst (corrupt_tcb_intent y bb); ipc_frame_ptr_at buf y b; not_idle_thread y b; valid_etcbs b\<rbrakk> \<Longrightarrow> case ((), transform ba) of (r, x) \<Rightarrow> transform ba = x
 2. \<And>b a ba bb. \<lbrakk>P b; (a, ba) \<in> fst (g b); ((), bb) \<in> fst (corrupt_frame buf (transform b)); ((), transform ba) \<in> fst (corrupt_tcb_intent y bb); ipc_frame_ptr_at buf y b; not_idle_thread y b; valid_etcbs b\<rbrakk> \<Longrightarrow> ((), transform ba) \<in> fst (corrupt_frame buf (transform b)) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb. \<lbrakk>P b; (a, ba) \<in> fst (g b); ((), bb) \<in> fst (corrupt_frame buf (transform b)); ((), transform ba) \<in> fst (corrupt_tcb_intent y bb); ipc_frame_ptr_at buf y b; not_idle_thread y b; valid_etcbs b\<rbrakk> \<Longrightarrow> ((), transform ba) \<in> fst (corrupt_frame buf (transform b)) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba x. \<lbrakk>P b; (a, ba) \<in> fst (g b); ((), transform ba) \<in> fst (corrupt_tcb_intent y (corrupt_intents x buf (transform b))); ipc_frame_ptr_at buf y b; not_idle_thread y b; valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>x. transform ba = corrupt_intents x buf (transform b) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba x x2 xa. \<lbrakk>ipc_frame_ptr_at buf y b; not_idle_thread y b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); cdl_objects (corrupt_intents x buf (transform b)) y = Some x2; ((), transform ba) \<in> fst ((case x2 of Tcb tcb \<Rightarrow> \<lambda>s. ({((), dupdate_cdl_object y (Tcb (dupdate_tcb_intent xa tcb)) s)}, False) | _ \<Rightarrow> \<lambda>s. ({}, True)) (corrupt_intents x buf (transform b)))\<rbrakk> \<Longrightarrow> \<exists>x. transform ba = corrupt_intents x buf (transform b) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba x x2 xa. \<lbrakk>ipc_frame_ptr_at buf y b; not_idle_thread y b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); cdl_objects (corrupt_intents x buf (transform b)) y = Some x2; ((), transform ba) \<in> fst ((case x2 of Tcb tcb \<Rightarrow> \<lambda>s. ({((), dupdate_cdl_object y (Tcb (dupdate_tcb_intent xa tcb)) s)}, False) | _ \<Rightarrow> \<lambda>s. ({}, True)) (corrupt_intents x buf (transform b)))\<rbrakk> \<Longrightarrow> transform ba = corrupt_intents (\<lambda>t. if t = y then ?T68 b a ba x x2 xa else x t) buf (transform b) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x xa tcb x3. \<lbrakk>y \<noteq> idle_thread b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); (if tcb_ipcframe_id x3 = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3)) else None) = None; kheap b y = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform_objects b y = Some (Tcb x3); transform_objects ba = (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b\<rbrakk> \<Longrightarrow> (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)) = (\<lambda>xb. case case transform_objects b xb of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (if xb = y then ?T68 b a ba x (Tcb x3) xa else x xb) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xb | Some x \<Rightarrow> Some x)
 2. \<And>b a ba x xa tcb x3 x3a. \<lbrakk>y \<noteq> idle_thread b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); kheap b y = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform_objects b y = Some (Tcb x3a); transform_objects ba = (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b; (if tcb_ipcframe_id x3a = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3a)) else None) = Some (Tcb x3)\<rbrakk> \<Longrightarrow> (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)) = (\<lambda>xb. case case transform_objects b xb of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (if xb = y then ?T68 b a ba x (Tcb x3) xa else x xb) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xb | Some x \<Rightarrow> Some x) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x xa tcb x3 xb. \<lbrakk>y \<noteq> idle_thread b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); (if tcb_ipcframe_id x3 = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3)) else None) = None; kheap b y = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform_objects b y = Some (Tcb x3); transform_objects ba = (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b\<rbrakk> \<Longrightarrow> ((\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3))) xb = (case case transform_objects b xb of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (if xb = y then ?T68 b a ba x (Tcb x3) xa else x xb) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xb | Some x \<Rightarrow> Some x)
 2. \<And>b a ba x xa tcb x3 x3a. \<lbrakk>y \<noteq> idle_thread b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); kheap b y = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform_objects b y = Some (Tcb x3a); transform_objects ba = (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b; (if tcb_ipcframe_id x3a = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3a)) else None) = Some (Tcb x3)\<rbrakk> \<Longrightarrow> (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)) = (\<lambda>xb. case case transform_objects b xb of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (if xb = y then ?T68 b a ba x (Tcb x3) xa else x xb) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xb | Some x \<Rightarrow> Some x) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x xa tcb x3. \<lbrakk>y \<noteq> idle_thread b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); (if (case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3)) else None) = None; kheap b y = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform_objects b y = Some (Tcb x3); transform_objects ba = (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b\<rbrakk> \<Longrightarrow> ((case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) = Some buf \<longrightarrow> dupdate_tcb_intent xa x3 = dupdate_tcb_intent (?T68 b a ba x (Tcb x3) xa) x3) \<and> ((case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) \<noteq> Some buf \<longrightarrow> dupdate_tcb_intent xa x3 = x3)
 2. \<And>b a ba x xa tcb x3 x3a. \<lbrakk>y \<noteq> idle_thread b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); kheap b y = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform_objects b y = Some (Tcb x3a); transform_objects ba = (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b; (if tcb_ipcframe_id x3a = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3a)) else None) = Some (Tcb x3)\<rbrakk> \<Longrightarrow> (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)) = (\<lambda>xb. case case transform_objects b xb of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (if xb = y then ?T68 b a ba x (Tcb x3) xa else x xb) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xb | Some x \<Rightarrow> Some x) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x xa tcb x3. \<lbrakk>y \<noteq> idle_thread b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); (if (case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3)) else None) = None; kheap b y = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; (case ekheap b y of Some x \<Rightarrow> transform_tcb (machine_state b) y tcb x) = Tcb x3; (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread ba}) ++ (\<lambda>ptr. map_option (transform_object (machine_state ba) ptr ((ekheap ba |` (- {idle_thread ba})) ptr)) ((kheap ba |` (- {idle_thread ba})) ptr)) = (\<lambda>xa. case case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr))) xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b\<rbrakk> \<Longrightarrow> ((case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) = Some buf \<longrightarrow> dupdate_tcb_intent xa x3 = dupdate_tcb_intent (?T68 b a ba x (Tcb x3) xa) x3) \<and> ((case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) \<noteq> Some buf \<longrightarrow> dupdate_tcb_intent xa x3 = x3)
 2. \<And>b a ba x xa tcb x3 x3a. \<lbrakk>y \<noteq> idle_thread b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); kheap b y = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform_objects b y = Some (Tcb x3a); transform_objects ba = (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b; (if tcb_ipcframe_id x3a = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3a)) else None) = Some (Tcb x3)\<rbrakk> \<Longrightarrow> (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)) = (\<lambda>xb. case case transform_objects b xb of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (if xb = y then ?T68 b a ba x (Tcb x3) xa else x xb) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xb | Some x \<Rightarrow> Some x) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x xa tcb x3 x31 x33 x34 x35. \<lbrakk>(case ekheap b y of Some x \<Rightarrow> transform_tcb (machine_state b) y tcb x) = Tcb x3; (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread ba}) ++ (\<lambda>ptr. map_option (transform_object (machine_state ba) ptr ((ekheap ba |` (- {idle_thread ba})) ptr)) ((kheap ba |` (- {idle_thread ba})) ptr)) = (\<lambda>xa. case case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr))) xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b; y \<noteq> idle_thread b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); (if (case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3)) else None) = None; kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35)\<rbrakk> \<Longrightarrow> ((case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) = Some buf \<longrightarrow> dupdate_tcb_intent xa x3 = dupdate_tcb_intent (?T68 b a ba x (Tcb x3) xa) x3) \<and> ((case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) \<noteq> Some buf \<longrightarrow> dupdate_tcb_intent xa x3 = x3)
 2. \<And>b a ba x xa tcb x3 x3a. \<lbrakk>y \<noteq> idle_thread b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); kheap b y = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform_objects b y = Some (Tcb x3a); transform_objects ba = (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b; (if tcb_ipcframe_id x3a = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3a)) else None) = Some (Tcb x3)\<rbrakk> \<Longrightarrow> (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)) = (\<lambda>xb. case case transform_objects b xb of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (if xb = y then ?T68 b a ba x (Tcb x3) xa else x xb) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xb | Some x \<Rightarrow> Some x) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x xa tcb x3 x31 x33 x34 x35. \<lbrakk>(case ekheap b y of Some x \<Rightarrow> transform_tcb (machine_state b) y tcb x) = Tcb x3; (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread ba}) ++ (\<lambda>ptr. map_option (transform_object (machine_state ba) ptr ((ekheap ba |` (- {idle_thread ba})) ptr)) ((kheap ba |` (- {idle_thread ba})) ptr)) = (\<lambda>xa. case case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread b}) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr ((ekheap b |` (- {idle_thread b})) ptr)) ((kheap b |` (- {idle_thread b})) ptr))) xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b; y \<noteq> idle_thread b; P b; (a, ba) \<in> fst (g b); (if (case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3)) else None) = None; kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); \<exists>etcb. ekheap b y = Some etcb\<rbrakk> \<Longrightarrow> ((case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) = Some buf \<longrightarrow> dupdate_tcb_intent xa x3 = dupdate_tcb_intent (?T68 b a ba x (Tcb x3) xa) x3) \<and> ((case cdl_tcb_caps x3 4 of None \<Rightarrow> None | Some (FrameCap xa oid xaa xb xc xd) \<Rightarrow> Some oid | Some _ \<Rightarrow> None) \<noteq> Some buf \<longrightarrow> dupdate_tcb_intent xa x3 = x3)
 2. \<And>b a ba x xa tcb x3 x3a. \<lbrakk>y \<noteq> idle_thread b; valid_etcbs b; P b; (a, ba) \<in> fst (g b); kheap b y = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform_objects b y = Some (Tcb x3a); transform_objects ba = (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)); transform_cdt ba = transform_cdt b; transform_current_thread ba = transform_current_thread b; interrupt_irq_node ba = interrupt_irq_node b; transform_asid_table ba = transform_asid_table b; cur_domain ba = cur_domain b; (if tcb_ipcframe_id x3a = Some buf then Some (Tcb (dupdate_tcb_intent (x y) x3a)) else None) = Some (Tcb x3)\<rbrakk> \<Longrightarrow> (\<lambda>xa. case case transform_objects b xa of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x xa) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xa | Some x \<Rightarrow> Some x)(y \<mapsto> Tcb (dupdate_tcb_intent xa x3)) = (\<lambda>xb. case case transform_objects b xb of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (if xb = y then ?T68 b a ba x (Tcb x3) xa else x xb) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> transform_objects b xb | Some x \<Rightarrow> Some x)