theory Example_Valid_StateH

lemma s0_pspace_rel:
  "pspace_relation (kheap s0_internal) kh0H" apply (simp add: pspace_relation_def s0_internal_def s0H_internal_def kh0H_dom kh0_pspace_dom) apply clarsimp apply (drule kh0_SomeD) apply (rename_tac y) apply (elim disjE) apply (clarsimp simp: pageBits_def) apply (clarsimp simp: kh0H_obj_def split del: if_split) apply (cut_tac x=y in pd_offs_in_range(3)) apply (clarsimp simp: pd_offs_range_def pde_relation_def pde_relation_aligned_def) apply (clarsimp simp: kh0H_all_obj_def kh0_obj_def other_obj_relation_def
                                    tcb_relation_def arch_tcb_relation_def fault_rel_optionation_def
                                    word_bits_def the_nat_to_bl_simps)+ apply (clarsimp simp: kh0H_obj_def High_pt_def High_pt'H_def High_pt'_def split del: if_split) apply (cut_tac x=y in pt_offs_in_range(2)) apply (clarsimp simp: pt_offs_range_def pte_relation_def pte_relation_aligned_def pte_relation'_def) apply (clarsimp simp: kh0H_obj_def Low_pt_def Low_pt'H_def Low_pt'_def split del: if_split) apply (cut_tac x=y in pt_offs_in_range(1)) apply (clarsimp simp: pt_offs_range_def pte_relation_def pte_relation_aligned_def pte_relation'_def) apply (clarsimp simp: kh0H_obj_def High_pd_def High_pd'H_def High_pd'_def split del: if_split) apply (cut_tac x=y in pd_offs_in_range(2)) apply (clarsimp simp: pd_offs_range_def pde_relation_def pde_relation_aligned_def pde_relation'_def) apply (clarsimp simp: kh0H_obj_def Low_pd_def Low_pd'H_def Low_pd'_def split del: if_split) apply (cut_tac x=y in pd_offs_in_range(1)) apply (clarsimp simp: pd_offs_range_def pde_relation_def pde_relation_aligned_def pde_relation'_def) apply (clarsimp simp: kh0H_obj_def irq_cnode_def cte_map_def cte_relation_def well_formed_cnode_n_def split: if_split_asm) apply (clarsimp simp: kh0H_obj_def kh0_obj_def other_obj_relation_def ntfn_relation_def) apply (clarsimp simp: kh0H_obj_def kh0_obj_def cte_relation_def cte_map_def) apply (cut_tac dom_caps(1))[1] apply (frule_tac m="Silc_caps" in domI) apply (cut_tac x=y in cnode_offs_in_range(3)) apply simp apply (clarsimp simp: cnode_offs_range_def Silc_cte_def Silc_cte'_def Silc_capsH_def the_nat_to_bl_simps Silc_caps_def cte_level_bits_def empty_cte_def split: if_split_asm) apply (clarsimp simp: kh0H_obj_def kh0_obj_def cte_relation_def cte_map_def) apply (cut_tac dom_caps(2))[1] apply (frule_tac m="High_caps" in domI) apply (cut_tac x=y in cnode_offs_in_range(2)) apply simp apply (clarsimp simp: cnode_offs_range_def High_cte_def High_cte'_def High_capsH_def the_nat_to_bl_simps High_caps_def cte_level_bits_def empty_cte_def split: if_split_asm) apply (clarsimp simp: kh0H_obj_def kh0_obj_def cte_relation_def cte_map_def) apply (cut_tac dom_caps(3))[1] apply (frule_tac m="Low_caps" in domI) apply (cut_tac x=y in cnode_offs_in_range(1)) apply simp apply (clarsimp simp: cnode_offs_range_def Low_cte_def Low_cte'_def Low_capsH_def the_nat_to_bl_simps Low_caps_def cte_level_bits_def empty_cte_def split: if_split_asm) apply (clarsimp simp: kh0H_obj_def irq_cnode_def cte_map_def cte_relation_def well_formed_cnode_n_def empty_cte_def dom_def split: if_split_asm) apply (drule irq_node_offs_range_correct) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_relation (kheap s0_internal) kh0H proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom kh0. \<forall>(y, P)\<in>obj_relation_cuts (the (kh0 x)) x. P (the (kh0 x)) (the (kh0H y)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; kh0 x = Some y\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = init_globals_frame \<and> y = ArchObj (DataPage False ARMSmallPage) \<or> x = init_global_pd \<and> y = ArchObj (PageDirectory global_pd) \<or> x = idle_tcb_ptr \<and> y = idle_tcb \<or> x = High_tcb_ptr \<and> y = High_tcb \<or> x = Low_tcb_ptr \<and> y = Low_tcb \<or> x = High_pt_ptr \<and> y = High_pt \<or> x = Low_pt_ptr \<and> y = Low_pt \<or> x = High_pd_ptr \<and> y = High_pd \<or> x = Low_pd_ptr \<and> y = Low_pd \<or> x = irq_cnode_ptr \<and> y = irq_cnode \<or> x = ntfn_ptr \<and> y = ntfn \<or> x = Silc_cnode_ptr \<and> y = Silc_cnode \<or> x = High_cnode_ptr \<and> y = High_cnode \<or> x = Low_cnode_ptr \<and> y = Low_cnode \<or> x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = init_globals_frame \<and> y = ArchObj (DataPage False ARMSmallPage) \<or> x = init_global_pd \<and> y = ArchObj (PageDirectory global_pd) \<or> x = idle_tcb_ptr \<and> y = idle_tcb \<or> x = High_tcb_ptr \<and> y = High_tcb \<or> x = Low_tcb_ptr \<and> y = Low_tcb \<or> x = High_pt_ptr \<and> y = High_pt \<or> x = Low_pt_ptr \<and> y = Low_pt \<or> x = High_pd_ptr \<and> y = High_pd \<or> x = Low_pd_ptr \<and> y = Low_pd \<or> x = irq_cnode_ptr \<and> y = irq_cnode \<or> x = ntfn_ptr \<and> y = ntfn \<or> x = Silc_cnode_ptr \<and> y = Silc_cnode \<or> x = High_cnode_ptr \<and> y = High_cnode \<or> x = Low_cnode_ptr \<and> y = Low_cnode \<or> x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (15 subgoals):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = init_globals_frame \<and> y = ArchObj (DataPage False ARMSmallPage)\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = init_global_pd \<and> y = ArchObj (PageDirectory global_pd)\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = idle_tcb_ptr \<and> y = idle_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_tcb_ptr \<and> y = High_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_tcb_ptr \<and> y = Low_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pt_ptr \<and> y = High_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pt_ptr \<and> y = Low_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 9. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 10. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = init_global_pd \<and> y = ArchObj (PageDirectory global_pd)\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = idle_tcb_ptr \<and> y = idle_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_tcb_ptr \<and> y = High_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_tcb_ptr \<and> y = Low_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pt_ptr \<and> y = High_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pt_ptr \<and> y = Low_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 9. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 10. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>y. pde_relation y (ArchObj (PageDirectory ((\<lambda>_. ARM_A.InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := ARM_A.SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) (the (map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned (init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2)) 2 \<and> init_global_pd \<le> init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<and> init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) - init_global_pd >> 2)) else None)))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = idle_tcb_ptr \<and> y = idle_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_tcb_ptr \<and> y = High_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_tcb_ptr \<and> y = Low_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pt_ptr \<and> y = High_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pt_ptr \<and> y = Low_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 9. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 10. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>y. init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<in> pd_offs_range init_global_pd \<Longrightarrow> pde_relation y (ArchObj (PageDirectory ((\<lambda>_. ARM_A.InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := ARM_A.SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) (the (map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned (init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2)) 2 \<and> init_global_pd \<le> init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<and> init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) - init_global_pd >> 2)) else None)))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = idle_tcb_ptr \<and> y = idle_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_tcb_ptr \<and> y = High_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_tcb_ptr \<and> y = Low_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pt_ptr \<and> y = High_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pt_ptr \<and> y = Low_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 9. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 10. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = idle_tcb_ptr \<and> y = idle_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_tcb_ptr \<and> y = High_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_tcb_ptr \<and> y = Low_tcb\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pt_ptr \<and> y = High_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pt_ptr \<and> y = Low_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 9. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 10. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
A total of 13 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>y. (is_aligned (High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2)) 2 \<and> High_pt_ptr \<le> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<and> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<le> 0x3FF + High_pt_ptr \<longrightarrow> pte_relation y (ArchObj (PageTable High_pt')) (KOArch (KOPTE (High_pt'H y)))) \<and> ((High_pt_ptr \<le> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<longrightarrow> is_aligned (High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2)) 2 \<longrightarrow> \<not> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<le> 0x3FF + High_pt_ptr) \<longrightarrow> pte_relation y (ArchObj (PageTable High_pt')) (the None))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pt_ptr \<and> y = Low_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 9. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 10. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (10 subgoals):
 1. \<And>y. (is_aligned (High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2)) 2 \<and> High_pt_ptr \<le> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<and> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<le> 0x3FF + High_pt_ptr \<longrightarrow> pte_relation y (ArchObj (PageTable ((\<lambda>_. ARM_A.InvalidPTE)(0 := ARM_A.SmallPagePTE shared_page_ptr_phys {} vm_read_only)))) (KOArch (KOPTE (if y = 0 then ARM_H.SmallPagePTE shared_page_ptr_phys False False False (vmrights_map vm_read_only) else ARM_H.InvalidPTE)))) \<and> ((High_pt_ptr \<le> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<longrightarrow> is_aligned (High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2)) 2 \<longrightarrow> \<not> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<le> 0x3FF + High_pt_ptr) \<longrightarrow> pte_relation y (ArchObj (PageTable ((\<lambda>_. ARM_A.InvalidPTE)(0 := ARM_A.SmallPagePTE shared_page_ptr_phys {} vm_read_only)))) (the None))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pt_ptr \<and> y = Low_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 9. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 10. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (10 subgoals):
 1. \<And>y. High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<in> pt_offs_range High_pt_ptr \<Longrightarrow> (is_aligned (High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2)) 2 \<and> High_pt_ptr \<le> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<and> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<le> 0x3FF + High_pt_ptr \<longrightarrow> pte_relation y (ArchObj (PageTable ((\<lambda>_. ARM_A.InvalidPTE)(0 := ARM_A.SmallPagePTE shared_page_ptr_phys {} vm_read_only)))) (KOArch (KOPTE (if y = 0 then ARM_H.SmallPagePTE shared_page_ptr_phys False False False (vmrights_map vm_read_only) else ARM_H.InvalidPTE)))) \<and> ((High_pt_ptr \<le> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<longrightarrow> is_aligned (High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2)) 2 \<longrightarrow> \<not> High_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<le> 0x3FF + High_pt_ptr) \<longrightarrow> pte_relation y (ArchObj (PageTable ((\<lambda>_. ARM_A.InvalidPTE)(0 := ARM_A.SmallPagePTE shared_page_ptr_phys {} vm_read_only)))) (the None))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pt_ptr \<and> y = Low_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 9. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 10. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (9 subgoals):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pt_ptr \<and> y = Low_pt\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 9. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (9 subgoals):
 1. \<And>y. pte_relation y (ArchObj (PageTable ((\<lambda>_. ARM_A.InvalidPTE)(0 := ARM_A.SmallPagePTE shared_page_ptr_phys {} vm_read_write)))) (the (map_option (\<lambda>x. KOArch (KOPTE (if x = 0 then ARM_H.SmallPagePTE shared_page_ptr_phys False False False (vmrights_map vm_read_write) else ARM_H.InvalidPTE))) (if is_aligned (Low_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2)) 2 \<and> Low_pt_ptr \<le> Low_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<and> Low_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (Low_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) - Low_pt_ptr >> 2)) else None)))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 9. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (9 subgoals):
 1. \<And>y. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<in> pt_offs_range Low_pt_ptr \<Longrightarrow> pte_relation y (ArchObj (PageTable ((\<lambda>_. ARM_A.InvalidPTE)(0 := ARM_A.SmallPagePTE shared_page_ptr_phys {} vm_read_write)))) (the (map_option (\<lambda>x. KOArch (KOPTE (if x = 0 then ARM_H.SmallPagePTE shared_page_ptr_phys False False False (vmrights_map vm_read_write) else ARM_H.InvalidPTE))) (if is_aligned (Low_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2)) 2 \<and> Low_pt_ptr \<le> Low_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<and> Low_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (Low_pt_ptr + (UCAST(8 \<rightarrow> 32) y << 2) - Low_pt_ptr >> 2)) else None)))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 9. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (8 subgoals):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_pd_ptr \<and> y = High_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (8 subgoals):
 1. \<And>y. pde_relation y (ArchObj (PageDirectory ((\<lambda>_. ARM_A.InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := ARM_A.SectionPDE (addrFromPPtr kernel_base) {} 0 {}, 0 := ARM_A.PageTablePDE (addrFromPPtr High_pt_ptr) {} undefined)))) (the (map_option (\<lambda>x. KOArch (KOPDE (if x = 0 then ARM_H.PageTablePDE (addrFromPPtr High_pt_ptr) False undefined else ((\<lambda>_. ARM_H.InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}))) x))) (if is_aligned (High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) 2 \<and> High_pd_ptr \<le> High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<and> High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) - High_pd_ptr >> 2)) else None)))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (8 subgoals):
 1. \<And>y. High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<in> pd_offs_range High_pd_ptr \<Longrightarrow> pde_relation y (ArchObj (PageDirectory ((\<lambda>_. ARM_A.InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := ARM_A.SectionPDE (addrFromPPtr kernel_base) {} 0 {}, 0 := ARM_A.PageTablePDE (addrFromPPtr High_pt_ptr) {} undefined)))) (the (map_option (\<lambda>x. KOArch (KOPDE (if x = 0 then ARM_H.PageTablePDE (addrFromPPtr High_pt_ptr) False undefined else ((\<lambda>_. ARM_H.InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}))) x))) (if is_aligned (High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) 2 \<and> High_pd_ptr \<le> High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<and> High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) - High_pd_ptr >> 2)) else None)))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 8. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (7 subgoals):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_pd_ptr \<and> y = Low_pd\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (7 subgoals):
 1. \<And>y. pde_relation y (ArchObj (PageDirectory ((\<lambda>_. ARM_A.InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := ARM_A.SectionPDE (addrFromPPtr kernel_base) {} 0 {}, 0 := ARM_A.PageTablePDE (addrFromPPtr Low_pt_ptr) {} undefined)))) (the (map_option (\<lambda>x. KOArch (KOPDE (if x = 0 then ARM_H.PageTablePDE (addrFromPPtr Low_pt_ptr) False undefined else ((\<lambda>_. ARM_H.InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}))) x))) (if is_aligned (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) 2 \<and> Low_pd_ptr \<le> Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<and> Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) - Low_pd_ptr >> 2)) else None)))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (7 subgoals):
 1. \<And>y. Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<in> pd_offs_range Low_pd_ptr \<Longrightarrow> pde_relation y (ArchObj (PageDirectory ((\<lambda>_. ARM_A.InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := ARM_A.SectionPDE (addrFromPPtr kernel_base) {} 0 {}, 0 := ARM_A.PageTablePDE (addrFromPPtr Low_pt_ptr) {} undefined)))) (the (map_option (\<lambda>x. KOArch (KOPDE (if x = 0 then ARM_H.PageTablePDE (addrFromPPtr Low_pt_ptr) False undefined else ((\<lambda>_. ARM_H.InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}))) x))) (if is_aligned (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2)) 2 \<and> Low_pd_ptr \<le> Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<and> Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) - Low_pd_ptr >> 2)) else None)))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 7. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (6 subgoals):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = irq_cnode_ptr \<and> y = irq_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 6. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (5 subgoals):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = ntfn_ptr \<and> y = ntfn\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (4 subgoals):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Silc_cnode_ptr \<and> y = Silc_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (4 subgoals):
 1. \<And>y ya. Silc_caps y = Some ya \<Longrightarrow> \<exists>cte. the (kh0H (Silc_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (4 subgoals):
 1. \<And>y ya. \<lbrakk>Silc_caps y = Some ya; dom Silc_caps = {x. length x = 10}\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (Silc_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (4 subgoals):
 1. \<And>y ya. \<lbrakk>Silc_caps y = Some ya; dom Silc_caps = {x. length x = 10}; y \<in> dom Silc_caps\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (Silc_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (5 subgoals):
 1. \<And>y ya. \<lbrakk>Silc_caps y = Some ya; dom Silc_caps = {x. length x = 10}; y \<in> dom Silc_caps\<rbrakk> \<Longrightarrow> length y = 10
 2. \<And>y ya. \<lbrakk>Silc_caps y = Some ya; dom Silc_caps = {x. length x = 10}; y \<in> dom Silc_caps; Silc_cnode_ptr + of_bl y * 0x10 \<in> cnode_offs_range Silc_cnode_ptr\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (Silc_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 5. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (4 subgoals):
 1. \<And>y ya. \<lbrakk>Silc_caps y = Some ya; dom Silc_caps = {x. length x = 10}; y \<in> dom Silc_caps; Silc_cnode_ptr + of_bl y * 0x10 \<in> cnode_offs_range Silc_cnode_ptr\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (Silc_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (3 subgoals):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = High_cnode_ptr \<and> y = High_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (3 subgoals):
 1. \<And>y ya. High_caps y = Some ya \<Longrightarrow> \<exists>cte. the (kh0H (High_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (3 subgoals):
 1. \<And>y ya. \<lbrakk>High_caps y = Some ya; dom High_caps = {x. length x = 10}\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (High_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (3 subgoals):
 1. \<And>y ya. \<lbrakk>High_caps y = Some ya; dom High_caps = {x. length x = 10}; y \<in> dom High_caps\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (High_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (4 subgoals):
 1. \<And>y ya. \<lbrakk>High_caps y = Some ya; dom High_caps = {x. length x = 10}; y \<in> dom High_caps\<rbrakk> \<Longrightarrow> length y = 10
 2. \<And>y ya. \<lbrakk>High_caps y = Some ya; dom High_caps = {x. length x = 10}; y \<in> dom High_caps; High_cnode_ptr + of_bl y * 0x10 \<in> cnode_offs_range High_cnode_ptr\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (High_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 4. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (3 subgoals):
 1. \<And>y ya. \<lbrakk>High_caps y = Some ya; dom High_caps = {x. length x = 10}; y \<in> dom High_caps; High_cnode_ptr + of_bl y * 0x10 \<in> cnode_offs_range High_cnode_ptr\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (High_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x = Low_cnode_ptr \<and> y = Low_cnode\<rbrakk> \<Longrightarrow> b y (the (kh0H a))
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (2 subgoals):
 1. \<And>y ya. Low_caps y = Some ya \<Longrightarrow> \<exists>cte. the (kh0H (Low_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (2 subgoals):
 1. \<And>y ya. \<lbrakk>Low_caps y = Some ya; dom Low_caps = {x. length x = 10}\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (Low_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (2 subgoals):
 1. \<And>y ya. \<lbrakk>Low_caps y = Some ya; dom Low_caps = {x. length x = 10}; y \<in> dom Low_caps\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (Low_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (3 subgoals):
 1. \<And>y ya. \<lbrakk>Low_caps y = Some ya; dom Low_caps = {x. length x = 10}; y \<in> dom Low_caps\<rbrakk> \<Longrightarrow> length y = 10
 2. \<And>y ya. \<lbrakk>Low_caps y = Some ya; dom Low_caps = {x. length x = 10}; y \<in> dom Low_caps; Low_cnode_ptr + of_bl y * 0x10 \<in> cnode_offs_range Low_cnode_ptr\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (Low_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 3. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (2 subgoals):
 1. \<And>y ya. \<lbrakk>Low_caps y = Some ya; dom Low_caps = {x. length x = 10}; y \<in> dom Low_caps; Low_cnode_ptr + of_bl y * 0x10 \<in> cnode_offs_range Low_cnode_ptr\<rbrakk> \<Longrightarrow> \<exists>cte. the (kh0H (Low_cnode_ptr + of_bl y * 2 ^ cte_level_bits)) = KOCTE cte \<and> cap_relation ya (cteCap cte)
 2. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> b y (the (kh0H a)) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> irq_node_offs_range \<Longrightarrow> \<exists>cte. the (kh0H x) = KOCTE cte \<and> cteCap cte = capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>irq. x = init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<Longrightarrow> \<exists>cte. the (kh0H x) = KOCTE cte \<and> cteCap cte = capability.NullCap proof (prove)
goal:
No subgoals!