theory VSpace_R

lemma performASIDPoolInvocation_corres:
  "ap' = asid_pool_invocation_map ap \<Longrightarrow>
  corres dc
          (valid_objs and pspace_aligned and pspace_distinct and valid_apinv ap and valid_etcbs)
          (pspace_aligned' and pspace_distinct' and valid_apinv' ap')
          (perform_asid_pool_invocation ap)
          (performASIDPoolInvocation ap')" apply (clarsimp simp: perform_asid_pool_invocation_def performASIDPoolInvocation_def) apply (cases ap, simp add: asid_pool_invocation_map_def) apply (rename_tac word1 word2 prod) apply (rule corres_guard_imp) apply (rule corres_split[OF getSlotCap_corres]) apply simp apply (rule_tac F="\<exists>p asid. rv = Structures_A.ArchObjectCap (ARM_A.PageDirectoryCap p asid)" in corres_gen_asm) apply clarsimp apply (rule_tac Q="valid_objs and pspace_aligned and pspace_distinct and asid_pool_at word2 and valid_etcbs and
                         cte_wp_at (\<lambda>c. cap_master_cap c =
                                        cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a,b)"
                      in corres_split) apply simp apply (rule get_asid_pool_corres_inv') apply (rule corres_split) apply (rule updateCap_same_master) apply simp apply (rule corres_rel_imp) apply simp apply (rule setObject_ASIDPool_corres[OF refl]) apply (simp add: inv_def) apply (rule ext) apply (clarsimp simp: mask_asid_low_bits_ucast_ucast) apply (drule ucast_ucast_eq, simp, simp, simp) apply assumption apply (wp set_cap_typ_at)+ apply clarsimp apply (erule cte_wp_at_weakenE) apply (clarsimp simp: is_cap_simps cap_master_cap_simps dest!: cap_master_cap_eqDs) apply (wp getASID_wp) apply (wp get_cap_wp getCTE_wp)+ apply (clarsimp simp: valid_apinv_def cte_wp_at_def cap_master_cap_def is_pd_cap_def obj_at_def) apply (clarsimp simp: a_type_def) apply (clarsimp simp: cte_wp_at_ctes_of valid_apinv'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ap' = asid_pool_invocation_map ap \<Longrightarrow> corres dc (valid_objs and pspace_aligned and pspace_distinct and valid_apinv ap and valid_etcbs) (pspace_aligned' and pspace_distinct' and valid_apinv' ap') (perform_asid_pool_invocation ap) (performASIDPoolInvocation ap') proof (prove)
