theory ArchArch_IF

lemma delete_asid_reads_respects:
  "reads_respects aag l (K (asid \<noteq> 0 \<and> is_subject_asid aag asid)) (delete_asid asid pd)" unfolding delete_asid_def apply (subst equiv_valid_def2) apply (rule_tac W="\<top>\<top>" and Q="\<lambda>rv s. rv = arm_asid_table (arch_state s) \<and>
                                        is_subject_asid aag asid \<and> asid \<noteq> 0" in equiv_valid_rv_bind) apply (rule equiv_valid_rv_guard_imp[OF equiv_valid_rv_trivial]) apply (wp, simp) apply (case_tac "rv (asid_high_bits_of asid) = rv' (asid_high_bits_of asid)") apply (simp) apply (case_tac "rv' (asid_high_bits_of asid)") apply (simp) apply (wp return_ev2, simp) apply (simp) apply (rule equiv_valid_2_guard_imp) apply (rule_tac R'="\<lambda>rv rv'. rv (ucast asid) = rv' (ucast asid)" in equiv_valid_2_bind) apply (simp add: when_def) apply (clarsimp | rule conjI)+ apply (rule_tac R'="\<top>\<top>" in equiv_valid_2_bind) apply (rule_tac R'="\<top>\<top>" in equiv_valid_2_bind) apply (rule_tac R'="\<top>\<top>" in equiv_valid_2_bind) apply (subst equiv_valid_def2[symmetric]) apply (rule reads_respects_unobservable_unit_return) apply (wp set_vm_root_states_equiv_for)+ apply (rule set_asid_pool_delete_ev2) apply (wp)+ apply (rule equiv_valid_2_unobservable) apply (wp invalidate_asid_entry_states_equiv_for invalidate_asid_entry_cur_thread)+ apply (simp add: invalidate_asid_entry_def
                           | wp invalidate_asid_kheap invalidate_hw_asid_entry_kheap load_hw_asid_kheap)+ apply (rule equiv_valid_2_unobservable) apply (wp flush_space_states_equiv_for flush_space_cur_thread)+ apply (wp load_hw_asid_kheap | simp add: flush_space_def | wpc)+ apply (clarsimp | rule return_ev2)+ apply (rule equiv_valid_2_guard_imp) apply (wp get_asid_pool_revrv) apply (simp)+ apply (wp)+ apply (clarsimp simp: obj_at_def)+ apply (clarsimp simp: equiv_valid_2_def reads_equiv_def
                         equiv_asids_def equiv_asid_def states_equiv_for_def) apply (erule_tac x="pasASIDAbs aag asid" in ballE) apply (clarsimp) apply (drule aag_can_read_own_asids) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (asid \<noteq> 0 \<and> is_subject_asid aag asid)) (delete_asid asid pd) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (asid \<noteq> 0 \<and> is_subject_asid aag asid)) (do asid_table <- gets (arm_asid_table \<circ> arch_state);
case asid_table (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od
od) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (K (asid \<noteq> 0 \<and> is_subject_asid aag asid)) (do asid_table <- gets (arm_asid_table \<circ> arch_state);
case asid_table (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od
od) proof (prove)
goal (3 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (K (asid \<noteq> 0 \<and> is_subject_asid aag asid)) (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> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 3. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>P. \<lbrace>P\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. K (asid \<noteq> 0 \<and> is_subject_asid aag asid) 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> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 4. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (2 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> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 2. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) = rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 2. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 3. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. rv (asid_high_bits_of asid) = rv' (asid_high_bits_of asid) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od)
 2. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 3. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of asid) = rv' (asid_high_bits_of asid); rv' (asid_high_bits_of asid) = None\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od)
 2. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = rv' (asid_high_bits_of asid); rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od)
 3. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 4. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv (asid_high_bits_of asid) = None; rv' (asid_high_bits_of asid) = None\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (return ()) (return ())
 2. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = rv' (asid_high_bits_of asid); rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od)
 3. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 4. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = rv' (asid_high_bits_of asid); rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od)
 2. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 3. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (do pool <- get_asid_pool a;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) (do pool <- get_asid_pool a;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od)
 2. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 3. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q15 rv rv' a) (?Q'15 rv rv' a) (do pool <- get_asid_pool a;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) (do pool <- get_asid_pool a;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od)
 2. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?Q15 rv rv' a s
 3. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?Q'15 rv rv' a s
 4. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 5. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = rv'a (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q19 rv rv' a rva) (?Q'19 rv rv' a rv'a) (when (rva (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)) (when (rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od))
 2. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?P19 rv rv' a) (?P'19 rv rv' a) (get_asid_pool a) (get_asid_pool a)
 3. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>?Q19 rv rv' a\<rbrace>
 4. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S'19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>?Q'19 rv rv' a\<rbrace>
 5. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P19 rv rv' a s \<and> ?S19 rv rv' a s
 6. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P'19 rv rv' a s \<and> ?S'19 rv rv' a s
 7. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 8. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = rv'a (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> (rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q19 rv rv' a rva) (?Q'19 rv rv' a rv'a) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)) \<and> (rv'a (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q19 rv rv' a rva) (?Q'19 rv rv' a rv'a) (return ()) (return ()))
 2. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?P19 rv rv' a) (?P'19 rv rv' a) (get_asid_pool a) (get_asid_pool a)
 3. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>?Q19 rv rv' a\<rbrace>
 4. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S'19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>?Q'19 rv rv' a\<rbrace>
 5. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P19 rv rv' a s \<and> ?S19 rv rv' a s
 6. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P'19 rv rv' a s \<and> ?S'19 rv rv' a s
 7. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 8. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q19 rv rv' a rva) (?Q'19 rv rv' a rv'a) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = rv'a (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> rv'a (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q19 rv rv' a rva) (?Q'19 rv rv' a rv'a) (return ()) (return ())
 3. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?P19 rv rv' a) (?P'19 rv rv' a) (get_asid_pool a) (get_asid_pool a)
 4. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>?Q19 rv rv' a\<rbrace>
 5. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S'19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>?Q'19 rv rv' a\<rbrace>
 6. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P19 rv rv' a s \<and> ?S19 rv rv' a s
 7. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P'19 rv rv' a s \<and> ?S'19 rv rv' a s
 8. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 9. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q31 rv rv' a rva rv'a rvb) (?Q'31 rv rv' a rva rv'a rv'b) (do y <- invalidate_asid_entry asid;
y <- set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od) (do y <- invalidate_asid_entry asid;
y <- set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P33 rv rv' a rva) (?P'35 rv rv' a rv'a) (flush_space asid) (flush_space asid)
 3. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S34 rv rv' a rva\<rbrace> flush_space asid \<lbrace>?Q31 rv rv' a rva rv'a\<rbrace>
 4. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S'36 rv rv' a rv'a\<rbrace> flush_space asid \<lbrace>?Q'31 rv rv' a rva rv'a\<rbrace>
 5. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = rv'a (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> rv'a (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. ?P33 rv rv' a rva s \<and> ?S34 rv rv' a rva s) (\<lambda>s. ?P'35 rv rv' a rv'a s \<and> ?S'36 rv rv' a rv'a s) (return ()) (return ())
 6. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?P19 rv rv' a) (?P'19 rv rv' a) (get_asid_pool a) (get_asid_pool a)
 7. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rva s. ?P33 rv rv' a rva s \<and> ?S34 rv rv' a rva s\<rbrace>
 8. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S'19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rv'a s. ?P'35 rv rv' a rv'a s \<and> ?S'36 rv rv' a rv'a s\<rbrace>
 9. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P19 rv rv' a s \<and> ?S19 rv rv' a s
 10. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P'19 rv rv' a s \<and> ?S'19 rv rv' a s
