From stdpp Require Import prelude.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
From VLSM.Lib Require Import Preamble.
From VLSM.Core Require Import VLSM VLSMProjections Composition Equivocation.[Loading ML file coq-itauto.plugin ... done]

Core: VLSM No-Equivocation Composition Constraints

Section sec_no_equivocations.

Context
  {message : Type}
  (vlsm : VLSM message)
  `{HasBeenSentCapability message vlsm}
  .

An equivocating transition can be prevented by checking that the message to be received has_been_sent previously in the state about to receive it.

However, since we might allow certain other messages, such as initial messages, we give a slightly more general definition, that of no_equivocation_except_from those specified by a given predicate.

Definition no_equivocations_except_from
  (exception : message -> Prop) (l : label vlsm) (som : state vlsm * option message) : Prop :=
  let (s, om) := som in
    from_option (fun m => has_been_sent vlsm s m \/ exception m) True om.

The no_equivocations constraint does not allow any exceptions (messages being received must have been previously sent).

Definition no_equivocations
  (l : label vlsm) (som : state vlsm * option message) : Prop :=
    no_equivocations_except_from (fun m => False) l som.

End sec_no_equivocations.

No-Equivocation Invariants

In this section we show that under no_equivocations assumptions:

for any valid state all messages directly_observed_were_sent.
the preloaded_with_all_messages_vlsm is equal to the no_equivocations VLSM.

Section sec_no_equivocation_invariants.

Context
  (message : Type)
  (X : VLSM message)
  `{HasBeenSentCapability message X}
  `{HasBeenDirectlyObservedCapability message X}
  (Henforced : forall l s om, input_constrained X l (s, om) -> no_equivocations X l (s, om))
  .

A VLSM that enforces the no_equivocations constraint and also supports has_been_directly_observed obeys the directly_observed_were_sent invariant which states that any message that has_been_directly_observed in a state, has_been_sent in the same state, too.

Definition directly_observed_were_sent (s : state X) : Prop :=
  forall msg : message,
    has_been_directly_observed X s msg -> has_been_sent X s msg.

Lemma directly_observed_were_sent_initial :
  forall (s : state X),
    initial_state_prop X s -> directly_observed_were_sent s.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
∀ s : state X,
  initial_state_prop s → directly_observed_were_sent s
Proof.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
∀ s : state X,
  initial_state_prop s → directly_observed_were_sent s
  intros s Hinitial msg Hsend.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
s: state X
Hinitial: initial_state_prop s
msg: message
Hsend: has_been_directly_observed X s msg
has_been_sent X s msg
  by apply has_been_directly_observed_no_inits in Hsend.
Qed.

Lemma directly_observed_were_sent_preserved :
  forall (l : label X) (s : state X) (im : option message) (s' : state X) (om : option message),
    input_valid_transition X l (s, im) (s', om) -> directly_observed_were_sent s ->
      directly_observed_were_sent s'.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
∀ (l : label X) (s : state X) (im : option message) 
  (s' : state X) (om : option message),
  input_valid_transition X l (s, im) (s', om)
  → directly_observed_were_sent s
    → directly_observed_were_sent s'
Proof.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
∀ (l : label X) (s : state X) (im : option message) 
  (s' : state X) (om : option message),
  input_valid_transition X l (s, im) (s', om)
  → directly_observed_were_sent s
    → directly_observed_were_sent s'
  intros l s im s' om Hptrans Hprev msg Hobs.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
l: label X
s: state X
im: option message
s': state X
om: option message
Hptrans: input_valid_transition X l (s, im) (s', om)
Hprev: directly_observed_were_sent s
msg: message
Hobs: has_been_directly_observed X s' msg
has_been_sent X s' msg
  apply preloaded_weaken_input_valid_transition in Hptrans.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
l: label X
s: state X
im: option message
s': state X
om: option message
Hptrans: input_constrained_transition X l (
  s, im) (s', om)
Hprev: directly_observed_were_sent s
msg: message
Hobs: has_been_directly_observed X s' msg
has_been_sent X s' msg
  eapply (oracle_step_update (has_been_directly_observed_stepwise_props X)) in Hobs;
    cbn in Hobs; [| done].message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
l: label X
s: state X
im: option message
s': state X
om: option message
Hptrans: input_constrained_transition X l (
  s, im) (s', om)
Hprev: directly_observed_were_sent s
msg: message
Hobs: (im = Some msg ∨ om = Some msg)
∨ has_been_directly_observed X s msg
has_been_sent X s' msg
  rewrite has_been_sent_step_update by done.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
l: label X
s: state X
im: option message
s': state X
om: option message
Hptrans: input_constrained_transition X l (
  s, im) (s', om)
Hprev: directly_observed_were_sent s
msg: message
Hobs: (im = Some msg ∨ om = Some msg)
∨ has_been_directly_observed X s msg
om = Some msg ∨ has_been_sent X s msg
  destruct Hobs as [[-> | ->] |].message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
l: label X
s, s': state X
om: option message
msg: message
Hptrans: input_constrained_transition X l
  (s, Some msg) (s', om)
Hprev: directly_observed_were_sent s
om = Some msg ∨ has_been_sent X s msg
message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
l: label X
s: state X
im: option message
s': state X
msg: message
Hptrans: input_constrained_transition X l (
  s, im) (s', Some msg)
Hprev: directly_observed_were_sent s
Some msg = Some msg ∨ has_been_sent X s msg
message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
l: label X
s: state X
im: option message
s': state X
om: option message
Hptrans: input_constrained_transition X l (
  s, im) (s', om)
Hprev: directly_observed_were_sent s
msg: message
H1: has_been_directly_observed X s msg
om = Some msg ∨ has_been_sent X s msg
  - (* by [no_equivocations], the incoming message [im] was previously sent *)message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
l: label X
s, s': state X
om: option message
msg: message
Hptrans: input_constrained_transition X l
  (s, Some msg) (s', om)
Hprev: directly_observed_were_sent s
om = Some msg ∨ has_been_sent X s msg
    destruct Hptrans as [Hv _].message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
l: label X
s, s': state X
om: option message
msg: message
Hv: input_valid (preloaded_with_all_messages_vlsm X)
  l (s, Some msg)
Hprev: directly_observed_were_sent s
om = Some msg ∨ has_been_sent X s msg
    by destruct (Henforced l s (Some msg) Hv); [right |].
  -message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
l: label X
s: state X
im: option message
s': state X
msg: message
Hptrans: input_constrained_transition X l (
  s, im) (s', Some msg)
Hprev: directly_observed_were_sent s
Some msg = Some msg ∨ has_been_sent X s msg by left.
  -message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
l: label X
s: state X
im: option message
s': state X
om: option message
Hptrans: input_constrained_transition X l (
  s, im) (s', om)
Hprev: directly_observed_were_sent s
msg: message
H1: has_been_directly_observed X s msg
om = Some msg ∨ has_been_sent X s msg by right; apply Hprev.
Qed.

Lemma directly_observed_were_sent_invariant :
  forall (s : state X),
    valid_state_prop X s -> directly_observed_were_sent s.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
∀ s : state X,
  valid_state_prop X s → directly_observed_were_sent s
Proof.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
∀ s : state X,
  valid_state_prop X s → directly_observed_were_sent s
  induction 1 using valid_state_prop_ind.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
s: state X
Hs: initial_state_prop s
directly_observed_were_sent s
message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
s': state X
l: label X
om, om': option message
s: state X
Ht: input_valid_transition X l (s, om) (s', om')
IHvalid_state_prop: directly_observed_were_sent s
directly_observed_were_sent s'
  -message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
s: state X
Hs: initial_state_prop s
directly_observed_were_sent s by apply directly_observed_were_sent_initial.
  -message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
s': state X
l: label X
om, om': option message
s: state X
Ht: input_valid_transition X l (s, om) (s', om')
IHvalid_state_prop: directly_observed_were_sent s
directly_observed_were_sent s' by eapply directly_observed_were_sent_preserved.
Qed.

If the validity function satisfies the no_equivocations constraint then it doesn't matter if we preload the composition with some initial messages, since all messages must be sent before being received, which means that one cannot use the new messages to create additional traces.

Lemma no_equivocations_preloaded_traces :
  forall (is : state (preloaded_with_all_messages_vlsm X)) (tr : list transition_item),
    finite_constrained_trace X is tr -> finite_valid_trace X is tr.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
∀ (is : state (preloaded_with_all_messages_vlsm X)) 
  (tr : list transition_item),
  finite_constrained_trace X is tr
  → finite_valid_trace X is tr
Proof.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
∀ (is : state (preloaded_with_all_messages_vlsm X)) 
  (tr : list transition_item),
  finite_constrained_trace X is tr
  → finite_valid_trace X is tr
  intros is tr Htr.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_constrained_trace X is tr
finite_valid_trace X is tr
  induction Htr using finite_valid_trace_rev_ind;
    [by cbn; apply finite_valid_trace_empty |].message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace
  (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l
  (finite_trace_last si tr, iom) (
  sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
IHHtr: finite_valid_trace X si tr
finite_valid_trace X si (tr ++ [x])
  destruct IHHtr as [IHtr His].message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace
  (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l
  (finite_trace_last si tr, iom) (
  sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
IHtr: finite_valid_trace_from X si tr
His: initial_state_prop si
finite_valid_trace X si (tr ++ [x])
  split; [| done].message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace
  (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l
  (finite_trace_last si tr, iom) (
  sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
IHtr: finite_valid_trace_from X si tr
His: initial_state_prop si
finite_valid_trace_from X si (tr ++ [x])
  rapply extend_right_finite_trace_from; [done |].message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace
  (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l
  (finite_trace_last si tr, iom) (
  sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
IHtr: finite_valid_trace_from X si tr
His: initial_state_prop si
input_valid_transition X l
  (finite_trace_last si tr, iom) (sf, oom)
  apply finite_valid_trace_last_pstate in IHtr as Hs.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace
  (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l
  (finite_trace_last si tr, iom) (
  sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
IHtr: finite_valid_trace_from X si tr
His: initial_state_prop si
Hs: valid_state_prop X (finite_trace_last si tr)
input_valid_transition X l
  (finite_trace_last si tr, iom) (sf, oom)
  repeat split; [done | | by apply Hx..].message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace
  (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l
  (finite_trace_last si tr, iom) (
  sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
IHtr: finite_valid_trace_from X si tr
His: initial_state_prop si
Hs: valid_state_prop X (finite_trace_last si tr)
option_valid_message_prop X iom
  destruct iom as [m |]; [| by apply option_valid_message_None].message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace
  (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
m: message
oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l
  (finite_trace_last si tr, Some m) (
  sf, oom)
x:= {|
  l := l;
  input := Some m;
  destination := sf;
  output := oom
|}: transition_item
IHtr: finite_valid_trace_from X si tr
His: initial_state_prop si
Hs: valid_state_prop X (finite_trace_last si tr)
option_valid_message_prop X (Some m)
  eapply sent_valid; [done |].message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace
  (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
m: message
oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l
  (finite_trace_last si tr, Some m) (
  sf, oom)
x:= {|
  l := l;
  input := Some m;
  destination := sf;
  output := oom
|}: transition_item
IHtr: finite_valid_trace_from X si tr
His: initial_state_prop si
Hs: valid_state_prop X (finite_trace_last si tr)
has_been_sent X (finite_trace_last si tr) m
  destruct Hx as [Hv _].message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace
  (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
m: message
oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: input_valid (preloaded_with_all_messages_vlsm X)
  l (finite_trace_last si tr, Some m)
x:= {|
  l := l;
  input := Some m;
  destination := sf;
  output := oom
|}: transition_item
IHtr: finite_valid_trace_from X si tr
His: initial_state_prop si
Hs: valid_state_prop X (finite_trace_last si tr)
has_been_sent X (finite_trace_last si tr) m
  by apply Henforced in Hv as [].
Qed.

Lemma preloaded_incl_no_equivocations :
  VLSM_incl (preloaded_with_all_messages_vlsm X) X.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
VLSM_incl (preloaded_with_all_messages_vlsm X) X
Proof.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
VLSM_incl (preloaded_with_all_messages_vlsm X) X
  specialize no_equivocations_preloaded_traces.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
(∀ (is : state (preloaded_with_all_messages_vlsm X)) 
   (tr : list transition_item),
   finite_constrained_trace X is tr
   → finite_valid_trace X is tr)
→ VLSM_incl (preloaded_with_all_messages_vlsm X) X
  clear -X.message: Type
X: VLSM message
(∀ (is : state (preloaded_with_all_messages_vlsm X)) 
   (tr : list transition_item),
   finite_constrained_trace X is tr
   → finite_valid_trace X is tr)
→ VLSM_incl (preloaded_with_all_messages_vlsm X) X destruct X as [T [S M]].message: Type
X: VLSM message
T: VLSMType message
S: state T → Prop
M:= {s : state T | S s}: Type
s0: Inhabited M
initial_message_prop: message → Prop
initial_message:= {m : message
| initial_message_prop m}: Type
transition: label T
→ state T * option message
  → state T * option message
valid: label T → state T * option message → Prop
(∀ (is : state
           (preloaded_with_all_messages_vlsm
              {|
                vlsm_type := T;
                vlsm_machine :=
                  {|
                    initial_state_prop := S;
                    s0 := s0;
                    initial_message_prop :=
                      initial_message_prop;
                    transition := transition;
                    valid := valid
                  |}
              |})) (tr : list transition_item),
   finite_constrained_trace
     {|
       vlsm_type := T;
       vlsm_machine :=
         {|
           initial_state_prop := S;
           s0 := s0;
           initial_message_prop :=
             initial_message_prop;
           transition := transition;
           valid := valid
         |}
     |} is tr
   → finite_valid_trace
       {|
         vlsm_type := T;
         vlsm_machine :=
           {|
             initial_state_prop := S;
             s0 := s0;
             initial_message_prop :=
               initial_message_prop;
             transition := transition;
             valid := valid
           |}
       |} is tr)
→ VLSM_incl
    (preloaded_with_all_messages_vlsm
       {|
         vlsm_type := T;
         vlsm_machine :=
           {|
             initial_state_prop := S;
             s0 := s0;
             initial_message_prop :=
               initial_message_prop;
             transition := transition;
             valid := valid
           |}
       |})
    {|
      vlsm_type := T;
      vlsm_machine :=
        {|
          initial_state_prop := S;
          s0 := s0;
          initial_message_prop := initial_message_prop;
          transition := transition;
          valid := valid
        |}
    |}
  by apply VLSM_incl_finite_traces_characterization.
Qed.

Lemma preloaded_eq_no_equivocations :
  VLSM_eq (preloaded_with_all_messages_vlsm X) X.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
VLSM_eq (preloaded_with_all_messages_vlsm X) X
Proof.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
VLSM_eq (preloaded_with_all_messages_vlsm X) X
  split.message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
VLSM_incl
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine := preloaded_with_all_messages_vlsm X
  |}
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine := X
  |}
message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
VLSM_incl
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine := X
  |}
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine := preloaded_with_all_messages_vlsm X
  |}
  -message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
VLSM_incl
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine := preloaded_with_all_messages_vlsm X
  |}
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine := X
  |} by apply preloaded_incl_no_equivocations.
  -message: Type
X: VLSM message
H: HasBeenSentCapability X
H0: HasBeenDirectlyObservedCapability X
Henforced: ∀ (l : label
         (preloaded_with_all_messages_vlsm
            X)) (s : state
                      (preloaded_with_all_messages_vlsm
                      X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
VLSM_incl
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine := X
  |}
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine := preloaded_with_all_messages_vlsm X
  |} by apply (vlsm_incl_preloaded_with_all_messages_vlsm X).
Qed.

End sec_no_equivocation_invariants.

Section sec_composite_no_equivocation.

Context
  {message : Type}
  `{finite.Finite index}
  (IM : index -> VLSM message)
  `{forall i, HasBeenSentCapability (IM i)}
  (constraint : composite_label IM -> composite_state IM * option message -> Prop)
  .

Definition sent_except_from
  (exception : message -> Prop) (es : composite_state IM) (iom : option message) : Prop :=
    from_option (fun im => composite_has_been_sent IM es im \/ exception im) True iom.

Definition composite_no_equivocations_except_from
  (exception : message -> Prop) (l : composite_label IM) (som : composite_state IM * option message)
  : Prop :=
    sent_except_from exception som.1 som.2.

The composite_no_equivocations constraint requires that messages being received must have been previously sent by a machine in the composition.

Definition composite_no_equivocations
  (l : composite_label IM) (som : composite_state IM * option message) : Prop :=
    composite_no_equivocations_except_from (fun m => False) l som.

Composite No-Equivocation Invariants

A VLSM composition whose constraint subsumes the no_equivocations constraint and also supports has_been_received (or has_been_directly_observed) obeys an invariant that any message that tests as has_been_received (resp. has_been_directly_observed) in a state also tests as has_been_sent in the same state.

Section sec_composite_no_equivocation_invariants.

Context
  `{forall i, HasBeenReceivedCapability (IM i)}
  (X := composite_vlsm IM constraint)
  (Hsubsumed : preloaded_constraint_subsumption (free_composite_vlsm IM) constraint
    composite_no_equivocations)
  .

