theory VSpace_R

lemma storeHWASID_valid_arch' [wp]:
  "\<lbrace>valid_arch_state' and
    (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and>
         armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace>
  storeHWASID asid hw_asid
  \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" supply image_cong_simp [cong del] apply (simp add: storeHWASID_def) apply wp prefer 2 apply assumption apply (simp add: valid_arch_state'_def comp_upd_simp fun_upd_def[symmetric]) apply wp apply (simp add: findPDForASIDAssert_def const_def
                    checkPDUniqueToASID_def checkPDASIDMapMembership_def) apply wp apply (rule_tac Q'="\<lambda>rv s. valid_asid_map' (armKSASIDMap (ksArchState s))
                                \<and> asid \<noteq> 0 \<and> asid \<le> mask asid_bits"
              in hoare_post_imp_R) apply (wp findPDForASID_inv2)+ apply (clarsimp simp: valid_asid_map'_def) apply (subst conj_commute, rule context_conjI) apply clarsimp apply (rule ccontr, erule notE, rule_tac a=x in ranI) apply (simp add: restrict_map_def) apply (erule(1) inj_on_fun_updI2) apply clarsimp apply (frule is_inv_NoneD[rotated], 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. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace> storeHWASID asid hw_asid \<lbrace>\<lambda>_. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace> storeHWASID asid hw_asid \<lbrace>\<lambda>_. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace> do pd <- findPDForASIDAssert asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>);
hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(hw_asid \<mapsto> asid)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>_. valid_arch_state'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s), ksArchState := armKSHWASIDTable_update (\<lambda>_. ((armKSHWASIDTable \<circ> ksArchState) (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>))(hw_asid \<mapsto> asid)) (ksArchState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>))\<rparr>)\<rbrace>
 2. \<And>s. (valid_arch_state' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_arch_state' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)) s \<Longrightarrow> ?Q s
 2. \<lbrace>?Q\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s), ksArchState := armKSHWASIDTable_update (\<lambda>_. ((armKSHWASIDTable \<circ> ksArchState) (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>))(hw_asid \<mapsto> asid)) (ksArchState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>))\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s), ksArchState := armKSHWASIDTable_update (\<lambda>_. ((armKSHWASIDTable \<circ> ksArchState) (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>))(hw_asid \<mapsto> asid)) (ksArchState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>))\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>pd s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> valid_asid_map' ((armKSASIDMap (ksArchState s))(asid \<mapsto> (hw_asid, pd)))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'18\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>rv s. valid_asid_map' ((armKSASIDMap (ksArchState s))(asid \<mapsto> (hw_asid, rv)))\<rbrace>
 2. \<And>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None \<Longrightarrow> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> ?P'18 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'18\<rbrace> do pd <- findPDForASID asid <catch> (\<lambda>y. fail);
