theory Arch_DR

lemma invoke_asid_pool_corres:
  "arch_invocation_relation (InvokeAsidPool ap_inv)
                            (arch_invocation.InvokeASIDPool ap_inv') \<Longrightarrow>
   dcorres dc \<top> (invs and valid_apinv ap_inv' and valid_etcbs)
    (invoke_asid_pool ap_inv)
    (perform_asid_pool_invocation ap_inv')" apply (rule dcorres_expand_pfx) apply (clarsimp simp:invoke_asid_pool_def perform_asid_pool_invocation_def) apply (clarsimp split:asid_pool_invocation.splits cdl_asid_pool_invocation.splits) apply (clarsimp simp:valid_apinv_def arch_invocation_relation_def
                       translate_arch_invocation_def) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule get_cap_corres; simp) apply (clarsimp split: cap.splits arch_cap.splits simp: corres_free_fail) apply (rule dcorres_symb_exec_r) apply (rule_tac F = "rv = pool" in corres_gen_asm2) apply (rule corres_split) apply (rule set_cap_corres; simp) apply (rule dcorres_set_asid_pool[unfolded fun_upd_def]) apply fastforce apply (clarsimp simp:transform_asid_pool_entry_def transform_cap_def)+ apply (wp set_cap_idle set_cap_arch_obj | clarsimp)+ apply (clarsimp simp:not_idle_thread_def invs_def valid_state_def
                       cte_wp_at_caps_of_state obj_at_def) apply (frule(1) valid_idle_has_null_cap,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_invocation_relation (InvokeAsidPool ap_inv) (InvokeASIDPool ap_inv') \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_apinv ap_inv' and valid_etcbs) (invoke_asid_pool ap_inv) (perform_asid_pool_invocation ap_inv') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>arch_invocation_relation (InvokeAsidPool ap_inv) (InvokeASIDPool ap_inv'); s = transform s'; True; (invs and valid_apinv ap_inv' and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (invoke_asid_pool ap_inv) (perform_asid_pool_invocation ap_inv') proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>arch_invocation_relation (InvokeAsidPool ap_inv) (InvokeASIDPool ap_inv'); invs s'; valid_apinv ap_inv' s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (case ap_inv of cdl_asid_pool_invocation.Assign asid pd_cap_ref ap_target_slot \<Rightarrow> KHeap_D.get_cap pd_cap_ref >>= case_cdl_cap fail (\<lambda>bool set1 set2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word set. fail) (\<lambda>word. fail) (\<lambda>word1 word2 nat1 nat2. fail) (\<lambda>word. fail) fail (\<lambda>word1 word2 bool1 bool2 bool3 bool4. fail) (\<lambda>word bool1 bool2. fail) (\<lambda>word. fail) fail fail fail (\<lambda>word. fail) (\<lambda>bool word set nat cdl_frame_cap_type option. fail) (\<lambda>word cdl_frame_cap_type option. fail) (\<lambda>pd_id x xa. do KHeap_D.set_cap pd_cap_ref (cdl_cap.PageDirectoryCap pd_id Real (Some asid));
KHeap_D.set_cap ap_target_slot (cdl_cap.PageDirectoryCap pd_id Fake None)
od) fail (\<lambda>word nat. fail) (\<lambda>word set. fail) fail (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail)) (case ap_inv' of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> CSpaceAcc_A.get_cap ct_slot >>= 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 pool_ptr;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid \<mapsto> pd_base));
CSpaceAcc_A.set_cap (ArchObjectCap $ arch_cap.PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od))) proof (prove)
goal (1 subgoal):
 1. \<And>s' a b aa ba ab bb x1 x2 ac bc. \<lbrakk>arch_invocation_relation (InvokeAsidPool (cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, bb))) (InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (ac, bc))); invs s'; valid_apinv (asid_pool_invocation.Assign x1 x2 (ac, bc)) s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, bb); ap_inv' = asid_pool_invocation.Assign x1 x2 (ac, bc)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.get_cap (aa, ba) >>= case_cdl_cap fail (\<lambda>bool set1 set2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word set. fail) (\<lambda>word. fail) (\<lambda>word1 word2 nat1 nat2. fail) (\<lambda>word. fail) fail (\<lambda>word1 word2 bool1 bool2 bool3 bool4. fail) (\<lambda>word bool1 bool2. fail) (\<lambda>word. fail) fail fail fail (\<lambda>word. fail) (\<lambda>bool word set nat cdl_frame_cap_type option. fail) (\<lambda>word cdl_frame_cap_type option. fail) (\<lambda>pd_id x xa. do y <- KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap pd_id Real (Some (a, b)));
