theory Arch_DR

lemma create_mapping_entries_dcorres:
  assumes pdid: "pdid = pd_ptr"
      and pd_aligned: "is_aligned pd_ptr pd_bits"
      and vp_aligned: "vmsz_aligned vptr pgsz"
      and kb: "vptr < kernel_base"
  shows
  "dcorres (dc \<oplus> (\<lambda>rv rv'. rv = case_sum (\<lambda>pair. [ (transform_pt_slot_ref \<circ> hd \<circ> snd) pair])
                                 (\<lambda>pair. [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) rv'
                     \<and> case_sum (transform_pte \<circ> fst) (transform_pde \<circ> fst) rv'
                           = FrameCap False (ptrFromPAddr base)
                               vm_rights (pageBitsForSize pgsz) Fake None))
     \<top>
     (page_directory_at pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned
             and (\<exists>\<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)))
     (cdl_page_mapping_entries vptr (pageBitsForSize pgsz) pd_ptr)
     (create_mapping_entries base vptr pgsz vm_rights attrib pd_ptr)" proof - have aligned_4_hd:
    "\<And>r :: word32. is_aligned r 6 \<Longrightarrow> hd (map (\<lambda>x. x + r) [0 , 4 .e. 0x3C]) = r" apply (subgoal_tac "r \<le> r + 0x3C") apply (clarsimp simp: upto_enum_step_def o_def | intro conjI)+ apply (subst hd_map) apply (clarsimp simp:upto_enum_def) apply (clarsimp simp:upto_enum_def hd_map) apply (rule is_aligned_no_wrap') apply simp apply simp done show ?thesis using pdid vp_aligned apply hypsubst_thin proof (induct pgsz) case ARMSmallPage show ?case using ARMSmallPage.prems apply (simp add: liftME_def[symmetric] o_def transform_pte_def
                                     lookup_error_injection dc_def[symmetric]) apply (rule dcorres_injection_handler_rhs) apply (simp add:liftE_bindE cdl_page_mapping_entries_def) apply (rule corres_dummy_returnOk_r) apply (rule corres_guard_imp) apply (rule corres_splitEE) apply (rule dcorres_lookup_pt_slot) apply (rule dcorres_returnOk; simp) apply wp+ apply simp apply (clarsimp simp:
          dest!:page_directory_at_aligned_pd_bits ) apply (frule less_kernel_base_mapping_slots_both[OF kb,where x = 0]) apply simp apply (simp add:pageBits_def pd_bits_def) done next case ARMLargePage show ?case using ARMLargePage.prems apply (simp add: liftME_def[symmetric] o_def transform_pte_def pd_bits_def pageBits_def
                                     lookup_error_injection dc_def[symmetric]) apply (rule dcorres_injection_handler_rhs) apply (simp add:liftE_bindE cdl_page_mapping_entries_def largePagePTE_offsets_def) apply (rule corres_dummy_returnOk_r) apply (rule corres_guard_imp) apply (rule corres_splitEE) apply (rule dcorres_lookup_pt_slot) apply (rule_tac F = "is_aligned rv' 6" in corres_gen_asm2) apply (rule dcorres_returnOk) apply (subst aligned_4_hd) apply clarsimp apply (clarsimp) apply (wpsimp wp: lookup_pt_slot_aligned_6')+ apply (clarsimp dest!:page_directory_at_aligned_pd_bits) apply (frule less_kernel_base_mapping_slots_both[OF kb,where x = 0]) apply simp apply (clarsimp simp:pageBits_def pd_bits_def vmsz_aligned_def) apply (rule_tac x=ref in exI, simp) done next case ARMSection show ?case using ARMSection.prems apply (simp add: liftME_def[symmetric] o_def transform_pte_def
                                     lookup_error_injection dc_def[symmetric]) apply (simp add:liftE_bindE cdl_page_mapping_entries_def) apply (rule corres_guard_imp) apply (rule_tac F = "is_aligned pd_ptr 14" in corres_gen_asm2) apply (rule dcorres_returnOk) apply (clarsimp simp:transform_pde_def vmsz_aligned_def) apply (simp add: dcorres_lookup_pd_slot) apply simp apply (clarsimp simp: pd_bits_def pageBits_def
          dest!:page_directory_at_aligned_pd_bits ) done next case ARMSuperSection show ?case using ARMSuperSection.prems using pd_aligned apply (simp add: liftME_def[symmetric] o_def transform_pte_def
                                     lookup_error_injection dc_def[symmetric]) apply (simp add:liftE_bindE cdl_page_mapping_entries_def superSectionPDE_offsets_def) apply (rule corres_guard_imp) apply (rule_tac F = "is_aligned pd_ptr 14" in corres_gen_asm2) apply (rule dcorres_returnOk) apply (clarsimp simp:transform_pde_def vmsz_aligned_def) apply (subst aligned_4_hd) apply (rule lookup_pd_slot_aligned_6) apply (simp add:vmsz_aligned_def)+ apply (simp add: dcorres_lookup_pd_slot) apply simp apply (clarsimp simp: pd_bits_def pageBits_def
          dest!:page_directory_at_aligned_pd_bits ) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize pgsz) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize pgsz) pd_ptr) (create_mapping_entries base vptr pgsz vm_rights attrib pd_ptr) proof (state)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize pgsz) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize pgsz) pd_ptr) (create_mapping_entries base vptr pgsz vm_rights attrib pd_ptr) proof (prove)
