diff --git a/theories/Core/Equivocation/LimitedMessageEquivocation.v b/theories/Core/Equivocation/LimitedMessageEquivocation.v index 8d110086..0a22e316 100644 --- a/theories/Core/Equivocation/LimitedMessageEquivocation.v +++ b/theories/Core/Equivocation/LimitedMessageEquivocation.v @@ -128,13 +128,12 @@ Context `{forall i, HasBeenSentCapability (IM i)} `{forall i, HasBeenReceivedCapability (IM i)} (Free := free_composite_vlsm IM) - (PreFree := pre_loaded_with_all_messages_vlsm Free) `{finite.Finite validator} `{ReachableThreshold validator Cv threshold} (A : validator -> index) (sender : message -> option validator) - `{!RelDecision (constrained_composite_state_is_equivocating_tracewise IM A sender)} - (HBE : BasicEquivocation (valid_state PreFree) validator Cv threshold + `{RelDecision _ _ (is_equivocating_tracewise_no_has_been_sent IM A sender)} + (HBE : BasicEquivocation (composite_state IM) validator Cv threshold := equivocation_dec_tracewise IM threshold A sender) . diff --git a/theories/Core/Equivocation/TraceWiseEquivocation.v b/theories/Core/Equivocation/TraceWiseEquivocation.v index a38a8e30..33433358 100644 --- a/theories/Core/Equivocation/TraceWiseEquivocation.v +++ b/theories/Core/Equivocation/TraceWiseEquivocation.v @@ -303,26 +303,19 @@ Proof. by destruct prefix; inversion Heq. Qed. -Definition constrained_composite_state_is_equivocating_tracewise - (vs : valid_state PreFree) (v : validator) : Prop := - is_equivocating_tracewise_no_has_been_sent (` vs) v. - Context - `{!RelDecision constrained_composite_state_is_equivocating_tracewise} + `{RelDecision _ _ is_equivocating_tracewise_no_has_been_sent} . #[export] Program Instance equivocation_dec_tracewise - : BasicEquivocation (valid_state PreFree) validator Cv threshold := + : BasicEquivocation (composite_state IM) validator Cv threshold := { state_validators := fun _ => list_to_set (enum validator); is_equivocating := is_equivocating_tracewise_no_has_been_sent; }. -Lemma equivocating_validators_is_equivocating_tracewise_iff - (s : composite_state IM) (Hs : valid_state_prop PreFree s) (v : validator) : - v ∈ equivocating_validators (exist _ s Hs) - <-> - is_equivocating_tracewise_no_has_been_sent s v. +Lemma equivocating_validators_is_equivocating_tracewise_iff s v + : v ∈ equivocating_validators s <-> is_equivocating_tracewise_no_has_been_sent s v. Proof. unfold equivocating_validators. simpl. @@ -330,53 +323,43 @@ Proof. by itauto (apply elem_of_enum). Qed. -#[export] Instance valid_state_equiv : Equiv (valid_state PreFree) := - fun s s' => proj1_sig s = proj1_sig s'. - -#[export] Instance valid_state_equivocating_validators_proper : - Proper ((≡) ==> (≡)) equivocating_validators. -Proof. - intros [s Hs] [_s Hs'] Heqv v; cbv in Heqv; subst _s. - by split; intros Hv; - do 2 eapply equivocating_validators_is_equivocating_tracewise_iff. -Qed. - Lemma equivocating_validators_empty_in_initial_state - (s : composite_state IM) (His : composite_initial_state_prop IM s) : - equivocating_validators (exist _ s (initial_state_is_valid PreFree _ His)) ≡@{Cv} ∅. + (s : composite_state IM) + (His : composite_initial_state_prop IM s) + : equivocating_validators s ≡@{Cv} ∅. Proof. - apply equiv_empty; intros v Hv. - apply equivocating_validators_is_equivocating_tracewise_iff in Hv. - by contradict Hv; apply initial_state_not_is_equivocating_tracewise. + intro v. split. + - rewrite equivocating_validators_is_equivocating_tracewise_iff. + by apply initial_state_not_is_equivocating_tracewise with (v := v) in His. + - by intro HV; contradict HV; apply not_elem_of_empty. Qed. Lemma input_valid_transition_receiving_no_sender_reflects_equivocating_validators - (l : label PreFree) (s s' : composite_state IM) (om om' : option message) + l s om s' om' (Ht : input_valid_transition PreFree l (s, om) (s', om')) - (Hno_sender : om ≫= sender = None) : - equivocating_validators (exist _ s' (input_valid_transition_destination _ Ht)) - ⊆ - equivocating_validators (exist _ s (input_valid_transition_origin _ Ht)). + (Hno_sender : om ≫= sender = None) + : equivocating_validators s' ⊆ equivocating_validators s. Proof. - intros v Hv%equivocating_validators_is_equivocating_tracewise_iff. + intros v Hs'%equivocating_validators_is_equivocating_tracewise_iff. by eapply equivocating_validators_is_equivocating_tracewise_iff, - transition_receiving_no_sender_reflects_is_equivocating_tracewise. + transition_receiving_no_sender_reflects_is_equivocating_tracewise. Qed. Lemma initial_state_equivocators_weight - (s : composite_state IM) (His : composite_initial_state_prop IM s) - : equivocation_fault (exist _ s (initial_state_is_valid PreFree _ His)) = 0%R. + (s : composite_state IM) + (Hs : composite_initial_state_prop IM s) + : equivocation_fault s = 0%R. Proof. - by apply sum_weights_empty, equivocating_validators_empty_in_initial_state. + apply equivocating_validators_empty_in_initial_state, elements_empty_iff in Hs. + unfold equivocation_fault. + by apply sum_weights_empty, elements_empty_iff. Qed. Lemma composite_transition_no_sender_equivocators_weight - (l : label PreFree) (s s' : composite_state IM) (om om' : option message) + l s om s' om' (Ht : input_valid_transition PreFree l (s, om) (s', om')) - (Hno_sender : om ≫= sender = None) : - (equivocation_fault (exist _ s' (input_valid_transition_destination _ Ht)) - <= - equivocation_fault (exist _ s (input_valid_transition_origin _ Ht)))%R. + (Hno_sender : om ≫= sender = None) + : (equivocation_fault s' <= equivocation_fault s)%R. Proof. specialize (input_valid_transition_receiving_no_sender_reflects_equivocating_validators _ _ _ _ _ Ht Hno_sender) as Heqv. diff --git a/theories/Core/Equivocation/WitnessedEquivocation.v b/theories/Core/Equivocation/WitnessedEquivocation.v index 27649001..79f84021 100644 --- a/theories/Core/Equivocation/WitnessedEquivocation.v +++ b/theories/Core/Equivocation/WitnessedEquivocation.v @@ -36,15 +36,15 @@ Context (IM : index -> VLSM message) `{forall i : index, HasBeenSentCapability (IM i)} `{forall i : index, HasBeenReceivedCapability (IM i)} + `{finite.Finite validator} (Free := free_composite_vlsm IM) (PreFree := pre_loaded_with_all_messages_vlsm Free) (threshold : R) `{ReachableThreshold validator Cv threshold} - `{!finite.Finite validator} (A : validator -> index) (sender : message -> option validator) - `{!RelDecision (constrained_composite_state_is_equivocating_tracewise IM A sender)} - (Htracewise_BasicEquivocation : BasicEquivocation (valid_state PreFree) validator Cv threshold + `{RelDecision _ _ (is_equivocating_tracewise_no_has_been_sent IM A sender)} + (Htracewise_BasicEquivocation : BasicEquivocation (composite_state IM) validator Cv threshold := equivocation_dec_tracewise IM threshold A sender) (equivocating_validators := equivocating_validators (BasicEquivocation := Htracewise_BasicEquivocation)) @@ -55,44 +55,21 @@ Context equivocators is precisely that of the [equivocating_validators] of <>. *) Definition trace_witnessing_equivocation_prop - {is s : composite_state IM} {tr : list (composite_transition_item IM)} - (Htr : finite_valid_trace_init_to PreFree is s tr) + is tr + (s := finite_trace_last is tr) : Prop := - forall v, v ∈ equivocating_validators (exist _ s (valid_trace_last_pstate Htr)) <-> + forall v, v ∈ equivocating_validators s <-> exists (m : message), (sender m = Some v) /\ equivocation_in_trace PreFree m tr. -Lemma trace_witnessing_equivocation_prop_pi - (is s s' : composite_state IM) (tr : list (composite_transition_item IM)) - (Htr : finite_valid_trace_init_to PreFree is s tr) - (Htr' : finite_valid_trace_init_to PreFree is s' tr) : - trace_witnessing_equivocation_prop Htr - <-> - trace_witnessing_equivocation_prop Htr'. -Proof. - unfold trace_witnessing_equivocation_prop. - remember (exist _ _ _) as sigma. - remember (exist _ _ (valid_trace_last_pstate Htr')) as sigma'. - apply valid_trace_get_last in Htr as Heqs. - apply valid_trace_get_last in Htr' as Heqs'. - subst s s'. - assert (Heqv : sigma ≡ sigma') by (subst; done). - unshelve eapply valid_state_equivocating_validators_proper - with (Cv := Cv) in Heqv; try typeclasses eauto. - apply forall_proper; intro v. - by split; intros <-; [symmetry |]; apply Heqv. -Qed. - Lemma equivocating_senders_in_trace_witnessing_equivocation_prop - {is s : composite_state IM} {tr : list (composite_transition_item IM)} - (Htr : finite_valid_trace_init_to PreFree is s tr) - (Hwitness : trace_witnessing_equivocation_prop Htr) - : set_eq - (elements (equivocating_validators (exist _ s (valid_trace_last_pstate Htr)))) - (equivocating_senders_in_trace IM sender tr). + is tr + (Htr : trace_witnessing_equivocation_prop is tr) + (s := finite_trace_last is tr) + : set_eq (elements (equivocating_validators s)) (equivocating_senders_in_trace IM sender tr). Proof. split; intros v Hv. - - by apply elem_of_elements, Hwitness in Hv; apply elem_of_equivocating_senders_in_trace. - - by eapply elem_of_elements, Hwitness, elem_of_equivocating_senders_in_trace. + - by apply elem_of_elements, Htr in Hv; apply elem_of_equivocating_senders_in_trace. + - by eapply elem_of_elements, Htr, elem_of_equivocating_senders_in_trace. Qed. (** @@ -102,9 +79,9 @@ Qed. Class WitnessedEquivocationCapability : Prop := { is_equivocating_tracewise_witness : - forall (s : composite_state IM), valid_state_prop PreFree s -> - exists is tr (Htr : finite_valid_trace_init_to PreFree is s tr), - trace_witnessing_equivocation_prop Htr + forall s, valid_state_prop PreFree s -> + exists is tr, finite_valid_trace_init_to PreFree is s tr /\ + trace_witnessing_equivocation_prop is tr }. Section sec_witnessed_equivocation_properties. @@ -115,18 +92,19 @@ Context . Lemma initial_state_witnessing_equivocation_prop - s (Hs : composite_initial_state_prop IM s) : - trace_witnessing_equivocation_prop - (conj (finite_valid_trace_from_to_empty _ _ (initial_state_is_valid PreFree _ Hs)) Hs). + s + (Hs : composite_initial_state_prop IM s) + : trace_witnessing_equivocation_prop s []. Proof. - split. - - intros Hv; contradict Hv; apply elem_of_equiv_empty, equiv_empty. - clear v; intros v Hv. - eapply valid_state_equivocating_validators_proper - with (x := exist _ s (initial_state_is_valid PreFree _ Hs)) in Hv; [| done]. - by eapply equivocating_validators_empty_in_initial_state. - - intros [m [_ Hmsg]]. - by elim (no_equivocation_in_empty_trace PreFree m). + intros v. + unfold finite_trace_last. simpl. + rewrite <- elem_of_elements. + replace (elements (equivocating_validators s)) with (@nil validator). + simpl. + split; [by inversion 1 |]. + intros [m [_ Hmsg]]. + - by elim (no_equivocation_in_empty_trace PreFree m). + - by symmetry; apply elements_empty_iff, equivocating_validators_empty_in_initial_state. Qed. (** @@ -134,20 +112,20 @@ Qed. its final transition is monotonic w.r.t. the [equivocating_validators]. *) Lemma equivocating_validators_witness_monotonicity - (is s' : composite_state IM) + (is s : composite_state IM) (tr : list (composite_transition_item IM)) + (Htr : finite_valid_trace_init_to PreFree is s tr) (item : composite_transition_item IM) - (Htr : finite_valid_trace_init_to PreFree is s' (tr ++ [item])) - (Hwitness : trace_witnessing_equivocation_prop Htr) - (s := finite_trace_last is tr) - (Htr' := finite_valid_trace_init_to_prefix_1 PreFree Htr) : - equivocating_validators (exist _ s (valid_trace_last_pstate Htr')) - ⊆ - equivocating_validators (exist _ s' (valid_trace_last_pstate Htr)). + (Hwitness : trace_witnessing_equivocation_prop is (tr ++ [item])) + (s' := destination item) + : equivocating_validators s ⊆ equivocating_validators s'. Proof. - intros v Hv; apply Hwitness. + intros v Hv. + specialize (Hwitness v). + rewrite finite_trace_last_is_last in Hwitness. + apply Hwitness. apply equivocating_validators_is_equivocating_tracewise_iff in Hv. - specialize (Hv _ _ Htr') as [m [Hmsg Heqv]]. + specialize (Hv _ _ Htr) as [m [Hmsg Heqv]]. exists m. split; [done |]. by apply equivocation_in_trace_prefix. Qed. @@ -160,24 +138,25 @@ Qed. [trace_witnessing_equivocation_prop]erty. *) Lemma input_valid_transition_reflects_trace_witnessing_equivocation_prop - (is s' : composite_state IM) + (is s : composite_state IM) (tr : list (composite_transition_item IM)) + (Htr : finite_valid_trace_init_to PreFree is s tr) (item : composite_transition_item IM) - (Htr : finite_valid_trace_init_to PreFree is s' (tr ++ [item])) - (s := finite_trace_last is tr) - (Htr' := finite_valid_trace_init_to_prefix_1 PreFree Htr) - (Hincl : equivocating_validators (exist _ s' (valid_trace_last_pstate Htr)) - ⊆ - equivocating_validators (exist _ s (valid_trace_last_pstate Htr'))) : - trace_witnessing_equivocation_prop Htr -> - trace_witnessing_equivocation_prop Htr'. + (Hwitness : trace_witnessing_equivocation_prop is (tr ++ [item])) + (s' := destination item) + (Hincl : equivocating_validators s' ⊆ equivocating_validators s) + : trace_witnessing_equivocation_prop is tr. Proof. - intros Hwitness v; split. + apply finite_valid_trace_init_to_last in Htr as Hlst. + intros v; split; simpl in *; rewrite Hlst in *. - intros Hv. - by unshelve eapply equivocating_validators_is_equivocating_tracewise_iff - with (Cv := Cv); try typeclasses eauto; cycle 3. + by eapply equivocating_validators_is_equivocating_tracewise_iff + with (ReachableThreshold0 := H11). - intros (msg & Hsender & Heqv). - apply Hincl, Hwitness. + apply Hincl. + specialize (Hwitness v); + rewrite finite_trace_last_is_last in Hwitness; + apply Hwitness. exists msg. split; [done |]. by apply equivocation_in_trace_prefix. Qed. @@ -191,18 +170,18 @@ Lemma equivocating_validators_step_update l s om s' om' (Ht : input_valid_transition PreFree l (s, om) (s', om')) v - : v ∈ equivocating_validators (exist _ s' (input_valid_transition_destination _ Ht)) -> - v ∈ equivocating_validators (exist _ s (input_valid_transition_origin _ Ht)) \/ + : v ∈ equivocating_validators s' -> + v ∈ equivocating_validators s \/ (exists m, om = Some m /\ sender m = Some v /\ forall is tr (Htr : finite_valid_trace_init_to PreFree is s tr) - (Hwitness : trace_witnessing_equivocation_prop Htr), + (Hwitness : trace_witnessing_equivocation_prop is tr), ~ trace_has_message (field_selector output) m tr). Proof. intro Hv. - destruct (decide (v ∈ equivocating_validators (s ↾ input_valid_transition_origin PreFree Ht))) - as [Hnv | Hnv]; [by left | right]. + destruct (decide (v ∈ elements (equivocating_validators s))) as [Hnv | Hnv] + ; rewrite elem_of_elements in Hnv; [by left | right]. apply equivocating_validators_is_equivocating_tracewise_iff in Hv. destruct (transition_is_equivocating_tracewise_char IM A sender _ _ _ _ _ Ht _ Hv) as [| Hom]; @@ -219,9 +198,9 @@ Proof. by inversion Heq_m. - elim Hnv. specialize (Hwitness v). - eapply valid_state_equivocating_validators_proper; - cycle 1; [apply Hwitness | done]. - exists m'. split; [done |]. + apply finite_valid_trace_from_to_last in Htr as Hs. + simpl in Hs, Hwitness. rewrite Hs in Hwitness. + apply Hwitness. exists m'. split; [done |]. exists prefix, item, suffix'. split; [| done]. change (item :: suffix' ++ [item']) with ([item] ++ suffix' ++ [item']) in Heq. @@ -243,95 +222,78 @@ Qed. is not sent by any trace witnessing the source of the transition. *) Lemma equivocating_validators_witness_last_char - (is s' : composite_state IM) + (is : composite_state IM) (tr : list (composite_transition_item IM)) - (item : composite_transition_item IM) + (l : composite_label IM) + (om : option message) + (s' : composite_state IM) + (om' : option message) + (item := {| l := l; input := om; destination := s'; output := om' |}) (Htr_item : finite_valid_trace_init_to PreFree is s' (tr ++ [item])) - (Hwitness : trace_witnessing_equivocation_prop Htr_item) + (Hwitness : trace_witnessing_equivocation_prop is (tr ++ [item])) (s := finite_trace_last is tr) - (Htr := finite_valid_trace_init_to_prefix_1 PreFree Htr_item) : - equivocating_validators (exist _ s (valid_trace_last_pstate Htr)) - ≡@{Cv} - equivocating_validators (exist _ s' (valid_trace_last_pstate Htr_item)) - /\ trace_witnessing_equivocation_prop Htr + : equivocating_validators s ≡@{Cv} equivocating_validators s' + /\ trace_witnessing_equivocation_prop is tr \/ - (exists m, input item = Some m /\ + (exists m, om = Some m /\ exists v, sender m = Some v /\ - v ∉ equivocating_validators (exist _ s (valid_trace_last_pstate Htr)) /\ - equivocating_validators (exist _ s' (valid_trace_last_pstate Htr_item)) - ≡@{Cv} - {[ v ]} ∪ (equivocating_validators (exist _ s (valid_trace_last_pstate Htr))) /\ - forall (is : composite_state IM) (tr : list transition_item) - (Htr : finite_valid_trace_init_to PreFree is s tr), - trace_witnessing_equivocation_prop Htr -> + v ∉ equivocating_validators s /\ + equivocating_validators s' ≡@{Cv} {[ v ]} ∪ (equivocating_validators s) /\ + forall (is : composite_state IM) (tr : list transition_item), + finite_valid_trace_init_to PreFree is s tr -> + trace_witnessing_equivocation_prop is tr -> ~ trace_has_message (field_selector output) m tr). Proof. - destruct item as [l om _s' om']. - apply finite_valid_trace_init_to_snoc in Htr_item as H_tr. - destruct H_tr as (H_tr & Hitem & Hdestination). - cbn in Hdestination; subst _s'. - inversion Hitem. - apply equivocating_validators_witness_monotonicity in Hwitness as Hincl. + destruct Htr_item as [Htr Hinit]. + apply finite_valid_trace_from_to_app_split in Htr. + destruct Htr as [Htr Hitem]. + inversion_clear Hitem. clear Htl. subst s. + apply equivocating_validators_witness_monotonicity with (s := (finite_trace_last is tr)) + in Hwitness as Hincl + ; [| by split]. + remember (finite_trace_last is tr) as s. destruct (om ≫= sender) as [v |] eqn: Heq_v. - destruct om as [m |]; [| by inversion Heq_v]. simpl in Heq_v. - destruct (decide - (equivocating_validators (s ↾ valid_trace_last_pstate Htr) - ≡ equivocating_validators (s' ↾ valid_trace_last_pstate Htr_item))) - as [Hequiv | Hnequiv]. - + left; split; [done |]. - apply input_valid_transition_reflects_trace_witnessing_equivocation_prop; - [| done]. - rewrite <- Hequiv. - by apply set_equiv_subseteq, valid_state_equivocating_validators_proper. + destruct (decide (set_eq (elements (equivocating_validators s)) (elements (equivocating_validators s')))). + + apply set_eq_fin_set in s0; left; split; [done |]. + by apply + (input_valid_transition_reflects_trace_witnessing_equivocation_prop + _ _ _ (conj Htr Hinit) _ Hwitness); + subst; intros ? ?; apply s0. + right. exists m; split; [done |]. exists v; split; [done |]. - specialize (equivocating_validators_step_update _ _ _ _ _ Hitem) as Honly_v. - assert (exists v, - v ∈ equivocating_validators (exist _ s' (valid_trace_last_pstate Htr_item)) - /\ - v ∉ equivocating_validators (exist _ s (valid_trace_last_pstate Htr))) - as (v'& Heqv & Hneqv). + specialize (equivocating_validators_step_update _ _ _ _ _ Ht) as Honly_v. + simpl in Honly_v. + assert (Hv : exists v, v ∈ equivocating_validators s' /\ v ∉ equivocating_validators s). { setoid_rewrite <- elem_of_elements. apply Exists_exists. - apply neg_Forall_Exists_neg; [by intro; apply elem_of_list_dec |]. - contradict Hnequiv; split. - - intros Hx; apply Hincl. - by eapply valid_state_equivocating_validators_proper; cycle 1. - - rewrite <- !elem_of_elements. - by rewrite Forall_forall in Hnequiv; apply Hnequiv. + apply neg_Forall_Exists_neg; [intro; apply elem_of_list_dec |]. + intro all. elim n. + split; [| by rewrite Forall_forall in all]. + by unfold set_eq, subseteq, list_subseteq; setoid_rewrite elem_of_elements. } - destruct (Honly_v v') as [| [_m [Heq_m [Heq_v' Hweqv]]]]; - [by eapply valid_state_equivocating_validators_proper; cycle 1 - | by contradict Hneqv; eapply valid_state_equivocating_validators_proper; cycle 1 - |]. - apply Some_inj in Heq_m as <-. - rewrite Heq_v in Heq_v'; apply Some_inj in Heq_v' as <-. + destruct Hv as [v' [Heqv Hneqv]]. + apply Honly_v in Heqv as Heq_v'. + destruct Heq_v' as [| [_m [Heq_m [Heq_v' Hweqv]]]]; [by subst |]. + inversion Heq_m. subst _m. clear Heq_m. + assert (v' = v) by congruence. subst v'. clear Heq_v'. split; [done |]. split; [| by subst]. intro v'; split; intro Hv'. * apply elem_of_union. - destruct (decide (v' ∈ equivocating_validators (s ↾ valid_trace_last_pstate Htr))) - as [Hveqv | Hveqv]; [by right | left]. + destruct (decide (v' ∈ elements (equivocating_validators s))) + as [Hveqv | Hveqv]; rewrite elem_of_elements in Hveqv; + [by right | left]. apply elem_of_singleton. - destruct (Honly_v v') as [| [_m [Heq_m [Heq_v' _]]]]; - [by eapply valid_state_equivocating_validators_proper; cycle 1 - | by contradict Hveqv; eapply valid_state_equivocating_validators_proper; cycle 1 - |]. - by apply Some_inj in Heq_m as <-; congruence. + by apply Honly_v in Hv'; + destruct Hv' as [| [_m [Heq_m [Heq_v' _]]]]; [by subst |]; congruence. * by apply elem_of_union in Hv' as [Heq_v' | Hs'0] ; [by apply elem_of_singleton in Heq_v'; subst v' | by apply Hincl]. - left; split. + subst; intro v; split; [by apply Hincl |]. intros Hvs'. - unshelve eapply valid_state_equivocating_validators_proper, - input_valid_transition_receiving_no_sender_reflects_equivocating_validators; - cycle 5; [done | done | done |..]. - by eapply valid_state_equivocating_validators_proper; cycle 1. - + eapply input_valid_transition_reflects_trace_witnessing_equivocation_prop; [| done]. - intros v Hv. - unshelve eapply valid_state_equivocating_validators_proper, - input_valid_transition_receiving_no_sender_reflects_equivocating_validators; - cycle 5; [done | done | done |..]. - by eapply valid_state_equivocating_validators_proper; cycle 1. + by eapply input_valid_transition_receiving_no_sender_reflects_equivocating_validators. + + eapply input_valid_transition_reflects_trace_witnessing_equivocation_prop; [done | done |]. + by eapply input_valid_transition_receiving_no_sender_reflects_equivocating_validators. Qed. (** ** Strongly witnessed equivocation @@ -339,47 +301,9 @@ Qed. A stronger [trace_witnessing_equivocation_prop]erty requires that any prefix of a trace is witnessing equivocation for its corresponding final state. *) -Definition strong_trace_witnessing_equivocation_prop - {is s} {tr} (Htr : finite_valid_trace_init_to PreFree is s tr) := - forall prefix (Hprefix : prefix `prefix_of` tr), - trace_witnessing_equivocation_prop - (finite_valid_trace_init_to_prefix _ Htr Hprefix). - -Lemma strong_trace_witnessing_equivocation_prop_stronger - {is s} {tr} (Htr : finite_valid_trace_init_to PreFree is s tr) : - strong_trace_witnessing_equivocation_prop Htr -> - trace_witnessing_equivocation_prop Htr. -Proof. - intros Hstrong. - unshelve eapply trace_witnessing_equivocation_prop_pi, Hstrong. - by eexists []; rewrite app_nil_r. -Qed. - -Lemma strong_trace_witnessing_equivocation_prop_pi - (is s s' : composite_state IM) (tr : list (composite_transition_item IM)) - (Htr : finite_valid_trace_init_to PreFree is s tr) - (Htr' : finite_valid_trace_init_to PreFree is s' tr) : - strong_trace_witnessing_equivocation_prop Htr - <-> - strong_trace_witnessing_equivocation_prop Htr'. -Proof. - apply forall_proper; intro prefix. - apply forall_proper; intro Hprefix. - by apply trace_witnessing_equivocation_prop_pi. -Qed. - -Lemma strong_trace_witnessing_equivocation_prop_prefix - (is s : composite_state IM) (tr : list (composite_transition_item IM)) - (Htr : finite_valid_trace_init_to PreFree is s tr) : - strong_trace_witnessing_equivocation_prop Htr -> - forall prefix (Hprefix : prefix `prefix_of` tr), - strong_trace_witnessing_equivocation_prop - (finite_valid_trace_init_to_prefix _ Htr Hprefix). -Proof. - intros Hwitness prefix His_prefix pre His_pre. - unshelve eapply trace_witnessing_equivocation_prop_pi, Hwitness. - by etransitivity. -Qed. +Definition strong_trace_witnessing_equivocation_prop is tr := + forall prefix suffix, prefix ++ suffix = tr -> + trace_witnessing_equivocation_prop is prefix. (** An advantage of the [strong_trace_witnessing_equivocation_prop]erty @@ -389,40 +313,35 @@ Lemma strong_witness_equivocating_validators_prefix_monotonicity (is s : composite_state IM) (tr : list (composite_transition_item IM)) (Htr : finite_valid_trace_init_to PreFree is s tr) - (Hwitness : strong_trace_witnessing_equivocation_prop Htr) - prefix - (His_prefix : prefix `prefix_of` tr) - (Hprefix := finite_valid_trace_init_to_prefix _ Htr His_prefix) - (ps := finite_trace_last is prefix) : - equivocating_validators (exist _ ps (valid_trace_last_pstate Hprefix)) - ⊆ - equivocating_validators (exist _ s (valid_trace_last_pstate Htr)). + (Hwitness : strong_trace_witnessing_equivocation_prop is tr) + prefix suffix + (Heqtr : prefix ++ suffix = tr) + (ps := finite_trace_last is prefix) + : equivocating_validators ps ⊆ equivocating_validators s. Proof. - revert s Htr Hwitness prefix His_prefix Hprefix ps. - induction tr using rev_ind; intros. - - destruct Htr as [Htr Hinit]; inversion Htr; subst. - apply prefix_nil_inv in His_prefix as Heq_prefix; subst. - by apply set_equiv_subseteq, valid_state_equivocating_validators_proper. - - apply finite_valid_trace_init_to_snoc in Htr as Htrx. - destruct Htrx as [H_tr Hx]. - assert (Hwitness_tr : strong_trace_witnessing_equivocation_prop H_tr). + revert prefix suffix Heqtr ps. + induction Htr using finite_valid_trace_init_to_rev_ind; intros. + - by apply app_eq_nil in Heqtr as []; subst. + - remember {| input := iom |} as item. + spec IHHtr. { - intros pre Hpre. - unshelve eapply trace_witnessing_equivocation_prop_pi, Hwitness. - by apply prefix_app_r. + intros pre suf Heq. + specialize (Hwitness pre (suf ++ [item])). + apply Hwitness. + by subst; apply app_assoc. } - destruct (Datatypes.id His_prefix) as [suffix Heqtr]. - destruct_list_last suffix suffix' item Heqsuffix; subst. + destruct_list_last suffix suffix' _item Heqsuffix. + rewrite app_nil_r in Heqtr. subst. subst ps. - apply valid_trace_get_last in Htr as Heqs; subst. - by apply set_equiv_subseteq, valid_state_equivocating_validators_proper. - + rewrite app_assoc in Heqtr. apply app_inj_tail in Heqtr as [-> ->]. - intros v Hv. - eapply equivocating_validators_witness_monotonicity; - [by apply strong_trace_witnessing_equivocation_prop_stronger |]. - eapply valid_state_equivocating_validators_proper; cycle 1; - [unshelve eapply (IHtr _ _ Hwitness_tr prefix); [by eexists |] | done]. - by eapply valid_state_equivocating_validators_proper; cycle 1. + by rewrite finite_trace_last_is_last. + + rewrite app_assoc in Heqtr. apply app_inj_tail in Heqtr. + destruct Heqtr as [Heqtr Heq_item]. subst _item. + specialize (IHHtr _ _ Heqtr). + transitivity (equivocating_validators s) + ; [done |]. + specialize (Hwitness (tr ++ [item]) []). + spec Hwitness. { apply app_nil_r. } + replace sf with (destination item) by (subst; done). + by apply (equivocating_validators_witness_monotonicity _ _ _ Htr _ Hwitness). Qed. (** @@ -432,45 +351,37 @@ Qed. the proof of Lemma [preloaded_has_strong_trace_witnessing_equivocation_prop]. *) Lemma strong_trace_witnessing_equivocation_prop_extend_eq - s is tr' (Htr' : finite_valid_trace_init_to PreFree is s tr') - item (Hitem : input_valid_transition_item PreFree s item) - (Htr'_item := finite_valid_trace_init_to_snoc_rev _ Htr' Hitem) - is' tr'' (Htr'' : finite_valid_trace_init_to PreFree is' s tr'') - (Htr''_item := finite_valid_trace_init_to_snoc_rev _ Htr'' Hitem) - (Hprefix : strong_trace_witnessing_equivocation_prop Htr'') - (Hwitness : trace_witnessing_equivocation_prop Htr'_item) - (Heq : - equivocating_validators (exist _ s (valid_trace_last_pstate Htr')) - ≡@{Cv} - equivocating_validators (exist _ (destination item) (input_valid_transition_destination _ Hitem))) - : strong_trace_witnessing_equivocation_prop Htr''_item. + s + is tr' + (Htr' : finite_valid_trace_init_to PreFree is s tr') + is' tr'' + (Htr'' : finite_valid_trace_init_to PreFree is' s tr'') + (Hprefix : strong_trace_witnessing_equivocation_prop is' tr'') + item + (Hwitness : trace_witnessing_equivocation_prop is (tr' ++ [item])) + (Heq : equivocating_validators s ≡@{Cv} equivocating_validators (destination item)) + : strong_trace_witnessing_equivocation_prop is' (tr'' ++ [item]). Proof. - intros prefix His_prefix. - destruct (Datatypes.id His_prefix) as [suffix Heq_tr''_item]. + intros prefix suffix Heq_tr''_item. destruct_list_last suffix suffix' sitem Hsuffix_eq. - - rewrite app_nil_r in Heq_tr''_item; subst. - intro v. - specialize (Hprefix tr''). + - rewrite app_nil_r in Heq_tr''_item. + subst. + intro v. rewrite finite_trace_last_is_last. + specialize (Hprefix tr'' []). + spec Hprefix; [by apply app_nil_r |]. + apply valid_trace_get_last in Htr'' as Hlst'. split. - + intros Hv. - eapply valid_state_equivocating_validators_proper - with (x := destination item ↾ input_valid_transition_destination PreFree Hitem), - Heq in Hv; - [| by symmetry; apply finite_trace_last_is_last]. - unshelve eapply valid_state_equivocating_validators_proper, Hprefix in Hv - as (m & Hmsg & Heqv); - [by exists []; rewrite app_nil_r | | by apply (valid_trace_get_last Htr'')]. + + intros Hv. apply Heq in Hv. + rewrite <- Hlst' in Hv. + apply Hprefix in Hv. + destruct Hv as [m [Hmsg Heqv]]. exists m. split; [done |]. by apply equivocation_in_trace_prefix. - + intros (m & Hmsg & Heqv). + + intros [m [Hmsg Heqv]]. apply equivocation_in_trace_last_char in Heqv. destruct Heqv as [Heqv | Heqv]. - * eapply valid_state_equivocating_validators_proper - with (x := destination item ↾ input_valid_transition_destination PreFree Hitem); - [by unfold equiv, valid_state_equiv; cbn; rewrite finite_trace_last_is_last |]. - apply Heq. - unshelve eapply valid_state_equivocating_validators_proper, Hprefix; - [by exists []; rewrite app_nil_r | by symmetry; apply (valid_trace_get_last Htr'') |]. + * apply Heq. rewrite <- Hlst'. + apply Hprefix. by exists m. * destruct Heqv as [Heq_om Heqv]. assert (Heqv' : ~ trace_has_message (field_selector output) m tr'). @@ -483,64 +394,64 @@ Proof. spec Hconsistency; [by exists is, tr', Htr' |]. by specialize (Hconsistency is' tr'' Htr''). } - eapply valid_state_equivocating_validators_proper, Hwitness; - [by apply finite_trace_last_is_last |]. + specialize (Hwitness v). + rewrite finite_trace_last_is_last in Hwitness. + simpl in Hwitness. + apply Hwitness. subst. exists m. split; [done |]. by eexists tr', _, []. - rewrite app_assoc in Heq_tr''_item. apply app_inj_tail in Heq_tr''_item. destruct Heq_tr''_item as [Heq_tr'' Heq_item]. - by unshelve eapply trace_witnessing_equivocation_prop_pi, Hprefix; eexists. + by apply (Hprefix _ _ Heq_tr''). Qed. Lemma strong_trace_witnessing_equivocation_prop_extend_neq - s is tr (Htr : finite_valid_trace_init_to PreFree is s tr) - (Hprefix : strong_trace_witnessing_equivocation_prop Htr) - item (Hitem : input_valid_transition_item PreFree s item) + s + is tr + (Htr : finite_valid_trace_init_to PreFree is s tr) + (Hprefix : strong_trace_witnessing_equivocation_prop is tr) + item msg (Hmsg : input item = Some msg) (Hwneq : ¬ trace_has_message (field_selector output) msg tr) v (Hsender : sender msg = Some v) - (Hneq : - equivocating_validators (exist _ (destination item) (input_valid_transition_destination _ Hitem)) - ≡@{Cv} - {[ v ]} ∪ (equivocating_validators (exist _ s (valid_trace_last_pstate Htr)))) : - strong_trace_witnessing_equivocation_prop - (finite_valid_trace_init_to_snoc_rev PreFree Htr Hitem). + (Hneq : equivocating_validators (destination item) ≡@{Cv} {[ v ]} ∪ (equivocating_validators s)) + : strong_trace_witnessing_equivocation_prop is (tr ++ [item]). Proof. - intros prefix His_prefix. - destruct (Datatypes.id His_prefix) as [suffix Heq_tr''_item]. + intros prefix suffix Heq_tr''_item. destruct_list_last suffix suffix' sitem Hsuffix_eq. - - rewrite app_nil_r in Heq_tr''_item; subst. - intro v'; split. - + intros Hv'. - eapply valid_state_equivocating_validators_proper, Hneq in Hv'; - [| by symmetry; apply finite_trace_last_is_last]. - rewrite elem_of_union, elem_of_singleton in Hv'. - destruct Hv' as [-> | Hv']. - * exists msg. split; [done |]. + - rewrite app_nil_r in Heq_tr''_item. + subst prefix suffix. + intro v'. rewrite finite_trace_last_is_last. simpl. + specialize (Hprefix tr []). + spec Hprefix; [by apply app_nil_r |]. + apply valid_trace_get_last in Htr as Hlst'. + split. + + intros Hv'. apply Hneq in Hv'. + apply elem_of_union in Hv'; rewrite elem_of_singleton in Hv'. + rewrite <- Hlst' in Hv'. + destruct Hv' as [Heq_v | Hv']. + * subst. + exists msg. split; [done |]. by eexists tr, _, []. - * unshelve eapply valid_state_equivocating_validators_proper, Hprefix - in Hv' as (m & ? & Heqv); - [| by exists []; rewrite app_nil_r | | by apply valid_trace_get_last in Htr as Hlst]. + * apply Hprefix in Hv'. + destruct Hv' as [m [? Heqv]]. exists m. split; [done |]. by apply equivocation_in_trace_prefix. - + intros (m & ? & Heqv). + + intros [m [? Heqv]]. apply equivocation_in_trace_last_char in Heqv. - eapply valid_state_equivocating_validators_proper, Hneq; - [by apply finite_trace_last_is_last |]. - rewrite elem_of_union, elem_of_singleton. + apply Hneq, elem_of_union; rewrite elem_of_singleton. destruct Heqv as [Heqv | Heqv]. - * right. - unshelve eapply valid_state_equivocating_validators_proper, Hprefix; - [ | by exists []; rewrite app_nil_r | by symmetry; apply valid_trace_get_last in Htr as Hlst | ]. + * rewrite <- Hlst'. + right. + apply Hprefix. by exists m. - * left. destruct Heqv as [Heqv _]; rewrite Hmsg in Heqv. - by apply Some_inj in Heqv; congruence. + * left. simpl in Heqv. + by destruct Heqv as [Heq_om Heqv]; congruence. - rewrite app_assoc in Heq_tr''_item. apply app_inj_tail in Heq_tr''_item. destruct Heq_tr''_item as [Heq_tr'' Heq_item]. - unshelve eapply trace_witnessing_equivocation_prop_pi, Hprefix. - by eexists. + by apply (Hprefix _ _ Heq_tr''). Qed. (** @@ -561,122 +472,118 @@ Qed. *) Lemma preloaded_has_strong_trace_witnessing_equivocation_prop s (Hs : valid_state_prop PreFree s) - : exists is' tr' (Htr' : finite_valid_trace_init_to PreFree is' s tr'), - strong_trace_witnessing_equivocation_prop Htr'. + : exists is' tr', + finite_valid_trace_init_to PreFree is' s tr' /\ + strong_trace_witnessing_equivocation_prop is' tr'. Proof. apply is_equivocating_tracewise_witness in Hs. - destruct Hs as (is & tr & Htr & Hwitness). - apply valid_trace_get_last in Htr as Hlst; subst s. + destruct Hs as [is [tr [Htr Hwitness]]]. + apply finite_valid_trace_init_to_last in Htr as Hlst. + subst s. + apply finite_valid_trace_init_to_forget_last in Htr. remember (length tr) as n. - remember - (size (equivocating_validators - (exist _ (finite_trace_last is tr) (valid_trace_last_pstate Htr)))) as m. - revert m n is tr Htr Heqm Heqn Hwitness. + remember (set_size (equivocating_validators (finite_trace_last is tr))) as m. + revert m n is tr Heqm Heqn Htr Hwitness. pose - (Pr m n := - forall is tr (Htr : finite_valid_trace_init_to PreFree is (finite_trace_last is tr) tr), - m = size (equivocating_validators (finite_trace_last is tr ↾ valid_trace_last_pstate Htr)) -> + (fun m n => + forall is tr, + m = set_size (equivocating_validators (finite_trace_last is tr)) -> n = length tr -> - trace_witnessing_equivocation_prop Htr -> - exists (is' : state PreFree) (tr' : list transition_item) - (Htr' : finite_valid_trace_init_to PreFree is' (finite_trace_last is tr) tr'), - strong_trace_witnessing_equivocation_prop Htr'). - apply (Wf_nat.lt_wf_double_ind Pr); subst Pr; cbn. + finite_valid_trace PreFree is tr -> + trace_witnessing_equivocation_prop is tr -> + let s := finite_trace_last is tr in + exists (is' : state PreFree) (tr' : list transition_item), + finite_valid_trace_init_to PreFree is' s tr' /\ + (forall prefix suffix : list transition_item, + prefix ++ suffix = tr' -> + trace_witnessing_equivocation_prop is' prefix)) + as Pr. + apply (Wf_nat.lt_wf_double_ind Pr). intros m n IHm IHn. intros is tr. destruct_list_last tr tr' item Htr_eq. - subst. - intros Htr _ _ _. - exists is, [], Htr. - intros prefix His_prefix. - destruct (Datatypes.id His_prefix) as [suffix Heq_tr]. - symmetry in Heq_tr; apply app_eq_nil in Heq_tr as [-> ->]. - unshelve eapply trace_witnessing_equivocation_prop_pi, initial_state_witnessing_equivocation_prop. - by apply Htr. - - intros Htr'_item ? Hn Hwitness. - apply finite_valid_trace_init_to_snoc in Htr'_item as H_tr'_item. - destruct H_tr'_item as (Htr' & Hitem & Hdestination). - + intros _ _ Htr _. + exists is, []. + split. + + by apply finite_valid_trace_init_add_last. + + intros prefix suffix Heq_tr. + apply app_eq_nil in Heq_tr. destruct Heq_tr. subst. + by apply initial_state_witnessing_equivocation_prop, Htr. + - rewrite finite_trace_last_is_last. + intros ? Hn Htr'_item Hwitness. + apply finite_valid_trace_init_add_last + with (sf := destination item) + in Htr'_item + ; [| by apply finite_trace_last_is_last]. destruct item as [l om s' om']. simpl in *. - destruct (equivocating_validators_witness_last_char _ _ _ _ Htr'_item Hwitness) - as [[Heq Hwitness'] | (msg & Heq_om & v & Hsender & Hnv & Hneq)]. + destruct + (equivocating_validators_witness_last_char _ _ _ _ _ _ Htr'_item Hwitness) + as [[Heq Hwitness'] | [msg [Heq_om [v [Hsender [Hnv Hneq]]]]]]. + specialize (IHn (length tr')). rewrite app_length in Hn. simpl in Hn. spec IHn; [lia |]. - specialize (IHn is tr' Htr'). - spec IHn. - { - subst m; symmetry; apply set_size_proper. - by etransitivity; [| etransitivity; [exact Heq |]]; - apply valid_state_equivocating_validators_proper. - } + specialize (IHn is tr'). + spec IHn; [by subst m; setoid_rewrite Heq |]. specialize (IHn eq_refl). + destruct Htr'_item as [Htr'_item Hinit]. + apply finite_valid_trace_from_to_app_split in Htr'_item. + destruct Htr'_item as [Htr' Hitem]. spec IHn. { - eapply trace_witnessing_equivocation_prop_pi, Hwitness'. + split; [| done]. + by apply finite_valid_trace_from_to_forget_last in Htr'. } - destruct IHn as (is' & tr'' & Htr'' & Hprefix). - pose proof (Htr''_item := finite_valid_trace_init_to_snoc_rev PreFree Htr'' Hitem). - rewrite finite_trace_last_is_last; cbn. - eexists _, _, Htr''_item. - unshelve eapply strong_trace_witnessing_equivocation_prop_pi, - strong_trace_witnessing_equivocation_prop_extend_eq; cycle 6; - [done | by eapply trace_witnessing_equivocation_prop_pi |..]. - * etransitivity; [done |]. - by eapply valid_state_equivocating_validators_proper, - finite_trace_last_is_last. - * done. + specialize (IHn Hwitness'). + destruct IHn as [is' [tr'' [[Htr'' Hinit'] Hprefix]]]. + specialize + (finite_valid_trace_from_to_app PreFree _ _ _ _ _ Htr'' Hitem) + as Htr''_item. + eexists is', _. + split; [done |]. + by apply (strong_trace_witnessing_equivocation_prop_extend_eq _ is tr' (conj Htr' Hinit)) + ; [by split | done..]. + subst. destruct Hneq as [Hneq Hwneq]. - - destruct - (is_equivocating_tracewise_witness (finite_trace_last is tr') - (valid_trace_last_pstate Htr')) - as (is' & tr''& Htr'' & Hwitness'). - specialize (IHm - (size (equivocating_validators - (finite_trace_last is tr' ↾ - valid_trace_last_pstate - (finite_valid_trace_init_to_prefix_1 PreFree Htr'_item)))) - (length tr'')). - spec IHm. - { - replace (size (equivocating_validators (exist _ (finite_trace_last is (tr' ++ _)) _))) - with (size ({[v]} ∪ equivocating_validators - (finite_trace_last is tr' ↾ valid_trace_last_pstate (finite_valid_trace_init_to_prefix_1 PreFree Htr'_item)))). - - rewrite size_union, size_singleton; [by unfold size; lia |]. - by intro v'; rewrite elem_of_singleton; intros ->. - - rewrite <- Hneq. - by apply set_size_proper, valid_state_equivocating_validators_proper. - } - specialize (IHm is' tr'' (valid_trace_add_default_last (valid_trace_forget_last Htr''))). - apply finite_valid_trace_init_to_last in Htr'' as Htr''_lst. - spec IHm. - { - by apply set_size_proper, valid_state_equivocating_validators_proper. + remember (finite_trace_last is tr') as s. + specialize (is_equivocating_tracewise_witness s) as Hwitness'. + spec Hwitness'. + { apply proj1, finite_valid_trace_from_to_app_split, proj1 + , finite_valid_trace_from_to_last_pstate + in Htr'_item. + by subst. } - specialize (IHm eq_refl). + destruct Hwitness' as [is' [tr''[Htr'' Hwitness']]]. + specialize (IHm (set_size (equivocating_validators s)) (length tr'')). spec IHm. { - by eapply trace_witnessing_equivocation_prop_pi, Hwitness'. + rewrite Hneq. + setoid_rewrite size_union; [by rewrite size_singleton; unfold size; lia |]. + by intro v'; rewrite elem_of_singleton; intros ->. } - destruct IHm as (is'' & tr''' & Htr''' & Hprefix). - assert (H_tr''' : finite_valid_trace_init_to PreFree is'' (finite_trace_last is tr') tr'''). - { - by clear -Htr''' Htr''_lst; rewrite <- Htr''_lst. - } - pose proof (Htr'''_item := finite_valid_trace_init_to_snoc_rev _ H_tr''' Hitem). + specialize (IHm is' tr''). + apply finite_valid_trace_init_to_last in Htr'' as Htr''_lst. + simpl in *. + rewrite Htr''_lst in IHm. + specialize (IHm eq_refl eq_refl). + spec IHm; [by apply finite_valid_trace_init_to_forget_last in Htr'' |]. + specialize (IHm Hwitness'). + destruct IHm as [is'' [tr''' [[Htr''' Hinit'] Hprefix]]]. + apply proj1, finite_valid_trace_from_to_app_split, proj2 in Htr'_item as Hitem. + simpl in *. + rewrite <- Heqs in Hitem. + specialize + (finite_valid_trace_from_to_app PreFree _ _ _ _ _ Htr''' Hitem) + as Htr'''_item. eexists is'', _. - rewrite finite_trace_last_is_last. - exists Htr'''_item. - unshelve eapply strong_trace_witnessing_equivocation_prop_pi, - strong_trace_witnessing_equivocation_prop_extend_neq; cycle 5; - [done | done | | done |..]. - * by unshelve eapply Hwneq, strong_trace_witnessing_equivocation_prop_stronger; - [| done | eapply strong_trace_witnessing_equivocation_prop_pi]. - * etransitivity; [| etransitivity; [exact Hneq |]]; - [by symmetry; eapply valid_state_equivocating_validators_proper |]. - apply sets.union_proper; [done |]. - by symmetry; apply valid_state_equivocating_validators_proper. - * by cbn in Htr''_lst |- *; rewrite Htr''_lst. + split; [done |]. + specialize (Hprefix tr''' []) as Hwitness'''. + spec Hwitness'''; [by apply app_nil_r |]. + specialize (Hwneq _ _ (conj Htr''' Hinit') Hwitness'''). + remember {| input := Some msg |} as item. + specialize (strong_trace_witnessing_equivocation_prop_extend_neq + _ _ _ (conj Htr''' Hinit') Hprefix item msg) as Hextend. + spec Hextend; [by subst |]. + specialize (Hextend Hwneq _ Hsender). + by apply Hextend; subst. Qed. (** @@ -687,16 +594,17 @@ Qed. *) Lemma free_has_strong_trace_witnessing_equivocation_prop s (Hs : valid_state_prop Free s) - : exists is' tr' (Htr' : finite_valid_trace_init_to PreFree is' s tr'), + : exists is' tr', finite_valid_trace_init_to Free is' s tr' /\ - strong_trace_witnessing_equivocation_prop Htr'. + strong_trace_witnessing_equivocation_prop is' tr'. Proof. apply (VLSM_incl_valid_state (vlsm_incl_pre_loaded_with_all_messages_vlsm Free)) in Hs as Hpre_s. - apply preloaded_has_strong_trace_witnessing_equivocation_prop in Hpre_s - as (is & tr & Htr & Hwitness). - exists is, tr, Htr; split; [| done]. - by apply (all_pre_traces_to_valid_state_are_valid_free IM). + apply preloaded_has_strong_trace_witnessing_equivocation_prop in Hpre_s. + destruct Hpre_s as [is [tr [Htr Hwitness]]]. + apply (all_pre_traces_to_valid_state_are_valid_free IM) in Htr + ; [| done]. + by exists is, tr. Qed. End sec_witnessed_equivocation_properties. @@ -723,14 +631,13 @@ Context `{forall i, HasBeenSentCapability (IM i)} `{forall i, HasBeenReceivedCapability (IM i)} (threshold : R) + `{finite.Finite validator} `{ReachableThreshold validator Cv threshold} - `{!finite.Finite validator} (A : validator -> index) (sender : message -> option validator) (Free := free_composite_vlsm IM) - (PreFree := pre_loaded_with_all_messages_vlsm Free) - `{!RelDecision (constrained_composite_state_is_equivocating_tracewise IM A sender)} - (Htracewise_BasicEquivocation : BasicEquivocation (valid_state PreFree) validator Cv threshold + `{RelDecision _ _ (is_equivocating_tracewise_no_has_been_sent IM A sender)} + (Htracewise_BasicEquivocation : BasicEquivocation (composite_state IM) validator Cv threshold := equivocation_dec_tracewise IM threshold A sender) `{FinSet message Cm} (message_dependencies : message -> Cm) @@ -750,10 +657,6 @@ Context Existing Instance Htracewise_BasicEquivocation. -Definition equivocating_validators_indices - {s : composite_state IM} (Hs : valid_state_prop PreFree s) : Ci := - fin_sets.set_map A (equivocating_validators (exist _ s Hs)). - (** Given the fact that the set of [equivocating_validators] can be empty, and the definition of the [fixed_equivocation_constraint] requires @@ -762,9 +665,9 @@ Definition equivocating_validators_indices when there are no [equivocating_validators]. *) Definition equivocating_validators_fixed_equivocation_constraint - {s : composite_state IM} (Hs : valid_state_prop PreFree s) + (s : composite_state IM) := - fixed_equivocation_constraint IM (equivocating_validators_indices Hs). + fixed_equivocation_constraint IM (Ci := Ci) (fin_sets.set_map A (equivocating_validators s)). Lemma equivocators_can_emit_free m (Hmsg : valid_message_prop Free m) @@ -775,7 +678,7 @@ Lemma equivocators_can_emit_free m l s (Hv : composite_valid IM l (s, Some m)) : can_emit - (equivocators_composition_for_directly_observed IM (equivocating_validators_indices (proj2_sig sf)) s) + (equivocators_composition_for_directly_observed IM (Ci := Ci) (fin_sets.set_map A (equivocating_validators sf)) s) m. Proof. apply emitted_messages_are_valid_iff in Hmsg @@ -802,7 +705,6 @@ Proof. apply (Hfull _ _ _ _ Hv) in Hdm. by exists i. } - destruct sf; cbn in *. eapply VLSM_embedding_can_emit; [| done]. unshelve eapply (Hproj (dexist (A v) _)). by apply elem_of_elements, elem_of_map_2. @@ -822,74 +724,61 @@ Qed. *) Lemma strong_witness_has_fixed_equivocation is s tr - (Hpre_s : valid_state_prop PreFree s) - (Htr : finite_valid_trace_init_to Free is s tr) - (H_tr := VLSM_incl_finite_valid_trace_init_to - (vlsm_incl_pre_loaded_with_all_messages_vlsm Free) _ _ _ Htr) - (Heqv : strong_trace_witnessing_equivocation_prop (Cv := Cv) IM threshold A sender H_tr) - : finite_valid_trace_init_to (fixed_equivocation_vlsm_composition IM - (equivocating_validators_indices Hpre_s)) is s tr. + (Htr : finite_valid_trace_init_to (free_composite_vlsm IM) is s tr) + (Heqv : strong_trace_witnessing_equivocation_prop (Cv := Cv) IM threshold A sender is tr) + : finite_valid_trace_init_to (fixed_equivocation_vlsm_composition IM (Ci := Ci) + (fin_sets.set_map A (equivocating_validators s))) is s tr. Proof. - revert s Hpre_s Htr H_tr Heqv. - induction tr using rev_ind. - - intros; destruct Htr as [Htr Hinit]; inversion Htr; subst. - split; [| done]. - by eapply (finite_valid_trace_from_to_empty (fixed_equivocation_vlsm_composition IM _)), - initial_state_is_valid. - - intros. - apply finite_valid_trace_init_to_snoc in Htr as Htrx; - destruct Htrx as (Htr' & Hx & Hs). - assert (Hpre_lst : valid_state_prop PreFree (finite_trace_last is tr)). - { - apply (VLSM_incl_valid_state (vlsm_incl_pre_loaded_with_all_messages_vlsm Free)). - by eapply input_valid_transition_origin. - } - specialize (IHtr _ Hpre_lst Htr'). - cbn in IHtr. spec IHtr. - { - unshelve eapply strong_trace_witnessing_equivocation_prop_pi, - strong_trace_witnessing_equivocation_prop_prefix; cycle 4; [done |..]. - by eexists. + split; [| by apply Htr]. + induction Htr using finite_valid_trace_init_to_rev_ind. + - eapply (finite_valid_trace_from_to_empty (fixed_equivocation_vlsm_composition IM + (Ci := Ci) (fin_sets.set_map A (equivocating_validators si)))). + by apply initial_state_is_valid. + - spec IHHtr. + { intros prefix. intros. + apply (Heqv prefix (suffix ++ [{| l := l; input := iom; destination := sf; output := oom |}])). + by subst; apply app_assoc. } - assert (Htr_sf : finite_valid_trace_init_to - (fixed_equivocation_vlsm_composition IM - (equivocating_validators_indices Hpre_s)) - is (finite_trace_last is tr) tr). - { revert IHtr. - apply VLSM_incl_finite_valid_trace_init_to, + apply (VLSM_incl_finite_valid_trace_init_to (vlsm_incl_pre_loaded_with_all_messages_vlsm Free)) + in Htr as Hpre_tr. + assert + (Htr_sf : finite_valid_trace_from_to + (fixed_equivocation_vlsm_composition IM (Ci := Ci) (fin_sets.set_map A (equivocating_validators sf))) si s tr). + { revert IHHtr. + apply VLSM_incl_finite_valid_trace_from_to, fixed_equivocation_vlsm_composition_index_incl. apply elements_subseteq, set_map_subset. - etransitivity; [| etransitivity]; cycle 1. - - apply (equivocating_validators_witness_monotonicity IM threshold (Cv := Cv) A sender _ _ _ _ H_tr). - by apply strong_trace_witnessing_equivocation_prop_stronger. - - by apply set_equiv_subseteq, valid_state_equivocating_validators_proper. - - by apply set_equiv_subseteq, valid_state_equivocating_validators_proper. + remember {| destination := sf |} as item. + replace sf with (destination item) by (subst; done). + eapply equivocating_validators_witness_monotonicity; [done |]. + by apply Heqv with (suffix := []), app_nil_r. } - clear IHtr. - subst s. - eapply (finite_valid_trace_init_to_snoc_rev - (fixed_equivocation_vlsm_composition IM - (equivocating_validators_indices Hpre_s))); [done |]. - destruct Hx as [(Hs & Hiom & Hv) Ht]. - apply strong_trace_witnessing_equivocation_prop_stronger in Heqv as Heqv_tr. - destruct x. - apply valid_trace_last_pstate in Htr_sf as Hlst. - destruct input as [im |]; [| by repeat split; auto using option_valid_message_None]. + clear IHHtr. + apply (extend_right_finite_trace_from_to _ Htr_sf). + destruct Ht as [(Hs & Hiom & Hv) Ht]. + apply finite_valid_trace_from_to_last_pstate in Htr_sf as Hs'. + specialize + (Heqv + (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}]) + []). + spec Heqv; [by apply app_nil_r |]. + destruct iom as [im |]; [| by repeat split; auto using option_valid_message_None]. apply Free_has_sender in Hiom as _Hsender. destruct (sender im) as [v |] eqn: Hsender; [| by congruence]. clear _Hsender. - specialize (Heqv_tr v); cbn in Heqv_tr. - destruct (decide (composite_has_been_directly_observed IM (finite_trace_last is tr) im)). + specialize (Heqv v). + rewrite finite_trace_last_is_last in Heqv. + simpl in Heqv. + assert (Hpre_s : valid_state_prop (pre_loaded_with_all_messages_vlsm Free) s). + { by apply proj1, finite_valid_trace_from_to_last_pstate in Hpre_tr. } + destruct (decide (composite_has_been_directly_observed IM s im)). { repeat split ; [done | apply option_valid_message_Some | done | | done]. - - by apply (composite_directly_observed_valid IM _ (finite_trace_last is tr)). + - by apply (composite_directly_observed_valid IM _ s). - by left. } - assert (Hequivocating_v : v ∈ equivocating_validators (exist _ _ Hpre_s)). - { - eapply valid_state_equivocating_validators_proper; cycle 1; - [apply Heqv_tr | done]. - exists im. split; [done |]. + assert (Hequivocating_v : v ∈ equivocating_validators sf). + { apply Heqv. exists im. split; [done |]. eexists tr, _, []. split; [done |]. split; [done |]. @@ -897,19 +786,19 @@ Proof. elim n. apply composite_has_been_directly_observed_sent_received_iff. left. - eapply (has_been_sent_examine_one_trace (vlsm := Free)) in Him_output; - [exact Him_output |]. - by apply (VLSM_incl_finite_valid_trace_init_to - (vlsm_incl_pre_loaded_with_all_messages_vlsm Free)). + specialize (proper_sent Free _ Hpre_s im) as Hsent_s. + apply proj2 in Hsent_s. apply Hsent_s. clear Hsent_s. + apply (has_been_sent_consistency Free _ Hpre_s im). + by exists si, tr, Hpre_tr. } specialize (equivocators_can_emit_free _ Hiom _ Hsender _ Hequivocating_v _ _ Hv) as Hemit_im. repeat split; [done | | done | by right | done]. apply emitted_messages_are_valid. specialize - (EquivPreloadedBase_Fixed_weak_embedding IM (Ci := Ci) _ _ (valid_trace_last_pstate Htr_sf)) as Hproj. + (EquivPreloadedBase_Fixed_weak_embedding IM _ _ Hs') as Hproj. spec Hproj; [by intros; apply no_initial_messages_in_IM |]. apply (VLSM_weak_embedding_can_emit Hproj). - by apply (VLSM_incl_can_emit (Equivocators_Fixed_Strong_incl IM _ _ (valid_trace_last_pstate Htr_sf))). + by apply (VLSM_incl_can_emit (Equivocators_Fixed_Strong_incl IM _ _ Hs')). Qed. (** @@ -919,19 +808,19 @@ Qed. *) Lemma equivocating_validators_fixed_equivocation_characterization (Hke : WitnessedEquivocationCapability IM threshold A sender (Cv := Cv)) - : forall s (Hpre_s : valid_state_prop PreFree s), + : forall s, valid_state_prop Free s -> valid_state_prop - (composite_vlsm IM (equivocating_validators_fixed_equivocation_constraint Hpre_s)) s. + (composite_vlsm IM (equivocating_validators_fixed_equivocation_constraint s)) s. Proof. - intros s Hpre_s Hs. + intros s Hs. destruct (free_has_strong_trace_witnessing_equivocation_prop IM threshold A sender _ s Hs) - as (is & tr & Hpre_tr & Htr & Heqv). - unshelve eapply finite_valid_trace_from_to_last_pstate, - strong_witness_has_fixed_equivocation; [| | done |]. - by eapply strong_trace_witnessing_equivocation_prop_pi. + as [is [tr [Htr Heqv]]]. + cut (finite_valid_trace_from_to (composite_vlsm IM + (equivocating_validators_fixed_equivocation_constraint s)) is s tr). + { by intro Htr'; apply finite_valid_trace_from_to_last_pstate in Htr'. } + by apply strong_witness_has_fixed_equivocation. Qed. End sec_witnessed_equivocation_fixed_set. -