theory ArchVSpace_AI

lemma find_free_hw_asid_invs [wp]:
  "\<lbrace>invs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>asid. invs\<rbrace>" apply (rule hoare_add_post) apply (rule find_free_hw_asid_valid_arch) apply fastforce apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def invalidate_asid_def
                   do_machine_op_def split_def
              cong: option.case_cong) apply (wp|wpc)+ apply (clarsimp simp: invs_def valid_state_def split del: if_split) apply (simp add: valid_global_refs_def global_refs_def cur_tcb_def
                   valid_irq_node_def valid_vspace_objs_arch_update
                   valid_global_objs_def valid_arch_caps_def second_level_tables_def
                   valid_table_caps_def valid_kernel_mappings_def
                   valid_machine_state_def valid_vs_lookup_arch_update) apply (elim conjE) apply (rule conjI) apply(erule use_valid[OF _ invalidateLocalTLB_ASID_valid_irq_states]) apply fastforce apply(rule conjI) apply clarsimp apply (drule use_valid) apply (rule_tac p=p in invalidateLocalTLB_ASID_underlying_memory, simp, fastforce) apply (clarsimp simp: valid_asid_map_def fun_upd_def[symmetric]
                        pd_at_asid_arch_up') apply (rule conjI, blast) apply (clarsimp simp: vspace_at_asid_def) apply (drule_tac P1 = "(=) (device_state (machine_state s))" in
    use_valid[OF _ invalidateLocalTLB_ASID_device_state_inv]) apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>asid. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'\<rbrace> find_free_hw_asid \<lbrace>?Q'\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> ?P' s
 3. \<lbrace>invs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>rv s. ?Q' rv s \<longrightarrow> invs s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<Longrightarrow> valid_arch_state s
 2. \<lbrace>invs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>rv s. valid_arch_state s \<longrightarrow> invs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>rv s. valid_arch_state s \<longrightarrow> invs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do hw_asid_table <- gets (arm_hwasid_table \<circ> arch_state);
