Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix(spec/votekeeper): Fix the VoteKeeper spec to account for skip threshold from higher round #74

Merged
merged 5 commits into from
Nov 17, 2023
Merged

fix(spec/votekeeper): Fix the VoteKeeper spec to account for skip threshold from higher round #74

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
6339453
fix(spec/votekeeper): Fix the VoteKeeper spec to account for skip thr…
romac Nov 15, 2023
5fbdbec
fix: Fix a bug where we would double count the weight of validators w…
romac Nov 15, 2023
f0bd9f9
Fix executor spec
romac Nov 15, 2023
7fc4287
Update bookkeepers currentRound after calling into consensus
romac Nov 17, 2023
498e081
Rename `init` to `initWith`
romac Nov 17, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Specs/Quint/executor.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {
Expand All @@ -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),
romac marked this conversation as resolved.
Show resolved Hide resolved
cs: initConsensusState(v),
proposals: Set(),
valset: vs,
Expand Down
37 changes: 23 additions & 14 deletions Specs/Quint/voteBookkeeper.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,7 @@ module voteBookkeeper {

type Bookkeeper = {
height: Height,
currentRound: Round,
totalWeight: Weight,
rounds: Round -> RoundVotes
}
Expand Down Expand Up @@ -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))
romac marked this conversation as resolved.
Show resolved Hide resolved
{ 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
}

Expand Down
76 changes: 71 additions & 5 deletions Specs/Quint/voteBookkeeperTest.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
romac marked this conversation as resolved.
Show resolved Hide resolved
bookkeeper' = { height: 10, currentRound: round, totalWeight: totalWeight, rounds: Map() },
lastEmitted' = { round: -1, name: "", value: "null" },
}

Expand All @@ -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))
Expand All @@ -60,18 +60,84 @@ 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))
.then(_assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"}))

// 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 with prevotes from two validators at a future round
run skipSmallQuorumAllPrevotesTest =
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"}))

// Cannot reach Skip via f+1 threshold with one prevote and one precommit from the same validator at a future round
run noSkipSmallQuorumMixedVotesSameValTest =
init(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 =
init(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 =
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"}))

// Reaching Skip via 2f+1 threshold with a single precommit from a single validator at a future round
run skipQuorumSinglePrecommitTest =
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: "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 =
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"}, 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 =
init(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"}))

}