kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchInfoFlow_IF

lemma equiv_asids_sym[InfoFlow_IF_assms]:
  "equiv_asids R s t \<Longrightarrow> equiv_asids R t s" by (auto simp: equiv_asids_def equiv_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_asids R s t \<Longrightarrow> equiv_asids R t s
theory ArchInfoFlow_IF

lemma equiv_asids_trans[InfoFlow_IF_assms]:
  "\<lbrakk> equiv_asids R s t; equiv_asids R t u \<rbrakk> \<Longrightarrow> equiv_asids R s u" by (fastforce simp: equiv_asids_def equiv_asid_def asid_pool_at_kheap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_asids R s t; equiv_asids R t u\<rbrakk> \<Longrightarrow> equiv_asids R s u
theory ArchInfoFlow_IF

lemma equiv_asids_non_asid_pool_kheap_update[InfoFlow_IF_assms]:
  "\<lbrakk> equiv_asids R s s'; non_asid_pool_kheap_update s kh; non_asid_pool_kheap_update s' kh' \<rbrakk>
     \<Longrightarrow> equiv_asids R (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)" apply (clarsimp simp: equiv_asids_def equiv_asid non_asid_pool_kheap_update_def) apply (fastforce simp: equiv_asid'_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_asids R s s'; non_asid_pool_kheap_update s kh; non_asid_pool_kheap_update s' kh'\<rbrakk> \<Longrightarrow> equiv_asids R (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>asid. \<lbrakk>\<forall>asid. asid \<noteq> 0 \<and> R asid \<longrightarrow> equiv_asid' asid (asid_table s (asid_high_bits_of asid)) (asid_table s' (asid_high_bits_of asid)) (kheap s) (kheap s'); \<forall>x. (\<exists>asid_pool. kheap s x = Some (ArchObj (ASIDPool asid_pool)) \<or> kh x = Some (ArchObj (ASIDPool asid_pool))) \<longrightarrow> kheap s x = kh x; \<forall>x. (\<exists>asid_pool. kheap s' x = Some (ArchObj (ASIDPool asid_pool)) \<or> kh' x = Some (ArchObj (ASIDPool asid_pool))) \<longrightarrow> kheap s' x = kh' x; asid \<noteq> 0; R asid\<rbrakk> \<Longrightarrow> equiv_asid' asid (asid_table s (asid_high_bits_of asid)) (asid_table s' (asid_high_bits_of asid)) kh kh' proof (prove)
goal:
No subgoals!
theory ArchInfoFlow_IF

lemma equiv_asids_identical_kheap_updates[InfoFlow_IF_assms]:
  "\<lbrakk> equiv_asids R s s'; identical_kheap_updates s s' kh kh' \<rbrakk>
     \<Longrightarrow> equiv_asids R (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)" apply (clarsimp simp: equiv_asids_def equiv_asid_def identical_kheap_updates_def asid_pool_at_kheap) apply (case_tac "kh pool_ptr = kh' pool_ptr"; fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_asids R s s'; identical_kheap_updates s s' kh kh'\<rbrakk> \<Longrightarrow> equiv_asids R (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>asid pool_ptr. \<lbrakk>\<forall>asid. asid \<noteq> 0 \<and> R asid \<longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table s' (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table s (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<exists>asid_pool. kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool))) \<and> (\<forall>asid_pool asid_pool'. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap s' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))); \<forall>x. kh x \<noteq> kh' x \<longrightarrow> kheap s x = kh x \<and> kheap s' x = kh' x; asid \<noteq> 0; R asid; asid_table s' (asid_high_bits_of asid) = Some pool_ptr\<rbrakk> \<Longrightarrow> (\<exists>asid_pool. kh pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<exists>asid_pool. kh' pool_ptr = Some (ArchObj (ASIDPool asid_pool))) \<and> (\<forall>asid_pool asid_pool'. kh pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kh' pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid)) proof (prove)
goal:
No subgoals!
theory ArchInfoFlow_IF

lemma equiv_asids_triv':
  "\<lbrakk> equiv_asids R s s'; kheap t = kheap s; kheap t' = kheap s';
     arm_asid_table (arch_state t) = arm_asid_table (arch_state s);
     arm_asid_table (arch_state t') = arm_asid_table (arch_state s') \<rbrakk>
     \<Longrightarrow> equiv_asids R t t'" by (fastforce simp: equiv_asids_def equiv_asid equiv_asid'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_asids R s s'; kheap t = kheap s; kheap t' = kheap s'; asid_table t = asid_table s; asid_table t' = asid_table s'\<rbrakk> \<Longrightarrow> equiv_asids R t t'
theory ArchInfoFlow_IF

lemma equiv_asids_triv[InfoFlow_IF_assms]:
  "\<lbrakk> equiv_asids R s s'; kheap t = kheap s; kheap t' = kheap s';
     arch_state t = arch_state s; arch_state t' = arch_state s' \<rbrakk>
     \<Longrightarrow> equiv_asids R t t'" by (fastforce simp: equiv_asids_triv')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_asids R s s'; kheap t = kheap s; kheap t' = kheap s'; arch_state t = arch_state s; arch_state t' = arch_state s'\<rbrakk> \<Longrightarrow> equiv_asids R t t'
