From eacbefe53150363c7c1be4ca39c56b21571825eb Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Mon, 15 Jan 2024 14:58:14 +0100 Subject: [PATCH] test for prevoting nil because of more recent lock --- specs/quint/specs/TendermintDSL.qnt | 4 ++ specs/quint/tests/line32/line32Test.qnt | 15 ++++++- specs/quint/tests/line32/line32run.qnt | 60 +++++++++++++++++++++++-- 3 files changed, 75 insertions(+), 4 deletions(-) diff --git a/specs/quint/specs/TendermintDSL.qnt b/specs/quint/specs/TendermintDSL.qnt index fe25cb19e..4bc6ecfd7 100644 --- a/specs/quint/specs/TendermintDSL.qnt +++ b/specs/quint/specs/TendermintDSL.qnt @@ -23,6 +23,10 @@ run ListDeliverProposal (active, propMsg) = { active.length().reps(i => deliverProposal(active[i], propMsg)) } +run ListDeliverVote (active, voteMsg) = { + active.length().reps(i => deliverVote(active[i], voteMsg)) +} + run ListDeliverSomeProposal (active) = { active.length().reps(i => deliverSomeProposal(active[i])) } diff --git a/specs/quint/tests/line32/line32Test.qnt b/specs/quint/tests/line32/line32Test.qnt index 0d97926ec..ce51f9008 100644 --- a/specs/quint/tests/line32/line32Test.qnt +++ b/specs/quint/tests/line32/line32Test.qnt @@ -13,10 +13,23 @@ import line32run( slowByz = "v3" ) as N4F3 from "./line32run" -run line32Test = { +run line32TestInvalid = { N4F3::runToLine32invalid } +import line32run( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set("v1"), + Values = Set("red", "blue"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0), // , 1, 2, 3) + testedVal = "v4", + slowByz = "v1" +) as N4F1 from "./line32run" +run line32TestLocked = { + N4F1::runToLine32locked +} } \ No newline at end of file diff --git a/specs/quint/tests/line32/line32run.qnt b/specs/quint/tests/line32/line32run.qnt index 4496a0273..ea83a8968 100644 --- a/specs/quint/tests/line32/line32run.qnt +++ b/specs/quint/tests/line32/line32run.qnt @@ -8,11 +8,10 @@ export TendermintDSL.* const testedVal : Address const slowByz : Address -// the driver does not store invalid proposals. So we need to receive prevotes first and then the proposal -// first we send the correct guy to round 1 - run runToLine32invalid = +// the driver does not store invalid proposals. So we need to receive prevotes first and then the proposal +// first we send the correct guy to round 1 val nextProposer = proposer(validatorSet, 0, 1) val propVal = "invalid" init @@ -43,4 +42,59 @@ run runToLine32invalid = ) + +run runToLine32locked = + // we need proposer of round 1 to not lock, and someone to lock. + val nextProposer = proposer(validatorSet, 0, 1) + val thirdProposer = proposer(validatorSet, 0, 2) + nondet value = oneOf(Values) + nondet nextValue = oneOf(Values.exclude(Set(value))) + init + .then(all { + everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, value) + }) + // third receive all prevotes + .then(ProcessDeliverAllVotes(Prevote, thirdProposer, correctList, validatorSet, 0, 0, Val(value))) + .then(correctList.length().reps(_ => valStep(thirdProposer))) + .then(2.reps(_ => valStep(thirdProposer))) + // now third proposer as locked and consumed step change + .then(ListDeliverVote(correctList.select(x => x != thirdProposer), mkVote(Prevote, slowByz, 0, 0, Nil))) + .then(ListTakeAStep(correctList.select(x => x != thirdProposer))) + .then(ListDeliverAllVotes(Prevote, correctList.select(x => x != thirdProposer), correctList.select(x => x != thirdProposer), validatorSet, 0, 0, Val(value))) + .then(correctList.length().reps(_ => ListTakeAStep(correctList.select(x => x != thirdProposer)))) // process 2f correct and 1 faulty prevotes processed + .then(ListTakeAStep(correctList.select(x => x != thirdProposer))) // consume step change + .then(ListDeliverVote(correctList, mkVote(Precommit, thirdProposer, 0, 0, Val(value)))) + .then(ListDeliverAllVotes(Precommit, correctList.select(x => x != thirdProposer), correctList, validatorSet, 0, 0, Nil)) + .then(correctList.length().reps(_ => ListTakeAStep(correctList))) + // here all correct have precommit timeout started + // thirdproposer has locked value + // we go to the next round + .then(all { + everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 1, nextValue) + }) + .then(ListDeliverVote(correctList.select(x => x != thirdProposer), mkVote(Prevote, slowByz, 0, 1, Val(nextValue)))) + .then(ListDeliverAllVotes(Prevote, correctList.select(x => x != thirdProposer), correctList.select(x => x != thirdProposer), validatorSet, 0, 1, Val(nextValue))) + .then(correctList.length().reps(_ => ListTakeAStep(correctList.select(x => x != thirdProposer)))) + .then(2.reps(_ => ListTakeAStep(correctList.select(x => x != thirdProposer)))) + .then(ListDeliverVote(correctList, mkVote(Precommit, slowByz, 0, 1, Nil))) + .then(ListDeliverAllVotes(Precommit, correctList.select(x => x != thirdProposer), correctList, validatorSet, 0, 1, Val(nextValue))) + .then(correctList.length().reps(_ => ListTakeAStep(correctList))) + // here all correct have precommit timeout started + // thirdproposer has locked value + // other correct processes have locked nextValue + // now we deliver the prevote from thirdProposer so that others have Polka for round 0 + .then(ListDeliverVote(correctList.select(x => x != thirdProposer), mkVote(Prevote, thirdProposer, 0, 0, Val(value)))) + .then(ListTakeAStep(correctList.select(x => x != thirdProposer))) + // we go to the next round + .then(all { + everyoneReceivesProposalVR(correctList, validatorList, validatorSet, 0, 2, value, 0) + }) + .then(all { // the others prevoted Nil because they had a more recent lock + assert(SetFromList(correctList.select(x => x != thirdProposer)).forall(x => + system.get(x).es.cs.step == PrevoteStep and + voteBuffer.get(x).contains(mkVote(Prevote, x, 0, 2, Nil)) + )), + unchangedAll + }) + }