theory Tcb_DR

lemma derive_cap_translate_tcb_invocation:
 "\<lbrace>(=) s\<rbrace>derive_cap a b \<lbrace>\<lambda>rv. (=) s\<rbrace>,\<lbrace>\<lambda>rv. \<top>\<rbrace>" apply (simp add:derive_cap_def) apply (case_tac b) apply (clarsimp simp:ensure_no_children_def whenE_def |wp)+ apply (clarsimp simp:arch_derive_cap_def) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply (clarsimp simp:ensure_no_children_def whenE_def |wp)+ apply (clarsimp split:option.splits | rule conjI | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> CSpace_A.derive_cap a b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> case b of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children a;
returnOk b
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 b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal (12 subgoals):
 1. b = cap.NullCap \<Longrightarrow> \<lbrace>(=) s\<rbrace> case b of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children a;
returnOk b
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 b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>x21 x22 x23 x24. b = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>(=) s\<rbrace> case b of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children a;
returnOk b
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 b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>x31 x32 x33. b = cap.EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>(=) s\<rbrace> case b of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children a;
returnOk b
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 b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>x41 x42 x43. b = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>(=) s\<rbrace> case b of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children a;
returnOk b
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 b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 5. \<And>x51 x52 x53. b = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>(=) s\<rbrace> case b of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children a;
returnOk b
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 b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 6. \<And>x61 x62 x63. b = cap.CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>(=) s\<rbrace> case b of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children a;
returnOk b
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 b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 7. \<And>x7. b = ThreadCap x7 \<Longrightarrow> \<lbrace>(=) s\<rbrace> case b of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children a;
returnOk b
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 b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 8. b = cap.DomainCap \<Longrightarrow> \<lbrace>(=) s\<rbrace> case b of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children a;
returnOk b
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 b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 9. b = IRQControlCap \<Longrightarrow> \<lbrace>(=) s\<rbrace> case b of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children a;
returnOk b
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 b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
 10. \<And>x10. b = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>(=) s\<rbrace> case b of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children a;
returnOk b
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 b \<lbrace>\<lambda>rv. (=) s\<rbrace>, \<lbrace>\<lambda>rv _. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>x12. b = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?P'117 x12\<rbrace> arch_derive_cap x12 \<lbrace>\<lambda>rv. (=) s\<rbrace>, -
 2. \<And>x12 sa. \<lbrakk>b = ArchObjectCap x12; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'117 x12 sa proof (prove)
goal (2 subgoals):
 1. \<And>x12. b = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?P'117 x12\<rbrace> 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) \<lbrace>\<lambda>rv. (=) s\<rbrace>, -
 2. \<And>x12 sa. \<lbrakk>b = ArchObjectCap x12; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'117 x12 sa proof (prove)
goal (2 subgoals):
 1. \<And>arch_cap. b = ArchObjectCap arch_cap \<Longrightarrow> \<lbrace>?P'117 arch_cap\<rbrace> 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) \<lbrace>\<lambda>rv. (=) s\<rbrace>, -
 2. \<And>x12 sa. \<lbrakk>b = ArchObjectCap x12; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'117 x12 sa proof (prove)
goal (6 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>b = ArchObjectCap arch_cap; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> \<lbrace>?P'117 arch_cap\<rbrace> 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) \<lbrace>\<lambda>rv. (=) s\<rbrace>, -
 2. \<And>arch_cap. \<lbrakk>b = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'117 arch_cap\<rbrace> 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) \<lbrace>\<lambda>rv. (=) s\<rbrace>, -
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>b = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>?P'117 arch_cap\<rbrace> 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) \<lbrace>\<lambda>rv. (=) s\<rbrace>, -
 4. \<And>arch_cap x41 x42. \<lbrakk>b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>?P'117 arch_cap\<rbrace> 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) \<lbrace>\<lambda>rv. (=) s\<rbrace>, -
 5. \<And>arch_cap x51 x52. \<lbrakk>b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>?P'117 arch_cap\<rbrace> 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) \<lbrace>\<lambda>rv. (=) s\<rbrace>, -
 6. \<And>x12 sa. \<lbrakk>b = ArchObjectCap x12; s = sa\<rbrakk> \<Longrightarrow> True \<and> ?P'117 x12 sa proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42. b = ArchObjectCap (arch_cap.PageTableCap x41 x42) \<Longrightarrow> \<lbrace>(=) s\<rbrace> case x42 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (arch_cap.PageTableCap x41 x42)) \<lbrace>\<lambda>rv. (=) s\<rbrace>, -
 2. \<And>arch_cap x51 x52. \<lbrakk>b = ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> 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) \<lbrace>\<lambda>rv. (=) s\<rbrace>, -
 3. \<And>x12 sa. \<lbrakk>b = ArchObjectCap x12; s = sa\<rbrakk> \<Longrightarrow> True \<and> s = sa proof (prove)
goal:
No subgoals!