theory ArchVSpace_AI

lemma find_free_hw_asid_valid_arch [wp]:
  "\<lbrace>valid_arch_state\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" 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|simp)+ apply (clarsimp simp: valid_arch_state_def) apply (frule is_inv_inj) apply (drule findNoneD) apply (drule_tac x="arm_next_asid (arch_state s)" in bspec) apply (simp add: minBound_word) apply (clarsimp simp: is_inv_def ran_upd dom_option_map
                        dom_upd) apply (drule_tac x="x" and y="arm_next_asid (arch_state s)" in inj_onD) apply simp apply blast apply blast apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<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>_. valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_arch_state s \<Longrightarrow> 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 \<longrightarrow> (\<forall>x\<in>fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)). valid_arch_state (s\<lparr>machine_state := snd x, 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_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)); 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))\<rbrakk> \<Longrightarrow> is_inv (\<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a) (map_option fst \<circ> (\<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)) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<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)); 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)); inj_on (arm_hwasid_table (arch_state s)) (dom (arm_hwasid_table (arch_state s)))\<rbrakk> \<Longrightarrow> is_inv (\<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a) (map_option fst \<circ> (\<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)) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<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)); ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); inj_on (arm_hwasid_table (arch_state s)) (dom (arm_hwasid_table (arch_state s))); \<forall>x\<in>set (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)]). arm_hwasid_table (arch_state s) x \<noteq> None\<rbrakk> \<Longrightarrow> is_inv (\<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a) (map_option fst \<circ> (\<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)) proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<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)); ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); inj_on (arm_hwasid_table (arch_state s)) (dom (arm_hwasid_table (arch_state s)))\<rbrakk> \<Longrightarrow> arm_next_asid (arch_state s) \<in> set (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)])
 2. \<And>s b. \<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)); ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); inj_on (arm_hwasid_table (arch_state s)) (dom (arm_hwasid_table (arch_state s))); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) \<noteq> None\<rbrakk> \<Longrightarrow> is_inv (\<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a) (map_option fst \<circ> (\<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)) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<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)); ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); inj_on (arm_hwasid_table (arch_state s)) (dom (arm_hwasid_table (arch_state s))); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) \<noteq> None\<rbrakk> \<Longrightarrow> is_inv (\<lambda>a. if a = arm_next_asid (arch_state s) then None else arm_hwasid_table (arch_state s) a) (map_option fst \<circ> (\<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)) proof (prove)
