theory ArchAcc_AI

lemma less_kernel_base_mapping_slots_both:
  "\<lbrakk> vptr < kernel_base; is_aligned pd pd_bits;
          (x = 0)
           \<or> (x < 2 ^ 4 \<and> vmsz_aligned vptr ARMSuperSection) \<rbrakk>
       \<Longrightarrow> ucast ((x << 2) + lookup_pd_slot pd vptr && mask pd_bits >> 2)
                \<notin> kernel_mapping_slots" apply (simp add: lookup_pd_slot_def Let_def) apply (subst field_simps, subst mask_add_aligned, assumption) apply (subst vptr_shifting_helper_magic) apply simp apply (simp add: shiftr_shiftl_mask_pd_bits triple_shift_fun) apply (simp add: kernel_mapping_slots_def linorder_not_le
                   shiftr_20_less) apply (rule le_m1_iff_lt[THEN iffD1,THEN iffD1]) apply (simp add:kernel_base_def) apply (erule disjE) apply (drule word_less_sub_1) apply simp apply (drule le_shiftr[where n=20]) apply (clarsimp simp :kernel_base_def vmsz_aligned_def)+ apply (drule(1) gap_between_aligned) apply (simp add:is_aligned_def) apply simp apply (rule order.trans[OF le_shiftr]) apply (rule word_plus_mono_right[OF _ is_aligned_no_wrap'[where off = "2^24-1"]]) apply (rule word_less_sub_1) apply (rule shiftl_less_t2n) apply simp+ apply (clarsimp dest!:word_less_sub_1) apply (erule order.trans[OF le_shiftr]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0 \<or> x < 2 ^ 4 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x << 2) + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0 \<or> x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x << 2) + (pd + (vptr >> 20 << 2)) && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0 \<or> x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x << 2) + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0 \<or> x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> x = 0 \<or> x < 2 ^ 4 \<and> vmsz_aligned vptr ARMSuperSection
 2. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0 \<or> x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((vptr + (x << 20) >> 20 << 2) && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0 \<or> x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((vptr + (x << 20) >> 20 << 2) && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0 \<or> x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr + (x << 20) >> 20) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0 \<or> x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 < kernel_base >> 20 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0 \<or> x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> 0 < kernel_base >> 20
 2. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0 \<or> x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> (kernel_base >> 20) - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0 \<or> x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> (kernel_base >> 20) - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x = 0\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> (kernel_base >> 20) - 1
 2. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> (kernel_base >> 20) - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; x = 0; vptr \<le> kernel_base - 1\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> (kernel_base >> 20) - 1
 2. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> (kernel_base >> 20) - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; x = 0; vptr \<le> kernel_base - 1\<rbrakk> \<Longrightarrow> vptr >> 20 \<le> (kernel_base >> 20) - 1
 2. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> (kernel_base >> 20) - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; x = 0; vptr >> 20 \<le> kernel_base - 1 >> 20\<rbrakk> \<Longrightarrow> vptr >> 20 \<le> (kernel_base >> 20) - 1
 2. \<lbrakk>vptr < kernel_base; is_aligned pd pd_bits; x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> (kernel_base >> 20) - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < 0xE0000000; is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> 0xDFF proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> is_aligned 0xE0000000 24
 2. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> 24 < LENGTH(32)
 3. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> 0xDFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> 24 < LENGTH(32)
 2. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> 0xDFF proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> vptr + (x << 20) >> 20 \<le> 0xDFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> vptr + (x << 20) \<le> ?v79
 2. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> ?v79 >> 20 \<le> 0xDFF proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> x << 20 \<le> 2 ^ 24 - 1
 2. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> is_aligned vptr ?sz83
 3. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> 2 ^ 24 - 1 < 2 ^ ?sz83
 4. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> vptr + (2 ^ 24 - 1) >> 20 \<le> 0xDFF proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> x << 20 < 2 ^ 24
 2. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> is_aligned vptr ?sz83
 3. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> 2 ^ 24 - 1 < 2 ^ ?sz83
 4. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> vptr + (2 ^ 24 - 1) >> 20 \<le> 0xDFF proof (prove)
goal (5 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> x < 2 ^ (24 - 20)
 2. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> 24 < LENGTH(32)
 3. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> is_aligned vptr ?sz83
 4. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> 2 ^ 24 - 1 < 2 ^ ?sz83
 5. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + (2 ^ 24 - 1) < 0xE0000000\<rbrakk> \<Longrightarrow> vptr + (2 ^ 24 - 1) >> 20 \<le> 0xDFF proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; x < 0x10; is_aligned vptr 24; vptr + 0xFFFFFF < 0xE0000000\<rbrakk> \<Longrightarrow> vptr + 0xFFFFFF >> 20 \<le> 0xDFF proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; is_aligned vptr 24; x \<le> 0xF; vptr + 0xFFFFFF \<le> 0xDFFFFFFF\<rbrakk> \<Longrightarrow> vptr + 0xFFFFFF >> 20 \<le> 0xDFF proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> 0xDFFFFFFF >> 20 \<le> 0xDFF proof (prove)
goal:
No subgoals!