kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchNoninterference

lemma owns_mapping_owns_asidpool:
  "\<lbrakk> kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s;
     is_subject aag p'; pas_wellformed (aag\<lparr>pasSubject := (pasObjectAbs aag p)\<rparr>) \<rbrakk>
     \<Longrightarrow> is_subject aag p" apply (frule asid_pool_into_aag) apply assumption+ apply (drule pas_wellformed_pasSubject_update_Control) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s; is_subject aag p'; pas_wellformed (aag\<lparr>pasSubject := pasObjectAbs aag p\<rparr>)\<rbrakk> \<Longrightarrow> is_subject aag p proof (prove)
goal (3 subgoals):
 1. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s; is_subject aag p'; pas_wellformed (aag\<lparr>pasSubject := pasObjectAbs aag p\<rparr>)\<rbrakk> \<Longrightarrow> pool ?r = Some ?p'
 2. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s; is_subject aag p'; pas_wellformed (aag\<lparr>pasSubject := pasObjectAbs aag p\<rparr>)\<rbrakk> \<Longrightarrow> pas_refined ?aag s
 3. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s; is_subject aag p'; pas_wellformed (aag\<lparr>pasSubject := pasObjectAbs aag p\<rparr>); (pasObjectAbs ?aag p, Control, pasObjectAbs ?aag ?p') \<in> pasPolicy ?aag\<rbrakk> \<Longrightarrow> is_subject aag p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s; is_subject aag p'; pas_wellformed (aag\<lparr>pasSubject := pasObjectAbs aag p\<rparr>); (pasObjectAbs aag p, Control, pasObjectAbs aag p') \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s; is_subject aag p'; (pasObjectAbs aag p, Control, pasObjectAbs aag p') \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, Control, pasObjectAbs aag ?p'4) \<in> pasPolicy aag
 2. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s; is_subject aag p'; (pasObjectAbs aag p, Control, pasObjectAbs aag p') \<in> pasPolicy aag; pasObjectAbs aag p = pasObjectAbs aag ?p'4\<rbrakk> \<Longrightarrow> is_subject aag p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (ArchObj (ASIDPool pool)); pool r = Some p'; pas_refined aag s; is_subject aag p'; (pasObjectAbs aag p, Control, pasObjectAbs aag p') \<in> pasPolicy aag; pasObjectAbs aag p = pasObjectAbs aag p'\<rbrakk> \<Longrightarrow> is_subject aag p proof (prove)
goal:
No subgoals!
theory ArchNoninterference

