test: Replace difftest model with Quint=>MBT (#1369)

* Start adding mbt using Quint model

* Clean up dependencies

* Start taking difftest code for mbt

* Implement chain startup

* Rewrite chain startup

* Continue chain setup

* Add trusting period

* Adjust tests for fee testing

* Use correct validators in RequestInitChain

* Remove min and max functions

* Add type annotations

* Make state printing more robust

* Fix setting default power reduction

* Adjust max steps and run all tests

* Change semantics of VotingPowerChange to take change amount, not new total

* Adjust voting power choices to be changes instead of absolute values

* Start refactoring relaying code

* Refactor map to list of pairs

* Add libraries for map rewrite

* Start fixing client updates

* Add ccv_happy module as a happyPath variant

* Fix model: packets are emitted based on the timestamp of the last block, not the new block

* Add viewer for ModelState and fix model-system equivalence checks

* Add type annotations

* Add ack delivery after each step

* Add programmatic ways of generating traces

* Make invariant optional

* Pretty up the output

* Add script for generating happy and normal traces

* Remove message sends for consumers that were started in this block

* Use .itf extension instead of .json

* Start adjusting behaviour for started/stopped consumers

* Use GetEmptyProtocolState instead of verbose declaration

* Add expired status and set timestamps of new consumers

* Add note to split up timestamps

* Advance MBT prototype

* Add test case for expired clients

* Adjust tests for new timestamp handling

* Use -1 as last timestamp when no block was comitted

* Fix client expiration conditions

* Start writing model with boundeddrift

* Add model with bounded drift

* Rename module to match filename

* Add extra log output and trace gen scripts

* Add Apalache output folder to gitignore

* Remove expired clients

* Remove different time offsets for different chains

* Fix timestamp

* Fix error where we would choose nondet from empty sets

* Add timeout timestamps to packets

* Adapt tests to the empty-validator-power behaviour

* Adjust timeout test

* Add logic for comparing timestamps of packets

* Fix: VSCTimeout is based on EndBlocj

* Add logic for timed out vsc packets

* Fix vsc timeouts should happen during endblock

* Revert the timestamp change

* Add more diverse traces

* Fix acct sequences not incrementing when messages error ot

* Move from difference folder to mbt folder

* Add back consumer chain stopping

* Disallow empty validator sets

* Add README and generate fewer traces

* Remove difftest link from old docs

* Revert changes to e2e tests

* Fix link to MBT

* Tidy go mod and use go 1.20

* Start linting

* Lint files

* Add nolint instruction from main

* Do not check for errors for consumer chain stopping

* Add mbt to makefile and CI

* Move reference to difftests into reference to MBT

* Remove cache npm

* Fix test-mbt-cov Make instructions

* Generate less traces and fix path for testing

* Fix test path

* Archive traces in workflow

* Add long version of MBT to makefile

* Use variable instead of true to better signal semantics

* Update testutil/simibc/chain_util.go

* Address comments

* Add punctuation remoced due to main merge

* Remove outdated doc line

* Add Quint tests to CI

* Update tests/mbt/model/ccv_model.qnt

Co-authored-by: insumity <[email protected]>

* Address comments

* Add zero check to VotingPowerChangeToEmptyTest

* Incorporate Karolos' comments

* Add spacing between jobs

* Update tests/mbt/model/ccv_model.qnt

Co-authored-by: insumity <[email protected]>

* Address comments

* Remove 4 week time advancement

* Upload traces even when test fails

* Fix condition for trace archival

* Remove unused index

* Remove outdated for loop

* Fix if condition for trace upload

* Add comment about timestamps

* Remove long time advancements

* Address comments

* Make comment clearer

* Update tests/mbt/driver/generate_traces.sh

Co-authored-by: Simon Noetzlin <[email protected]>

* Update tests/mbt/run_invariants.sh

Co-authored-by: Simon Noetzlin <[email protected]>

* Update tests/mbt/driver/README.md

Co-authored-by: Simon Noetzlin <[email protected]>

* Update testutil/simibc/relayed_path.go

Co-authored-by: Simon Noetzlin <[email protected]>

* Update tests/mbt/driver/generate_more_traces.sh

Co-authored-by: Simon Noetzlin <[email protected]>

* Remove difftest folder

* Minor fixes based on PR comments

* Make timedout status a const

* Lengthen retention to 6 days

---------

Co-authored-by: insumity <[email protected]>
Co-authored-by: Simon Noetzlin <[email protected]>

.github/workflows/test.yml

@@ -90,7 +90,7 @@ jobs:
           name: "${{ github.sha }}-integration-coverage"
           path: ./integration-profile.out
 
-  test-difference:
+  test-mbt:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
@@ -100,6 +100,11 @@ jobs:
           check-latest: true
           cache: true
           cache-dependency-path: go.sum
+      - uses: actions/setup-node@v4
+        with:
+          node-version: ">= 18"
+          check-latest: true
+      - run: npm i @informalsystems/quint -g
       - uses: technote-space/[email protected]
         id: git_diff
         with:
@@ -111,19 +116,26 @@ jobs:
             **/go.sum
             **/Makefile
             Makefile
-      - name: difference tests
+      - name: mbt tests
         if: env.GIT_DIFF
         run: |
-          make test-difference-cov
+          make test-mbt-cov
       - uses: actions/upload-artifact@v3
         if: env.GIT_DIFF
         with:
-          name: "${{ github.sha }}-difference-coverage"
-          path: ./difference-profile.out
-
+          name: "${{ github.sha }}-mbt-coverage"
+          path: ./mbt-profile.out
+      - name: Archive MBT traces
+        uses: actions/upload-artifact@v3
+        if: ${{ success() || failure() }} # to upload the traces only when the test failed
+        with:
+          name: mbt-traces
+          path: tests/mbt/driver/traces
+          retention-days: 6 # to not clog our cloud storage too much, we retain only for a few days
+
   repo-analysis:
     runs-on: ubuntu-latest
-    needs: [tests, test-integration, test-difference]
+    needs: [tests, test-integration, test-mbt]
     steps:
       - uses: actions/checkout@v4
       - uses: technote-space/[email protected]
@@ -146,7 +158,7 @@ jobs:
       - uses: actions/download-artifact@v3
         if: env.GIT_DIFF
         with:
-          name: "${{ github.sha }}-difference-coverage"
+          name: "${{ github.sha }}-mbt-coverage"
         continue-on-error: true
       - name: sonarcloud
         if: ${{ env.GIT_DIFF && !github.event.pull_request.draft }}
@@ -243,4 +255,26 @@ jobs:
       - name: trace-e2e tests
         if: env.GIT_DIFF
         run: |
-          run: make test-trace
+          make test-trace
+  model-analysis:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          lfs: true
+      - name: checkout LFS objects
+        run: git lfs checkout
+      - uses: actions/setup-node@v4
+        with:
+          node-version: ">= 18"
+          check-latest: true
+      - run: npm i @informalsystems/quint -g
+      - uses: technote-space/[email protected]
+        id: git_diff
+        with:
+          PATTERNS: |
+            tests/mbt/model/**.qnt
+      - name: verify the Quint model
+        if: env.GIT_DIFF
+        run: |
+          make verify-models

Makefile

@@ -10,10 +10,10 @@ install: go.sum
 		go install $(BUILD_FLAGS) ./cmd/interchain-security-sd
 
 # run all tests: unit, integration, diff, and E2E
-test: test-unit test-integration test-difference test-e2e
+test: test-unit test-integration test-mbt test-e2e
 
 # shortcut for local development
-test-dev: test-unit test-integration test-difference
+test-dev: test-unit test-integration test-mbt
 
 # run unit tests
 test-unit:
@@ -29,12 +29,25 @@ test-integration:
 test-integration-cov:
 	go test ./tests/integration/... -timeout 30m -coverpkg=./... -coverprofile=integration-profile.out -covermode=atomic
 
-# run difference tests
-test-difference:
-	go test ./tests/difference/... -timeout 30m
-
-test-difference-cov:
-	go test ./tests/difference/... -timeout 30m -coverpkg=./... -coverprofile=difference-profile.out -covermode=atomic
+# run mbt tests
+test-mbt:
+	cd tests/mbt/driver;\
+	sh generate_traces.sh;\
+	cd ../../..;\
+	go test ./tests/mbt/... -timeout 30m
+
+test-mbt-cov:
+	cd tests/mbt/driver;\
+	sh generate_traces.sh;\
+	cd ../../..;\
+	go test ./tests/mbt/... -timeout 30m -coverpkg=./... -coverprofile=mbt-profile.out -covermode=atomic
+
+# runs mbt tests, but generates more traces
+test-mbt-more-traces:
+	cd tests/mbt/driver;\
+	sh generate_more_traces.sh;\
+	cd ../../..;\
+	go test ./tests/mbt/... -timeout 30m
 
 # run E2E tests
 test-e2e:
@@ -92,6 +105,16 @@ test-no-cache:
 test-trace:
 	go run ./tests/e2e/... --test-file tests/e2e/tracehandler_testdata/happyPath.json::default
 
+# tests and verifies the Quint models.
+# Note: this is *not* using the Quint models to test the system,
+# this tests/verifies the Quint models *themselves*.
+verify-models:
+	quint test tests/mbt/model/ccv_test.qnt;\
+	quint test tests/mbt/model/ccv_model.qnt;\
+	quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" tests/mbt/model/ccv_model.qnt --max-steps 200 --max-samples 200
+
+
+
 ###############################################################################
 ###                                Linting                                  ###
 ###############################################################################

TESTING.md

@@ -14,9 +14,9 @@ Unit tests are useful for simple standalone functionality, and CRUD operations.
 
 To run integration tests against your own consumer/provider implementations, use [instance_test.go](tests/integration/instance_test.go) as an example. All you'll need to do is make sure your applications implement the necessary interfaces defined in [interfaces.go](testutil/integration/interfaces.go), pattern match [specific_setup.go](testutil/ibc_testing/specific_setup.go), then pass in the appropriate types and parameters to the suite, as is done in `instance_test.go` for the dummy provider/consumer implementations.
 
-## Differential Tests (WIP)
+## Model-Based Tests (MBT)
 
-[Differential tests](tests/difference/) is similar to integration tests, but they compare the system state to an expected state generated from a model implementation.
+[MBT](tests/mbt/) tests are similar to integration tests, but they compare the system state to an expected state generated from a formally verified specification written in Quint.
 
 ## End-to-End (E2E) Tests 
 
@@ -35,10 +35,10 @@ make test-unit
 # run integration tests
 make test-integration
 
-# run difference tests
-make test-difference
+# run mbt tests
+make test-mbt
 
-# run unit, integration, and difference tests - shortcut for local development
+# run unit and integration, and mbt tests - shortcut for local development
 mate test-dev
 
 # run E2E tests
@@ -128,4 +128,4 @@ If using VSCode, see [vscode-go/wiki/debugging](https://github.com/golang/vscode
 
 ## More
 
-More instructions will be added soon, in time for the testnet. 
+More instructions will be added soon, in time for the testnet. 

app/consumer-democracy/proposals_whitelisting_test.go

@@ -12,7 +12,8 @@ import (
 )
 
 func TestDemocracyGovernanceWhitelistingKeys(t *testing.T) {
-	_, valUpdates, _ := testutil.CreateValidators(t, 4)
+	_, valUpdates, _, err := testutil.CreateValidators(4)
+	require.NoError(t, err)
 	ibctesting.DefaultTestingAppInit = icstestingutils.DemocracyConsumerAppIniter(valUpdates)
 	chain := ibctesting.NewTestChain(t, ibctesting.NewCoordinator(t, 0), "test")
 	paramKeeper := chain.App.(*appConsumer.App).ParamsKeeper

go.mod

@@ -166,6 +166,7 @@ require (
 )
 
 require (
+	github.com/informalsystems/itf-go v0.0.1
 	github.com/spf13/viper v1.16.0
 	google.golang.org/genproto/googleapis/api v0.0.0-20230822172742-b8732ec3820d
 )

go.sum

@@ -654,6 +654,8 @@ github.com/inconshreveable/mousetrap v1.0.0/go.mod h1:PxqpIevigyE2G7u3NXJIT2ANyt
 github.com/inconshreveable/mousetrap v1.1.0 h1:wN+x4NVGpMsO7ErUn/mUI3vEoE6Jt13X2s0bqwp9tc8=
 github.com/inconshreveable/mousetrap v1.1.0/go.mod h1:vpF70FUmC8bwa3OWnCshd2FqLfsEA9PFc4w1p2J65bw=
 github.com/influxdata/influxdb1-client v0.0.0-20191209144304-8bf82d3c094d/go.mod h1:qj24IKcXYK6Iy9ceXlo3Tc+vtHo9lIhSX5JddghvEPo=
+github.com/informalsystems/itf-go v0.0.1 h1:lVvdg3v+IMWOsVfIvOOGy1hHFO5KxoS8b8EiwKLbQDg=
+github.com/informalsystems/itf-go v0.0.1/go.mod h1:wgqaQ/yl2kbNlgw6GaleuHEefpZvkZo6Hc0jc8cGG9M=
 github.com/jhump/protoreflect v1.15.1 h1:HUMERORf3I3ZdX05WaQ6MIpd/NJ434hTp5YiKgfCL6c=
 github.com/jmespath/go-jmespath v0.0.0-20180206201540-c2b33e8439af/go.mod h1:Nht3zPeWKUH0NzdCt2Blrr5ys8VGpn0CEB0cQHVjt7k=
 github.com/jmespath/go-jmespath v0.4.0 h1:BEgLn5cpjn8UN1mAw4NjwDrS35OdebyEtFe+9YPoQUg=