kings-crown/FVELER_Isabelle huggingface dataset:
theory FinalCaps

lemma is_derived_overlaps':
  "\<lbrakk> is_derived (cdt s) slot cap cap';
     (obj_refs cap' \<noteq> {} \<or> cap_irqs cap' \<noteq> {}) \<or>
     (obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}) \<rbrakk>
     \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<or>
         cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}" apply (simp add: is_derived_def) apply (case_tac cap', simp_all add: cap_master_cap_def split: cap.splits) apply (fastforce dest: master_arch_cap_obj_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_derived (cdt s) slot cap cap'; (obj_refs cap' \<noteq> {} \<or> cap_irqs cap' \<noteq> {}) \<or> obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<or> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap \<noteq> NullCap \<and> \<not> is_zombie cap' \<and> cap \<noteq> IRQControlCap \<and> (if is_untyped_cap cap' then cap_master_cap cap' = cap_master_cap cap \<and> descendants_of slot (cdt s) = {} else cap_master_cap cap' = cap_master_cap cap \<and> (cap_badge cap', cap_badge cap) \<in> capBadge_ordering False) \<and> is_master_reply_cap cap' = is_reply_cap cap \<and> is_derived_arch cap cap' \<and> \<not> is_reply_cap cap' \<and> \<not> is_master_reply_cap cap; obj_refs cap = {} \<longrightarrow> obj_refs cap' = {} \<longrightarrow> cap_irqs cap' = {} \<longrightarrow> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x12 x12a. \<lbrakk>aobj_ref x12a = None \<longrightarrow> (\<exists>y. aobj_ref x12 = Some y); cap' = ArchObjectCap x12; cap = ArchObjectCap x12a; \<not> is_zombie (ArchObjectCap x12) \<and> cap_master_arch_cap x12 = cap_master_arch_cap x12a \<and> is_master_reply_cap (ArchObjectCap x12) = is_reply_cap (ArchObjectCap x12a) \<and> is_derived_arch (ArchObjectCap x12a) (ArchObjectCap x12) \<and> \<not> is_reply_cap (ArchObjectCap x12) \<and> \<not> is_master_reply_cap (ArchObjectCap x12a)\<rbrakk> \<Longrightarrow> set_option (aobj_ref x12a) \<inter> set_option (aobj_ref x12) \<noteq> {} proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma is_derived_overlaps:
  "\<lbrakk> cte_wp_at (is_derived (cdt s) slot cap) slot s;
     obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {} \<rbrakk>
     \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap s" apply (simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at') apply (drule cte_wp_at_norm) apply (erule exE, rename_tac cap') apply (rule_tac x=cap' in exI) apply (blast dest: is_derived_overlaps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (is_derived (cdt s) slot cap) slot s; obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (is_derived (cdt s) slot cap) slot s; obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') slot s \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; \<exists>c. cte_wp_at ((=) c) slot s \<and> is_derived (cdt s) slot cap c\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') slot s \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; cte_wp_at ((=) cap') slot s \<and> is_derived (cdt s) slot cap cap'\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') slot s \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; cte_wp_at ((=) cap') slot s \<and> is_derived (cdt s) slot cap cap'\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap') slot s \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma is_derived_overlaps2:
  "\<lbrakk> cte_wp_at ((=) cap') slot s;
     is_derived (cdt s) slot cap cap';
     obj_refs cap' \<noteq> {} \<or> cap_irqs cap' \<noteq> {} \<rbrakk>
     \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap' s" apply (simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at') apply (blast dest: cte_wp_at_norm is_derived_overlaps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap') slot s; is_derived (cdt s) slot cap cap'; obj_refs cap' \<noteq> {} \<or> cap_irqs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap') slot s; is_derived (cdt s) slot cap cap'; obj_refs cap' = {} \<longrightarrow> cap_irqs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'a. cte_wp_at ((=) cap'a) slot s \<and> (cap_irqs cap' \<inter> cap_irqs cap'a = {} \<longrightarrow> obj_refs cap' \<inter> obj_refs cap'a = {} \<longrightarrow> arch_gen_refs cap' \<inter> arch_gen_refs cap'a \<noteq> {}) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma disj_dup: "A \<and> B \<and> C \<and> C'\<Longrightarrow> A \<and> B \<and> C \<and> A \<and> B \<and> C'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<and> B \<and> C \<and> C' \<Longrightarrow> A \<and> B \<and> C \<and> A \<and> B \<and> C'
theory FinalCaps