KHeap_D.set_cap (ab, bb) (cdl_cap.PageDirectoryCap pd_id Fake None)
od) fail (\<lambda>word nat. fail) (\<lambda>word set. fail) fail (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail)) (CSpaceAcc_A.get_cap (ac, bc) >>= 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 <- CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some x1))) (ac, bc);
set_asid_pool x2 (pool(UCAST(32 \<rightarrow> 10) x1 \<mapsto> pd_base))
od))) proof (prove)
goal (1 subgoal):
 1. \<And>s' a b aa ba ab x1 ac bc pool. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); cte_wp_at (\<lambda>cap. local.is_pd_cap cap \<and> cap_asid cap = None) (ac, bc) s'; ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.get_cap (aa, ba) >>= case_cdl_cap fail (\<lambda>bool set1 set2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word set. fail) (\<lambda>word. fail) (\<lambda>word1 word2 nat1 nat2. fail) (\<lambda>word. fail) fail (\<lambda>word1 word2 bool1 bool2 bool3 bool4. fail) (\<lambda>word bool1 bool2. fail) (\<lambda>word. fail) fail fail fail (\<lambda>word. fail) (\<lambda>bool word set nat cdl_frame_cap_type option. fail) (\<lambda>word cdl_frame_cap_type option. fail) (\<lambda>pd_id x xa. do y <- KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap pd_id Real (Some (a, b)));
KHeap_D.set_cap (ab, b) (cdl_cap.PageDirectoryCap pd_id Fake None)
od) fail (\<lambda>word nat. fail) (\<lambda>word set. fail) fail (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail)) (CSpaceAcc_A.get_cap (ac, bc) >>= 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 ab;
y <- CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some x1))) (ac, bc);
set_asid_pool ab (pool(UCAST(32 \<rightarrow> 10) x1 \<mapsto> pd_base))
od))) proof (prove)
goal (1 subgoal):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.get_cap (aa, ba) >>= case_cdl_cap fail (\<lambda>bool set1 set2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word set. fail) (\<lambda>word. fail) (\<lambda>word1 word2 nat1 nat2. fail) (\<lambda>word. fail) fail (\<lambda>word1 word2 bool1 bool2 bool3 bool4. fail) (\<lambda>word bool1 bool2. fail) (\<lambda>word. fail) fail fail fail (\<lambda>word. fail) (\<lambda>bool word set nat cdl_frame_cap_type option. fail) (\<lambda>word cdl_frame_cap_type option. fail) (\<lambda>pd_id x xa. do y <- KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap pd_id Real (Some (a, b)));
KHeap_D.set_cap (ab, b) (cdl_cap.PageDirectoryCap pd_id Fake None)
od) fail (\<lambda>word nat. fail) (\<lambda>word set. fail) fail (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail)) (CSpaceAcc_A.get_cap (ac, bc) >>= 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 ab;
y <- CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some x1))) (ac, bc);
set_asid_pool ab (pool(UCAST(32 \<rightarrow> 10) x1 \<mapsto> pd_base))
od))) proof (prove)
goal (3 subgoals):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> dcorres dc (?Q39 s' a b aa ba ab x1 ac bc pool cap) (?Q'39 s' a b aa ba ab x1 ac bc pool cap) (KHeap_D.get_cap (aa, ba) >>= case_cdl_cap fail (\<lambda>bool set1 set2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word set. fail) (\<lambda>word. fail) (\<lambda>word1 word2 nat1 nat2. fail) (\<lambda>word. fail) fail (\<lambda>word1 word2 bool1 bool2 bool3 bool4. fail) (\<lambda>word bool1 bool2. fail) (\<lambda>word. fail) fail fail fail (\<lambda>word. fail) (\<lambda>bool word set nat cdl_frame_cap_type option. fail) (\<lambda>word cdl_frame_cap_type option. fail) (\<lambda>pd_id x xa. do y <- KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap pd_id Real (Some (a, b)));
KHeap_D.set_cap (ab, b) (cdl_cap.PageDirectoryCap pd_id Fake None)
od) fail (\<lambda>word nat. fail) (\<lambda>word set. fail) fail (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail)) (CSpaceAcc_A.get_cap (ac, bc) >>= 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 ab;
y <- CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some x1))) (ac, bc);
set_asid_pool ab (pool(UCAST(32 \<rightarrow> 10) x1 \<mapsto> pd_base))
od)))
 2. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; transform s' = s\<rbrakk> \<Longrightarrow> ?Q39 s' a b aa ba ab x1 ac bc pool cap s
 3. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; s' = s\<rbrakk> \<Longrightarrow> ?Q'39 s' a b aa ba ab x1 ac bc pool cap s proof (prove)
