diff --git a/Specs/Quint/executor.qnt b/Specs/Quint/executor.qnt index 718dc522c..da46db545 100644 --- a/Specs/Quint/executor.qnt +++ b/Specs/Quint/executor.qnt @@ -10,8 +10,8 @@ module executor { import consensus.* from "./consensus" import voteBookkeeper.* from "./voteBookkeeper" -pure def initBookKeeper (totalVotingPower: int): Bookkeeper = - { height: 0, totalWeight: totalVotingPower, rounds: Map() } +pure def initBookKeeper (currentRound: Round, totalVotingPower: int): Bookkeeper = + { height: 0, currentRound: currentRound, totalWeight: totalVotingPower, rounds: Map() } type ExecutorState = { @@ -30,7 +30,7 @@ type ExecutorState = { pure def initExecutor (v: Address_t, vs: Address_t -> int) : ExecutorState = { val tvp = vs.keys().fold(0, (sum, key) => sum + vs.get(key)) { - bk: initBookKeeper(tvp), + bk: initBookKeeper(0, tvp), cs: initConsensusState(v), proposals: Set(), valset: vs, @@ -149,14 +149,18 @@ pure def ListContains(list, value) = // check whether the event has been already sent to consensus. If not, do so. pure def callConsensus (es: ExecutorState, bk: Bookkeeper, ev: Event) : (ExecutorState, ConsensusOutput) = { - // check whether we already executed the event already + // Check whether we already executed the event already if (es.executedEvents.ListContains((ev, es.cs.height, es.cs.round))) - ( { ...es, bk:bk, cs: es.cs}, - defaultResult ) + ({ ...es, bk: bk, cs: es.cs }, defaultResult) else + // Go to consensus val res = consensus(es.cs, ev) - ( { ...es, bk: bk, cs: res.cs, executedEvents: es.executedEvents.append((ev, res.cs.height, res.cs.round))}, - res.out ) + // Update the round in the vote keeper, in case we moved to a new round + val newBk = { ...bk, currentRound: res.cs.round } + // Record that we executed the event + val events = es.executedEvents.append((ev, res.cs.height, res.cs.round)) + + ({ ...es, bk: newBk, cs: res.cs, executedEvents: events }, res.out) } diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt index 051abf9a0..15d725605 100644 --- a/Specs/Quint/voteBookkeeper.qnt +++ b/Specs/Quint/voteBookkeeper.qnt @@ -62,6 +62,7 @@ module voteBookkeeper { type Bookkeeper = { height: Height, + currentRound: Round, totalWeight: Weight, rounds: Round -> RoundVotes } @@ -183,29 +184,37 @@ module voteBookkeeper { else roundVotes.votesAddressesWeights.mapSafeSet(vote.address, weight) - val threshold = computeThreshold(updatedVoteCount, vote.value) - val event = toEvent(vote.round, vote.typ, threshold) - val finalEvent = - if (not(event.in(roundVotes.emittedEvents))) - event - else if (roundVotes.emittedEvents == Set() and isSkip(updatedVotesAddressesWeights.mapSumValues(), total)) - { round: vote.round, name: "Skip", value: "null" } - else - { round: vote.round, name: "None", value: "null" } - - val updatedEmmittedEvents = roundVotes.emittedEvents.setAddIf(finalEvent, finalEvent.name != "None") - val updatedRoundVotes = if (vote.typ == "Prevote") roundVotes.with("prevotes", updatedVoteCount) else roundVotes.with("precommits", updatedVoteCount) + + // Combined weight of all validators at this height + val combinedWeight = updatedVotesAddressesWeights.mapSumValues() + + val finalEvent = + if (vote.round > keeper.currentRound and isSkip(combinedWeight, total)) + { round: vote.round, name: "Skip", value: "null" } + else + val threshold = computeThreshold(updatedVoteCount, vote.value) + val event = toEvent(vote.round, vote.typ, threshold) + if (not(event.in(roundVotes.emittedEvents))) + event + else + { round: vote.round, name: "None", value: "null" } + + val updatedEmittedEvents = roundVotes.emittedEvents.setAddIf(finalEvent, finalEvent.name != "None") + val updatedRoundVotes2 = updatedRoundVotes .with("votesAddressesWeights", updatedVotesAddressesWeights) - .with("emittedEvents", updatedEmmittedEvents) + .with("emittedEvents", updatedEmittedEvents) + val newBookkeeper = + keeper.with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes2)) + { - bookkeeper: keeper.with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes2)), + bookkeeper: newBookkeeper, event: finalEvent } diff --git a/Specs/Quint/voteBookkeeperTest.qnt b/Specs/Quint/voteBookkeeperTest.qnt index 3ffa98f44..ae635f823 100644 --- a/Specs/Quint/voteBookkeeperTest.qnt +++ b/Specs/Quint/voteBookkeeperTest.qnt @@ -20,8 +20,8 @@ module voteBookkeeperTest { lastEmitted' = lastEmitted, } - action init(totalWeight: Weight): bool = all { - bookkeeper' = { height: 10, totalWeight: totalWeight, rounds: Map() }, + action initWith(round: Round, totalWeight: Weight): bool = all { + bookkeeper' = { height: 10, currentRound: round, totalWeight: totalWeight, rounds: Map() }, lastEmitted' = { round: -1, name: "", value: "null" }, } @@ -44,7 +44,7 @@ module voteBookkeeperTest { // all messages are received in order. We assume three validators in the validator set wtih 60%, 30% and 10% // each of the total voting power run synchronousConsensusTest = - init(100) + initWith(1, 100) .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60)) .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10)) @@ -60,7 +60,7 @@ module voteBookkeeperTest { // Reaching PolkaAny run polkaAnyTest = - init(100) + initWith(1, 100) .then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60)) .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) @@ -68,10 +68,76 @@ module voteBookkeeperTest { // Reaching PolkaNil run polkaNilTest = - init(100) + initWith(1, 100) .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60)) .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) .then(_assert(lastEmitted == {round: 1, name: "PolkaNil", value: "null"})) + // Reaching Skip via n+1 threshold with prevotes from two validators at a future round + run skipSmallQuorumAllPrevotesTest = + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "bob"}, 30)) + .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + + // Cannot reach Skip via f+1 threshold with one prevote and one precommit from the same validator at a future round + run noSkipSmallQuorumMixedVotesSameValTest = + initWith(1, 90) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 20)) + .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 20)) + .then(_assert(lastEmitted != {round: 2, name: "Skip", value: "null"})) + + // Reaching Skip via f+1 threshold with one prevote and one precommit from two validators at a future round + run skipSmallQuorumMixedVotesTwoValsTest = + initWith(1, 80) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 50)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 20)) + .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + + // Reaching Skip via 2f+1 threshold with a single prevote from a single validator at a future round + run skipQuorumSinglePrevoteTest = + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 60)) + .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + + // Reaching Skip via 2f+1 threshold with a single precommit from a single validator at a future round + run skipQuorumSinglePrecommitTest = + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 60)) + .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + + // Cannot reach Skip via 2f+1 threshold with one prevote and one precommit from the same validator at a future round + run noSkipQuorumMixedVotesSameValTest = + initWith(1, 100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 30)) + .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 30)) + .then(_assert(lastEmitted != {round: 2, name: "Skip", value: "null"})) + + // Reaching Skip via 2f+1 threshold with one prevote and one precommit from two validators at a future round + run skipQuorumMixedVotesTwoValsTest = + initWith(1, 80) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 20)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 50)) + .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"})) + }