lemma weak_derived_overlaps:
  "\<lbrakk> cte_wp_at (weak_derived cap) slot s;
     obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {} \<rbrakk>
     \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap s" apply (simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at') apply (drule cte_wp_at_norm) apply (erule exE, rename_tac cap') apply (rule_tac x=cap' in exI) apply (blast dest: weak_derived_overlaps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (weak_derived cap) slot s; obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (weak_derived cap) slot s; obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') slot s \<and> (obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; \<exists>c. cte_wp_at ((=) c) slot s \<and> weak_derived cap c\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') slot s \<and> (obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; cte_wp_at ((=) cap') slot s \<and> weak_derived cap cap'\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') slot s \<and> (obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; cte_wp_at ((=) cap') slot s \<and> weak_derived cap cap'\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap') slot s \<and> (obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma not_cap_points_to_label_transfers_across_overlapping_caps:
  "\<lbrakk> \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot));
     slot \<in> slots_holding_overlapping_caps cap s \<rbrakk>
     \<Longrightarrow> \<not> intra_label_cap aag slot s" apply (simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at') apply (elim exE conjE, rename_tac cap') apply (simp add: intra_label_cap_def) apply (rule_tac x=cap' in exI) apply (auto simp: cap_points_to_label_def
              dest: caps_ref_single_objects caps_ref_single_irqs caps_ref_either_an_object_or_irq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); slot \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); \<exists>cap'. cte_wp_at ((=) cap') slot s \<and> (obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {})\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag slot s proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); cte_wp_at ((=) cap') slot s; obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag slot s proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); cte_wp_at ((=) cap') slot s; obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at ((=) cap) slot s \<and> \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); cte_wp_at ((=) cap') slot s; obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap') slot s \<and> \<not> cap_points_to_label aag cap' (pasObjectAbs aag (fst slot)) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma slots_holding_overlapping_caps_max_free_index_update[simp]:
  "slots_holding_overlapping_caps (max_free_index_update cap) s =
   slots_holding_overlapping_caps cap s" by (simp add: slots_holding_overlapping_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slots_holding_overlapping_caps (max_free_index_update cap) s = slots_holding_overlapping_caps cap s
theory FinalCaps

