theory ArchAcc_R

lemma createMappingEntries_valid_slots' [wp]:
  "\<lbrace>valid_objs' and
    K (vmsz_aligned' base sz \<and> vmsz_aligned' vptr sz \<and> ptrFromPAddr base \<noteq> 0) \<rbrace>
  createMappingEntries base vptr sz vm_rights attrib pd
  \<lbrace>\<lambda>m. valid_slots' m\<rbrace>, -" apply (simp add: createMappingEntries_def) apply (rule hoare_pre) apply (wp|wpc|simp add: valid_slots'_def valid_mapping'_def)+ apply (simp add: vmsz_aligned'_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and K (vmsz_aligned' base sz \<and> vmsz_aligned' vptr sz \<and> ptrFromPAddr base \<noteq> 0)\<rbrace> createMappingEntries base vptr sz vm_rights attrib pd \<lbrace>valid_slots'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and (\<lambda>y. vmsz_aligned' base sz \<and> vmsz_aligned' vptr sz \<and> ptrFromPAddr base \<noteq> 0)\<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>valid_slots'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<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>valid_slots'\<rbrace>, -
 2. \<And>s. (valid_objs' and (\<lambda>y. vmsz_aligned' base sz \<and> vmsz_aligned' vptr sz \<and> ptrFromPAddr base \<noteq> 0)) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> vmsz_aligned' base sz \<and> vmsz_aligned' vptr sz \<and> ptrFromPAddr base \<noteq> 0 \<Longrightarrow> (sz = ARMSmallPage \<longrightarrow> is_aligned base 12) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned base 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned base 20) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned base 24) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> is_aligned base (pageBitsForSize sz) \<and> is_aligned vptr (pageBitsForSize sz) \<and> ptrFromPAddr base \<noteq> 0 \<Longrightarrow> (sz = ARMSmallPage \<longrightarrow> is_aligned base 12) \<and> (sz = ARMLargePage \<longrightarrow> is_aligned base 16) \<and> (sz = ARMSection \<longrightarrow> is_aligned base 20) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned base 24) proof (prove)
goal:
No subgoals!