test: Replace difftest model with Quint=>MBT

.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=