goal (6 subgoals):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> dcorres (?r'43 s' a b aa ba ab x1 ac bc pool cap) (?P43 s' a b aa ba ab x1 ac bc pool cap) (?P'43 s' a b aa ba ab x1 ac bc pool cap) (KHeap_D.get_cap (aa, ba)) (CSpaceAcc_A.get_cap (ac, bc))
 2. \<And>s' a b aa ba ab x1 ac bc pool cap rv rv'. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; ?r'43 s' a b aa ba ab x1 ac bc pool cap rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R43 s' a b aa ba ab x1 ac bc pool cap rv) (?R'43 s' a b aa ba ab x1 ac bc pool cap rv') (case rv of cdl_cap.PageDirectoryCap pd_id x xa \<Rightarrow> do y <- KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap pd_id Real (Some (a, b)));
KHeap_D.set_cap (ab, b) (cdl_cap.PageDirectoryCap pd_id Fake None)
od | _ \<Rightarrow> fail) (case rv' of ArchObjectCap (arch_cap.PageDirectoryCap pd_base xa) \<Rightarrow> do pool <- get_asid_pool ab;
y <- CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some x1))) (ac, bc);
set_asid_pool ab (pool(UCAST(32 \<rightarrow> 10) x1 \<mapsto> pd_base))
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 3. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> KHeap_D.get_cap (aa, ba) \<lbrace>?R43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 4. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> CSpaceAcc_A.get_cap (ac, bc) \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 5. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; transform s' = s\<rbrakk> \<Longrightarrow> (?P43 s' a b aa ba ab x1 ac bc pool cap and ?Q43 s' a b aa ba ab x1 ac bc pool cap) s
 6. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; s' = s\<rbrakk> \<Longrightarrow> (?P'43 s' a b aa ba ab x1 ac bc pool cap and ?Q'43 s' a b aa ba ab x1 ac bc pool cap) s proof (prove)
goal (5 subgoals):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap rv rv'. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = transform_cap rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R43 s' a b aa ba ab x1 ac bc pool cap rv) (?R'43 s' a b aa ba ab x1 ac bc pool cap rv') (case rv of cdl_cap.PageDirectoryCap pd_id x xa \<Rightarrow> do y <- KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap pd_id Real (Some (a, b)));
KHeap_D.set_cap (ab, b) (cdl_cap.PageDirectoryCap pd_id Fake None)
od | _ \<Rightarrow> fail) (case rv' of ArchObjectCap (arch_cap.PageDirectoryCap pd_base xa) \<Rightarrow> do pool <- get_asid_pool ab;
y <- CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap pd_base (Some x1))) (ac, bc);
set_asid_pool ab (pool(UCAST(32 \<rightarrow> 10) x1 \<mapsto> pd_base))
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> KHeap_D.get_cap (aa, ba) \<lbrace>?R43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 3. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> CSpaceAcc_A.get_cap (ac, bc) \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 4. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 s' a b aa ba ab x1 ac bc pool cap) s
 5. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (ac, bc)) and valid_etcbs and ?Q'43 s' a b aa ba ab x1 ac bc pool cap) s proof (prove)
