theory ArchFinalise_AI

lemma delete_asid_pool_unmapped[wp]:
  "\<lbrace>\<top>\<rbrace>
     delete_asid_pool asid poolptr
   \<lbrace>\<lambda>rv s. \<not> ([VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> poolptr) s\<rbrace>" apply (simp add: delete_asid_pool_def) apply wp apply (rule hoare_strengthen_post [where Q="\<lambda>_. \<top>"]) apply wp+ defer apply wp+ apply (clarsimp simp: vs_lookup_def vs_asid_refs_def
                  dest!: graph_ofD) apply (erule rtranclE) apply (simp add: up_ucast_inj_eq) apply (drule vs_lookup1D) apply clarsimp apply (clarsimp simp: vs_refs_def
                  split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits
                  dest!: graph_ofD) apply (clarsimp simp: vs_lookup_def vs_asid_refs_def
                 dest!: graph_ofD
                 split: if_split_asm) apply (erule rtranclE) apply (simp add: up_ucast_inj_eq) apply (drule vs_lookup1D) apply clarsimp apply (clarsimp simp: vs_refs_def
                 split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits
                 dest!: graph_ofD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> delete_asid_pool asid poolptr \<lbrace>\<lambda>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do y <- assert (asid && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
when (asid_table (asid_high_bits_of asid) = Some poolptr) (do pool <- get_asid_pool poolptr;
y <- mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + 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 asid := None)\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)
od \<lbrace>\<lambda>rv s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y asid_table pool. asid_table (asid_high_bits_of asid) = Some poolptr \<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 (asid + offset);
invalidate_asid_entry (asid + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>ya s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>)\<rbrace>
 2. \<And>y asid_table. asid_table (asid_high_bits_of asid) = Some poolptr \<Longrightarrow> \<lbrace>?Q3 y asid_table\<rbrace> get_asid_pool poolptr \<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 asid) = Some poolptr then ?Q3 y asid_table else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 5. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>y asid_table pool. asid_table (asid_high_bits_of asid) = Some poolptr \<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 (asid + offset);
invalidate_asid_entry (asid + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>y asid_table pool rv s. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; True\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>)
 3. \<And>y asid_table. asid_table (asid_high_bits_of asid) = Some poolptr \<Longrightarrow> \<lbrace>?Q3 y asid_table\<rbrace> get_asid_pool poolptr \<lbrace>?B4 y asid_table\<rbrace>
 4. \<And>y. \<lbrace>?B1 y\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of asid) = Some poolptr then ?Q3 y asid_table else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup s)\<rbrace>
 5. \<lbrace>?Q\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 6. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>y asid_table pool rv s. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; True\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>)
 2. \<And>y asid_table. asid_table (asid_high_bits_of asid) = Some poolptr \<Longrightarrow> \<lbrace>?Q3 y asid_table\<rbrace> get_asid_pool poolptr \<lbrace>\<lambda>pool _. True\<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 asid) = Some poolptr then ?Q3 y asid_table else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 5. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>y asid_table. asid_table (asid_high_bits_of asid) = Some poolptr \<Longrightarrow> \<lbrace>?Q3 y asid_table\<rbrace> get_asid_pool poolptr \<lbrace>\<lambda>pool _. True\<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 asid) = Some poolptr then ?Q3 y asid_table else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s
 5. \<And>y asid_table pool rv s. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; True\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> asid && mask local.asid_low_bits = 0 \<longrightarrow> (if (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = Some poolptr then \<lambda>s. \<forall>pool. ako_at (ASIDPool pool) poolptr s \<longrightarrow> True else (\<lambda>s. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup s)) s
 2. \<And>y asid_table pool rv s. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; True\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba. \<lbrakk>asid_table s (asid_high_bits_of asid) \<noteq> Some poolptr; asid && mask local.asid_low_bits = 0; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<in> (vs_lookup1 s)\<^sup>*; asid_table s aa = Some ba\<rbrakk> \<Longrightarrow> False
 2. \<And>y asid_table pool rv s. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; True\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s aa ba. \<lbrakk>asid_table s (asid_high_bits_of asid) \<noteq> Some poolptr; asid && mask local.asid_low_bits = 0; asid_table s aa = Some ba; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr)\<rbrakk> \<Longrightarrow> False
 2. \<And>s aa ba y. \<lbrakk>asid_table s (asid_high_bits_of asid) \<noteq> Some poolptr; asid && mask local.asid_low_bits = 0; asid_table s aa = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> False
 3. \<And>y asid_table pool rv s. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; True\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba y. \<lbrakk>asid_table s (asid_high_bits_of asid) \<noteq> Some poolptr; asid && mask local.asid_low_bits = 0; asid_table s aa = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> False
 2. \<And>y asid_table pool rv s. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; True\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba y. \<lbrakk>asid_table s (asid_high_bits_of asid) \<noteq> Some poolptr; asid && mask local.asid_low_bits = 0; asid_table s aa = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), y) \<in> (vs_lookup1 s)\<^sup>*; \<exists>rs r p p' ko. y = (rs, p) \<and> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> False
 2. \<And>y asid_table pool rv s. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; True\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba p ko. \<lbrakk>asid_table s (asid_high_bits_of asid) \<noteq> Some poolptr; asid && mask local.asid_low_bits = 0; asid_table s aa = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [], p) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko p s; (VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None, poolptr) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> False
 2. \<And>y asid_table pool rv s. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; True\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>y asid_table pool rv s. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; True\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<notin> vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>asid_table s aa ba. \<lbrakk>(([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<in> (vs_lookup1 (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None else asid_table a\<rparr>\<rparr>))\<^sup>*; asid_table (asid_high_bits_of asid) = Some poolptr; aa \<noteq> asid_high_bits_of asid; asid_table aa = Some ba\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>asid_table s aa ba. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; aa \<noteq> asid_high_bits_of asid; asid_table aa = Some ba; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr)\<rbrakk> \<Longrightarrow> False
 2. \<And>asid_table s aa ba y. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; aa \<noteq> asid_high_bits_of asid; asid_table aa = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), y) \<in> (vs_lookup1 (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None else asid_table a\<rparr>\<rparr>))\<^sup>*; (y, [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<in> vs_lookup1 (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None else asid_table a\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>asid_table s aa ba y. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; aa \<noteq> asid_high_bits_of asid; asid_table aa = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), y) \<in> (vs_lookup1 (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None else asid_table a\<rparr>\<rparr>))\<^sup>*; (y, [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) \<in> vs_lookup1 (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None else asid_table a\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>asid_table s aa ba y. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; aa \<noteq> asid_high_bits_of asid; asid_table aa = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), y) \<in> (vs_lookup1 (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None else asid_table a\<rparr>\<rparr>))\<^sup>*; \<exists>rs r p p' ko. y = (rs, p) \<and> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], poolptr) = (r # rs, p') \<and> ko_at ko p (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None else asid_table a\<rparr>\<rparr>) \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>asid_table s aa ba p ko. \<lbrakk>asid_table (asid_high_bits_of asid) = Some poolptr; aa \<noteq> asid_high_bits_of asid; asid_table aa = Some ba; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [], p) \<in> (vs_lookup1 (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of asid then None else asid_table a\<rparr>\<rparr>))\<^sup>*; ko_at ko p s; (VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None, poolptr) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!