theory ArchFinalise_AI

lemma (* arch_finalise_cap_invs *)[wp,Finalise_AI_asms]:
  "\<lbrace>invs and valid_cap (ArchObjectCap cap)\<rbrace>
     arch_finalise_cap cap final
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: arch_finalise_cap_def) apply (rule hoare_pre) apply (wp unmap_page_invs | wpc)+ apply (clarsimp simp: valid_cap_def cap_aligned_def) apply (auto simp: mask_def vmsz_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap (ArchObjectCap cap)\<rbrace> arch_finalise_cap cap final \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap (ArchObjectCap cap)\<rbrace> case cap of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do delete_asid_pool b ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) | ASIDControlCap \<Rightarrow> return (NullCap, NullCap) | PageCap x ptr xa s None \<Rightarrow> return (NullCap, NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do unmap_page s a v ptr;
return (NullCap, NullCap)
od | PageTableCap ptr None \<Rightarrow> return (NullCap, NullCap) | PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do unmap_page_table a v ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) | PageDirectoryCap ptr None \<Rightarrow> return (NullCap, NullCap) | PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do delete_asid a ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case cap of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do delete_asid_pool b ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) | ASIDControlCap \<Rightarrow> return (NullCap, NullCap) | PageCap x ptr xa s None \<Rightarrow> return (NullCap, NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do unmap_page s a v ptr;
return (NullCap, NullCap)
od | PageTableCap ptr None \<Rightarrow> return (NullCap, NullCap) | PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do unmap_page_table a v ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) | PageDirectoryCap ptr None \<Rightarrow> return (NullCap, NullCap) | PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do delete_asid a ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>s. (invs and valid_cap (ArchObjectCap cap)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and valid_cap (ArchObjectCap cap)) s \<Longrightarrow> (\<forall>x xa. cap = ASIDPoolCap x xa \<longrightarrow> (final = True \<longrightarrow> (invs and K (xa \<le> mask local.asid_bits)) s) \<and> (final = False \<longrightarrow> invs s)) \<and> (cap = ASIDControlCap \<longrightarrow> invs s) \<and> (\<forall>x xa xb xc xd. cap = PageCap x xa xb xc xd \<longrightarrow> (xd = None \<longrightarrow> invs s) \<and> (\<forall>x. xd = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> (invs and K (xa \<le> mask local.asid_bits \<and> xb < kernel_base \<and> vmsz_aligned xb xc)) s))) \<and> (\<forall>x xa. cap = PageTableCap x xa \<longrightarrow> (xa = None \<longrightarrow> invs s) \<and> (\<forall>x. xa = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> (final = True \<longrightarrow> (invs and K (xa \<le> mask local.asid_bits \<and> xb < kernel_base \<and> vmsz_aligned xb ARMSection)) s) \<and> (final = False \<longrightarrow> invs s)))) \<and> (\<forall>x xa. cap = PageDirectoryCap x xa \<longrightarrow> (xa = None \<longrightarrow> invs s) \<and> (\<forall>x. xa = Some x \<longrightarrow> (final = True \<longrightarrow> (invs and K (x \<le> mask local.asid_bits)) s) \<and> (final = False \<longrightarrow> invs s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; is_aligned (the (aobj_ref cap)) (arch_obj_size cap); arch_obj_size cap < word_bits; case 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)\<rbrakk> \<Longrightarrow> (\<forall>x xa. cap = ASIDPoolCap x xa \<longrightarrow> final \<longrightarrow> xa \<le> mask local.asid_bits) \<and> (\<forall>x xa xb xc xd. cap = PageCap x xa xb xc xd \<longrightarrow> (\<forall>a b. xd = Some (a, b) \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b xc)) \<and> (\<forall>x xa. cap = PageTableCap x xa \<longrightarrow> (\<forall>a b. xa = Some (a, b) \<longrightarrow> final \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b ARMSection)) \<and> (\<forall>x xa. cap = PageDirectoryCap x xa \<longrightarrow> (\<forall>x. xa = Some x \<longrightarrow> final \<longrightarrow> x \<le> mask local.asid_bits)) proof (prove)
goal:
No subgoals!