theory Finalise_DR

lemma dcorres_delete_asid_pool:
  "dcorres dc \<top> \<top>
    (CSpace_D.delete_asid_pool (unat (asid_high_bits_of asid)) oid)
    (ARM_A.delete_asid_pool asid oid)" apply (simp add:CSpace_D.delete_asid_pool_def ARM_A.delete_asid_pool_def) apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified]) apply (clarsimp simp:gets_def) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:when_def) apply (rule conjI) prefer 2 apply (clarsimp, rule corres_alternate2) apply (clarsimp) apply clarsimp apply (rule corres_alternate1) apply (rule dcorres_absorb_get_l) apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified]) apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified]) apply (rule corres_dummy_return_l) apply (rule corres_split_forwards'[where r'=dc and Q="\<lambda>rv. \<top>" and Q'="\<lambda>rv. \<top>", simplified]) prefer 2 apply clarsimp apply (rule dcorres_absorb_get_r) apply (rule corres_guard_imp) apply (rule dcorres_set_vm_root) apply clarsimp+ apply (rule corres_guard_imp[where Q=\<top> and Q'=\<top>, simplified]) apply (clarsimp simp:simpler_modify_def put_def bind_def corres_underlying_def) apply (clarsimp simp:transform_def transform_objects_def transform_cdt_def
                          transform_current_thread_def) apply (clarsimp simp:transform_asid_table_def) apply (rule ext) apply (clarsimp simp:unat_map_def asid_high_bits_of_def
                          transform_asid_table_entry_def transform_asid_def) apply safe apply (drule unat_cong) apply (subst (asm) word_unat.Abs_inverse) apply (clarsimp simp:unats_def unat_ucast)+ apply (rule mapM_wp) apply clarsimp apply wp apply fastforce apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (CSpace_D.delete_asid_pool (unat (asid_high_bits_of asid)) oid) (local.delete_asid_pool asid oid) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (do asid_table <- gets cdl_asid_table;
modify (cdl_asid_table_update (\<lambda>_. asid_table(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (do y <- assert (asid && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
when (asid_table (asid_high_bits_of asid) = Some oid) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)
od) proof (prove)
goal (2 subgoals):
 1. \<And>rv. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (do asid_table <- gets cdl_asid_table;
modify (cdl_asid_table_update (\<lambda>_. asid_table(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (do asid_table <- gets (arm_asid_table \<circ> arch_state);
when (asid_table (asid_high_bits_of asid) = Some oid) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of asid := None)\<rparr>\<rparr>);
gets cur_thread >>= set_vm_root
od)
od)
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (do s <- get;
when (asid_table s (asid_high_bits_of asid) = Some oid) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>sa. sa\<lparr>arch_state := arch_state sa\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)
od)
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (when (asid_table s' (asid_high_bits_of asid) = Some oid) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. when (\<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y) (do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od))
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s'. (asid_table s' (asid_high_bits_of asid) = Some oid \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)) \<and> (asid_table s' (asid_high_bits_of asid) \<noteq> Some oid \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (return ()))
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s'. asid_table s' (asid_high_bits_of asid) = Some oid \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)
 2. \<And>s'. asid_table s' (asid_high_bits_of asid) \<noteq> Some oid \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (return ())
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s'. asid_table s' (asid_high_bits_of asid) \<noteq> Some oid \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (return ())
 2. \<And>s'. asid_table s' (asid_high_bits_of asid) = Some oid \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s'. asid_table s' (asid_high_bits_of asid) \<noteq> Some oid \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (return ())
 2. \<And>s'. asid_table s' (asid_high_bits_of asid) = Some oid \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s'. asid_table s' (asid_high_bits_of asid) = Some oid \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s'. asid_table s' (asid_high_bits_of asid) = Some oid \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od \<sqinter> return ()) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s'. asid_table s' (asid_high_bits_of asid) = Some oid \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table s)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))
od) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s' s'a. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))) (do pool <- get_asid_pool oid;
y <- mapM (\<lambda>offset. if \<exists>y. pool (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s' s'a rv. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) (\<lambda>_. True) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))) (do y <- mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)
 2. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' s'a rv rva. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) (\<lambda>_. True) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))) (do y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)
 2. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s' s'a rv rva. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) (\<lambda>_. True) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap))) >>= return) (do y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>);
s <- get;
set_vm_root (cur_thread s)
od)
 2. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s' s'a rv rva. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) (\<lambda>_. True) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>))
 2. \<And>s' s'a rv rva rvb rv'. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return rvb) (do s <- get;
set_vm_root (cur_thread s)
od)
 3. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s' s'a rv rva rvb rv'. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return rvb) (do s <- get;
set_vm_root (cur_thread s)
od)
 2. \<And>s' s'a rv rva. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) (\<lambda>_. True) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>))
 3. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s'a. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do s <- get;
set_vm_root (cur_thread s)
od)
 2. \<And>s' s'a rv rva. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) (\<lambda>_. True) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>))
 3. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s'a s'. \<lbrakk>asid_table s'a (asid_high_bits_of asid) = Some oid; True; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (set_vm_root (cur_thread s'))
 2. \<And>s' s'a rv rva. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) (\<lambda>_. True) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>))
 3. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s'a s'. \<lbrakk>asid_table s'a (asid_high_bits_of asid) = Some oid; True; True\<rbrakk> \<Longrightarrow> dcorres dc (?Q44 s'a s') (?Q'44 s'a s') (return ()) (set_vm_root (cur_thread s'))
 2. \<And>s'a s' s. \<lbrakk>asid_table s'a (asid_high_bits_of asid) = Some oid; True; True; transform s' = s\<rbrakk> \<Longrightarrow> ?Q44 s'a s' s
 3. \<And>s'a s' s. \<lbrakk>asid_table s'a (asid_high_bits_of asid) = Some oid; True; True; s' = s\<rbrakk> \<Longrightarrow> ?Q'44 s'a s' s
 4. \<And>s' s'a rv rva. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) (\<lambda>_. True) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>))
 5. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s'a s' s. \<lbrakk>asid_table s'a (asid_high_bits_of asid) = Some oid; True; True; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s'a s' s. \<lbrakk>asid_table s'a (asid_high_bits_of asid) = Some oid; True; True; s' = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s'a rv rva. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) (\<lambda>_. True) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s')(asid_high_bits_of asid := None)\<rparr>\<rparr>))
 4. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s'a. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> dcorres dc ((=) (transform s'a)) (\<lambda>_. True) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s'a)(asid_high_bits_of asid := None)\<rparr>\<rparr>))
 2. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s'a. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (modify (cdl_asid_table_update (\<lambda>_. (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)))) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s'a)(asid_high_bits_of asid := None)\<rparr>\<rparr>))
 2. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s'a b. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> transform (b\<lparr>arch_state := arch_state b\<lparr>arm_asid_table := (asid_table s'a)(asid_high_bits_of asid := None)\<rparr>\<rparr>) = transform b\<lparr>cdl_asid_table := (cdl_asid_table (transform s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)\<rparr>
 2. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s'a b. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> transform_asid_table (b\<lparr>arch_state := arch_state b\<lparr>arm_asid_table := (asid_table s'a)(asid_high_bits_of asid := None)\<rparr>\<rparr>) = (transform_asid_table s'a)(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)
 2. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s'a. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> unat_map (Some \<circ> transform_asid_table_entry \<circ> (asid_table s'a)(asid_high_bits_of asid := None)) = (unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)
 2. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s'a x. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> unat_map (Some \<circ> transform_asid_table_entry \<circ> (asid_table s'a)(asid_high_bits_of asid := None)) x = ((unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table s'a))(unat (asid_high_bits_of asid) \<mapsto> cdl_cap.NullCap)) x
 2. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s'a x. asid_table s'a (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = Some oid \<Longrightarrow> (word_of_nat x = UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits) \<longrightarrow> (x < 128 \<longrightarrow> x = unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))) \<and> (\<not> x < 128 \<longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)))) \<and> (word_of_nat x \<noteq> UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits) \<longrightarrow> \<not> x < 128 \<longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)))
 2. \<And>s' s'a rv cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' s'a cs. \<lbrakk>asid_table s' (asid_high_bits_of asid) = Some oid; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s'a x. \<lbrakk>asid_table s'a (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = Some oid; word_of_nat x = UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits); x < 128\<rbrakk> \<Longrightarrow> x = unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))
 2. \<And>s'a x. \<lbrakk>asid_table s'a (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = Some oid; word_of_nat (unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))) = UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits); \<not> unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) < 128\<rbrakk> \<Longrightarrow> False
 3. \<And>s'a x. \<lbrakk>asid_table s'a (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = Some oid; word_of_nat (unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))) \<noteq> UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits); \<not> unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) < 128\<rbrakk> \<Longrightarrow> False
 4. \<And>s' s'a rv cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>s' s'a cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s'a x. \<lbrakk>asid_table s'a (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = Some oid; x < 128; unat (word_of_nat x) = unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))\<rbrakk> \<Longrightarrow> x = unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))
 2. \<And>s'a x. \<lbrakk>asid_table s'a (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = Some oid; word_of_nat (unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))) = UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits); \<not> unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) < 128\<rbrakk> \<Longrightarrow> False
 3. \<And>s'a x. \<lbrakk>asid_table s'a (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = Some oid; word_of_nat (unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))) \<noteq> UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits); \<not> unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) < 128\<rbrakk> \<Longrightarrow> False
 4. \<And>s' s'a rv cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>s' s'a cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s'a x. \<lbrakk>asid_table s'a (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = Some oid; x < 128\<rbrakk> \<Longrightarrow> x \<in> unats LENGTH(7)
 2. \<And>s'a x. \<lbrakk>asid_table s'a (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = Some oid; x < 128; x = unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))\<rbrakk> \<Longrightarrow> x = unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))
 3. \<And>s'a x. \<lbrakk>asid_table s'a (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = Some oid; word_of_nat (unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))) = UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits); \<not> unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) < 128\<rbrakk> \<Longrightarrow> False
 4. \<And>s'a x. \<lbrakk>asid_table s'a (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = Some oid; word_of_nat (unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits))) \<noteq> UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits); \<not> unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) < 128\<rbrakk> \<Longrightarrow> False
 5. \<And>s' s'a rv cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>s' s'a cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s'a rv cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> mapM (\<lambda>offset. if \<exists>y. rv (UCAST(32 \<rightarrow> 10) offset) = Some y then do y <- flush_space (asid + offset);