goal (1 subgoal):
 1. \<And>r. is_aligned r 6 \<Longrightarrow> hd (map (\<lambda>x. x + r) [0 , 4 .e. 0x3C]) = r proof (prove)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>is_aligned r 6; r \<le> r + 0x3C\<rbrakk> \<Longrightarrow> hd (map (\<lambda>x. x + r) [0 , 4 .e. 0x3C]) = r
 2. \<And>r. is_aligned r 6 \<Longrightarrow> r \<le> r + 0x3C proof (prove)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>is_aligned r 6; r \<le> r + 0x3C\<rbrakk> \<Longrightarrow> hd (map (\<lambda>x. x * 4 + r) [0 .e. 0xF]) = r
 2. \<And>r. is_aligned r 6 \<Longrightarrow> r \<le> r + 0x3C proof (prove)
goal (3 subgoals):
 1. \<And>r. \<lbrakk>is_aligned r 6; r \<le> r + 0x3C\<rbrakk> \<Longrightarrow> [0 .e. 0xF] \<noteq> []
 2. \<And>r. \<lbrakk>is_aligned r 6; r \<le> r + 0x3C\<rbrakk> \<Longrightarrow> hd [0 .e. 0xF] * 4 + r = r
 3. \<And>r. is_aligned r 6 \<Longrightarrow> r \<le> r + 0x3C proof (prove)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>is_aligned r 6; r \<le> r + 0x3C\<rbrakk> \<Longrightarrow> hd [0 .e. 0xF] * 4 + r = r
 2. \<And>r. is_aligned r 6 \<Longrightarrow> r \<le> r + 0x3C proof (prove)
goal (1 subgoal):
 1. \<And>r. is_aligned r 6 \<Longrightarrow> r \<le> r + 0x3C proof (prove)
goal (2 subgoals):
 1. \<And>r. is_aligned r 6 \<Longrightarrow> is_aligned r (?sz17 r)
 2. \<And>r. is_aligned r 6 \<Longrightarrow> 0x3C < 2 ^ ?sz17 r proof (prove)
goal (1 subgoal):
 1. \<And>r. is_aligned r 6 \<Longrightarrow> 0x3C < 2 ^ 6 proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned ?r 6 \<Longrightarrow> hd (map (\<lambda>x. x + ?r) [0 , 4 .e. 0x3C]) = ?r

goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize pgsz) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize pgsz) pd_ptr) (create_mapping_entries base vptr pgsz vm_rights attrib pd_ptr) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize pgsz) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize pgsz) pd_ptr) (create_mapping_entries base vptr pgsz vm_rights attrib pd_ptr) proof (prove)
using this:
pdid = pd_ptr
vmsz_aligned vptr pgsz

goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize pgsz) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize pgsz) pd_ptr) (create_mapping_entries base vptr pgsz vm_rights attrib pd_ptr) proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr pgsz \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize pgsz) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize pgsz) pd_ptr) (create_mapping_entries base vptr pgsz vm_rights attrib pd_ptr) proof (state)
goal (4 subgoals):
 1. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSmallPage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSmallPage) pd_ptr) (create_mapping_entries base vptr ARMSmallPage vm_rights attrib pd_ptr)
 2. vmsz_aligned vptr ARMLargePage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMLargePage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMLargePage) pd_ptr) (create_mapping_entries base vptr ARMLargePage vm_rights attrib pd_ptr)
 3. vmsz_aligned vptr ARMSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSection) pd_ptr) (create_mapping_entries base vptr ARMSection vm_rights attrib pd_ptr)
 4. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (state)
this:
vmsz_aligned vptr ARMSmallPage

goal (4 subgoals):
 1. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSmallPage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSmallPage) pd_ptr) (create_mapping_entries base vptr ARMSmallPage vm_rights attrib pd_ptr)
 2. vmsz_aligned vptr ARMLargePage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMLargePage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMLargePage) pd_ptr) (create_mapping_entries base vptr ARMLargePage vm_rights attrib pd_ptr)
 3. vmsz_aligned vptr ARMSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSection) pd_ptr) (create_mapping_entries base vptr ARMSection vm_rights attrib pd_ptr)
 4. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSmallPage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSmallPage) pd_ptr) (create_mapping_entries base vptr ARMSmallPage vm_rights attrib pd_ptr) proof (prove)
using this:
vmsz_aligned vptr ARMSmallPage

goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSmallPage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSmallPage) pd_ptr) (create_mapping_entries base vptr ARMSmallPage vm_rights attrib pd_ptr) proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref xa])) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) a)) (cdl_page_mapping_entries vptr 12 pd_ptr) (injection_handler (FailedLookup False) (lookup_pt_slot pd_ptr vptr)) proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref xa])) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) a)) (cdl_page_mapping_entries vptr 12 pd_ptr) (lookup_pt_slot pd_ptr vptr) proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref xa])) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) a)) (doE p <- cdl_lookup_pt_slot pd_ptr vptr;
returnOk [p]
odE) (lookup_pt_slot pd_ptr vptr) proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref xa])) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) a)) (doE p <- cdl_lookup_pt_slot pd_ptr vptr;
returnOk [p]
odE) (lookup_pt_slot pd_ptr vptr >>=E returnOk) proof (prove)
goal (3 subgoals):
 1. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref xa])) ?Q8 ?Q'8 (doE p <- cdl_lookup_pt_slot pd_ptr vptr;
