theory Arch_R

lemma createMappingEntires_valid_slots_duplicated'[wp]:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s
   \<and>  page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits\<rbrace>
  createMappingEntries base vptr vmsz vmrights attrib pd
  \<lbrace>\<lambda>rv s. slots_duplicated_ensured rv s\<rbrace>, -" apply (clarsimp simp:createMappingEntries_def) apply (rule hoare_pre) apply (wpc | wp lookupPTSlot_page_table_at'
     | simp add: slots_duplicated_ensured_def)+ apply (rule_tac Q' = "\<lambda>p s.  is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s"
       in  hoare_post_imp_R) apply (wp lookupPTSlot_aligned lookupPTSlot_page_table_at') apply (rename_tac rv s) apply (rule_tac x = rv in exI) apply (clarsimp simp: largePagePTEOffsets_def pteBits_def) apply (frule is_aligned_no_wrap'[where off = "0x3c"]) apply simp apply (drule upto_enum_step_shift[where n = 6 and m = 2,simplified]) apply (clarsimp simp: mask_def add.commute upto_enum_step_def take_bit_Suc) apply simp apply wp+ apply (intro conjI impI) apply ((clarsimp simp: vmsz_aligned_def pageBitsForSize_def
              slots_duplicated_ensured_def
              split:vmpage_size.splits)+)[8] apply clarsimp apply (drule lookup_pd_slot_aligned_6) apply (simp add:pdBits_def pageBits_def pdeBits_def) apply (clarsimp simp:slots_duplicated_ensured_def) apply (rule_tac x = "(lookup_pd_slot pd vptr)" in exI) apply clarsimp apply (frule is_aligned_no_wrap'[where off = "0x3c" and sz = 6]) apply simp apply (drule upto_enum_step_shift[where n = 6 and m = 2,simplified]) apply (clarsimp simp: mask_def add.commute upto_enum_step_def take_bit_Suc
                         superSectionPDEOffsets_def pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits\<rbrace> createMappingEntries base vptr vmsz vmrights attrib pd \<lbrace>slots_duplicated_ensured\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits\<rbrace> case vmsz of ARMSmallPage \<Rightarrow> doE p <- lookupErrorOnFailure False $ lookupPTSlot pd vptr;
returnOk $ Inl (ARM_H.SmallPagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE | ARMLargePage \<Rightarrow> doE p <- lookupErrorOnFailure False $ lookupPTSlot pd vptr;
returnOk $ Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) largePagePTEOffsets)
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case vmsz of ARMSmallPage \<Rightarrow> doE p <- lookupErrorOnFailure False $ lookupPTSlot pd vptr;
returnOk $ Inl (ARM_H.SmallPagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE | ARMLargePage \<Rightarrow> doE p <- lookupErrorOnFailure False $ lookupPTSlot pd vptr;
returnOk $ Inl (ARM_H.LargePagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) largePagePTEOffsets)
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 2. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. vmsz = ARMLargePage \<Longrightarrow> \<lbrace>?P'33\<rbrace> lookupPTSlot pd vptr \<lbrace>\<lambda>p a. \<exists>pa. map (\<lambda>x. x + p) largePagePTEOffsets = [pa , pa + 4 .e. pa + mask 6] \<and> is_aligned pa 6 \<and> page_table_at' (pa && ~~ mask ptBits) a\<rbrace>, -
 2. vmsz = ARMSection \<Longrightarrow> \<lbrace>?R10\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 3. vmsz = ARMSuperSection \<Longrightarrow> \<lbrace>?R9\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> ?P'33 s) \<and> (vmsz = ARMSection \<longrightarrow> ?R10 s) \<and> (vmsz = ARMSuperSection \<longrightarrow> ?R9 s) proof (prove)
