From 0a7d41220ee97a30fb9641abf3dfa124ec5f3fc4 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Fri, 24 Nov 2023 15:09:13 +0100 Subject: [PATCH 1/2] chore: Make `quint-forall.sh` script executable --- Scripts/quint-forall.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) mode change 100644 => 100755 Scripts/quint-forall.sh diff --git a/Scripts/quint-forall.sh b/Scripts/quint-forall.sh old mode 100644 new mode 100755 index dc0fb1bd7..6ab2fe003 --- a/Scripts/quint-forall.sh +++ b/Scripts/quint-forall.sh @@ -1,4 +1,4 @@ -#!/bin/env bash +#!/usr/bin/env bash BLUE=$(tput setaf 4) RED=$(tput setaf 1) From 77b211df694dccf92ab89e2ded7f0e1acffc66c4 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Fri, 24 Nov 2023 15:09:29 +0100 Subject: [PATCH 2/2] spec: Align VoteKeeper spec with the code --- Specs/Quint/executor.qnt | 14 +++-- Specs/Quint/voteBookkeeper.qnt | 5 +- Specs/Quint/voteBookkeeperTest.qnt | 86 +++++++++++++++--------------- 3 files changed, 51 insertions(+), 54 deletions(-) diff --git a/Specs/Quint/executor.qnt b/Specs/Quint/executor.qnt index 0984c4014..1a671d071 100644 --- a/Specs/Quint/executor.qnt +++ b/Specs/Quint/executor.qnt @@ -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 = { @@ -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, @@ -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) } @@ -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) @@ -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) diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt index 25b085a3f..cde151a75 100644 --- a/Specs/Quint/voteBookkeeper.qnt +++ b/Specs/Quint/voteBookkeeper.qnt @@ -62,7 +62,6 @@ module voteBookkeeper { type Bookkeeper = { height: Height, - currentRound: Round, totalWeight: Weight, rounds: Round -> RoundVotes } @@ -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 @@ -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) diff --git a/Specs/Quint/voteBookkeeperTest.qnt b/Specs/Quint/voteBookkeeperTest.qnt index ae635f823..4541bb798 100644 --- a/Specs/Quint/voteBookkeeperTest.qnt +++ b/Specs/Quint/voteBookkeeperTest.qnt @@ -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, @@ -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"})) }