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 ProjectionTraces Validator.[Loading ML file coq-itauto.plugin ... done]
From VLSM.Core Require Import PreloadedVLSM.

Core: VLSM Byzantine Traces

In this section, we introduce two definitions of Byzantine traces, prove that they are equivalent (lemma byzantine_alt_byzantine_iff), and then prove that both definitions are equivalent with the definition of a valid trace in the corresponding preloaded VLSM (lemmas byzantine_preloaded_with_all_messages and preloaded_with_all_messages_alt_eq).

Note that, contrary to what one might think, the byzantine trace property does not only capture traces exhibiting byzantine behavior, but also all valid traces (consequence of lemma vlsm_incl_preloaded_with_all_messages_vlsm). Therefore to avoid confusion we will call proper byzantine traces, or traces exhibiting byzantine behavior the collection of traces with the byzantine trace property but without the valid trace property.

In the remainder of this section, we fix a VLSM M.

Definition and basic properties

Section sec_byzantine_traces.

Context
  {message : Type}
  (M : VLSM message)
  .

The first definition says that a trace has the byzantine trace property if it is the projection of a trace which can be obtained by freely composing M with an arbitrary VLSM M' (over the same set of messages).

Below, binary_free_composition_fst represents the projection of the free composition of M and M' to the component corresponding to M.

