-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathForceMove.tla
581 lines (515 loc) · 33.8 KB
/
ForceMove.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
----------------------------- MODULE ForceMove -----------------------------
EXTENDS Integers, TLC, Utils
CONSTANTS
StartingTurnNumber,
NumParticipants,
MaxActions,
CountActions,
EveRefutes,
EveCheckpoints,
ForceMoveOverwrites,
AliceRefutes,
NULL
(***************************************************************************)
(* The purpose of this specification is to outline an algorithm that *)
(* guarantees that a challenge is registered on chain with turnNumber *)
(* equal to LatestTurnNumber. It is guaranteed even with an antagonist *)
(* who can do anything (including front-run Alice an arbitrary number of *)
(* times) except *)
(* - signing data with Alice's private key *)
(* - corrupting the blockchain *)
(* *)
(* This guarantee has a key assumption, namely: *)
(* 1. When a challenge is recorded on the adjudicator, Alice is *)
(* always able to *)
(* a) notice the event *)
(* b) submit a transaction *)
(* c) receive confirmation that that transaction was mined *)
(* all before the challenge times out. *)
(* *)
(* If guarantee is met, then either *)
(* A. the channel concludes at this state; or *)
(* B. someone responds with a move that progresses the channel *)
(* C. someone checkpoints with a move that progresses the *)
(* channel *)
(* *)
(* Alice must accept A. She must also accept C -- indeed, she must accept *)
(* any supported state that is recorded on chain, since she must have *)
(* signed at least one "recent" state in its support, and has no control *)
(* over what the other participants does after that state. She would be *)
(* most satisfied with B. *)
(* *)
(* In reality, it is possible that Alice receives a state with turnNumber *)
(* LatestTurnNumber+1, and in this case Alice could (gracefully) abort her *)
(* algorithm and continue the channel. A future version of this *)
(* specification could consider this possibility. *)
(* *)
(* By inductively applying her algorithm, Alice can therefore guarantee *)
(* that either the channel progresses as long as she wishes, or it *)
(* concludes on the latest state that she has. *)
(***************************************************************************)
ASSUME
/\ StartingTurnNumber \in Nat
/\ /\ NumParticipants \in Nat
/\ NumParticipants > 1
(* --algorithm forceMove
(***************************************************************************)
(* Alice calls adjudicator functions by submitting a pending transaction *)
(* with the function type and arguments. The TransactionProcessor *)
(* processes this transaction and modifies the adjudicator state on her *)
(* behalf. However, when Eve calls functions, she directly modifies the *)
(* adjudicator state. This emulates a reality where Eve can consistently *)
(* front-run Alice's transactions, when desired. *)
(***************************************************************************)
variables
adjudicator = [turnNumber |-> 0, mode |-> ChannelMode.OPEN ],
TransactionPool = NULL,
Alice \in ParticipantIDXs \ { ParticipantIDX(LatestTurnNumber + 1) },
alicesActionCount = 0
\* We can't specify any properties that require any memory of the
\* behaviour up to the certain point (ie. the behaviour has passed through state X seven times in a row)
\* we thus have to embed the "memory" of the behaviour in the state itself,
\* if we want to check some property the depends on the history of the behaviour
define
Number == Nat \cup { 0 }
LatestTurnNumber == StartingTurnNumber + NumParticipants - 1
ParticipantIDXs == 1..NumParticipants
ParticipantIDX(turnNumber) == 1 + ((turnNumber - 1) % NumParticipants)
Signer(state) == ParticipantIDX(state.turnNumber)
KnownTurnNumbers == 0..(StartingTurnNumber + NumParticipants)
ValidStates == [ turnNumber: Nat ]
AlicesStates == { c \in ValidStates :
/\ c.turnNumber \in KnownTurnNumbers
}
StoredStates == { c \in AlicesStates : c.turnNumber >= StartingTurnNumber }
AlicesNextTurnNumber == CHOOSE n \in (LatestTurnNumber+1)..(LatestTurnNumber+NumParticipants) : ParticipantIDX(n) = Alice
TargetTurnNumbers == (LatestTurnNumber + 1)..(AlicesNextTurnNumber - 1)
\* The spec makes an assumption about what supported states Eve has:
\* Since Eve cannot forge Alice's signature, Eve cannot have a supported state with turn number
\* greater than or equal to AlicesNextTurnNumber
EvesSupportedStates == { c \in ValidStates : c.turnNumber < AlicesNextTurnNumber}
EvesStates == EvesSupportedStates \union { c \in ValidStates : ParticipantIDX(c.turnNumber) # Alice }
challengeOngoing == adjudicator.mode = ChannelMode.CHALLENGE
channelOpen == adjudicator.mode = ChannelMode.OPEN
increasesTurnNumber(state) == state.turnNumber > adjudicator.turnNumber
validState(c) == c \in ValidStates
validTransition(c) ==
/\ challengeOngoing
/\ c.turnNumber = adjudicator.turnNumber + 1
AlicesGoalMet == adjudicator.turnNumber \in TargetTurnNumbers
end define;
macro validateState(c, type)
begin
if ~validState(c) then
print(<<type, c>>);
assert FALSE;
end if;
end macro;
macro clearChallenge(turnNumber)
begin
assert turnNumber \in Nat;
adjudicator := [
mode |-> ChannelMode.OPEN,
turnNumber |-> turnNumber
];
end macro;
macro respondWithMove(state)
begin
validateState(state, "respond");
if validTransition(state)
then clearChallenge(state.turnNumber);
end if;
end macro;
macro checkpoint(state)
begin
validateState(state, "checkpoint");
if increasesTurnNumber(state)
then clearChallenge(state.turnNumber);
end if;
end macro;
macro forceMove(state)
begin
validateState(state, "forceMove");
if
\/ /\ channelOpen
/\ state.turnNumber >= adjudicator.turnNumber
\/ /\ challengeOngoing
/\ ForceMoveOverwrites
/\ state.turnNumber > adjudicator.turnNumber
then
adjudicator := [ mode |-> ChannelMode.CHALLENGE, turnNumber |-> state.turnNumber ];
end if;
end macro;
macro refute(state)
begin
validateState(state, "refute");
if
/\ challengeOngoing
/\ ParticipantIDX(state.turnNumber) = ParticipantIDX(adjudicator.turnNumber)
/\ state.turnNumber > adjudicator.turnNumber
then clearChallenge(adjudicator.turnNumber)
end if;
end macro;
macro submitTX(transaction)
begin
if TransactionPool # NULL
then
print(<<TransactionPool, transaction>>);
assert FALSE;
end if;
TransactionPool := transaction;
if CountActions then alicesActionCount := alicesActionCount + 1; end if;
end macro;
fair process TransactionProcessor = "TransactionProcessor"
begin
(***************************************************************************)
(* This process records submitted transactions. *)
(***************************************************************************)
TransactionProcessor:
while ~AlicesGoalMet \/ TransactionPool # NULL do
if TransactionPool # NULL then
if TransactionPool.type = ForceMoveAPI.FORCE_MOVE then forceMove(TransactionPool.state);
elsif TransactionPool.type = ForceMoveAPI.RESPOND then respondWithMove(TransactionPool.state);
elsif TransactionPool.type = ForceMoveAPI.REFUTE then refute(TransactionPool.state);
elsif TransactionPool.type = ForceMoveAPI.CHECKPOINT then checkpoint(TransactionPool.state);
else assert FALSE;
end if;
TransactionPool := NULL;
end if;
end while;
end process;
fair process alice = "Alice"
begin
(***************************************************************************)
(* Alice has states (n - numParticipants)..(n-1). She wants to end up *)
(* with states (n - numParticipants + 1)..n. *)
(* *)
(* She is allowed to: *)
(* A. Call submitForceMove with any states that she currently has *)
(* B. Call respondWithMove whenever there's an active challenge where *)
(* it's her turn to move *)
(* C. Call checkpoint at any time. *)
(* D. Call refute at any time. *)
(***************************************************************************)
A:
while ~AlicesGoalMet do
await TransactionPool = NULL;
if challengeOngoing then with turnNumber = adjudicator.turnNumber do
if turnNumber < LatestTurnNumber then
if AliceRefutes then with state = CHOOSE s \in StoredStates :
/\ s.turnNumber > adjudicator.turnNumber
/\ ParticipantIDX(s.turnNumber) = ParticipantIDX(adjudicator.turnNumber)
do submitTX([ type |-> ForceMoveAPI.REFUTE, state |-> state]);
end with;
end if;
end if;
end with; else
submitTX([state |-> [turnNumber |-> LatestTurnNumber ], type |-> ForceMoveAPI.FORCE_MOVE]);
end if;
end while;
end process;
fair process eve = "Eve"
begin
(***************************************************************************)
(* Eve can do almost anything. She can sign any data with any private *)
(* key, except she cannot sign a state with Alice's private key when the *)
(* turn number is greater than or equal to StartingTurnNumber *)
(* *)
(* She can front-run any transaction an arbitrary number of times: if *)
(* Alice else calls an adjudicator function by submitting a transaction, *)
(* Eve can then instantly mine a transaction before Alice's is mined *)
(***************************************************************************)
E:
while ~AlicesGoalMet do
either
\* TODO: challenge with more states than this
with state \in EvesSupportedStates
do forceMove(state);
end with;
or if challengeOngoing
then either
with state \in EvesSupportedStates do respondWithMove(state); end with;
or if EveCheckpoints then with state \in EvesSupportedStates do checkpoint(state); end with; end if;
or if EveRefutes then with state \in EvesStates do refute(state); end with; end if;
end either;
end if; end either;
end while;
end process;
end algorithm;
*)
\* BEGIN TRANSLATION - the hash of the PCal code: PCal-7553a0e9503658653aa4bda6917162f2
\* Label TransactionProcessor of process TransactionProcessor at line 192 col 1 changed to TransactionProcessor_
VARIABLES adjudicator, TransactionPool, Alice, alicesActionCount, pc
(* define statement *)
Number == Nat \cup { 0 }
LatestTurnNumber == StartingTurnNumber + NumParticipants - 1
ParticipantIDXs == 1..NumParticipants
ParticipantIDX(turnNumber) == 1 + ((turnNumber - 1) % NumParticipants)
Signer(state) == ParticipantIDX(state.turnNumber)
KnownTurnNumbers == 0..(StartingTurnNumber + NumParticipants)
ValidStates == [ turnNumber: Nat ]
AlicesStates == { c \in ValidStates :
/\ c.turnNumber \in KnownTurnNumbers
}
StoredStates == { c \in AlicesStates : c.turnNumber >= StartingTurnNumber }
AlicesNextTurnNumber == CHOOSE n \in (LatestTurnNumber+1)..(LatestTurnNumber+NumParticipants) : ParticipantIDX(n) = Alice
TargetTurnNumbers == (LatestTurnNumber + 1)..(AlicesNextTurnNumber - 1)
EvesSupportedStates == { c \in ValidStates : c.turnNumber < AlicesNextTurnNumber}
EvesStates == EvesSupportedStates \union { c \in ValidStates : ParticipantIDX(c.turnNumber) # Alice }
challengeOngoing == adjudicator.mode = ChannelMode.CHALLENGE
channelOpen == adjudicator.mode = ChannelMode.OPEN
increasesTurnNumber(state) == state.turnNumber > adjudicator.turnNumber
validState(c) == c \in ValidStates
validTransition(c) ==
/\ challengeOngoing
/\ c.turnNumber = adjudicator.turnNumber + 1
AlicesGoalMet == adjudicator.turnNumber \in TargetTurnNumbers
vars == << adjudicator, TransactionPool, Alice, alicesActionCount, pc >>
ProcSet == {"TransactionProcessor"} \cup {"Alice"} \cup {"Eve"}
Init == (* Global variables *)
/\ adjudicator = [turnNumber |-> 0, mode |-> ChannelMode.OPEN ]
/\ TransactionPool = NULL
/\ Alice \in ParticipantIDXs \ { ParticipantIDX(LatestTurnNumber + 1) }
/\ alicesActionCount = 0
/\ pc = [self \in ProcSet |-> CASE self = "TransactionProcessor" -> "TransactionProcessor_"
[] self = "Alice" -> "A"
[] self = "Eve" -> "E"]
TransactionProcessor_ == /\ pc["TransactionProcessor"] = "TransactionProcessor_"
/\ IF ~AlicesGoalMet \/ TransactionPool # NULL
THEN /\ IF TransactionPool # NULL
THEN /\ IF TransactionPool.type = ForceMoveAPI.FORCE_MOVE
THEN /\ IF ~validState((TransactionPool.state))
THEN /\ PrintT((<<"forceMove", (TransactionPool.state)>>))
/\ Assert(FALSE,
"Failure of assertion at line 120, column 5 of macro called at line 194, column 66.")
ELSE /\ TRUE
/\ IF \/ /\ channelOpen
/\ (TransactionPool.state).turnNumber >= adjudicator.turnNumber
\/ /\ challengeOngoing
/\ ForceMoveOverwrites
/\ (TransactionPool.state).turnNumber > adjudicator.turnNumber
THEN /\ adjudicator' = [ mode |-> ChannelMode.CHALLENGE, turnNumber |-> (TransactionPool.state).turnNumber ]
ELSE /\ TRUE
/\ UNCHANGED adjudicator
ELSE /\ IF TransactionPool.type = ForceMoveAPI.RESPOND
THEN /\ IF ~validState((TransactionPool.state))
THEN /\ PrintT((<<"respond", (TransactionPool.state)>>))
/\ Assert(FALSE,
"Failure of assertion at line 120, column 5 of macro called at line 195, column 66.")
ELSE /\ TRUE
/\ IF validTransition((TransactionPool.state))
THEN /\ Assert(((TransactionPool.state).turnNumber) \in Nat,
"Failure of assertion at line 126, column 1 of macro called at line 195, column 66.")
/\ adjudicator' = [
mode |-> ChannelMode.OPEN,
turnNumber |-> ((TransactionPool.state).turnNumber)
]
ELSE /\ TRUE
/\ UNCHANGED adjudicator
ELSE /\ IF TransactionPool.type = ForceMoveAPI.REFUTE
THEN /\ IF ~validState((TransactionPool.state))
THEN /\ PrintT((<<"refute", (TransactionPool.state)>>))
/\ Assert(FALSE,
"Failure of assertion at line 120, column 5 of macro called at line 196, column 66.")
ELSE /\ TRUE
/\ IF /\ challengeOngoing
/\ ParticipantIDX((TransactionPool.state).turnNumber) = ParticipantIDX(adjudicator.turnNumber)
/\ (TransactionPool.state).turnNumber > adjudicator.turnNumber
THEN /\ Assert((adjudicator.turnNumber) \in Nat,
"Failure of assertion at line 126, column 1 of macro called at line 196, column 66.")
/\ adjudicator' = [
mode |-> ChannelMode.OPEN,
turnNumber |-> (adjudicator.turnNumber)
]
ELSE /\ TRUE
/\ UNCHANGED adjudicator
ELSE /\ IF TransactionPool.type = ForceMoveAPI.CHECKPOINT
THEN /\ IF ~validState((TransactionPool.state))
THEN /\ PrintT((<<"checkpoint", (TransactionPool.state)>>))
/\ Assert(FALSE,
"Failure of assertion at line 120, column 5 of macro called at line 197, column 66.")
ELSE /\ TRUE
/\ IF increasesTurnNumber((TransactionPool.state))
THEN /\ Assert(((TransactionPool.state).turnNumber) \in Nat,
"Failure of assertion at line 126, column 1 of macro called at line 197, column 66.")
/\ adjudicator' = [
mode |-> ChannelMode.OPEN,
turnNumber |-> ((TransactionPool.state).turnNumber)
]
ELSE /\ TRUE
/\ UNCHANGED adjudicator
ELSE /\ Assert(FALSE,
"Failure of assertion at line 198, column 14.")
/\ UNCHANGED adjudicator
/\ TransactionPool' = NULL
ELSE /\ TRUE
/\ UNCHANGED << adjudicator,
TransactionPool >>
/\ pc' = [pc EXCEPT !["TransactionProcessor"] = "TransactionProcessor_"]
ELSE /\ pc' = [pc EXCEPT !["TransactionProcessor"] = "Done"]
/\ UNCHANGED << adjudicator,
TransactionPool >>
/\ UNCHANGED << Alice, alicesActionCount >>
TransactionProcessor == TransactionProcessor_
A == /\ pc["Alice"] = "A"
/\ IF ~AlicesGoalMet
THEN /\ TransactionPool = NULL
/\ IF challengeOngoing
THEN /\ LET turnNumber == adjudicator.turnNumber IN
IF turnNumber < LatestTurnNumber
THEN /\ IF AliceRefutes
THEN /\ LET state == CHOOSE s \in StoredStates :
/\ s.turnNumber > adjudicator.turnNumber
/\ ParticipantIDX(s.turnNumber) = ParticipantIDX(adjudicator.turnNumber) IN
/\ IF TransactionPool # NULL
THEN /\ PrintT((<<TransactionPool, ([ type |-> ForceMoveAPI.REFUTE, state |-> state])>>))
/\ Assert(FALSE,
"Failure of assertion at line 180, column 5 of macro called at line 226, column 17.")
ELSE /\ TRUE
/\ TransactionPool' = [ type |-> ForceMoveAPI.REFUTE, state |-> state]
/\ IF CountActions
THEN /\ alicesActionCount' = alicesActionCount + 1
ELSE /\ TRUE
/\ UNCHANGED alicesActionCount
ELSE /\ TRUE
/\ UNCHANGED << TransactionPool,
alicesActionCount >>
ELSE /\ TRUE
/\ UNCHANGED << TransactionPool,
alicesActionCount >>
ELSE /\ IF TransactionPool # NULL
THEN /\ PrintT((<<TransactionPool, ([state |-> [turnNumber |-> LatestTurnNumber ], type |-> ForceMoveAPI.FORCE_MOVE])>>))
/\ Assert(FALSE,
"Failure of assertion at line 180, column 5 of macro called at line 231, column 9.")
ELSE /\ TRUE
/\ TransactionPool' = [state |-> [turnNumber |-> LatestTurnNumber ], type |-> ForceMoveAPI.FORCE_MOVE]
/\ IF CountActions
THEN /\ alicesActionCount' = alicesActionCount + 1
ELSE /\ TRUE
/\ UNCHANGED alicesActionCount
/\ pc' = [pc EXCEPT !["Alice"] = "A"]
ELSE /\ pc' = [pc EXCEPT !["Alice"] = "Done"]
/\ UNCHANGED << TransactionPool, alicesActionCount >>
/\ UNCHANGED << adjudicator, Alice >>
alice == A
E == /\ pc["Eve"] = "E"
/\ IF ~AlicesGoalMet
THEN /\ \/ /\ \E state \in EvesSupportedStates:
/\ IF ~validState(state)
THEN /\ PrintT((<<"forceMove", state>>))
/\ Assert(FALSE,
"Failure of assertion at line 120, column 5 of macro called at line 252, column 12.")
ELSE /\ TRUE
/\ IF \/ /\ channelOpen
/\ state.turnNumber >= adjudicator.turnNumber
\/ /\ challengeOngoing
/\ ForceMoveOverwrites
/\ state.turnNumber > adjudicator.turnNumber
THEN /\ adjudicator' = [ mode |-> ChannelMode.CHALLENGE, turnNumber |-> state.turnNumber ]
ELSE /\ TRUE
/\ UNCHANGED adjudicator
\/ /\ IF challengeOngoing
THEN /\ \/ /\ \E state \in EvesSupportedStates:
/\ IF ~validState(state)
THEN /\ PrintT((<<"respond", state>>))
/\ Assert(FALSE,
"Failure of assertion at line 120, column 5 of macro called at line 256, column 47.")
ELSE /\ TRUE
/\ IF validTransition(state)
THEN /\ Assert((state.turnNumber) \in Nat,
"Failure of assertion at line 126, column 1 of macro called at line 256, column 47.")
/\ adjudicator' = [
mode |-> ChannelMode.OPEN,
turnNumber |-> (state.turnNumber)
]
ELSE /\ TRUE
/\ UNCHANGED adjudicator
\/ /\ IF EveCheckpoints
THEN /\ \E state \in EvesSupportedStates:
/\ IF ~validState(state)
THEN /\ PrintT((<<"checkpoint", state>>))
/\ Assert(FALSE,
"Failure of assertion at line 120, column 5 of macro called at line 257, column 73.")
ELSE /\ TRUE
/\ IF increasesTurnNumber(state)
THEN /\ Assert((state.turnNumber) \in Nat,
"Failure of assertion at line 126, column 1 of macro called at line 257, column 73.")
/\ adjudicator' = [
mode |-> ChannelMode.OPEN,
turnNumber |-> (state.turnNumber)
]
ELSE /\ TRUE
/\ UNCHANGED adjudicator
ELSE /\ TRUE
/\ UNCHANGED adjudicator
\/ /\ IF EveRefutes
THEN /\ \E state \in EvesStates:
/\ IF ~validState(state)
THEN /\ PrintT((<<"refute", state>>))
/\ Assert(FALSE,
"Failure of assertion at line 120, column 5 of macro called at line 258, column 60.")
ELSE /\ TRUE
/\ IF /\ challengeOngoing
/\ ParticipantIDX(state.turnNumber) = ParticipantIDX(adjudicator.turnNumber)
/\ state.turnNumber > adjudicator.turnNumber
THEN /\ Assert((adjudicator.turnNumber) \in Nat,
"Failure of assertion at line 126, column 1 of macro called at line 258, column 60.")
/\ adjudicator' = [
mode |-> ChannelMode.OPEN,
turnNumber |-> (adjudicator.turnNumber)
]
ELSE /\ TRUE
/\ UNCHANGED adjudicator
ELSE /\ TRUE
/\ UNCHANGED adjudicator
ELSE /\ TRUE
/\ UNCHANGED adjudicator
/\ pc' = [pc EXCEPT !["Eve"] = "E"]
ELSE /\ pc' = [pc EXCEPT !["Eve"] = "Done"]
/\ UNCHANGED adjudicator
/\ UNCHANGED << TransactionPool, Alice, alicesActionCount >>
eve == E
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == TransactionProcessor \/ alice \/ eve
\/ Terminating
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(TransactionProcessor)
/\ WF_vars(alice)
/\ WF_vars(eve)
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-909bec0176088e127165e58e0167acee
AllowedTransactions == [ type: Range(ForceMoveAPI), state: ValidStates ]
AllowedChannels == [ mode: Range(ChannelMode), turnNumber: Number ]
\* Safety & liveness properties
TypeOK ==
/\ adjudicator \in AllowedChannels
/\ \/ TransactionPool \in AllowedTransactions
\/ TransactionPool = NULL
AliceCanProgressChannel == <>[](adjudicator.turnNumber \in TargetTurnNumbers)
\* We can verify that Alice can never directly modify the adjudicator with this property, with
\* the exception that she can finalize the channel.
AliceMustSubmitTransactions == [][
/\ TransactionPool = NULL
/\ TransactionPool' # NULL
=> UNCHANGED adjudicator
]_<<TransactionPool, adjudicator>>
TurnNumberIncrements == [][
adjudicator'.turnNumber >= adjudicator.turnNumber
]_<<adjudicator>>
\* Alice should be able to accomplish her goal by submitting a single transaction.
AliceCannotBeGriefed == alicesActionCount <= MaxActions
\* Eve front runs if she changes the adjudicator after Alice submitted a transaction, but before
\* the transaction is processed
\* Violations of this property are therefore _examples_ of Eve's ability to front-run
\* Alice's transactions
EveDoesntFrontRun == [][~(
/\ TransactionPool # NULL \* transaction has been submitted
/\ TransactionPool' = TransactionPool \* transaction is not processed
/\ adjudicator' # adjudicator \* adjudicator is changed
)]_<<TransactionPool, adjudicator>>
=============================================================================
\* Modification History
\* Last modified Fri Jun 12 08:38:05 MDT 2020 by andrewstewart
\* Created Tue Aug 06 14:38:11 MDT 2019 by andrewstewart