theory Finalise_DR

lemma is_aligned_less_kernel_base_helper:
  "\<lbrakk>is_aligned (ptr :: word32) 6;
    ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; x < 0x40 \<rbrakk>
   \<Longrightarrow> ucast (x + ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots" apply (simp add: kernel_mapping_slots_def) apply (simp add: word_le_nat_alt shiftr_20_unat_ucast
                   unat_ucast_pd_bits_shift) apply (fold word_le_nat_alt, unfold linorder_not_le) apply (drule word_le_minus_one_leq[where x=x]) apply (subst add.commute, subst is_aligned_add_or, assumption) apply (erule order_le_less_trans, simp) apply (simp add: word_ao_dist shiftr_over_or_dist) apply (subst less_mask_eq, erule order_le_less_trans) apply (simp add: pd_bits_def pageBits_def) apply (subst is_aligned_add_or[symmetric]) apply (rule_tac n=4 in is_aligned_shiftr) apply (simp add: is_aligned_andI1) apply (rule shiftr_less_t2n) apply (erule order_le_less_trans, simp) apply (rule aligned_add_offset_less) apply (rule_tac n=4 in is_aligned_shiftr) apply (simp add: is_aligned_andI1) apply (simp add: kernel_base_def is_aligned_def) apply assumption apply (rule shiftr_less_t2n) apply (erule order_le_less_trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; x < 0x40\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (x + ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2); x < 0x40\<rbrakk> \<Longrightarrow> \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (x + ptr && mask pd_bits >> 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; \<not> unat (kernel_base >> 20) \<le> unat (ptr && mask pd_bits >> 2); x < 0x40\<rbrakk> \<Longrightarrow> \<not> unat (kernel_base >> 20) \<le> unat (x + ptr && mask pd_bits >> 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x < 0x40\<rbrakk> \<Longrightarrow> x + ptr && mask pd_bits >> 2 < kernel_base >> 20 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x40 - 1\<rbrakk> \<Longrightarrow> x + ptr && mask pd_bits >> 2 < kernel_base >> 20 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x40 - 1\<rbrakk> \<Longrightarrow> x < 2 ^ 6
 2. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x40 - 1\<rbrakk> \<Longrightarrow> (ptr || x) && mask pd_bits >> 2 < kernel_base >> 20 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x40 - 1\<rbrakk> \<Longrightarrow> (ptr || x) && mask pd_bits >> 2 < kernel_base >> 20 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> (ptr && mask pd_bits >> 2) || (x && mask pd_bits >> 2) < kernel_base >> 20 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20\<rbrakk> \<Longrightarrow> 0x3F < 2 ^ pd_bits
 2. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> (ptr && mask pd_bits >> 2) || (x >> 2) < kernel_base >> 20 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> (ptr && mask pd_bits >> 2) || (x >> 2) < kernel_base >> 20 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> is_aligned (ptr && mask pd_bits >> 2) ?n30
 2. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> x >> 2 < 2 ^ ?n30
 3. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> (ptr && mask pd_bits >> 2) + (x >> 2) < kernel_base >> 20 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> is_aligned (ptr && mask pd_bits) (4 + 2)
 2. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> x >> 2 < 2 ^ 4
 3. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> (ptr && mask pd_bits >> 2) + (x >> 2) < kernel_base >> 20 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> x >> 2 < 2 ^ 4
 2. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> (ptr && mask pd_bits >> 2) + (x >> 2) < kernel_base >> 20 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> x < 2 ^ (2 + 4)
 2. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> (ptr && mask pd_bits >> 2) + (x >> 2) < kernel_base >> 20 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> (ptr && mask pd_bits >> 2) + (x >> 2) < kernel_base >> 20 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> is_aligned (ptr && mask pd_bits >> 2) ?n36
 2. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> is_aligned (kernel_base >> 20) ?n36
 3. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> ptr && mask pd_bits >> 2 < kernel_base >> 20
 4. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> x >> 2 < 2 ^ ?n36 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> is_aligned (ptr && mask pd_bits) (4 + 2)
 2. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> is_aligned (kernel_base >> 20) 4
 3. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> ptr && mask pd_bits >> 2 < kernel_base >> 20
 4. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> x >> 2 < 2 ^ 4 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> is_aligned (kernel_base >> 20) 4
 2. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> ptr && mask pd_bits >> 2 < kernel_base >> 20
 3. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> x >> 2 < 2 ^ 4 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> ptr && mask pd_bits >> 2 < kernel_base >> 20
 2. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> x >> 2 < 2 ^ 4 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> x >> 2 < 2 ^ 4 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20; x \<le> 0x3F\<rbrakk> \<Longrightarrow> x < 2 ^ (2 + 4) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; ptr && mask pd_bits >> 2 < kernel_base >> 20\<rbrakk> \<Longrightarrow> 0x3F < 2 ^ (2 + 4) proof (prove)
goal:
No subgoals!