kings-crown/FVELER_Isabelle huggingface dataset:
theory FinalCaps

lemma caps_of_state_pspace':
  assumes x: "kheap s (fst slot) = kheap s' (fst slot)"
  shows "caps_of_state s slot = caps_of_state s' slot" by (simp add: caps_of_state_cte_wp_at cte_wp_at_pspace'[OF x])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s slot = caps_of_state s' slot
theory FinalCaps

lemma caps_of_state_intra_label_cap:
  "\<lbrakk> caps_of_state s slot = Some cap; caps_of_state t slot = Some cap; intra_label_cap aag slot s\<rbrakk>
     \<Longrightarrow> intra_label_cap aag slot t" by (fastforce simp: intra_label_cap_def cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some cap; caps_of_state t slot = Some cap; intra_label_cap aag slot s\<rbrakk> \<Longrightarrow> intra_label_cap aag slot t
theory FinalCaps

lemma is_final_then_nonempty_refs:
  "is_final_cap' cap s \<Longrightarrow> gen_obj_refs cap \<noteq> {}" by (auto simp add: is_final_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_final_cap' cap s \<Longrightarrow> gen_obj_refs cap \<noteq> {}
theory FinalCaps

lemma caps_ref_single_objects:
  "\<lbrakk> x \<in> obj_refs cap; y \<in> obj_refs cap \<rbrakk> \<Longrightarrow> x = y" by (cases cap; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> obj_refs cap; y \<in> obj_refs cap\<rbrakk> \<Longrightarrow> x = y
theory FinalCaps

lemma caps_ref_single_irqs:
  "\<lbrakk> x \<in> cap_irqs cap; y \<in> cap_irqs cap \<rbrakk> \<Longrightarrow> x = y" by (cases cap; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> cap_irqs cap; y \<in> cap_irqs cap\<rbrakk> \<Longrightarrow> x = y
theory FinalCaps

lemma intra_label_capD:
  "\<lbrakk> intra_label_cap aag slot s; cte_wp_at ((=) cap) slot s \<rbrakk>
     \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))" by (auto simp: intra_label_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>intra_label_cap aag slot s; cte_wp_at ((=) cap) slot s\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
theory FinalCaps

lemma intra_label_capD':
  "\<lbrakk> intra_label_cap aag slot s; caps_of_state s slot = Some cap \<rbrakk>
     \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))" by (auto simp: intra_label_cap_def cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>intra_label_cap aag slot s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
theory FinalCaps