A total of 12 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q37 rv rv' a rva rv'a rvb rv'b rvc) (?Q'37 rv rv' a rva rv'a rvb rv'b rv'c) (do y <- set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od) (do y <- set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P39 rv rv' a rva rv'a rvb) (?P'41 rv rv' a rva rv'a rv'b) (invalidate_asid_entry asid) (invalidate_asid_entry asid)
 3. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S40 rv rv' a rva rv'a rvb\<rbrace> invalidate_asid_entry asid \<lbrace>?Q37 rv rv' a rva rv'a rvb rv'b\<rbrace>
 4. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'42 rv rv' a rva rv'a rv'b\<rbrace> invalidate_asid_entry asid \<lbrace>?Q'37 rv rv' a rva rv'a rvb rv'b\<rbrace>
 5. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P33 rv rv' a rva) (?P'35 rv rv' a rv'a) (flush_space asid) (flush_space asid)
 6. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S34 rv rv' a rva\<rbrace> flush_space asid \<lbrace>\<lambda>rvb s. ?P39 rv rv' a rva rv'a rvb s \<and> ?S40 rv rv' a rva rv'a rvb s\<rbrace>
 7. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S'36 rv rv' a rv'a\<rbrace> flush_space asid \<lbrace>\<lambda>rv'b s. ?P'41 rv rv' a rva rv'a rv'b s \<and> ?S'42 rv rv' a rva rv'a rv'b s\<rbrace>
 8. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = rv'a (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> rv'a (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. ?P33 rv rv' a rva s \<and> ?S34 rv rv' a rva s) (\<lambda>s. ?P'35 rv rv' a rv'a s \<and> ?S'36 rv rv' a rv'a s) (return ()) (return ())
 9. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?P19 rv rv' a) (?P'19 rv rv' a) (get_asid_pool a) (get_asid_pool a)
 10. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rva s. ?P33 rv rv' a rva s \<and> ?S34 rv rv' a rva s\<rbrace>
