theory ArchArch_AC

lemma lookup_pt_slot_authorised:
  "\<lbrace>\<exists>\<rhd> pd and valid_vspace_objs and pspace_aligned and pas_refined aag
          and K (is_subject aag pd) and K (is_aligned pd 14 \<and> vptr < kernel_base)\<rbrace>
   lookup_pt_slot pd vptr
   \<lbrace>\<lambda>rv _. is_subject aag (rv && ~~ mask pt_bits)\<rbrace>, -" apply (simp add: lookup_pt_slot_def) apply (wp get_pde_wp | wpc)+ apply (subgoal_tac "is_aligned pd pd_bits") apply (clarsimp simp: lookup_pd_slot_pd) apply (drule(2) valid_vspace_objsD) apply (clarsimp simp: obj_at_def) apply (drule kheap_eq_state_vrefs_pas_refinedD) apply (erule vs_refs_no_global_pts_pdI) apply (drule(1) less_kernel_base_mapping_slots) apply (simp add: kernel_mapping_slots_def) apply assumption apply (simp add: aag_has_Control_iff_owns) apply (drule_tac f="\<lambda>pde. valid_pde pde s" in arg_cong, simp) apply (clarsimp simp: obj_at_def less_kernel_base_mapping_slots) apply (erule pspace_alignedE, erule domI) apply (simp add: pt_bits_def pageBits_def) apply (subst is_aligned_add_helper, assumption) apply (rule shiftl_less_t2n) apply (rule order_le_less_trans, rule word_and_le1, simp) apply simp apply simp apply (simp add: pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and K (is_subject aag pd) and K (is_aligned pd 14 \<and> vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv _. is_subject aag (rv && ~~ mask pt_bits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> 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 _. is_subject aag (rv && ~~ mask pt_bits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> True \<and> (\<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> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)) \<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 (2 subgoals):
 1. \<And>s. \<lbrakk>((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s; is_aligned pd pd_bits\<rbrakk> \<Longrightarrow> True \<and> (\<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> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)) \<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))
 2. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>is_aligned pd pd_bits; (ref \<rhd> pd) s; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 2. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 2. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 2. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (4 subgoals):
 1. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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> (?p'74 s pda x xa xb, ?r74 s pda x xa xb, ?t74 s pda x xa xb, ?a74 s pda x xa xb) \<in> vs_refs_no_global_pts (ArchObj (PageDirectory pda))
 2. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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> pas_refined (?aag74 s pda x xa xb) s
 3. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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; (pasObjectAbs (?aag74 s pda x xa xb) pd, ?a74 s pda x xa xb, pasObjectAbs (?aag74 s pda x xa xb) (?p'74 s pda x xa xb)) \<in> pasPolicy (?aag74 s pda x xa xb)\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 4. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (4 subgoals):
 1. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)
 2. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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> pas_refined (?aag74 s pda x xa xb) s
 3. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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; (pasObjectAbs (?aag74 s pda x xa xb) pd, Control, pasObjectAbs (?aag74 s pda x xa xb) (ptrFromPAddr x)) \<in> pasPolicy (?aag74 s pda x xa xb)\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 4. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (4 subgoals):
 1. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)
 2. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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> pas_refined (?aag74 s pda x xa xb) s
 3. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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; (pasObjectAbs (?aag74 s pda x xa xb) pd, Control, pasObjectAbs (?aag74 s pda x xa xb) (ptrFromPAddr x)) \<in> pasPolicy (?aag74 s pda x xa xb)\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 4. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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> pas_refined (?aag74 s pda x xa xb) s
 2. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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; (pasObjectAbs (?aag74 s pda x xa xb) pd, Control, pasObjectAbs (?aag74 s pda x xa xb) (ptrFromPAddr x)) \<in> pasPolicy (?aag74 s pda x xa xb)\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 3. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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; (pasObjectAbs aag pd, Control, pasObjectAbs aag (ptrFromPAddr x)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 2. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s pda x xa xb. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; 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; is_subject aag (ptrFromPAddr x)\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 2. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s pda x. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s = typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 2. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s pda x pt. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pspace_aligned s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 2. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s pda x pt. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) (obj_bits (the (kheap s (ptrFromPAddr x))))\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)
 2. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s pda x pt. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask 10)
 2. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>s pda x pt. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ 10
 2. \<And>s pda x pt. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x)
 3. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (4 subgoals):
 1. \<And>s pda x pt. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (10 - 2)
 2. \<And>s pda x pt. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 3. \<And>s pda x pt. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x)
 4. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>s pda x pt. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 2. \<And>s pda x pt. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x)
 3. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s pda x pt. \<lbrakk>is_aligned pd pd_bits; valid_vspace_objs s; pas_refined aag s; is_subject aag pd; is_aligned pd 14; vptr < kernel_base; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; is_subject aag (ptrFromPAddr x); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> is_subject aag (ptrFromPAddr x)
 2. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined aag and (\<lambda>y. is_subject aag pd) and (\<lambda>y. is_aligned pd 14 \<and> vptr < kernel_base)) s \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal:
No subgoals!