lemma is_subject_kheap_eq:
  "\<lbrakk> reads_equiv aag s t; is_subject aag ptr \<rbrakk>
     \<Longrightarrow> kheap s ptr = kheap t ptr" apply (clarsimp simp: reads_equiv_def2) apply (erule states_equiv_forE_kheap) apply (blast intro: aag_can_read_self) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s t; is_subject aag ptr\<rbrakk> \<Longrightarrow> kheap s ptr = kheap t ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag ptr; states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s t; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t)\<rbrakk> \<Longrightarrow> kheap s ptr = kheap t ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag ptr; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap t x\<rbrakk> \<Longrightarrow> kheap s ptr = kheap t ptr proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma aag_can_read_kheap_eq:
  "\<lbrakk> reads_equiv aag s t; aag_can_read aag ptr \<rbrakk>
     \<Longrightarrow> kheap s ptr = kheap t ptr" apply (clarsimp simp: reads_equiv_def2) apply (erule states_equiv_forE_kheap) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s t; aag_can_read aag ptr\<rbrakk> \<Longrightarrow> kheap s ptr = kheap t ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aag_can_read aag ptr; states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s t; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t)\<rbrakk> \<Longrightarrow> kheap s ptr = kheap t ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aag_can_read aag ptr; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap t x\<rbrakk> \<Longrightarrow> kheap s ptr = kheap t ptr proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma caps_ref_either_an_object_or_irq':
   "ref \<in> cap_irqs cap' \<Longrightarrow>
    (obj_refs cap' = {} \<and> arch_gen_refs cap' = {})" apply (case_tac cap', simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ref \<in> cap_irqs cap' \<Longrightarrow> obj_refs cap' = {} \<and> arch_gen_refs cap' = {} proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma cap_points_to_label_def':
  "cap_points_to_label aag cap l = (\<forall>x \<in> gen_obj_refs cap. pasGenAbs aag x = l)" unfolding cap_points_to_label_def by (simp add: gen_obj_refs_def ball_Un FIXME_arch_gen_refs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_points_to_label aag cap l = (\<forall>x\<in>gen_obj_refs cap. pasGenAbs aag x = l) proof (prove)
goal (1 subgoal):
 1. ((\<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l) \<and> (\<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l)) = (\<forall>x\<in>gen_obj_refs cap. pasGenAbs aag x = l)
theory FinalCaps

lemma caps_ref_either_an_object_or_irq:
   "ref \<in> obj_refs cap'
    \<Longrightarrow> cap_irqs cap' = {} \<and> arch_gen_refs cap' = {}" apply (clarsimp simp: FIXME_arch_gen_refs) apply (case_tac cap'; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ref \<in> obj_refs cap' \<Longrightarrow> cap_irqs cap' = {} \<and> arch_gen_refs cap' = {} proof (prove)
goal (1 subgoal):
 1. ref \<in> obj_refs cap' \<Longrightarrow> cap_irqs cap' = {} proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma caps_ref_either_an_object_or_irq'':
   "ref \<in> arch_gen_refs cap'
    \<Longrightarrow> obj_refs cap' = {} \<and> cap_irqs cap' = {}" apply (clarsimp simp: FIXME_arch_gen_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ref \<in> arch_gen_refs cap' \<Longrightarrow> obj_refs cap' = {} \<and> cap_irqs cap' = {} proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma arch_gen_refs_no_intersection[simp]:
  "arch_gen_refs c \<inter> arch_gen_refs c' = {}" by (cases c; auto simp: FIXME_arch_gen_refs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_gen_refs c \<inter> arch_gen_refs c' = {}
theory FinalCaps

lemma is_final_cap'_read_equiv_eq:
  "\<lbrakk> silc_inv aag st s; cte_wp_at ((=) cap) slot s; silc_inv aag st t;
     cte_wp_at ((=) cap) slot t; aag_can_read_not_silc aag (fst slot); reads_equiv aag s t \<rbrakk>
     \<Longrightarrow> is_final_cap' cap s = is_final_cap' cap t" apply (rule iffI) subgoal by (rule is_final_cap'_read_equiv_imp) apply (drule reads_equiv_sym) subgoal by (rule is_final_cap'_read_equiv_imp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) slot s; silc_inv aag st t; cte_wp_at ((=) cap) slot t; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t\<rbrakk> \<Longrightarrow> is_final_cap' cap s = is_final_cap' cap t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) slot s; silc_inv aag st t; cte_wp_at ((=) cap) slot t; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s\<rbrakk> \<Longrightarrow> is_final_cap' cap t
 2. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) slot s; silc_inv aag st t; cte_wp_at ((=) cap) slot t; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap t\<rbrakk> \<Longrightarrow> is_final_cap' cap s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) slot s; silc_inv aag st t; cte_wp_at ((=) cap) slot t; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s\<rbrakk> \<Longrightarrow> is_final_cap' cap t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) slot s; silc_inv aag st t; cte_wp_at ((=) cap) slot t; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap t\<rbrakk> \<Longrightarrow> is_final_cap' cap s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) slot s; silc_inv aag st t; cte_wp_at ((=) cap) slot t; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; is_final_cap' cap t; reads_equiv aag t s\<rbrakk> \<Longrightarrow> is_final_cap' cap s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) slot s; silc_inv aag st t; cte_wp_at ((=) cap) slot t; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; is_final_cap' cap t; reads_equiv aag t s\<rbrakk> \<Longrightarrow> is_final_cap' cap s proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma is_final_cap_reads_respects:
  "reads_respects_f aag l (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) cap) slot s \<and>
                                                    aag_can_read_not_silc aag (fst slot)))
                          (is_final_cap cap)" unfolding is_final_cap_def by (clarsimp simp: equiv_valid_def2 equiv_valid_2_def in_monad
                     reads_equiv_f_def is_final_cap'_read_equiv_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) cap) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) (is_final_cap cap) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) cap) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) (gets (is_final_cap' cap))