goal (1 subgoal):
 1. ap' = asid_pool_invocation_map ap \<Longrightarrow> corres dc (valid_objs and pspace_aligned and pspace_distinct and valid_apinv ap and valid_etcbs) (pspace_aligned' and pspace_distinct' and valid_apinv' (asid_pool_invocation_map ap)) (case ap of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> do pd_cap <- get_cap ct_slot;
case pd_cap of cap.ArchObjectCap (arch_cap.PageDirectoryCap pd_base x) \<Rightarrow> do pool <- get_asid_pool pool_ptr;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid \<mapsto> pd_base));
set_cap (cap.ArchObjectCap $ arch_cap.PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od | cap.ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) (case asid_pool_invocation_map ap of asidpool_invocation.Assign asid poolPtr ctSlot \<Rightarrow> do oldcap <- getSlotCap ctSlot;
pool <- liftM (inv asidpool.ASIDPool) $ getObject poolPtr;
cap <- liftM capCap $ return oldcap;
updateCap ctSlot (capability.ArchObjectCap $ capPDMappedASID_update (\<lambda>_. Just asid) cap);
pool' <- return (pool aLU [(asid && mask asidLowBits, Just $ capPDBasePtr cap)]);
setObject poolPtr $ asidpool.ASIDPool pool'
od) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>ap' = asidpool_invocation.Assign x1 x2 (cte_map x3); ap = asid_pool_invocation.Assign x1 x2 x3\<rbrakk> \<Longrightarrow> corres dc (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign x1 x2 x3) and valid_etcbs) (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign x1 x2 (cte_map x3))) (get_cap x3 >>= case_cap fail (\<lambda>bool word nat1 nat2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word bool set. fail) (\<lambda>word nat list. fail) (\<lambda>word. fail) fail fail (\<lambda>word. fail) (\<lambda>word option nat. fail) (case_arch_cap (\<lambda>word1 word2. fail) fail (\<lambda>bool word set vmpage_size option. fail) (\<lambda>word option. fail) (\<lambda>pd_base x. do pool <- get_asid_pool x2;
y <- set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some x1))) x3;
set_asid_pool x2 (pool(UCAST(32 \<rightarrow> 10) x1 \<mapsto> pd_base))
od))) (do oldcap <- getSlotCap (cte_map x3);
pool <- liftM (inv asidpool.ASIDPool) (getObject x2);
y <- updateCap (cte_map x3) (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap oldcap)));
setObject x2 (asidpool.ASIDPool (pool(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap oldcap))))
od) proof (prove)
goal (1 subgoal):
 1. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> corres dc (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) (get_cap prod >>= case_cap fail (\<lambda>bool word nat1 nat2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word bool set. fail) (\<lambda>word nat list. fail) (\<lambda>word. fail) fail fail (\<lambda>word. fail) (\<lambda>word option nat. fail) (case_arch_cap (\<lambda>word1 word2. fail) fail (\<lambda>bool word set vmpage_size option. fail) (\<lambda>word option. fail) (\<lambda>pd_base x. do pool <- get_asid_pool word2;
y <- set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some word1))) prod;
set_asid_pool word2 (pool(UCAST(32 \<rightarrow> 10) word1 \<mapsto> pd_base))
od))) (do oldcap <- getSlotCap (cte_map prod);
pool <- liftM (inv asidpool.ASIDPool) (getObject word2);
y <- updateCap (cte_map prod) (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some word1) (capCap oldcap)));
setObject word2 (asidpool.ASIDPool (pool(word1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap oldcap))))
od) proof (prove)
goal (3 subgoals):
 1. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> corres dc (?Q2 word1 word2 prod) (?Q'2 word1 word2 prod) (get_cap prod >>= case_cap fail (\<lambda>bool word nat1 nat2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word bool set. fail) (\<lambda>word nat list. fail) (\<lambda>word. fail) fail fail (\<lambda>word. fail) (\<lambda>word option nat. fail) (case_arch_cap (\<lambda>word1 word2. fail) fail (\<lambda>bool word set vmpage_size option. fail) (\<lambda>word option. fail) (\<lambda>pd_base x. do pool <- get_asid_pool word2;
y <- set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some word1))) prod;
set_asid_pool word2 (pool(UCAST(32 \<rightarrow> 10) word1 \<mapsto> pd_base))
od))) (do oldcap <- getSlotCap (cte_map prod);
pool <- liftM (inv asidpool.ASIDPool) (getObject word2);
y <- updateCap (cte_map prod) (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some word1) (capCap oldcap)));
setObject word2 (asidpool.ASIDPool (pool(word1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap oldcap))))
od)
 2. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q2 word1 word2 prod s
 3. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> ?Q'2 word1 word2 prod s proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> cte_map prod = cte_map prod
 2. \<And>word1 word2 prod rv oldcap. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; cap_relation rv oldcap\<rbrakk> \<Longrightarrow> corres dc (?R6 word1 word2 prod rv) (?R'6 word1 word2 prod oldcap) (case rv of cap.ArchObjectCap (arch_cap.PageDirectoryCap pd_base xa) \<Rightarrow> do pool <- get_asid_pool word2;
y <- set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some word1))) prod;
set_asid_pool word2 (pool(UCAST(32 \<rightarrow> 10) word1 \<mapsto> pd_base))
od | cap.ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail) (do pool <- liftM (inv asidpool.ASIDPool) (getObject word2);
y <- updateCap (cte_map prod) (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some word1) (capCap oldcap)));
setObject word2 (asidpool.ASIDPool (pool(word1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap oldcap))))
od)
 3. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>?R6 word1 word2 prod\<rbrace>
 4. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>?R'6 word1 word2 prod\<rbrace>
 5. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 6. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 prod rv oldcap. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; cap_relation rv oldcap\<rbrakk> \<Longrightarrow> corres dc (?R6 word1 word2 prod rv) (?R'6 word1 word2 prod oldcap) (case rv of cap.ArchObjectCap (arch_cap.PageDirectoryCap pd_base xa) \<Rightarrow> do pool <- get_asid_pool word2;
y <- set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some word1))) prod;
set_asid_pool word2 (pool(UCAST(32 \<rightarrow> 10) word1 \<mapsto> pd_base))
od | cap.ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail) (do pool <- liftM (inv asidpool.ASIDPool) (getObject word2);
y <- updateCap (cte_map prod) (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some word1) (capCap oldcap)));
setObject word2 (asidpool.ASIDPool (pool(word1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap oldcap))))
od)
 2. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>?R6 word1 word2 prod\<rbrace>
 3. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>?R'6 word1 word2 prod\<rbrace>
 4. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 5. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 prod rv oldcap. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; cap_relation rv oldcap; \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid)\<rbrakk> \<Longrightarrow> corres dc (?P13 word1 word2 prod rv) (?R'6 word1 word2 prod oldcap) (case rv of cap.ArchObjectCap (arch_cap.PageDirectoryCap pd_base xa) \<Rightarrow> do pool <- get_asid_pool word2;
y <- set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some word1))) prod;
set_asid_pool word2 (pool(UCAST(32 \<rightarrow> 10) word1 \<mapsto> pd_base))
od | cap.ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail) (do pool <- liftM (inv asidpool.ASIDPool) (getObject word2);
y <- updateCap (cte_map prod) (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some word1) (capCap oldcap)));
setObject word2 (asidpool.ASIDPool (pool(word1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap oldcap))))
od)
 2. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. ?P13 word1 word2 prod rv and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 3. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>?R'6 word1 word2 prod\<rbrace>
 4. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 5. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> corres dc (?P13 word1 word2 (a, b) (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (?R'6 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))) (do pool <- get_asid_pool word2;
y <- set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b);
set_asid_pool word2 (pool(UCAST(32 \<rightarrow> 10) word1 \<mapsto> p))
od) (do pool <- liftM (inv asidpool.ASIDPool) (getObject word2);
y <- updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1)));
setObject word2 (asidpool.ASIDPool (pool(word1 && mask local.asid_low_bits \<mapsto> p)))
od)
 2. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. ?P13 word1 word2 prod rv and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 3. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>?R'6 word1 word2 prod\<rbrace>
 4. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 5. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> corres (?r'20 word1 word2 a b p asid) (?P29 word1 word2 (a, b) (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (?P'28 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))) (get_asid_pool word2) (liftM (inv asidpool.ASIDPool) (getObject word2))
 2. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); ?r'20 word1 word2 a b p asid rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R20 word1 word2 a b p asid rv) (?R'20 word1 word2 a b p asid rv') (do y <- set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b);
