theory ArchKernelInit_AI

lemma invs_A:
  "invs init_A_st" apply (simp add: invs_def) apply (rule conjI) prefer 2 apply (simp add: cur_tcb_def state_defs obj_at_def) apply (simp add: valid_state_def) apply (rule conjI) apply (simp add: valid_pspace_def) apply (rule conjI) apply (clarsimp simp: kernel_base_def valid_objs_def state_defs
                          valid_obj_def valid_vm_rights_def vm_kernel_only_def
                          dom_if_Some cte_level_bits_def) apply (rule conjI) apply (simp add: vmsz_aligned_def, rule is_aligned_addrFromPPtr_n;
            clarsimp simp: is_aligned_def) apply (rule conjI) apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def is_master_reply_cap_def
                           valid_cap_def obj_at_def valid_tcb_state_def valid_arch_tcb_def
                           cap_aligned_def word_bits_def valid_ipc_buffer_cap_simps)+ apply (clarsimp simp: valid_cs_def word_bits_def cte_level_bits_def
                          init_irq_ptrs_all_ineqs valid_tcb_def
                   split: if_split_asm) apply (simp add: vmsz_aligned_def, rule is_aligned_addrFromPPtr_n;
           clarsimp simp: is_aligned_def) apply (rule conjI) apply (clarsimp simp: pspace_aligned_def state_defs wf_obj_bits [OF wf_empty_bits]
                          dom_if_Some cte_level_bits_def) apply (safe intro!: aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl],
           simp_all add: is_aligned_def word_bits_def kernel_base_def)[1] apply (rule conjI) apply (simp add:pspace_distinct_init_A) apply (rule conjI) apply (clarsimp simp: if_live_then_nonz_cap_def obj_at_def state_defs live_def hyp_live_def) apply (rule conjI) apply (clarsimp simp: zombies_final_def cte_wp_at_cases state_defs
                          tcb_cap_cases_def is_zombie_def) apply (clarsimp simp: sym_refs_def state_refs_of_def state_defs state_hyp_refs_of_def) apply (rule conjI) apply (clarsimp simp: valid_mdb_def init_cdt_def no_mloop_def
                         mdb_cte_at_def) apply (clarsimp simp: untyped_mdb_def caps_of_state_init_A_st_Null
                         untyped_inc_def ut_revocable_def
                         irq_revocable_def reply_master_revocable_def
                         reply_mdb_def reply_caps_mdb_def
                         reply_masters_mdb_def) apply (simp add:descendants_inc_def) apply (rule conjI) apply (simp add: valid_ioc_def init_A_st_def init_ioc_def cte_wp_at_cases2) apply (intro allI impI, elim exE conjE) apply (case_tac obj, simp_all add: cap_of_def) apply (clarsimp simp: init_kheap_def split: if_split_asm) apply (rule conjI) apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def state_defs valid_arch_idle_def) apply (rule conjI) apply (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def state_defs) apply (rule conjI) apply (clarsimp simp: if_unsafe_then_cap_def caps_of_state_init_A_st_Null) apply (subst conj_assoc[symmetric]) apply (subst conj_assoc[symmetric]) apply (subst conj_assoc) apply (rule conjI) using cte_wp_at_init_A_st_Null apply (fastforce simp: valid_reply_caps_def unique_reply_caps_def
                         has_reply_cap_def is_reply_cap_to_def pred_tcb_at_def obj_at_def
                         caps_of_state_init_A_st_Null is_master_reply_cap_to_def
                         valid_reply_masters_def valid_global_refs_def
                         valid_refs_def[unfolded cte_wp_at_caps_of_state]) apply (rule conjI) apply (clarsimp simp: valid_arch_state_def) apply (rule conjI) apply (clarsimp simp: valid_asid_table_def state_defs) apply (rule conjI) apply (clarsimp simp: valid_arch_state_def obj_at_def state_defs
                          a_type_def) apply (rule conjI) apply (simp add: valid_global_pts_def state_defs) apply (simp add: state_defs is_inv_def) apply (rule conjI) apply (clarsimp simp: valid_irq_node_def obj_at_def state_defs
                         is_cap_table_def wf_empty_bits
                         init_irq_ptrs_all_ineqs cte_level_bits_def
                         init_irq_ptrs_eq[unfolded cte_level_bits_def]) apply (intro conjI) apply (rule inj_onI) apply (simp add: init_irq_ptrs_eq[unfolded cte_level_bits_def]) apply clarsimp apply word_bitwise apply (simp add: valid_irq_handlers_def caps_of_state_init_A_st_Null
                   ran_def cong: rev_conj_cong) apply (rule conjI) apply (clarsimp simp: valid_irq_states_def init_A_st_def init_machine_state_def valid_irq_masks_def init_irq_masks_def) apply (rule conjI) apply (clarsimp simp: valid_machine_state_def init_A_st_def
                         init_machine_state_def init_underlying_memory_def) apply (rule conjI) apply (clarsimp simp: obj_at_def state_defs valid_vspace_objs_def) apply (clarsimp simp: vs_lookup_def vs_asid_refs_def) apply (rule conjI) apply (clarsimp simp: valid_arch_caps_def) apply (rule conjI) apply (clarsimp simp: valid_vs_lookup_def) apply (clarsimp simp: vs_lookup_pages_def state_defs vs_asid_refs_def) apply (clarsimp simp: valid_table_caps_def caps_of_state_init_A_st_Null
                         unique_table_caps_def unique_table_refs_def) apply (rule conjI) apply (clarsimp simp: valid_global_objs_def state_defs) apply (clarsimp simp: valid_ao_at_def obj_at_def empty_table_def pde_ref_def
                         valid_pde_mappings_def valid_vso_at_def) apply (simp add: kernel_mapping_slots_def kernel_base_def) apply (rule is_aligned_addrFromPPtr_n; simp add: pageBits_def is_aligned_def) apply (rule conjI) apply (simp add: valid_kernel_mappings_def state_defs
                         valid_kernel_mappings_if_pd_def pde_ref_def
                         ran_def) apply (auto simp: pde_ref_def split: if_split_asm)[1] apply (rule conjI) apply (clarsimp simp: equal_kernel_mappings_def state_defs obj_at_def) apply (rule conjI) apply (clarsimp simp: valid_asid_map_def state_defs) apply (rule conjI) apply (clarsimp simp: valid_global_vspace_mappings_def obj_at_def state_defs
                         valid_pd_kernel_mappings_def mask_pde_mapping_bits) apply (simp add: valid_pde_kernel_mappings_def kernel_base_def) apply (rule conjI) apply (fastforce simp:pde_mapping_bits_def) apply (intro ballI impI) apply (clarsimp simp:pde_mapping_bits_def) apply word_bitwise apply clarsimp apply (rule conjI) apply (clarsimp simp: pspace_in_kernel_window_def state_defs mask_def) apply (intro conjI impI) apply (rule in_kernel_base|simp)+ apply (erule exE,drule sym,simp add:field_simps) apply (rule in_kernel_base[simplified add.commute]) apply (rule word_less_add_right, simp add: cte_level_bits_def) apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1] apply simp apply (simp add:cte_level_bits_def field_simps) apply (subst add.commute) apply (rule le_plus') apply simp+ apply (rule less_imp_le) apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1] apply (rule in_kernel_base|simp)+ apply (simp add: cap_refs_in_kernel_window_def caps_of_state_init_A_st_Null
                  valid_refs_def[unfolded cte_wp_at_caps_of_state]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs init_A_st proof (prove)
goal (1 subgoal):
 1. valid_state init_A_st \<and> cur_tcb init_A_st proof (prove)
goal (2 subgoals):
 1. valid_state init_A_st
 2. cur_tcb init_A_st proof (prove)
goal (2 subgoals):
 1. cur_tcb init_A_st
 2. valid_state init_A_st proof (prove)
goal (1 subgoal):
 1. valid_state init_A_st proof (prove)
goal (1 subgoal):
 1. valid_pspace init_A_st \<and> valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_pspace init_A_st
 2. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_objs init_A_st \<and> pspace_aligned init_A_st \<and> pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 2. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. valid_objs init_A_st
 2. pspace_aligned init_A_st \<and> pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 3. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. vmsz_aligned (addrFromPPtr 0xE0000000) ARMSection \<and> valid_tcb 0xE0001000 \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr> \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr> \<and> (\<forall>ptr. (ptr = 0xE0001000 \<longrightarrow> (\<exists>irq. 0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) = 0) \<longrightarrow> valid_tcb 0xE0001000 \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr> \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>) \<and> (ptr \<noteq> 0xE0001000 \<longrightarrow> ptr \<noteq> 0xE0005000 \<longrightarrow> (ptr = 0xE0060000 \<longrightarrow> (\<exists>irq. UCAST(10 \<rightarrow> 32) irq << 4 = 0x58000) \<longrightarrow> vmsz_aligned (addrFromPPtr 0xE0000000) ARMSection) \<and> (ptr \<noteq> 0xE0060000 \<longrightarrow> (\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = ptr) \<longrightarrow> valid_cs 0 (empty_cnode 0) \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>)))
 2. pspace_aligned init_A_st \<and> pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 3. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (4 subgoals):
 1. vmsz_aligned (addrFromPPtr 0xE0000000) ARMSection
 2. valid_tcb 0xE0001000 \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr> \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr> \<and> (\<forall>ptr. (ptr = 0xE0001000 \<longrightarrow> (\<exists>irq. 0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) = 0) \<longrightarrow> valid_tcb 0xE0001000 \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr> \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>) \<and> (ptr \<noteq> 0xE0001000 \<longrightarrow> ptr \<noteq> 0xE0005000 \<longrightarrow> (ptr = 0xE0060000 \<longrightarrow> (\<exists>irq. UCAST(10 \<rightarrow> 32) irq << 4 = 0x58000) \<longrightarrow> vmsz_aligned (addrFromPPtr 0xE0000000) ARMSection) \<and> (ptr \<noteq> 0xE0060000 \<longrightarrow> (\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = ptr) \<longrightarrow> valid_cs 0 (empty_cnode 0) \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>)))
 3. pspace_aligned init_A_st \<and> pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 4. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. valid_tcb 0xE0001000 \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr> \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr> \<and> (\<forall>ptr. (ptr = 0xE0001000 \<longrightarrow> (\<exists>irq. 0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) = 0) \<longrightarrow> valid_tcb 0xE0001000 \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr> \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>) \<and> (ptr \<noteq> 0xE0001000 \<longrightarrow> ptr \<noteq> 0xE0005000 \<longrightarrow> (ptr = 0xE0060000 \<longrightarrow> (\<exists>irq. UCAST(10 \<rightarrow> 32) irq << 4 = 0x58000) \<longrightarrow> vmsz_aligned (addrFromPPtr 0xE0000000) ARMSection) \<and> (ptr \<noteq> 0xE0060000 \<longrightarrow> (\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = ptr) \<longrightarrow> valid_cs 0 (empty_cnode 0) \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>)))
 2. pspace_aligned init_A_st \<and> pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 3. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (4 subgoals):
 1. valid_tcb 0xE0001000 \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr> \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>
 2. \<forall>ptr. (ptr = 0xE0001000 \<longrightarrow> (\<exists>irq. 0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) = 0) \<longrightarrow> valid_tcb 0xE0001000 \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr> \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>) \<and> (ptr \<noteq> 0xE0001000 \<longrightarrow> ptr \<noteq> 0xE0005000 \<longrightarrow> (ptr = 0xE0060000 \<longrightarrow> (\<exists>irq. UCAST(10 \<rightarrow> 32) irq << 4 = 0x58000) \<longrightarrow> vmsz_aligned (addrFromPPtr 0xE0000000) ARMSection) \<and> (ptr \<noteq> 0xE0060000 \<longrightarrow> (\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = ptr) \<longrightarrow> valid_cs 0 (empty_cnode 0) \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>))
 3. pspace_aligned init_A_st \<and> pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 4. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. \<And>ptr. \<lbrakk>ptr \<noteq> 0xE0001000; ptr \<noteq> 0xE0005000\<rbrakk> \<Longrightarrow> (ptr = 0xE0060000 \<longrightarrow> (\<exists>irq. UCAST(10 \<rightarrow> 32) irq << 4 = 0x58000) \<longrightarrow> vmsz_aligned (addrFromPPtr 0xE0000000) ARMSection) \<and> (ptr \<noteq> 0xE0060000 \<longrightarrow> (\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = ptr) \<longrightarrow> valid_cs 0 (empty_cnode 0) \<lparr>kheap = (\<lambda>x. if \<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x then Some (CNode 0 (empty_cnode 0)) else None)(0xE0001000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, 0xE0005000 \<mapsto> ArchObj (DataPage False ARMSmallPage), 0xE0060000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(0xE00 := SectionPDE (addrFromPPtr 0xE0000000) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = 0xE0001000, idle_thread = 0xE0001000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = 0xE0060000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if 0xE0000000 \<le> ref \<and> ref \<le> 0xE0000000 + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>)
 2. pspace_aligned init_A_st \<and> pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 3. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. \<And>irq. UCAST(10 \<rightarrow> 32) irq << 4 = 0x58000 \<Longrightarrow> vmsz_aligned (addrFromPPtr 0xE0000000) ARMSection
 2. pspace_aligned init_A_st \<and> pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 3. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. pspace_aligned init_A_st \<and> pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 2. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. pspace_aligned init_A_st
 2. pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 3. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. is_aligned (kernel_base + 0x60000) 14 \<and> is_aligned (kernel_base + 0x5000) 12 \<and> is_aligned (kernel_base + 0x1000) 9 \<and> (\<forall>x. (x = kernel_base + 0x1000 \<longrightarrow> (\<exists>irq. 0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) = 0) \<longrightarrow> is_aligned (kernel_base + 0x1000) 9) \<and> (x \<noteq> kernel_base + 0x1000 \<longrightarrow> (x = kernel_base + 0x5000 \<longrightarrow> (\<exists>irq. 0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) = 0) \<longrightarrow> is_aligned (kernel_base + 0x5000) 12) \<and> (x \<noteq> kernel_base + 0x5000 \<longrightarrow> (x = kernel_base + 0x60000 \<longrightarrow> (\<exists>irq. UCAST(10 \<rightarrow> 32) irq << 4 = 0x58000) \<longrightarrow> is_aligned (kernel_base + 0x60000) 14) \<and> (x \<noteq> kernel_base + 0x60000 \<longrightarrow> (\<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x) \<longrightarrow> is_aligned x 4))))
 2. pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 3. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. pspace_distinct init_A_st \<and> if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 2. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. pspace_distinct init_A_st
 2. if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 3. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. if_live_then_nonz_cap init_A_st \<and> zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 2. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. if_live_then_nonz_cap init_A_st
 2. zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 3. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. zombies_final init_A_st \<and> sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 2. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. zombies_final init_A_st
 2. sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 3. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. sym_refs (state_refs_of init_A_st) \<and> sym_refs (state_hyp_refs_of init_A_st)
 2. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_mdb init_A_st \<and> valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_mdb init_A_st
 2. valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. untyped_mdb (\<lambda>x. None) (caps_of_state init_A_st) \<and> descendants_inc (\<lambda>x. None) (caps_of_state init_A_st) \<and> untyped_inc (\<lambda>x. None) (caps_of_state init_A_st) \<and> ut_revocable (is_original_cap init_A_st) (caps_of_state init_A_st) \<and> irq_revocable (is_original_cap init_A_st) (caps_of_state init_A_st) \<and> reply_master_revocable (is_original_cap init_A_st) (caps_of_state init_A_st) \<and> reply_mdb (\<lambda>x. None) (caps_of_state init_A_st)
 2. valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. descendants_inc (\<lambda>x. None) (caps_of_state init_A_st)
 2. valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_ioc init_A_st \<and> valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_ioc init_A_st
 2. valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<forall>a b. (\<exists>obj. init_kheap a = Some obj \<and> (\<exists>cap. cap_of obj b = Some cap \<and> cap \<noteq> NullCap)) \<longrightarrow> (\<exists>sz fun. init_kheap a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. init_kheap a = Some (TCB tcb) \<and> (\<exists>cap. tcb_cnode_map tcb b = Some cap \<and> cap \<noteq> NullCap))
 2. valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>a b obj cap. \<lbrakk>init_kheap a = Some obj; cap_of obj b = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> (\<exists>sz fun. init_kheap a = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. init_kheap a = Some (TCB tcb) \<and> (\<exists>cap. tcb_cnode_map tcb b = Some cap \<and> cap \<noteq> NullCap))
 2. valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>a b obj cap x11 x12. \<lbrakk>init_kheap a = Some (CNode x11 x12); x12 b = Some cap; cap \<noteq> NullCap; obj = CNode x11 x12\<rbrakk> \<Longrightarrow> well_formed_cnode_n x11 x12
 2. valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_idle init_A_st \<and> only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_idle init_A_st
 2. only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. only_idle init_A_st \<and> if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. only_idle init_A_st
 2. if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap init_A_st \<and> valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. if_unsafe_then_cap init_A_st
 2. valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. (valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st) \<and> valid_global_refs init_A_st \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. ((valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st) \<and> valid_global_refs init_A_st) \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. (valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st) \<and> valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st
 2. valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
