theory Dpolicy

lemma thread_state_cap_transform_tcb:
  "\<lbrakk> opt_cap ptr (transform s) = Some cap; is_thread_state_cap cap \<rbrakk> \<Longrightarrow>
     \<exists>tcb. get_tcb (fst ptr) s = Some tcb" apply (case_tac ptr) apply (simp add:opt_cap_def slots_of_def transform_def transform_objects_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 (fst ptr)") apply (clarsimp simp: map_add_def object_slots_def) apply (simp add:get_tcb_def object_slots_def) apply (case_tac aa, simp_all add: nat_split_conv_to_if
                             split: if_split_asm) apply (clarsimp simp:transform_cnode_contents_def) apply (case_tac z, simp_all add:is_thread_state_cap_def split:if_split_asm) apply (rename_tac arch_cap) apply (case_tac arch_cap; simp) apply (clarsimp simp:transform_cnode_contents_def) apply (case_tac z, simp_all add:is_thread_state_cap_def split:if_split_asm) apply (rename_tac arch_cap) apply (case_tac arch_cap; 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 transform_asid_pool_entry_def
                    split:if_split_asm option.splits) apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def
                   split:if_split_asm ARM_A.pte.splits) apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def
                   split:if_split_asm ARM_A.pde.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>opt_cap ptr (transform s) = Some cap; is_thread_state_cap cap\<rbrakk> \<Longrightarrow> \<exists>tcb. get_tcb (fst ptr) s = Some tcb proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>opt_cap ptr (transform s) = Some cap; is_thread_state_cap cap; ptr = (a, b)\<rbrakk> \<Longrightarrow> \<exists>tcb. get_tcb (fst ptr) s = Some tcb 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_thread_state_cap cap; ptr = (a, b)\<rbrakk> \<Longrightarrow> \<exists>tcb. get_tcb a s = Some tcb 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_thread_state_cap cap; ptr = (a, b); a = idle_thread s\<rbrakk> \<Longrightarrow> \<exists>tcb. get_tcb a s = Some tcb
 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_thread_state_cap cap; ptr = (a, b); a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<exists>tcb. get_tcb a s = Some tcb 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_thread_state_cap cap; ptr = (a, b); a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<exists>tcb. get_tcb a s = Some tcb 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_thread_state_cap cap; ptr = (a, b); a \<noteq> idle_thread s; kheap s (fst ptr) = None\<rbrakk> \<Longrightarrow> \<exists>tcb. get_tcb a s = Some tcb
 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_thread_state_cap cap; ptr = (a, b); a \<noteq> idle_thread s; kheap s (fst ptr) = Some aa\<rbrakk> \<Longrightarrow> \<exists>tcb. get_tcb a s = Some tcb 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_thread_state_cap cap; ptr = (a, b); a \<noteq> idle_thread s; kheap s (fst ptr) = Some aa\<rbrakk> \<Longrightarrow> \<exists>tcb. get_tcb a s = Some tcb proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>(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 = Some cap; is_thread_state_cap cap; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some aa\<rbrakk> \<Longrightarrow> \<exists>tcb. (case aa of TCB x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some tcb proof (prove)
goal (3 subgoals):
 1. \<And>a b aa x11 x12. \<lbrakk>is_thread_state_cap cap; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode 0 x12); aa = kernel_object.CNode 0 x12; x11 = 0; transform_cnode_contents 0 x12 b = Some cap\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa x11 x12. \<lbrakk>is_thread_state_cap cap; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> False
 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_thread_state_cap cap; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b x12 z. \<lbrakk>is_thread_state_cap (transform_cap z); ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode 0 x12); option_map_join x12 (nat_to_bl 0 b) = Some z; cap = transform_cap z\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa x11 x12. \<lbrakk>is_thread_state_cap cap; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> False
 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_thread_state_cap cap; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b x12 z x12a. \<lbrakk>case transform_cap (ArchObjectCap x12a) of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode 0 x12); option_map_join x12 (nat_to_bl 0 b) = Some (ArchObjectCap x12a); cap = transform_cap (ArchObjectCap x12a); z = ArchObjectCap x12a\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa x11 x12. \<lbrakk>case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> False
 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b x12 z arch_cap. \<lbrakk>case transform_cap (ArchObjectCap arch_cap) of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode 0 x12); option_map_join x12 (nat_to_bl 0 b) = Some (ArchObjectCap arch_cap); cap = transform_cap (ArchObjectCap arch_cap); z = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa x11 x12. \<lbrakk>case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> False
 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b aa x11 x12. \<lbrakk>case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); aa = kernel_object.CNode x11 x12; 0 < x11; transform_cnode_contents x11 x12 b = Some cap\<rbrakk> \<Longrightarrow> False
 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b x11 x12 z. \<lbrakk>case transform_cap z of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); 0 < x11; option_map_join x12 (nat_to_bl x11 b) = Some z; cap = transform_cap z\<rbrakk> \<Longrightarrow> False
 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b x11 x12 z x12a. \<lbrakk>case transform_cap (ArchObjectCap x12a) of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); 0 < x11; option_map_join x12 (nat_to_bl x11 b) = Some (ArchObjectCap x12a); cap = transform_cap (ArchObjectCap x12a); z = ArchObjectCap x12a\<rbrakk> \<Longrightarrow> False
 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b x11 x12 z arch_cap. \<lbrakk>case transform_cap (ArchObjectCap arch_cap) of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (kernel_object.CNode x11 x12); 0 < x11; option_map_join x12 (nat_to_bl x11 b) = Some (ArchObjectCap arch_cap); cap = transform_cap (ArchObjectCap arch_cap); z = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> False
 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj x5); 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj arch_kernel_obj); 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (ASIDPool x1)); 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2)); 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); 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; case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> True | PendingSyncRecvCap x xa xb \<Rightarrow> True | PendingNtfnRecvCap x \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | _ \<Rightarrow> False; ptr = (a, b); a \<noteq> idle_thread s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); aa = ArchObj (arch_kernel_obj.PageDirectory x3); arch_kernel_obj = arch_kernel_obj.PageDirectory x3\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!