theory ArchInfoFlow_IF

lemma globals_equiv_refl[InfoFlow_IF_assms]:
  "globals_equiv s s" by (simp add: globals_equiv_def idle_equiv_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv s s
theory ArchInfoFlow_IF

lemma globals_equiv_trans[InfoFlow_IF_assms]:
  "\<lbrakk> globals_equiv s t; globals_equiv t u \<rbrakk> \<Longrightarrow> globals_equiv s u" unfolding globals_equiv_def arch_globals_equiv_def by clarsimp (metis idle_equiv_trans idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_equiv s t; globals_equiv t u\<rbrakk> \<Longrightarrow> globals_equiv s u proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(arm_global_pd (arch_state s) = arm_global_pd (arch_state t) \<and> kheap s (arm_global_pd (arch_state s)) = kheap t (arm_global_pd (arch_state s)) \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state t))) \<and> idle_equiv s t \<and> cur_thread s = cur_thread t \<and> dom (device_state (machine_state s)) = dom (device_state (machine_state t)); (arm_global_pd (arch_state t) = arm_global_pd (arch_state u) \<and> kheap t (arm_global_pd (arch_state t)) = kheap u (arm_global_pd (arch_state t)) \<and> (cur_thread t \<noteq> idle_thread t \<longrightarrow> exclusive_state (machine_state t) = exclusive_state (machine_state u))) \<and> idle_equiv t u \<and> cur_thread t = cur_thread u \<and> dom (device_state (machine_state t)) = dom (device_state (machine_state u))\<rbrakk> \<Longrightarrow> (arm_global_pd (arch_state s) = arm_global_pd (arch_state u) \<and> kheap s (arm_global_pd (arch_state s)) = kheap u (arm_global_pd (arch_state s)) \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state u))) \<and> idle_equiv s u \<and> cur_thread s = cur_thread u \<and> dom (device_state (machine_state s)) = dom (device_state (machine_state u))
theory ArchInfoFlow_IF

lemma equiv_asids_guard_imp[InfoFlow_IF_assms]:
  "\<lbrakk> equiv_asids R s s'; \<And>x. Q x \<Longrightarrow> R x \<rbrakk> \<Longrightarrow> equiv_asids Q s s'" by (auto simp: equiv_asids_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_asids R s s'; \<And>x. Q x \<Longrightarrow> R x\<rbrakk> \<Longrightarrow> equiv_asids Q s s'
theory FinalCaps

lemma strengthen_cte_wp_at[strg]:
  "(\<And>x. st F (\<longrightarrow>) (P x) (Q x)) \<Longrightarrow> st F (\<longrightarrow>) (cte_wp_at P slot s) (cte_wp_at Q slot s)" by (cases F, auto elim:cte_wp_at_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. st F (\<longrightarrow>) (P x) (Q x)) \<Longrightarrow> st F (\<longrightarrow>) (cte_wp_at P slot s) (cte_wp_at Q slot s)
theory FinalCaps

lemma slots_holding_overlapping_caps_def':
  "slots_holding_overlapping_caps cap s =
   {cref. cte_wp_at (\<lambda>cap'. gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}) cref s}" unfolding slots_holding_overlapping_caps_def cte_wp_at_def gen_obj_refs_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slots_holding_overlapping_caps cap s = {cref. cte_wp_at (\<lambda>cap'. gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}) cref s} proof (prove)
goal (1 subgoal):
 1. {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> (obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<or> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {} \<or> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})} = {cref. \<exists>capa. fst (get_cap cref s) = {(capa, s)} \<and> (ObjRef ` obj_refs cap \<union> IRQRef ` cap_irqs cap \<union> ArchRef ` arch_gen_refs cap) \<inter> (ObjRef ` obj_refs capa \<union> IRQRef ` cap_irqs capa \<union> ArchRef ` arch_gen_refs capa) \<noteq> {}}
theory FinalCaps

lemma silc_inv_exst[simp]:
  "silc_inv aag st (trans_state f s) = silc_inv aag st s" by (auto simp: silc_inv_def silc_dom_equiv_def intra_label_cap_def
                 equiv_for_def slots_holding_overlapping_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_inv aag st (trans_state f s) = silc_inv aag st s
theory FinalCaps

lemma silc_inv_silc_dom_equiv:
  "silc_inv aag st s \<Longrightarrow> silc_dom_equiv aag st s" unfolding silc_inv_def by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_inv aag st s \<Longrightarrow> silc_dom_equiv aag st s proof (prove)
goal (1 subgoal):
 1. 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) \<Longrightarrow> silc_dom_equiv aag st s
