-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathp2p.tla
1168 lines (1021 loc) · 75.6 KB
/
p2p.tla
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
-------------------------------- MODULE p2p ---------------------------------
(***************************************************************************)
(* This module defines a simple peer-to-peer network protocol that allows *)
(* peers to connect, exchange blocks, and synchronize their chains. *)
(***************************************************************************)
EXTENDS TLC, Sequences, Naturals, FiniteSets, Utils, Blockchain
\* Define the network to be used by the algorithm.
CONSTANT RunningBlockchain
\* Maximum number of blocks to be retrieved in a single getblocks response.
CONSTANT MaxGetBlocksInvResponse
\* Maximum number of outbound connections a peer can have.
CONSTANT MaxConnectionsPerPeer
\* Difference in the SYNCHRONIZER process id so that it does not conflict with the LISTENER one.
PeerProcessDiffId == 1000
-----------------------------------------------------------------------------
(*--algorithm p2p
variables
\* Represent the whole universe of peers in the network with all of their data.
the_network = RunningBlockchain;
\* Each peer has a channel to communicate with other peers. Number of connections is limited.
channels = [i \in 1..Len(the_network) |->
[j \in 1..MaxConnectionsPerPeer |-> [
header |-> defaultInitValue,
payload |-> defaultInitValue
]]
];
define
\* Import the operators used in the algorithm.
LOCAL Ops == INSTANCE Operators
(***********************************************************************)
(* This property checks for the existence of at least one execution *)
(* path in which all peers eventually have the same chain tip. It *)
(* ensures that there is a scenario in which synchronization occurs, *)
(* but does NOT guarantee that synchronization will happen in every *)
(* possible execution. This makes it an existential check, not a *)
(* liveness property. *)
(***********************************************************************)
ExistsSyncPath ==
\E peer1, peer2 \in 1..Len(RunningBlockchain) :
<>(Ops!GetPeerTipByIndex(peer1).height = Ops!GetPeerTipByIndex(peer2).height)
(***********************************************************************)
(* Liveness: Eventually, all peers will have the same chain tip. *)
(* This property ensures that synchronization will happen in every *)
(* possible path. *)
(* *)
(* Note: This property is not guaranteed to hold in the current *)
(* implementation. *)
(***********************************************************************)
Liveness ==
\A peer1, peer2 \in 1..Len(RunningBlockchain) :
<>(Ops!GetPeerTipByIndex(peer1).height = Ops!GetPeerTipByIndex(peer2).height)
(***********************************************************************)
(* Ensures that no peer in the network has a chain tip that is higher *)
(* than the chain tip of any peer it is connected to. This guarantees *)
(* that peers do not "advance" their chain beyond the knowledge of *)
(* their connected peers, ensuring consistent progress across the *)
(* network. *)
(***********************************************************************)
ChainTipRespectsPeerSet ==
\A peer \in 1..Len(RunningBlockchain) :
\A remote_peer \in 1..Len(the_network[peer].peer_set) :
Ops!GetPeerTipByIndex(peer).height <= Ops!GetPeerTipByIndex(remote_peer).height
(***********************************************************************)
(* Ensures that each block in a peer’s local blockchain has a height *)
(* less than or equal to the peer’s chain tip. This prevents peers from*)
(* including invalid blocks that exceed the current chain tip. *)
(***********************************************************************)
ValidBlockPropagation ==
\A peer \in 1..Len(RunningBlockchain) :
\A block \in the_network[peer].blocks :
block.height <= Ops!GetPeerTipByIndex(peer).height
(***********************************************************************)
(* Ensures that the blocks within each peer’s blockchain are correctly *)
(* ordered by height. For blocks with height greater than 1, each block*)
(* must directly follow the block with height block.height - 1. This *)
(* prevents gaps or misordering within a peer's chain. *)
(***********************************************************************)
BlockOrdering ==
\A peer \in 1..Len(RunningBlockchain) :
\A block \in the_network[peer].blocks :
IF block.height < 2 THEN
TRUE
ELSE
block.height =
(CHOOSE b \in the_network[peer].blocks : b.height = block.height - 1).height + 1
(***********************************************************************)
(* Ensures that each peer eventually reaches a chain tip that is at *)
(* least as high as the initial chain tip it started with. This ensures*)
(* that peers make progress in synchronizing their chains over time. *)
(***********************************************************************)
SyncProgress ==
\A peer \in 1..Len(RunningBlockchain) :
<>(Ops!GetPeerTipByIndex(peer).height >=
Ops!GetPeerTipByIndexAndNetwork(peer, RunningBlockchain).height)
(***********************************************************************)
(* Ensures that no peer exceeds the maximum number of connections *)
(* allowed, ensuring that the network respects its maximum connection *)
(* constraints. This prevents any peer from overloading its connection *)
(* capacity. *)
(***********************************************************************)
ConnectionLimit ==
\A peer \in 1..Len(RunningBlockchain) :
Len(the_network[peer].peer_set) <= MaxConnectionsPerPeer
(***********************************************************************)
(* Ensures that for any two peers, if they have blocks at the same *)
(* height, the blocks must be identical in both content and hash. This *)
(* guarantees that no two peers hold blocks with the same height but *)
(* different content, preventing inconsistencies and potential forks *)
(* in the blockchain. *)
(***********************************************************************)
ConsistentBlocksAcrossPeers ==
\A peer1, peer2 \in 1..Len(RunningBlockchain) :
peer1 # peer2 =>
\A block1 \in the_network[peer1].blocks, block2 \in the_network[peer2].blocks :
block1.height = block2.height =>
block1.hash = block2.hash /\ block1.block = block2.block
(***************************************************************************)
(* The overall inductive invariant that combines several sub-properties *)
(* to ensure safety and correctness in the peer-to-peer protocol: *)
(* - ChainTipRespectsPeerSet ensures chain tip consistency between peers. *)
(* - ValidBlockPropagation ensures peers propagate valid blocks. *)
(* - BlockOrdering ensures correct block order within each peer’s chain. *)
(* - SyncProgress ensures that peers continue to progress toward *)
(* synchronization. *)
(* - ConnectionLimit ensures peers respect connection limits. *)
(***************************************************************************)
InductiveInvariant ==
/\ ChainTipRespectsPeerSet
/\ ValidBlockPropagation
/\ BlockOrdering
/\ SyncProgress
/\ ConnectionLimit
/\ ConsistentBlocksAcrossPeers
end define;
\* Announce the intention of a peer to connect with another in the network by sending an `addr` message.
procedure announce(local_peer_id, remote_peer_id)
begin
SendAddrMsg:
channels[local_peer_id][remote_peer_id] := [
header |-> [command_name |-> "addr"],
payload |-> [
address_count |-> 1,
\* Only a single address is supported.
addresses |-> the_network[local_peer_id].peer
]
];
return;
end procedure;
\* Given that an `addr` message is received, send a `version` message from the remote peer to start the connection.
procedure addr(local_peer_id, remote_peer_id)
begin
SendVersionMsg:
channels[local_peer_id][remote_peer_id] := [
header |-> [command_name |-> "version"],
payload |-> [
addr_recv |-> the_network[local_peer_id].peer,
addr_trans |-> the_network[local_peer_id].peer_set[remote_peer_id].address,
start_height |->
Ops!GetPeerTipByAddress(the_network[local_peer_id].peer_set[remote_peer_id].address).height]
];
return;
end procedure;
\* Given a `version` message is received, send `verack` to acknowledge the connection.
procedure version(local_peer_id, remote_peer_id)
begin
HandleVersionMsg:
the_network[local_peer_id].peer_set[remote_peer_id].tip :=
channels[local_peer_id][remote_peer_id].payload.start_height;
SendVerackMsg:
channels[local_peer_id][remote_peer_id] := [
header |-> [command_name |-> "verack"],
payload |-> defaultInitValue
];
return;
end procedure;
\* Given a `verack` message is received, establish the connection.
procedure verack(local_peer_id, remote_peer_id)
begin
HandleVerackMsg:
the_network[local_peer_id].peer_set[remote_peer_id].established := TRUE;
return;
end procedure;
\* Given a `getblocks` message is received, send an `inv` message with the blocks requested.
procedure getblocks(local_peer_id, remote_peer_id)
variables
found_blocks, hash_count, block_header_hashes, remote_peer_blocks, start_height, end_height;
begin
HandleGetBlocksMsg:
\* Retrieve necessary values from the channel payload
hash_count := channels[local_peer_id][remote_peer_id].payload.hash_count;
block_header_hashes := channels[local_peer_id][remote_peer_id].payload.block_header_hashes;
\* Fetch the blocks of the remote peer
remote_peer_blocks :=
Ops!GetPeerBlocks(the_network[local_peer_id].peer_set[remote_peer_id].address);
\* Determine the range of blocks to retrieve
if hash_count = 0 then
start_height := 1;
else
\* Assuming the hashes are in order, the height of the first hash should be the tip, ignore the rest.
start_height :=
Ops!FindBlockByHash(remote_peer_blocks, block_header_hashes[1]).height + 1;
end if;
end_height := start_height + (MaxGetBlocksInvResponse - 1);
\* Find the blocks within the specified range.
found_blocks := Ops!FindBlocks(remote_peer_blocks, start_height, end_height);
SendInvMsg:
channels[local_peer_id][remote_peer_id] := [
header |-> [command_name |-> "inv"],
payload |-> [
count |-> Cardinality(found_blocks),
inventory |-> [
h \in 1..Cardinality(found_blocks) |-> [
type_identifier |-> "MSG_BLOCK",
hash |-> SetToSeq({ s.hash : s \in found_blocks })[h]
]
]
]
];
return;
end procedure;
\* Request blocks from the remote peer by sending a `getblocks` message with local hashes.
procedure request_blocks(hashes, local_peer_id, remote_peer_id)
begin
SendGetBlocksMsg:
channels[local_peer_id][remote_peer_id] := [
header |-> [command_name |-> "getblocks"],
payload |-> [
hash_count |-> Len(hashes),
block_header_hashes |-> hashes]
];
return;
end procedure;
\* Given an `inv` message is received, send a `getdata` message to request the blocks.
procedure inv(local_peer_id, remote_peer_id)
begin
SendGetDataMsg:
channels[local_peer_id][remote_peer_id] := [
header |-> [command_name |-> "getdata"],
payload |-> channels[local_peer_id][remote_peer_id].payload
];
return;
end procedure;
\* Incorporate data to the local peer from the inventory received.
procedure getdata(local_peer_id, remote_peer_id)
variables blocks_data;
begin
HandleGetDataMsg:
blocks_data := [item \in 1..Len(channels[local_peer_id][remote_peer_id].payload.inventory) |->
Ops!FindBlockByHash(
Ops!GetPeerBlocks(the_network[local_peer_id].peer_set[remote_peer_id].address),
channels[local_peer_id][remote_peer_id].payload.inventory[item].hash
)
];
IncorporateBlocks:
the_network[local_peer_id].blocks := the_network[local_peer_id].blocks \cup ToSet(blocks_data);
return;
end procedure;
\* A set of listener process for each peer to listen to incoming messages and act accordingly.
process LISTENER \in 1 .. Len(RunningBlockchain)
variables command;
begin
Listening:
await Len(the_network) >= 2;
with remote_peer_index \in 1..Len(the_network[self].peer_set) do
if channels[self][remote_peer_index].header = defaultInitValue then
goto Listening;
end if;
end with;
Requests:
with remote_peer_index \in 1..Len(the_network[self].peer_set) do
await channels[self][remote_peer_index].header # defaultInitValue;
command := channels[self][remote_peer_index].header.command_name;
if command = "addr" then
call addr(self, remote_peer_index);
goto Listening;
elsif command = "version" then
call version(self, remote_peer_index);
goto Listening;
elsif command = "verack" then
call verack(self, remote_peer_index);
elsif command = "getblocks" then
call getblocks(self, remote_peer_index);
goto Listening;
elsif command = "inv" then
call inv(self, remote_peer_index);
goto Listening;
elsif command = "getdata" then
call getdata(self, remote_peer_index);
end if;
end with;
ListenerLoop:
with remote_peer_index \in 1..Len(the_network[self].peer_set) do
channels[self][remote_peer_index] :=
[header |-> defaultInitValue, payload |-> defaultInitValue];
goto Listening;
end with;
end process;
\* A set of processes to synchronize each peer with the network.
process SYNCHRONIZER \in PeerProcessDiffId + 1 .. PeerProcessDiffId + Len(RunningBlockchain)
variables local_peer_index = self - PeerProcessDiffId, best_tip = 0;
begin
Announce:
\* The network must have at least two peer.
assert Len(the_network) >= 2;
\* The peer set size must be at least 1, ignoring the peers that are seeders only.
await Len(the_network[local_peer_index].peer_set) > 0;
\* Connect to each available peer we have.
with remote_peer_index \in 1..Len(the_network[local_peer_index].peer_set) do
call announce(local_peer_index, remote_peer_index);
end with;
RequestInventory:
with remote_peer_index \in 1..Len(the_network[local_peer_index].peer_set) do
\* Make sure the connection is established before requesting any block from this peer.
await the_network[local_peer_index].peer_set[remote_peer_index].established = TRUE;
\* Find the best tip among all peers.
if the_network[local_peer_index].peer_set[remote_peer_index].tip > best_tip then
best_tip := the_network[local_peer_index].peer_set[remote_peer_index].tip;
end if;
\* Wait for the peer channel to be empty before requesting new blocks.
await channels[local_peer_index][remote_peer_index].header = defaultInitValue
/\ channels[local_peer_index][remote_peer_index].payload = defaultInitValue;
\* Check if the local peer is behind the remote peer.
if Ops!GetPeerTipByIndex(local_peer_index).height <
the_network[local_peer_index].peer_set[remote_peer_index].tip then
\* Request blocks.
if Ops!GetPeerTipByIndex(local_peer_index).height = 0 then
call request_blocks(<<>>, local_peer_index, remote_peer_index);
else
call request_blocks(
<<Ops!GetPeerTipByIndex(local_peer_index).hash>>,
local_peer_index,
remote_peer_index
);
end if;
end if;
end with;
CheckSync:
await Ops!GetPeerTipByIndex(local_peer_index).height > 0;
if Ops!GetPeerTipByIndex(local_peer_index).height < best_tip then
goto RequestInventory;
else
\* Make sure all connections are still established and all communication channels are empty
with remote_peer_index \in 1..Len(the_network[local_peer_index].peer_set) do
await the_network[local_peer_index].peer_set[remote_peer_index].established = TRUE
/\ channels[local_peer_index][remote_peer_index].header = defaultInitValue
/\ channels[local_peer_index][remote_peer_index].payload = defaultInitValue;
end with;
end if;
end process;
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "fb1948d7" /\ chksum(tla) = "bceb3955")
\* Parameter local_peer_id of procedure announce at line 155 col 20 changed to local_peer_id_
\* Parameter remote_peer_id of procedure announce at line 155 col 35 changed to remote_peer_id_
\* Parameter local_peer_id of procedure addr at line 170 col 16 changed to local_peer_id_a
\* Parameter remote_peer_id of procedure addr at line 170 col 31 changed to remote_peer_id_a
\* Parameter local_peer_id of procedure version at line 185 col 19 changed to local_peer_id_v
\* Parameter remote_peer_id of procedure version at line 185 col 34 changed to remote_peer_id_v
\* Parameter local_peer_id of procedure verack at line 199 col 18 changed to local_peer_id_ve
\* Parameter remote_peer_id of procedure verack at line 199 col 33 changed to remote_peer_id_ve
\* Parameter local_peer_id of procedure getblocks at line 207 col 21 changed to local_peer_id_g
\* Parameter remote_peer_id of procedure getblocks at line 207 col 36 changed to remote_peer_id_g
\* Parameter local_peer_id of procedure request_blocks at line 249 col 34 changed to local_peer_id_r
\* Parameter remote_peer_id of procedure request_blocks at line 249 col 49 changed to remote_peer_id_r
\* Parameter local_peer_id of procedure inv at line 262 col 15 changed to local_peer_id_i
\* Parameter remote_peer_id of procedure inv at line 262 col 30 changed to remote_peer_id_i
CONSTANT defaultInitValue
VARIABLES the_network, channels, pc, stack
(* define statement *)
LOCAL Ops == INSTANCE Operators
ExistsSyncPath ==
\E peer1, peer2 \in 1..Len(RunningBlockchain) :
<>(Ops!GetPeerTipByIndex(peer1).height = Ops!GetPeerTipByIndex(peer2).height)
Liveness ==
\A peer1, peer2 \in 1..Len(RunningBlockchain) :
<>(Ops!GetPeerTipByIndex(peer1).height = Ops!GetPeerTipByIndex(peer2).height)
ChainTipRespectsPeerSet ==
\A peer \in 1..Len(RunningBlockchain) :
\A remote_peer \in 1..Len(the_network[peer].peer_set) :
Ops!GetPeerTipByIndex(peer).height <= Ops!GetPeerTipByIndex(remote_peer).height
ValidBlockPropagation ==
\A peer \in 1..Len(RunningBlockchain) :
\A block \in the_network[peer].blocks :
block.height <= Ops!GetPeerTipByIndex(peer).height
BlockOrdering ==
\A peer \in 1..Len(RunningBlockchain) :
\A block \in the_network[peer].blocks :
IF block.height < 2 THEN
TRUE
ELSE
block.height =
(CHOOSE b \in the_network[peer].blocks : b.height = block.height - 1).height + 1
SyncProgress ==
\A peer \in 1..Len(RunningBlockchain) :
<>(Ops!GetPeerTipByIndex(peer).height >=
Ops!GetPeerTipByIndexAndNetwork(peer, RunningBlockchain).height)
ConnectionLimit ==
\A peer \in 1..Len(RunningBlockchain) :
Len(the_network[peer].peer_set) <= MaxConnectionsPerPeer
ConsistentBlocksAcrossPeers ==
\A peer1, peer2 \in 1..Len(RunningBlockchain) :
peer1 # peer2 =>
\A block1 \in the_network[peer1].blocks, block2 \in the_network[peer2].blocks :
block1.height = block2.height =>
block1.hash = block2.hash /\ block1.block = block2.block
InductiveInvariant ==
/\ ChainTipRespectsPeerSet
/\ ValidBlockPropagation
/\ BlockOrdering
/\ SyncProgress
/\ ConnectionLimit
/\ ConsistentBlocksAcrossPeers
VARIABLES local_peer_id_, remote_peer_id_, local_peer_id_a, remote_peer_id_a,
local_peer_id_v, remote_peer_id_v, local_peer_id_ve,
remote_peer_id_ve, local_peer_id_g, remote_peer_id_g, found_blocks,
hash_count, block_header_hashes, remote_peer_blocks, start_height,
end_height, hashes, local_peer_id_r, remote_peer_id_r,
local_peer_id_i, remote_peer_id_i, local_peer_id, remote_peer_id,
blocks_data, command, local_peer_index, best_tip
vars == << the_network, channels, pc, stack, local_peer_id_, remote_peer_id_,
local_peer_id_a, remote_peer_id_a, local_peer_id_v,
remote_peer_id_v, local_peer_id_ve, remote_peer_id_ve,
local_peer_id_g, remote_peer_id_g, found_blocks, hash_count,
block_header_hashes, remote_peer_blocks, start_height, end_height,
hashes, local_peer_id_r, remote_peer_id_r, local_peer_id_i,
remote_peer_id_i, local_peer_id, remote_peer_id, blocks_data,
command, local_peer_index, best_tip >>
ProcSet == (1 .. Len(RunningBlockchain)) \cup (PeerProcessDiffId + 1 .. PeerProcessDiffId + Len(RunningBlockchain))
Init == (* Global variables *)
/\ the_network = RunningBlockchain
/\ channels = [i \in 1..Len(the_network) |->
[j \in 1..MaxConnectionsPerPeer |-> [
header |-> defaultInitValue,
payload |-> defaultInitValue
]]
]
(* Procedure announce *)
/\ local_peer_id_ = [ self \in ProcSet |-> defaultInitValue]
/\ remote_peer_id_ = [ self \in ProcSet |-> defaultInitValue]
(* Procedure addr *)
/\ local_peer_id_a = [ self \in ProcSet |-> defaultInitValue]
/\ remote_peer_id_a = [ self \in ProcSet |-> defaultInitValue]
(* Procedure version *)
/\ local_peer_id_v = [ self \in ProcSet |-> defaultInitValue]
/\ remote_peer_id_v = [ self \in ProcSet |-> defaultInitValue]
(* Procedure verack *)
/\ local_peer_id_ve = [ self \in ProcSet |-> defaultInitValue]
/\ remote_peer_id_ve = [ self \in ProcSet |-> defaultInitValue]
(* Procedure getblocks *)
/\ local_peer_id_g = [ self \in ProcSet |-> defaultInitValue]
/\ remote_peer_id_g = [ self \in ProcSet |-> defaultInitValue]
/\ found_blocks = [ self \in ProcSet |-> defaultInitValue]
/\ hash_count = [ self \in ProcSet |-> defaultInitValue]
/\ block_header_hashes = [ self \in ProcSet |-> defaultInitValue]
/\ remote_peer_blocks = [ self \in ProcSet |-> defaultInitValue]
/\ start_height = [ self \in ProcSet |-> defaultInitValue]
/\ end_height = [ self \in ProcSet |-> defaultInitValue]
(* Procedure request_blocks *)
/\ hashes = [ self \in ProcSet |-> defaultInitValue]
/\ local_peer_id_r = [ self \in ProcSet |-> defaultInitValue]
/\ remote_peer_id_r = [ self \in ProcSet |-> defaultInitValue]
(* Procedure inv *)
/\ local_peer_id_i = [ self \in ProcSet |-> defaultInitValue]
/\ remote_peer_id_i = [ self \in ProcSet |-> defaultInitValue]
(* Procedure getdata *)
/\ local_peer_id = [ self \in ProcSet |-> defaultInitValue]
/\ remote_peer_id = [ self \in ProcSet |-> defaultInitValue]
/\ blocks_data = [ self \in ProcSet |-> defaultInitValue]
(* Process LISTENER *)
/\ command = [self \in 1 .. Len(RunningBlockchain) |-> defaultInitValue]
(* Process SYNCHRONIZER *)
/\ local_peer_index = [self \in PeerProcessDiffId + 1 .. PeerProcessDiffId + Len(RunningBlockchain) |-> self - PeerProcessDiffId]
/\ best_tip = [self \in PeerProcessDiffId + 1 .. PeerProcessDiffId + Len(RunningBlockchain) |-> 0]
/\ stack = [self \in ProcSet |-> << >>]
/\ pc = [self \in ProcSet |-> CASE self \in 1 .. Len(RunningBlockchain) -> "Listening"
[] self \in PeerProcessDiffId + 1 .. PeerProcessDiffId + Len(RunningBlockchain) -> "Announce"]
SendAddrMsg(self) == /\ pc[self] = "SendAddrMsg"
/\ channels' = [channels EXCEPT ![local_peer_id_[self]][remote_peer_id_[self]] = [
header |-> [command_name |-> "addr"],
payload |-> [
address_count |-> 1,
addresses |-> the_network[local_peer_id_[self]].peer
]
]]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ local_peer_id_' = [local_peer_id_ EXCEPT ![self] = Head(stack[self]).local_peer_id_]
/\ remote_peer_id_' = [remote_peer_id_ EXCEPT ![self] = Head(stack[self]).remote_peer_id_]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << the_network, local_peer_id_a,
remote_peer_id_a, local_peer_id_v,
remote_peer_id_v, local_peer_id_ve,
remote_peer_id_ve, local_peer_id_g,
remote_peer_id_g, found_blocks,
hash_count, block_header_hashes,
remote_peer_blocks, start_height,
end_height, hashes, local_peer_id_r,
remote_peer_id_r, local_peer_id_i,
remote_peer_id_i, local_peer_id,
remote_peer_id, blocks_data, command,
local_peer_index, best_tip >>
announce(self) == SendAddrMsg(self)
SendVersionMsg(self) == /\ pc[self] = "SendVersionMsg"
/\ channels' = [channels EXCEPT ![local_peer_id_a[self]][remote_peer_id_a[self]] = [
header |-> [command_name |-> "version"],
payload |-> [
addr_recv |-> the_network[local_peer_id_a[self]].peer,
addr_trans |-> the_network[local_peer_id_a[self]].peer_set[remote_peer_id_a[self]].address,
start_height |->
Ops!GetPeerTipByAddress(the_network[local_peer_id_a[self]].peer_set[remote_peer_id_a[self]].address).height]
]]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ local_peer_id_a' = [local_peer_id_a EXCEPT ![self] = Head(stack[self]).local_peer_id_a]
/\ remote_peer_id_a' = [remote_peer_id_a EXCEPT ![self] = Head(stack[self]).remote_peer_id_a]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << the_network, local_peer_id_,
remote_peer_id_, local_peer_id_v,
remote_peer_id_v, local_peer_id_ve,
remote_peer_id_ve, local_peer_id_g,
remote_peer_id_g, found_blocks,
hash_count, block_header_hashes,
remote_peer_blocks, start_height,
end_height, hashes, local_peer_id_r,
remote_peer_id_r, local_peer_id_i,
remote_peer_id_i, local_peer_id,
remote_peer_id, blocks_data, command,
local_peer_index, best_tip >>
addr(self) == SendVersionMsg(self)
HandleVersionMsg(self) == /\ pc[self] = "HandleVersionMsg"
/\ the_network' = [the_network EXCEPT ![local_peer_id_v[self]].peer_set[remote_peer_id_v[self]].tip = channels[local_peer_id_v[self]][remote_peer_id_v[self]].payload.start_height]
/\ pc' = [pc EXCEPT ![self] = "SendVerackMsg"]
/\ UNCHANGED << channels, stack, local_peer_id_,
remote_peer_id_, local_peer_id_a,
remote_peer_id_a, local_peer_id_v,
remote_peer_id_v, local_peer_id_ve,
remote_peer_id_ve, local_peer_id_g,
remote_peer_id_g, found_blocks,
hash_count, block_header_hashes,
remote_peer_blocks, start_height,
end_height, hashes, local_peer_id_r,
remote_peer_id_r, local_peer_id_i,
remote_peer_id_i, local_peer_id,
remote_peer_id, blocks_data, command,
local_peer_index, best_tip >>
SendVerackMsg(self) == /\ pc[self] = "SendVerackMsg"
/\ channels' = [channels EXCEPT ![local_peer_id_v[self]][remote_peer_id_v[self]] = [
header |-> [command_name |-> "verack"],
payload |-> defaultInitValue
]]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ local_peer_id_v' = [local_peer_id_v EXCEPT ![self] = Head(stack[self]).local_peer_id_v]
/\ remote_peer_id_v' = [remote_peer_id_v EXCEPT ![self] = Head(stack[self]).remote_peer_id_v]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << the_network, local_peer_id_,
remote_peer_id_, local_peer_id_a,
remote_peer_id_a, local_peer_id_ve,
remote_peer_id_ve, local_peer_id_g,
remote_peer_id_g, found_blocks,
hash_count, block_header_hashes,
remote_peer_blocks, start_height,
end_height, hashes, local_peer_id_r,
remote_peer_id_r, local_peer_id_i,
remote_peer_id_i, local_peer_id,
remote_peer_id, blocks_data, command,
local_peer_index, best_tip >>
version(self) == HandleVersionMsg(self) \/ SendVerackMsg(self)
HandleVerackMsg(self) == /\ pc[self] = "HandleVerackMsg"
/\ the_network' = [the_network EXCEPT ![local_peer_id_ve[self]].peer_set[remote_peer_id_ve[self]].established = TRUE]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ local_peer_id_ve' = [local_peer_id_ve EXCEPT ![self] = Head(stack[self]).local_peer_id_ve]
/\ remote_peer_id_ve' = [remote_peer_id_ve EXCEPT ![self] = Head(stack[self]).remote_peer_id_ve]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << channels, local_peer_id_,
remote_peer_id_, local_peer_id_a,
remote_peer_id_a, local_peer_id_v,
remote_peer_id_v, local_peer_id_g,
remote_peer_id_g, found_blocks,
hash_count, block_header_hashes,
remote_peer_blocks, start_height,
end_height, hashes, local_peer_id_r,
remote_peer_id_r, local_peer_id_i,
remote_peer_id_i, local_peer_id,
remote_peer_id, blocks_data, command,
local_peer_index, best_tip >>
verack(self) == HandleVerackMsg(self)
HandleGetBlocksMsg(self) == /\ pc[self] = "HandleGetBlocksMsg"
/\ hash_count' = [hash_count EXCEPT ![self] = channels[local_peer_id_g[self]][remote_peer_id_g[self]].payload.hash_count]
/\ block_header_hashes' = [block_header_hashes EXCEPT ![self] = channels[local_peer_id_g[self]][remote_peer_id_g[self]].payload.block_header_hashes]
/\ remote_peer_blocks' = [remote_peer_blocks EXCEPT ![self] = Ops!GetPeerBlocks(the_network[local_peer_id_g[self]].peer_set[remote_peer_id_g[self]].address)]
/\ IF hash_count'[self] = 0
THEN /\ start_height' = [start_height EXCEPT ![self] = 1]
ELSE /\ start_height' = [start_height EXCEPT ![self] = Ops!FindBlockByHash(remote_peer_blocks'[self], block_header_hashes'[self][1]).height + 1]
/\ end_height' = [end_height EXCEPT ![self] = start_height'[self] + (MaxGetBlocksInvResponse - 1)]
/\ found_blocks' = [found_blocks EXCEPT ![self] = Ops!FindBlocks(remote_peer_blocks'[self], start_height'[self], end_height'[self])]
/\ pc' = [pc EXCEPT ![self] = "SendInvMsg"]
/\ UNCHANGED << the_network, channels, stack,
local_peer_id_, remote_peer_id_,
local_peer_id_a, remote_peer_id_a,
local_peer_id_v, remote_peer_id_v,
local_peer_id_ve,
remote_peer_id_ve, local_peer_id_g,
remote_peer_id_g, hashes,
local_peer_id_r, remote_peer_id_r,
local_peer_id_i, remote_peer_id_i,
local_peer_id, remote_peer_id,
blocks_data, command,
local_peer_index, best_tip >>
SendInvMsg(self) == /\ pc[self] = "SendInvMsg"
/\ channels' = [channels EXCEPT ![local_peer_id_g[self]][remote_peer_id_g[self]] = [
header |-> [command_name |-> "inv"],
payload |-> [
count |-> Cardinality(found_blocks[self]),
inventory |-> [
h \in 1..Cardinality(found_blocks[self]) |-> [
type_identifier |-> "MSG_BLOCK",
hash |-> SetToSeq({ s.hash : s \in found_blocks[self] })[h]
]
]
]
]]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ found_blocks' = [found_blocks EXCEPT ![self] = Head(stack[self]).found_blocks]
/\ hash_count' = [hash_count EXCEPT ![self] = Head(stack[self]).hash_count]
/\ block_header_hashes' = [block_header_hashes EXCEPT ![self] = Head(stack[self]).block_header_hashes]
/\ remote_peer_blocks' = [remote_peer_blocks EXCEPT ![self] = Head(stack[self]).remote_peer_blocks]
/\ start_height' = [start_height EXCEPT ![self] = Head(stack[self]).start_height]
/\ end_height' = [end_height EXCEPT ![self] = Head(stack[self]).end_height]
/\ local_peer_id_g' = [local_peer_id_g EXCEPT ![self] = Head(stack[self]).local_peer_id_g]
/\ remote_peer_id_g' = [remote_peer_id_g EXCEPT ![self] = Head(stack[self]).remote_peer_id_g]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << the_network, local_peer_id_,
remote_peer_id_, local_peer_id_a,
remote_peer_id_a, local_peer_id_v,
remote_peer_id_v, local_peer_id_ve,
remote_peer_id_ve, hashes, local_peer_id_r,
remote_peer_id_r, local_peer_id_i,
remote_peer_id_i, local_peer_id,
remote_peer_id, blocks_data, command,
local_peer_index, best_tip >>
getblocks(self) == HandleGetBlocksMsg(self) \/ SendInvMsg(self)
SendGetBlocksMsg(self) == /\ pc[self] = "SendGetBlocksMsg"
/\ channels' = [channels EXCEPT ![local_peer_id_r[self]][remote_peer_id_r[self]] = [
header |-> [command_name |-> "getblocks"],
payload |-> [
hash_count |-> Len(hashes[self]),
block_header_hashes |-> hashes[self]]
]]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ hashes' = [hashes EXCEPT ![self] = Head(stack[self]).hashes]
/\ local_peer_id_r' = [local_peer_id_r EXCEPT ![self] = Head(stack[self]).local_peer_id_r]
/\ remote_peer_id_r' = [remote_peer_id_r EXCEPT ![self] = Head(stack[self]).remote_peer_id_r]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << the_network, local_peer_id_,
remote_peer_id_, local_peer_id_a,
remote_peer_id_a, local_peer_id_v,
remote_peer_id_v, local_peer_id_ve,
remote_peer_id_ve, local_peer_id_g,
remote_peer_id_g, found_blocks,
hash_count, block_header_hashes,
remote_peer_blocks, start_height,
end_height, local_peer_id_i,
remote_peer_id_i, local_peer_id,
remote_peer_id, blocks_data, command,
local_peer_index, best_tip >>
request_blocks(self) == SendGetBlocksMsg(self)
SendGetDataMsg(self) == /\ pc[self] = "SendGetDataMsg"
/\ channels' = [channels EXCEPT ![local_peer_id_i[self]][remote_peer_id_i[self]] = [
header |-> [command_name |-> "getdata"],
payload |-> channels[local_peer_id_i[self]][remote_peer_id_i[self]].payload
]]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ local_peer_id_i' = [local_peer_id_i EXCEPT ![self] = Head(stack[self]).local_peer_id_i]
/\ remote_peer_id_i' = [remote_peer_id_i EXCEPT ![self] = Head(stack[self]).remote_peer_id_i]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << the_network, local_peer_id_,
remote_peer_id_, local_peer_id_a,
remote_peer_id_a, local_peer_id_v,
remote_peer_id_v, local_peer_id_ve,
remote_peer_id_ve, local_peer_id_g,
remote_peer_id_g, found_blocks,
hash_count, block_header_hashes,
remote_peer_blocks, start_height,
end_height, hashes, local_peer_id_r,
remote_peer_id_r, local_peer_id,
remote_peer_id, blocks_data, command,
local_peer_index, best_tip >>
inv(self) == SendGetDataMsg(self)
HandleGetDataMsg(self) == /\ pc[self] = "HandleGetDataMsg"
/\ blocks_data' = [blocks_data EXCEPT ![self] = [item \in 1..Len(channels[local_peer_id[self]][remote_peer_id[self]].payload.inventory) |->
Ops!FindBlockByHash(
Ops!GetPeerBlocks(the_network[local_peer_id[self]].peer_set[remote_peer_id[self]].address),
channels[local_peer_id[self]][remote_peer_id[self]].payload.inventory[item].hash
)
]]
/\ pc' = [pc EXCEPT ![self] = "IncorporateBlocks"]
/\ UNCHANGED << the_network, channels, stack,
local_peer_id_, remote_peer_id_,
local_peer_id_a, remote_peer_id_a,
local_peer_id_v, remote_peer_id_v,
local_peer_id_ve, remote_peer_id_ve,
local_peer_id_g, remote_peer_id_g,
found_blocks, hash_count,
block_header_hashes,
remote_peer_blocks, start_height,
end_height, hashes, local_peer_id_r,
remote_peer_id_r, local_peer_id_i,
remote_peer_id_i, local_peer_id,
remote_peer_id, command,
local_peer_index, best_tip >>
IncorporateBlocks(self) == /\ pc[self] = "IncorporateBlocks"
/\ the_network' = [the_network EXCEPT ![local_peer_id[self]].blocks = the_network[local_peer_id[self]].blocks \cup ToSet(blocks_data[self])]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ blocks_data' = [blocks_data EXCEPT ![self] = Head(stack[self]).blocks_data]
/\ local_peer_id' = [local_peer_id EXCEPT ![self] = Head(stack[self]).local_peer_id]
/\ remote_peer_id' = [remote_peer_id EXCEPT ![self] = Head(stack[self]).remote_peer_id]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << channels, local_peer_id_,
remote_peer_id_, local_peer_id_a,
remote_peer_id_a, local_peer_id_v,
remote_peer_id_v, local_peer_id_ve,
remote_peer_id_ve, local_peer_id_g,
remote_peer_id_g, found_blocks,
hash_count, block_header_hashes,
remote_peer_blocks, start_height,
end_height, hashes, local_peer_id_r,
remote_peer_id_r, local_peer_id_i,
remote_peer_id_i, command,
local_peer_index, best_tip >>
getdata(self) == HandleGetDataMsg(self) \/ IncorporateBlocks(self)
Listening(self) == /\ pc[self] = "Listening"
/\ Len(the_network) >= 2
/\ \E remote_peer_index \in 1..Len(the_network[self].peer_set):
IF channels[self][remote_peer_index].header = defaultInitValue
THEN /\ pc' = [pc EXCEPT ![self] = "Listening"]
ELSE /\ pc' = [pc EXCEPT ![self] = "Requests"]
/\ UNCHANGED << the_network, channels, stack,
local_peer_id_, remote_peer_id_,
local_peer_id_a, remote_peer_id_a,
local_peer_id_v, remote_peer_id_v,
local_peer_id_ve, remote_peer_id_ve,
local_peer_id_g, remote_peer_id_g,
found_blocks, hash_count,
block_header_hashes, remote_peer_blocks,
start_height, end_height, hashes,
local_peer_id_r, remote_peer_id_r,
local_peer_id_i, remote_peer_id_i,
local_peer_id, remote_peer_id, blocks_data,
command, local_peer_index, best_tip >>
Requests(self) == /\ pc[self] = "Requests"
/\ \E remote_peer_index \in 1..Len(the_network[self].peer_set):
/\ channels[self][remote_peer_index].header # defaultInitValue
/\ command' = [command EXCEPT ![self] = channels[self][remote_peer_index].header.command_name]
/\ IF command'[self] = "addr"
THEN /\ /\ local_peer_id_a' = [local_peer_id_a EXCEPT ![self] = self]
/\ remote_peer_id_a' = [remote_peer_id_a EXCEPT ![self] = remote_peer_index]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "addr",
pc |-> "Listening",
local_peer_id_a |-> local_peer_id_a[self],
remote_peer_id_a |-> remote_peer_id_a[self] ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "SendVersionMsg"]
/\ UNCHANGED << local_peer_id_v,
remote_peer_id_v,
local_peer_id_ve,
remote_peer_id_ve,
local_peer_id_g,
remote_peer_id_g,
found_blocks, hash_count,
block_header_hashes,
remote_peer_blocks,
start_height, end_height,
local_peer_id_i,
remote_peer_id_i,
local_peer_id,
remote_peer_id, blocks_data >>
ELSE /\ IF command'[self] = "version"
THEN /\ /\ local_peer_id_v' = [local_peer_id_v EXCEPT ![self] = self]
/\ remote_peer_id_v' = [remote_peer_id_v EXCEPT ![self] = remote_peer_index]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "version",
pc |-> "Listening",
local_peer_id_v |-> local_peer_id_v[self],
remote_peer_id_v |-> remote_peer_id_v[self] ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "HandleVersionMsg"]
/\ UNCHANGED << local_peer_id_ve,
remote_peer_id_ve,
local_peer_id_g,
remote_peer_id_g,
found_blocks,
hash_count,
block_header_hashes,
remote_peer_blocks,
start_height,
end_height,
local_peer_id_i,
remote_peer_id_i,
local_peer_id,
remote_peer_id,
blocks_data >>
ELSE /\ IF command'[self] = "verack"
THEN /\ /\ local_peer_id_ve' = [local_peer_id_ve EXCEPT ![self] = self]
/\ remote_peer_id_ve' = [remote_peer_id_ve EXCEPT ![self] = remote_peer_index]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "verack",
pc |-> "ListenerLoop",
local_peer_id_ve |-> local_peer_id_ve[self],
remote_peer_id_ve |-> remote_peer_id_ve[self] ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "HandleVerackMsg"]
/\ UNCHANGED << local_peer_id_g,
remote_peer_id_g,
found_blocks,
hash_count,
block_header_hashes,
remote_peer_blocks,
start_height,
end_height,
local_peer_id_i,
remote_peer_id_i,
local_peer_id,
remote_peer_id,
blocks_data >>
ELSE /\ IF command'[self] = "getblocks"
THEN /\ /\ local_peer_id_g' = [local_peer_id_g EXCEPT ![self] = self]
/\ remote_peer_id_g' = [remote_peer_id_g EXCEPT ![self] = remote_peer_index]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "getblocks",
pc |-> "Listening",
found_blocks |-> found_blocks[self],
hash_count |-> hash_count[self],
block_header_hashes |-> block_header_hashes[self],
remote_peer_blocks |-> remote_peer_blocks[self],
start_height |-> start_height[self],
end_height |-> end_height[self],
local_peer_id_g |-> local_peer_id_g[self],
remote_peer_id_g |-> remote_peer_id_g[self] ] >>
\o stack[self]]
/\ found_blocks' = [found_blocks EXCEPT ![self] = defaultInitValue]
/\ hash_count' = [hash_count EXCEPT ![self] = defaultInitValue]
/\ block_header_hashes' = [block_header_hashes EXCEPT ![self] = defaultInitValue]
/\ remote_peer_blocks' = [remote_peer_blocks EXCEPT ![self] = defaultInitValue]
/\ start_height' = [start_height EXCEPT ![self] = defaultInitValue]
/\ end_height' = [end_height EXCEPT ![self] = defaultInitValue]
/\ pc' = [pc EXCEPT ![self] = "HandleGetBlocksMsg"]
/\ UNCHANGED << local_peer_id_i,
remote_peer_id_i,
local_peer_id,
remote_peer_id,
blocks_data >>
ELSE /\ IF command'[self] = "inv"
THEN /\ /\ local_peer_id_i' = [local_peer_id_i EXCEPT ![self] = self]
/\ remote_peer_id_i' = [remote_peer_id_i EXCEPT ![self] = remote_peer_index]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "inv",
pc |-> "Listening",
local_peer_id_i |-> local_peer_id_i[self],
remote_peer_id_i |-> remote_peer_id_i[self] ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "SendGetDataMsg"]
/\ UNCHANGED << local_peer_id,
remote_peer_id,
blocks_data >>
ELSE /\ IF command'[self] = "getdata"
THEN /\ /\ local_peer_id' = [local_peer_id EXCEPT ![self] = self]
/\ remote_peer_id' = [remote_peer_id EXCEPT ![self] = remote_peer_index]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "getdata",
pc |-> "ListenerLoop",
blocks_data |-> blocks_data[self],
local_peer_id |-> local_peer_id[self],
remote_peer_id |-> remote_peer_id[self] ] >>