theory Arch_R

lemma less_pptrBase_valid_pde_offset':
  "\<lbrakk> vptr < pptrBase; x = 0 \<or> is_aligned vptr 24; x \<le> 0xF \<rbrakk>
     \<Longrightarrow> valid_pde_mapping_offset' (((x * 4) + (vptr >> 20 << 2)) && mask pdBits)" apply (clarsimp simp: pptrBase_def pdBits_def pageBits_def
                        valid_pde_mapping_offset'_def pd_asid_slot_def) apply (drule word_le_minus_one_leq, simp add: pdeBits_def) apply (drule le_shiftr[where u=vptr and n=20]) apply (subst(asm) iffD2[OF mask_eq_iff_w2p]) apply (simp add: word_size) apply (simp add: shiftl_t2n unat_arith_simps iffD1[OF unat_mult_lem]) apply (erule disjE) apply (simp add: shiftl_t2n unat_arith_simps iffD1[OF unat_mult_lem]) apply (frule arg_cong[where f="\<lambda>v. v && mask 6"]) apply (subst(asm) field_simps, subst(asm) is_aligned_add_helper[where n=6],
         rule is_aligned_shiftl) apply (rule is_aligned_shiftr, simp) apply (simp add: unat_arith_simps iffD1[OF unat_mult_lem]) apply (simp add: mask_def[where n=6]) apply (simp add: shiftl_t2n unat_arith_simps iffD1[OF unat_mult_lem]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < pptrBase; x = 0 \<or> is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' (x * 4 + (vptr >> 20 << 2) && mask pdBits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < 0xE0000000; x = 0 \<or> is_aligned vptr 24; x \<le> 0xF; x * 4 + (vptr >> 20 << 2) && mask (12 + pdeBits) = 0x3FC0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 0 \<or> is_aligned vptr 24; x \<le> 0xF; x * 4 + (vptr >> 20 << 2) && mask 14 = 0x3FC0; vptr \<le> 0xDFFFFFFF\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 0 \<or> is_aligned vptr 24; x \<le> 0xF; x * 4 + (vptr >> 20 << 2) && mask 14 = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vptr >> 20 \<le> 0xDFFFFFFF >> 20; x = 0 \<or> is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> 14 < size (x * 4 + (vptr >> 20 << 2))
 2. \<lbrakk>vptr >> 20 \<le> 0xDFFFFFFF >> 20; x = 0 \<or> is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> x * 4 + (vptr >> 20 << 2) < 2 ^ 14
 3. \<lbrakk>x = 0 \<or> is_aligned vptr 24; x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vptr >> 20 \<le> 0xDFFFFFFF >> 20; x = 0 \<or> is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> x * 4 + (vptr >> 20 << 2) < 2 ^ 14
 2. \<lbrakk>x = 0 \<or> is_aligned vptr 24; x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 0 \<or> is_aligned vptr 24; x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20; x = 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20; is_aligned vptr 24\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20; is_aligned vptr 24\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20; is_aligned vptr 24; x * 4 + (vptr >> 20 << 2) && mask 6 = 0x3FC0 && mask 6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20; is_aligned vptr 24\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 20) (6 - 2)
 2. \<lbrakk>x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20; is_aligned vptr 24\<rbrakk> \<Longrightarrow> x * 4 < 2 ^ 6
 3. \<lbrakk>x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20; is_aligned vptr 24; x * 4 = 0x3FC0 && mask 6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20; is_aligned vptr 24\<rbrakk> \<Longrightarrow> x * 4 < 2 ^ 6
 2. \<lbrakk>x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20; is_aligned vptr 24; x * 4 = 0x3FC0 && mask 6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> 0xF; x * 4 + (vptr >> 20 << 2) = 0x3FC0; vptr >> 20 \<le> 0xDFFFFFFF >> 20; is_aligned vptr 24; x * 4 = 0x3FC0 && mask 6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> 0xF; vptr >> 20 << 2 = 0x3FC0; vptr >> 20 \<le> 0xDFF; is_aligned vptr 24; x * 4 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!