theory ArchAcc_R

lemma createMappingEntries_corres [corres]:
  "\<lbrakk> vm_rights' = vmrights_map vm_rights;
     attrib' = vmattributes_map attrib; base = base'; vptr = vptr'; pgsz = pgsz'; pd = pd' \<rbrakk>
  \<Longrightarrow> corres (ser \<oplus> mapping_map)
          (\<lambda>s. (pgsz = ARMSmallPage \<or> pgsz = ARMLargePage \<longrightarrow> pde_at (lookup_pd_slot pd vptr) s)
           \<and> (is_aligned pd pd_bits \<and> vmsz_aligned vptr pgsz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)
           \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)
          (pspace_aligned' and pspace_distinct')
          (create_mapping_entries base vptr pgsz vm_rights attrib pd)
          (createMappingEntries base' vptr' pgsz' vm_rights' attrib' pd')" unfolding createMappingEntries_def mapping_map_def by (cases pgsz; corresKsimp simp: vmattributes_map_def less_kernel_base_mapping_slots
                                   largePagePTEOffsets_def
                                   largePagePTE_offsets_def
                                   superSectionPDEOffsets_def
                                   superSectionPDE_offsets_def
                                   pteBits_def pdeBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vm_rights' = vmrights_map vm_rights; attrib' = vmattributes_map attrib; base = base'; vptr = vptr'; pgsz = pgsz'; pd = pd'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> mapping_map) (\<lambda>s. (pgsz = ARMSmallPage \<or> pgsz = ARMLargePage \<longrightarrow> pde_at (lookup_pd_slot pd vptr) s) \<and> (is_aligned pd pd_bits \<and> vmsz_aligned vptr pgsz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)) (pspace_aligned' and pspace_distinct') (create_mapping_entries base vptr pgsz vm_rights attrib pd) (createMappingEntries base' vptr' pgsz' vm_rights' attrib' pd') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vm_rights' = vmrights_map vm_rights; attrib' = vmattributes_map attrib; base = base'; vptr = vptr'; pgsz = pgsz'; pd = pd'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (pte_relation' \<otimes> (=) \<oplus> pde_relation' \<otimes> (=))) (\<lambda>s. (pgsz = ARMSmallPage \<or> pgsz = ARMLargePage \<longrightarrow> pde_at (lookup_pd_slot pd vptr) s) \<and> (is_aligned pd pd_bits \<and> vmsz_aligned vptr pgsz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)) (pspace_aligned' and pspace_distinct') (create_mapping_entries base vptr pgsz vm_rights attrib pd) (case pgsz' 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)