Skip to content

Commit

Permalink
spec: Align VoteKeeper spec with the code (#84)
Browse files Browse the repository at this point in the history
  • Loading branch information
@romac
romac authored Nov 27, 2023
1 parent a755b7b commit 1c3d844
Show file tree
Hide file tree
Showing 4 changed files with 52 additions and 55 deletions.
2 changes: 1 addition & 1 deletion Scripts/quint-forall.sh
100644 → 100755
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#!/bin/env bash
#!/usr/bin/env bash

BLUE=$(tput setaf 4)
RED=$(tput setaf 1)
Expand Down
14 changes: 6 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 (currentRound: Round, totalVotingPower: int): Bookkeeper =
{ height: 0, currentRound: currentRound, totalWeight: totalVotingPower, rounds: Map() }
pure def initBookKeeper(totalVotingPower: int): Bookkeeper =
{ height: 0, 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(0, tvp),
bk: initBookKeeper(tvp),
cs: initConsensusState(v),
proposals: Set(),
valset: vs,
Expand Down Expand Up @@ -155,12 +155,10 @@ pure def callConsensus (es: ExecutorState, bk: Bookkeeper, ev: Event) : (Executo
else
// Go to consensus
val res = consensus(es.cs, ev)
// 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)
({ ...es, bk: bk, cs: res.cs, executedEvents: events }, res.out)
}


Expand Down Expand Up @@ -483,7 +481,7 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co
res
}
else if (input.name == "votemessage" and input.vote.step == "Precommit") {
val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src))
val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src), es.cs.round)
val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event}
// only a commit event can come here.
val cons_res = Precommit(newES, input, res.event)
Expand All @@ -495,7 +493,7 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co
cons_res
}
else if (input.name == "votemessage" and input.vote.step == "Prevote") {
val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src))
val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src), es.cs.round)
val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event}
// only a commit event can come here.
val cons_res = Prevote(newES, input, res.event)
Expand Down
5 changes: 2 additions & 3 deletions Specs/Quint/voteBookkeeper.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,6 @@ module voteBookkeeper {

type Bookkeeper = {
height: Height,
currentRound: Round,
totalWeight: Weight,
rounds: Round -> RoundVotes
}
Expand Down Expand Up @@ -158,7 +157,7 @@ module voteBookkeeper {
// TO DISCUSS:
// - There might be a problem if we generalize from single-shot to multi-shot: the keeper only keeps the totalWeight
// of the current height; I wonder if we need to keep the totalWeight for every Height that we may receive a vote for.
pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: Weight): { bookkeeper: Bookkeeper, event: ExecutorEvent } =
pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: Weight, currentRound: Round): { bookkeeper: Bookkeeper, event: ExecutorEvent } =
val height = keeper.height
val total = keeper.totalWeight

Expand Down Expand Up @@ -194,7 +193,7 @@ module voteBookkeeper {
val combinedWeight = updatedVotesAddressesWeights.mapSumValues()

val finalEvent =
if (vote.round > keeper.currentRound and isSkip(combinedWeight, total))
if (vote.round > currentRound and isSkip(combinedWeight, total))
{ round: vote.round, name: "Skip", value: "null" }
else
val threshold = computeThreshold(updatedVoteCount, vote.value)
Expand Down
86 changes: 43 additions & 43 deletions Specs/Quint/voteBookkeeperTest.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,13 @@ module voteBookkeeperTest {
lastEmitted' = lastEmitted,
}

action initWith(round: Round, totalWeight: Weight): bool = all {
bookkeeper' = { height: 10, currentRound: round, totalWeight: totalWeight, rounds: Map() },
action initWith(totalWeight: Weight): bool = all {
bookkeeper' = { height: 10, totalWeight: totalWeight, rounds: Map() },
lastEmitted' = { round: -1, name: "", value: "null" },
}

action applyVoteAction(vote: Vote, weight: Weight): bool =
val result = applyVote(bookkeeper, vote, weight)
action applyVoteAction(vote: Vote, weight: Weight, currentRound: Round): bool =
val result = applyVote(bookkeeper, vote, weight, currentRound)
all {
bookkeeper' = result.bookkeeper,
lastEmitted' = result.event,
Expand All @@ -44,100 +44,100 @@ 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 =
initWith(1, 100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60))
initWith(100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10))
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10, 1))
.then(_assert(lastEmitted == {round: 1, name: "PolkaValue", value: "proposal"}))
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "bob"}, 30))
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "bob"}, 30, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "bob"}, 30))
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "bob"}, 30, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "john"}, 10))
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "john"}, 10, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "alice"}, 60))
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "alice"}, 60, 1))
.then(_assert(lastEmitted == {round: 1, name: "PrecommitValue", value: "proposal"}))

// Reaching PolkaAny
run polkaAnyTest =
initWith(1, 100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60))
initWith(100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10))
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10, 1))
.then(_assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"}))

// Reaching PolkaNil
run polkaNilTest =
initWith(1, 100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60))
initWith(100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10))
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10, 1))
.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))
initWith(100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10, 1))
.then(_assert(lastEmitted == {round: 2, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "bob"}, 30))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "bob"}, 30, 1))
.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))
initWith(90)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 20))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 20, 1))
.then(_assert(lastEmitted == {round: 2, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 20))
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 20, 1))
.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))
initWith(80)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 50, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10, 1))
.then(_assert(lastEmitted == {round: 2, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 20))
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 20, 1))
.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))
initWith(100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 60))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 60, 1))
.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))
initWith(100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 60))
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 60, 1))
.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))
initWith(100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 30))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 30, 1))
.then(_assert(lastEmitted == {round: 2, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 30))
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 30, 1))
.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))
initWith(80)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 20, 1))
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10))
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10, 1))
.then(_assert(lastEmitted == {round: 2, name: "None", value: "null"}))
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 50))
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 50, 1))
.then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"}))

}

0 comments on commit 1c3d844

Please sign in to comment.