set_asid_pool word2 (rv(UCAST(32 \<rightarrow> 10) word1 \<mapsto> p))
od) (do y <- updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1)));
setObject word2 (asidpool.ASIDPool (rv'(word1 && mask local.asid_low_bits \<mapsto> p)))
od)
 3. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>?R20 word1 word2 a b p asid\<rbrace>
 4. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>?R'20 word1 word2 a b p asid\<rbrace>
 5. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. ?P29 word1 word2 prod rv and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 6. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. ?P'28 word1 word2 prod a and ?Q'27 word1 word2 prod a\<rbrace>
 7. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 8. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> corres (\<lambda>x. ?r'20 word1 word2 a b p asid x \<circ> inv asidpool.ASIDPool) (?P29 word1 word2 (a, b) (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (?P'28 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))) (get_asid_pool word2) (getObject word2)
 2. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); ?r'20 word1 word2 a b p asid rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R20 word1 word2 a b p asid rv) (?R'20 word1 word2 a b p asid rv') (do y <- set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b);
set_asid_pool word2 (rv(UCAST(32 \<rightarrow> 10) word1 \<mapsto> p))
od) (do y <- updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1)));
setObject word2 (asidpool.ASIDPool (rv'(word1 && mask local.asid_low_bits \<mapsto> p)))
od)
 3. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>?R20 word1 word2 a b p asid\<rbrace>
 4. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>?R'20 word1 word2 a b p asid\<rbrace>
 5. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. ?P29 word1 word2 prod rv and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 6. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. ?P'28 word1 word2 prod a and ?Q'27 word1 word2 prod a\<rbrace>
 7. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 8. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (7 subgoals):
 1. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> corres dc (?R20 word1 word2 a b p asid rv) (?R'20 word1 word2 a b p asid rv') (do y <- set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b);
set_asid_pool word2 (rv(UCAST(32 \<rightarrow> 10) word1 \<mapsto> p))
od) (do y <- updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1)));
setObject word2 (asidpool.ASIDPool (rv'(word1 && mask local.asid_low_bits \<mapsto> p)))
od)
 2. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>?R20 word1 word2 a b p asid\<rbrace>
 3. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>?R'20 word1 word2 a b p asid\<rbrace>
 4. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 5. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 6. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 7. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> corres (?r'33 word1 word2 a b p asid rv rv') (?P34 word1 word2 a b p asid rv) (?P'36 word1 word2 a b p asid rv') (set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b)) (updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))))
 2. \<And>word1 word2 a b p asid rv rv' rva rv'a. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32); ?r'33 word1 word2 a b p asid rv rv' rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?R33 word1 word2 a b p asid rv rv' rva) (?R'33 word1 word2 a b p asid rv rv' rv'a) (set_asid_pool word2 (rv(UCAST(32 \<rightarrow> 10) word1 \<mapsto> p))) (setObject word2 (asidpool.ASIDPool (rv'(word1 && mask local.asid_low_bits \<mapsto> p))))
 3. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 word1 word2 a b p asid rv\<rbrace> set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b) \<lbrace>?R33 word1 word2 a b p asid rv rv'\<rbrace>
 4. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 word1 word2 a b p asid rv'\<rbrace> updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))) \<lbrace>?R'33 word1 word2 a b p asid rv rv'\<rbrace>
 5. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>\<lambda>rv. ?P34 word1 word2 a b p asid rv and ?Q35 word1 word2 a b p asid rv\<rbrace>
 6. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. ?P'36 word1 word2 a b p asid rv' and ?Q'37 word1 word2 a b p asid rv'\<rbrace>
 7. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 8. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 9. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 10. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> cap_relation (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1)))
 2. \<And>word1 word2 a b p asid rv rv' rva rv'a. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?R33 word1 word2 a b p asid rv rv' rva) (?R'33 word1 word2 a b p asid rv rv' rv'a) (set_asid_pool word2 (rv(UCAST(32 \<rightarrow> 10) word1 \<mapsto> p))) (setObject word2 (asidpool.ASIDPool (rv'(word1 && mask local.asid_low_bits \<mapsto> p))))
 3. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 word1 word2 a b p asid rv\<rbrace> set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b) \<lbrace>?R33 word1 word2 a b p asid rv rv'\<rbrace>
 4. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 word1 word2 a b p asid rv'\<rbrace> updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))) \<lbrace>?R'33 word1 word2 a b p asid rv rv'\<rbrace>
 5. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q35 word1 word2 a b p asid rv\<rbrace>
 6. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'37 word1 word2 a b p asid rv'\<rbrace>
 7. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 8. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 9. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 10. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (9 subgoals):
 1. \<And>word1 word2 a b p asid rv rv' rva rv'a. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?R33 word1 word2 a b p asid rv rv' rva) (?R'33 word1 word2 a b p asid rv rv' rv'a) (set_asid_pool word2 (rv(UCAST(32 \<rightarrow> 10) word1 \<mapsto> p))) (setObject word2 (asidpool.ASIDPool (rv'(word1 && mask local.asid_low_bits \<mapsto> p))))
 2. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 word1 word2 a b p asid rv\<rbrace> set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b) \<lbrace>?R33 word1 word2 a b p asid rv rv'\<rbrace>
 3. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 word1 word2 a b p asid rv'\<rbrace> updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))) \<lbrace>?R'33 word1 word2 a b p asid rv rv'\<rbrace>
 4. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q35 word1 word2 a b p asid rv\<rbrace>
 5. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'37 word1 word2 a b p asid rv'\<rbrace>
 6. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 7. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 8. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 9. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 a b p asid rv rv' rva rv'a. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a\<rbrakk> \<Longrightarrow> corres (?r'47 word1 word2 a b p asid rv rv' rva rv'a) (?R33 word1 word2 a b p asid rv rv' rva) (?R'33 word1 word2 a b p asid rv rv' rv'a) (set_asid_pool word2 (rv(UCAST(32 \<rightarrow> 10) word1 \<mapsto> p))) (setObject word2 (asidpool.ASIDPool (rv'(word1 && mask local.asid_low_bits \<mapsto> p))))
 2. \<And>word1 word2 a b p asid rv rv' rva rv'a x y. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; ?r'47 word1 word2 a b p asid rv rv' rva rv'a x y\<rbrakk> \<Longrightarrow> dc x y
 3. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 word1 word2 a b p asid rv\<rbrace> set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b) \<lbrace>?R33 word1 word2 a b p asid rv rv'\<rbrace>
 4. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 word1 word2 a b p asid rv'\<rbrace> updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))) \<lbrace>?R'33 word1 word2 a b p asid rv rv'\<rbrace>
 5. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q35 word1 word2 a b p asid rv\<rbrace>
 6. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'37 word1 word2 a b p asid rv'\<rbrace>
 7. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 8. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 9. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 10. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))\<rbrakk> \<Longrightarrow> corres (?r'47 word1 word2 a b p asid (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a)) rv' () ()) (?R33 word1 word2 a b p asid (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a)) rv' ()) (?R'33 word1 word2 a b p asid (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a)) rv' ()) (set_asid_pool word2 (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) word1 then Some p else rv' (UCAST(10 \<rightarrow> 32) a))) (setObject word2 (asidpool.ASIDPool (\<lambda>a. if a = word1 && mask local.asid_low_bits then Some p else rv' a)))
 2. \<And>word1 word2 a b p asid rv rv' rva rv'a x y. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; ?r'47 word1 word2 a b p asid rv rv' rva rv'a x y\<rbrakk> \<Longrightarrow> dc x y
 3. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 word1 word2 a b p asid rv\<rbrace> set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b) \<lbrace>?R33 word1 word2 a b p asid rv rv'\<rbrace>
 4. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 word1 word2 a b p asid rv'\<rbrace> updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))) \<lbrace>?R'33 word1 word2 a b p asid rv rv'\<rbrace>
 5. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q35 word1 word2 a b p asid rv\<rbrace>
 6. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'37 word1 word2 a b p asid rv'\<rbrace>
 7. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 8. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 9. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 10. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))\<rbrakk> \<Longrightarrow> (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) word1 then Some p else rv' (UCAST(10 \<rightarrow> 32) a)) = inv asidpool.ASIDPool (asidpool.ASIDPool (\<lambda>a. if a = word1 && mask local.asid_low_bits then Some p else rv' a)) \<circ> UCAST(10 \<rightarrow> 32)
 2. \<And>word1 word2 a b p asid rv rv' rva rv'a x y. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc x y\<rbrakk> \<Longrightarrow> dc x y
 3. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 word1 word2 a b p asid rv\<rbrace> set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b) \<lbrace>\<lambda>a. typ_at (AArch AASIDPool) word2 and valid_etcbs\<rbrace>
 4. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 word1 word2 a b p asid rv'\<rbrace> updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))) \<lbrace>\<lambda>a. asid_pool_at' word2\<rbrace>
 5. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q35 word1 word2 a b p asid rv\<rbrace>
 6. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'37 word1 word2 a b p asid rv'\<rbrace>
 7. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 8. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 9. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 10. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 a b p rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))\<rbrakk> \<Longrightarrow> (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) word1 then Some p else rv' (UCAST(10 \<rightarrow> 32) a)) = (\<lambda>a. if a = word1 && mask local.asid_low_bits then Some p else rv' a) \<circ> UCAST(10 \<rightarrow> 32)
 2. \<And>word1 word2 a b p asid rv rv' rva rv'a x y. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc x y\<rbrakk> \<Longrightarrow> dc x y
 3. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 word1 word2 a b p asid rv\<rbrace> set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b) \<lbrace>\<lambda>a. typ_at (AArch AASIDPool) word2 and valid_etcbs\<rbrace>
 4. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 word1 word2 a b p asid rv'\<rbrace> updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))) \<lbrace>\<lambda>a. asid_pool_at' word2\<rbrace>
 5. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q35 word1 word2 a b p asid rv\<rbrace>
 6. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'37 word1 word2 a b p asid rv'\<rbrace>
 7. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 8. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 9. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 10. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 a b p rv rv' x. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = (\<lambda>a. rv' (UCAST(10 \<rightarrow> 32) a))\<rbrakk> \<Longrightarrow> (if x = UCAST(32 \<rightarrow> 10) word1 then Some p else rv' (UCAST(10 \<rightarrow> 32) x)) = ((\<lambda>a. if a = word1 && mask local.asid_low_bits then Some p else rv' a) \<circ> UCAST(10 \<rightarrow> 32)) x
 2. \<And>word1 word2 a b p asid rv rv' rva rv'a x y. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc x y\<rbrakk> \<Longrightarrow> dc x y
 3. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 word1 word2 a b p asid rv\<rbrace> set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b) \<lbrace>\<lambda>a. typ_at (AArch AASIDPool) word2 and valid_etcbs\<rbrace>
 4. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 word1 word2 a b p asid rv'\<rbrace> updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))) \<lbrace>\<lambda>a. asid_pool_at' word2\<rbrace>
 5. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q35 word1 word2 a b p asid rv\<rbrace>
 6. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'37 word1 word2 a b p asid rv'\<rbrace>
 7. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 8. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 9. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 10. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 a b p rv' x. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); x \<noteq> UCAST(32 \<rightarrow> 10) word1; UCAST(10 \<rightarrow> 32) x = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) word1)\<rbrakk> \<Longrightarrow> rv' (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) word1)) = Some p
 2. \<And>word1 word2 a b p asid rv rv' rva rv'a x y. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc x y\<rbrakk> \<Longrightarrow> dc x y
 3. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 word1 word2 a b p asid rv\<rbrace> set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b) \<lbrace>\<lambda>a. typ_at (AArch AASIDPool) word2 and valid_etcbs\<rbrace>
 4. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 word1 word2 a b p asid rv'\<rbrace> updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))) \<lbrace>\<lambda>a. asid_pool_at' word2\<rbrace>
 5. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q35 word1 word2 a b p asid rv\<rbrace>
 6. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'37 word1 word2 a b p asid rv'\<rbrace>
 7. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 8. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 9. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 10. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (9 subgoals):
 1. \<And>word1 word2 a b p asid rv rv' rva rv'a x y. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32); dc rva rv'a; dc x y\<rbrakk> \<Longrightarrow> dc x y
 2. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 word1 word2 a b p asid rv\<rbrace> set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b) \<lbrace>\<lambda>a. typ_at (AArch AASIDPool) word2 and valid_etcbs\<rbrace>
 3. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 word1 word2 a b p asid rv'\<rbrace> updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))) \<lbrace>\<lambda>a. asid_pool_at' word2\<rbrace>
 4. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q35 word1 word2 a b p asid rv\<rbrace>
 5. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'37 word1 word2 a b p asid rv'\<rbrace>
 6. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 7. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 8. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 9. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 word1 word2 a b p asid rv\<rbrace> set_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) (a, b) \<lbrace>\<lambda>a. typ_at (AArch AASIDPool) word2 and valid_etcbs\<rbrace>
 2. \<And>word1 word2 a b p asid rv rv'. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); rv = rv' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 word1 word2 a b p asid rv'\<rbrace> updateCap (cte_map (a, b)) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p (Some word1))) \<lbrace>\<lambda>a. asid_pool_at' word2\<rbrace>
 3. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)\<rbrace> get_asid_pool word2 \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and ?Q35 word1 word2 a b p asid rv\<rbrace>
 4. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and ?Q'37 word1 word2 a b p asid rv'\<rbrace>
 5. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 6. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 7. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 8. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 a b p asid s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b)) s\<rbrakk> \<Longrightarrow> \<forall>pool. ako_at (arch_kernel_obj.ASIDPool pool) word2 s \<longrightarrow> (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) and (\<lambda>s. typ_at (AArch AASIDPool) word2 s \<and> valid_etcbs s)) s
 2. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and asid_pool_at' word2\<rbrace>
 3. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 4. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 5. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 6. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 a b p asid s pool. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); valid_objs s; pspace_aligned s; pspace_distinct s; typ_at (AArch AASIDPool) word2 s; valid_etcbs s; cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) (a, b) s; ako_at (arch_kernel_obj.ASIDPool pool) word2 s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c) (a, b) s
 2. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and asid_pool_at' word2\<rbrace>
 3. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 4. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 5. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 6. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 a b p asid s pool c. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); valid_objs s; pspace_aligned s; pspace_distinct s; typ_at (AArch AASIDPool) word2 s; valid_etcbs s; ako_at (arch_kernel_obj.ASIDPool pool) word2 s; cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrakk> \<Longrightarrow> cap_master_cap c = cap_master_cap (cap.ArchObjectCap (arch_cap.PageDirectoryCap p (Some word1))) \<and> \<not> is_reply_cap c \<and> \<not> is_master_reply_cap c \<and> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c
 2. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and asid_pool_at' word2\<rbrace>
 3. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 4. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 5. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 6. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 a b p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 word1 word2 (a, b) (capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid))\<rbrace> liftM (inv asidpool.ASIDPool) (getObject word2) \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map (a, b)) and asid_pool_at' word2\<rbrace>
 2. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 3. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and ?Q'27 word1 word2 prod a\<rbrace>
 4. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 5. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 word1 word2 prod\<rbrace> get_cap prod \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap rv) prod) and (\<lambda>s. \<exists>p asid. rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))\<rbrace>
 2. \<And>word1 word2 prod. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 word1 word2 prod\<rbrace> getSlotCap (cte_map prod) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and (\<lambda>a. \<forall>ko. ko_at' ko word2 a \<longrightarrow> ((\<lambda>rv' s. pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map prod) s \<and> asid_pool_at' word2 s) \<circ> inv asidpool.ASIDPool) ko a)\<rbrace>
 3. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and ?Q6 word1 word2 prod) s
 4. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and ?Q'6 word1 word2 prod) s proof (prove)