goal (5 subgoals):
 1. vmsz = ARMLargePage \<Longrightarrow> \<lbrace>?P'33\<rbrace> lookupPTSlot pd vptr \<lbrace>\<lambda>p s. is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace>, -
 2. \<And>rv s. \<lbrakk>vmsz = ARMLargePage; is_aligned rv 6 \<and> page_table_at' (rv && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<exists>p. map (\<lambda>x. x + rv) largePagePTEOffsets = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s
 3. vmsz = ARMSection \<Longrightarrow> \<lbrace>?R10\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 4. vmsz = ARMSuperSection \<Longrightarrow> \<lbrace>?R9\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 5. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> ?P'33 s) \<and> (vmsz = ARMSection \<longrightarrow> ?R10 s) \<and> (vmsz = ARMSuperSection \<longrightarrow> ?R9 s) proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>vmsz = ARMLargePage; is_aligned rv 6 \<and> page_table_at' (rv && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<exists>p. map (\<lambda>x. x + rv) largePagePTEOffsets = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s
 2. vmsz = ARMSection \<Longrightarrow> \<lbrace>?R10\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 3. vmsz = ARMSuperSection \<Longrightarrow> \<lbrace>?R9\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> (is_aligned vptr 16 \<and> valid_objs' s) \<and> valid_objs' s) \<and> (vmsz = ARMSection \<longrightarrow> ?R10 s) \<and> (vmsz = ARMSuperSection \<longrightarrow> ?R9 s) proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>vmsz = ARMLargePage; is_aligned rv 6 \<and> page_table_at' (rv && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<exists>p. map (\<lambda>x. x + rv) largePagePTEOffsets = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s
 2. vmsz = ARMSection \<Longrightarrow> \<lbrace>?R10\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 3. vmsz = ARMSuperSection \<Longrightarrow> \<lbrace>?R9\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> (is_aligned vptr 16 \<and> valid_objs' s) \<and> valid_objs' s) \<and> (vmsz = ARMSection \<longrightarrow> ?R10 s) \<and> (vmsz = ARMSuperSection \<longrightarrow> ?R9 s) proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>vmsz = ARMLargePage; is_aligned rv 6 \<and> page_table_at' (rv && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + rv) largePagePTEOffsets = [rv , rv + 4 .e. rv + mask 6] \<and> is_aligned rv 6 \<and> page_table_at' (rv && ~~ mask ptBits) s
 2. vmsz = ARMSection \<Longrightarrow> \<lbrace>?R10\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 3. vmsz = ARMSuperSection \<Longrightarrow> \<lbrace>?R9\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> (is_aligned vptr 16 \<and> valid_objs' s) \<and> valid_objs' s) \<and> (vmsz = ARMSection \<longrightarrow> ?R10 s) \<and> (vmsz = ARMSuperSection \<longrightarrow> ?R9 s) proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>vmsz = ARMLargePage; is_aligned rv 6; page_table_at' (rv && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + rv) [0 , 4 .e. 0x3C] = [rv , rv + 4 .e. rv + mask 6]
 2. vmsz = ARMSection \<Longrightarrow> \<lbrace>?R10\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 3. vmsz = ARMSuperSection \<Longrightarrow> \<lbrace>?R9\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> (is_aligned vptr 16 \<and> valid_objs' s) \<and> valid_objs' s) \<and> (vmsz = ARMSection \<longrightarrow> ?R10 s) \<and> (vmsz = ARMSuperSection \<longrightarrow> ?R9 s) proof (prove)
goal (5 subgoals):
 1. \<And>rv s. \<lbrakk>vmsz = ARMLargePage; is_aligned rv 6; page_table_at' (rv && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> 0x3C < 2 ^ 6
 2. \<And>rv s. \<lbrakk>vmsz = ARMLargePage; is_aligned rv 6; page_table_at' (rv && ~~ mask ptBits) s; rv \<le> rv + 0x3C\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + rv) [0 , 4 .e. 0x3C] = [rv , rv + 4 .e. rv + mask 6]
 3. vmsz = ARMSection \<Longrightarrow> \<lbrace>?R10\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 4. vmsz = ARMSuperSection \<Longrightarrow> \<lbrace>?R9\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 5. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> (is_aligned vptr 16 \<and> valid_objs' s) \<and> valid_objs' s) \<and> (vmsz = ARMSection \<longrightarrow> ?R10 s) \<and> (vmsz = ARMSuperSection \<longrightarrow> ?R9 s) proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>vmsz = ARMLargePage; is_aligned rv 6; page_table_at' (rv && ~~ mask ptBits) s; rv \<le> rv + 0x3C\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + rv) [0 , 4 .e. 0x3C] = [rv , rv + 4 .e. rv + mask 6]
 2. vmsz = ARMSection \<Longrightarrow> \<lbrace>?R10\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 3. vmsz = ARMSuperSection \<Longrightarrow> \<lbrace>?R9\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> (is_aligned vptr 16 \<and> valid_objs' s) \<and> valid_objs' s) \<and> (vmsz = ARMSection \<longrightarrow> ?R10 s) \<and> (vmsz = ARMSuperSection \<longrightarrow> ?R9 s) proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>vmsz = ARMLargePage; page_table_at' (rv && ~~ mask ptBits) s; rv \<le> rv + 0x3C; [rv , rv + 4 .e. 0x3F + rv] = map ((+) rv) [0 , 4 .e. 0x3F]\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + rv) [0 , 4 .e. 0x3C] = [rv , rv + 4 .e. rv + mask 6]
 2. vmsz = ARMSection \<Longrightarrow> \<lbrace>?R10\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 3. vmsz = ARMSuperSection \<Longrightarrow> \<lbrace>?R9\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> (is_aligned vptr 16 \<and> valid_objs' s) \<and> valid_objs' s) \<and> (vmsz = ARMSection \<longrightarrow> ?R10 s) \<and> (vmsz = ARMSuperSection \<longrightarrow> ?R9 s) proof (prove)
goal (3 subgoals):
 1. vmsz = ARMSection \<Longrightarrow> \<lbrace>?R10\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [p])
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 2. vmsz = ARMSuperSection \<Longrightarrow> \<lbrace>?R9\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 3. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> (is_aligned vptr 16 \<and> valid_objs' s) \<and> valid_objs' s) \<and> (vmsz = ARMSection \<longrightarrow> ?R10 s) \<and> (vmsz = ARMSuperSection \<longrightarrow> ?R9 s) proof (prove)
goal (3 subgoals):
 1. vmsz = ARMSection \<Longrightarrow> \<lbrace>?R10\<rbrace> returnOk (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [lookup_pd_slot pd vptr])) \<lbrace>slots_duplicated_ensured\<rbrace>, -
 2. vmsz = ARMSuperSection \<Longrightarrow> \<lbrace>?R9\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
