theory CSpace_R

lemma deriveCap_corres:
 "\<lbrakk>cap_relation c c'; cte = cte_map slot \<rbrakk> \<Longrightarrow>
  corres (ser \<oplus> cap_relation)
         (cte_at slot)
         (pspace_aligned' and pspace_distinct' and cte_at' cte and valid_mdb')
         (derive_cap slot c) (deriveCap cte c')" apply (unfold derive_cap_def deriveCap_def) apply (case_tac c) apply (simp_all add: returnOk_def Let_def is_zombie_def isCap_simps
                          split: sum.splits) apply (rule_tac Q="\<lambda>_ _. True" and Q'="\<lambda>_ _. True" in
               corres_initial_splitE [OF ensureNoChildren_corres]) apply simp apply clarsimp apply wp+ apply clarsimp apply (rule corres_rel_imp) apply (rule corres_guard_imp) apply (rule arch_deriveCap_corres) apply (clarsimp simp: o_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cte = cte_map slot\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (derive_cap slot c) (global.deriveCap cte c') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cte = cte_map slot\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (case c of cap.UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | cap.IRQControlCap \<Rightarrow> returnOk cap.NullCap | cap.Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | cap.ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c) (let cap = c' in if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE ensureNoChildren cte;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Let (capCap cap) (Arch.deriveCap cte) else returnOk cap) proof (prove)
goal (12 subgoals):
 1. \<lbrakk>cap_relation c c'; cte = cte_map slot; c = cap.NullCap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (case c of cap.UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | cap.IRQControlCap \<Rightarrow> returnOk cap.NullCap | cap.Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | cap.ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c) (let cap = c' in if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE ensureNoChildren cte;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Let (capCap cap) (Arch.deriveCap cte) else returnOk cap)
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap_relation c c'; cte = cte_map slot; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (case c of cap.UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | cap.IRQControlCap \<Rightarrow> returnOk cap.NullCap | cap.Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | cap.ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c) (let cap = c' in if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE ensureNoChildren cte;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Let (capCap cap) (Arch.deriveCap cte) else returnOk cap)
 3. \<And>x31 x32 x33. \<lbrakk>cap_relation c c'; cte = cte_map slot; c = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (case c of cap.UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | cap.IRQControlCap \<Rightarrow> returnOk cap.NullCap | cap.Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | cap.ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c) (let cap = c' in if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE ensureNoChildren cte;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Let (capCap cap) (Arch.deriveCap cte) else returnOk cap)
 4. \<And>x41 x42 x43. \<lbrakk>cap_relation c c'; cte = cte_map slot; c = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (case c of cap.UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | cap.IRQControlCap \<Rightarrow> returnOk cap.NullCap | cap.Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | cap.ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c) (let cap = c' in if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE ensureNoChildren cte;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Let (capCap cap) (Arch.deriveCap cte) else returnOk cap)
 5. \<And>x51 x52 x53. \<lbrakk>cap_relation c c'; cte = cte_map slot; c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (case c of cap.UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | cap.IRQControlCap \<Rightarrow> returnOk cap.NullCap | cap.Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | cap.ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c) (let cap = c' in if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE ensureNoChildren cte;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Let (capCap cap) (Arch.deriveCap cte) else returnOk cap)
 6. \<And>x61 x62 x63. \<lbrakk>cap_relation c c'; cte = cte_map slot; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (case c of cap.UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | cap.IRQControlCap \<Rightarrow> returnOk cap.NullCap | cap.Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | cap.ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c) (let cap = c' in if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE ensureNoChildren cte;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Let (capCap cap) (Arch.deriveCap cte) else returnOk cap)
 7. \<And>x7. \<lbrakk>cap_relation c c'; cte = cte_map slot; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (case c of cap.UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | cap.IRQControlCap \<Rightarrow> returnOk cap.NullCap | cap.Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | cap.ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c) (let cap = c' in if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE ensureNoChildren cte;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Let (capCap cap) (Arch.deriveCap cte) else returnOk cap)
 8. \<lbrakk>cap_relation c c'; cte = cte_map slot; c = cap.DomainCap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (case c of cap.UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | cap.IRQControlCap \<Rightarrow> returnOk cap.NullCap | cap.Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | cap.ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c) (let cap = c' in if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE ensureNoChildren cte;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Let (capCap cap) (Arch.deriveCap cte) else returnOk cap)
 9. \<lbrakk>cap_relation c c'; cte = cte_map slot; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (case c of cap.UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | cap.IRQControlCap \<Rightarrow> returnOk cap.NullCap | cap.Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | cap.ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c) (let cap = c' in if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE ensureNoChildren cte;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Let (capCap cap) (Arch.deriveCap cte) else returnOk cap)
 10. \<And>x10. \<lbrakk>cap_relation c c'; cte = cte_map slot; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cte and valid_mdb') (case c of cap.UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | cap.IRQControlCap \<Rightarrow> returnOk cap.NullCap | cap.Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | cap.ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c) (let cap = c' in if isZombie cap then returnOk capability.NullCap else if isIRQControlCap cap then returnOk capability.NullCap else if isUntypedCap cap then doE ensureNoChildren cte;
returnOk cap
odE else if isReplyCap cap then returnOk capability.NullCap else if isArchObjectCap cap then Let (capCap cap) (Arch.deriveCap cte) else returnOk cap)
A total of 12 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; cte = cte_map slot; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (doE y <- ensure_no_children slot;
return (Inr (cap.UntypedCap x21 x22 x23 x24))
odE) (doE y <- ensureNoChildren (cte_map slot);
return (Inr (capability.UntypedCap x21 x22 x23 x24))
odE)
 2. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; cte = cte_map slot; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> ((\<exists>v0. c' = capability.ArchObjectCap v0) \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap)))))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (Arch.deriveCap (cte_map slot) (capCap c'))))))) \<and> ((\<forall>v0. c' \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap)))))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr c'))))))) proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; cte = cte_map slot; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cte_map slot = cte_map slot
 2. \<And>x21 x22 x23 x24 rv rv'. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; cte = cte_map slot; c = cap.UntypedCap x21 x22 x23 x24; dc rv rv'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (\<lambda>_. True) (\<lambda>_. True) (return (Inr (cap.UntypedCap x21 x22 x23 x24))) (return (Inr (capability.UntypedCap x21 x22 x23 x24)))
 3. \<And>x21 x22 x23 x24. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; cte = cte_map slot; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>_. True) slot\<rbrace> ensure_no_children slot \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<And>x21 x22 x23 x24. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; cte = cte_map slot; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb'\<rbrace> ensureNoChildren (cte_map slot) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; cte = cte_map slot; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> ((\<exists>v0. c' = capability.ArchObjectCap v0) \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap)))))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (Arch.deriveCap (cte_map slot) (capCap c'))))))) \<and> ((\<forall>v0. c' \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap)))))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr c'))))))) proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x23 x24 rv rv'. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; cte = cte_map slot; c = cap.UntypedCap x21 x22 x23 x24; dc rv rv'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (\<lambda>_. True) (\<lambda>_. True) (return (Inr (cap.UntypedCap x21 x22 x23 x24))) (return (Inr (capability.UntypedCap x21 x22 x23 x24)))
 2. \<And>x21 x22 x23 x24. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; cte = cte_map slot; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>_. True) slot\<rbrace> ensure_no_children slot \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 3. \<And>x21 x22 x23 x24. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; cte = cte_map slot; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb'\<rbrace> ensureNoChildren (cte_map slot) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; cte = cte_map slot; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> ((\<exists>v0. c' = capability.ArchObjectCap v0) \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap)))))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (Arch.deriveCap (cte_map slot) (capCap c'))))))) \<and> ((\<forall>v0. c' \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap)))))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr c'))))))) proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; cte = cte_map slot; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>_. True) slot\<rbrace> ensure_no_children slot \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 2. \<And>x21 x22 x23 x24. \<lbrakk>c' = capability.UntypedCap x21 x22 x23 x24; cte = cte_map slot; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb'\<rbrace> ensureNoChildren (cte_map slot) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 3. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; cte = cte_map slot; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> ((\<exists>v0. c' = capability.ArchObjectCap v0) \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap)))))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (Arch.deriveCap (cte_map slot) (capCap c'))))))) \<and> ((\<forall>v0. c' \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap)))))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr c'))))))) proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; cte = cte_map slot; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> ((\<exists>v0. c' = capability.ArchObjectCap v0) \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap)))))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (Arch.deriveCap (cte_map slot) (capCap c'))))))) \<and> ((\<forall>v0. c' \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap)))))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.ReplyCap v0 v1 v2) \<longrightarrow> ((\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (doE y <- ensureNoChildren (cte_map slot);
return (Inr c')
odE)))) \<and> ((\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> (c' = capability.IRQControlCap \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> (c' \<noteq> capability.IRQControlCap \<longrightarrow> ((\<exists>v0 v1 v2. c' = capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr capability.NullCap))) \<and> ((\<forall>v0 v1 v2. c' \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (return (Inr c'))))))) proof (prove)
goal (1 subgoal):
 1. \<And>x12 a'. \<lbrakk>cte = cte_map slot; c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (Arch.deriveCap (cte_map slot) a') proof (prove)
goal (2 subgoals):
 1. \<And>x12 a'. \<lbrakk>cte = cte_map slot; c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'\<rbrakk> \<Longrightarrow> corres (?r'55 x12 a') (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') (arch_derive_cap x12) (Arch.deriveCap (cte_map slot) a')
 2. \<And>x12 a' x y. \<lbrakk>cte = cte_map slot; c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'; ?r'55 x12 a' x y\<rbrakk> \<Longrightarrow> (ser \<oplus> cap_relation) x y proof (prove)
goal (4 subgoals):
 1. \<And>x12 a'. \<lbrakk>cte = cte_map slot; c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'\<rbrakk> \<Longrightarrow> corres (?r'55 x12 a') (?Q58 x12 a') (?Q'58 x12 a') (arch_derive_cap x12) (Arch.deriveCap (cte_map slot) a')
 2. \<And>x12 a' s. \<lbrakk>cte = cte_map slot; c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'; cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> ?Q58 x12 a' s
 3. \<And>x12 a' s. \<lbrakk>cte = cte_map slot; c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'; (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') s\<rbrakk> \<Longrightarrow> ?Q'58 x12 a' s
 4. \<And>x12 a' x y. \<lbrakk>cte = cte_map slot; c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'; ?r'55 x12 a' x y\<rbrakk> \<Longrightarrow> (ser \<oplus> cap_relation) x y proof (prove)
goal (4 subgoals):
 1. \<And>x12 a'. \<lbrakk>cte = cte_map slot; c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'\<rbrakk> \<Longrightarrow> cap_relation (cap.ArchObjectCap x12) (capability.ArchObjectCap a')
 2. \<And>x12 a' s. \<lbrakk>cte = cte_map slot; c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'; cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> True
 3. \<And>x12 a' s. \<lbrakk>cte = cte_map slot; c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'; (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb') s\<rbrakk> \<Longrightarrow> True
 4. \<And>x12 a' x y. \<lbrakk>cte = cte_map slot; c = cap.ArchObjectCap x12; acap_relation x12 a'; c' = capability.ArchObjectCap a'; (ser \<oplus> cap_relation) x y\<rbrakk> \<Longrightarrow> (ser \<oplus> cap_relation) x y proof (prove)
goal:
No subgoals!