Definition composite_directly_observed_were_sent (s : state (composite_type IM)) : Prop :=
  forall msg : message,
    composite_has_been_directly_observed IM s msg -> composite_has_been_sent IM s msg.

Lemma composite_directly_observed_were_sent_invariant :
  forall (s : state X),
    valid_state_prop X s -> composite_directly_observed_were_sent s.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
X:= composite_vlsm IM constraint: VLSM message
Hsubsumed: preloaded_constraint_subsumption
  (free_composite_vlsm IM) constraint
  composite_no_equivocations
∀ s : state X,
  valid_state_prop X s
  → composite_directly_observed_were_sent s
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
X:= composite_vlsm IM constraint: VLSM message
Hsubsumed: preloaded_constraint_subsumption
  (free_composite_vlsm IM) constraint
  composite_no_equivocations
∀ s : state X,
  valid_state_prop X s
  → composite_directly_observed_were_sent s
  intros s Hs m Hobs.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
X:= composite_vlsm IM constraint: VLSM message
Hsubsumed: preloaded_constraint_subsumption
  (free_composite_vlsm IM) constraint
  composite_no_equivocations
s: state X
Hs: valid_state_prop X s
m: message
Hobs: composite_has_been_directly_observed IM s m
composite_has_been_sent IM s m
  change (has_been_sent X s m).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