y <- assert (pd && mask pdBits = 0);
y <- checkPDAt pd;
y <- stateAssert (\<lambda>s. pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid}))) [];
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pd = xa);
return pd
od \<lbrace>\<lambda>rv s. valid_asid_map' ((armKSASIDMap (ksArchState s))(asid \<mapsto> (hw_asid, rv)))\<rbrace>
 2. \<And>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None \<Longrightarrow> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> ?P'18 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'44\<rbrace> findPDForASID asid \<lbrace>\<lambda>pd s. pd && mask pdBits = 0 \<longrightarrow> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})) \<longrightarrow> (case (armKSASIDMap \<circ> ksArchState) s asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pd = xa) \<longrightarrow> valid_asid_map' ((armKSASIDMap (ksArchState s))(asid \<mapsto> (hw_asid, pd)))\<rbrace>, -
 2. \<And>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None \<Longrightarrow> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> True \<and> ?P'44 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'44\<rbrace> findPDForASID asid \<lbrace>\<lambda>rv s. valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits\<rbrace>, -
 2. \<And>rv s. valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<Longrightarrow> rv && mask pdBits = 0 \<longrightarrow> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})) \<longrightarrow> (case (armKSASIDMap \<circ> ksArchState) s asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> rv = xa) \<longrightarrow> valid_asid_map' ((armKSASIDMap (ksArchState s))(asid \<mapsto> (hw_asid, rv)))
 3. \<And>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None \<Longrightarrow> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> True \<and> ?P'44 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<Longrightarrow> rv && mask pdBits = 0 \<longrightarrow> rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})) \<longrightarrow> (case (armKSASIDMap \<circ> ksArchState) s asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> rv = xa) \<longrightarrow> valid_asid_map' ((armKSASIDMap (ksArchState s))(asid \<mapsto> (hw_asid, rv)))
 2. \<And>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None \<Longrightarrow> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> True \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> valid_asid_map' (armKSASIDMap (ksArchState s))) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<noteq> 0) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<le> mask local.asid_bits) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; asid \<noteq> 0; asid \<le> mask local.asid_bits; rv && mask pdBits = 0; rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> rv = xa\<rbrakk> \<Longrightarrow> inj_on ((map_option snd \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> rv)) (dom (armKSASIDMap (ksArchState s))) \<and> Some rv \<notin> (map_option snd \<circ> armKSASIDMap (ksArchState s)) ` (dom (armKSASIDMap (ksArchState s)) - {asid})
 2. \<And>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None \<Longrightarrow> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> True \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> valid_asid_map' (armKSASIDMap (ksArchState s))) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<noteq> 0) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<le> mask local.asid_bits) proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; asid \<noteq> 0; asid \<le> mask local.asid_bits; rv && mask pdBits = 0; rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> rv = xa\<rbrakk> \<Longrightarrow> Some rv \<notin> (map_option snd \<circ> armKSASIDMap (ksArchState s)) ` (dom (armKSASIDMap (ksArchState s)) - {asid})
 2. \<And>rv s. \<lbrakk>inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; asid \<noteq> 0; asid \<le> mask local.asid_bits; rv && mask pdBits = 0; rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> rv = xa; Some rv \<notin> (map_option snd \<circ> armKSASIDMap (ksArchState s)) ` (dom (armKSASIDMap (ksArchState s)) - {asid})\<rbrakk> \<Longrightarrow> inj_on ((map_option snd \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> rv)) (dom (armKSASIDMap (ksArchState s)))
 3. \<And>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None \<Longrightarrow> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> True \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> valid_asid_map' (armKSASIDMap (ksArchState s))) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<noteq> 0) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<le> mask local.asid_bits) proof (prove)
goal (3 subgoals):
 1. \<And>s x a b. \<lbrakk>inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; asid \<noteq> 0; asid \<le> mask local.asid_bits; b && mask pdBits = 0; b \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> b = xa; armKSASIDMap (ksArchState s) x = Some (a, b)\<rbrakk> \<Longrightarrow> x = asid
 2. \<And>rv s. \<lbrakk>inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; asid \<noteq> 0; asid \<le> mask local.asid_bits; rv && mask pdBits = 0; rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> rv = xa; Some rv \<notin> (map_option snd \<circ> armKSASIDMap (ksArchState s)) ` (dom (armKSASIDMap (ksArchState s)) - {asid})\<rbrakk> \<Longrightarrow> inj_on ((map_option snd \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> rv)) (dom (armKSASIDMap (ksArchState s)))
 3. \<And>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None \<Longrightarrow> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> True \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> valid_asid_map' (armKSASIDMap (ksArchState s))) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<noteq> 0) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<le> mask local.asid_bits) proof (prove)
goal (3 subgoals):
 1. \<And>s x a b. \<lbrakk>inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; asid \<noteq> 0; asid \<le> mask local.asid_bits; b && mask pdBits = 0; case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> b = xa; armKSASIDMap (ksArchState s) x = Some (a, b); x \<noteq> asid\<rbrakk> \<Longrightarrow> (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})) x = Some b
 2. \<And>rv s. \<lbrakk>inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; asid \<noteq> 0; asid \<le> mask local.asid_bits; rv && mask pdBits = 0; rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> rv = xa; Some rv \<notin> (map_option snd \<circ> armKSASIDMap (ksArchState s)) ` (dom (armKSASIDMap (ksArchState s)) - {asid})\<rbrakk> \<Longrightarrow> inj_on ((map_option snd \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> rv)) (dom (armKSASIDMap (ksArchState s)))
 3. \<And>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None \<Longrightarrow> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> True \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> valid_asid_map' (armKSASIDMap (ksArchState s))) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<noteq> 0) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<le> mask local.asid_bits) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; asid \<noteq> 0; asid \<le> mask local.asid_bits; rv && mask pdBits = 0; rv \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})); case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> rv = xa; Some rv \<notin> (map_option snd \<circ> armKSASIDMap (ksArchState s)) ` (dom (armKSASIDMap (ksArchState s)) - {asid})\<rbrakk> \<Longrightarrow> inj_on ((map_option snd \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> rv)) (dom (armKSASIDMap (ksArchState s)))
 2. \<And>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None \<Longrightarrow> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> True \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> valid_asid_map' (armKSASIDMap (ksArchState s))) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<noteq> 0) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<le> mask local.asid_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None \<Longrightarrow> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) \<and> True \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> valid_asid_map' (armKSASIDMap (ksArchState s))) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<noteq> 0) \<and> (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits \<longrightarrow> asid \<le> mask local.asid_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); armKSASIDMap (ksArchState s) asid = None; armKSHWASIDTable (ksArchState s) hw_asid = None\<rbrakk> \<Longrightarrow> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); armKSASIDMap (ksArchState s) asid = None; armKSHWASIDTable (ksArchState s) hw_asid = None; asid \<notin> ran (armKSHWASIDTable (ksArchState s))\<rbrakk> \<Longrightarrow> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); armKSASIDMap (ksArchState s) asid = None; armKSHWASIDTable (ksArchState s) hw_asid = None; \<forall>a. armKSHWASIDTable (ksArchState s) a \<noteq> Some asid\<rbrakk> \<Longrightarrow> is_inv ((armKSHWASIDTable (ksArchState s))(hw_asid \<mapsto> asid)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(asid \<mapsto> hw_asid)) proof (prove)
goal:
No subgoals!