invalidate_asid_entry (asid + offset)
od else return ()) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>s' s'a cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s'a rv cs x. \<lbrakk>asid_table s'a (asid_high_bits_of asid) = Some oid; x \<in> ?S103 s'a rv cs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> if \<exists>y. rv (UCAST(32 \<rightarrow> 10) x) = Some y then do y <- flush_space (asid + x);
invalidate_asid_entry (asid + x)
od else return () \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>
 2. \<And>s'a rv cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> set [0 .e. 2 ^ local.asid_low_bits - 1] \<subseteq> ?S103 s'a rv cs
 3. \<And>s' s'a cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s'a rv cs x y. \<lbrakk>asid_table s'a (asid_high_bits_of asid) = Some oid; x \<in> ?S103 s'a rv cs; rv (UCAST(32 \<rightarrow> 10) x) = Some y\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do y <- flush_space (asid + x);
invalidate_asid_entry (asid + x)
od \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>
 2. \<And>s'a rv cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> set [0 .e. 2 ^ local.asid_low_bits - 1] \<subseteq> ?S103 s'a rv cs
 3. \<And>s' s'a cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s'a rv cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> set [0 .e. 2 ^ local.asid_low_bits - 1] \<subseteq> ?S103 s'a rv cs
 2. \<And>s' s'a cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s' s'a cs. asid_table s'a (asid_high_bits_of asid) = Some oid \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_asid_pool oid \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!