From 2299f1a4f3a9e58a89a35c3fc18c8ae582a7cbd6 Mon Sep 17 00:00:00 2001 From: Traian Florin Serbanuta Date: Thu, 14 Dec 2023 09:30:37 +0200 Subject: [PATCH] Progress --- theories/Core/Equivocation.v | 8 ++ .../Equivocation/MinimalEquivocationTrace.v | 84 ++++++++++++++++++- theories/Core/MessageDependencies.v | 19 +++++ 3 files changed, 109 insertions(+), 2 deletions(-) diff --git a/theories/Core/Equivocation.v b/theories/Core/Equivocation.v index 55dcd145..c1e6bb9f 100644 --- a/theories/Core/Equivocation.v +++ b/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. diff --git a/theories/Core/Equivocation/MinimalEquivocationTrace.v b/theories/Core/Equivocation/MinimalEquivocationTrace.v index 99acdcd1..d7452884 100644 --- a/theories/Core/Equivocation/MinimalEquivocationTrace.v +++ b/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. -End sec_minimal_equivocation_trace. +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 |..]. + Search input output. + specialize (has_been_sent_examine_one_trace (vlsm := Free)). + + +End sec_tracewise_equivocation. diff --git a/theories/Core/MessageDependencies.v b/theories/Core/MessageDependencies.v index 95325c44..c992dd5c 100644 --- a/theories/Core/MessageDependencies.v +++ b/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.