theory Arch_C

lemma createMappingEntries_valid_pte_slots'2:
  "\<lbrace>K (vmsz_aligned' vptr sz) and valid_objs'\<rbrace>
     createMappingEntries base vptr sz vm_rights attrib pt
   \<lbrace>\<lambda>rv. valid_pte_slots'2 rv\<rbrace>,-" apply (simp add: createMappingEntries_def valid_pde_slots'2_def) apply (cases sz, simp_all) apply (wp | simp)+ apply (simp add:lookupPTSlot_def) apply (wp getPDE_wp|wpc|simp add: checkPTAt_def valid_pte_slots'2_def)+ apply (clarsimp simp:valid_pte_slots'2_def lookup_pt_slot_no_fail_def) apply (rule_tac x = 0 in exI) apply (subst vaddr_segment_nonsense3[simplified pt_bits_stuff]) apply (simp add: page_table_at'_def ptBits_def pageBits_def pteBits_def) apply simp apply (rule aligned_add_aligned[where n = 2]) apply (drule pde_align_ptBits) apply simp apply (erule is_aligned_weaken) apply (simp add:ptBits_def pageBits_def) apply (simp add: is_aligned_shiftl) apply simp apply (simp add:lookupPTSlot_def) apply (wp getPDE_wp|wpc|simp add: valid_pte_slots'2_def checkPTAt_def)+ apply (clarsimp simp:valid_pte_slots'2_def lookup_pt_slot_no_fail_def) apply (rule_tac x = 4 in exI) apply (clarsimp simp:upto_enum_step_def largePagePTEOffsets_def pteBits_def
                    split:if_splits) apply (rule context_conjI) apply (simp add: vmsz_aligned'_def upto_enum_def hd_map_simp) apply (erule(1) aligned_add_aligned[OF pde_align_ptBits]) apply (rule is_aligned_shiftl[OF aligned_already_mask],simp) apply (rule is_aligned_shiftr) apply simp apply (simp add:ptBits_def pageBits_def) apply (clarsimp simp:upto_enum_def hd_map_simp) apply (subst vaddr_segment_nonsense3[simplified pt_bits_stuff]) apply (simp add: page_table_at'_def ptBits_def pageBits_def pteBits_def) apply simp apply (wp | simp add:valid_pte_slots'2_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (vmsz_aligned' vptr sz) and valid_objs'\<rbrace> createMappingEntries base vptr sz vm_rights attrib pt \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. vmsz_aligned' vptr sz) and valid_objs'\<rbrace> case sz of local.ARMSmallPage \<Rightarrow> doE p <- lookupErrorOnFailure False $ lookupPTSlot pt vptr;