Definition byzantine_trace_prop (tr : Trace M) : Prop :=
  exists (M' : VLSM message),
    valid_trace_prop (binary_free_composition_fst M M') tr.

The first result says that all traces with the byzantine trace property for a VLSM M are traces of the preloaded_with_all_messages_vlsm associated to M.

Lemma byzantine_preloaded_with_all_messages :
  forall (tr : Trace M),
    byzantine_trace_prop tr ->
    constrained_trace_prop M tr.message: Type
M: VLSM message
∀ tr : Trace,
  byzantine_trace_prop tr
  → constrained_trace_prop M tr
Proof.message: Type
M: VLSM message
∀ tr : Trace,
  byzantine_trace_prop tr
  → constrained_trace_prop M tr
  intros tr [M' Htr]; cbn in Htr.message: Type
M: VLSM message
tr: Trace
M': VLSM message
Htr: valid_trace_prop
  (binary_free_composition_fst M M') tr
constrained_trace_prop M tr
  by apply proj_preloaded_with_all_messages_incl in Htr.
Qed.

An alternative definition

The alternative definition of byzantine trace property relies on the composition of the VLSM with a special VLSM which can produce all messages.

We will define its type (emit_any_message_vlsm_type) and the VLSM itself (emit_any_message_vlsm) below.

The labels of emit_any_message_vlsm are its messages and there is a single state.

Definition emit_any_message_vlsm_type : VLSMType message :=
{|
  label := message;
  state := unit;
|}.

To define the VLSM, we need to prove that the type of states is inhabited, since we need an initial state.

Program Definition emit_any_message_vlsm_s0 : {_ : state emit_any_message_vlsm_type | True} :=
  exist _ tt _.
Next Obligation.message: Type
M: VLSM message
(λ _ : state emit_any_message_vlsm_type, True) ()
Proof.message: Type
M: VLSM message
(λ _ : state emit_any_message_vlsm_type, True) () done. Defined.

#[export] Instance emit_any_message_vlsm_state_inh :
  Inhabited {_ : state emit_any_message_vlsm_type | True} :=
    populate emit_any_message_vlsm_s0.

The definition of emit_any_message_vlsm_machine says that:

all states are initial
no messages are initial
the single state is the initial state
the transition function generates the message given as the label
all transitions are valid

Definition emit_any_message_vlsm_machine : VLSMMachine emit_any_message_vlsm_type :=
{|
  initial_state_prop := fun _ => True;
  initial_message_prop := fun _ => False;
  s0 := emit_any_message_vlsm_state_inh;
  transition := fun l _ => (tt, Some l);
  valid := fun _ _ => True;
|}.

Definition emit_any_message_vlsm : VLSM message :=
  mk_vlsm emit_any_message_vlsm_machine.

Using the VLSM defined above, we can define the alternative byzantine trace property of a trace tr for the VLSM M as being a trace in the projection of the free composition between M and the emit_any_message_vlsm, to the component corresponding to M.

Definition alternate_byzantine_trace_prop (tr : Trace M) : Prop :=
  valid_trace_prop (binary_free_composition_fst M emit_any_message_vlsm) tr.

Since the byzantine trace property was referring to the free composition with any other VLSM, we can instantiate that definition to the emit_any_message_vlsm to derive that a trace with the alternative byzantine trace property also has the byzantine trace property.

Lemma byzantine_alt_byzantine :
  forall (tr : Trace M),
    alternate_byzantine_trace_prop tr ->
    byzantine_trace_prop tr.message: Type
M: VLSM message
∀ tr : Trace,
  alternate_byzantine_trace_prop tr
  → byzantine_trace_prop tr
Proof.message: Type
M: VLSM message
∀ tr : Trace,
  alternate_byzantine_trace_prop tr
  → byzantine_trace_prop tr
  by exists emit_any_message_vlsm.
Qed.

Equivalence between the two Byzantine trace definitions

In this section we prove that the alternate_byzantine_trace_prop is equivalent to byzantine_trace_prop.

Since we have already proven that alternate_byzantine_trace_prop implies byzantine_trace_prop (lemma byzantine_alt_byzantine), and since we know that the traces satisfying byzantine_trace_prop are valid traces for the preloaded_with_all_messages_vlsm, to prove the equivalence it is enough to close the circle by proving the VLSM inclusion between the preloaded_with_all_messages_vlsm and the projection VLSM used to define alternate_byzantine_trace_prop.

Section sec_preloaded_with_all_messages_byzantine_alt.

Let Alt denote the free composition of M with the emit_any_message_vlsm, and let Alt1 denote the projection of Alt to the component of M.

Context
  (Alt1 := binary_free_composition_fst M emit_any_message_vlsm)
  (Alt := binary_free_composition M emit_any_message_vlsm)
  .

First, note that using the results above it is easy to prove the inclusion of Alt1 into Preloaded.

Lemma alt_preloaded_with_all_messages_incl :
  VLSM_incl Alt1 (preloaded_with_all_messages_vlsm M).message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
VLSM_incl Alt1 (preloaded_with_all_messages_vlsm M)
Proof.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
VLSM_incl Alt1 (preloaded_with_all_messages_vlsm M)
  by intros t Hvt; apply byzantine_preloaded_with_all_messages, byzantine_alt_byzantine.
Qed.

To prove the reverse inclusion (between preloaded M and Alt1) we will use the basic_VLSM_incl meta-result about proving inclusions between VLSMs which states that:

if all valid messages in the first are valid messages in the second, and
if all valid states in the first are also valid states in the second, and
if all input_valid_transitions in the first are also input_valid_transitions in the second, then
the first VLSM is included in the second.

First note that all messages are valid for Alt, as emit_any_message_vlsm can generate any message without changing state.

Lemma alt_option_valid_message :
  forall (om : option message),
    option_valid_message_prop Alt om.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
∀ om : option message,
  option_valid_message_prop Alt om
Proof.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
∀ om : option message,
  option_valid_message_prop Alt om
  intros [m |]; [| by apply option_valid_message_None].message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
m: message
option_valid_message_prop Alt (Some m)
  pose (s := ``(vs0 Alt)).message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
m: message
s:= `(vs0 Alt): state Alt
option_valid_message_prop Alt (Some m)
  exists s.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
m: message
s:= `(vs0 Alt): state Alt
valid_state_message_prop Alt s (Some m)
  eapply (valid_generated_state_message Alt)
    with s None s None (existT second _);
    [by apply valid_initial_state, proj2_sig.. | by split |].message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
m: message
s:= `(vs0 Alt): state Alt
transition (existT second ?Goal) (s, None) =
(s, Some m)
  by cbn; state_update_simpl.
Qed.

In the projection, all messages are valid.

Lemma alt_proj_option_valid_message :
  forall (m : option message),
    option_valid_message_prop Alt1 m.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
∀ m : option message, option_valid_message_prop Alt1 m
Proof.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
∀ m : option message, option_valid_message_prop Alt1 m by apply any_message_is_valid_in_preloaded. Qed.

Next we define the "lifting" of a state s from M to Alt, by simply setting to s the corresponding component of the initial (composite) state s0 of Alt.

Definition lifted_alt_state (s : state M) : state Alt :=
  lift_to_composite_state' (binary_IM M emit_any_message_vlsm) first s.

Lifting a constrained state of M we obtain a valid state of Alt.

Lemma preloaded_alt_valid_state :
  forall (sj : state M) (om : option message),
    constrained_state_message_prop M sj om ->
    valid_state_prop Alt (lifted_alt_state sj).message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
∀ (sj : state M) (om : option message),
  constrained_state_message_prop M sj om
  → valid_state_prop Alt (lifted_alt_state sj)
Proof.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
∀ (sj : state M) (om : option message),
  constrained_state_message_prop M sj om
  → valid_state_prop Alt (lifted_alt_state sj)
  intros sj om Hp.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
sj: state M
om: option message
Hp: constrained_state_message_prop M sj om
valid_state_prop Alt (lifted_alt_state sj)
  assert (Hsj : constrained_state_prop M sj)
    by (exists om; done); clear Hp.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
sj: state M
om: option message
Hsj: constrained_state_prop M sj
valid_state_prop Alt (lifted_alt_state sj)
  induction Hsj using valid_state_prop_ind;
    [by apply initial_state_is_valid; intros [] |].message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
om: option message
s': state (preloaded_with_all_messages_vlsm M)
l: label (preloaded_with_all_messages_vlsm M)
om0, om': option message
s: state (preloaded_with_all_messages_vlsm M)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm M) l (
  s, om0) (s', om')
IHHsj: valid_state_prop Alt (lifted_alt_state s)
valid_state_prop Alt (lifted_alt_state s')
  exists om'.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
om: option message
s': state (preloaded_with_all_messages_vlsm M)
l: label (preloaded_with_all_messages_vlsm M)
om0, om': option message
s: state (preloaded_with_all_messages_vlsm M)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm M) l (
  s, om0) (s', om')
IHHsj: valid_state_prop Alt (lifted_alt_state s)
valid_state_message_prop Alt (lifted_alt_state s') om'
  eapply (@input_valid_transition_outputs_valid_state_message _ Alt (existT first l)
    (lifted_alt_state s) (lifted_alt_state s') om0).message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
om: option message
s': state (preloaded_with_all_messages_vlsm M)
l: label (preloaded_with_all_messages_vlsm M)
om0, om': option message
s: state (preloaded_with_all_messages_vlsm M)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm M) l (
  s, om0) (s', om')
IHHsj: valid_state_prop Alt (lifted_alt_state s)
input_valid_transition Alt (existT first l)
  (lifted_alt_state s, om0) (lifted_alt_state s', om')
  repeat split; cbn; [by apply IHHsj | by apply alt_option_valid_message | by apply Ht |].message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
om: option message
s': state (preloaded_with_all_messages_vlsm M)
l: label (preloaded_with_all_messages_vlsm M)
om0, om': option message
s: state (preloaded_with_all_messages_vlsm M)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm M) l (
  s, om0) (s', om')
IHHsj: valid_state_prop Alt (lifted_alt_state s)
(let (si', om') :=
   transition l (lifted_alt_state s first, om0) in
 (state_update (binary_IM M emit_any_message_vlsm)
    (lifted_alt_state s) first si', om')) =
(lifted_alt_state s', om')
  unfold lifted_alt_state, lift_to_composite_state', lift_to_composite_state.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
om: option message
s': state (preloaded_with_all_messages_vlsm M)
l: label (preloaded_with_all_messages_vlsm M)
om0, om': option message
s: state (preloaded_with_all_messages_vlsm M)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm M) l (
  s, om0) (s', om')
IHHsj: valid_state_prop Alt (lifted_alt_state s)
(let (si', om') :=
   transition l
     (state_update (binary_IM M emit_any_message_vlsm)
        (`(composite_s0
             (binary_IM M emit_any_message_vlsm)))
        first s first, om0) in
 (state_update (binary_IM M emit_any_message_vlsm)
    (state_update (binary_IM M emit_any_message_vlsm)
       (`(composite_s0
            (binary_IM M emit_any_message_vlsm)))
       first s) first si', om')) =
(state_update (binary_IM M emit_any_message_vlsm)
   (`(composite_s0 (binary_IM M emit_any_message_vlsm)))
   first s', om')
  state_update_simpl; cbn in *.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
om: option message
s': state M
l: label M
om0, om': option message
s: state M
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm M) l (
  s, om0) (s', om')
IHHsj: valid_state_prop Alt (lifted_alt_state s)
(let (si', om') := transition l (s, om0) in
 (state_update (binary_IM M emit_any_message_vlsm)
    (state_update (binary_IM M emit_any_message_vlsm)
       (λ n : binary_index,
          `(vs0 (binary_IM M emit_any_message_vlsm n)))
       first s) first si', om')) =
(state_update (binary_IM M emit_any_message_vlsm)
   (λ n : binary_index,
      `(vs0 (binary_IM M emit_any_message_vlsm n)))
   first s', om')
  destruct Ht as [_ Ht]; cbn in Ht; rewrite Ht.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
om: option message
s': state M
l: label M
om0, om': option message
s: state M
Ht: transition l (s, om0) = (s', om')
IHHsj: valid_state_prop Alt (lifted_alt_state s)
(state_update (binary_IM M emit_any_message_vlsm)
   (state_update (binary_IM M emit_any_message_vlsm)
      (λ n : binary_index,
         `(vs0 (binary_IM M emit_any_message_vlsm n)))
      first s) first s', om') =
(state_update (binary_IM M emit_any_message_vlsm)
   (λ n : binary_index,
      `(vs0 (binary_IM M emit_any_message_vlsm n)))
   first s', om')
  by rewrite state_update_twice.
Qed.

Finally, we can use basic_VLSM_incl together with the results above to show that Preloaded is included in Alt1.

Lemma preloaded_with_all_messages_alt_incl :
  VLSM_incl (preloaded_with_all_messages_vlsm M) Alt1.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
VLSM_incl (preloaded_with_all_messages_vlsm M) Alt1
Proof.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
VLSM_incl (preloaded_with_all_messages_vlsm M) Alt1
  apply (basic_VLSM_incl _ Alt1); intro; intros;
    [done | by apply alt_proj_option_valid_message | | by apply H].message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
l: label
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
om: option message
Hv: input_valid
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} l (s, om)
HsY: valid_state_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  (id s)
HomY: option_valid_message_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  om
valid (id l) (id s, om)
  exists (lifted_alt_state s).message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
l: label
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
om: option message
Hv: input_valid
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} l (s, om)
HsY: valid_state_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  (id s)
HomY: option_valid_message_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  om
lifted_alt_state s first = id s
∧ input_valid
    (composite_vlsm
       (binary_IM M emit_any_message_vlsm)
       (free_constraint
          (binary_IM M emit_any_message_vlsm)))
    (existT first (id l)) (lifted_alt_state s, om)
  split; [done |].message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
l: label
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
om: option message
Hv: input_valid
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} l (s, om)
HsY: valid_state_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  (id s)
HomY: option_valid_message_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  om
input_valid
  (composite_vlsm (binary_IM M emit_any_message_vlsm)
     (free_constraint
        (binary_IM M emit_any_message_vlsm)))
  (existT first (id l)) (lifted_alt_state s, om)
  destruct Hv as [[_om Hps] [Hpm Hv]].message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
l: label
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
om, _om: option message
Hps: valid_state_message_prop
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} s _om
Hpm: option_valid_message_prop
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} om
Hv: valid l (s, om)
HsY: valid_state_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  (id s)
HomY: option_valid_message_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  om
input_valid
  (composite_vlsm (binary_IM M emit_any_message_vlsm)
     (free_constraint
        (binary_IM M emit_any_message_vlsm)))
  (existT first (id l)) (lifted_alt_state s, om)
  split_and!; [| | done].message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
