diff --git a/Specs/Quint/extraSpells.qnt b/Specs/Quint/extraSpells.qnt index b0444ed17..a0fb9b7cc 100644 --- a/Specs/Quint/extraSpells.qnt +++ b/Specs/Quint/extraSpells.qnt @@ -115,6 +115,22 @@ module extraSpells { assert(Set(3) == Set(3).setAdd(3)), } + /// Add a set element only if a condition is true. + /// + /// - @param __set a set to add an element to + /// - @param __elem an element to add + /// - @param __cond a condition that must be true to add the element to the set + /// - @returns a new set that contains all elements of __set and __elem, if __cond is true + pure def setAddIf(__set: Set[a], __elem: a, __cond: bool): Set[a] = + if (__cond) __set.setAdd(__elem) else __set + + run setAddIfTest = all { + assert(Set(2, 3, 4, 5) == Set(2, 3, 4).setAddIf(5, true)), + assert(Set(2, 3, 4) == Set(2, 3, 4).setAddIf(5, false)), + assert(Set(3) == Set(3).setAddIf(3, true)), + assert(Set(3) == Set(3).setAddIf(3, false)), + } + /// Safely set a map entry. /// /// - @param __map a map to set an entry to @@ -160,11 +176,24 @@ module extraSpells { /// plus the ones in __entries pure def mapAddSet(__map: a -> int, __entries: a -> int): a -> int = { __map.keys().union(__entries.keys()).mapBy(__k => if (__map.has(__k) and __entries.has(__k)) __map.get(__k) + __entries.get(__k) - else if (__map.has(__k)) __map.get(__k) else __entries.get(__k)) + else if (__map.has(__k)) __map.get(__k) else __entries.get(__k)) } run mapAddSetTest = all { assert(Map(2 -> 3, 4 -> 5, 7 -> 8).mapAddSet(Map(3 -> 6, 8 -> 9)) == Map(2 -> 3, 4 -> 5, 3 -> 6, 7 -> 8, 8 -> 9)), assert(Map(2 -> 3, 4 -> 5, 7 -> 8).mapAddSet(Map(3 -> 6, 7 -> 9)) == Map(2 -> 3, 4 -> 5, 3 -> 6, 7 -> 17)), } + + /// Compute the sum of all values in the map. + /// + /// - @param __map a map with values of type int + /// - @returns the sum of the values of all entries in __map + pure def mapSumValues(__map: a -> int): int = + __map.keys().fold(0, (__acc, __val) => __acc + __map.get(__val)) + + run mapSumValuesTest = all { + assert(0 == Map().mapSumValues()), + assert(6 == Map("a" -> 0, "b" -> 1, "c" -> 2, "d" -> 3).mapSumValues()), + } + } \ No newline at end of file diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt index b43607b1d..66441c3f4 100644 --- a/Specs/Quint/voteBookkeeper.qnt +++ b/Specs/Quint/voteBookkeeper.qnt @@ -21,12 +21,13 @@ module voteBookkeeper { // A value is a string type Value = str - // Weigth is an integer + // Weight is an integer type Weight = int - // The vote type + type VoteType = str + type Vote = { - typ: str, + typ: VoteType, round: Round, value: Value, address: Address @@ -72,62 +73,83 @@ module voteBookkeeper { // Internal functions // creates a new voteCount - pure def newVoteCount(total: Weight): VoteCount = { - {totalWeight: total, valuesWeights: Map(), votesAddresses: Set()} - } + pure def newVoteCount(total: Weight): VoteCount = + { totalWeight: total, valuesWeights: Map(), votesAddresses: Set() } // Returns true if weight > 2/3 * total (quorum: at least f+1 correct) - pure def isQuorum(weight: int, total: int): bool = { + pure def isQuorum(weight: Weight, total: Weight): bool = 3 * weight > 2 * total - } + + // True iff the vote count has a quorum on a specific value. + pure def hasQuorumOnValue(voteCount: VoteCount, value: Value): bool = + isQuorum(voteCount.valuesWeights.getOrElse(value, 0), voteCount.totalWeight) + + // True iff the vote count has a quorum on any value. + pure def hasQuorumOnAny(voteCount: VoteCount): bool = + isQuorum(voteCount.valuesWeights.mapSumValues(), voteCount.totalWeight) // Returns true if weight > 1/3 * total (small quorum: at least one correct) - pure def isSkip(weight: int, total: int): bool = { + pure def isSkip(weight: Weight, total: Weight): bool = 3 * weight > total - } + // Adds a vote of weight weigth to a voteCount if there is not vote registered for the voter. - pure def addVote(voteCount: VoteCount, vote: Vote, weight: Weight): VoteCount = { - if (vote.address.in(voteCount.votesAddresses)) voteCount - else val newWeight = voteCount.valuesWeights.getOrElse(vote.value, 0) + weight - voteCount.with("valuesWeights", voteCount.valuesWeights.mapSafeSet(vote.value, newWeight)) - .with("votesAddresses", voteCount.votesAddresses.setAdd(vote.address)) - } + pure def addVote(voteCount: VoteCount, vote: Vote, weight: Weight): VoteCount = + if (vote.address.in(voteCount.votesAddresses)) + // Do not count vote if address has already voted. + voteCount + else + val newWeight = voteCount.valuesWeights.getOrElse(vote.value, 0) + weight + voteCount + .with("valuesWeights", voteCount.valuesWeights.mapSafeSet(vote.value, newWeight)) + .with("votesAddresses", voteCount.votesAddresses.setAdd(vote.address)) // Given a voteCount and a value, the function returns: // - A threshold Value if there is a quorum for the given value; // - A threshold Nil if there is a quorum for the nil and no quorum for the value; // - A threshold Any if there is no quorum for the value or nil and there is a quroum for any (including nil); // - A threshold Unreached otherwise indicating that no quorum has been yet reached. - pure def computeThreshold(voteCount: VoteCount, value: Value): Threshold = { - val weight = voteCount.valuesWeights.getOrElse(value, 0) - val totalWeight = voteCount.totalWeight - val sumWeight = voteCount.valuesWeights.keys().fold(0, (sum, v) => sum + voteCount.valuesWeights.get(v)) - if (value != "nil" and isQuorum(weight, totalWeight)) {name: "Value", value: value} - else if (value == "nil" and isQuorum(weight, totalWeight)) {name: "Nil", value: "null"} - else if (isQuorum(sumWeight, totalWeight)) {name: "Any", value: "null"} - else {name: "Unreached", value: "null"} - } - - // Given a round, voteType and threshold it resturns the corresponding ExecutorEvent - pure def toEvent(round: Round, voteType: str, threshold: Threshold): ExecutorEvent = { - if (threshold.name == "Unreached") {round: round, name: "None", value: "null"} - else if (voteType == "Prevote" and threshold.name == "Value") {round: round, name: "PolkaValue", value: threshold.value} - else if (voteType == "Prevote" and threshold.name == "Nil") {round: round, name: "PolkaNil", value: "null"} - else if (voteType == "Prevote" and threshold.name == "Any") {round: round, name: "PolkaAny", value: "null"} - else if (voteType == "Precommit" and threshold.name == "Value") {round: round, name: "PrecommitValue", value: threshold.value} - else if (voteType == "Precommit" and threshold.name == "Any") {round: round, name: "PrecommitAny", value: "null"} - else if (voteType == "Precommit" and threshold.name == "Nil") {round: round, name: "PrecommitAny", value: "null"} - else if (threshold.name == "Skip") {round: round, name: "Skip", value: "null"} - else {round: round, name: "None", value: "null"} - } - - + pure def computeThreshold(voteCount: VoteCount, value: Value): Threshold = + if (voteCount.hasQuorumOnValue(value)) { + if (value == "nil") + { name: "Nil", value: "null" } + else + { name: "Value", value: value } + } else if (voteCount.hasQuorumOnAny()) { + { name: "Any", value: "null" } + } else + { name: "Unreached", value: "null" } + + // Given a round, voteType and threshold, return the corresponding ExecutorEvent + pure def toEvent(round: Round, voteType: VoteType, threshold: Threshold): ExecutorEvent = + if (threshold.name == "Unreached") + { round: round, name: "None", value: "null" } + + // prevote + else if (voteType == "Prevote" and threshold.name == "Value") + { round: round, name: "PolkaValue", value: threshold.value } + else if (voteType == "Prevote" and threshold.name == "Nil") + { round: round, name: "PolkaNil", value: "null" } + else if (voteType == "Prevote" and threshold.name == "Any") + { round: round, name: "PolkaAny", value: "null" } + + // precommit + else if (voteType == "Precommit" and threshold.name == "Value") + { round: round, name: "PrecommitValue", value: threshold.value } + else if (voteType == "Precommit" and threshold.name == "Any") + { round: round, name: "PrecommitAny", value: "null" } + else if (voteType == "Precommit" and threshold.name == "Nil") + { round: round, name: "PrecommitAny", value: "null" } + + else if (threshold.name == "Skip") + { round: round, name: "Skip", value: "null" } + + else + { round: round, name: "None", value: "null" } // Executor interface - type BKResult = {bookkeeper: Bookkeeper, event: ExecutorEvent} - + type BKResult = { bookkeeper: Bookkeeper, event: ExecutorEvent } - // Called by the executor when it receives a vote. The functiojn takes the following steps: + // Called by the executor when it receives a vote. The function takes the following steps: // - It first adds the vote and then computes a threshold. // - If there exist a threshold and has not emitted before, the function returns the corresponsing ExecutorEvent. // - Othewise, the function returns a no-threshold event. @@ -135,53 +157,75 @@ 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: int): {bookkeeper: Bookkeeper, event: ExecutorEvent} = { + pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: Weight): { bookkeeper: Bookkeeper, event: ExecutorEvent } = val height = keeper.height val total = keeper.totalWeight - val roundVotes = keeper.rounds.getOrElse(vote.round, {height: height, - round: vote.round, - prevotes: newVoteCount(total), - precommits: newVoteCount(total), - emittedEvents: Set(), - votesAddressesWeights: Map()}) - val updatedVoteCount = if (vote.typ == "Prevote") roundVotes.prevotes.addVote(vote, weight) - else roundVotes.precommits.addVote(vote, weight) + + val defaultRoundVotes = { + height: height, + round: vote.round, + prevotes: newVoteCount(total), + precommits: newVoteCount(total), + emittedEvents: Set(), + votesAddressesWeights: Map() + } + val roundVotes = keeper.rounds.getOrElse(vote.round, defaultRoundVotes) + + val updatedVoteCount = + if (vote.typ == "Prevote") + roundVotes.prevotes.addVote(vote, weight) + else + roundVotes.precommits.addVote(vote, weight) + + val updatedVotesAddressesWeights = + if (roundVotes.votesAddressesWeights.has(vote.address)) + roundVotes.votesAddressesWeights + else + roundVotes.votesAddressesWeights.mapSafeSet(vote.address, weight) + val threshold = computeThreshold(updatedVoteCount, vote.value) val event = toEvent(vote.round, vote.typ, threshold) - val updatedVotesAddressesWeights = if (roundVotes.votesAddressesWeights.has(vote.address)) roundVotes.votesAddressesWeights - else roundVotes.votesAddressesWeights.mapSafeSet(vote.address, weight) - val sumSkip = updatedVotesAddressesWeights.keys().fold(0, (sum, v) => sum + updatedVotesAddressesWeights.get(v)) - val finalEvent = if (not(event.in(roundVotes.emittedEvents))) event - else if (roundVotes.emittedEvents == Set() and isSkip(sumSkip, total)) {round: vote.round, name: "Skip", value: "null"} - else {round: vote.round, name: "None", value: "null"} - val updatedRoundVotes = if (vote.typ == "Prevote") roundVotes.with("prevotes", updatedVoteCount) - else roundVotes.with("precommits", updatedVoteCount) - val updatedEmmittedEvents = if (finalEvent.name != "None") roundVotes.emittedEvents.setAdd(finalEvent) - else roundVotes.emittedEvents - val updatedBookkeeper = keeper.with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes.with("votesAddressesWeights", updatedVotesAddressesWeights) - .with("emittedEvents", updatedEmmittedEvents))) - {bookkeeper: updatedBookkeeper, event: finalEvent} - } + 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) + val updatedRoundVotes2 = updatedRoundVotes + .with("votesAddressesWeights", updatedVotesAddressesWeights) + .with("emittedEvents", updatedEmmittedEvents) + + { + bookkeeper: keeper.with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes2)), + event: finalEvent + } // Called by the executor to check if there is a specific threshold for a given round and voteType. // TO DISCUSS: // - The function does not consider Skip threshold. This because if the executor receives a Skip event // and do not act on it, this means that it will never do it in the future. We should discuss that this // is the case. - pure def checkThreshold(keeper: Bookkeeper, round: Round, voteType: str, threshold: Threshold): bool = { + pure def checkThreshold(keeper: Bookkeeper, round: Round, voteType: VoteType, threshold: Threshold): bool = if (keeper.rounds.has(round)) { val roundVotes = keeper.rounds.get(round) - val voteCount = if (voteType == "Prevote") roundVotes.prevotes - else roundVotes.precommits - val total = voteCount.totalWeight - val sumWeight = voteCount.valuesWeights.keys().fold(0, (sum, v) => sum + voteCount.valuesWeights.get(v)) - if (threshold.name == "Value") isQuorum(voteCount.valuesWeights.getOrElse(threshold.value, 0), total) - else if (threshold.name == "Nil") isQuorum(voteCount.valuesWeights.getOrElse("nil", 0), total) - else if (threshold.name == "Any") isQuorum(sumWeight, total) - else false + val voteCount = if (voteType == "Prevote") roundVotes.prevotes else roundVotes.precommits + if (threshold.name == "Value") { + voteCount.hasQuorumOnValue(threshold.value) + } else if (threshold.name == "Nil") { + voteCount.hasQuorumOnValue("nil") + } else if (threshold.name == "Any") { + voteCount.hasQuorumOnAny() + } else false } else false - } - // run PrecommitTest = all { // val bin : Bookkeeper = { @@ -227,7 +271,7 @@ module voteBookkeeper { assert(isSkip(3,6) == true) } - run addVoteTest = { + run addVoteTest = val voteCount = {totalWeight: 100, valuesWeights: Map("val1" -> 30, "val2" -> 20), votesAddresses: Set("alice", "bob")} val vote = {typ: "precommit", round: 10, value: "val3", address: "john"} all { @@ -238,14 +282,12 @@ module voteBookkeeper { // existing voter assert(addVote(voteCount, vote.with("address", "alice"), 10) == voteCount), } - } - run computeThresholdTest = { + run computeThresholdTest = val voteCount = {totalWeight: 100, valuesWeights: Map(), votesAddresses: Set("alice", "bob")} val mapValueReached = Map("val1" -> 67, "val2" -> 20) val mapNilReached = Map("nil" -> 70, "val2" -> 20) val mapNoneReached = Map("nil" -> 20, "val2" -> 20) - all { assert(computeThreshold(voteCount, "val3") == {name: "Unreached", value: "null"}), assert(computeThreshold(voteCount.with("valuesWeights", mapValueReached), "val1") == {name: "Value", value: "val1"}), @@ -255,9 +297,8 @@ module voteBookkeeper { assert(computeThreshold(voteCount.with("valuesWeights", mapNoneReached), "val1") == {name: "Unreached", value: "null"}), assert(computeThreshold(voteCount.with("valuesWeights", mapNoneReached), "nil") == {name: "Unreached", value: "null"}), } - } - run toEventTest = { + run toEventTest = val thresholdUnreached = {name: "Unreached", value: "null"} val thresholdAny = {name: "Any", value: "null"} val thresholdNil = {name: "Nil", value: "null"} @@ -278,7 +319,5 @@ module voteBookkeeper { assert(toEvent(round, "Precommit", {name: "Error", value: "null"}) == {round: round, name: "None", value: "null"}), assert(toEvent(round, "Error", thresholdAny) == {round: round, name: "None", value: "null"}), } - } - -} \ No newline at end of file +} diff --git a/Specs/Quint/voteBookkeeperTest.qnt b/Specs/Quint/voteBookkeeperTest.qnt index 3fbf034f2..3ffa98f44 100644 --- a/Specs/Quint/voteBookkeeperTest.qnt +++ b/Specs/Quint/voteBookkeeperTest.qnt @@ -1,6 +1,6 @@ module voteBookkeeperTest { -import voteBookkeeper.* from "./voteBookkeeper" + import voteBookkeeper.* from "./voteBookkeeper" // **************************************************************************** // State machine state @@ -16,62 +16,62 @@ import voteBookkeeper.* from "./voteBookkeeper" // **************************************************************************** action allUnchanged: bool = all { - bookkeeper' = bookkeeper, - lastEmitted' = lastEmitted + bookkeeper' = bookkeeper, + lastEmitted' = lastEmitted, } action init(totalWeight: Weight): bool = all { - bookkeeper' = {height: 10, totalWeight: totalWeight, rounds: Map()}, - lastEmitted' = {round: -1, name: "", value: "null"} + bookkeeper' = { height: 10, totalWeight: totalWeight, rounds: Map() }, + lastEmitted' = { round: -1, name: "", value: "null" }, } - action applyVoteAction(vote: Vote, weight: Weight): bool = all { + action applyVoteAction(vote: Vote, weight: Weight): bool = val result = applyVote(bookkeeper, vote, weight) all { bookkeeper' = result.bookkeeper, - lastEmitted' = result.event - } - } + lastEmitted' = result.event, + } // **************************************************************************** // Test traces // **************************************************************************** + // auxiliary action for tests + action _assert(predicate: bool): bool = + all { predicate, allUnchanged } + // Consensus full execution with all honest validators (including the leader) and a synchronous network: // 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 = { + run synchronousConsensusTest = init(100) .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "PolkaValue", value: "proposal"}), allUnchanged }) + .then(_assert(lastEmitted == {round: 1, name: "PolkaValue", value: "proposal"})) .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "bob"}, 30)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "bob"}, 30)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "alice"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "PrecommitValue", value: "proposal"}), allUnchanged }) - } + .then(_assert(lastEmitted == {round: 1, name: "PrecommitValue", value: "proposal"})) // Reaching PolkaAny - run polkaAnyTest = { + run polkaAnyTest = init(100) .then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"}), allUnchanged }) - } + .then(_assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"})) // Reaching PolkaNil - run polkaNilTest = { + run polkaNilTest = init(100) .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "PolkaNil", value: "null"}), allUnchanged }) - } + .then(_assert(lastEmitted == {round: 1, name: "PolkaNil", value: "null"})) -} \ No newline at end of file +}