Progress

Author: Traian Florin Serbanuta

theories/Core/Equivocation.v

@@ -126,6 +126,14 @@ Definition equivocation_in_trace
     /\ input item = Some msg
     /\ ~ trace_has_message (field_selector output) msg prefix.
 
+(**
+  Note that the [equivocation_in_trace] definition counts as an equivocation
+  a message which is emitted at the same time it is received.
+  However, the received-not-sent evidence of equivocation would not be able to
+  detect such a case; hence, we here define the property of a VLSM to never
+  be allowed to send the message it receives in the same transition.
+*)
+
 #[export] Instance equivocation_in_trace_dec
   `{EqDecision message}
   : RelDecision equivocation_in_trace.

theories/Core/Equivocation/MinimalEquivocationTrace.v

@@ -4,7 +4,7 @@ From VLSM.Lib Require Import Preamble ListExtras StdppListSet StdppExtras NatExt
 From VLSM.Lib Require Import Measurable EquationsExtras.
 From VLSM.Core Require Import VLSM Composition.
 From VLSM.Core Require Import Equivocation MessageDependencies TraceableVLSM.
-From VLSM.Core Require Import AnnotatedVLSM MsgDepLimitedEquivocation.
+From VLSM.Core Require Import TraceWiseEquivocation.
 
 (** * Core: Minimally Equivocating Traces
 
@@ -702,4 +702,84 @@ Proof.
   by intros ? **; eapply minimal_equivocation_choice_monotone.
 Qed.
 
+Lemma state_to_minimal_equivocation_trace_equivocation_monotonic_final :
+  forall (s : composite_state IM) (Hs_pre :  composite_constrained_state_prop IM s)
+    (is : composite_state IM) (tr : list (composite_transition_item IM)),
+    state_to_minimal_equivocation_trace s Hs_pre = (is, tr) ->
+    forall (item : composite_transition_item IM), item ∈ tr ->
+    forall v : validator,
+      msg_dep_is_globally_equivocating IM message_dependencies sender
+        (destination item) v ->
+      msg_dep_is_globally_equivocating IM message_dependencies sender s v.
+Proof.
+  intros * Htr_min; rewrite <- Forall_forall.
+  assert (Hall := state_to_minimal_equivocation_trace_equivocation_monotonic _ _ _ _ Htr_min).
+  apply reachable_composite_state_to_trace in Htr_min;
+    [| by apply minimal_equivocation_choice_is_choosing_well].
+  induction Htr_min using finite_valid_trace_init_to_rev_ind;
+    [by constructor |].
+  apply Forall_app; split; [| by apply Forall_singleton].
+  apply input_valid_transition_origin in Ht as Hs.
+  apply input_valid_transition_destination in Ht as Hsf.
+  eapply Forall_impl.
+  - by apply IHHtr_min; [| intros * ->; eapply Hall; simplify_list_eq].
+  - cbn; intros item Hitem_s v Hv.
+    apply Hitem_s in Hv.
+    specialize (Hall tr []); setoid_rewrite app_nil_r in Hall.
+    apply (Hall _ eq_refl).
+    by apply valid_trace_get_last in Htr_min; subst.
+Qed.
+
+Section sec_tracewise_equivocation.
+
+Context
+  (Hfull : forall i, message_dependencies_full_node_condition_prop (IM i) message_dependencies)
+  (PreFree := pre_loaded_with_all_messages_vlsm Free)
+  .
+
+Lemma minimal_equivocation_trace_includes_tracewise_equivocation :
+  forall (s : composite_state IM) (Hs : constrained_state_prop Free s),
+  forall is tr, state_to_minimal_equivocation_trace s Hs = (is, tr) ->
+  forall v, is_equivocating_tracewise_no_has_been_sent IM A sender s v ->
+  exists (m : message), (sender m = Some v) /\ equivocation_in_trace PreFree m tr.
+Proof.
+  intros s Hs is tr Heqtr v Heqv.
+  edestruct Heqv.
+  - eapply reachable_composite_state_to_trace; [| done].
+    by apply minimal_equivocation_choice_is_choosing_well.
+  - by eexists.
+Qed.
+
+Lemma minimal_equivocation_trace_equivocation_is_statewise_equivocating :
+  forall (s : composite_state IM) (Hs : constrained_state_prop Free s),
+  forall is tr, state_to_minimal_equivocation_trace s Hs = (is, tr) ->
+  forall (m : message), equivocation_in_trace PreFree m tr ->
+  forall (v : validator), sender m = Some v ->
+  is_equivocating_statewise IM A sender s v.
+Proof.
+  intros * Htr_min m (pre & item & suffix & -> & Hinput & Hno_output) v Hsender.
+  eapply full_node_is_globally_equivocating_statewise_iff;
+    [by apply channel_authentication_sender_safety | done |].
+  eapply full_node_is_globally_equivocating_iff; [done.. |].
+  eapply state_to_minimal_equivocation_trace_equivocation_monotonic_final;
+    [done | by apply elem_of_app; right; left |].
+  apply reachable_composite_state_to_trace in Htr_min;
+    [| by apply minimal_equivocation_choice_is_choosing_well].
+  apply finite_valid_trace_init_to_prefix with (pre := pre ++ [item]) in Htr_min;
+    [| by exists suffix; simplify_list_eq].
+  rewrite finite_trace_last_is_last in Htr_min.
+  apply valid_trace_last_pstate in Htr_min as Hditem.
+  eapply full_node_is_globally_equivocating_iff; [done.. |].
+  apply finite_valid_trace_init_to_snoc in Htr_min as Hitem.
+  destruct Hitem as (_ & Hitem & _).
+  exists m; constructor; [done |..].
+  - exists (projT1 (l item)).
+    apply input_valid_transition_preloaded_project_active_free in Hitem.
+    by eapply has_been_received_step_update; [done | left].
+  - contradict Hno_output.
+    destruct (has_been_sent_step_update (vlsm := Free) Hitem m) as [[] _]; [done |..].
+Admitted.
+
+End sec_tracewise_equivocation.
+
 End sec_minimal_equivocation_trace.

theories/Core/MessageDependencies.v

@@ -823,6 +823,25 @@ Definition full_node_is_globally_equivocating
   (s : composite_state IM) (v : validator) : Prop :=
   exists m : message, FullNodeGlobalEquivocationEvidence s v m.
 
+Lemma full_node_is_globally_equivocating_statewise_iff
+  (A : validator -> index) (Hsender_safety : sender_safety_alt_prop IM A sender) :
+  forall (s : composite_state IM), constrained_state_prop Free s ->
+  forall (v : validator),
+  full_node_is_globally_equivocating s v
+    <->
+  is_equivocating_statewise IM A sender s v.
+Proof.
+  intros s Hs v; split.
+  - intros [m [Hsender [i Hreceived] Hnsent]].
+    exists i, m; split_and!; [done | | done].
+    by do 2 red; contradict Hnsent; eexists.
+  - intros (i & m & Hsender & Hnsent & Hreceived).
+    exists m; constructor; [done | by eexists |].
+    do 2 red in Hnsent; contradict Hnsent.
+    apply valid_state_has_trace in Hs as (? & ? & ?).
+    by eapply has_been_sent_iff_by_sender.
+Qed.
+
 Lemma full_node_is_globally_equivocating_stronger s v :
   full_node_is_globally_equivocating s v ->
   msg_dep_is_globally_equivocating s v.