Skip to content

Commit 1c3d844

Browse files
romacromac
authored
spec: Align VoteKeeper spec with the code (#84)
1 parent a755b7b commit 1c3d844

File tree

4 files changed

+52
-55
lines changed

4 files changed

+52
-55
lines changed

‎Scripts/quint-forall.sh‎

100644100755
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#!/bin/env bash
1+
#!/usr/bin/env bash
22

33
BLUE=$(tput setaf 4)
44
RED=$(tput setaf 1)

‎Specs/Quint/executor.qnt‎

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@ module executor {
1010
import consensus.* from "./consensus"
1111
import voteBookkeeper.* from "./voteBookkeeper"
1212

13-
pure def initBookKeeper (currentRound: Round, totalVotingPower: int): Bookkeeper =
14-
{ height: 0, currentRound: currentRound, totalWeight: totalVotingPower, rounds: Map() }
13+
pure def initBookKeeper(totalVotingPower: int): Bookkeeper =
14+
{ height: 0, totalWeight: totalVotingPower, rounds: Map() }
1515

1616

1717
type ExecutorState = {
@@ -30,7 +30,7 @@ type ExecutorState = {
3030
pure def initExecutor (v: Address_t, vs: Address_t -> int) : ExecutorState = {
3131
val tvp = vs.keys().fold(0, (sum, key) => sum + vs.get(key))
3232
{
33-
bk: initBookKeeper(0, tvp),
33+
bk: initBookKeeper(tvp),
3434
cs: initConsensusState(v),
3535
proposals: Set(),
3636
valset: vs,
@@ -155,12 +155,10 @@ pure def callConsensus (es: ExecutorState, bk: Bookkeeper, ev: Event) : (Executo
155155
else
156156
// Go to consensus
157157
val res = consensus(es.cs, ev)
158-
// Update the round in the vote keeper, in case we moved to a new round
159-
val newBk = { ...bk, currentRound: res.cs.round }
160158
// Record that we executed the event
161159
val events = es.executedEvents.append((ev, res.cs.height, res.cs.round))
162160

163-
({ ...es, bk: newBk, cs: res.cs, executedEvents: events }, res.out)
161+
({ ...es, bk: bk, cs: res.cs, executedEvents: events }, res.out)
164162
}
165163

166164

@@ -483,7 +481,7 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co
483481
res
484482
}
485483
else if (input.name == "votemessage" and input.vote.step == "Precommit") {
486-
val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src))
484+
val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src), es.cs.round)
487485
val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event}
488486
// only a commit event can come here.
489487
val cons_res = Precommit(newES, input, res.event)
@@ -495,7 +493,7 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co
495493
cons_res
496494
}
497495
else if (input.name == "votemessage" and input.vote.step == "Prevote") {
498-
val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src))
496+
val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src), es.cs.round)
499497
val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event}
500498
// only a commit event can come here.
501499
val cons_res = Prevote(newES, input, res.event)

‎Specs/Quint/voteBookkeeper.qnt‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,6 @@ module voteBookkeeper {
6262

6363
type Bookkeeper = {
6464
height: Height,
65-
currentRound: Round,
6665
totalWeight: Weight,
6766
rounds: Round -> RoundVotes
6867
}
@@ -158,7 +157,7 @@ module voteBookkeeper {
158157
// TO DISCUSS:
159158
// - There might be a problem if we generalize from single-shot to multi-shot: the keeper only keeps the totalWeight
160159
// of the current height; I wonder if we need to keep the totalWeight for every Height that we may receive a vote for.
161-
pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: Weight): { bookkeeper: Bookkeeper, event: ExecutorEvent } =
160+
pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: Weight, currentRound: Round): { bookkeeper: Bookkeeper, event: ExecutorEvent } =
162161
val height = keeper.height
163162
val total = keeper.totalWeight
164163

@@ -194,7 +193,7 @@ module voteBookkeeper {
194193
val combinedWeight = updatedVotesAddressesWeights.mapSumValues()
195194

196195
val finalEvent =
197-
if (vote.round > keeper.currentRound and isSkip(combinedWeight, total))
196+
if (vote.round > currentRound and isSkip(combinedWeight, total))
198197
{ round: vote.round, name: "Skip", value: "null" }
199198
else
200199
val threshold = computeThreshold(updatedVoteCount, vote.value)

‎Specs/Quint/voteBookkeeperTest.qnt‎

Lines changed: 43 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -20,13 +20,13 @@ module voteBookkeeperTest {
2020
lastEmitted' = lastEmitted,
2121
}
2222

23-
action initWith(round: Round, totalWeight: Weight): bool = all {
24-
bookkeeper' = { height: 10, currentRound: round, totalWeight: totalWeight, rounds: Map() },
23+
action initWith(totalWeight: Weight): bool = all {
24+
bookkeeper' = { height: 10, totalWeight: totalWeight, rounds: Map() },
2525
lastEmitted' = { round: -1, name: "", value: "null" },
2626
}
2727

28-
action applyVoteAction(vote: Vote, weight: Weight): bool =
29-
val result = applyVote(bookkeeper, vote, weight)
28+
action applyVoteAction(vote: Vote, weight: Weight, currentRound: Round): bool =
29+
val result = applyVote(bookkeeper, vote, weight, currentRound)
3030
all {
3131
bookkeeper' = result.bookkeeper,
3232
lastEmitted' = result.event,
@@ -44,100 +44,100 @@ module voteBookkeeperTest {
4444
// all messages are received in order. We assume three validators in the validator set wtih 60%, 30% and 10%
4545
// each of the total voting power
4646
run synchronousConsensusTest =
47-
initWith(1, 100)
48-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60))
47+
initWith(100)
48+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60, 1))
4949
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
50-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10))
50+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10, 1))
5151
.then(_assert(lastEmitted == {round: 1, name: "PolkaValue", value: "proposal"}))
52-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "bob"}, 30))
52+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "bob"}, 30, 1))
5353
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
54-
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "bob"}, 30))
54+
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "bob"}, 30, 1))
5555
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
56-
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "john"}, 10))
56+
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "john"}, 10, 1))
5757
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
58-
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "alice"}, 60))
58+
.then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "alice"}, 60, 1))
5959
.then(_assert(lastEmitted == {round: 1, name: "PrecommitValue", value: "proposal"}))
6060

