kings-crown/FVELER_Isabelle huggingface dataset:
theory FinalCaps

lemma set_cap_default_cap_silc_inv:
  "\<lbrace>silc_inv aag st and K (is_subject aag (fst slot) \<and> is_subject aag oref)\<rbrace>
   set_cap (default_cap a oref b dev) slot
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_pre) apply (rule set_cap_silc_inv) apply (auto simp: cap_points_to_label_def
              dest: subsetD[OF obj_refs_default_cap] simp: silc_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (is_subject aag (fst slot) \<and> is_subject aag oref)\<rbrace> set_cap (default_cap a oref b dev) slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap (default_cap a oref b dev) slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. (silc_inv aag st and K (is_subject aag (fst slot) \<and> is_subject aag oref)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and K (is_subject aag (fst slot) \<and> is_subject aag oref)) s \<Longrightarrow> ((\<lambda>s. \<not> cap_points_to_label aag (default_cap a oref b dev) (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps (default_cap a oref b dev) s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma slots_holding_overlapping_caps_from_silc_inv:
  assumes a: "\<lbrace>silc_inv aag st and P\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
  shows "\<lbrace>silc_inv aag st and (\<lambda> s. slot \<in> (slots_holding_overlapping_caps cap s) \<and>
                                pasObjectAbs aag (fst slot) = SilcLabel) and P\<rbrace>
         f
         \<lbrace>\<lambda>_ s. slot \<in> (slots_holding_overlapping_caps cap s)\<rbrace>" apply (simp add: valid_def split_def | intro impI allI ballI | elim conjE)+ apply (simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def) apply (erule subst[rotated], rule cte_wp_at_pspace') apply (case_tac x, simp) apply (drule use_valid[OF _ a]) apply simp by (fastforce simp: silc_inv_def silc_dom_equiv_def elim: equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and (\<lambda>s. slot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst slot) = SilcLabel) and P\<rbrace> f \<lbrace>\<lambda>_ s. slot \<in> slots_holding_overlapping_caps cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>x \<in> fst (f s); silc_inv aag st s; slot \<in> slots_holding_overlapping_caps cap s; pasObjectAbs aag (fst slot) = SilcLabel; P s\<rbrakk> \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap (snd x) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>x \<in> fst (f s); silc_inv aag st s; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) slot s; pasObjectAbs aag (fst slot) = SilcLabel; P s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) slot (snd x) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>x \<in> fst (f s); silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; P s\<rbrakk> \<Longrightarrow> kheap s (fst slot) = kheap (snd x) (fst slot) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b. \<lbrakk>(a, b) \<in> fst (f s); silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; P s; x = (a, b)\<rbrakk> \<Longrightarrow> kheap s (fst slot) = kheap b (fst slot) proof (prove)
goal (2 subgoals):
 1. \<And>s x a b. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; P s; x = (a, b)\<rbrakk> \<Longrightarrow> (silc_inv aag st and P) s
 2. \<And>s x a b. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; P s; x = (a, b); silc_inv aag st b\<rbrakk> \<Longrightarrow> kheap s (fst slot) = kheap b (fst slot) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; P s; x = (a, b); silc_inv aag st b\<rbrakk> \<Longrightarrow> kheap s (fst slot) = kheap b (fst slot)
theory FinalCaps

lemma delete_objects_silc_inv:
  "\<lbrace>silc_inv aag st and K (\<forall>p\<in>ptr_range ptr bits. is_subject aag p)\<rbrace>
   delete_objects ptr bits
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_gen_asm) unfolding delete_objects_def apply (wp detype_silc_inv |  simp add: ptr_range_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (\<forall>p\<in>ptr_range ptr bits. is_subject aag p)\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>ptr_range ptr bits. is_subject aag p \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>ptr_range ptr bits. is_subject aag p \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> do do_machine_op (freeMemory ptr bits);
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma is_arch_update_overlaps:
  "\<lbrakk> cte_wp_at (\<lambda>c. is_arch_update cap c) slot s; \<not> cap_points_to_label aag cap l \<rbrakk>
     \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap s" apply (clarsimp simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def) apply (erule cte_wp_at_weakenE) apply (clarsimp simp: is_arch_update_def) apply (clarsimp simp: cap_master_cap_def cap_points_to_label_def split: cap.splits) apply (fastforce dest: master_arch_cap_obj_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (is_arch_update cap) slot s; \<not> cap_points_to_label aag cap l\<rbrakk> \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (is_arch_update cap) slot s; \<not> cap_points_to_label aag cap l\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) slot s proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>\<not> cap_points_to_label aag cap l; is_arch_update cap c\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>\<not> cap_points_to_label aag cap l; is_arch_cap cap; cap_master_cap cap = cap_master_cap c; cap_irqs cap \<inter> cap_irqs c = {}; obj_refs cap \<inter> obj_refs c = {}; arch_gen_refs cap \<inter> arch_gen_refs c = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x12 x12a x. \<lbrakk>aobj_ref x12 \<noteq> Some x; arch_gen_obj_refs x12a \<inter> arch_gen_obj_refs x12 = {}; is_arch_cap (ArchObjectCap x12a); cap = ArchObjectCap x12a; cap_master_arch_cap x12a = cap_master_arch_cap x12; pasObjectAbs aag x \<noteq> l; aobj_ref x12a = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma send_signal_silc_inv[wp]:
  "send_signal ntfnptr badge \<lbrace>silc_inv aag st\<rbrace>" unfolding send_signal_def apply (wp get_simple_ko_wp gts_wp cancel_ipc_indirect_silc_inv | wpc | simp)+ apply (clarsimp simp: receive_blocked_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb $ setRegister badge_register badge;
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge)
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge')
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<Longrightarrow> \<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> ntfn_obj ntfn = IdleNtfn \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s)) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma slots_holding_overlapping_caps_eq:
  assumes "obj_refs cap = obj_refs cap'"
  assumes "cap_irqs cap = cap_irqs cap'"
  shows "slots_holding_overlapping_caps cap s = slots_holding_overlapping_caps cap' s" using assms by (fastforce simp: slots_holding_overlapping_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slots_holding_overlapping_caps cap s = slots_holding_overlapping_caps cap' s proof (prove)
using this:
obj_refs cap = obj_refs cap'
cap_irqs cap = cap_irqs cap'

goal (1 subgoal):
 1. slots_holding_overlapping_caps cap s = slots_holding_overlapping_caps cap' s
theory FinalCaps

lemma intra_label_cap_pres':
  assumes cte: "\<And>P. \<lbrace>\<lambda>s. cte_wp_at P slot s \<and> R s\<rbrace> f \<lbrace>\<lambda> _. cte_wp_at P slot\<rbrace>"
  shows "\<lbrace>intra_label_cap aag slot and cte_wp_at Q slot and R\<rbrace>
         f
         \<lbrace>\<lambda>_ s. intra_label_cap aag slot s\<rbrace>" apply (clarsimp simp: valid_def intra_label_cap_def) apply (drule cte_wp_at_norm) apply (elim exE conjE, rename_tac cap') apply (subgoal_tac "cap' = cap", blast) apply (drule use_valid[OF _ cte], fastforce) apply (rule_tac s=b in cte_wp_at_eqD2, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>intra_label_cap aag slot and cte_wp_at Q slot and R\<rbrace> f \<lbrace>\<lambda>_. intra_label_cap aag slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>(a, b) \<in> fst (f s); \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); cte_wp_at Q slot s; R s; cte_wp_at ((=) cap) slot b\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>(a, b) \<in> fst (f s); \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); R s; cte_wp_at ((=) cap) slot b; \<exists>c. cte_wp_at ((=) c) slot s \<and> Q c\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap cap'. \<lbrakk>(a, b) \<in> fst (f s); \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); R s; cte_wp_at ((=) cap) slot b; cte_wp_at ((=) cap') slot s; Q cap'\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap cap'. \<lbrakk>(a, b) \<in> fst (f s); \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); R s; cte_wp_at ((=) cap) slot b; cte_wp_at ((=) cap') slot s; Q cap'\<rbrakk> \<Longrightarrow> cap' = cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap cap'. \<lbrakk>\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); R s; cte_wp_at ((=) cap) slot b; cte_wp_at ((=) cap') slot s; Q cap'; cte_wp_at ((=) cap') slot b\<rbrakk> \<Longrightarrow> cap' = cap proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma get_cap_slots_holding_overlapping_caps:
  "\<lbrace>silc_inv aag st\<rbrace>
   get_cap slot
   \<lbrace>\<lambda>cap s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
            \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and>
                     pasObjectAbs aag a = SilcLabel)\<rbrace>" apply (wp get_cap_wp) apply (fastforce dest: silc_invD simp: intra_label_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma get_cap_cte_wp_at_triv:
  "\<lbrace>\<top>\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. cte_wp_at ((=) rv) slot s\<rbrace>" by (wp get_cap_wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_cap slot \<lbrace>\<lambda>rv. cte_wp_at ((=) rv) slot\<rbrace>
theory FinalCaps

lemma get_cap_valid_max_free_index_update:
  "\<lbrace>\<lambda>s. \<exists>cap. cte_wp_at ((=) cap) slot s \<and> valid_cap cap s \<and> is_untyped_cap cap\<rbrace>
   get_cap slot
   \<lbrace>\<lambda>rv s. s \<turnstile> max_free_index_update rv\<rbrace>" apply (wp get_cap_wp) apply clarsimp apply (drule (1) cte_wp_at_eqD2, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>cap. cte_wp_at ((=) cap) slot s \<and> s \<turnstile> cap \<and> is_untyped_cap cap\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. s \<turnstile> max_free_index_update rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>cap. cte_wp_at ((=) cap) slot s \<and> s \<turnstile> cap \<and> is_untyped_cap cap \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> s \<turnstile> max_free_index_update cap proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>cte_wp_at ((=) cap) slot s; s \<turnstile> cap; is_untyped_cap cap; cte_wp_at ((=) capa) slot s\<rbrakk> \<Longrightarrow> s \<turnstile> max_free_index_update capa proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma get_cap_perform_asid_control_invocation_helper:
  "\<lbrace>\<lambda>s. (\<exists>cap. cte_wp_at ((=) cap) x2 s \<and> valid_cap cap s \<and> is_untyped_cap cap) \<and> R\<rbrace>
   get_cap x2
   \<lbrace>\<lambda>rv s. free_index_of rv \<le> max_free_index (untyped_sz_bits rv) \<and> is_untyped_cap rv \<and>
           max_free_index (untyped_sz_bits rv) \<le> 2 ^ cap_bits rv \<and> R\<rbrace>" apply (wp get_cap_wp) apply clarsimp apply (drule (1) cte_wp_at_eqD2) apply (case_tac capa, simp_all add: max_free_index_def free_index_of_def valid_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>cap. cte_wp_at ((=) cap) x2 s \<and> s \<turnstile> cap \<and> is_untyped_cap cap) \<and> R\<rbrace> get_cap x2 \<lbrace>\<lambda>rv s. free_index_of rv \<le> max_free_index (untyped_sz_bits rv) \<and> is_untyped_cap rv \<and> max_free_index (untyped_sz_bits rv) \<le> 2 ^ cap_bits rv \<and> R\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>cap. cte_wp_at ((=) cap) x2 s \<and> s \<turnstile> cap \<and> is_untyped_cap cap) \<and> R \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) x2 s \<longrightarrow> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap \<and> R proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>R; cte_wp_at ((=) capa) x2 s; s \<turnstile> capa; is_untyped_cap capa; cte_wp_at ((=) cap) x2 s\<rbrakk> \<Longrightarrow> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>R; s \<turnstile> capa; is_untyped_cap capa; cte_wp_at ((=) cap) x2 s; cap = capa\<rbrakk> \<Longrightarrow> free_index_of cap \<le> max_free_index (untyped_sz_bits cap) \<and> is_untyped_cap cap \<and> max_free_index (untyped_sz_bits cap) \<le> 2 ^ cap_bits cap proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma untyped_caps_are_intra_label:
  "cte_wp_at is_untyped_cap slot s \<Longrightarrow> intra_label_cap aag slot s" apply (clarsimp simp: intra_label_cap_def cap_points_to_label_def) apply (drule (1) cte_wp_at_eqD2) apply (case_tac cap, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at is_untyped_cap slot s \<Longrightarrow> intra_label_cap aag slot s proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cte_wp_at is_untyped_cap slot s; cte_wp_at ((=) cap) slot s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>obj_refs cap. pasObjectAbs aag x = pasObjectAbs aag (fst slot)) \<and> (\<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = pasObjectAbs aag (fst slot)) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cte_wp_at is_untyped_cap slot s; is_untyped_cap cap\<rbrakk> \<Longrightarrow> (\<forall>x\<in>obj_refs cap. pasObjectAbs aag x = pasObjectAbs aag (fst slot)) \<and> (\<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = pasObjectAbs aag (fst slot)) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma interrupt_derived_ntfn_cap_identical_refs:
  "\<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap\<rbrakk> \<Longrightarrow>
   obj_refs cap = obj_refs cap' \<and>
   cap_irqs cap = cap_irqs cap'" apply (case_tac cap) apply (simp_all add: interrupt_derived_def cap_master_cap_def split: cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' \<and> cap_irqs cap = cap_irqs cap' proof (prove)
goal (12 subgoals):
 1. \<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap; cap = NullCap\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' \<and> cap_irqs cap = cap_irqs cap'
 2. \<And>x21 x22 x23 x24. \<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' \<and> cap_irqs cap = cap_irqs cap'
 3. \<And>x31 x32 x33. \<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' \<and> cap_irqs cap = cap_irqs cap'
 4. \<And>x41 x42 x43. \<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' \<and> cap_irqs cap = cap_irqs cap'
 5. \<And>x51 x52 x53. \<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' \<and> cap_irqs cap = cap_irqs cap'
 6. \<And>x61 x62 x63. \<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' \<and> cap_irqs cap = cap_irqs cap'
 7. \<And>x7. \<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' \<and> cap_irqs cap = cap_irqs cap'
 8. \<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap; cap = DomainCap\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' \<and> cap_irqs cap = cap_irqs cap'
 9. \<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' \<and> cap_irqs cap = cap_irqs cap'
 10. \<And>x10. \<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs cap' \<and> cap_irqs cap = cap_irqs cap'
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma cap_delete_one_cte_wp_at_other:
  "\<lbrace>cte_wp_at P slot and K (slot \<noteq> irq_slot)\<rbrace>
   cap_delete_one irq_slot
   \<lbrace>\<lambda>rv s. cte_wp_at P slot s\<rbrace>" unfolding cap_delete_one_def apply (wp unless_wp empty_slot_cte_wp_elsewhere get_cap_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P slot and K (slot \<noteq> irq_slot)\<rbrace> cap_delete_one irq_slot \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P slot and K (slot \<noteq> irq_slot)\<rbrace> do cap <- get_cap irq_slot;
unless (cap = NullCap) $ do final <- is_final_cap cap;
fast_finalise cap final;
empty_slot irq_slot NullCap
od
od \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace> proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma cap_insert_silc_inv'':
  "\<lbrace>silc_inv aag st and (\<lambda> s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest))
                              \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
                                           pasObjectAbs aag (fst lslot) = SilcLabel))
                    and K (is_subject aag (fst src) \<and> is_subject aag (fst dest))\<rbrace>
   cap_insert cap src dest
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_pre_imp[rotated]) apply (rule cap_insert_silc_inv''') apply clarsimp by (metis is_subject_not_silc_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (is_subject aag (fst src) \<and> is_subject aag (fst dest))\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. (silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (is_subject aag (fst src) \<and> is_subject aag (fst dest))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (is_subject aag (fst src) \<and> is_subject aag (fst dest))) s \<Longrightarrow> (silc_inv aag st and (\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and K (pasObjectAbs aag (fst src) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>silc_inv aag st s; \<not> cap_points_to_label aag cap SilcLabel \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); pasObjectAbs aag (fst src) = SilcLabel; pasObjectAbs aag (fst dest) = SilcLabel; pasSubject aag = SilcLabel\<rbrakk> \<Longrightarrow> False