theory Intent_DR

lemma select_f_get_register:
  "(as_user thread (getRegister register)) =
    (do tcb\<leftarrow>gets_the (get_tcb thread);return (arch_tcb_context_get (tcb_arch tcb) register) od)" apply (simp add: assert_opt_def as_user_def set_object_def get_object_def gets_the_def
                   a_type_def assert_def put_def select_f_def getRegister_def gets_def get_def
                   return_def bind_def) apply (rule ext) apply (case_tac "get_tcb thread s") apply (clarsimp simp: fail_def return_def)+ apply (clarsimp simp: get_tcb_def split: option.splits Structures_A.kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. as_user thread (getRegister register) = do tcb <- gets_the (get_tcb thread);
return (arch_tcb_context_get (tcb_arch tcb) register)
od proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. (\<Union>a\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). fst (case a of (tcb, s) \<Rightarrow> (\<Union>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<Union>x\<in>fst (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<Union>x\<in>fst (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). fst (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>y\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<exists>x\<in>fst (case y of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). snd (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>x\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). snd (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s)))) \<or> (\<exists>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). snd (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False))) \<or> snd ((if \<exists>y. kheap s thread = Some y then return () else fail) s))), (\<exists>x\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). snd (case x of (tcb, s) \<Rightarrow> (\<Union>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<Union>x\<in>fst (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<Union>x\<in>fst (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). fst (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>y\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<exists>x\<in>fst (case y of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). snd (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>x\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). snd (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s)))) \<or> (\<exists>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). snd (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False))) \<or> snd ((if \<exists>y. kheap s thread = Some y then return () else fail) s)))) \<or> snd ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s))) = (\<lambda>s. (\<Union>a\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). fst (case a of (tcb, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>x\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). snd (case x of (tcb, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> snd ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>a\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). fst (case a of (tcb, s) \<Rightarrow> (\<Union>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<Union>x\<in>fst (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<Union>x\<in>fst (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). fst (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>y\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<exists>x\<in>fst (case y of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). snd (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>x\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). snd (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s)))) \<or> (\<exists>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). snd (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False))) \<or> snd ((if \<exists>y. kheap s thread = Some y then return () else fail) s))), (\<exists>x\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). snd (case x of (tcb, s) \<Rightarrow> (\<Union>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<Union>x\<in>fst (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<Union>x\<in>fst (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). fst (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>y\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<exists>x\<in>fst (case y of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). snd (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>x\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). snd (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s)))) \<or> (\<exists>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). snd (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False))) \<or> snd ((if \<exists>y. kheap s thread = Some y then return () else fail) s)))) \<or> snd ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s)) = (\<Union>a\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). fst (case a of (tcb, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>x\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). snd (case x of (tcb, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> snd ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. get_tcb thread s = None \<Longrightarrow> (\<Union>a\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). fst (case a of (tcb, s) \<Rightarrow> (\<Union>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<Union>x\<in>fst (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<Union>x\<in>fst (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). fst (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>y\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<exists>x\<in>fst (case y of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). snd (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>x\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). snd (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s)))) \<or> (\<exists>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). snd (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False))) \<or> snd ((if \<exists>y. kheap s thread = Some y then return () else fail) s))), (\<exists>x\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). snd (case x of (tcb, s) \<Rightarrow> (\<Union>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<Union>x\<in>fst (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<Union>x\<in>fst (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). fst (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>y\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<exists>x\<in>fst (case y of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). snd (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>x\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). snd (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s)))) \<or> (\<exists>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). snd (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False))) \<or> snd ((if \<exists>y. kheap s thread = Some y then return () else fail) s)))) \<or> snd ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s)) = (\<Union>a\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). fst (case a of (tcb, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>x\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). snd (case x of (tcb, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> snd ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s))
 2. \<And>s a. get_tcb thread s = Some a \<Longrightarrow> (\<Union>a\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). fst (case a of (tcb, s) \<Rightarrow> (\<Union>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<Union>x\<in>fst (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<Union>x\<in>fst (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). fst (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>y\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<exists>x\<in>fst (case y of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). snd (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>x\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). snd (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s)))) \<or> (\<exists>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). snd (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False))) \<or> snd ((if \<exists>y. kheap s thread = Some y then return () else fail) s))), (\<exists>x\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). snd (case x of (tcb, s) \<Rightarrow> (\<Union>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<Union>x\<in>fst (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<Union>x\<in>fst (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). fst (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>y\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). \<exists>x\<in>fst (case y of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s))). snd (case x of (y, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> (\<exists>y\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). \<exists>x\<in>fst (case y of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False)). snd (case x of (kobj, s) \<Rightarrow> (\<Union>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). fst (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False)), (\<exists>x\<in>fst ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s). snd (case x of (y, s) \<Rightarrow> ({((), update_kheap ((kheap s)(thread \<mapsto> TCB tcb)) s)}, False))) \<or> snd ((if (case kobj of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB then return () else fail) s)))) \<or> (\<exists>x\<in>fst ((if \<exists>y. kheap s thread = Some y then return () else fail) s). snd (case x of (y, sa) \<Rightarrow> ({(the (kheap s thread), sa)}, False))) \<or> snd ((if \<exists>y. kheap s thread = Some y then return () else fail) s)))) \<or> snd ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s)) = (\<Union>a\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). fst (case a of (tcb, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False)), (\<exists>x\<in>fst ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). snd (case x of (tcb, s) \<Rightarrow> ({(arch_tcb_context_get (tcb_arch tcb) register, s)}, False))) \<or> snd ((case get_tcb thread s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a. get_tcb thread s = Some a \<Longrightarrow> ((case the (kheap s thread) of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB \<longrightarrow> ((\<exists>y. kheap s thread = Some y) \<longrightarrow> update_kheap ((kheap s)(thread \<mapsto> TCB a)) s = s) \<and> (\<exists>y. kheap s thread = Some y)) \<and> ((case the (kheap s thread) of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) \<noteq> ATCB \<longrightarrow> kheap s thread = None \<and> (\<exists>y. kheap s thread = Some y)) proof (prove)
goal:
No subgoals!