goal (5 subgoals):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> dcorres dc (?R43 s' a b aa ba ab x1 ac bc pool cap (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52))) (?R'43 s' a b aa ba ab x1 ac bc pool cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))) (do y <- KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap x51 Real (Some (a, b)));
KHeap_D.set_cap (ab, b) (cdl_cap.PageDirectoryCap x51 Fake None)
od) (do pool <- get_asid_pool ab;
y <- CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x1))) (ac, bc);
set_asid_pool ab (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) x1 then Some x51 else pool a)
od)
 2. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> KHeap_D.get_cap (aa, ba) \<lbrace>?R43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 3. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> CSpaceAcc_A.get_cap (ac, bc) \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 4. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 s' a b aa ba ab x1 ac bc pool cap) s
 5. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (ac, bc)) and valid_etcbs and ?Q'43 s' a b aa ba ab x1 ac bc pool cap) s proof (prove)
goal (7 subgoals):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> dcorres dc (?R43 s' a b aa ba ab x1 ac bc pool cap (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52))) (?Q'74 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv) (do y <- KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap x51 Real (Some (a, b)));
KHeap_D.set_cap (ab, b) (cdl_cap.PageDirectoryCap x51 Fake None)
od) (do y <- CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x1))) (ac, bc);
set_asid_pool ab (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) x1 then Some x51 else rv a)
od)
 2. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))\<rbrace> get_asid_pool ab \<lbrace>?Q'74 s' a b aa ba ab x1 ac bc pool cap x51 x52\<rbrace>
 3. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 cs. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> KHeap_D.get_cap (aa, ba) \<lbrace>?R43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 5. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> CSpaceAcc_A.get_cap (ac, bc) \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 6. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 s' a b aa ba ab x1 ac bc pool cap) s
 7. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (ac, bc)) and valid_etcbs and ?Q'43 s' a b aa ba ab x1 ac bc pool cap) s proof (prove)
goal (7 subgoals):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool\<rbrakk> \<Longrightarrow> dcorres dc (?R43 s' a b aa ba ab x1 ac bc pool cap (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52))) (?P'79 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv) (do y <- KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap x51 Real (Some (a, b)));
KHeap_D.set_cap (ab, b) (cdl_cap.PageDirectoryCap x51 Fake None)
od) (do y <- CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x1))) (ac, bc);
set_asid_pool ab (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) x1 then Some x51 else rv a)
od)
 2. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r. ?P'79 s' a b aa ba ab x1 ac bc pool cap x51 x52 r and (\<lambda>s. r = pool)\<rbrace>
 3. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 cs. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> KHeap_D.get_cap (aa, ba) \<lbrace>?R43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 5. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> CSpaceAcc_A.get_cap (ac, bc) \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 6. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 s' a b aa ba ab x1 ac bc pool cap) s
 7. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (ac, bc)) and valid_etcbs and ?Q'43 s' a b aa ba ab x1 ac bc pool cap) s proof (prove)
