From aa8581a9f0fcef9ede503fb1f172b1a3d403ad0b Mon Sep 17 00:00:00 2001 From: Kukovec Date: Fri, 6 May 2022 11:31:49 +0200 Subject: [PATCH] move + rename --- .../proposer-based-timestamp/tla/Apalache.tla | 109 ----- .../tla/MC_PBT_2C_2F.tla | 68 ++++ .../tla/MC_PBT_3C_1F.tla | 68 ++++ ...intPBT_002_draft.tla => TendermintPBT.tla} | 385 +++++++++--------- .../{tla => v1}/TendermintPBT_001_draft.tla | 0 5 files changed, 335 insertions(+), 295 deletions(-) delete mode 100644 spec/consensus/proposer-based-timestamp/tla/Apalache.tla create mode 100644 spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla create mode 100644 spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla rename spec/consensus/proposer-based-timestamp/tla/{TendermintPBT_002_draft.tla => TendermintPBT.tla} (72%) rename spec/consensus/proposer-based-timestamp/{tla => v1}/TendermintPBT_001_draft.tla (100%) diff --git a/spec/consensus/proposer-based-timestamp/tla/Apalache.tla b/spec/consensus/proposer-based-timestamp/tla/Apalache.tla deleted file mode 100644 index 044bff666..000000000 --- a/spec/consensus/proposer-based-timestamp/tla/Apalache.tla +++ /dev/null @@ -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 <> and <> 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); - *) -SetAsFun(S) == - LET Dom == { x: <> \in S } - Rng == { y: <> \in S } - IN - [ x \in Dom |-> CHOOSE y \in Rng: <> \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) ) - -=============================================================================== diff --git a/spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla new file mode 100644 index 000000000..d7de3df73 --- /dev/null +++ b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla @@ -0,0 +1,68 @@ +----------------------------- MODULE MC_PBT_2C_2F ------------------------------- +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: <> -> TIME; + proposalReceptionTime \* used to keep track when a process receives a message + +\* Invariant support +VARIABLES + \* @type: <> -> TIME; + beginRound \* the minimum of the local clocks at the time any process entered a new round + +INSTANCE TendermintPBT WITH + Corr <- {"c1", "c2"}, + Faulty <- {"f3", "f4"}, + N <- 4, + T <- 1, + ValidValues <- { "v0", "v1" }, + InvalidValues <- {"v2"}, + MaxRound <- 3, + MaxTimestamp <- 7, + MinTimestamp <- 2, + Delay <- 2, + Precision <- 2, + PreloadAllFaultyMsgs <- TRUE, + N_GEN <- 5 + +\* run Apalache with --cinit=CInit +CInit == \* the proposer is arbitrary -- works for safety + ArbitraryProposer + +============================================================================= diff --git a/spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla new file mode 100644 index 000000000..aec3d17a9 --- /dev/null +++ b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla @@ -0,0 +1,68 @@ +----------------------------- MODULE MC_PBT_3C_1F ------------------------------- +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: <> -> TIME; + proposalReceptionTime \* used to keep track when a process receives a message + +\* Invariant support +VARIABLES + \* @type: <> -> TIME; + beginRound \* the minimum of the local clocks at the time any process entered a new round + +INSTANCE TendermintPBT WITH + Corr <- {"c1", "c2", "c3"}, + Faulty <- {"f4"}, + N <- 4, + T <- 1, + ValidValues <- { "v0", "v1" }, + InvalidValues <- {"v2"}, + MaxRound <- 3, + MaxTimestamp <- 7, + MinTimestamp <- 2, + Delay <- 2, + Precision <- 2, + PreloadAllFaultyMsgs <- TRUE, + N_GEN <- 5 + +\* run Apalache with --cinit=CInit +CInit == \* the proposer is arbitrary -- works for safety + ArbitraryProposer + +============================================================================= diff --git a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT.tla similarity index 72% rename from spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla rename to spec/consensus/proposer-based-timestamp/tla/TendermintPBT.tla index 983c7351b..a2ee26d64 100644 --- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla +++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT.tla @@ -1,4 +1,4 @@ --------------------- MODULE TendermintPBT_002_draft --------------------------- +-------------------- MODULE TendermintPBT --------------------------- (* A TLA+ specification of a simplified Tendermint consensus, with added clocks and proposer-based timestamps. This TLA+ specification extends and modifies @@ -12,7 +12,7 @@ Jure Kukovec, Informal Systems, 2022. *) -EXTENDS Integers, FiniteSets, Apalache, typedefs +EXTENDS Integers, FiniteSets, Apalache, Sequences, typedefs (********************* PROTOCOL PARAMETERS **********************************) \* General protocol parameters @@ -47,6 +47,13 @@ CONSTANTS ASSUME(N = Cardinality(Corr \union Faulty)) +\* Modeling parameter +CONSTANTS + \* @type: Bool; + PreloadAllFaultyMsgs, + \* @type: Int; + N_GEN + (*************************** DEFINITIONS ************************************) \* @type: Set(PROCESS); AllProcs == Corr \union Faulty \* the set of all processes @@ -75,6 +82,14 @@ Decisions == Proposals \X Rounds \* @type: DECISION; NilDecision == <> +ArbitraryProposer == Proposer \in [Rounds -> AllProcs] +CorrectProposer == Proposer \in [Rounds -> Corr] +CyclicalProposer == + LET ProcOrder == + LET App(s,e) == Append(s,e) + IN ApaFoldSet(App, <<>>, AllProcs) + IN Proposer = [ r \in Rounds |-> ProcOrder[1 + (r % N)] ] + ValidProposals == ValidValues \X (MinTimestamp..MaxTimestamp) \X Rounds \* a value hash is modeled as identity \* @type: (t) => t; @@ -108,13 +123,13 @@ 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) == ApaFoldSet( Min2, MaxTimestamp, S ) \* 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) == ApaFoldSet( Max2, NilTimestamp, S ) \* Max(S) == CHOOSE x \in S : \A y \in S : y <= x \* @type: (Set(MESSAGE)) => Int; @@ -122,7 +137,7 @@ Card(S) == LET \* @type: (Int, MESSAGE) => Int; PlusOne(i, m) == i + 1 - IN FoldSet( PlusOne, 0, S ) + IN ApaFoldSet( PlusOne, 0, S ) (********************* PROTOCOL STATE VARIABLES ******************************) VARIABLES @@ -166,33 +181,18 @@ 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); - receivedTimelyProposal, \* used to keep track when a process receives a timely PROPOSAL message \* @type: <> -> TIME; - inspectedProposal \* used to keep track when a process tries to receive a message + proposalReceptionTime \* used to keep track when a process receives a message \* Action is excluded from the tuple, because it always changes bookkeepingVars == <> + evidence, (*action,*) proposalReceptionTime>> \* 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 - -invariantVars == - <> + \* @type: <> -> TIME; + beginRound \* the minimum of the local clocks at the time any process entered a new round (* to see a type invariant, check TendermintAccInv3 *) @@ -280,6 +280,39 @@ BenignRoundsInMessages(msgfun) == \A m \in msgfun[r]: r = m.round +\* @type: (ROUND -> Set(MESSAGE), Set(MESSAGE)) => Bool; +BenignAndSubset(msgfun, set) == + /\ \A r \in Rounds: + \* The generated values belong to SUBSET set + /\ msgfun[r] \subseteq set + \* the message function never contains a message for a wrong round + /\ \A m \in msgfun[r]: r = m.round + +InitGen == + /\ msgsPropose \in [Rounds -> Gen(N_GEN)] + /\ msgsPrevote \in [Rounds -> Gen(N_GEN)] + /\ msgsPrecommit \in [Rounds -> Gen(N_GEN)] + /\ BenignAndSubset(msgsPropose, AllFaultyProposals) + /\ BenignAndSubset(msgsPrevote, AllFaultyPrevotes) + /\ BenignAndSubset(msgsPrecommit, AllFaultyPrecommits) + +InitPreloadAllMsgs == + /\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals] + /\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes] + /\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits] + /\ BenignRoundsInMessages(msgsPropose) + /\ BenignRoundsInMessages(msgsPrevote) + /\ BenignRoundsInMessages(msgsPrecommit) + +InitMsgs == + \/ /\ PreloadAllFaultyMsgs + \* /\ InitPreloadAllMsgs + /\ InitGen + \/ /\ ~PreloadAllFaultyMsgs + /\ msgsPropose = [r \in Rounds |-> {}] + /\ msgsPrevote = [r \in Rounds |-> {}] + /\ msgsPrecommit = [r \in Rounds |-> {}] + \* The initial states of the protocol. Some faults can be in the system already. Init == /\ round = [p \in Corr |-> 0] @@ -291,31 +324,48 @@ Init == /\ lockedRound = [p \in Corr |-> NilRound] /\ validValue = [p \in Corr |-> NilProposal] /\ 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] - /\ BenignRoundsInMessages(msgsPropose) - /\ BenignRoundsInMessages(msgsPrevote) - /\ BenignRoundsInMessages(msgsPrecommit) + /\ InitMsgs + /\ proposalReceptionTime = [r \in Rounds, p \in Corr |-> NilTimestamp] /\ evidence = {} - /\ action' = "Init" + /\ action = "Init" /\ beginRound = - [r \in Rounds |-> + [r \in Rounds, c \in Corr |-> IF r = 0 - THEN Min({localClock[p] : p \in Corr}) + THEN localClock[c] ELSE MaxTimestamp ] - /\ endConsensus = [p \in Corr |-> NilTimestamp] - /\ lastBeginRound = - [r \in Rounds |-> - IF r = 0 - THEN Max({localClock[p] : p \in Corr}) - ELSE NilTimestamp - ] - /\ proposalTime = [r \in Rounds |-> NilTimestamp] - /\ proposalReceivedTime = [r \in Rounds |-> NilTimestamp] + +lastBeginRound == [ r \in Rounds |-> + Max({beginRound[r,p] : p \in Corr}) +] + +firstBeginRound == [ r \in Rounds |-> + Min({beginRound[r,p] : p \in Corr}) +] + +\* Faulty processes send messages +FaultyBroadcast == + /\ ~PreloadAllFaultyMsgs + /\ action' = "FaultyBroadcast" + /\ \E r \in Rounds: + \/ \E msgs \in SUBSET FaultyProposals(r): + /\ msgsPropose' = [msgsPropose EXCEPT ![r] = @ \union msgs] + /\ UNCHANGED <> + /\ UNCHANGED + <<(*msgsPropose,*) msgsPrevote, msgsPrecommit, + evidence, (*action,*) proposalReceptionTime>> + \/ \E msgs \in SUBSET FaultyPrevotes(r): + /\ msgsPrevote' = [msgsPrevote EXCEPT ![r] = @ \union msgs] + /\ UNCHANGED <> + /\ UNCHANGED + <> + \/ \E msgs \in SUBSET FaultyPrecommits(r): + /\ msgsPrecommit' = [msgsPrecommit EXCEPT ![r] = @ \union msgs] + /\ UNCHANGED <> + /\ UNCHANGED + <> (************************ MESSAGE PASSING ********************************) \* @type: (PROCESS, ROUND, PROPOSAL, ROUND) => Bool; @@ -391,8 +441,7 @@ StartRound(p, r) == /\ 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])] + /\ beginRound' = [beginRound EXCEPT ![r,p] = localClock[p]] \* lines 14-19, a proposal may be sent later \* @type: (PROCESS) => Bool; @@ -403,7 +452,6 @@ 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 @@ -411,17 +459,14 @@ InsertProposal(p) == ELSE Proposal(v, localClock[p], r) IN /\ BroadcastProposal(p, r, proposal, validRound[p]) - /\ proposalTime' = [proposalTime EXCEPT ![r] = realTime] /\ UNCHANGED <> /\ UNCHANGED <<(*msgsPropose,*) msgsPrevote, msgsPrecommit, - evidence, receivedTimelyProposal, inspectedProposal>> - /\ UNCHANGED - <> + evidence, proposalReceptionTime>> + /\ UNCHANGED beginRound /\ action' = "InsertProposal" -\* a new action used to filter messages that are not on time +\* a new action used to register the proposal and note the reception time. \* [PBTS-RECEPTION-STEP.0] \* @type: (PROCESS) => Bool; ReceiveProposal(p) == @@ -439,30 +484,13 @@ ReceiveProposal(p) == ] 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 <> + /\ proposalReceptionTime[r,p] = NilTimestamp + /\ proposalReceptionTime' = [proposalReceptionTime EXCEPT ![r,p] = localClock[p]] /\ UNCHANGED <> /\ UNCHANGED <> - /\ UNCHANGED - <> + evidence(*, proposalReceptionTime*)>> + /\ UNCHANGED beginRound /\ action' = "ReceiveProposal" \* lines 22-27 @@ -487,22 +515,29 @@ UponProposalInPropose(p) == validRound |-> NilRound ] IN - /\ msg \in receivedTimelyProposal[p] \* updated line 22 /\ evidence' = {msg} \union evidence /\ LET mid == (* line 23 *) - IF IsValid(prop) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v) + IF + \* Timeliness is checked against the process time, as was + \* recorded in proposalReceptionTime, not as it is now. + \* In the implementation, if the proposal is not timely, then we prevote + \* nil. In the natural-language specification, nothing happens. + \* This specification maintains consistency with the implementation. + /\ IsTimely( proposalReceptionTime[r, p], t) \* updated line 22 + /\ IsValid(prop) + /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v) THEN Id(prop) ELSE NilProposal IN BroadcastPrevote(p, r, mid) \* lines 24-26 /\ step' = [step EXCEPT ![p] = "PREVOTE"] - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "UponProposalInPropose" \* lines 28-33 @@ -541,13 +576,13 @@ UponProposalInProposeAndPrevote(p) == IN BroadcastPrevote(p, r, mid) \* lines 24-26 /\ step' = [step EXCEPT ![p] = "PREVOTE"] - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "UponProposalInProposeAndPrevote" \* lines 34-35 + lines 61-64 (onTimeoutPrevote) @@ -562,13 +597,13 @@ UponQuorumOfPrevotesAny(p) == /\ evidence' = MyEvidence \union evidence /\ BroadcastPrecommit(p, round[p], NilProposal) /\ step' = [step EXCEPT ![p] = "PRECOMMIT"] - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "UponQuorumOfPrevotesAny" \* lines 36-46 @@ -610,13 +645,13 @@ UponProposalInPrevoteOrCommitAndPrevote(p) == \* lines 42-43 /\ validValue' = [validValue EXCEPT ![p] = prop] /\ validRound' = [validRound EXCEPT ![p] = r] - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "UponProposalInPrevoteOrCommitAndPrevote" \* lines 47-48 + 65-67 (onTimeoutPrecommit) @@ -631,15 +666,12 @@ UponQuorumOfPrecommitsAny(p) == /\ 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 <> + (*evidence,*) proposalReceptionTime>> /\ action' = "UponQuorumOfPrecommitsAny" \* lines 49-54 @@ -664,14 +696,13 @@ UponProposalInPrecommitNoDecision(p) == ] IN /\ msg \in msgsPropose[r] \* line 49 - /\ inspectedProposal[r,p] /= NilTimestamp \* Keep? + /\ proposalReceptionTime[r,p] /= NilTimestamp \* Keep? /\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(prop) } IN /\ Cardinality(PV) >= THRESHOLD2 \* line 49 /\ evidence' = PV \union {msg} \union evidence /\ decision' = [decision EXCEPT ![p] = Decision(prop, r)] \* 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 @@ -679,10 +710,8 @@ UponProposalInPrecommitNoDecision(p) == lockedRound, validValue, validRound>> /\ UNCHANGED <> - /\ UNCHANGED - <> + (*evidence,*) proposalReceptionTime>> + /\ UNCHANGED beginRound /\ action' = "UponProposalInPrecommitNoDecision" \* the actions below are not essential for safety, but added for completeness @@ -694,13 +723,13 @@ OnTimeoutPropose(p) == /\ p /= Proposer[round[p]] /\ BroadcastPrevote(p, round[p], NilProposal) /\ step' = [step EXCEPT ![p] = "PREVOTE"] - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> /\ UNCHANGED <> + evidence, proposalReceptionTime>> /\ action' = "OnTimeoutPropose" \* lines 44-46 @@ -712,36 +741,34 @@ OnQuorumOfNilPrevotes(p) == /\ evidence' = PV \union evidence /\ BroadcastPrecommit(p, round[p], Id(NilProposal)) /\ step' = [step EXCEPT ![p] = "PRECOMMIT"] - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "OnQuorumOfNilPrevotes" \* lines 55-56 \* @type: (PROCESS) => Bool; OnRoundCatchup(p) == - \E r \in {rr \in Rounds: rr > round[p]}: - LET RoundMsgs == msgsPropose[r] \union msgsPrevote[r] \union msgsPrecommit[r] IN - \E MyEvidence \in SUBSET RoundMsgs: - LET Faster == { m.src: m \in MyEvidence } IN - /\ 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 - <> - /\ action' = "OnRoundCatchup" + \E r \in Rounds: + /\ r > round[p] + /\ LET RoundMsgs == msgsPropose[r] \union msgsPrevote[r] \union msgsPrecommit[r] IN + \E MyEvidence \in SUBSET RoundMsgs: + LET Faster == { m.src: m \in MyEvidence } IN + /\ Cardinality(Faster) >= THRESHOLD1 + /\ evidence' = MyEvidence \union evidence + /\ StartRound(p, r) + /\ UNCHANGED temporalVars + /\ UNCHANGED + <<(*round, step,*) decision, lockedValue, + lockedRound, validValue, validRound>> + /\ UNCHANGED + <> + /\ action' = "OnRoundCatchup" (********************* PROTOCOL TRANSITIONS ******************************) @@ -753,19 +780,8 @@ AdvanceRealTime == /\ t > realTime /\ realTime' = t /\ localClock' = [p \in Corr |-> localClock[p] + (t - realTime)] - /\ UNCHANGED <> + /\ UNCHANGED <> /\ 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 <> -\* /\ UNCHANGED realTime -\* /\ action' = "AdvanceLocalClock" \* process timely messages \* @type: (PROCESS) => Bool; @@ -792,6 +808,7 @@ MessageProcessing(p) == *) Next == \/ AdvanceRealTime + \/ FaultyBroadcast \/ /\ SynchronizedLocalClocks /\ \E p \in Corr: MessageProcessing(p) @@ -810,76 +827,72 @@ AgreementOnValue == /\ decision[p] = Decision(prop, r1) /\ decision[q] = Decision(prop, r2) -\* [PBTS-CONSENSUS-TIME-VALID.0] +DisagreementOnValue == + \E p, q \in Corr: + \E p1 \in ValidProposals, p2 \in ValidProposals, r1 \in Rounds, r2 \in Rounds: + /\ p1 /= p2 + /\ decision[p] = Decision(p1, r1) + /\ decision[q] = Decision(p2, r2) + +\* [PBTS-INV-VALID.0] +ConsensusValidValue == + \A p \in Corr: + \* decision[p] = Decision(Proposal(v,t,pr), r) + LET prop == decision[p][1] IN + prop /= NilProposal => prop[1] \in ValidValues + +\* [PBTS-INV-MONOTONICITY.0] +\* TODO: we would need to compare timestamps of blocks from different height + +\* [PBTS-INV-TIMELY.0] ConsensusTimeValid == \A p \in Corr: \* if a process decides on v and t \E v \in ValidValues, t \in Timestamps, pr \in Rounds, dr \in Rounds : + \* FIXME: do we need to enforce pr <= dr? decision[p] = Decision(Proposal(v,t,pr), dr) - \* then - \* TODO: consider tighter bound where beginRound[pr] is replaced - \* w/ MedianOfRound[pr] - => (/\ beginRound[pr] - Precision - Delay <= t - /\ t <= endConsensus[p] + Precision) + \* then a process found t timely at its proposal round (pr) + => \E q \in Corr: + LET propRecvTime == proposalReceptionTime[pr, q] IN + ( + /\ beginRound[pr, q] <= propRecvTime + /\ beginRound[pr+1, q] >= propRecvTime + /\ IsTimely(propRecvTime, t) + ) -\* [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] +IsFirstProposedInRound(prop, src, r) == + \E msg \in msgsPropose[r]: + /\ msg.proposal = prop + /\ msg.src = src + \* If a proposal is reused this changes from Nil to a valid round + /\ msg.validRound = NilRound -\* [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) +TimeLiveness == +\A r \in Rounds \ {MaxRound}, v \in ValidValues: + LET p == Proposer[r] IN + /\ p \in Corr \* Correct process is proposer in round r + /\ + \E t \in Timestamps: + LET prop == Proposal(v,t,r) IN + ( + /\ IsFirstProposedInRound(prop, p, r) \* p proposes v with some timestamp t in round r + /\ LET tOffset == t + Delay + Precision IN + /\ firstBeginRound[r] <= t + /\ t <= lastBeginRound[r] + /\ lastBeginRound[r] <= tOffset + /\ tOffset <= firstBeginRound[r+1] + ) => + \A q \in Corr: + \* q eventually decides prop + LET dq == decision[q] IN + dq /= NilDecision => dq[1] = prop -\* [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 - -\* [PBTS-MSG-FAIR.0] -BoundedDelay == - \A r \in Rounds : - (/\ proposalTime[r] /= NilTimestamp - /\ proposalTime[r] + Delay < realTime) - => \A p \in Corr: inspectedProposal[r,p] /= NilTimestamp - -\* [PBTS-CONSENSUS-TIME-LIVE.0] -ConsensusTimeLive == - \A r \in Rounds, p \in Corr : - (/\ proposalTime[r] /= NilTimestamp - /\ proposalTime[r] + Delay < realTime - /\ Proposer[r] \in Corr - /\ round[p] <= r) - => \E msg \in RoundProposals(r) : msg \in receivedTimelyProposal[p] \* a conjunction of all invariants Inv == /\ AgreementOnValue + /\ ConsensusValidValue /\ ConsensusTimeValid - /\ ConsensusSafeValidCorrProp - \* /\ ConsensusRealTimeValid - \* /\ ConsensusRealTimeValidCorr - \* /\ BoundedDelay - -\* Liveness == -\* ConsensusTimeLive + /\ TimeLiveness ============================================================================= diff --git a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla b/spec/consensus/proposer-based-timestamp/v1/TendermintPBT_001_draft.tla similarity index 100% rename from spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla rename to spec/consensus/proposer-based-timestamp/v1/TendermintPBT_001_draft.tla