theory Dpolicy

lemma caps_of_state_transform_opt_cap_rev:
  "\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap;
     is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap \<rbrakk> \<Longrightarrow>
     \<exists>cap' ptr'. cap = transform_cap cap' \<and> ptr = transform_cslot_ptr ptr' \<and>
                 caps_of_state s ptr' = Some cap'" apply clarify apply (drule invs_valid_objs) apply (case_tac ptr) apply (clarsimp simp:opt_cap_def transform_def transform_objects_def
                       transform_cslot_ptr_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 (clarsimp simp:valid_objs_def dom_def) apply (drule_tac x=a in spec, clarsimp) apply (case_tac aa, simp_all add: object_slots_def caps_of_state_def2 nat_split_conv_to_if
                             split: if_split_asm) apply (clarsimp simp:valid_obj_def valid_cs_def valid_cs_size_def) apply (clarsimp simp:transform_cnode_contents_def) apply (rule_tac x=z in exI, simp) apply (rule_tac x="the (nat_to_bl 0 b)" in exI) apply (clarsimp simp:option_map_join_def split:option.splits) apply (rule nat_to_bl_to_bin, simp+) apply (clarsimp simp:valid_obj_def valid_cs_def valid_cs_size_def) apply (clarsimp simp:transform_cnode_contents_def) apply (rule_tac x=z in exI, simp) apply (rename_tac n list cap') apply (rule_tac x="the (nat_to_bl n b)" in exI) apply (clarsimp simp:option_map_join_def split:option.splits) apply (rule nat_to_bl_to_bin, simp+) apply (drule valid_etcbs_tcb_etcb [rotated], fastforce) apply clarsimp apply (clarsimp simp:transform_tcb_def tcb_slot_defs split:if_split_asm) apply (clarsimp simp: is_null_cap_def is_bound_ntfn_cap_def infer_tcb_bound_notification_def
                         split: option.splits) apply (simp add:is_thread_state_cap_def infer_tcb_pending_op_def is_null_cap_def is_real_cap_def
                    split:Structures_A.thread_state.splits option.splits) apply (rule exI, rule conjI, simp, rule exI, rule conjI,
              (rule bl_to_bin_tcb_cnode_index | rule bl_to_bin_tcb_cnode_index[symmetric]),
              simp, simp add:tcb_cap_cases_def)+ apply (rule exI, rule conjI, simp) apply (rule_tac x="tcb_cnode_index 0" in exI) apply (subst bl_to_bin_tcb_cnode_index_le0; simp) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj; simp) apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def split:if_split_asm) apply (clarsimp simp:is_real_cap_def is_null_cap_def transform_asid_pool_entry_def
                    split:option.splits) apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:if_split_asm) apply (clarsimp simp:is_real_cap_def is_null_cap_def transform_pte_def
                   split:ARM_A.pte.splits) apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:if_split_asm) apply (clarsimp simp:is_real_cap_def is_null_cap_def transform_pde_def
                  split:ARM_A.pde.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; opt_cap ptr (transform s) = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> \<exists>cap' ptr'. cap = transform_cap cap' \<and> ptr = transform_cslot_ptr ptr' \<and> caps_of_state s ptr' = Some cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>opt_cap ptr (transform s) = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; invs s; valid_list s\<rbrakk> \<Longrightarrow> \<exists>cap' ptr'. cap = transform_cap cap' \<and> ptr = transform_cslot_ptr ptr' \<and> caps_of_state s ptr' = Some cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>opt_cap ptr (transform s) = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; valid_objs s\<rbrakk> \<Longrightarrow> \<exists>cap' ptr'. cap = transform_cap cap' \<and> ptr = transform_cslot_ptr ptr' \<and> caps_of_state s ptr' = Some cap' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>opt_cap ptr (transform s) = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; valid_objs s; ptr = (a, b)\<rbrakk> \<Longrightarrow> \<exists>cap' ptr'. cap = transform_cap cap' \<and> ptr = transform_cslot_ptr ptr' \<and> caps_of_state s ptr' = Some cap' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; valid_objs s; ptr = (a, b)\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> caps_of_state s (a, ba) = Some cap') proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; valid_objs s; ptr = (a, b); a = idle_thread s\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> caps_of_state s (a, ba) = Some cap')
 2. \<And>a b. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; valid_objs s; ptr = (a, b); a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> caps_of_state s (a, ba) = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; valid_objs s; ptr = (a, b); a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> caps_of_state s (a, ba) = Some cap') proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; valid_objs s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = None\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> caps_of_state s (a, ba) = Some cap')
 2. \<And>a b aa. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; valid_objs s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some aa\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> caps_of_state s (a, ba) = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; valid_objs s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some aa\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> caps_of_state s (a, ba) = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>object_slots (transform_object (machine_state s) a (ekheap s a) aa) b = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some aa\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> caps_of_state s (a, ba) = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>object_slots (transform_object (machine_state s) a (ekheap s a) aa) b = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some aa; valid_obj a aa s\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> caps_of_state s (a, ba) = Some cap') proof (prove)
