theory Arch_R

lemma createMappingEntries_valid_pde_slots':
  "\<lbrace>K (vmsz_aligned' vptr sz \<and> is_aligned pd pdBits
                \<and> vptr < pptrBase)\<rbrace>
     createMappingEntries base vptr sz vm_rights attrib pd
   \<lbrace>\<lambda>rv s. valid_pde_slots' rv\<rbrace>,-" apply (simp add: createMappingEntries_def valid_pde_slots'_def) apply (cases sz, simp_all) apply (wp | simp)+ apply (clarsimp simp: lookup_pd_slot_def Let_def mask_add_aligned) apply (erule less_pptrBase_valid_pde_offset'') apply (rule hoare_pre, wp) apply (clarsimp simp: vmsz_aligned'_def superSectionPDEOffsets_def pdeBits_def del: ballI) apply (subst p_0x3C_shift[symmetric]) apply (simp add: lookup_pd_slot_def Let_def) apply (erule aligned_add_aligned) apply (rule is_aligned_shiftl, rule is_aligned_shiftr) apply simp apply (simp add: pdBits_def pageBits_def word_bits_def) apply (simp add: pdBits_def pageBits_def) apply (clarsimp simp: upto_enum_step_def linorder_not_less pd_bits_def
                        lookup_pd_slot_def Let_def field_simps
                        mask_add_aligned pdeBits_def take_bit_Suc) apply (erule less_pptrBase_valid_pde_offset'
    [unfolded pdBits_def pageBits_def pdeBits_def, simplified], simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (vmsz_aligned' vptr sz \<and> is_aligned pd pdBits \<and> vptr < pptrBase)\<rbrace> createMappingEntries base vptr sz vm_rights attrib pd \<lbrace>\<lambda>rv s. valid_pde_slots' rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. vmsz_aligned' vptr sz \<and> is_aligned pd pdBits \<and> vptr < pptrBase\<rbrace> case sz of ARMSmallPage \<Rightarrow> doE p <- lookupErrorOnFailure False $ lookupPTSlot pd vptr;
returnOk $ Inl (ARM_H.SmallPagePTE base (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, [p])
odE | 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 | 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 | 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. case rv of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. sz = ARMSmallPage \<Longrightarrow> \<lbrace>\<lambda>y. vmsz_aligned' vptr ARMSmallPage \<and> is_aligned pd pdBits \<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. case rv of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde\<rbrace>, -
 2. sz = ARMLargePage \<Longrightarrow> \<lbrace>\<lambda>y. vmsz_aligned' vptr ARMLargePage \<and> is_aligned pd pdBits \<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. case rv of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde\<rbrace>, -
 3. sz = ARMSection \<Longrightarrow> \<lbrace>\<lambda>y. vmsz_aligned' vptr ARMSection \<and> is_aligned pd pdBits \<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. case rv of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde\<rbrace>, -
 4. sz = ARMSuperSection \<Longrightarrow> \<lbrace>\<lambda>y. vmsz_aligned' vptr ARMSuperSection \<and> is_aligned pd pdBits \<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. case rv of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz = ARMSection; vmsz_aligned' vptr ARMSection \<and> is_aligned pd pdBits \<and> vptr < pptrBase\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' (lookup_pd_slot pd vptr && mask pdBits)
 2. sz = ARMSuperSection \<Longrightarrow> \<lbrace>\<lambda>y. vmsz_aligned' vptr ARMSuperSection \<and> is_aligned pd pdBits \<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. case rv of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz = ARMSection; vmsz_aligned' vptr ARMSection; is_aligned pd pdBits; vptr < pptrBase\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' ((vptr >> 20 << 2) && mask pdBits)
 2. sz = ARMSuperSection \<Longrightarrow> \<lbrace>\<lambda>y. vmsz_aligned' vptr ARMSuperSection \<and> is_aligned pd pdBits \<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. case rv of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. sz = ARMSuperSection \<Longrightarrow> \<lbrace>\<lambda>y. vmsz_aligned' vptr ARMSuperSection \<and> is_aligned pd pdBits \<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. case rv of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; vmsz_aligned' vptr ARMSuperSection \<and> is_aligned pd pdBits \<and> vptr < pptrBase\<rbrakk> \<Longrightarrow> case Inr (ARM_H.SuperSectionPDE base (armParityEnabled attrib) (armPageCacheable attrib) False (armExecuteNever attrib) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDEOffsets) of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; is_aligned pd pdBits; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [0 , 4 .e. 0x3C]. valid_pde_mapping_offset' (x + lookup_pd_slot pd vptr && mask pdBits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; is_aligned pd pdBits; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot pd vptr) 6
 2. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; is_aligned pd pdBits; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>p\<in>set [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + 0x3C]. valid_pde_mapping_offset' (p && mask pdBits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; is_aligned pd pdBits; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (pd + (vptr >> 20 << 2)) 6
 2. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; is_aligned pd pdBits; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>p\<in>set [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + 0x3C]. valid_pde_mapping_offset' (p && mask pdBits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 20 << 2) 6
 2. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> 6 \<le> pdBits
 3. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; is_aligned pd pdBits; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>p\<in>set [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + 0x3C]. valid_pde_mapping_offset' (p && mask pdBits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> is_aligned vptr (6 - 2 + 20)
 2. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> 6 \<le> pdBits
 3. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; is_aligned pd pdBits; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>p\<in>set [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + 0x3C]. valid_pde_mapping_offset' (p && mask pdBits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; vptr < pptrBase\<rbrakk> \<Longrightarrow> 6 \<le> pdBits
 2. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; is_aligned pd pdBits; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>p\<in>set [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + 0x3C]. valid_pde_mapping_offset' (p && mask pdBits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; is_aligned pd pdBits; vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>p\<in>set [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + 0x3C]. valid_pde_mapping_offset' (p && mask pdBits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; is_aligned pd (12 + pdeBits); vptr < pptrBase\<rbrakk> \<Longrightarrow> \<forall>p\<in>set [lookup_pd_slot pd vptr , lookup_pd_slot pd vptr + 4 .e. lookup_pd_slot pd vptr + 0x3C]. valid_pde_mapping_offset' (p && mask (12 + pdeBits)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>sz = ARMSuperSection; is_aligned vptr 24; is_aligned pd 14; vptr < pptrBase; pd + (vptr >> 20 << 2) \<le> pd + (0x3C + (vptr >> 20 << 2)); p \<le> 0xF\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' (p * 4 + (vptr >> 20 << 2) && mask 14) proof (prove)
goal:
No subgoals!