theory VSpace_R

lemma findFreeHWASID_valid_arch [wp]:
  "\<lbrace>valid_arch_state'\<rbrace> findFreeHWASID \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" apply (simp add: findFreeHWASID_def invalidateHWASIDEntry_def
                   invalidateASID_def doMachineOp_def split_def
              cong: option.case_cong) apply (wp|wpc|simp split del: if_split)+ apply (clarsimp simp: valid_arch_state'_def fun_upd_def[symmetric]
                        comp_upd_simp valid_asid_map'_def) apply (frule is_inv_inj) apply (drule findNoneD) apply (drule_tac x="armKSNextASID (ksArchState s)" in bspec) apply clarsimp apply (clarsimp simp: is_inv_def ran_upd[folded fun_upd_def]
                        dom_option_map inj_on_fun_upd_elsewhere) apply (rule conjI) apply clarsimp apply (drule_tac x="x" and y="armKSNextASID (ksArchState s)" in inj_onD) apply simp apply blast apply blast apply simp apply (rule conjI) apply (erule subset_inj_on, clarsimp) apply (erule order_trans[rotated]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> findFreeHWASID \<lbrace>\<lambda>_. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> do hwASIDTable <- gets (armKSHWASIDTable \<circ> ksArchState);
nextASID <- gets (armKSNextASID \<circ> ksArchState);
case find (\<lambda>a. hwASIDTable a = None) ([nextASID .e. maxBound] @ init [minBound .e. nextASID]) of None \<Rightarrow> do y <- do y <- findPDForASIDAssert (the (hwASIDTable nextASID));
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(the (hwASIDTable nextASID) := None)) (ksArchState s)\<rparr>)
od;
y <- do ms <- gets ksMachineState;
p <- select_f (invalidateLocalTLB_ASID nextASID ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od;
y <- do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(nextASID := None)) (ksArchState s)\<rparr>)
od;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if nextASID = maxBound then minBound else nextASID + 1) (ksArchState s)\<rparr>);
return nextASID
od | Some x2 \<Rightarrow> return x2
od \<lbrace>\<lambda>_. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_arch_state' s \<Longrightarrow> find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None \<longrightarrow> (\<forall>x\<in>fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)). valid_arch_state' (s\<lparr>ksMachineState := snd x, ksArchState := armKSNextASID_update (\<lambda>_. if armKSNextASID (ksArchState s) = maxBound then minBound else (armKSNextASID \<circ> ksArchState) s + 1) (armKSHWASIDTable_update (\<lambda>_ a. if a = armKSNextASID (ksArchState s) then None else armKSHWASIDTable (ksArchState s) a) (armKSASIDMap_update (\<lambda>_ a. if a = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) a) (ksArchState s)))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<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)); inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s))\<rbrakk> \<Longrightarrow> is_inv ((armKSHWASIDTable (ksArchState s))(armKSNextASID (ksArchState s) := None)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) := None)) \<and> inj_on ((map_option snd \<circ> armKSASIDMap (ksArchState s))(the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) := None)) (dom (armKSASIDMap (ksArchState s)) - {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))}) \<and> dom (armKSASIDMap (ksArchState s)) - {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<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)); inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s)))\<rbrakk> \<Longrightarrow> is_inv ((armKSHWASIDTable (ksArchState s))(armKSNextASID (ksArchState s) := None)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) := None)) \<and> inj_on ((map_option snd \<circ> armKSASIDMap (ksArchState s))(the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) := None)) (dom (armKSASIDMap (ksArchState s)) - {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))}) \<and> dom (armKSASIDMap (ksArchState s)) - {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<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)); inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); \<forall>x\<in>set ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]). armKSHWASIDTable (ksArchState s) x \<noteq> None\<rbrakk> \<Longrightarrow> is_inv ((armKSHWASIDTable (ksArchState s))(armKSNextASID (ksArchState s) := None)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) := None)) \<and> inj_on ((map_option snd \<circ> armKSASIDMap (ksArchState s))(the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) := None)) (dom (armKSASIDMap (ksArchState s)) - {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))}) \<and> dom (armKSASIDMap (ksArchState s)) - {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<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)); inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s)))\<rbrakk> \<Longrightarrow> armKSNextASID (ksArchState s) \<in> set ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)])
 2. \<And>s b. \<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)); inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) \<noteq> None\<rbrakk> \<Longrightarrow> is_inv ((armKSHWASIDTable (ksArchState s))(armKSNextASID (ksArchState s) := None)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) := None)) \<and> inj_on ((map_option snd \<circ> armKSASIDMap (ksArchState s))(the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) := None)) (dom (armKSASIDMap (ksArchState s)) - {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))}) \<and> dom (armKSASIDMap (ksArchState s)) - {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<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)); inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) \<noteq> None\<rbrakk> \<Longrightarrow> is_inv ((armKSHWASIDTable (ksArchState s))(armKSNextASID (ksArchState s) := None)) ((map_option fst \<circ> armKSASIDMap (ksArchState s))(the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) := None)) \<and> inj_on ((map_option snd \<circ> armKSASIDMap (ksArchState s))(the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) := None)) (dom (armKSASIDMap (ksArchState s)) - {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))}) \<and> dom (armKSASIDMap (ksArchState s)) - {the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)))} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (1 subgoal):
 1. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> (\<forall>x. x \<noteq> armKSNextASID (ksArchState s) \<longrightarrow> armKSHWASIDTable (ksArchState s) x \<noteq> Some y) \<and> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s)) - {y}) \<and> dom (armKSASIDMap (ksArchState s)) - {y} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (2 subgoals):
 1. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> \<forall>x. x \<noteq> armKSNextASID (ksArchState s) \<longrightarrow> armKSHWASIDTable (ksArchState s) x \<noteq> Some y
 2. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s)) - {y}) \<and> dom (armKSASIDMap (ksArchState s)) - {y} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (2 subgoals):
 1. \<And>s b y x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b)); x \<noteq> armKSNextASID (ksArchState s); armKSHWASIDTable (ksArchState s) x = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s)) - {y}) \<and> dom (armKSASIDMap (ksArchState s)) - {y} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (5 subgoals):
 1. \<And>s b y x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b)); x \<noteq> armKSNextASID (ksArchState s); armKSHWASIDTable (ksArchState s) x = Some y\<rbrakk> \<Longrightarrow> armKSHWASIDTable (ksArchState s) x = armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))
 2. \<And>s b y x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b)); x \<noteq> armKSNextASID (ksArchState s); armKSHWASIDTable (ksArchState s) x = Some y\<rbrakk> \<Longrightarrow> x \<in> dom (armKSHWASIDTable (ksArchState s))
 3. \<And>s b y x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b)); x \<noteq> armKSNextASID (ksArchState s); armKSHWASIDTable (ksArchState s) x = Some y\<rbrakk> \<Longrightarrow> armKSNextASID (ksArchState s) \<in> dom (armKSHWASIDTable (ksArchState s))
 4. \<And>s b y x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b)); x \<noteq> armKSNextASID (ksArchState s); armKSHWASIDTable (ksArchState s) x = Some y; x = armKSNextASID (ksArchState s)\<rbrakk> \<Longrightarrow> False
 5. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s)) - {y}) \<and> dom (armKSASIDMap (ksArchState s)) - {y} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (4 subgoals):
 1. \<And>s b y x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b)); x \<noteq> armKSNextASID (ksArchState s); armKSHWASIDTable (ksArchState s) x = Some y\<rbrakk> \<Longrightarrow> x \<in> dom (armKSHWASIDTable (ksArchState s))
 2. \<And>s b y x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b)); x \<noteq> armKSNextASID (ksArchState s); armKSHWASIDTable (ksArchState s) x = Some y\<rbrakk> \<Longrightarrow> armKSNextASID (ksArchState s) \<in> dom (armKSHWASIDTable (ksArchState s))
 3. \<And>s b y x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b)); x \<noteq> armKSNextASID (ksArchState s); armKSHWASIDTable (ksArchState s) x = Some y; x = armKSNextASID (ksArchState s)\<rbrakk> \<Longrightarrow> False
 4. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s)) - {y}) \<and> dom (armKSASIDMap (ksArchState s)) - {y} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (3 subgoals):
 1. \<And>s b y x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b)); x \<noteq> armKSNextASID (ksArchState s); armKSHWASIDTable (ksArchState s) x = Some y\<rbrakk> \<Longrightarrow> armKSNextASID (ksArchState s) \<in> dom (armKSHWASIDTable (ksArchState s))
 2. \<And>s b y x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b)); x \<noteq> armKSNextASID (ksArchState s); armKSHWASIDTable (ksArchState s) x = Some y; x = armKSNextASID (ksArchState s)\<rbrakk> \<Longrightarrow> False
 3. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s)) - {y}) \<and> dom (armKSASIDMap (ksArchState s)) - {y} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (2 subgoals):
 1. \<And>s b y x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b)); x \<noteq> armKSNextASID (ksArchState s); armKSHWASIDTable (ksArchState s) x = Some y; x = armKSNextASID (ksArchState s)\<rbrakk> \<Longrightarrow> False
 2. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s)) - {y}) \<and> dom (armKSASIDMap (ksArchState s)) - {y} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (1 subgoal):
 1. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s)) - {y}) \<and> dom (armKSASIDMap (ksArchState s)) - {y} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (2 subgoals):
 1. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s)) - {y})
 2. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> dom (armKSASIDMap (ksArchState s)) - {y} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (1 subgoal):
 1. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> dom (armKSASIDMap (ksArchState s)) - {y} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal (1 subgoal):
 1. \<And>s b y. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s)); inj_on (armKSHWASIDTable (ksArchState s)) (dom (armKSHWASIDTable (ksArchState s))); armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s)) = Some y; ran (armKSHWASIDTable (ksArchState s)) = dom (armKSASIDMap (ksArchState s)); \<forall>x y. armKSHWASIDTable (ksArchState s) x = Some y \<longrightarrow> (\<exists>b. armKSASIDMap (ksArchState s) y = Some (x, b))\<rbrakk> \<Longrightarrow> dom (armKSASIDMap (ksArchState s)) - {y} \<subseteq> dom (armKSASIDMap (ksArchState s)) proof (prove)
goal:
No subgoals!