theory CNode_DR

lemma set_get_set_asid_pool:
  "do _ \<leftarrow> set_asid_pool a x; ap \<leftarrow> get_asid_pool a; set_asid_pool a (y ap) od = set_asid_pool a (y x)" apply (rule ext) apply (simp add: get_asid_pool_def set_asid_pool_def get_object_def set_object_def
                   a_type_def bind_assoc exec_gets) apply (case_tac "kheap xa a", simp_all) apply (case_tac aa, simp_all) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj, simp_all) apply (simp add:set_object_def exec_gets bind_assoc exec_get exec_put) apply (simp add: put_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- set_asid_pool a x;
ap <- get_asid_pool a;
set_asid_pool a (y ap)
od = set_asid_pool a (y x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. (do _ <- set_asid_pool a x;
ap <- get_asid_pool a;
set_asid_pool a (y ap)
od) xa = set_asid_pool a (y x) xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. (do xb <- assert (\<exists>y. kheap xa a = Some y);
xa <- assert ((case the (kheap xa a) 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)) = AArch AASIDPool);
xa <- get;
_ <- put (update_kheap ((kheap xa)(a \<mapsto> ArchObj (ASIDPool x))) xa);
x <- gets kheap;
xa <- assert (\<exists>y. x a = Some y);
ap <- case the (x a) of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- gets kheap;
ya <- assert (\<exists>y. x a = Some y);
ya <- assert ((case the (x a) 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)) = AArch AASIDPool);
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (ASIDPool (y ap)))) s)
od) xa = (do ya <- assert (\<exists>y. kheap xa a = Some y);
ya <- assert ((case the (kheap xa a) 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)) = AArch AASIDPool);
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (ASIDPool (y x)))) s)
od) xa proof (prove)
goal (1 subgoal):
 1. \<And>xa aa. kheap xa a = Some aa \<Longrightarrow> (do xa <- assert ((case aa 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)) = AArch AASIDPool);
xa <- get;
_ <- put (update_kheap ((kheap xa)(a \<mapsto> ArchObj (ASIDPool x))) xa);
x <- gets kheap;
xa <- assert (\<exists>y. x a = Some y);
ap <- case the (x a) of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- gets kheap;
ya <- assert (\<exists>y. x a = Some y);
ya <- assert ((case the (x a) 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)) = AArch AASIDPool);
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (ASIDPool (y ap)))) s)
od) xa = (do ya <- assert ((case aa 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)) = AArch AASIDPool);
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (ASIDPool (y x)))) s)
od) xa proof (prove)
goal (1 subgoal):
 1. \<And>xa aa x5. \<lbrakk>kheap xa a = Some (ArchObj x5); aa = ArchObj x5\<rbrakk> \<Longrightarrow> (do xa <- assert ((case x5 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) = AASIDPool);
xa <- get;
_ <- put (update_kheap ((kheap xa)(a \<mapsto> ArchObj (ASIDPool x))) xa);
x <- gets kheap;
xa <- assert (\<exists>y. x a = Some y);
ap <- case the (x a) of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- gets kheap;
ya <- assert (\<exists>y. x a = Some y);
ya <- assert ((case the (x a) 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)) = AArch AASIDPool);
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (ASIDPool (y ap)))) s)
od) xa = (do ya <- assert ((case x5 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) = AASIDPool);
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (ASIDPool (y x)))) s)
od) xa proof (prove)
goal (1 subgoal):
 1. \<And>xa aa arch_kernel_obj. \<lbrakk>kheap xa a = Some (ArchObj arch_kernel_obj); aa = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> (do xa <- assert ((case arch_kernel_obj 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) = AASIDPool);
xa <- get;
_ <- put (update_kheap ((kheap xa)(a \<mapsto> ArchObj (ASIDPool x))) xa);
x <- gets kheap;
xa <- assert (\<exists>y. x a = Some y);
ap <- case the (x a) of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- gets kheap;
ya <- assert (\<exists>y. x a = Some y);
ya <- assert ((case the (x a) 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)) = AArch AASIDPool);
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (ASIDPool (y ap)))) s)
od) xa = (do ya <- assert ((case arch_kernel_obj 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) = AASIDPool);
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (ASIDPool (y x)))) s)
od) xa proof (prove)
goal (1 subgoal):
 1. \<And>xa aa arch_kernel_obj x1. \<lbrakk>kheap xa a = Some (ArchObj (ASIDPool x1)); aa = ArchObj (ASIDPool x1); arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> (do xa <- get;
_ <- put (update_kheap ((kheap xa)(a \<mapsto> ArchObj (ASIDPool x))) xa);
x <- gets kheap;
xa <- assert (\<exists>y. x a = Some y);
ap <- case the (x a) of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- gets kheap;
ya <- assert (\<exists>y. x a = Some y);
ya <- assert ((case the (x a) 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)) = AArch AASIDPool);
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (ASIDPool (y ap)))) s)
od) xa = (do s <- get;
put (update_kheap ((kheap s)(a \<mapsto> ArchObj (ASIDPool (y x)))) s)
od) xa proof (prove)
goal (1 subgoal):
 1. \<And>xa aa arch_kernel_obj x1. \<lbrakk>kheap xa a = Some (ArchObj (ASIDPool x1)); aa = ArchObj (ASIDPool x1); arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> put (update_kheap ((kheap xa)(a \<mapsto> ArchObj (ASIDPool (y x)))) xa) (update_kheap ((kheap xa)(a \<mapsto> ArchObj (ASIDPool x))) xa) = put (update_kheap ((kheap xa)(a \<mapsto> ArchObj (ASIDPool (y x)))) xa) xa proof (prove)
goal:
No subgoals!