theory ArchVSpace_AI

lemma find_pd_for_asid_lookup_ref:
  "\<lbrace>\<top>\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. ([VSRef (asid && mask asid_low_bits) (Some AASIDPool),
                                      VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pd)\<rbrace>, -" apply (simp add: find_pd_for_asid_def assertE_def whenE_def split del: if_split) apply (wp|wpc|clarsimp|rule conjI)+ apply (drule vs_lookup_atI) apply (erule vs_lookup_step) apply (erule vs_lookup1I [OF _ _ refl]) apply (simp add: vs_refs_def) apply (rule image_eqI[rotated], erule graph_ofI) apply (simp add: mask_asid_low_bits_ucast_ucast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> find_pd_for_asid asid \<lbrace>vs_lookup_abbr [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE y <- if 0 < asid then returnOk () else fail;
asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
pool <- case asid_table (asid_high_bits_of asid) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE \<lbrace>vs_lookup_abbr [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> xa) s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>0 < asid; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x) s\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> xa) s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>0 < asid; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], x), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], xa) \<in> vs_lookup1 s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>0 < asid; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), xa) \<in> vs_refs (ArchObj (ASIDPool pool)) proof (prove)
goal (1 subgoal):
 1. \<And>pool xa. \<lbrakk>0 < asid; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), xa) \<in> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool proof (prove)
goal (1 subgoal):
 1. \<And>pool xa. \<lbrakk>0 < asid; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), xa) = (case (UCAST(32 \<rightarrow> 10) asid, xa) of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) proof (prove)
goal:
No subgoals!