goal (2 subgoals):
 1. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (valid_objs and pspace_aligned and pspace_distinct and valid_apinv (asid_pool_invocation.Assign word1 word2 prod) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) prod and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) prod s \<longrightarrow> (typ_at (AArch AASIDPool) word2 and (valid_objs and pspace_aligned and pspace_distinct and typ_at (AArch AASIDPool) word2 and valid_etcbs and cte_wp_at (\<lambda>c. cap_master_cap c = cap_master_cap cap) prod) and (\<lambda>s. \<exists>p asid. cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid))) s)) s
 2. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and (pspace_aligned' and pspace_distinct' and (\<lambda>a. \<forall>ko. ko_at' ko word2 a \<longrightarrow> ((\<lambda>rv' s. pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map prod) s \<and> asid_pool_at' word2 s) \<circ> inv asidpool.ASIDPool) ko a))) s proof (prove)
goal (2 subgoals):
 1. \<And>word1 word2 a b s pool p asid. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map (a, b)); ap = asid_pool_invocation.Assign word1 word2 (a, b); valid_objs s; pspace_aligned s; pspace_distinct s; kheap s word2 = Some (ArchObj (arch_kernel_obj.ASIDPool pool)); pool (UCAST(32 \<rightarrow> 10) word1) = None; 0 < word1; fst (get_cap (a, b) s) = {(cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid), s)}; word1 < 2 ^ local.asid_bits; cap_asid (cap.ArchObjectCap (arch_cap.PageDirectoryCap p asid)) = None; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of word1)) None] \<rhd> word2) s; valid_etcbs s\<rbrakk> \<Longrightarrow> a_type (ArchObj (arch_kernel_obj.ASIDPool pool)) = AArch AASIDPool
 2. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and (pspace_aligned' and pspace_distinct' and (\<lambda>a. \<forall>ko. ko_at' ko word2 a \<longrightarrow> ((\<lambda>rv' s. pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map prod) s \<and> asid_pool_at' word2 s) \<circ> inv asidpool.ASIDPool) ko a))) s proof (prove)
goal (1 subgoal):
 1. \<And>word1 word2 prod s. \<lbrakk>ap' = asidpool_invocation.Assign word1 word2 (cte_map prod); ap = asid_pool_invocation.Assign word1 word2 prod; (pspace_aligned' and pspace_distinct' and valid_apinv' (asidpool_invocation.Assign word1 word2 (cte_map prod))) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and (pspace_aligned' and pspace_distinct' and (\<lambda>a. \<forall>ko. ko_at' ko word2 a \<longrightarrow> ((\<lambda>rv' s. pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map prod) s \<and> asid_pool_at' word2 s) \<circ> inv asidpool.ASIDPool) ko a))) s proof (prove)
goal:
No subgoals!