l: label
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
om, _om: option message
Hps: valid_state_message_prop
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} s _om
Hpm: option_valid_message_prop
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} om
Hv: valid l (s, om)
HsY: valid_state_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  (id s)
HomY: option_valid_message_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  om
valid_state_prop
  (composite_vlsm (binary_IM M emit_any_message_vlsm)
     (free_constraint
        (binary_IM M emit_any_message_vlsm)))
  (lifted_alt_state s)
message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
l: label
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
om, _om: option message
Hps: valid_state_message_prop
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} s _om
Hpm: option_valid_message_prop
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} om
Hv: valid l (s, om)
HsY: valid_state_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  (id s)
HomY: option_valid_message_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  om
option_valid_message_prop
  (composite_vlsm (binary_IM M emit_any_message_vlsm)
     (free_constraint
        (binary_IM M emit_any_message_vlsm))) om
  -message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
l: label
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
om, _om: option message
Hps: valid_state_message_prop
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} s _om
Hpm: option_valid_message_prop
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} om
Hv: valid l (s, om)
HsY: valid_state_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  (id s)
HomY: option_valid_message_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  om
valid_state_prop
  (composite_vlsm (binary_IM M emit_any_message_vlsm)
     (free_constraint
        (binary_IM M emit_any_message_vlsm)))
  (lifted_alt_state s) by apply preloaded_alt_valid_state in Hps.
  -message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
