theory Finalise_DR

lemma set_cap_noop_dcorres3:
  "dcorres dc \<top> (cte_wp_at (\<lambda>cap'. transform_cap cap = transform_cap cap'
                                 \<and> arch_page_vmpage_size cap = arch_page_vmpage_size cap') ptr)
    (return ()) (set_cap cap ptr)" apply (rule corres_noop, simp_all) apply (simp add: set_cap_def split_def set_object_def) apply (wp get_object_wp | wpc)+ apply (clarsimp simp: obj_at_def) apply (erule cte_wp_atE) apply (clarsimp simp: transform_def transform_current_thread_def
                         transform_objects_def) apply (rule ext) apply (simp add: fun_upd_def[symmetric]
               del: dom_fun_upd) apply (simp add: restrict_map_def transform_cnode_contents_def
                    fun_eq_iff option_map_join_def map_add_def
             split: option.split nat.split) apply (clarsimp simp: transform_def transform_current_thread_def
                        transform_objects_def fun_eq_iff
                        arch_page_vmpage_size_def) apply (simp add: restrict_map_def transform_cnode_contents_def map_add_def
                   transform_tcb_def fun_eq_iff infer_tcb_pending_op_def
            split: option.split cong: Structures_A.thread_state.case_cong) apply (subgoal_tac "snd ptr = tcb_cnode_index 4 \<longrightarrow>
                       (\<forall>ms ns. get_ipc_buffer_words ms (tcb\<lparr>tcb_ipcframe := cap\<rparr>) ns
                          = get_ipc_buffer_words ms tcb ns)") apply (simp cong: transform_full_intent_cong) apply (simp add: transform_full_intent_def Let_def get_tcb_message_info_def
                    get_tcb_mrs_def) apply fastforce apply clarsimp apply (simp add: transform_cap_def split: cap.split_asm arch_cap.split_asm if_split_asm,
         simp_all add: get_ipc_buffer_words_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>cap'. transform_cap cap = transform_cap cap' \<and> arch_page_vmpage_size cap = arch_page_vmpage_size cap') ptr) (return ()) (CSpaceAcc_A.set_cap cap ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>\<lambda>s'. transform s' = s \<and> cte_wp_at (\<lambda>cap'. transform_cap cap = transform_cap cap' \<and> arch_page_vmpage_size cap = arch_page_vmpage_size cap') ptr s'\<rbrace> CSpaceAcc_A.set_cap cap ptr \<lbrace>\<lambda>rv s'. transform s' = s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>\<lambda>s'. transform s' = s \<and> cte_wp_at (\<lambda>cap'. transform_cap cap = transform_cap cap' \<and> arch_page_vmpage_size cap = arch_page_vmpage_size cap') ptr s'\<rbrace> do obj <- KHeap_A.get_object (fst ptr);
