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

spec: Align VoteKeeper spec with the code #84

Merged
merged 2 commits into from
Nov 27, 2023
Merged

spec: Align VoteKeeper spec with the code #84

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0a7d412
chore: Make `quint-forall.sh` script executable
romac Nov 24, 2023
77b211d
spec: Align VoteKeeper spec with the code
romac Nov 24, 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
2 changes: 1 addition & 1 deletion Scripts/quint-forall.sh
100644 → 100755
View file
Open in desktop
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
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 (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
Open in desktop
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
Open in desktop
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"}))

}