theory Dpolicy

lemma opt_cap_None_word_bits:
  "\<lbrakk> einvs s; snd ptr \<ge> 2 ^ word_bits \<rbrakk> \<Longrightarrow> opt_cap ptr (transform s) = None" apply (case_tac ptr) apply (clarsimp simp:opt_cap_def transform_def transform_objects_def slots_of_def) apply (rule_tac P="a=idle_thread s" in case_split) apply (clarsimp simp: map_add_def object_slots_def) apply (case_tac "kheap s a") apply (clarsimp simp: map_add_def object_slots_def) apply (drule invs_valid_objs) apply (simp add:object_slots_def valid_objs_def) apply (case_tac aa, simp_all add: nat_split_conv_to_if
                             split: if_split_asm) apply (clarsimp simp:transform_cnode_contents_def object_slots_def) apply (drule_tac x=a in bspec) apply (simp add:dom_def)+ apply (clarsimp simp:valid_obj_def valid_cs_def valid_cs_size_def) apply (rule conjI) apply (clarsimp simp:option_map_join_def nat_to_bl_def) apply (metis gr0I le_antisym less_eq_Suc_le less_eq_nat.simps(1)
                  lt_word_bits_lt_pow zero_less_Suc) apply (clarsimp simp:option_map_join_def nat_to_bl_def) apply (drule not_le_imp_less) apply (subgoal_tac "b < 2 ^ word_bits") apply simp apply (rule less_trans) apply simp apply (rule power_strict_increasing, simp+) apply (frule valid_etcbs_tcb_etcb[rotated], fastforce) apply (clarsimp simp:transform_tcb_def tcb_slot_defs word_bits_def) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj; simp) apply (simp add:transform_asid_pool_contents_def transform_page_table_contents_def
                    transform_page_directory_contents_def unat_map_def word_bits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; 2 ^ word_bits \<le> snd ptr\<rbrakk> \<Longrightarrow> opt_cap ptr (transform s) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>einvs s; 2 ^ word_bits \<le> snd ptr; ptr = (a, b)\<rbrakk> \<Longrightarrow> opt_cap ptr (transform s) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) a of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = None proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); invs s; valid_list s; valid_sched s; a = idle_thread s\<rbrakk> \<Longrightarrow> (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) a of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = None
 2. \<And>a b. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) a of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = None proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) a of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = None proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = None\<rbrakk> \<Longrightarrow> (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) a of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = None
 2. \<And>a b aa. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some aa\<rbrakk> \<Longrightarrow> (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) a of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = None proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); invs s; valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some aa\<rbrakk> \<Longrightarrow> (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) a of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = None proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some aa; valid_objs s\<rbrakk> \<Longrightarrow> (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) a of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = None proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some aa; \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) aa of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (3 subgoals):
 1. \<And>a b aa x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> (x11 = 0 \<longrightarrow> transform_cnode_contents 0 x12 b = None) \<and> (0 < x11 \<longrightarrow> transform_cnode_contents x11 x12 b = None)
 2. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 3. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (3 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s\<rbrakk> \<Longrightarrow> (x11 = 0 \<longrightarrow> option_map_join x12 (nat_to_bl 0 b) = None) \<and> (0 < x11 \<longrightarrow> option_map_join x12 (nat_to_bl x11 b) = None)
 2. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 3. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (4 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12)\<rbrakk> \<Longrightarrow> a \<in> dom (kheap s)
 2. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<exists>obj. kheap s a = Some obj \<and> valid_obj a obj s\<rbrakk> \<Longrightarrow> (x11 = 0 \<longrightarrow> option_map_join x12 (nat_to_bl 0 b) = None) \<and> (0 < x11 \<longrightarrow> option_map_join x12 (nat_to_bl x11 b) = None)
 3. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 4. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (3 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); valid_obj a (kernel_object.CNode x11 x12) s\<rbrakk> \<Longrightarrow> (x11 = 0 \<longrightarrow> option_map_join x12 (nat_to_bl 0 b) = None) \<and> (0 < x11 \<longrightarrow> option_map_join x12 (nat_to_bl x11 b) = None)
 2. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 3. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (3 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> (x11 = 0 \<longrightarrow> option_map_join x12 (nat_to_bl 0 b) = None) \<and> (0 < x11 \<longrightarrow> option_map_join x12 (nat_to_bl x11 b) = None)
 2. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 3. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (4 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> x11 = 0 \<longrightarrow> option_map_join x12 (nat_to_bl 0 b) = None
 2. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> 0 < x11 \<longrightarrow> option_map_join x12 (nat_to_bl x11 b) = None
 3. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 4. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (4 subgoals):
 1. \<And>a b x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode 0 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; cte_level_bits < word_bits; well_formed_cnode_n 0 x12; \<not> Suc 0 \<le> b\<rbrakk> \<Longrightarrow> x12 [] = None
 2. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> 0 < x11 \<longrightarrow> option_map_join x12 (nat_to_bl x11 b) = None
 3. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 4. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (3 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> 0 < x11 \<longrightarrow> option_map_join x12 (nat_to_bl x11 b) = None
 2. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 3. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (3 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; \<not> 2 ^ x11 \<le> b; 0 < x11\<rbrakk> \<Longrightarrow> x12 (bin_to_bl_aux x11 (int b) []) = None
 2. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 3. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (3 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; 0 < x11; b < 2 ^ x11\<rbrakk> \<Longrightarrow> x12 (bin_to_bl_aux x11 (int b) []) = None
 2. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 3. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (4 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; 0 < x11; b < 2 ^ x11; b < 2 ^ word_bits\<rbrakk> \<Longrightarrow> x12 (bin_to_bl_aux x11 (int b) []) = None
 2. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; 0 < x11; b < 2 ^ x11\<rbrakk> \<Longrightarrow> b < 2 ^ word_bits
 3. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 4. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (3 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; 0 < x11; b < 2 ^ x11\<rbrakk> \<Longrightarrow> b < 2 ^ word_bits
 2. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 3. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (4 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; 0 < x11; b < 2 ^ x11\<rbrakk> \<Longrightarrow> b < ?y55 a b x11 x12
 2. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; 0 < x11; b < 2 ^ x11\<rbrakk> \<Longrightarrow> ?y55 a b x11 x12 < 2 ^ word_bits
 3. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 4. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (3 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; 0 < x11; b < 2 ^ x11\<rbrakk> \<Longrightarrow> 2 ^ x11 < 2 ^ word_bits
 2. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 3. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (2 subgoals):
 1. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 2. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (2 subgoals):
 1. \<And>a b aa x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (TCB x2); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = TCB x2; \<exists>etcb. ekheap s a = Some etcb\<rbrakk> \<Longrightarrow> (case case ekheap s a of Some etcb \<Rightarrow> transform_tcb (machine_state s) a x2 etcb of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None
 2. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (1 subgoal):
 1. \<And>a b aa x5. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj x5) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (1 subgoal):
 1. \<And>a b aa arch_kernel_obj. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj arch_kernel_obj); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> (case transform_object (machine_state s) a (ekheap s a) (ArchObj arch_kernel_obj) of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) b = None proof (prove)
goal (3 subgoals):
 1. \<And>a b aa arch_kernel_obj x1. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (ASIDPool x1)); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj (ASIDPool x1); arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> transform_asid_pool_contents x1 b = None
 2. \<And>a b aa arch_kernel_obj x2. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> transform_page_table_contents x2 b = None
 3. \<And>a b aa arch_kernel_obj x3. \<lbrakk>2 ^ word_bits \<le> b; ptr = (a, b); valid_list s; valid_sched s; a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> transform_page_directory_contents x3 b = None proof (prove)
goal:
No subgoals!