Skip to content

Commit

Permalink
fix(spec/votekeeper): Fix the VoteKeeper spec to account for skip thr…
Browse files Browse the repository at this point in the history 
…eshold from higher round (#74)
  • Loading branch information
@romac
romac authored Nov 17, 2023
1 parent 8654e59 commit dc2d587
Show file tree
Hide file tree
Showing 3 changed files with 106 additions and 27 deletions.
20 changes: 12 additions & 8 deletions Specs/Quint/executor.qnt
View file
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),
cs: initConsensusState(v),
proposals: Set(),
valset: vs,
Expand Down Expand Up @@ -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)
}


Expand Down
37 changes: 23 additions & 14 deletions Specs/Quint/voteBookkeeper.qnt
View file
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))
{ 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
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 initWith(round: Round, totalWeight: Weight): bool = all {
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)
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))
Expand All @@ -60,18 +60,84 @@ 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))
.then(_assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"}))

// 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"}))

}

0 comments on commit dc2d587

Please sign in to comment.