theory ArchVSpace_AI

lemma lookup_pt_slot_cap_to:
  shows "\<lbrace>invs and \<exists>\<rhd>pd and K (is_aligned pd pd_bits)
                  and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr
   \<lbrace>\<lambda>rv s.  \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap
                                \<and> rv && ~~ mask pt_bits \<in> obj_refs cap
                                \<and>  s \<turnstile> cap \<and> cap_asid cap \<noteq> None
                                \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrace>, -" proof - have shift: "(2::word32) ^ pt_bits = 2 ^ 8 << 2" by (simp add:pt_bits_def pageBits_def ) show ?thesis apply (simp add: lookup_pt_slot_def) apply (wp get_pde_wp | wpc)+ apply (clarsimp simp: lookup_pd_slot_pd) apply (frule(1) valid_vspace_objsD) apply fastforce apply (drule vs_lookup_step) apply (erule vs_lookup1I[OF _ _ refl]) apply (simp add: vs_refs_def image_def) apply (rule rev_bexI) apply (erule pde_graph_ofI) apply (erule (1) less_kernel_base_mapping_slots) apply (simp add: pde_ref_def) apply fastforce apply (drule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp) apply simp apply (elim exEI, clarsimp) apply (subst is_aligned_add_helper[THEN conjunct2]) apply (drule caps_of_state_valid) apply fastforce apply (clarsimp dest!:valid_cap_aligned simp:cap_aligned_def vs_cap_ref_def
      obj_refs_def obj_ref_of_def pageBitsForSize_def pt_bits_def pageBits_def
      elim!:is_aligned_weaken
      split:arch_cap.split_asm cap.splits option.split_asm vmpage_size.split_asm) apply (rule less_le_trans[OF shiftl_less_t2n[where m = 10]]) apply (rule le_less_trans[OF word_and_le1]) apply simp apply simp apply (simp add:pt_bits_def pageBits_def) apply (drule caps_of_state_valid) apply fastforce apply (drule bspec) apply (drule(1) less_kernel_base_mapping_slots) apply simp apply (clarsimp simp: valid_pde_def obj_at_def
                        vs_cap_ref_def is_pt_cap_def valid_cap_simps cap_aligned_def
                 split: cap.split_asm arch_cap.split_asm vmpage_size.splits
                        option.split_asm if_splits) apply (erule is_aligned_add[OF is_aligned_weaken],simp
      ,rule is_aligned_shiftl[OF is_aligned_andI1,OF is_aligned_shiftr],simp)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrace>, - proof (state)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. 2 ^ pt_bits = 2 ^ 8 << 2 proof (state)
this:
2 ^ pt_bits = 2 ^ 8 << 2

goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base)\<rbrace> liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20)) \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base)) s \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> True) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6))) \<and> (\<forall>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SectionPDE x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SuperSectionPDE x xa xb \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; (ref \<rhd> pd) s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; (ref \<rhd> pd) s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 2. \<And>s pda ref x xa xb. \<lbrakk>invs s; (ref \<rhd> pd) s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; (ref \<rhd> pd) s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> ((ref, pd), ?ref'67 s pda ref x xa xb, ?p'67 s pda ref x xa xb) \<in> vs_lookup1 s
 2. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s; (?ref'67 s pda ref x xa xb \<rhd> ?p'67 s pda ref x xa xb) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> (?r70 s pda ref x xa xb, ?p'67 s pda ref x xa xb) \<in> vs_refs (ArchObj (PageDirectory pda))
 2. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s; ((?r70 s pda ref x xa xb # ref) \<rhd> ?p'67 s pda ref x xa xb) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> \<exists>xc\<in>graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pda x)). (?r70 s pda ref x xa xb, ?p'67 s pda ref x xa xb) = (case xc of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s; ((?r70 s pda ref x xa xb # ref) \<rhd> ?p'67 s pda ref x xa xb) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> ?x76 s pda ref x xa xb \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pda x))
 2. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> (?r70 s pda ref x xa xb, ?p'67 s pda ref x xa xb) = (case ?x76 s pda ref x xa xb of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 3. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s; ((?r70 s pda ref x xa xb # ref) \<rhd> ?p'67 s pda ref x xa xb) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> pde_ref (PageTablePDE x xa xb) = Some (?v79 s pda ref x xa xb)
 3. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> (?r70 s pda ref x xa xb, ?p'67 s pda ref x xa xb) = (case (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2), ?v79 s pda ref x xa xb) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 4. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s; ((?r70 s pda ref x xa xb # ref) \<rhd> ?p'67 s pda ref x xa xb) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> pde_ref (PageTablePDE x xa xb) = Some (?v79 s pda ref x xa xb)
 2. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> (?r70 s pda ref x xa xb, ?p'67 s pda ref x xa xb) = (case (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2), ?v79 s pda ref x xa xb) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 3. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s; ((?r70 s pda ref x xa xb # ref) \<rhd> ?p'67 s pda ref x xa xb) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> (?r70 s pda ref x xa xb, ?p'67 s pda ref x xa xb) = (case (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2), ptrFromPAddr x) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s; ((?r70 s pda ref x xa xb # ref) \<rhd> ?p'67 s pda ref x xa xb) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<rhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s; \<exists>slot cap. caps_of_state s slot = Some cap \<and> ptrFromPAddr x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> ptrFromPAddr x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> (\<exists>y. cap_asid cap = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) pt_bits
 2. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ pt_bits
 3. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref); s \<turnstile> xe\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) pt_bits
 3. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ pt_bits
 4. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref); s \<turnstile> xe\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) pt_bits
 2. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ pt_bits
 3. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ pt_bits
 2. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (10 - 2)
 2. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 3. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> 2 ^ 10 \<le> 2 ^ pt_bits
 4. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> 0xFF < 2 ^ (10 - 2)
 2. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 3. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> 2 ^ 10 \<le> 2 ^ pt_bits
 4. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 2. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> 2 ^ 10 \<le> 2 ^ pt_bits
 3. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> 2 ^ 10 \<le> 2 ^ pt_bits
 2. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; caps_of_state s (xc, xd) = Some xe; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref); s \<turnstile> xe\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref); s \<turnstile> xe\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref); s \<turnstile> xe\<rbrakk> \<Longrightarrow> ?x407 s pda ref x xa xb xc xd xe \<in> - kernel_mapping_slots
 2. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref); s \<turnstile> xe; valid_pde (pda (?x407 s pda ref x xa xb xc xd xe)) s\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref); s \<turnstile> xe; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> ?x407 s pda ref x xa xb xc xd xe \<in> - kernel_mapping_slots
 2. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref); s \<turnstile> xe; valid_pde (pda (?x407 s pda ref x xa xb xc xd xe)) s\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb xc xd xe. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; ptrFromPAddr x \<in> obj_refs xe; vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) (Some APageDirectory) # ref); s \<turnstile> xe; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> is_pt_cap xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> s \<turnstile> xe \<and> (\<exists>y. cap_asid xe = Some y) \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s pda x xa xb a b pt. \<lbrakk>invs s; is_aligned pd pd_bits; vptr < kernel_base; kheap s pd = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) 10; 10 < word_bits; b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)); 0 < a; a < 2 ^ local.asid_bits; b < kernel_base; is_aligned b 20; is_aligned vptr 16\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6 proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrace>, -

goal:
No subgoals!