A total of 15 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q43 rv rv' a rva rv'a rvb rv'b rvc rv'c rvd) (?Q'43 rv rv' a rva rv'a rvb rv'b rvc rv'c rv'd) (gets cur_thread >>= set_vm_root) (gets cur_thread >>= set_vm_root)
 2. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P45 rv rv' a rva rv'a rvb rv'b rvc) (?P'47 rv rv' a rva rv'a rvb rv'b rv'c) (set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None))) (set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None)))
 3. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S46 rv rv' a rva rv'a rvb rv'b rvc\<rbrace> set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?Q43 rv rv' a rva rv'a rvb rv'b rvc rv'c\<rbrace>
 4. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'48 rv rv' a rva rv'a rvb rv'b rv'c\<rbrace> set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?Q'43 rv rv' a rva rv'a rvb rv'b rvc rv'c\<rbrace>
 5. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P39 rv rv' a rva rv'a rvb) (?P'41 rv rv' a rva rv'a rv'b) (invalidate_asid_entry asid) (invalidate_asid_entry asid)
 6. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S40 rv rv' a rva rv'a rvb\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvc s. ?P45 rv rv' a rva rv'a rvb rv'b rvc s \<and> ?S46 rv rv' a rva rv'a rvb rv'b rvc s\<rbrace>
 7. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'42 rv rv' a rva rv'a rv'b\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv'c s. ?P'47 rv rv' a rva rv'a rvb rv'b rv'c s \<and> ?S'48 rv rv' a rva rv'a rvb rv'b rv'c s\<rbrace>
 8. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P33 rv rv' a rva) (?P'35 rv rv' a rv'a) (flush_space asid) (flush_space asid)
 9. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S34 rv rv' a rva\<rbrace> flush_space asid \<lbrace>\<lambda>rvb s. ?P39 rv rv' a rva rv'a rvb s \<and> ?S40 rv rv' a rva rv'a rvb s\<rbrace>
 10. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S'36 rv rv' a rv'a\<rbrace> flush_space asid \<lbrace>\<lambda>rv'b s. ?P'41 rv rv' a rva rv'a rv'b s \<and> ?S'42 rv rv' a rva rv'a rv'b s\<rbrace>
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True; True\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>b. ?Q'52 rv rv' a rva rv'a rvb rv'b rvc rv'c) (gets cur_thread >>= set_vm_root)
 2. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P45 rv rv' a rva rv'a rvb rv'b rvc) (?P'47 rv rv' a rva rv'a rvb rv'b rv'c) (set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None))) (set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None)))
 3. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S46 rv rv' a rva rv'a rvb rv'b rvc\<rbrace> set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rvd b. ?Q'52 rv rv' a rva rv'a rvb rv'b rvc rv'c\<rbrace>
 4. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'48 rv rv' a rva rv'a rvb rv'b rv'c\<rbrace> set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rv'd b. ?Q'52 rv rv' a rva rv'a rvb rv'b rvc rv'c\<rbrace>
 5. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P39 rv rv' a rva rv'a rvb) (?P'41 rv rv' a rva rv'a rv'b) (invalidate_asid_entry asid) (invalidate_asid_entry asid)
 6. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S40 rv rv' a rva rv'a rvb\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvc s. ?P45 rv rv' a rva rv'a rvb rv'b rvc s \<and> ?S46 rv rv' a rva rv'a rvb rv'b rvc s\<rbrace>
 7. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'42 rv rv' a rva rv'a rv'b\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv'c s. ?P'47 rv rv' a rva rv'a rvb rv'b rv'c s \<and> ?S'48 rv rv' a rva rv'a rvb rv'b rv'c s\<rbrace>
 8. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P33 rv rv' a rva) (?P'35 rv rv' a rv'a) (flush_space asid) (flush_space asid)
 9. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S34 rv rv' a rva\<rbrace> flush_space asid \<lbrace>\<lambda>rvb s. ?P39 rv rv' a rva rv'a rvb s \<and> ?S40 rv rv' a rva rv'a rvb s\<rbrace>
 10. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S'36 rv rv' a rv'a\<rbrace> flush_space asid \<lbrace>\<lambda>rv'b s. ?P'41 rv rv' a rva rv'a rv'b s \<and> ?S'42 rv rv' a rva rv'a rv'b s\<rbrace>
A total of 18 subgoals... proof (prove)
goal (23 subgoals):
 1. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c rvd rv'd P Q R S st. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True; True\<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' a rva rv'a rvb rv'b rvc rv'c rvd rv'd P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True; True\<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>
 3. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c rvd rv'd P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True; True\<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>
 4. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c rvd rv'd P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True; True\<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>
 5. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c rvd rv'd P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True; True\<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>
 6. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c rvd rv'd P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> gets cur_thread >>= set_vm_root \<lbrace>\<lambda>rv s. P (irq_state_of_state s)\<rbrace>
 7. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P45 rv rv' a rva rv'a rvb rv'b rvc) (?P'47 rv rv' a rva rv'a rvb rv'b rv'c) (set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None))) (set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None)))
 8. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S46 rv rv' a rva rv'a rvb rv'b rvc\<rbrace> set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rvd a. True\<rbrace>
 9. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'48 rv rv' a rva rv'a rvb rv'b rv'c\<rbrace> set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rv'd a. True\<rbrace>
 10. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P39 rv rv' a rva rv'a rvb) (?P'41 rv rv' a rva rv'a rv'b) (invalidate_asid_entry asid) (invalidate_asid_entry asid)
