theory VSpace_R

lemma findFreeHWASID_invs_no_cicd':
  "\<lbrace>invs_no_cicd'\<rbrace> findFreeHWASID \<lbrace>\<lambda>asid. invs_no_cicd'\<rbrace>" apply (rule hoare_add_post) apply (rule findFreeHWASID_valid_arch) apply (fastforce simp: all_invs_but_ct_idle_or_in_cur_domain'_def) apply (simp add: findFreeHWASID_def invalidateHWASIDEntry_def invalidateASID_def
                   doMachineOp_def split_def
              cong: option.case_cong) apply (wp findPDForASIDAssert_pd_at_wp | wpc)+ apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_arch_state'_def
             valid_global_refs'_def global_refs'_def valid_machine_state'_def
             ct_not_inQ_def
           split del: if_split) apply (intro conjI) apply (fastforce dest: no_irq_use [OF no_irq_invalidateLocalTLB_ASID]) apply clarsimp apply (drule_tac x=p in spec) apply (drule use_valid) apply (rule_tac p=p in invalidateLocalTLB_ASID_underlying_memory) apply blast apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> findFreeHWASID \<lbrace>\<lambda>asid. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'\<rbrace> findFreeHWASID \<lbrace>?Q'\<rbrace>
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ?P' s
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> findFreeHWASID \<lbrace>\<lambda>rv s. ?Q' rv s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_arch_state' s
 2. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> findFreeHWASID \<lbrace>\<lambda>rv s. valid_arch_state' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> findFreeHWASID \<lbrace>\<lambda>rv s. valid_arch_state' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> do hwASIDTable <- gets (armKSHWASIDTable \<circ> ksArchState);
nextASID <- gets (armKSNextASID \<circ> ksArchState);
case find (\<lambda>a. hwASIDTable a = None) ([nextASID .e. maxBound] @ init [minBound .e. nextASID]) of None \<Rightarrow> do y <- do y <- findPDForASIDAssert (the (hwASIDTable nextASID));
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(the (hwASIDTable nextASID) := None)) (ksArchState s)\<rparr>)
od;
y <- do ms <- gets ksMachineState;
p <- select_f (invalidateLocalTLB_ASID nextASID ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od;
y <- do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(nextASID := None)) (ksArchState s)\<rparr>)
od;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if nextASID = maxBound then minBound else nextASID + 1) (ksArchState s)\<rparr>);
return nextASID
od | Some x2 \<Rightarrow> return x2
od \<lbrace>\<lambda>rv s. valid_arch_state' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) s .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) s]) = None \<longrightarrow> (\<forall>pd. pd_at_asid' pd (the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s))) s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s))})) \<longrightarrow> (\<forall>x\<in>fst (invalidateLocalTLB_ASID ((armKSNextASID \<circ> ksArchState) s) (ksMachineState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s)\<rparr>))). valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x, ksArchState := armKSHWASIDTable_update (\<lambda>_. ((armKSHWASIDTable \<circ> ksArchState) (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x\<rparr>))((armKSNextASID \<circ> ksArchState) s := None)) (ksArchState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x\<rparr>)), ksArchState := armKSNextASID_update (\<lambda>_. if (armKSNextASID \<circ> ksArchState) s = maxBound then minBound else (armKSNextASID \<circ> ksArchState) s + 1) (ksArchState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x, ksArchState := armKSHWASIDTable_update (\<lambda>_. ((armKSHWASIDTable \<circ> ksArchState) (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x\<rparr>))((armKSNextASID \<circ> ksArchState) s := None)) (ksArchState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x\<rparr>))\<rparr>))\<rparr>) \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x, ksArchState := armKSHWASIDTable_update (\<lambda>_. ((armKSHWASIDTable \<circ> ksArchState) (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x\<rparr>))((armKSNextASID \<circ> ksArchState) s := None)) (ksArchState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x\<rparr>)), ksArchState := armKSNextASID_update (\<lambda>_. if (armKSNextASID \<circ> ksArchState) s = maxBound then minBound else (armKSNextASID \<circ> ksArchState) s + 1) (ksArchState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x, ksArchState := armKSHWASIDTable_update (\<lambda>_. ((armKSHWASIDTable \<circ> ksArchState) (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x\<rparr>))((armKSNextASID \<circ> ksArchState) s := None)) (ksArchState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(the ((armKSHWASIDTable \<circ> ksArchState) s ((armKSNextASID \<circ> ksArchState) s)) := None)) (ksArchState s), ksMachineState := snd x\<rparr>))\<rparr>))\<rparr>)))) \<and> (\<forall>x. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) s .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) s]) = Some x \<longrightarrow> valid_arch_state' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) proof (prove)
goal (1 subgoal):
 1. \<And>s pd 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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)\<rbrakk> \<Longrightarrow> valid_irq_masks' (intStateIRQTable (ksInterruptState s)) (irq_masks b) \<and> (\<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory b p = 0) proof (prove)
goal (2 subgoals):
 1. \<And>s pd 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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)\<rbrakk> \<Longrightarrow> valid_irq_masks' (intStateIRQTable (ksInterruptState s)) (irq_masks b)
 2. \<And>s pd 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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)\<rbrakk> \<Longrightarrow> \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory b p = 0 proof (prove)
goal (1 subgoal):
 1. \<And>s pd 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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)\<rbrakk> \<Longrightarrow> \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory b p = 0 proof (prove)
goal (1 subgoal):
 1. \<And>s pd b p. \<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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a); \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (1 subgoal):
 1. \<And>s pd b p. \<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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a); \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s pd b p. \<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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a); \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P110 s pd b p\<rbrace> invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) \<lbrace>?Q110 s pd b p\<rbrace>
 2. \<And>s pd b p. \<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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a); \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> ?P110 s pd b p (ksMachineState s)
 3. \<And>s pd b p. \<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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a); \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; ?Q110 s pd b p () b\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (2 subgoals):
 1. \<And>s pd b p. \<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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a); \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0\<rbrakk> \<Longrightarrow> underlying_memory (ksMachineState s) p = ?um114 s pd b p
 2. \<And>s pd b p. \<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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a); \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; underlying_memory b p = ?um114 s pd b p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (1 subgoal):
 1. \<And>s pd b p. \<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_refs' kernel_data_refs (ctes_of s); ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); 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)); valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; cur_tcb' s; valid_queues' s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (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; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; pd_at_asid' pd (the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))) s; pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))})); is_inv (\<lambda>a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a)); valid_asid_map' (\<lambda>a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a); \<not> pointerInUserData p s; underlying_memory b p \<noteq> 0; pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; underlying_memory b p = underlying_memory (ksMachineState s) p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!