l: label
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |}
om, _om: option message
Hps: valid_state_message_prop
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} s _om
Hpm: option_valid_message_prop
  {|
    vlsm_type := Alt1;
    vlsm_machine :=
      preloaded_vlsm_machine M
        (λ _ : message, True)
  |} om
Hv: valid l (s, om)
HsY: valid_state_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  (id s)
HomY: option_valid_message_prop
  {| vlsm_type := Alt1; vlsm_machine := Alt1 |}
  om
option_valid_message_prop
  (composite_vlsm (binary_IM M emit_any_message_vlsm)
     (free_constraint
        (binary_IM M emit_any_message_vlsm))) om by apply alt_option_valid_message.
Qed.

Hence, Preloaded and Alt1 are actually trace-equivalent.

Lemma preloaded_with_all_messages_alt_eq :
  VLSM_eq (preloaded_with_all_messages_vlsm M) Alt1.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
VLSM_eq (preloaded_with_all_messages_vlsm M) Alt1
Proof.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
VLSM_eq (preloaded_with_all_messages_vlsm M) Alt1
  split.message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
VLSM_incl
  {|
    vlsm_type := preloaded_with_all_messages_vlsm M;
    vlsm_machine := preloaded_with_all_messages_vlsm M
  |}
  {|
    vlsm_type := preloaded_with_all_messages_vlsm M;
    vlsm_machine := Alt1
  |}