returnOk $ Inl (ARM_H.SmallPagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [p])
odE | local.ARMLargePage \<Rightarrow> doE p <- lookupErrorOnFailure False $ lookupPTSlot pt vptr;
returnOk $ Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets)
odE | local.ARMSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pt vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [p])
odE | local.ARMSuperSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pt vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. sz = Wellformed_C.ARMSmallPage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSmallPage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.SmallPagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [p]))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 2. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. sz = Wellformed_C.ARMSmallPage \<Longrightarrow> \<lbrace>?P'8\<rbrace> lookupPTSlot pt vptr \<lbrace>\<lambda>p. valid_pte_slots'2 (Inl (ARM_H.SmallPagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [p]))\<rbrace>, -
 2. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSmallPage; ((\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSmallPage) and valid_objs') s\<rbrakk> \<Longrightarrow> True \<and> ?P'8 s
 3. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 5. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. sz = Wellformed_C.ARMSmallPage \<Longrightarrow> \<lbrace>?P'8\<rbrace> doE pde <- liftE (getObject (lookup_pd_slot pt 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. valid_pte_slots'2 (Inl (ARM_H.SmallPagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [p]))\<rbrace>, -
 2. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSmallPage; ((\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSmallPage) and valid_objs') s\<rbrakk> \<Longrightarrow> True \<and> ?P'8 s
 3. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 5. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage \<and> valid_objs' s\<rbrakk> \<Longrightarrow> \<forall>ko. ko_at' ko (lookup_pd_slot pt vptr) s \<longrightarrow> (\<forall>x. (\<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb) \<longrightarrow> page_table_at' (ptrFromPAddr x) s \<longrightarrow> (\<exists>sz\<le>4. Suc 0 = 2 ^ sz \<and> is_aligned (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr) (Suc (Suc sz)) \<and> page_table_at' (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr && ~~ mask ptBits) s \<and> (sz = 0 \<or> sz = 4)))
 2. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<exists>sz\<le>4. Suc 0 = 2 ^ sz \<and> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) (Suc (Suc sz)) \<and> page_table_at' (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask ptBits) s \<and> (sz = 0 \<or> sz = 4)
 2. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 0 \<le> 4 \<and> Suc 0 = 2 ^ 0 \<and> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) (Suc (Suc 0)) \<and> page_table_at' (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask ptBits) s \<and> (0 = 0 \<or> 0 = 4)
 2. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 0 \<le> 4 \<and> Suc 0 = 2 ^ 0 \<and> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) (Suc (Suc 0)) \<and> page_table_at' (ptrFromPAddr x) s \<and> (0 = 0 \<or> 0 = 4)
 3. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 5. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 0 \<le> 4 \<and> Suc 0 = 2 ^ 0 \<and> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) (Suc (Suc 0)) \<and> page_table_at' (ptrFromPAddr x) s \<and> (0 = 0 \<or> 0 = 4)
 2. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) (Suc (Suc 0))
 2. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (6 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 2
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (Suc (Suc 0))
 3. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> Suc (Suc 0) \<le> 2
 4. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 5. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 6. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (7 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) ptBits\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 2
 3. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (Suc (Suc 0))
 4. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> Suc (Suc 0) \<le> 2
 5. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 6. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 7. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (6 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) ptBits\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 2
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (Suc (Suc 0))
 3. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> Suc (Suc 0) \<le> 2
 4. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 5. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 6. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (6 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 2 \<le> ptBits
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (Suc (Suc 0))
 3. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> Suc (Suc 0) \<le> 2
 4. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 5. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 6. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (Suc (Suc 0))
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> Suc (Suc 0) \<le> 2
 3. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 5. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMSmallPage; vmsz_aligned' vptr Wellformed_C.ARMSmallPage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> Suc (Suc 0) \<le> 2
 2. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pt vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 2. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage) and valid_objs'\<rbrace> doE p <- lookupErrorOnFailure False (doE pde <- liftE (getObject (lookup_pd_slot pt 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);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>valid_pte_slots'2\<rbrace>, -
 2. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage \<and> valid_objs' s\<rbrakk> \<Longrightarrow> \<forall>ko. ko_at' ko (lookup_pd_slot pt vptr) s \<longrightarrow> (\<forall>x. (\<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb) \<longrightarrow> page_table_at' (ptrFromPAddr x) s \<longrightarrow> (\<exists>sz\<le>4. length largePagePTEOffsets = 2 ^ sz \<and> is_aligned (hd (map (\<lambda>xa. xa + lookup_pt_slot_no_fail (ptrFromPAddr x) vptr) largePagePTEOffsets)) (Suc (Suc sz)) \<and> page_table_at' (hd (map (\<lambda>xa. xa + lookup_pt_slot_no_fail (ptrFromPAddr x) vptr) largePagePTEOffsets) && ~~ mask ptBits) s \<and> (sz = 0 \<or> sz = 4)))
 2. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<exists>sz\<le>4. length largePagePTEOffsets = 2 ^ sz \<and> is_aligned (hd (map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) largePagePTEOffsets)) (Suc (Suc sz)) \<and> page_table_at' (hd (map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) largePagePTEOffsets) && ~~ mask ptBits) s \<and> (sz = 0 \<or> sz = 4)
 2. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 4 \<le> 4 \<and> length largePagePTEOffsets = 2 ^ 4 \<and> is_aligned (hd (map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) largePagePTEOffsets)) (Suc (Suc 4)) \<and> page_table_at' (hd (map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) largePagePTEOffsets) && ~~ mask ptBits) s \<and> (4 = 0 \<or> 4 = 4)
 2. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF])) 6 \<and> page_table_at' (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF]) && ~~ mask ptBits) s
 2. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF])) 6
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s; is_aligned (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF])) 6\<rbrakk> \<Longrightarrow> page_table_at' (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF]) && ~~ mask ptBits) s
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; is_aligned vptr 16; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s; is_aligned (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF])) 6\<rbrakk> \<Longrightarrow> page_table_at' (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF]) && ~~ mask ptBits) s
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) 6
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 6 \<le> ptBits
 3. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s; is_aligned (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF])) 6\<rbrakk> \<Longrightarrow> page_table_at' (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF]) && ~~ mask ptBits) s
 4. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 5. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>s x. \<lbrakk>sz = Wellformed_C.ARMLargePage; is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 12) 4
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 6 \<le> ptBits
 3. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s; is_aligned (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF])) 6\<rbrakk> \<Longrightarrow> page_table_at' (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF]) && ~~ mask ptBits) s
 4. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 5. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>s x. \<lbrakk>sz = Wellformed_C.ARMLargePage; is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned vptr (4 + 12)
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 6 \<le> ptBits
 3. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s; is_aligned (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF])) 6\<rbrakk> \<Longrightarrow> page_table_at' (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF]) && ~~ mask ptBits) s
 4. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 5. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 6 \<le> ptBits
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s; is_aligned (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF])) 6\<rbrakk> \<Longrightarrow> page_table_at' (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF]) && ~~ mask ptBits) s
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s; is_aligned (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF])) 6\<rbrakk> \<Longrightarrow> page_table_at' (hd (map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> (\<lambda>x. x * 4)) [0 .e. 0xF]) && ~~ mask ptBits) s
 2. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask ptBits) s
 2. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x) s
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>sz = Wellformed_C.ARMLargePage; vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pt vptr) s; page_table_at' (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x) s
 2. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pt vptr])) \<lbrace>valid_pte_slots'2\<rbrace>, -
 2. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection) and valid_objs'\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pt vptr) superSectionPDEOffsets)) \<lbrace>valid_pte_slots'2\<rbrace>, - proof (prove)
goal:
No subgoals!