theory Retype_AI

lemma psp_dist:
  shows         "pspace_distinct s'" proof - have distinct:"pspace_distinct s" apply (rule valid_pspaceE) apply (rule vp) apply simp done moreover { fix x y assume xne: "x \<noteq> y" and xv: "x \<in> set (retype_addrs ptr ty n us)" and yv: "y \<in> set (retype_addrs ptr ty n us)" have "is_aligned x (obj_bits_api ty us)" apply (rule retype_addrs_aligned) apply fact+ apply (insert cover) apply (auto simp: range_cover_def word_bits_def) done moreover have "is_aligned y (obj_bits_api ty us)" apply (rule retype_addrs_aligned) apply fact+ apply (insert cover) apply (auto simp: range_cover_def word_bits_def) done ultimately have
      "{x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter>
       {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}" using xne tyunt cover apply - apply (rule aligned_neq_into_no_overlap) apply (simp_all add: range_cover_def word_bits_def obj_bits_dev_irr) done } note inter = this moreover { fix x y ko' assume xne: "x \<noteq> y" and xv: "x \<in> set (retype_addrs ptr ty n us)"
        and yv: "y \<notin> set (retype_addrs ptr ty n us)" and  "kheap s y = Some ko'" have "{x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}" apply (rule pspace_no_overlap_retype_addrs_empty [OF orth]) apply fact+ apply (insert cover tyunt) apply (simp add: range_cover_def word_bits_def)+ done } note inter' = this show ?thesis unfolding pspace_distinct_def s'_def ps_def apply (clarsimp split: if_split_asm option.splits
              simp del: Int_atLeastAtMost) apply (intro conjI impI allI) apply (erule(2) inter) apply clarify apply (erule(3) inter') apply clarify apply (subst Int_commute) apply (erule(3) inter'[OF neq_commute[THEN iffD1]]) apply clarify apply (insert vp[unfolded valid_pspace_def pspace_distinct_def]) apply clarify apply (drule_tac x = x in spec) apply (drule_tac x = y in spec) apply (erule allE impE)+ apply fastforce apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_distinct s' proof (state)
goal (1 subgoal):
 1. pspace_distinct s' proof (prove)
goal (1 subgoal):
 1. pspace_distinct s proof (prove)
goal (2 subgoals):
 1. valid_pspace ?s
 2. \<lbrakk>valid_objs ?s; pspace_aligned ?s; sym_refs (state_refs_of ?s); sym_refs (state_hyp_refs_of ?s); pspace_distinct ?s; if_live_then_nonz_cap ?s; zombies_final ?s\<rbrakk> \<Longrightarrow> pspace_distinct s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s\<rbrakk> \<Longrightarrow> pspace_distinct s proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_distinct s

goal (1 subgoal):
 1. pspace_distinct s' proof (state)
this:
pspace_distinct s

goal (1 subgoal):
 1. pspace_distinct s' proof (state)
this:
pspace_distinct s

goal (1 subgoal):
 1. pspace_distinct s' proof (state)
goal (1 subgoal):
 1. pspace_distinct s' proof (state)
this:
x \<noteq> y
x \<in> set (retype_addrs ptr ty n us)
y \<in> set (retype_addrs ptr ty n us)

goal (1 subgoal):
 1. pspace_distinct s' proof (prove)
goal (1 subgoal):
 1. is_aligned x (obj_bits_api ty us) proof (prove)
goal (4 subgoals):
 1. x \<in> set (retype_addrs ?ptr ty ?n us)
 2. is_aligned ?ptr (obj_bits_api ty us)
 3. ?sz < word_bits
 4. obj_bits_api ty us \<le> ?sz proof (prove)
goal (3 subgoals):
 1. is_aligned ptr (obj_bits_api ty us)
 2. ?sz < word_bits
 3. obj_bits_api ty us \<le> ?sz proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> is_aligned ptr (obj_bits_api ty us)
 2. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> ?sz < word_bits
 3. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> obj_bits_api ty us \<le> ?sz proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned x (obj_bits_api ty us)

goal (1 subgoal):
 1. pspace_distinct s' proof (state)
this:
is_aligned x (obj_bits_api ty us)

goal (1 subgoal):
 1. pspace_distinct s' proof (prove)
goal (1 subgoal):
 1. is_aligned y (obj_bits_api ty us) proof (prove)
goal (4 subgoals):
 1. y \<in> set (retype_addrs ?ptr ty ?n us)
 2. is_aligned ?ptr (obj_bits_api ty us)
 3. ?sz < word_bits
 4. obj_bits_api ty us \<le> ?sz proof (prove)
