Merge branch 'main' into fix

cosmos · Dec 19, 2023 · 92a253b · 92a253b
2 parents 0a5d214 + 634efd3
commit 92a253b
Show file tree

Hide file tree

Showing 74 changed files with 3,103 additions and 9,125 deletions.
diff --git a/.github/.codespellignore b/.github/.codespellignore
@@ -0,0 +1,3 @@
+clienta
+connectiona
+sover
diff --git a/.github/PULL_REQUEST_TEMPLATE/production.md b/.github/PULL_REQUEST_TEMPLATE/production.md
@@ -19,7 +19,7 @@ please add links to any relevant follow up issues.*
 I have...
 
 * [ ] Included the correct [type prefix](https://github.com/commitizen/conventional-commit-types/blob/v3.0.0/index.json) in the PR title
-* [ ] Added `!` to the type prefix if state-machine breaking change (i.e., requires coordinated upgrade)
+* [ ] Added `!` to the type prefix if the change is [state-machine breaking](https://github.com/cosmos/interchain-security/blob/main/RELEASES.md#breaking-changes)
 * [ ] Confirmed this PR does not introduce changes requiring state migrations, OR migration code has been added to consumer and/or provider modules
 * [ ] Targeted the correct branch (see [PR Targeting](https://github.com/cosmos/interchain-security/blob/main/CONTRIBUTING.md#pr-targeting))
 * [ ] Provided a link to the relevant issue or specification
@@ -40,7 +40,7 @@ your handle next to the items reviewed if you only reviewed selected items.*
 I have...
 
 * [ ] confirmed the correct [type prefix](https://github.com/commitizen/conventional-commit-types/blob/v3.0.0/index.json) in the PR title
-* [ ] confirmed `!` in the type prefix if API or client breaking change
+* [ ] confirmed `!` the type prefix if the change is state-machine breaking
 * [ ] confirmed this PR does not introduce changes requiring state migrations, OR confirmed migration code has been added to consumer and/or provider modules
 * [ ] confirmed all author checklist items have been addressed
 * [ ] reviewed state machine logic

diff --git a/.github/workflows/codespell.yml b/.github/workflows/codespell.yml
@@ -0,0 +1,28 @@
+name: Fix typos nightly
+
+on:
+  schedule:
+    - cron: "0 12 * * *"
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - name: Run codespell
+        continue-on-error: true
+        run: |
+          sudo apt-get install codespell -y
+          codespell -w --skip="*.pb.go,*.pb.gw.go,*.json,*.git,*.js" --ignore-words=.github/.codespellignore
+      - uses: peter-evans/create-pull-request@v5
+        with:
+          token: ${{ secrets.PRBOT_PAT }}
+          commit-message: "chore: spelling errors fixes"
+          title: "chore: fix spelling errors"
+          branch: "bot/fix-typos"
+          delete-branch: true
+          body: |
+            This PR fixes typos in the codebase.
+            Please review it, and merge if everything is fine.
+            If there are proto changes, run `make proto-gen` and commit the changes.
diff --git a/.github/workflows/test.yml b/.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]
@@ -135,18 +147,18 @@ jobs:
             go.sum
             **/go.mod
             **/go.sum
-      - uses: actions/download-artifact@v3
+      - uses: actions/download-artifact@v4
         if: env.GIT_DIFF
         with:
           name: "${{ github.sha }}-coverage"
-      - uses: actions/download-artifact@v3
+      - uses: actions/download-artifact@v4
         if: env.GIT_DIFF
         with:
           name: "${{ github.sha }}-integration-coverage"
-      - uses: actions/download-artifact@v3
+      - uses: actions/download-artifact@v4
         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 }}
@@ -181,7 +193,9 @@ jobs:
             **/Makefile
             Makefile
       - name: e2e tests
-        run: make test-e2e-short
+        if: env.GIT_DIFF
+        run: |
+          make test-e2e-short
   
   test-cometmock:
     runs-on: ubuntu-latest
@@ -209,7 +223,9 @@ jobs:
             **/Makefile
             Makefile
       - name: cometmock tests
-        run: make test-e2e-short-cometmock
+        if: env.GIT_DIFF
+        run: |
+          make test-e2e-short-cometmock
   
   test-trace:
     runs-on: ubuntu-latest
@@ -237,4 +253,28 @@ jobs:
             **/Makefile
             Makefile
       - name: trace-e2e tests
-        run: make test-trace
+        if: env.GIT_DIFF
+        run: |
+          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
diff --git a/Makefile b/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                                  ###
 ###############################################################################

diff --git a/TESTING.md b/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, integration, and mbt tests - shortcut for local development
 make test-dev
 
 # run E2E tests

diff --git a/app/consumer-democracy/proposals_whitelisting_test.go b/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

diff --git a/docs/docs/consumer-development/onboarding.md b/docs/docs/consumer-development/onboarding.md
@@ -95,7 +95,7 @@ Example of a consumer chain addition proposal.
 	// sub-protocol. If DistributionTransmissionChannel == "", a new transfer
 	// channel is created on top of the same connection as the CCV channel.
 	// Note that transfer_channel_id is the ID of the channel end on the consumer chain.
-    // it is most relevant for chains performing a sovereign to consumer changeover
+    // it is most relevant for chains performing a standalone to consumer changeover
     // in order to maintain the existing ibc transfer channel
     "distribution_transmission_channel": "channel-123"
 }

diff --git a/docs/docs/features/proposals.md b/docs/docs/features/proposals.md
@@ -43,7 +43,7 @@ Minimal example:
     "historical_entries": 10000,
     "genesis_hash": "d86d756e10118e66e6805e9cc476949da2e750098fcc7634fd0cc77f57a0b2b0",
     "binary_hash": "376cdbd3a222a3d5c730c9637454cd4dd925e2f9e2e0d0f3702fc922928583f1"
-    // relevant for chains performing a sovereign to consumer changeover
+    // relevant for chains performing a standalone to consumer changeover
     // in order to maintain the existing ibc transfer channel
     "distribution_transmission_channel": "channel-123"
 }