lemma arch_switch_to_thread_reads_respects_g'[Noninterference_assms]:
  "equiv_valid (reads_equiv_g aag) (affects_equiv aag l)
               (\<lambda>s s'. affects_equiv aag l s s' \<and>
                       arch_globals_equiv_strengthener (machine_state s) (machine_state s'))
               (\<lambda>s. is_subject aag t)
               (arch_switch_to_thread t)" apply (simp add: arch_switch_to_thread_def) apply (rule equiv_valid_guard_imp) by (wp bind_ev_general dmo_clearExMonitor_reads_respects_g' thread_get_reads_respects_g | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid (reads_equiv_g aag) (affects_equiv aag l) (\<lambda>s s'. affects_equiv aag l s s' \<and> arch_globals_equiv_strengthener (machine_state s) (machine_state s')) (\<lambda>s. is_subject aag t) (arch_switch_to_thread t) proof (prove)
goal (1 subgoal):
 1. equiv_valid (reads_equiv_g aag) (affects_equiv aag l) (\<lambda>s s'. affects_equiv aag l s s' \<and> exclusive_state (machine_state s) = exclusive_state (machine_state s')) (\<lambda>s. is_subject aag t) (do y <- set_vm_root t;
do_machine_op clearExMonitor
od) proof (prove)
goal (2 subgoals):
 1. equiv_valid (reads_equiv_g aag) (affects_equiv aag l) (\<lambda>s s'. affects_equiv aag l s s' \<and> exclusive_state (machine_state s) = exclusive_state (machine_state s')) ?Q (do y <- set_vm_root t;
do_machine_op clearExMonitor
od)
 2. \<And>s. is_subject aag t \<Longrightarrow> ?Q s
theory ArchNoninterference

lemma arch_switch_to_idle_thread_reads_respects_g[Noninterference_assms, wp]:
  "reads_respects_g aag l \<top> (arch_switch_to_idle_thread)" apply (simp add: arch_switch_to_idle_thread_def) apply wp apply (clarsimp simp: reads_equiv_g_def globals_equiv_idle_thread_ptr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) arch_switch_to_idle_thread proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (gets idle_thread >>= set_vm_root) proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t proof (prove)
goal:
No subgoals!
theory ArchNoninterference

lemma arch_globals_equiv_threads_eq[Noninterference_assms]:
  "arch_globals_equiv t' t'' kh kh' as as' ms ms'
   \<Longrightarrow> arch_globals_equiv t t kh kh' as as' ms ms'" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_globals_equiv t' t'' kh kh' as as' ms ms' \<Longrightarrow> arch_globals_equiv t t kh kh' as as' ms ms'
theory ArchNoninterference

lemma arch_globals_equiv_globals_equiv_scheduler[Noninterference_assms, elim]:
  "arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t)
                      (arch_state s) (arch_state t) (machine_state s) (machine_state t)
   \<Longrightarrow> arch_globals_equiv_scheduler (kheap s) (kheap t) (arch_state s) (arch_state t)" by (auto simp: arch_globals_equiv_scheduler_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_globals_equiv (cur_thread t) (idle_thread s) (kheap s) (kheap t) (arch_state s) (arch_state t) (machine_state s) (machine_state t) \<Longrightarrow> arch_globals_equiv_scheduler (kheap s) (kheap t) (arch_state s) (arch_state t)
theory ArchNoninterference

lemma integrity_asids_update_reference_state[Noninterference_assms]:
  "is_subject aag t
   \<Longrightarrow> integrity_asids aag {pasSubject aag} x asid s (s\<lparr>kheap := (kheap s)(t \<mapsto> blah)\<rparr>)" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_subject aag t \<Longrightarrow> integrity_asids aag {pasSubject aag} x asid s (s\<lparr>kheap := (kheap s)(t \<mapsto> blah)\<rparr>)
theory ArchNoninterference

lemma getActiveIRQ_no_non_kernel_IRQs[Noninterference_assms]:
  "getActiveIRQ True = getActiveIRQ False" by (clarsimp simp: getActiveIRQ_def non_kernel_IRQs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. getActiveIRQ True = getActiveIRQ False
theory Noninterference_Base_Refinement

lemma reachable:
  "conc.reachable s \<Longrightarrow> abs.reachable s" apply(simp add: conc.reachable_def abs.reachable_def) using refines by (fastforce simp: refines_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. conc.reachable s \<Longrightarrow> abs.reachable s proof (prove)
goal (1 subgoal):
 1. \<exists>js. s \<in> execution C s0 js \<Longrightarrow> \<exists>js. s \<in> execution A s0 js proof (prove)
using this:
C \<sqsubseteq> A

goal (1 subgoal):
 1. \<exists>js. s \<in> execution C s0 js \<Longrightarrow> \<exists>js. s \<in> execution A s0 js
theory Noninterference_Base_Refinement

lemma Step:
  "conc.Step a \<subseteq> abs.Step a" apply(simp add: conc.Step_def abs.Step_def) using refines by(fastforce simp: refines_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. conc.Step a \<subseteq> abs.Step a proof (prove)
goal (1 subgoal):
 1. {(s, s'). s' \<in> execution C s [a]} \<subseteq> {(s, s'). s' \<in> execution A s [a]} proof (prove)
using this:
C \<sqsubseteq> A

goal (1 subgoal):
 1. {(s, s'). s' \<in> execution C s [a]} \<subseteq> {(s, s'). s' \<in> execution A s [a]}
theory Noninterference_Base_Refinement

lemma confidentiality_u_refinement_closed:
  "abs.confidentiality_u \<Longrightarrow> conc.confidentiality_u" apply(simp add: abs.confidentiality_u_def) apply(subst conc.confidentiality_u_def) apply(blast intro: subsetD[OF Step] reachable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. abs.confidentiality_u \<Longrightarrow> conc.confidentiality_u proof (prove)
goal (1 subgoal):
 1. \<forall>a u s t. abs.reachable s \<and> abs.reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> abs.Step a \<and> (t, t') \<in> abs.Step a \<longrightarrow> s' \<sim>u\<sim> t') \<Longrightarrow> conc.confidentiality_u proof (prove)
goal (1 subgoal):
 1. \<forall>a u s t. abs.reachable s \<and> abs.reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> abs.Step a \<and> (t, t') \<in> abs.Step a \<longrightarrow> s' \<sim>u\<sim> t') \<Longrightarrow> \<forall>a u s t. conc.reachable s \<and> conc.reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> conc.Step a \<and> (t, t') \<in> conc.Step a \<longrightarrow> s' \<sim>u\<sim> t') proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Refinement

lemma confidentiality_u_weak_refinement_closed:
  "abs.confidentiality_u_weak \<Longrightarrow> conc.confidentiality_u_weak" apply(simp add: abs.confidentiality_u_weak_def) apply(subst conc.confidentiality_u_weak_def) apply(blast intro: subsetD[OF Step] reachable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. abs.confidentiality_u_weak \<Longrightarrow> conc.confidentiality_u_weak proof (prove)
goal (1 subgoal):
 1. \<forall>a u s t. abs.reachable s \<and> abs.reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> abs.Step a \<and> (t, t') \<in> abs.Step a \<longrightarrow> s' \<sim>u\<sim> t') \<Longrightarrow> conc.confidentiality_u_weak proof (prove)
goal (1 subgoal):
 1. \<forall>a u s t. abs.reachable s \<and> abs.reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> abs.Step a \<and> (t, t') \<in> abs.Step a \<longrightarrow> s' \<sim>u\<sim> t') \<Longrightarrow> \<forall>a u s t. conc.reachable s \<and> conc.reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> conc.Step a \<and> (t, t') \<in> conc.Step a \<longrightarrow> s' \<sim>u\<sim> t') proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Refinement

lemma integrity_u_refinement_closed:
  "abs.integrity_u \<Longrightarrow> conc.integrity_u" apply(simp add: abs.integrity_u_def) apply(subst conc.integrity_u_def) apply(blast intro: subsetD[OF Step] reachable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. abs.integrity_u \<Longrightarrow> conc.integrity_u proof (prove)
goal (1 subgoal):
 1. \<forall>a u s. abs.reachable s \<longrightarrow> (dom a s, u) \<notin> policy \<longrightarrow> (\<forall>s'. (s, s') \<in> abs.Step a \<longrightarrow> s \<sim>u\<sim> s') \<Longrightarrow> conc.integrity_u proof (prove)
goal (1 subgoal):
 1. \<forall>a u s. abs.reachable s \<longrightarrow> (dom a s, u) \<notin> policy \<longrightarrow> (\<forall>s'. (s, s') \<in> abs.Step a \<longrightarrow> s \<sim>u\<sim> s') \<Longrightarrow> \<forall>a u s. conc.reachable s \<longrightarrow> (dom a s, u) \<notin> policy \<longrightarrow> (\<forall>s'. (s, s') \<in> conc.Step a \<longrightarrow> s \<sim>u\<sim> s') proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Refinement

lemma uwr_equiv:
  "abs.uwr_equiv s as t bs u \<Longrightarrow> conc.uwr_equiv s as t bs u" apply(insert refines) apply(fastforce simp: abs.uwr_equiv_def conc.uwr_equiv_def simp: refines_def dest: subsetD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. abs.uwr_equiv s as t bs u \<Longrightarrow> conc.uwr_equiv s as t bs u proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs.uwr_equiv s as t bs u; C \<sqsubseteq> A\<rbrakk> \<Longrightarrow> conc.uwr_equiv s as t bs u proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Refinement

lemma xNonleakage_gen_refinement_closed:
  "abs.xNonleakage_gen \<Longrightarrow> conc.xNonleakage_gen" apply(frule abs.xNonleakage_gen_confidentiality_u) apply(frule xources_subset) apply(clarsimp simp: abs.xNonleakage_gen_def conc.xNonleakage_gen_def) apply(drule (1) sameFor_subset_dom[OF _ xources_subset]) apply(blast dest: reachable uwr_equiv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. abs.xNonleakage_gen \<Longrightarrow> conc.xNonleakage_gen proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs.xNonleakage_gen; abs.confidentiality_u\<rbrakk> \<Longrightarrow> conc.xNonleakage_gen proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs.xNonleakage_gen; abs.confidentiality_u; abs.xources ?as2 ?s2 ?u2 \<subseteq> conc.xources ?as2 ?s2 ?u2\<rbrakk> \<Longrightarrow> conc.xNonleakage_gen proof (prove)
goal (1 subgoal):
 1. \<And>as s u t. \<lbrakk>\<forall>as s u t. abs.reachable s \<and> abs.reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>abs.xources as s u\<approx> t \<longrightarrow> abs.uwr_equiv s as t as u; abs.confidentiality_u; abs.xources ?as2 ?s2 ?u2 \<subseteq> conc.xources ?as2 ?s2 ?u2; conc.reachable s; conc.reachable t; s \<sim>schedDomain\<sim> t; s \<approx>conc.xources as s u\<approx> t\<rbrakk> \<Longrightarrow> conc.uwr_equiv s as t as u proof (prove)
goal (1 subgoal):
 1. \<And>as s u t. \<lbrakk>\<forall>as s u t. abs.reachable s \<and> abs.reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>abs.xources as s u\<approx> t \<longrightarrow> abs.uwr_equiv s as t as u; abs.confidentiality_u; abs.xources ?as2 ?s2 ?u2 \<subseteq> conc.xources ?as2 ?s2 ?u2; conc.reachable s; conc.reachable t; s \<sim>schedDomain\<sim> t; s \<approx>abs.xources as s u\<approx> t\<rbrakk> \<Longrightarrow> conc.uwr_equiv s as t as u proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Refinement

lemma Noninfluence_strong_uwr_refinement_closed:
  "abs.Noninfluence_strong_uwr \<Longrightarrow>
    conc.Noninfluence_strong_uwr" apply(frule abs.Noninfluence_strong_uwr_confidentiality_u_weak) apply(drule abs.Noninfluence_strong_uwr_integrity_u) apply(drule confidentiality_u_weak_refinement_closed) apply(drule integrity_u_refinement_closed) apply(blast intro: conc.Noninfluence_strong_uwr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. abs.Noninfluence_strong_uwr \<Longrightarrow> conc.Noninfluence_strong_uwr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs.Noninfluence_strong_uwr; abs.confidentiality_u_weak\<rbrakk> \<Longrightarrow> conc.Noninfluence_strong_uwr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs.confidentiality_u_weak; abs.integrity_u\<rbrakk> \<Longrightarrow> conc.Noninfluence_strong_uwr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs.integrity_u; conc.confidentiality_u_weak\<rbrakk> \<Longrightarrow> conc.Noninfluence_strong_uwr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>conc.confidentiality_u_weak; conc.integrity_u\<rbrakk> \<Longrightarrow> conc.Noninfluence_strong_uwr proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Refinement

lemma Nonleakage_gen_refinement_closed:
  "abs.Nonleakage_gen \<Longrightarrow>
    conc.Nonleakage_gen" apply(simp add: abs.Nonleakage_gen_equiv_confidentiality_u conc.Nonleakage_gen_equiv_confidentiality_u) apply(erule confidentiality_u_refinement_closed) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. abs.Nonleakage_gen \<Longrightarrow> conc.Nonleakage_gen proof (prove)
goal (1 subgoal):
 1. abs.confidentiality_u \<Longrightarrow> conc.confidentiality_u proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Refinement

lemma Noninfluence_strong_quasi_refinement_closed:
  "\<lbrakk>abs.confidentiality_u_weak; abs.integrity_u;
        output_consistent\<rbrakk> \<Longrightarrow>
    conc.Noninfluence_strong" apply(rule conc.Noninfluence_strong) apply(erule confidentiality_u_weak_refinement_closed) apply assumption apply(erule integrity_u_refinement_closed) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs.confidentiality_u_weak; abs.integrity_u; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.Noninfluence_strong proof (prove)
goal (3 subgoals):
 1. \<lbrakk>abs.confidentiality_u_weak; abs.integrity_u; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.confidentiality_u_weak
 2. \<lbrakk>abs.confidentiality_u_weak; abs.integrity_u; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.output_consistent
 3. \<lbrakk>abs.confidentiality_u_weak; abs.integrity_u; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.integrity_u proof (prove)
goal (2 subgoals):
 1. \<lbrakk>abs.confidentiality_u_weak; abs.integrity_u; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.output_consistent
 2. \<lbrakk>abs.confidentiality_u_weak; abs.integrity_u; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.integrity_u proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs.confidentiality_u_weak; abs.integrity_u; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.integrity_u proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Refinement

lemma Noninfluence_strong_uwr_quasi_refinement_closed:
  "\<lbrakk>abs.Noninfluence_strong_uwr;
        output_consistent\<rbrakk> \<Longrightarrow>
    conc.Noninfluence_strong" apply(rule conc.Noninfluence_strong) apply(rule confidentiality_u_weak_refinement_closed) apply(erule abs.Noninfluence_strong_uwr_confidentiality_u_weak) apply assumption apply(rule integrity_u_refinement_closed) apply(erule abs.Noninfluence_strong_uwr_integrity_u) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs.Noninfluence_strong_uwr; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.Noninfluence_strong proof (prove)
goal (3 subgoals):
 1. \<lbrakk>abs.Noninfluence_strong_uwr; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.confidentiality_u_weak
 2. \<lbrakk>abs.Noninfluence_strong_uwr; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.output_consistent
 3. \<lbrakk>abs.Noninfluence_strong_uwr; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.integrity_u proof (prove)
goal (3 subgoals):
 1. \<lbrakk>abs.Noninfluence_strong_uwr; conc.output_consistent\<rbrakk> \<Longrightarrow> abs.confidentiality_u_weak
 2. \<lbrakk>abs.Noninfluence_strong_uwr; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.output_consistent
 3. \<lbrakk>abs.Noninfluence_strong_uwr; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.integrity_u proof (prove)
goal (2 subgoals):
 1. \<lbrakk>abs.Noninfluence_strong_uwr; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.output_consistent
 2. \<lbrakk>abs.Noninfluence_strong_uwr; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.integrity_u proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs.Noninfluence_strong_uwr; conc.output_consistent\<rbrakk> \<Longrightarrow> conc.integrity_u proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs.Noninfluence_strong_uwr; conc.output_consistent\<rbrakk> \<Longrightarrow> abs.integrity_u proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma subjectReads_T:
  "subjectReads example_auth_graph (partition_label T) = {partition_label T}" apply(auto elim: subjectReads.induct) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectReads example_auth_graph (partition_label T) = {partition_label T} proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma CTR_in_subjectReads_NTFN1:
  "partition_label CTR \<in> subjectReads example_auth_graph (partition_label NTFN1)" apply(rule read_sync_ep_read_receivers[where ep="partition_label NTFN1"], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label CTR \<in> subjectReads example_auth_graph (partition_label NTFN1) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma EP_in_subjectReads_NTFN1:
  "partition_label EP \<in> subjectReads example_auth_graph (partition_label NTFN1)" apply(rule reads_read_queued_thread_read_ep[where t="partition_label CTR" and a="partition_label EP"], auto intro: CTR_in_subjectReads_NTFN1[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectReads example_auth_graph (partition_label NTFN1) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma C_in_subjectReads_NTFN1:
  "partition_label C \<in> subjectReads example_auth_graph (partition_label NTFN1)" apply(rule reads_read_thread_read_pages) apply (rule CTR_in_subjectReads_NTFN1) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label C \<in> subjectReads example_auth_graph (partition_label NTFN1) proof (prove)
goal (2 subgoals):
 1. ?t \<in> subjectReads example_auth_graph (partition_label NTFN1)
 2. (?t, Read, partition_label C) \<in> example_auth_graph proof (prove)
goal (1 subgoal):
 1. (partition_label CTR, Read, partition_label C) \<in> example_auth_graph proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma NTFN2_in_subjectReads_NTFN1:
  "partition_label NTFN2 \<in> subjectReads example_auth_graph (partition_label NTFN1)" apply (rule reads_read_queued_thread_read_ep[where t="partition_label RM" and a="partition_label NTFN2"]) by (auto intro: RM_in_subjectReads_NTFN1[simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN2 \<in> subjectReads example_auth_graph (partition_label NTFN1) proof (prove)
goal (5 subgoals):
 1. (partition_label NTFN2, ?auth', partition_label NTFN2) \<in> example_auth_graph
 2. ?auth' \<in> {Notify, SyncSend, Reset}
 3. (partition_label RM, ?auth, partition_label NTFN2) \<in> example_auth_graph
 4. ?auth \<in> {SyncSend, Receive}
 5. partition_label RM \<in> subjectReads example_auth_graph (partition_label NTFN1)
theory PolicyExample

lemma RM_in_subjectReads_NTFN2:
  "partition_label RM \<in> subjectReads example_auth_graph (partition_label NTFN2)" apply(rule read_sync_ep_read_receivers[where ep="partition_label NTFN2"], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectReads example_auth_graph (partition_label NTFN2) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma EP_in_subjectReads_NTFN2:
  "partition_label EP \<in> subjectReads example_auth_graph (partition_label NTFN2)" apply(rule reads_read_queued_thread_read_ep[where t="partition_label RM" and a="partition_label EP"], auto intro: RM_in_subjectReads_NTFN2[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectReads example_auth_graph (partition_label NTFN2) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma CTR_in_subjectReads_NTFN2:
  "partition_label CTR \<in> subjectReads example_auth_graph (partition_label NTFN2)" apply(rule read_sync_ep_read_senders[where ep="partition_label EP"], auto intro: EP_in_subjectReads_NTFN2[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label CTR \<in> subjectReads example_auth_graph (partition_label NTFN2) proof (prove)
goal:
No subgoals!