theory Arch_R

lemma invs_asid_table_strengthen':
  "invs' s \<and> asid_pool_at' ap s \<and> asid \<le> 2 ^ asid_high_bits - 1 \<longrightarrow>
   invs' (s\<lparr>ksArchState :=
            armKSASIDTable_update (\<lambda>_. ((armKSASIDTable \<circ> ksArchState) s)(asid \<mapsto> ap)) (ksArchState s)\<rparr>)" apply (clarsimp simp: invs'_def valid_state'_def) apply (rule conjI) apply (clarsimp simp: valid_global_refs'_def global_refs'_def) apply (clarsimp simp: valid_arch_state'_def) apply (clarsimp simp: valid_asid_table'_def ran_def) apply (rule conjI) apply (clarsimp split: if_split_asm) apply fastforce apply (rule conjI) apply (clarsimp simp: valid_pspace'_def) apply (simp add: valid_machine_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<and> asid_pool_at' ap s \<and> asid \<le> 2 ^ local.asid_high_bits - 1 \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. ((armKSASIDTable \<circ> ksArchState) s)(asid \<mapsto> ap)) (ksArchState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> valid_global_refs' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) \<and> valid_arch_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> valid_global_refs' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>)
 2. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> valid_arch_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> valid_arch_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1; valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s))\<rbrakk> \<Longrightarrow> valid_asid_table' (\<lambda>a. if a = asid then Some ap else armKSASIDTable (ksArchState s) a) s \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; \<forall>a. armKSASIDTable (ksArchState s) a \<noteq> Some 0\<rbrakk> \<Longrightarrow> dom (\<lambda>a. if a = asid then Some ap else armKSASIDTable (ksArchState s) a) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> ap \<noteq> 0 \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; \<forall>a. armKSASIDTable (ksArchState s) a \<noteq> Some 0\<rbrakk> \<Longrightarrow> dom (\<lambda>a. if a = asid then Some ap else armKSASIDTable (ksArchState s) a) \<subseteq> {0..2 ^ local.asid_high_bits - 1}
 2. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; \<forall>a. armKSASIDTable (ksArchState s) a \<noteq> Some 0\<rbrakk> \<Longrightarrow> ap \<noteq> 0 \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; \<forall>a. armKSASIDTable (ksArchState s) a \<noteq> Some 0; x \<noteq> asid; armKSASIDTable (ksArchState s) x = Some y\<rbrakk> \<Longrightarrow> x \<le> 2 ^ local.asid_high_bits - 1
 2. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; \<forall>a. armKSASIDTable (ksArchState s) a \<noteq> Some 0\<rbrakk> \<Longrightarrow> ap \<noteq> 0 \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; \<forall>a. armKSASIDTable (ksArchState s) a \<noteq> Some 0\<rbrakk> \<Longrightarrow> ap \<noteq> 0 \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; \<forall>a. armKSASIDTable (ksArchState s) a \<noteq> Some 0\<rbrakk> \<Longrightarrow> ap \<noteq> 0
 2. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; \<forall>a. armKSASIDTable (ksArchState s) a \<noteq> Some 0\<rbrakk> \<Longrightarrow> valid_machine_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; asid_pool_at' ap s; asid \<le> 2 ^ local.asid_high_bits - 1; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; \<forall>a. armKSASIDTable (ksArchState s) a \<noteq> Some 0\<rbrakk> \<Longrightarrow> valid_machine_state' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(asid \<mapsto> ap)) (ksArchState s)\<rparr>) proof (prove)
goal:
No subgoals!