obj' <- case obj of kernel_object.CNode sz cn \<Rightarrow> if snd ptr \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ kernel_object.CNode sz $ cn(snd ptr \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd ptr = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd ptr = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd ptr = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd ptr = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd ptr = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- KHeap_A.get_object (fst ptr);
y <- assert (a_type kobj = a_type obj');
s <- get;
put (update_kheap ((kheap s)(fst ptr \<mapsto> obj')) s)
od \<lbrace>\<lambda>rv s'. transform s' = s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sa. transform sa = s \<and> cte_wp_at (\<lambda>cap'. transform_cap cap = transform_cap cap' \<and> arch_page_vmpage_size cap = arch_page_vmpage_size cap') ptr sa \<Longrightarrow> \<forall>ko. ko_at ko (fst ptr) sa \<longrightarrow> (\<forall>x xa. ko = kernel_object.CNode x xa \<longrightarrow> (snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) sa \<longrightarrow> a_type ko = a_type (kernel_object.CNode x $ xa(snd ptr \<mapsto> cap)) \<longrightarrow> transform (update_kheap ((kheap sa)(fst ptr \<mapsto> kernel_object.CNode x $ xa(snd ptr \<mapsto> cap))) sa) = s)) \<and> (\<not> (snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa) \<longrightarrow> True)) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) sa \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_ctable := cap\<rparr>) \<longrightarrow> transform (update_kheap ((kheap sa)(fst ptr \<mapsto> TCB $ x\<lparr>tcb_ctable := cap\<rparr>)) sa) = s)) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index 1 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) sa \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_vtable := cap\<rparr>) \<longrightarrow> transform (update_kheap ((kheap sa)(fst ptr \<mapsto> TCB $ x\<lparr>tcb_vtable := cap\<rparr>)) sa) = s)) \<and> (snd ptr \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) sa \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_reply := cap\<rparr>) \<longrightarrow> transform (update_kheap ((kheap sa)(fst ptr \<mapsto> TCB $ x\<lparr>tcb_reply := cap\<rparr>)) sa) = s)) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) sa \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_caller := cap\<rparr>) \<longrightarrow> transform (update_kheap ((kheap sa)(fst ptr \<mapsto> TCB $ x\<lparr>tcb_caller := cap\<rparr>)) sa) = s)) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) sa \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_ipcframe := cap\<rparr>) \<longrightarrow> transform (update_kheap ((kheap sa)(fst ptr \<mapsto> TCB $ x\<lparr>tcb_ipcframe := cap\<rparr>)) sa) = s)) \<and> (snd ptr \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. ko = kernel_object.Endpoint x \<longrightarrow> True) \<and> (\<forall>x. ko = kernel_object.Notification x \<longrightarrow> True) \<and> (\<forall>x. ko = ArchObj x \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>sa ko. \<lbrakk>cte_wp_at (\<lambda>cap'. transform_cap cap = transform_cap cap' \<and> arch_page_vmpage_size cap = arch_page_vmpage_size cap') ptr sa; kheap sa (fst ptr) = Some ko\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = kernel_object.CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> a_type (kernel_object.CNode x xa) = a_type (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) else kheap sa a) sa) = transform sa) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_reply := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_caller := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap sa a) sa) = transform sa))))) proof (prove)
goal (2 subgoals):
 1. \<And>sa ko sz fun cte. \<lbrakk>kheap sa (fst ptr) = Some ko; kheap sa (fst ptr) = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun (snd ptr) = Some cte; transform_cap cap = transform_cap cte \<and> arch_page_vmpage_size cap = arch_page_vmpage_size cte\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = kernel_object.CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> a_type (kernel_object.CNode x xa) = a_type (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) else kheap sa a) sa) = transform sa) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_reply := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_caller := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap sa a) sa) = transform sa)))))
 2. \<And>sa ko tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some ko; kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb) \<and> arch_page_vmpage_size cap = arch_page_vmpage_size (getF tcb)\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = kernel_object.CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> a_type (kernel_object.CNode x xa) = a_type (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) else kheap sa a) sa) = transform sa) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_reply := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_caller := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap sa a) sa) = transform sa))))) proof (prove)
goal (2 subgoals):
 1. \<And>sa sz fun cte. \<lbrakk>kheap sa (fst ptr) = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; transform_cap cap = transform_cap cte; arch_page_vmpage_size cap = arch_page_vmpage_size cte; fun (snd ptr) = Some cte; a_type (kernel_object.CNode sz fun) = a_type (kernel_object.CNode sz (\<lambda>a. if a = snd ptr then Some cap else fun a))\<rbrakk> \<Longrightarrow> (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptra. map_option (transform_object (machine_state sa) ptra ((ekheap sa |` (- {idle_thread sa})) ptra)) (((\<lambda>a. if a = fst ptr then Some (kernel_object.CNode sz (\<lambda>a. if a = snd ptr then Some cap else fun a)) else kheap sa a) |` (- {idle_thread sa})) ptra)) = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptr. map_option (transform_object (machine_state sa) ptr ((ekheap sa |` (- {idle_thread sa})) ptr)) ((kheap sa |` (- {idle_thread sa})) ptr))
 2. \<And>sa ko tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some ko; kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb) \<and> arch_page_vmpage_size cap = arch_page_vmpage_size (getF tcb)\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = kernel_object.CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> a_type (kernel_object.CNode x xa) = a_type (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) else kheap sa a) sa) = transform sa) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_reply := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_caller := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap sa a) sa) = transform sa))))) proof (prove)
