theory ArchVSpace_AI

lemma store_hw_asid_invs:
  "\<lbrace>invs and
   (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and>
        arm_hwasid_table (arch_state s) hw_asid = None \<and>
        asid \<le> mask asid_bits)\<rbrace>
  store_hw_asid asid hw_asid
  \<lbrace>\<lambda>x. invs\<rbrace>" apply (rule hoare_add_post) apply (rule store_hw_asid_valid_arch) apply fastforce apply (simp add: store_hw_asid_def) apply (wp find_pd_for_asid_assert_wp) apply (clarsimp simp: invs_def valid_state_def) apply (simp add: valid_global_refs_def global_refs_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 (simp add: valid_asid_map_def fun_upd_def[symmetric]
                   pd_at_asid_arch_up) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None \<and> asid \<le> mask local.asid_bits)\<rbrace> store_hw_asid asid hw_asid \<lbrace>\<lambda>x. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'\<rbrace> store_hw_asid asid hw_asid \<lbrace>?Q'\<rbrace>
 2. \<And>s. (invs and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?P' s
 3. \<lbrace>invs and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None \<and> asid \<le> mask local.asid_bits)\<rbrace> store_hw_asid asid hw_asid \<lbrace>\<lambda>rv s. ?Q' rv s \<longrightarrow> invs s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None)) s
 2. \<lbrace>invs and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None \<and> asid \<le> mask local.asid_bits)\<rbrace> store_hw_asid asid hw_asid \<lbrace>\<lambda>rv s. valid_arch_state s \<longrightarrow> invs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None \<and> asid \<le> mask local.asid_bits)\<rbrace> store_hw_asid asid hw_asid \<lbrace>\<lambda>rv s. valid_arch_state s \<longrightarrow> invs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None \<and> asid \<le> mask local.asid_bits)\<rbrace> do pd <- find_pd_for_asid_assert asid;
asid_map <- gets (arm_asid_map \<circ> arch_state);
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(asid \<mapsto> (hw_asid, pd))\<rparr>\<rparr>);
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(hw_asid \<mapsto> asid)\<rparr>\<rparr>)
od \<lbrace>\<lambda>rv s. valid_arch_state s \<longrightarrow> invs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> \<forall>pd. vspace_at_asid asid pd s \<and> asid \<noteq> 0 \<longrightarrow> valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid \<mapsto> (hw_asid, pd))\<rparr>, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid \<mapsto> (hw_asid, pd))\<rparr>\<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)(asid \<mapsto> (hw_asid, pd))\<rparr>\<rparr>))(hw_asid \<mapsto> asid)\<rparr>\<rparr>) \<longrightarrow> invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid \<mapsto> (hw_asid, pd))\<rparr>, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid \<mapsto> (hw_asid, pd))\<rparr>\<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)(asid \<mapsto> (hw_asid, pd))\<rparr>\<rparr>))(hw_asid \<mapsto> asid)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<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; arm_asid_map (arch_state s) asid = None; arm_hwasid_table (arch_state s) hw_asid = None; asid \<le> mask local.asid_bits; vspace_at_asid asid pd s; asid \<noteq> 0; valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = asid then Some (hw_asid, pd) else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = hw_asid then Some asid else arm_hwasid_table (arch_state s) a\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> valid_global_refs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = asid then Some (hw_asid, pd) else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = hw_asid then Some asid else arm_hwasid_table (arch_state s) a\<rparr>\<rparr>) \<and> valid_irq_node (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = asid then Some (hw_asid, pd) else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = hw_asid then Some asid else arm_hwasid_table (arch_state s) a\<rparr>\<rparr>) \<and> valid_machine_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = asid then Some (hw_asid, pd) else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = hw_asid then Some asid else arm_hwasid_table (arch_state s) a\<rparr>\<rparr>) \<and> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = asid then Some (hw_asid, pd) else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = hw_asid then Some asid else arm_hwasid_table (arch_state s) a\<rparr>\<rparr>) \<and> valid_arch_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = asid then Some (hw_asid, pd) else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = hw_asid then Some asid else arm_hwasid_table (arch_state s) a\<rparr>\<rparr>) \<and> valid_global_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = asid then Some (hw_asid, pd) else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = hw_asid then Some asid else arm_hwasid_table (arch_state s) a\<rparr>\<rparr>) \<and> valid_kernel_mappings (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = asid then Some (hw_asid, pd) else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = hw_asid then Some asid else arm_hwasid_table (arch_state s) a\<rparr>\<rparr>) \<and> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = asid then Some (hw_asid, pd) else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = hw_asid then Some asid else arm_hwasid_table (arch_state s) a\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<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; cur_tcb s; arm_asid_map (arch_state s) asid = None; arm_hwasid_table (arch_state s) hw_asid = None; asid \<le> mask local.asid_bits; vspace_at_asid asid pd s; asid \<noteq> 0; valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = asid then Some (hw_asid, pd) else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = hw_asid then Some asid else arm_hwasid_table (arch_state s) a\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := \<lambda>a. if a = asid then Some (hw_asid, pd) else arm_asid_map (arch_state s) a, arm_hwasid_table := \<lambda>a. if a = hw_asid then Some asid else arm_hwasid_table (arch_state s) a\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!