theory ArchFinalise_AI

lemma delete_asid_pool_invs[wp]:
  "\<lbrace>invs and K (base \<le> mask asid_bits)\<rbrace>
     delete_asid_pool base pptr
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: delete_asid_pool_def) apply wp apply (strengthen invs_arm_asid_table_unmap) apply simp apply (rule hoare_vcg_conj_lift,
           (rule mapM_invalidate[where ptr=pptr])?,
           ((wp mapM_wp' | simp add: if_apply_def2)+)[1])+ apply wp+ apply (clarsimp simp: is_aligned_mask[symmetric]) apply (rule conjI) apply (rule vs_lookupI) apply (erule vs_asid_refsI) apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (base \<le> mask local.asid_bits)\<rbrace> delete_asid_pool base pptr \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>y. base \<le> mask local.asid_bits)\<rbrace> do y <- assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
when (asid_table (asid_high_bits_of base) = Some pptr) (do pool <- get_asid_pool pptr;
y <- mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of base := None)\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y asid_table pool. asid_table (asid_high_bits_of base) = Some pptr \<Longrightarrow> \<lbrace>?B4 y asid_table pool\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>ya s. invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of base := None)\<rparr>\<rparr>)\<rbrace>
 2. \<And>y asid_table. asid_table (asid_high_bits_of base) = Some pptr \<Longrightarrow> \<lbrace>?Q3 y asid_table\<rbrace> get_asid_pool pptr \<lbrace>?B4 y asid_table\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of base) = Some pptr then ?Q3 y asid_table else invs\<rbrace>
 4. \<lbrace>?Q\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs and (\<lambda>y. base \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>y asid_tablea pool. asid_tablea (asid_high_bits_of base) = Some pptr \<Longrightarrow> \<lbrace>?B4 y asid_tablea pool\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. invs s \<and> is_aligned base local.asid_low_bits \<and> base \<le> mask local.asid_bits \<and> (\<forall>x\<in>set [0 .e. 2 ^ local.asid_low_bits - 1]. arm_asid_map (arch_state s) (base + x) = None) \<and> asid_tablea = asid_table s\<rbrace>
 2. \<And>y asid_table. asid_table (asid_high_bits_of base) = Some pptr \<Longrightarrow> \<lbrace>?Q3 y asid_table\<rbrace> get_asid_pool pptr \<lbrace>?B4 y asid_table\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of base) = Some pptr then ?Q3 y asid_table else invs\<rbrace>
 4. \<lbrace>?Q\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs and (\<lambda>y. base \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>asid_tablea pool. asid_tablea (asid_high_bits_of base) = Some pptr \<Longrightarrow> \<lbrace>?B4 () asid_tablea pool\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. invs s \<and> is_aligned base local.asid_low_bits \<and> base \<le> mask local.asid_bits \<and> (\<forall>x\<le>2 ^ local.asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None) \<and> asid_tablea = asid_table s\<rbrace>
 2. \<And>y asid_table. asid_table (asid_high_bits_of base) = Some pptr \<Longrightarrow> \<lbrace>?Q3 y asid_table\<rbrace> get_asid_pool pptr \<lbrace>?B4 y asid_table\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of base) = Some pptr then ?Q3 y asid_table else invs\<rbrace>
 4. \<lbrace>?Q\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs and (\<lambda>y. base \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>y asid_tablea. asid_tablea (asid_high_bits_of base) = Some pptr \<Longrightarrow> \<lbrace>?P'90 y asid_tablea\<rbrace> get_asid_pool pptr \<lbrace>\<lambda>rv s. asid_tablea = asid_table s\<rbrace>
 2. \<And>y. \<lbrace>?B1 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of base) = Some pptr then \<lambda>s. (\<forall>pool. ako_at (ASIDPool pool) pptr s \<longrightarrow> invs s) \<and> (\<forall>pool. ako_at (ASIDPool pool) pptr s \<longrightarrow> is_aligned base local.asid_low_bits) \<and> (\<forall>pool. ako_at (ASIDPool pool) pptr s \<longrightarrow> base \<le> mask local.asid_bits) \<and> (\<forall>pool. ako_at (ASIDPool pool) pptr s \<longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> pptr and ako_at (ASIDPool pool) pptr and valid_asid_map and K (is_aligned base local.asid_low_bits)) s) \<and> ?P'90 y asid_table s else invs\<rbrace>
 3. \<lbrace>?Q\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 4. \<And>s. (invs and (\<lambda>y. base \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and (\<lambda>y. base \<le> mask local.asid_bits)) s \<Longrightarrow> base && mask local.asid_low_bits = 0 \<longrightarrow> (if (arm_asid_table \<circ> arch_state) s (asid_high_bits_of base) = Some pptr then \<lambda>sa. (\<forall>pool. ako_at (ASIDPool pool) pptr sa \<longrightarrow> invs sa) \<and> (\<forall>pool. ako_at (ASIDPool pool) pptr sa \<longrightarrow> is_aligned base local.asid_low_bits) \<and> (\<forall>pool. ako_at (ASIDPool pool) pptr sa \<longrightarrow> base \<le> mask local.asid_bits) \<and> (\<forall>pool. ako_at (ASIDPool pool) pptr sa \<longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> pptr and ako_at (ASIDPool pool) pptr and valid_asid_map and K (is_aligned base local.asid_low_bits)) sa) \<and> (\<forall>pool. ako_at (ASIDPool pool) pptr sa \<longrightarrow> (arm_asid_table \<circ> arch_state) s = asid_table sa) else invs) s proof (prove)