message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
VLSM_incl
  {|
    vlsm_type := preloaded_with_all_messages_vlsm M;
    vlsm_machine := Alt1
  |}
  {|
    vlsm_type := preloaded_with_all_messages_vlsm M;
    vlsm_machine := preloaded_with_all_messages_vlsm M
  |}
  -message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
VLSM_incl
  {|
    vlsm_type := preloaded_with_all_messages_vlsm M;
    vlsm_machine := preloaded_with_all_messages_vlsm M
  |}
  {|
    vlsm_type := preloaded_with_all_messages_vlsm M;
    vlsm_machine := Alt1
  |} by apply preloaded_with_all_messages_alt_incl.
  -message: Type
M: VLSM message
Alt1:= binary_free_composition_fst M
  emit_any_message_vlsm: VLSM message
Alt:= binary_free_composition M emit_any_message_vlsm: VLSM message
VLSM_incl
  {|
    vlsm_type := preloaded_with_all_messages_vlsm M;
    vlsm_machine := Alt1
  |}
  {|
    vlsm_type := preloaded_with_all_messages_vlsm M;
    vlsm_machine := preloaded_with_all_messages_vlsm M
  |} by apply alt_preloaded_with_all_messages_incl.
Qed.

End sec_preloaded_with_all_messages_byzantine_alt.

Finally, we can conclude that the two definitions for byzantine traces are equivalent.

Lemma byzantine_alt_byzantine_iff :
  forall (tr : Trace M),
    alternate_byzantine_trace_prop tr <-> byzantine_trace_prop tr.message: Type
M: VLSM message
∀ tr : Trace,
  alternate_byzantine_trace_prop tr
  ↔ byzantine_trace_prop tr
Proof.message: Type
M: VLSM message
∀ tr : Trace,
  alternate_byzantine_trace_prop tr
  ↔ byzantine_trace_prop tr
  split; intros.message: Type
M: VLSM message
tr: Trace
H: alternate_byzantine_trace_prop tr
byzantine_trace_prop tr
message: Type
M: VLSM message
tr: Trace
H: byzantine_trace_prop tr
alternate_byzantine_trace_prop tr
  -message: Type
M: VLSM message
tr: Trace
H: alternate_byzantine_trace_prop tr
byzantine_trace_prop tr by apply byzantine_alt_byzantine.
  -message: Type
M: VLSM message
tr: Trace
H: byzantine_trace_prop tr
alternate_byzantine_trace_prop tr by apply preloaded_with_all_messages_alt_incl, byzantine_preloaded_with_all_messages.
Qed.

End sec_byzantine_traces.

Byzantine fault tolerance for a single validator

Given that projections of composition of validator VLSMs are equivalent to their corresponding VLSM preloaded with all messages (preloaded_with_all_messages_validating_proj_eq), we can derive that for validators, all their byzantine traces are included in the valid traces of their projection from the composition.

Section sec_single_validator_byzantine_traces.