6161
// Reaching PolkaAny
6262
run polkaAnyTest =
63-
initWith(1, 100)
64-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60))
63+
initWith(100)
64+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60, 1))
6565
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
66-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10))
66+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10, 1))
6767
.then(_assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"}))
6868

6969
// Reaching PolkaNil
7070
run polkaNilTest =
71-
initWith(1, 100)
72-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60))
71+
initWith(100)
72+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60, 1))
7373
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
74-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10))
74+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10, 1))
7575
.then(_assert(lastEmitted == {round: 1, name: "PolkaNil", value: "null"}))
7676

7777
// Reaching Skip via n+1 threshold with prevotes from two validators at a future round
7878
run skipSmallQuorumAllPrevotesTest =
79-
initWith(1, 100)
80-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60))
79+
initWith(100)
80+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60, 1))
8181
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
82-
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10))
82+
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10, 1))
8383
.then(_assert(lastEmitted == {round: 2, name: "None", value: "null"}))
84-
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "bob"}, 30))
84+
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "bob"}, 30, 1))
8585
.then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"}))
8686

8787
// Cannot reach Skip via f+1 threshold with one prevote and one precommit from the same validator at a future round
8888
run noSkipSmallQuorumMixedVotesSameValTest =
89-
initWith(1, 90)
90-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10))
89+
initWith(90)
90+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1))
9191
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
92-
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 20))
92+
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 20, 1))
9393
.then(_assert(lastEmitted == {round: 2, name: "None", value: "null"}))
94-
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 20))
94+
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 20, 1))
9595
.then(_assert(lastEmitted != {round: 2, name: "Skip", value: "null"}))
9696

9797
// Reaching Skip via f+1 threshold with one prevote and one precommit from two validators at a future round
9898
run skipSmallQuorumMixedVotesTwoValsTest =
99-
initWith(1, 80)
100-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 50))
99+
initWith(80)
100+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 50, 1))
101101
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
102-
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10))
102+
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10, 1))
103103
.then(_assert(lastEmitted == {round: 2, name: "None", value: "null"}))
104-
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 20))
104+
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 20, 1))
105105
.then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"}))
106106

107107
// Reaching Skip via 2f+1 threshold with a single prevote from a single validator at a future round
108108
run skipQuorumSinglePrevoteTest =
109-
initWith(1, 100)
110-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10))
109+
initWith(100)
110+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1))
111111
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
112-
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 60))
112+
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 60, 1))
113113
.then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"}))
114114

115115
// Reaching Skip via 2f+1 threshold with a single precommit from a single validator at a future round
116116
run skipQuorumSinglePrecommitTest =
117-
initWith(1, 100)
118-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10))
117+
initWith(100)
118+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1))
119119
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
120-
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 60))
120+
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 60, 1))
121121
.then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"}))
122122

123123
// Cannot reach Skip via 2f+1 threshold with one prevote and one precommit from the same validator at a future round
124124
run noSkipQuorumMixedVotesSameValTest =
125-
initWith(1, 100)
126-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10))
125+
initWith(100)
126+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 10, 1))
127127
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
128-
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 30))
128+
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 30, 1))
129129
.then(_assert(lastEmitted == {round: 2, name: "None", value: "null"}))
130-
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 30))
130+
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "john"}, 30, 1))
131131
.then(_assert(lastEmitted != {round: 2, name: "Skip", value: "null"}))
132132

133133
// Reaching Skip via 2f+1 threshold with one prevote and one precommit from two validators at a future round
134134
run skipQuorumMixedVotesTwoValsTest =
135-
initWith(1, 80)
136-
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 20))
135+
initWith(80)
136+
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 20, 1))
137137
.then(_assert(lastEmitted == {round: 1, name: "None", value: "null"}))
138-
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10))
138+
.then(applyVoteAction({typ: "Prevote", round: 2, value: "proposal", address: "john"}, 10, 1))
139139
.then(_assert(lastEmitted == {round: 2, name: "None", value: "null"}))
140-
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 50))
140+
.then(applyVoteAction({typ: "Precommit", round: 2, value: "proposal", address: "bob"}, 50, 1))
141141
.then(_assert(lastEmitted == {round: 2, name: "Skip", value: "null"}))
142142

143143
}

0 commit comments

Comments
 (0)