theory Example_Valid_StateH

lemma pt_offs_range_correct':
  "\<lbrakk>x \<in> pt_offs_range ptr; is_aligned ptr 10\<rbrakk>
    \<Longrightarrow> \<exists>y. x = ptr + (ucast (y:: 8 word) << 2)" apply (clarsimp simp: pt_offs_range_def s0_ptr_defs cte_level_bits_def) apply (rule_tac x="ucast ((x - ptr) >> 2)" in exI) apply (clarsimp simp: ucast_ucast_mask) apply (subst aligned_shiftr_mask_shiftl) apply (rule aligned_sub_aligned) apply assumption apply (erule is_aligned_weaken) apply simp apply simp apply simp apply (rule_tac n=10 in mask_eqI) apply (subst mask_add_aligned) apply (simp add: is_aligned_def) apply (simp add: mask_twice) apply (subst diff_conv_add_uminus) apply (subst add.commute[symmetric]) apply (subst mask_add_aligned) apply (simp add: is_aligned_minus) apply simp apply (subst diff_conv_add_uminus) apply (subst add_mask_lower_bits) apply (simp add: is_aligned_def) apply clarsimp apply (cut_tac x=x and y="ptr + 0x3FF" and n=10 in neg_mask_mono_le) apply (simp add: add.commute) apply (drule_tac n=10 in aligned_le_sharp) apply (simp add: is_aligned_def) apply (simp add: add.commute) apply (subst(asm) mask_out_add_aligned[symmetric]) apply (erule is_aligned_weaken) apply simp apply (simp add: mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> pt_offs_range ptr; is_aligned ptr 10\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + (UCAST(8 \<rightarrow> 32) y << 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + (UCAST(8 \<rightarrow> 32) y << 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (x - ptr >> 2)) << 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + ((x - ptr >> 2) && mask 8 << 2) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned (x - ptr) 2
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (8 + 2)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned ptr 2
 3. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 4. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (8 + 2)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned ptr 2
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 3. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (8 + 2)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> 2 \<le> 10
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 3. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (8 + 2)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (8 + 2)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (8 + 2)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask 10) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 10 = ptr + (x - ptr && mask 10) && mask 10
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr + (x - ptr && mask 10) && ~~ mask 10 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned ptr 10
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 10 = (x - ptr && mask 10) && mask 10
 3. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr + (x - ptr && mask 10) && ~~ mask 10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 10 = (x - ptr && mask 10) && mask 10
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr + (x - ptr && mask 10) && ~~ mask 10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 10 = x - ptr && mask 10
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr + (x - ptr && mask 10) && ~~ mask 10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 10 = x + - ptr && mask 10
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr + (x - ptr && mask 10) && ~~ mask 10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 10 = - ptr + x && mask 10
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr + (x - ptr && mask 10) && ~~ mask 10 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned (- ptr) 10
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 10 = x && mask 10
 3. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr + (x - ptr && mask 10) && ~~ mask 10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 10 = x && mask 10
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr + (x - ptr && mask 10) && ~~ mask 10 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr + (x - ptr && mask 10) && ~~ mask 10 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr + (x + - ptr && mask 10) && ~~ mask 10 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned ptr 10
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>10. n' < LENGTH(32) \<longrightarrow> \<not> (x + - ptr && mask 10) !! n'
 3. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>10. n' < LENGTH(32) \<longrightarrow> \<not> (x + - ptr && mask 10) !! n'
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x \<le> ptr + 0x3FF
 2. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2; x && ~~ mask 10 \<le> ptr + 0x3FF && ~~ mask 10\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; ptr \<le> x; x \<le> 0x3FF + ptr; is_aligned x 2; x && ~~ mask 10 \<le> ptr + 0x3FF && ~~ mask 10\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 10; x \<le> 0x3FF + ptr; is_aligned x 2; x && ~~ mask 10 \<le> ptr + 0x3FF && ~~ mask 10\<rbrakk> \<Longrightarrow> is_aligned ptr 10
 2. \<lbrakk>is_aligned ptr 10; x \<le> 0x3FF + ptr; is_aligned x 2; x && ~~ mask 10 \<le> ptr + 0x3FF && ~~ mask 10; ptr \<le> x && ~~ mask 10\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; x \<le> 0x3FF + ptr; is_aligned x 2; x && ~~ mask 10 \<le> ptr + 0x3FF && ~~ mask 10; ptr \<le> x && ~~ mask 10\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; x \<le> ptr + 0x3FF; is_aligned x 2; x && ~~ mask 10 \<le> ptr + 0x3FF && ~~ mask 10; ptr \<le> x && ~~ mask 10\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<le> x && ~~ mask 10; is_aligned ptr 10; x \<le> ptr + 0x3FF; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned ptr 10
 2. \<lbrakk>is_aligned ptr 10; x \<le> ptr + 0x3FF; is_aligned x 2; x && ~~ mask 10 \<le> ptr + (0x3FF && ~~ mask 10); ptr \<le> x && ~~ mask 10\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<le> x && ~~ mask 10; x \<le> ptr + 0x3FF; is_aligned x 2\<rbrakk> \<Longrightarrow> 10 \<le> 10
 2. \<lbrakk>is_aligned ptr 10; x \<le> ptr + 0x3FF; is_aligned x 2; x && ~~ mask 10 \<le> ptr + (0x3FF && ~~ mask 10); ptr \<le> x && ~~ mask 10\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 10; x \<le> ptr + 0x3FF; is_aligned x 2; x && ~~ mask 10 \<le> ptr + (0x3FF && ~~ mask 10); ptr \<le> x && ~~ mask 10\<rbrakk> \<Longrightarrow> x && ~~ mask 10 = ptr proof (prove)
goal:
No subgoals!