Merge remote-tracking branch 'origin/master' into elmo-constrained-st…

…ate-decidable

theories/Core/ByzantineTraces.v

@@ -52,7 +52,7 @@ Definition byzantine_trace_prop (tr : Trace M) : Prop :=
 Lemma byzantine_pre_loaded_with_all_messages :
   forall (tr : Trace M),
     byzantine_trace_prop tr ->
-    valid_trace_prop (pre_loaded_with_all_messages_vlsm M) tr.
+    constrained_trace_prop M tr.
 Proof.
   intros tr [M' Htr]; cbn in Htr.
   by apply proj_pre_loaded_with_all_messages_incl in Htr.
@@ -149,13 +149,11 @@ Qed.
 Section sec_pre_loaded_with_all_messages_byzantine_alt.
 
 (**
-  Let <<PreLoaded>> denote the [pre_loaded_with_all_messages_vlsm] of <<M>>,
-  let <<Alt>> denote the free composition of <<M>> with the [emit_any_message_vlsm],
+  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
-  (PreLoaded := pre_loaded_with_all_messages_vlsm M)
   (Alt1 := binary_free_composition_fst M emit_any_message_vlsm)
   (Alt := binary_free_composition M emit_any_message_vlsm)
   .
@@ -165,13 +163,13 @@ Context
   of <<Alt1>> into <<Preloaded>>.
 *)
 Lemma alt_pre_loaded_with_all_messages_incl :
-  VLSM_incl Alt1 PreLoaded.
+  VLSM_incl Alt1 (pre_loaded_with_all_messages_vlsm M).
 Proof.
   by intros t Hvt; apply byzantine_pre_loaded_with_all_messages, byzantine_alt_byzantine.
 Qed.
 
 (**
-  To prove the reverse inclusion (between <<PreLoaded>> and <<Alt1>>) we will use the
+  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:
 
@@ -212,9 +210,9 @@ Proof. by apply any_message_is_valid_in_preloaded. Qed.
 Definition lifted_alt_state (s : state M) : state Alt :=
   lift_to_composite_state' (binary_IM M emit_any_message_vlsm) first s.
 
-(** Lifting a valid state of <<PreLoaded>> we obtain a valid state of <<Alt>>. *)
+(** Lifting a constrained state of <<M>> we obtain a valid state of <<Alt>>. *)
 Lemma preloaded_alt_valid_state :
-  forall (sj : state PreLoaded) (om : option message),
+  forall (sj : state M) (om : option message),
     constrained_state_message_prop M sj om ->
     valid_state_prop Alt (lifted_alt_state sj).
 Proof.
@@ -238,9 +236,9 @@ Qed.
   results above to show that <<Preloaded>> is included in <<Alt1>>.
 *)
 Lemma pre_loaded_with_all_messages_alt_incl :
-  VLSM_incl PreLoaded Alt1.
+  VLSM_incl (pre_loaded_with_all_messages_vlsm M) Alt1.
 Proof.
-  apply (basic_VLSM_incl PreLoaded Alt1); intro; intros;
+  apply (basic_VLSM_incl _ Alt1); intro; intros;
     [done | by apply alt_proj_option_valid_message | | by apply H].
   exists (lifted_alt_state s).
   split; [done |].
@@ -252,7 +250,7 @@ Qed.
 
 (** Hence, <<Preloaded>> and <<Alt1>> are actually trace-equivalent. *)
 Lemma pre_loaded_with_all_messages_alt_eq :
-  VLSM_eq PreLoaded Alt1.
+  VLSM_eq (pre_loaded_with_all_messages_vlsm M) Alt1.
 Proof.
   split.
   - by apply pre_loaded_with_all_messages_alt_incl.
@@ -331,17 +329,16 @@ Context
   (IM : index -> VLSM message)
   (constraint : composite_label IM -> composite_state IM  * option message -> Prop)
   (X := composite_vlsm IM constraint)
-  (PreLoadedX := pre_loaded_with_all_messages_vlsm X)
   (Hvalidator : forall i : index, component_message_validator_prop IM constraint i)
   .
 
 (**
-  Since we know that <<PreloadedX>> contains precisely the byzantine traces
-  of <<X>>, we just need to show that <<PreLoadedX>> is included in <<X>> to
+  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_pre_loaded_with_all_messages_incl :
-  VLSM_incl PreLoadedX X.
+  VLSM_incl (pre_loaded_with_all_messages_vlsm X) X.
 Proof.
   apply VLSM_incl_finite_traces_characterization.
   intros s tr Htr.

theories/Core/Composition.v

@@ -1333,7 +1333,6 @@ Context
   `{EqDecision index}
   (IM : index -> VLSM message)
   (Free := free_composite_vlsm IM)
-  (RFree := pre_loaded_with_all_messages_vlsm Free)
   .
 
 Definition composite_valid_transition l s1 iom s2 oom : Prop :=
@@ -1344,7 +1343,9 @@ Definition composite_valid_transition_item
   composite_valid_transition (l item) s (input item) (destination item) (output item).
 
 Lemma composite_valid_transition_reachable_iff l s1 iom s2 oom :
-  composite_valid_transition l s1 iom s2 oom <-> valid_transition RFree l s1 iom s2 oom.
+  composite_valid_transition l s1 iom s2 oom
+    <->
+  valid_transition (pre_loaded_with_all_messages_vlsm Free) l s1 iom s2 oom.
 Proof.
   by split; intros []; constructor.
 Qed.
@@ -1356,7 +1357,9 @@ Definition composite_valid_transition_future : relation (composite_state IM) :=
   tc composite_valid_transition_next.
 
 Lemma composite_valid_transition_next_reachable_iff s1 s2 :
-  composite_valid_transition_next s1 s2 <-> valid_transition_next RFree s1 s2.
+  composite_valid_transition_next s1 s2
+    <->
+  valid_transition_next (pre_loaded_with_all_messages_vlsm Free) s1 s2.
 Proof.
   by split; intros []; econstructor; apply composite_valid_transition_reachable_iff.
 Qed.

theories/Core/Equivocation.v

@@ -1035,7 +1035,6 @@ Proof.
   intros l s im s' om Htrans msg.
   rename Htrans into Htrans'.
   pose proof Htrans' as [[Hproto_s [Hproto_m Hvalid]] Htrans].
-  set (preloaded := pre_loaded_with_all_messages_vlsm vlsm) in * |- *.
   pose proof (valid_state_has_trace _ _ Hproto_s)
     as [is [tr [Htr Hinit]]].
   pose proof (Htr' := extend_right_finite_trace_from_to _ Htr Htrans').
@@ -2621,7 +2620,6 @@ Context
   {message : Type}
   `{EqDecision message}
   (X : VLSM message)
-  (PreX := pre_loaded_with_all_messages_vlsm X)
   `{HasBeenSentCapability message X}
   `{HasBeenReceivedCapability message X}
   .
@@ -2631,7 +2629,7 @@ Definition state_received_not_sent (s : state X) (m : message) : Prop :=
 
 Lemma state_received_not_sent_trace_iff
   (m : message)
-  (s is : state (PreX))
+  (s is : state (pre_loaded_with_all_messages_vlsm X))
   (tr : list transition_item)
   (Htr : finite_constrained_trace_init_to X is s tr)
   : state_received_not_sent s m <-> trace_received_not_sent_before_or_after tr m.
@@ -2660,7 +2658,7 @@ Definition state_received_not_sent_invariant
 
 Lemma state_received_not_sent_invariant_trace_iff
   (P : message -> Prop)
-  (s is : state (PreX))
+  (s is : state (pre_loaded_with_all_messages_vlsm X))
   (tr : list transition_item)
   (Htr : finite_constrained_trace_init_to X is s tr)
   : state_received_not_sent_invariant s P <->
@@ -2679,8 +2677,8 @@ Definition cannot_resend_message_stepwise_prop : Prop :=
 
 Lemma cannot_resend_received_message_in_future
   (Hno_resend : cannot_resend_message_stepwise_prop)
-  (s1 s2 : state (PreX))
-  (Hfuture : in_futures PreX s1 s2)
+  (s1 s2 : state (pre_loaded_with_all_messages_vlsm X))
+  (Hfuture : in_futures (pre_loaded_with_all_messages_vlsm X) s1 s2)
   : forall m : message,
     state_received_not_sent s1 m -> state_received_not_sent s2 m.
 Proof.
@@ -2721,8 +2719,8 @@ Lemma lift_preloaded_trace_to_seeded
   (P : message -> Prop)
   (tr : list transition_item)
   (Htrm : trace_received_not_sent_before_or_after_invariant tr P)
-  (is : state (PreX))
-  (Htr : finite_valid_trace PreX is tr)
+  (is : state (pre_loaded_with_all_messages_vlsm X))
+  (Htr : finite_constrained_trace X is tr)
   : finite_valid_trace (pre_loaded_vlsm X P) is tr.
 Proof.
   unfold trace_received_not_sent_before_or_after_invariant in Htrm.
@@ -2794,7 +2792,7 @@ Lemma lift_generated_to_seeded
   (s : state X)
   (Hequiv_s : state_received_not_sent_invariant s P)
   (m : message)
-  (Hgen : can_produce PreX s m)
+  (Hgen : can_produce (pre_loaded_with_all_messages_vlsm X) s m)
   : can_produce (pre_loaded_vlsm X P) s m.
 Proof.
   apply non_empty_valid_trace_from_can_produce.
@@ -2849,7 +2847,6 @@ Context
   `{forall i : index, (HasBeenReceivedCapability (IM i))}
   (constraint : composite_label IM -> composite_state IM * option message -> Prop)
   (X := composite_vlsm IM constraint)
-  (PreX := pre_loaded_with_all_messages_vlsm X)
   (Y := free_composite_vlsm IM)
   (PreY := pre_loaded_with_all_messages_vlsm Y).
 

theories/Core/Equivocation/FixedSetEquivocation.v

@@ -650,7 +650,6 @@ Context
   (Fixed := fixed_equivocation_vlsm_composition IM equivocators)
   (StrongFixed := strong_fixed_equivocation_vlsm_composition IM equivocators)
   (Free := free_composite_vlsm IM)
-  (PreFree := pre_loaded_with_all_messages_vlsm Free)
   .
 
 (**
@@ -741,7 +740,6 @@ Context
   (Free := free_composite_vlsm IM)
   (Fixed := fixed_equivocation_vlsm_composition IM equivocators)
   (StrongFixed := strong_fixed_equivocation_vlsm_composition IM equivocators)
-  (PreFree := pre_loaded_with_all_messages_vlsm Free)
   .
 
 (**
@@ -1041,7 +1039,6 @@ Context
   (StrongFixed := strong_fixed_equivocation_vlsm_composition IM equivocators)
   (StrongFixedNonEquivocating := pre_induced_sub_projection IM (elements non_equivocators)
                                 (strong_fixed_equivocation_constraint IM equivocators))
-  (PreFree := pre_loaded_with_all_messages_vlsm Free)
   .
 
 (**

theories/Core/Equivocation/LimitedMessageEquivocation.v

@@ -199,7 +199,6 @@ Context
   `{RelDecision _ _ (is_equivocating_tracewise_no_has_been_sent IM A sender)}
   (Fixed := fixed_equivocation_vlsm_composition IM equivocators)
   (StrongFixed := strong_fixed_equivocation_vlsm_composition IM equivocators)
-  (PreFree := pre_loaded_with_all_messages_vlsm Free)
   (Limited : VLSM message := tracewise_limited_equivocation_vlsm_composition (Cv := Cv) IM threshold A sender)
   (HBE : BasicEquivocation (composite_state IM) validator Cv threshold :=
     equivocation_dec_tracewise IM threshold A sender)

theories/Core/Equivocation/NoEquivocation.v

@@ -108,7 +108,7 @@ Qed.
 *)
 Lemma no_equivocations_preloaded_traces :
   forall (is : state (pre_loaded_with_all_messages_vlsm X)) (tr : list transition_item),
-    finite_valid_trace (pre_loaded_with_all_messages_vlsm X) is tr -> finite_valid_trace X is tr.
+    finite_constrained_trace X is tr -> finite_valid_trace X is tr.
 Proof.
   intros is tr Htr.
   induction Htr using finite_valid_trace_rev_ind;

theories/Core/Equivocation/TraceWiseEquivocation.v

@@ -32,7 +32,6 @@ Context
   `{finite.Finite validator}
   (A : validator -> index)
   (sender : message -> option validator)
-  (PreFree := pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))
   .
 
 (**
@@ -96,7 +95,7 @@ Lemma elem_of_equivocating_senders_in_trace
   : v ∈ equivocating_senders_in_trace tr <->
     exists (m : message),
     (sender m = Some v) /\
-    equivocation_in_trace PreFree m tr.
+    equivocation_in_trace (free_composite_vlsm IM) m tr.
 Proof.
   unfold equivocating_senders_in_trace.
   rewrite elem_of_remove_dups, elem_of_list_omap.
@@ -170,7 +169,7 @@ Definition is_equivocating_tracewise_no_has_been_sent
   (Htr : finite_constrained_trace_init_to (free_composite_vlsm IM) is s tr),
   exists (m : message),
   (sender m = Some v) /\
-  equivocation_in_trace PreFree m tr.
+  equivocation_in_trace (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) m tr.
 
 Lemma is_equivocating_tracewise_no_has_been_sent_equivocating_senders_in_trace
   (s : composite_state IM)

theories/Core/Equivocation/WitnessedEquivocation.v

@@ -489,7 +489,7 @@ Proof.
     forall is tr,
     m = set_size (equivocating_validators (finite_trace_last is tr)) ->
     n = length tr ->
-    finite_valid_trace PreFree is tr ->
+    finite_constrained_trace Free is tr ->
     trace_witnessing_equivocation_prop is tr ->
     let s := finite_trace_last is tr in
     exists (is' : state PreFree) (tr' : list transition_item),

theories/Core/EquivocationProjections.v

@@ -423,7 +423,6 @@ Context
   (A : validator -> index)
   (sender : message -> option validator)
   (Hsender_safety : sender_safety_alt_prop IM A sender)
-  (PreFree := pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))
   (j : index)
   (m : message)
   (Hj : option_map A (sender m) = Some j)
@@ -434,8 +433,9 @@ Context
   by the free composition (pre-loaded with all messages), then it can also be
   emitted by the component corresponding to its sender (pre-loaded with all messages).
 *)
-Lemma can_emit_projection
-  : can_emit PreFree m -> can_emit (pre_loaded_with_all_messages_vlsm (IM j)) m.
+Lemma can_emit_projection :
+  can_emit (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) m ->
+  can_emit (pre_loaded_with_all_messages_vlsm (IM j)) m.
 Proof.
   destruct (sender m) as [v |] eqn: Hsender; simpl in Hj; [| by congruence].
   apply Some_inj in Hj.

theories/Core/Equivocators/EquivocatorsCompositionProjections.v

@@ -1007,7 +1007,7 @@ Lemma preloaded_equivocators_valid_trace_project_inv
   (is : composite_state (equivocator_IM IM))
   (tr : list (composite_transition_item (equivocator_IM IM)))
   (final_state := finite_trace_last is tr)
-  (Htr : finite_valid_trace PreFreeE is tr)
+  (Htr : finite_constrained_trace FreeE is tr)
   (trX : list (composite_transition_item IM))
   (initial_descriptors : equivocator_descriptors IM)
   (Hproject : equivocators_trace_project final_descriptors tr = Some (trX, initial_descriptors))
@@ -2125,7 +2125,7 @@ Proof.
     apply VLSM_incl_finite_valid_trace_from; [| done].
     by apply constrained_preloaded_incl.
   - intros * Htr.
-    assert (Hpre_tr : finite_valid_trace PreFreeE sX trX).
+    assert (Hpre_tr : finite_constrained_trace FreeE sX trX).
     {
       apply VLSM_incl_finite_valid_trace; [| done].
       by apply constrained_preloaded_incl.

theories/Core/Equivocators/FixedEquivocation.v

@@ -490,7 +490,7 @@ Proof.
       by apply equivocators_fixed_equivocations_vlsm_incl_free.
     }
     assert
-      (Htr'pre : finite_valid_trace (pre_loaded_with_all_messages_vlsm FreeE) is tr').
+      (Htr'pre : finite_constrained_trace FreeE is tr').
     {
       split; [| done].
       specialize (vlsm_incl_pre_loaded_with_all_messages_vlsm FreeE) as Hincl.
@@ -570,7 +570,7 @@ Proof.
             by (apply finite_valid_trace_last_pstate, Htr'pre).
         apply proper_sent; [done |].
         apply has_been_sent_consistency; [typeclasses eauto | done |].
-        by exists is, tr', (valid_trace_add_default_last Htr'pre).
+        by red in Htr'pre; exists is, tr', (valid_trace_add_default_last Htr'pre).
     + exists trX'. exists initial_descriptors. subst foldx. split; [done |].
       split; [by apply Htr_project |].
       split; [| done].
@@ -628,14 +628,14 @@ Proof.
   subst lst.
   rewrite Hfinal_state.
 
-  assert (Htr_Pre : finite_valid_trace (pre_loaded_with_all_messages_vlsm FreeE) is tr).
+  assert (Htr_Pre : finite_constrained_trace FreeE is tr).
   {
     apply VLSM_incl_finite_valid_trace; [| done].
     by apply constrained_preloaded_incl.
   }
 
-  assert (HtrX_Pre : finite_valid_trace (pre_loaded_with_all_messages_vlsm Free)
-                      (equivocators_state_project IM initial_descriptors is) trX).
+  assert (HtrX_Pre : finite_constrained_trace Free
+    (equivocators_state_project IM initial_descriptors is) trX).
   {
     revert HtrX_Free; apply VLSM_incl_finite_valid_trace.
     by apply vlsm_incl_pre_loaded_with_all_messages_vlsm.
@@ -650,6 +650,7 @@ Proof.
   rewrite (has_been_directly_observed_sent_received_iff Free) by done.
   right. apply proper_sent; [done |].
   apply has_been_sent_consistency; [by typeclasses eauto | done |].
+  red in HtrX_Pre.
   exists (equivocators_state_project IM initial_descriptors is), trX,
     (valid_trace_add_default_last HtrX_Pre).
 
@@ -752,7 +753,7 @@ Proof.
   intros pre item suf m Heq Hm Hitem.
   destruct (free_equivocators_valid_trace_project descriptors is tr Hproper Htr)
     as [trX [initial_descriptors [Hinitial_descriptors [Htr_project [Hfinal_state HtrXFree]]]]].
-  assert (HtrXPre : finite_valid_trace (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))
+  assert (HtrXPre : finite_constrained_trace (free_composite_vlsm IM)
     (equivocators_state_project IM initial_descriptors is) trX).
   {
     revert HtrXFree; apply VLSM_incl_finite_valid_trace.
@@ -763,7 +764,7 @@ Proof.
     subst lst_trX s; cbn in Hfinal_state |- *; rewrite Hfinal_state.
     by apply finite_valid_trace_last_pstate, HtrXPre.
   }
-  assert (Htr_free : finite_valid_trace  (pre_loaded_with_all_messages_vlsm FreeE) is tr).
+  assert (Htr_free : finite_constrained_trace FreeE is tr).
   {
     apply VLSM_incl_finite_valid_trace; [| done].
     by apply constrained_preloaded_incl.
@@ -968,7 +969,7 @@ Proof.
   elim Hno. clear Hno.
   apply composite_has_been_directly_observed_sent_received_iff.
   left.
-  assert (HtrX_free : finite_valid_trace (pre_loaded_with_all_messages_vlsm Free)
+  assert (HtrX_free : finite_constrained_trace Free
     (equivocators_state_project IM initial_descriptors is) trX).
   {
     revert HtrX; apply VLSM_incl_finite_valid_trace.
@@ -980,6 +981,7 @@ Proof.
   rewrite Hlast_state.
   apply (composite_proper_sent IM); [done |].
   apply has_been_sent_consistency; [by typeclasses eauto | done |].
+  red in HtrX_free.
   exists (equivocators_state_project IM initial_descriptors is), trX,
     (valid_trace_add_default_last HtrX_free).
   clear HtrX HtrX_free Hfree_lst.
@@ -1300,7 +1302,7 @@ Proof.
   - apply PreFreeE_Free_vlsm_projection_type.
     apply VLSM_incl_finite_valid_trace_from; [| done].
     by apply equivocators_fixed_equivocations_vlsm_incl_PreFree.
-  - assert (Hpre_tr : finite_valid_trace (pre_loaded_with_all_messages_vlsm FreeE) sX trX).
+  - assert (Hpre_tr : finite_constrained_trace FreeE sX trX).
     {
       apply VLSM_incl_finite_valid_trace; [| done].
       by apply equivocators_fixed_equivocations_vlsm_incl_PreFree.