goal (10 subgoals):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool\<rbrakk> \<Longrightarrow> dcorres (?r'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv) (?P87 s' a b aa ba ab x1 ac bc pool cap (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52))) (?P'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv) (KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap x51 Real (Some (a, b)))) (CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x1))) (ac, bc))
 2. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv'. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool; ?r'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva) (?R'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rv') (KHeap_D.set_cap (ab, b) (cdl_cap.PageDirectoryCap x51 Fake None)) (set_asid_pool ab (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) x1 then Some x51 else rv a))
 3. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 s' a b aa ba ab x1 ac bc pool cap (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52))\<rbrace> KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap x51 Real (Some (a, b))) \<lbrace>?R81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv\<rbrace>
 4. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv\<rbrace> CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x1))) (ac, bc) \<lbrace>?R'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv\<rbrace>
 5. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r. ?P'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 r and ?Q'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 r and (\<lambda>s. r = pool)\<rbrace>
 6. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 cs. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> KHeap_D.get_cap (aa, ba) \<lbrace>\<lambda>c. ?P87 s' a b aa ba ab x1 ac bc pool cap c and ?Q85 s' a b aa ba ab x1 ac bc pool cap c\<rbrace>
 8. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> CSpaceAcc_A.get_cap (ac, bc) \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 9. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 s' a b aa ba ab x1 ac bc pool cap) s
 10. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (ac, bc)) and valid_etcbs and ?Q'43 s' a b aa ba ab x1 ac bc pool cap) s proof (prove)
goal (9 subgoals):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv'. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool; dc rva rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva) (?R'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rv') (KHeap_D.set_cap (ab, b) (cdl_cap.PageDirectoryCap x51 Fake None)) (set_asid_pool ab (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) x1 then Some x51 else rv a))
 2. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 s' a b aa ba ab x1 ac bc pool cap (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52))\<rbrace> KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap x51 Real (Some (a, b))) \<lbrace>?R81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv\<rbrace>
 3. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv\<rbrace> CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x1))) (ac, bc) \<lbrace>?R'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv\<rbrace>
 4. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r. (\<lambda>s. valid_idle s \<and> fst (ac, bc) \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 r and (\<lambda>s. r = pool)\<rbrace>
 5. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 cs. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> KHeap_D.get_cap (aa, ba) \<lbrace>\<lambda>c. (\<lambda>a. True) and ?Q85 s' a b aa ba ab x1 ac bc pool cap c\<rbrace>
 7. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> CSpaceAcc_A.get_cap (ac, bc) \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 8. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 s' a b aa ba ab x1 ac bc pool cap) s
 9. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (ac, bc)) and valid_etcbs and ?Q'43 s' a b aa ba ab x1 ac bc pool cap) s proof (prove)
goal (11 subgoals):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv'. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool; dc rva rv'\<rbrakk> \<Longrightarrow> (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) x1 then Some x51 else rv a) = (\<lambda>x. if x = UCAST(32 \<rightarrow> 10) (?asid102 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv') then ?pd102 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv' else ?pool103 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rv' x)
 2. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv'. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool; dc rva rv'\<rbrakk> \<Longrightarrow> b = snd (transform_asid (?asid102 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv'))
 3. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv'. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool; dc rva rv'\<rbrakk> \<Longrightarrow> cdl_cap.PageDirectoryCap x51 Fake None = transform_asid_pool_entry (?pd102 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv')
 4. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 s' a b aa ba ab x1 ac bc pool cap (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52))\<rbrace> KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap x51 Real (Some (a, b))) \<lbrace>\<lambda>rva _. True\<rbrace>
 5. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv\<rbrace> CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x1))) (ac, bc) \<lbrace>\<lambda>rv'. valid_idle and ako_at (ASIDPool (?pool103 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rv')) ab\<rbrace>
 6. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r. (\<lambda>s. valid_idle s \<and> fst (ac, bc) \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 r and (\<lambda>s. r = pool)\<rbrace>
 7. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 cs. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> KHeap_D.get_cap (aa, ba) \<lbrace>\<lambda>c. (\<lambda>a. True) and ?Q85 s' a b aa ba ab x1 ac bc pool cap c\<rbrace>
 9. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> CSpaceAcc_A.get_cap (ac, bc) \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 10. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 s' a b aa ba ab x1 ac bc pool cap) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv'. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool; dc rva rv'\<rbrakk> \<Longrightarrow> b = snd (transform_asid x1)
 2. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv rva rv'. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool; dc rva rv'\<rbrakk> \<Longrightarrow> cdl_cap.PageDirectoryCap x51 Fake None = transform_asid_pool_entry (Some x51)
 3. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool\<rbrakk> \<Longrightarrow> \<lbrace>?Q85 s' a b aa ba ab x1 ac bc pool cap (cdl_cap.PageDirectoryCap x51 Real (map_option transform_asid x52))\<rbrace> KHeap_D.set_cap (aa, ba) (cdl_cap.PageDirectoryCap x51 Real (Some (a, b))) \<lbrace>\<lambda>rva _. True\<rbrace>
 4. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 rv. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; rv = pool\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 rv\<rbrace> CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x1))) (ac, bc) \<lbrace>\<lambda>rv'. valid_idle and ako_at (ASIDPool rv) ab\<rbrace>
 5. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r. (\<lambda>s. valid_idle s \<and> fst (ac, bc) \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 r and (\<lambda>s. r = pool)\<rbrace>
 6. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 cs. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> KHeap_D.get_cap (aa, ba) \<lbrace>\<lambda>c. (\<lambda>a. True) and ?Q85 s' a b aa ba ab x1 ac bc pool cap c\<rbrace>
 8. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> CSpaceAcc_A.get_cap (ac, bc) \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 9. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 s' a b aa ba ab x1 ac bc pool cap) s
 10. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (ac, bc)) and valid_etcbs and ?Q'43 s' a b aa ba ab x1 ac bc pool cap) s proof (prove)
