theory ArchArch_IF

lemma delete_asid_pool_reads_respects:
  "reads_respects aag l (K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base
                                    \<longrightarrow> is_subject_asid aag asid'))
                  (delete_asid_pool base ptr)" unfolding delete_asid_pool_def apply (rule equiv_valid_guard_imp) apply (rule bind_ev) apply (simp) apply (subst equiv_valid_def2) apply (rule_tac W="\<top>\<top>"
                 and Q="\<lambda>rv s. rv = arm_asid_table (arch_state s) \<and>
                               (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base
                                        \<longrightarrow> is_subject_asid aag asid')"
                  in equiv_valid_rv_bind) apply (rule equiv_valid_rv_guard_imp[OF equiv_valid_rv_trivial]) apply (wp, simp) apply (simp add: when_def) apply (clarsimp | rule conjI)+ apply (subst bind_assoc[symmetric]) apply (subst (3) bind_assoc[symmetric]) apply (rule equiv_valid_2_guard_imp) apply (rule equiv_valid_2_bind) apply (rule equiv_valid_2_bind) apply (rule equiv_valid_2_unobservable) apply (wp set_vm_root_states_equiv_for)+ apply (rule arm_asid_table_delete_ev2) apply (wp)+ apply (rule equiv_valid_2_unobservable) by (wp mapM_wp' invalidate_asid_entry_states_equiv_for flush_space_states_equiv_for
         invalidate_asid_entry_cur_thread invalidate_asid_entry_sched_act invalidate_asid_entry_wuc
         flush_space_cur_thread flush_space_sched_act flush_space_wuc return_ev2
      | rule conjI | drule (1) requiv_arm_asid_table_asid_high_bits_of_asid_eq'
      | clarsimp | simp add: equiv_valid_2_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (delete_asid_pool base ptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do 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;
mapM (\<lambda>offset. when (pool (UCAST(32 \<rightarrow> 10) offset) \<noteq> None) $ do flush_space $ base + offset;
invalidate_asid_entry $ base + offset
od) [0 .e. (1 << local.asid_low_bits) - 1];
asid_table' <- return (asid_table(asid_high_bits_of base := 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) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (do 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;
mapM (\<lambda>offset. when (pool (UCAST(32 \<rightarrow> 10) offset) \<noteq> None) $ do flush_space $ base + offset;
invalidate_asid_entry $ base + offset
od) [0 .e. (1 << local.asid_low_bits) - 1];
asid_table' <- return (asid_table(asid_high_bits_of base := 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)
 2. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>rv. reads_respects aag l (?Q3 rv) (K_bind (do 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;
mapM (\<lambda>offset. when (pool (UCAST(32 \<rightarrow> 10) offset) \<noteq> None) $ do flush_space $ base + offset;
invalidate_asid_entry $ base + offset
od) [0 .e. (1 << local.asid_low_bits) - 1];
asid_table' <- return (asid_table(asid_high_bits_of base := 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) rv)
 2. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 3. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
 4. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (4 subgoals):
 1. reads_respects aag l (?Q3 ()) (do 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)
 2. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 3. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
 4. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (4 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (?Q8 ()) (do 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)
 2. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 3. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
 4. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?P'3 s \<and> ?P''3 s
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (6 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (?Q8 ()) (gets (arm_asid_table \<circ> arch_state))
 2. \<And>rv rv'. True \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (when (rv (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 := rv(asid_high_bits_of base := None)\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) (when (rv' (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 := rv'(asid_high_bits_of base := None)\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od))
 3. \<lbrace>?Q8 ()\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrace>
 4. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 5. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
 6. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?P'3 s \<and> ?P''3 s
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (7 subgoals):
 1. \<And>P. \<lbrace>P\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. ?Q8 () s \<Longrightarrow> True
 3. \<And>rv rv'. True \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (when (rv (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 := rv(asid_high_bits_of base := None)\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) (when (rv' (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 := rv'(asid_high_bits_of base := None)\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od))
 4. \<lbrace>?Q8 ()\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrace>
 5. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 6. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
 7. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?P'3 s \<and> ?P''3 s
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. True \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (when (rv (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 := rv(asid_high_bits_of base := None)\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) (when (rv' (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 := rv'(asid_high_bits_of base := None)\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od))
 2. \<lbrace>?Q8 ()\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrace>
 3. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 4. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
 5. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?P'3 s \<and> ?P''3 s
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. (rv (asid_high_bits_of base) = Some ptr \<longrightarrow> (rv' (asid_high_bits_of base) = Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) \<and> (rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (return ()))) \<and> (rv (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> (rv' (asid_high_bits_of base) = Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) \<and> (rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (return ())))
 2. \<lbrace>?Q8 ()\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrace>
 3. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 4. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
 5. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?P'3 s \<and> ?P''3 s
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)
 2. \<And>rv rv'. rv (asid_high_bits_of base) = Some ptr \<Longrightarrow> rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (return ())
 3. \<And>rv rv'. rv (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> (rv' (asid_high_bits_of base) = Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) \<and> (rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (return ()))
 4. \<lbrace>?Q8 ()\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrace>
 5. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 6. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
 7. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?P'3 s \<and> ?P''3 s
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do y <- do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)
 2. \<And>rv rv'. rv (asid_high_bits_of base) = Some ptr \<Longrightarrow> rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (return ())
 3. \<And>rv rv'. rv (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> (rv' (asid_high_bits_of base) = Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) \<and> (rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (return ()))
 4. \<lbrace>?Q8 ()\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrace>
 5. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 6. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
 7. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?P'3 s \<and> ?P''3 s
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do y <- do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (do y <- do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)
 2. \<And>rv rv'. rv (asid_high_bits_of base) = Some ptr \<Longrightarrow> rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (return ())
 3. \<And>rv rv'. rv (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> (rv' (asid_high_bits_of base) = Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) \<and> (rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (return ()))
 4. \<lbrace>?Q8 ()\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrace>
 5. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 6. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
 7. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?P'3 s \<and> ?P''3 s
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (9 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (?Q59 rv rv') (?Q'59 rv rv') (do y <- do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (do y <- do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)
 2. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?Q59 rv rv' s
 3. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?Q'59 rv rv' s
 4. \<And>rv rv'. rv (asid_high_bits_of base) = Some ptr \<Longrightarrow> rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (return ())
 5. \<And>rv rv'. rv (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> (rv' (asid_high_bits_of base) = Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) \<and> (rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (return ()))
 6. \<lbrace>?Q8 ()\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrace>
 7. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 8. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
 9. \<And>s. K (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid') s \<Longrightarrow> ?P'3 s \<and> ?P''3 s
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (12 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (?Q63 rv rv' rva) (?Q'63 rv rv' rv'a) (do y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (do y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)
 2. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'63 rv rv') (?P63 rv rv') (?P'63 rv rv') (do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od) (do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od)
 3. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?S63 rv rv'\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>?Q63 rv rv'\<rbrace>
 4. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?S'63 rv rv'\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>?Q'63 rv rv'\<rbrace>
 5. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?P63 rv rv' s \<and> ?S63 rv rv' s
 6. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?P'63 rv rv' s \<and> ?S'63 rv rv' s
 7. \<And>rv rv'. rv (asid_high_bits_of base) = Some ptr \<Longrightarrow> rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (return ())
 8. \<And>rv rv'. rv (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> (rv' (asid_high_bits_of base) = Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) \<and> (rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (return ()))
 9. \<lbrace>?Q8 ()\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrace>
 10. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
A total of 12 subgoals...
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (15 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a; ?R'72 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (?Q72 rv rv' rva rv'a rvb) (?Q'72 rv rv' rva rv'a rv'b) (gets cur_thread >>= set_vm_root) (gets cur_thread >>= set_vm_root)
 2. \<And>rv rv' rva rv'a. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'72 rv rv' rva rv'a) (?P82 rv rv' rva) (?P'80 rv rv' rv'a) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>))
 3. \<And>rv rv' rva rv'a. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S81 rv rv' rva\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>) \<lbrace>?Q72 rv rv' rva rv'a\<rbrace>
 4. \<And>rv rv' rva rv'a. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'79 rv rv' rv'a\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>) \<lbrace>?Q'72 rv rv' rva rv'a\<rbrace>
 5. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'63 rv rv') (?P63 rv rv') (?P'63 rv rv') (do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od) (do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od)
 6. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?S63 rv rv'\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>a b. ?P82 rv rv' a b \<and> ?S81 rv rv' a b\<rbrace>
 7. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?S'63 rv rv'\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>a b. ?P'80 rv rv' a b \<and> ?S'79 rv rv' a b\<rbrace>
 8. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?P63 rv rv' s \<and> ?S63 rv rv' s
 9. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?P'63 rv rv' s \<and> ?S'63 rv rv' s
 10. \<And>rv rv'. rv (asid_high_bits_of base) = Some ptr \<Longrightarrow> rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (return ())
A total of 15 subgoals...
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (26 subgoals):
 1. \<And>rv rv' rva rv'a rvb rv'b P Q R S st. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a; ?R'72 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>states_equiv_for P Q R S st\<rbrace> gets cur_thread >>= set_vm_root \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
 2. \<And>rv rv' rva rv'a rvb rv'b P Q R S st. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a; ?R'72 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>states_equiv_for P Q R S st\<rbrace> gets cur_thread >>= set_vm_root \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
 3. \<And>rv rv' rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a; ?R'72 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> gets cur_thread >>= set_vm_root \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 4. \<And>rv rv' rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a; ?R'72 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> gets cur_thread >>= set_vm_root \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 5. \<And>rv rv' rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a; ?R'72 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> gets cur_thread >>= set_vm_root \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>
 6. \<And>rv rv' rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a; ?R'72 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> gets cur_thread >>= set_vm_root \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>
 7. \<And>rv rv' rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a; ?R'72 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> gets cur_thread >>= set_vm_root \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 8. \<And>rv rv' rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a; ?R'72 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> gets cur_thread >>= set_vm_root \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 9. \<And>rv rv' rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a; ?R'72 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> gets cur_thread >>= set_vm_root \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
 10. \<And>rv rv' rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a; ?R'72 rv rv' rva rv'a rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> gets cur_thread >>= set_vm_root \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
A total of 26 subgoals...
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (14 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'72 rv rv' rva rv'a) (?P82 rv rv' rva) (?P'80 rv rv' rv'a) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>))
 2. \<And>rv rv' rva rv'a. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S81 rv rv' rva\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>rv rv' rva rv'a. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'79 rv rv' rv'a\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>) \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'63 rv rv') (?P63 rv rv') (?P'63 rv rv') (do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od) (do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od)
 5. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?S63 rv rv'\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>a b. ?P82 rv rv' a b \<and> ?S81 rv rv' a b\<rbrace>
 6. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?S'63 rv rv'\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>a b. ?P'80 rv rv' a b \<and> ?S'79 rv rv' a b\<rbrace>
 7. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?P63 rv rv' s \<and> ?S63 rv rv' s
 8. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?P'63 rv rv' s \<and> ?S'63 rv rv' s
 9. \<And>rv rv'. rv (asid_high_bits_of base) = Some ptr \<Longrightarrow> rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (return ())
 10. \<And>rv rv'. rv (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> (rv' (asid_high_bits_of base) = Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) \<and> (rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (return ()))
A total of 14 subgoals...
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (13 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S81 rv rv' rva\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>rv rv' rva rv'a. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; ?R'63 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'79 rv rv' rv'a\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'63 rv rv') (?P63 rv rv') (?P'63 rv rv') (do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od) (do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od)
 4. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?S63 rv rv'\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>a b. rv = asid_table b \<and> ?S81 rv rv' a b\<rbrace>
 5. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?S'63 rv rv'\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>a b. rv' = asid_table b \<and> ?S'79 rv rv' a b\<rbrace>
 6. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?P63 rv rv' s \<and> ?S63 rv rv' s
 7. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?P'63 rv rv' s \<and> ?S'63 rv rv' s
 8. \<And>rv rv'. rv (asid_high_bits_of base) = Some ptr \<Longrightarrow> rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (return ())
 9. \<And>rv rv'. rv (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> (rv' (asid_high_bits_of base) = Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) \<and> (rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (return ()))
 10. \<lbrace>?Q8 ()\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrace>
A total of 13 subgoals...
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (11 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (?R'63 rv rv') (?P63 rv rv') (?P'63 rv rv') (do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od) (do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od)
 2. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?S63 rv rv'\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>a b. rv = asid_table b \<and> True\<rbrace>
 3. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>?S'63 rv rv'\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>a b. rv' = asid_table b \<and> True\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?P63 rv rv' s \<and> ?S63 rv rv' s
 5. \<And>rv rv' s. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr; rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> ?P'63 rv rv' s \<and> ?S'63 rv rv' s
 6. \<And>rv rv'. rv (asid_high_bits_of base) = Some ptr \<Longrightarrow> rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od) (return ())
 7. \<And>rv rv'. rv (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> (rv' (asid_high_bits_of base) = Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (do pool <- get_asid_pool ptr;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := \<lambda>a. if a = asid_high_bits_of base then None else rv' a\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)) \<and> (rv' (asid_high_bits_of base) \<noteq> Some ptr \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>a b. True) (\<lambda>s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (\<lambda>s. rv' = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')) (return ()) (return ()))
 8. \<lbrace>?Q8 ()\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of base \<longrightarrow> is_subject_asid aag asid')\<rbrace>
 9. reads_respects aag l ?P'3 (assert (base && mask local.asid_low_bits = 0))
 10. \<lbrace>?P''3\<rbrace> assert (base && mask local.asid_low_bits = 0) \<lbrace>?Q3\<rbrace>
A total of 11 subgoals...
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 () proof (prove)
goal (22 subgoals):
 1. \<And>rv rv' P Q R S st. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>states_equiv_for P Q R S st\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
 2. \<And>rv rv' P Q R S st. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>states_equiv_for P Q R S st\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
 3. \<And>rv rv' P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 4. \<And>rv rv' P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 5. \<And>rv rv' P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>
 6. \<And>rv rv' P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>
 7. \<And>rv rv' P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 8. \<And>rv rv' P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 9. \<And>rv rv' P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
 10. \<And>rv rv' P. \<lbrakk>rv (asid_high_bits_of base) = Some ptr; rv' (asid_high_bits_of base) = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> do pool <- get_asid_pool ptr;
mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (base + offset);
invalidate_asid_entry (base + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1]
od \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
A total of 22 subgoals...
flex-flex pairs:
?Q8 () \<equiv>\<^sup>? ?Q3 ()