theory ArchInvariants_AI

lemma valid_arch_cap_typ:
  assumes P: "\<And>T p. \<lbrace>\<lambda>s. (typ_at (AArch T) p s )\<rbrace> f \<lbrace>\<lambda>rv s. (typ_at (AArch T) p s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. valid_arch_cap c s\<rbrace> f \<lbrace>\<lambda>rv s. valid_arch_cap c s\<rbrace>" unfolding valid_arch_cap_def apply (case_tac c; simp) apply (wp P hoare_vcg_ball_lift hoare_vcg_imp_lift hoare_vcg_conj_lift | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_cap c\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_cap c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case c 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)\<rbrace> f \<lbrace>\<lambda>rv s. case c 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)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. c = ASIDPoolCap x11 x12 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (AArch AASIDPool) x11 s \<and> is_aligned x12 local.asid_low_bits \<and> x12 \<le> 2 ^ local.asid_bits - 1\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (AArch AASIDPool) x11 s \<and> is_aligned x12 local.asid_low_bits \<and> x12 \<le> 2 ^ local.asid_bits - 1\<rbrace>
 2. c = ASIDControlCap \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>rv s. True\<rbrace>
 3. \<And>x31 x32 x33 x34 x35. c = PageCap x31 x32 x33 x34 x35 \<Longrightarrow> \<lbrace>\<lambda>s. (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s \<and> x33 \<in> valid_vm_rights \<and> (case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref x34 \<and> ref < kernel_base)) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s \<and> x33 \<in> valid_vm_rights \<and> (case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref x34 \<and> ref < kernel_base))\<rbrace> f \<lbrace>\<lambda>rv s. (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s \<and> x33 \<in> valid_vm_rights \<and> (case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref x34 \<and> ref < kernel_base)) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s \<and> x33 \<in> valid_vm_rights \<and> (case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref x34 \<and> ref < kernel_base))\<rbrace>
 4. \<And>x41 x42. c = PageTableCap x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (AArch APageTable) x41 s \<and> (case x42 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))\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (AArch APageTable) x41 s \<and> (case x42 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))\<rbrace>
 5. \<And>x51 x52. c = PageDirectoryCap x51 x52 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (AArch APageDirectory) x51 s \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (AArch APageDirectory) x51 s \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)\<rbrace> proof (prove)
goal:
No subgoals!