theory FinalCaps

lemma silc_inv_cnode_onlyE:
  assumes si: "silc_inv aag st s"
  assumes posl: "pasObjectAbs aag x = SilcLabel"
  obtains sz where "cap_table_at sz x s" using si posl silc_inv_cnode_only by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>sz. cap_table_at sz x s \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
silc_inv aag st s
pasObjectAbs aag x = SilcLabel
\<lbrakk>silc_inv ?aag ?st ?s; pasObjectAbs ?aag ?x = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>sz. cap_table_at sz ?x ?s

goal (1 subgoal):
 1. (\<And>sz. cap_table_at sz x s \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory FinalCaps

lemma silc_inv_no_transferable:
  "\<lbrakk> silc_inv aag st s;  pasObjectAbs aag (fst slot) = SilcLabel;
     cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot st \<rbrakk>
     \<Longrightarrow> False" unfolding silc_inv_def by (force simp del: split_paired_All)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = SilcLabel; cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot st\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<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; cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) slot st\<rbrakk> \<Longrightarrow> False
theory FinalCaps

lemma cte_wp_at_pspace_specI:
  "\<lbrakk> cte_wp_at P slot s; kheap s (fst slot) = kheap s' (fst slot) \<rbrakk>
     \<Longrightarrow> cte_wp_at P slot s'" by (simp add: cte_wp_at_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P slot s; kheap s (fst slot) = kheap s' (fst slot)\<rbrakk> \<Longrightarrow> cte_wp_at P slot s'
theory FinalCaps

lemma (in is_extended') silc_inv[wp]: "I (silc_inv aag st)" by (rule lift_inv,simp)

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

lemma get_cap_cte_wp_at':
  "(fst (get_cap p s) = {(r,s)}) = cte_wp_at ((=) r) p s" by (auto simp: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fst (get_cap p s) = {(r, s)}) = cte_wp_at ((=) r) p s
theory FinalCaps

lemma silc_invD:
  "\<lbrakk> silc_inv aag st s; cte_wp_at ((=) cap) slot s; \<not> intra_label_cap aag slot s \<rbrakk>
     \<Longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
                 pasObjectAbs aag (fst lslot) = SilcLabel)" apply (clarsimp simp: silc_inv_def) apply (drule_tac x="fst slot" in spec, drule_tac x="snd slot" in spec, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) slot s; \<not> intra_label_cap aag slot s\<rbrakk> \<Longrightarrow> \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap) slot s; \<not> intra_label_cap aag slot s; SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<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 is_final_cap'_def4:
  "is_final_cap' cap s \<equiv> \<exists>a b. slots_holding_overlapping_caps cap s = {(a,b)}" by (simp add: is_final_cap'_def slots_holding_overlapping_caps_def gen_obj_refs_Int)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_final_cap' cap s \<equiv> \<exists>a b. slots_holding_overlapping_caps cap s = {(a, b)}
theory FinalCaps

lemma silc_inv:
  "silc_inv aag st s \<Longrightarrow>
     (\<forall>cap slot. cte_wp_at ((=) cap) slot s \<and> is_final_cap' cap s \<longrightarrow>
                 (intra_label_cap aag slot s \<or> (pasObjectAbs aag (fst slot) = SilcLabel)))" apply clarsimp apply (erule contrapos_np) apply (drule (2) silc_invD) apply (subgoal_tac "(a,b) \<in> slots_holding_overlapping_caps cap s") apply (clarsimp simp: is_final_cap'_def4 cte_wp_at_def) apply (auto simp: slots_holding_overlapping_caps_def cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_inv aag st s \<Longrightarrow> \<forall>cap slot. cte_wp_at ((=) cap) slot s \<and> is_final_cap' cap s \<longrightarrow> intra_label_cap aag slot s \<or> pasObjectAbs aag (fst slot) = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>cap a b. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) (a, b) s; is_final_cap' cap s; pasObjectAbs aag a \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> intra_label_cap aag (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>cap a b. \<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) (a, b) s; is_final_cap' cap s; \<not> intra_label_cap aag (a, b) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag a = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>cap a b. \<lbrakk>cte_wp_at ((=) cap) (a, b) s; is_final_cap' cap s; \<not> intra_label_cap aag (a, b) s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> pasObjectAbs aag a = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>cap a b. \<lbrakk>cte_wp_at ((=) cap) (a, b) s; is_final_cap' cap s; \<not> intra_label_cap aag (a, b) s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel; (a, b) \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> pasObjectAbs aag a = SilcLabel
 2. \<And>cap a b. \<lbrakk>cte_wp_at ((=) cap) (a, b) s; is_final_cap' cap s; \<not> intra_label_cap aag (a, b) s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> (a, b) \<in> slots_holding_overlapping_caps cap s proof (prove)
goal (1 subgoal):
 1. \<And>cap a b. \<lbrakk>cte_wp_at ((=) cap) (a, b) s; is_final_cap' cap s; \<not> intra_label_cap aag (a, b) s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> (a, b) \<in> slots_holding_overlapping_caps cap s proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma silc_inv_finalD:
  "\<lbrakk> silc_inv aag st s; cte_wp_at ((=) cap) slot s; is_final_cap' cap s \<rbrakk>
     \<Longrightarrow> intra_label_cap aag slot s \<or> (pasObjectAbs aag (fst slot) = SilcLabel)" apply clarsimp apply (erule contrapos_np) apply (drule (2) silc_invD) apply (subgoal_tac "slot \<in> slots_holding_overlapping_caps cap s") apply (clarsimp simp: is_final_cap'_def4 cte_wp_at_def) apply (auto simp: slots_holding_overlapping_caps_def cte_wp_at_def) done

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

lemma silc_inv_finalE:
  assumes hyp: "silc_inv aag st s" "cte_wp_at ((=) cap) slot s" "is_final_cap' cap s"
  obtains "intra_label_cap aag slot s" | "pasObjectAbs aag (fst slot) = SilcLabel" using hyp silc_inv_finalD by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>intra_label_cap aag slot s \<Longrightarrow> thesis; pasObjectAbs aag (fst slot) = SilcLabel \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis proof (prove)
using this:
silc_inv aag st s
cte_wp_at ((=) cap) slot s
is_final_cap' cap s
\<lbrakk>silc_inv ?aag ?st ?s; cte_wp_at ((=) ?cap) ?slot ?s; is_final_cap' ?cap ?s\<rbrakk> \<Longrightarrow> intra_label_cap ?aag ?slot ?s \<or> pasObjectAbs ?aag (fst ?slot) = SilcLabel

goal (1 subgoal):
 1. \<lbrakk>intra_label_cap aag slot s \<Longrightarrow> thesis; pasObjectAbs aag (fst slot) = SilcLabel \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
theory FinalCaps

lemma cte_wp_at_pspace':
  "kheap s (fst p) = kheap s' (fst p) \<Longrightarrow> cte_wp_at P p s = cte_wp_at P p s'" apply (rule iffI) apply (erule cte_wp_atE) apply (auto intro: cte_wp_at_cteI dest: sym)[1] apply (auto intro: cte_wp_at_tcbI dest: sym)[1] apply (erule cte_wp_atE) apply (auto intro: cte_wp_at_cteI dest: sym)[1] apply (auto intro: cte_wp_at_tcbI dest: sym)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s (fst p) = kheap s' (fst p) \<Longrightarrow> cte_wp_at P p s = cte_wp_at P p s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s (fst p) = kheap s' (fst p); cte_wp_at P p s\<rbrakk> \<Longrightarrow> cte_wp_at P p s'
 2. \<lbrakk>kheap s (fst p) = kheap s' (fst p); cte_wp_at P p s'\<rbrakk> \<Longrightarrow> cte_wp_at P p s proof (prove)
goal (3 subgoals):
 1. \<And>sz fun cte. \<lbrakk>kheap s (fst p) = kheap s' (fst p); kheap s (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some cte; P cte\<rbrakk> \<Longrightarrow> cte_wp_at P p s'
 2. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst p) = kheap s' (fst p); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P p s'
 3. \<lbrakk>kheap s (fst p) = kheap s' (fst p); cte_wp_at P p s'\<rbrakk> \<Longrightarrow> cte_wp_at P p s proof (prove)
goal (2 subgoals):
 1. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst p) = kheap s' (fst p); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P p s'
 2. \<lbrakk>kheap s (fst p) = kheap s' (fst p); cte_wp_at P p s'\<rbrakk> \<Longrightarrow> cte_wp_at P p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s (fst p) = kheap s' (fst p); cte_wp_at P p s'\<rbrakk> \<Longrightarrow> cte_wp_at P p s proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cte. \<lbrakk>kheap s (fst p) = kheap s' (fst p); kheap s' (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some cte; P cte\<rbrakk> \<Longrightarrow> cte_wp_at P p s
 2. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst p) = kheap s' (fst p); kheap s' (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P p s proof (prove)
goal (1 subgoal):
 1. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst p) = kheap s' (fst p); kheap s' (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P p s proof (prove)
goal:
No subgoals!