goal (2 subgoals):
 1. \<And>sa sz fun cte x. \<lbrakk>kheap sa (fst ptr) = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; transform_cap cap = transform_cap cte; arch_page_vmpage_size cap = arch_page_vmpage_size cte; fun (snd ptr) = Some cte; a_type (kernel_object.CNode sz fun) = a_type (kernel_object.CNode sz (\<lambda>a. if a = snd ptr then Some cap else fun a))\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptra. map_option (transform_object (machine_state sa) ptra ((ekheap sa |` (- {idle_thread sa})) ptra)) (((\<lambda>a. if a = fst ptr then Some (kernel_object.CNode sz (\<lambda>a. if a = snd ptr then Some cap else fun a)) else kheap sa a) |` (- {idle_thread sa})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptr. map_option (transform_object (machine_state sa) ptr ((ekheap sa |` (- {idle_thread sa})) ptr)) ((kheap sa |` (- {idle_thread sa})) ptr))) x
 2. \<And>sa ko tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some ko; kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb) \<and> arch_page_vmpage_size cap = arch_page_vmpage_size (getF tcb)\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = kernel_object.CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> a_type (kernel_object.CNode x xa) = a_type (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) else kheap sa a) sa) = transform sa) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_reply := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_caller := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap sa a) sa) = transform sa))))) proof (prove)
goal (2 subgoals):
 1. \<And>sa sz fun cte x. \<lbrakk>kheap sa (fst ptr) = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; transform_cap cap = transform_cap cte; arch_page_vmpage_size cap = arch_page_vmpage_size cte; fun (snd ptr) = Some cte; a_type (kernel_object.CNode sz fun) = a_type (kernel_object.CNode sz (fun(snd ptr \<mapsto> cap)))\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptra. map_option (transform_object (machine_state sa) ptra ((ekheap sa |` (- {idle_thread sa})) ptra)) (if ptra = fst ptr then Some (kernel_object.CNode sz (fun(snd ptr \<mapsto> cap))) else (kheap sa |` (- {idle_thread sa} - {fst ptr})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptr. map_option (transform_object (machine_state sa) ptr ((ekheap sa |` (- {idle_thread sa})) ptr)) ((kheap sa |` (- {idle_thread sa})) ptr))) x
 2. \<And>sa ko tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some ko; kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb) \<and> arch_page_vmpage_size cap = arch_page_vmpage_size (getF tcb)\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = kernel_object.CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> a_type (kernel_object.CNode x xa) = a_type (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) else kheap sa a) sa) = transform sa) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_reply := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_caller := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap sa a) sa) = transform sa))))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ko tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some ko; kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb) \<and> arch_page_vmpage_size cap = arch_page_vmpage_size (getF tcb)\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = kernel_object.CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> a_type (kernel_object.CNode x xa) = a_type (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (kernel_object.CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) else kheap sa a) sa) = transform sa) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_reply := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_caller := cap\<rparr>)) else kheap sa a) sa) = transform sa) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> transform (update_kheap (\<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap sa a) sa) = transform sa))))) proof (prove)
goal (1 subgoal):
 1. \<And>sa tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb); (case cap of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz) = (case getF tcb of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz)\<rbrakk> \<Longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> (\<forall>x. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptra. map_option (transform_object (machine_state sa) ptra ((ekheap sa |` (- {idle_thread sa})) ptra)) (((\<lambda>a. if a = fst ptr then Some (TCB (tcb\<lparr>tcb_ctable := cap\<rparr>)) else kheap sa a) |` (- {idle_thread sa})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptr. map_option (transform_object (machine_state sa) ptr ((ekheap sa |` (- {idle_thread sa})) ptr)) ((kheap sa |` (- {idle_thread sa})) ptr))) x)) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> (\<forall>x. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptra. map_option (transform_object (machine_state sa) ptra ((ekheap sa |` (- {idle_thread sa})) ptra)) (((\<lambda>a. if a = fst ptr then Some (TCB (tcb\<lparr>tcb_vtable := cap\<rparr>)) else kheap sa a) |` (- {idle_thread sa})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptr. map_option (transform_object (machine_state sa) ptr ((ekheap sa |` (- {idle_thread sa})) ptr)) ((kheap sa |` (- {idle_thread sa})) ptr))) x)) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> (\<forall>x. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptra. map_option (transform_object (machine_state sa) ptra ((ekheap sa |` (- {idle_thread sa})) ptra)) (((\<lambda>a. if a = fst ptr then Some (TCB (tcb\<lparr>tcb_reply := cap\<rparr>)) else kheap sa a) |` (- {idle_thread sa})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptr. map_option (transform_object (machine_state sa) ptr ((ekheap sa |` (- {idle_thread sa})) ptr)) ((kheap sa |` (- {idle_thread sa})) ptr))) x)) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> (\<forall>x. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptra. map_option (transform_object (machine_state sa) ptra ((ekheap sa |` (- {idle_thread sa})) ptra)) (((\<lambda>a. if a = fst ptr then Some (TCB (tcb\<lparr>tcb_caller := cap\<rparr>)) else kheap sa a) |` (- {idle_thread sa})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptr. map_option (transform_object (machine_state sa) ptr ((ekheap sa |` (- {idle_thread sa})) ptr)) ((kheap sa |` (- {idle_thread sa})) ptr))) x)) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>x. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptra. map_option (transform_object (machine_state sa) ptra ((ekheap sa |` (- {idle_thread sa})) ptra)) (((\<lambda>a. if a = fst ptr then Some (TCB (tcb\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap sa a) |` (- {idle_thread sa})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread sa}) ++ (\<lambda>ptr. map_option (transform_object (machine_state sa) ptr ((ekheap sa |` (- {idle_thread sa})) ptr)) ((kheap sa |` (- {idle_thread sa})) ptr))) x))))) proof (prove)