X:= composite_vlsm IM constraint: VLSM message
Hsubsumed: preloaded_constraint_subsumption
  (free_composite_vlsm IM) constraint
  composite_no_equivocations
s: state X
Hs: valid_state_prop X s
m: message
Hobs: composite_has_been_directly_observed IM s m
has_been_sent X s m
  apply (directly_observed_were_sent_invariant message X); [| done |].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
X:= composite_vlsm IM constraint: VLSM message
Hsubsumed: preloaded_constraint_subsumption
  (free_composite_vlsm IM) constraint
  composite_no_equivocations
s: state X
Hs: valid_state_prop X s
m: message
Hobs: composite_has_been_directly_observed IM s m
∀ (l : label (preloaded_with_all_messages_vlsm X)) 
  (s : state (preloaded_with_all_messages_vlsm X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om)
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
X:= composite_vlsm IM constraint: VLSM message
Hsubsumed: preloaded_constraint_subsumption
  (free_composite_vlsm IM) constraint
  composite_no_equivocations
s: state X
Hs: valid_state_prop X s
m: message
Hobs: composite_has_been_directly_observed IM s m
has_been_directly_observed X s m
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
X:= composite_vlsm IM constraint: VLSM message
Hsubsumed: preloaded_constraint_subsumption
  (free_composite_vlsm IM) constraint
  composite_no_equivocations
s: state X
Hs: valid_state_prop X s
m: message
Hobs: composite_has_been_directly_observed IM s m
∀ (l : label (preloaded_with_all_messages_vlsm X)) 
  (s : state (preloaded_with_all_messages_vlsm X)) 
  (om : option message),
  input_constrained X l (s, om)
  → no_equivocations X l (s, om) by intros l s0 om; apply Hsubsumed.
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
X:= composite_vlsm IM constraint: VLSM message
Hsubsumed: preloaded_constraint_subsumption
  (free_composite_vlsm IM) constraint
  composite_no_equivocations
s: state X
Hs: valid_state_prop X s
m: message
Hobs: composite_has_been_directly_observed IM s m
has_been_directly_observed X s m by apply composite_has_been_directly_observed_sent_received_iff.
Qed.

End sec_composite_no_equivocation_invariants.

Section sec_seeded_composite_vlsm_no_equivocation.

Preloading a VLSM composition with no equivocations constraint

When adding initial messages to a VLSM composition with a no equivocation constraint, we cannot simply use the preloaded_vlsm construct because the no-equivocation constraint must also be altered to reflect that the newly added initial messages are safe to be received at all times.

Section sec_seeded_composite_vlsm_no_equivocation_definition.

Context
  (seed : message -> Prop)
  .

Constraint is updated to also allow seeded messages.

Definition no_equivocations_additional_constraint_with_preloaded
  (l : composite_label IM) (som : composite_state IM * option message) : Prop :=
    composite_no_equivocations_except_from seed l som /\ constraint l som.

Definition composite_no_equivocation_vlsm_with_preloaded : VLSM message :=
  preloaded_vlsm (composite_vlsm IM no_equivocations_additional_constraint_with_preloaded) seed.

Definition free_composite_no_equivocation_vlsm_with_preloaded : VLSM message :=
  preloaded_vlsm (free_composite_vlsm IM) seed.

Lemma seeded_no_equivocation_incl_preloaded :
  VLSM_incl composite_no_equivocation_vlsm_with_preloaded
    (preloaded_with_all_messages_vlsm (free_composite_vlsm IM)).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
seed: message → Prop
VLSM_incl
  composite_no_equivocation_vlsm_with_preloaded
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
seed: message → Prop
VLSM_incl
  composite_no_equivocation_vlsm_with_preloaded
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  apply (VLSM_incl_trans _ (preloaded_with_all_messages_vlsm (composite_vlsm IM _))).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
seed: message → Prop
VLSM_incl
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded);
    vlsm_machine :=
      preloaded_vlsm_machine
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded)
        seed
  |}
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded);
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded)
  |}
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
seed: message → Prop
VLSM_incl
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded);
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded)
  |}
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded);
    vlsm_machine :=
      preloaded_vlsm_machine 
        (free_composite_vlsm IM) 
        (λ _ : message, True)
  |}
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
seed: message → Prop
VLSM_incl
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded);
    vlsm_machine :=
      preloaded_vlsm_machine
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded)
        seed
  |}
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded);
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded)
  |} by cbn; apply (@preloaded_vlsm_incl message (composite_vlsm IM _)).
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
seed: message → Prop
VLSM_incl
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded);
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded)
  |}
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm
        (composite_vlsm IM
           no_equivocations_additional_constraint_with_preloaded);
    vlsm_machine :=
      preloaded_vlsm_machine (free_composite_vlsm IM)
        (λ _ : message, True)
  |} by apply (preloaded_constraint_subsumption_incl_free (free_composite_vlsm IM)).