goal (7 subgoals):
 1. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 pool\<rbrace> CSpaceAcc_A.set_cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x1))) (ac, bc) \<lbrace>\<lambda>rv'. valid_idle and ako_at (ASIDPool pool) ab\<rbrace>
 2. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r. (\<lambda>s. valid_idle s \<and> fst (ac, bc) \<noteq> idle_thread s \<and> valid_etcbs s) and ?Q'81 s' a b aa ba ab x1 ac bc pool cap x51 x52 r and (\<lambda>s. r = pool)\<rbrace>
 3. \<And>s' a b aa ba ab x1 ac bc pool cap x51 x52 cs. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool ab \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> KHeap_D.get_cap (aa, ba) \<lbrace>\<lambda>c. (\<lambda>a. True) and ?Q85 s' a b aa ba ab x1 ac bc pool cap c\<rbrace>
 5. \<And>s' a b aa ba ab x1 ac bc pool cap. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace> CSpaceAcc_A.get_cap (ac, bc) \<lbrace>?R'43 s' a b aa ba ab x1 ac bc pool cap\<rbrace>
 6. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q43 s' a b aa ba ab x1 ac bc pool cap) s
 7. \<And>s' a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s'; valid_etcbs s'; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s'; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s'; caps_of_state s' (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (ac, bc)) and valid_etcbs and ?Q'43 s' a b aa ba ab x1 ac bc pool cap) s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab x1 ac bc pool cap s. \<lbrakk>invs s; valid_etcbs s; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (ac, bc); transform_asid x1 = (a, b); transform_cslot_ptr (ac, bc) = (aa, ba); ako_at (ASIDPool pool) ab s; pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s; caps_of_state s (ac, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> valid_idle s \<and> not_idle_thread ac s \<and> (\<forall>poola. ako_at (ASIDPool poola) ab s \<longrightarrow> valid_idle s \<and> ac \<noteq> idle_thread s \<and> valid_idle s \<and> cte_wp_at (\<lambda>_. True) (ac, bc) s \<and> poola = pool) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab x1 bc pool cap s. \<lbrakk>valid_etcbs s; ap_inv = cdl_asid_pool_invocation.Assign (a, b) (aa, ba) (ab, b); ap_inv' = asid_pool_invocation.Assign x1 ab (idle_thread s, bc); transform_asid x1 = (a, b); transform_cslot_ptr (idle_thread s, bc) = (aa, ba); kheap s ab = Some (ArchObj (ASIDPool pool)); pool (UCAST(32 \<rightarrow> 10) x1) = None; 0 < x1; x1 < 2 ^ local.asid_bits; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> ab) s; caps_of_state s (idle_thread s, bc) = Some cap; local.is_pd_cap cap; cap_asid cap = None; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!