fix(spec/votekeeper): Fix the VoteKeeper spec to account for skip thr…

…eshold from higher round
informalsystems · Nov 15, 2023 · 849e614 · 849e614
1 parent 518053d
commit 849e614
Show file tree

Hide file tree

Showing 2 changed files with 47 additions and 19 deletions.
diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt
@@ -62,6 +62,7 @@ module voteBookkeeper {
 
     type Bookkeeper = {
         height: Height,
+        currentRound: Round,
         totalWeight: Weight,
         rounds: Round -> RoundVotes
     }
@@ -183,29 +184,38 @@ module voteBookkeeper {
             else 
                 roundVotes.votesAddressesWeights.mapSafeSet(vote.address, weight)
 
-        val threshold = computeThreshold(updatedVoteCount, vote.value)
-        val event = toEvent(vote.round, vote.typ, threshold)
-        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 combinedWeight = updatedRoundVotes.prevotes.valuesWeights.getOrElse(vote.value, 0)
+            + updatedRoundVotes.precommits.valuesWeights.getOrElse(vote.value, 0)
+
+        val finalEvent =
+            // TODO: do we need to check if we have not emitted any event yet for the vote round?
+            if (vote.round > keeper.currentRound and isSkip(combinedWeight, total))
+                { round: vote.round, name: "Skip", value: "null" }
+            else
+                val threshold = computeThreshold(updatedVoteCount, vote.value)
+                val event = toEvent(vote.round, vote.typ, threshold)
+                if (not(event.in(roundVotes.emittedEvents))) 
+                    event
+                else 
+                    { round: vote.round, name: "None", value: "null" }
+
+        val updatedEmittedEvents = roundVotes.emittedEvents.setAddIf(finalEvent, finalEvent.name != "None")
+
         val updatedRoundVotes2 = updatedRoundVotes
                 .with("votesAddressesWeights", updatedVotesAddressesWeights)
-                .with("emittedEvents", updatedEmmittedEvents)
+                .with("emittedEvents", updatedEmittedEvents)
 
+        val newBookkeeper =
+            keeper.with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes2))
+
         { 
-            bookkeeper: keeper.with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes2)), 
+            bookkeeper: newBookkeeper, 
             event: finalEvent 
         }
 

diff --git a/Specs/Quint/voteBookkeeperTest.qnt b/Specs/Quint/voteBookkeeperTest.qnt
@@ -20,8 +20,8 @@ module voteBookkeeperTest {
         lastEmitted' = lastEmitted,
     }
 
-    action init(totalWeight: Weight): bool = all {
-        bookkeeper' = { height: 10, totalWeight: totalWeight, rounds: Map() },
+    action init(round: Round, totalWeight: Weight): bool = all {
+        bookkeeper' = { height: 10, currentRound: round, totalWeight: totalWeight, rounds: Map() },
         lastEmitted' = { round: -1, name: "", value: "null" },
     }
 
@@ -44,7 +44,7 @@ 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 =
-        init(100)
+        init(1, 100)
         .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60))
         .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
         .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10))
@@ -60,18 +60,36 @@ module voteBookkeeperTest {
 
     // Reaching PolkaAny 
     run polkaAnyTest =
-        init(100)
+        init(1, 100)
         .then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60))
         .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
         .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10))
         .then(_assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"}))
 
     // Reaching PolkaNil
     run polkaNilTest =
-        init(100)
+        init(1, 100)
         .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60))
         .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
         .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10))
         .then(_assert(lastEmitted == {round: 1, name: "PolkaNil", value: "null"}))
 
+    // Reaching Skip via n+1 threshold
+    run skipHonestTest =
+        init(1, 100)
+        .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60))
+        .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
+        .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10))
+        .then(_assert(lastEmitted == {round: 2, name: "None", value: "null"}))
+        .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "bob"}, 30))
+        .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"}))
+
+    // Reaching Skip via 2f+1 threshold
+    run skipQuorumTest =
+        init(1, 100)
+        .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10))
+        .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
+        .then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 60))
+        .then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"}))
+
 }