theory CNode_DR

lemma derive_cap_dummy:
  "dcorres dc \<top> \<top> (return x) (derive_cap slot cap)" apply (simp add: derive_cap_def) apply (cases cap, simp_all add: returnOk_def) apply (simp add: bindE_def) apply (rule corres_dummy_return_l) apply (rule corres_guard_imp) apply (rule corres_split[OF ensure_no_children_dummy, where R="\<lambda>_. \<top>" and R'="\<lambda>_. \<top>"]) apply (clarsimp simp: corres_underlying_def lift_def return_def split: sum.splits) apply (fastforce simp: in_monad) apply wp+ apply simp apply simp apply (clarsimp simp: arch_derive_cap_def) apply (rename_tac arch_cap) apply (case_tac arch_cap, simp_all split: option.splits) apply (simp_all add: returnOk_def throwError_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (CSpace_A.derive_cap slot cap) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (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. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (doE y <- CSpace_A.ensure_no_children slot;
return (Inr (cap.UntypedCap x21 x22 x23 x24))
odE)
 2. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (arch_derive_cap x12) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (CSpace_A.ensure_no_children slot >>= lift (\<lambda>y. return (Inr (cap.UntypedCap x21 x22 x23 x24))))
 2. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (arch_derive_cap x12) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x >>= return) (CSpace_A.ensure_no_children slot >>= lift (\<lambda>y. return (Inr (cap.UntypedCap x21 x22 x23 x24))))
 2. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (arch_derive_cap x12) proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x23 x24. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> dcorres dc (?Q7 x21 x22 x23 x24) (?Q'7 x21 x22 x23 x24) (return x >>= return) (CSpace_A.ensure_no_children slot >>= lift (\<lambda>y. return (Inr (cap.UntypedCap x21 x22 x23 x24))))
 2. \<And>x21 x22 x23 x24 s. \<lbrakk>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 = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ?Q'7 x21 x22 x23 x24 s
 4. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (arch_derive_cap x12) proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 x24 x rv'. \<lbrakk>cap = cap.UntypedCap x21 x22 x23 x24; dc x rv'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (lift (\<lambda>y. return (Inr (cap.UntypedCap x21 x22 x23 x24))) rv')
 2. \<And>x21 x22 x23 x24. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>?Q11 x21 x22 x23 x24\<rbrace> return x \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x21 x22 x23 x24. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>?Q'11 x21 x22 x23 x24\<rbrace> CSpace_A.ensure_no_children slot \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>x21 x22 x23 x24 s. \<lbrakk>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 = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'11 x21 x22 x23 x24) s
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (arch_derive_cap x12) proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 x24 x1 b a ba. \<lbrakk>cap = cap.UntypedCap x21 x22 x23 x24; (a, ba) \<in> fst (throwError x1 b)\<rbrakk> \<Longrightarrow> transform ba = transform b
 2. \<And>x21 x22 x23 x24. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>?Q11 x21 x22 x23 x24\<rbrace> return x \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x21 x22 x23 x24. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>?Q'11 x21 x22 x23 x24\<rbrace> CSpace_A.ensure_no_children slot \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>x21 x22 x23 x24 s. \<lbrakk>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 = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'11 x21 x22 x23 x24) s
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (arch_derive_cap x12) proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 x24. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>?Q11 x21 x22 x23 x24\<rbrace> return x \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>?Q'11 x21 x22 x23 x24\<rbrace> CSpace_A.ensure_no_children slot \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x21 x22 x23 x24 s. \<lbrakk>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 = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'11 x21 x22 x23 x24) s
 5. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (arch_derive_cap x12) proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x23 x24 s. \<lbrakk>cap = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s
 2. \<And>x21 x22 x23 x24 s. \<lbrakk>cap = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
 3. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (arch_derive_cap x12) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 s. \<lbrakk>cap = cap.UntypedCap x21 x22 x23 x24; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
 2. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (arch_derive_cap x12) proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (arch_derive_cap x12) proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (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. cap = ArchObjectCap arch_cap \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (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 (5 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>cap = ArchObjectCap (ASIDPoolCap x11 x12); arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (returnOk (ArchObjectCap (ASIDPoolCap x11 x12)))
 2. \<And>arch_cap. \<lbrakk>cap = ArchObjectCap ASIDControlCap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (returnOk (ArchObjectCap ASIDControlCap))
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (returnOk (ArchObjectCap (PageCap x31 x32 x33 x34 None)))
 4. \<And>arch_cap x41 x42. \<lbrakk>cap = ArchObjectCap (arch_cap.PageTableCap x41 x42); arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> (x42 = None \<longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (throwError IllegalOperation)) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (returnOk (ArchObjectCap (arch_cap.PageTableCap x41 (Some (a, b))))))
 5. \<And>arch_cap x51 x52. \<lbrakk>cap = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> (x52 = None \<longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (throwError IllegalOperation)) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (returnOk (ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x2))))) proof (prove)
goal:
No subgoals!