theory ArchVSpace_AI

lemma page_table_mapped_wp:
  "\<lbrace>\<lambda>s. valid_vspace_objs s \<and> pspace_aligned s
        \<and> (\<not> ([VSRef (vptr >> 20) (Some APageDirectory),
               VSRef (asid && mask asid_low_bits) (Some AASIDPool),
               VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pt) s
                  \<longrightarrow> Q None s)
        \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> page_directory_at pd s
                 \<and> is_aligned pd pd_bits
                    \<longrightarrow> Q (Some pd) s)\<rbrace>
     page_table_mapped asid vptr pt
   \<lbrace>Q\<rbrace>"
  (is "\<lbrace>?P\<rbrace> page_table_mapped asid vptr pt \<lbrace>Q\<rbrace>") apply (simp add: page_table_mapped_def) apply (rule hoare_pre) apply (wp get_pde_wp find_pd_for_asid_lots | wpc)+ apply (clarsimp simp: lookup_pd_slot_def Let_def vspace_at_asid_def) apply (rule conjI[rotated]) apply (clarsimp simp: vs_lookup_def vs_asid_refs_def
                  dest!: graph_ofD vs_lookup1D vs_lookup1_rtrancl_iterations) apply (drule spec, erule notE, rule ImageI[rotated]) apply (rule image_eqI, rule refl, erule graph_ofI) apply (rule r_into_rtrancl, simp) apply (erule(1) vs_lookup1I) apply simp apply (clarsimp simp: vs_lookup_Cons_eq) apply (frule(1) pd_aligned) apply (clarsimp simp: vs_lookup1_def obj_at_def pd_shifting
                        vs_refs_def pd_shifting_dual vptr_shifting_3_ways) apply (simp add: pd_bits_def pageBits_def) apply (auto simp: pde_ref_def ucast_up_ucast_id is_up_def a_type_simps
                    source_size_def target_size_def word_size
                    addrFromPPtr_def ptrFromPAddr_def
             split: if_split_asm
             dest!: graph_ofD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_vspace_objs s \<and> pspace_aligned s \<and> (([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s) \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s)\<rbrace> page_table_mapped asid vptr pt \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_vspace_objs s \<and> pspace_aligned s \<and> (([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s) \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s)\<rbrace> doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE <catch> (\<lambda>y. return None) \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE <catch> (\<lambda>y. return None) \<lbrace>Q\<rbrace>
 2. \<And>s. valid_vspace_objs s \<and> pspace_aligned s \<and> (([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s) \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_vspace_objs s \<and> pspace_aligned s \<and> (([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s) \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s) \<Longrightarrow> (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> (\<forall>pd. ako_at (PageDirectory pd) (lookup_pd_slot rv vptr && ~~ mask pd_bits) s \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x xa xb. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb \<longrightarrow> Q (if addrFromPPtr pt = x then Some rv else None) s) \<and> (\<forall>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = SectionPDE x xa xb xc \<longrightarrow> Q None s) \<and> (\<forall>x xa xb. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = SuperSectionPDE x xa xb \<longrightarrow> Q None s))) \<and> ((\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. Q None s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_vspace_objs s; pspace_aligned s; ([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s\<rbrakk> \<Longrightarrow> (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> typ_at (AArch APageDirectory) rv s \<longrightarrow> (\<forall>pd. ako_at (PageDirectory pd) (rv + (vptr >> 20 << 2) && ~~ mask pd_bits) s \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s))) \<and> ((\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> Q None s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_vspace_objs s; pspace_aligned s; ([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s\<rbrakk> \<Longrightarrow> (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> Q None s
 2. \<And>s. \<lbrakk>valid_vspace_objs s; pspace_aligned s; ([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s\<rbrakk> \<Longrightarrow> \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> typ_at (AArch APageDirectory) rv s \<longrightarrow> (\<forall>pd. ako_at (PageDirectory pd) (rv + (vptr >> 20 << 2) && ~~ mask pd_bits) s \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa p p' ko koa. \<lbrakk>valid_vspace_objs s; pspace_aligned s; \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], rv) \<notin> (vs_lookup1 s)\<^sup>* `` (\<lambda>x. case x of (r, x) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], x)) ` graph_of (asid_table s); \<not> Q None s; asid_table s aa = Some p; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), p') \<in> vs_refs ko; ko_at koa p' s; (VSRef (vptr >> 20) (Some APageDirectory), pt) \<in> vs_refs koa; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>valid_vspace_objs s; pspace_aligned s; ([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s\<rbrakk> \<Longrightarrow> \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> typ_at (AArch APageDirectory) rv s \<longrightarrow> (\<forall>pd. ako_at (PageDirectory pd) (rv + (vptr >> 20 << 2) && ~~ mask pd_bits) s \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s)) proof (prove)
goal (3 subgoals):
 1. \<And>s aa p p' ko koa. \<lbrakk>valid_vspace_objs s; pspace_aligned s; \<not> Q None s; asid_table s aa = Some p; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), p') \<in> vs_refs ko; ko_at koa p' s; (VSRef (vptr >> 20) (Some APageDirectory), pt) \<in> vs_refs koa; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> ?a150 s aa p p' ko koa \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], x)) ` graph_of (asid_table s)
 2. \<And>s aa p p' ko koa. \<lbrakk>valid_vspace_objs s; pspace_aligned s; \<not> Q None s; asid_table s aa = Some p; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), p') \<in> vs_refs ko; ko_at koa p' s; (VSRef (vptr >> 20) (Some APageDirectory), pt) \<in> vs_refs koa; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> (?a150 s aa p p' ko koa, [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], ?rv146 s aa p p' ko koa) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>s. \<lbrakk>valid_vspace_objs s; pspace_aligned s; ([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s\<rbrakk> \<Longrightarrow> \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> typ_at (AArch APageDirectory) rv s \<longrightarrow> (\<forall>pd. ako_at (PageDirectory pd) (rv + (vptr >> 20 << 2) && ~~ mask pd_bits) s \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa p p' ko koa. \<lbrakk>valid_vspace_objs s; pspace_aligned s; \<not> Q None s; asid_table s aa = Some p; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), p') \<in> vs_refs ko; ko_at koa p' s; (VSRef (vptr >> 20) (Some APageDirectory), pt) \<in> vs_refs koa; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> (case (aa, p) of (r, x) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], x), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], ?rv146 s aa p p' ko koa) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>s. \<lbrakk>valid_vspace_objs s; pspace_aligned s; ([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s\<rbrakk> \<Longrightarrow> \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> typ_at (AArch APageDirectory) rv s \<longrightarrow> (\<forall>pd. ako_at (PageDirectory pd) (rv + (vptr >> 20 << 2) && ~~ mask pd_bits) s \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa p p' ko koa. \<lbrakk>valid_vspace_objs s; pspace_aligned s; \<not> Q None s; asid_table s aa = Some p; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), p') \<in> vs_refs ko; ko_at koa p' s; (VSRef (vptr >> 20) (Some APageDirectory), pt) \<in> vs_refs koa; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], p), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], ?rv146 s aa p p' ko koa) \<in> vs_lookup1 s
 2. \<And>s. \<lbrakk>valid_vspace_objs s; pspace_aligned s; ([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s\<rbrakk> \<Longrightarrow> \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> typ_at (AArch APageDirectory) rv s \<longrightarrow> (\<forall>pd. ako_at (PageDirectory pd) (rv + (vptr >> 20 << 2) && ~~ mask pd_bits) s \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa p p' ko koa. \<lbrakk>valid_vspace_objs s; pspace_aligned s; \<not> Q None s; asid_table s aa = Some p; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), p') \<in> vs_refs ko; ko_at koa p' s; (VSRef (vptr >> 20) (Some APageDirectory), pt) \<in> vs_refs koa; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None] = [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None]
 2. \<And>s. \<lbrakk>valid_vspace_objs s; pspace_aligned s; ([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s\<rbrakk> \<Longrightarrow> \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> typ_at (AArch APageDirectory) rv s \<longrightarrow> (\<forall>pd. ako_at (PageDirectory pd) (rv + (vptr >> 20 << 2) && ~~ mask pd_bits) s \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_vspace_objs s; pspace_aligned s; ([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s\<rbrakk> \<Longrightarrow> \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> typ_at (AArch APageDirectory) rv s \<longrightarrow> (\<forall>pd. ako_at (PageDirectory pd) (rv + (vptr >> 20 << 2) && ~~ mask pd_bits) s \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s)) proof (prove)
goal (1 subgoal):
 1. \<And>s rv pd. \<lbrakk>valid_vspace_objs s; pspace_aligned s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv), [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup1 s \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s; typ_at (AArch APageDirectory) rv s; ako_at (PageDirectory pd) (rv + (vptr >> 20 << 2) && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s) proof (prove)
goal (1 subgoal):
 1. \<And>s rv pd. \<lbrakk>valid_vspace_objs s; pspace_aligned s; (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv), [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup1 s \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s; typ_at (AArch APageDirectory) rv s; ako_at (PageDirectory pd) (rv + (vptr >> 20 << 2) && ~~ mask pd_bits) s; is_aligned rv 14\<rbrakk> \<Longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pd (UCAST(32 \<rightarrow> 12) (rv + (vptr >> 20 << 2) && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s) proof (prove)
goal (1 subgoal):
 1. \<And>s rv pda. \<lbrakk>valid_vspace_objs s; pspace_aligned s; (VSRef (vptr >> 20) (Some APageDirectory), pt) \<notin> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pda x)) \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> (\<exists>ko. kheap s pd = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned pd pd_bits \<longrightarrow> Q (Some pd) s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s; kheap s rv = Some (ArchObj (PageDirectory pda)); is_aligned rv 14\<rbrakk> \<Longrightarrow> (pda (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pda (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pda (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pda (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s) proof (prove)
goal (1 subgoal):
 1. \<And>s rv pda. \<lbrakk>valid_vspace_objs s; pspace_aligned s; (VSRef (vptr >> 20) (Some APageDirectory), pt) \<notin> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pda x)) \<longrightarrow> Q None s; \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> (\<exists>ko. kheap s pd = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned pd 14 \<longrightarrow> Q (Some pd) s; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s; kheap s rv = Some (ArchObj (PageDirectory pda)); is_aligned rv 14\<rbrakk> \<Longrightarrow> (pda (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pda (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x xa xb) \<longrightarrow> Q (Some rv) s) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pda (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x xa xb) \<longrightarrow> Q None s)) \<and> ((\<exists>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = SectionPDE x xa xb xc) \<longrightarrow> Q None s) \<and> ((\<exists>x xa xb. pda (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = SuperSectionPDE x xa xb) \<longrightarrow> Q None s) proof (prove)
goal:
No subgoals!