theory Init_R

lemma non_empty_refine_state_relation:
  "(zeroed_abstract_state, zeroed_intermediate_state) \<in> state_relation" apply (clarsimp simp: state_relation_def zeroed_state_defs state.defs) apply (intro conjI) apply (clarsimp simp: pspace_relation_def pspace_dom_def) apply (clarsimp simp: ekheap_relation_def) apply (clarsimp simp: ready_queues_relation_def) apply (clarsimp simp: ghost_relation_def) apply (fastforce simp: cdt_relation_def swp_def dest: cte_wp_at_domI) apply (clarsimp simp: cdt_list_relation_def map_to_ctes_def) apply (clarsimp simp: revokable_relation_def map_to_ctes_def) apply (clarsimp simp: zeroed_state_defs arch_state_relation_def) apply (clarsimp simp: interrupt_state_relation_def irq_state_relation_def cte_level_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (zeroed_abstract_state, zeroed_intermediate_state) \<in> state_relation proof (prove)
goal (1 subgoal):
 1. pspace_relation (\<lambda>x. None) (\<lambda>x. None) \<and> ekheap_relation (\<lambda>y. None) (\<lambda>x. None) \<and> ready_queues_relation (\<lambda>_ _. []) (\<lambda>y. []) \<and> ghost_relation (\<lambda>x. None) (\<lambda>x. None) (\<lambda>x. None) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None)) \<and> cdt_list_relation (\<lambda>y. []) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None)) \<and> revokable_relation (\<lambda>y. True) (null_filter (caps_of_state \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>)) (map_to_ctes (\<lambda>x. None)) \<and> (\<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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, ARMKernelState (\<lambda>x. None) (\<lambda>x. None) 0 (\<lambda>x. None) 0 [] (\<lambda>y. ArmVSpaceUserRegion)) \<in> arch_state_relation \<and> interrupt_state_relation (\<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits) (\<lambda>y. irq_state.IRQInactive) (InterruptState 0 (\<lambda>y. irqstate.IRQInactive)) proof (prove)
goal (9 subgoals):
 1. pspace_relation (\<lambda>x. None) (\<lambda>x. None)
 2. ekheap_relation (\<lambda>y. None) (\<lambda>x. None)
 3. ready_queues_relation (\<lambda>_ _. []) (\<lambda>y. [])
 4. ghost_relation (\<lambda>x. None) (\<lambda>x. None) (\<lambda>x. None)
 5. cdt_relation (swp (cte_wp_at (\<lambda>_. True)) \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None))
 6. cdt_list_relation (\<lambda>y. []) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None))
 7. revokable_relation (\<lambda>y. True) (null_filter (caps_of_state \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>)) (map_to_ctes (\<lambda>x. None))
 8. (\<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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, ARMKernelState (\<lambda>x. None) (\<lambda>x. None) 0 (\<lambda>x. None) 0 [] (\<lambda>y. ArmVSpaceUserRegion)) \<in> arch_state_relation
 9. interrupt_state_relation (\<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits) (\<lambda>y. irq_state.IRQInactive) (InterruptState 0 (\<lambda>y. irqstate.IRQInactive)) proof (prove)
goal (8 subgoals):
 1. ekheap_relation (\<lambda>y. None) (\<lambda>x. None)
 2. ready_queues_relation (\<lambda>_ _. []) (\<lambda>y. [])
 3. ghost_relation (\<lambda>x. None) (\<lambda>x. None) (\<lambda>x. None)
 4. cdt_relation (swp (cte_wp_at (\<lambda>_. True)) \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None))
 5. cdt_list_relation (\<lambda>y. []) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None))
 6. revokable_relation (\<lambda>y. True) (null_filter (caps_of_state \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>)) (map_to_ctes (\<lambda>x. None))
 7. (\<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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, ARMKernelState (\<lambda>x. None) (\<lambda>x. None) 0 (\<lambda>x. None) 0 [] (\<lambda>y. ArmVSpaceUserRegion)) \<in> arch_state_relation
 8. interrupt_state_relation (\<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits) (\<lambda>y. irq_state.IRQInactive) (InterruptState 0 (\<lambda>y. irqstate.IRQInactive)) proof (prove)
goal (7 subgoals):
 1. ready_queues_relation (\<lambda>_ _. []) (\<lambda>y. [])
 2. ghost_relation (\<lambda>x. None) (\<lambda>x. None) (\<lambda>x. None)
 3. cdt_relation (swp (cte_wp_at (\<lambda>_. True)) \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None))
 4. cdt_list_relation (\<lambda>y. []) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None))
 5. revokable_relation (\<lambda>y. True) (null_filter (caps_of_state \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>)) (map_to_ctes (\<lambda>x. None))
 6. (\<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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, ARMKernelState (\<lambda>x. None) (\<lambda>x. None) 0 (\<lambda>x. None) 0 [] (\<lambda>y. ArmVSpaceUserRegion)) \<in> arch_state_relation
 7. interrupt_state_relation (\<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits) (\<lambda>y. irq_state.IRQInactive) (InterruptState 0 (\<lambda>y. irqstate.IRQInactive)) proof (prove)
