theory Arch_C

lemma createMappingEntries_valid_pde_slots'2:
  "\<lbrace>page_directory_at' pd and K (vmsz_aligned' vptr sz \<and> vptr < pptrBase)\<rbrace>
     createMappingEntries base vptr sz vm_rights attrib pd
   \<lbrace>\<lambda>rv. valid_pde_slots'2 rv\<rbrace>,-" apply (simp add: createMappingEntries_def valid_pde_slots'2_def) apply (cases sz, simp_all) apply (wp | simp)+ apply (clarsimp simp: page_directory_at'_def
                         lookup_pd_slot_eq[unfolded pd_bits_def, folded pdBits_def]) apply (clarsimp simp: lookup_pd_slot_def Let_def mask_add_aligned) apply (rule conjI) apply (erule less_pptrBase_valid_pde_offset'') apply (rule conjI) apply (clarsimp simp: vaddr_segment_nonsense6) apply (rule_tac x= 0 in exI) apply simp apply (erule aligned_add_aligned
      [OF is_aligned_weaken is_aligned_shiftl,where n = 2]) apply (simp add:pdBits_def) apply (simp add:vmsz_aligned'_def) apply simp apply (rule hoare_pre, wp) apply (clarsimp simp: vmsz_aligned'_def page_directory_at'_def lookup_pd_slot_def) apply (rule conjI) subgoal \<comment> \<open>valid_pde_mapping_offset'\<close> apply (clarsimp simp: superSectionPDEOffsets_def length_upto_enum_step pdeBits_def) apply (clarsimp simp: upto_enum_step_def upto_enum_def comp_def) apply (clarsimp simp: linorder_not_less field_simps mask_add_aligned) apply (erule less_pptrBase_valid_pde_offset', simp+) apply (rule word_of_nat_le, simp) done apply (rule conjI) subgoal \<comment> \<open>pde_at'\<close> apply (clarsimp simp: superSectionPDEOffsets_def length_upto_enum_step pdeBits_def) apply (clarsimp simp:upto_enum_step_def upto_enum_def hd_map_simp comp_def) apply (simp add: vaddr_segment_nonsense6) done apply (rule_tac x = 4 in exI) apply (clarsimp simp: superSectionPDEOffsets_def length_upto_enum_step pdeBits_def) apply (clarsimp simp:upto_enum_step_def upto_enum_def hd_map_simp comp_def isSuperSectionPDE_def) apply (erule aligned_add_aligned) apply (rule is_aligned_shiftl, simp) apply (rule is_aligned_shiftr) apply simp apply (simp add: pdBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>page_directory_at' pd and K (vmsz_aligned' vptr sz \<and> vptr < pptrBase)\<rbrace> createMappingEntries base vptr sz vm_rights attrib pd \<lbrace>valid_pde_slots'2\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr sz \<and> vptr < pptrBase)\<rbrace> case sz of local.ARMSmallPage \<Rightarrow> doE p <- lookupErrorOnFailure False $ lookupPTSlot pd vptr;
returnOk $ Inl (ARM_H.SmallPagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [p])
odE | local.ARMLargePage \<Rightarrow> doE p <- lookupErrorOnFailure False $ lookupPTSlot pd 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 pd 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 pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. sz = Wellformed_C.ARMSmallPage \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSmallPage \<and> vptr < pptrBase)\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pd vptr);
returnOk (Inl (ARM_H.SmallPagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [p]))
odE \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, -
 2. sz = Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMLargePage \<and> vptr < pptrBase)\<rbrace> doE p <- lookupErrorOnFailure False (lookupPTSlot pd vptr);
