theory Tcb_DR

lemma derive_cnode_cap_as_vroot:
  "\<lbrace>(=) s \<rbrace> derive_cap (ba, ca) aa
   \<lbrace>\<lambda>vroot_cap'.
      if is_valid_vtable_root vroot_cap' then \<lambda>sa. sa = s  \<and> vroot_cap' = aa
      else (=) s\<rbrace>, \<lbrace>\<lambda>r. (=) s\<rbrace>" apply (simp add:derive_cap_def is_valid_vtable_root_def) apply (case_tac aa) apply (clarsimp|wp)+ apply (rename_tac arch_cap) apply (case_tac arch_cap) apply (clarsimp simp:arch_derive_cap_def split:option.splits |wp)+ apply (intro conjI) apply (clarsimp simp:arch_derive_cap_def split:option.splits |wp)+ apply (intro conjI) apply (clarsimp simp:arch_derive_cap_def | wp)+ done

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