goal (6 subgoals):
 1. ghost_relation (\<lambda>x. None) (\<lambda>x. None) (\<lambda>x. None)
 2. cdt_relation (swp (cte_wp_at (\<lambda>_. True)) \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None))
 3. cdt_list_relation (\<lambda>y. []) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None))
 4. revokable_relation (\<lambda>y. True) (null_filter (caps_of_state \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>)) (map_to_ctes (\<lambda>x. None))
 5. (\<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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, ARMKernelState (\<lambda>x. None) (\<lambda>x. None) 0 (\<lambda>x. None) 0 [] (\<lambda>y. ArmVSpaceUserRegion)) \<in> arch_state_relation
 6. interrupt_state_relation (\<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits) (\<lambda>y. irq_state.IRQInactive) (InterruptState 0 (\<lambda>y. irqstate.IRQInactive)) proof (prove)
goal (5 subgoals):
 1. cdt_relation (swp (cte_wp_at (\<lambda>_. True)) \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None))
 2. cdt_list_relation (\<lambda>y. []) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None))
 3. revokable_relation (\<lambda>y. True) (null_filter (caps_of_state \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>)) (map_to_ctes (\<lambda>x. None))
 4. (\<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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, ARMKernelState (\<lambda>x. None) (\<lambda>x. None) 0 (\<lambda>x. None) 0 [] (\<lambda>y. ArmVSpaceUserRegion)) \<in> arch_state_relation
 5. interrupt_state_relation (\<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits) (\<lambda>y. irq_state.IRQInactive) (InterruptState 0 (\<lambda>y. irqstate.IRQInactive)) proof (prove)
goal (4 subgoals):
 1. cdt_list_relation (\<lambda>y. []) (\<lambda>x. None) (map_to_ctes (\<lambda>x. None))
 2. revokable_relation (\<lambda>y. True) (null_filter (caps_of_state \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>)) (map_to_ctes (\<lambda>x. None))
 3. (\<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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, ARMKernelState (\<lambda>x. None) (\<lambda>x. None) 0 (\<lambda>x. None) 0 [] (\<lambda>y. ArmVSpaceUserRegion)) \<in> arch_state_relation
 4. interrupt_state_relation (\<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits) (\<lambda>y. irq_state.IRQInactive) (InterruptState 0 (\<lambda>y. irqstate.IRQInactive)) proof (prove)
goal (3 subgoals):
 1. revokable_relation (\<lambda>y. True) (null_filter (caps_of_state \<lparr>kheap = \<lambda>x. None, cdt = \<lambda>x. None, is_original_cap = \<lambda>y. True, cur_thread = 0, idle_thread = 0, machine_state = init_machine_state, interrupt_irq_node = \<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits, interrupt_states = \<lambda>y. irq_state.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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, exst = \<lparr>work_units_completed_internal = 0, scheduler_action_internal = resume_cur_thread, ekheap_internal = \<lambda>y. None, domain_list_internal = [], domain_index_internal = 0, cur_domain_internal = 0, domain_time_internal = 0, ready_queues_internal = \<lambda>_ _. [], cdt_list_internal = \<lambda>y. []\<rparr>\<rparr>)) (map_to_ctes (\<lambda>x. None))
 2. (\<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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, ARMKernelState (\<lambda>x. None) (\<lambda>x. None) 0 (\<lambda>x. None) 0 [] (\<lambda>y. ArmVSpaceUserRegion)) \<in> arch_state_relation
 3. interrupt_state_relation (\<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits) (\<lambda>y. irq_state.IRQInactive) (InterruptState 0 (\<lambda>y. irqstate.IRQInactive)) proof (prove)
goal (2 subgoals):
 1. (\<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 = 0, arm_global_pts = [], arm_kernel_vspace = \<lambda>y. ArmVSpaceUserRegion\<rparr>, ARMKernelState (\<lambda>x. None) (\<lambda>x. None) 0 (\<lambda>x. None) 0 [] (\<lambda>y. ArmVSpaceUserRegion)) \<in> arch_state_relation
 2. interrupt_state_relation (\<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits) (\<lambda>y. irq_state.IRQInactive) (InterruptState 0 (\<lambda>y. irqstate.IRQInactive)) proof (prove)
goal (1 subgoal):
 1. interrupt_state_relation (\<lambda>irq. UCAST(10 \<rightarrow> 32) irq << cte_level_bits) (\<lambda>y. irq_state.IRQInactive) (InterruptState 0 (\<lambda>y. irqstate.IRQInactive)) proof (prove)
goal:
No subgoals!