goal (1 subgoal):
 1. \<And>sa tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb); (case cap of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz) = (case getF tcb of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz)\<rbrakk> \<Longrightarrow> (\<exists>x2. ekheap sa (fst ptr) = Some x2) \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> (tcb_cspace_slot \<noteq> tcb_vspace_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_replycap_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_ctable tcb)) \<and> transform_full_intent (machine_state sa) (fst ptr) (tcb\<lparr>tcb_ctable := cap\<rparr>) = transform_full_intent (machine_state sa) (fst ptr) tcb) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> (tcb_vspace_slot \<noteq> tcb_replycap_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_vtable tcb)) \<and> transform_full_intent (machine_state sa) (fst ptr) (tcb\<lparr>tcb_vtable := cap\<rparr>) = transform_full_intent (machine_state sa) (fst ptr) tcb) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> (tcb_replycap_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_reply tcb)) \<and> transform_full_intent (machine_state sa) (fst ptr) (tcb\<lparr>tcb_reply := cap\<rparr>) = transform_full_intent (machine_state sa) (fst ptr) tcb) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> (tcb_caller_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_caller_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_caller_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_caller tcb)) \<and> transform_full_intent (machine_state sa) (fst ptr) (tcb\<lparr>tcb_caller := cap\<rparr>) = transform_full_intent (machine_state sa) (fst ptr) tcb) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> (tcb_ipcbuffer_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_ipcbuffer_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_ipcframe tcb)) \<and> transform_full_intent (machine_state sa) (fst ptr) (tcb\<lparr>tcb_ipcframe := cap\<rparr>) = transform_full_intent (machine_state sa) (fst ptr) tcb)))) proof (prove)
goal (2 subgoals):
 1. \<And>sa tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb); (case cap of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz) = (case getF tcb of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz); snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ms ns. get_ipc_buffer_words ms (tcb\<lparr>tcb_ipcframe := cap\<rparr>) ns = get_ipc_buffer_words ms tcb ns)\<rbrakk> \<Longrightarrow> (\<exists>x2. ekheap sa (fst ptr) = Some x2) \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> (tcb_cspace_slot \<noteq> tcb_vspace_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_replycap_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_ctable tcb)) \<and> transform_full_intent (machine_state sa) (fst ptr) (tcb\<lparr>tcb_ctable := cap\<rparr>) = transform_full_intent (machine_state sa) (fst ptr) tcb) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> (tcb_vspace_slot \<noteq> tcb_replycap_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_vtable tcb)) \<and> transform_full_intent (machine_state sa) (fst ptr) (tcb\<lparr>tcb_vtable := cap\<rparr>) = transform_full_intent (machine_state sa) (fst ptr) tcb) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> (tcb_replycap_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_reply tcb)) \<and> transform_full_intent (machine_state sa) (fst ptr) (tcb\<lparr>tcb_reply := cap\<rparr>) = transform_full_intent (machine_state sa) (fst ptr) tcb) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> (tcb_caller_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_caller_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_caller_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_caller tcb)) \<and> transform_full_intent (machine_state sa) (fst ptr) (tcb\<lparr>tcb_caller := cap\<rparr>) = transform_full_intent (machine_state sa) (fst ptr) tcb) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> (tcb_ipcbuffer_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_ipcbuffer_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_ipcframe tcb)) \<and> transform_full_intent (machine_state sa) (fst ptr) (tcb\<lparr>tcb_ipcframe := cap\<rparr>) = transform_full_intent (machine_state sa) (fst ptr) tcb))))
 2. \<And>sa tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb); (case cap of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz) = (case getF tcb of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz)\<rbrakk> \<Longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ms ns. get_ipc_buffer_words ms (tcb\<lparr>tcb_ipcframe := cap\<rparr>) ns = get_ipc_buffer_words ms tcb ns) proof (prove)