Context
  {message : Type}
  `{EqDecision index}
  (IM : index -> VLSM message)
  (constraint : composite_label IM -> composite_state IM  * option message -> Prop)
  (i : index)
  (Hvalidator : component_projection_validator_prop IM constraint i)
  .

Lemma validator_component_byzantine_fault_tolerance :
  forall (tr : Trace),
    byzantine_trace_prop (IM i) tr ->
    valid_trace_prop (pre_composite_vlsm_induced_projection_validator IM constraint i) tr.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
i: index
Hvalidator: component_projection_validator_prop IM
  constraint i
∀ tr : Trace,
  byzantine_trace_prop (IM i) tr
  → valid_trace_prop
      (pre_composite_vlsm_induced_projection_validator
         IM constraint i) tr
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
i: index
Hvalidator: component_projection_validator_prop IM
  constraint i
∀ tr : Trace,
  byzantine_trace_prop (IM i) tr
  → valid_trace_prop
      (pre_composite_vlsm_induced_projection_validator
         IM constraint i) tr
  intros tr Htr.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
i: index
Hvalidator: component_projection_validator_prop IM
  constraint i
tr: Trace
Htr: byzantine_trace_prop (IM i) tr
valid_trace_prop
  (pre_composite_vlsm_induced_projection_validator IM
     constraint i) tr
  eapply VLSM_incl_valid_trace.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
i: index
Hvalidator: component_projection_validator_prop IM
  constraint i
tr: Trace
Htr: byzantine_trace_prop (IM i) tr
VLSM_incl_part ?MX
  (preloaded_vlsm_machine
     (composite_vlsm_induced_projection_validator IM
        constraint i) (λ _ : message, True))
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
i: index
Hvalidator: component_projection_validator_prop IM
  constraint i
tr: Trace
Htr: byzantine_trace_prop (IM i) tr
valid_trace_prop
  {|
    vlsm_type :=
      composite_vlsm_induced_projection_validator IM
        constraint i;
    vlsm_machine := ?MX
  |} tr
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
i: index
Hvalidator: component_projection_validator_prop IM
  constraint i
tr: Trace
Htr: byzantine_trace_prop (IM i) tr
VLSM_incl_part ?MX
  (preloaded_vlsm_machine
     (composite_vlsm_induced_projection_validator IM
        constraint i) (λ _ : message, True)) by apply preloaded_with_all_messages_validator_component_proj_incl.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
i: index
Hvalidator: component_projection_validator_prop IM
  constraint i
tr: Trace
Htr: byzantine_trace_prop (IM i) tr
valid_trace_prop
  {|
    vlsm_type :=
      composite_vlsm_induced_projection_validator IM
        constraint i;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm (IM i)
  |} tr by apply byzantine_preloaded_with_all_messages in Htr.
Qed.

End sec_single_validator_byzantine_traces.

Byzantine fault tolerance for a composition of validators

In this section we show that if all components of a composite VLSM X satisfy projection_validator_prop, then its byzantine traces (that is, traces obtained upon placing this composition in any, possibly adversarial, context) are valid traces of X.

Section sec_composite_validator_byzantine_traces.

Let us fix an indexed set of VLSMs IM and their constrained composition X, and let PreloadedX be the preloaded_with_all_messages_vlsm associated to X.

Context
  {message : Type}
  `{EqDecision index}
  (IM : index -> VLSM message)
  (constraint : composite_label IM -> composite_state IM  * option message -> Prop)
  (X := composite_vlsm IM constraint)
  (Hvalidator : forall i : index, component_message_validator_prop IM constraint i)
  .

Since we know that preloaded X contains precisely the byzantine traces of X, we just need to show that preloaded X is included in X to prove our main result.

Lemma validator_preloaded_with_all_messages_incl :
  VLSM_incl (preloaded_with_all_messages_vlsm X) X.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
VLSM_incl (preloaded_with_all_messages_vlsm X) X
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
VLSM_incl (preloaded_with_all_messages_vlsm X) X
  apply VLSM_incl_finite_traces_characterization.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
∀ (s : state
         {|
           vlsm_type :=
             preloaded_with_all_messages_vlsm X;
           vlsm_machine :=
             preloaded_vlsm_machine X
               (λ _ : message, True)
         |}) (tr : list transition_item),
  finite_valid_trace
    {|
      vlsm_type := preloaded_with_all_messages_vlsm X;
      vlsm_machine :=
        preloaded_vlsm_machine X (λ _ : message, True)
    |} s tr
  → finite_valid_trace
      {|
        vlsm_type :=
          preloaded_with_all_messages_vlsm X;
        vlsm_machine :=
          ConstrainedVLSM.constrained_vlsm_machine
            (free_composite_vlsm IM) constraint
      |} s tr
  intros s tr Htr.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
finite_valid_trace
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} s tr
  split; [| by apply Htr].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
finite_valid_trace_from
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} s tr
  destruct Htr as [Htr Hs].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