theory FinalCaps

lemma slots_holding_overlapping_caps_def2:
  "slots_holding_overlapping_caps cap s =
     ctes_wp_at (\<lambda>c. (obj_refs cap \<inter> obj_refs c \<noteq> {}) \<or>
                     (cap_irqs cap \<inter> cap_irqs c \<noteq> {}) \<or>
                     (arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {})) s" by (simp add: slots_holding_overlapping_caps_def ctes_wp_at_def cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slots_holding_overlapping_caps cap s = ctes_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c \<noteq> {} \<or> cap_irqs cap \<inter> cap_irqs c \<noteq> {} \<or> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) s
theory FinalCaps

lemma not_intra_label_cap_pres:
  assumes cte: "\<And>P. \<lbrace>cte_wp_at P slot\<rbrace> f \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace>"
  shows "\<lbrace>\<lambda>s. \<not> intra_label_cap aag slot s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> intra_label_cap aag slot s\<rbrace>" apply (clarsimp simp: valid_def intra_label_cap_def) apply (rule_tac x=cap in exI) apply (drule_tac use_valid[OF _ cte], assumption) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> intra_label_cap aag slot s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> intra_label_cap aag slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>(a, b) \<in> fst (f s); cte_wp_at ((=) cap) slot s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at ((=) cap) slot b \<and> \<not> 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); cte_wp_at ((=) cap) slot s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) slot b \<and> \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>cte_wp_at ((=) cap) slot s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)); cte_wp_at ((=) cap) slot b\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) slot b \<and> \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma hoare_contrapositive:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<not> Q r s'; (r, s') \<in> fst (f s) \<rbrakk> \<Longrightarrow> \<not> P s" apply (case_tac "P s") apply (blast dest: use_valid) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<not> Q r s'; (r, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> \<not> P s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<not> Q r s'; (r, s') \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> \<not> P s
 2. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<not> Q r s'; (r, s') \<in> fst (f s); \<not> P s\<rbrakk> \<Longrightarrow> \<not> P s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<not> Q r s'; (r, s') \<in> fst (f s); \<not> P s\<rbrakk> \<Longrightarrow> \<not> P s proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma allI': "\<forall>x y. P x y \<Longrightarrow> \<forall>y x. P x y" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. P x y \<Longrightarrow> \<forall>y x. P x y
theory FinalCaps

