theory PageTableDuplicates

lemma globalPDEWindow_neg_mask:
  "\<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a);is_aligned ptr pdBits\<rbrakk>
  \<Longrightarrow> y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ (pdBits) - 1)}
  \<Longrightarrow> x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ (pdBits) - 1)}" apply (clarsimp simp: pptrBase_def) apply (intro conjI) apply (rule_tac y = "y &&~~ mask (vs_ptr_align a)" in order_trans) apply (rule is_aligned_le_mask) apply (rule is_aligned_weaken[OF _ vs_ptr_align_upbound]) apply (erule aligned_add_aligned[OF is_aligned_weaken[OF _ le_refl]]) apply (simp add:is_aligned_def) apply (simp add:pdBits_def pageBits_def) apply simp apply (drule sym) apply (simp add:word_and_le2) apply (drule_tac x = y in neg_mask_mono_le[where n = pdBits]) apply (subst (asm) is_aligned_add_helper) apply simp apply (simp add:pdBits_def pageBits_def pdeBits_def) apply (rule order_trans[OF and_neg_mask_plus_mask_mono[where n = pdBits]]) apply (drule mask_out_first_mask_some[where m = pdBits]) apply (cut_tac a = a in vs_ptr_align_upbound) apply (simp add:pdBits_def pageBits_def) apply (cut_tac a = a in vs_ptr_align_upbound) apply (drule le_trans[where k = 14]) apply simp apply (simp add:and_not_mask_twice max_def
    pdBits_def pageBits_def pdeBits_def) apply (simp add:mask_def) apply (subst add.commute) apply (subst add.commute[where a = ptr]) apply (rule word_plus_mono_right) apply simp apply (rule olen_add_eqv[THEN iffD2]) apply (simp add:field_simps) apply (erule is_aligned_no_wrap') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> ptr + 0x3800 \<le> x \<and> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> ptr + 0x3800 \<le> x
 2. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> ptr + 0x3800 \<le> y && ~~ mask (vs_ptr_align a)
 2. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> y && ~~ mask (vs_ptr_align a) \<le> x
 3. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> is_aligned (ptr + 0x3800) (vs_ptr_align a)
 2. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> ptr + 0x3800 \<le> y
 3. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> y && ~~ mask (vs_ptr_align a) \<le> x
 4. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> is_aligned (ptr + 0x3800) 6
 2. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> ptr + 0x3800 \<le> y
 3. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> y && ~~ mask (vs_ptr_align a) \<le> x
 4. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> is_aligned 0x3800 6
 2. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> 6 \<le> pdBits
 3. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> ptr + 0x3800 \<le> y
 4. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> y && ~~ mask (vs_ptr_align a) \<le> x
 5. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> 6 \<le> pdBits
 2. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> ptr + 0x3800 \<le> y
 3. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> y && ~~ mask (vs_ptr_align a) \<le> x
 4. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> ptr + 0x3800 \<le> y
 2. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> y && ~~ mask (vs_ptr_align a) \<le> x
 3. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> y && ~~ mask (vs_ptr_align a) \<le> x
 2. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1); y && ~~ mask (vs_ptr_align a) = x && ~~ mask (vs_ptr_align a)\<rbrakk> \<Longrightarrow> y && ~~ mask (vs_ptr_align a) \<le> x
 2. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y \<le> ptr + (2 ^ pdBits - 1)\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr + (2 ^ pdBits - 1) && ~~ mask pdBits\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits
 2. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y\<rbrakk> \<Longrightarrow> 2 ^ pdBits - 1 < 2 ^ pdBits
 3. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y\<rbrakk> \<Longrightarrow> 2 ^ pdBits - 1 < 2 ^ pdBits
 2. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr\<rbrakk> \<Longrightarrow> x \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a); is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr\<rbrakk> \<Longrightarrow> (x && ~~ mask pdBits) + mask pdBits \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr\<rbrakk> \<Longrightarrow> vs_ptr_align a \<le> pdBits
 2. \<lbrakk>is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr; x && ~~ mask pdBits = (y && ~~ mask (vs_ptr_align a)) && ~~ mask pdBits\<rbrakk> \<Longrightarrow> (x && ~~ mask pdBits) + mask pdBits \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr; vs_ptr_align a \<le> 6\<rbrakk> \<Longrightarrow> vs_ptr_align a \<le> pdBits
 2. \<lbrakk>is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr; x && ~~ mask pdBits = (y && ~~ mask (vs_ptr_align a)) && ~~ mask pdBits\<rbrakk> \<Longrightarrow> (x && ~~ mask pdBits) + mask pdBits \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr; x && ~~ mask pdBits = (y && ~~ mask (vs_ptr_align a)) && ~~ mask pdBits\<rbrakk> \<Longrightarrow> (x && ~~ mask pdBits) + mask pdBits \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr; x && ~~ mask pdBits = (y && ~~ mask (vs_ptr_align a)) && ~~ mask pdBits; vs_ptr_align a \<le> 6\<rbrakk> \<Longrightarrow> (x && ~~ mask pdBits) + mask pdBits \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr; x && ~~ mask pdBits = (y && ~~ mask (vs_ptr_align a)) && ~~ mask pdBits\<rbrakk> \<Longrightarrow> 6 \<le> 14
 2. \<lbrakk>is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr; x && ~~ mask pdBits = (y && ~~ mask (vs_ptr_align a)) && ~~ mask pdBits; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> (x && ~~ mask pdBits) + mask pdBits \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr pdBits; ptr + 0x3800 \<le> y; y && ~~ mask pdBits \<le> ptr; x && ~~ mask pdBits = (y && ~~ mask (vs_ptr_align a)) && ~~ mask pdBits; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> (x && ~~ mask pdBits) + mask pdBits \<le> ptr + (2 ^ pdBits - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + 0x3800 \<le> y; y && ~~ mask 14 \<le> ptr; x && ~~ mask 14 = y && ~~ mask 14; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> (y && ~~ mask 14) + mask 14 \<le> ptr + 0x3FFF proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + 0x3800 \<le> y; y && 0xFFFFC000 \<le> ptr; x && 0xFFFFC000 = y && 0xFFFFC000; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> (y && 0xFFFFC000) + 0x3FFF \<le> ptr + 0x3FFF proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + 0x3800 \<le> y; y && 0xFFFFC000 \<le> ptr; x && 0xFFFFC000 = y && 0xFFFFC000; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> 0x3FFF + (y && 0xFFFFC000) \<le> ptr + 0x3FFF proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + 0x3800 \<le> y; y && 0xFFFFC000 \<le> ptr; x && 0xFFFFC000 = y && 0xFFFFC000; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> 0x3FFF + (y && 0xFFFFC000) \<le> 0x3FFF + ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr + 0x3800 \<le> y; y && 0xFFFFC000 \<le> ptr; x && 0xFFFFC000 = y && 0xFFFFC000; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> y && 0xFFFFC000 \<le> ptr
 2. \<lbrakk>is_aligned ptr 14; ptr + 0x3800 \<le> y; y && 0xFFFFC000 \<le> ptr; x && 0xFFFFC000 = y && 0xFFFFC000; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> 0x3FFF \<le> 0x3FFF + ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + 0x3800 \<le> y; y && 0xFFFFC000 \<le> ptr; x && 0xFFFFC000 = y && 0xFFFFC000; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> 0x3FFF \<le> 0x3FFF + ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + 0x3800 \<le> y; y && 0xFFFFC000 \<le> ptr; x && 0xFFFFC000 = y && 0xFFFFC000; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> ptr \<le> 0x3FFF + ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + 0x3800 \<le> y; y && 0xFFFFC000 \<le> ptr; x && 0xFFFFC000 = y && 0xFFFFC000; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 0x3FFF proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr + 0x3800 \<le> y; y && 0xFFFFC000 \<le> ptr; x && 0xFFFFC000 = y && 0xFFFFC000; vs_ptr_align a \<le> 14\<rbrakk> \<Longrightarrow> 0x3FFF < 2 ^ 14 proof (prove)
goal:
No subgoals!