theory Finalise_DR

lemma dcorres_delete_asid:
  "dcorres dc \<top> (valid_idle)
    (CSpace_D.delete_asid (transform_asid asid) word)
    (ARM_A.delete_asid asid word)" apply (clarsimp simp:CSpace_D.delete_asid_def ARM_A.delete_asid_def) apply (clarsimp simp:gets_def) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:when_def split:option.splits) apply (rule conjI) apply clarsimp apply (rule corres_alternate2) apply clarsimp apply clarsimp apply (rule dcorres_symb_exec_r_strong) apply clarsimp apply (rule conjI) apply clarsimp apply (rule corres_alternate1) apply (rule dcorres_absorb_get_l) apply (drule_tac s="transform s'" in sym) apply (clarsimp simp:when_def asid_table_transform transform_asid_def
                          transform_asid_table_entry_def
                     split:option.splits if_splits) apply (rule dcorres_symb_exec_r_strong) apply (rule dcorres_symb_exec_r_strong) apply (rule corres_guard_imp) apply (rule corres_dummy_return_l) apply (rule corres_split\<comment> \<open>[OF corres_trivial,where r'=dc]\<close>) apply (rule dcorres_set_asid_pool) apply simp apply (clarsimp simp:transform_asid_def) apply (clarsimp simp:transform_asid_pool_entry_def) apply (rule dcorres_symb_exec_r[OF dcorres_set_vm_root]) apply (wp | clarsimp)+ apply simp apply (wp | clarsimp)+ apply (rule hoare_pre, wp) apply simp apply (wp | clarsimp)+ apply (rule corres_alternate2) apply simp apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) valid_idle (CSpace_D.delete_asid (transform_asid asid) word) (local.delete_asid asid word) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) valid_idle (do asid_table <- gets cdl_asid_table;
case asid_table (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p x) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (do asid_table <- gets (arm_asid_table \<circ> arch_state);
case asid_table (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some word) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) valid_idle (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (do s <- get;
case asid_table s (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some word) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; valid_idle s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (case asid_table s' (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some word) $ do flush_space asid;
invalidate_asid_entry asid;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) asid := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. valid_idle s' \<Longrightarrow> (asid_table s' (asid_high_bits_of asid) = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())) \<and> (\<forall>x2. asid_table s' (asid_high_bits_of asid) = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (do pool <- get_asid_pool x2;
if pool (UCAST(32 \<rightarrow> 10) asid) = Some word then do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od else return ()
od)) proof (prove)
goal (2 subgoals):
 1. \<And>s'. valid_idle s' \<Longrightarrow> asid_table s' (asid_high_bits_of asid) = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 2. \<And>s'. valid_idle s' \<Longrightarrow> \<forall>x2. asid_table s' (asid_high_bits_of asid) = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (do pool <- get_asid_pool x2;
if pool (UCAST(32 \<rightarrow> 10) asid) = Some word then do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od else return ()
od) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 2. \<And>s'. valid_idle s' \<Longrightarrow> \<forall>x2. asid_table s' (asid_high_bits_of asid) = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (do pool <- get_asid_pool x2;
if pool (UCAST(32 \<rightarrow> 10) asid) = Some word then do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od else return ()
od) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (return ())
 2. \<And>s'. valid_idle s' \<Longrightarrow> \<forall>x2. asid_table s' (asid_high_bits_of asid) = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (do pool <- get_asid_pool x2;
