theory Example_Valid_State

lemma valid_irq_node_s0[simp]:
  "valid_irq_node s0_internal" apply (clarsimp simp: valid_irq_node_def) apply (rule conjI) apply (simp add: s0_internal_def) apply (rule injI) apply simp apply (rule ccontr) apply (rule_tac bnd="0x400" and 'a=32 in shift_distinct_helper[rotated 3]) apply assumption apply (simp add: cte_level_bits_def) apply (simp add: cte_level_bits_def) apply (rule ucast_less[where 'b=10, simplified]) apply simp apply (rule ucast_less[where 'b=10, simplified]) apply simp apply (rule notI) apply (drule ucast_up_inj) apply simp apply simp apply (clarsimp simp: obj_at_def s0_internal_def) apply (force simp: kh0_def is_cap_table_def well_formed_cnode_n_def dom_empty_cnode) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_node s0_internal proof (prove)
goal (1 subgoal):
 1. inj (interrupt_irq_node s0_internal) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal) proof (prove)
goal (2 subgoals):
 1. inj (interrupt_irq_node s0_internal)
 2. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (2 subgoals):
 1. inj (\<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits))
 2. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (2 subgoals):
 1. \<And>x y. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) x << cte_level_bits) = init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) y << cte_level_bits) \<Longrightarrow> x = y
 2. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (2 subgoals):
 1. \<And>x y. UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits \<Longrightarrow> x = y
 2. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> False
 2. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> ?x7 x y << ?n7 x y = ?y7 x y << ?n7 x y
 2. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> ?n7 x y < LENGTH(32)
 3. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> 0x400 - 1 \<le> 2 ^ (LENGTH(32) - ?n7 x y) - 1
 4. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> ?x7 x y < 0x400
 5. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> ?y7 x y < 0x400
 6. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> ?x7 x y \<noteq> ?y7 x y
 7. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (6 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> cte_level_bits < LENGTH(32)
 2. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> 0x400 - 1 \<le> 2 ^ (LENGTH(32) - cte_level_bits) - 1
 3. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x < 0x400
 4. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) y < 0x400
 5. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x \<noteq> UCAST(10 \<rightarrow> 32) y
 6. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> 0x400 - 1 \<le> 2 ^ (LENGTH(32) - cte_level_bits) - 1
 2. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x < 0x400
 3. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) y < 0x400
 4. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x \<noteq> UCAST(10 \<rightarrow> 32) y
 5. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x < 0x400
 2. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) y < 0x400
 3. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x \<noteq> UCAST(10 \<rightarrow> 32) y
 4. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 2. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) y < 0x400
 3. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x \<noteq> UCAST(10 \<rightarrow> 32) y
 4. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) y < 0x400
 2. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x \<noteq> UCAST(10 \<rightarrow> 32) y
 3. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 2. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x \<noteq> UCAST(10 \<rightarrow> 32) y
 3. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x \<noteq> UCAST(10 \<rightarrow> 32) y
 2. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y; UCAST(10 \<rightarrow> 32) x = UCAST(10 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> False
 2. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y\<rbrakk> \<Longrightarrow> LENGTH(10) \<le> LENGTH(32)
 2. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y; x = y\<rbrakk> \<Longrightarrow> False
 3. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>UCAST(10 \<rightarrow> 32) x << cte_level_bits = UCAST(10 \<rightarrow> 32) y << cte_level_bits; x \<noteq> y; x = y\<rbrakk> \<Longrightarrow> False
 2. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (1 subgoal):
 1. \<forall>irq. cap_table_at 0 (interrupt_irq_node s0_internal irq) s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>irq. \<exists>ko. kh0 (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) = Some ko \<and> is_cap_table 0 ko proof (prove)
goal:
No subgoals!