diff --git a/Specs/Quint/asyncModelsTest.qnt b/Specs/Quint/asyncModelsTest.qnt index 5b22b976f..93a120eae 100644 --- a/Specs/Quint/asyncModelsTest.qnt +++ b/Specs/Quint/asyncModelsTest.qnt @@ -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")) @@ -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), @@ -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 @@ -155,4 +244,4 @@ run DisagreementTest = { -} \ No newline at end of file +} diff --git a/Specs/Quint/consensus.qnt b/Specs/Quint/consensus.qnt index 3991b091b..3e282a873 100644 --- a/Specs/Quint/consensus.qnt +++ b/Specs/Quint/consensus.qnt @@ -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") diff --git a/Specs/Quint/executor.qnt b/Specs/Quint/executor.qnt index da46db545..0984c4014 100644 --- a/Specs/Quint/executor.qnt +++ b/Specs/Quint/executor.qnt @@ -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) } @@ -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) } @@ -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 @@ -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) @@ -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) @@ -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, @@ -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)) @@ -477,6 +489,8 @@ 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 } @@ -484,7 +498,14 @@ pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, Co 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) @@ -591,4 +612,4 @@ pure def nextActionCommand (state: NodeState, command: str) : (NodeState, Execut (state, defaultInput) } -} \ No newline at end of file +} diff --git a/Specs/Quint/parameterizedTest.qnt b/Specs/Quint/parameterizedTest.qnt new file mode 100644 index 000000000..9c29bbaf1 --- /dev/null +++ b/Specs/Quint/parameterizedTest.qnt @@ -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))) +} + + +} \ No newline at end of file diff --git a/Specs/Quint/statemachineAsync.qnt b/Specs/Quint/statemachineAsync.qnt index 2d532e2ff..f714141d8 100644 --- a/Specs/Quint/statemachineAsync.qnt +++ b/Specs/Quint/statemachineAsync.qnt @@ -17,7 +17,9 @@ module statemachineAsync { import executor.* from "./executor" +export executor.* import consensus.* from "./consensus" +export consensus.* import voteBookkeeper.* from "./voteBookkeeper" const validators : Set[Address_t] @@ -109,13 +111,15 @@ action valStep(v: Address_t) : bool = { val sys = sys1.put(v, { ...sys1.get(v), es: res._1}) // do networking if (res._2.name == "proposal") all { - propBuffer' = sendProposal(propBuffer, res._2.proposal), // TODO: this is immediate + // TODO: do we need to start a timeout on this result, that is, when we are proposer and + // send a proposal? + propBuffer' = sendProposal(propBuffer, res._2.proposal), voteBuffer' = voteBuffer, system' = sys, } else if (res._2.name == "votemessage") all { propBuffer' = propBuffer, - voteBuffer' = sendVote(voteBuffer, res._2.voteMessage), // TODO: this is immediate + voteBuffer' = sendVote(voteBuffer, res._2.voteMessage), system' = sys, } else if (res._2.name == "timeout") all { @@ -184,4 +188,4 @@ action step = { } -} \ No newline at end of file +} diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt index 15d725605..25b085a3f 100644 --- a/Specs/Quint/voteBookkeeper.qnt +++ b/Specs/Quint/voteBookkeeper.qnt @@ -153,7 +153,7 @@ module voteBookkeeper { // 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. + // - Otherwise, 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