theory Retype_R

lemma obj_range'_subset_strong:
  assumes "range_cover ptr sz (objBitsKO val) n"
      and "ptr' \<in> set (new_cap_addrs n ptr val)"
  shows "obj_range' ptr' val \<subseteq> {ptr..ptr + (of_nat n * 2 ^ objBitsKO val) - 1}" proof - { assume cover: "range_cover ptr sz (objBitsKO val) n"
      and  mem_p: "ptr' \<in> set (new_cap_addrs n ptr val)"
      and  not_0: "n\<noteq> 0" note n_less = range_cover.range_cover_n_less[OF cover] have unat_of_nat_m1: "unat (of_nat n - (1::machine_word)) < n" using not_0 n_less by (simp add:unat_of_nat_minus_1) have decomp:
      "of_nat n * 2 ^ objBitsKO val =
       of_nat (n - 1) * 2 ^ objBitsKO val + (2 :: machine_word) ^ objBitsKO val" apply (simp add:distrib_right[where b = "1 :: machine_word",simplified,symmetric]) using not_0 n_less apply simp done have "ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + of_nat n * 2 ^ objBitsKO val - 1" using cover apply (subst decomp) apply (simp add:add.assoc[symmetric]) apply (simp add:p_assoc_help) apply (rule order_trans[OF word_plus_mono_left word_plus_mono_right]) using mem_p not_0 apply (clarsimp simp:new_cap_addrs_def shiftl_t2n) apply (rule word_plus_mono_right) apply (subst mult.commute) apply (rule word_mult_le_mono1[OF word_of_nat_le]) using n_less not_0 apply (simp add:unat_of_nat_minus_1) apply (rule p2_gt_0[THEN iffD2]) apply (simp add:word_bits_def range_cover_def) apply (simp only: word_bits_def[symmetric]) apply (clarsimp simp: unat_of_nat_minus_1[OF n_less(1) not_0]) apply (rule nat_less_power_trans2
            [OF range_cover.range_cover_le_n_less(2),OF cover, folded word_bits_def]) apply (simp add:unat_of_nat_m1 less_imp_le) apply (simp add:range_cover_def word_bits_def) apply (rule machine_word_plus_mono_right_split[where sz = sz]) using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::machine_word))"] apply (clarsimp simp:unat_of_nat_m1) apply (simp add:range_cover_def word_bits_def) apply (rule olen_add_eqv[THEN iffD2]) apply (subst add.commute[where a = "2^objBitsKO val - 1"]) apply (subst p_assoc_help[symmetric]) apply (rule is_aligned_no_overflow) apply (clarsimp simp:range_cover_def word_bits_def) apply (erule aligned_add_aligned[OF _  is_aligned_mult_triv2]; simp) apply simp by (meson assms(1) is_aligned_add is_aligned_mult_triv2 is_aligned_no_overflow' range_cover_def) } with assms show ?thesis unfolding obj_range'_def apply - apply (frule(1) obj_range'_subset) apply (simp add: obj_range'_def) apply (cases "n = 0"; clarsimp simp:new_cap_addrs_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (state)
goal (1 subgoal):
 1. obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (state)
goal (1 subgoal):
 1. obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (state)
this:
range_cover ptr sz (objBitsKO val) n
ptr' \<in> set (new_cap_addrs n ptr val)
n \<noteq> 0

goal (1 subgoal):
 1. obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (state)
this:
n < 2 ^ LENGTH(32)
n < 2 ^ (LENGTH(32) - objBitsKO val)

goal (1 subgoal):
 1. obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat n - 1) < n proof (prove)
using this:
n \<noteq> 0
n < 2 ^ LENGTH(32)
n < 2 ^ (LENGTH(32) - objBitsKO val)

goal (1 subgoal):
 1. unat (word_of_nat n - 1) < n proof (state)
this:
unat (word_of_nat n - 1) < n

goal (1 subgoal):
 1. obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (prove)
goal (1 subgoal):
 1. word_of_nat n * 2 ^ objBitsKO val = word_of_nat (n - 1) * 2 ^ objBitsKO val + 2 ^ objBitsKO val proof (prove)
goal (1 subgoal):
 1. word_of_nat n * 2 ^ objBitsKO val = (word_of_nat (n - Suc 0) + 1) * 2 ^ objBitsKO val proof (prove)
using this:
n \<noteq> 0
n < 2 ^ LENGTH(32)
n < 2 ^ (LENGTH(32) - objBitsKO val)

goal (1 subgoal):
 1. word_of_nat n * 2 ^ objBitsKO val = (word_of_nat (n - Suc 0) + 1) * 2 ^ objBitsKO val proof (prove)
goal:
No subgoals! proof (state)
this:
word_of_nat n * 2 ^ objBitsKO val = word_of_nat (n - 1) * 2 ^ objBitsKO val + 2 ^ objBitsKO val

goal (1 subgoal):
 1. obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (prove)
goal (1 subgoal):
 1. ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat n * 2 ^ objBitsKO val - 1 proof (prove)
using this:
range_cover ptr sz (objBitsKO val) n

