theory PageTableDuplicates

lemma new_cap_addrs_same_align_pdpt_bits:
assumes inset: "p\<in>set (new_cap_addrs (2 ^ us) ptr ko)"
  and   lowbound: "vs_entry_align ko \<le> us"
  and   pdpt_align:"p && ~~ mask (vs_ptr_align ko) = p' && ~~ mask (vs_ptr_align ko)"
shows
    "\<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30;is_aligned p' 2\<rbrakk>
  \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko)" apply (subgoal_tac "\<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6;
         x < 2 ^ us\<rbrakk>
        \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (of_nat x << 2)") prefer 2 using lowbound inset apply - apply (drule mask_out_first_mask_some[where m = "us + 2"]) apply (simp add:mask_lower_twice)+ apply (subst (asm) is_aligned_add_helper[THEN conjunct2]) apply simp apply (rule shiftl_less_t2n) apply (simp add:of_nat_power) apply simp apply (rule_tac x= "unat (p' && mask (Suc (Suc us)) >> 2) " in bexI) apply simp apply (subst shiftr_shiftl1) apply simp+ apply (subst is_aligned_neg_mask_eq[where n = 2]) apply (erule is_aligned_andI1) apply (simp add:mask_out_sub_mask) apply simp apply (rule unat_less_power) apply (simp add:word_bits_def) apply (rule shiftr_less_t2n) apply (rule le_less_trans[OF word_and_le1]) apply (rule less_le_trans[OF mask_lt_2pn]) apply simp apply simp using pdpt_align apply (clarsimp simp: image_def vs_entry_align_def vs_ptr_align_def
    new_cap_addrs_def objBits_simps archObjSize_def pdeBits_def pteBits_def
    split:ARM_H.pde.splits ARM_H.pte.splits arch_kernel_object.splits
    Structures_H.kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko)
 2. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)
 2. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
using this:
vs_entry_align ko \<le> us
p \<in> set (new_cap_addrs (2 ^ us) ptr ko)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)
 2. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)
 2. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> 6 \<le> us + 2
 2. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr + (word_of_nat x << 2) && ~~ mask (us + 2) = (p' && ~~ mask 6) && ~~ mask (us + 2)\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)
 3. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr + (word_of_nat x << 2) && ~~ mask (Suc (Suc us)) = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)
 2. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> is_aligned ptr (Suc (Suc us))
 2. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> word_of_nat x << 2 < 2 ^ Suc (Suc us)
 3. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)
 4. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> word_of_nat x << 2 < 2 ^ Suc (Suc us)
 2. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)
 3. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> word_of_nat x < 2 ^ (Suc (Suc us) - 2)
 2. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> Suc (Suc us) < LENGTH(32)
 3. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)
 4. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> Suc (Suc us) < LENGTH(32)
 2. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)
 3. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2)
 2. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> p' = ptr + (word_of_nat (unat (p' && mask (Suc (Suc us)) >> 2)) << 2)
 2. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> unat (p' && mask (Suc (Suc us)) >> 2) \<in> {0..<2 ^ us}
 3. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> p' = (p' && ~~ mask (Suc (Suc us))) + (p' && mask (Suc (Suc us)) >> 2 << 2)
 2. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> unat (p' && mask (Suc (Suc us)) >> 2) \<in> {0..<2 ^ us}
 3. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> 2 \<le> 2
 2. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> p' = (p' && ~~ mask (Suc (Suc us))) + ((p' && mask (Suc (Suc us)) >> 2 - 2) && ~~ mask 2)
 3. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> unat (p' && mask (Suc (Suc us)) >> 2) \<in> {0..<2 ^ us}
 4. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> p' = (p' && ~~ mask (Suc (Suc us))) + ((p' && mask (Suc (Suc us))) && ~~ mask 2)
 2. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> unat (p' && mask (Suc (Suc us)) >> 2) \<in> {0..<2 ^ us}
 3. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> is_aligned (p' && mask (Suc (Suc us))) 2
 2. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> p' = (p' && ~~ mask (Suc (Suc us))) + (p' && mask (Suc (Suc us)))
 3. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> unat (p' && mask (Suc (Suc us)) >> 2) \<in> {0..<2 ^ us}
 4. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> p' = (p' && ~~ mask (Suc (Suc us))) + (p' && mask (Suc (Suc us)))
 2. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> unat (p' && mask (Suc (Suc us)) >> 2) \<in> {0..<2 ^ us}
 3. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko + us); is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> unat (p' && mask (Suc (Suc us)) >> 2) \<in> {0..<2 ^ us}
 2. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> unat (p' && mask (Suc (Suc us)) >> 2) < 2 ^ us
 2. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> us < LENGTH(32)
 2. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> p' && mask (Suc (Suc us)) >> 2 < 2 ^ us
 3. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> p' && mask (Suc (Suc us)) >> 2 < 2 ^ us
 2. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> p' && mask (Suc (Suc us)) < 2 ^ (2 + us)
 2. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> mask (Suc (Suc us)) < 2 ^ (2 + us)
 2. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> Suc (Suc us) < LENGTH(32)
 2. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> 2 ^ Suc (Suc us) \<le> 2 ^ (2 + us)
 3. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (p' && ~~ mask (Suc (Suc us))) (objBitsKO ko + us); us < 30; is_aligned p' 2; 4 \<le> us; x < 2 ^ us; vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) (p' && ~~ mask (Suc (Suc us))) ko); ptr = p' && ~~ mask (Suc (Suc us))\<rbrakk> \<Longrightarrow> 2 ^ Suc (Suc us) \<le> 2 ^ (2 + us)
 2. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
using this:
p && ~~ mask (vs_ptr_align ko) = p' && ~~ mask (vs_ptr_align ko)

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO ko + us); us < 30; is_aligned p' 2; \<And>x. \<lbrakk>is_aligned ptr (Suc (Suc us)); us < 30; is_aligned p' 2; 4 \<le> us; ptr + (word_of_nat x << 2) && ~~ mask 6 = p' && ~~ mask 6; x < 2 ^ us\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<2 ^ us}. p' = ptr + (word_of_nat x << 2); vs_entry_align ko \<le> us; p \<in> set (new_cap_addrs (2 ^ us) ptr ko)\<rbrakk> \<Longrightarrow> p' \<in> set (new_cap_addrs (2 ^ us) ptr ko) proof (prove)
goal:
No subgoals!