spec: Overview over consensus logic covered with tests

.github/workflows/quint.yml

@@ -26,10 +26,12 @@ jobs:
   quint-test:
     name: Test
     runs-on: ubuntu-latest
+    env:
+      MAX_SAMPLES: 100
     steps:
       - uses: actions/checkout@v4
       - uses: actions/setup-node@v3
         with:
           node-version: "18"
       - run: npm install -g @informalsystems/quint
-      - run: bash Scripts/quint-forall.sh test Specs/Quint/*Test.qnt
+      - run: bash Scripts/quint-forall.sh "test --max-samples $MAX_SAMPLES" Specs/Quint/*Test.qnt

Scripts/quint-forall.sh

@@ -32,7 +32,7 @@ failed_files=()
 
 for file in "${files[@]}"; do
   info "Running: quint $cmd ${UNDERLINE}$file"
-  if ! npx @informalsystems/quint "$cmd" "$file"; then
+  if ! npx @informalsystems/quint $cmd "$file"; then
     failed_files+=("$file")
     failed=$((failed + 1))
   fi

Specs/Quint/TendermintDSL.qnt

@@ -0,0 +1,52 @@
+// -*- mode: Bluespec; -*-
+
+module TendermintDSL {
+
+import statemachineAsync.* from "./statemachineAsync"
+export statemachineAsync.*
+
+val validatorList = validators.fold(List(), (s, x) => s.append(x))
+val correctList = Correct.fold(List(), (s, x) => s.append(x))
+val faultyList = Faulty.fold(List(), (s, x) => s.append(x))
+
+run ListTakeAStep (active) = {
+    active.length().reps(i => valStep(active[i]))
+}
+
+run ListDeliverProposal (active, proposalMsg) = {
+    active.length().reps(i => deliverProposal(active[i], proposalMsg))
+}
+
+run ListDeliverSomeProposal (active) = {
+    active.length().reps(i => deliverSomeProposal(active[i]))
+}
+
+run ProcessDeliverAllVotes  (cstep, recepient, fromList, valset, h, r, value) = {
+    fromList.length().reps(i => deliverVote(recepient, { src: fromList[i], height: h, round: r, step: cstep, id: value }))
+}
+
+run ListDeliverAllVotes (cstep, fromList, toList, valset, h, r, value) = {
+    toList.length().reps(i => ProcessDeliverAllVotes (cstep, toList[i], fromList, valset, h, r, value))
+}
+
+
+run everyoneReceivesProposal (active, valList, valset, h, r, value) = {
+    val p = Proposer (valset, h, r)
+    setNextValueToPropose(p, value)
+    .then(ListTakeAStep(active))
+    .then(all {
+        assert(true),
+        ListDeliverSomeProposal(active)
+    })
+    .then(ListTakeAStep(active))    
+}
+
+run fromPrevoteToPrecommit (prevoteSenders, prevoteReceivers, valList, valset, h, r, value) = {
+    ListDeliverAllVotes("Prevote", prevoteSenders, prevoteReceivers, valset, h, r, value)
+    .then(prevoteSenders.length().reps(_ => ListTakeAStep(prevoteReceivers)))
+    // extra step due to timeoutprevote double step
+    .then(ListTakeAStep(prevoteReceivers))
+}
+
+
+}

Specs/Quint/asyncModelsTest.qnt

@@ -94,6 +94,9 @@ run ThreeDecideInRound1V4stillinZeroTest = {
     .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" }))
@@ -112,6 +115,10 @@ run ThreeDecideInRound1V4stillinZeroTest = {
     .then(N4F0::valStep("v1"))
     .then(N4F0::valStep("v2"))
     .then(N4F0::valStep("v3"))
+    .then(all {
+        assert(N4F0::system.get("v3").es.chain.head() == "another block"),
+        N4F0::unchangedAll
+    })       
 }
 
 run DecideForFutureRoundTest = {
@@ -156,10 +163,10 @@ 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 == 0),
+        N4F0::valStep("v4")})
     .then(all {
         assert(N4F0::system.get("v4").es.cs.round == 1),
         N4F0::unchangedAll
@@ -200,7 +207,7 @@ run DisagreementTest = {
     .then(N4F2::valStep("v3"))
     .then(N4F2::valStep("v4"))
     .then(all{
-        // they voted diN4F2N4F2erently
+        // they voted differently
         assert(N4F2::voteBuffer == Map(
             "v3" -> Set({ height: 0, id: "a", round: 0, src: "v4", step: "Prevote" },  
                         { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }),
@@ -216,6 +223,8 @@ run DisagreementTest = {
     .then(N4F2::valStep("v3"))  
     .then(N4F2::valStep("v3"))   
     .then(N4F2::valStep("v3"))
+    .then(N4F2::valStep("v3"))
+    .then(N4F2::valStep("v4"))
     .then(N4F2::valStep("v4"))
     .then(N4F2::valStep("v4"))
     .then(N4F2::valStep("v4"))

Specs/Quint/coverage.md

@@ -0,0 +1,43 @@
+# Tests for consensus statemachine (and sometimes driver)
+
+## Overview over covered consensus algorithm lines
+
+| line | comment | (C) | test |
+|  -----:| ---- | -----| -----| 
+ 16 |  reuse valid value | | line28Test.qnt
+ 18 | new value | X2 
+ 19 | send proposal | | (A) RoundswitchTest (^1)
+ 21 | start timeoutPropose | X1, X2b, X2c
+ 24 | prevote value | X1, X2
+ 26 | prevote nil (on invalid or locked) | X2c
+ 30 | prevote value on old prevotes | | line28Test.qnt
+ 32 | prevote nil on old prevotes (on invalid or locked)  |
+ 35 | start timeoutPrevote  | X2
+ 40 | precommit value  | X1
+ 42 without 41  | set valid without locked  | | line42Test
+ 45 | precommit nil | X2b
+ 48 | start timeoutPrecommit  | X2 , X2b
+ 51 | decide  | X1
+ 56 | skip round  | | (A) RoundswitchTest
+ 57 | OnTimeoutPropose  | X2b
+ 61 | OnTimeOutPrevote  | X2
+ 64 | OnTimeOutPrecommit  | X2, X2b
+
+## Comments
+
+- (C) 
+    - refers to DecideNonProposerTest in consensusTest.qnt. 
+    - X1 covered in height 1, X2b: covered in height 2 round 2, etc.
+    - is only containing the consensus state machine. No driver
+    - contains an event to go to height 1
+- (A) asyncModelsTest.qnt
+- ^1 ThreeDecideInRound1V4stillinZeroTest delivers proposal so it must have been sent before
+
+
+## Other tests
+
+- asyncModelsTest.qnt
+    - DisagreementTest: 2/4 faulty lead to disagreement
+    - three processes go to round 1 and decide, on process left behind. Test whether process decides
+        - DecideForFutureRoundTest: first receives proposal then precommits
+        - DecideOnProposalTest: first receives precommits then proposal

Specs/Quint/driver.qnt

@@ -227,16 +227,31 @@ pure def Prevote (es: DriverState, input: DriverInput,  vkOutput: VoteKeeperOutp
                                             value: vkOutput.value,
                                             vr: vkOutput.round})   
                                             // TODO: the value should come from the proposal   
-        else if (vkOutput.round == es.cs.round and
-                es.proposals.exists(p => p.round == es.cs.round and
+        else if (vkOutput.round == es.cs.round)
+            if (es.proposals.exists(p => p.round == es.cs.round and
                 id(p.proposal) == vkOutput.value)) 
-                callConsensus(es, es.bk, {  name: "ProposalAndPolkaAndValid",
+                val pend = (  {  name: "ProposalAndPolkaAndValid",
+                                            height: es.cs.height,
+                                            round: es.cs.round,
+                                            value: vkOutput.value,
+                                            vr: vkOutput.round}, es.cs.height, es.cs.round)   
+                callConsensus( { ...es,  pendingInputs: es.pendingInputs.union(Set(pend)) },
+                                es.bk, 
+                                {   name: "PolkaAny",
+                                    height: es.cs.height,
+                                    round: es.cs.round,
+                                    value: vkOutput.value,
+                                    vr: vkOutput.round})   
+            else
+                // there is no matching proposal
+                callConsensus(es, es.bk, {  name: "PolkaAny",
                                             height: es.cs.height,
                                             round: es.cs.round,
                                             value: vkOutput.value,
                                             vr: vkOutput.round})   
+
         else
-            // we don't have a matching proposal so we do nothing
+            // It is for a future round
             // TODO: we might check whether it is for a future round and jump
             (es, defaultOutput)
     else if (vkOutput.name == "PolkaAny")
@@ -356,7 +371,7 @@ pure def ProposalMsg (es: DriverState, input: DriverInput) : (DriverState, Conse
             else if (newES.cs.step == "Prevote" or newES.cs.step == "Precommit") 
                 if (receivedCommitCurrentVal)
                     // here we need to call both, Commit and Polka. 
-                    // We do commit and append pola to pending
+                    // We do commit and append polka to pending
                     val pend = ( {  name: "ProposalAndPolkaAndValid",
                                     height: newES.cs.height,
                                     round: newES.cs.round,
@@ -450,11 +465,15 @@ pure def decided (es: DriverState, res: ConsensusOutput) : (DriverState, Consens
 }
 
 
-// take input out of pending events and then call consensus with that event
+// take input out of pending inputs and then call consensus with that input
 // We do this when the driver is asked to work on pending events
-pure def PendingInput (es: DriverState, input: DriverInput) : (DriverState, ConsensusOutput) = {
-    val newState = { ...es, pendingInputs: es.pendingInputs.exclude(Set((input.csInput, es.cs.height, es.cs.round)))}
-    callConsensus(newState, es.bk, input.csInput)
+pure def PendingInput (es: DriverState): (DriverState, ConsensusOutput) = {
+    val ev = es.pendingInputs.fold((defaultConsensusInput, -1, -1), (sum, y) => y)
+    val newState = { ...es, pendingInputs: es.pendingInputs.exclude(Set(ev))}
+     if (ev._2 == es.cs.height and ev._3 == es.cs.round)
+        callConsensus(newState, es.bk, ev._1)
+    else
+       (newState, defaultOutput)
 }
 
 
@@ -522,7 +541,7 @@ pure def driver (es: DriverState, input: DriverInput) : (DriverState, ConsensusO
         skip (new, 0)
     }
     else if (input.name == "pending") {
-        PendingInput(es, input)
+        PendingInput(es)
     }
     else if (input.name == "SetNextProposedValue")
         setValue(es, input.nextValueToPropose)
@@ -539,6 +558,12 @@ pure def nextAction (state: NodeState) : (NodeState, DriverInput) = {
     if (not(state.es.started))
         (state, { ...defaultInput, name: "start" })
 
+    else if (state.es.pendingInputs != Set())
+        // this might be cheating as we look into the "es"
+        (state, { ...defaultInput, name: "pending" })
+        // I DID IT. TODO: In the "starkBFT Spec" Google doc, it is written that pending events
+        // should be executed before new messages, which would requir to push this
+        // branch up.
     else if (state.incomingProposals != Set())
         // pick proposal, remove it from incoming
         // val prop = state.incomingProposals.chooseSome()
@@ -562,13 +587,6 @@ pure def nextAction (state: NodeState) : (NodeState, DriverInput) = {
         val timeout = timeouts.fold(("", 0, 0), (sum, y) => y)
         val newstate = { ...state, timeout: state.timeout.exclude(Set(timeout))}
         (newstate, { ...defaultInput, name: "timeout", timeout: timeout._1})
-
-    else if (state.es.pendingInputs != Set())
-        // this might be cheating as we look into the "es"
-        (state, { ...defaultInput, name: "pending" })
-        // TODO: In the "starkBFT Spec" Google doc, it is written that pending events
-        // should be executed before new messages, which would requir to push this
-        // branch up.
     else
         (state, defaultInput)
 }
@@ -578,6 +596,10 @@ pure def nextActionCommand (state: NodeState, command: str) : (NodeState, Driver
     if (command == "start" and not(state.es.started))
         (state, { ...defaultInput, name: "start" })
 
+    else if (command == "pending" and state.es.pendingInputs != Set())
+        // this might be cheating as we look into the "es"
+        (state, { ...defaultInput, name: "pending" })
+
     else if (command == "proposal" and state.incomingProposals != Set())
         // pick proposal, remove it from incoming
         // val prop = state.incomingProposals.chooseSome()
@@ -602,10 +624,6 @@ pure def nextActionCommand (state: NodeState, command: str) : (NodeState, Driver
         val newstate = { ...state, timeout: state.timeout.exclude(Set(timeout))}
         (newstate, { ...defaultInput, name: "timeout", timeout: timeout._1})
 
-    else if (command == "pending" and state.es.pendingInputs != Set())
-        // this might be cheating as we look into the "es"
-        (state, { ...defaultInput, name: "pending" })
-
     else
         (state, defaultInput)
 }

Specs/Quint/line28Test.qnt

@@ -0,0 +1,34 @@
+// -*- mode: Bluespec; -*-
+
+module line28Test {
+
+import line28run(
+    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)
+    otherSet = Set("v2", "v4")
+) as N4F1 from "./line28run"
+
+run line28Test = {
+    N4F1::runToLine28
+}
+
+import line28run(
+    validators = Set("v1", "v2", "v3", "v4", "v5", "v6", "v7"),
+    validatorSet = Set("v1", "v2", "v3", "v4", "v5", "v6", "v7").mapBy(x => 1),
+    Faulty = Set("v1"),
+    Values = Set("red", "blue"),
+    Rounds = Set(0, 1, 2, 3),
+    Heights = Set(0), // , 1, 2, 3)
+    otherSet = Set("v2", "v4", "v6", "v7")
+) as N7F1 from "./line28run"
+
+run Bigline28Test = {
+    N7F1::runToLine28
+}
+
+
+}

Specs/Quint/line28run.qnt

@@ -0,0 +1,40 @@
+// -*- mode: Bluespec; -*-
+
+module line28run {
+
+import TendermintDSL.* from "./TendermintDSL"
+export TendermintDSL.*
+
+const otherSet : Set[Address_t]
+val others = otherSet.fold(List(), (s, x) => s.append(x)) 
+
+run runToLine28 = {
+    val nextProposer = Proposer (validatorSet, 0, 1)
+    init
+    .then(all {
+        // others should be at most 2/3.
+        // if this assertion fails the set need to be set differently
+        assert(3 * size(otherSet) <= 2 * size(validators)),  
+        assert(3 * size(otherSet.union(Faulty)) > 2 * size(validators)),  
+        everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, "blue")
+    })
+    // receive all prevotes    
+    .then(fromPrevoteToPrecommit (correctList, correctList, validatorList, validatorSet, 0, 0, "blue"))
+    // now the faulty nodes precommit nil
+    .then(ListDeliverAllVotes("Precommit", faultyList, correctList, validatorSet, 0, 0, "nil"))
+    .then(faultyList.length().reps(_ => ListTakeAStep(correctList)))   
+    // now the other precommits are delivered, so that timeoutPrecommit is started
+    .then(ListDeliverAllVotes("Precommit", others, correctList, validatorSet, 0, 0, "blue"))
+    .then(others.length().reps(_ => ListTakeAStep(correctList)))
+    // TimeoutPrecommit is there an can fire and bring is to the next round.
+    .then(all{
+        assert(system.get(nextProposer).timeout.contains(("TimeoutPrecommit", 0, 0))),
+        everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, "red")
+    })
+    .then(all{
+        assert(voteBuffer.get(nextProposer).contains( { height: 0, id: "blue", round: 1, src: nextProposer, step: "Prevote" })),
+        unchangedAll
+    })
+}
+
+}

Specs/Quint/line42Test.qnt

@@ -0,0 +1,19 @@
+// -*- mode: Bluespec; -*-
+
+module line42Test {
+
+import line42run(
+    validators = Set("v1", "v2", "v3", "v4"),
+    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
+    Faulty = Set(),
+    Values = Set("red", "blue"),
+    Rounds = Set(0, 1, 2, 3),
+    Heights = Set(0), // , 1, 2, 3)
+    testedVal = "v4"
+) as N4F0 from "./line42run"
+
+run line42Test = {
+    N4F0::runToLine42
+}
+
+}