theory CNode_DR

lemma derive_cap_dcorres:
  "cap' = transform_cap cap \<Longrightarrow>
   dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) \<top>
           (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_at slot s)
           (CSpace_D.derive_cap (transform_cslot_ptr slot) cap')
           (CSpace_A.derive_cap slot cap)" unfolding CSpace_D.derive_cap_def derive_cap_def apply (cases cap, simp_all add: dcorres_returnOk')
   \<comment> \<open>Untyped\<close> apply (rule corres_guard_imp) apply (rule corres_splitEE[where r' = "(=)"]) apply (rule dcorres_ensure_no_children) apply (rule dcorres_returnOk) apply simp apply wp apply wp apply simp apply fastforce apply (simp add: arch_derive_cap_def) apply (rename_tac arch_cap) apply (case_tac arch_cap, simp_all add: dcorres_returnOk') apply (rule dcorres_returnOk') apply (clarsimp simp:transform_mapping_def) apply (fastforce intro: corres_alternate1 corres_alternate2 dcorres_returnOk'
                   split: option.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap' = transform_cap cap \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (CSpace_D.derive_cap (transform_cslot_ptr slot) cap') (CSpace_A.derive_cap slot cap) proof (prove)
goal (1 subgoal):
 1. cap' = transform_cap cap \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case cap' of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (case cap of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children slot;
returnOk cap
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | IRQControlCap \<Rightarrow> returnOk cap.NullCap | Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (doE y <- CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22))
odE) (doE y <- CSpace_A.ensure_no_children slot;
returnOk (cap.UntypedCap x21 x22 x23 x24)
odE)
 2. \<And>x12. \<lbrakk>cap' = transform_cap (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap x12) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (arch_derive_cap x12) proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (?Q7 x21 x22 x23 x24) (?Q'7 x21 x22 x23 x24) (doE y <- CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22))
odE) (doE y <- CSpace_A.ensure_no_children slot;
returnOk (cap.UntypedCap x21 x22 x23 x24)
odE)
 2. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ?Q7 x21 x22 x23 x24 s
 3. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> ?Q'7 x21 x22 x23 x24 s
 4. \<And>x12. \<lbrakk>cap' = transform_cap (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap x12) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (arch_derive_cap x12) proof (prove)