if pool (UCAST(32 \<rightarrow> 10) asid) = Some word then do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od else return ()
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. valid_idle s' \<Longrightarrow> \<forall>x2. asid_table s' (asid_high_bits_of asid) = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (do pool <- get_asid_pool x2;
if pool (UCAST(32 \<rightarrow> 10) asid) = Some word then do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od else return ()
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (do pool <- get_asid_pool x2;
if pool (UCAST(32 \<rightarrow> 10) asid) = Some word then do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od else return ()
od) proof (prove)
goal (3 subgoals):
 1. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (if rv (UCAST(32 \<rightarrow> 10) asid) = Some word then do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od else return ())
 2. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 3. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> (rv (UCAST(32 \<rightarrow> 10) asid) = Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)) \<and> (rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ()))
 2. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 3. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) = Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 3. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 4. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 3. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 4. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 3. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 4. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; transform s' = transform s'a; ?Q'18 s' x2 rv s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (case cdl_asid_table (transform s'a) (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 3. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 4. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (case cdl_asid_table (transform s'a) (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 3. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 4. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s'a) (KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 3. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 4. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (?Q'42 s' x2 rv s'a rva) (KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap) (do y <- invalidate_asid_entry asid;
y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>?Q'42 s' x2 rv s'a\<rbrace>
 3. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 5. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 6. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (?Q'46 s' x2 rv s'a rva rvb) (KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap) (do y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' x2 rv s'a rva\<rbrace> invalidate_asid_entry asid \<lbrace>?Q'46 s' x2 rv s'a rva\<rbrace>
 3. \<And>s' x2 rv s'a rva cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. ?Q'42 s' x2 rv s'a rva ps \<and> transform ps = cs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>?Q'42 s' x2 rv s'a\<rbrace>
 5. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 7. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 8. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q50 s' x2 rv s'a rva rvb) (?Q'50 s' x2 rv s'a rva rvb) (KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap) (do y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q50 s' x2 rv s'a rva rvb s
 3. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; ?Q'46 s' x2 rv s'a rva rvb s\<rbrakk> \<Longrightarrow> ?Q'50 s' x2 rv s'a rva rvb s
 4. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' x2 rv s'a rva\<rbrace> invalidate_asid_entry asid \<lbrace>?Q'46 s' x2 rv s'a rva\<rbrace>
 5. \<And>s' x2 rv s'a rva cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. ?Q'42 s' x2 rv s'a rva ps \<and> transform ps = cs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>?Q'42 s' x2 rv s'a\<rbrace>
 7. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 9. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 10. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q50 s' x2 rv s'a rva rvb) (?Q'50 s' x2 rv s'a rva rvb) (KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap >>= return) (do y <- set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
 2. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q50 s' x2 rv s'a rva rvb s
 3. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; ?Q'46 s' x2 rv s'a rva rvb s\<rbrakk> \<Longrightarrow> ?Q'50 s' x2 rv s'a rva rvb s
 4. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' x2 rv s'a rva\<rbrace> invalidate_asid_entry asid \<lbrace>?Q'46 s' x2 rv s'a rva\<rbrace>
 5. \<And>s' x2 rv s'a rva cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. ?Q'42 s' x2 rv s'a rva ps \<and> transform ps = cs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>?Q'42 s' x2 rv s'a\<rbrace>
 7. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 9. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 10. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (13 subgoals):
 1. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> dcorres (?r'56 s' x2 rv s'a rva rvb) (?P56 s' x2 rv s'a rva rvb) (?P'56 s' x2 rv s'a rva rvb) (KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap) (set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)))
 2. \<And>s' x2 rv s'a rva rvb x y. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; ?r'56 s' x2 rv s'a rva rvb x y\<rbrakk> \<Longrightarrow> dcorres dc (?R56 s' x2 rv s'a rva rvb x) (?R'56 s' x2 rv s'a rva rvb y) (return x) (gets cur_thread >>= set_vm_root)
 3. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s' x2 rv s'a rva rvb\<rbrace> KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap \<lbrace>?R56 s' x2 rv s'a rva rvb\<rbrace>
 4. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'56 s' x2 rv s'a rva rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R'56 s' x2 rv s'a rva rvb\<rbrace>
 5. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; transform s' = s\<rbrakk> \<Longrightarrow> (?P56 s' x2 rv s'a rva rvb and ?Q56 s' x2 rv s'a rva rvb) s
 6. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; ?Q'46 s' x2 rv s'a rva rvb s\<rbrakk> \<Longrightarrow> (?P'56 s' x2 rv s'a rva rvb and ?Q'56 s' x2 rv s'a rva rvb) s
 7. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' x2 rv s'a rva\<rbrace> invalidate_asid_entry asid \<lbrace>?Q'46 s' x2 rv s'a rva\<rbrace>
 8. \<And>s' x2 rv s'a rva cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. ?Q'42 s' x2 rv s'a rva ps \<and> transform ps = cs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>?Q'42 s' x2 rv s'a\<rbrace>
 10. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 13 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> rv(UCAST(32 \<rightarrow> 10) asid := None) = (?pool61 s' x2 rv s'a rva rvb)(UCAST(32 \<rightarrow> 10) (?asid61 s' x2 rv s'a rva rvb) := ?pd61 s' x2 rv s'a rva rvb)
 2. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) asid) = snd (transform_asid (?asid61 s' x2 rv s'a rva rvb))
 3. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> cdl_cap.NullCap = transform_asid_pool_entry (?pd61 s' x2 rv s'a rva rvb)
 4. \<And>s' x2 rv s'a rva rvb x y. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R56 s' x2 rv s'a rva rvb x) (?R'56 s' x2 rv s'a rva rvb y) (return x) (gets cur_thread >>= set_vm_root)
 5. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s' x2 rv s'a rva rvb\<rbrace> KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap \<lbrace>?R56 s' x2 rv s'a rva rvb\<rbrace>
 6. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'56 s' x2 rv s'a rva rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R'56 s' x2 rv s'a rva rvb\<rbrace>
 7. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q56 s' x2 rv s'a rva rvb) s
 8. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; ?Q'46 s' x2 rv s'a rva rvb s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (ASIDPool (?pool61 s' x2 rv s'a rva rvb)) x2 and ?Q'56 s' x2 rv s'a rva rvb) s
 9. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' x2 rv s'a rva\<rbrace> invalidate_asid_entry asid \<lbrace>?Q'46 s' x2 rv s'a rva\<rbrace>
 10. \<And>s' x2 rv s'a rva cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. ?Q'42 s' x2 rv s'a rva ps \<and> transform ps = cs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) asid) = snd (transform_asid asid)
 2. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> cdl_cap.NullCap = transform_asid_pool_entry None
 3. \<And>s' x2 rv s'a rva rvb x y. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R56 s' x2 rv s'a rva rvb x) (?R'56 s' x2 rv s'a rva rvb y) (return x) (gets cur_thread >>= set_vm_root)
 4. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s' x2 rv s'a rva rvb\<rbrace> KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap \<lbrace>?R56 s' x2 rv s'a rva rvb\<rbrace>
 5. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'56 s' x2 rv s'a rva rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R'56 s' x2 rv s'a rva rvb\<rbrace>
 6. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q56 s' x2 rv s'a rva rvb) s
 7. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; ?Q'46 s' x2 rv s'a rva rvb s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (ASIDPool rv) x2 and ?Q'56 s' x2 rv s'a rva rvb) s
 8. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' x2 rv s'a rva\<rbrace> invalidate_asid_entry asid \<lbrace>?Q'46 s' x2 rv s'a rva\<rbrace>
 9. \<And>s' x2 rv s'a rva cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. ?Q'42 s' x2 rv s'a rva ps \<and> transform ps = cs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>?Q'42 s' x2 rv s'a\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> cdl_cap.NullCap = transform_asid_pool_entry None
 2. \<And>s' x2 rv s'a rva rvb x y. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R56 s' x2 rv s'a rva rvb x) (?R'56 s' x2 rv s'a rva rvb y) (return x) (gets cur_thread >>= set_vm_root)
 3. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s' x2 rv s'a rva rvb\<rbrace> KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap \<lbrace>?R56 s' x2 rv s'a rva rvb\<rbrace>
 4. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'56 s' x2 rv s'a rva rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R'56 s' x2 rv s'a rva rvb\<rbrace>
 5. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q56 s' x2 rv s'a rva rvb) s
 6. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; ?Q'46 s' x2 rv s'a rva rvb s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (ASIDPool rv) x2 and ?Q'56 s' x2 rv s'a rva rvb) s
 7. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' x2 rv s'a rva\<rbrace> invalidate_asid_entry asid \<lbrace>?Q'46 s' x2 rv s'a rva\<rbrace>
 8. \<And>s' x2 rv s'a rva cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. ?Q'42 s' x2 rv s'a rva ps \<and> transform ps = cs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>?Q'42 s' x2 rv s'a\<rbrace>
 10. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>s' x2 rv s'a rva rvb x y. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R56 s' x2 rv s'a rva rvb x) (?R'56 s' x2 rv s'a rva rvb y) (return x) (gets cur_thread >>= set_vm_root)
 2. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s' x2 rv s'a rva rvb\<rbrace> KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap \<lbrace>?R56 s' x2 rv s'a rva rvb\<rbrace>
 3. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'56 s' x2 rv s'a rva rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R'56 s' x2 rv s'a rva rvb\<rbrace>
 4. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q56 s' x2 rv s'a rva rvb) s
 5. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; ?Q'46 s' x2 rv s'a rva rvb s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (ASIDPool rv) x2 and ?Q'56 s' x2 rv s'a rva rvb) s
 6. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' x2 rv s'a rva\<rbrace> invalidate_asid_entry asid \<lbrace>?Q'46 s' x2 rv s'a rva\<rbrace>
 7. \<And>s' x2 rv s'a rva cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. ?Q'42 s' x2 rv s'a rva ps \<and> transform ps = cs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>?Q'42 s' x2 rv s'a\<rbrace>
 9. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s' x2 rv s'a rva rvb x y. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?R'56 s' x2 rv s'a rva rvb y\<rbrace> gets cur_thread \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>s' x2 rv s'a rva rvb x y cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s' x2 rv s'a rva rvb\<rbrace> KHeap_D.set_cap (x2, unat (UCAST(32 \<rightarrow> 10) asid)) cdl_cap.NullCap \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>s' x2 rv s'a rva rvb. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'56 s' x2 rv s'a rva rvb\<rbrace> set_asid_pool x2 (rv(UCAST(32 \<rightarrow> 10) asid := None)) \<lbrace>?R'56 s' x2 rv s'a rva rvb\<rbrace>
 5. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q56 s' x2 rv s'a rva rvb) s
 6. \<And>s' x2 rv s'a rva rvb s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; ?Q'46 s' x2 rv s'a rva rvb s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (ASIDPool rv) x2 and ?Q'56 s' x2 rv s'a rva rvb) s
 7. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' x2 rv s'a rva\<rbrace> invalidate_asid_entry asid \<lbrace>?Q'46 s' x2 rv s'a rva\<rbrace>
 8. \<And>s' x2 rv s'a rva cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. ?Q'42 s' x2 rv s'a rva ps \<and> transform ps = cs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>?Q'42 s' x2 rv s'a\<rbrace>
 10. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
