theory ArchAcc_R

lemma lookupPTSlot_corres [@lift_corres_args, corres]:
  "corres (lfr \<oplus> (=))
          (pde_at (lookup_pd_slot pd vptr) and pspace_aligned and valid_vspace_objs
          and (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) and
          K (is_aligned pd pd_bits \<and> vptr < kernel_base
          \<and> ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
          (pspace_aligned' and pspace_distinct')
          (lookup_pt_slot pd vptr) (lookupPTSlot pd vptr)" unfolding lookup_pt_slot_def lookupPTSlot_def lookupPTSlotFromPT_def apply (corresKsimp simp: pde_relation_aligned_def lookup_failure_map_def
                          ptBits_def pdeBits_def pageBits_def pteBits_def mask_def
                      wp: get_pde_wp_valid getPDE_wp) by (auto simp: lookup_failure_map_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> (=)) (pde_at (lookup_pd_slot pd vptr) and pspace_aligned and valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and K (is_aligned pd pd_bits \<and> vptr < kernel_base \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) (pspace_aligned' and pspace_distinct') (lookup_pt_slot pd vptr) (lookupPTSlot pd vptr) proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> (=)) (pde_at (lookup_pd_slot pd vptr) and pspace_aligned and valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and K (is_aligned pd pd_bits \<and> vptr < kernel_base \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) (pspace_aligned' and pspace_distinct') (doE pd_slot <- returnOk (lookup_pd_slot pd vptr);
pde <- liftE $ get_pde pd_slot;
case pde of ARM_A.PageTablePDE ptab x xa \<Rightarrow> doE pt <- returnOk (ptrFromPAddr ptab);
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt + (pt_index << 2)) >>=E returnOk
odE | _ \<Rightarrow> throwError $ ExceptionTypes_A.lookup_failure.MissingCapability 20
odE) (doE pdSlot <- returnOk (lookupPDSlot pd vptr);
pde <- withoutFailure $ getObject pdSlot;
case pde of ARM_H.PageTablePDE x xa xb \<Rightarrow> doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ do ptIndex <- return (fromVPtr $ vptr `~shiftR~` pageBits && mask (ptBits - pteBits));
ptSlot <- return (pt + (PPtr $ ptIndex `~shiftL~` pteBits));
checkPTAt pt;
return ptSlot
od
odE | _ \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 20
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s s' ref. \<lbrakk>(s, s') \<in> state_relation; pde_at (lookup_pd_slot pd vptr) s; pspace_aligned' s'; pspace_distinct' s'; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ (2 ^ pd_bits - 1))) s; is_aligned pd pd_bits; vptr < kernel_base; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && 2 ^ pd_bits - 1 >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (\<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ (2 ^ pd_bits - 1)) s \<longrightarrow> valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && 2 ^ pd_bits - 1 >> 2))) s \<longrightarrow> (\<forall>rv'. (if is_aligned (lookup_pd_slot pd vptr >> 2) (case rv' of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0) then pde_relation' (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && 2 ^ pd_bits - 1 >> 2))) rv' else pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && 2 ^ pd_bits - 1 >> 2)) = ARM_A.InvalidPDE) \<longrightarrow> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && 2 ^ pd_bits - 1 >> 2)) = ARM_A.PageTablePDE x xa xb \<longrightarrow> (\<forall>xc. (\<exists>x xa. rv' = ARM_H.PageTablePDE xc x xa) \<longrightarrow> ptrFromPAddr x = ptrFromPAddr xc \<and> ptrFromPAddr (?ptr1079 (ARM_A.PageTablePDE x xa xb) x xa xb) = ptrFromPAddr xc)))) \<and> (\<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ (2 ^ pd_bits - 1)) s \<longrightarrow> valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && 2 ^ pd_bits - 1 >> 2))) s \<longrightarrow> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && 2 ^ pd_bits - 1 >> 2)) = ARM_A.PageTablePDE x xa xb \<longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr (?ptr1079 (ARM_A.PageTablePDE x xa xb) x xa xb)) s)) \<and> pde_at' (lookup_pd_slot pd vptr) s'