theory ArchFinalise_AC

lemma arch_finalise_cap_respects[Finalise_AC_assms, wp]:
  "\<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap (ArchObjectCap cap)
                       and K (pas_cap_cur_auth aag (ArchObjectCap cap))\<rbrace>
   arch_finalise_cap cap final
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: arch_finalise_cap_def) apply (wpsimp wp: unmap_page_respects unmap_page_table_respects delete_asid_respects) apply (auto simp: cap_auth_conferred_def arch_cap_auth_conferred_def is_page_cap_def
                    aag_cap_auth_def pas_refined_all_auth_is_owns valid_cap_simps
                    cap_links_asid_slot_def label_owns_asid_slot_def
             intro: pas_refined_Control_into_is_subject_asid) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap (ArchObjectCap cap) and K (pas_cap_cur_auth aag (ArchObjectCap cap))\<rbrace> arch_finalise_cap cap final \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and invs and pas_refined aag and valid_cap (ArchObjectCap cap) and (\<lambda>y. pas_cap_cur_auth aag (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>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; invs s; pas_refined aag s; s \<turnstile> ArchObjectCap cap; pas_cap_cur_auth aag (ArchObjectCap cap)\<rbrakk> \<Longrightarrow> (\<forall>x xa. cap = ASIDPoolCap x xa \<longrightarrow> final \<longrightarrow> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of xa \<longrightarrow> is_subject_asid aag asid')) \<and> (\<forall>x xa xb xc xd. cap = PageCap x xa xb xc xd \<longrightarrow> (\<forall>a b. xd = Some (a, b) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> is_subject_asid aag a \<and> vmsz_aligned b xc \<and> b < kernel_base)) \<and> (\<forall>x xa. cap = PageTableCap x xa \<longrightarrow> (\<forall>a b. xa = Some (a, b) \<longrightarrow> final \<longrightarrow> is_subject_asid aag a \<and> b < kernel_base)) \<and> (\<forall>x xa. cap = PageDirectoryCap x xa \<longrightarrow> (\<exists>x. xa = Some x) \<longrightarrow> final \<longrightarrow> is_subject aag x) proof (prove)
goal:
No subgoals!