theory ArchFinalise_AI

lemma delete_asid_pool_unmapped2:
  "\<lbrace>\<lambda>s. (base' = base \<and> ptr' = ptr)
         \<or> \<not> ([VSRef (ucast (asid_high_bits_of base')) None] \<rhd> ptr') s\<rbrace>
     delete_asid_pool base ptr
   \<lbrace>\<lambda>rv s. \<not> ([VSRef (ucast (asid_high_bits_of base')) None] \<rhd> ptr') s\<rbrace>"
  (is "valid ?P ?f (\<lambda>rv. ?Q)") apply (cases "base = base' \<and> ptr = ptr'") apply simp apply (wp delete_asid_pool_unmapped) apply (simp add: delete_asid_pool_def) apply wp apply (rule_tac Q="\<lambda>rv s. ?Q s \<and> asid_table = arm_asid_table (arch_state s)"
                 in hoare_post_imp) apply (clarsimp simp: fun_upd_def[symmetric]) apply (drule vs_lookup_clear_asid_table[rule_format]) apply simp apply (wp mapM_wp')+ apply clarsimp apply wp+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace> delete_asid_pool base ptr \<lbrace>\<lambda>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace> proof (prove)
goal (2 subgoals):
 1. base = base' \<and> ptr = ptr' \<Longrightarrow> \<lbrace>\<lambda>s. base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace> delete_asid_pool base ptr \<lbrace>\<lambda>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace>
 2. \<not> (base = base' \<and> ptr = ptr') \<Longrightarrow> \<lbrace>\<lambda>s. base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace> delete_asid_pool base ptr \<lbrace>\<lambda>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace> proof (prove)
goal (2 subgoals):
 1. base = base' \<and> ptr = ptr' \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> delete_asid_pool base' ptr' \<lbrace>\<lambda>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace>
 2. \<not> (base = base' \<and> ptr = ptr') \<Longrightarrow> \<lbrace>\<lambda>s. base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace> delete_asid_pool base ptr \<lbrace>\<lambda>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> (base = base' \<and> ptr = ptr') \<Longrightarrow> \<lbrace>\<lambda>s. base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace> delete_asid_pool base ptr \<lbrace>\<lambda>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace> proof (prove)
goal (1 subgoal):
 1. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>\<lambda>s. base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<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 ptr) (do pool <- get_asid_pool ptr;
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 s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y asid_table pool. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_table (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?B10 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. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup (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. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_table (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 y asid_table\<rbrace> get_asid_pool ptr \<lbrace>?B10 y asid_table\<rbrace>
 3. \<And>y. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?B7 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of base) = Some ptr then ?Q9 y asid_table else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s)\<rbrace>
 4. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?Q6\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?B7\<rbrace>
 5. \<And>s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>y asid_tablea pool rv s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_tablea (asid_high_bits_of base) = Some ptr; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s \<and> asid_tablea = asid_table s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_tablea(asid_high_bits_of base := None)\<rparr>\<rparr>)
 2. \<And>y asid_tablea pool. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_tablea (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?B10 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>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s \<and> asid_tablea = asid_table s\<rbrace>
 3. \<And>y asid_table. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_table (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 y asid_table\<rbrace> get_asid_pool ptr \<lbrace>?B10 y asid_table\<rbrace>
 4. \<And>y. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?B7 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of base) = Some ptr then ?Q9 y asid_table else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s)\<rbrace>
 5. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?Q6\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?B7\<rbrace>
 6. \<And>s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_table s (asid_high_bits_of base) = Some ptr; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None] \<rhd> ptr') (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> False
 2. \<And>y asid_tablea pool. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_tablea (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?B10 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>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s \<and> asid_tablea = asid_table s\<rbrace>
 3. \<And>y asid_table. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_table (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 y asid_table\<rbrace> get_asid_pool ptr \<lbrace>?B10 y asid_table\<rbrace>
 4. \<And>y. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?B7 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of base) = Some ptr then ?Q9 y asid_table else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s)\<rbrace>
 5. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?Q6\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?B7\<rbrace>
 6. \<And>s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_table s (asid_high_bits_of base) = Some ptr; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None] \<rhd> ptr') s\<rbrakk> \<Longrightarrow> False
 2. \<And>y asid_tablea pool. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_tablea (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?B10 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>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s \<and> asid_tablea = asid_table s\<rbrace>
 3. \<And>y asid_table. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_table (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 y asid_table\<rbrace> get_asid_pool ptr \<lbrace>?B10 y asid_table\<rbrace>
 4. \<And>y. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?B7 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of base) = Some ptr then ?Q9 y asid_table else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s)\<rbrace>
 5. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?Q6\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?B7\<rbrace>
 6. \<And>s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>y asid_tablea pool. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_tablea (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?B10 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>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s \<and> asid_tablea = asid_table s\<rbrace>
 2. \<And>y asid_table. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_table (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 y asid_table\<rbrace> get_asid_pool ptr \<lbrace>?B10 y asid_table\<rbrace>
 3. \<And>y. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?B7 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of base) = Some ptr then ?Q9 y asid_table else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s)\<rbrace>
 4. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?Q6\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?B7\<rbrace>
 5. \<And>s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>y asid_tablea pool x s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_tablea (asid_high_bits_of base) = Some ptr; x \<in> set [0 .e. 2 ^ local.asid_low_bits - 1]; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s \<and> asid_tablea = asid_table s\<rbrakk> \<Longrightarrow> (if \<exists>y. pool (UCAST(32 \<rightarrow> 10) x) = Some y then \<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s \<and> asid_tablea = asid_table s else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s \<and> asid_tablea = asid_table s)) s
 2. \<And>y asid_tablea. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_tablea (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 y asid_tablea\<rbrace> get_asid_pool ptr \<lbrace>\<lambda>pool s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s \<and> asid_tablea = asid_table s\<rbrace>
 3. \<And>y. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?B7 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of base) = Some ptr then ?Q9 y asid_table else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s)\<rbrace>
 4. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?Q6\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?B7\<rbrace>
 5. \<And>s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>y asid_tablea. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; asid_tablea (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 y asid_tablea\<rbrace> get_asid_pool ptr \<lbrace>\<lambda>pool s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s \<and> asid_tablea = asid_table s\<rbrace>
 2. \<And>y. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?B7 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of base) = Some ptr then ?Q9 y asid_table else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s)\<rbrace>
 3. base = base' \<longrightarrow> ptr \<noteq> ptr' \<Longrightarrow> \<lbrace>?Q6\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?B7\<rbrace>
 4. \<And>s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>base = base' \<longrightarrow> ptr \<noteq> ptr'; base' = base \<and> ptr' = ptr \<or> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> base && mask local.asid_low_bits = 0 \<longrightarrow> (if (arm_asid_table \<circ> arch_state) s (asid_high_bits_of base) = Some ptr then \<lambda>sa. \<forall>pool. ako_at (ASIDPool pool) ptr sa \<longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup sa \<and> (arm_asid_table \<circ> arch_state) s = asid_table sa else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of base')) None], ptr') \<notin> vs_lookup s)) s proof (prove)
goal:
No subgoals!