theory ArchCSpace_AI

lemma mask_cap_valid[simp, CSpace_AI_assms]:
  "s \<turnstile> c \<Longrightarrow> s \<turnstile> mask_cap R c" apply (cases c, simp_all add: valid_cap_def mask_cap_def
                             cap_rights_update_def
                             cap_aligned_def
                             acap_rights_update_def split:bool.splits) using valid_validate_vm_rights[simplified valid_vm_rights_def] apply (rename_tac arch_cap) by (case_tac arch_cap, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> c \<Longrightarrow> s \<turnstile> mask_cap R c proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>is_aligned (the (aobj_ref x12)) (arch_obj_size x12) \<and> arch_obj_size x12 < word_bits \<and> (case x12 of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | PageDirectoryCap r mapdata \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)); c = ArchObjectCap x12\<rbrakk> \<Longrightarrow> is_aligned (the (aobj_ref (case x12 of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights x12 \<inter> R)) xa xb | _ \<Rightarrow> x12))) (arch_obj_size (case x12 of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights x12 \<inter> R)) xa xb | _ \<Rightarrow> x12)) \<and> arch_obj_size (case x12 of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights x12 \<inter> R)) xa xb | _ \<Rightarrow> x12) < word_bits \<and> (case case x12 of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights x12 \<inter> R)) xa xb | _ \<Rightarrow> x12 of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | PageDirectoryCap r mapdata \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)) proof (prove)
using this:
validate_vm_rights ?rs \<in> {vm_read_write, vm_read_only, vm_kernel_only}

goal (1 subgoal):
 1. \<And>x12. \<lbrakk>is_aligned (the (aobj_ref x12)) (arch_obj_size x12) \<and> arch_obj_size x12 < word_bits \<and> (case x12 of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | PageDirectoryCap r mapdata \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)); c = ArchObjectCap x12\<rbrakk> \<Longrightarrow> is_aligned (the (aobj_ref (case x12 of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights x12 \<inter> R)) xa xb | _ \<Rightarrow> x12))) (arch_obj_size (case x12 of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights x12 \<inter> R)) xa xb | _ \<Rightarrow> x12)) \<and> arch_obj_size (case x12 of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights x12 \<inter> R)) xa xb | _ \<Rightarrow> x12) < word_bits \<and> (case case x12 of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights x12 \<inter> R)) xa xb | _ \<Rightarrow> x12 of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | PageDirectoryCap r mapdata \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)) proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. \<lbrakk>is_aligned (the (aobj_ref arch_cap)) (arch_obj_size arch_cap) \<and> arch_obj_size arch_cap < word_bits \<and> (case arch_cap of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | PageDirectoryCap r mapdata \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)); c = ArchObjectCap arch_cap; \<And>rs. validate_vm_rights rs \<in> {vm_read_write, vm_read_only, vm_kernel_only}\<rbrakk> \<Longrightarrow> is_aligned (the (aobj_ref (case arch_cap of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights arch_cap \<inter> R)) xa xb | _ \<Rightarrow> arch_cap))) (arch_obj_size (case arch_cap of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights arch_cap \<inter> R)) xa xb | _ \<Rightarrow> arch_cap)) \<and> arch_obj_size (case arch_cap of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights arch_cap \<inter> R)) xa xb | _ \<Rightarrow> arch_cap) < word_bits \<and> (case case arch_cap of PageCap dev x rs' xa xb \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights arch_cap \<inter> R)) xa xb | _ \<Rightarrow> arch_cap of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | PageDirectoryCap r mapdata \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1))