goal (4 subgoals):
 1. \<And>a b aa x11 x12. \<lbrakk>is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode 0 x12); valid_obj a (kernel_object.CNode 0 x12) s; aa = kernel_object.CNode 0 x12; x11 = 0; transform_cnode_contents 0 x12 b = Some cap\<rbrakk> \<Longrightarrow> (well_formed_cnode_n 0 x12 \<longrightarrow> (\<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap'))) \<and> well_formed_cnode_n 0 x12
 2. \<And>a b aa x11 x12. \<lbrakk>is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); valid_obj a (kernel_object.CNode x11 x12) s; aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> (well_formed_cnode_n x11 x12 \<longrightarrow> (\<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap'))) \<and> well_formed_cnode_n x11 x12
 3. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 4. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a b x12. \<lbrakk>is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode 0 x12); transform_cnode_contents 0 x12 b = Some cap; \<forall>cap\<in>ran x12. s \<turnstile> cap; cte_level_bits < word_bits; well_formed_cnode_n 0 x12\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap')
 2. \<And>a b aa x11 x12. \<lbrakk>is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); valid_obj a (kernel_object.CNode x11 x12) s; aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> (well_formed_cnode_n x11 x12 \<longrightarrow> (\<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap'))) \<and> well_formed_cnode_n x11 x12
 3. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 4. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a b x12 z. \<lbrakk>is_real_cap (transform_cap z); \<not> is_thread_state_cap (transform_cap z); \<not> is_null_cap (transform_cap z); \<not> is_bound_ntfn_cap (transform_cap z); valid_sched s; valid_list s; ptr = (a, b); 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; option_map_join x12 (nat_to_bl 0 b) = Some z; cap = transform_cap z\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap z = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap')
 2. \<And>a b aa x11 x12. \<lbrakk>is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); valid_obj a (kernel_object.CNode x11 x12) s; aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> (well_formed_cnode_n x11 x12 \<longrightarrow> (\<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap'))) \<and> well_formed_cnode_n x11 x12
 3. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 4. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a b x12 z. \<lbrakk>is_real_cap (transform_cap z); \<not> is_thread_state_cap (transform_cap z); \<not> is_null_cap (transform_cap z); \<not> is_bound_ntfn_cap (transform_cap z); valid_sched s; valid_list s; ptr = (a, b); 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; option_map_join x12 (nat_to_bl 0 b) = Some z; cap = transform_cap z\<rbrakk> \<Longrightarrow> \<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some z
 2. \<And>a b aa x11 x12. \<lbrakk>is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); valid_obj a (kernel_object.CNode x11 x12) s; aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> (well_formed_cnode_n x11 x12 \<longrightarrow> (\<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap'))) \<and> well_formed_cnode_n x11 x12
 3. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 4. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a b x12 z. \<lbrakk>is_real_cap (transform_cap z); \<not> is_thread_state_cap (transform_cap z); \<not> is_null_cap (transform_cap z); \<not> is_bound_ntfn_cap (transform_cap z); valid_sched s; valid_list s; ptr = (a, b); 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; option_map_join x12 (nat_to_bl 0 b) = Some z; cap = transform_cap z\<rbrakk> \<Longrightarrow> b = nat (bl_to_bin (the (nat_to_bl 0 b))) \<and> x12 (the (nat_to_bl 0 b)) = Some z
 2. \<And>a b aa x11 x12. \<lbrakk>is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); valid_obj a (kernel_object.CNode x11 x12) s; aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> (well_formed_cnode_n x11 x12 \<longrightarrow> (\<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap'))) \<and> well_formed_cnode_n x11 x12
 3. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 4. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a b x12 z x2. \<lbrakk>cap = transform_cap z; is_real_cap (transform_cap z); \<not> is_thread_state_cap (transform_cap z); \<not> is_null_cap (transform_cap z); \<not> is_bound_ntfn_cap (transform_cap z); valid_sched s; valid_list s; ptr = (a, b); 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; nat_to_bl 0 b = Some x2; x12 x2 = Some z\<rbrakk> \<Longrightarrow> b = nat (bl_to_bin x2)
 2. \<And>a b aa x11 x12. \<lbrakk>is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); valid_obj a (kernel_object.CNode x11 x12) s; aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> (well_formed_cnode_n x11 x12 \<longrightarrow> (\<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap'))) \<and> well_formed_cnode_n x11 x12
 3. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 4. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b aa x11 x12. \<lbrakk>is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); valid_obj a (kernel_object.CNode x11 x12) s; aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> (well_formed_cnode_n x11 x12 \<longrightarrow> (\<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap'))) \<and> well_formed_cnode_n x11 x12
 2. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 3. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); 0 < x11; transform_cnode_contents x11 x12 b = Some cap; \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap')
 2. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 3. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b x11 x12 z. \<lbrakk>is_real_cap (transform_cap z); \<not> is_thread_state_cap (transform_cap z); \<not> is_null_cap (transform_cap z); \<not> is_bound_ntfn_cap (transform_cap z); valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); 0 < x11; \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; option_map_join x12 (nat_to_bl x11 b) = Some z; cap = transform_cap z\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap z = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some cap')
 2. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 3. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b x11 x12 z. \<lbrakk>is_real_cap (transform_cap z); \<not> is_thread_state_cap (transform_cap z); \<not> is_null_cap (transform_cap z); \<not> is_bound_ntfn_cap (transform_cap z); valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); 0 < x11; \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; option_map_join x12 (nat_to_bl x11 b) = Some z; cap = transform_cap z\<rbrakk> \<Longrightarrow> \<exists>ba. b = nat (bl_to_bin ba) \<and> x12 ba = Some z
 2. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 3. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b n list cap'. \<lbrakk>is_real_cap (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> is_bound_ntfn_cap (transform_cap cap'); valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode n list); 0 < n; \<forall>cap\<in>ran list. s \<turnstile> cap; n < word_bits - cte_level_bits; well_formed_cnode_n n list; option_map_join list (nat_to_bl n b) = Some cap'; cap = transform_cap cap'\<rbrakk> \<Longrightarrow> \<exists>ba. b = nat (bl_to_bin ba) \<and> list ba = Some cap'
 2. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 3. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b n list cap'. \<lbrakk>is_real_cap (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> is_bound_ntfn_cap (transform_cap cap'); valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode n list); 0 < n; \<forall>cap\<in>ran list. s \<turnstile> cap; n < word_bits - cte_level_bits; well_formed_cnode_n n list; option_map_join list (nat_to_bl n b) = Some cap'; cap = transform_cap cap'\<rbrakk> \<Longrightarrow> b = nat (bl_to_bin (the (nat_to_bl n b))) \<and> list (the (nat_to_bl n b)) = Some cap'
 2. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 3. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b n list cap' x2. \<lbrakk>cap = transform_cap cap'; is_real_cap (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> is_bound_ntfn_cap (transform_cap cap'); valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode n list); 0 < n; \<forall>cap\<in>ran list. s \<turnstile> cap; n < word_bits - cte_level_bits; well_formed_cnode_n n list; nat_to_bl n b = Some x2; list x2 = Some cap'\<rbrakk> \<Longrightarrow> b = nat (bl_to_bin x2)
 2. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 3. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (TCB x2); valid_obj a (TCB x2) s; aa = TCB x2\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 2. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b aa x2. \<lbrakk>(case case ekheap s a of Some x2a \<Rightarrow> transform_tcb (machine_state s) a x2 x2a 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; aa = TCB x2; \<exists>etcb. ekheap s a = Some etcb\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 2. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b x2 etcb. \<lbrakk>(case 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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb\<rbrakk> \<Longrightarrow> \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>ba. b = nat (bl_to_bin ba) \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases ba = Some (a, aa, b)) \<and> a x2 = cap'))
 2. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (8 subgoals):
 1. \<And>a x2 etcb. \<lbrakk>is_real_cap (infer_tcb_bound_notification (tcb_bound_notification x2)); \<not> is_thread_state_cap (infer_tcb_bound_notification (tcb_bound_notification x2)); \<not> is_null_cap (infer_tcb_bound_notification (tcb_bound_notification x2)); \<not> is_bound_ntfn_cap (infer_tcb_bound_notification (tcb_bound_notification x2)); valid_sched s; valid_list s; ptr = (a, 6); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = infer_tcb_bound_notification (tcb_bound_notification x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. infer_tcb_bound_notification (tcb_bound_notification x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 6 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 2. \<And>a x2 etcb. \<lbrakk>is_real_cap (infer_tcb_pending_op a (tcb_state x2)); \<not> is_thread_state_cap (infer_tcb_pending_op a (tcb_state x2)); \<not> is_null_cap (infer_tcb_pending_op a (tcb_state x2)); \<not> is_bound_ntfn_cap (infer_tcb_pending_op a (tcb_state x2)); valid_sched s; valid_list s; ptr = (a, 5); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = infer_tcb_pending_op a (tcb_state x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. infer_tcb_pending_op a (tcb_state x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 5 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 3. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_ipcframe x2)); \<not> is_thread_state_cap (transform_cap (tcb_ipcframe x2)); \<not> is_null_cap (transform_cap (tcb_ipcframe x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_ipcframe x2)); valid_sched s; valid_list s; ptr = (a, 4); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_ipcframe x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_ipcframe x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 4 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 4. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_caller x2)); \<not> is_thread_state_cap (transform_cap (tcb_caller x2)); \<not> is_null_cap (transform_cap (tcb_caller x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_caller x2)); valid_sched s; valid_list s; ptr = (a, 3); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_caller x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_caller x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 3 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 5. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_reply x2)); \<not> is_thread_state_cap (transform_cap (tcb_reply x2)); \<not> is_null_cap (transform_cap (tcb_reply x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_reply x2)); valid_sched s; valid_list s; ptr = (a, 2); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_reply x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_reply x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 2 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 6. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_vtable x2)); \<not> is_thread_state_cap (transform_cap (tcb_vtable x2)); \<not> is_null_cap (transform_cap (tcb_vtable x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_vtable x2)); valid_sched s; valid_list s; ptr = (a, Suc 0); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_vtable x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_vtable x2) = transform_cap cap' \<and> (\<exists>b. Suc 0 = nat (bl_to_bin b) \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 7. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_ctable x2)); \<not> is_thread_state_cap (transform_cap (tcb_ctable x2)); \<not> is_null_cap (transform_cap (tcb_ctable x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_ctable x2)); valid_sched s; valid_list s; ptr = (a, 0); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_ctable x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_ctable x2) = transform_cap cap' \<and> (\<exists>b. bl_to_bin b \<le> 0 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 8. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (7 subgoals):
 1. \<And>a x2 etcb. \<lbrakk>is_real_cap (infer_tcb_pending_op a (tcb_state x2)); \<not> is_thread_state_cap (infer_tcb_pending_op a (tcb_state x2)); \<not> is_null_cap (infer_tcb_pending_op a (tcb_state x2)); \<not> is_bound_ntfn_cap (infer_tcb_pending_op a (tcb_state x2)); valid_sched s; valid_list s; ptr = (a, 5); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = infer_tcb_pending_op a (tcb_state x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. infer_tcb_pending_op a (tcb_state x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 5 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 2. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_ipcframe x2)); \<not> is_thread_state_cap (transform_cap (tcb_ipcframe x2)); \<not> is_null_cap (transform_cap (tcb_ipcframe x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_ipcframe x2)); valid_sched s; valid_list s; ptr = (a, 4); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_ipcframe x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_ipcframe x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 4 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 3. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_caller x2)); \<not> is_thread_state_cap (transform_cap (tcb_caller x2)); \<not> is_null_cap (transform_cap (tcb_caller x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_caller x2)); valid_sched s; valid_list s; ptr = (a, 3); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_caller x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_caller x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 3 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 4. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_reply x2)); \<not> is_thread_state_cap (transform_cap (tcb_reply x2)); \<not> is_null_cap (transform_cap (tcb_reply x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_reply x2)); valid_sched s; valid_list s; ptr = (a, 2); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_reply x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_reply x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 2 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 5. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_vtable x2)); \<not> is_thread_state_cap (transform_cap (tcb_vtable x2)); \<not> is_null_cap (transform_cap (tcb_vtable x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_vtable x2)); valid_sched s; valid_list s; ptr = (a, Suc 0); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_vtable x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_vtable x2) = transform_cap cap' \<and> (\<exists>b. Suc 0 = nat (bl_to_bin b) \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 6. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_ctable x2)); \<not> is_thread_state_cap (transform_cap (tcb_ctable x2)); \<not> is_null_cap (transform_cap (tcb_ctable x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_ctable x2)); valid_sched s; valid_list s; ptr = (a, 0); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_ctable x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_ctable x2) = transform_cap cap' \<and> (\<exists>b. bl_to_bin b \<le> 0 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 7. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_ipcframe x2)); \<not> is_thread_state_cap (transform_cap (tcb_ipcframe x2)); \<not> is_null_cap (transform_cap (tcb_ipcframe x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_ipcframe x2)); valid_sched s; valid_list s; ptr = (a, 4); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_ipcframe x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_ipcframe x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 4 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 2. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_caller x2)); \<not> is_thread_state_cap (transform_cap (tcb_caller x2)); \<not> is_null_cap (transform_cap (tcb_caller x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_caller x2)); valid_sched s; valid_list s; ptr = (a, 3); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_caller x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_caller x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 3 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 3. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_reply x2)); \<not> is_thread_state_cap (transform_cap (tcb_reply x2)); \<not> is_null_cap (transform_cap (tcb_reply x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_reply x2)); valid_sched s; valid_list s; ptr = (a, 2); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_reply x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_reply x2) = transform_cap cap' \<and> (\<exists>b. nat (bl_to_bin b) = 2 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 4. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_vtable x2)); \<not> is_thread_state_cap (transform_cap (tcb_vtable x2)); \<not> is_null_cap (transform_cap (tcb_vtable x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_vtable x2)); valid_sched s; valid_list s; ptr = (a, Suc 0); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_vtable x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_vtable x2) = transform_cap cap' \<and> (\<exists>b. Suc 0 = nat (bl_to_bin b) \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 5. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_ctable x2)); \<not> is_thread_state_cap (transform_cap (tcb_ctable x2)); \<not> is_null_cap (transform_cap (tcb_ctable x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_ctable x2)); valid_sched s; valid_list s; ptr = (a, 0); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_ctable x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_ctable x2) = transform_cap cap' \<and> (\<exists>b. bl_to_bin b \<le> 0 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 6. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_ctable x2)); \<not> is_thread_state_cap (transform_cap (tcb_ctable x2)); \<not> is_null_cap (transform_cap (tcb_ctable x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_ctable x2)); valid_sched s; valid_list s; ptr = (a, 0); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_ctable x2)\<rbrakk> \<Longrightarrow> \<exists>cap'. transform_cap (tcb_ctable x2) = transform_cap cap' \<and> (\<exists>b. bl_to_bin b \<le> 0 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = cap'))
 2. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_ctable x2)); \<not> is_thread_state_cap (transform_cap (tcb_ctable x2)); \<not> is_null_cap (transform_cap (tcb_ctable x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_ctable x2)); valid_sched s; valid_list s; ptr = (a, 0); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_ctable x2)\<rbrakk> \<Longrightarrow> \<exists>b. bl_to_bin b \<le> 0 \<and> (\<exists>a. (\<exists>aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<and> a x2 = tcb_ctable x2)
 2. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a x2 etcb. \<lbrakk>is_real_cap (transform_cap (tcb_ctable x2)); \<not> is_thread_state_cap (transform_cap (tcb_ctable x2)); \<not> is_null_cap (transform_cap (tcb_ctable x2)); \<not> is_bound_ntfn_cap (transform_cap (tcb_ctable x2)); valid_sched s; valid_list s; ptr = (a, 0); a \<noteq> idle_thread s; valid_obj a (TCB x2) s; ekheap s a = Some etcb; cap = transform_cap (tcb_ctable x2)\<rbrakk> \<Longrightarrow> bl_to_bin (tcb_cnode_index 0) \<le> 0 \<and> (\<exists>a. (\<exists>aa b. tcb_cap_cases (tcb_cnode_index 0) = Some (a, aa, b)) \<and> a x2 = tcb_ctable x2)
 2. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa x5. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); valid_obj a (ArchObj x5) s; aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa arch_kernel_obj. \<lbrakk>(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 = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj arch_kernel_obj); valid_obj a (ArchObj arch_kernel_obj) s; aa = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b aa arch_kernel_obj x1. \<lbrakk>transform_asid_pool_contents x1 b = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (ASIDPool x1)); valid_obj a (ArchObj (ASIDPool x1)) s; aa = ArchObj (ASIDPool x1); arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa arch_kernel_obj x2. \<lbrakk>transform_page_table_contents x2 b = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); valid_obj a (ArchObj (arch_kernel_obj.PageTable x2)) s; aa = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> False
 3. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); valid_obj a (ArchObj (arch_kernel_obj.PageDirectory x3)) s; aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b x1. \<lbrakk>is_real_cap (transform_asid_pool_entry (x1 (word_of_nat b))); \<not> is_thread_state_cap (transform_asid_pool_entry (x1 (word_of_nat b))); \<not> is_null_cap (transform_asid_pool_entry (x1 (word_of_nat b))); \<not> is_bound_ntfn_cap (transform_asid_pool_entry (x1 (word_of_nat b))); valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (ASIDPool x1)); valid_obj a (ArchObj (ASIDPool x1)) s; b < 1024; cap = transform_asid_pool_entry (x1 (word_of_nat b))\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa arch_kernel_obj x2. \<lbrakk>transform_page_table_contents x2 b = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); valid_obj a (ArchObj (arch_kernel_obj.PageTable x2)) s; aa = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> False
 3. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); valid_obj a (ArchObj (arch_kernel_obj.PageDirectory x3)) s; aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b aa arch_kernel_obj x2. \<lbrakk>transform_page_table_contents x2 b = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); valid_obj a (ArchObj (arch_kernel_obj.PageTable x2)) s; aa = ArchObj (arch_kernel_obj.PageTable x2); arch_kernel_obj = arch_kernel_obj.PageTable x2\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); valid_obj a (ArchObj (arch_kernel_obj.PageDirectory x3)) s; aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b x2. \<lbrakk>is_real_cap (transform_pte (x2 (word_of_nat b))); \<not> is_thread_state_cap (transform_pte (x2 (word_of_nat b))); \<not> is_null_cap (transform_pte (x2 (word_of_nat b))); \<not> is_bound_ntfn_cap (transform_pte (x2 (word_of_nat b))); valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); valid_obj a (ArchObj (arch_kernel_obj.PageTable x2)) s; b < 256; cap = transform_pte (x2 (word_of_nat b))\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); valid_obj a (ArchObj (arch_kernel_obj.PageDirectory x3)) s; aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa arch_kernel_obj x3. \<lbrakk>transform_page_directory_contents x3 b = Some cap; is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); valid_obj a (ArchObj (arch_kernel_obj.PageDirectory x3)) s; aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b x3. \<lbrakk>is_real_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_thread_state_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_null_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); \<not> is_bound_ntfn_cap (transform_pde (kernel_pde_mask x3 (word_of_nat b))); valid_sched s; valid_list s; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); valid_obj a (ArchObj (arch_kernel_obj.PageDirectory x3)) s; b < 4096; cap = transform_pde (kernel_pde_mask x3 (word_of_nat b))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!