theory ArchAcc_R

lemma arch_deriveCap_corres [corres]:
 "cap_relation (cap.ArchObjectCap c) (ArchObjectCap c') \<Longrightarrow>
  corres (ser \<oplus> (\<lambda>c c'. cap_relation c c'))
         \<top> \<top>
         (arch_derive_cap c)
         (Arch.deriveCap slot c')" unfolding arch_derive_cap_def ARM_H.deriveCap_def Let_def apply (cases c, simp_all add: isCap_simps split: option.splits split del: if_split) apply (clarify?, rule corres_noopE; wpsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation (cap.ArchObjectCap c) (capability.ArchObjectCap c') \<Longrightarrow> corres (ser \<oplus> cap_relation) (\<lambda>_. True) (\<lambda>_. True) (arch_derive_cap c) (Arch.deriveCap slot c') proof (prove)
goal (1 subgoal):
 1. cap_relation (cap.ArchObjectCap c) (capability.ArchObjectCap c') \<Longrightarrow> corres (ser \<oplus> cap_relation) (\<lambda>_. True) (\<lambda>_. True) (case c of arch_cap.PageCap dev r R pgs x \<Rightarrow> returnOk (cap.ArchObjectCap (arch_cap.PageCap dev r R pgs None)) | arch_cap.PageTableCap xa None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | arch_cap.PageTableCap xa (Some x) \<Rightarrow> returnOk (cap.ArchObjectCap c) | arch_cap.PageDirectoryCap xa None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | arch_cap.PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (cap.ArchObjectCap c) | _ \<Rightarrow> returnOk (cap.ArchObjectCap c)) (if isPageTableCap c' \<and> capPTMappedAddress c' \<noteq> None then returnOk $ capability.ArchObjectCap c' else if isPageTableCap c' \<and> capPTMappedAddress c' = None then throw Fault_H.syscall_error.IllegalOperation else if isPageDirectoryCap c' \<and> capPDMappedASID c' \<noteq> None then returnOk $ capability.ArchObjectCap c' else if isPageDirectoryCap c' \<and> capPDMappedASID c' = None then throw Fault_H.syscall_error.IllegalOperation else if isPageCap c' then returnOk $ capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) c' else if isASIDControlCap c' then returnOk $ capability.ArchObjectCap c' else if isASIDPoolCap c' then returnOk $ capability.ArchObjectCap c' else undefined) proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>c' = arch_capability.ASIDPoolCap x11 x12; c = arch_cap.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (cap.ArchObjectCap (arch_cap.ASIDPoolCap x11 x12))) (returnOk (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12)))
 2. \<lbrakk>c' = arch_capability.ASIDControlCap; c = arch_cap.ASIDControlCap\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (cap.ArchObjectCap arch_cap.ASIDControlCap)) (returnOk (capability.ArchObjectCap arch_capability.ASIDControlCap))
 3. \<And>x31 x32 x33 x34 x35. \<lbrakk>c' = arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35; c = arch_cap.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> corres (ser \<oplus> cap_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 None))) (returnOk (capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 None)))
 4. \<And>x41 x42. \<lbrakk>c' = arch_capability.PageTableCap x41 x42; c = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>a b. x42 = Some (a, b) \<longrightarrow> corres (ser \<oplus> cap_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (cap.ArchObjectCap (arch_cap.PageTableCap x41 (Some (a, b))))) (returnOk (capability.ArchObjectCap (arch_capability.PageTableCap x41 (Some (a, b)))))
 5. \<And>x51 x52. \<lbrakk>c' = arch_capability.PageDirectoryCap x51 x52; c = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>x2. x52 = Some x2 \<longrightarrow> corres (ser \<oplus> cap_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 (Some x2)))) (returnOk (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 (Some x2)))) proof (prove)
goal:
No subgoals!