theory ArchVSpace_AI

lemma find_pd_for_asid_assert_wp:
  "\<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<and> asid \<noteq> 0 \<longrightarrow> P pd s\<rbrace> find_pd_for_asid_assert asid \<lbrace>P\<rbrace>" apply (simp add: find_pd_for_asid_assert_def
                   find_pd_for_asid_def assertE_def
                 split del: if_split) apply (wp get_pde_wp get_asid_pool_wp | wpc)+ apply clarsimp apply (drule spec, erule mp) apply (clarsimp simp: vspace_at_asid_def word_neq_0_conv) apply (rule vs_lookupI) apply (simp add: vs_asid_refs_def) apply (rule image_eqI[OF refl]) apply (erule graph_ofI) apply (rule r_into_rtrancl, simp) apply (erule vs_lookup1I) apply (simp add: vs_refs_def) apply (rule image_eqI[rotated]) apply (erule graph_ofI) apply simp apply (simp add: mask_asid_low_bits_ucast_ucast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<and> asid \<noteq> 0 \<longrightarrow> P pd s\<rbrace> find_pd_for_asid_assert asid \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<and> asid \<noteq> 0 \<longrightarrow> P pd s\<rbrace> do pd <- 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 <catch> (\<lambda>y. fail);
y <- get_pde pd;
return pd
od \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>pd. vspace_at_asid asid pd s \<and> asid \<noteq> 0 \<longrightarrow> P pd s \<Longrightarrow> True \<and> 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> (\<forall>pd. ako_at (PageDirectory pd) (x && ~~ mask pd_bits) s \<longrightarrow> P x s))))) \<and> (\<not> 0 < asid \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa pd. \<lbrakk>\<forall>pd. vspace_at_asid asid pd s \<and> asid \<noteq> 0 \<longrightarrow> P pd s; 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; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> P xa s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa pd. \<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; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> vspace_at_asid asid xa s \<and> asid \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa pd. \<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; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) 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 (2 subgoals):
 1. \<And>s x pool xa pd. \<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; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> ?ref'84 s x pool xa pd \<in> vs_asid_refs (asid_table s)
 2. \<And>s x pool xa pd. \<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; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (?ref'84 s x pool xa pd, [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 pd. \<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; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> ?ref'84 s x pool xa pd \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` graph_of (asid_table s)
 2. \<And>s x pool xa pd. \<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; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (?ref'84 s x pool xa pd, [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 pd. \<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; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> ?x89 s x pool xa pd \<in> graph_of (asid_table s)
 2. \<And>s x pool xa pd. \<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; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (case ?x89 s x pool xa pd of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p), [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 pd. \<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; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (case (asid_high_bits_of asid, x) of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p), [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 pd. \<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; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<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 pd. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (?r95 s x pool xa pd, xa) \<in> vs_refs (ArchObj (ASIDPool pool))
 2. \<And>s x pool xa pd. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] = [?r95 s x pool xa pd, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] proof (prove)
goal (2 subgoals):
 1. \<And>s x pool xa pd. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (?r95 s x pool xa pd, xa) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x)) ` graph_of pool
 2. \<And>s x pool xa pd. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] = [?r95 s x pool xa pd, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] proof (prove)
goal (3 subgoals):
 1. \<And>s x pool xa pd. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> ?x101 s x pool xa pd \<in> graph_of pool
 2. \<And>s x pool xa pd. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (?r95 s x pool xa pd, xa) = (case ?x101 s x pool xa pd of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x))
 3. \<And>s x pool xa pd. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] = [?r95 s x pool xa pd, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] proof (prove)
goal (2 subgoals):
 1. \<And>s x pool xa pd. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (?r95 s x pool xa pd, xa) = (case (UCAST(32 \<rightarrow> 10) asid, xa) of (r, x) \<Rightarrow> (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), x))
 2. \<And>s x pool xa pd. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] = [?r95 s x pool xa pd, VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa pd. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ako_at (PageDirectory pd) (xa && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] = [VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] proof (prove)
goal:
No subgoals!