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 index 159ad5464..393342821 100644 --- a/spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla +++ b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla @@ -61,10 +61,11 @@ INSTANCE TendermintPBT_002_draft WITH MaxTimestamp <- 7, MinTimestamp <- 2, Delay <- 2, - Precision <- 2 + Precision <- 2, + PreloadAllFaultyMsgs <- FALSE \* run Apalache with --cinit=CInit CInit == \* the proposer is arbitrary -- works for safety - Proposer \in [Rounds -> AllProcs] + 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 index 4b08ed27a..2bedb48db 100644 --- a/spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla +++ b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla @@ -61,10 +61,11 @@ INSTANCE TendermintPBT_002_draft WITH MaxTimestamp <- 7, MinTimestamp <- 2, Delay <- 2, - Precision <- 2 + Precision <- 2, + PreloadAllFaultyMsgs <- FALSE \* run Apalache with --cinit=CInit CInit == \* the proposer is arbitrary -- works for safety - Proposer \in [Rounds -> AllProcs] + ArbitraryProposer ============================================================================= diff --git a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla index 31e0a5044..436b9286c 100644 --- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla +++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla @@ -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,11 @@ CONSTANTS ASSUME(N = Cardinality(Corr \union Faulty)) +\* Modeling parameter +CONSTANTS + \* @type: Bool; + PreloadAllFaultyMsgs + (*************************** DEFINITIONS ************************************) \* @type: Set(PROCESS); AllProcs == Corr \union Faulty \* the set of all processes @@ -75,6 +80,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) \* can't call-by-name for built-in operators + IN ApaFoldSet(Append, <<>>, 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 +121,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 +135,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 @@ -272,6 +285,19 @@ BenignRoundsInMessages(msgfun) == \A m \in msgfun[r]: r = m.round +InitMsgs == + \/ /\ PreloadAllFaultyMsgs + /\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals] + /\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes] + /\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits] + /\ BenignRoundsInMessages(msgsPropose) + /\ BenignRoundsInMessages(msgsPrevote) + /\ BenignRoundsInMessages(msgsPrecommit) + \/ /\ ~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] @@ -283,13 +309,8 @@ 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] + /\ InitMsgs /\ proposalReceptionTime = [r \in Rounds, p \in Corr |-> NilTimestamp] - /\ BenignRoundsInMessages(msgsPropose) - /\ BenignRoundsInMessages(msgsPrevote) - /\ BenignRoundsInMessages(msgsPrecommit) /\ evidence = {} /\ action = "Init" /\ beginRound = @@ -306,6 +327,30 @@ Init == ELSE NilTimestamp ] +\* 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; BroadcastProposal(pSrc, pRound, pProposal, pValidRound) == @@ -380,7 +425,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,p] = Min2(@, localClock[p])] + /\ beginRound' = [beginRound EXCEPT ![r,p] = localClock[p]] /\ lastBeginRound' = [lastBeginRound EXCEPT ![r] = Max2(@, localClock[p])] \* lines 14-19, a proposal may be sent later @@ -697,23 +742,24 @@ OnQuorumOfNilPrevotes(p) == \* 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*)>> - /\ 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 + <<(*beginRound,*) endConsensus(*, lastBeginRound*)>> + /\ UNCHANGED + <<(*round, step,*) decision, lockedValue, + lockedRound, validValue, validRound>> + /\ UNCHANGED + <> + /\ action' = "OnRoundCatchup" (********************* PROTOCOL TRANSITIONS ******************************) @@ -764,6 +810,7 @@ MessageProcessing(p) == *) Next == \/ AdvanceRealTime + \/ FaultyBroadcast \/ /\ SynchronizedLocalClocks /\ \E p \in Corr: MessageProcessing(p) @@ -793,7 +840,8 @@ DisagreementOnValue == ConsensusValidValue == \A p \in Corr: \* decision[p] = Decision(Proposal(v,t,pr), r) - LET prop == decision[p][1] IN prop /= NilProposal => IsValid(prop[1]) + 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 @@ -841,12 +889,12 @@ ContainsPrevoteFromCorrect(set) == DerivedProofOfLocks == \A r \in Rounds, prop \in ValidProposals: LET t == prop[2] IN + LET rStar == prop[3] IN LET PS == POLSet(prop, r) IN ( /\ IsValidPOL(PS) /\ ContainsPrevoteFromCorrect(PS) ) => - \E rStar \in Rounds: LET PSStar == POLSet(prop, rStar) IN /\ rStar <= r /\ ContainsPrevoteFromCorrect(PSStar)