First quint draft that is somewhat complete with consensus, executor,…

… voteKeeper (#40)

* executor start

* PreCommit function

* TODOs

* line 28 is in the books

* prevote, precommit, and timeout done. proposal missing

* starting to put things together for state machine

* a somewhat complete version of the executor logic

* state machine, but needs to be debugged

* moving statemachine. problem with chooseSome

* it moves

* more things moving

* some problem with bookkeeper

* more things move

* I have seen a Polka

* cleanup

* cleaning

* successful test of statemachine

* before consensus return refactor

* first pending event added

* cleaned consensus

* commit to merge with Manuel's updated votekeeper

* to merge Daniel's comment

* executor start

* PreCommit function

* TODOs

* line 28 is in the books

* prevote, precommit, and timeout done. proposal missing

* starting to put things together for state machine

* a somewhat complete version of the executor logic

* state machine, but needs to be debugged

* moving statemachine. problem with chooseSome

* it moves

* more things moving

* some problem with bookkeeper

* more things move

* I have seen a Polka

* cleanup

* cleaning

* successful test of statemachine

* before consensus return refactor

* first pending event added

* cleaned consensus

* commit to merge with Manuel's updated votekeeper

* to merge Daniel's comment

* addressed Daniel's comments

* addressed Daniel's comments and run tests

* completed the timeout test

* clean up and comments

* added checks for increasing round numbers

* added hash function checks

* valset error thrown in test fixed

* added action and logic to get value from the outside into the system

* comments following the discussion on where to put the reponsibility for getValue

* transformed that executed events into list

* added an asynchronous execution environment

* added round number checks to ProposalMsg

* test for disagreement in asynchronous setting

* Parameterization of the Asynchronous model

* Typecheck all Quint specs on CI and run test for `consensustest.qnt`

* Update Specs/Quint/AsyncModels.qnt

Co-authored-by: Romain Ruetschi <romain@informal.systems>

* added a type invariant

* updated syntax to Quint 0.14.4

* moved bookkeeper statemachine out for modularity

* Update Quint test job

* commented a line that failed a test. Need to discuss with Manu

* Run test on all Quint files

* Use script to run all tests even in the presence of failures

* fixed the logic and the test for Precommit,Nil

* Update Specs/Quint/voteBookkeeperTest.qnt

Signed-off-by: Josef Widder <josef@informal.systems>

Co-authored-by: Hernán Vanzetto <15466498+hvanz@users.noreply.github.com>

* rename files for test CI

* Update .github/workflows/quint.yml

* renamed one more file with a test

* module renamed

* start with a test where a process enters round 1 and messages are already around

* added todos

* Pass over the votekeeper spec (#69)

Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com>

---------

Co-authored-by: Romain Ruetschi <romain@informal.systems>
Co-authored-by: Hernán Vanzetto <15466498+hvanz@users.noreply.github.com>

.github/workflows/quint.yml

@@ -15,15 +15,22 @@ 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
+      - run: bash Scripts/quint-forall.sh typecheck Specs/Quint/*.qnt
+
+  quint-test:
+    name: Test
+    runs-on: ubuntu-latest
+    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
 

Scripts/quint-forall.sh

@@ -0,0 +1,48 @@
+#!/bin/env bash
+
+BLUE=$(tput setaf 4)
+RED=$(tput setaf 1)
+RESET=$(tput sgr0)
+UNDERLINE=$(tput smul)
+
+# [INFO] message in blue
+info()
+{
+  echo "${BLUE}[INFO] $*${RESET}"
+} 
+
+# [ERROR] message in red
+error()
+{
+  echo "${RED}[ERROR] $*${RESET} "
+}
+
+# Run `quint $command` on all given files.
+
+cmd="$1"
+files=("${@:2}")
+
+if [[ "${#files[@]}" -eq 0 ]]; then
+  echo "${UNDERLINE}Usage:${RESET} $0 <command> <file> [<file> ...]"
+  exit 1
+fi
+
+failed=0
+failed_files=()
+
+for file in "${files[@]}"; do
+  info "Running: quint $cmd ${UNDERLINE}$file"
+  if ! npx @informalsystems/quint "$cmd" "$file"; then
+    failed_files+=("$file")
+    failed=$((failed + 1))
+  fi
+  echo ""
+done
+
+if [[ "$failed" -gt 0 ]]; then
+  error "Failed on $failed files:"
+  for file in "${failed_files[@]}"; do
+    error " - ${UNDERLINE}$file"
+  done
+  exit 1
+fi

Specs/Quint/asyncModelsTest.qnt

@@ -0,0 +1,158 @@
+// -*- mode: Bluespec; -*-
+
+module asyncModelsTest {
+
+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"
+
+run NewRoundTest = {
+    N4F0::init
+    .then(N4F0::setNextValueToPropose("v2", "block"))
+    .then(N4F0::valStep("v1"))
+    .then(N4F0::valStep("v2"))
+    .then(N4F0::valStep("v3"))
+    .then(N4F0::valStep("v4"))
+    .then(N4F0::valStep("v1"))
+    .then(N4F0::deliverProposal("v2", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 }))
+    .then(N4F0::valStep("v2"))
+    .then(N4F0::valStep("v3")) 
+    .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" }))
+    .then(N4F0::deliverVote("v1", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" }))
+    .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v3", step: "Prevote" }))
+    .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" }))
+    .then(N4F0::deliverVote("v2", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" }))
+    .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v3", step: "Prevote" }))
+    .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" }))
+    .then(N4F0::deliverVote("v3", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" }))
+    .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, 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")) 
+    // timeoutPrevote started
+    .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: "nil", round: 0, src: "v1", step: "Precommit" }))
+    .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" }))
+    .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v3", step: "Precommit" }))
+    .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v1", step: "Precommit" }))
+    .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" }))
+    .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v3", step: "Precommit" }))
+    .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v1", step: "Precommit" }))
+    .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" }))
+    .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, 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"))    
+    .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::valStep("v1"))
+    .then(N4F0::valStep("v2"))
+    .then(N4F0::valStep("v3")) 
+  
+          */              
+}
+
+import statemachineAsync(
+    validators = Set("v1", "v2", "v3", "v4"),
+    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
+    Faulty = Set("v1"),
+    Values = Set("a", "b"),
+    Rounds = Set(0, 1, 2, 3),
+    Heights = Set(0) // , 1, 2, 3)
+) as N4F1 from "./statemachineAsync"
+
+// quint run --init=N4F1::init --step=N4F1::step --invariant=N4F1::AgreementInv AsyncModels.qnt
+// quint run --init=N4F1::init --step=N4F1::step --invariant=N4F1::ConsensusOutputInv AsyncModels.qnt
+
+import statemachineAsync(
+    validators = Set("v1", "v2", "v3", "v4"),
+    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
+    Faulty = Set("v1", "v2"),
+    Values = Set("a", "b"),
+    Rounds = Set(0),  // , 1, 2, 3)
+    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
+// this run leads to disagreement
+run DisagreementTest = {
+    N4F2::init
+    .then(N4F2::valStep("v3"))
+    .then(N4F2::valStep("v4"))
+    .then(N4F2::deliverProposal("v3", { height: 0, proposal: "b", round: 0, src: "v2", validRound: -1 }))
+    .then(N4F2::deliverProposal("v4", { height: 0, proposal: "a", round: 0, src: "v2", validRound: -1 }))
+    .then(N4F2::valStep("v3"))
+    .then(N4F2::valStep("v4"))
+    .then(all{
+        // they voted diN4F2N4F2erently
+        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" }),
+            "v4" -> Set({ height: 0, id: "a", round: 0, src: "v4", step: "Prevote" }, 
+                        { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }))),
+            N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v1", step: "Prevote" })
+    })
+    .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v2", step: "Prevote" }))
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v1", step: "Prevote" }))
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v2", step: "Prevote" }))
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }))
+    .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v4", step: "Prevote" }))
+    .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(all{
+        // they precommited diN4F2N4F2erently
+        assert( N4F2::voteBuffer.get("v3").contains({ height: 0, id: "a", round: 0, src: "v4", step: "Precommit" }) and
+                N4F2::voteBuffer.get("v4").contains({ height: 0, id: "b", round: 0, src: "v3", step: "Precommit" })), 
+        N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v1", step: "Precommit" }) })
+    .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v2", step: "Precommit" }))    
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v1", step: "Precommit" })) 
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v2", step: "Precommit" })) 
+    .then(N4F2::valStep("v3"))  
+    .then(N4F2::valStep("v3"))   
+    .then(N4F2::valStep("v4"))
+    .then(N4F2::valStep("v4"))
+    .then(all{
+        assert(N4F2::AgreementInv),
+        N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v4", step: "Precommit" }) })
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v3", step: "Precommit" }))
+    .then(N4F2::valStep("v3"))   
+    .then(N4F2::valStep("v4"))
+    .then(all{
+        assert(not(N4F2::AgreementInv)),
+        N4F2::unchangedAll})   
+}
+
+
+
+}