returnOk [p]
odE) (lookup_pt_slot pd_ptr vptr >>=E returnOk)
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSmallPage; True\<rbrakk> \<Longrightarrow> ?Q8 s
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSmallPage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ?Q'8 s proof (prove)
goal (6 subgoals):
 1. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> dcorres (dc \<oplus> ?r'12) ?P12 ?P'12 (cdl_lookup_pt_slot pd_ptr vptr) (lookup_pt_slot pd_ptr vptr)
 2. \<And>p rv'. \<lbrakk>vmsz_aligned vptr ARMSmallPage; ?r'12 p rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref xa])) (?R12 p) (?R'12 rv') (returnOk [p]) (returnOk rv')
 3. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> \<lbrace>?Q12\<rbrace> cdl_lookup_pt_slot pd_ptr vptr \<lbrace>?R12\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> \<lbrace>?Q'12\<rbrace> lookup_pt_slot pd_ptr vptr \<lbrace>?R'12\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSmallPage; True\<rbrakk> \<Longrightarrow> (?P12 and ?Q12) s
 6. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSmallPage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> (?P'12 and ?Q'12) s proof (prove)
goal (5 subgoals):
 1. \<And>p rv'. \<lbrakk>vmsz_aligned vptr ARMSmallPage; p = transform_pt_slot_ref rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref xa])) (?R12 p) (?R'12 rv') (returnOk [p]) (returnOk rv')
 2. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> \<lbrace>?Q12\<rbrace> cdl_lookup_pt_slot pd_ptr vptr \<lbrace>?R12\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> \<lbrace>?Q'12\<rbrace> lookup_pt_slot pd_ptr vptr \<lbrace>?R'12\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSmallPage; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12) s
 5. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSmallPage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned and K (is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'12) s proof (prove)
goal (4 subgoals):
 1. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> \<lbrace>?Q12\<rbrace> cdl_lookup_pt_slot pd_ptr vptr \<lbrace>\<lambda>p _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. vmsz_aligned vptr ARMSmallPage \<Longrightarrow> \<lbrace>?Q'12\<rbrace> lookup_pt_slot pd_ptr vptr \<lbrace>\<lambda>rv' _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSmallPage; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12) s
 4. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSmallPage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned and K (is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'12) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSmallPage; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSmallPage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned and K (is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. True \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSmallPage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned and K (is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. True \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s ref. \<lbrakk>vmsz_aligned vptr ARMSmallPage; valid_idle s; valid_vspace_objs s; pspace_aligned s; (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s; is_aligned pd_ptr pd_bits\<rbrakk> \<Longrightarrow> is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (2 subgoals):
 1. \<And>s ref. \<lbrakk>vmsz_aligned vptr ARMSmallPage; valid_idle s; valid_vspace_objs s; pspace_aligned s; (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s; is_aligned pd_ptr pd_bits\<rbrakk> \<Longrightarrow> 0 = 0 \<or> 0 < 2 ^ 4 \<and> vmsz_aligned vptr ARMSuperSection
 2. \<And>s ref. \<lbrakk>vmsz_aligned vptr ARMSmallPage; valid_idle s; valid_vspace_objs s; pspace_aligned s; (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s; is_aligned pd_ptr pd_bits; UCAST(32 \<rightarrow> 12) ((0 << 2) + lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<And>s ref. \<lbrakk>vmsz_aligned vptr ARMSmallPage; valid_idle s; valid_vspace_objs s; pspace_aligned s; (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s; is_aligned pd_ptr pd_bits; UCAST(32 \<rightarrow> 12) ((0 << 2) + lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal:
No subgoals! proof (state)
this:
dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSmallPage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSmallPage) pd_ptr) (create_mapping_entries base vptr ARMSmallPage vm_rights attrib pd_ptr)

goal (3 subgoals):
 1. vmsz_aligned vptr ARMLargePage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMLargePage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMLargePage) pd_ptr) (create_mapping_entries base vptr ARMLargePage vm_rights attrib pd_ptr)
 2. vmsz_aligned vptr ARMSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSection) pd_ptr) (create_mapping_entries base vptr ARMSection vm_rights attrib pd_ptr)
 3. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (state)
goal (3 subgoals):
 1. vmsz_aligned vptr ARMLargePage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMLargePage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMLargePage) pd_ptr) (create_mapping_entries base vptr ARMLargePage vm_rights attrib pd_ptr)
 2. vmsz_aligned vptr ARMSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSection) pd_ptr) (create_mapping_entries base vptr ARMSection vm_rights attrib pd_ptr)
 3. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (state)
this:
vmsz_aligned vptr ARMLargePage

goal (3 subgoals):
 1. vmsz_aligned vptr ARMLargePage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMLargePage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMLargePage) pd_ptr) (create_mapping_entries base vptr ARMLargePage vm_rights attrib pd_ptr)
 2. vmsz_aligned vptr ARMSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSection) pd_ptr) (create_mapping_entries base vptr ARMSection vm_rights attrib pd_ptr)
 3. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMLargePage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMLargePage) pd_ptr) (create_mapping_entries base vptr ARMLargePage vm_rights attrib pd_ptr) proof (prove)
using this:
vmsz_aligned vptr ARMLargePage

goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMLargePage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMLargePage) pd_ptr) (create_mapping_entries base vptr ARMLargePage vm_rights attrib pd_ptr) proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMLargePage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref (hd (map (\<lambda>x. x + xa) largePagePTE_offsets))])) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) a)) (cdl_page_mapping_entries vptr 16 pd_ptr) (injection_handler (FailedLookup False) (lookup_pt_slot pd_ptr vptr)) proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMLargePage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref (hd (map (\<lambda>x. x + xa) largePagePTE_offsets))])) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) a)) (cdl_page_mapping_entries vptr 16 pd_ptr) (lookup_pt_slot pd_ptr vptr) proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMLargePage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref (hd (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]))])) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) a)) (doE p <- cdl_lookup_pt_slot pd_ptr vptr;
returnOk [p]
odE) (lookup_pt_slot pd_ptr vptr) proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMLargePage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref (hd (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]))])) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) a)) (doE p <- cdl_lookup_pt_slot pd_ptr vptr;
returnOk [p]
odE) (lookup_pt_slot pd_ptr vptr >>=E returnOk) proof (prove)
goal (3 subgoals):
 1. vmsz_aligned vptr ARMLargePage \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref (hd (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]))])) ?Q9 ?Q'9 (doE p <- cdl_lookup_pt_slot pd_ptr vptr;