Qed.

End sec_seeded_composite_vlsm_no_equivocation_definition.

Adds a no-equivocations condition on top of an existing constraint.

Definition no_equivocations_additional_constraint
  (l : composite_label IM) (som : composite_state IM * option message) : Prop :=
    composite_no_equivocations l som /\ constraint l som.

Lemma false_composite_no_equivocation_vlsm_with_preloaded :
  VLSM_eq
    (composite_no_equivocation_vlsm_with_preloaded (fun m => False))
    (composite_vlsm IM no_equivocations_additional_constraint).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
VLSM_eq
  (composite_no_equivocation_vlsm_with_preloaded
     (λ _ : message, False))
  (composite_vlsm IM
     no_equivocations_additional_constraint)
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
VLSM_eq
  (composite_no_equivocation_vlsm_with_preloaded
     (λ _ : message, False))
  (composite_vlsm IM
     no_equivocations_additional_constraint)
  unfold composite_no_equivocation_vlsm_with_preloaded.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
VLSM_eq
  (preloaded_vlsm
     (composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False)))
     (λ _ : message, False))
  (composite_vlsm IM
     no_equivocations_additional_constraint)
  apply VLSM_eq_trans with
    (composite_vlsm IM (no_equivocations_additional_constraint_with_preloaded (fun _ =>  False))).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
