Skip to content

Commit

Permalink
spec: Add skip round logic (#75)
Browse files Browse the repository at this point in the history
* start skip round logic (missing to see what messages are there upon skipping)

* added skip round reaction upon votes

* bug in strings calling bookkeeper fixed

* another wrong string

* added round switch test - not activated yet

* tests around round switching

* failing test

* Fix typos

* added a test that generates a lot of unsuccessful rounds

* added assertion for correct round

* Ensure `Skip` event is emitted even when no threshold has been reached yet

* Ensure `Skip` event is emitted only when vote round is strictly greater than the current round

* Remove debug statement

* parameterized test is more concise

* made parameterized test even more concise

* added an assertion at the end of unsuccessful round

---------

Co-authored-by: Romain Ruetschi <romain@informal.systems>
  • Loading branch information
josef-widder and romac authored Nov 24, 2023
1 parent 2a7862b commit ce7a130
Show file tree
Hide file tree
Showing 6 changed files with 234 additions and 34 deletions.
111 changes: 100 additions & 11 deletions Specs/Quint/asyncModelsTest.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,11 @@ import statemachineAsync(
Heights = Set(0) // , 1, 2, 3)
) as N4F0 from "./statemachineAsync"

run NewRoundTest = {

run ThreeDecideInRound1V4stillinZeroTest = {
N4F0::init
.then(N4F0::setNextValueToPropose("v2", "block"))
.then(N4F0::valStep("v1"))
.then(N4F0::valStep("v1"))
.then(N4F0::valStep("v2"))
.then(N4F0::valStep("v3"))
.then(N4F0::valStep("v4"))
Expand Down Expand Up @@ -64,21 +65,109 @@ run NewRoundTest = {
.then(N4F0::valStep("v3"))
.then(N4F0::valStep("v1"))
.then(N4F0::valStep("v2"))
.then(N4F0::valStep("v3"))
.then(N4F0::valStep("v3"))
.then(N4F0::setNextValueToPropose("v3", "another block"))
.then(N4F0::valStep("v1"))
.then(N4F0::valStep("v2"))
.then(N4F0::valStep("v3"))
// .then(N4F0::deliverProposal("v1", { height: 0, proposal: "block", round: 1, src: "v2", validRound: -1 }))
/* .then(N4F0::deliverProposal("v1", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 }))
.then(N4F0::deliverProposal("v2", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 }))
.then(N4F0::deliverProposal("v3", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 }))
.then(N4F0::deliverProposal("v1", { height: 0, proposal: "another block", round: 1, src: "v3", validRound: -1 }))
.then(N4F0::deliverProposal("v2", { height: 0, proposal: "another block", round: 1, src: "v3", validRound: -1 }))
.then(N4F0::deliverProposal("v3", { height: 0, proposal: "another block", round: 1, src: "v3", validRound: -1 }))
.then(N4F0::valStep("v1"))
.then(N4F0::valStep("v2"))
.then(N4F0::valStep("v3"))
.then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v1", step: "Prevote" }))
.then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v2", step: "Prevote" }))
.then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v3", step: "Prevote" }))
.then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v1", step: "Prevote" }))
.then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v2", step: "Prevote" }))
.then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v3", step: "Prevote" }))
.then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v1", step: "Prevote" }))
.then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v2", step: "Prevote" }))
.then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v3", step: "Prevote" }))
.then(N4F0::valStep("v1"))
.then(N4F0::valStep("v2"))
.then(N4F0::valStep("v3"))
.then(N4F0::valStep("v1"))
.then(N4F0::valStep("v2"))
.then(N4F0::valStep("v3"))
.then(N4F0::valStep("v1"))
.then(N4F0::valStep("v2"))
.then(N4F0::valStep("v3"))
.then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
.then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v2", step: "Precommit" }))
.then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" }))
.then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
.then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v2", step: "Precommit" }))
.then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" }))
.then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
.then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v2", step: "Precommit" }))
.then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" }))
.then(N4F0::valStep("v1"))
.then(N4F0::valStep("v2"))
.then(N4F0::valStep("v3"))
*/
.then(N4F0::valStep("v1"))
.then(N4F0::valStep("v2"))
.then(N4F0::valStep("v3"))
.then(N4F0::valStep("v1"))
.then(N4F0::valStep("v2"))
.then(N4F0::valStep("v3"))
}

run DecideForFutureRoundTest = {
ThreeDecideInRound1V4stillinZeroTest
.then(N4F0::deliverProposal("v4", { height: 0, proposal: "another block", round: 1, src: "v3", validRound: -1 }))
.then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
.then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v2", step: "Precommit" }))
.then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" }))
// .then(4.reps(i => N4F0::valStep("v4")))
.then(N4F0::valStep("v4"))
.then(N4F0::valStep("v4"))
.then(N4F0::valStep("v4"))
.then(N4F0::valStep("v4"))
.then(all {
assert(N4F0::system.get("v4").es.chain.head() == "another block"),
N4F0::unchangedAll
})
// .then(N4F0::valStep("v4"))

}

run DecideOnProposalTest = {
ThreeDecideInRound1V4stillinZeroTest
.then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
.then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v2", step: "Precommit" }))
.then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" }))
.then(N4F0::valStep("v4"))
.then(N4F0::valStep("v4"))
.then(N4F0::valStep("v4"))
.then(N4F0::deliverProposal("v4", { height: 0, proposal: "another block", round: 1, src: "v3", validRound: -1 }))
.then(all {
assert(N4F0::system.get("v4").es.chain == List()),
N4F0::valStep("v4")
})
.then(all {
assert(N4F0::system.get("v4").es.chain.head() == "another block"),
N4F0::unchangedAll
})
}

run RoundswitchTest = {
ThreeDecideInRound1V4stillinZeroTest
.then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
.then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v2", step: "Prevote" }))
.then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" }))
.then(N4F0::valStep("v4"))
.then(N4F0::valStep("v4"))
.then(N4F0::valStep("v4"))
.then(all {
assert(N4F0::system.get("v4").es.cs.round == 1),
N4F0::unchangedAll
})
}



import statemachineAsync(
validators = Set("v1", "v2", "v3", "v4"),
validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
Expand All @@ -100,7 +189,7 @@ import statemachineAsync(
Heights = Set(0) // , 1, 2, 3)
) as N4F2 from "./statemachineAsync"

// v3 and v4 are correct. v2 is a N4N4F22aulty proposal and proposes diN4N4F22N4N4F22erently to v3 and v4
// v3 and v4 are correct. v2 is a faulty proposal and proposes differently to v3 and v4
// this run leads to disagreement
run DisagreementTest = {
N4F2::init
Expand Down Expand Up @@ -155,4 +244,4 @@ run DisagreementTest = {



}
}
2 changes: 2 additions & 0 deletions Specs/Quint/consensus.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -410,6 +410,8 @@ pure def consensus (state: ConsensusState, ev: Event) : ConsResult = {
PrecommitAny(state, ev)
else if (ev.name == "ProposalAndCommitAndValid")
ProposalAndCommitAndValid(state, ev)
else if (ev.name == "RoundSkip")
RoundSkip (state, ev)
else if (ev.name == "TimeoutPropose")
TimeoutPropose (state, ev)
else if (ev.name == "TimeoutPrevote")
Expand Down
59 changes: 40 additions & 19 deletions Specs/Quint/executor.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -197,15 +197,20 @@ pure def Precommit (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent)
}
}
else if (eev.name == "PrecommitAny" and eev.round == es.cs.round) {
callConsensus(es, es.bk, { name: "PrecommitAny",
height: input.vote.height,
round: input.vote.round,
value: input.vote.id,
vr: -1})
callConsensus(es, es.bk, { name: "PrecommitAny",
height: input.vote.height,
round: input.vote.round,
value: input.vote.id,
vr: -1})
}
else if (eev.name == "Skip" and eev.round > es.cs.round)
callConsensus(es, es.bk, { name: "RoundSkip",
height: input.vote.height,
round: input.vote.round,
value: input.vote.id,
vr: -1})
else
// none of the supported Precommit events. Do nothing
// TODO: catch skip round event
(es, defaultResult)
}

Expand Down Expand Up @@ -253,8 +258,13 @@ pure def Prevote (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent)
round: es.cs.round,
value: eev.value,
vr: eev.round})
else if (eev.name == "Skip" and eev.round > es.cs.round)
callConsensus(es, es.bk, { name: "RoundSkip",
height: input.vote.height,
round: input.vote.round,
value: input.vote.id,
vr: -1})
else
// TODO: catch skip round event
(es, defaultResult)
}