goal (1 subgoal):
 1. ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat n * 2 ^ objBitsKO val - 1 proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + (word_of_nat (n - 1) * 2 ^ objBitsKO val + 2 ^ objBitsKO val) - 1 proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + 2 ^ objBitsKO val - 1 proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr' + (2 ^ objBitsKO val - 1) \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr' \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
using this:
ptr' \<in> set (new_cap_addrs n ptr val)
n \<noteq> 0

goal (4 subgoals):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr' \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr + 2 ^ objBitsKO val * word_of_nat x \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> 2 ^ objBitsKO val * word_of_nat x \<le> (word_of_nat n - 1) * 2 ^ objBitsKO val
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> word_of_nat x * 2 ^ objBitsKO val \<le> (word_of_nat n - 1) * 2 ^ objBitsKO val
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> x \<le> unat (word_of_nat n - 1)
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> 0 < 2 ^ objBitsKO val
 3. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 4. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 6. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 7. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
using this:
n < 2 ^ LENGTH(32)
n < 2 ^ (LENGTH(32) - objBitsKO val)
n \<noteq> 0

goal (7 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> x \<le> unat (word_of_nat n - 1)
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> 0 < 2 ^ objBitsKO val
 3. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 4. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 6. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 7. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> 0 < 2 ^ objBitsKO val
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 3. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 6. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> objBitsKO val < LENGTH(32)
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 3. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 6. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ objBitsKO val) < 2 ^ LENGTH(32)
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> unat (word_of_nat n - 1) * unat (2 ^ objBitsKO val) < 2 ^ word_bits
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> (n - Suc 0) * 2 ^ objBitsKO val < 2 ^ word_bits
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> n - Suc 0 \<le> n
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> objBitsKO val \<le> word_bits
 3. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 6. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> objBitsKO val \<le> word_bits
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ objBitsKO val
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat ((word_of_nat n - 1) * 2 ^ objBitsKO val) < 2 ^ sz
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> sz < word_bits
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
using this:
unat (word_of_nat n - 1) < n \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat (unat (word_of_nat n - 1)) * 2 ^ objBitsKO val) < 2 ^ sz

goal (5 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat ((word_of_nat n - 1) * 2 ^ objBitsKO val) < 2 ^ sz
 2. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> sz < word_bits
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 5. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (objBitsKO val) n; x < n; ptr' = ptr + 2 ^ objBitsKO val * word_of_nat x\<rbrakk> \<Longrightarrow> sz < word_bits
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 4. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> 2 ^ objBitsKO val - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val)
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1)
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + 2 ^ objBitsKO val - 1
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (3 subgoals):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> is_aligned (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val) (objBitsKO val)
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val)\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val) (objBitsKO val)
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 3. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> 2 ^ objBitsKO val - 1 \<le> 2 ^ objBitsKO val - 1
 2. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO val) n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ objBitsKO val + (2 ^ objBitsKO val - 1) proof (state)
this:
ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat n * 2 ^ objBitsKO val - 1

goal (1 subgoal):
 1. obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (state)
this:
\<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val); n \<noteq> 0\<rbrakk> \<Longrightarrow> ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat n * 2 ^ objBitsKO val - 1

goal (1 subgoal):
 1. obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (chain)
picking this:
range_cover ptr sz (objBitsKO val) n
ptr' \<in> set (new_cap_addrs n ptr val)
\<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val); n \<noteq> 0\<rbrakk> \<Longrightarrow> ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat n * 2 ^ objBitsKO val - 1 proof (prove)
using this:
range_cover ptr sz (objBitsKO val) n
ptr' \<in> set (new_cap_addrs n ptr val)
\<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val); n \<noteq> 0\<rbrakk> \<Longrightarrow> ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat n * 2 ^ objBitsKO val - 1

goal (1 subgoal):
 1. obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (prove)
using this:
range_cover ptr sz (objBitsKO val) n
ptr' \<in> set (new_cap_addrs n ptr val)
\<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val); n \<noteq> 0\<rbrakk> \<Longrightarrow> ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat n * 2 ^ objBitsKO val - 1

goal (1 subgoal):
 1. {ptr'..ptr' + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val); \<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val); n \<noteq> 0\<rbrakk> \<Longrightarrow> ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat n * 2 ^ objBitsKO val - 1\<rbrakk> \<Longrightarrow> {ptr'..ptr' + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val); \<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val); n \<noteq> 0\<rbrakk> \<Longrightarrow> ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat n * 2 ^ objBitsKO val - 1; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr'..ptr' + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val) n; ptr' \<in> set (new_cap_addrs n ptr val); 0 < n \<Longrightarrow> ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat n * 2 ^ objBitsKO val - 1; ptr' \<le> ptr' + 2 ^ objBitsKO val - 1 \<longrightarrow> ptr \<le> ptr' \<and> ptr' + 2 ^ objBitsKO val - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr' \<le> ptr' + 2 ^ objBitsKO val - 1 \<longrightarrow> ptr' + 2 ^ objBitsKO val - 1 \<le> ptr + word_of_nat n * 2 ^ objBitsKO val - 1 proof (prove)
goal:
No subgoals! proof (state)
this:
obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1}

goal:
No subgoals!