-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathELMO.v
3097 lines (2904 loc) · 130 KB
/
ELMO.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
From VLSM.Lib Require Import Itauto.
From Coq Require Import FunctionalExtensionality Reals.
From stdpp Require Import prelude finite.
From VLSM.Lib Require Import Preamble Measurable FinSetExtras RealsExtras ListExtras.
From VLSM.Core Require Import VLSM VLSMProjections Composition Equivocation.
From VLSM.Core Require Import ReachableThreshold Validator ProjectionTraces MessageDependencies.
From VLSM.Core Require Import TraceableVLSM MinimalEquivocationTrace.
From VLSM.Core Require Import AnnotatedVLSM MsgDepLimitedEquivocation.
From VLSM.Examples Require Import BaseELMO UMO MO.
Create HintDb ELMO_hints.
#[local] Hint Resolve submseteq_tail_l : ELMO_hints.
(** * ELMO: Protocol Definitions and Properties for ELMO
This module contains definitions and properties of ELMO components and
the ELMO protocol.
*)
Section sec_ELMO.
Context
{Address : Type}
`{EqDecision Address}
`{Measurable Address}
(State := @State Address)
(Observation := @Observation Address)
(Message := @Message Address)
(threshold : R)
`{finite.Finite index}
(idx : index -> Address)
`{!Inj (=) (=) idx}
`{!ReachableThreshold (Message_validator idx) (listset (Message_validator idx)) threshold}.
#[export] Instance ReachableThreshold_Address :
ReachableThreshold Address (listset Address) threshold.
Proof.
destruct ReachableThreshold0 as (Hgt0 & vs & Hvs).
split; [done |].
exists (set_map proj1_sig vs).
replace (sum_weights _) with (sum_weights vs); [done |].
clear Hvs; revert vs; apply set_ind.
- intros vs1 vs2 Heqv Hvs1.
replace (sum_weights vs2) with (sum_weights vs1)
by (apply sum_weights_proper; done).
by rewrite Hvs1; apply sum_weights_proper; rewrite Heqv.
- by rewrite !sum_weights_empty.
- intros v vs Hv Hvs.
rewrite sum_weights_disj_union, Hvs by set_solver.
replace (sum_weights (set_map _ ({[v]} ∪ _)))
with (sum_weights (set_map (C := listset (Message_validator idx))
(D := listset Address) proj1_sig {[v]} ∪ set_map (D := listset Address) proj1_sig vs))
by (apply sum_weights_proper; rewrite set_map_union; done).
rewrite sum_weights_disj_union; cycle 1.
+ rewrite set_map_singleton.
cut (`v ∉ set_map (D := listset Address) proj1_sig vs); [by set_solver |].
contradict Hv.
apply elem_of_map in Hv as (v' & Hv' & Hv).
by apply dsig_eq in Hv' as ->.
+ replace (sum_weights (set_map _ {[v]}))
with (sum_weights (Cv := listset Address) {[` v]}).
* by rewrite !sum_weights_singleton.
* by apply sum_weights_proper; rewrite set_map_singleton.
Qed.
Definition immediate_dependency (m1 m2 : Message) : Prop :=
m1 ∈ messages (state m2).
Lemma immediate_dependency_msg_dep_rel :
forall dm m : Message,
immediate_dependency dm m <-> msg_dep_rel Message_dependencies dm m.
Proof.
unfold immediate_dependency, messages, messages',
msg_dep_rel, Message_dependencies; cbn.
by setoid_rewrite elem_of_list_to_set.
Qed.
#[local] Notation happensBefore := (tc immediate_dependency).
#[local] Infix "<hb" := happensBefore (at level 70).
Lemma happensBefore_msg_dep :
forall dm m : Message,
dm <hb m <-> msg_dep_happens_before Message_dependencies dm m.
Proof.
by split;
(induction 1; [by constructor 1; apply immediate_dependency_msg_dep_rel |]);
(etransitivity; [| done]);
constructor 1; apply immediate_dependency_msg_dep_rel.
Qed.
(**
The full node condition says that a node can receive a message
only if the direct observations of that node already include
all messages from the direct observations of the state inside
the message (not necessarily with the same [Send]/[Receive] label).
This will let us define validity predicates without needing
to recurse into the states inside observations in a state,
because a correctly-operating node would have checked the
shallow condition for those messages when their observations
were added to the state.
*)
Definition full_node (s : State) (m : Message) : Prop :=
messages (state m) ⊆+ messages s.
Lemma full_node_reachable_messages_ind
(P : State -> Message -> Prop)
(Hnew : forall s l msg
(Hfull : full_node s msg)
(IH : forall m, m ∈ messages s -> P s m),
P (s <+> MkObservation l msg) msg)
(Hprev : forall s ob m (IH : P s m), P (s <+> ob) m)
:
forall s, UMO_reachable full_node s ->
forall m, m ∈ messages s -> P s m.
Proof.
unfold full_node in Hnew.
by apply UMO_reachable_elem_of_messages_ind; auto.
Qed.
Lemma messages_hb_transitive :
forall s,
UMO_reachable full_node s ->
forall m,
m ∈ messages s ->
forall m',
m' <hb m ->
m' ∈ messages s.
Proof.
refine (UMO_reachable_elem_of_messages_ind _ _ _ _ _);
[intros | intros s Hs IH m' Hm'%tc_r_iff
| intros s Hs mr Hmr%submseteq_list_subseteq IH m' Hm'%tc_r_iff];
apply elem_of_messages_addObservation; right.
- by itauto.
- by destruct Hm' as [| (m & ? & ?)]; [| eapply IH].
- destruct Hm' as [| (m & ? & ?)]; [by apply Hmr |].
by eapply IH; [apply Hmr |].
Qed.
(**
Some claims about the full node condition hold for any UMO-based VLSM
whose validity predicate implies the full node condition. By UMO-based we
mean a [VLSM] built over the [ELMO_component_type] which also has the same
transition function as UMO/MO, an initial state predicate that ensures
[obs] of an initial state is empty, and a validity predicate that
implies [UMO_component_valid].
If that's all we know about the VLSM, knowing that a [State] is reachable
in that VLSM is only as informative as knowing that the state is
[UMO_reachable full_node].
(This lemma needs no assumption about [UMO_component_valid] because
reachability is the same anyway, because [UMO_component_valid]
returns the state unchanged on invalid input.)
*)
Lemma full_node_VLSM_reachable
(VM : VLSMMachine ELMO_component_type)
(V := mk_vlsm VM)
(VM_transition_is_UMO :
forall (l : Label) (s : State) (om : option Message),
transition V l (s, om) = UMO_component_transition l s om)
(VM_init_empty :
forall s : State, initial_state_prop V s -> obs s = [])
(VM_enforces_full_node :
forall (l : Label) (s : State) (m : Message),
valid V l (s, Some m) -> full_node s m) :
forall (s : State),
constrained_state_prop V s ->
UMO_reachable full_node s.
Proof.
intro s.
induction 1 using valid_state_prop_ind.
- destruct s as [obs adr].
apply VM_init_empty in Hs; cbn in Hs; subst.
by apply reach_init.
- destruct Ht as [(_ & _ & Hvalid) Ht]; cbn in Ht, Hvalid.
rewrite VM_transition_is_UMO in Ht.
destruct l, om; injection Ht as [= <- <-]; [| done.. |].
+ apply VM_enforces_full_node in Hvalid.
by apply reach_recv.
+ by apply reach_send.
Qed.
(**
A simplified version of [local_equivocators] that only checks for
incompatible messages among the immediate observations of the state.
This relies on the full node condition.
*)
Set Warnings "-cannot-define-projection".
Record local_equivocators_simple (s : State) (i : Address) : Prop :=
{
les_m1 : Message;
les_m2 : Message;
les_adr1 : adr (state les_m1) = i;
les_adr2 : adr (state les_m2) = i;
les_obs_m1 : les_m1 ∈ messages s;
les_obs_m2 : les_m2 ∈ messages s;
les_incomparable : incomparable les_m1 les_m2;
}.
Set Warnings "cannot-define-projection".
(**
A variant of [local equivocators] that relies more on the full node condition
and directly shows how the set of equivocators can grow.
Only a newly received message needs to be checked against previous messages,
other addresses are equivocating if they are equivocating in the previous
state.
*)
Inductive local_equivocators_full_obs : list Observation -> Address -> Prop :=
| lefo_last :
forall (ol : list Observation) (m1 m2 : Message),
m2 ∈ receivedMessages' ol ->
incomparable m1 m2 ->
local_equivocators_full_obs (addObservation' (MkObservation Receive m1) ol) (adr (state m1))
| lefo_prev :
forall (ol : list Observation) (l : Label) (m : Message) (i : Address),
local_equivocators_full_obs ol i ->
local_equivocators_full_obs (addObservation' (MkObservation l m) ol) i.
Lemma lefo_alt (ol : list Observation) (o : Observation) (a : Address) :
local_equivocators_full_obs (addObservation' o ol) a <->
(a = adr (state (message o))
/\ label o = Receive
/\ exists m2, m2 ∈ receivedMessages' ol
/\ incomparable (message o) m2)
\/ local_equivocators_full_obs ol a.
Proof.
split.
- by inversion 1; subst; [left; split_and!; [.. | eexists] | right].
- destruct o as [l m1]; cbn.
by intros [(-> & -> & m2 & Hrecv & Hadr & Hincomp) |]; econstructor.
Qed.
#[export] Instance local_equivocators_full_obs_dec : RelDecision local_equivocators_full_obs.
Proof.
intros ol a.
induction ol using addObservation'_rec.
- by right; inversion 1.
- apply (Decision_iff (iff_Symmetric _ _ (lefo_alt _ _ _))).
by pose proof @list_exist_dec; typeclasses eauto.
Defined.
Definition local_equivocators_full (s : State) : Address -> Prop :=
local_equivocators_full_obs (obs s).
#[export] Instance local_equivocators_full_dec : RelDecision local_equivocators_full :=
fun s a => local_equivocators_full_obs_dec (obs s) a.
(**
An ELMO component has the same elements as a MO component
except for the validity predicate, which:
- checks message validity
- enforces the full-node condition
- only allows receiving a message if it will not bring the total [weight]
of the locally-visible equivocation above [equivocation_threshold]
*)
Definition no_self_equiv (s : State) (m : Message) : Prop :=
adr s = adr (state m) -> m ∈ sentMessages s.
Inductive MessageHasSender (m : Message) : Prop :=
| message_has_sender : forall i, adr (state m) = idx i -> MessageHasSender m.
Inductive ELMO_msg_valid_full : Message -> Prop :=
| MVF_nil :
forall m : Message,
obs (state m) = [] -> MessageHasSender m -> ELMO_msg_valid_full m
| MVF_send :
forall m,
ELMO_msg_valid_full m ->
ELMO_msg_valid_full (m <*> MkObservation Send m)
| MVF_recv :
forall m mo,
full_node (state m) mo ->
no_self_equiv (state m) mo ->
ELMO_msg_valid_full m ->
ELMO_msg_valid_full (m <*> MkObservation Receive mo).
Lemma ELMO_msg_valid_full_to_reach (m : Message) :
ELMO_msg_valid_full m ->
UMO_reachable (fun s m => full_node s m /\ no_self_equiv s m) (state m).
Proof.
by induction 1; destruct m as [ms]; cbn in *;
[replace ms with (MkState [] (adr ms)) by (apply eq_State; done) | ..];
constructor.
Qed.
Lemma ELMO_msg_valid_full_has_sender (m : Message) :
ELMO_msg_valid_full m -> MessageHasSender m.
Proof.
by induction 1; [done | ..]; destruct IHELMO_msg_valid_full; econstructor.
Qed.
#[local] Instance ELMO_local_equivocation : BasicEquivocation State Address (listset Address) threshold :=
{
is_equivocating := local_equivocators_full;
is_equivocating_dec := local_equivocators_full_dec;
state_validators := const (list_to_set (map idx (enum index)));
}.
Definition local_equivocation_limit_ok (s : State) : Prop := not_heavy s.
Record ELMO_recv_valid (s : State) (m : Message) : Prop :=
{
ELMO_mv_full_node : full_node s m;
ELMO_mv_no_self_equiv : no_self_equiv s m;
ELMO_mv_msg_valid_full : ELMO_msg_valid_full m;
ELMO_mv_local_equivocation_limit_ok :
local_equivocation_limit_ok (s <+> MkObservation Receive m);
}.
Inductive ELMO_component_valid : Label -> State -> option Message -> Prop :=
| ELMOCV_Receive :
forall (s : State) (m : Message),
ELMO_recv_valid s m ->
ELMO_component_valid Receive s (Some m)
| ELMOCV_Send :
forall s : State,
ELMO_component_valid Send s None.
(**
This definition is closer to the way the validity condition
might be defined by hand, but is probably less convenient than
the inductive definition of [ELMO_component_valid]. So we prove
that they are equivalent.
*)
Definition ELMO_component_valid_alt (l : Label) (s : State) (om : option Message) : Prop :=
UMO_component_valid l s om /\ (l = Receive -> from_option (ELMO_recv_valid s) False om).
Definition ELMO_component_valid_alt_iff :
forall (l : Label) (s : State) (om : option Message),
ELMO_component_valid l s om <-> ELMO_component_valid_alt l s om.
Proof.
split.
- by destruct 1; split; [constructor | auto | constructor | auto].
- by intros [[] Hfo]; constructor; apply Hfo.
Qed.
Definition ELMO_component_machine (i : index) : VLSMMachine ELMO_component_type :=
{|
initial_state_prop := UMO_component_initial_state_prop (idx i);
initial_message_prop := const False;
s0 := Inhabited_UMO_component_initial_state_type (idx i);
transition := fun l '(st, om) => UMO_component_transition l st om;
valid := fun l '(st, om) => ELMO_component_valid l st om;
|}.
Definition ELMO_component (i : index) : VLSM Message :=
{|
vlsm_type := ELMO_component_type;
vlsm_machine := ELMO_component_machine i;
|}.
#[export] Instance ComputableSentMessages_ELMO_component
(i : index) : ComputableSentMessages (ELMO_component i).
Proof.
constructor 1 with sentMessages; constructor.
- by intros [] []; cbn in *; subst; cbn; apply not_elem_of_nil.
- intros l s im s' om [(Hvsp & Hovmp & Hv) Ht] m; cbn in *.
destruct l, im; cbn in *; [| by exfalso; inversion Hv.. |];
inversion_clear Ht; destruct s; cbn.
+ by rewrite decide_False; cbn; firstorder congruence.
+ rewrite decide_True by done; cbn.
unfold Message; rewrite elem_of_cons.
by firstorder congruence.
Defined.
#[export] Instance ComputableReceivedMessages_ELMO_component
(i : index) : ComputableReceivedMessages (ELMO_component i).
Proof.
constructor 1 with receivedMessages; constructor.
- by intros [] []; cbn in *; subst; cbn; apply not_elem_of_nil.
- intros l s im s' om [(Hvsp & Hovmp & Hv) Ht] m; cbn in *.
destruct l, im; cbn in *; [| by exfalso; inversion Hv.. |];
inversion_clear Ht; destruct s; cbn.
+ rewrite decide_True by done; cbn.
unfold Message; rewrite elem_of_cons.
by firstorder congruence.
+ by rewrite decide_False; cbn; firstorder congruence.
Defined.
#[export] Instance HasBeenDirectlyObservedCapability_ELMO_component
(i : index) : HasBeenDirectlyObservedCapability (ELMO_component i) :=
HasBeenDirectlyObservedCapability_from_sent_received (ELMO_component i).
Lemma ELMO_reachable_view (s : State) i :
constrained_state_prop (ELMO_component i) s
<->
UMO_reachable ELMO_recv_valid s /\ adr s = idx i.
Proof.
eapply iff_trans.
- apply UMO_based_valid_reachable; [| | done].
+ by inversion 1.
+ by cbn; split; inversion 1; [| constructor].
- apply Morphisms_Prop.and_iff_morphism.
+ by split; apply UMO_reachable_impl; inversion 1; subst; [| constructor].
+ by cbn; firstorder.
Qed.
Lemma ELMO_component_message_dependencies_full_node_condition :
forall i : index,
message_dependencies_full_node_condition_prop
(ELMO_component i) Message_dependencies.
Proof.
intros i [] s m Hv; inversion Hv as [? ? [Hfull] |]; subst.
intros dm Hdm; cbn in Hdm.
apply elem_of_list_to_set in Hdm.
eapply elem_of_submseteq, elem_of_messages in Hdm; [| done].
by destruct Hdm as []; [left | right].
Qed.
Lemma ELMO_full_node_reachable i s :
constrained_state_prop (ELMO_component i) s -> UMO_reachable full_node s.
Proof.
intro Hs; apply ELMO_reachable_view in Hs as [? _].
eapply UMO_reachable_impl; [| done].
by inversion 1.
Qed.
Lemma ELMO_no_self_equiv_reachable i s :
constrained_state_prop (ELMO_component i) s -> UMO_reachable no_self_equiv s.
Proof.
intro Hs; apply ELMO_reachable_view in Hs as [? _].
eapply UMO_reachable_impl; [| done].
by inversion 1.
Qed.
Section sec_ELMO_component_lemmas.
(** ** Component lemmas *)
Context
(i : index)
(Ei : VLSM Message := ELMO_component i)
.
Lemma ELMO_reachable_adr (s : State) :
constrained_state_prop Ei s -> adr s = idx i.
Proof.
by intros [_ Hadr]%ELMO_reachable_view.
Qed.
Lemma ELMO_constrained_transition_output_not_initial :
forall l (s : State) (om : option Message) (s' : State) (om' : option Message),
input_constrained_transition Ei l (s, om) (s', om') ->
~ initial_state_prop Ei s'.
Proof.
intros l s om [ol a] om' [(_ & _ & Hv) Ht]; compute; intros [-> _].
by inversion Hv; subst; inversion Ht.
Qed.
Lemma ELMO_input_constrained_transition_inj :
forall l (s : State) (om : option Message) (s' : State) (om' : option Message),
input_constrained_transition Ei l (s, om) (s', om') ->
forall l0 s0 om0 om'0,
input_constrained_transition Ei l0 (s0, om0) (s', om'0) ->
l0 = l /\ s0 = s /\ om0 = om /\ om'0 = om'.
Proof.
intros l s om s' om' [(_ & _ & Hvalid) Ht] l0 s0 om0 om'0 [(_ & _ & Hvalid0) Ht0].
inversion Hvalid; subst; cbn in Ht; injection Ht as [= <- <-];
inversion Hvalid0; subst; inversion Ht0; [| done].
by replace s0 with s by (apply eq_State; done).
Qed.
Lemma ELMO_component_valid_transition_size :
forall (s1 s2 : State) (iom oom : option Message) (lbl : Label),
ELMO_component_valid lbl s1 iom ->
UMO_component_transition lbl s1 iom = (s2, oom) ->
sizeState s1 < sizeState s2.
Proof. by intros [] s2 [im |] oom []; do 2 inversion_clear 1; cbn; lia. Qed.
#[export] Instance ELMOTransitionMonotoneVLSM : TransitionMonotoneVLSM Ei sizeState.
Proof.
constructor; intros s1 s2 [? ? ? [Hv Ht]].
by eapply ELMO_component_valid_transition_size; cbn in *.
Qed.
Lemma state_suffix_addObservation_inv :
forall (s1 s2 : State) (ob : Observation),
state_suffix s1 (s2 <+> ob) ->
s1 = s2 \/ state_suffix s1 s2.
Proof.
intros s1 s2 ob (Hadr & [[| _o os] Hsuf] & Hstrict);
[by contradict Hstrict; exists [] |].
destruct s2; cbn in *.
inversion Hsuf; subst _o obs.
destruct os; [left; apply eq_State; cbn in *; congruence |].
right; constructor; [done |].
split; [by eexists | destruct s1; cbn; clear].
intros [os' Heqos].
apply f_equal with (f := length) in Heqos.
rewrite app_length in Heqos; cbn in Heqos; rewrite app_length in Heqos.
by lia.
Qed.
(** There is a unique trace from any prefix of a reachable state to that state. *)
Lemma ELMO_unique_trace_segments (s sf : State) :
constrained_state_prop Ei sf -> (s = sf \/ state_suffix s sf) ->
exists! (tr : list transition_item),
finite_constrained_trace_from_to Ei s sf tr.
Proof.
intros Hsf [-> | Hsuf];
[by exists []; split; [by constructor |]; intros;
symmetry; eapply transition_monotone_empty_trace; [typeclasses eauto |]
|].
induction Hsf using valid_state_prop_ind.
- unfold initial_state_prop in Hs; cbn in Hs.
eapply UMO_component_initial_state_spec in Hs as ->.
by contradict Hsuf; apply state_suffix_empty_minimal.
- assert (s = s0 \/ state_suffix s s0) as [-> | Hss0].
{
assert (exists o, s' = s0 <+> o) as [o ->]
by (destruct Ht as [(_ & _ & Hv) Ht]; inversion Hv; subst;
inversion Ht; eexists; done).
by apply state_suffix_addObservation_inv in Hsuf.
}
+ exists [Build_transition_item l om s' om'].
split; [by apply finite_valid_trace_from_to_singleton |].
intros tr' Htr'.
induction Htr' using finite_valid_trace_from_to_rev_ind;
[by contradict Hsuf; apply Irreflexive_state_suffix | clear IHHtr'].
destruct (ELMO_input_constrained_transition_inj _ _ _ _ _ Ht _ _ _ _ Ht0)
as (-> & -> & -> & ->).
eapply transition_monotone_empty_trace in Htr'; [| typeclasses eauto].
by subst.
+ destruct (IHHsf Hss0) as (tr & Htr & Htr_unique).
exists (tr ++ [Build_transition_item l om s' om']).
split; [by apply extend_right_finite_trace_from_to with (s2 := s0) |].
intros tr' Htr'.
induction Htr' using finite_valid_trace_from_to_rev_ind;
[by contradict Hsuf; apply Irreflexive_state_suffix | clear IHHtr'].
destruct (ELMO_input_constrained_transition_inj _ _ _ _ _ Ht _ _ _ _ Ht0)
as (-> & -> & -> & ->).
by f_equal; apply Htr_unique.
Qed.
(**
From every reachable state of an [ELMO_component] we can extract a unique
trace reaching that state from the initial state.
*)
Lemma ELMO_unique_traces (sf : State) :
constrained_state_prop Ei sf ->
exists! tr : list transition_item, exists si : State,
finite_constrained_trace_init_to Ei si sf tr.
Proof.
intros Hsf.
pose (si := MkState [] (idx i)).
cut (exists! (tr : list transition_item), finite_constrained_trace_from_to Ei si sf tr).
{
intros (tr & Htr & Htr_unique).
exists tr; split; [by exists si; split |].
by intros _tr [[] [H_tr []]]; cbn in *; subst; apply Htr_unique.
}
apply ELMO_unique_trace_segments; [done |].
destruct (decide (si = sf)) as [| Hneq]; [by left | right].
subst si; constructor; cbn; [by rewrite ELMO_reachable_adr |].
split; [by eexists; rewrite app_nil_r |].
intros [os Hos].
symmetry in Hos; apply app_nil in Hos as [_ Hosf].
by contradict Hneq; apply eq_State; [| symmetry; apply ELMO_reachable_adr].
Qed.
Lemma full_node_rebase_rec_obs :
forall (s s' : State) (m : Message),
UMO_reachable full_node s ->
full_node s (MkMessage s') ->
forall l, rec_obs s' (MkObservation l m) ->
exists l, rec_obs s (MkObservation l m).
Proof.
intros s s' m Hs Hfull l Hm.
remember (MkObservation l m) as ob eqn: Heq_ob.
revert l m Heq_ob; induction Hm; intros l0 m0 ->.
- assert (Hm : m0 ∈ messages s) by (revert Hfull; apply elem_of_submseteq; constructor).
by apply elem_of_list_fmap in Hm as [[l' m'] [-> Hm]]; exists l'; apply obs_rec_obs.
- eapply IHHm; [| done].
by revert Hfull; apply submseteq_tail_l.
- assert (m ∈ messages s) by (revert Hfull; apply elem_of_submseteq; constructor).
by exists l0; apply (unfold_robs _ _ Hs); right; exists m.
Qed.
Lemma full_node_messages_iff_rec_obs :
forall (s : State), UMO_reachable full_node s ->
forall (m : Message),
m ∈ messages s <-> (exists l, rec_obs s (MkObservation l m)).
Proof.
intros s Hs; induction Hs using UMO_reachable_ind'.
- by split; [intros Hm | intros [? Hm]]; inversion Hm.
- intros m.
setoid_rewrite elem_of_messages_addObservation; rewrite (IHHs m);
setoid_rewrite rec_obs_addObservation_iff; cbn.
split.
+ by intros [<- | [l0]]; eauto.
+ by intros [l0 [| [[= _] | [->]]]]; eauto using full_node_rebase_rec_obs.
Qed.
(**
Because of the [no_self_equiv] assumption,
a component might have received its own messages,
but only messages it also sent.
*)
Lemma self_messages_sent (s : State) :
UMO_reachable no_self_equiv s ->
forall m, adr (state m) = adr s -> m ∈ messages s -> m ∈ sentMessages s.
Proof.
intros Hs m Hadr Hm; revert s Hs m Hm Hadr.
by apply (UMO_reachable_elem_of_messages_ind no_self_equiv
(fun s m => adr (state m) = adr s -> m ∈ sentMessages s));
intros; apply elem_of_sentMessages_addObservation; constructor; auto.
Qed.
Lemma local_equivocators_simple_addObservation :
forall (s : State) (ob : Observation) (a : Address),
local_equivocators_simple (s <+> ob) a ->
local_equivocators_simple s a
\/
adr (state (message ob)) = a /\
message ob ∉ messages s /\
exists m, m ∈ messages s /\ incomparable (message ob) m.
Proof.
intros s ob a [].
apply elem_of_messages_addObservation in les_obs_m1 as [-> | Hm1], les_obs_m2 as [-> | Hm2].
- by destruct les_incomparable as [? []]; constructor.
- destruct (decide (message ob ∈ messages s)).
+ by left; exists (message ob) les_m2.
+ by firstorder.
- symmetry in les_incomparable.
destruct (decide (message ob ∈ messages s)).
+ by left; exists les_m1 (message ob).
+ by firstorder.
- by left; eauto using local_equivocators_simple.
Qed.
Lemma local_equivocators_simple_add_Send (s : State) :
UMO_reachable no_self_equiv s ->
forall a, local_equivocators_simple (s <+> MkObservation Send (MkMessage s)) a ->
local_equivocators_simple s a.
Proof.
intros Hs a Ha.
apply local_equivocators_simple_addObservation
in Ha as [| (<- & _ & m & Hm & Hincomp)]; [done |]; cbn in *.
destruct Hincomp as [Hadr []].
by apply self_messages_sent in Hm; [constructor | ..].
Qed.
(**
This lemma is convenient to prove for [local_equivocators_simple],
and our assumption is slightly weaker than [constrained_state_prop Ei].
*)
Lemma local_equivocators_simple_no_self (s : State) :
UMO_reachable no_self_equiv s ->
~ local_equivocators_simple s (adr s).
Proof.
intros Hs; induction Hs as [| | ? ? Hno_self_eqv].
- by destruct 1; inversion les_obs_m1.
- by contradict IHHs; apply local_equivocators_simple_add_Send in IHHs.
- contradict IHHs.
unfold no_self_equiv in Hno_self_eqv.
cbn in IHHs; destruct IHHs.
assert (adr (state msg) = adr s -> msg ∈ messages s).
{
intro Hmsg; symmetry in Hmsg.
apply Hno_self_eqv, elem_of_list_fmap in Hmsg as (ob & Hmsg & Hob).
apply elem_of_list_fmap.
exists ob.
by apply list_filter_subseteq in Hob.
}
assert (les_m1 ∈ messages s)
by (apply elem_of_messages_addObservation in les_obs_m1 as [-> | l]; auto).
assert (les_m2 ∈ messages s)
by (apply elem_of_messages_addObservation in les_obs_m2 as [-> | l]; auto).
by exists les_m1 les_m2.
Qed.
Lemma local_equivocators_full_nondecreasing (s : State) l om s' om' :
transition Ei l (s, om) = (s', om') ->
(forall a, local_equivocators_full s a ->
local_equivocators_full s' a).
Proof.
by destruct l, om; cbn; injection 1; intros; subst; try constructor.
Qed.
Lemma local_equivocators_full_increase_only_received_adr (s : State) m s' om' :
transition Ei Receive (s, Some m) = (s', om') ->
forall a, local_equivocators_full s' a ->
local_equivocators_full s a \/ a = adr (state m).
Proof.
by inversion 1; subst; inversion 1; subst; [right | left].
Qed.
Lemma local_equivocators_simple_add_Receive (s : State) (msg : Message) :
UMO_reachable no_self_equiv s -> no_self_equiv s msg ->
forall i, local_equivocators_simple (s <+> MkObservation Receive msg) i ->
local_equivocators_simple s i
\/ adr (state msg) = i /\ i <> adr s /\
exists m, m ∈ messages s /\ incomparable msg m.
Proof.
intros Hs Hno_equiv a Ha.
assert (a <> adr (s <+> MkObservation Receive msg))
by (contradict Ha; subst; apply local_equivocators_simple_no_self; constructor; done).
apply local_equivocators_simple_addObservation in Ha; cbn in *.
by itauto.
Qed.
(**
Any message in <<messages s>> which does not have the same address as <<s>>
must be found in [receivedMessages].
*)
Lemma not_adr_received (s : State) :
UMO_reachable no_self_equiv s ->
forall msg,
adr (state msg) <> adr s ->
msg ∈ messages s -> msg ∈ receivedMessages s.
Proof.
intros Hs msg Hadr Hmsg; revert s Hs msg Hmsg Hadr.
by apply (UMO_reachable_elem_of_messages_ind _
(fun s m => adr (state m) <> adr s -> m ∈ receivedMessages s));
simpl; intros; apply elem_of_receivedMessages_addObservation; constructor; auto.
Qed.
(**
Little lemmas used while proving equivalence between
[local_equivocators], [local_equivocators_simple],
and [local_equivocators_full].
*)
Lemma received_in_messages (s : State) :
forall msg, msg ∈ receivedMessages s -> msg ∈ messages s.
Proof.
intros msg Hmsg.
apply elem_of_list_fmap in Hmsg as (ob & Hmsg & Hob).
apply elem_of_list_fmap.
exists ob; split; [done |].
by eapply list_filter_subseteq.
Qed.
Lemma local_equivocators_simple_prev (s : State) (ob : Observation) (a : Address) :
local_equivocators_simple s a ->
local_equivocators_simple (s <+> ob) a.
Proof.
by destruct 1; exists les_m1 les_m2; try (apply elem_of_messages_addObservation; right).
Qed.
Lemma reachable_msg_obs :
forall P (s : State),
UMO_reachable P s ->
forall (m : Message) (ob : Observation),
rec_obs (state m) ob ->
m ∈ messages s ->
rec_obs s ob.
Proof.
intros P s Hs m ob Hob Hm;
revert s Hs m Hm ob Hob.
by refine (UMO_reachable_elem_of_messages_ind _ _ _ _ _); auto using @rec_obs.
Qed.
Lemma reachable_obs_msg (s : State) :
UMO_reachable full_node s ->
forall ob, rec_obs s ob -> message ob ∈ messages s.
Proof.
intros Hs ob; induction Hs as [| | ? ? Hfull]; intros Hob.
- by inversion Hob.
- by inversion Hob using rec_obs_send_inv; intros; apply elem_of_messages_addObservation; auto.
- apply elem_of_messages_addObservation; cbn.
inversion Hob using rec_obs_recv_inv; [by auto.. |].
pose proof (fun m H => elem_of_submseteq _ _ m H Hfull) as Hmsg.
intros [Hm | (m & Hm & Hob')]%unfold_rec_obs.
+ by right; apply Hmsg, elem_of_list_fmap_1.
+ apply (elem_of_list_fmap_1 message) in Hm.
by right; apply IHHs, (unfold_robs full_node); eauto.
Qed.
Lemma local_equivocators_simple_iff_full (s : State) :
UMO_reachable no_self_equiv s ->
forall a, local_equivocators_simple s a <-> local_equivocators_full s a.
Proof.
intros Hs a; split.
- induction Hs.
+ by destruct 1; inversion les_obs_m1.
+ intros Ha.
apply lefo_prev, IHHs.
revert Ha; apply local_equivocators_simple_add_Send.
by eapply UMO_reachable_impl.
+ intros Ha.
apply local_equivocators_simple_add_Receive in Ha; [| done..].
destruct Ha as [| (<- & Hnot_s & m & Hm & Hincomp)]; [by apply lefo_prev, IHHs |].
assert (adr (state m) <> adr s) by (destruct Hincomp; congruence).
by revert Hincomp; apply lefo_last, not_adr_received.
- destruct s as [s_obs s_a].
unfold local_equivocators_full; cbn.
intro Hlefo; induction Hlefo as [? ? ? ? Hm12 |].
+ exists m1 m2; [done | .. | done].
* by symmetry; apply Hm12.
* by apply elem_of_cons; left.
* apply elem_of_cons; right; change (m2 ∈ messages (MkState ol s_a)).
by apply received_in_messages.
+ change (MkState _ _) with (MkState ol s_a <+> MkObservation l m) in Hs |- *.
apply local_equivocators_simple_prev, IHHlefo.
by inversion Hs; destruct s.
Qed.
Lemma local_equivocators_iff_simple (s : State) :
UMO_reachable full_node s ->
forall a, local_equivocators s a <-> local_equivocators_simple s a.
Proof.
intro Hs; split; destruct 1.
- by exists (message lceqv_ob1) (message lceqv_ob2); auto using reachable_obs_msg.
- apply (full_node_messages_iff_rec_obs s Hs) in les_obs_m1 as [l1 Hm1], les_obs_m2 as [l2 Hm2].
by exists (MkObservation l1 les_m1) (MkObservation l2 les_m2); auto using reachable_obs_msg.
Qed.
Lemma local_equivocators_iff_full (s : State) :
UMO_reachable (fun s m => full_node s m /\ no_self_equiv s m) s ->
forall a, local_equivocators s a <-> local_equivocators_full s a.
Proof.
intros Hs a.
by rewrite local_equivocators_iff_simple;
[apply local_equivocators_simple_iff_full |];
revert Hs; apply UMO_reachable_impl; itauto.
Qed.
(**
The [msg_valid_full] predicate holds for any reachable state,
even though it is only explicitly checked when receiving messages.
*)
Lemma ELMO_reachable_msg_valid_full :
forall s : State,
constrained_state_prop Ei s -> ELMO_msg_valid_full (MkMessage s).
Proof.
intros s [Hs Hi]%ELMO_reachable_view.
induction Hs as [| | ? ? Hvalid]; [| specialize (IHHs Hi)..].
- by constructor; [| eexists].
- by constructor.
- by eapply MVF_recv in IHHs; [| apply Hvalid..].
Qed.
Lemma reachable_full_node_for_all_messages i' (s : State) :
constrained_state_prop (ELMO_component i') s ->
forall m, m ∈ messages s -> full_node s m.
Proof.
intros [Hs _]%ELMO_reachable_view.
induction Hs as [| | ? ? Hvalid].
- by inversion 1.
- by intros m [-> | Hm%IHHs]%elem_of_messages_addObservation; apply submseteq_cons.
- intros m Hm.
apply submseteq_cons; change (full_node s m).
apply elem_of_messages_addObservation in Hm as [-> | Hm].
+ by apply Hvalid.
+ by apply IHHs in Hm.
Qed.
Lemma reachable_sent_messages_reachable i' (s ms : State) :
constrained_state_prop (ELMO_component i') s ->
MkMessage ms ∈ sentMessages s ->
constrained_state_prop (ELMO_component i') ms.
Proof.
intros [Hs Hadr]%ELMO_reachable_view Hms.
apply ELMO_reachable_view.
induction Hs; [| | by auto].
- by apply not_elem_of_nil in Hms.
- by apply elem_of_sentMessages_addObservation in Hms as [[[= ->] _] | Hms]; auto.
Qed.
Lemma reachable_sent_messages_adr (s : State) (m : Message) :
constrained_state_prop Ei s ->
m ∈ sentMessages s ->
adr (state m) = idx i.
Proof.
intros Hs Hm; destruct m.
by eapply ELMO_reachable_adr, reachable_sent_messages_reachable.
Qed.
Lemma reachable_messages_are_msg_valid (s : State) (m : Message) :
constrained_state_prop Ei s ->
m ∈ messages s ->
ELMO_msg_valid_full m.
Proof.
intros [Hs Hadr]%ELMO_reachable_view Hm.
revert s Hs m Hm Hadr.
refine (UMO_reachable_elem_of_messages_ind _ _ _ _ _); [done | | by destruct 2].
by intros; apply ELMO_reachable_msg_valid_full, ELMO_reachable_view.
Qed.
Lemma equivocators_of_msg_subset_of_recv (s : State) (m : Message) :
full_node s m ->
forall a,
local_equivocators_simple (state m) a
-> local_equivocators_simple (s <+> MkObservation Receive m) a.
Proof.
intros Hfull a []; destruct m as [ms]; cbn in *.
assert (forall x, x ∈ messages ms -> x ∈ messages (s <+> MkObservation Receive (MkMessage ms)))
by (intros; apply elem_of_messages_addObservation; right; eapply elem_of_submseteq; done).
by eauto using local_equivocators_simple.
Qed.
Lemma equivocation_limit_recv_ok_msg_ok (s : State) (m : Message) :
full_node s m ->
no_self_equiv s m ->
UMO_reachable no_self_equiv s ->
UMO_reachable no_self_equiv (state m) ->
local_equivocation_limit_ok (s <+> MkObservation Receive m) ->
local_equivocation_limit_ok (state m).
Proof.
intros Hfull Hno_self Hs Hms Hs'.
eapply Rle_trans; [| done].
apply incl_equivocating_validators_equivocation_fault, filter_subprop; cbn; intros a Ha.
rewrite <- local_equivocators_simple_iff_full in Ha by done.
rewrite <- local_equivocators_simple_iff_full by (constructor; done).
by apply equivocators_of_msg_subset_of_recv.
Qed.
Lemma ELMO_msg_valid_prefix (m : Message) (ob : Observation) :
ELMO_msg_valid_full (m <*> ob) ->
ELMO_msg_valid_full m.
Proof.
inversion 1 as [? Hobs | |].
- by inversion Hobs.
- by replace m with m0 by (apply eq_Message; done).
- by replace m with m0 by (apply eq_Message; done).
Qed.
Lemma adr_neq_no_self_equiv (s : State) (m : Message) :
adr s <> adr (state m) ->
no_self_equiv s m.
Proof. by unfold no_self_equiv. Qed.
Lemma full_node_prefix s m ob :
full_node s (m <*> ob) ->
full_node s m.
Proof. by apply submseteq_tail_l. Qed.
Lemma ELMO_msg_valid_full_Send_inv
(P : Message -> Message -> Prop) :
(forall m om, m = om -> P m om) ->
forall (m om : Message),
ELMO_msg_valid_full (m <*> MkObservation Send om) ->
P m om.
Proof.
intros Hm m om.
inversion 1 as [? Hobs | |].
- by inversion Hobs.
- by apply Hm, eq_Message.
Qed.
Lemma incomparable_iff (m1 m2 : Message) :
incomparable m1 m2
<->
adr (state m1) = adr (state m2)
/\ m1 <> m2
/\ m1 ∉ sentMessages (state m2)
/\ m2 ∉ sentMessages (state m1).
Proof.
split.
- intros [Hadr Hnot]; split; [done |].
by repeat split; contradict Hnot; subst; constructor.
- intros (Hadr & Hneq & Hnot_m12 & Hnot_m21).
split; [done |].
by destruct 1 as [| m1 m2 [] | m1 m2 []].
Qed.
Lemma equivocation_limit_recv_msg_prefix_ok (v : State) (m : Message) ob
(m' := m <*> ob)
(v' := v <+> MkObservation Receive m')
(v'' := v <+> MkObservation Receive m)
:
adr (state m) <> adr v ->
constrained_state_prop Ei v ->
m' ∉ receivedMessages v ->
m ∉ receivedMessages v ->
ELMO_recv_valid v m' ->
local_equivocation_limit_ok (v <+> MkObservation Receive (m <*> ob)) ->
local_equivocation_limit_ok (v <+> MkObservation Receive m).
Proof.
intros Hadrs Hv Hfresh_m' Hfresh_m Hvalid Hs'.
eapply Rle_trans; [| done].
apply incl_equivocating_validators_equivocation_fault, filter_subprop; cbn.
fold v'' m' v'.
intros k Hk; cbn in *.
apply lefo_alt in Hk as [(-> & _ & u & Hu & Hincomp) |]; [| by apply lefo_prev].
apply (lefo_last _ m' u Hu).
apply incomparable_iff in Hincomp as (Hadr & Hneq & H_m1_m2 & H_m2_m1).
apply incomparable_iff; repeat split; [done | by intros <- | |].
- intro Hm'.
contradict Hfresh_m'.
apply not_adr_received; [| done |].
+ apply UMO_reachable_impl with (1 := ELMO_mv_no_self_equiv).
by apply ELMO_reachable_view in Hv as [].
+ eapply elem_of_submseteq.
* by apply elem_of_messages; left.
* apply reachable_full_node_for_all_messages with (1 := Hv).
by apply elem_of_messages; right.
- intros [[-> Hob] |]%elem_of_sentMessages_addObservation; [| done].
destruct ob as [[] om], Hob, Hneq; cbn in *.
assert (ELMO_msg_valid_full m') as Hmv by apply Hvalid.
by inversion Hmv; [| apply eq_Message].
Qed.
Hint Resolve