(*<*)
(*
 * Copyright 2015, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory Proofs
imports
  TSO
  Phases
  MarkObject
  StrongTricolour
  Valid_Refs
  Worklists
  Global_Noninterference
  Noninterference
  Initial_Conditions
begin

(*>*)
section‹Top-level safety \label{sec:top-level-correctness}›

lemma (in gc) I:
  "{ I } gc"
apply (simp add: I_defs)
apply (rule valid_pre)
apply ( rule valid_conj_lift valid_all_lift | fastforce )+
done

lemma (in sys) I:
  "{ I } sys"
apply (simp add: I_defs)
apply (rule valid_pre)
apply ( rule valid_conj_lift valid_all_lift | fastforce )+
done

text‹

  need to separately treat the two cases of a single mutator and
  mutators. In the latter case we have the additional
  of showing mutual non-interference amongst mutators.

 ›

lemma mut_invsL[intro]:
  "{I} mutator m {mut_m.invsL m'}"
proof(cases "m = m'")
  case True
  interpret mut_m m' by unfold_locales
  from True show ?thesis
    apply (simp add: I_defs)
    apply (rule valid_pre)
    apply ( rule valid_conj_lift | fastforce )+
    done
next
  case False
  then interpret mut_m' m' m by unfold_locales blast
  from False show ?thesis
    apply (simp add: I_defs)
    apply (rule valid_pre)
    apply ( rule valid_conj_lift | fastforce )+
    done
qed

(* FIXME split mutators_phase_inv from global invs to local invs. Move to StrongTricolour or similar. note dependence on I *)
lemma mutators_phase_inv[intro]:
  "{ I } mutator m { LSTP (mut_m.mutator_phase_inv m') }"
proof(cases "m = m'")
  case True
  interpret mut_m m' by unfold_locales
  from True show ?thesis
    apply (simp add: I_defs)
    apply (rule valid_pre)
    apply ( rule valid_conj_lift valid_all_lift | fastforce )+
    done
next
  case False
  then interpret mut_m' m' m by unfold_locales blast
  from False show ?thesis
    apply (simp add: I_defs)
    apply (rule valid_pre)
    apply ( rule valid_conj_lift valid_all_lift | fastforce )+
    done
qed

lemma (in mut_m) I:
  "{ I } mutator m"
apply (simp add: I_def gc.invsL_def invs_def Local_Invariants.invsL_def)
apply (rule valid_pre)
apply ( rule valid_conj_lift valid_all_lift | fastforce )+
apply (simp add: I_defs)
done

context gc_system
begin

theorem I: "gc_system ⊨ I"
apply (rule VCG)
 apply (rule init_inv)
apply (rename_tac p)
apply (case_tac p, simp_all)
  apply (rule mut_m.I[unfolded valid_proc_def, simplified])
 apply (rule gc.I[unfolded valid_proc_def, simplified])
apply (rule sys.I[unfolded valid_proc_def, simplified])
done

text‹

 label{sec:proofs-headline-safety}

  headline safety result follows directly.

 ›

corollary safety: "gc_system ⊨ LSTP valid_refs"
using I unfolding I_def invs_def valid_refs_def prerun_valid_def
apply clarsimp
apply (drule_tac x=σ in spec)
apply (drule (1) mp)
apply (rule alwaysI)
apply (erule_tac i=i in alwaysE)
apply (clarsimp simp: valid_refs_invD(1))
done

end

text‹

  GC is correct for the remaining fixed-but-arbitrary initial
 .

 ›

interpretation gc_system_interpretation: gc_system undefined .

(* unused_thms Main Sublist CIMP - *)


section‹ A concrete system state \label{sec:concrete-system-state} ›

text‹

  demonstrate that our definitions are not vacuous by exhibiting a
  initial state that satisfies the initial conditions. The heap
  shown in Figure~\ref{fig:concrete-heap}. We use Isabelle's notation
  types of a given size.

 begin{figure}
 \centering
 \includegraphics{heap.pdf}
 \caption{A concrete system state.}
 \label{fig:concrete-heap}
 end{figure}

 ›
(*<*)

end
(*>*)