returnOk [p]
odE) (lookup_pt_slot pd_ptr vptr >>=E returnOk)
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; True\<rbrakk> \<Longrightarrow> ?Q9 s
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s)\<rbrakk> \<Longrightarrow> ?Q'9 s proof (prove)
goal (6 subgoals):
 1. vmsz_aligned vptr ARMLargePage \<Longrightarrow> dcorres (dc \<oplus> ?r'13) ?P13 ?P'13 (cdl_lookup_pt_slot pd_ptr vptr) (lookup_pt_slot pd_ptr vptr)
 2. \<And>p rv'. \<lbrakk>vmsz_aligned vptr ARMLargePage; ?r'13 p rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref (hd (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]))])) (?R13 p) (?R'13 rv') (returnOk [p]) (returnOk rv')
 3. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q13\<rbrace> cdl_lookup_pt_slot pd_ptr vptr \<lbrace>?R13\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q'13\<rbrace> lookup_pt_slot pd_ptr vptr \<lbrace>?R'13\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; True\<rbrakk> \<Longrightarrow> (?P13 and ?Q13) s
 6. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s)\<rbrakk> \<Longrightarrow> (?P'13 and ?Q'13) s proof (prove)
goal (5 subgoals):
 1. \<And>p rv'. \<lbrakk>vmsz_aligned vptr ARMLargePage; p = transform_pt_slot_ref rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref (hd (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]))])) (?R13 p) (?R'13 rv') (returnOk [p]) (returnOk rv')
 2. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q13\<rbrace> cdl_lookup_pt_slot pd_ptr vptr \<lbrace>?R13\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q'13\<rbrace> lookup_pt_slot pd_ptr vptr \<lbrace>?R'13\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q13) s
 5. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s)\<rbrakk> \<Longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned and K (is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'13) s proof (prove)
goal (5 subgoals):
 1. \<And>p rv'. \<lbrakk>vmsz_aligned vptr ARMLargePage; p = transform_pt_slot_ref rv'; is_aligned rv' 6\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pt_slot_ref (hd (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]))])) (?R13 p) (?P'20 rv') (returnOk [p]) (returnOk rv')
 2. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q13\<rbrace> cdl_lookup_pt_slot pd_ptr vptr \<lbrace>?R13\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q'13\<rbrace> lookup_pt_slot pd_ptr vptr \<lbrace>\<lambda>rv'. ?P'20 rv' and (\<lambda>s. is_aligned rv' 6)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q13) s
 5. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s)\<rbrakk> \<Longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned and K (is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'13) s proof (prove)
goal (5 subgoals):
 1. \<And>p rv'. \<lbrakk>vmsz_aligned vptr ARMLargePage; p = transform_pt_slot_ref rv'; is_aligned rv' 6\<rbrakk> \<Longrightarrow> [p] = [transform_pt_slot_ref (hd (map (\<lambda>x. x + rv') [0 , 4 .e. 0x3C]))]
 2. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q13\<rbrace> cdl_lookup_pt_slot pd_ptr vptr \<lbrace>\<lambda>p _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q'13\<rbrace> lookup_pt_slot pd_ptr vptr \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (\<lambda>s. is_aligned rv' 6)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q13) s
 5. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s)\<rbrakk> \<Longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned and K (is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'13) s proof (prove)
goal (6 subgoals):
 1. \<And>p rv'. \<lbrakk>vmsz_aligned vptr ARMLargePage; p = transform_pt_slot_ref rv'; is_aligned rv' 6\<rbrakk> \<Longrightarrow> is_aligned rv' 6
 2. \<And>p rv'. \<lbrakk>vmsz_aligned vptr ARMLargePage; p = transform_pt_slot_ref rv'; is_aligned rv' 6\<rbrakk> \<Longrightarrow> [p] = [transform_pt_slot_ref rv']
 3. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q13\<rbrace> cdl_lookup_pt_slot pd_ptr vptr \<lbrace>\<lambda>p _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q'13\<rbrace> lookup_pt_slot pd_ptr vptr \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (\<lambda>s. is_aligned rv' 6)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q13) s
 6. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s)\<rbrakk> \<Longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned and K (is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'13) s proof (prove)
goal (5 subgoals):
 1. \<And>p rv'. \<lbrakk>vmsz_aligned vptr ARMLargePage; p = transform_pt_slot_ref rv'; is_aligned rv' 6\<rbrakk> \<Longrightarrow> [p] = [transform_pt_slot_ref rv']
 2. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q13\<rbrace> cdl_lookup_pt_slot pd_ptr vptr \<lbrace>\<lambda>p _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q'13\<rbrace> lookup_pt_slot pd_ptr vptr \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (\<lambda>s. is_aligned rv' 6)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q13) s
 5. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s)\<rbrakk> \<Longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned and K (is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'13) s proof (prove)
goal (4 subgoals):
 1. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q13\<rbrace> cdl_lookup_pt_slot pd_ptr vptr \<lbrace>\<lambda>p _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. vmsz_aligned vptr ARMLargePage \<Longrightarrow> \<lbrace>?Q'13\<rbrace> lookup_pt_slot pd_ptr vptr \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (\<lambda>s. is_aligned rv' 6)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q13) s
 4. \<And>s. \<lbrakk>vmsz_aligned vptr ARMLargePage; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s)\<rbrakk> \<Longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned and K (is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'13) s proof (prove)
goal (1 subgoal):
 1. \<And>s ref. \<lbrakk>vmsz_aligned vptr ARMLargePage; typ_at (AArch APageDirectory) pd_ptr s; valid_idle s; valid_vspace_objs s; pspace_aligned s; (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) \<and> is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) \<and> is_aligned pd_ptr 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<And>s ref. \<lbrakk>vmsz_aligned vptr ARMLargePage; valid_idle s; valid_vspace_objs s; pspace_aligned s; (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s; is_aligned pd_ptr pd_bits\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) \<and> is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) \<and> is_aligned pd_ptr 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (2 subgoals):
 1. \<And>s ref. \<lbrakk>vmsz_aligned vptr ARMLargePage; valid_idle s; valid_vspace_objs s; pspace_aligned s; (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s; is_aligned pd_ptr pd_bits\<rbrakk> \<Longrightarrow> 0 = 0 \<or> 0 < 2 ^ 4 \<and> vmsz_aligned vptr ARMSuperSection
 2. \<And>s ref. \<lbrakk>vmsz_aligned vptr ARMLargePage; valid_idle s; valid_vspace_objs s; pspace_aligned s; (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s; is_aligned pd_ptr pd_bits; UCAST(32 \<rightarrow> 12) ((0 << 2) + lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) \<and> is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) \<and> is_aligned pd_ptr 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<And>s ref. \<lbrakk>vmsz_aligned vptr ARMLargePage; valid_idle s; valid_vspace_objs s; pspace_aligned s; (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s; is_aligned pd_ptr pd_bits; UCAST(32 \<rightarrow> 12) ((0 << 2) + lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) \<and> is_aligned pd_ptr 14 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s) \<and> is_aligned pd_ptr 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<And>s ref. \<lbrakk>is_aligned vptr 16; valid_idle s; valid_vspace_objs s; pspace_aligned s; (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s; is_aligned pd_ptr 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd_ptr vptr && mask 14 >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask 14)) s proof (prove)