goal (3 subgoals):
 1. is_aligned ptr (obj_bits_api ty us)
 2. ?sz < word_bits
 3. obj_bits_api ty us \<le> ?sz proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> is_aligned ptr (obj_bits_api ty us)
 2. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> ?sz < word_bits
 3. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> obj_bits_api ty us \<le> ?sz proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned y (obj_bits_api ty us)

goal (1 subgoal):
 1. pspace_distinct s' proof (chain)
picking this:
is_aligned x (obj_bits_api ty us)
is_aligned y (obj_bits_api ty us) proof (prove)
using this:
is_aligned x (obj_bits_api ty us)
is_aligned y (obj_bits_api ty us)

goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {} proof (prove)
using this:
is_aligned x (obj_bits_api ty us)
is_aligned y (obj_bits_api ty us)
x \<noteq> y
ty \<noteq> Untyped
range_cover ptr sz (obj_bits_api ty us) n

goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x (obj_bits_api ty us); is_aligned y (obj_bits_api ty us); x \<noteq> y; ty \<noteq> Untyped; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x (obj_bits_api ty us); is_aligned y (obj_bits_api ty us); x \<noteq> y; ty \<noteq> Untyped; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<lbrakk>is_aligned x (obj_bits_api ty us); is_aligned y (obj_bits_api ty us); x \<noteq> y; ty \<noteq> Untyped; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits (default_object ty dev us))
 3. \<lbrakk>is_aligned x (obj_bits_api ty us); is_aligned y (obj_bits_api ty us); x \<noteq> y; ty \<noteq> Untyped; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> is_aligned y (obj_bits (default_object ty dev us)) proof (prove)
goal:
No subgoals! proof (state)
this:
{x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}

goal (1 subgoal):
 1. pspace_distinct s' proof (state)
this:
\<lbrakk>?x2 \<noteq> ?y2; ?x2 \<in> set (retype_addrs ptr ty n us); ?y2 \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> {?x2..?x2 + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {?y2..?y2 + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}

goal (1 subgoal):
 1. pspace_distinct s' proof (state)
this:
\<lbrakk>?x2 \<noteq> ?y2; ?x2 \<in> set (retype_addrs ptr ty n us); ?y2 \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> {?x2..?x2 + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {?y2..?y2 + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}

goal (1 subgoal):
 1. pspace_distinct s' proof (state)
this:
\<lbrakk>?x2 \<noteq> ?y2; ?x2 \<in> set (retype_addrs ptr ty n us); ?y2 \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> {?x2..?x2 + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {?y2..?y2 + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}

goal (1 subgoal):
 1. pspace_distinct s' proof (state)
this:
\<lbrakk>?x2 \<noteq> ?y2; ?x2 \<in> set (retype_addrs ptr ty n us); ?y2 \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> {?x2..?x2 + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {?y2..?y2 + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}

goal (1 subgoal):
 1. pspace_distinct s' proof (state)
goal (1 subgoal):
 1. pspace_distinct s' proof (state)
this:
x \<noteq> y
x \<in> set (retype_addrs ptr ty n us)
y \<notin> set (retype_addrs ptr ty n us)
kheap s y = Some ko'

goal (1 subgoal):
 1. pspace_distinct s' proof (prove)
goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (6 subgoals):
 1. x \<in> set (retype_addrs ptr ty ?n us)
 2. y \<notin> set (retype_addrs ptr ty ?n us)
 3. kheap s y = Some ko'
 4. ty \<noteq> Untyped
 5. range_cover ptr sz (obj_bits_api ty us) ?n
 6. obj_bits_api ty us \<le> sz proof (prove)
goal (3 subgoals):
 1. ty \<noteq> Untyped
 2. range_cover ptr sz (obj_bits_api ty us) n
 3. obj_bits_api ty us \<le> sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> ty \<noteq> Untyped
 2. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> range_cover ptr sz (obj_bits_api ty us) n
 3. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> sz proof (prove)
goal:
No subgoals! proof (state)
this:
{x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}

goal (1 subgoal):
 1. pspace_distinct s' proof (state)
this:
\<lbrakk>?x2 \<noteq> ?y2; ?x2 \<in> set (retype_addrs ptr ty n us); ?y2 \<notin> set (retype_addrs ptr ty n us); kheap s ?y2 = Some ?ko'2\<rbrakk> \<Longrightarrow> {?x2..?x2 + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {?y2..?y2 + (2 ^ obj_bits ?ko'2 - 1)} = {}

goal (1 subgoal):
 1. pspace_distinct s' proof (state)
this:
\<lbrakk>?x2 \<noteq> ?y2; ?x2 \<in> set (retype_addrs ptr ty n us); ?y2 \<notin> set (retype_addrs ptr ty n us); kheap s ?y2 = Some ?ko'2\<rbrakk> \<Longrightarrow> {?x2..?x2 + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {?y2..?y2 + (2 ^ obj_bits ?ko'2 - 1)} = {}

