theory CNode_DR

lemma dcorres_set_asid_pool_empty:
  "dcorres dc \<top> (valid_idle and asid_pool_at a and
                 (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)))
    (mapM_x PageTableUnmap_D.empty_slot
                            (map (Pair a) [0 .e. 2 ^ ARM_A.asid_low_bits - 1]))
    (set_asid_pool a Map.empty)" apply (unfold set_asid_pool_empty) apply (rule dcorres_list_all2_mapM_[where F="\<lambda>x y. snd x = snd (transform_asid y)"]) apply (clarsimp simp:PageTableUnmap_D.empty_slot_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (subgoal_tac "aa=a", clarsimp) apply (clarsimp simp:assert_opt_def split:option.splits) apply (intro conjI, clarsimp simp:opt_cap_asid_pool_Some typ_at_eq_kheap_obj) apply (clarsimp, intro conjI, clarsimp) apply (rule dcorres_symb_exec_r) apply (rule corres_guard_imp) apply (rule dcorres_set_asid_pool_none_trivial) apply (wp | clarsimp | simp)+ apply (rule dcorres_symb_exec_r) apply (rule corres_dummy_return_pr) apply (rule corres_guard_imp) apply (rule corres_split[OF dummy_remove_cdt_asid_pool_slot]) apply (clarsimp) apply (rule dcorres_set_asid_pool) apply fastforce apply clarsimp apply (clarsimp simp:transform_asid_pool_entry_def) apply (wp | clarsimp)+ apply simp apply (wp get_asid_pool_triv | clarsimp simp:typ_at_eq_kheap_obj obj_at_def swp_def)+ apply (subgoal_tac "(aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ ARM_A.asid_low_bits])") apply clarsimp apply (clarsimp simp del:set_map simp: suffix_def) apply (wp | clarsimp simp:swp_def)+ apply (clarsimp simp:list_all2_iff transform_asid_def asid_low_bits_def set_zip) apply (clarsimp simp: upto_enum_def ucast_of_nat_small unat_of_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) (mapM_x PageTableUnmap_D.empty_slot (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])) (set_asid_pool a (\<lambda>x. None)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) (mapM_x PageTableUnmap_D.empty_slot (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])) (mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. 2 ^ local.asid_low_bits - 1]) proof (prove)
goal (4 subgoals):
 1. \<And>x xs y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>a. True) (valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) (PageTableUnmap_D.empty_slot x) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)
 2. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 3. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 4. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (4 subgoals):
 1. \<And>aa xs y ys. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>a. True) (\<lambda>b. valid_idle b \<and> typ_at (AArch AASIDPool) a b \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a b) (cdt b)) (do x <- get;
cap <- assert_opt (opt_cap (aa, snd (transform_asid y)) x);
if cap = cdl_cap.NullCap then return () else do remove_parent (aa, snd (transform_asid y));
KHeap_D.set_cap (aa, snd (transform_asid y)) cdl_cap.NullCap
od
od) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)
 2. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 3. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 4. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (4 subgoals):
 1. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (aa, snd (transform_asid y)) (transform s'));
if cap = cdl_cap.NullCap then return () else do remove_parent (aa, snd (transform_asid y));
KHeap_D.set_cap (aa, snd (transform_asid y)) cdl_cap.NullCap
od
od) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)
 2. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 3. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 4. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (5 subgoals):
 1. \<And>xs y ys s'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (a, snd (transform_asid y)) (transform s'));
if cap = cdl_cap.NullCap then return () else do remove_parent (a, snd (transform_asid y));
KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap
od
od) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)
 2. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 3. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 4. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 5. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (5 subgoals):
 1. \<And>xs y ys s'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> (opt_cap (a, snd (transform_asid y)) (transform s') = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') fail (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)) \<and> (\<forall>x2. (x2 = cdl_cap.NullCap \<longrightarrow> opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)) \<and> (x2 \<noteq> cdl_cap.NullCap \<longrightarrow> opt_cap (a, snd (transform_asid y)) (transform s') = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (a, snd (transform_asid y));
KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap
od) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)))
 2. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 3. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 4. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 5. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (5 subgoals):
 1. \<And>xs y ys s'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> \<forall>x2. (x2 = cdl_cap.NullCap \<longrightarrow> opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)) \<and> (x2 \<noteq> cdl_cap.NullCap \<longrightarrow> opt_cap (a, snd (transform_asid y)) (transform s') = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (a, snd (transform_asid y));
KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap
od) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od))
 2. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 3. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 4. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 5. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (6 subgoals):
 1. \<And>xs y ys s'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)
 2. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> x2 \<noteq> cdl_cap.NullCap \<longrightarrow> opt_cap (a, snd (transform_asid y)) (transform s') = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (a, snd (transform_asid y));
KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap
od) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)
 3. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 4. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 5. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 6. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (8 subgoals):
 1. \<And>xs y ys s' rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (?Q'45 xs y ys s' rv) (return ()) (set_asid_pool a (rv(UCAST(32 \<rightarrow> 10) y := None)))
 2. \<And>xs y ys s'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'45 xs y ys s'\<rbrace>
 3. \<And>xs y ys s' cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> x2 \<noteq> cdl_cap.NullCap \<longrightarrow> opt_cap (a, snd (transform_asid y)) (transform s') = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (a, snd (transform_asid y));
KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap
od) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)
 5. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 6. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 7. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 8. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (10 subgoals):
 1. \<And>xs y ys s' rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?Q49 xs y ys s' rv) (?Q'49 xs y ys s' rv) (return ()) (set_asid_pool a (rv(UCAST(32 \<rightarrow> 10) y := None)))
 2. \<And>xs y ys s' rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> ?Q49 xs y ys s' rv s
 3. \<And>xs y ys s' rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap; ?Q'45 xs y ys s' rv s\<rbrakk> \<Longrightarrow> ?Q'49 xs y ys s' rv s
 4. \<And>xs y ys s'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'45 xs y ys s'\<rbrace>
 5. \<And>xs y ys s' cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> x2 \<noteq> cdl_cap.NullCap \<longrightarrow> opt_cap (a, snd (transform_asid y)) (transform s') = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (a, snd (transform_asid y));
KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap
od) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)
 7. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 8. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 9. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 10. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (9 subgoals):
 1. \<And>xs y ys s' rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> opt_cap (a, snd (transform_asid y)) s = Some cdl_cap.NullCap
 2. \<And>xs y ys s' rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap; ?Q'45 xs y ys s' rv s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (ASIDPool rv) a) s
 3. \<And>xs y ys s'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'45 xs y ys s'\<rbrace>
 4. \<And>xs y ys s' cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); opt_cap (a, snd (transform_asid y)) (transform s') = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> x2 \<noteq> cdl_cap.NullCap \<longrightarrow> opt_cap (a, snd (transform_asid y)) (transform s') = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (a, snd (transform_asid y));
KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap
od) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)
 6. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 7. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 8. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 9. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (5 subgoals):
 1. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (a, snd (transform_asid y));
KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap
od) (do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od)
 2. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 3. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 4. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 5. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (7 subgoals):
 1. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (?Q'68 xs y ys s' x2 rv) (do ya <- remove_parent (a, snd (transform_asid y));
KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap
od) (set_asid_pool a (rv(UCAST(32 \<rightarrow> 10) y := None)))
 2. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'68 xs y ys s' x2\<rbrace>
 3. \<And>xs y ys s' x2 cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 5. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 6. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 7. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (7 subgoals):
 1. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (?Q'68 xs y ys s' x2 rv) (do ya <- remove_parent (a, snd (transform_asid y));
KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap
od) (do return (?b72 xs y ys s' x2 rv);
set_asid_pool a (rv(UCAST(32 \<rightarrow> 10) y := None))
od)
 2. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'68 xs y ys s' x2\<rbrace>
 3. \<And>xs y ys s' x2 cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 5. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 6. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 7. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (9 subgoals):
 1. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> dcorres dc (?Q74 xs y ys s' x2 rv) (?Q'74 xs y ys s' x2 rv) (do ya <- remove_parent (a, snd (transform_asid y));
KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap
od) (do return (?b72 xs y ys s' x2 rv);
set_asid_pool a (rv(UCAST(32 \<rightarrow> 10) y := None))
od)
 2. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; transform s' = s\<rbrakk> \<Longrightarrow> ?Q74 xs y ys s' x2 rv s
 3. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; ?Q'68 xs y ys s' x2 rv s\<rbrakk> \<Longrightarrow> ?Q'74 xs y ys s' x2 rv s
 4. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'68 xs y ys s' x2\<rbrace>
 5. \<And>xs y ys s' x2 cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 7. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 8. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 9. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (11 subgoals):
 1. \<And>xs y ys s' x2 rv ya rv'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; dc ya rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R78 xs y ys s' x2 rv ya) (?R'78 xs y ys s' x2 rv rv') (KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap) (K_bind (set_asid_pool a (rv(UCAST(32 \<rightarrow> 10) y := None))) rv')
 2. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q78 xs y ys s' x2 rv\<rbrace> remove_parent (a, snd (transform_asid y)) \<lbrace>?R78 xs y ys s' x2 rv\<rbrace>
 3. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 xs y ys s' x2 rv\<rbrace> return (?b72 xs y ys s' x2 rv) \<lbrace>?R'78 xs y ys s' x2 rv\<rbrace>
 4. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q78 xs y ys s' x2 rv) s
 5. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; ?Q'68 xs y ys s' x2 rv s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch AASIDPool) a and ?Q'78 xs y ys s' x2 rv) s
 6. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'68 xs y ys s' x2\<rbrace>
 7. \<And>xs y ys s' x2 cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 9. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 10. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>xs y ys s' x2 rv rv'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> dcorres dc (?R78 xs y ys s' x2 rv ()) (?R'78 xs y ys s' x2 rv rv') (KHeap_D.set_cap (a, snd (transform_asid y)) cdl_cap.NullCap) (set_asid_pool a (rv(UCAST(32 \<rightarrow> 10) y := None)))
 2. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q78 xs y ys s' x2 rv\<rbrace> remove_parent (a, snd (transform_asid y)) \<lbrace>?R78 xs y ys s' x2 rv\<rbrace>
 3. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 xs y ys s' x2 rv\<rbrace> return (?b72 xs y ys s' x2 rv) \<lbrace>?R'78 xs y ys s' x2 rv\<rbrace>
 4. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q78 xs y ys s' x2 rv) s
 5. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; ?Q'68 xs y ys s' x2 rv s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch AASIDPool) a and ?Q'78 xs y ys s' x2 rv) s
 6. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'68 xs y ys s' x2\<rbrace>
 7. \<And>xs y ys s' x2 cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 9. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 10. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>xs y ys s' x2 rv rv'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> rv(UCAST(32 \<rightarrow> 10) y := None) = (?pool85 xs y ys s' x2 rv rv')(UCAST(32 \<rightarrow> 10) (?asid85 xs y ys s' x2 rv rv') := ?pd85 xs y ys s' x2 rv rv')
 2. \<And>xs y ys s' x2 rv rv'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> snd (transform_asid y) = snd (transform_asid (?asid85 xs y ys s' x2 rv rv'))
 3. \<And>xs y ys s' x2 rv rv'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> cdl_cap.NullCap = transform_asid_pool_entry (?pd85 xs y ys s' x2 rv rv')
 4. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q78 xs y ys s' x2 rv\<rbrace> remove_parent (a, snd (transform_asid y)) \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 xs y ys s' x2 rv\<rbrace> return (?b72 xs y ys s' x2 rv) \<lbrace>\<lambda>rv'. valid_idle and ako_at (ASIDPool (?pool85 xs y ys s' x2 rv rv')) a\<rbrace>
 6. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q78 xs y ys s' x2 rv) s
 7. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; ?Q'68 xs y ys s' x2 rv s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch AASIDPool) a and ?Q'78 xs y ys s' x2 rv) s
 8. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'68 xs y ys s' x2\<rbrace>
 9. \<And>xs y ys s' x2 cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>xs y ys s' x2 rv rv'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> snd (transform_asid y) = snd (transform_asid y)
 2. \<And>xs y ys s' x2 rv rv'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> cdl_cap.NullCap = transform_asid_pool_entry None
 3. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q78 xs y ys s' x2 rv\<rbrace> remove_parent (a, snd (transform_asid y)) \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 xs y ys s' x2 rv\<rbrace> return (?b72 xs y ys s' x2 rv) \<lbrace>\<lambda>rv'. valid_idle and ako_at (ASIDPool rv) a\<rbrace>
 5. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q78 xs y ys s' x2 rv) s
 6. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; ?Q'68 xs y ys s' x2 rv s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch AASIDPool) a and ?Q'78 xs y ys s' x2 rv) s
 7. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'68 xs y ys s' x2\<rbrace>
 8. \<And>xs y ys s' x2 cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 10. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>xs y ys s' x2 rv rv'. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> cdl_cap.NullCap = transform_asid_pool_entry None
 2. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q78 xs y ys s' x2 rv\<rbrace> remove_parent (a, snd (transform_asid y)) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 xs y ys s' x2 rv\<rbrace> return (?b72 xs y ys s' x2 rv) \<lbrace>\<lambda>rv'. valid_idle and ako_at (ASIDPool rv) a\<rbrace>
 4. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q78 xs y ys s' x2 rv) s
 5. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; ?Q'68 xs y ys s' x2 rv s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch AASIDPool) a and ?Q'78 xs y ys s' x2 rv) s
 6. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'68 xs y ys s' x2\<rbrace>
 7. \<And>xs y ys s' x2 cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 9. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 10. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q78 xs y ys s' x2 rv\<rbrace> remove_parent (a, snd (transform_asid y)) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>xs y ys s' x2 rv. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 xs y ys s' x2 rv\<rbrace> return (?b72 xs y ys s' x2 rv) \<lbrace>\<lambda>rv'. valid_idle and ako_at (ASIDPool rv) a\<rbrace>
 3. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q78 xs y ys s' x2 rv) s
 4. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; ?Q'68 xs y ys s' x2 rv s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch AASIDPool) a and ?Q'78 xs y ys s' x2 rv) s
 5. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'68 xs y ys s' x2\<rbrace>
 6. \<And>xs y ys s' x2 cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 8. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 9. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 10. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (7 subgoals):
 1. \<And>xs y ys s' x2 rv s. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2; ?Q'68 xs y ys s' x2 rv s\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> valid_idle s \<and> typ_at (AArch AASIDPool) a s \<and> valid_idle s \<and> ako_at (ASIDPool rv) a s
 2. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>?Q'68 xs y ys s' x2\<rbrace>
 3. \<And>xs y ys s' x2 cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 5. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 6. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 7. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (6 subgoals):
 1. \<And>xs y ys s' x2. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> valid_idle s \<and> typ_at (AArch AASIDPool) a s \<and> valid_idle s \<and> ako_at (ASIDPool r) a s\<rbrace>
 2. \<And>xs y ys s' x2 cs. \<lbrakk>suffix ((a, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; typ_at (AArch AASIDPool) a s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); x2 \<noteq> cdl_cap.NullCap; opt_cap (a, snd (transform_asid y)) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>aa xs y ys s'. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; True; valid_idle s' \<and> typ_at (AArch AASIDPool) a s' \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s')\<rbrakk> \<Longrightarrow> aa = a
 4. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 5. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 6. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (4 subgoals):
 1. \<And>aa xs y ys s' f. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); kheap s' a = Some (ArchObj (ASIDPool f))\<rbrakk> \<Longrightarrow> aa = a
 2. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 3. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 4. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (5 subgoals):
 1. \<And>aa xs y ys s' f. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); kheap s' a = Some (ArchObj (ASIDPool f)); (aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ local.asid_low_bits])\<rbrakk> \<Longrightarrow> aa = a
 2. \<And>aa xs y ys s' f. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); kheap s' a = Some (ArchObj (ASIDPool f))\<rbrakk> \<Longrightarrow> (aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ local.asid_low_bits])
 3. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 4. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 5. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (4 subgoals):
 1. \<And>aa xs y ys s' f. \<lbrakk>suffix ((aa, snd (transform_asid y)) # xs) (map (Pair a) [0..<2 ^ local.asid_low_bits]); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]; valid_idle s'; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s') (cdt s'); kheap s' a = Some (ArchObj (ASIDPool f))\<rbrakk> \<Longrightarrow> (aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ local.asid_low_bits])
 2. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 3. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 4. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (3 subgoals):
 1. \<And>x y xs. \<lbrakk>snd x = snd (transform_asid y); suffix (x # xs) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. True\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv a. True\<rbrace>
 2. \<And>x y ys. \<lbrakk>snd x = snd (transform_asid y); suffix (y # ys) [0 .e. 2 ^ local.asid_low_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) y := None))
od \<lbrace>\<lambda>rv. valid_idle and typ_at (AArch AASIDPool) a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 3. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0 .e. 2 ^ local.asid_low_bits - 1]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>x y. snd x = snd (transform_asid y)) (map (Pair a) [0..<2 ^ local.asid_low_bits]) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (1 subgoal):
 1. \<And>b. b < 1024 \<Longrightarrow> b = unat (UCAST(32 \<rightarrow> 10) ([0 .e. 0x3FF] ! b)) proof (prove)
goal:
No subgoals!