@@ -75,18 +75,38 @@ Minimal example:
 ```
 
 ## ChangeRewardDenomProposal
-:::tip
-`ChangeRewardDenomProposal` will only be accepted on the provider chain if at least one of the denomsToAdd or denomsToRemove fields is populated with at least one denom. Also, a denom cannot be repeated in both sets.
-:::
 
 Proposal type used to mutate the set of denoms accepted by the provider as rewards.
 
+:::tip
+A `ChangeRewardDenomProposal` will only be accepted on the provider chain if at least one of the `denomsToAdd` or `denomsToRemove` fields is populated with at least one denom. Also, a denom cannot be repeated in both sets.
+:::
+
 Minimal example:
 ```js
+{
+  "title": "Add uatom as a reward denom",
+  "description": "Here is more information about the proposal",
+  "denomsToAdd": ["uatom"],
+  "denomsToRemove": []
+}
+```
+
+:::tip
+Besides native provider denoms (e.g., `uatom` for the Cosmos Hub), please use the `ibc/*` denom trace format.
+For example, for `untrn` transferred over the path `transfer/channel-569`, the denom trace 
+can be queried using the following command:
+```bash
+> gaiad query ibc-transfer denom-hash transfer/channel-569/untrn
+hash: 0025F8A87464A471E66B234C4F93AEC5B4DA3D42D7986451A059273426290DD5
+```
+Then use the resulting hash in the `ChangeRewardDenomProposal`, e.g., 
+```js
 {
   "title": "Add untrn as a reward denom",
   "description": "Here is more information about the proposal",
-  "denomsToAdd": ["untrn"],
+  "denomsToAdd": ["ibc/0025F8A87464A471E66B234C4F93AEC5B4DA3D42D7986451A059273426290DD5"],
   "denomsToRemove": []
 }
 ```
+:::