theory ArchVSpace_AI

lemma find_pd_for_asid_pd_at_asid [wp]:
  "\<lbrace>\<top>\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. vspace_at_asid asid pd\<rbrace>, -" apply (simp add: find_pd_for_asid_def assertE_def split del: if_split) apply (rule hoare_pre) apply (wp|wpc)+ apply (clarsimp simp: vspace_at_asid_def) apply (rule vs_lookupI) apply (simp add: vs_asid_refs_def graph_of_def) apply fastforce apply (rule r_into_rtrancl) apply (erule vs_lookup1I) prefer 2 apply (rule refl) apply (simp add: vs_refs_def graph_of_def mask_asid_low_bits_ucast_ucast) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> find_pd_for_asid asid \<lbrace>vspace_at_asid asid\<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>vspace_at_asid asid\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<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>vspace_at_asid asid\<rbrace>, -
 2. \<And>s. True \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> True \<and> True \<and> (0 < asid \<longrightarrow> ((arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = None \<longrightarrow> True) \<and> (\<forall>x. (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = Some x \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x s \<longrightarrow> (pool (UCAST(32 \<rightarrow> 10) asid) = None \<longrightarrow> True) \<and> (\<forall>x. pool (UCAST(32 \<rightarrow> 10) asid) = Some x \<longrightarrow> vspace_at_asid asid x s)))) \<and> (\<not> 0 < asid \<longrightarrow> True) 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 (2 subgoals):
 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> ?ref'74 s x pool xa \<in> vs_asid_refs (asid_table s)
 2. \<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> (?ref'74 s x pool xa, [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)\<^sup>* proof (prove)
goal (2 subgoals):
 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> ?ref'74 s x pool xa \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` {(x, y). asid_table s x = Some y}
 2. \<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> (?ref'74 s x pool xa, [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)\<^sup>* 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 (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)\<^sup>* 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 (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 (2 subgoals):
 1. \<And>s x pool xa. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> (?r87 s x pool xa, xa) \<in> vs_refs (ArchObj (ASIDPool pool))
 2. \<And>s x pool xa. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; 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] = [?r87 s x pool xa, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] proof (prove)
goal (2 subgoals):
 1. \<And>s x pool xa. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; 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] = [?r87 s x pool xa, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]
 2. \<And>s x pool xa. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> (?r87 s x pool xa, xa) \<in> vs_refs (ArchObj (ASIDPool pool)) proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; 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>s x pool xa. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), xa) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` {(x, y). pool x = Some y} proof (prove)
goal:
No subgoals!