goal:
No subgoals! proof (state)
this:
dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMLargePage) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMLargePage) pd_ptr) (create_mapping_entries base vptr ARMLargePage vm_rights attrib pd_ptr)

goal (2 subgoals):
 1. vmsz_aligned vptr ARMSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSection) pd_ptr) (create_mapping_entries base vptr ARMSection vm_rights attrib pd_ptr)
 2. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (state)
goal (2 subgoals):
 1. vmsz_aligned vptr ARMSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSection) pd_ptr) (create_mapping_entries base vptr ARMSection vm_rights attrib pd_ptr)
 2. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (state)
this:
vmsz_aligned vptr ARMSection

goal (2 subgoals):
 1. vmsz_aligned vptr ARMSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSection) pd_ptr) (create_mapping_entries base vptr ARMSection vm_rights attrib pd_ptr)
 2. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSection) pd_ptr) (create_mapping_entries base vptr ARMSection vm_rights attrib pd_ptr) proof (prove)
using this:
vmsz_aligned vptr ARMSection

goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSection) pd_ptr) (create_mapping_entries base vptr ARMSection vm_rights attrib pd_ptr) proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pd_slot_ref xa] \<and> transform_pde (SectionPDE base (attrib - {Global}) 0 vm_rights) = FrameCap False (ptrFromPAddr base) vm_rights 20 Fake None)) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) a)) (cdl_page_mapping_entries vptr 20 pd_ptr) (returnOk (lookup_pd_slot pd_ptr vptr)) proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pd_slot_ref xa] \<and> transform_pde (SectionPDE base (attrib - {Global}) 0 vm_rights) = FrameCap False (ptrFromPAddr base) vm_rights 20 Fake None)) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) a)) (returnOk [cdl_lookup_pd_slot pd_ptr vptr]) (returnOk (lookup_pd_slot pd_ptr vptr)) proof (prove)
goal (3 subgoals):
 1. vmsz_aligned vptr ARMSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pd_slot_ref xa] \<and> transform_pde (SectionPDE base (attrib - {Global}) 0 vm_rights) = FrameCap False (ptrFromPAddr base) vm_rights 20 Fake None)) ?Q5 ?Q'5 (returnOk [cdl_lookup_pd_slot pd_ptr vptr]) (returnOk (lookup_pd_slot pd_ptr vptr))
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSection; True\<rbrakk> \<Longrightarrow> ?Q5 s
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSection; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ?Q'5 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vmsz_aligned vptr ARMSection; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pd_slot_ref xa] \<and> transform_pde (SectionPDE base (attrib - {Global}) 0 vm_rights) = FrameCap False (ptrFromPAddr base) vm_rights 20 Fake None)) ?Q5 ?P'9 (returnOk [cdl_lookup_pd_slot pd_ptr vptr]) (returnOk (lookup_pd_slot pd_ptr vptr))
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSection; True\<rbrakk> \<Longrightarrow> ?Q5 s
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSection; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> (?P'9 and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vmsz_aligned vptr ARMSection; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> [cdl_lookup_pd_slot pd_ptr vptr] = [transform_pd_slot_ref (lookup_pd_slot pd_ptr vptr)] \<and> transform_pde (SectionPDE base (attrib - {Global}) 0 vm_rights) = FrameCap False (ptrFromPAddr base) vm_rights 20 Fake None
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSection; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSection; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned vptr 20; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> cdl_lookup_pd_slot pd_ptr vptr = transform_pd_slot_ref (lookup_pd_slot pd_ptr vptr)
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSection; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSection; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSection; True\<rbrakk> \<Longrightarrow> True
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSection; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSection; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal:
No subgoals! proof (state)
this:
dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSection) pd_ptr) (create_mapping_entries base vptr ARMSection vm_rights attrib pd_ptr)