goal (2 subgoals):
 1. \<And>sa tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb); (case cap of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz) = (case getF tcb of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz); snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ms ns. get_ipc_buffer_words ms (tcb\<lparr>tcb_ipcframe := cap\<rparr>) ns = get_ipc_buffer_words ms tcb ns)\<rbrakk> \<Longrightarrow> (\<exists>x2. ekheap sa (fst ptr) = Some x2) \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> tcb_cspace_slot \<noteq> tcb_vspace_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_replycap_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_ctable tcb)) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> tcb_vspace_slot \<noteq> tcb_replycap_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_vtable tcb)) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> tcb_replycap_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_reply tcb)) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> tcb_caller_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_caller_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_caller_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_caller tcb)) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> (tcb_ipcbuffer_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_ipcbuffer_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_ipcframe tcb)) \<and> transform_full_intent (machine_state sa) (fst ptr) (tcb\<lparr>tcb_ipcframe := cap\<rparr>) = transform_full_intent (machine_state sa) (fst ptr) tcb))))
 2. \<And>sa tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb); (case cap of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz) = (case getF tcb of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz)\<rbrakk> \<Longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ms ns. get_ipc_buffer_words ms (tcb\<lparr>tcb_ipcframe := cap\<rparr>) ns = get_ipc_buffer_words ms tcb ns) proof (prove)
goal (2 subgoals):
 1. \<And>sa tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb); (case cap of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz) = (case getF tcb of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz); snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ms ns. get_ipc_buffer_words ms (tcb\<lparr>tcb_ipcframe := cap\<rparr>) ns = get_ipc_buffer_words ms tcb ns)\<rbrakk> \<Longrightarrow> (\<exists>x2. ekheap sa (fst ptr) = Some x2) \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> tcb_cspace_slot \<noteq> tcb_vspace_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_replycap_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_cspace_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_ctable tcb)) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> tcb_vspace_slot \<noteq> tcb_replycap_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_vspace_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_vtable tcb)) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> tcb_replycap_slot \<noteq> tcb_caller_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_replycap_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_reply tcb)) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> tcb_caller_slot \<noteq> tcb_ipcbuffer_slot \<longrightarrow> tcb_caller_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_caller_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_caller tcb)) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> fst ptr \<noteq> idle_thread sa \<longrightarrow> tcb_ipcbuffer_slot \<noteq> tcb_pending_op_slot \<longrightarrow> tcb_ipcbuffer_slot \<noteq> tcb_boundntfn_slot \<longrightarrow> transform_cap (getF tcb) = transform_cap (tcb_ipcframe tcb)))))
 2. \<And>sa tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb); (case cap of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz) = (case getF tcb of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz)\<rbrakk> \<Longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ms ns. get_ipc_buffer_words ms (tcb\<lparr>tcb_ipcframe := cap\<rparr>) ns = get_ipc_buffer_words ms tcb ns) proof (prove)
goal (1 subgoal):
 1. \<And>sa tcb getF setF restr. \<lbrakk>kheap sa (fst ptr) = Some (TCB tcb); tcb_cap_cases (snd ptr) = Some (getF, setF, restr); transform_cap cap = transform_cap (getF tcb); (case cap of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz) = (case getF tcb of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz)\<rbrakk> \<Longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ms ns. get_ipc_buffer_words ms (tcb\<lparr>tcb_ipcframe := cap\<rparr>) ns = get_ipc_buffer_words ms tcb ns) proof (prove)
goal (1 subgoal):
 1. \<And>sa tcb ms ns. \<lbrakk>kheap sa (fst ptr) = Some (TCB tcb); transform_cap cap = transform_cap (tcb_ipcframe tcb); (case cap of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz) = (case tcb_ipcframe tcb of ArchObjectCap (PageCap dev xa xaa sz xb) \<Rightarrow> sz); snd ptr = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> get_ipc_buffer_words ms (tcb\<lparr>tcb_ipcframe := cap\<rparr>) ns = get_ipc_buffer_words ms tcb ns proof (prove)
goal:
No subgoals!