Rearranging modules in the Tendermint spec

examples/.scripts/run-example.sh

@@ -15,6 +15,8 @@ result () {
 
     # Skip tests for parameterized modules
     if [[ "$cmd" == "test" && (
+            "$file" == "cosmos/tendermint/Tendermint.qnt" ||
+            "$file" == "cosmos/tendermint/TendermintTest.qnt" ||
             "$file" == "cosmos/lightclient/Blockchain.qnt" ||
             "$file" == "cosmos/lightclient/LCVerificationApi.qnt" ) ]] ; then
       printf "N/A[^parameterized]"; return
@@ -24,6 +26,8 @@ result () {
             "$file" == "cosmos/lightclient/Blockchain.qnt" ||
             "$file" == "cosmos/lightclient/LCVerificationApi.qnt" ||
             "$file" == "cosmos/lightclient/typedefs.qnt" ||
+            "$file" == "cosmos/tendermint/Tendermint.qnt" ||
+            "$file" == "cosmos/tendermint/TendermintTest.qnt" ||
             "$file" =~ ^spells/ ||
             "$file" == "solidity/SimpleAuction/SimpleAuction.qnt" ||
             "$file" == "cosmos/ics20/base.qnt" ) ]] ; then
@@ -51,8 +55,6 @@ result () {
     elif [[ "$file" == "cosmos/ics23/ics23.qnt" && "$cmd" == "verify" ]] ; then
       printf "<sup>https://github.com/informalsystems/quint/issues/693,</sup>"
       printf "<sup>https://github.com/informalsystems/quint/pull/975</sup>"
-    elif [[ "$file" == "cosmos/tendermint/TendermintAcc005.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" ) ]] ; then
-      printf "<sup>https://github.com/informalsystems/quint/pull/1023</sup>"
     elif [[ "$file" == "cosmwasm/zero-to-hero/vote.qnt" && "$cmd" == "verify" ]] ; then
       printf "<sup>https://github.com/informalsystems/quint/issues/693</sup>"
     elif [[ "$file" == "language-features/option.qnt" && "$cmd" == "verify"  ]] ; then
@@ -109,6 +111,8 @@ get_verify_args () {
         "$file" == "classic/distributed/ReadersWriters/ReadersWriters.qnt" ||
         "$file" == "cosmos/lightclient/Lightclient.qnt" ]] ; then
     args="--init=Init --step=Next"
+  elif [[ "$file" == "cosmos/tendermint/TendermintModels.qnt" ]] ; then
+    args="--init=n4_f1::Init --step=n4_f1::Next --invariant=n4_f1::Agreement"
   fi
   echo "${args}"
 }

examples/README.md

