update with renamings (#2)

_CoqProject

@@ -1,7 +1,5 @@
 -Q theories/VLSM VLSM
 
--arg -w -arg -deprecated-hint-without-locality
-
 theories/VLSM/Lib/Preamble.v
 theories/VLSM/Lib/SsrExport.v
 theories/VLSM/Lib/StdppExtras.v
@@ -26,7 +24,7 @@ theories/VLSM/Core/VLSM.v
 theories/VLSM/Core/Composition.v
 theories/VLSM/Core/Plans.v
 theories/VLSM/Core/VLSMProjections.v
-theories/VLSM/Core/Validating.v
+theories/VLSM/Core/Validator.v
 theories/VLSM/Core/Decisions.v
 theories/VLSM/Core/MessageDependencies.v
 theories/VLSM/Core/ProjectionTraces.v

theories/VLSM/Core/ByzantineTraces.v

@@ -1,6 +1,6 @@
 From stdpp Require Import prelude.
 From Coq Require Import FinFun.
-From VLSM Require Import Lib.Preamble Core.VLSM Core.VLSMProjections Core.Composition Core.ProjectionTraces Core.Validating.
+From VLSM Require Import Lib.Preamble Core.VLSM Core.VLSMProjections Core.Composition Core.ProjectionTraces Core.Validator.
 
 (** * VLSM Byzantine Traces
 
@@ -11,10 +11,10 @@ and equivalent with traces on the corresponding pre-loaded VLSM
 
 Note that, contrary to what one might think, the [byzantine_trace_prop]erty
 does not only capture traces exhibiting byzantine behavior, but also all
-[protocol_trace]s (consequence of Lemma [vlsm_incl_pre_loaded_with_all_messages_vlsm]).
+[valid_trace]s (consequence of Lemma [vlsm_incl_pre_loaded_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_prop]erty but without the [protocol_trace_prop]erty.
+the [byzantine_trace_prop]erty but without the [valid_trace_prop]erty.
 
 In the remainder of this section, we fix a (regular) VLSM <<M>> with
 signature <<S>> and of type <<T>>.
@@ -44,7 +44,7 @@ Definition byzantine_trace_prop
     (tr : vTrace M) :=
     exists (M' : VLSM message)
         (Proj := binary_free_composition_fst M M'),
-        protocol_trace_prop Proj tr.
+        valid_trace_prop Proj tr.
 
 (**
 
@@ -56,7 +56,7 @@ Lemma byzantine_pre_loaded_with_all_messages
     (PreLoaded := pre_loaded_with_all_messages_vlsm M)
     (tr : vTrace M)
     (Hbyz : byzantine_trace_prop tr)
-    : protocol_trace_prop PreLoaded tr.
+    : valid_trace_prop PreLoaded tr.
 Proof.
     destruct Hbyz as [M' Htr].
     simpl in Htr.
@@ -154,7 +154,7 @@ Definition alternate_byzantine_trace_prop
     (tr : vTrace M)
     (Proj := binary_free_composition_fst M emit_any_message_vlsm)
     :=
-    protocol_trace_prop Proj tr.
+    valid_trace_prop Proj tr.
 
 (**
 
@@ -182,7 +182,7 @@ equivalent to the [byzantine_trace_prop]erty.
 Since we have already proven that the [alternate_byzantine_trace_prop]erty
 implies the [byzantine_trace_prop]erty (Lemma [byzantine_alt_byzantine]),
 and since we know that the traces with the [byzantine_trace_prop]erty
-are [protocol_trace]s for the [pre_loaded_with_all_messages_vlsm], to prove the
+are [valid_trace]s for the [pre_loaded_with_all_messages_vlsm], to prove the
 equivalence it is enough to close the circle by proving the
 [VLSM_incl]usion between the [pre_loaded_with_all_messages_vlsm] and the projection VLSM used
 in the definition of the [alternate_byzantine_trace_prop]erty.
@@ -209,7 +209,7 @@ of <<Alt1>> into <<Preloaded>>
     Lemma alt_pre_loaded_with_all_messages_incl
         : VLSM_incl Alt1 PreLoaded.
     Proof.
-        intros t Hpt.
+        intros t Hvt.
         apply byzantine_pre_loaded_with_all_messages.
         apply byzantine_alt_byzantine.
         assumption.
@@ -219,29 +219,29 @@ of <<Alt1>> into <<Preloaded>>
 To prove the reverse inclusion (between <<PreLoaded>> and <<Alt1>>) we will use the
 [basic_VLSM_incl] meta-result about proving inclusions bewteen
 VLSMs which states that
-- if all [valid] messages in the first are [protocol_message]s in the second, and
-- if all [protocol_state]s in the first are also [protocol_state]s in the second,
-- and if all [protocol_transition]s in the first are also [protocol_transition]s
+- if all [valid] messages in the first are [valid_message]s in the second, and
+- if all [valid_state]s in the first are also [valid_state]s in the second,
+- and if all [input_valid_transition]s in the first are also [input_valid_transition]s
 in the second,
 - then the first VLSM is included in the second.
 
 We will tackle each of these properties in the sequel.
 
-First note that _all_ messages are [protocol_message]s for <<Alt>>, as
+First note that _all_ messages are [valid_message]s for <<Alt>>, as
 [emit_any_message_vlsm] can generate any message without changing state.
 *)
 
-    Lemma alt_option_protocol_message
+    Lemma alt_option_valid_message
         (om : option message)
-        : option_protocol_message_prop Alt om.
+        : option_valid_message_prop Alt om.
     Proof.
-        destruct om as [m|];[|apply option_protocol_message_None].
+        destruct om as [m|];[|apply option_valid_message_None].
         pose (s :=proj1_sig (vs0 Alt): vstate Alt).
         unfold vstate in s.
         exists s.
-        assert (protocol_prop Alt s None) as Hs
-          by (apply protocol_initial_state;apply proj2_sig).
-        eapply (protocol_generated Alt) with s None s None (existT second _)
+        assert (valid_state_message_prop Alt s None) as Hs
+          by (apply valid_initial_state;apply proj2_sig).
+        eapply (valid_generated_state_message Alt) with s None s None (existT second _)
         ;[assumption|assumption|split; exact I|].
         simpl. f_equal.
         rewrite state_update_id; reflexivity.
@@ -251,12 +251,12 @@ First note that _all_ messages are [protocol_message]s for <<Alt>>, as
 Using the above, it is straight-forward to show that:
 *)
 
-    Lemma alt_proj_option_protocol_message
+    Lemma alt_proj_option_valid_message
         (m : option message)
-        : option_protocol_message_prop Alt1 m.
+        : option_valid_message_prop Alt1 m.
     Proof.
-        apply protocol_message_projection.
-        apply alt_option_protocol_message.
+        apply valid_message_projection.
+        apply alt_option_valid_message.
     Qed.
 
 (**
@@ -271,24 +271,24 @@ by simply setting to <<s>> the  corresponding component of the initial
              (binary_IM M emit_any_message_vlsm) first s.
 
 (**
-Lifting a [protocol_state] of <<PreLoaded>> we obtain a [protocol_state] of <<Alt>>.
+Lifting a [valid_state] of <<PreLoaded>> we obtain a [valid_state] of <<Alt>>.
 *)
-    Lemma preloaded_alt_protocol_state
+    Lemma preloaded_alt_valid_state
         (sj : state)
         (om : option message)
-        (Hp : protocol_prop PreLoaded sj om)
-        : protocol_state_prop Alt (lifted_alt_state sj).
+        (Hp : valid_state_message_prop PreLoaded sj om)
+        : valid_state_prop Alt (lifted_alt_state sj).
     Proof.
-      assert (protocol_state_prop PreLoaded sj) as Hsj
+      assert (valid_state_prop PreLoaded sj) as Hsj
         by (exists om;assumption);clear Hp.
-      induction Hsj using protocol_state_prop_ind.
-      - apply initial_is_protocol.
+      induction Hsj using valid_state_prop_ind.
+      - apply initial_state_is_valid.
         intros [];[exact Hs|exact I].
       - exists om'.
-        assert (option_protocol_message_prop Alt om0) as Hom0
-          by apply alt_option_protocol_message.
-        cut (protocol_transition Alt (existT first l) (lifted_alt_state s,om0) (lifted_alt_state s', om'))
-          ;[apply protocol_prop_transition_out|].
+        assert (option_valid_message_prop Alt om0) as Hom0
+          by apply alt_option_valid_message.
+        cut (input_valid_transition Alt (existT first l) (lifted_alt_state s,om0) (lifted_alt_state s', om'))
+          ;[apply input_valid_transition_outputs_valid_state_message|].
         split.
         * split;[assumption|].
           split;[assumption|].
@@ -315,13 +315,13 @@ results above to show that <<Preloaded>> is included in <<Alt1>>.
     Proof.
         apply (basic_VLSM_incl (machine PreLoaded) (machine Alt1))
         ; intro; intros; [assumption| | |apply H].
-        - apply alt_proj_option_protocol_message.
+        - apply alt_proj_option_valid_message.
         - exists (lifted_alt_state s).
           split; [reflexivity|].
           destruct Hv as [[_om Hps] [Hpm Hv]].
           repeat split.
-          + apply preloaded_alt_protocol_state with _om; assumption.
-          + apply alt_option_protocol_message.
+          + apply preloaded_alt_valid_state with _om; assumption.
+          + apply alt_option_valid_message.
           + assumption.
     Qed.
 
@@ -359,24 +359,24 @@ End ByzantineTraces.
 
 (** ** Byzantine fault tolerance for a single validator
 
-Given that projections of validating VLSMs are equal to their corresponding
+Given that projections of composition of validator VLSMs are equal to their corresponding
 pre-loaded with all messages VLSM ([pre_loaded_with_all_messages_validating_proj_eq]),
-we can derive that for validating VLSMs, all their byzantine traces are
-included in the [protocol_trace]s of their projection from the composition.
+we can derive that for validators, all their byzantine traces are
+included in the [valid_trace]s of their projection from the composition.
 *)
-Lemma validating_component_byzantine_fault_tolerance
+Lemma validator_component_byzantine_fault_tolerance
     message `{EqDecision index}
     (IM : index -> VLSM message)
     (constraint : composite_label IM -> composite_state IM  * option message -> Prop)
     (i : index)
-    (Hvalidating: validating_projection_prop IM constraint i)
+    (Hvalidator: projection_validator_prop IM constraint i)
     : forall tr, byzantine_trace_prop (IM i) tr ->
-        protocol_trace_prop (composite_vlsm_constrained_projection IM constraint i) tr.
+        valid_trace_prop (composite_vlsm_constrained_projection IM constraint i) tr.
 Proof.
     intros tr Htr.
     apply
-        (VLSM_incl_protocol_trace
-            (pre_loaded_with_all_messages_validating_proj_incl _ _ _ Hvalidating)).
+        (VLSM_incl_valid_trace
+            (pre_loaded_with_all_messages_validator_proj_incl _ _ _ Hvalidator)).
     revert Htr.
     apply byzantine_pre_loaded_with_all_messages.
 Qed.
@@ -385,11 +385,11 @@ Qed.
 (** ** Byzantine fault tolerance for a composition of validators
 
 In this section we show that if all components of a composite VLSM <<X>> have
-the [validating_projection_prop]erty, then its byzantine traces (that is,
+the [projection_validator_prop]erty, then its byzantine traces (that is,
 traces obtained upon placing this composition in any, possibly adversarial,
-context) are [protocol_traces] of <<X>>.
+context) are [valid_trace]s of <<X>>.
 *)
-Section composite_validating_byzantine_traces.
+Section composite_validator_byzantine_traces.
 
     Context {message : Type}
             {index : Type}
@@ -399,7 +399,7 @@ Section composite_validating_byzantine_traces.
             (X := composite_vlsm IM constraint)
             (PreLoadedX := pre_loaded_with_all_messages_vlsm X)
             (FreeX := free_composite_vlsm IM)
-            (Hvalidating: forall i : index, validating_projection_prop IM constraint i)
+            (Hvalidator: forall i : index, projection_validator_prop IM constraint i)
             .
 
 (**
@@ -412,58 +412,58 @@ of <<X>>, we just need to show that <<PreLoadedX>> is
 included in <<X>> to prove our main result.
 
 *)
-    Lemma validating_pre_loaded_with_all_messages_incl
+    Lemma validator_pre_loaded_with_all_messages_incl
         : VLSM_incl PreLoadedX X.
     Proof.
         apply VLSM_incl_finite_traces_characterization.
         intros.
         split; [|apply H].
         destruct H as [Htr Hs].
-        induction Htr using finite_protocol_trace_from_rev_ind.
-        - apply (finite_ptrace_empty X).
-          apply initial_is_protocol; assumption.
+        induction Htr using finite_valid_trace_from_rev_ind.
+        - apply (finite_valid_trace_from_empty X).
+          apply initial_state_is_valid; assumption.
         - specialize (IHHtr Hs) as IHtr; clear IHHtr.
           apply (extend_right_finite_trace_from X).
           assumption.
           destruct Hx as [Hvx Htx].
           split; [|assumption].
-          apply finite_ptrace_last_pstate in IHtr.
+          apply finite_valid_trace_last_pstate in IHtr.
           simpl in *.
           match type of IHtr with
-          | protocol_state_prop _ ?s => remember s as lst
+          | valid_state_prop _ ?s => remember s as lst
           end.
           split; [assumption|].
           repeat split; [|apply Hvx|apply Hvx].
           destruct Hvx as [Hlst [_ [Hv _]]].
           destruct l as (i, li). simpl in *.
-          specialize (protocol_state_project_preloaded_to_preloaded _ IM constraint lst i Hlst)
+          specialize (valid_state_project_preloaded_to_preloaded _ IM constraint lst i Hlst)
             as Hlsti.
-          assert (Hpv : protocol_valid (pre_loaded_with_all_messages_vlsm (IM i)) li (lst i, iom)).
+          assert (Hiv : input_valid (pre_loaded_with_all_messages_vlsm (IM i)) li (lst i, iom)).
           { split; [assumption|]. split; [|assumption].
-            eexists _. apply (pre_loaded_with_all_messages_message_protocol_prop (IM i)).
+            eexists _. apply (pre_loaded_with_all_messages_message_valid_initial_state_message (IM i)).
           }
-          apply Hvalidating in Hpv.
-          clear -Hpv.
-          destruct Hpv as [_ [_ [_ [Hinput _]]]].
+          apply Hvalidator in Hiv.
+          clear -Hiv.
+          destruct Hiv as [_ [_ [_ [Hinput _]]]].
           destruct Hinput as [s Hinput].
           exists s.
           revert Hinput.
-          apply (constraint_subsumption_protocol_prop IM constraint).
+          apply (constraint_subsumption_valid_state_message_preservation IM constraint).
           intro. intros. destruct som. apply H.
     Qed.
 
 (**
-Finally, we can conclude that a composition of validating components can
+Finally, we can conclude that a composition of validator components can
 resist any kind of external influence:
 *)
-    Lemma composite_validating_byzantine_traces_are_not_byzantine
+    Lemma composite_validator_byzantine_traces_are_not_byzantine
         (tr : vTrace X)
         (Hbyz : byzantine_trace_prop X tr)
-        : protocol_trace_prop X tr.
+        : valid_trace_prop X tr.
     Proof.
-        apply validating_pre_loaded_with_all_messages_incl.
+        apply validator_pre_loaded_with_all_messages_incl.
         apply alt_pre_loaded_with_all_messages_incl.
         apply byzantine_alt_byzantine_iff.
         assumption.
     Qed.
-End composite_validating_byzantine_traces.
+End composite_validator_byzantine_traces.