Require Export EventOrdering.


Section correct.

  Context { pn  : @Node }.
  Context { pk  : @Key }.
  Context { m   : @Msg }.

  Local Open Scope eo.

  (* This defines what it means for a node [n] to be correct in a partial cut [L]
     of an event ordering [eo]: the keys of all events [e1] happening before [e]
     (an event of the partial cut [L]) at location [n], are different from the keys
     held at other locations at events [e2] prior to [e] *)
  Definition correct (eo : EventOrdering) (n : name) (L : list Event) :=
    forall e e1 e2,
      In e L
      -> e1 ≼ e
      -> e2 ≼ e
      -> loc e1 = n
      -> loc e2 <> n
      -> disjoint (lkm_sending_keys (keys e1)) (lkm_sending_keys (keys e2)).

  Definition correct_e {eo : EventOrdering} (e : Event) :=
    correct eo (loc e) [e].

End correct.
