theory ArchAcc_AI

lemma lookup_pd_slot_add_eq:
  "\<lbrakk> is_aligned pd pd_bits; is_aligned vptr 24; x \<in> set [0 , 4 .e. 0x3C] \<rbrakk>
  \<Longrightarrow> (x + lookup_pd_slot pd vptr && ~~ mask pd_bits) = pd" apply (simp add: pageBits_def add.commute add.left_commute lookup_pd_slot_def Let_def) apply (clarsimp simp: upto_enum_step_def word_shift_by_2) apply (erule add_mask_lower_bits2) apply (subgoal_tac "2 < pd_bits \<and> size vptr \<le> 18 + pd_bits") apply (simp add: and_mask_0_iff_le_mask le_mask_iff) apply (subst word_plus_and_or_coroll) apply (subst word_bw_comms) apply (rule aligned_mask_disjoint[where n=6]) apply (rule is_aligned_shiftl, rule is_aligned_shiftr, simp) apply (rule order.trans, rule leq_high_bits_shiftr_low_bits_leq_bits[where high_bits=4]) apply (clarsimp simp: mask_def, simp) apply (clarsimp simp: shiftr_over_or_dist word_or_zero) apply (intro conjI) apply (clarsimp simp: shiftl_shiftr3) apply (subgoal_tac "xa >> pd_bits - 2 = 0", simp) apply (rule shiftr_le_0, rule unat_less_helper) apply (erule order.strict_trans1, simp) apply (clarsimp simp: pd_bits_def pageBits_def) apply (clarsimp simp: shiftl_shiftr2 shiftr_shiftr shiftr_zero_size) apply (clarsimp simp: pd_bits_def pageBits_def word_bits_size word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; is_aligned vptr 24; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> x + lookup_pd_slot pd vptr && ~~ mask pd_bits = pd proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; is_aligned vptr 24; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> pd + (x + (vptr >> 20 << 2)) && ~~ mask pd_bits = pd proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned pd pd_bits; is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> pd + ((xa << 2) + (vptr >> 20 << 2)) && ~~ mask pd_bits = pd proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> (xa << 2) + (vptr >> 20 << 2) && ~~ mask pd_bits = 0 proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> (xa << 2) + (vptr >> 20 << 2) && ~~ mask pd_bits = 0
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> (xa << 2) + (vptr >> 20 << 2) >> pd_bits = 0
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> (xa << 2) && (vptr >> 20 << 2) = 0
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> (xa << 2) || (vptr >> 20 << 2) >> pd_bits = 0
 3. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> (vptr >> 20 << 2) && (xa << 2) = 0
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> (xa << 2) || (vptr >> 20 << 2) >> pd_bits = 0
 3. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 20 << 2) 6
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> xa << 2 \<le> mask 6
 3. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> (xa << 2) || (vptr >> 20 << 2) >> pd_bits = 0
 4. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> xa << 2 \<le> mask 6
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> (xa << 2) || (vptr >> 20 << 2) >> pd_bits = 0
 3. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> xa \<le> mask 4
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> mask (2 + 4) \<le> mask 6
 3. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> (xa << 2) || (vptr >> 20 << 2) >> pd_bits = 0
 4. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> (xa << 2) || (vptr >> 20 << 2) >> pd_bits = 0
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> xa << 2 >> pd_bits = 0 \<and> vptr >> 20 << 2 >> pd_bits = 0
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> xa << 2 >> pd_bits = 0
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> vptr >> 20 << 2 >> pd_bits = 0
 3. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> (xa >> pd_bits - 2) && mask (size xa - pd_bits) = 0
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> vptr >> 20 << 2 >> pd_bits = 0
 3. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> xa >> pd_bits - 2 = 0
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> vptr >> 20 << 2 >> pd_bits = 0
 3. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> xa < word_of_nat (2 ^ (pd_bits - 2))
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> vptr >> 20 << 2 >> pd_bits = 0
 3. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> 0xF < 2 ^ (pd_bits - 2)
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> vptr >> 20 << 2 >> pd_bits = 0
 3. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF; 2 < pd_bits; size vptr \<le> 18 + pd_bits\<rbrakk> \<Longrightarrow> vptr >> 20 << 2 >> pd_bits = 0
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 < pd_bits \<and> size vptr \<le> 18 + pd_bits proof (prove)
goal:
No subgoals!