Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

spec: Fix round skip logic #82

Merged
merged 3 commits into from
Nov 24, 2023
Merged

spec: Fix round skip logic #82

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a1b94a4
Ensure `Skip` event is emitted even when no threshold has been reache…
romac Nov 24, 2023
e4882a4
Ensure `Skip` event is emitted only when vote round is strictly great…
romac Nov 24, 2023
fc8c60f
Remove debug statement
romac Nov 24, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion Specs/Quint/asyncModelsTest.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,6 @@ run RoundswitchTest = {
.then(N4F0::valStep("v4"))
.then(N4F0::valStep("v4"))
.then(all {
// this should work, once the bookkeeper skip event is fixed
assert(N4F0::system.get("v4").es.cs.round == 1),
N4F0::unchangedAll
})
Expand Down
6 changes: 3 additions & 3 deletions Specs/Quint/executor.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -479,7 +479,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)
Expand All @@ -491,7 +491,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)
Expand Down Expand Up @@ -608,4 +608,4 @@ pure def nextActionCommand (state: NodeState, command: str) : (NodeState, Execut
(state, defaultInput)
}

}
}
2 changes: 1 addition & 1 deletion Specs/Quint/statemachineAsync.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,4 +186,4 @@ action step = {
}


}
}
6 changes: 3 additions & 3 deletions Specs/Quint/voteBookkeeper.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,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

Expand Down Expand Up @@ -186,9 +186,9 @@ module voteBookkeeper {
val threshold = computeThreshold(updatedVoteCount, vote.value)
val event = toEvent(vote.round, vote.typ, threshold)
val finalEvent =
if (not(event.in(roundVotes.emittedEvents)))
if (event.name != "None" and not(event.in(roundVotes.emittedEvents)))
event
else if (roundVotes.emittedEvents == Set() and isSkip(updatedVotesAddressesWeights.mapSumValues(), total))
else if (vote.round > currentRound and roundVotes.emittedEvents == Set() and isSkip(updatedVotesAddressesWeights.mapSumValues(), total))
{ round: vote.round, name: "Skip", value: "null" }
else
{ round: vote.round, name: "None", value: "null" }
Expand Down
24 changes: 12 additions & 12 deletions Specs/Quint/voteBookkeeperTest.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,8 @@ module voteBookkeeperTest {
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,
Expand All @@ -45,33 +45,33 @@ module voteBookkeeperTest {
// each of the total voting power
run synchronousConsensusTest =
init(100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60))
.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 =
init(100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60))
.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 =
init(100)
.then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60))
.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"}))

}