goal (1 subgoal):
 1. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (state)
goal (1 subgoal):
 1. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (state)
this:
vmsz_aligned vptr ARMSuperSection

goal (1 subgoal):
 1. vmsz_aligned vptr ARMSuperSection \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (prove)
using this:
vmsz_aligned vptr ARMSuperSection

goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (prove)
using this:
vmsz_aligned vptr ARMSuperSection
is_aligned pd_ptr pd_bits

goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pd_slot_ref (hd (map (\<lambda>x. x + xa) superSectionPDE_offsets))] \<and> transform_pde (SuperSectionPDE base (attrib - {Global}) vm_rights) = FrameCap False (ptrFromPAddr base) vm_rights 24 Fake None)) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) a)) (cdl_page_mapping_entries vptr 24 pd_ptr) (returnOk (lookup_pd_slot pd_ptr vptr)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pd_slot_ref (hd (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]))] \<and> transform_pde (SuperSectionPDE base (attrib - {Global}) vm_rights) = FrameCap False (ptrFromPAddr base) vm_rights 24 Fake None)) (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) pd_ptr a \<and> valid_idle a \<and> valid_vspace_objs a \<and> pspace_aligned a \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) a)) (returnOk [cdl_lookup_pd_slot pd_ptr vptr]) (returnOk (lookup_pd_slot pd_ptr vptr)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pd_slot_ref (hd (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]))] \<and> transform_pde (SuperSectionPDE base (attrib - {Global}) vm_rights) = FrameCap False (ptrFromPAddr base) vm_rights 24 Fake None)) ?Q5 ?Q'5 (returnOk [cdl_lookup_pd_slot pd_ptr vptr]) (returnOk (lookup_pd_slot pd_ptr vptr))
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; True\<rbrakk> \<Longrightarrow> ?Q5 s
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ?Q'5 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x xa. x = [transform_pd_slot_ref (hd (map (\<lambda>x. x + xa) [0 , 4 .e. 0x3C]))] \<and> transform_pde (SuperSectionPDE base (attrib - {Global}) vm_rights) = FrameCap False (ptrFromPAddr base) vm_rights 24 Fake None)) ?Q5 ?P'9 (returnOk [cdl_lookup_pd_slot pd_ptr vptr]) (returnOk (lookup_pd_slot pd_ptr vptr))
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; True\<rbrakk> \<Longrightarrow> ?Q5 s
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> (?P'9 and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> [cdl_lookup_pd_slot pd_ptr vptr] = [transform_pd_slot_ref (hd (map (\<lambda>x. x + lookup_pd_slot pd_ptr vptr) [0 , 4 .e. 0x3C]))] \<and> transform_pde (SuperSectionPDE base (attrib - {Global}) vm_rights) = FrameCap False (ptrFromPAddr base) vm_rights 24 Fake None
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned vptr 24; is_aligned pd_ptr pd_bits; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> cdl_lookup_pd_slot pd_ptr vptr = transform_pd_slot_ref (hd (map (\<lambda>x. x + lookup_pd_slot pd_ptr vptr) [0 , 4 .e. 0x3C]))
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned vptr 24; is_aligned pd_ptr pd_bits; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot pd_ptr vptr) 6
 2. \<lbrakk>is_aligned vptr 24; is_aligned pd_ptr pd_bits; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> cdl_lookup_pd_slot pd_ptr vptr = transform_pd_slot_ref (lookup_pd_slot pd_ptr vptr)
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>is_aligned vptr 24; is_aligned pd_ptr pd_bits; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> vmsz_aligned vptr ARMSuperSection
 2. \<lbrakk>is_aligned vptr 24; is_aligned pd_ptr pd_bits; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> is_aligned pd_ptr 14
 3. \<lbrakk>is_aligned vptr 24; is_aligned pd_ptr pd_bits; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> cdl_lookup_pd_slot pd_ptr vptr = transform_pd_slot_ref (lookup_pd_slot pd_ptr vptr)
 4. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned vptr 24; is_aligned pd_ptr pd_bits; is_aligned pd_ptr 14\<rbrakk> \<Longrightarrow> cdl_lookup_pd_slot pd_ptr vptr = transform_pd_slot_ref (lookup_pd_slot pd_ptr vptr)
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; True\<rbrakk> \<Longrightarrow> True
 2. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz_aligned vptr ARMSuperSection; is_aligned pd_ptr pd_bits; typ_at (AArch APageDirectory) pd_ptr s \<and> valid_idle s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. is_aligned pd_ptr 14)) s proof (prove)
goal:
No subgoals! proof (state)
this:
dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl a \<Rightarrow> (transform_pte \<circ> fst) a | Inr a \<Rightarrow> (transform_pde \<circ> fst) a) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize ARMSuperSection) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize ARMSuperSection) pd_ptr) (create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd_ptr)

goal:
No subgoals! proof (state)
this:
dcorres (dc \<oplus> (\<lambda>rv rv'. rv = (case rv' of Inl pair \<Rightarrow> [(transform_pt_slot_ref \<circ> hd \<circ> snd) pair] | Inr pair \<Rightarrow> [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) \<and> (case rv' of Inl x \<Rightarrow> (transform_pte \<circ> fst) x | Inr x \<Rightarrow> (transform_pde \<circ> fst) x) = FrameCap False (ptrFromPAddr base) vm_rights (pageBitsForSize pgsz) Fake None)) (\<lambda>_. True) (typ_at (AArch APageDirectory) pd_ptr and valid_idle and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)) s)) (cdl_page_mapping_entries vptr (pageBitsForSize pgsz) pd_ptr) (create_mapping_entries base vptr pgsz vm_rights attrib pd_ptr)

goal:
No subgoals!