A total of 23 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P45 rv rv' a rva rv'a rvb rv'b rvc) (?P'47 rv rv' a rva rv'a rvb rv'b rv'c) (set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None))) (set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None)))
 2. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S46 rv rv' a rva rv'a rvb rv'b rvc\<rbrace> set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rvd a. True\<rbrace>
 3. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'48 rv rv' a rva rv'a rvb rv'b rv'c\<rbrace> set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rv'd a. True\<rbrace>
 4. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P39 rv rv' a rva rv'a rvb) (?P'41 rv rv' a rva rv'a rv'b) (invalidate_asid_entry asid) (invalidate_asid_entry asid)
 5. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S40 rv rv' a rva rv'a rvb\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvc s. ?P45 rv rv' a rva rv'a rvb rv'b rvc s \<and> ?S46 rv rv' a rva rv'a rvb rv'b rvc s\<rbrace>
 6. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'42 rv rv' a rva rv'a rv'b\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv'c s. ?P'47 rv rv' a rva rv'a rvb rv'b rv'c s \<and> ?S'48 rv rv' a rva rv'a rvb rv'b rv'c s\<rbrace>
 7. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P33 rv rv' a rva) (?P'35 rv rv' a rv'a) (flush_space asid) (flush_space asid)
 8. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S34 rv rv' a rva\<rbrace> flush_space asid \<lbrace>\<lambda>rvb s. ?P39 rv rv' a rva rv'a rvb s \<and> ?S40 rv rv' a rva rv'a rvb s\<rbrace>
 9. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S'36 rv rv' a rv'a\<rbrace> flush_space asid \<lbrace>\<lambda>rv'b s. ?P'41 rv rv' a rva rv'a rv'b s \<and> ?S'42 rv rv' a rva rv'a rv'b s\<rbrace>
 10. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = rv'a (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> rv'a (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. ?P33 rv rv' a rva s \<and> ?S34 rv rv' a rva s) (\<lambda>s. ?P'35 rv rv' a rv'a s \<and> ?S'36 rv rv' a rv'a s) (return ()) (return ())
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S46 rv rv' a rva rv'a rvb rv'b rvc\<rbrace> set_asid_pool a (rva(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rvd a. True\<rbrace>
 2. \<And>rv rv' a rva rv'a rvb rv'b rvc rv'c. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'48 rv rv' a rva rv'a rvb rv'b rv'c\<rbrace> set_asid_pool a (rv'a(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rv'd a. True\<rbrace>
 3. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P39 rv rv' a rva rv'a rvb) (?P'41 rv rv' a rva rv'a rv'b) (invalidate_asid_entry asid) (invalidate_asid_entry asid)
 4. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S40 rv rv' a rva rv'a rvb\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvc s. (asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rva)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid) \<and> ?S46 rv rv' a rva rv'a rvb rv'b rvc s\<rbrace>
 5. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'42 rv rv' a rva rv'a rv'b\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv'c s. (asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rv'a)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid) \<and> ?S'48 rv rv' a rva rv'a rvb rv'b rv'c s\<rbrace>
 6. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P33 rv rv' a rva) (?P'35 rv rv' a rv'a) (flush_space asid) (flush_space asid)
 7. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S34 rv rv' a rva\<rbrace> flush_space asid \<lbrace>\<lambda>rvb s. ?P39 rv rv' a rva rv'a rvb s \<and> ?S40 rv rv' a rva rv'a rvb s\<rbrace>
 8. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S'36 rv rv' a rv'a\<rbrace> flush_space asid \<lbrace>\<lambda>rv'b s. ?P'41 rv rv' a rva rv'a rv'b s \<and> ?S'42 rv rv' a rva rv'a rv'b s\<rbrace>
 9. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = rv'a (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> rv'a (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. ?P33 rv rv' a rva s \<and> ?S34 rv rv' a rva s) (\<lambda>s. ?P'35 rv rv' a rv'a s \<and> ?S'36 rv rv' a rv'a s) (return ()) (return ())
 10. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?P19 rv rv' a) (?P'19 rv rv' a) (get_asid_pool a) (get_asid_pool a)
