theory Example_Valid_State

lemma valid_arch_state_s0[simp]:
  "valid_arch_state s0_internal" apply (clarsimp simp: valid_arch_state_def s0_internal_def arch_state0_def) apply (intro conjI) apply (clarsimp simp: obj_at_def kh0_def) apply (simp add: valid_asid_table_def) apply (clarsimp simp: obj_at_def kh0_def a_type_def) apply (simp add: valid_global_pts_def) apply (simp add: is_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state s0_internal proof (prove)
goal (1 subgoal):
 1. valid_asid_table (\<lambda>x. None) \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr> \<and> typ_at (AArch APageDirectory) init_global_pd \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr> \<and> valid_global_pts \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr> \<and> is_inv (\<lambda>x. None) (\<lambda>x. None) proof (prove)
goal (4 subgoals):
 1. valid_asid_table (\<lambda>x. None) \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr>
 2. typ_at (AArch APageDirectory) init_global_pd \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr>
 3. valid_global_pts \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr>
 4. is_inv (\<lambda>x. None) (\<lambda>x. None) proof (prove)
goal (4 subgoals):
 1. valid_asid_table (\<lambda>x. None) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> Low_cnode, High_cnode_ptr \<mapsto> High_cnode, Silc_cnode_ptr \<mapsto> Silc_cnode, ntfn_ptr \<mapsto> ntfn, irq_cnode_ptr \<mapsto> irq_cnode, Low_pd_ptr \<mapsto> Low_pd, High_pd_ptr \<mapsto> High_pd, Low_pt_ptr \<mapsto> Low_pt, High_pt_ptr \<mapsto> High_pt, Low_tcb_ptr \<mapsto> Low_tcb, High_tcb_ptr \<mapsto> High_tcb, idle_tcb_ptr \<mapsto> idle_tcb, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr>
 2. typ_at (AArch APageDirectory) init_global_pd \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr>
 3. valid_global_pts \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr>
 4. is_inv (\<lambda>x. None) (\<lambda>x. None) proof (prove)
goal (3 subgoals):
 1. typ_at (AArch APageDirectory) init_global_pd \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr>
 2. valid_global_pts \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr>
 3. is_inv (\<lambda>x. None) (\<lambda>x. None) proof (prove)
goal (2 subgoals):
 1. valid_global_pts \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), 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 = init_global_pd, 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 = exst0\<rparr>
 2. is_inv (\<lambda>x. None) (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. is_inv (\<lambda>x. None) (\<lambda>x. None) proof (prove)
goal:
No subgoals!