goal (1 subgoal):
 1. \<And>s pool. \<lbrakk>invs s; base \<le> mask local.asid_bits; asid_table s (asid_high_bits_of base) = Some pptr; is_aligned base local.asid_low_bits; ako_at (ASIDPool pool) pptr s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> pptr) s \<and> valid_asid_map s proof (prove)
goal (2 subgoals):
 1. \<And>s pool. \<lbrakk>invs s; base \<le> mask local.asid_bits; asid_table s (asid_high_bits_of base) = Some pptr; is_aligned base local.asid_low_bits; ako_at (ASIDPool pool) pptr s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None] \<rhd> pptr) s
 2. \<And>s pool. \<lbrakk>invs s; base \<le> mask local.asid_bits; asid_table s (asid_high_bits_of base) = Some pptr; is_aligned base local.asid_low_bits; ako_at (ASIDPool pool) pptr s\<rbrakk> \<Longrightarrow> valid_asid_map s proof (prove)
goal (3 subgoals):
 1. \<And>s pool. \<lbrakk>invs s; base \<le> mask local.asid_bits; asid_table s (asid_high_bits_of base) = Some pptr; is_aligned base local.asid_low_bits; ako_at (ASIDPool pool) pptr s\<rbrakk> \<Longrightarrow> ?ref'117 s pool \<in> vs_asid_refs (asid_table s)
 2. \<And>s pool. \<lbrakk>invs s; base \<le> mask local.asid_bits; asid_table s (asid_high_bits_of base) = Some pptr; is_aligned base local.asid_low_bits; ako_at (ASIDPool pool) pptr s\<rbrakk> \<Longrightarrow> (?ref'117 s pool, [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], pptr) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>s pool. \<lbrakk>invs s; base \<le> mask local.asid_bits; asid_table s (asid_high_bits_of base) = Some pptr; is_aligned base local.asid_low_bits; ako_at (ASIDPool pool) pptr s\<rbrakk> \<Longrightarrow> valid_asid_map s proof (prove)
goal (2 subgoals):
 1. \<And>s pool. \<lbrakk>invs s; base \<le> mask local.asid_bits; asid_table s (asid_high_bits_of base) = Some pptr; is_aligned base local.asid_low_bits; ako_at (ASIDPool pool) pptr s\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], pptr), [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base)) None], pptr) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>s pool. \<lbrakk>invs s; base \<le> mask local.asid_bits; asid_table s (asid_high_bits_of base) = Some pptr; is_aligned base local.asid_low_bits; ako_at (ASIDPool pool) pptr s\<rbrakk> \<Longrightarrow> valid_asid_map s proof (prove)
goal (1 subgoal):
 1. \<And>s pool. \<lbrakk>invs s; base \<le> mask local.asid_bits; asid_table s (asid_high_bits_of base) = Some pptr; is_aligned base local.asid_low_bits; ako_at (ASIDPool pool) pptr s\<rbrakk> \<Longrightarrow> valid_asid_map s proof (prove)
goal:
No subgoals!