next_asid <- gets (arm_next_asid \<circ> arch_state);
case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- do asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(the (hw_asid_table next_asid) := None)\<rparr>\<rparr>)
od;
y <- do ms <- gets machine_state;
p <- select_f (invalidateLocalTLB_ASID next_asid ms);
modify (machine_state_update (\<lambda>_. snd p))
od;
y <- do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(next_asid := None)\<rparr>\<rparr>)
od;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2
od \<lbrace>\<lambda>rv s. valid_arch_state s \<longrightarrow> invs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> (find (\<lambda>a. (arm_hwasid_table \<circ> arch_state) s a = None) (take (Suc (unat maxBound) - unat minBound) [(arm_next_asid \<circ> arch_state) s .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat ((arm_next_asid \<circ> arch_state) s)))) [minBound .e. (arm_next_asid \<circ> arch_state) s]) = None \<longrightarrow> (\<forall>x\<in>fst (invalidateLocalTLB_ASID ((arm_next_asid \<circ> arch_state) s) (machine_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>\<rparr>))). valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>)\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>))((arm_next_asid \<circ> arch_state) s := None)\<rparr>, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>)\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>))((arm_next_asid \<circ> arch_state) s := None)\<rparr>\<rparr>)\<lparr>arm_next_asid := (arm_next_asid \<circ> arch_state) s + 1\<rparr>\<rparr>) \<longrightarrow> invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>)\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>))((arm_next_asid \<circ> arch_state) s := None)\<rparr>, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>)\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>))((arm_next_asid \<circ> arch_state) s := None)\<rparr>\<rparr>)\<lparr>arm_next_asid := (arm_next_asid \<circ> arch_state) s + 1\<rparr>\<rparr>))) \<and> (\<forall>x. find (\<lambda>a. (arm_hwasid_table \<circ> arch_state) s a = None) (take (Suc (unat maxBound) - unat minBound) [(arm_next_asid \<circ> arch_state) s .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat ((arm_next_asid \<circ> arch_state) s)))) [minBound .e. (arm_next_asid \<circ> arch_state) s]) = Some x \<longrightarrow> valid_arch_state s \<longrightarrow> invs s) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> valid_global_refs (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> valid_irq_node (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> valid_irq_states (s\<lparr>machine_state := b\<rparr>) \<and> valid_machine_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> valid_vspace_objs (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> valid_arch_caps (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> valid_global_objs (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> valid_kernel_mappings (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> valid_asid_map (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cur_tcb (s\<lparr>machine_state := b\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s); valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; valid_vs_lookup s \<and> (\<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s)) \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s); valid_vso_at (arm_global_pd (arch_state s)) s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s \<and> (\<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))); \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := b\<rparr>) \<and> (\<forall>p. in_user_frame p s \<or> underlying_memory b p = 0) \<and> valid_asid_map (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := b\<rparr>) \<and> (\<forall>p. in_user_frame p s \<or> underlying_memory b p = 0) \<and> valid_asid_map (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := b\<rparr>)
 2. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory b p = 0) \<and> valid_asid_map (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := machine_state s\<rparr>)
 2. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory b p = 0) \<and> valid_asid_map (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory b p = 0) \<and> valid_asid_map (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> \<forall>p. in_user_frame p s \<or> underlying_memory b p = 0
 2. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s b p. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); underlying_memory b p \<noteq> 0\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s b p. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); underlying_memory b p \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P103 s b p\<rbrace> invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) \<lbrace>?Q103 s b p\<rbrace>
 2. \<And>s b p. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); underlying_memory b p \<noteq> 0\<rbrakk> \<Longrightarrow> ?P103 s b p (machine_state s)
 3. \<And>s b p. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); underlying_memory b p \<noteq> 0; ?Q103 s b p () b\<rbrakk> \<Longrightarrow> in_user_frame p s
 4. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := (arm_asid_map (arch_state s))(the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) := None), arm_hwasid_table := (arm_hwasid_table (arch_state s))(arm_next_asid (arch_state s) := None), arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> dom (arm_asid_map (arch_state s)) - {the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)))} \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)) - {the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)))} \<times> UNIV. case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd (s\<lparr>machine_state := b\<rparr>) \<and> asid \<noteq> 0) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := (arm_asid_map (arch_state s))(the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) := None), arm_hwasid_table := (arm_hwasid_table (arch_state s))(arm_next_asid (arch_state s) := None), arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)) - {the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)))} \<times> UNIV. case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd (s\<lparr>machine_state := b\<rparr>) \<and> asid \<noteq> 0) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := (arm_asid_map (arch_state s))(the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) := None), arm_hwasid_table := (arm_hwasid_table (arch_state s))(arm_next_asid (arch_state s) := None), arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := (arm_asid_map (arch_state s))(the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) := None), arm_hwasid_table := (arm_hwasid_table (arch_state s))(arm_next_asid (arch_state s) := None), arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> device_state (machine_state s) = device_state (machine_state s)
 2. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := (arm_asid_map (arch_state s))(the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) := None), arm_hwasid_table := (arm_hwasid_table (arch_state s))(arm_next_asid (arch_state s) := None), arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0; device_state (machine_state s) = device_state b\<rbrakk> \<Longrightarrow> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_refs (insert (idle_thread s) (insert (arm_global_pd (arch_state s)) (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))))) s; valid_arch_state s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; \<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; equal_kernel_mappings s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; valid_arch_state (s\<lparr>machine_state := b, arch_state := arch_state s\<lparr>arm_asid_map := (arm_asid_map (arch_state s))(the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) := None), arm_hwasid_table := (arm_hwasid_table (arch_state s))(arm_next_asid (arch_state s) := None), arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_vs_lookup s; valid_vso_at (arm_global_pd (arch_state s)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s); obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0; device_state (machine_state s) = device_state b\<rbrakk> \<Longrightarrow> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b), arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) then None else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a, arm_next_asid := arm_next_asid (arch_state s) + 1\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!