A total of 16 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P39 rv rv' a rva rv'a rvb) (?P'41 rv rv' a rva rv'a rv'b) (invalidate_asid_entry asid) (invalidate_asid_entry asid)
 2. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S40 rv rv' a rva rv'a rvb\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvc s. (asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rva)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid) \<and> True\<rbrace>
 3. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'42 rv rv' a rva rv'a rv'b\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv'c s. (asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rv'a)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid) \<and> True\<rbrace>
 4. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P33 rv rv' a rva) (?P'35 rv rv' a rv'a) (flush_space asid) (flush_space asid)
 5. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S34 rv rv' a rva\<rbrace> flush_space asid \<lbrace>\<lambda>rvb s. ?P39 rv rv' a rva rv'a rvb s \<and> ?S40 rv rv' a rva rv'a rvb s\<rbrace>
 6. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S'36 rv rv' a rv'a\<rbrace> flush_space asid \<lbrace>\<lambda>rv'b s. ?P'41 rv rv' a rva rv'a rv'b s \<and> ?S'42 rv rv' a rva rv'a rv'b s\<rbrace>
 7. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = rv'a (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> rv'a (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. ?P33 rv rv' a rva s \<and> ?S34 rv rv' a rva s) (\<lambda>s. ?P'35 rv rv' a rv'a s \<and> ?S'36 rv rv' a rv'a s) (return ()) (return ())
 8. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?P19 rv rv' a) (?P'19 rv rv' a) (get_asid_pool a) (get_asid_pool a)
 9. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rva s. ?P33 rv rv' a rva s \<and> ?S34 rv rv' a rva s\<rbrace>
 10. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S'19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rv'a s. ?P'35 rv rv' a rv'a s \<and> ?S'36 rv rv' a rv'a s\<rbrace>
A total of 14 subgoals... proof (prove)
goal (25 subgoals):
 1. \<And>rv rv' a rva rv'a rvb rv'b P Q R S st. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>states_equiv_for P Q R S st\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
 2. \<And>rv rv' a rva rv'a rvb rv'b P Q R S st. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>states_equiv_for P Q R S st\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
 3. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 4. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 5. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>
 6. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>
 7. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 8. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 9. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
 10. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
A total of 25 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 2. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 3. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
 4. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
 5. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (irq_state_of_state s)\<rbrace>
 6. \<And>rv rv' a rva rv'a rvb rv'b P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv s. P (irq_state_of_state s)\<rbrace>
 7. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S40 rv rv' a rva rv'a rvb\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvc s. (asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rva)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid) \<and> True\<rbrace>
 8. \<And>rv rv' a rva rv'a rvb rv'b. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd; True\<rbrakk> \<Longrightarrow> \<lbrace>?S'42 rv rv' a rva rv'a rv'b\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rv'c s. (asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rv'a)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid) \<and> True\<rbrace>
 9. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P33 rv rv' a rva) (?P'35 rv rv' a rv'a) (flush_space asid) (flush_space asid)
 10. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S34 rv rv' a rva\<rbrace> flush_space asid \<lbrace>\<lambda>rvb s. True \<and> ?S40 rv rv' a rva rv'a rvb s\<rbrace>
A total of 19 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?P33 rv rv' a rva) (?P'35 rv rv' a rv'a) (flush_space asid) (flush_space asid)
 2. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S34 rv rv' a rva\<rbrace> flush_space asid \<lbrace>\<lambda>rvb s. True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rva)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 3. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S'36 rv rv' a rv'a\<rbrace> flush_space asid \<lbrace>\<lambda>rv'b s. True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rv'a)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 4. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = rv'a (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> rv'a (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. ?P33 rv rv' a rva s \<and> ?S34 rv rv' a rva s) (\<lambda>s. ?P'35 rv rv' a rv'a s \<and> ?S'36 rv rv' a rv'a s) (return ()) (return ())
 5. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?P19 rv rv' a) (?P'19 rv rv' a) (get_asid_pool a) (get_asid_pool a)
 6. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rva s. ?P33 rv rv' a rva s \<and> ?S34 rv rv' a rva s\<rbrace>
 7. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S'19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rv'a s. ?P'35 rv rv' a rv'a s \<and> ?S'36 rv rv' a rv'a s\<rbrace>
 8. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P19 rv rv' a s \<and> ?S19 rv rv' a s
 9. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P'19 rv rv' a s \<and> ?S'19 rv rv' a s
 10. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
A total of 11 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>rv rv' a rva rv'a P Q R S st. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>states_equiv_for P Q R S st\<rbrace> flush_space asid \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
 2. \<And>rv rv' a rva rv'a P Q R S st. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>states_equiv_for P Q R S st\<rbrace> flush_space asid \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>
 3. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 4. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 5. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>
 6. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>
 7. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 8. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 9. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
 10. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