@@ -64,7 +64,9 @@ listed without any additional command line arguments.
 | [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [cosmos/lightclient/typedefs.qnt](./cosmos/lightclient/typedefs.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
-| [cosmos/tendermint/TendermintAcc005.qnt](./cosmos/tendermint/TendermintAcc005.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/pull/1023</sup> | :x:<sup>https://github.com/informalsystems/quint/pull/1023</sup> |
+| [cosmos/tendermint/Tendermint.qnt](./cosmos/tendermint/Tendermint.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
+| [cosmos/tendermint/TendermintModels.qnt](./cosmos/tendermint/TendermintModels.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [cosmos/tendermint/TendermintTest.qnt](./cosmos/tendermint/TendermintTest.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693</sup> |
 | [language-features/booleans.qnt](./language-features/booleans.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/counters.qnt](./language-features/counters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

examples/cosmos/tendermint/README.md

@@ -1,10 +1,8 @@
-[TendermintAcc005.qnt][] is a manually translated version of the TLA+
-specification [TendermintAcc005.tla][], which is currently located in the
-directory
-[accoutability](https://github.com/cometbft/cometbft/tree/igor/tendermint-ind-inv/spec/light-client/accountability)
-of [CometBFT][].
-
+[Tendermint.qnt][] is a Quint version of the TLA+ specification
+[TendermintAcc005.tla][], which is currently located under the
+[accountability][] specification of [CometBFT][].
 
 [TendermintAcc005.qnt]: ./TendermintAcc005.qnt
 [TendermintAcc005.tla]: ./tla/TendermintAcc005.tla
 [CometBFT]: https://github.com/cometbft/cometbft
+[accountability]: https://github.com/cometbft/cometbft/tree/main/spec/light-client/accountability

examples/cosmos/tendermint/TendermintAcc005.qnt → examples/cosmos/tendermint/Tendermint.qnt

@@ -1,5 +1,5 @@
 // -*- mode: Bluespec; -*-
-module TendermintAcc {
+module Tendermint {
   /*
    A Quint specification of a simplified Tendermint consensus, tuned for
    fork accountability. The simplifications are as follows:
@@ -320,9 +320,9 @@ module TendermintAcc {
     }
 
   // lines 34-35 + lines 61-64 (onTimeoutPrevote)
-  action UponQuorumOfPrevotesAny(p, Evidence) =
+  action UponQuorumOfPrevotesAny(p: str, Evidence: Set[{ id: Value_t, round: Round_t, src: Proc_t }]): bool =
     // find the unique voters in the evidence
-    val Voters = Evidence.map(m => m.src)
+    val Voters: Set[str] = Evidence.map(m => m.src)
     // compare the number of the unique voters against the threshold
     all {
       step.get(p) == "prevote", // line 34 and 61
@@ -380,9 +380,9 @@ module TendermintAcc {
     }
 
   // lines 47-48 + 65-67 (onTimeoutPrecommit)
-  action UponQuorumOfPrecommitsAny(p, Evidence) =
+  action UponQuorumOfPrecommitsAny(p: str, Evidence: Set[{ id: Value_t, round: Round_t, src: Proc_t }]): bool =
     // find the unique committers in the evidence
-    val Committers =  Evidence.map( m => m.src )
+    val Committers: Set[str] = Evidence.map( m => m.src )
     // compare the number of the unique committers against the threshold
     all {
       size(Committers) >= THRESHOLD2,  // line 47
@@ -531,23 +531,22 @@ module TendermintAcc {
     }
 
   //**************************** FORK SCENARIOS  ***************************
+  def EquivocationIn(p, S) =
+    tuples(S, S).exists((m1, m2) =>
+      and {
+        m1 != m2,
+        m1.src == p,
+        m2.src == p,
+        m1.round == m2.round,
+      }
+    )
 
   // equivocation by a process p
-  def EquivocationBy(p) =
-    def EquivocationIn(S) =
-      tuples(S, S).exists((m1, m2) =>
-        and {
-          m1 != m2,
-          m1.src == p,
-          m2.src == p,
-          m1.round == m2.round,
-        }
-      )
-
+  def EquivocationBy(p: str): bool =
     or {
-      EquivocationIn(evidencePropose),
-      EquivocationIn(evidencePrevote),
-      EquivocationIn(evidencePrecommit),
+      EquivocationIn(p, evidencePropose),
+      EquivocationIn(p, evidencePrevote),
+      EquivocationIn(p, evidencePrecommit),
     }
 
   // amnesic behavior by a process p
@@ -661,122 +660,3 @@ module TendermintAcc {
       AllInMax implies AllDecided
   )
 }
-
-// Tests that demonstrate typical behavior.
-module TendermintTest {
-  import TendermintAcc.*
-  export TendermintAcc.*
-
-  // Quint will automatically compute the unchanged block in the future
-  action unchangedAll = all {
-    step' = step,
-    fired_action' = fired_action,
-    round' = round,
-    validValue' = validValue,
-    validRound' = validRound,
-    msgsPrevote' = msgsPrevote,
-    msgsPropose' = msgsPropose,
-    msgsPrecommit' = msgsPrecommit,
-    decision' = decision,
-    lockedValue' = lockedValue,
-    lockedRound' = lockedRound,
-    evidencePropose' = evidencePropose,
-    evidencePrevote' = evidencePrevote,
-    evidencePrecommit' = evidencePrecommit,
-  }
-
-  // three correct processes behave and decide on the same value
-  run decisionTest = {
-    nondet v = oneOf(ValidValues)
-    val p1 = Proposer.get(0)
-    nondet p2 = Corr.exclude(Set(p1)).oneOf()
-    nondet p3 = Corr.exclude(Set(p1, p2)).oneOf()
-    Init.then(InsertProposal(p1, v))
-        .then(UponProposalInPropose(p1, v))
-        .then(UponProposalInPropose(p2, v))
-        .then(UponProposalInPropose(p3, v))
-        .then(UponProposalInPrevoteOrCommitAndPrevote(p1, v, NilRound))
-        .then(UponProposalInPrevoteOrCommitAndPrevote(p2, v, NilRound))
-        .then(UponProposalInPrevoteOrCommitAndPrevote(p3, v, NilRound))
-        .then(UponProposalInPrecommitNoDecision(p1, v, 0, NilRound))
-        .then(UponProposalInPrecommitNoDecision(p2, v, 0, NilRound))
-        .then(UponProposalInPrecommitNoDecision(p3, v, 0, NilRound))
-        .then(all {
-          assert(decision.get(p1) == v),
-          assert(decision.get(p2) == v),
-          assert(decision.get(p3) == v),
-          unchangedAll,
-        })
-  }
-
-  // a correct proposer cannot propose twice in the same round
-  run noProposeTwiceTest = {
-    val p1 = Proposer.get(0)
-    Init.then(InsertProposal(p1, "v0"))
-        .then(InsertProposal(p1, "v1"))
-        .fail()
-  }
-
-  // a correct proposer proposes but other processes timeout
-  run timeoutProposeTest = {
-    val p1 = Proposer.get(0)
-    nondet p2 = Corr.exclude(Set(p1)).oneOf()
-    nondet p3 = Corr.exclude(Set(p1, p2)).oneOf()
-    Init.then(InsertProposal(p1, "v0"))
-        .then(UponProposalInPropose(p1, "v0"))
-        .then(OnTimeoutPropose(p2))
-        .then(OnTimeoutPropose(p3))
-        .then(
-          val E = msgsPrevote.get(0).filter(m => m.src.in(Corr))
-          UponQuorumOfPrevotesAny(p1, E)
-            .then(UponQuorumOfPrevotesAny(p2, E))
-            .then(UponQuorumOfPrevotesAny(p3, E))
-        )
-        .then(
-          val E = msgsPrecommit.get(0).filter(m => m.src.in(Corr))
-          UponQuorumOfPrecommitsAny(p1, E)
-            .then(UponQuorumOfPrecommitsAny(p2, E))
-            .then(UponQuorumOfPrecommitsAny(p3, E))
-        )
-        .then(all {
-          // all correct processes switch to the next round
-          assert(Corr.forall(p => round.get(p) == 1)),
-          unchangedAll,
-        })
-  }
-}
-
-module InstanceTests {
-  import TendermintTest(
-    Corr = Set("p1", "p2", "p3"),
-    Faulty = Set("p4"),
-    N = 4,
-    T = 1,
-    ValidValues = Set("v0", "v1"),
-    InvalidValues = Set("v2"),
-    MaxRound = 4,
-    Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1")
-  ) as Tendermint_n4_f1
-
-  import TendermintTest(
-    Corr = Set("p1", "p2", "p3"),
-    Faulty = Set("p3", "p4"),
-    N = 4,
-    T = 1,
-    ValidValues = Set("v0", "v1"),
-    InvalidValues = Set("v2"),
-    MaxRound = 4,
-    Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1")
-  ) as Tendermint_n4_f2
-
-  import TendermintTest(
-    Corr = Set("p1", "p2", "p3"),
-    Faulty = Set("p4", "p5"),
-    N = 5,
-    T = 1,
-    ValidValues = Set("v0", "v1"),
-    InvalidValues = Set("v2"),
-    MaxRound = 4,
-    Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1")
-  ) as Tendermint_n5_f2
-}

examples/cosmos/tendermint/TendermintModels.qnt

@@ -0,0 +1,35 @@
+/// A few handy small models that are good for debugging and inspection
+module TendermintModels {
+  import TendermintTest(
+    Corr = Set("p1", "p2", "p3"),
+    Faulty = Set("p4"),
+    N = 4,
+    T = 1,
+    ValidValues = Set("v0", "v1"),
+    InvalidValues = Set("v2"),
+    MaxRound = 4,
+    Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1")
+  ) as n4_f1 from "./TendermintTest"
+
+  import TendermintTest(
+    Corr = Set("p1", "p2", "p3"),
+    Faulty = Set("p3", "p4"),
+    N = 4,
+    T = 1,
+    ValidValues = Set("v0", "v1"),
+    InvalidValues = Set("v2"),
+    MaxRound = 4,
+    Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1")
+  ) as n4_f2 from "./TendermintTest"
+
+  import TendermintTest(
+    Corr = Set("p1", "p2", "p3"),
+    Faulty = Set("p4", "p5"),
+    N = 5,
+    T = 1,
+    ValidValues = Set("v0", "v1"),
+    InvalidValues = Set("v2"),
+    MaxRound = 4,
+    Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1")
+  ) as n5_f2 from "./TendermintTest"
+}

examples/cosmos/tendermint/TendermintTest.qnt

@@ -0,0 +1,83 @@
+// Tests that demonstrate typical behavior.
+module TendermintTest {
+  import Tendermint.* from "./Tendermint"
+  export Tendermint.*
+
+  // Quint will automatically compute the unchanged block in the future
+  action unchangedAll = all {
+    step' = step,
+    fired_action' = fired_action,
+    round' = round,
+    validValue' = validValue,
+    validRound' = validRound,
+    msgsPrevote' = msgsPrevote,
+    msgsPropose' = msgsPropose,
+    msgsPrecommit' = msgsPrecommit,
+    decision' = decision,
+    lockedValue' = lockedValue,
+    lockedRound' = lockedRound,
+    evidencePropose' = evidencePropose,
+    evidencePrevote' = evidencePrevote,
+    evidencePrecommit' = evidencePrecommit,
+  }
+
+  // three correct processes behave and decide on the same value
+  run decisionTest = {
+    nondet v = oneOf(ValidValues)
+    val p1 = Proposer.get(0)
+    nondet p2 = Corr.exclude(Set(p1)).oneOf()
+    nondet p3 = Corr.exclude(Set(p1, p2)).oneOf()
+    Init.then(InsertProposal(p1, v))
+        .then(UponProposalInPropose(p1, v))
+        .then(UponProposalInPropose(p2, v))
+        .then(UponProposalInPropose(p3, v))
+        .then(UponProposalInPrevoteOrCommitAndPrevote(p1, v, NilRound))
+        .then(UponProposalInPrevoteOrCommitAndPrevote(p2, v, NilRound))
+        .then(UponProposalInPrevoteOrCommitAndPrevote(p3, v, NilRound))
+        .then(UponProposalInPrecommitNoDecision(p1, v, 0, NilRound))
+        .then(UponProposalInPrecommitNoDecision(p2, v, 0, NilRound))
+        .then(UponProposalInPrecommitNoDecision(p3, v, 0, NilRound))
+        .then(all {
+          assert(decision.get(p1) == v),
+          assert(decision.get(p2) == v),
+          assert(decision.get(p3) == v),
+          unchangedAll,
+        })
+  }
+
+  // a correct proposer cannot propose twice in the same round
+  run noProposeTwiceTest = {
+    val p1 = Proposer.get(0)
+    Init.then(InsertProposal(p1, "v0"))
+        .then(InsertProposal(p1, "v1"))
+        .fail()
+  }
+
+  // a correct proposer proposes but other processes timeout
+  run timeoutProposeTest = {
+    val p1 = Proposer.get(0)
+    nondet p2 = Corr.exclude(Set(p1)).oneOf()
+    nondet p3 = Corr.exclude(Set(p1, p2)).oneOf()
+    Init.then(InsertProposal(p1, "v0"))
+        .then(UponProposalInPropose(p1, "v0"))
+        .then(OnTimeoutPropose(p2))
+        .then(OnTimeoutPropose(p3))
+        .then(
+          val E = msgsPrevote.get(0).filter(m => m.src.in(Corr))
+          UponQuorumOfPrevotesAny(p1, E)
+            .then(UponQuorumOfPrevotesAny(p2, E))
+            .then(UponQuorumOfPrevotesAny(p3, E))
+        )
+        .then(
+          val E = msgsPrecommit.get(0).filter(m => m.src.in(Corr))
+          UponQuorumOfPrecommitsAny(p1, E)
+            .then(UponQuorumOfPrecommitsAny(p2, E))
+            .then(UponQuorumOfPrecommitsAny(p3, E))
+        )
+        .then(all {
+          // all correct processes switch to the next round
+          assert(Corr.forall(p => round.get(p) == 1)),
+          unchangedAll,
+        })
+  }
+}

quint/cli-tests.md

@@ -70,17 +70,17 @@ Temporarily disabled.
 ### OK on parse Tendermint
 
 <!-- !test check Tendermint -->
-    quint parse ../examples/cosmos/tendermint/TendermintAcc005.qnt
+    quint parse ../examples/cosmos/tendermint/Tendermint.qnt
 
 ### OK on typecheck Tendermint
 
 <!-- !test check Tendermint - Types & Effects -->
-    quint typecheck ../examples/cosmos/tendermint/TendermintAcc005.qnt
+    quint typecheck ../examples/cosmos/tendermint/Tendermint.qnt
 
 ### OK on test Tendermint
 
 <!-- !test check Tendermint - Test -->
-    quint test --max-samples=100 --main InstanceTests ../examples/cosmos/tendermint/TendermintAcc005.qnt
+    quint test --max-samples=100 --main TendermintModels ../examples/cosmos/tendermint/TendermintModels.qnt
 
 ### OK on parse imports