mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-04-23 01:00:31 +00:00
Code Issues Packages Projects Releases Wiki Activity

Revert "Migration of TLA+ files from the spec repo (#8004)" (#8016)

Browse Source 
This reverts commit e762dbb603.

These files need a more thorough review before integration.
This commit is contained in:
M. J. Fromberger
2022-02-25 16:37:31 -08:00
committed by GitHub
parent f25b7ceeb2
commit b848c79971
4 changed files with 220 additions and 511 deletions
Download Patch File Download Diff File Expand all files Collapse all files

109
spec/consensus/proposer-based-timestamp/tla/Apalache.tla
View File

@@ -1,109 +0,0 @@
--------------------------- MODULE Apalache -----------------------------------
(*
* This is a standard module for use with the Apalache model checker.
* The meaning of the operators is explained in the comments.
* Many of the operators serve as additional annotations of their arguments.
* As we like to preserve compatibility with TLC and TLAPS, we define the
* operator bodies by erasure. The actual interpretation of the operators is
* encoded inside Apalache. For the moment, these operators are mirrored in
* the class at.forsyte.apalache.tla.lir.oper.ApalacheOper.
*
* Igor Konnov, Jure Kukovec, Informal Systems 2020-2021
*)
(**
* An assignment of an expression e to a state variable x. Typically, one
* uses the non-primed version of x in the initializing predicate Init and
* the primed version of x (that is, x') in the transition predicate Next.
* Although TLA+ does not have a concept of a variable assignment, we find
* this concept extremely useful for symbolic model checking. In pure TLA+,
* one would simply write x = e, or x \in {e}.
*
* Apalache automatically converts some expressions of the form
* x = e or x \in {e} into assignments. However, if you like to annotate
* assignments by hand, you can use this operator.
*
* For a further discussion on that matter, see:
* https://github.com/informalsystems/apalache/blob/ik/idiomatic-tla/docs/idiomatic/assignments.md
*)
x := e == x = e
(**
* A generator of a data structure. Given a positive integer `bound`, and
* assuming that the type of the operator application is known, we
* recursively generate a TLA+ data structure as a tree, whose width is
* bound by the number `bound`.
*
* The body of this operator is redefined by Apalache.
*)
Gen(size) == {}
(**
* Convert a set of pairs S to a function F. Note that if S contains at least
* two pairs <<x, y>> and <<u, v>> such that x = u and y /= v,
* then F is not uniquely defined. We use CHOOSE to resolve this ambiguity.
* Apalache implements a more efficient encoding of this operator
* than the default one.
*
* @type: Set(<<a, b>>) => (a -> b);
*)
SetAsFun(S) ==
LET Dom == { x: <<x, y>> \in S }
Rng == { y: <<x, y>> \in S }
IN
[ x \in Dom |-> CHOOSE y \in Rng: <<x, y>> \in S ]
(**
* As TLA+ is untyped, one can use function- and sequence-specific operators
* interchangeably. However, to maintain correctness w.r.t. our type-system,
* an explicit cast is needed when using functions as sequences.
*)
LOCAL INSTANCE Sequences
FunAsSeq(fn, maxSeqLen) == SubSeq(fn, 1, maxSeqLen)
(**
* Annotating an expression \E x \in S: P as Skolemizable. That is, it can
* be replaced with an expression c \in S /\ P(c) for a fresh constant c.
* Not every exisential can be replaced with a constant, this should be done
* with care. Apalache detects Skolemizable expressions by static analysis.
*)
Skolem(e) == e
(**
* A hint to the model checker to expand a set S, instead of dealing
* with it symbolically. Apalache finds out which sets have to be expanded
* by static analysis.
*)
Expand(S) == S
(**
* A hint to the model checker to replace its argument Cardinality(S) >= k
* with a series of existential quantifiers for a constant k.
* Similar to Skolem, this has to be done carefully. Apalache automatically
* places this hint by static analysis.
*)
ConstCardinality(cardExpr) == cardExpr
(**
* The folding operator, used to implement computation over a set.
* Apalache implements a more efficient encoding than the one below.
* (from the community modules).
*)
RECURSIVE FoldSet(_,_,_)
FoldSet( Op(_,_), v, S ) == IF S = {}
THEN v
ELSE LET w == CHOOSE x \in S: TRUE
IN LET T == S \ {w}
IN FoldSet( Op, Op(v,w), T )
(**
* The folding operator, used to implement computation over a sequence.
* Apalache implements a more efficient encoding than the one below.
* (from the community modules).
*)
RECURSIVE FoldSeq(_,_,_)
FoldSeq( Op(_,_), v, seq ) == IF seq = <<>>
THEN v
ELSE FoldSeq( Op, Op(v,Head(seq)), Tail(seq) )
===============================================================================

77
spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla
View File

@@ -1,77 +0,0 @@
----------------------------- MODULE MC_PBT -------------------------------
CONSTANT
\* @type: ROUND -> PROCESS;
Proposer
VARIABLES
\* @type: PROCESS -> ROUND;
round, \* a process round number
\* @type: PROCESS -> STEP;
step, \* a process step
\* @type: PROCESS -> DECISION;
decision, \* process decision
\* @type: PROCESS -> VALUE;
lockedValue, \* a locked value
\* @type: PROCESS -> ROUND;
lockedRound, \* a locked round
\* @type: PROCESS -> PROPOSAL;
validValue, \* a valid value
\* @type: PROCESS -> ROUND;
validRound \* a valid round
\* time-related variables
VARIABLES
\* @type: PROCESS -> TIME;
localClock, \* a process local clock: Corr -> Ticks
\* @type: TIME;
realTime \* a reference Newtonian real time
\* book-keeping variables
VARIABLES
\* @type: ROUND -> Set(PROPMESSAGE);
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
\* @type: Set(MESSAGE);
evidence, \* the messages that were used by the correct processes to make transitions
\* @type: ACTION;
action, \* we use this variable to see which action was taken
\* @type: PROCESS -> Set(PROPMESSAGE);
receivedTimelyProposal, \* used to keep track when a process receives a timely VALUE message
\* @type: <<ROUND,PROCESS>> -> TIME;
inspectedProposal \* used to keep track when a process tries to receive a message
\* Invariant support
VARIABLES
\* @type: ROUND -> TIME;
beginRound, \* the minimum of the local clocks at the time any process entered a new round
\* @type: PROCESS -> TIME;
endConsensus, \* the local time when a decision is made
\* @type: ROUND -> TIME;
lastBeginRound, \* the maximum of the local clocks in each round
\* @type: ROUND -> TIME;
proposalTime, \* the real time when a proposer proposes in a round
\* @type: ROUND -> TIME;
proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round
INSTANCE TendermintPBT_002_draft WITH
Corr <- {"c1", "c2"},
Faulty <- {"f3", "f4"},
N <- 4,
T <- 1,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 5,
MaxTimestamp <- 10,
MinTimestamp <- 2,
Delay <- 2,
Precision <- 2
\* run Apalache with --cinit=CInit
CInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]
=============================================================================

540
spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla
View File

@@ -5,11 +5,10 @@
the Tendermint TLA+ specification for fork accountability:
https://github.com/tendermint/spec/blob/master/spec/light-client/accountability/TendermintAcc_004_draft.tla
* Version 2. A preliminary specification.
* Version 1. A preliminary specification.
Zarko Milosevic, Igor Konnov, Informal Systems, 2019-2020.
Ilina Stoilkovska, Josef Widder, Informal Systems, 2021.
Jure Kukovec, Informal Systems, 2022.
*)
EXTENDS Integers, FiniteSets, Apalache, typedefs
@@ -39,11 +38,13 @@ CONSTANTS
\* @type: TIME;
MaxTimestamp, \* the maximal value of the clock tick
\* @type: TIME;
MinTimestamp, \* the minimal value of the clock tick
\* @type: TIME;
Delay, \* message delay
\* @type: TIME;
Precision \* clock precision: the maximal difference between two local clocks
Precision, \* clock precision: the maximal difference between two local clocks
\* @type: TIME;
Accuracy, \* clock accuracy: the maximal difference between a local clock and the real time
\* @type: Bool;
ClockDrift \* is there clock drift between the local clocks and the global clock
ASSUME(N = Cardinality(Corr \union Faulty))
@@ -65,39 +66,24 @@ Values == ValidValues \union InvalidValues \* the set of all values
\* @type: VALUE;
NilValue == "None" \* a special value for a nil round, outside of Values
\* @type: Set(PROPOSAL);
Proposals == Values \X Timestamps \X Rounds
Proposals == Values \X Timestamps
\* @type: PROPOSAL;
NilProposal == <<NilValue, NilTimestamp, NilRound>>
NilProposal == <<NilValue, NilTimestamp>>
\* @type: Set(VALUE);
ValuesOrNil == Values \union {NilValue}
\* @type: Set(DECISION);
Decisions == Proposals \X Rounds
Decisions == Values \X Timestamps \X Rounds
\* @type: DECISION;
NilDecision == <<NilProposal, NilRound>>
NilDecision == <<NilValue, NilTimestamp, NilRound>>
ValidProposals == ValidValues \X (MinTimestamp..MaxTimestamp) \X Rounds
\* a value hash is modeled as identity
\* @type: (t) => t;
Id(v) == v
\* The validity predicate
\* @type: (PROPOSAL) => Bool;
IsValid(p) == p \in ValidProposals
\* Time validity check. If we want MaxTimestamp = \infty, set ValidTime(t) == TRUE
ValidTime(t) == t < MaxTimestamp
\* @type: (PROPMESSAGE) => VALUE;
MessageValue(msg) == msg.proposal[1]
\* @type: (PROPMESSAGE) => TIME;
MessageTime(msg) == msg.proposal[2]
\* @type: (PROPMESSAGE) => ROUND;
MessageRound(msg) == msg.proposal[3]
\* @type: (TIME, TIME) => Bool;
IsTimely(processTime, messageTime) ==
/\ processTime >= messageTime - Precision
/\ processTime <= messageTime + Precision + Delay
\* @type: (VALUE) => Bool;
IsValid(v) == v \in ValidValues
\* the two thresholds that are used in the algorithm
\* @type: Int;
@@ -105,24 +91,23 @@ THRESHOLD1 == T + 1 \* at least one process is not faulty
\* @type: Int;
THRESHOLD2 == 2 * T + 1 \* a quorum when having N > 3 * T
\* @type: (TIME, TIME) => TIME;
Min2(a,b) == IF a <= b THEN a ELSE b
\* @type: (Set(TIME)) => TIME;
Min(S) == FoldSet( Min2, MaxTimestamp, S )
\* Min(S) == CHOOSE x \in S : \A y \in S : x <= y
Min(S) == CHOOSE x \in S : \A y \in S : x <= y
\* @type: (TIME, TIME) => TIME;
Max2(a,b) == IF a >= b THEN a ELSE b
\* @type: (Set(TIME)) => TIME;
Max(S) == FoldSet( Max2, NilTimestamp, S )
\* Max(S) == CHOOSE x \in S : \A y \in S : y <= x
Max(S) == CHOOSE x \in S : \A y \in S : y <= x
\* @type: (Set(MESSAGE)) => Int;
Card(S) ==
LET
\* @type: (Int, MESSAGE) => Int;
PlusOne(i, m) == i + 1
IN FoldSet( PlusOne, 0, S )
(********************* TYPE ANNOTATIONS FOR APALACHE **************************)
\* a type annotation for an empty set of messages
\* @type: Set(MESSAGE);
EmptyMsgSet == {}
\* @type: Set(RCVPROP);
EmptyRcvProp == {}
\* @type: Set(PROCESS);
EmptyProcSet == {}
(********************* PROTOCOL STATE VARIABLES ******************************)
VARIABLES
@@ -136,15 +121,11 @@ VARIABLES
lockedValue, \* a locked value
\* @type: PROCESS -> ROUND;
lockedRound, \* a locked round
\* @type: PROCESS -> PROPOSAL;
\* @type: PROCESS -> VALUE;
validValue, \* a valid value
\* @type: PROCESS -> ROUND;
validRound \* a valid round
coreVars ==
<<round, step, decision, lockedValue,
lockedRound, validValue, validRound>>
\* time-related variables
VARIABLES
\* @type: PROCESS -> TIME;
@@ -152,8 +133,6 @@ VARIABLES
\* @type: TIME;
realTime \* a reference Newtonian real time
temporalVars == <<localClock, realTime>>
\* book-keeping variables
VARIABLES
\* @type: ROUND -> Set(PROPMESSAGE);
@@ -166,35 +145,28 @@ VARIABLES
evidence, \* the messages that were used by the correct processes to make transitions
\* @type: ACTION;
action, \* we use this variable to see which action was taken
\* @type: PROCESS -> Set(PROPMESSAGE);
\* @type: Set(RCVPROP);
receivedTimelyProposal, \* used to keep track when a process receives a timely PROPOSAL message
\* @type: <<ROUND,PROCESS>> -> TIME;
inspectedProposal \* used to keep track when a process tries to receive a message
\* Action is excluded from the tuple, because it always changes
bookkeepingVars ==
<<msgsPropose, msgsPrevote, msgsPrecommit,
evidence, (*action,*) receivedTimelyProposal,
inspectedProposal>>
\* Invariant support
VARIABLES
\* @type: ROUND -> TIME;
beginRound, \* the minimum of the local clocks at the time any process entered a new round
\* @type: ROUND -> Set(PROCESS);
inspectedProposal, \* used to keep track when a process tries to receive a message
\* @type: TIME;
beginConsensus, \* the minimum of the local clocks in the initial state
\* @type: PROCESS -> TIME;
endConsensus, \* the local time when a decision is made
\* @type: ROUND -> TIME;
lastBeginRound, \* the maximum of the local clocks in each round
\* @type: TIME;
lastBeginConsensus, \* the maximum of the local clocks in the initial state
\* @type: ROUND -> TIME;
proposalTime, \* the real time when a proposer proposes in a round
\* @type: ROUND -> TIME;
proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round
invariantVars ==
<<beginRound, endConsensus, lastBeginRound,
proposalTime, proposalReceivedTime>>
(* to see a type invariant, check TendermintAccInv3 *)
\* a handy definition used in UNCHANGED
vars == <<round, step, decision, lockedValue, lockedRound,
validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
localClock, realTime, receivedTimelyProposal, inspectedProposal, action,
beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
(********************* PROTOCOL INITIALIZATION ******************************)
\* @type: (ROUND) => Set(PROPMESSAGE);
@@ -283,37 +255,30 @@ BenignRoundsInMessages(msgfun) ==
\* The initial states of the protocol. Some faults can be in the system already.
Init ==
/\ round = [p \in Corr |-> 0]
/\ localClock \in [Corr -> MinTimestamp..(MinTimestamp + Precision)]
/\ \/ /\ ~ClockDrift
/\ localClock \in [Corr -> 0..Accuracy]
\/ /\ ClockDrift
/\ localClock = [p \in Corr |-> 0]
/\ realTime = 0
/\ step = [p \in Corr |-> "PROPOSE"]
/\ decision = [p \in Corr |-> NilDecision]
/\ lockedValue = [p \in Corr |-> NilValue]
/\ lockedRound = [p \in Corr |-> NilRound]
/\ validValue = [p \in Corr |-> NilProposal]
/\ validValue = [p \in Corr |-> NilValue]
/\ validRound = [p \in Corr |-> NilRound]
/\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
/\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
/\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
/\ receivedTimelyProposal = [p \in Corr |-> {}]
/\ inspectedProposal = [r \in Rounds, p \in Corr |-> NilTimestamp]
/\ receivedTimelyProposal = EmptyRcvProp
/\ inspectedProposal = [r \in Rounds |-> EmptyProcSet]
/\ BenignRoundsInMessages(msgsPropose)
/\ BenignRoundsInMessages(msgsPrevote)
/\ BenignRoundsInMessages(msgsPrecommit)
/\ evidence = {}
/\ evidence = EmptyMsgSet
/\ action' = "Init"
/\ beginRound =
[r \in Rounds |->
IF r = 0
THEN Min({localClock[p] : p \in Corr})
ELSE MaxTimestamp
]
/\ beginConsensus = Min({localClock[p] : p \in Corr})
/\ endConsensus = [p \in Corr |-> NilTimestamp]
/\ lastBeginRound =
[r \in Rounds |->
IF r = 0
THEN Max({localClock[p] : p \in Corr})
ELSE NilTimestamp
]
/\ lastBeginConsensus = Max({localClock[p] : p \in Corr})
/\ proposalTime = [r \in Rounds |-> NilTimestamp]
/\ proposalReceivedTime = [r \in Rounds |-> NilTimestamp]
@@ -331,7 +296,7 @@ BroadcastProposal(pSrc, pRound, pProposal, pValidRound) ==
validRound |-> pValidRound
]
IN
/\ msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]
msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]
\* @type: (PROCESS, ROUND, PROPOSAL) => Bool;
BroadcastPrevote(pSrc, pRound, pId) ==
@@ -345,7 +310,7 @@ BroadcastPrevote(pSrc, pRound, pId) ==
id |-> pId
]
IN
/\ msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]
msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]
\* @type: (PROCESS, ROUND, PROPOSAL) => Bool;
BroadcastPrecommit(pSrc, pRound, pId) ==
@@ -359,7 +324,7 @@ BroadcastPrecommit(pSrc, pRound, pId) ==
id |-> pId
]
IN
/\ msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]
msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]
(***************************** TIME **************************************)
@@ -374,14 +339,14 @@ SynchronizedLocalClocks ==
/\ localClock[q] - localClock[p] < Precision
\* [PBTS-PROPOSE.0]
\* @type: (VALUE, TIME, ROUND) => PROPOSAL;
Proposal(v, t, r) ==
<<v, t, r>>
\* @type: (VALUE, TIME) => PROPOSAL;
Proposal(v, t) ==
<<v, t>>
\* [PBTS-DECISION-ROUND.0]
\* @type: (PROPOSAL, ROUND) => DECISION;
Decision(p, r) ==
<<p, r>>
\* @type: (VALUE, TIME, ROUND) => DECISION;
Decision(v, t, r) ==
<<v, t, r>>
(**************** MESSAGE PROCESSING TRANSITIONS *************************)
\* lines 12-13
@@ -389,10 +354,7 @@ Decision(p, r) ==
StartRound(p, r) ==
/\ step[p] /= "DECIDED" \* a decided process does not participate in consensus
/\ round' = [round EXCEPT ![p] = r]
/\ step' = [step EXCEPT ![p] = "PROPOSE"]
\* We only need to update (last)beginRound[r] once a process enters round `r`
/\ beginRound' = [beginRound EXCEPT ![r] = Min2(@, localClock[p])]
/\ lastBeginRound' = [lastBeginRound EXCEPT ![r] = Max2(@, localClock[p])]
/\ step' = [step EXCEPT ![p] = "PROPOSE"]
\* lines 14-19, a proposal may be sent later
\* @type: (PROCESS) => Bool;
@@ -403,22 +365,20 @@ InsertProposal(p) ==
\* if the proposer is sending a proposal, then there are no other proposals
\* by the correct processes for the same round
/\ \A m \in msgsPropose[r]: m.src /= p
\* /\ localClock[p] >
/\ \E v \in ValidValues:
LET proposal ==
IF validValue[p] /= NilProposal
LET value ==
IF validValue[p] /= NilValue
THEN validValue[p]
ELSE Proposal(v, localClock[p], r)
ELSE v
IN LET
proposal == Proposal(value, localClock[p])
IN
/\ BroadcastProposal(p, r, proposal, validRound[p])
/\ BroadcastProposal(p, round[p], proposal, validRound[p])
/\ proposalTime' = [proposalTime EXCEPT ![r] = realTime]
/\ UNCHANGED <<temporalVars, coreVars>>
/\ UNCHANGED
<<(*msgsPropose,*) msgsPrevote, msgsPrecommit,
evidence, receivedTimelyProposal, inspectedProposal>>
/\ UNCHANGED
<<beginRound, endConsensus, lastBeginRound,
(*proposalTime,*) proposalReceivedTime>>
/\ UNCHANGED <<evidence, round, decision, lockedValue, lockedRound,
validValue, step, validRound, msgsPrevote, msgsPrecommit,
localClock, realTime, receivedTimelyProposal, inspectedProposal,
beginConsensus, endConsensus, lastBeginConsensus, proposalReceivedTime>>
/\ action' = "InsertProposal"
\* a new action used to filter messages that are not on time
@@ -434,120 +394,92 @@ ReceiveProposal(p) ==
type |-> "PROPOSAL",
src |-> Proposer[round[p]],
round |-> round[p],
proposal |-> Proposal(v, t, r),
proposal |-> Proposal(v, t),
validRound |-> NilRound
]
IN
/\ msg \in msgsPropose[round[p]]
/\ inspectedProposal[r,p] = NilTimestamp
/\ msg \notin receivedTimelyProposal[p]
/\ inspectedProposal' = [inspectedProposal EXCEPT ![r,p] = localClock[p]]
/\ LET
isTimely == IsTimely(localClock[p], t)
IN
\/ /\ isTimely
/\ receivedTimelyProposal' = [receivedTimelyProposal EXCEPT ![p] = @ \union {msg}]
/\ LET
isNilTimestamp == proposalReceivedTime[r] = NilTimestamp
IN
\/ /\ isNilTimestamp
/\ proposalReceivedTime' = [proposalReceivedTime EXCEPT ![r] = realTime]
\/ /\ ~isNilTimestamp
/\ UNCHANGED proposalReceivedTime
\/ /\ ~isTimely
/\ UNCHANGED <<receivedTimelyProposal, proposalReceivedTime>>
/\ UNCHANGED <<temporalVars, coreVars>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, msgsPrecommit,
evidence(*, receivedTimelyProposal, inspectedProposal*)>>
/\ UNCHANGED
<<beginRound, endConsensus, lastBeginRound,
proposalTime(*, proposalReceivedTime*)>>
/\ p \notin inspectedProposal[r]
/\ <<p, msg>> \notin receivedTimelyProposal
/\ inspectedProposal' = [inspectedProposal EXCEPT ![r] = @ \union {p}]
/\ \/ /\ localClock[p] - Precision < t
/\ t < localClock[p] + Precision + Delay
/\ receivedTimelyProposal' = receivedTimelyProposal \union {<<p, msg>>}
/\ \/ /\ proposalReceivedTime[r] = NilTimestamp
/\ proposalReceivedTime' = [proposalReceivedTime EXCEPT ![r] = realTime]
\/ /\ proposalReceivedTime[r] /= NilTimestamp
/\ UNCHANGED proposalReceivedTime
\/ /\ \/ localClock[p] - Precision >= t
\/ t >= localClock[p] + Precision + Delay
/\ UNCHANGED <<receivedTimelyProposal, proposalReceivedTime>>
/\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
localClock, realTime, beginConsensus, endConsensus, lastBeginConsensus, proposalTime>>
/\ action' = "ReceiveProposal"
\* lines 22-27
\* @type: (PROCESS) => Bool;
UponProposalInPropose(p) ==
\E v \in Values, t \in Timestamps:
LET
r == round[p]
IN LET
\* @type: PROPOSAL;
prop == Proposal(v,t,r)
IN
/\ step[p] = "PROPOSE" (* line 22 *)
/\ LET
\* @type: PROPMESSAGE;
msg ==
[
type |-> "PROPOSAL",
src |-> Proposer[r],
round |-> r,
proposal |-> prop,
src |-> Proposer[round[p]],
round |-> round[p],
proposal |-> Proposal(v, t),
validRound |-> NilRound
]
IN
/\ msg \in receivedTimelyProposal[p] \* updated line 22
/\ <<p, msg>> \in receivedTimelyProposal \* updated line 22
/\ evidence' = {msg} \union evidence
/\ LET mid == (* line 23 *)
IF IsValid(prop) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
THEN Id(prop)
IF IsValid(v) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
THEN Id(Proposal(v, t))
ELSE NilProposal
IN
BroadcastPrevote(p, r, mid) \* lines 24-26
BroadcastPrevote(p, round[p], mid) \* lines 24-26
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED
<<round, (*step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
/\ UNCHANGED <<round, decision, lockedValue, lockedRound,
validValue, validRound, msgsPropose, msgsPrecommit,
localClock, realTime, receivedTimelyProposal, inspectedProposal,
beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
/\ action' = "UponProposalInPropose"
\* lines 28-33
\* [PBTS-ALG-OLD-PREVOTE.0]
\* @type: (PROCESS) => Bool;
UponProposalInProposeAndPrevote(p) ==
\E v \in Values, t \in Timestamps, vr \in Rounds, pr \in Rounds:
LET
r == round[p]
IN LET
\* @type: PROPOSAL;
prop == Proposal(v,t,pr)
IN
/\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < r \* line 28, the while part
/\ pr <= vr
/\ LET
\E v \in Values, t1 \in Timestamps, t2 \in Timestamps, vr \in Rounds:
/\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < round[p] \* line 28, the while part
/\ LET
\* @type: PROPMESSAGE;
msg ==
[
type |-> "PROPOSAL",
src |-> Proposer[r],
round |-> r,
proposal |-> prop,
src |-> Proposer[round[p]],
round |-> round[p],
proposal |-> Proposal(v, t1),
validRound |-> vr
]
IN
\* Changed from 001: no need to re-check timeliness
/\ msg \in msgsPropose[r] \* line 28
/\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(prop) } IN
/\ <<p, msg>> \in receivedTimelyProposal \* updated line 28
/\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(Proposal(v, t2)) } IN
/\ Cardinality(PV) >= THRESHOLD2 \* line 28
/\ evidence' = PV \union {msg} \union evidence
/\ LET mid == (* line 29 *)
IF IsValid(prop) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v)
THEN Id(prop)
IF IsValid(v) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v)
THEN Id(Proposal(v, t1))
ELSE NilProposal
IN
BroadcastPrevote(p, r, mid) \* lines 24-26
BroadcastPrevote(p, round[p], mid) \* lines 24-26
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED
<<round, (*step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
/\ UNCHANGED <<round, decision, lockedValue, lockedRound,
validValue, validRound, msgsPropose, msgsPrecommit,
localClock, realTime, receivedTimelyProposal, inspectedProposal,
beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
/\ action' = "UponProposalInProposeAndPrevote"
\* lines 34-35 + lines 61-64 (onTimeoutPrevote)
@@ -562,13 +494,10 @@ UponQuorumOfPrevotesAny(p) ==
/\ evidence' = MyEvidence \union evidence
/\ BroadcastPrecommit(p, round[p], NilProposal)
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED
<<round, (*step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
/\ UNCHANGED <<round, decision, lockedValue, lockedRound,
validValue, validRound, msgsPropose, msgsPrevote,
localClock, realTime, receivedTimelyProposal, inspectedProposal,
beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
/\ action' = "UponQuorumOfPrevotesAny"
\* lines 36-46
@@ -576,47 +505,36 @@ UponQuorumOfPrevotesAny(p) ==
\* @type: (PROCESS) => Bool;
UponProposalInPrevoteOrCommitAndPrevote(p) ==
\E v \in ValidValues, t \in Timestamps, vr \in RoundsOrNil:
LET
r == round[p]
IN LET
\* @type: PROPOSAL;
prop == Proposal(v,t,r)
IN
/\ step[p] \in {"PREVOTE", "PRECOMMIT"} \* line 36
/\ LET
\* @type: PROPMESSAGE;
msg ==
[
type |-> "PROPOSAL",
src |-> Proposer[r],
round |-> r,
proposal |-> prop,
src |-> Proposer[round[p]],
round |-> round[p],
proposal |-> Proposal(v, t),
validRound |-> vr
]
IN
\* Changed from 001: no need to re-check timeliness
/\ msg \in msgsPropose[r] \* line 36
/\ LET PV == { m \in msgsPrevote[r]: m.id = Id(prop) } IN
/\ <<p, msg>> \in receivedTimelyProposal \* updated line 36
/\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(Proposal(v, t)) } IN
/\ Cardinality(PV) >= THRESHOLD2 \* line 36
/\ evidence' = PV \union {msg} \union evidence
/\ IF step[p] = "PREVOTE"
THEN \* lines 38-41:
/\ lockedValue' = [lockedValue EXCEPT ![p] = v]
/\ lockedRound' = [lockedRound EXCEPT ![p] = r]
/\ BroadcastPrecommit(p, r, Id(prop))
/\ lockedRound' = [lockedRound EXCEPT ![p] = round[p]]
/\ BroadcastPrecommit(p, round[p], Id(Proposal(v, t)))
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
ELSE
UNCHANGED <<lockedValue, lockedRound, msgsPrecommit, step>>
\* lines 42-43
/\ validValue' = [validValue EXCEPT ![p] = prop]
/\ validRound' = [validRound EXCEPT ![p] = r]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED
<<round, (*step,*) decision(*, lockedValue,
lockedRound, validValue, validRound*)>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
/\ validValue' = [validValue EXCEPT ![p] = v]
/\ validRound' = [validRound EXCEPT ![p] = round[p]]
/\ UNCHANGED <<round, decision, msgsPropose, msgsPrevote,
localClock, realTime, receivedTimelyProposal, inspectedProposal,
beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
/\ action' = "UponProposalInPrevoteOrCommitAndPrevote"
\* lines 47-48 + 65-67 (onTimeoutPrecommit)
@@ -629,17 +547,11 @@ UponQuorumOfPrecommitsAny(p) ==
/\ Cardinality(Committers) >= THRESHOLD2 \* line 47
/\ evidence' = MyEvidence \union evidence
/\ round[p] + 1 \in Rounds
/\ StartRound(p, round[p] + 1)
/\ UNCHANGED temporalVars
/\ UNCHANGED
<<(*beginRound,*) endConsensus, (*lastBeginRound,*)
proposalTime, proposalReceivedTime>>
/\ UNCHANGED
<<(*round, step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, msgsPrecommit,
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
/\ StartRound(p, round[p] + 1)
/\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
validRound, msgsPropose, msgsPrevote, msgsPrecommit,
localClock, realTime, receivedTimelyProposal, inspectedProposal,
beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
/\ action' = "UponQuorumOfPrecommitsAny"
\* lines 49-54
@@ -647,11 +559,7 @@ UponQuorumOfPrecommitsAny(p) ==
\* @type: (PROCESS) => Bool;
UponProposalInPrecommitNoDecision(p) ==
/\ decision[p] = NilDecision \* line 49
/\ \E v \in ValidValues, t \in Timestamps (* line 50*) , r \in Rounds, pr \in Rounds, vr \in RoundsOrNil:
LET
\* @type: PROPOSAL;
prop == Proposal(v,t,pr)
IN
/\ \E v \in ValidValues, t \in Timestamps (* line 50*) , r \in Rounds, vr \in RoundsOrNil:
/\ LET
\* @type: PROPMESSAGE;
msg ==
@@ -659,30 +567,24 @@ UponProposalInPrecommitNoDecision(p) ==
type |-> "PROPOSAL",
src |-> Proposer[r],
round |-> r,
proposal |-> prop,
proposal |-> Proposal(v, t),
validRound |-> vr
]
IN
/\ msg \in msgsPropose[r] \* line 49
/\ inspectedProposal[r,p] /= NilTimestamp \* Keep?
/\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(prop) } IN
/\ p \in inspectedProposal[r]
/\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(Proposal(v, t)) } IN
/\ Cardinality(PV) >= THRESHOLD2 \* line 49
/\ evidence' = PV \union {msg} \union evidence
/\ decision' = [decision EXCEPT ![p] = Decision(prop, r)] \* update the decision, line 51
/\ decision' = [decision EXCEPT ![p] = Decision(v, t, round[p])] \* update the decision, line 51
\* The original algorithm does not have 'DECIDED', but it increments the height.
\* We introduced 'DECIDED' here to prevent the process from changing its decision.
/\ endConsensus' = [endConsensus EXCEPT ![p] = localClock[p]]
/\ step' = [step EXCEPT ![p] = "DECIDED"]
/\ UNCHANGED temporalVars
/\ UNCHANGED
<<round, (*step, decision,*) lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, msgsPrecommit,
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
/\ UNCHANGED
<<beginRound, (*endConsensus,*) lastBeginRound,
proposalTime, proposalReceivedTime>>
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
validRound, msgsPropose, msgsPrevote, msgsPrecommit,
localClock, realTime, receivedTimelyProposal, inspectedProposal,
beginConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
/\ action' = "UponProposalInPrecommitNoDecision"
\* the actions below are not essential for safety, but added for completeness
@@ -694,13 +596,10 @@ OnTimeoutPropose(p) ==
/\ p /= Proposer[round[p]]
/\ BroadcastPrevote(p, round[p], NilProposal)
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED
<<round, (*step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
evidence, receivedTimelyProposal, inspectedProposal>>
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
validRound, decision, evidence, msgsPropose, msgsPrecommit,
localClock, realTime, receivedTimelyProposal, inspectedProposal,
beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
/\ action' = "OnTimeoutPropose"
\* lines 44-46
@@ -712,13 +611,10 @@ OnQuorumOfNilPrevotes(p) ==
/\ evidence' = PV \union evidence
/\ BroadcastPrecommit(p, round[p], Id(NilProposal))
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED
<<round, (*step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, (*msgsPrecommit,*)
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
validRound, decision, msgsPropose, msgsPrevote,
localClock, realTime, receivedTimelyProposal, inspectedProposal,
beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
/\ action' = "OnQuorumOfNilPrevotes"
\* lines 55-56
@@ -731,16 +627,10 @@ OnRoundCatchup(p) ==
/\ Cardinality(Faster) >= THRESHOLD1
/\ evidence' = MyEvidence \union evidence
/\ StartRound(p, r)
/\ UNCHANGED temporalVars
/\ UNCHANGED
<<(*beginRound,*) endConsensus, (*lastBeginRound,*)
proposalTime, proposalReceivedTime>>
/\ UNCHANGED
<<(*round, step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, msgsPrecommit,
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
/\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
validRound, msgsPropose, msgsPrevote, msgsPrecommit,
localClock, realTime, receivedTimelyProposal, inspectedProposal,
beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
/\ action' = "OnRoundCatchup"
@@ -748,24 +638,28 @@ OnRoundCatchup(p) ==
\* advance the global clock
\* @type: Bool;
AdvanceRealTime ==
/\ ValidTime(realTime)
/\ \E t \in Timestamps:
/\ t > realTime
/\ realTime' = t
/\ localClock' = [p \in Corr |-> localClock[p] + (t - realTime)]
/\ UNCHANGED <<coreVars, bookkeepingVars, invariantVars>>
/\ realTime < MaxTimestamp
/\ realTime' = realTime + 1
/\ \/ /\ ~ClockDrift
/\ localClock' = [p \in Corr |-> localClock[p] + 1]
\/ /\ ClockDrift
/\ UNCHANGED localClock
/\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
localClock, receivedTimelyProposal, inspectedProposal,
beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
/\ action' = "AdvanceRealTime"
\* advance the local clock of node p to some larger time t, not necessarily by 1
\* #type: (PROCESS) => Bool;
\* AdvanceLocalClock(p) ==
\* /\ ValidTime(localClock[p])
\* /\ \E t \in Timestamps:
\* /\ t > localClock[p]
\* /\ localClock' = [localClock EXCEPT ![p] = t]
\* /\ UNCHANGED <<coreVars, bookkeepingVars, invariantVars>>
\* /\ UNCHANGED realTime
\* /\ action' = "AdvanceLocalClock"
\* advance the local clock of node p
\* @type: (PROCESS) => Bool;
AdvanceLocalClock(p) ==
/\ localClock[p] < MaxTimestamp
/\ localClock' = [localClock EXCEPT ![p] = @ + 1]
/\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
realTime, receivedTimelyProposal, inspectedProposal,
beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
/\ action' = "AdvanceLocalClock"
\* process timely messages
\* @type: (PROCESS) => Bool;
@@ -790,8 +684,10 @@ MessageProcessing(p) ==
* A system transition. In this specificatiom, the system may eventually deadlock,
* e.g., when all processes decide. This is expected behavior, as we focus on safety.
*)
Next ==
Next ==
\/ AdvanceRealTime
\/ /\ ClockDrift
/\ \E p \in Corr: AdvanceLocalClock(p)
\/ /\ SynchronizedLocalClocks
/\ \E p \in Corr: MessageProcessing(p)
@@ -804,62 +700,59 @@ AgreementOnValue ==
\A p, q \in Corr:
/\ decision[p] /= NilDecision
/\ decision[q] /= NilDecision
=> \E v \in ValidValues, t \in Timestamps, pr \in Rounds, r1 \in Rounds, r2 \in Rounds :
LET prop == Proposal(v,t,pr)
IN
/\ decision[p] = Decision(prop, r1)
/\ decision[q] = Decision(prop, r2)
=> \E v \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r1 \in Rounds, r2 \in Rounds :
/\ decision[p] = Decision(v, t1, r1)
/\ decision[q] = Decision(v, t2, r2)
\* [PBTS-INV-TIME-AGR.0]
AgreementOnTime ==
\A p, q \in Corr:
\A v1 \in ValidValues, v2 \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r \in Rounds :
/\ decision[p] = Decision(v1, t1, r)
/\ decision[q] = Decision(v2, t2, r)
=> t1 = t2
\* [PBTS-CONSENSUS-TIME-VALID.0]
ConsensusTimeValid ==
\A p \in Corr:
\A p \in Corr, t \in Timestamps :
\* if a process decides on v and t
\E v \in ValidValues, t \in Timestamps, pr \in Rounds, dr \in Rounds :
decision[p] = Decision(Proposal(v,t,pr), dr)
(\E v \in ValidValues, r \in Rounds : decision[p] = Decision(v, t, r))
\* then
\* TODO: consider tighter bound where beginRound[pr] is replaced
\* w/ MedianOfRound[pr]
=> (/\ beginRound[pr] - Precision - Delay <= t
/\ t <= endConsensus[p] + Precision)
=> /\ beginConsensus - Precision <= t
/\ t < endConsensus[p] + Precision + Delay
\* [PBTS-CONSENSUS-SAFE-VALID-CORR-PROP.0]
ConsensusSafeValidCorrProp ==
\A v \in ValidValues:
\* and there exists a process that decided on v, t
/\ \E p \in Corr, t \in Timestamps, pr \in Rounds, dr \in Rounds :
\* if the proposer in the round is correct
(/\ Proposer[pr] \in Corr
/\ decision[p] = Decision(Proposal(v,t,pr), dr))
\* then t is between the minimal and maximal initial local time
=> /\ beginRound[pr] <= t
/\ t <= lastBeginRound[pr]
\A v \in ValidValues, t \in Timestamps :
\* if the proposer in the first round is correct
(/\ Proposer[0] \in Corr
\* and there exists a process that decided on v, t
/\ \E p \in Corr, r \in Rounds : decision[p] = Decision(v, t, r))
\* then t is between the minimal and maximal initial local time
=> /\ beginConsensus <= t
/\ t <= lastBeginConsensus
\* [PBTS-CONSENSUS-REALTIME-VALID-CORR.0]
ConsensusRealTimeValidCorr ==
\A r \in Rounds :
\E p \in Corr, v \in ValidValues, t \in Timestamps, pr \in Rounds:
(/\ decision[p] = Decision(Proposal(v,t,pr), r)
/\ proposalTime[r] /= NilTimestamp)
=> (/\ proposalTime[r] - Precision <= t
/\ t <= proposalTime[r] + Precision)
\A t \in Timestamps, r \in Rounds :
(/\ \E p \in Corr, v \in ValidValues : decision[p] = Decision(v, t, r)
/\ proposalTime[r] /= NilTimestamp)
=> /\ proposalTime[r] - Accuracy < t
/\ t < proposalTime[r] + Accuracy
\* [PBTS-CONSENSUS-REALTIME-VALID.0]
ConsensusRealTimeValid ==
\A t \in Timestamps, r \in Rounds :
(\E p \in Corr, v \in ValidValues, pr \in Rounds :
decision[p] = Decision(Proposal(v,t,pr), r))
=> /\ proposalReceivedTime[r] - Precision < t
/\ t < proposalReceivedTime[r] + Precision + Delay
DecideAfterMin == TRUE
\* if decide => time > min
(\E p \in Corr, v \in ValidValues : decision[p] = Decision(v, t, r))
=> /\ proposalReceivedTime[r] - Accuracy - Precision < t
/\ t < proposalReceivedTime[r] + Accuracy + Precision + Delay
\* [PBTS-MSG-FAIR.0]
BoundedDelay ==
\A r \in Rounds :
(/\ proposalTime[r] /= NilTimestamp
/\ proposalTime[r] + Delay < realTime)
=> \A p \in Corr: inspectedProposal[r,p] /= NilTimestamp
=> inspectedProposal[r] = Corr
\* [PBTS-CONSENSUS-TIME-LIVE.0]
ConsensusTimeLive ==
@@ -868,18 +761,19 @@ ConsensusTimeLive ==
/\ proposalTime[r] + Delay < realTime
/\ Proposer[r] \in Corr
/\ round[p] <= r)
=> \E msg \in RoundProposals(r) : msg \in receivedTimelyProposal[p]
=> \E msg \in RoundProposals(r) : <<p, msg>> \in receivedTimelyProposal
\* a conjunction of all invariants
Inv ==
/\ AgreementOnValue
/\ AgreementOnTime
/\ ConsensusTimeValid
/\ ConsensusSafeValidCorrProp
\* /\ ConsensusRealTimeValid
\* /\ ConsensusRealTimeValidCorr
\* /\ BoundedDelay
/\ ConsensusRealTimeValid
/\ ConsensusRealTimeValidCorr
/\ BoundedDelay
\* Liveness ==
\* ConsensusTimeLive
Liveness ==
ConsensusTimeLive
=============================================================================

5
spec/consensus/proposer-based-timestamp/tla/typedefs.tla
View File

@@ -7,8 +7,9 @@
@typeAlias: ACTION = Str;
@typeAlias: TRACE = Seq(Str);
@typeAlias: TIME = Int;
@typeAlias: PROPOSAL = <<VALUE, TIME, ROUND>>;
@typeAlias: DECISION = <<PROPOSAL, ROUND>>;
@typeAlias: PROPOSAL = <<VALUE, TIME>>;
@typeAlias: DECISION = <<VALUE, TIME, ROUND>>;
@typeAlias: RCVPROP = <<PROCESS, PROPMESSAGE>>;
@typeAlias: PROPMESSAGE =
[
type: STEP,