theory CSpace1_R

lemma is_final_untyped_ptrs:
  "\<lbrakk> ctes_of (s' :: kernel_state) (cte_map slot) = Some cte; ctes_of s' y = Some cte'; cte_map slot \<noteq> y;
     pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s;
     cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> obj_refs cap \<noteq> {}) slot s \<rbrakk>
         \<Longrightarrow> capClass (cteCap cte') \<noteq> PhysicalClass
           \<or> isUntypedCap (cteCap cte')
           \<or> capUntypedPtr (cteCap cte) \<noteq> capUntypedPtr (cteCap cte')" apply clarsimp apply (drule(2) pspace_relation_cte_wp_atI[rotated])+ apply clarsimp apply (drule_tac s=s in cte_map_inj_eq,
          (clarsimp elim!: cte_wp_at_weakenE[OF _ TrueI])+) apply (clarsimp simp: cte_wp_at_def) apply (erule(3) final_cap_duplicate [where r="ObjRef (capUntypedPtr (cteCap cte))",
                                       OF _ _ distinct_lemma[where f=cte_map]]) apply (rule obj_ref_is_gen_obj_ref) apply (erule(1) obj_refs_cap_relation_untyped_ptr) apply (rule obj_ref_is_gen_obj_ref) apply (erule(1) obj_refs_cap_relation_untyped_ptr) apply (rule obj_ref_is_gen_obj_ref) apply (drule(2) cap_relation_untyped_ptr_obj_refs)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s' (cte_map slot) = Some cte; ctes_of s' y = Some cte'; cte_map slot \<noteq> y; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> obj_refs cap \<noteq> {}) slot s\<rbrakk> \<Longrightarrow> capClass (cteCap cte') \<noteq> PhysicalClass \<or> isUntypedCap (cteCap cte') \<or> global.capUntypedPtr (cteCap cte) \<noteq> global.capUntypedPtr (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s' (cte_map slot) = Some cte; ctes_of s' y = Some cte'; cte_map slot \<noteq> y; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> obj_refs cap \<noteq> {}) slot s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_map slot \<noteq> y; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> obj_refs cap \<noteq> {}) slot s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); \<exists>c slota. cte_wp_at ((=) c) slota s \<and> cap_relation c (cteCap cte) \<and> cte_map slot = cte_map slota; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte') \<and> y = cte_map slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> obj_refs cap \<noteq> {}) slot s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); cte_wp_at ((=) c) (a, b) s; cte_wp_at ((=) ca) (aa, ba) s; cap_relation c (cteCap cte); cte_map slot = cte_map (a, b); cap_relation ca (cteCap cte'); y = cte_map (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> obj_refs cap \<noteq> {}) (a, b) s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); cte_wp_at ((=) c) (a, b) s; cte_wp_at ((=) ca) (aa, ba) s; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (a, b) s) = {(c, s)}; fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> ObjRef (global.capUntypedPtr (cteCap cte)) \<in> gen_obj_refs c
 2. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> ObjRef (global.capUntypedPtr (cteCap cte)) \<in> gen_obj_refs c
 3. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> ObjRef (global.capUntypedPtr (cteCap cte)) \<in> gen_obj_refs ca proof (prove)
goal (3 subgoals):
 1. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte) \<in> obj_refs c
 2. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> ObjRef (global.capUntypedPtr (cteCap cte)) \<in> gen_obj_refs c
 3. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> ObjRef (global.capUntypedPtr (cteCap cte)) \<in> gen_obj_refs ca proof (prove)
goal (2 subgoals):
 1. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> ObjRef (global.capUntypedPtr (cteCap cte)) \<in> gen_obj_refs c
 2. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> ObjRef (global.capUntypedPtr (cteCap cte)) \<in> gen_obj_refs ca proof (prove)
goal (2 subgoals):
 1. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte) \<in> obj_refs c
 2. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> ObjRef (global.capUntypedPtr (cteCap cte)) \<in> gen_obj_refs ca proof (prove)
goal (1 subgoal):
 1. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> ObjRef (global.capUntypedPtr (cteCap cte)) \<in> gen_obj_refs ca proof (prove)
goal (1 subgoal):
 1. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); cap_relation ca (cteCap cte'); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte) \<in> obj_refs ca proof (prove)
goal (1 subgoal):
 1. \<And>c ca a aa b ba. \<lbrakk>cte_map (a, b) \<noteq> cte_map (aa, ba); pspace_relation (kheap s) (ksPSpace s'); valid_objs s; pspace_aligned s; pspace_distinct s; capClass (cteCap cte') = PhysicalClass; \<not> isUntypedCap (cteCap cte'); global.capUntypedPtr (cteCap cte) = global.capUntypedPtr (cteCap cte'); fst (get_cap (aa, ba) s) = {(ca, s)}; cap_relation c (cteCap cte); y = cte_map (aa, ba); slot = (a, b); is_final_cap' c s; obj_refs c \<noteq> {}; global.capUntypedPtr (cteCap cte') \<in> obj_refs ca\<rbrakk> \<Longrightarrow> global.capUntypedPtr (cteCap cte) \<in> obj_refs ca proof (prove)
goal:
No subgoals!