theory ArchAcc_AI

lemma pte_at_aligned_vptr:
  "\<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; page_table_at pt s;
   pspace_aligned s; is_aligned vptr 16 \<rbrakk>
  \<Longrightarrow> pte_at (x + (pt + (((vptr >> 12) && 0xFF) << 2))) s" apply (erule page_table_pte_at_diffE[where x="(x >> 2) + ((vptr >> 12) && 0xFF)"];simp?) apply (simp add: word_shiftl_add_distrib upto_enum_step_def) apply (clarsimp simp: word_shift_by_2 shiftr_shiftl1 is_aligned_shift) apply (subst add.commute, rule is_aligned_add_less_t2n) apply (rule is_aligned_andI1[where n=4], rule is_aligned_shiftr, simp) apply (rule shiftr_less_t2n) apply (clarsimp dest!: upto_enum_step_subset[THEN subsetD]) apply (erule order_le_less_trans, simp) apply (simp add: pt_bits_def pageBits_def) apply (simp add: pt_bits_def pageBits_def) apply (rule order_le_less_trans, rule word_and_le1, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; typ_at (AArch APageTable) pt s; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> pte_at (x + (pt + ((vptr >> 12) && 0xFF << 2))) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> x + ((vptr >> 12) && 0xFF << 2) = (x >> 2) + ((vptr >> 12) && 0xFF) << 2
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> (x >> 2) + ((vptr >> 12) && 0xFF) < 2 ^ (pt_bits - 2) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> (\<lambda>x. x * 4) ` {x. x \<le> 0xF}; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> x = x >> 2 << 2
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> (x >> 2) + ((vptr >> 12) && 0xFF) < 2 ^ (pt_bits - 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> (x >> 2) + ((vptr >> 12) && 0xFF) < 2 ^ (pt_bits - 2) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF) ?n21
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> x >> 2 < 2 ^ ?n21
 3. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> ?n21 \<le> pt_bits - 2
 4. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (pt_bits - 2) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> x >> 2 < 2 ^ 4
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> 4 \<le> pt_bits - 2
 3. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (pt_bits - 2) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> x < 2 ^ (2 + 4)
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> 4 \<le> pt_bits - 2
 3. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (pt_bits - 2) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pspace_aligned s; is_aligned vptr 16; x \<le> 0x3C\<rbrakk> \<Longrightarrow> x < 0x40
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> 4 \<le> pt_bits - 2
 3. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (pt_bits - 2) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> 4 \<le> pt_bits - 2
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (pt_bits - 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (pt_bits - 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 16\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 0x100 proof (prove)
goal:
No subgoals!