theory PageTableDuplicates

lemma lookupPTSlot_aligned:
  "\<lbrace>\<lambda>s. valid_objs' s \<and> vmsz_aligned' vptr sz \<and> sz \<noteq> ARMSuperSection\<rbrace>
   lookupPTSlot pd vptr
  \<lbrace>\<lambda>rv s. is_aligned rv ((pageBitsForSize sz) - 10)\<rbrace>,-" apply (simp add:lookupPTSlot_def) apply (wp|wpc|simp)+ apply (wp getPDE_wp) apply (clarsimp simp:obj_at'_def vmsz_aligned'_def) apply (clarsimp simp:projectKO_def fail_def
    projectKO_opt_pde return_def lookup_pt_slot_no_fail_def
    split:option.splits Structures_H.kernel_object.splits
    arch_kernel_object.splits) apply (erule(1) valid_objsE') apply (rule aligned_add_aligned) apply (simp add:valid_obj'_def) apply (erule is_aligned_ptrFromPAddr_n) apply (simp add:ptBits_def pageBits_def pteBits_def) apply (rule is_aligned_shiftl) apply (rule is_aligned_andI1) apply (rule is_aligned_shiftr) apply (case_tac sz,simp_all)[1] apply (simp add:ptBits_def word_bits_def pageBits_def) apply (case_tac sz,simp_all add:ptBits_def pageBits_def pteBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs' s \<and> vmsz_aligned' vptr sz \<and> sz \<noteq> ARMSuperSection\<rbrace> lookupPTSlot pd vptr \<lbrace>\<lambda>rv s. is_aligned rv (pageBitsForSize sz - 10)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs' s \<and> vmsz_aligned' vptr sz \<and> sz \<noteq> ARMSuperSection\<rbrace> doE pde <- liftE (getObject (lookup_pd_slot pd vptr));
case pde of ARM_H.PageTablePDE x xa xb \<Rightarrow> doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE | _ \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 20
odE \<lbrace>\<lambda>rv s. is_aligned rv (pageBitsForSize sz - 10)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'76\<rbrace> getObject (lookup_pd_slot pd vptr) \<lbrace>\<lambda>x s. \<forall>xa. (\<exists>xb xc. x = ARM_H.PageTablePDE xa xb xc) \<longrightarrow> page_table_at' (ptrFromPAddr xa) s \<longrightarrow> is_aligned (lookup_pt_slot_no_fail (ptrFromPAddr xa) vptr) (pageBitsForSize sz - 10)\<rbrace>
 2. \<And>s. valid_objs' s \<and> vmsz_aligned' vptr sz \<and> sz \<noteq> ARMSuperSection \<Longrightarrow> True \<and> ?P'76 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> vmsz_aligned' vptr sz \<and> sz \<noteq> ARMSuperSection \<Longrightarrow> True \<and> (\<forall>ko. ko_at' ko (lookup_pd_slot pd vptr) s \<longrightarrow> (\<forall>x. (\<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb) \<longrightarrow> page_table_at' (ptrFromPAddr x) s \<longrightarrow> is_aligned (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr) (pageBitsForSize sz - 10))) proof (prove)
goal (1 subgoal):
 1. \<And>s koa x xa xb. \<lbrakk>valid_objs' s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some koa; is_aligned (lookup_pd_slot pd vptr) (objBitsKO koa); fst (projectKO koa s) = {(ARM_H.PageTablePDE x xa xb, s)}; ps_clear (lookup_pd_slot pd vptr) (objBitsKO koa) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr) (pageBitsForSize sz - 10) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; valid_objs' s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) (pageBitsForSize sz - 10) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) (pageBitsForSize sz - 10) proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (?n173 s x xa xb)
 2. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pageBitsForSize sz - 10)
 3. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> pageBitsForSize sz - 10 \<le> ?n173 s x xa xb proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); is_aligned x ptBits\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (?n173 s x xa xb)
 2. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pageBitsForSize sz - 10)
 3. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> pageBitsForSize sz - 10 \<le> ?n173 s x xa xb proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))))\<rbrakk> \<Longrightarrow> ptBits \<le> 24
 2. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pageBitsForSize sz - 10)
 3. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> pageBitsForSize sz - 10 \<le> ptBits proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pageBitsForSize sz - 10)
 2. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> pageBitsForSize sz - 10 \<le> ptBits proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF) (pageBitsForSize sz - 10 - 2)
 2. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> pageBitsForSize sz - 10 \<le> ptBits proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 12) (pageBitsForSize sz - 10 - 2)
 2. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> pageBitsForSize sz - 10 \<le> ptBits proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> is_aligned vptr (pageBitsForSize sz - 10 - 2 + 12)
 2. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> pageBitsForSize sz - 10 \<le> ptBits proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> pageBitsForSize sz - 10 \<le> ptBits proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>ps_clear (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))) s; page_table_at' (ptrFromPAddr x) s; is_aligned vptr (pageBitsForSize sz); sz \<noteq> ARMSuperSection; ksPSpace s (lookup_pd_slot pd vptr) = Some (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))); is_aligned (lookup_pd_slot pd vptr) (objBitsKO (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb)))); valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> pageBitsForSize sz - 10 \<le> 8 + pteBits proof (prove)
goal:
No subgoals!