Hs: initial_state_prop s
finite_valid_trace_from
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} s tr
  induction Htr using finite_valid_trace_from_rev_ind;
    [by apply (finite_valid_trace_from_empty X), initial_state_is_valid |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
iom, oom: option message
l: label
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
Hx: input_valid_transition
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} l (finite_trace_last s tr, iom) (
  sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: initial_state_prop s
→ finite_valid_trace_from
    {|
      vlsm_type :=
        preloaded_with_all_messages_vlsm X;
      vlsm_machine :=
        ConstrainedVLSM.constrained_vlsm_machine
          (free_composite_vlsm IM) constraint
    |} s tr
finite_valid_trace_from
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} s (tr ++ [x])
  apply (extend_right_finite_trace_from X); [by apply IHHtr |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
iom, oom: option message
l: label
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
Hx: input_valid_transition
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} l (finite_trace_last s tr, iom) (
  sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: initial_state_prop s
→ finite_valid_trace_from
    {|
      vlsm_type :=
        preloaded_with_all_messages_vlsm X;
      vlsm_machine :=
        ConstrainedVLSM.constrained_vlsm_machine
          (free_composite_vlsm IM) constraint
    |} s tr
input_valid_transition X l
  (finite_trace_last s tr, iom) (sf, oom)
  destruct Hx as [Hvx Htx].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
iom, oom: option message
l: label
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
Hvx: input_valid
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} l (finite_trace_last s tr, iom)
Htx: transition l (finite_trace_last s tr, iom) =
(sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: initial_state_prop s
→ finite_valid_trace_from
    {|
      vlsm_type :=
        preloaded_with_all_messages_vlsm X;
      vlsm_machine :=
        ConstrainedVLSM.constrained_vlsm_machine
          (free_composite_vlsm IM) constraint
    |} s tr
input_valid_transition X l
  (finite_trace_last s tr, iom) (sf, oom)
  split; [| done].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
iom, oom: option message
l: label
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
Hvx: input_valid
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} l (finite_trace_last s tr, iom)
Htx: transition l (finite_trace_last s tr, iom) =
(sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: initial_state_prop s
→ finite_valid_trace_from
    {|
      vlsm_type :=
        preloaded_with_all_messages_vlsm X;
      vlsm_machine :=
        ConstrainedVLSM.constrained_vlsm_machine
          (free_composite_vlsm IM) constraint
    |} s tr
input_valid X l (finite_trace_last s tr, iom)
  apply finite_valid_trace_last_pstate in IHHtr; [| done].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
iom, oom: option message
l: label
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
Hvx: input_valid
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} l (finite_trace_last s tr, iom)
Htx: transition l (finite_trace_last s tr, iom) =
(sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} (finite_trace_last s tr)
input_valid X l (finite_trace_last s tr, iom)
  repeat split; [done | | by apply Hvx..].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
iom, oom: option message
l: label
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
Hvx: input_valid
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} l (finite_trace_last s tr, iom)
Htx: transition l (finite_trace_last s tr, iom) =
(sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} (finite_trace_last s tr)
option_valid_message_prop X iom
  destruct Hvx as (Hlst & _ & Hv & _).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
iom, oom: option message
l: label
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
Hlst: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (finite_trace_last s tr)
Hv: valid l (finite_trace_last s tr, iom)
Htx: transition l (finite_trace_last s tr, iom) =
(sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} (finite_trace_last s tr)
option_valid_message_prop X iom
  destruct l as [i li].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
iom, oom: option message
i: index
li: label (IM i)
Hlst: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (finite_trace_last s tr)
Hv: valid (existT i li) (finite_trace_last s tr, iom)
Htx: transition (existT i li)
  (finite_trace_last s tr, iom) = (
sf, oom)
x:= {|
  l := existT i li;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} (finite_trace_last s tr)
option_valid_message_prop X iom
  destruct iom as [im |]; [| by apply option_valid_message_None].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
im: message
oom: option message
i: index
li: label (IM i)
Hlst: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (finite_trace_last s tr)
Hv: valid (existT i li)
  (finite_trace_last s tr, Some im)
Htx: transition (existT i li)
  (finite_trace_last s tr, Some im) = (
sf, oom)
x:= {|
  l := existT i li;
  input := Some im;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} (finite_trace_last s tr)
option_valid_message_prop X (Some im)
  eapply Hvalidator.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
im: message
oom: option message
i: index
li: label (IM i)
Hlst: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (finite_trace_last s tr)
Hv: valid (existT i li)
  (finite_trace_last s tr, Some im)