using this:
cte_wp_at ?P ?p init_A_st \<Longrightarrow> ?P NullCap

goal (2 subgoals):
 1. valid_reply_caps init_A_st \<and> valid_reply_masters init_A_st \<and> valid_global_refs init_A_st
 2. valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_arch_state init_A_st \<and> valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_arch_state init_A_st
 2. valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_asid_table (asid_table init_A_st) init_A_st \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state init_A_st)) init_A_st \<and> valid_global_pts init_A_st \<and> is_inv (arm_hwasid_table (arch_state init_A_st)) (map_option fst \<circ> arm_asid_map (arch_state init_A_st))
 2. valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. valid_asid_table (asid_table init_A_st) init_A_st
 2. typ_at (AArch APageDirectory) (arm_global_pd (arch_state init_A_st)) init_A_st \<and> valid_global_pts init_A_st \<and> is_inv (arm_hwasid_table (arch_state init_A_st)) (map_option fst \<circ> arm_asid_map (arch_state init_A_st))
 3. valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. typ_at (AArch APageDirectory) (arm_global_pd (arch_state init_A_st)) init_A_st \<and> valid_global_pts init_A_st \<and> is_inv (arm_hwasid_table (arch_state init_A_st)) (map_option fst \<circ> arm_asid_map (arch_state init_A_st))
 2. valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. typ_at (AArch APageDirectory) (arm_global_pd (arch_state init_A_st)) init_A_st
 2. valid_global_pts init_A_st \<and> is_inv (arm_hwasid_table (arch_state init_A_st)) (map_option fst \<circ> arm_asid_map (arch_state init_A_st))
 3. valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_global_pts init_A_st \<and> is_inv (arm_hwasid_table (arch_state init_A_st)) (map_option fst \<circ> arm_asid_map (arch_state init_A_st))
 2. valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. valid_global_pts init_A_st
 2. is_inv (arm_hwasid_table (arch_state init_A_st)) (map_option fst \<circ> arm_asid_map (arch_state init_A_st))
 3. valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. is_inv (arm_hwasid_table (arch_state init_A_st)) (map_option fst \<circ> arm_asid_map (arch_state init_A_st))
 2. valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_irq_node init_A_st \<and> valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_irq_node init_A_st
 2. valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. inj (\<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << 4)) \<and> (\<forall>irq. 0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<and> (0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<longrightarrow> 0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<and> (0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<longrightarrow> UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000)))
 2. valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. inj (\<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << 4))
 2. \<forall>irq. 0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<and> (0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<longrightarrow> 0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<and> (0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<longrightarrow> UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000))
 3. valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) x << 4) = kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) y << 4)\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>irq. 0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<and> (0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<longrightarrow> 0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<and> (0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<longrightarrow> UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000))
 3. valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<forall>irq. 0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<and> (0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<longrightarrow> 0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<and> (0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<longrightarrow> UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000))
 2. valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>irq. 0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<and> (0x7000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<longrightarrow> 0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<and> (0x3000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> 0 \<longrightarrow> UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000))
 2. valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_irq_handlers init_A_st \<and> valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_irq_states init_A_st \<and> valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_irq_states init_A_st
 2. valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_machine_state init_A_st \<and> valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_machine_state init_A_st
 2. valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs init_A_st \<and> valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_vspace_objs init_A_st
 2. valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>p. ((\<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = p) \<longrightarrow> p \<noteq> kernel_base + 0x1000 \<longrightarrow> p \<noteq> kernel_base + 0x5000 \<longrightarrow> p = kernel_base + 0x60000 \<longrightarrow> (\<exists>rs. (rs \<rhd> (kernel_base + 0x60000)) \<lparr>kheap = (\<lambda>x. if \<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(kernel_base + 0x1000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, kernel_base + 0x5000 \<mapsto> ArchObj (DataPage False ARMSmallPage), kernel_base + 0x60000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = kernel_base + 0x1000, idle_thread = kernel_base + 0x1000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = kernel_base + 0x60000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>) \<longrightarrow> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<notin> kernel_mapping_slots \<longrightarrow> data_at ARMSection kernel_base \<lparr>kheap = (\<lambda>x. if \<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(kernel_base + 0x1000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, kernel_base + 0x5000 \<mapsto> ArchObj (DataPage False ARMSmallPage), kernel_base + 0x60000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = kernel_base + 0x1000, idle_thread = kernel_base + 0x1000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = kernel_base + 0x60000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>) \<and> ((\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> p) \<longrightarrow> p \<noteq> kernel_base + 0x1000 \<longrightarrow> p \<noteq> kernel_base + 0x5000 \<longrightarrow> p = kernel_base + 0x60000 \<longrightarrow> (\<exists>rs. (rs \<rhd> (kernel_base + 0x60000)) \<lparr>kheap = (\<lambda>x. if \<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(kernel_base + 0x1000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, kernel_base + 0x5000 \<mapsto> ArchObj (DataPage False ARMSmallPage), kernel_base + 0x60000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = kernel_base + 0x1000, idle_thread = kernel_base + 0x1000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = kernel_base + 0x60000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>) \<longrightarrow> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<notin> kernel_mapping_slots \<longrightarrow> data_at ARMSection kernel_base \<lparr>kheap = (\<lambda>x. if \<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(kernel_base + 0x1000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, kernel_base + 0x5000 \<mapsto> ArchObj (DataPage False ARMSmallPage), kernel_base + 0x60000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = kernel_base + 0x1000, idle_thread = kernel_base + 0x1000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = kernel_base + 0x60000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>)
 2. valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_arch_caps init_A_st \<and> valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_arch_caps init_A_st
 2. valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_vs_lookup init_A_st \<and> valid_table_caps init_A_st \<and> unique_table_caps (caps_of_state init_A_st) \<and> unique_table_refs (caps_of_state init_A_st)
 2. valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. valid_vs_lookup init_A_st
 2. valid_table_caps init_A_st \<and> unique_table_caps (caps_of_state init_A_st) \<and> unique_table_refs (caps_of_state init_A_st)
 3. valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. \<And>p ref. (ref \<unrhd> p) init_A_st \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state init_A_st (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)
 2. valid_table_caps init_A_st \<and> unique_table_caps (caps_of_state init_A_st) \<and> unique_table_refs (caps_of_state init_A_st)
 3. valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_table_caps init_A_st \<and> unique_table_caps (caps_of_state init_A_st) \<and> unique_table_refs (caps_of_state init_A_st)
 2. valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_global_objs init_A_st \<and> valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_global_objs init_A_st
 2. valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_vso_at (kernel_base + 0x60000) \<lparr>kheap = (\<lambda>x. if \<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(kernel_base + 0x1000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, kernel_base + 0x5000 \<mapsto> ArchObj (DataPage False ARMSmallPage), kernel_base + 0x60000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = kernel_base + 0x1000, idle_thread = kernel_base + 0x1000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = kernel_base + 0x60000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr> \<and> obj_at (empty_table (set (second_level_tables \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = kernel_base + 0x60000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>))) (kernel_base + 0x60000) \<lparr>kheap = (\<lambda>x. if \<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(kernel_base + 0x1000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, kernel_base + 0x5000 \<mapsto> ArchObj (DataPage False ARMSmallPage), kernel_base + 0x60000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = kernel_base + 0x1000, idle_thread = kernel_base + 0x1000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = kernel_base + 0x60000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>
 2. valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. (UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<notin> kernel_mapping_slots \<longrightarrow> data_at ARMSection kernel_base \<lparr>kheap = (\<lambda>x. if \<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(kernel_base + 0x1000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, kernel_base + 0x5000 \<mapsto> ArchObj (DataPage False ARMSmallPage), kernel_base + 0x60000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = kernel_base + 0x1000, idle_thread = kernel_base + 0x1000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = kernel_base + 0x60000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>) \<and> is_aligned (addrFromPPtr kernel_base) pageBits \<and> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<in> kernel_mapping_slots
 2. valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. is_aligned (addrFromPPtr 0xE0000000) pageBits
 2. valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_kernel_mappings init_A_st \<and> equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_kernel_mappings init_A_st
 2. equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<forall>x. (\<exists>a. ((\<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = a) \<longrightarrow> (a = kernel_base + 0x1000 \<longrightarrow> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr> = x) \<and> (a \<noteq> kernel_base + 0x1000 \<longrightarrow> (a = kernel_base + 0x5000 \<longrightarrow> ArchObj (DataPage False ARMSmallPage) = x) \<and> (a \<noteq> kernel_base + 0x5000 \<longrightarrow> (a = kernel_base + 0x60000 \<longrightarrow> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {}))) = x) \<and> (a \<noteq> kernel_base + 0x60000 \<longrightarrow> CNode 0 (empty_cnode 0) = x)))) \<and> ((\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> a) \<longrightarrow> (a = kernel_base + 0x1000 \<longrightarrow> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr> = x) \<and> (a \<noteq> kernel_base + 0x1000 \<longrightarrow> (a = kernel_base + 0x5000 \<longrightarrow> ArchObj (DataPage False ARMSmallPage) = x) \<and> (a \<noteq> kernel_base + 0x5000 \<longrightarrow> (a = kernel_base + 0x60000 \<longrightarrow> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {}))) = x) \<and> a = kernel_base + 0x60000)))) \<longrightarrow> (case x of ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state \<lparr>kheap = (\<lambda>x. if \<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(kernel_base + 0x1000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, kernel_base + 0x5000 \<mapsto> ArchObj (DataPage False ARMSmallPage), kernel_base + 0x60000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = kernel_base + 0x1000, idle_thread = kernel_base + 0x1000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = kernel_base + 0x60000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>))) = (x \<in> kernel_mapping_slots) | ArchObj _ \<Rightarrow> True | _ \<Rightarrow> True)
 2. equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. equal_kernel_mappings init_A_st \<and> valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. equal_kernel_mappings init_A_st
 2. valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_asid_map init_A_st \<and> valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_asid_map init_A_st
 2. valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. valid_global_vspace_mappings init_A_st \<and> pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. valid_global_vspace_mappings init_A_st
 2. pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>x. (x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> valid_pde_kernel_mappings (SectionPDE (addrFromPPtr kernel_base) {} 0 {}) (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) << pde_mapping_bits) (\<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + (2 ^ pde_mapping_bits - 1) then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion) \<lparr>kheap = (\<lambda>x. if \<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(kernel_base + 0x1000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, kernel_base + 0x5000 \<mapsto> ArchObj (DataPage False ARMSmallPage), kernel_base + 0x60000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = kernel_base + 0x1000, idle_thread = kernel_base + 0x1000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = kernel_base + 0x60000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + (2 ^ pde_mapping_bits - 1) then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> valid_pde_kernel_mappings InvalidPDE (UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) (\<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + (2 ^ pde_mapping_bits - 1) then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion) \<lparr>kheap = (\<lambda>x. if \<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(kernel_base + 0x1000 \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = init_arch_tcb\<rparr>, kernel_base + 0x5000 \<mapsto> ArchObj (DataPage False ARMSmallPage), kernel_base + 0x60000 \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = init_cdt, is_original_cap = init_ioc, cur_thread = kernel_base + 0x1000, idle_thread = kernel_base + 0x1000, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = \<lambda>_. IRQInactive, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = kernel_base + 0x60000, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + (2 ^ pde_mapping_bits - 1) then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = ext_init\<rparr>)
 2. pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>x. (x = 0xE00 \<longrightarrow> 0xE00 << pde_mapping_bits = 0xE0000000 \<and> (\<exists>use. (\<forall>x\<in>{0xE00 << pde_mapping_bits..(0xE00 << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. (0xE0000000 \<le> x \<and> x \<le> 0xDFFFFFFF + 2 ^ pde_mapping_bits \<longrightarrow> ArmVSpaceKernelWindow = use) \<and> ((0xE0000000 \<le> x \<longrightarrow> \<not> x \<le> 0xDFFFFFFF + 2 ^ pde_mapping_bits) \<longrightarrow> ArmVSpaceInvalidRegion = use)) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow))) \<and> (x \<noteq> 0xE00 \<longrightarrow> (\<forall>x\<in>{UCAST(12 \<rightarrow> 32) x << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. 0xE0000000 \<le> x \<longrightarrow> \<not> x \<le> 0xDFFFFFFF + 2 ^ pde_mapping_bits))
 2. pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (3 subgoals):
 1. \<And>x. x = 0xE00 \<longrightarrow> 0xE00 << pde_mapping_bits = 0xE0000000 \<and> (\<exists>use. (\<forall>x\<in>{0xE00 << pde_mapping_bits..(0xE00 << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. (0xE0000000 \<le> x \<and> x \<le> 0xDFFFFFFF + 2 ^ pde_mapping_bits \<longrightarrow> ArmVSpaceKernelWindow = use) \<and> ((0xE0000000 \<le> x \<longrightarrow> \<not> x \<le> 0xDFFFFFFF + 2 ^ pde_mapping_bits) \<longrightarrow> ArmVSpaceInvalidRegion = use)) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow))
 2. \<And>x. x \<noteq> 0xE00 \<longrightarrow> (\<forall>x\<in>{UCAST(12 \<rightarrow> 32) x << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. 0xE0000000 \<le> x \<longrightarrow> \<not> x \<le> 0xDFFFFFFF + 2 ^ pde_mapping_bits)
 3. pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<noteq> 0xE00 \<longrightarrow> (\<forall>x\<in>{UCAST(12 \<rightarrow> 32) x << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. 0xE0000000 \<le> x \<longrightarrow> \<not> x \<le> 0xDFFFFFFF + 2 ^ pde_mapping_bits)
 2. pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; xa \<in> {UCAST(12 \<rightarrow> 32) x << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) x << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}; 0xE0000000 \<le> xa\<rbrakk> \<Longrightarrow> \<not> xa \<le> 0xDFFFFFFF + 2 ^ pde_mapping_bits
 2. pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa \<le> 0xE00FFFFF\<rbrakk> \<Longrightarrow> False
 2. pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x !! 10 \<longrightarrow> x !! 9 \<longrightarrow> x !! 0 \<or> x !! 1 \<or> x !! 2 \<or> x !! 3 \<or> x !! 4 \<or> x !! 5 \<or> x !! 6 \<or> x !! 7 \<or> x !! 8 \<or> \<not> x !! 11; xa !! 31 \<and> xa !! 30 \<and> xa !! 29; xa !! 31 \<and> \<not> x !! 11 \<or> (xa !! 31 \<or> \<not> x !! 11) \<and> (xa !! 30 \<and> \<not> x !! 10 \<or> (xa !! 30 \<or> \<not> x !! 10) \<and> (xa !! 29 \<and> \<not> x !! 9 \<or> (xa !! 29 \<or> \<not> x !! 9) \<and> (xa !! 28 \<and> \<not> x !! 8 \<or> (xa !! 28 \<or> \<not> x !! 8) \<and> (xa !! 27 \<and> \<not> x !! 7 \<or> (xa !! 27 \<or> \<not> x !! 7) \<and> (xa !! 26 \<and> \<not> x !! 6 \<or> (xa !! 26 \<or> \<not> x !! 6) \<and> (xa !! 25 \<and> \<not> x !! 5 \<or> (xa !! 25 \<or> \<not> x !! 5) \<and> (xa !! 24 \<and> \<not> x !! 4 \<or> (xa !! 24 \<or> \<not> x !! 4) \<and> (xa !! 23 \<and> \<not> x !! 3 \<or> (xa !! 23 \<or> \<not> x !! 3) \<and> (xa !! 22 \<and> \<not> x !! 2 \<or> (xa !! 22 \<or> \<not> x !! 2) \<and> (xa !! 21 \<and> \<not> x !! 1 \<or> (xa !! 21 \<or> \<not> x !! 1) \<and> (xa !! 20 \<and> \<not> x !! 0 \<or> xa !! 20 \<or> \<not> x !! 0))))))))))); x !! 11 \<and> \<not> xa !! 31 \<or> (x !! 11 \<or> \<not> xa !! 31) \<and> (x !! 10 \<and> \<not> xa !! 30 \<or> (x !! 10 \<or> \<not> xa !! 30) \<and> (x !! 9 \<and> \<not> xa !! 29 \<or> (x !! 9 \<or> \<not> xa !! 29) \<and> (x !! 8 \<and> \<not> xa !! 28 \<or> (x !! 8 \<or> \<not> xa !! 28) \<and> (x !! 7 \<and> \<not> xa !! 27 \<or> (x !! 7 \<or> \<not> xa !! 27) \<and> (x !! 6 \<and> \<not> xa !! 26 \<or> (x !! 6 \<or> \<not> xa !! 26) \<and> (x !! 5 \<and> \<not> xa !! 25 \<or> (x !! 5 \<or> \<not> xa !! 25) \<and> (x !! 4 \<and> \<not> xa !! 24 \<or> (x !! 4 \<or> \<not> xa !! 24) \<and> (x !! 3 \<and> \<not> xa !! 23 \<or> (x !! 3 \<or> \<not> xa !! 23) \<and> (x !! 2 \<and> \<not> xa !! 22 \<or> (x !! 2 \<or> \<not> xa !! 22) \<and> (x !! 1 \<and> \<not> xa !! 21 \<or> (x !! 1 \<or> \<not> xa !! 21) \<and> (x !! 0 \<and> \<not> xa !! 20 \<or> x !! 0 \<or> \<not> xa !! 20))))))))))); xa !! 29 \<longrightarrow> xa !! 30 \<longrightarrow> xa !! 31 \<longrightarrow> \<not> xa !! 28 \<and> \<not> xa !! 27 \<and> \<not> xa !! 26 \<and> \<not> xa !! 25 \<and> \<not> xa !! 24 \<and> \<not> xa !! 23 \<and> \<not> xa !! 22 \<and> \<not> xa !! 21 \<and> \<not> xa !! 20\<rbrakk> \<Longrightarrow> False
 2. pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. pspace_in_kernel_window init_A_st \<and> cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. pspace_in_kernel_window init_A_st
 2. cap_refs_in_kernel_window init_A_st proof (prove)
goal (2 subgoals):
 1. \<And>x. ((\<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x) \<longrightarrow> (x = kernel_base + 0x1000 \<longrightarrow> (\<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF)) \<and> (x \<noteq> kernel_base + 0x1000 \<longrightarrow> (x = kernel_base + 0x5000 \<longrightarrow> (\<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF)) \<and> (x \<noteq> kernel_base + 0x5000 \<longrightarrow> (x = kernel_base + 0x60000 \<longrightarrow> (\<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF)) \<and> (x \<noteq> kernel_base + 0x60000 \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ cte_level_bits - 1}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF))))) \<and> ((\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x) \<longrightarrow> (x = kernel_base + 0x1000 \<longrightarrow> (\<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF)) \<and> (x \<noteq> kernel_base + 0x1000 \<longrightarrow> (x = kernel_base + 0x5000 \<longrightarrow> (\<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF)) \<and> (x \<noteq> kernel_base + 0x5000 \<longrightarrow> x = kernel_base + 0x60000 \<longrightarrow> (\<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF))))
 2. cap_refs_in_kernel_window init_A_st proof (prove)
goal (8 subgoals):
 1. \<And>x. \<lbrakk>\<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 2. \<And>x. \<lbrakk>\<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 3. \<And>x. \<lbrakk>\<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. \<And>x. \<lbrakk>\<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x \<noteq> kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{x..x + 2 ^ cte_level_bits - 1}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 6. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 7. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 8. cap_refs_in_kernel_window init_A_st proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>\<exists>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x \<noteq> kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{x..x + 2 ^ cte_level_bits - 1}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 2. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 3. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. cap_refs_in_kernel_window init_A_st proof (prove)
goal (5 subgoals):
 1. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << cte_level_bits \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x8000)\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + ((UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x8000)..kernel_base + ((UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + (2 ^ cte_level_bits + 0x7FFF))}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 2. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 3. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. cap_refs_in_kernel_window init_A_st proof (prove)
goal (6 subgoals):
 1. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << cte_level_bits \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x8000)\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x8000 < 0xFFFFF
 2. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << cte_level_bits \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x8000)\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + (2 ^ cte_level_bits + 0x7FFF) \<le> 0xFFFFF
 3. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 6. cap_refs_in_kernel_window init_A_st proof (prove)
goal (7 subgoals):
 1. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << 4) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << 4) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << 4) + 0x8000)\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq << 4 < 0xF7FFF
 2. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << cte_level_bits \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x8000)\<rbrakk> \<Longrightarrow> 0x8000 \<le> 0xFFFFF
 3. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << cte_level_bits \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x8000)\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + (2 ^ cte_level_bits + 0x7FFF) \<le> 0xFFFFF
 4. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 6. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 7. cap_refs_in_kernel_window init_A_st proof (prove)
goal (6 subgoals):
 1. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << cte_level_bits \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x8000)\<rbrakk> \<Longrightarrow> 0x8000 \<le> 0xFFFFF
 2. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << cte_level_bits \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x8000)\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + (2 ^ cte_level_bits + 0x7FFF) \<le> 0xFFFFF
 3. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 6. cap_refs_in_kernel_window init_A_st proof (prove)
goal (5 subgoals):
 1. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << cte_level_bits \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + 0x8000)\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) + (2 ^ cte_level_bits + 0x7FFF) \<le> 0xFFFFF
 2. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 3. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. cap_refs_in_kernel_window init_A_st proof (prove)