Expand Down Expand Up @@ -283,7 +293,7 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState,
val receivedCommit = checkThreshold( newES.bk,
input.proposal.round,
"Precommit",
{name: "PrecommitValue",
{name: "Value",
value: id(input.proposal.proposal)})
if (receivedCommit)
// we have a commit that matches the proposal. We don't need to compare against
Expand All @@ -296,7 +306,7 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState,
round: input.proposal.round,
value: id(input.proposal.proposal),
vr: input.proposal.validRound})
else if (input.proposal.round != es.cs.round or input.proposal.height != es.cs.round)
else if (input.proposal.round != es.cs.round or input.proposal.height != es.cs.height)
// the proposal is from the right proposer and valid, but not for this round
// keep the proposal, do nothing else
(newES, defaultResult)
Expand All @@ -305,17 +315,17 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState,
val receivedPolkaValidRoundVal = checkThreshold(newES.bk,
input.proposal.validRound,
"Prevote",
{name: "PolkaValue",
{name: "Value",
value: id(input.proposal.proposal)})
val receivedPolkaCurrentVal = checkThreshold( newES.bk,
newES.cs.round,
"Prevote",
{name: "PolkaValue",
{name: "Value",
value: id(input.proposal.proposal)})
val receivedCommitCurrentVal = checkThreshold( newES.bk,
newES.cs.round,
"Precommit",
{name: "PrecommitValue",
{name: "Value",
value: id(input.proposal.proposal)})
if (newES.cs.step == "propose")
if (input.proposal.validRound == -1)
Expand Down Expand Up @@ -379,7 +389,7 @@ pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState,
// (not(valid(input.proposal)))
// keep ES (don't use newES here), that is, drop proposal
if (es.cs.step == "propose" and es.cs.round == input.proposal.round and es.cs.height == input.proposal.height)
if (checkThreshold(es.bk, es.cs.round, "Prevote", {name: "PolkaValue", value: id(input.proposal.proposal)}))
if (checkThreshold(es.bk, es.cs.round, "Prevote", {name: "Value", value: id(input.proposal.proposal)}))
val event: Event = {name: "ProposalAndPolkaAndInValid",
height: es.cs.height,
round: es.cs.round,
Expand Down Expand Up @@ -464,11 +474,13 @@ pure def setValue(es: ExecutorState, value: Value_t) : (ExecutorState, Consensus
pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = {
// TODO: shall we check whether the sender actually is in the validator set
if (input.name == "proposal") {
val cons_res = ProposalMsg(es, input)
if (cons_res._2.name == "decided")
decided (cons_res._1, cons_res._2)
val res = ProposalMsg(es, input)
if (res._2.name == "decided")
decided (res._1, res._2)
else if (res._2.name == "skipRound")
skip (res._1, res._2.skipRound)
else
cons_res
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))
Expand All @@ -477,14 +489,23 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co
val cons_res = Precommit(newES, input, res.event)
if (cons_res._2.name == "decided")
decided (cons_res._1, cons_res._2)
else if (cons_res._2.name == "skipRound")
skip (cons_res._1, cons_res._2.skipRound)
else
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 newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event}
// only a commit event can come here.
Prevote(newES, input, res.event)
val cons_res = Prevote(newES, input, res.event)
if (cons_res._2.name == "decided")
// TODO: dead branch. But we should put this after consensus call logic into a function
decided (cons_res._1, cons_res._2)
else if (cons_res._2.name == "skipRound")
skip (cons_res._1, cons_res._2.skipRound)
else
cons_res
}
else if (input.name == "timeout") {
val res = Timeout(es, input)
Expand Down Expand Up @@ -591,4 +612,4 @@ pure def nextActionCommand (state: NodeState, command: str) : (NodeState, Execut
(state, defaultInput)
}

}
}
84 changes: 84 additions & 0 deletions Specs/Quint/parameterizedTest.qnt
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
module parameterizedTest {

import statemachineAsync(
validators = Set("v1", "v2", "v3", "v4"),
validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
Faulty = Set(),
Values = Set("a", "b"),
Rounds = Set(0, 1, 2, 3),
Heights = Set(0) // , 1, 2, 3)
) as N4F0 from "./statemachineAsync"

val validatorList = N4F0::validators.fold(List(), (s, x) => s.append(x))

run everyoneTakesAStep = {
validatorList.length().reps(i => N4F0::valStep(validatorList[i]))
}

// here there is a different prevote from the proposer
run oneDeliversPrevote (validator, prop, r, proposer, nonprop) = {
nonprop.length().reps( i =>
N4F0::deliverVote(validator, { height: 0, id: "nil", round: r, src: nonprop[i], step: "Prevote" }))
.then(N4F0::deliverVote(validator, { height: 0, id: prop, round: r, src: proposer, step: "Prevote" }))
}

run everyoneDeliversPrevote (prop, r, proposer, nonprop) = {
validatorList.length().reps(i => oneDeliversPrevote (validatorList[i], prop, r, proposer, nonprop))
}

// all the precommits are for "nil"
run oneDeliversPrecommit (validator, prop, r, proposer, nonprop) = {
validatorList.length().reps(i =>
N4F0::deliverVote(validator, { height: 0, id: "nil", round: r, src: validatorList[i], step: "Precommit" }))
}

run everyoneDeliversPrecommit (prop, r, proposer, nonprop) = {
validatorList.length().reps(i => oneDeliversPrecommit (validatorList[i], prop, r, proposer, nonprop))
}

run UnSuccessfulRound (prop: str, r: int) : bool = {
val proposer = N4F0::Proposer(N4F0::validatorSet, 0, r)
val nonprop = validatorList.select(x => x != proposer)
// everyone is in round r and proposer sent a proposal
all {
assert(N4F0::propBuffer.keys().forall(p => N4F0::propBuffer.get(p).contains(
{ height: 0, proposal: prop, round: r, src: proposer, validRound: -1 }) )),
N4F0::unchangedAll
}
.then(N4F0::deliverProposal(proposer, { height: 0, proposal: prop, round: r, src: proposer, validRound: -1 }))
.then(everyoneTakesAStep)
.then(everyoneDeliversPrevote(prop, r, proposer, nonprop))
.then(3.reps(i => everyoneTakesAStep))
.then(all {
assert(N4F0::system.keys().forall(p => N4F0::system.get(p).timeout.contains(
("TimeoutPrevote", 0, r)) )),
N4F0::unchangedAll
})
.then(everyoneTakesAStep)
.then(everyoneDeliversPrecommit(prop, r, proposer, nonprop))
.then(4.reps(i => everyoneTakesAStep))
.then(all {
assert(N4F0::system.keys().forall(p => N4F0::system.get(p).timeout.contains(
("TimeoutPrecommit", 0, r)) )),
N4F0::unchangedAll
})
}

run UnSuccessfulRoundWithSetup (prop: str, r: int) : bool = {
N4F0::setNextValueToPropose(N4F0::Proposer(N4F0::validatorSet, 0, r), prop)
.then(everyoneTakesAStep)
.then(all {
assert(N4F0::system.keys().forall(p => N4F0::system.get(p).es.cs.round == r)),
UnSuccessfulRound (prop, r)
})
}

run multiRoundTest = {
val proposals = ["blue", "red", "green", "yellow"]
val repetitions = proposals.length()
N4F0::init
.then(repetitions.reps(i => UnSuccessfulRoundWithSetup(proposals[i], i)))
}


}
Loading

0 comments on commit ce7a130

Please sign in to comment.