From 9e04f22b383fd7ff9f99142daace1d0ae3e5488e Mon Sep 17 00:00:00 2001 From: Martin Hutle <147692059+martin-hutle@users.noreply.github.com> Date: Thu, 19 Dec 2024 09:35:20 +0100 Subject: [PATCH] feat(spec): New height logic / fast track (#591) * new height logic (fast track) first draft * update on integration into existing spec * fix typos * Update specs/quint/specs/driver.qnt Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> * Update specs/quint/specs/driver.qnt Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> * Update specs/quint/specs/driver.qnt Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> * update initialization of driver as suggested in PR comment * fix/test: first test and fixed new height logic * spelling * fixed proposer selection to include heights and added further new height tests * update tests, fixed bug in height logic, typos * height logic tests (cont.) * merged refactorization into branch, adapted changes * fixed catchUpToHigherRoundAfterHeightChange test * typos * fixed new round in new height logic (proposer case) * fixed issues #670, finished new-height tests * included comments from Josef --------- Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> Co-authored-by: Romain Ruetschi --- specs/consensus/quint/driver.qnt | 166 ++++++++++++- .../tests/newheightlogic/heightLogicTest.qnt | 40 +++ .../tests/newheightlogic/heightLogicrun.qnt | 228 ++++++++++++++++++ 3 files changed, 422 insertions(+), 12 deletions(-) create mode 100644 specs/consensus/quint/tests/newheightlogic/heightLogicTest.qnt create mode 100644 specs/consensus/quint/tests/newheightlogic/heightLogicrun.qnt diff --git a/specs/consensus/quint/driver.qnt b/specs/consensus/quint/driver.qnt index 2da8be8b3..5fda2ed26 100644 --- a/specs/consensus/quint/driver.qnt +++ b/specs/consensus/quint/driver.qnt @@ -3,10 +3,11 @@ module driver { import extraSpells.* from "./spells/extra" + import basicSpells.* from "./spells/basic" import types.* from "./types" import consensus.* from "./consensus" import votekeeper.* from "./votekeeper" - + // ************************************************************************* // State // ************************************************************************* @@ -48,6 +49,139 @@ module driver { pure def setValue(s: NodeState, value: NonNilValue): NodeState = { ...s, nextValueToPropose: Val(value) } + + + // ************************************************************************* + // New Height Logic + // ************************************************************************* + + // *** helper functions ******************/ + + pure def maxRound(S: Set[Round]): Round = + S.fold(0, (x,agg) => max(x,agg)) + + pure def removeMessagesFromOlderHeights(ns: NodeState, height: Height) : NodeState = + val proposals = ns.incomingProposals.filter(v => v.height >= height) + val votes = ns.incomingVotes.filter(v => v.height >= height) + val certificates = ns.incomingCertificates.filter(cert => cert.forall(v => v.height >= height)) + { ... ns, + incomingProposals: proposals, + incomingVotes: votes, + incomingCertificates: certificates } + + + + // getNewHeightAction() manages the fast processing of messages when a new height h is + // started. It is called from nextAction when a the consensus algorithm has not yet started, + // and returns a node state with + // - an updated votekeeper with all votes of this height processed + // - all messages from the previous heights and the current height removed + // - pendingInputs updated with the returned ConsensusInput if there is one + // and a driver input. + // It considers 3 cases: + // 1) there is a proposal+commit certificate for that proposal in any round + // => a PendingDInput with ProposalAndCommitAndValidCInput is returned + // 2) there is a VotekeeperOutput for round r > 0 + // => a PendingDInput with NewRoundCInput is returned + // 3) else + // => only the Votekeeper is updated and StartDInput is returned + + pure def getNewHeightAction(ns: NodeState, vs: ValidatorSet, h: Height): (NodeState, DriverInput) = + val proposalsForHeight = ns.incomingProposals.filter(v => v.height == h) + val votesForHeight = ns.incomingVotes.filter(v => v.height == h) + val maxVotesRound = maxRound(votesForHeight.map( vote => vote.round)) // needed to avoid skip rounds in applyVote + val certificatesForHeight = ns.incomingCertificates.filter(cert => cert.forall(v => v.height == h)) + val maxCertRound = maxRound(certificatesForHeight.map( cert => maxRound(cert.map(vote => vote.round)))) // needed to avoid skip rounds in applyVote + + // init new driver with empty votekeeper + val vkEmpty = initBookKeeper(h, vs) + + // load votekeeper with votes + val vkWithVotes = votesForHeight.fold(vkEmpty, (vk, vote) => + val res = applyVote(vk, vote, maxVotesRound) + res.bookkeeper + ) + + // load votekeeper with certificates + val vkWithCertificates = certificatesForHeight.fold(vkWithVotes, (vk, cert) => + val res = applyCertificate(vk, cert, maxCertRound) + res.bookkeeper + ) + + // check if there is a value to decide: decisionVal is a decision value or Nil + val decisionValAndRound = vkWithCertificates.rounds.keys().fold((Nil, -1), (agg, rNr) => + if (agg._1 != Nil) agg + else { + vkWithCertificates.rounds.get(rNr).emittedOutputs.fold((Nil, -1), (agg2, output) => + match output { + | PrecommitValueVKOutput(value) => + val validProposals = proposalsForHeight.filter(p => p.proposal.isValid() and p.proposal == value._2 and p.srcAddress == proposer(vs,h,rNr)) + if (validProposals != Set()) + (Val(value._2),rNr) + else + agg2 + | _ => agg2 + } + ) + } + ) + + // else compute consensus round to start + val roundToStart = vkWithCertificates.rounds.keys().fold(0, (agg, rNr) => + vkWithCertificates.rounds.get(rNr).emittedOutputs.fold(0, (agg2, output) => + match output { + | PolkaAnyVKOutput(round) => max(round,agg2) + | PolkaNilVKOutput(round) => max(round,agg2) + | PolkaValueVKOutput(output) => max(output._1,agg2) + | PrecommitAnyVKOutput(round) => max(round,agg2) + | PrecommitValueVKOutput(output) => max(output._1,agg2) + | SkipVKOutput(round) => max(round,agg2) + | _ => agg2 + } + ) + ) + + // determine consensus input, needed as parameter in PendingDInput return value and in pendingInputs + val resultInput = if (decisionValAndRound._1 != Nil) + val decisionVal : NonNilValue = getVal(decisionValAndRound._1) + val decisionRound = decisionValAndRound._2 + Set((ProposalAndCommitAndValidCInput((decisionRound, decisionVal)),h, decisionRound)) + else if (roundToStart > 0) + Set((NewRoundCInput(roundToStart), h, -1)) + else + Set() + + val resultDriver = { ...ns.es, bk: vkWithCertificates, pendingInputs: resultInput, started: true } + + val resultAction = if (decisionValAndRound._1 != Nil) + val decisionVal : NonNilValue = getVal(decisionValAndRound._1) + val decisionRound = decisionValAndRound._2 + PendingDInput(ProposalAndCommitAndValidCInput((decisionRound, decisionVal))) + else if (roundToStart > 0) { + if (isProposer({...ns, es:resultDriver}, h, roundToStart)) { + PendingDInput(NewRoundProposerCInput(roundToStart)) + } + else { + PendingDInput(NewRoundCInput(roundToStart)) + } + } + else + StartDInput + + // remove messages from previous heights + val ns2 = ns.removeMessagesFromOlderHeights(h) + + // result state new driver and processed votes and certificates removed + // Note: processed proposals messages are not removed + val resultNodeState = {...ns2, + es: resultDriver, + incomingVotes: ns2.incomingVotes.exclude(votesForHeight), + incomingCertificates: ns2.incomingCertificates.exclude(certificatesForHeight) } + + (resultNodeState, resultAction) + + + // ************************************************************************* // Input / Output // ************************************************************************* @@ -84,11 +218,18 @@ module driver { // a function, that is, any two validators need to agree on this pure def proposer(valset: Address -> Weight, height: Height, round: Round): Address = { // Here: rotating coordinator. We can do something more clever actually using the valset - val prop = (round + 1) % 4 - if (prop == 0) "v1" - else if (prop == 1) "v2" - else if (prop == 2) "v3" - else "v4" + // Update: generalized to arbitrary validator set, same proposer at different heights for test cases + val valList = valset.keys().fold(List(), (s, x) => s.append(x)) + val prop = (round + 1) % length(valList) // start with v2 as before + valList[prop] + // if (prop == 0) "v1" + // else if (prop == 1) "v2" + // else if (prop == 2) "v3" + // else "v4" + } + + pure def isProposer(state: NodeState, height: Height, round: Round) : bool = { + state.es.cs.p == proposer(state.es.bk.validatorSet, height, round) } pure def getValue(state: NodeState): Value = state.nextValueToPropose @@ -218,9 +359,10 @@ module driver { if (newES.cs.step == ProposeStep) val receivedPolkaValidRoundVal = checkThreshold(newES.bk, prop.validRound, Prevote, th) if (prop.validRound == -1) - if (receivedPolkaCurrentVal) - callConsensus(newES, newES.bk, NoCertificate, ProposalAndPolkaAndValidCInput(propId)) - else + // removed (see Issue #670) +// if (receivedPolkaCurrentVal) +// callConsensus(newES, newES.bk, NoCertificate, ProposalAndPolkaAndValidCInput(propId)) +// else callConsensus(newES, newES.bk, NoCertificate, ProposalCInput((prop.round, propId))) else if (receivedPolkaValidRoundVal) callConsensus(newES, newES.bk, NoCertificate, ProposalAndPolkaPreviousAndValidCInput((propId, prop.validRound))) @@ -428,7 +570,7 @@ module driver { incomingSyncProposals: Set(), incomingSyncCertificates: Set(), getValueRequests: Set(), - nextValueToPropose: Nil, + nextValueToPropose: Nil, } pure def existsTimeout(state: NodeState): bool = @@ -458,7 +600,7 @@ module driver { val syncProposalsForCurrentHeight = state.incomingSyncProposals.filter(p => p.height == state.es.cs.height) if (not(state.es.started)) - (state, StartDInput) + getNewHeightAction(state, state.es.valset, state.es.cs.height) else if (syncCertificatesForCurrentHeight != Set()) // val cert = syncCertificatesForCurrentHeight.chooseSome() @@ -535,7 +677,7 @@ module driver { val syncCertificatesForCurrentHeight = state.incomingSyncCertificates.filter(cert => cert.forall(v => v.height == state.es.cs.height)) val syncProposalsForCurrentHeight = state.incomingSyncProposals.filter(p => p.height == state.es.cs.height) if (command == StartCmd and not(state.es.started)) - (state, StartDInput) + getNewHeightAction(state, state.es.valset, state.es.cs.height) else if (command == ProposeValueCmd and state.getValueRequests.contains((state.es.cs.height, state.es.cs.round))) val newstate = { ...state, getValueRequests: state.getValueRequests.exclude(Set((state.es.cs.height, state.es.cs.round)))} diff --git a/specs/consensus/quint/tests/newheightlogic/heightLogicTest.qnt b/specs/consensus/quint/tests/newheightlogic/heightLogicTest.qnt new file mode 100644 index 000000000..5904121fc --- /dev/null +++ b/specs/consensus/quint/tests/newheightlogic/heightLogicTest.qnt @@ -0,0 +1,40 @@ +module heightLogicTest { + +import heightLogicrun ( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Map("v1" -> 1, "v2" -> 1, "v3" -> 1, "v4" -> 1), + Faulty = Set(), + Values = Set("a", "b", "c"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0, 1), + slow = "v4" +) as SLOW1 from "./heightLogicrun" + +run fastProcessesDecidesAtHeight0SlowOneCatchesUpTest = { + SLOW1::fastProcessesDecidesAtHeight0SlowOneCatchesUp +} + +run everyoneIsFastInRound0Test = { + SLOW1::everyoneIsFastInRound0 +} + +run multiHeightRunTest = { + SLOW1::multiHeightRun +} + +run slowProcessAtHeight1Test = { + SLOW1::slowProcessAtHeight1 +} + +run catchUpToHigherRoundTest = { + SLOW1::catchUpToHigherRound +} + +run catchUpToHigherRoundAfterHeightChangeTest = { + SLOW1::catchUpToHigherRoundAfterHeightChange +} + +run preloadVotekeeperOnlyTest = { + SLOW1::preloadVotekeeperOnly +} +} \ No newline at end of file diff --git a/specs/consensus/quint/tests/newheightlogic/heightLogicrun.qnt b/specs/consensus/quint/tests/newheightlogic/heightLogicrun.qnt new file mode 100644 index 000000000..236ec4ace --- /dev/null +++ b/specs/consensus/quint/tests/newheightlogic/heightLogicrun.qnt @@ -0,0 +1,228 @@ +module heightLogicrun { + +import TendermintDSL.* from "../../TendermintDSL" +export TendermintDSL.* + +const slow : Address + +val fastSet = Correct.exclude(Set(slow)) +val fastList = fastSet.fold(List(), (s, x) => s.append(x)) +val ValueList = Values.fold(List(), (s, x) => s.append(x)) + +// ************************************************************************* +// state predicates +// ************************************************************************* + +def threeProcessesHaveDecided(h: Height) : bool = { + size(system.keys().filter(validator => length(system.get(validator).es.chain) > h)) >= 3 +} + +def allProcessesHaveDecided(h: Height) : bool = { + size(system.keys().filter(validator => length(system.get(validator).es.chain) > h)) == size(system.keys()) +} + +def listIsAtHeight(list: List[Address], h: Height) : bool = { + length(list.select(validator => system.get(validator).es.cs.height == h)) == length(list) +} + +def isAtHeight(vals: Set[Address], h: Height) : bool = { + size(vals.filter(validator => system.get(validator).es.cs.height == h)) == size(vals) +} + +// ************************************************************************* +// DSL extension for heights +// ************************************************************************* + +run ListNewHeight(active, valset, h) = { + active.length().reps(i => newHeightAction(active[i], valset, h)) + +} + +run fastProcessesDecideAtHeight(h : Height, value: NonNilValue) : bool = { + // all processes in fastList are synchronous in round 0 of height h + // slow process has all messages in incomingVotes/incomingProposal but takes no step + val prop = proposer(validatorSet, h, 0) + setNextValueToPropose(prop, value) + .then(reps(2, _ => ListTakeAStep(fastList))) + .then(ListDeliverProposal(validatorList,mkProposal(prop, h, 0, value, -1))) + .then(ListTakeAStep(fastList)) + .then(ListDeliverAllVotes (Prevote, fastList, validatorList, validatorSet, h, 0, Val(value))) + .then(reps(length(fastList) + 2, _ => ListTakeAStep(fastList))) // why +2 and not +1 steps?? + .then(ListDeliverAllVotes (Precommit, fastList, validatorList, validatorSet, h, 0, Val(value))) + .then(reps(length(fastList) + 1, _ => ListTakeAStep(fastList))) + .expect(threeProcessesHaveDecided(h)) +} + +run everyoneIsFastInRound(h: Height, r: Round, value: NonNilValue) : bool = { + val prop = proposer(validatorSet, h, r) + setNextValueToPropose(prop, value) + .then(reps(2, _ => ListTakeAStep(validatorList))) + .then(ListDeliverProposal(validatorList,mkProposal(prop, h, 0, value, -1))) + .then(ListTakeAStep(validatorList)) + .then(ListDeliverAllVotes (Prevote, validatorList, validatorList, validatorSet, h, 0, Val(value))) + .then(reps(length(validatorList) + 2, _ => ListTakeAStep(validatorList))) // why +2 and not +1 steps? + .then(ListDeliverAllVotes (Precommit, validatorList, validatorList, validatorSet, h, 0, Val(value))) + .then(reps(length(validatorList) + 1, _ => ListTakeAStep(validatorList))) + .expect(allProcessesHaveDecided(0)) +} + +run fastProcessesDoNotDecide(h: Height, r: Round, value: NonNilValue, value2: NonNilValue) : bool = { + //val nextProposer = proposer(validatorSet, h, 1) + val thisProposer = proposer(validatorSet, h, r) + init + .then(onlyProposerReceivesProposal(fastList, validatorList, validatorSet, h, r, value)) + .then(ListDeliverAllVotes(Prevote, List(thisProposer), fastList, validatorSet, h, r, Val(value))) + .then(ListDeliverAllVotes(Prevote, fastList.select(x => x != thisProposer), fastList, validatorSet, h, r, Nil)) + .then(fastList.length().reps(_ => ListTakeAStep(fastList))) + .then(all{ + assert(SetFromList(fastList).forall(proc => system.get(proc).timeouts.contains((PrevoteTimeout, h, r)))), + ListTakeAStep(fastList) + }) + .then(all{ + assert(SetFromList(fastList).forall(proc => system.get(proc).es.pendingStepChange == PrecommitStep)), + ListTakeAStep(fastList) + }) + .then(ListDeliverAllVotes(Precommit, fastList, fastList, validatorSet, h, r, Nil)) + .then(fastList.length().reps(_ => ListTakeAStep(fastList))) + // FastList now go to next round on timeoutPrecommit + .then(all{ + assert(SetFromList(fastList).forall(proc => system.get(proc).timeouts.contains((PrecommitTimeout, h, r)))), + everyoneReceivesProposal (fastList, validatorList, validatorSet, h, r + 1, value2) + }) + .then(fromPrevoteToPrecommit(fastList, fastList, validatorList, validatorSet, r, r + 1, Val(value2))) + .then(ListDeliverAllVotes(Precommit, fastList, fastList, validatorSet, h, r+ 1, Val(value2))) + .then(fastList.length().reps(_ => ListTakeAStep(fastList))) + .then(all { + assert(SetFromList(fastList).forall(proc => system.get(proc).es.chain[h].decision.proposal == value2)), + unchangedAll + }) +} + +// ************************************************************************* +// Test runs +// ************************************************************************* + +// simple normal case run +run everyoneIsFastInRound0 = { + init + .then(everyoneIsFastInRound(0, 0, ValueList[0])) +} + +// simple normal case multi-height run +run multiHeightRun = { + init + .then(everyoneIsFastInRound(0, 0, ValueList[0])) + .then(ListNewHeight(validatorList, validatorSet, 1)) + .then(everyoneIsFastInRound(1, 0, ValueList[1])) +} + +// catch up at same height +run fastProcessesDecidesAtHeight0SlowOneCatchesUp = { + // all processes are correct, v4 is slow + // the fast process decide in round 0 + // then the slow process starts at height 0, round 0 + // it is expected that + init + .then(fastProcessesDecideAtHeight(0, ValueList[0])) + + // now v4 catches up + .then(valStep(slow)) + .then(valStep(slow)) + .expect(allProcessesHaveDecided(0)) +} + +// catch up at new height (2f+1 precommits) +run slowProcessAtHeight1 = { + // all processes are fast at height 0 + // fast processes enter height 1 and decide + // slow process catches up with decision in O(1) steps + init + .then(everyoneIsFastInRound(0, 0, ValueList[0])) + .then(ListNewHeight(fastList, validatorSet, 1)) + .expect(listIsAtHeight(fastList, 1)) + .expect(listIsAtHeight([slow], 0)) + .then(fastProcessesDecideAtHeight(1, ValueList[1])) + .expect(listIsAtHeight([slow], 0)) + // now v4 enters height 1 + .then(ListNewHeight([slow], validatorSet, 1)) + .then(valStep(slow)) + .then(valStep(slow)) + .expect(allProcessesHaveDecided(1)) +} + +// catch up to higher round (same height) +run catchUpToHigherRound = { + init + .then(fastProcessesDoNotDecide(0, 0, ValueList[0], ValueList[1])) + // deliver all prevotes of round 0 and 1 + .then(ListDeliverAllVotes(Prevote, ["v1", "v3"], [slow], validatorSet, 0, 0, Nil)) + .then(ListDeliverAllVotes(Prevote, ["v2"], [slow], validatorSet, 0, 0, Val("a"))) + .then(ListDeliverAllVotes(Prevote, fastList, [slow], validatorSet, 0, 1, Val("b"))) + .then(valStep(slow)) + .then(valStep(slow)) + .then(valStep(slow)) +} + +// catch up to higher round (new height) +run catchUpToHigherRoundAfterHeightChange = { + val h1r0proposer = proposer(validatorSet, 1, 0) + val value = "a" + val value2 = "b" + + init + // height 0 + .then(everyoneIsFastInRound(0, 0, ValueList[0])) + .expect(allProcessesHaveDecided(0)) + .then(ListNewHeight(fastList, validatorSet, 1)) + + // height 1 with unsuccessful round 0 + .then(onlyProposerReceivesProposal(fastList, validatorList, validatorSet, 1, 0, value)) + .then(ListDeliverAllVotes(Prevote, List(h1r0proposer), fastList, validatorSet, 1, 0, Val(value))) + .then(ListDeliverAllVotes(Prevote, fastList.select(x => x != h1r0proposer), fastList, validatorSet, 1, 0, Nil)) + .then(fastList.length().reps(_ => ListTakeAStep(fastList))) + .then(all{ + assert(SetFromList(fastList).forall(proc => system.get(proc).timeouts.contains((PrevoteTimeout, 1, 0)))), + ListTakeAStep(fastList) + }) + .then(all{ + assert(SetFromList(fastList).forall(proc => system.get(proc).es.pendingStepChange == PrecommitStep)), + ListTakeAStep(fastList) + }) + .then(ListDeliverAllVotes(Precommit, fastList, fastList, validatorSet, 1, 0, Nil)) + .then(fastList.length().reps(_ => ListTakeAStep(fastList))) + // FastList now go to next round on timeoutPrecommit + .then(all{ + assert(SetFromList(fastList).forall(proc => system.get(proc).timeouts.contains((PrecommitTimeout, 1, 0)))), + everyoneReceivesProposal (fastList, validatorList, validatorSet, 1, 1, value2) + }) + .then(fromPrevoteToPrecommit(fastList, fastList, validatorList, validatorSet, 1, 1, Val(value2))) + .then(ListDeliverAllVotes(Precommit, fastList, fastList, validatorSet, 1, 1, Val(value2))) + .then(ListNewHeight([slow], validatorSet, 1)) + .then(ListDeliverAllVotes(Precommit, fastList, [slow], validatorSet, 1, 0, Nil)) + .then(ListDeliverAllVotes(Prevote, fastList, [slow], validatorSet, 1, 1, Val(value2))) + .then(ListDeliverAllVotes(Precommit, fastList, [slow], validatorSet, 1, 1, Val(value2))) + .then(valStep(slow)) + .expect(system.get(slow).es.cs.round == 1) +} + +run preloadVotekeeperOnly = { + val prop = proposer(validatorSet, 0, 0) + val value = "a" + init + .then(setNextValueToPropose(prop, value)) + .then(reps(2, _ => ListTakeAStep(fastList))) + .then(ListDeliverProposal(validatorList,mkProposal(prop, 0, 0, value, -1))) + .then(ListTakeAStep(fastList)) + .then(ListDeliverAllVotes (Prevote, fastList, validatorList, validatorSet, 0, 0, Val(value))) + // now slow catches up + // new height logic (StartDInput) + .then(valStep(slow)) + // StepChangeDInput + .then(valStep(slow)) + // ProposalDInput + .then(valStep(slow)) + .then(valStep(slow)) + .expect(system.get(slow).es.cs.step == PrecommitStep) +} +} +