goal (5 subgoals):
 1. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << 4) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << 4) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << 4) + 0x8000)\<rbrakk> \<Longrightarrow> (UCAST(10 \<rightarrow> 32) irq << 4) + 0x800F \<le> 0xFFFFF
 2. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 3. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. cap_refs_in_kernel_window init_A_st proof (prove)
goal (5 subgoals):
 1. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << 4) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << 4) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << 4) + 0x8000)\<rbrakk> \<Longrightarrow> 0x800F + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xFFFFF
 2. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 3. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. cap_refs_in_kernel_window init_A_st proof (prove)
goal (6 subgoals):
 1. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << 4) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << 4) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << 4) + 0x8000)\<rbrakk> \<Longrightarrow> 0x800F \<le> 0xFFFFF
 2. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << 4) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << 4) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << 4) + 0x8000)\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq << 4 \<le> 0xFFFFF - 0x800F
 3. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 6. cap_refs_in_kernel_window init_A_st proof (prove)
goal (5 subgoals):
 1. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << 4) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << 4) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << 4) + 0x8000)\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq << 4 \<le> 0xF7FF0
 2. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 3. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. cap_refs_in_kernel_window init_A_st proof (prove)
goal (5 subgoals):
 1. \<And>x irq. \<lbrakk>(UCAST(10 \<rightarrow> 32) irq << 4) + 0x7000 \<noteq> 0; (UCAST(10 \<rightarrow> 32) irq << 4) + 0x3000 \<noteq> 0; UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> 0x58000; x = kernel_base + ((UCAST(10 \<rightarrow> 32) irq << 4) + 0x8000)\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq << 4 < 0xF7FF0
 2. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 3. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 5. cap_refs_in_kernel_window init_A_st proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x = kernel_base + 0x1000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x1000..0x11FF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 2. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x = kernel_base + 0x5000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x5000..0x5FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 3. \<And>x. \<lbrakk>\<forall>irq. kernel_base + 0x8000 + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> x; x \<noteq> kernel_base + 0x1000; x \<noteq> kernel_base + 0x5000; x = kernel_base + 0x60000\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + 0x60000..0x63FFF + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF
 4. cap_refs_in_kernel_window init_A_st proof (prove)
goal (1 subgoal):
 1. cap_refs_in_kernel_window init_A_st proof (prove)
goal:
No subgoals!