goal (1 subgoal):
 1. \<And>s b y x. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); inj_on (arm_hwasid_table (arch_state s)) (dom (arm_hwasid_table (arch_state s))); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; ran (arm_hwasid_table (arch_state s)) = dom (arm_asid_map (arch_state s)); \<forall>x y. arm_hwasid_table (arch_state s) x = Some y \<longrightarrow> (\<exists>b. arm_asid_map (arch_state s) y = Some (x, b)); x \<noteq> arm_next_asid (arch_state s); arm_hwasid_table (arch_state s) x = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s b y x. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; ran (arm_hwasid_table (arch_state s)) = dom (arm_asid_map (arch_state s)); \<forall>x y. arm_hwasid_table (arch_state s) x = Some y \<longrightarrow> (\<exists>b. arm_asid_map (arch_state s) y = Some (x, b)); x \<noteq> arm_next_asid (arch_state s); arm_hwasid_table (arch_state s) x = Some y\<rbrakk> \<Longrightarrow> arm_hwasid_table (arch_state s) x = arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))
 2. \<And>s b y x. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; ran (arm_hwasid_table (arch_state s)) = dom (arm_asid_map (arch_state s)); \<forall>x y. arm_hwasid_table (arch_state s) x = Some y \<longrightarrow> (\<exists>b. arm_asid_map (arch_state s) y = Some (x, b)); x \<noteq> arm_next_asid (arch_state s); arm_hwasid_table (arch_state s) x = Some y\<rbrakk> \<Longrightarrow> x \<in> dom (arm_hwasid_table (arch_state s))
 3. \<And>s b y x. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; ran (arm_hwasid_table (arch_state s)) = dom (arm_asid_map (arch_state s)); \<forall>x y. arm_hwasid_table (arch_state s) x = Some y \<longrightarrow> (\<exists>b. arm_asid_map (arch_state s) y = Some (x, b)); x \<noteq> arm_next_asid (arch_state s); arm_hwasid_table (arch_state s) x = Some y\<rbrakk> \<Longrightarrow> arm_next_asid (arch_state s) \<in> dom (arm_hwasid_table (arch_state s))
 4. \<And>s b y x. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; ran (arm_hwasid_table (arch_state s)) = dom (arm_asid_map (arch_state s)); \<forall>x y. arm_hwasid_table (arch_state s) x = Some y \<longrightarrow> (\<exists>b. arm_asid_map (arch_state s) y = Some (x, b)); x \<noteq> arm_next_asid (arch_state s); arm_hwasid_table (arch_state s) x = Some y; x = arm_next_asid (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s b y x. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; ran (arm_hwasid_table (arch_state s)) = dom (arm_asid_map (arch_state s)); \<forall>x y. arm_hwasid_table (arch_state s) x = Some y \<longrightarrow> (\<exists>b. arm_asid_map (arch_state s) y = Some (x, b)); x \<noteq> arm_next_asid (arch_state s); arm_hwasid_table (arch_state s) x = Some y\<rbrakk> \<Longrightarrow> x \<in> dom (arm_hwasid_table (arch_state s))
 2. \<And>s b y x. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; ran (arm_hwasid_table (arch_state s)) = dom (arm_asid_map (arch_state s)); \<forall>x y. arm_hwasid_table (arch_state s) x = Some y \<longrightarrow> (\<exists>b. arm_asid_map (arch_state s) y = Some (x, b)); x \<noteq> arm_next_asid (arch_state s); arm_hwasid_table (arch_state s) x = Some y\<rbrakk> \<Longrightarrow> arm_next_asid (arch_state s) \<in> dom (arm_hwasid_table (arch_state s))
 3. \<And>s b y x. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; ran (arm_hwasid_table (arch_state s)) = dom (arm_asid_map (arch_state s)); \<forall>x y. arm_hwasid_table (arch_state s) x = Some y \<longrightarrow> (\<exists>b. arm_asid_map (arch_state s) y = Some (x, b)); x \<noteq> arm_next_asid (arch_state s); arm_hwasid_table (arch_state s) x = Some y; x = arm_next_asid (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s b y x. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; ran (arm_hwasid_table (arch_state s)) = dom (arm_asid_map (arch_state s)); \<forall>x y. arm_hwasid_table (arch_state s) x = Some y \<longrightarrow> (\<exists>b. arm_asid_map (arch_state s) y = Some (x, b)); x \<noteq> arm_next_asid (arch_state s); arm_hwasid_table (arch_state s) x = Some y\<rbrakk> \<Longrightarrow> arm_next_asid (arch_state s) \<in> dom (arm_hwasid_table (arch_state s))
 2. \<And>s b y x. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; ran (arm_hwasid_table (arch_state s)) = dom (arm_asid_map (arch_state s)); \<forall>x y. arm_hwasid_table (arch_state s) x = Some y \<longrightarrow> (\<exists>b. arm_asid_map (arch_state s) y = Some (x, b)); x \<noteq> arm_next_asid (arch_state s); arm_hwasid_table (arch_state s) x = Some y; x = arm_next_asid (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s b y x. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; ran (arm_hwasid_table (arch_state s)) = dom (arm_asid_map (arch_state s)); \<forall>x y. arm_hwasid_table (arch_state s) x = Some y \<longrightarrow> (\<exists>b. arm_asid_map (arch_state s) y = Some (x, b)); x \<noteq> arm_next_asid (arch_state s); arm_hwasid_table (arch_state s) x = Some y; x = arm_next_asid (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!