theory Example_Valid_State

lemma irq_node_offs_range_correct:
  "x \<in> irq_node_offs_range
    \<Longrightarrow> \<exists>irq. x = init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits)" apply (clarsimp simp: irq_node_offs_min irq_node_offs_max irq_node_offs_range_def
                        s0_ptr_defs cte_level_bits_def) apply (rule_tac x="ucast ((x - 0xE0008000) >> 4)" in exI) apply (clarsimp simp: ucast_ucast_mask) apply (subst aligned_shiftr_mask_shiftl) apply (rule aligned_sub_aligned) apply assumption apply (simp add: is_aligned_def) apply simp apply simp apply (rule_tac n=14 in mask_eqI) apply (subst mask_add_aligned) apply (simp add: is_aligned_def) apply (simp add: mask_twice) apply (simp add: diff_conv_add_uminus del: add_uminus_conv_diff) apply (subst add.commute[symmetric]) apply (subst mask_add_aligned) apply (simp add: is_aligned_def) apply simp apply (simp add: diff_conv_add_uminus del: add_uminus_conv_diff) apply (subst add_mask_lower_bits) apply (simp add: is_aligned_def) apply clarsimp apply (cut_tac x=x and y="0xE000BFFF" and n=14 in neg_mask_mono_le) apply (force dest: word_less_sub_1) apply (drule_tac n=14 in aligned_le_sharp) apply (simp add: is_aligned_def) apply (simp add: mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> irq_node_offs_range \<Longrightarrow> \<exists>irq. x = init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> \<exists>irq. x = 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x = 0xE0008000 + (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (x - 0xE0008000 >> 4)) << 4) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x = 0xE0008000 + ((x - 0xE0008000 >> 4) && mask 10 << 4) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned (x - 0xE0008000) 4
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x = 0xE0008000 + (x - 0xE0008000 && mask (10 + 4)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned x 4
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned 0xE0008000 4
 3. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> 4 < LENGTH(32)
 4. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x = 0xE0008000 + (x - 0xE0008000 && mask (10 + 4)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned 0xE0008000 4
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> 4 < LENGTH(32)
 3. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x = 0xE0008000 + (x - 0xE0008000 && mask (10 + 4)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> 4 < LENGTH(32)
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x = 0xE0008000 + (x - 0xE0008000 && mask (10 + 4)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x = 0xE0008000 + (x - 0xE0008000 && mask (10 + 4)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x = 0xE0008000 + (x - 0xE0008000 && mask 14) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && mask 14 = 0xE0008000 + (x - 0xE0008000 && mask 14) && mask 14
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 + (x - 0xE0008000 && mask 14) && ~~ mask 14 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned 0xE0008000 14
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && mask 14 = (x - 0xE0008000 && mask 14) && mask 14
 3. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 + (x - 0xE0008000 && mask 14) && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && mask 14 = (x - 0xE0008000 && mask 14) && mask 14
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 + (x - 0xE0008000 && mask 14) && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && mask 14 = x - 0xE0008000 && mask 14
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 + (x - 0xE0008000 && mask 14) && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && mask 14 = x + 0x1FFF8000 && mask 14
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 + (x - 0xE0008000 && mask 14) && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && mask 14 = 0x1FFF8000 + x && mask 14
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 + (x - 0xE0008000 && mask 14) && ~~ mask 14 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned 0x1FFF8000 14
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && mask 14 = x && mask 14
 3. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 + (x - 0xE0008000 && mask 14) && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && mask 14 = x && mask 14
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 + (x - 0xE0008000 && mask 14) && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 + (x - 0xE0008000 && mask 14) && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 + (x + 0x1FFF8000 && mask 14) && ~~ mask 14 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> is_aligned 0xE0008000 14
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>14. n' < LENGTH(32) \<longrightarrow> \<not> (x + 0x1FFF8000 && mask 14) !! n'
 3. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>14. n' < LENGTH(32) \<longrightarrow> \<not> (x + 0x1FFF8000 && mask 14) !! n'
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x \<le> 0xE000BFFF
 2. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4; x && ~~ mask 14 \<le> 0xE000BFFF && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4; x && ~~ mask 14 \<le> 0xE000BFFF && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 0xE000C000; is_aligned x 4; x && ~~ mask 14 \<le> 0xE000BFFF && ~~ mask 14\<rbrakk> \<Longrightarrow> is_aligned 0xE0008000 14
 2. \<lbrakk>x < 0xE000C000; is_aligned x 4; x && ~~ mask 14 \<le> 0xE000BFFF && ~~ mask 14; 0xE0008000 \<le> x && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 0xE000C000; is_aligned x 4; x && ~~ mask 14 \<le> 0xE000BFFF && ~~ mask 14; 0xE0008000 \<le> x && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = 0xE0008000 proof (prove)
goal:
No subgoals!