theory FinalCaps

lemma is_final_cap'_read_equiv_imp:
  "\<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; is_final_cap' cap s \<rbrakk>
     \<Longrightarrow> is_final_cap' cap t" unfolding F[symmetric] subgoal premises prems proof (rule ccontr) assume not_final: "\<not> is_final_cap' cap t" from prems have ilcs : "intra_label_cap aag slot s" by (fastforce elim: silc_inv_finalE[OF _ caps_of_state_cteD, where s = s]) hence ilct: "intra_label_cap aag slot t" using prems caps_of_state_intra_label_cap by blast from prems have sdest: "silc_dom_equiv aag s t" by (fastforce simp: silc_dom_equiv_def intro: equiv_for_trans
                    dest: silc_inv_silc_dom_equiv elim: equiv_for_sym) 

    (* if cap is non final, then there must exists another cap overlapping somewhere *)
     from not_final prems obtain slot' where "slot' \<in> slots_holding_overlapping_caps cap t"
                                        and diff: "slot' \<noteq> slot" by (fastforce elim: not_is_final_cap_caps_of_stateE[OF _ _ is_final_then_nonempty_refs]) then obtain cap' where cap': "caps_of_state t slot' = Some cap'"
                       and cap_overlap_cap': "gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}" by (fastforce simp: slots_holding_overlapping_caps_def' cte_wp_at_caps_of_state) note prems = prems not_final cap' cap_overlap_cap' diff show False proof (cases "aag_can_read aag (fst slot')") case True 
      (* This case is easy: slot' is in subjectReads domain, so cap' is also in slot' in s.
         Thus cap is not final: Direct contracticion*)
       thus ?thesis using prems apply - apply (erule(1) not_is_final_cap[THEN notE]) apply (simp add: caps_of_state_pspace'[OF aag_can_read_kheap_eq]) by fastforce+ next case False note cant_read = this 
      (* slot is in subjectRead, slot' isn't. However they hold overlaping caps. Thus: *)
       hence not_intra : "\<not> intra_label_cap aag slot' t" using prems ilct by (fastforce simp: cap_points_to_label_def' dest!: intra_label_capD') 
      (* Then, accroding to silc_inv, there is a third cap in SilcLabel overlapping cap and cap'*)
       then obtain lslot where "lslot \<in> slots_holding_overlapping_caps cap' t"
                          and lslot_silc: "pasObjectAbs aag (fst lslot) = SilcLabel" using prems silc_invD[simplified F[symmetric]] by blast then obtain lcap where lcap_t: "caps_of_state t lslot = Some lcap"
                         and lcap_overlap_cap': "gen_obj_refs cap' \<inter> gen_obj_refs lcap \<noteq> {}" by (fastforce simp: slots_holding_overlapping_caps_def' cte_wp_at_caps_of_state) 
      (* As lslot is in SilcLabel, kheap do not change between s and t and thus: *)
       have lcap_s: "caps_of_state s lslot = Some lcap" using lcap_t prems sdest apply (unfold silc_dom_equiv_def) apply (drule equiv_forD, rule lslot_silc) by (subst caps_of_state_pspace'; assumption) 
      (* lcap thus overlaps cap in s but cap was final in s: contradiction *)
       then show ?thesis  (* TODO CLEANUP *)
         using prems lslot_silc lcap_overlap_cap' lcap_s apply - apply (drule gen_obj_refs_distinct_or_equal)+ apply simp apply (erule(1) not_is_final_cap[where slot' = lslot, THEN notE,rotated]) apply (blast dest:is_final_then_nonempty_refs) apply assumption apply force done qed qed 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; is_final_cap' cap s\<rbrakk> \<Longrightarrow> is_final_cap' cap t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; 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. is_final_cap' cap t proof (state)
goal (1 subgoal):
 1. \<not> is_final_cap' cap t \<Longrightarrow> False proof (state)
this:
\<not> is_final_cap' cap t

goal (1 subgoal):
 1. \<not> is_final_cap' cap t \<Longrightarrow> False proof (chain)
picking this:
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s proof (prove)
using this:
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s

goal (1 subgoal):
 1. intra_label_cap aag slot s proof (state)
this:
intra_label_cap aag slot s

goal (1 subgoal):
 1. \<not> is_final_cap' cap t \<Longrightarrow> False proof (prove)
using this:
intra_label_cap aag slot s

goal (1 subgoal):
 1. intra_label_cap aag slot t proof (prove)
using this:
intra_label_cap aag slot s
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s
\<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

goal (1 subgoal):
 1. intra_label_cap aag slot t proof (state)
this:
intra_label_cap aag slot t

goal (1 subgoal):
 1. \<not> is_final_cap' cap t \<Longrightarrow> False proof (chain)
picking this:
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s proof (prove)
using this:
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s

goal (1 subgoal):
 1. silc_dom_equiv aag s t proof (state)
this:
silc_dom_equiv aag s t

goal (1 subgoal):
 1. \<not> is_final_cap' cap t \<Longrightarrow> False proof (state)
this:
silc_dom_equiv aag s t

goal (1 subgoal):
 1. \<not> is_final_cap' cap t \<Longrightarrow> False proof (chain)
picking this:
\<not> is_final_cap' cap t
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s proof (prove)
using this:
\<not> is_final_cap' cap t
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s

goal (1 subgoal):
 1. (\<And>slot'. \<lbrakk>slot' \<in> slots_holding_overlapping_caps cap t; slot' \<noteq> slot\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
slot' \<in> slots_holding_overlapping_caps cap t
slot' \<noteq> slot

goal (1 subgoal):
 1. \<not> is_final_cap' cap t \<Longrightarrow> False proof (chain)
picking this:
slot' \<in> slots_holding_overlapping_caps cap t
slot' \<noteq> slot proof (prove)
using this:
slot' \<in> slots_holding_overlapping_caps cap t
slot' \<noteq> slot

goal (1 subgoal):
 1. (\<And>cap'. \<lbrakk>caps_of_state t slot' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
caps_of_state t slot' = Some cap'
gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}

goal (1 subgoal):
 1. \<not> is_final_cap' cap t \<Longrightarrow> False proof (state)
this:
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s
\<not> is_final_cap' cap t
caps_of_state t slot' = Some cap'
gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}
slot' \<noteq> slot

goal (1 subgoal):
 1. \<not> is_final_cap' cap t \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. False proof (state)
goal (2 subgoals):
 1. aag_can_read aag (fst slot') \<Longrightarrow> False
 2. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (state)
this:
aag_can_read aag (fst slot')

goal (2 subgoals):
 1. aag_can_read aag (fst slot') \<Longrightarrow> False
 2. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (state)
this:
aag_can_read aag (fst slot')

goal (2 subgoals):
 1. aag_can_read aag (fst slot') \<Longrightarrow> False
 2. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (prove)
using this:
aag_can_read aag (fst slot')

goal (1 subgoal):
 1. False proof (prove)
using this:
aag_can_read aag (fst slot')
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s
\<not> is_final_cap' cap t
caps_of_state t slot' = Some cap'
gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}
slot' \<noteq> slot

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aag_can_read aag (fst slot'); silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}; slot' \<noteq> slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>aag_can_read aag (fst slot'); silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> caps_of_state s slot' = Some ?cap'13
 2. \<lbrakk>aag_can_read aag (fst slot'); silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> gen_obj_refs cap \<inter> gen_obj_refs ?cap'13 \<noteq> {}
 3. \<lbrakk>aag_can_read aag (fst slot'); silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> is_final_cap' cap s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aag_can_read aag (fst slot'); silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}
 2. \<lbrakk>aag_can_read aag (fst slot'); silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> is_final_cap' cap s proof (state)
this:
False

goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (state)
goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (state)
this:
pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag)

goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (state)
this:
pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag)

goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (state)
this:
pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag)

goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (prove)
using this:
pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag)

goal (1 subgoal):
 1. \<not> intra_label_cap aag slot' t proof (prove)
using this:
pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag)
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s
\<not> is_final_cap' cap t
caps_of_state t slot' = Some cap'
gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}
slot' \<noteq> slot
intra_label_cap aag slot t

goal (1 subgoal):
 1. \<not> intra_label_cap aag slot' t proof (state)
this:
\<not> intra_label_cap aag slot' t

goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (state)
this:
\<not> intra_label_cap aag slot' t

goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (chain)
picking this:
\<not> intra_label_cap aag slot' t proof (prove)
using this:
\<not> intra_label_cap aag slot' t

goal (1 subgoal):
 1. (\<And>lslot. \<lbrakk>lslot \<in> slots_holding_overlapping_caps cap' t; pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
\<not> intra_label_cap aag slot' t
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s
\<not> is_final_cap' cap t
caps_of_state t slot' = Some cap'
gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}
slot' \<noteq> slot
\<lbrakk>silc_inv ?aag ?st ?s; caps_of_state ?s ?slot = Some ?cap; \<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

goal (1 subgoal):
 1. (\<And>lslot. \<lbrakk>lslot \<in> slots_holding_overlapping_caps cap' t; pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
lslot \<in> slots_holding_overlapping_caps cap' t
pasObjectAbs aag (fst lslot) = SilcLabel

goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (chain)
picking this:
lslot \<in> slots_holding_overlapping_caps cap' t
pasObjectAbs aag (fst lslot) = SilcLabel proof (prove)
using this:
lslot \<in> slots_holding_overlapping_caps cap' t
pasObjectAbs aag (fst lslot) = SilcLabel

goal (1 subgoal):
 1. (\<And>lcap. \<lbrakk>caps_of_state t lslot = Some lcap; gen_obj_refs cap' \<inter> gen_obj_refs lcap \<noteq> {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
caps_of_state t lslot = Some lcap
gen_obj_refs cap' \<inter> gen_obj_refs lcap \<noteq> {}

goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (state)
this:
caps_of_state t lslot = Some lcap
gen_obj_refs cap' \<inter> gen_obj_refs lcap \<noteq> {}

goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. caps_of_state s lslot = Some lcap proof (prove)
using this:
caps_of_state t lslot = Some lcap
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s
\<not> is_final_cap' cap t
caps_of_state t slot' = Some cap'
gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}
slot' \<noteq> slot
silc_dom_equiv aag s t

goal (1 subgoal):
 1. caps_of_state s lslot = Some lcap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state t lslot = Some lcap; silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}; slot' \<noteq> slot; equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap s t\<rbrakk> \<Longrightarrow> caps_of_state s lslot = Some lcap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state t lslot = Some lcap; silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}; slot' \<noteq> slot; kheap s (fst lslot) = kheap t (fst lslot)\<rbrakk> \<Longrightarrow> caps_of_state s lslot = Some lcap proof (state)
this:
caps_of_state s lslot = Some lcap

goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (state)
this:
caps_of_state s lslot = Some lcap

goal (1 subgoal):
 1. pasObjectAbs aag (fst slot') \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<Longrightarrow> False proof (chain)
picking this:
caps_of_state s lslot = Some lcap proof (prove)
using this:
caps_of_state s lslot = Some lcap

goal (1 subgoal):
 1. False proof (prove)
using this:
caps_of_state s lslot = Some lcap

goal (1 subgoal):
 1. False proof (prove)
using this:
caps_of_state s lslot = Some lcap
silc_inv aag st s
caps_of_state s slot = Some cap
silc_inv aag st t
caps_of_state t slot = Some cap
aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
reads_equiv aag s t
is_final_cap' cap s
\<not> is_final_cap' cap t
caps_of_state t slot' = Some cap'
gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}
slot' \<noteq> slot
pasObjectAbs aag (fst lslot) = SilcLabel
gen_obj_refs cap' \<inter> gen_obj_refs lcap \<noteq> {}
caps_of_state s lslot = Some lcap

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s lslot = Some lcap; silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}; slot' \<noteq> slot; pasObjectAbs aag (fst lslot) = SilcLabel; gen_obj_refs cap' \<inter> gen_obj_refs lcap \<noteq> {}; caps_of_state s lslot = Some lcap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s lslot = Some lcap; silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; slot' \<noteq> slot; pasObjectAbs aag (fst lslot) = SilcLabel; caps_of_state s lslot = Some lcap; gen_obj_refs cap = gen_obj_refs cap'; gen_obj_refs cap' = gen_obj_refs lcap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; caps_of_state s slot = Some cap; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; slot' \<noteq> slot; pasObjectAbs aag (fst lslot) = SilcLabel; caps_of_state s lslot = Some lcap; gen_obj_refs cap = gen_obj_refs lcap; gen_obj_refs cap' = gen_obj_refs lcap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>silc_inv aag st s; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; slot' \<noteq> slot; pasObjectAbs aag (fst lslot) = SilcLabel; caps_of_state s lslot = Some lcap; gen_obj_refs cap = gen_obj_refs lcap; gen_obj_refs cap' = gen_obj_refs lcap\<rbrakk> \<Longrightarrow> gen_obj_refs cap \<inter> gen_obj_refs lcap \<noteq> {}
 2. \<lbrakk>silc_inv aag st s; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; slot' \<noteq> slot; pasObjectAbs aag (fst lslot) = SilcLabel; caps_of_state s lslot = Some lcap; gen_obj_refs cap = gen_obj_refs lcap; gen_obj_refs cap' = gen_obj_refs lcap\<rbrakk> \<Longrightarrow> is_final_cap' cap s
 3. \<lbrakk>silc_inv aag st s; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; slot' \<noteq> slot; pasObjectAbs aag (fst lslot) = SilcLabel; caps_of_state s lslot = Some lcap; gen_obj_refs cap = gen_obj_refs lcap; gen_obj_refs cap' = gen_obj_refs lcap\<rbrakk> \<Longrightarrow> lslot \<noteq> slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>silc_inv aag st s; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; slot' \<noteq> slot; pasObjectAbs aag (fst lslot) = SilcLabel; caps_of_state s lslot = Some lcap; gen_obj_refs cap = gen_obj_refs lcap; gen_obj_refs cap' = gen_obj_refs lcap\<rbrakk> \<Longrightarrow> is_final_cap' cap s
 2. \<lbrakk>silc_inv aag st s; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; slot' \<noteq> slot; pasObjectAbs aag (fst lslot) = SilcLabel; caps_of_state s lslot = Some lcap; gen_obj_refs cap = gen_obj_refs lcap; gen_obj_refs cap' = gen_obj_refs lcap\<rbrakk> \<Longrightarrow> lslot \<noteq> slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; silc_inv aag st t; caps_of_state t slot = Some cap; aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel; reads_equiv aag s t; is_final_cap' cap s; \<not> is_final_cap' cap t; caps_of_state t slot' = Some cap'; slot' \<noteq> slot; pasObjectAbs aag (fst lslot) = SilcLabel; caps_of_state s lslot = Some lcap; gen_obj_refs cap = gen_obj_refs lcap; gen_obj_refs cap' = gen_obj_refs lcap\<rbrakk> \<Longrightarrow> lslot \<noteq> slot proof (prove)
goal:
No subgoals! proof (state)
this:
False

goal:
No subgoals! proof (state)
this:
False

goal:
No subgoals! proof (prove)
goal:
No subgoals!