Skip to content

Commit

Permalink
Pass over the votekeeper spec
Browse files Browse the repository at this point in the history
  • Loading branch information
@hvanz
hvanz committed Nov 14, 2023
1 parent 5991bba commit 518053d
Show file tree
Hide file tree
Showing 3 changed files with 181 additions and 113 deletions.
31 changes: 30 additions & 1 deletion Specs/Quint/extraSpells.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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()),
}

}
211 changes: 125 additions & 86 deletions Specs/Quint/voteBookkeeper.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -72,116 +73,159 @@ 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.
// - Note that if there is no threshold after adding the vote, the function checks if there is a skip threshold.
// 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 = {
Expand Down Expand Up @@ -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 {
Expand 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"}),
Expand All @@ -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"}
Expand All @@ -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"}),
}
}


}
}
Loading

0 comments on commit 518053d

Please sign in to comment.