A total of 13 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>s' x2 rv s'a s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; ?Q'46 s' x2 rv s'a () () s\<rbrakk> \<Longrightarrow> valid_idle s \<and> ako_at (ASIDPool rv) x2 s
 2. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' x2 rv s'a rva\<rbrace> invalidate_asid_entry asid \<lbrace>?Q'46 s' x2 rv s'a rva\<rbrace>
 3. \<And>s' x2 rv s'a rva cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. ?Q'42 s' x2 rv s'a rva ps \<and> transform ps = cs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>?Q'42 s' x2 rv s'a\<rbrace>
 5. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 7. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 8. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s' x2 rv s'a rva. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 s' x2 rv s'a rva\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r a. valid_idle a \<and> ako_at (ASIDPool rv) x2 a\<rbrace>
 2. \<And>s' x2 rv s'a rva cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. ?Q'42 s' x2 rv s'a rva ps \<and> transform ps = cs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>?Q'42 s' x2 rv s'a\<rbrace>
 4. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 6. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 7. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s' x2 rv s'a. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'a\<rbrace> flush_space asid \<lbrace>\<lambda>r s. valid_idle s \<and> ako_at (ASIDPool rv) x2 s\<rbrace>
 2. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 4. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 5. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s' x2 rv s'a s. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'; s'a = s\<rbrakk> \<Longrightarrow> valid_idle s \<and> ako_at (ASIDPool rv) x2 s
 2. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; ?Q'18 s' x2 rv s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (?Q'18 s' x2 rv) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 4. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>?Q'18 s' x2\<rbrace>
 5. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' x2 rv s'a cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) = Some word; valid_idle s'a \<and> ako_at (ASIDPool rv) x2 s'a; transform s'a = transform s'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s'a = ps \<and> transform ps = cs\<rbrace> flush_space asid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word \<longrightarrow> dcorres dc ((=) (transform s')) (\<lambda>s. valid_idle s \<and> ako_at (ASIDPool rv) x2 s) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 3. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. valid_idle s \<and> ako_at (ASIDPool r) x2 s\<rbrace>
 4. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (\<lambda>s. valid_idle s \<and> ako_at (ASIDPool rv) x2 s) (do s <- get;
case cdl_asid_table s (fst (transform_asid asid)) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd (transform_asid asid)) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ())
 2. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. valid_idle s \<and> ako_at (ASIDPool r) x2 s\<rbrace>
 3. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s' x2 rv. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2; rv (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some word\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (\<lambda>s. valid_idle s \<and> ako_at (ASIDPool rv) x2 s) (return ()) (return ())
 2. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. valid_idle s \<and> ako_at (ASIDPool r) x2 s\<rbrace>
 3. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s' x2. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. valid_idle s \<and> ako_at (ASIDPool r) x2 s\<rbrace>
 2. \<And>s' x2 cs. \<lbrakk>valid_idle s'; asid_table s' (asid_high_bits_of asid) = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. s' = ps \<and> transform ps = cs\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!