goal (7 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (=)) (?P11 x21 x22 x23 x24) (?P'11 x21 x22 x23 x24) (CSpace_D.ensure_no_children (transform_cslot_ptr slot)) (CSpace_A.ensure_no_children slot)
 2. \<And>x21 x22 x23 x24 y ya. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; y = ya\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (?R11 x21 x22 x23 x24 y) (?R'11 x21 x22 x23 x24 ya) (returnOk (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22))) (returnOk (cap.UntypedCap x21 x22 x23 x24))
 3. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>?Q11 x21 x22 x23 x24\<rbrace> CSpace_D.ensure_no_children (transform_cslot_ptr slot) \<lbrace>?R11 x21 x22 x23 x24\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 x21 x22 x23 x24\<rbrace> CSpace_A.ensure_no_children slot \<lbrace>?R'11 x21 x22 x23 x24\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> (?P11 x21 x22 x23 x24 and ?Q11 x21 x22 x23 x24) s
 6. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> (?P'11 x21 x22 x23 x24 and ?Q'11 x21 x22 x23 x24) s
 7. \<And>x12. \<lbrakk>cap' = transform_cap (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap x12) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (arch_derive_cap x12) proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 x24 y ya. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; y = ya\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (?R11 x21 x22 x23 x24 y) (?R'11 x21 x22 x23 x24 ya) (returnOk (cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22))) (returnOk (cap.UntypedCap x21 x22 x23 x24))
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>?Q11 x21 x22 x23 x24\<rbrace> CSpace_D.ensure_no_children (transform_cslot_ptr slot) \<lbrace>?R11 x21 x22 x23 x24\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 x21 x22 x23 x24\<rbrace> CSpace_A.ensure_no_children slot \<lbrace>?R'11 x21 x22 x23 x24\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q11 x21 x22 x23 x24) s
 5. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at (?P16 x21 x22 x23 x24)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'11 x21 x22 x23 x24) s
 6. \<And>x12. \<lbrakk>cap' = transform_cap (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap x12) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (arch_derive_cap x12) proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 x24 y ya. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; y = ya\<rbrakk> \<Longrightarrow> cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22) = transform_cap (cap.UntypedCap x21 x22 x23 x24)
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>?Q11 x21 x22 x23 x24\<rbrace> CSpace_D.ensure_no_children (transform_cslot_ptr slot) \<lbrace>\<lambda>y _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 x21 x22 x23 x24\<rbrace> CSpace_A.ensure_no_children slot \<lbrace>\<lambda>ya _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q11 x21 x22 x23 x24) s
 5. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at (?P16 x21 x22 x23 x24)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'11 x21 x22 x23 x24) s
 6. \<And>x12. \<lbrakk>cap' = transform_cap (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap x12) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (arch_derive_cap x12) proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>?Q11 x21 x22 x23 x24\<rbrace> CSpace_D.ensure_no_children (transform_cslot_ptr slot) \<lbrace>\<lambda>y _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 x21 x22 x23 x24\<rbrace> CSpace_A.ensure_no_children slot \<lbrace>\<lambda>ya _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q11 x21 x22 x23 x24) s
 4. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at (?P16 x21 x22 x23 x24)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'11 x21 x22 x23 x24) s
 5. \<And>x12. \<lbrakk>cap' = transform_cap (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap x12) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (arch_derive_cap x12) proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 x21 x22 x23 x24\<rbrace> CSpace_A.ensure_no_children slot \<lbrace>\<lambda>ya _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at (?P16 x21 x22 x23 x24)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'11 x21 x22 x23 x24) s
 4. \<And>x12. \<lbrakk>cap' = transform_cap (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap x12) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (arch_derive_cap x12) proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at (?P16 x21 x22 x23 x24)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) and (\<lambda>s. True \<and> True)) s
 3. \<And>x12. \<lbrakk>cap' = transform_cap (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap x12) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (arch_derive_cap x12) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 s. \<lbrakk>cap' = cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22); cap = cap.UntypedCap x21 x22 x23 x24; mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at (?P16 x21 x22 x23 x24)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) and (\<lambda>s. True \<and> True)) s
 2. \<And>x12. \<lbrakk>cap' = transform_cap (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap x12) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (arch_derive_cap x12) proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>cap' = transform_cap (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap x12) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (arch_derive_cap x12) proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>cap' = transform_cap (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap x12) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (case x12 of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | arch_cap.PageTableCap xa None \<Rightarrow> throwError IllegalOperation | arch_cap.PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap x12) | arch_cap.PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | arch_cap.PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap x12) | _ \<Rightarrow> returnOk (ArchObjectCap x12)) proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. \<lbrakk>cap' = transform_cap (ArchObjectCap arch_cap); cap = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (case transform_cap (ArchObjectCap arch_cap) of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE CSpace_D.ensure_no_children (transform_cslot_ptr slot);
returnOk cap'
odE | cdl_cap.ReplyCap x xa \<Rightarrow> returnOk cdl_cap.NullCap | MasterReplyCap oref \<Rightarrow> returnOk cdl_cap.NullCap | IrqControlCap \<Rightarrow> returnOk cdl_cap.NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | cdl_cap.PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap' | ZombieCap x \<Rightarrow> returnOk cdl_cap.NullCap | _ \<Rightarrow> returnOk cap') (case arch_cap of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | arch_cap.PageTableCap xa None \<Rightarrow> throwError IllegalOperation | arch_cap.PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap arch_cap) | arch_cap.PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | arch_cap.PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap arch_cap) | _ \<Rightarrow> returnOk (ArchObjectCap arch_cap)) proof (prove)
goal (3 subgoals):
 1. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>cap' = FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35); cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (returnOk (FrameCap x31 x32 x33 (pageBitsForSize x34) Real None)) (returnOk (ArchObjectCap (PageCap x31 x32 x33 x34 None)))
 2. \<And>arch_cap x41 x42. \<lbrakk>cap' = cdl_cap.PageTableCap x41 Real (transform_mapping x42); cap = ArchObjectCap (arch_cap.PageTableCap x41 x42); arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (throw \<sqinter> returnOk (cdl_cap.PageTableCap x41 Real (transform_mapping x42))) (case x42 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (arch_cap.PageTableCap x41 x42)))
 3. \<And>arch_cap x51 x52. \<lbrakk>cap' = cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52); cap = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (throw \<sqinter> returnOk (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52))) (case x52 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))) proof (prove)
goal (3 subgoals):
 1. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>cap' = FrameCap x31 x32 x33 (pageBitsForSize x34) Real (transform_mapping x35); cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> FrameCap x31 x32 x33 (pageBitsForSize x34) Real None = transform_cap (ArchObjectCap (PageCap x31 x32 x33 x34 None))
 2. \<And>arch_cap x41 x42. \<lbrakk>cap' = cdl_cap.PageTableCap x41 Real (transform_mapping x42); cap = ArchObjectCap (arch_cap.PageTableCap x41 x42); arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (throw \<sqinter> returnOk (cdl_cap.PageTableCap x41 Real (transform_mapping x42))) (case x42 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (arch_cap.PageTableCap x41 x42)))
 3. \<And>arch_cap x51 x52. \<lbrakk>cap' = cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52); cap = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (throw \<sqinter> returnOk (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52))) (case x52 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))) proof (prove)
goal (2 subgoals):
 1. \<And>arch_cap x41 x42. \<lbrakk>cap' = cdl_cap.PageTableCap x41 Real (transform_mapping x42); cap = ArchObjectCap (arch_cap.PageTableCap x41 x42); arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (throw \<sqinter> returnOk (cdl_cap.PageTableCap x41 Real (transform_mapping x42))) (case x42 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (arch_cap.PageTableCap x41 x42)))
 2. \<And>arch_cap x51 x52. \<lbrakk>cap' = cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52); cap = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>c c'. c = transform_cap c')) (\<lambda>_. True) (\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) slot s) (throw \<sqinter> returnOk (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52))) (case x52 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))) proof (prove)
goal:
No subgoals!