theory Finalise_R

lemma invalidateASIDEntry_invs' [wp]:
  "\<lbrace>invs'\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>r. invs'\<rbrace>" apply (simp add: invalidateASIDEntry_def invalidateASID_def
                   invalidateHWASIDEntry_def bind_assoc) apply (wp loadHWASID_wp | simp)+ apply (clarsimp simp: fun_upd_def[symmetric]) apply (rule conjI) apply (clarsimp simp: invs'_def valid_state'_def) apply (rule conjI) apply (simp add: valid_global_refs'_def
                     global_refs'_def) apply (simp add: valid_arch_state'_def ran_def
                    valid_asid_table'_def is_inv_None_upd
                    valid_machine_state'_def
                    comp_upd_simp fun_upd_def[symmetric]
                    inj_on_fun_upd_elsewhere
                    valid_asid_map'_def
                    ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) subgoal by (auto elim!: subset_inj_on) apply (clarsimp simp: invs'_def valid_state'_def) apply (rule conjI) apply (simp add: valid_global_refs'_def
                    global_refs'_def) apply (rule conjI) apply (simp add: valid_arch_state'_def ran_def
                    valid_asid_table'_def None_upd_eq
                    fun_upd_def[symmetric] comp_upd_simp) apply (simp add: valid_machine_state'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do maybeHWASID <- loadHWASID asid;
y <- when (\<exists>y. maybeHWASID = Some y) (do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(the maybeHWASID := None)) (ksArchState s)\<rparr>)
od);
y <- findPDForASIDAssert asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(asid := None)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<exists>y b. armKSASIDMap (ksArchState s) asid = Some (y, b)) \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_ a. if a = asid then None else armKSASIDMap (ksArchState s) a) (armKSHWASIDTable_update (\<lambda>_ a. if a = the (map_option fst (armKSASIDMap (ksArchState s) asid)) then None else armKSHWASIDTable (ksArchState s) a) (ksArchState s))\<rparr>)) \<and> (armKSASIDMap (ksArchState s) asid = None \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_ a. if a = asid then None else armKSASIDMap (ksArchState s) a) (ksArchState s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<exists>y b. armKSASIDMap (ksArchState s) asid = Some (y, b)) \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState s))(asid := None)) (armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState s))(the (map_option fst (armKSASIDMap (ksArchState s) asid)) := None)) (ksArchState s))\<rparr>)) \<and> (armKSASIDMap (ksArchState s) asid = None \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s. invs' s \<Longrightarrow> (\<exists>y b. armKSASIDMap (ksArchState s) asid = Some (y, b)) \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState s))(asid := None)) (armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState s))(the (map_option fst (armKSASIDMap (ksArchState s) asid)) := None)) (ksArchState s))\<rparr>)
 2. \<And>s. invs' s \<Longrightarrow> armKSASIDMap (ksArchState s) asid = None \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y b. \<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; armKSASIDMap (ksArchState s) asid = Some (y, b)\<rbrakk> \<Longrightarrow> valid_global_refs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState s))(asid := None)) (armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState s))(y := None)) (ksArchState s))\<rparr>) \<and> valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState s))(asid := None)) (armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState s))(y := None)) (ksArchState s))\<rparr>) \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState s))(asid := None)) (armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState s))(y := None)) (ksArchState s))\<rparr>)
 2. \<And>s. invs' s \<Longrightarrow> armKSASIDMap (ksArchState s) asid = None \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s y b. \<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; armKSASIDMap (ksArchState s) asid = Some (y, b)\<rbrakk> \<Longrightarrow> valid_global_refs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState s))(asid := None)) (armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState s))(y := None)) (ksArchState s))\<rparr>)
 2. \<And>s y b. \<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; armKSASIDMap (ksArchState s) asid = Some (y, b)\<rbrakk> \<Longrightarrow> valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState s))(asid := None)) (armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState s))(y := None)) (ksArchState s))\<rparr>) \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState s))(asid := None)) (armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState s))(y := None)) (ksArchState s))\<rparr>)
 3. \<And>s. invs' s \<Longrightarrow> armKSASIDMap (ksArchState s) asid = None \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y b. \<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; armKSASIDMap (ksArchState s) asid = Some (y, b)\<rbrakk> \<Longrightarrow> valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState s))(asid := None)) (armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState s))(y := None)) (ksArchState s))\<rparr>) \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. (armKSASIDMap (ksArchState s))(asid := None)) (armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState s))(y := None)) (ksArchState s))\<rparr>)
 2. \<And>s. invs' s \<Longrightarrow> armKSASIDMap (ksArchState s) asid = None \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y b. \<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; dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> (\<forall>a. armKSASIDTable (ksArchState s) a \<noteq> Some 0) \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))) \<and> dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; irqs_masked' s; valid_queues' s; ct_not_inQ s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) 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; armKSASIDMap (ksArchState s) asid = Some (y, b)\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s)) - {asid}) \<and> dom (armKSASIDMap (ksArchState s)) - {asid} \<subseteq> {0..mask local.asid_bits} - {0}
 2. \<And>s. invs' s \<Longrightarrow> armKSASIDMap (ksArchState s) asid = None \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (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_; dom (armKSASIDTable (ksArchState s_)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> (\<forall>a. armKSASIDTable (ksArchState s_) a \<noteq> Some 0) \<and> page_directory_at' (armKSGlobalPD (ksArchState s_)) s_ \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s_)) s_ \<and> is_inv (armKSHWASIDTable (ksArchState s_)) (map_option fst \<circ> armKSASIDMap (ksArchState s_)) \<and> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s_)) (dom (armKSASIDMap (ksArchState s_))) \<and> dom (armKSASIDMap (ksArchState s_)) \<subseteq> {0..mask local.asid_bits} - {0}; valid_irq_node' (irq_node' s_) s_; valid_irq_handlers' s_; valid_irq_states' s_; \<forall>p. pointerInUserData p s_ \<or> pointerInDeviceData p s_ \<or> underlying_memory (ksMachineState s_) p = 0; irqs_masked' s_; valid_queues' s_; ct_not_inQ s_; ksSchedulerAction s_ = ResumeCurrentThread \<longrightarrow> ksCurThread s_ = ksIdleThread s_ \<or> obj_at' (\<lambda>tcb. ksCurDomain s_ = tcbDomain tcb) (ksCurThread s_) 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_; armKSASIDMap (ksArchState s_) asid = Some (y_, b_)\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s_)) (dom (armKSASIDMap (ksArchState s_)) - {asid}) \<and> dom (armKSASIDMap (ksArchState s_)) - {asid} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> armKSASIDMap (ksArchState s) asid = None \<longrightarrow> invs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<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; armKSASIDMap (ksArchState s) asid = None\<rbrakk> \<Longrightarrow> valid_global_refs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) \<and> valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<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; armKSASIDMap (ksArchState s) asid = None\<rbrakk> \<Longrightarrow> valid_global_refs' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>)
 2. \<And>s. \<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; armKSASIDMap (ksArchState s) asid = None\<rbrakk> \<Longrightarrow> valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<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; armKSASIDMap (ksArchState s) asid = None\<rbrakk> \<Longrightarrow> valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) \<and> valid_machine_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<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; armKSASIDMap (ksArchState s) asid = None\<rbrakk> \<Longrightarrow> valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>)
 2. \<And>s. \<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; armKSASIDMap (ksArchState s) asid = None\<rbrakk> \<Longrightarrow> valid_machine_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<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; armKSASIDMap (ksArchState s) asid = None\<rbrakk> \<Longrightarrow> valid_machine_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>) proof (prove)
goal:
No subgoals!