theory VSpace_R

lemma deleteASID_corres:
  "corres dc
          (invs and valid_etcbs and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0))
          (pspace_aligned' and pspace_distinct' and no_0_obj'
              and valid_arch_state' and cur_tcb')
          (delete_asid asid pd) (deleteASID asid pd)" apply (simp add: delete_asid_def deleteASID_def) apply (rule corres_guard_imp) apply (rule corres_split[OF corres_gets_asid]) apply (corres_cases; clarsimp) apply (rule_tac P="\<lambda>s. asid_high_bits_of asid \<in> dom (asidTable o ucast) \<longrightarrow>
                             asid_pool_at (the ((asidTable o ucast) (asid_high_bits_of asid))) s" and
                      P'="pspace_aligned' and pspace_distinct'" and
                      Q="invs and valid_etcbs and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0) and
                         (\<lambda>s. arm_asid_table (arch_state s) = asidTable \<circ> ucast)" in
                      corres_split) apply (simp add: dom_def) apply (rule get_asid_pool_corres_inv') apply (rule corres_when, simp add: mask_asid_low_bits_ucast_ucast) apply (rule corres_split[OF flushSpace_corres[where pd=pd]]) apply (rule corres_split[OF invalidateASIDEntry_corres[where pd=pd]]) apply (rule_tac P="asid_pool_at (the (asidTable (ucast (asid_high_bits_of asid))))
                               and valid_etcbs"
                        and P'="pspace_aligned' and pspace_distinct'"
                         in corres_split) apply (simp del: fun_upd_apply) apply (rule setObject_ASIDPool_corres') apply (simp add: inv_def mask_asid_low_bits_ucast_ucast) apply (rule ext) apply (clarsimp simp: o_def) apply (erule notE) apply (erule ucast_ucast_eq, simp, simp) apply (rule corres_split[OF getCurThread_corres]) apply simp apply (rule setVMRoot_corres) apply wp+ apply (simp del: fun_upd_apply) apply (fold cur_tcb_def) apply (wp set_asid_pool_asid_map_unmap
                       set_asid_pool_vspace_objs_unmap_single
                       set_asid_pool_vs_lookup_unmap')+ apply simp apply (fold cur_tcb'_def) apply (wp invalidate_asid_entry_invalidates)+ apply (wp | clarsimp simp: o_def)+ apply (subgoal_tac "vspace_at_asid asid pd s") apply (auto simp: obj_at_def a_type_def graph_of_def
                          invs_vspace_objs[simplified]
                   split: if_split_asm)[1] apply (simp add: vspace_at_asid_def) apply (rule vs_lookupI) apply (simp add: vs_asid_refs_def) apply (rule image_eqI[OF refl]) apply (erule graph_ofI) apply (rule r_into_rtrancl) apply simp apply (erule vs_lookup1I [OF _ _ refl]) apply (simp add: vs_refs_def) apply (rule image_eqI[rotated], erule graph_ofI) apply (simp add: mask_asid_low_bits_ucast_ucast) apply wp apply (simp add: o_def) apply (wp getASID_wp) apply clarsimp apply assumption apply wp+ apply clarsimp apply (clarsimp simp: valid_arch_state_def valid_asid_table_def
                  dest!: invs_arch_state) apply blast apply (clarsimp simp: valid_arch_state'_def valid_asid_table'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') (delete_asid asid pd) (deleteASID asid pd) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') (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 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
od) (do asidTable <- gets (armKSASIDTable \<circ> ksArchState);
case asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) of None \<Rightarrow> return () | Some poolPtr \<Rightarrow> do pool <- liftM (inv asidpool.ASIDPool) (getObject poolPtr);
when (pool (asid && mask local.asid_low_bits) = Some pd) (do y <- flushSpace asid;
y <- invalidateASIDEntry asid;
y <- setObject poolPtr (asidpool.ASIDPool (pool(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od)
od
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q4 ?Q'4 (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 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
od) (do asidTable <- gets (armKSASIDTable \<circ> ksArchState);
case asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) of None \<Rightarrow> return () | Some poolPtr \<Rightarrow> do pool <- liftM (inv asidpool.ASIDPool) (getObject poolPtr);
when (pool (asid && mask local.asid_low_bits) = Some pd) (do y <- flushSpace asid;
y <- invalidateASIDEntry asid;
y <- setObject poolPtr (asidpool.ASIDPool (pool(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od)
od
od)
 2. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ?Q4 s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ?Q'4 s proof (prove)
goal (5 subgoals):
 1. \<And>asid_table asidTable. asid_table = asidTable \<circ> UCAST(7 \<rightarrow> 32) \<Longrightarrow> corres dc (?R8 asid_table) (?R'8 asidTable) (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 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 asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) of None \<Rightarrow> return () | Some poolPtr \<Rightarrow> do pool <- liftM (inv asidpool.ASIDPool) (getObject poolPtr);
when (pool (asid && mask local.asid_low_bits) = Some pd) (do y <- flushSpace asid;
y <- invalidateASIDEntry asid;
y <- setObject poolPtr (asidpool.ASIDPool (pool(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od)
od)
 2. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>?R8\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>?R'8\<rbrace>
 4. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> corres dc (?Q51 (asidTable \<circ> UCAST(7 \<rightarrow> 32)) x2) (?B'53 asidTable) (do pool <- get_asid_pool x2;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od) (do pool <- liftM (inv asidpool.ASIDPool) (getObject x2);
when (pool (asid && mask local.asid_low_bits) = Some pd) (do y <- flushSpace asid;
y <- invalidateASIDEntry asid;
y <- setObject x2 (asidpool.ASIDPool (pool(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od)
od)
 2. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_table s) \<and> (\<forall>x. asid_table (asid_high_bits_of asid) = Some x \<longrightarrow> ?Q51 asid_table x s)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> ?B'53 asidTable s\<rbrace>
 4. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> corres (?r'66 asidTable x2) (\<lambda>s. asid_high_bits_of asid \<in> dom (asidTable \<circ> UCAST(7 \<rightarrow> 32)) \<longrightarrow> typ_at (AArch AASIDPool) (the ((asidTable \<circ> UCAST(7 \<rightarrow> 32)) (asid_high_bits_of asid))) s) (pspace_aligned' and pspace_distinct') (get_asid_pool x2) (liftM (inv asidpool.ASIDPool) (getObject x2))
 2. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; ?r'66 asidTable x2 rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R66 asidTable x2 rv) (?R'66 asidTable x2 rv') (when (rv (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)) (when (rv' (asid && mask local.asid_low_bits) = Some pd) (do y <- flushSpace asid;
y <- invalidateASIDEntry asid;
y <- setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od))
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>?R66 asidTable x2\<rbrace>
 4. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>?R'66 asidTable x2\<rbrace>
 5. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 7. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> corres (\<lambda>x. ?r'66 asidTable x2 x \<circ> inv asidpool.ASIDPool) (typ_at (AArch AASIDPool) x2) (pspace_aligned' and pspace_distinct') (get_asid_pool x2) (getObject x2)
 2. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; ?r'66 asidTable x2 rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R66 asidTable x2 rv) (?R'66 asidTable x2 rv') (when (rv (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)) (when (rv' (asid && mask local.asid_low_bits) = Some pd) (do y <- flushSpace asid;
y <- invalidateASIDEntry asid;
y <- setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od))
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>?R66 asidTable x2\<rbrace>
 4. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>?R'66 asidTable x2\<rbrace>
 5. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 7. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> corres dc (?R66 asidTable x2 rv) (?R'66 asidTable x2 rv') (when (rv (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)) (when (rv' (asid && mask local.asid_low_bits) = Some pd) (do y <- flushSpace asid;
y <- invalidateASIDEntry asid;
y <- setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od))
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>?R66 asidTable x2\<rbrace>
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>?R'66 asidTable x2\<rbrace>
 4. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 6. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> corres dc (?P81 asidTable x2 rv) (?P'83 asidTable x2 rv') (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od) (do y <- flushSpace asid;
y <- invalidateASIDEntry asid;
y <- setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od)
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> ?P81 asidTable x2 rv x\<rbrace>
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> ?P'83 asidTable x2 rv' x\<rbrace>
 4. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 6. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (9 subgoals):
 1. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?R86 asidTable x2 rv rv' rva) (?R'86 asidTable x2 rv rv' rv'a) (do y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od) (do y <- invalidateASIDEntry asid;
y <- setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od)
 2. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>?R86 asidTable x2 rv rv'\<rbrace>
 3. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>?R'86 asidTable x2 rv rv'\<rbrace>
 4. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 5. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
 6. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 7. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 8. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 9. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (11 subgoals):
 1. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> corres dc (?R96 asidTable x2 rv rv' rva rv'a rvb) (?R'96 asidTable x2 rv rv' rva rv'a rv'b) (do y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od) (do y <- setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od)
 2. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>?R96 asidTable x2 rv rv' rva rv'a\<rbrace>
 3. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>?R'96 asidTable x2 rv rv' rva rv'a\<rbrace>
 4. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 5. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 6. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 7. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
 8. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 10. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> corres (?r'106 asidTable x2 rv rv' rva rv'a rvb rv'b) (typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs) (pspace_aligned' and pspace_distinct') (set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None))) (setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))))
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; ?r'106 asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrakk> \<Longrightarrow> corres dc (?R106 asidTable x2 rv rv' rva rv'a rvb rv'b rvc) (?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 3. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 5. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and ?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace>
 6. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 7. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 8. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 9. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 10. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> corres (?r'106 asidTable x2 (rv' \<circ> UCAST(10 \<rightarrow> 32)) rv' () () () ()) (typ_at (AArch AASIDPool) x2 and valid_etcbs) (pspace_aligned' and pspace_distinct') (set_asid_pool x2 ((\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))(UCAST(32 \<rightarrow> 10) asid := None))) (setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))))
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; ?r'106 asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrakk> \<Longrightarrow> corres dc (?R106 asidTable x2 rv rv' rva rv'a rvb rv'b rvc) (?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 3. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 5. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and ?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace>
 6. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 7. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 8. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 9. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 10. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))(UCAST(32 \<rightarrow> 10) asid := None) = inv asidpool.ASIDPool (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<circ> UCAST(10 \<rightarrow> 32)
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> corres dc (?R106 asidTable x2 rv rv' rva rv'a rvb rv'b rvc) (?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 3. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 5. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and ?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace>
 6. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 7. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 8. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 9. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 10. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) asid then None else rv' (UCAST(10 \<rightarrow> 32) a)) = (\<lambda>a. if a = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid) then None else rv' a) \<circ> UCAST(10 \<rightarrow> 32)
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> corres dc (?R106 asidTable x2 rv rv' rva rv'a rvb rv'b rvc) (?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 3. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 5. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and ?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace>
 6. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 7. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 8. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 9. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 10. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>asidTable x2 rv rv' x. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> (if x = UCAST(32 \<rightarrow> 10) asid then None else rv' (UCAST(10 \<rightarrow> 32) x)) = ((\<lambda>a. if a = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid) then None else rv' a) \<circ> UCAST(10 \<rightarrow> 32)) x
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> corres dc (?R106 asidTable x2 rv rv' rva rv'a rvb rv'b rvc) (?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 3. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 5. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and ?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace>
 6. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 7. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 8. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 9. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 10. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>asidTable x2 rv' x. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; x \<noteq> UCAST(32 \<rightarrow> 10) asid; UCAST(10 \<rightarrow> 32) x = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> rv' (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) = None
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> corres dc (?R106 asidTable x2 rv rv' rva rv'a rvb rv'b rvc) (?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 3. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 5. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and ?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace>
 6. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 7. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 8. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 9. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 10. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>asidTable x2 rv' x. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; UCAST(10 \<rightarrow> 32) x = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)\<rbrakk> \<Longrightarrow> x = UCAST(32 \<rightarrow> 10) asid
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> corres dc (?R106 asidTable x2 rv rv' rva rv'a rvb rv'b rvc) (?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 3. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 5. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and ?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace>
 6. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 7. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 8. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 9. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 10. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> corres dc (?R106 asidTable x2 rv rv' rva rv'a rvb rv'b rvc) (?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 3. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>?R'106 asidTable x2 rv rv' rva rv'a rvb rv'b\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and ?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace>
 5. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 6. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 7. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 8. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 9. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
 10. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c rvd rv'd. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c; rvd = rv'd\<rbrakk> \<Longrightarrow> corres dc (?R133 asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c rvd) (?R'133 asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c rv'd) (set_vm_root rvd) (setVMRoot rv'd)
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q134 asidTable x2 rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets cur_thread \<lbrace>?R133 asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrace>
 3. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'135 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c\<rbrace> getCurThread \<lbrace>?R'133 asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q134 asidTable x2 rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 5. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'135 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
 6. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and ?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace>
 7. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 8. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 9. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 10. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>asidTable x2 rv rv' rvd rv'd. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); rvd = rv'd\<rbrakk> \<Longrightarrow> corres dc (?R133 asidTable x2 (rv' \<circ> UCAST(10 \<rightarrow> 32)) rv' () () () () () () rv'd) (?R'133 asidTable x2 (rv' \<circ> UCAST(10 \<rightarrow> 32)) rv' () () () () () () rv'd) (set_vm_root rv'd) (setVMRoot rv'd)
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q134 asidTable x2 rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets cur_thread \<lbrace>?R133 asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrace>
 3. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'135 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c\<rbrace> getCurThread \<lbrace>?R'133 asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q134 asidTable x2 rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 5. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'135 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
 6. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and ?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace>
 7. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 8. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 9. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 10. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q134 asidTable x2 rv rv' rva rv'a rvb rv'b rvc\<rbrace> gets cur_thread \<lbrace>\<lambda>a. tcb_at a and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs\<rbrace>
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b rvc rv'c. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b; dc rvc rv'c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'135 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c\<rbrace> getCurThread \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' a and no_0_obj'\<rbrace>
 3. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rvc. (\<lambda>_. True) and ?Q134 asidTable x2 rv rv' rva rv'a rvb rv'b rvc\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and ?Q'135 asidTable x2 rv rv' rva rv'a rvb rv'b rv'c\<rbrace>
 5. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and ?Q107 asidTable x2 rv rv' rva rv'a rvb\<rbrace>
 6. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 7. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 8. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 9. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 10. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
A total of 14 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?P'152 asidTable x2 rv rv' rva rv'a rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rv s. (tcb_at (cur_thread s) and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s\<rbrace>
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and (\<lambda>a. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' (ksCurThread a) and no_0_obj') a)\<rbrace>
 3. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and (\<lambda>s. True \<and> ?P'152 asidTable x2 rv rv' rva rv'a rvb s)\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 5. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 6. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 7. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 8. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
 9. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 10. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'152 asidTable x2 (rv' \<circ> UCAST(10 \<rightarrow> 32)) rv' () () ()\<rbrace> set_asid_pool x2 ((\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rv s. tcb_at (cur_thread s) s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_asid_map s \<and> unique_table_refs (caps_of_state s) \<and> valid_vs_lookup s \<and> valid_global_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_vspace_objs s\<rbrace>
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and (\<lambda>a. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' (ksCurThread a) and no_0_obj') a)\<rbrace>
 3. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and (\<lambda>s. True \<and> ?P'152 asidTable x2 rv rv' rva rv'a rvb s)\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 5. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 6. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 7. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 8. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
 9. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 10. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'152 asidTable x2 (rv' \<circ> UCAST(10 \<rightarrow> 32)) rv' () () ()\<rbrace> set_asid_pool x2 ((\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>\<lambda>rv s. cur_tcb s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_asid_map s \<and> unique_table_refs (caps_of_state s) \<and> valid_vs_lookup s \<and> valid_global_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_vspace_objs s\<rbrace>
 2. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>\<lambda>rv'c. (\<lambda>_. True) and (\<lambda>a. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' (ksCurThread a) and no_0_obj') a)\<rbrace>
 3. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and (\<lambda>s. True \<and> ?P'152 asidTable x2 rv rv' rva rv'a rvb s)\<rbrace>
 4. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and ?Q'108 asidTable x2 rv rv' rva rv'a rv'b\<rbrace>
 5. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 6. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 7. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 8. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
 9. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 10. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>asidTable x2 rv rv' rva rv'a rvb rv'b. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc rvb rv'b\<rbrakk> \<Longrightarrow> \<lbrace>?P'234 asidTable x2 rv rv' rva rv'a rv'b\<rbrace> setObject x2 (asidpool.ASIDPool (rv'(asid && mask local.asid_low_bits := None))) \<lbrace>\<lambda>rv s. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' (ksCurThread s) and no_0_obj') s\<rbrace>
 2. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and (\<lambda>s. True \<and> cur_tcb s \<and> valid_arch_state s \<and> valid_objs s \<and> (valid_asid_map and ako_at (arch_kernel_obj.ASIDPool (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))) x2 and (\<lambda>s. \<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x2 \<longrightarrow> arm_asid_map (arch_state s) asida = None)) s \<and> unique_table_refs (caps_of_state s) \<and> (valid_vs_lookup and obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (arch_kernel_obj.ASIDPool ap') \<and> graph_of ((\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))(UCAST(32 \<rightarrow> 10) asid := None)) \<subseteq> graph_of ap') x2) s \<and> (valid_global_objs and valid_arch_state) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (valid_vspace_objs and ako_at (arch_kernel_obj.ASIDPool (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))) x2) s)\<rbrace>
 3. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and (\<lambda>s. True \<and> ?P'234 asidTable x2 rv rv' rva rv'a rv'b s)\<rbrace>
 4. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 5. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 6. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 7. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
 8. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 10. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'234 asidTable x2 (rv' \<circ> UCAST(10 \<rightarrow> 32)) rv' () () ()\<rbrace> setObject x2 (asidpool.ASIDPool (\<lambda>a. if a = asid && mask local.asid_low_bits then None else rv' a)) \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> tcb_at' (ksCurThread s) s \<and> no_0_obj' s\<rbrace>
 2. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and (\<lambda>s. True \<and> cur_tcb s \<and> valid_arch_state s \<and> valid_objs s \<and> (valid_asid_map and ako_at (arch_kernel_obj.ASIDPool (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))) x2 and (\<lambda>s. \<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x2 \<longrightarrow> arm_asid_map (arch_state s) asida = None)) s \<and> unique_table_refs (caps_of_state s) \<and> (valid_vs_lookup and obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (arch_kernel_obj.ASIDPool ap') \<and> graph_of ((\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))(UCAST(32 \<rightarrow> 10) asid := None)) \<subseteq> graph_of ap') x2) s \<and> (valid_global_objs and valid_arch_state) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (valid_vspace_objs and ako_at (arch_kernel_obj.ASIDPool (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))) x2) s)\<rbrace>
 3. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and (\<lambda>s. True \<and> ?P'234 asidTable x2 rv rv' rva rv'a rv'b s)\<rbrace>
 4. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 5. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 6. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 7. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
 8. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 10. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'234 asidTable x2 (rv' \<circ> UCAST(10 \<rightarrow> 32)) rv' () () ()\<rbrace> setObject x2 (asidpool.ASIDPool (\<lambda>a. if a = asid && mask local.asid_low_bits then None else rv' a)) \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s\<rbrace>
 2. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 asidTable x2 rv rv' rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>rvb. typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) and valid_etcbs and (\<lambda>s. True \<and> cur_tcb s \<and> valid_arch_state s \<and> valid_objs s \<and> (valid_asid_map and ako_at (arch_kernel_obj.ASIDPool (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))) x2 and (\<lambda>s. \<forall>asida\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asida = UCAST(32 \<rightarrow> 10) asid \<longrightarrow> asid_table s (asid_high_bits_of asida) = Some x2 \<longrightarrow> arm_asid_map (arch_state s) asida = None)) s \<and> unique_table_refs (caps_of_state s) \<and> (valid_vs_lookup and obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (arch_kernel_obj.ASIDPool ap') \<and> graph_of ((\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))(UCAST(32 \<rightarrow> 10) asid := None)) \<subseteq> graph_of ap') x2) s \<and> (valid_global_objs and valid_arch_state) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (valid_vspace_objs and ako_at (arch_kernel_obj.ASIDPool (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))) x2) s)\<rbrace>
 3. \<And>asidTable x2 rv rv' rva rv'a. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'102 asidTable x2 rv rv' rv'a\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>rv'b. pspace_aligned' and pspace_distinct' and (\<lambda>s. True \<and> ?P'234 asidTable x2 rv rv' rva rv'a rv'b s)\<rbrace>
 4. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q91 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rva. valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct and ?Q101 asidTable x2 rv rv' rva\<rbrace>
 5. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'102 asidTable x2 rv rv' rv'a\<rbrace>
 6. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and ?Q91 asidTable x2 rv) x\<rbrace>
 7. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
 8. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 10. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?P'438 asidTable x2 rv\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> pspace_distinct s \<and> typ_at (AArch AASIDPool) (the (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)))) s \<and> valid_etcbs s \<and> True \<and> cur_tcb s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_asid_map s \<and> ako_at (arch_kernel_obj.ASIDPool (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))) x2 s \<and> (valid_asid_map and valid_arch_state and K (asid \<le> mask local.asid_bits) and (\<lambda>s. asid_table s (asid_high_bits_of asid) = Some x2)) s \<and> unique_table_refs (caps_of_state s) \<and> valid_vs_lookup s \<and> obj_at (\<lambda>a. \<exists>ap'. a = ArchObj (arch_kernel_obj.ASIDPool ap') \<and> graph_of ((\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))(UCAST(32 \<rightarrow> 10) asid := None)) \<subseteq> graph_of ap') x2 s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_vspace_objs s \<and> ako_at (arch_kernel_obj.ASIDPool (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))) x2 s\<rbrace>
 2. \<And>asidTable x2 rv rv'. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'92 asidTable x2 rv'\<rbrace> flushSpace asid \<lbrace>\<lambda>rv'a. pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)\<rbrace>
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asidTable \<circ> UCAST(7 \<rightarrow> 32))\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>rv x. rv (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd and (\<lambda>s. valid_vspace_objs s \<and> valid_asid_map s \<and> K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) s \<and> vspace_at_asid asid pd s \<and> valid_vs_lookup s \<and> ?P'438 asidTable x2 rv s)) x\<rbrace>
 4. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'92 asidTable x2 rv') x\<rbrace>
 5. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 7. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> unique_table_refs (caps_of_state s) \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_arch_state s \<and> vspace_at_asid asid pd s \<and> valid_vspace_objs s \<and> valid_asid_map s \<and> vspace_at_asid asid pd s \<and> valid_vs_lookup s \<and> unique_table_refs (caps_of_state s) \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> pspace_distinct s \<and> typ_at (AArch AASIDPool) x2 s \<and> cur_tcb s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_asid_map s \<and> valid_arch_state s \<and> unique_table_refs (caps_of_state s) \<and> valid_vs_lookup s \<and> obj_at (\<lambda>a. \<exists>ap'. a = ArchObj (arch_kernel_obj.ASIDPool ap') \<and> graph_of (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) asid then None else pool a) \<subseteq> graph_of ap') x2 s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_vspace_objs s
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 3. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 5. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> unique_table_refs (caps_of_state s) \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_arch_state s \<and> vspace_at_asid asid pd s \<and> valid_vspace_objs s \<and> valid_asid_map s \<and> vspace_at_asid asid pd s \<and> valid_vs_lookup s \<and> unique_table_refs (caps_of_state s) \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> pspace_distinct s \<and> typ_at (AArch AASIDPool) x2 s \<and> cur_tcb s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_asid_map s \<and> valid_arch_state s \<and> unique_table_refs (caps_of_state s) \<and> valid_vs_lookup s \<and> obj_at (\<lambda>a. \<exists>ap'. a = ArchObj (arch_kernel_obj.ASIDPool ap') \<and> graph_of (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) asid then None else pool a) \<subseteq> graph_of ap') x2 s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_vspace_objs s
 2. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> vspace_at_asid asid pd s
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 4. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 6. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> vspace_at_asid asid pd s
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 3. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 5. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 3. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 5. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> ?ref'694 asidTable x2 s pool \<in> vs_asid_refs (asid_table s)
 2. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> (?ref'694 asidTable x2 s pool, [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 4. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 6. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> ?ref'694 asidTable x2 s pool \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` graph_of (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x))
 2. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> (?ref'694 asidTable x2 s pool, [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 4. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 6. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> ?x699 asidTable x2 s pool \<in> graph_of (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x))
 2. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> (case ?x699 asidTable x2 s pool of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 4. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 6. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> (case (asid_high_bits_of asid, x2) of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 3. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 5. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> (case (asid_high_bits_of asid, x2) of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> vs_lookup1 s
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 3. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 5. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); ako_at (arch_kernel_obj.ASIDPool pool) x2 s; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], x2), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> vs_lookup1 s
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 3. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 5. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs (ArchObj (arch_kernel_obj.ASIDPool pool))
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 3. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 5. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` graph_of pool
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 3. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 5. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>asidTable x2 s pool. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s = (\<lambda>x. asidTable (UCAST(7 \<rightarrow> 32) x)); pool (UCAST(32 \<rightarrow> 10) asid) = Some pd\<rbrakk> \<Longrightarrow> (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) = (case (UCAST(32 \<rightarrow> 10) asid, pd) of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x))
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 3. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 5. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject x2) \<lbrace>\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x\<rbrace>
 2. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 4. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> getObject x2 \<lbrace>(\<lambda>rv' x. rv' (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s)) x) \<circ> inv asidpool.ASIDPool\<rbrace>
 2. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 4. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?Q'77 asidTable\<rbrace> getObject x2 \<lbrace>\<lambda>x xa. inv asidpool.ASIDPool x (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> pspace_aligned' xa \<and> pspace_distinct' xa \<and> no_0_obj' xa \<and> pspace_aligned' xa \<and> pspace_distinct' xa \<and> no_0_obj' xa \<and> pspace_aligned' xa \<and> pspace_distinct' xa \<and> pspace_aligned' xa \<and> pspace_distinct' xa \<and> valid_arch_state' xa \<and> cur_tcb' xa \<and> no_0_obj' xa\<rbrace>
 2. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 4. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable x2 s. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; ?Q'77 asidTable s\<rbrakk> \<Longrightarrow> \<forall>ko. ko_at' ko x2 s \<longrightarrow> inv asidpool.ASIDPool ko (asid && mask local.asid_low_bits) = Some pd \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s
 2. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 4. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable x2 s ko. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; ?Q'77 asidTable s; ko_at' ko x2 s; inv asidpool.ASIDPool ko (asid && mask local.asid_low_bits) = Some pd\<rbrakk> \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_arch_state' s \<and> cur_tcb' s \<and> no_0_obj' s
 2. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and ?Q'77 asidTable) s\<rbrace>
 4. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q8\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_tablea s. (asid_tablea (asid_high_bits_of asid) = None \<longrightarrow> ?Q50 asid_tablea s) \<and> (\<forall>x. asid_tablea (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>s. asid_high_bits_of asid \<in> dom asid_tablea \<longrightarrow> typ_at (AArch AASIDPool) (the (asid_tablea (asid_high_bits_of asid))) s) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. asid_table s = asid_tablea))) s)\<rbrace>
 2. \<lbrace>?Q'8\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. ?A'52 asidTable s \<and> (pspace_aligned' and pspace_distinct' and (\<lambda>a. pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> valid_arch_state' a \<and> cur_tcb' a \<and> no_0_obj' a)) s\<rbrace>
 3. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 4. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and valid_etcbs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = None \<longrightarrow> True) \<and> (\<forall>x. (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = Some x \<longrightarrow> ((\<lambda>sa. asid_high_bits_of asid \<in> dom ((arm_asid_table \<circ> arch_state) s) \<longrightarrow> typ_at (AArch AASIDPool) (the ((arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid))) sa) and (invs and valid_etcbs and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>sa. asid_table sa = (arm_asid_table \<circ> arch_state) s))) s))) s
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> (pspace_aligned' and pspace_distinct' and (\<lambda>a. pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> valid_arch_state' a \<and> cur_tcb' a \<and> no_0_obj' a)) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>invs s; valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = Some x\<rbrakk> \<Longrightarrow> typ_at (AArch AASIDPool) x s
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> (pspace_aligned' and pspace_distinct' and (\<lambda>a. pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> valid_arch_state' a \<and> cur_tcb' a \<and> no_0_obj' a)) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>valid_etcbs s; asid \<le> mask local.asid_bits; asid \<noteq> 0; asid_table s (asid_high_bits_of asid) = Some x; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> typ_at (AArch AASIDPool) x s
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> (pspace_aligned' and pspace_distinct' and (\<lambda>a. pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> valid_arch_state' a \<and> cur_tcb' a \<and> no_0_obj' a)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> (pspace_aligned' and pspace_distinct' and (\<lambda>a. pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> valid_arch_state' a \<and> cur_tcb' a \<and> no_0_obj' a)) s)) s proof (prove)
goal:
No subgoals!