diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt index 66441c3f4..c859ac579 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,38 @@ 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) + + val combinedWeight = updatedRoundVotes.prevotes.valuesWeights.getOrElse(vote.value, 0) + + updatedRoundVotes.precommits.valuesWeights.getOrElse(vote.value, 0) + + val finalEvent = + // TODO: do we need to check if we have not emitted any event yet for the vote round? + 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..ac9177dd0 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 init(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) + init(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) + init(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,28 @@ module voteBookkeeperTest { // Reaching PolkaNil run polkaNilTest = - init(100) + init(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 + run skipHonestTest = + init(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"})) + + // Reaching Skip via 2f+1 threshold + run skipQuorumTest = + init(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"})) + }