theory Arch_R

lemma lookupPTSlot_aligned:
  "\<lbrace>\<lambda>s. is_aligned vptr 16 \<and> valid_objs' s\<rbrace> lookupPTSlot pd vptr \<lbrace>\<lambda>p s. is_aligned p 6\<rbrace>,-" apply (simp add:lookupPTSlot_def) apply (wp getPDE_wp |wpc|simp)+ apply (clarsimp simp:obj_at'_real_def ko_wp_at'_def) apply (erule(1) valid_objsE') apply (clarsimp simp:projectKO_opt_pde
    split:Structures_H.kernel_object.splits arch_kernel_object.splits) apply (simp add:valid_obj'_def lookup_pt_slot_no_fail_def) apply (rule aligned_add_aligned) apply (erule is_aligned_ptrFromPAddr_n) apply (simp add: ptBits_def pteBits_def) apply (rule is_aligned_shiftl,simp) apply (rule is_aligned_andI1) apply (rule is_aligned_shiftr) apply simp apply (simp add: ptBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned vptr 16 \<and> valid_objs' s\<rbrace> lookupPTSlot pd vptr \<lbrace>\<lambda>p s. is_aligned p 6\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned vptr 16 \<and> valid_objs' s\<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>p s. is_aligned p 6\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. is_aligned vptr 16 \<and> valid_objs' s \<Longrightarrow> \<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) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s koa x xa xb. \<lbrakk>is_aligned vptr 16; valid_objs' s; ksPSpace s (lookup_pd_slot pd vptr) = Some koa; is_aligned (lookup_pd_slot pd vptr) (objBitsKO koa); projectKO_opt koa = Some (ARM_H.PageTablePDE x xa xb); 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) 6 proof (prove)
goal (1 subgoal):
 1. \<And>s koa x xa xb. \<lbrakk>is_aligned vptr 16; ksPSpace s (lookup_pd_slot pd vptr) = Some koa; is_aligned (lookup_pd_slot pd vptr) (objBitsKO koa); projectKO_opt koa = Some (ARM_H.PageTablePDE x xa xb); ps_clear (lookup_pd_slot pd vptr) (objBitsKO koa) s; page_table_at' (ptrFromPAddr x) s; valid_obj' koa s\<rbrakk> \<Longrightarrow> is_aligned (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr) 6 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_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s; is_aligned vptr 16; 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 (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr) 6 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 x ptBits; is_aligned vptr 16; 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)) 6 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 x ptBits; is_aligned vptr 16; 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) (?n152 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 x ptBits; is_aligned vptr 16; 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 ((vptr >> 12) && 0xFF << 2) 6
 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 x ptBits; is_aligned vptr 16; 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> 6 \<le> ?n152 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 16; 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 x ptBits; is_aligned vptr 16; 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 ((vptr >> 12) && 0xFF << 2) 6
 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 x ptBits; is_aligned vptr 16; 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> 6 \<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 x ptBits; is_aligned vptr 16; 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 ((vptr >> 12) && 0xFF << 2) 6
 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 x ptBits; is_aligned vptr 16; 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> 6 \<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 x ptBits; is_aligned vptr 16; 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 ((vptr >> 12) && 0xFF) 4
 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 x ptBits; is_aligned vptr 16; 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> 6 \<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 x ptBits; is_aligned vptr 16; 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 (vptr >> 12) 4
 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 x ptBits; is_aligned vptr 16; 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> 6 \<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 x ptBits; is_aligned vptr 16; 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 vptr (4 + 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 x ptBits; is_aligned vptr 16; 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> 6 \<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 x ptBits; is_aligned vptr 16; 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> 6 \<le> ptBits proof (prove)
goal:
No subgoals!