lemma cte_wp_at_eq:
  assumes a: "\<And>cap. \<lbrace>cte_wp_at ((=) cap) slot\<rbrace> f \<lbrace>\<lambda>_. cte_wp_at ((=) cap) slot\<rbrace>"
  shows "\<lbrace>cte_wp_at P slot\<rbrace> f \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace>" apply (clarsimp simp: valid_def) apply (drule cte_wp_at_norm) apply (elim exE conjE, rename_tac cap) apply (drule use_valid) apply (rule a) apply assumption apply (simp add: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P slot\<rbrace> f \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cte_wp_at P slot s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> cte_wp_at P slot b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<exists>c. cte_wp_at ((=) c) slot s \<and> P c\<rbrakk> \<Longrightarrow> cte_wp_at P slot b proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>(a, b) \<in> fst (f s); cte_wp_at ((=) cap) slot s; P cap\<rbrakk> \<Longrightarrow> cte_wp_at P slot b proof (prove)
goal (3 subgoals):
 1. \<And>s a b cap. \<lbrakk>cte_wp_at ((=) cap) slot s; P cap\<rbrakk> \<Longrightarrow> \<lbrace>?P13 s a b cap\<rbrace> f \<lbrace>?Q13 s a b cap\<rbrace>
 2. \<And>s a b cap. \<lbrakk>cte_wp_at ((=) cap) slot s; P cap\<rbrakk> \<Longrightarrow> ?P13 s a b cap s
 3. \<And>s a b cap. \<lbrakk>cte_wp_at ((=) cap) slot s; P cap; ?Q13 s a b cap a b\<rbrakk> \<Longrightarrow> cte_wp_at P slot b proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>cte_wp_at ((=) cap) slot s; P cap\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap17 s a b cap)) slot s
 2. \<And>s a b cap. \<lbrakk>cte_wp_at ((=) cap) slot s; P cap; cte_wp_at ((=) (?cap17 s a b cap)) slot b\<rbrakk> \<Longrightarrow> cte_wp_at P slot b proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>cte_wp_at ((=) cap) slot s; P cap; cte_wp_at ((=) cap) slot b\<rbrakk> \<Longrightarrow> cte_wp_at P slot b proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma (in is_extended') not_cte_wp_at[wp]: "I (\<lambda>s. \<not> cte_wp_at P t s)" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at P t s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> cte_wp_at P t s\<rbrace>
theory FinalCaps

lemma slots_holding_overlapping_caps_exst_update[simp]:
  "slots_holding_overlapping_caps cap (trans_state f s) =
   slots_holding_overlapping_caps cap s" by (simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slots_holding_overlapping_caps cap (trans_state f s) = slots_holding_overlapping_caps cap s
theory FinalCaps

lemma slots_holding_overlapping_caps_is_original_cap_update[simp]:
  "slots_holding_overlapping_caps cap (s\<lparr>is_original_cap := X\<rparr>) =
   slots_holding_overlapping_caps cap s" by (simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slots_holding_overlapping_caps cap (s\<lparr>is_original_cap := X\<rparr>) = slots_holding_overlapping_caps cap s
theory FinalCaps

lemma intra_label_cap_is_original_cap[simp]:
  "intra_label_cap aag slot (s\<lparr>is_original_cap := X\<rparr>) = intra_label_cap aag slot s" by (simp add: intra_label_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intra_label_cap aag slot (s\<lparr>is_original_cap := X\<rparr>) = intra_label_cap aag slot s
theory FinalCaps

lemma silc_inv_is_original_cap[simp]:
  "silc_inv aag st (s\<lparr>is_original_cap := X\<rparr>) = silc_inv aag st s" by (simp add: silc_inv_def silc_dom_equiv_def equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_inv aag st (s\<lparr>is_original_cap := X\<rparr>) = silc_inv aag st s
theory FinalCaps

lemma thread_set_tcb_fault_update_silc_inv[wp]:
  "\<lbrace>silc_inv aag st\<rbrace>
   thread_set (tcb_fault_update blah) t
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" by (rule thread_set_silc_inv; simp add: tcb_cap_cases_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> thread_set (tcb_fault_update blah) t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
theory FinalCaps

lemma reply_masters_mdbE:
  assumes rmm: "reply_masters_mdb m cs"
  assumes csr: "cs ptr = Some (ReplyCap t True rights)"
  obtains "m ptr = None"
      and "\<And>ptr'. ptr' \<in> descendants_of ptr m \<Longrightarrow> \<exists>R. cs ptr' = Some(ReplyCap t False R)" using rmm csr unfolding reply_masters_mdb_def by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>m ptr = None; \<And>ptr'. ptr' \<in> descendants_of ptr m \<Longrightarrow> \<exists>R. cs ptr' = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
reply_masters_mdb m cs
cs ptr = Some (ReplyCap t True rights)

goal (1 subgoal):
 1. (\<lbrakk>m ptr = None; \<And>ptr'. ptr' \<in> descendants_of ptr m \<Longrightarrow> \<exists>R. cs ptr' = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))
cs ptr = Some (ReplyCap t True rights)

goal (1 subgoal):
 1. (\<lbrakk>m ptr = None; \<And>ptr'. ptr' \<in> descendants_of ptr m \<Longrightarrow> \<exists>R. cs ptr' = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory FinalCaps

lemma cap_delete_one_silc_inv:
  "\<lbrace>silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>
   cap_delete_one slot
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding cap_delete_one_def by (wpsimp wp: unless_wp empty_slot_silc_inv get_cap_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace> do cap <- get_cap slot;
unless (cap = NullCap) $ do final <- is_final_cap cap;
fast_finalise cap final;
empty_slot slot NullCap
od
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
theory FinalCaps

lemma cap_delete_one_silc_inv_subject:
  "\<lbrace>silc_inv aag st and K (is_subject aag (fst slot))\<rbrace>
   cap_delete_one slot
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding cap_delete_one_def apply (wpsimp wp: unless_wp empty_slot_silc_inv get_cap_wp) unfolding silc_inv_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (is_subject aag (fst slot))\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (is_subject aag (fst slot))\<rbrace> do cap <- get_cap slot;
unless (cap = NullCap) $ do final <- is_final_cap cap;
fast_finalise cap final;
empty_slot slot NullCap
od
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; cap \<noteq> NullCap; cte_wp_at ((=) cap) slot s; pasSubject aag = SilcLabel\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>SilcLabel \<noteq> pasSubject aag \<and> (\<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s)) \<and> (\<forall>y auth. (y, auth, SilcLabel) \<in> pasPolicy aag \<longrightarrow> y = SilcLabel) \<and> (\<forall>slot cap. cte_wp_at ((=) cap) slot s \<and> \<not> intra_label_cap aag slot s \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s) \<and> silc_dom_equiv aag st s \<and> (\<forall>slot. pasObjectAbs aag (fst slot) = SilcLabel \<and> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot st \<longrightarrow> False); pasObjectAbs aag (fst slot) = SilcLabel; cap \<noteq> NullCap; cte_wp_at ((=) cap) slot s; pasSubject aag = SilcLabel\<rbrakk> \<Longrightarrow> False
theory FinalCaps

lemma cancel_ipc_silc_inv:
  "\<lbrace>silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag t)\<rbrace>
   cancel_ipc t
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding cancel_ipc_def apply (wp get_simple_ko_wp reply_cancel_ipc_silc_inv get_thread_state_inv hoare_vcg_all_lift
         | wpc
         | simp (no_asm) add: blocked_cancel_ipc_def get_ep_queue_def get_blocking_object_def
         | wp (once) hoare_drop_imps)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag t)\<rbrace> cancel_ipc t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag t)\<rbrace> do state <- get_thread_state t;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<Longrightarrow> silc_inv aag st s \<and> (\<forall>x xa. ko_at (Endpoint xa) x s \<longrightarrow> ((\<exists>x. xa = SendEP x) \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x. xa = RecvEP x) \<longrightarrow> silc_inv aag st s)) \<and> silc_inv aag st s \<and> valid_mdb s \<and> pas_refined aag s \<and> is_subject aag t \<and> silc_inv aag st s proof (prove)
goal:
No subgoals!