returnOk (Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + p) largePagePTEOffsets))
odE \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, -
 3. sz = Wellformed_C.ARMSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, -
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; page_directory_at' pd s \<and> vmsz_aligned' vptr Wellformed_C.ARMSection \<and> vptr < pptrBase\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' (lookup_pd_slot pd vptr && mask pdBits) \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. Suc 0 = 2 ^ sz \<and> is_aligned (lookup_pd_slot pd vptr) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))
 2. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' (lookup_pd_slot pd vptr && mask pdBits) \<and> (\<forall>y<0x1000. pde_at' ((lookup_pd_slot pd vptr && ~~ mask pdBits) + (y << 2)) s) \<and> (\<exists>sz\<le>4. Suc 0 = 2 ^ sz \<and> is_aligned (lookup_pd_slot pd vptr) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))
 2. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' ((vptr >> 20 << 2) && mask pdBits) \<and> (\<forall>y<0x1000. pde_at' ((pd + (vptr >> 20 << 2) && ~~ mask pdBits) + (y << 2)) s) \<and> (\<exists>sz\<le>4. Suc 0 = 2 ^ sz \<and> is_aligned (pd + (vptr >> 20 << 2)) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))
 2. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' ((vptr >> 20 << 2) && mask pdBits)
 2. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> (\<forall>y<0x1000. pde_at' ((pd + (vptr >> 20 << 2) && ~~ mask pdBits) + (y << 2)) s) \<and> (\<exists>sz\<le>4. Suc 0 = 2 ^ sz \<and> is_aligned (pd + (vptr >> 20 << 2)) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> (\<forall>y<0x1000. pde_at' ((pd + (vptr >> 20 << 2) && ~~ mask pdBits) + (y << 2)) s) \<and> (\<exists>sz\<le>4. Suc 0 = 2 ^ sz \<and> is_aligned (pd + (vptr >> 20 << 2)) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))
 2. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. pde_at' ((pd + (vptr >> 20 << 2) && ~~ mask pdBits) + (y << 2)) s
 2. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<exists>sz\<le>4. Suc 0 = 2 ^ sz \<and> is_aligned (pd + (vptr >> 20 << 2)) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4)
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<exists>sz\<le>4. Suc 0 = 2 ^ sz \<and> is_aligned (pd + (vptr >> 20 << 2)) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4)
 2. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> 0 \<le> 4 \<and> Suc 0 = 2 ^ 0 \<and> is_aligned (pd + (vptr >> 20 << 2)) (Suc (Suc 0)) \<and> (0 = 0 \<or> 0 = 4)
 2. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (pd + (vptr >> 20 << 2)) (Suc (Suc 0))
 2. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> 2 \<le> pdBits
 2. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 20) (Suc (Suc 0) - 2)
 3. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> Suc (Suc 0) \<le> 2
 4. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 20) (Suc (Suc 0) - 2)
 2. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> Suc (Suc 0) \<le> 2
 3. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; vmsz_aligned' vptr Wellformed_C.ARMSection; vptr < pptrBase\<rbrakk> \<Longrightarrow> Suc (Suc 0) \<le> 2
 2. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. sz = Wellformed_C.ARMSuperSection \<Longrightarrow> \<lbrace>page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)\<rbrace> returnOk (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) \<lbrace>\<lambda>rv s. \<forall>a b. rv = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; (page_directory_at' pd and (\<lambda>y. vmsz_aligned' vptr Wellformed_C.ARMSuperSection \<and> vptr < pptrBase)) s\<rbrakk> \<Longrightarrow> \<forall>a b. Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets) = Inr (a, b) \<longrightarrow> (\<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits)) \<and> page_directory_at' (hd b && ~~ mask pdBits) s \<and> (\<exists>sz\<le>4. length b = 2 ^ sz \<and> is_aligned (hd b) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set superSectionPDEOffsets. valid_pde_mapping_offset' (x + (pd + (vptr >> 20 << 2)) && mask pdBits)) \<and> (\<forall>y<0x1000. pde_at' ((hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) superSectionPDEOffsets) && ~~ mask pdBits) + (y << 2)) s) \<and> (\<exists>sz\<le>4. length superSectionPDEOffsets = 2 ^ sz \<and> is_aligned (hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) superSectionPDEOffsets)) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>x\<in>set superSectionPDEOffsets. valid_pde_mapping_offset' (x + (pd + (vptr >> 20 << 2)) && mask pdBits)
 2. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> (\<forall>y<0x1000. pde_at' ((hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) superSectionPDEOffsets) && ~~ mask pdBits) + (y << 2)) s) \<and> (\<exists>sz\<le>4. length superSectionPDEOffsets = 2 ^ sz \<and> is_aligned (hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) superSectionPDEOffsets)) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s_; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>x\<in>set superSectionPDEOffsets. valid_pde_mapping_offset' (x + (pd + (vptr >> 20 << 2)) && mask pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s_; is_aligned vptr 24; vptr < pptrBase; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' (x + (pd + (vptr >> 20 << 2)) && mask pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s_; is_aligned vptr 24; vptr < pptrBase; xa < 16\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' (word_of_nat xa * 4 + (pd + (vptr >> 20 << 2)) && mask pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s_; is_aligned vptr 24; vptr < pptrBase; xa < 16\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' (word_of_nat xa * 4 + (vptr >> 20 << 2) && mask pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s_; is_aligned vptr 24; xa < 16\<rbrakk> \<Longrightarrow> word_of_nat xa \<le> 0xF proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> (\<forall>y<0x1000. pde_at' ((hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) superSectionPDEOffsets) && ~~ mask pdBits) + (y << 2)) s) \<and> (\<exists>sz\<le>4. length superSectionPDEOffsets = 2 ^ sz \<and> is_aligned (hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) superSectionPDEOffsets)) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. pde_at' ((hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) superSectionPDEOffsets) && ~~ mask pdBits) + (y << 2)) s
 2. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<exists>sz\<le>4. length superSectionPDEOffsets = 2 ^ sz \<and> is_aligned (hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) superSectionPDEOffsets)) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s_; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. pde_at' ((hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) superSectionPDEOffsets) && ~~ mask pdBits) + (y << 2)) s_ proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s_; is_aligned vptr 24; vptr < pptrBase; y < 0x1000\<rbrakk> \<Longrightarrow> pde_at' ((hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) [0 , 4 .e. 0x3C]) && ~~ mask pdBits) + (y << 2)) s_ proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s_; is_aligned vptr 24; vptr < pptrBase; y < 0x1000\<rbrakk> \<Longrightarrow> pde_at' ((pd + (vptr >> 20 << 2) && ~~ mask pdBits) + (y << 2)) s_ proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<exists>sz\<le>4. length superSectionPDEOffsets = 2 ^ sz \<and> is_aligned (hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) superSectionPDEOffsets)) (Suc (Suc sz)) \<and> (sz = 0 \<or> sz = 4) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> 4 \<le> 4 \<and> length superSectionPDEOffsets = 2 ^ 4 \<and> is_aligned (hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) superSectionPDEOffsets)) (Suc (Suc 4)) \<and> (4 = 0 \<or> 4 = 4) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (hd (map (\<lambda>x. x + (pd + (vptr >> 20 << 2))) [0 , 4 .e. 0x3C])) 6 proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; is_aligned pd pdBits; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (pd + (vptr >> 20 << 2)) 6 proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 20 << 2) 6
 2. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> 6 \<le> pdBits proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 20) 4
 2. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> 6 \<le> pdBits proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned vptr (4 + 20)
 2. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> 6 \<le> pdBits proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = Wellformed_C.ARMSuperSection; \<forall>y<0x1000. pde_at' (pd + (y << 2)) s; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> 6 \<le> pdBits proof (prove)
goal:
No subgoals!