goal (1 subgoal):
 1. pspace_distinct s' proof (prove)
goal (1 subgoal):
 1. pspace_distinct s' proof (prove)
goal (1 subgoal):
 1. \<forall>x y ko ko'. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) x = Some ko \<and> kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> set (retype_addrs ptr ty n us) \<longrightarrow> (\<forall>y. (y \<in> set (retype_addrs ptr ty n us) \<longrightarrow> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}) \<and> (y \<notin> set (retype_addrs ptr ty n us) \<longrightarrow> (\<forall>ko'. kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {})))) \<and> (x \<notin> set (retype_addrs ptr ty n us) \<longrightarrow> (\<forall>y. (y \<in> set (retype_addrs ptr ty n us) \<longrightarrow> (\<forall>ko. kheap s x = Some ko \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {})) \<and> (y \<notin> set (retype_addrs ptr ty n us) \<longrightarrow> (\<forall>ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {})))) proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> set (retype_addrs ptr ty n us); y \<in> set (retype_addrs ptr ty n us); x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}
 2. \<And>x y ko'. \<lbrakk>x \<in> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s y = Some ko' \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}
 3. \<And>x y ko. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<in> set (retype_addrs ptr ty n us); kheap s x = Some ko \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}
 4. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y ko'. \<lbrakk>x \<in> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s y = Some ko' \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}
 2. \<And>x y ko. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<in> set (retype_addrs ptr ty n us); kheap s x = Some ko \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}
 3. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y ko'. \<lbrakk>x \<in> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s y = Some ko'; x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}
 2. \<And>x y ko. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<in> set (retype_addrs ptr ty n us); kheap s x = Some ko \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}
 3. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y ko. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<in> set (retype_addrs ptr ty n us); kheap s x = Some ko \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}
 2. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y ko. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<in> set (retype_addrs ptr ty n us); kheap s x = Some ko; x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} = {}
 2. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y ko. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<in> set (retype_addrs ptr ty n us); kheap s x = Some ko; x \<noteq> y\<rbrakk> \<Longrightarrow> {y..y + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {x..x + (2 ^ obj_bits ko - 1)} = {}
 2. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko; kheap s y = Some ko'; x \<noteq> y\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko; kheap s y = Some ko'; x \<noteq> y; (valid_objs and pspace_aligned and (\<lambda>s. \<forall>x y ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}) and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))) s\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko; kheap s y = Some ko'; x \<noteq> y; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); zombies_final s; if_live_then_nonz_cap s; \<forall>x y ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}; valid_objs s; pspace_aligned s\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko; kheap s y = Some ko'; x \<noteq> y; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); zombies_final s; if_live_then_nonz_cap s; valid_objs s; pspace_aligned s; \<forall>y ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko; kheap s y = Some ko'; x \<noteq> y; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); zombies_final s; if_live_then_nonz_cap s; valid_objs s; pspace_aligned s; \<forall>ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko; kheap s y = Some ko'; x \<noteq> y; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); zombies_final s; if_live_then_nonz_cap s; valid_objs s; pspace_aligned s\<rbrakk> \<Longrightarrow> kheap s x = Some (?ko92 x y ko ko') \<and> kheap s y = Some (?ko'94 x y ko ko') \<and> x \<noteq> y
 2. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko; kheap s y = Some ko'; x \<noteq> y; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); zombies_final s; if_live_then_nonz_cap s; valid_objs s; pspace_aligned s; {x..x + (2 ^ obj_bits (?ko92 x y ko ko') - 1)} \<inter> {y..y + (2 ^ obj_bits (?ko'94 x y ko ko') - 1)} = {}\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y ko ko'. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); y \<notin> set (retype_addrs ptr ty n us); kheap s x = Some ko; kheap s y = Some ko'; x \<noteq> y; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); zombies_final s; if_live_then_nonz_cap s; valid_objs s; pspace_aligned s; {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {} proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_distinct s'

goal:
No subgoals!