theory Intent_DR

lemma corrupt_frame_include_self:
  assumes corres:"dcorres dc \<top> P (do corrupt_tcb_intent y;corrupt_frame buf 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 supply option.case_cong[cong] apply (clarsimp simp:corres_underlying_def) apply (frule imp) apply (erule allE, erule (1) impE) apply (drule_tac x = "(a,ba)" in bspec) apply simp+ apply (clarsimp simp:bind_def) apply (rule_tac x = "((),transform ba)" in bexI) apply simp apply (clarsimp simp:corrupt_tcb_intent_def bind_def) apply (clarsimp simp:update_thread_def gets_the_def gets_def get_def bind_def in_monad) apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def) apply (clarsimp split:cap.splits arch_cap.splits) apply (clarsimp simp:select_def KHeap_D.set_object_def simpler_modify_def) apply (clarsimp simp:corrupt_frame_def bind_def select_def) apply (clarsimp simp:simpler_modify_def corrupt_intents_def) apply (drule(1) valid_etcbs_tcb_etcb, clarsimp) apply (subst(asm) opt_object_tcb) apply (erule get_tcb_rev) apply (erule get_etcb_rev) apply (simp add:not_idle_thread_def) apply (clarsimp simp:transform_tcb_def in_monad set_object_def) apply (rule_tac x = x in exI) apply (clarsimp simp:transform_def KHeap_D.set_object_def simpler_modify_def) apply (case_tac "transform b") apply (clarsimp simp:transform_def map_add_def) apply (rule ext) apply (drule_tac x = xa in fun_cong) apply (case_tac xa) apply (clarsimp simp:not_idle_thread_def tcb_ipcframe_id_def restrict_map_def transform_objects_def
                  split: if_split) apply (clarsimp dest!:get_tcb_rev simp: transform_objects_tcb tcb_ipcbuffer_slot_def
                        tcb_pending_op_slot_def tcb_boundntfn_slot_def) apply (clarsimp simp: tcb_ipcbuffer_slot_def tcb_ipcframe_id_def | rule conjI)+ apply (clarsimp simp:transform_def transform_object_def transform_tcb_def tcb_ipcframe_id_def
        tcb_ipcbuffer_slot_def tcb_pending_op_slot_def tcb_boundntfn_slot_def dest!:get_tcb_SomeD) done

(* 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_tcb_intent y;
corrupt_frame buf
od) g

goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) P (corrupt_frame buf) g proof (prove)
using this:
dcorres dc (\<lambda>_. True) P (do corrupt_tcb_intent y;
corrupt_frame buf
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>x\<in>fst ((do y <- corrupt_tcb_intent y;
corrupt_frame buf
od) (transform b)). 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>x\<in>fst ((do y <- corrupt_tcb_intent y;
corrupt_frame buf
od) (transform b)). 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>x\<in>fst ((do y <- corrupt_tcb_intent y;
corrupt_frame buf
od) (transform b)). 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>x\<in>fst ((do y <- corrupt_tcb_intent y;
corrupt_frame buf
od) (transform b)). 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>x\<in>fst ((do y <- corrupt_tcb_intent y;
corrupt_frame buf
od) (transform b)). 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_tcb_intent y (transform b)); ((), transform ba) \<in> fst (corrupt_frame buf 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_tcb_intent y (transform b)); ((), transform ba) \<in> fst (corrupt_frame buf 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_tcb_intent y (transform b)); ((), transform ba) \<in> fst (corrupt_frame buf 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_tcb_intent y (transform b)); ((), transform ba) \<in> fst (corrupt_frame buf 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 aa bc. \<lbrakk>P b; (a, ba) \<in> fst (g b); ((), transform ba) \<in> fst (corrupt_frame buf bb); ipc_frame_ptr_at buf y b; not_idle_thread y b; valid_etcbs b; (aa, bc) \<in> fst (select UNIV (transform b)); ((), bb) \<in> fst (update_thread y (dupdate_tcb_intent aa) bc)\<rbrakk> \<Longrightarrow> ((), transform ba) \<in> fst (corrupt_frame buf (transform b)) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb aa bc ac. \<lbrakk>P b; (a, ba) \<in> fst (g b); ((), transform ba) \<in> fst (corrupt_frame buf bb); ipc_frame_ptr_at buf y b; not_idle_thread y b; valid_etcbs b; (aa, bc) \<in> fst (select UNIV (transform b)); cdl_objects bc y = Some ac; ((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) bc)\<rbrakk> \<Longrightarrow> ((), transform ba) \<in> fst (corrupt_frame buf (transform b)) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb aa bc ac tcb. \<lbrakk>P b; (a, ba) \<in> fst (g b); ((), transform ba) \<in> fst (corrupt_frame buf bb); not_idle_thread y b; valid_etcbs b; (aa, bc) \<in> fst (select UNIV (transform b)); cdl_objects bc y = Some ac; ((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) bc); 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\<rbrakk> \<Longrightarrow> ((), transform ba) \<in> fst (corrupt_frame buf (transform b)) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb aa bc ac tcb x31 x33 x34 x35. \<lbrakk>P b; (a, ba) \<in> fst (g b); ((), transform ba) \<in> fst (corrupt_frame buf bb); not_idle_thread y b; valid_etcbs b; (aa, bc) \<in> fst (select UNIV (transform b)); cdl_objects bc y = Some ac; ((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) bc); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35)\<rbrakk> \<Longrightarrow> ((), transform ba) \<in> fst (corrupt_frame buf (transform b)) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb aa ac tcb x31 x33 x34 x35. \<lbrakk>P b; (a, ba) \<in> fst (g b); ((), transform ba) \<in> fst (corrupt_frame buf bb); not_idle_thread y b; valid_etcbs b; cdl_objects (transform b) y = Some ac; ((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35)\<rbrakk> \<Longrightarrow> ((), transform ba) \<in> fst (corrupt_frame buf (transform b)) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; valid_etcbs b; cdl_objects (transform b) y = Some ac; ((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); ((), transform ba) \<in> fst (modify (corrupt_intents x buf) bb)\<rbrakk> \<Longrightarrow> \<exists>x. ((), transform ba) \<in> fst (modify (corrupt_intents x buf) (transform b)) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; valid_etcbs b; cdl_objects (transform b) y = Some ac; ((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>\<rbrakk> \<Longrightarrow> \<exists>xa. bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> = transform b\<lparr>cdl_objects := cdl_objects (transform b) ++ (\<lambda>ptr. case cdl_objects (transform b) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (xa ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x etcb. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; cdl_objects (transform b) y = Some ac; ((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb\<rbrakk> \<Longrightarrow> \<exists>xa. bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> = transform b\<lparr>cdl_objects := cdl_objects (transform b) ++ (\<lambda>ptr. case cdl_objects (transform b) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (xa ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> proof (prove)
goal (4 subgoals):
 1. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x etcb. \<lbrakk>((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb; P b; (a, ba) \<in> fst (g b); not_idle_thread y b\<rbrakk> \<Longrightarrow> get_tcb y b = Some (?tcb161 b a ba bb aa ac tcb x31 x33 x34 x35 x etcb)
 2. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x etcb. \<lbrakk>((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb; P b; (a, ba) \<in> fst (g b); not_idle_thread y b\<rbrakk> \<Longrightarrow> get_etcb y b = Some (?etcb161 b a ba bb aa ac tcb x31 x33 x34 x35 x etcb)
 3. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x etcb. \<lbrakk>((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb; P b; (a, ba) \<in> fst (g b); not_idle_thread y b\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread b
 4. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x etcb. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; Some (transform_tcb (machine_state b) y (?tcb161 b a ba bb aa ac tcb x31 x33 x34 x35 x etcb) (?etcb161 b a ba bb aa ac tcb x31 x33 x34 x35 x etcb)) = Some ac; ((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb\<rbrakk> \<Longrightarrow> \<exists>xa. bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> = transform b\<lparr>cdl_objects := cdl_objects (transform b) ++ (\<lambda>ptr. case cdl_objects (transform b) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (xa ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x etcb. \<lbrakk>((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb; P b; (a, ba) \<in> fst (g b); not_idle_thread y b\<rbrakk> \<Longrightarrow> get_etcb y b = Some (?etcb161 b a ba bb aa ac tcb x31 x33 x34 x35 x etcb)
 2. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x etcb. \<lbrakk>((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb; P b; (a, ba) \<in> fst (g b); not_idle_thread y b\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread b
 3. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x etcb. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; Some (transform_tcb (machine_state b) y tcb (?etcb161 b a ba bb aa ac tcb x31 x33 x34 x35 x etcb)) = Some ac; ((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb\<rbrakk> \<Longrightarrow> \<exists>xa. bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> = transform b\<lparr>cdl_objects := cdl_objects (transform b) ++ (\<lambda>ptr. case cdl_objects (transform b) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (xa ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x etcb. \<lbrakk>((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb; P b; (a, ba) \<in> fst (g b); not_idle_thread y b\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread b
 2. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x etcb. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; Some (transform_tcb (machine_state b) y tcb etcb) = Some ac; ((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb\<rbrakk> \<Longrightarrow> \<exists>xa. bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> = transform b\<lparr>cdl_objects := cdl_objects (transform b) ++ (\<lambda>ptr. case cdl_objects (transform b) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (xa ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb aa ac tcb x31 x33 x34 x35 x etcb. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; Some (transform_tcb (machine_state b) y tcb etcb) = Some ac; ((), bb) \<in> fst ((case ac of Tcb tcb \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent aa tcb)) | _ \<Rightarrow> fail) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb\<rbrakk> \<Longrightarrow> \<exists>xa. bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> = transform b\<lparr>cdl_objects := cdl_objects (transform b) ++ (\<lambda>ptr. case cdl_objects (transform b) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (xa ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb aa tcb x31 x33 x34 x35 x etcb. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; ((), bb) \<in> fst (KHeap_D.set_object y (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb\<rbrakk> \<Longrightarrow> \<exists>xa. bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> = transform b\<lparr>cdl_objects := cdl_objects (transform b) ++ (\<lambda>ptr. case cdl_objects (transform b) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (xa ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>b a ba bb aa tcb x31 x33 x34 x35 x etcb. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; ((), bb) \<in> fst (KHeap_D.set_object y (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) (transform b)); kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); transform ba = bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr>; ekheap b y = Some etcb\<rbrakk> \<Longrightarrow> bb\<lparr>cdl_objects := cdl_objects bb ++ (\<lambda>ptr. case cdl_objects bb ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> = transform b\<lparr>cdl_objects := cdl_objects (transform b) ++ (\<lambda>ptr. case cdl_objects (transform b) ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa tcb x31 x33 x34 x35 x etcb. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); ekheap b y = Some etcb; transform_objects ba = (transform_objects b)(y \<mapsto> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) ++ (\<lambda>ptr. case if ptr = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None); 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> (transform_objects b)(y \<mapsto> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) ++ (\<lambda>ptr. case if ptr = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None) = transform_objects b ++ (\<lambda>ptr. case transform_objects b ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa tcb x31 x33 x34 x35 x etcb cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); ekheap b y = Some etcb; transform_objects ba = (transform_objects b)(y \<mapsto> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) ++ (\<lambda>ptr. case if ptr = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None); 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; transform b = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>\<rbrakk> \<Longrightarrow> (transform_objects b)(y \<mapsto> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) ++ (\<lambda>ptr. case if ptr = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None) = transform_objects b ++ (\<lambda>ptr. case transform_objects b ptr of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x ptr) tcb)) else None | Some _ \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa tcb x31 x33 x34 x35 x etcb. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); ekheap b y = Some etcb; transform_objects ba = (\<lambda>xa. case case if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else 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> if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b xa | Some x2 \<Rightarrow> Some x2); 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 if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else 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> if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b xa | Some x2 \<Rightarrow> Some x2) = (\<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 x2 \<Rightarrow> Some x2) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa tcb x31 x33 x34 x35 x etcb xa. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); ekheap b y = Some etcb; transform_objects ba = (\<lambda>xa. case case if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else 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> if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b xa | Some x2 \<Rightarrow> Some x2); 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 case if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else 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> if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b xa | Some x2 \<Rightarrow> Some x2) = (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 x2 \<Rightarrow> Some x2) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa tcb x31 x33 x34 x35 x etcb xa. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); ekheap b y = Some etcb; 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; transform_objects ba xa = (case case if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else 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> if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b xa | Some x2 \<Rightarrow> Some x2)\<rbrakk> \<Longrightarrow> (case case if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else 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> if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b xa | Some x2 \<Rightarrow> Some x2) = (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 x2 \<Rightarrow> Some x2) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa tcb x31 x33 x34 x35 x etcb xa n. \<lbrakk>P b; (a, ba) \<in> fst (g b); not_idle_thread y b; kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); ekheap b y = Some etcb; 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; transform_objects ba xa = (case case if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else 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> if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b xa | Some x2 \<Rightarrow> Some x2); xa = word_of_nat n; n < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> (case case if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else 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> if xa = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b xa | Some x2 \<Rightarrow> Some x2) = (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 x2 \<Rightarrow> Some x2) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa tcb x31 x33 x34 x35 x etcb n. \<lbrakk>P b; (a, ba) \<in> fst (g b); y \<noteq> idle_thread b; kheap b y = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); ekheap b y = Some etcb; 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; ((\<lambda>x. if x \<noteq> idle_thread ba then Some cdl_object.Untyped else None) ++ (\<lambda>ptr. map_option (transform_object (machine_state ba) ptr (if ptr \<noteq> idle_thread ba then ekheap ba ptr else None)) (if ptr \<noteq> idle_thread ba then kheap ba ptr else None))) (word_of_nat n) = (case case if word_of_nat n = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b (word_of_nat n) of None \<Rightarrow> None | Some (Tcb tcb) \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x (word_of_nat n)) tcb)) else None | Some _ \<Rightarrow> None of None \<Rightarrow> if word_of_nat n = y then Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) else transform_objects b (word_of_nat n) | Some x2 \<Rightarrow> Some x2); n < 4294967296\<rbrakk> \<Longrightarrow> (tcb_ipcbuffer_slot = tcb_pending_op_slot \<longrightarrow> (tcb_pending_op_slot = tcb_boundntfn_slot \<longrightarrow> ((case infer_tcb_bound_notification (tcb_bound_notification tcb) of FrameCap x oid xa xb xc xd \<Rightarrow> Some oid | _ \<Rightarrow> None) = Some buf \<longrightarrow> word_of_nat n = y \<longrightarrow> Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = x y, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) = (case case transform_tcb (machine_state b) y tcb etcb of Tcb tcb \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x (word_of_nat n)) tcb)) else None | _ \<Rightarrow> None of None \<Rightarrow> Some (transform_tcb (machine_state b) y tcb etcb) | Some x2 \<Rightarrow> Some x2)) \<and> ((case infer_tcb_bound_notification (tcb_bound_notification tcb) of FrameCap x oid xa xb xc xd \<Rightarrow> Some oid | _ \<Rightarrow> None) \<noteq> Some buf \<longrightarrow> word_of_nat n = y \<longrightarrow> Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) = (case case transform_tcb (machine_state b) y tcb etcb of Tcb tcb \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x (word_of_nat n)) tcb)) else None | _ \<Rightarrow> None of None \<Rightarrow> Some (transform_tcb (machine_state b) y tcb etcb) | Some x2 \<Rightarrow> Some x2))) \<and> (tcb_pending_op_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> ((case infer_tcb_pending_op y (tcb_state tcb) of FrameCap x oid xa xb xc xd \<Rightarrow> Some oid | _ \<Rightarrow> None) = Some buf \<longrightarrow> word_of_nat n = y \<longrightarrow> Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = x y, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) = (case case transform_tcb (machine_state b) y tcb etcb of Tcb tcb \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x (word_of_nat n)) tcb)) else None | _ \<Rightarrow> None of None \<Rightarrow> Some (transform_tcb (machine_state b) y tcb etcb) | Some x2 \<Rightarrow> Some x2)) \<and> ((case infer_tcb_pending_op y (tcb_state tcb) of FrameCap x oid xa xb xc xd \<Rightarrow> Some oid | _ \<Rightarrow> None) \<noteq> Some buf \<longrightarrow> word_of_nat n = y \<longrightarrow> Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) = (case case transform_tcb (machine_state b) y tcb etcb of Tcb tcb \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x (word_of_nat n)) tcb)) else None | _ \<Rightarrow> None of None \<Rightarrow> Some (transform_tcb (machine_state b) y tcb etcb) | Some x2 \<Rightarrow> Some x2)))) \<and> (tcb_ipcbuffer_slot \<noteq> tcb_pending_op_slot \<longrightarrow> (tcb_ipcbuffer_slot = tcb_boundntfn_slot \<longrightarrow> ((case infer_tcb_bound_notification (tcb_bound_notification tcb) of FrameCap x oid xa xb xc xd \<Rightarrow> Some oid | _ \<Rightarrow> None) = Some buf \<longrightarrow> word_of_nat n = y \<longrightarrow> Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = x y, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) = (case case transform_tcb (machine_state b) y tcb etcb of Tcb tcb \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x (word_of_nat n)) tcb)) else None | _ \<Rightarrow> None of None \<Rightarrow> Some (transform_tcb (machine_state b) y tcb etcb) | Some x2 \<Rightarrow> Some x2)) \<and> ((case infer_tcb_bound_notification (tcb_bound_notification tcb) of FrameCap x oid xa xb xc xd \<Rightarrow> Some oid | _ \<Rightarrow> None) \<noteq> Some buf \<longrightarrow> word_of_nat n = y \<longrightarrow> Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) = (case case transform_tcb (machine_state b) y tcb etcb of Tcb tcb \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x (word_of_nat n)) tcb)) else None | _ \<Rightarrow> None of None \<Rightarrow> Some (transform_tcb (machine_state b) y tcb etcb) | Some x2 \<Rightarrow> Some x2))) \<and> (tcb_ipcbuffer_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> word_of_nat n = y \<longrightarrow> Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = x y, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) = (case case transform_tcb (machine_state b) y tcb etcb of Tcb tcb \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x (word_of_nat n)) tcb)) else None | _ \<Rightarrow> None of None \<Rightarrow> Some (transform_tcb (machine_state b) y tcb etcb) | Some x2 \<Rightarrow> Some x2))) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa tcb x31 x33 x34 x35 x etcb n. \<lbrakk>P b; (a, ba) \<in> fst (g b); word_of_nat n \<noteq> idle_thread b; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); ekheap b (word_of_nat n) = Some etcb; 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; ((\<lambda>x. if x \<noteq> idle_thread ba then Some cdl_object.Untyped else None) ++ (\<lambda>ptr. map_option (transform_object (machine_state ba) ptr (if ptr \<noteq> idle_thread ba then ekheap ba ptr else None)) (if ptr \<noteq> idle_thread ba then kheap ba ptr else None))) (word_of_nat n) = (case if tcb_ipcframe_id \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), 4 \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), 5 \<mapsto> infer_tcb_pending_op (word_of_nat n) (tcb_state tcb), 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr> = Some buf then Some (Tcb (dupdate_tcb_intent (x (word_of_nat n)) \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), 4 \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), 5 \<mapsto> infer_tcb_pending_op (word_of_nat n) (tcb_state tcb), 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) else None of None \<Rightarrow> Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), 4 \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), 5 \<mapsto> infer_tcb_pending_op (word_of_nat n) (tcb_state tcb), 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = aa, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) | Some x2 \<Rightarrow> Some x2); n < 4294967296; get_tcb (word_of_nat n) b = Some tcb; y = word_of_nat n\<rbrakk> \<Longrightarrow> Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), 4 \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), 5 \<mapsto> infer_tcb_pending_op (word_of_nat n) (tcb_state tcb), 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = x (word_of_nat n), cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) = (case case transform_tcb (machine_state b) (word_of_nat n) tcb etcb of Tcb tcb \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x (word_of_nat n)) tcb)) else None | _ \<Rightarrow> None of None \<Rightarrow> Some (transform_tcb (machine_state b) (word_of_nat n) tcb etcb) | Some x2 \<Rightarrow> Some x2) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba tcb x31 x33 x34 x35 x etcb n. \<lbrakk>P b; (a, ba) \<in> fst (g b); word_of_nat n \<noteq> idle_thread b; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 buf x33 x34 x35); ekheap b (word_of_nat n) = Some etcb; 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; n < 4294967296; get_tcb (word_of_nat n) b = Some tcb; y = word_of_nat n; (\<exists>z. (if word_of_nat n \<noteq> idle_thread ba then kheap ba (word_of_nat n) else None) = Some z \<and> transform_object (machine_state ba) (word_of_nat n) (if word_of_nat n \<noteq> idle_thread ba then ekheap ba (word_of_nat n) else None) z = Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), 4 \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), 5 \<mapsto> infer_tcb_pending_op (word_of_nat n) (tcb_state tcb), 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = x (word_of_nat n), cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<or> (if word_of_nat n \<noteq> idle_thread ba then kheap ba (word_of_nat n) else None) = None \<and> (if word_of_nat n \<noteq> idle_thread ba then Some cdl_object.Untyped else None) = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), 4 \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), 5 \<mapsto> infer_tcb_pending_op (word_of_nat n) (tcb_state tcb), 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = x (word_of_nat n), cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), 4 \<mapsto> FrameCap x31 buf x33 (pageBitsForSize x34) Real (transform_mapping x35), 5 \<mapsto> infer_tcb_pending_op (word_of_nat n) (tcb_state tcb), 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = x (word_of_nat n), cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) = (case case transform_tcb (machine_state b) (word_of_nat n) tcb etcb of Tcb tcb \<Rightarrow> if tcb_ipcframe_id tcb = Some buf then Some (Tcb (dupdate_tcb_intent (x (word_of_nat n)) tcb)) else None | _ \<Rightarrow> None of None \<Rightarrow> Some (transform_tcb (machine_state b) (word_of_nat n) tcb etcb) | Some x2 \<Rightarrow> Some x2) proof (prove)
goal:
No subgoals!