lemma set_cap_well_formed_cnode_helper:
  "\<lbrakk> well_formed_cnode_n x xa; xa (snd slot) = Some y \<rbrakk>
     \<Longrightarrow> well_formed_cnode_n x (\<lambda>a. if a = snd slot then Some cap else xa a)" apply (simp add: well_formed_cnode_n_def) apply (rule equalityI) apply (drule equalityD1) apply (fastforce dest: subsetD split: if_splits) apply (drule equalityD2) apply (fastforce dest: subsetD split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> well_formed_cnode_n x (\<lambda>a. if a = snd slot then Some cap else xa a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom xa = {xa. length xa = x}; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> dom (\<lambda>a. if a = snd slot then Some cap else xa a) = {xa. length xa = x} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dom xa = {xa. length xa = x}; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> dom (\<lambda>a. if a = snd slot then Some cap else xa a) \<subseteq> {xa. length xa = x}
 2. \<lbrakk>dom xa = {xa. length xa = x}; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> {xa. length xa = x} \<subseteq> dom (\<lambda>a. if a = snd slot then Some cap else xa a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xa (snd slot) = Some y; dom xa \<subseteq> {xa. length xa = x}\<rbrakk> \<Longrightarrow> dom (\<lambda>a. if a = snd slot then Some cap else xa a) \<subseteq> {xa. length xa = x}
 2. \<lbrakk>dom xa = {xa. length xa = x}; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> {xa. length xa = x} \<subseteq> dom (\<lambda>a. if a = snd slot then Some cap else xa a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom xa = {xa. length xa = x}; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow> {xa. length xa = x} \<subseteq> dom (\<lambda>a. if a = snd slot then Some cap else xa a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xa (snd slot) = Some y; {xa. length xa = x} \<subseteq> dom xa\<rbrakk> \<Longrightarrow> {xa. length xa = x} \<subseteq> dom (\<lambda>a. if a = snd slot then Some cap else xa a) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma nonempty_refs:
  "\<not> cap_points_to_label aag cap l \<Longrightarrow> obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}" by (auto simp: cap_points_to_label_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> cap_points_to_label aag cap l \<Longrightarrow> obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}
theory FinalCaps

lemma set_cdt_silc_inv:
  "\<lbrace>silc_inv aag st and K (all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) m)\<rbrace>
   set_cdt m
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (simp add: set_cdt_def) apply wp apply (simp add: intra_label_cap_def slots_holding_overlapping_caps_def
                   silc_inv_def silc_dom_equiv_def equiv_for_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) m)\<rbrace> set_cdt m \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and (\<lambda>y. all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) m)\<rbrace> do s <- get;
put (s\<lparr>cdt := m\<rparr>)
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and (\<lambda>y. all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) m)) s \<Longrightarrow> silc_inv aag st (s\<lparr>cdt := m\<rparr>) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma update_cdt_silc_inv:
  "\<lbrace>silc_inv aag st and (\<lambda>s. all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (f (cdt s)))\<rbrace>
   update_cdt f
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (simp add: update_cdt_def) apply (wp set_cdt_silc_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and (\<lambda>s. all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (f (cdt s)))\<rbrace> update_cdt f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and (\<lambda>s. all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (f (cdt s)))\<rbrace> do t <- gets cdt;
set_cdt (f t)
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma cap_irqs_max_free_index_update[simp]:
  "cap_irqs (max_free_index_update cap) = cap_irqs cap" apply (case_tac cap, simp_all add: free_index_update_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_irqs (max_free_index_update cap) = cap_irqs cap proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma cap_points_to_label_max_free_index_update[simp]:
  "cap_points_to_label aag (max_free_index_update cap) l =  cap_points_to_label aag cap l" apply (simp add: cap_points_to_label_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_points_to_label aag (max_free_index_update cap) l = cap_points_to_label aag cap l proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma set_untyped_cap_as_full_slots_holding_overlapping_caps_other:
  "\<lbrace>\<lambda>s. x \<in> slots_holding_overlapping_caps capa s \<and>
        pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag (fst slot)\<rbrace>
   set_untyped_cap_as_full src_cap cap slot
   \<lbrace>\<lambda>_ s. x \<in> slots_holding_overlapping_caps capa s\<rbrace>" unfolding set_untyped_cap_as_full_def apply (rule hoare_pre) apply (wp set_cap_slots_holding_overlapping_caps_other[where aag=aag]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. x \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag (fst slot)\<rbrace> set_untyped_cap_as_full src_cap cap slot \<lbrace>\<lambda>_ s. x \<in> slots_holding_overlapping_caps capa s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. x \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag (fst slot)\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) slot else return () \<lbrace>\<lambda>_ s. x \<in> slots_holding_overlapping_caps capa s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) slot else return () \<lbrace>\<lambda>_ s. x \<in> slots_holding_overlapping_caps capa s\<rbrace>
 2. \<And>s. x \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag (fst slot) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. x \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag (fst slot) \<Longrightarrow> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> x \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag (fst slot)) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<longrightarrow> x \<in> slots_holding_overlapping_caps capa s) proof (prove)
goal:
No subgoals!