theory ArchAcc_R

lemma arch_deriveCap_valid:
  "\<lbrace>valid_cap' (ArchObjectCap arch_cap)\<rbrace>
     Arch.deriveCap u arch_cap
   \<lbrace>\<lambda>rv. valid_cap' rv\<rbrace>,-" apply (simp      add: ARM_H.deriveCap_def
                  cong: if_cong
             split del: if_split) apply (rule hoare_pre, wp undefined_validE_R) apply (cases arch_cap, simp_all add: isCap_defs) apply (simp add: valid_cap'_def capAligned_def
                   capUntypedPtr_def ARM_H.capUntypedPtr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' (capability.ArchObjectCap arch_cap)\<rbrace> Arch.deriveCap u arch_cap \<lbrace>valid_cap'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' (capability.ArchObjectCap arch_cap)\<rbrace> if isPageTableCap arch_cap \<and> (\<exists>a b. capPTMappedAddress arch_cap = Some (a, b)) then returnOk (capability.ArchObjectCap arch_cap) else if isPageTableCap arch_cap \<and> capPTMappedAddress arch_cap = None then throwError Fault_H.syscall_error.IllegalOperation else if isPageDirectoryCap arch_cap \<and> (\<exists>y. capPDMappedASID arch_cap = Some y) then returnOk (capability.ArchObjectCap arch_cap) else if isPageDirectoryCap arch_cap \<and> capPDMappedASID arch_cap = None then throwError Fault_H.syscall_error.IllegalOperation else if isPageCap arch_cap then returnOk (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) arch_cap)) else if isASIDControlCap arch_cap then returnOk (capability.ArchObjectCap arch_cap) else if isASIDPoolCap arch_cap then returnOk (capability.ArchObjectCap arch_cap) else undefined \<lbrace>valid_cap'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_cap' (capability.ArchObjectCap arch_cap) s \<Longrightarrow> (isPageTableCap arch_cap \<and> (\<exists>a b. capPTMappedAddress arch_cap = Some (a, b)) \<longrightarrow> valid_cap' (capability.ArchObjectCap arch_cap) s) \<and> (\<not> (isPageTableCap arch_cap \<and> (\<exists>a b. capPTMappedAddress arch_cap = Some (a, b))) \<longrightarrow> (isPageTableCap arch_cap \<and> capPTMappedAddress arch_cap = None \<longrightarrow> True) \<and> (\<not> (isPageTableCap arch_cap \<and> capPTMappedAddress arch_cap = None) \<longrightarrow> (isPageDirectoryCap arch_cap \<and> (\<exists>y. capPDMappedASID arch_cap = Some y) \<longrightarrow> valid_cap' (capability.ArchObjectCap arch_cap) s) \<and> (\<not> (isPageDirectoryCap arch_cap \<and> (\<exists>y. capPDMappedASID arch_cap = Some y)) \<longrightarrow> (isPageDirectoryCap arch_cap \<and> capPDMappedASID arch_cap = None \<longrightarrow> True) \<and> (\<not> (isPageDirectoryCap arch_cap \<and> capPDMappedASID arch_cap = None) \<longrightarrow> (isPageCap arch_cap \<longrightarrow> valid_cap' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) arch_cap)) s) \<and> (\<not> isPageCap arch_cap \<longrightarrow> (isASIDControlCap arch_cap \<longrightarrow> valid_cap' (capability.ArchObjectCap arch_cap) s) \<and> (\<not> isASIDControlCap arch_cap \<longrightarrow> (isASIDPoolCap arch_cap \<longrightarrow> valid_cap' (capability.ArchObjectCap arch_cap) s) \<and> (\<not> isASIDPoolCap arch_cap \<longrightarrow> False))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s x31 x32 x33 x34 x35. \<lbrakk>valid_cap' (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) s; arch_cap = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> valid_cap' (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 None)) s proof (prove)
goal:
No subgoals!