A total of 22 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 2. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>
 3. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
 4. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>
 5. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (irq_state_of_state s)\<rbrace>
 6. \<And>rv rv' a rva rv'a P. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (irq_state_of_state s)\<rbrace>
 7. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S34 rv rv' a rva\<rbrace> flush_space asid \<lbrace>\<lambda>rvb s. True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rva)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 8. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = Some pd; rv'a (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> \<lbrace>?S'36 rv rv' a rv'a\<rbrace> flush_space asid \<lbrace>\<lambda>rv'b s. True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rv'a)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 9. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = rv'a (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> rv'a (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. True \<and> ?S34 rv rv' a rva s) (\<lambda>s. True \<and> ?S'36 rv rv' a rv'a s) (return ()) (return ())
 10. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?P19 rv rv' a) (?P'19 rv rv' a) (get_asid_pool a) (get_asid_pool a)
A total of 16 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' a rva rv'a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rva (UCAST(32 \<rightarrow> 10) asid) = rv'a (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> rv'a (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd \<longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rva)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid) (\<lambda>s. asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rv'a)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid) (return ()) (return ())
 2. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?P19 rv rv' a) (?P'19 rv rv' a) (get_asid_pool a) (get_asid_pool a)
 3. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rva s. True \<and> True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rva)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 4. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S'19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rv'a s. True \<and> True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rv'a)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 5. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P19 rv rv' a s \<and> ?S19 rv rv' a s
 6. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P'19 rv rv' a s \<and> ?S'19 rv rv' a s
 7. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 8. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?P19 rv rv' a) (?P'19 rv rv' a) (get_asid_pool a) (get_asid_pool a)
 2. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rva s. True \<and> True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rva)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 3. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S'19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rv'a s. True \<and> True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rv'a)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 4. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P19 rv rv' a s \<and> ?S19 rv rv' a s
 5. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P'19 rv rv' a s \<and> ?S'19 rv rv' a s
 6. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 7. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?Q610 rv rv' a) (?Q'610 rv rv' a) (get_asid_pool a) (get_asid_pool a)
 2. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; ?P19 rv rv' a s\<rbrakk> \<Longrightarrow> ?Q610 rv rv' a s
 3. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; ?P'19 rv rv' a s\<rbrakk> \<Longrightarrow> ?Q'610 rv rv' a s
 4. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rva s. True \<and> True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rva)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 5. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S'19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rv'a s. True \<and> True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rv'a)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 6. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P19 rv rv' a s \<and> ?S19 rv rv' a s
 7. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P'19 rv rv' a s \<and> ?S'19 rv rv' a s
 8. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 9. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; ?P19 rv rv' a s\<rbrakk> \<Longrightarrow> Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0
 2. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; ?P'19 rv rv' a s\<rbrakk> \<Longrightarrow> Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0
 3. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rva s. True \<and> True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rva)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 4. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S'19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rv'a s. True \<and> True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rv'a)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 5. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P19 rv rv' a s \<and> ?S19 rv rv' a s
 6. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ?P'19 rv rv' a s \<and> ?S'19 rv rv' a s
 7. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 8. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rva s. asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rva)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 2. \<And>rv rv' a. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?S'19 rv rv' a\<rbrace> get_asid_pool a \<lbrace>\<lambda>rv'a s. True \<and> True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool rv'a)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid\<rbrace>
 3. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> ?S19 rv rv' a s
 4. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> ?S'19 rv rv' a s
 5. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 6. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> (\<forall>pool. ako_at (ASIDPool pool) a s \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool pool)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid)
 2. \<And>rv rv' a s. \<lbrakk>rv (asid_high_bits_of asid) = Some a; rv' (asid_high_bits_of asid) = Some a; rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> (\<forall>pool. ako_at (ASIDPool pool) a s \<longrightarrow> True \<and> True \<and> asid_table s (asid_high_bits_of asid) = Some a \<and> kheap s a = Some (ArchObj (ASIDPool pool)) \<and> asid \<noteq> 0 \<and> is_subject_asid aag asid)
 3. \<And>rv rv'. \<lbrakk>True; rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od)
 4. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. rv (asid_high_bits_of asid) \<noteq> rv' (asid_high_bits_of asid) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (\<lambda>s. rv' = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (case rv (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) (case rv' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od)
 2. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s t b ba. \<lbrakk>asid_table s (asid_high_bits_of asid) \<noteq> asid_table t (asid_high_bits_of asid); ((), b) \<in> fst ((case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) s); ((), ba) \<in> fst ((case asid_table t (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) t); is_subject_asid aag asid; asid \<noteq> 0; \<forall>d\<in>subjectReads (pasPolicy aag) (pasSubject aag). equiv_for (\<lambda>x. d = pasObjectAbs aag x) kheap s t \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) underlying_memory (machine_state s) (machine_state t) \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) device_state (machine_state s) (machine_state t) \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt s t \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) ekheap s t \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt_list s t \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) is_original_cap s t \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_states s t \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_irq_node s t \<and> equiv_for (\<lambda>x. d \<in> pasDomainAbs aag x) ready_queues s t \<and> (\<forall>asid. asid \<noteq> 0 \<and> d = pasASIDAbs aag asid \<longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table t (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table s (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr s = typ_at (AArch AASIDPool) pool_ptr t \<and> (\<forall>asid_pool asid_pool'. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid)))); cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); affects_equiv aag l s t\<rbrakk> \<Longrightarrow> (\<forall>d\<in>subjectReads (pasPolicy aag) (pasSubject aag). equiv_for (\<lambda>x. d = pasObjectAbs aag x) kheap b ba \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) underlying_memory (machine_state b) (machine_state ba) \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) device_state (machine_state b) (machine_state ba) \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt b ba \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) ekheap b ba \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt_list b ba \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) is_original_cap b ba \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_states b ba \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_irq_node b ba \<and> equiv_for (\<lambda>x. d \<in> pasDomainAbs aag x) ready_queues b ba \<and> (\<forall>asid. asid \<noteq> 0 \<and> d = pasASIDAbs aag asid \<longrightarrow> asid_table b (asid_high_bits_of asid) = asid_table ba (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table b (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr b = typ_at (AArch AASIDPool) pool_ptr ba \<and> (\<forall>asid_pool asid_pool'. kheap b pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap ba pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))))) \<and> cur_thread b = cur_thread ba \<and> cur_domain b = cur_domain ba \<and> scheduler_action b = scheduler_action ba \<and> work_units_completed b = work_units_completed ba \<and> equiv_irq_state (machine_state b) (machine_state ba) \<and> affects_equiv aag l b ba
 2. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s t b ba. \<lbrakk>asid_table s (asid_high_bits_of asid) \<noteq> asid_table t (asid_high_bits_of asid); ((), b) \<in> fst ((case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) s); ((), ba) \<in> fst ((case asid_table t (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) t); is_subject_asid aag asid; asid \<noteq> 0; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); affects_equiv aag l s t; equiv_for (\<lambda>x. pasASIDAbs aag asid = pasObjectAbs aag x) kheap s t \<and> equiv_for (\<lambda>x. pasASIDAbs aag asid = pasObjectAbs aag x) underlying_memory (machine_state s) (machine_state t) \<and> equiv_for (\<lambda>x. pasASIDAbs aag asid = pasObjectAbs aag x) device_state (machine_state s) (machine_state t) \<and> equiv_for ((\<lambda>x. pasASIDAbs aag asid = pasObjectAbs aag x) \<circ> fst) cdt s t \<and> equiv_for (\<lambda>x. pasASIDAbs aag asid = pasObjectAbs aag x) ekheap s t \<and> equiv_for ((\<lambda>x. pasASIDAbs aag asid = pasObjectAbs aag x) \<circ> fst) cdt_list s t \<and> equiv_for ((\<lambda>x. pasASIDAbs aag asid = pasObjectAbs aag x) \<circ> fst) is_original_cap s t \<and> equiv_for (\<lambda>x. pasASIDAbs aag asid = pasIRQAbs aag x) interrupt_states s t \<and> equiv_for (\<lambda>x. pasASIDAbs aag asid = pasIRQAbs aag x) interrupt_irq_node s t \<and> equiv_for (\<lambda>x. pasASIDAbs aag asid \<in> pasDomainAbs aag x) ready_queues s t \<and> (\<forall>asida. asida \<noteq> 0 \<and> pasASIDAbs aag asid = pasASIDAbs aag asida \<longrightarrow> asid_table s (asid_high_bits_of asida) = asid_table t (asid_high_bits_of asida) \<and> (\<forall>pool_ptr. asid_table s (asid_high_bits_of asida) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr s = typ_at (AArch AASIDPool) pool_ptr t \<and> (\<forall>asid_pool asid_pool'. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asida) = asid_pool' (UCAST(32 \<rightarrow> 10) asida))))\<rbrakk> \<Longrightarrow> (\<forall>d\<in>subjectReads (pasPolicy aag) (pasSubject aag). equiv_for (\<lambda>x. d = pasObjectAbs aag x) kheap b ba \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) underlying_memory (machine_state b) (machine_state ba) \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) device_state (machine_state b) (machine_state ba) \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt b ba \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) ekheap b ba \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt_list b ba \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) is_original_cap b ba \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_states b ba \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_irq_node b ba \<and> equiv_for (\<lambda>x. d \<in> pasDomainAbs aag x) ready_queues b ba \<and> (\<forall>asid. asid \<noteq> 0 \<and> d = pasASIDAbs aag asid \<longrightarrow> asid_table b (asid_high_bits_of asid) = asid_table ba (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table b (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr b = typ_at (AArch AASIDPool) pool_ptr ba \<and> (\<forall>asid_pool asid_pool'. kheap b pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap ba pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))))) \<and> cur_thread b = cur_thread ba \<and> cur_domain b = cur_domain ba \<and> scheduler_action b = scheduler_action ba \<and> work_units_completed b = work_units_completed ba \<and> equiv_irq_state (machine_state b) (machine_state ba) \<and> affects_equiv aag l b ba
 2. \<And>s t b ba. \<lbrakk>asid_table s (asid_high_bits_of asid) \<noteq> asid_table t (asid_high_bits_of asid); ((), b) \<in> fst ((case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) s); ((), ba) \<in> fst ((case asid_table t (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) t); is_subject_asid aag asid; asid \<noteq> 0; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); affects_equiv aag l s t; pasASIDAbs aag asid \<notin> subjectReads (pasPolicy aag) (pasSubject aag)\<rbrakk> \<Longrightarrow> (\<forall>d\<in>subjectReads (pasPolicy aag) (pasSubject aag). equiv_for (\<lambda>x. d = pasObjectAbs aag x) kheap b ba \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) underlying_memory (machine_state b) (machine_state ba) \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) device_state (machine_state b) (machine_state ba) \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt b ba \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) ekheap b ba \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt_list b ba \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) is_original_cap b ba \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_states b ba \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_irq_node b ba \<and> equiv_for (\<lambda>x. d \<in> pasDomainAbs aag x) ready_queues b ba \<and> (\<forall>asid. asid \<noteq> 0 \<and> d = pasASIDAbs aag asid \<longrightarrow> asid_table b (asid_high_bits_of asid) = asid_table ba (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table b (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr b = typ_at (AArch AASIDPool) pool_ptr ba \<and> (\<forall>asid_pool asid_pool'. kheap b pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap ba pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))))) \<and> cur_thread b = cur_thread ba \<and> cur_domain b = cur_domain ba \<and> scheduler_action b = scheduler_action ba \<and> work_units_completed b = work_units_completed ba \<and> equiv_irq_state (machine_state b) (machine_state ba) \<and> affects_equiv aag l b ba
 3. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s t b ba. \<lbrakk>asid_table s (asid_high_bits_of asid) \<noteq> asid_table t (asid_high_bits_of asid); ((), b) \<in> fst ((case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) s); ((), ba) \<in> fst ((case asid_table t (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) t); is_subject_asid aag asid; asid \<noteq> 0; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); affects_equiv aag l s t; pasASIDAbs aag asid \<notin> subjectReads (pasPolicy aag) (pasSubject aag)\<rbrakk> \<Longrightarrow> (\<forall>d\<in>subjectReads (pasPolicy aag) (pasSubject aag). equiv_for (\<lambda>x. d = pasObjectAbs aag x) kheap b ba \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) underlying_memory (machine_state b) (machine_state ba) \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) device_state (machine_state b) (machine_state ba) \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt b ba \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) ekheap b ba \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt_list b ba \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) is_original_cap b ba \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_states b ba \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_irq_node b ba \<and> equiv_for (\<lambda>x. d \<in> pasDomainAbs aag x) ready_queues b ba \<and> (\<forall>asid. asid \<noteq> 0 \<and> d = pasASIDAbs aag asid \<longrightarrow> asid_table b (asid_high_bits_of asid) = asid_table ba (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table b (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr b = typ_at (AArch AASIDPool) pool_ptr ba \<and> (\<forall>asid_pool asid_pool'. kheap b pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap ba pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))))) \<and> cur_thread b = cur_thread ba \<and> cur_domain b = cur_domain ba \<and> scheduler_action b = scheduler_action ba \<and> work_units_completed b = work_units_completed ba \<and> equiv_irq_state (machine_state b) (machine_state ba) \<and> affects_equiv aag l b ba
 2. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s t b ba. \<lbrakk>asid_table s (asid_high_bits_of asid) \<noteq> asid_table t (asid_high_bits_of asid); ((), b) \<in> fst ((case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) s); ((), ba) \<in> fst ((case asid_table t (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) t); asid \<noteq> 0; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); affects_equiv aag l s t; pasASIDAbs aag asid \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_read_asid aag asid\<rbrakk> \<Longrightarrow> (\<forall>d\<in>subjectReads (pasPolicy aag) (pasSubject aag). equiv_for (\<lambda>x. d = pasObjectAbs aag x) kheap b ba \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) underlying_memory (machine_state b) (machine_state ba) \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) device_state (machine_state b) (machine_state ba) \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt b ba \<and> equiv_for (\<lambda>x. d = pasObjectAbs aag x) ekheap b ba \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) cdt_list b ba \<and> equiv_for ((\<lambda>x. d = pasObjectAbs aag x) \<circ> fst) is_original_cap b ba \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_states b ba \<and> equiv_for (\<lambda>x. d = pasIRQAbs aag x) interrupt_irq_node b ba \<and> equiv_for (\<lambda>x. d \<in> pasDomainAbs aag x) ready_queues b ba \<and> (\<forall>asid. asid \<noteq> 0 \<and> d = pasASIDAbs aag asid \<longrightarrow> asid_table b (asid_high_bits_of asid) = asid_table ba (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table b (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr b = typ_at (AArch AASIDPool) pool_ptr ba \<and> (\<forall>asid_pool asid_pool'. kheap b pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap ba pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))))) \<and> cur_thread b = cur_thread ba \<and> cur_domain b = cur_domain ba \<and> scheduler_action b = scheduler_action ba \<and> work_units_completed b = work_units_completed ba \<and> equiv_irq_state (machine_state b) (machine_state ba) \<and> affects_equiv aag l b ba
 2. \<lbrace>K (asid \<noteq> 0 \<and> is_subject_asid aag asid)\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>rv s. rv = asid_table s \<and> is_subject_asid aag asid \<and> asid \<noteq> 0\<rbrace> proof (prove)
goal:
No subgoals!