VLSM_eq
  {|
    vlsm_type :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False));
    vlsm_machine :=
      preloaded_vlsm_machine
        (composite_vlsm IM
           (no_equivocations_additional_constraint_with_preloaded
              (λ _ : message, False)))
        (λ _ : message, False)
  |}
  {|
    vlsm_type :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False));
    vlsm_machine :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False))
  |}
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
VLSM_eq
  {|
    vlsm_type :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False));
    vlsm_machine :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False))
  |}
  {|
    vlsm_type :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False));
    vlsm_machine :=
      constrained_vlsm_machine
        (free_composite_vlsm IM)
        no_equivocations_additional_constraint
  |}
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
VLSM_eq
  {|
    vlsm_type :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False));
    vlsm_machine :=
      preloaded_vlsm_machine
        (composite_vlsm IM
           (no_equivocations_additional_constraint_with_preloaded
              (λ _ : message, False)))
        (λ _ : message, False)
  |}
  {|
    vlsm_type :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False));
    vlsm_machine :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False))
  |} by apply VLSM_eq_sym, vlsm_is_preloaded_with_False.
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
VLSM_eq
  {|
    vlsm_type :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False));
    vlsm_machine :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False))
  |}
  {|
    vlsm_type :=
      composite_vlsm IM
        (no_equivocations_additional_constraint_with_preloaded
           (λ _ : message, False));
    vlsm_machine :=
      constrained_vlsm_machine
        (free_composite_vlsm IM)
        no_equivocations_additional_constraint
  |} by split; apply (constraint_subsumption_incl (free_composite_vlsm IM));
      intros l [s [m |]] Hpv; apply Hpv.
Qed.

End sec_seeded_composite_vlsm_no_equivocation.

End sec_composite_no_equivocation.