diff --git a/spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla similarity index 75% rename from spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla rename to spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla index 53f7336fb..159ad5464 100644 --- a/spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla +++ b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla @@ -1,4 +1,4 @@ ------------------------------ MODULE MC_PBT ------------------------------- +----------------------------- MODULE MC_PBT_2C_2F ------------------------------- CONSTANT \* @type: ROUND -> PROCESS; Proposer @@ -38,24 +38,17 @@ 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 VALUE 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 \* Invariant support VARIABLES - \* @type: ROUND -> TIME; + \* @type: <> -> 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 - + lastBeginRound \* the maximum of the local clocks in each round INSTANCE TendermintPBT_002_draft WITH Corr <- {"c1", "c2"}, @@ -64,8 +57,8 @@ INSTANCE TendermintPBT_002_draft WITH T <- 1, ValidValues <- { "v0", "v1" }, InvalidValues <- {"v2"}, - MaxRound <- 5, - MaxTimestamp <- 10, + MaxRound <- 3, + MaxTimestamp <- 7, MinTimestamp <- 2, Delay <- 2, Precision <- 2 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..4b08ed27a --- /dev/null +++ b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla @@ -0,0 +1,70 @@ +----------------------------- 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 + \* @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 + +INSTANCE TendermintPBT_002_draft 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 + +\* run Apalache with --cinit=CInit +CInit == \* the proposer is arbitrary -- works for safety + Proposer \in [Rounds -> AllProcs] + +============================================================================= 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 983c7351b..863ddbf19 100644 --- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla +++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla @@ -166,33 +166,25 @@ 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; + \* @type: <> -> 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 + lastBeginRound \* the maximum of the local clocks in each round invariantVars == - <> + <> (* to see a type invariant, check TendermintAccInv3 *) @@ -294,15 +286,14 @@ Init == /\ 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] + /\ proposalReceptionTime = [r \in Rounds, p \in Corr |-> NilTimestamp] /\ BenignRoundsInMessages(msgsPropose) /\ BenignRoundsInMessages(msgsPrevote) /\ BenignRoundsInMessages(msgsPrecommit) /\ 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}) ELSE MaxTimestamp @@ -314,8 +305,6 @@ Init == THEN Max({localClock[p] : p \in Corr}) ELSE NilTimestamp ] - /\ proposalTime = [r \in Rounds |-> NilTimestamp] - /\ proposalReceivedTime = [r \in Rounds |-> NilTimestamp] (************************ MESSAGE PASSING ********************************) \* @type: (PROCESS, ROUND, PROPOSAL, ROUND) => Bool; @@ -391,7 +380,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])] + /\ beginRound' = [beginRound EXCEPT ![r,p] = Min2(@, localClock[p])] /\ lastBeginRound' = [lastBeginRound EXCEPT ![r] = Max2(@, localClock[p])] \* lines 14-19, a proposal may be sent later @@ -403,7 +392,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 +399,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 invariantVars /\ 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 +424,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 invariantVars /\ action' = "ReceiveProposal" \* lines 22-27 @@ -487,10 +455,17 @@ 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 @@ -502,7 +477,7 @@ UponProposalInPropose(p) == lockedRound, validValue, validRound>> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "UponProposalInPropose" \* lines 28-33 @@ -547,7 +522,7 @@ UponProposalInProposeAndPrevote(p) == lockedRound, validValue, validRound>> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "UponProposalInProposeAndPrevote" \* lines 34-35 + lines 61-64 (onTimeoutPrevote) @@ -568,7 +543,7 @@ UponQuorumOfPrevotesAny(p) == lockedRound, validValue, validRound>> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "UponQuorumOfPrevotesAny" \* lines 36-46 @@ -616,7 +591,7 @@ UponProposalInPrevoteOrCommitAndPrevote(p) == lockedRound, validValue, validRound*)>> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "UponProposalInPrevoteOrCommitAndPrevote" \* lines 47-48 + 65-67 (onTimeoutPrecommit) @@ -632,14 +607,13 @@ UponQuorumOfPrecommitsAny(p) == /\ StartRound(p, round[p] + 1) /\ UNCHANGED temporalVars /\ UNCHANGED - <<(*beginRound,*) endConsensus, (*lastBeginRound,*) - proposalTime, proposalReceivedTime>> + <<(*beginRound,*) endConsensus(*, lastBeginRound*)>> /\ UNCHANGED <<(*round, step,*) decision, lockedValue, lockedRound, validValue, validRound>> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "UponQuorumOfPrecommitsAny" \* lines 49-54 @@ -664,7 +638,7 @@ 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 @@ -679,10 +653,9 @@ UponProposalInPrecommitNoDecision(p) == lockedRound, validValue, validRound>> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ UNCHANGED - <> + <> /\ action' = "UponProposalInPrecommitNoDecision" \* the actions below are not essential for safety, but added for completeness @@ -700,7 +673,7 @@ OnTimeoutPropose(p) == lockedRound, validValue, validRound>> /\ UNCHANGED <> + evidence, proposalReceptionTime>> /\ action' = "OnTimeoutPropose" \* lines 44-46 @@ -718,7 +691,7 @@ OnQuorumOfNilPrevotes(p) == lockedRound, validValue, validRound>> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "OnQuorumOfNilPrevotes" \* lines 55-56 @@ -733,14 +706,13 @@ OnRoundCatchup(p) == /\ StartRound(p, r) /\ UNCHANGED temporalVars /\ UNCHANGED - <<(*beginRound,*) endConsensus, (*lastBeginRound,*) - proposalTime, proposalReceivedTime>> + <<(*beginRound,*) endConsensus(*, lastBeginRound*)>> /\ UNCHANGED <<(*round, step,*) decision, lockedValue, lockedRound, validValue, validRound>> /\ UNCHANGED <> + (*evidence,*) proposalReceptionTime>> /\ action' = "OnRoundCatchup" @@ -810,6 +782,13 @@ AgreementOnValue == /\ decision[p] = Decision(prop, r1) /\ decision[q] = Decision(prop, r2) +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-CONSENSUS-TIME-VALID.0] ConsensusTimeValid == \A p \in Corr: @@ -819,7 +798,7 @@ ConsensusTimeValid == \* then \* TODO: consider tighter bound where beginRound[pr] is replaced \* w/ MedianOfRound[pr] - => (/\ beginRound[pr] - Precision - Delay <= t + => (/\ beginRound[pr,p] - Precision - Delay <= t /\ t <= endConsensus[p] + Precision) \* [PBTS-CONSENSUS-SAFE-VALID-CORR-PROP.0] @@ -831,53 +810,58 @@ ConsensusSafeValidCorrProp == (/\ 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 + => /\ beginRound[pr, p] <= t /\ t <= lastBeginRound[pr] -\* [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) + +\* @type: (PROPOSAL, ROUND) => Set(PREMESSAGE); +POLSet(prop, rnd) == + { msg \in msgsPrevote[rnd]: msg.id = prop} +\* @type: (Set(PREMESSAGE)) => Bool; +IsValidPOL(s) == Cardinality(s) >= THRESHOLD2 + +\* @type: (Set(PREMESSAGE)) => Bool; +ContainsPrevoteFromCorrect(set) == + \E p \in Corr, msg \in set: msg.src = p + +\* [PBS-DERIVED-POL.1] +DerivedProofOfLocks == + \A r \in Rounds, prop \in ValidProposals: + LET t == prop[2] 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) + /\ \E p \in Corr: IsTimely( proposalReceptionTime[rStar, p], t) + + + +\* [PBTS-CONSENSUS-REALTIME-VALID-CORR.0] +\* ConsensusRealTimeValidCorr == TODO? \* [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 +\* ConsensusRealTimeValid == TODO? 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 +\* BoundedDelay == TODO? \* [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] +\* ConsensusTimeLive == TODO? \* a conjunction of all invariants Inv == /\ AgreementOnValue /\ ConsensusTimeValid /\ ConsensusSafeValidCorrProp - \* /\ ConsensusRealTimeValid - \* /\ ConsensusRealTimeValidCorr - \* /\ BoundedDelay + /\ DerivedProofOfLocks \* Liveness == \* ConsensusTimeLive