theory Detype_R

lemma no_overlap_check:
  "\<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s;
    pspace_aligned' s;n\<noteq> 0\<rbrakk>
   \<Longrightarrow> case_option (return ())
                   (case_prod (\<lambda>x y. haskell_assert (x < fromPPtr ptr) []))
                   (fst (lookupAround2 (ptr + of_nat (shiftL n bits - Suc 0))
                                       (ksPSpace s))) s =
       return () s" apply (clarsimp split:option.splits simp:assert_def lookupAround2_char1 not_less) apply (rule ccontr) apply (frule(1) pspace_no_overlapD') apply (erule_tac x = a in in_empty_interE) apply clarsimp apply (drule(1) pspace_alignedD') apply (erule is_aligned_no_overflow) apply clarsimp apply (erule order_trans) apply (frule range_cover_cell_subset[where x = "of_nat n - 1"]) apply (rule gt0_iff_gem1[THEN iffD1]) apply (simp add:word_gt_0) apply (rule range_cover_not_zero) apply simp apply assumption apply (clarsimp simp:shiftL_nat field_simps) apply (erule impE) apply (frule range_cover_subset_not_empty[rotated,where x = "of_nat n - 1"]) apply (rule gt0_iff_gem1[THEN iffD1]) apply (simp add:word_gt_0) apply (rule range_cover_not_zero) apply simp apply assumption apply (clarsimp simp:field_simps) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; n \<noteq> 0\<rbrakk> \<Longrightarrow> (case fst (lookupAround2 (ptr + word_of_nat (shiftL n bits - Suc 0)) (ksPSpace s)) of None \<Rightarrow> return () | Some (xa, y) \<Rightarrow> haskell_assert (xa < fromPPtr ptr) []) s = return () s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL n bits - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b\<rbrakk> \<Longrightarrow> fail s = return () s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL n bits - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL n bits - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {a..a + 2 ^ objBitsKO b - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL n bits - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> a \<in> {a..a + 2 ^ objBitsKO b - 1}
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL n bits - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL n bits - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> a \<le> a + 2 ^ objBitsKO b - 1
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL n bits - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL n bits - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; fail s \<noteq> return () s; is_aligned a (objBitsKO b)\<rbrakk> \<Longrightarrow> a \<le> a + 2 ^ objBitsKO b - 1
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL n bits - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL n bits - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; a \<le> ptr + word_of_nat (shiftL n bits - Suc 0); \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> a \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> ptr + word_of_nat (shiftL n bits - Suc 0) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> word_of_nat n - 1 < word_of_nat n
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat (shiftL n bits - Suc 0) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> 0 < word_of_nat n
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat (shiftL n bits - Suc 0) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat (shiftL n bits - Suc 0) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> range_cover (?ptr41 a b) (?sz41 a b) (?bits41 a b) n
 3. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat (shiftL n bits - Suc 0) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> range_cover (?ptr41 a b) (?sz41 a b) (?bits41 a b) n
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat (shiftL n bits - Suc 0) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat (shiftL n bits - Suc 0) \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat (shiftL n bits - Suc 0) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ptr \<le> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<and> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<le> ptr + word_of_nat n * 2 ^ bits - 1
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; ptr \<le> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<and> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> word_of_nat n - 1 < word_of_nat n
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<le> ptr + word_of_nat n * 2 ^ bits - 1
 3. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; ptr \<le> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<and> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> 0 < word_of_nat n
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<le> ptr + word_of_nat n * 2 ^ bits - 1
 3. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; ptr \<le> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<and> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<le> ptr + word_of_nat n * 2 ^ bits - 1
 3. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; ptr \<le> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<and> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> range_cover (?ptr53 a b) (?sz53 a b) (?bits53 a b) n
 3. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<le> ptr + word_of_nat n * 2 ^ bits - 1
 4. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; ptr \<le> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<and> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s\<rbrakk> \<Longrightarrow> range_cover (?ptr53 a b) (?sz53 a b) (?bits53 a b) n
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<le> ptr + word_of_nat n * 2 ^ bits - 1
 3. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; ptr \<le> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<and> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; {ptr + (word_of_nat n - 1) * 2 ^ bits..ptr + (word_of_nat n - 1) * 2 ^ bits + 2 ^ bits - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<le> ptr + word_of_nat n * 2 ^ bits - 1
 2. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; ptr \<le> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<and> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s; 0 < n; ptr \<le> a; \<forall>z. a < z \<and> z \<le> ptr + word_of_nat n * 2 ^ bits - 1 \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; fail s \<noteq> return () s; ptr \<le> ptr + word_of_nat n * 2 ^ bits - 2 ^ bits \<and> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ bits - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal:
No subgoals!