theory ArchKernelInit_AI

lemma init_irq_ptrs_ineqs:
  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr"
  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
                \<le> init_irq_node_ptr + 2 ^ 14 - 1" proof - have P: "ucast irq < (2 ^ (14 - cte_level_bits) :: word32)" apply (rule order_le_less_trans[OF
        ucast_le_ucast[where 'a=10 and 'b=32,simplified,THEN iffD2, OF word_n1_ge]]) apply (simp add: cte_level_bits_def minus_one_norm) done show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr" apply (rule is_aligned_no_wrap'[where sz=14]) apply (simp add: is_aligned_def init_irq_node_ptr_def kernel_base_def) apply (rule shiftl_less_t2n[OF P]) apply simp done show Q: "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
                \<le> init_irq_node_ptr + 2 ^ 14 - 1" apply (simp only: add_diff_eq[symmetric] add.assoc) apply (rule word_add_le_mono2) apply (simp only: trans [OF shiftl_t2n mult.commute]) apply (rule nasty_split_lt[OF P]) apply (simp_all add: cte_level_bits_def
        word_bits_def kernel_base_def init_irq_node_ptr_def) done show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
                \<le> init_irq_node_ptr + 2 ^ 14 - 1" apply (simp only: add_diff_eq[symmetric]) apply (rule word_add_le_mono2) apply (rule word_le_minus_one_leq, rule shiftl_less_t2n[OF P]) apply simp apply (simp add: kernel_base_def
      cte_level_bits_def word_bits_def init_irq_node_ptr_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. init_irq_node_ptr \<le> init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 2 ^ cte_level_bits - 1 \<le> init_irq_node_ptr + 2 ^ 14 - 1 &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<le> init_irq_node_ptr + 2 ^ 14 - 1 proof (state)
goal (3 subgoals):
 1. init_irq_node_ptr \<le> init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)
 2. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 2 ^ cte_level_bits - 1 \<le> init_irq_node_ptr + 2 ^ 14 - 1
 3. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<le> init_irq_node_ptr + 2 ^ 14 - 1 proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) irq < 2 ^ (14 - cte_level_bits) proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) (- 1) < 2 ^ (14 - cte_level_bits) proof (prove)
goal:
No subgoals! proof (state)
this:
UCAST(10 \<rightarrow> 32) irq < 2 ^ (14 - cte_level_bits)

goal (3 subgoals):
 1. init_irq_node_ptr \<le> init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)
 2. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 2 ^ cte_level_bits - 1 \<le> init_irq_node_ptr + 2 ^ 14 - 1
 3. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<le> init_irq_node_ptr + 2 ^ 14 - 1 proof (prove)
goal (1 subgoal):
 1. init_irq_node_ptr \<le> init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) proof (prove)
goal (2 subgoals):
 1. is_aligned init_irq_node_ptr 14
 2. UCAST(10 \<rightarrow> 32) irq << cte_level_bits < 2 ^ 14 proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) irq << cte_level_bits < 2 ^ 14 proof (prove)
goal (1 subgoal):
 1. 14 < LENGTH(32) proof (prove)
goal:
No subgoals! proof (state)
this:
init_irq_node_ptr \<le> init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)

goal (2 subgoals):
 1. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 2 ^ cte_level_bits - 1 \<le> init_irq_node_ptr + 2 ^ 14 - 1
 2. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<le> init_irq_node_ptr + 2 ^ 14 - 1 proof (prove)
goal (1 subgoal):
 1. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 2 ^ cte_level_bits - 1 \<le> init_irq_node_ptr + 2 ^ 14 - 1 proof (prove)
goal (1 subgoal):
 1. init_irq_node_ptr + ((UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + (2 ^ cte_level_bits - 1)) \<le> init_irq_node_ptr + (2 ^ 14 - 1) proof (prove)
goal (2 subgoals):
 1. (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + (2 ^ cte_level_bits - 1) \<le> 2 ^ 14 - 1
 2. unat (2 ^ 14 - 1) + unat init_irq_node_ptr < 2 ^ LENGTH(32) proof (prove)
goal (2 subgoals):
 1. UCAST(10 \<rightarrow> 32) irq * 2 ^ cte_level_bits + (2 ^ cte_level_bits - 1) \<le> 2 ^ 14 - 1
 2. unat (2 ^ 14 - 1) + unat init_irq_node_ptr < 2 ^ LENGTH(32) proof (prove)
goal (3 subgoals):
 1. cte_level_bits \<le> 14
 2. 14 < LENGTH(32)
 3. unat (2 ^ 14 - 1) + unat init_irq_node_ptr < 2 ^ LENGTH(32) proof (prove)
goal:
No subgoals! proof (state)
this:
init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 2 ^ cte_level_bits - 1 \<le> init_irq_node_ptr + 2 ^ 14 - 1

goal (1 subgoal):
 1. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<le> init_irq_node_ptr + 2 ^ 14 - 1 proof (prove)
goal (1 subgoal):
 1. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<le> init_irq_node_ptr + 2 ^ 14 - 1 proof (prove)
goal (1 subgoal):
 1. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<le> init_irq_node_ptr + (2 ^ 14 - 1) proof (prove)
goal (2 subgoals):
 1. UCAST(10 \<rightarrow> 32) irq << cte_level_bits \<le> 2 ^ 14 - 1
 2. unat (2 ^ 14 - 1) + unat init_irq_node_ptr < 2 ^ LENGTH(32) proof (prove)
goal (2 subgoals):
 1. 14 < LENGTH(32)
 2. unat (2 ^ 14 - 1) + unat init_irq_node_ptr < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. unat (2 ^ 14 - 1) + unat init_irq_node_ptr < 2 ^ LENGTH(32) proof (prove)
goal:
No subgoals! proof (state)
this:
init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<le> init_irq_node_ptr + 2 ^ 14 - 1

goal:
No subgoals!