theory Example_Valid_StateH

lemma cnode_offs_range_correct':
  "\<lbrakk>x \<in> cnode_offs_range ptr; is_aligned ptr 14\<rbrakk>
    \<Longrightarrow> \<exists>y. length y = 10 \<and> (x = ptr + of_bl y * 0x10)" apply (clarsimp simp: cnode_offs_range_def s0_ptr_defs cte_level_bits_def) apply (rule_tac x="to_bl (ucast ((x - ptr) div 0x10):: 10 word)" in exI) apply (clarsimp simp: to_bl_ucast of_bl_drop) apply (subst le_mask_eq) apply simp apply (rule word_div_mult') apply simp apply simp apply (rule word_diff_ls') apply (drule_tac a=x and n=4 in aligned_le_sharp) apply simp 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) apply simp apply (clarsimp simp: neg_mask_is_div[where n=4, simplified, symmetric]) apply (subst is_aligned_neg_mask_eq) apply (rule aligned_sub_aligned) apply assumption apply (erule is_aligned_weaken) apply simp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> cnode_offs_range ptr; is_aligned ptr 14\<rbrakk> \<Longrightarrow> \<exists>y. length y = 10 \<and> x = ptr + of_bl y * 0x10 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> \<exists>y. length y = 10 \<and> x = ptr + of_bl y * 0x10 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> length (to_bl (UCAST(32 \<rightarrow> 10) ((x - ptr) div 0x10))) = 10 \<and> x = ptr + of_bl (to_bl (UCAST(32 \<rightarrow> 10) ((x - ptr) div 0x10))) * 0x10 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + ((x - ptr) div 0x10 && mask 10) * 0x10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> (x - ptr) div 0x10 \<le> 2 ^ 10 - 1
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> (x - ptr) div 0x10 \<le> 0x3FF
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> 0 < 0x10
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x - ptr \<le> 0x3FF * 0x10
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x - ptr \<le> 0x3FF * 0x10
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x - ptr \<le> 0x3FF0
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x \<le> 0x3FF0 + ptr
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> ptr \<le> x
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned x 4
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; is_aligned x 4; x \<le> 0x3FFF + ptr && ~~ mask 4\<rbrakk> \<Longrightarrow> x \<le> 0x3FF0 + ptr
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> ptr \<le> x
 4. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; is_aligned x 4; x \<le> 0x3FFF + ptr && ~~ mask 4\<rbrakk> \<Longrightarrow> x \<le> 0x3FF0 + ptr
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> ptr \<le> x
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; is_aligned x 4; x \<le> ptr + 0x3FFF && ~~ mask 4\<rbrakk> \<Longrightarrow> x \<le> ptr + 0x3FF0
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> ptr \<le> x
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned ptr 4
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; is_aligned x 4; x \<le> ptr + (0x3FFF && ~~ mask 4)\<rbrakk> \<Longrightarrow> x \<le> ptr + 0x3FF0
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> ptr \<le> x
 4. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ptr \<le> x; is_aligned x 4\<rbrakk> \<Longrightarrow> 4 \<le> 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; is_aligned x 4; x \<le> ptr + (0x3FFF && ~~ mask 4)\<rbrakk> \<Longrightarrow> x \<le> ptr + 0x3FF0
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> ptr \<le> x
 4. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; is_aligned x 4; x \<le> ptr + (0x3FFF && ~~ mask 4)\<rbrakk> \<Longrightarrow> x \<le> ptr + 0x3FF0
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> ptr \<le> x
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> ptr \<le> x
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) div 0x10 * 0x10 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && ~~ mask 4) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned (x - ptr) 4
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned x 4
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned ptr 4
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> 4 < LENGTH(32)
 4. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned ptr 4
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> 4 < LENGTH(32)
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> 4 \<le> 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> 4 < LENGTH(32)
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> 4 < LENGTH(32)
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 4\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) proof (prove)
goal:
No subgoals!