returnOk $ Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + p) superSectionPDEOffsets)
odE \<lbrace>slots_duplicated_ensured\<rbrace>, -
 3. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> (is_aligned vptr 16 \<and> valid_objs' s) \<and> valid_objs' s) \<and> (vmsz = ARMSection \<longrightarrow> ?R10 s) \<and> (vmsz = ARMSuperSection \<longrightarrow> ?R9 s) proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits \<Longrightarrow> (vmsz = ARMSmallPage \<longrightarrow> True \<and> valid_objs' s) \<and> (vmsz = ARMLargePage \<longrightarrow> True \<and> (is_aligned vptr 16 \<and> valid_objs' s) \<and> valid_objs' s) \<and> (vmsz = ARMSection \<longrightarrow> slots_duplicated_ensured (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [lookup_pd_slot pd vptr])) s) \<and> (vmsz = ARMSuperSection \<longrightarrow> True \<and> slots_duplicated_ensured (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + lookupPDSlot pd vptr) superSectionPDEOffsets)) s) proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits; vmsz = ARMSmallPage\<rbrakk> \<Longrightarrow> True
 2. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits; vmsz = ARMSmallPage\<rbrakk> \<Longrightarrow> valid_objs' s
 3. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits; vmsz = ARMLargePage\<rbrakk> \<Longrightarrow> True
 4. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits; vmsz = ARMLargePage\<rbrakk> \<Longrightarrow> is_aligned vptr 16
 5. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits; vmsz = ARMLargePage\<rbrakk> \<Longrightarrow> valid_objs' s
 6. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits; vmsz = ARMLargePage\<rbrakk> \<Longrightarrow> valid_objs' s
 7. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits; vmsz = ARMSection\<rbrakk> \<Longrightarrow> slots_duplicated_ensured (Inr (ARM_H.SectionPDE base (armParityEnabled attrib) 0 (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, [lookup_pd_slot pd vptr])) s
 8. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits; vmsz = ARMSuperSection\<rbrakk> \<Longrightarrow> True
 9. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits; vmsz = ARMSuperSection\<rbrakk> \<Longrightarrow> slots_duplicated_ensured (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + lookupPDSlot pd vptr) superSectionPDEOffsets)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned vptr vmsz \<and> valid_objs' s \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned pd pdBits; vmsz = ARMSuperSection\<rbrakk> \<Longrightarrow> slots_duplicated_ensured (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + lookupPDSlot pd vptr) superSectionPDEOffsets)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz = ARMSuperSection; vs_valid_duplicates' (ksPSpace s); vmsz_aligned vptr ARMSuperSection; valid_objs' s; page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> slots_duplicated_ensured (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vmsz = ARMSuperSection; vs_valid_duplicates' (ksPSpace s); valid_objs' s; page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s; is_aligned pd pdBits\<rbrakk> \<Longrightarrow> is_aligned (?pd82 s) 14
 2. \<And>s. \<lbrakk>vmsz = ARMSuperSection; vs_valid_duplicates' (ksPSpace s); valid_objs' s; page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s; is_aligned pd pdBits; is_aligned (lookup_pd_slot (?pd82 s) vptr) 6\<rbrakk> \<Longrightarrow> slots_duplicated_ensured (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz = ARMSuperSection; vs_valid_duplicates' (ksPSpace s); valid_objs' s; page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s; is_aligned pd pdBits; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> slots_duplicated_ensured (Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vmrights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz = ARMSuperSection; vs_valid_duplicates' (ksPSpace s); valid_objs' s; page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s; is_aligned pd pdBits; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> \<exists>p. map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s \<and> is_aligned p 6 proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz = ARMSuperSection; vs_valid_duplicates' (ksPSpace s); valid_objs' s; page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s; is_aligned pd pdBits; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets = [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + mask 6] \<and> is_aligned (lookup_pd_slot pd vptr) 6 \<and> page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s \<and> is_aligned (lookup_pd_slot pd vptr) 6 proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz = ARMSuperSection; vs_valid_duplicates' (ksPSpace s); valid_objs' s; page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s; is_aligned pd pdBits; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets = [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + mask 6] proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vmsz = ARMSuperSection; vs_valid_duplicates' (ksPSpace s); valid_objs' s; page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s; is_aligned pd pdBits; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> 0x3C < 2 ^ 6
 2. \<And>s. \<lbrakk>vmsz = ARMSuperSection; vs_valid_duplicates' (ksPSpace s); valid_objs' s; page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s; is_aligned pd pdBits; is_aligned (lookup_pd_slot pd vptr) 6; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets = [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + mask 6] proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz = ARMSuperSection; vs_valid_duplicates' (ksPSpace s); valid_objs' s; page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s; is_aligned pd pdBits; is_aligned (lookup_pd_slot pd vptr) 6; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets = [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + mask 6] proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz = ARMSuperSection; vs_valid_duplicates' (ksPSpace s); valid_objs' s; page_directory_at' (lookup_pd_slot pd vptr && ~~ mask pdBits) s; is_aligned pd pdBits; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C; [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. 0x3F + lookup_pd_slot pd vptr] = map ((+) (lookup_pd_slot pd vptr)) [0 , 4 .e. 0x3F]\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets = [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + mask 6] proof (prove)
goal:
No subgoals!