Merge branch 'main' into romac/rust-state-machine

.github/workflows/quint.yml

@@ -0,0 +1,29 @@
+on:
+  workflow_dispatch:
+  push:
+    branches:
+      - main
+    paths:
+      - Specs/Quint/**
+  pull_request:
+    paths:
+      - Specs/Quint/**
+
+name: Quint
+
+jobs:
+  quint-typecheck:
+    name: Typecheck
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: ./Specs/Quint
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v3
+        with:
+          node-version: "18"
+      - run: npm install -g @informalsystems/quint
+      - run: npx @informalsystems/quint typecheck consensus.qnt
+      - run: npx @informalsystems/quint typecheck voteBookkeeper.qnt
+

Specs/Quint/0DecideNonProposerTest.itf.json

@@ -0,0 +1 @@
+{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"consensus.qnt","status":"passed","description":"Created by Quint on Wed Oct 25 2023 15:38:28 GMT+0200 (Central European Summer Time)","timestamp":1698241108633},"vars":["system","_Event","_Result"],"states":[{"#meta":{"index":0},"_Event":{"height":-1,"name":"Initial","round":-1,"value":"","vr":-1},"_Result":{"decided":"","name":"","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"newRound","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":1},"_Event":{"height":1,"name":"NewRound","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":2},"_Event":{"height":1,"name":"NewRound","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":3},"_Event":{"height":1,"name":"Proposal","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":4},"_Event":{"height":1,"name":"Proposal","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":5},"_Event":{"height":1,"name":"ProposalAndPolkaAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"precommit","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":6},"_Event":{"height":1,"name":"ProposalAndPolkaAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":1,"id":"block","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"precommit","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":7},"_Event":{"height":1,"name":"ProposalAndCommitAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"block","name":"decided","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"decided","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":8},"_Event":{"height":1,"name":"ProposalAndCommitAndValid","round":0,"value":"block","vr":-1},"_Result":{"decided":"block","name":"decided","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":1,"lockedRound":0,"lockedValue":"block","p":"Josef","round":0,"step":"decided","validRound":0,"validValue":"block"}]]}},{"#meta":{"index":9},"_Event":{"height":2,"name":"NewHeight","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"newRound","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":10},"_Event":{"height":2,"name":"NewHeight","round":0,"value":"","vr":-1},"_Result":{"decided":"","name":"","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"newRound","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":11},"_Event":{"height":2,"name":"NewRoundProposer","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"proposal","proposal":{"height":2,"proposal":"nextBlock","round":0,"src":"Josef","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":12},"_Event":{"height":2,"name":"NewRoundProposer","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"proposal","proposal":{"height":2,"proposal":"nextBlock","round":0,"src":"Josef","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":13},"_Event":{"height":2,"name":"Proposal","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nextBlock","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":14},"_Event":{"height":2,"name":"Proposal","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nextBlock","round":0,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":15},"_Event":{"height":2,"name":"PolkaAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrevote","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":16},"_Event":{"height":2,"name":"PolkaAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrevote","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":17},"_Event":{"height":2,"name":"TimeoutPrevote","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":18},"_Event":{"height":2,"name":"TimeoutPrevote","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":0,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":19},"_Event":{"height":2,"name":"PrecommitAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":20},"_Event":{"height":2,"name":"PrecommitAny","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":21},"_Event":{"height":2,"name":"TimeoutPrecommit","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":22},"_Event":{"height":2,"name":"TimeoutPrecommit","round":0,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":1,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":0,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":23},"_Event":{"height":2,"name":"NewRound","round":1,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":24},"_Event":{"height":2,"name":"NewRound","round":1,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":25},"_Event":{"height":2,"name":"TimeoutPropose","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":26},"_Event":{"height":2,"name":"TimeoutPropose","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"prevote","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":27},"_Event":{"height":2,"name":"PolkaNil","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":28},"_Event":{"height":2,"name":"PolkaNil","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":1,"src":"Josef","step":"precommit"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":29},"_Event":{"height":2,"name":"PrecommitAny","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":30},"_Event":{"height":2,"name":"PrecommitAny","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPrecommit","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":31},"_Event":{"height":2,"name":"TimeoutPrecommit","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":2,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":32},"_Event":{"height":2,"name":"TimeoutPrecommit","round":1,"value":"nextBlock","vr":-1},"_Result":{"decided":"","name":"skipRound","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":2,"timeout":"","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":1,"step":"precommit","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":33},"_Event":{"height":2,"name":"NewRound","round":2,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":2,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":34},"_Event":{"height":2,"name":"NewRound","round":2,"value":"","vr":-1},"_Result":{"decided":"","name":"timeout","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"timeoutPropose","voteMessage":{"height":-1,"id":"","round":-1,"src":"","step":""}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":2,"step":"propose","validRound":-1,"validValue":"nil"}]]}},{"#meta":{"index":35},"_Event":{"height":2,"name":"ProposalInvalid","round":2,"value":"","vr":-1},"_Result":{"decided":"","name":"votemessage","proposal":{"height":-1,"proposal":"","round":-1,"src":"","validRound":-1},"skipRound":-1,"timeout":"","voteMessage":{"height":2,"id":"nil","round":2,"src":"Josef","step":"prevote"}},"system":{"#map":[["Josef",{"height":2,"lockedRound":-1,"lockedValue":"nil","p":"Josef","round":2,"step":"prevote","validRound":-1,"validValue":"nil"}]]}}]}