theory ArchArch_AC

lemma delete_asid_pool_pas_refined [wp]:
  "delete_asid_pool param_a param_b \<lbrace>pas_refined aag\<rbrace>" unfolding delete_asid_pool_def apply (wp | wpc | simp)+ apply (rule_tac Q = "\<lambda>_ s. pas_refined aag s \<and>
                                 asid_table = arm_asid_table (arch_state s)" in hoare_post_imp) apply clarsimp apply (erule pas_refined_clear_asid) apply (wp mapM_wp' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> delete_asid_pool param_a param_b \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> do assert (param_a && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
when (asid_table (asid_high_bits_of param_a) = Some param_b) $ do pool <- get_asid_pool param_b;
mapM (\<lambda>offset. when (pool (UCAST(32 \<rightarrow> 10) offset) \<noteq> None) $ do flush_space $ param_a + offset;
invalidate_asid_entry $ param_a + offset
od) [0 .e. (1 << local.asid_low_bits) - 1];
asid_table' <- return (asid_table(asid_high_bits_of param_a := None));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>asid_table pool. asid_table (asid_high_bits_of param_a) = Some param_b \<Longrightarrow> \<lbrace>?B6 () asid_table pool\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (param_a + offset);
invalidate_asid_entry (param_a + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>xa a. pas_refined aag (a\<lparr>arch_state := arch_state a\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of param_a then None else asid_table a\<rparr>\<rparr>)\<rbrace>
 2. \<And>x asid_table. asid_table (asid_high_bits_of param_a) = Some param_b \<Longrightarrow> \<lbrace>?Q5 x asid_table\<rbrace> get_asid_pool param_b \<lbrace>?B6 x asid_table\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of param_a) = Some param_b then ?Q5 x asid_table else pas_refined aag\<rbrace>
 4. \<lbrace>?Q\<rbrace> assert (param_a && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 5. \<And>s. pas_refined aag s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>asid_tablea pool rv s. \<lbrakk>asid_tablea (asid_high_bits_of param_a) = Some param_b; pas_refined aag s \<and> asid_tablea = asid_table s\<rbrakk> \<Longrightarrow> pas_refined aag (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of param_a then None else asid_tablea a\<rparr>\<rparr>)
 2. \<And>asid_tablea pool. asid_tablea (asid_high_bits_of param_a) = Some param_b \<Longrightarrow> \<lbrace>?B6 () asid_tablea pool\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (param_a + offset);
invalidate_asid_entry (param_a + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>_ s. pas_refined aag s \<and> asid_tablea = asid_table s\<rbrace>
 3. \<And>x asid_table. asid_table (asid_high_bits_of param_a) = Some param_b \<Longrightarrow> \<lbrace>?Q5 x asid_table\<rbrace> get_asid_pool param_b \<lbrace>?B6 x asid_table\<rbrace>
 4. \<And>x. \<lbrace>?B1 x\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of param_a) = Some param_b then ?Q5 x asid_table else pas_refined aag\<rbrace>
 5. \<lbrace>?Q\<rbrace> assert (param_a && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 6. \<And>s. pas_refined aag s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>asid_table s (asid_high_bits_of param_a) = Some param_b; pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of param_a then None else asid_table s a\<rparr>\<rparr>)
 2. \<And>asid_tablea pool. asid_tablea (asid_high_bits_of param_a) = Some param_b \<Longrightarrow> \<lbrace>?B6 () asid_tablea pool\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (param_a + offset);
invalidate_asid_entry (param_a + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>_ s. pas_refined aag s \<and> asid_tablea = asid_table s\<rbrace>
 3. \<And>x asid_table. asid_table (asid_high_bits_of param_a) = Some param_b \<Longrightarrow> \<lbrace>?Q5 x asid_table\<rbrace> get_asid_pool param_b \<lbrace>?B6 x asid_table\<rbrace>
 4. \<And>x. \<lbrace>?B1 x\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of param_a) = Some param_b then ?Q5 x asid_table else pas_refined aag\<rbrace>
 5. \<lbrace>?Q\<rbrace> assert (param_a && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 6. \<And>s. pas_refined aag s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>asid_tablea pool. asid_tablea (asid_high_bits_of param_a) = Some param_b \<Longrightarrow> \<lbrace>?B6 () asid_tablea pool\<rbrace> mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (param_a + offset);
invalidate_asid_entry (param_a + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>_ s. pas_refined aag s \<and> asid_tablea = asid_table s\<rbrace>
 2. \<And>x asid_table. asid_table (asid_high_bits_of param_a) = Some param_b \<Longrightarrow> \<lbrace>?Q5 x asid_table\<rbrace> get_asid_pool param_b \<lbrace>?B6 x asid_table\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table. if asid_table (asid_high_bits_of param_a) = Some param_b then ?Q5 x asid_table else pas_refined aag\<rbrace>
 4. \<lbrace>?Q\<rbrace> assert (param_a && mask local.asid_low_bits = 0) \<lbrace>?B1\<rbrace>
 5. \<And>s. pas_refined aag s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!