Htx: transition (existT i li)
  (finite_trace_last s tr, Some im) = (
sf, oom)
x:= {|
  l := existT i li;
  input := Some im;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} (finite_trace_last s tr)
input_constrained (IM ?i) ?li (?si, Some im)
  split_and!; [| | by cbn; apply Hv].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
im: message
oom: option message
i: index
li: label (IM i)
Hlst: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (finite_trace_last s tr)
Hv: valid (existT i li)
  (finite_trace_last s tr, Some im)
Htx: transition (existT i li)
  (finite_trace_last s tr, Some im) = (
sf, oom)
x:= {|
  l := existT i li;
  input := Some im;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} (finite_trace_last s tr)
valid_state_prop
  (preloaded_with_all_messages_vlsm (IM i))
  (finite_trace_last s tr i)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
im: message
oom: option message
i: index
li: label (IM i)
Hlst: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (finite_trace_last s tr)
Hv: valid (existT i li)
  (finite_trace_last s tr, Some im)
Htx: transition (existT i li)
  (finite_trace_last s tr, Some im) = (
sf, oom)
x:= {|
  l := existT i li;
  input := Some im;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} (finite_trace_last s tr)
option_valid_message_prop
  (preloaded_with_all_messages_vlsm (IM i)) 
  (Some im)
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
im: message
oom: option message
i: index
li: label (IM i)
Hlst: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (finite_trace_last s tr)
Hv: valid (existT i li)
  (finite_trace_last s tr, Some im)
Htx: transition (existT i li)
  (finite_trace_last s tr, Some im) = (
sf, oom)
x:= {|
  l := existT i li;
  input := Some im;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} (finite_trace_last s tr)
valid_state_prop
  (preloaded_with_all_messages_vlsm (IM i))
  (finite_trace_last s tr i) by eapply valid_state_project_preloaded_to_preloaded in Hlst.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
im: message
oom: option message
i: index
li: label (IM i)
Hlst: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (finite_trace_last s tr)
Hv: valid (existT i li)
  (finite_trace_last s tr, Some im)
Htx: transition (existT i li)
  (finite_trace_last s tr, Some im) = (
sf, oom)
x:= {|
  l := existT i li;
  input := Some im;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} (finite_trace_last s tr)
option_valid_message_prop
  (preloaded_with_all_messages_vlsm (IM i)) (Some im) eexists _.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
s: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
tr: list transition_item
Htr: finite_valid_trace_from
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} s tr
sf: state
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |}
im: message
oom: option message
i: index
li: label (IM i)
Hlst: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (finite_trace_last s tr)
Hv: valid (existT i li)
  (finite_trace_last s tr, Some im)
Htx: transition (existT i li)
  (finite_trace_last s tr, Some im) = (
sf, oom)
x:= {|
  l := existT i li;
  input := Some im;
  destination := sf;
  output := oom
|}: transition_item
Hs: initial_state_prop s
IHHtr: valid_state_prop
  {|
    vlsm_type :=
      preloaded_with_all_messages_vlsm X;
    vlsm_machine :=
      ConstrainedVLSM.constrained_vlsm_machine
        (free_composite_vlsm IM) constraint
  |} (finite_trace_last s tr)
valid_state_message_prop
  (preloaded_with_all_messages_vlsm (IM i)) ?Goal
  (Some im)
    by apply preloaded_with_all_messages_message_valid_initial_state_message.
Qed.

Finally, we can conclude that a composition of validator components can resist any kind of external influence.

Lemma composite_validator_byzantine_traces_are_not_byzantine :
  forall (tr : Trace X),
    byzantine_trace_prop X tr ->
    valid_trace_prop X tr.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
∀ tr : Trace,
  byzantine_trace_prop X tr → valid_trace_prop X tr
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
∀ tr : Trace,
  byzantine_trace_prop X tr → valid_trace_prop X tr
  intros tr Hbyz.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
tr: Trace
Hbyz: byzantine_trace_prop X tr
valid_trace_prop X tr
  apply validator_preloaded_with_all_messages_incl.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
Hvalidator: ∀ i : index,
  component_message_validator_prop IM
    constraint i
tr: Trace
Hbyz: byzantine_trace_prop X tr
valid_trace_prop
  {|
    vlsm_type := preloaded_with_all_messages_vlsm X;
    vlsm_machine := preloaded_with_all_messages_vlsm X
  |} tr
  by apply byzantine_alt_byzantine_iff, alt_preloaded_with_all_messages_incl in Hbyz.
Qed.

End sec_composite_validator_byzantine_traces.