theory ArchVSpace_AI

lemma invalidate_asid_entry_invalidates:
  "\<lbrace>valid_asid_map and valid_arch_state and K (asid \<le> mask asid_bits) and
    (\<lambda>s. arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some ap)\<rbrace>
   invalidate_asid_entry asid
   \<lbrace>\<lambda>rv s. \<forall>asida. asida \<le> mask asid_bits \<longrightarrow>
              ucast asida = (ucast asid :: 10 word) \<longrightarrow>
              arm_asid_table (arch_state s) (asid_high_bits_of asida) =
                Some ap \<longrightarrow>
              arm_asid_map (arch_state s) asida = None\<rbrace>" apply (simp add: invalidate_asid_entry_def invalidate_asid_def invalidate_hw_asid_entry_def) apply (wp load_hw_asid_wp) apply (clarsimp simp del: None_upd_eq) apply (rule drop_imp) apply (clarsimp simp: valid_arch_state_def valid_asid_table_def) apply (drule_tac x="asid_high_bits_of asid" and y="asid_high_bits_of asida" in inj_onD) apply simp apply blast apply blast apply clarsimp apply (drule asid_low_high_bits', simp) apply (fastforce simp: mask_def) apply (fastforce simp: mask_def) apply (erule (1) notE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and valid_arch_state and K (asid \<le> mask local.asid_bits) and (\<lambda>s. asid_table s (asid_high_bits_of asid) = Some ap)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. \<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some ap \<longrightarrow> arm_asid_map (arch_state s) asida = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and valid_arch_state and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. asid_table s (asid_high_bits_of asid) = Some ap)\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
y <- when (\<exists>y. maybe_hw_asid = Some 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(the maybe_hw_asid := None)\<rparr>\<rparr>)
od);
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(asid := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>rv s. \<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some ap \<longrightarrow> arm_asid_map (arch_state s) asida = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_asid_map and valid_arch_state and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. asid_table s (asid_high_bits_of asid) = Some ap)) s \<Longrightarrow> (if \<exists>y. map_option fst (arm_asid_map (arch_state s) asid) = Some y then \<lambda>sa. \<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>, arch_state := arch_state (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>)\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>))(asid := None)\<rparr>\<rparr>) (asid_high_bits_of asida) = Some ap \<longrightarrow> arm_asid_map (arch_state (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>, arch_state := arch_state (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>)\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>))(asid := None)\<rparr>\<rparr>)) asida = None else (\<lambda>s. \<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid := None)\<rparr>\<rparr>) (asid_high_bits_of asida) = Some ap \<longrightarrow> arm_asid_map (arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid := None)\<rparr>\<rparr>)) asida = None)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_asid_map s; valid_arch_state s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap\<rbrakk> \<Longrightarrow> ((\<exists>y b. arm_asid_map (arch_state s) asid = Some (y, b)) \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some ap \<longrightarrow> arm_asid_map (arch_state s) asida = None)) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> (\<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some ap \<longrightarrow> arm_asid_map (arch_state s) asida = None)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_asid_map s; valid_arch_state s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap\<rbrakk> \<Longrightarrow> \<forall>asida. asida \<noteq> asid \<longrightarrow> asida \<le> mask local.asid_bits \<longrightarrow> UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some ap \<longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (1 subgoal):
 1. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (4 subgoals):
 1. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap\<rbrakk> \<Longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table s (asid_high_bits_of asida)
 2. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap\<rbrakk> \<Longrightarrow> asid_high_bits_of asid \<in> dom (asid_table s)
 3. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap\<rbrakk> \<Longrightarrow> asid_high_bits_of asida \<in> dom (asid_table s)
 4. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (3 subgoals):
 1. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap\<rbrakk> \<Longrightarrow> asid_high_bits_of asid \<in> dom (asid_table s)
 2. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap\<rbrakk> \<Longrightarrow> asid_high_bits_of asida \<in> dom (asid_table s)
 3. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (2 subgoals):
 1. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap\<rbrakk> \<Longrightarrow> asid_high_bits_of asida \<in> dom (asid_table s)
 2. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (1 subgoal):
 1. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asid) = Some ap; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (1 subgoal):
 1. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid; asid_table s (asid_high_bits_of asida) = Some ap; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (3 subgoals):
 1. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some ap; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> asida \<le> 2 ^ local.asid_bits - 1
 2. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some ap; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> asid \<le> 2 ^ local.asid_bits - 1
 3. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some ap; asid_high_bits_of asid = asid_high_bits_of asida; asida = asid\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (2 subgoals):
 1. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some ap; asid_high_bits_of asid = asid_high_bits_of asida\<rbrakk> \<Longrightarrow> asid \<le> 2 ^ local.asid_bits - 1
 2. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some ap; asid_high_bits_of asid = asid_high_bits_of asida; asida = asid\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal (1 subgoal):
 1. \<And>s asida. \<lbrakk>valid_asid_map s; asid \<le> mask local.asid_bits; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p 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)); asida \<noteq> asid; asida \<le> mask local.asid_bits; asid_table s (asid_high_bits_of asida) = Some ap; asid_high_bits_of asid = asid_high_bits_of asida; asida = asid\<rbrakk> \<Longrightarrow> arm_asid_map (arch_state s) asida = None proof (prove)
goal:
No subgoals!