theory CSpace1_R

lemma cte_map_pulls_cte_to_abstract:
  "\<lbrakk> y = cte_map z; pspace_relation (kheap s) (ksPSpace s');
     ksPSpace s' y = Some (KOCTE cte);
     valid_objs s; pspace_aligned s; pspace_distinct s; cte_at z s \<rbrakk>
     \<Longrightarrow> \<exists>sz cs cap. kheap s (fst z) = Some (CNode sz cs) \<and> cs (snd z) = Some cap
                  \<and> cap_relation cap (cteCap cte)" apply (rule pspace_dom_relatedE, assumption+) apply (erule(1) obj_relation_cutsE, simp_all) apply clarsimp apply (frule(1) cte_map_inj_eq[OF sym], simp_all) apply (rule cte_wp_at_cteI, (fastforce split: if_split_asm)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' y = Some (KOCTE cte); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) z s\<rbrakk> \<Longrightarrow> \<exists>sz cs cap. kheap s (fst z) = Some (CNode sz cs) \<and> cs (snd z) = Some cap \<and> cap_relation cap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>ya ko P. \<lbrakk>y = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' y = Some (KOCTE cte); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) z s; kheap s ya = Some ko; (y, P) \<in> obj_relation_cuts ko ya; P ko (KOCTE cte)\<rbrakk> \<Longrightarrow> \<exists>sz cs cap. kheap s (fst z) = Some (CNode sz cs) \<and> cs (snd z) = Some cap \<and> cap_relation cap (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>ya ko P sz cs za cap ctea. \<lbrakk>cte_map (ya, za) = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' (cte_map z) = Some (KOCTE ctea); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) z s; kheap s ya = Some (CNode sz cs); P (CNode sz cs) (KOCTE ctea); ko = CNode sz cs; well_formed_cnode_n sz cs; y = cte_map z; cte = ctea; cs za = Some cap; cap_relation cap (cteCap ctea)\<rbrakk> \<Longrightarrow> \<exists>sz cs. kheap s (fst z) = Some (CNode sz cs) \<and> (\<exists>cap. cs (snd z) = Some cap \<and> cap_relation cap (cteCap ctea))
 2. \<And>ya ko P sz dev n. \<lbrakk>ya + n * 2 ^ pageBits = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' (cte_map z) = Some (if dev then KOUserDataDevice else KOUserData); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) z s; kheap s ya = Some (ArchObj (DataPage dev sz)); P (ArchObj (DataPage dev sz)) (if dev then KOUserDataDevice else KOUserData); ko = ArchObj (DataPage dev sz); KOCTE cte = (if dev then KOUserDataDevice else KOUserData); y = cte_map z; n < 2 ^ (pageBitsForSize sz - pageBits)\<rbrakk> \<Longrightarrow> \<exists>sz cs. kheap s (fst z) = Some (CNode sz cs) \<and> (\<exists>cap. cs (snd z) = Some cap \<and> cap_relation cap (cteCap cte)) proof (prove)
goal (2 subgoals):
 1. \<And>ya P sz cs za cap. \<lbrakk>cte_map (ya, za) = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' (cte_map z) = Some (KOCTE cte); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) z s; kheap s ya = Some (CNode sz cs); P (CNode sz cs) (KOCTE cte); well_formed_cnode_n sz cs; y = cte_map z; cs za = Some cap; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<exists>sz cs. kheap s (fst z) = Some (CNode sz cs) \<and> (\<exists>cap. cs (snd z) = Some cap \<and> cap_relation cap (cteCap cte))
 2. \<And>ya ko P sz dev n. \<lbrakk>ya + n * 2 ^ pageBits = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' (cte_map z) = Some (if dev then KOUserDataDevice else KOUserData); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) z s; kheap s ya = Some (ArchObj (DataPage dev sz)); P (ArchObj (DataPage dev sz)) (if dev then KOUserDataDevice else KOUserData); ko = ArchObj (DataPage dev sz); KOCTE cte = (if dev then KOUserDataDevice else KOUserData); y = cte_map z; n < 2 ^ (pageBitsForSize sz - pageBits)\<rbrakk> \<Longrightarrow> \<exists>sz cs. kheap s (fst z) = Some (CNode sz cs) \<and> (\<exists>cap. cs (snd z) = Some cap \<and> cap_relation cap (cteCap cte)) proof (prove)
goal (2 subgoals):
 1. \<And>ya P sz cs za cap. \<lbrakk>cte_map (ya, za) = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' (cte_map z) = Some (KOCTE cte); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) z s; kheap s ya = Some (CNode sz cs); P (CNode sz cs) (KOCTE cte); well_formed_cnode_n sz cs; y = cte_map z; cs za = Some cap; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ya, za) s
 2. \<And>ya ko P sz dev n. \<lbrakk>ya + n * 2 ^ pageBits = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' (cte_map z) = Some (if dev then KOUserDataDevice else KOUserData); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>_. True) z s; kheap s ya = Some (ArchObj (DataPage dev sz)); P (ArchObj (DataPage dev sz)) (if dev then KOUserDataDevice else KOUserData); ko = ArchObj (DataPage dev sz); KOCTE cte = (if dev then KOUserDataDevice else KOUserData); y = cte_map z; n < 2 ^ (pageBitsForSize sz - pageBits)\<rbrakk> \<Longrightarrow> \<exists>sz cs. kheap s (fst z) = Some (CNode sz cs) \<and> (\<exists>cap. cs (snd z) = Some cap \<and> cap_relation cap (cteCap cte)) proof (prove)
goal:
No subgoals!