theory ArchVSpace_AI

lemma store_hw_asid_valid_arch:
  notes hoare_pre [wp_pre del]
  shows "\<lbrace>valid_arch_state and
    (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and>
         arm_hwasid_table (arch_state s) hw_asid = None)\<rbrace>
  store_hw_asid asid hw_asid
  \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" apply (simp add: store_hw_asid_def) apply wp apply (simp add: valid_arch_state_def fun_upd_def[symmetric] comp_upd_simp) apply (rule hoare_pre, wp) apply clarsimp apply (frule is_inv_NoneD[rotated]) apply simp apply (simp add: ran_def) apply (simp add: is_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None)\<rbrace> store_hw_asid asid hw_asid \<lbrace>\<lambda>_. valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None)\<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>_. valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None)\<rbrace> find_pd_for_asid_assert asid \<lbrace>\<lambda>pd s. 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>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_asid_table (asid_table s) s \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s \<and> valid_global_pts s \<and> is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))) and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None)\<rbrace> find_pd_for_asid_assert asid \<lbrace>\<lambda>pd s. valid_asid_table (asid_table s) s \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s \<and> valid_global_pts s \<and> is_inv ((arm_hwasid_table (arch_state s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> arm_asid_map (arch_state s))(asid \<mapsto> hw_asid))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. valid_asid_table (asid_table s) s \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s \<and> valid_global_pts s \<and> is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))) and (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> arm_hwasid_table (arch_state s) hw_asid = None)) s \<Longrightarrow> valid_asid_table (asid_table s) s \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s \<and> valid_global_pts s \<and> is_inv ((arm_hwasid_table (arch_state s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> arm_asid_map (arch_state s))(asid \<mapsto> hw_asid)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) asid = None; arm_hwasid_table (arch_state s) hw_asid = None\<rbrakk> \<Longrightarrow> is_inv ((arm_hwasid_table (arch_state s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> arm_asid_map (arch_state s))(asid \<mapsto> hw_asid)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) asid = None; arm_hwasid_table (arch_state s) hw_asid = None\<rbrakk> \<Longrightarrow> (map_option fst \<circ> arm_asid_map (arch_state s)) (?x21 s) = None
 2. \<And>s. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) asid = None; arm_hwasid_table (arch_state s) hw_asid = None; ?x21 s \<notin> ran (arm_hwasid_table (arch_state s))\<rbrakk> \<Longrightarrow> is_inv ((arm_hwasid_table (arch_state s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> arm_asid_map (arch_state s))(asid \<mapsto> hw_asid)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) asid = None; arm_hwasid_table (arch_state s) hw_asid = None; asid \<notin> ran (arm_hwasid_table (arch_state s))\<rbrakk> \<Longrightarrow> is_inv ((arm_hwasid_table (arch_state s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> arm_asid_map (arch_state s))(asid \<mapsto> hw_asid)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) asid = None; arm_hwasid_table (arch_state s) hw_asid = None; \<forall>a. arm_hwasid_table (arch_state s) a \<noteq> Some asid\<rbrakk> \<Longrightarrow> is_inv ((arm_hwasid_table (arch_state s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> arm_asid_map (arch_state s))(asid \<mapsto> hw_asid)) proof (prove)
goal:
No subgoals!