Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 117 commits into from
Dec 18, 2023
Merged
Show file tree
Hide file tree
Changes from 115 commits
Commits
Show all changes
117 commits
Select commit Hold shift + click to select a range
a4840fc
Start adding mbt using Quint model
p-offtermatt Oct 19, 2023
5ffe647
Clean up dependencies
p-offtermatt Oct 19, 2023
5f96643
Start taking difftest code for mbt
p-offtermatt Nov 1, 2023
2285a4c
Implement chain startup
p-offtermatt Nov 2, 2023
ae5b106
Rewrite chain startup
p-offtermatt Nov 2, 2023
50231fb
Continue chain setup
p-offtermatt Nov 6, 2023
2d29208
Add trusting period
p-offtermatt Nov 6, 2023
81bcd3b
Adjust tests for fee testing
p-offtermatt Nov 7, 2023
eedcf46
Use correct validators in RequestInitChain
p-offtermatt Nov 7, 2023
1bb6ed0
Remove min and max functions
p-offtermatt Nov 7, 2023
065f458
Add type annotations
p-offtermatt Nov 8, 2023
b1fde43
Make state printing more robust
p-offtermatt Nov 8, 2023
44914e2
Fix setting default power reduction
p-offtermatt Nov 8, 2023
e9d7107
Adjust max steps and run all tests
p-offtermatt Nov 8, 2023
b8640d9
Change semantics of VotingPowerChange to take change amount, not new …
p-offtermatt Nov 8, 2023
a8f45c4
Adjust voting power choices to be changes instead of absolute values
p-offtermatt Nov 8, 2023
ef7a80e
Start refactoring relaying code
p-offtermatt Nov 8, 2023
6336273
Refactor map to list of pairs
p-offtermatt Nov 10, 2023
dd9d878
Add libraries for map rewrite
p-offtermatt Nov 10, 2023
61b6a85
Start fixing client updates
p-offtermatt Nov 10, 2023
abc12cf
Add ccv_happy module as a happyPath variant
p-offtermatt Nov 14, 2023
ad25029
Fix model: packets are emitted based on the timestamp of the last blo…
p-offtermatt Nov 16, 2023
fea71dc
Add viewer for ModelState and fix model-system equivalence checks
p-offtermatt Nov 16, 2023
8f8d2c4
Add type annotations
p-offtermatt Nov 20, 2023
6dacc09
Add ack delivery after each step
p-offtermatt Nov 22, 2023
2c3a6d5
Add programmatic ways of generating traces
p-offtermatt Nov 22, 2023
71a3b80
Make invariant optional
p-offtermatt Nov 22, 2023
c510e61
Pretty up the output
p-offtermatt Nov 22, 2023
db16905
Add script for generating happy and normal traces
p-offtermatt Nov 22, 2023
436aec4
Remove message sends for consumers that were started in this block
p-offtermatt Nov 23, 2023
5d17552
Use .itf extension instead of .json
p-offtermatt Nov 23, 2023
d085cce
Start adjusting behaviour for started/stopped consumers
p-offtermatt Nov 23, 2023
3a7564e
Use GetEmptyProtocolState instead of verbose declaration
p-offtermatt Nov 24, 2023
1b8ae7b
Add expired status and set timestamps of new consumers
p-offtermatt Nov 24, 2023
c7cba8b
Add note to split up timestamps
p-offtermatt Nov 24, 2023
2d130df
Advance MBT prototype
p-offtermatt Nov 24, 2023
8f31705
Add test case for expired clients
p-offtermatt Nov 27, 2023
8681895
Adjust tests for new timestamp handling
p-offtermatt Nov 28, 2023
f229db7
Use -1 as last timestamp when no block was comitted
p-offtermatt Nov 28, 2023
8bbb86a
Fix client expiration conditions
p-offtermatt Nov 28, 2023
9237c34
Start writing model with boundeddrift
p-offtermatt Nov 28, 2023
2b9873a
Add model with bounded drift
p-offtermatt Nov 28, 2023
dd2cd7c
Rename module to match filename
p-offtermatt Nov 28, 2023
603a668
Add extra log output and trace gen scripts
p-offtermatt Nov 28, 2023
719614c
Add Apalache output folder to gitignore
p-offtermatt Nov 28, 2023
468dc7f
Remove expired clients
p-offtermatt Nov 28, 2023
31bd231
Remove different time offsets for different chains
p-offtermatt Nov 29, 2023
76dcc15
Fix timestamp
p-offtermatt Nov 29, 2023
3286e09
Fix error where we would choose nondet from empty sets
p-offtermatt Nov 29, 2023
1433ee4
Add timeout timestamps to packets
p-offtermatt Nov 29, 2023
0f8228d
Adapt tests to the empty-validator-power behaviour
p-offtermatt Nov 29, 2023
6887906
Adjust timeout test
p-offtermatt Nov 29, 2023
ab1430a
Add logic for comparing timestamps of packets
p-offtermatt Nov 29, 2023
dbbe2b0
Fix: VSCTimeout is based on EndBlocj
p-offtermatt Nov 29, 2023
680f3c4
Add logic for timed out vsc packets
p-offtermatt Nov 29, 2023
4238978
Fix vsc timeouts should happen during endblock
p-offtermatt Nov 29, 2023
2d1a874
Revert the timestamp change
p-offtermatt Nov 29, 2023
bcdd85c
Add more diverse traces
p-offtermatt Nov 29, 2023
eacfd87
Fix acct sequences not incrementing when messages error ot
p-offtermatt Nov 30, 2023
33de97b
Move from difference folder to mbt folder
p-offtermatt Nov 30, 2023
0e584c3
Add back consumer chain stopping
p-offtermatt Nov 30, 2023
95e5253
Disallow empty validator sets
p-offtermatt Nov 30, 2023
d272b73
Add README and generate fewer traces
p-offtermatt Nov 30, 2023
5dcf517
merge in main
p-offtermatt Nov 30, 2023
684a2e5
Remove difftest link from old docs
p-offtermatt Nov 30, 2023
703e462
Fix merge conflicts
p-offtermatt Nov 30, 2023
b8db7bc
Revert changes to e2e tests
p-offtermatt Nov 30, 2023
ce62ab0
Fix link to MBT
p-offtermatt Nov 30, 2023
7eeb540
Tidy go mod and use go 1.20
p-offtermatt Nov 30, 2023
2a9c39b
Start linting
p-offtermatt Nov 30, 2023
b533d1f
Lint files
p-offtermatt Nov 30, 2023
4c205f6
Add nolint instruction from main
p-offtermatt Nov 30, 2023
4c74bcb
Do not check for errors for consumer chain stopping
p-offtermatt Nov 30, 2023
fc48575
Add mbt to makefile and CI
p-offtermatt Nov 30, 2023
680b9df
Move reference to difftests into reference to MBT
p-offtermatt Nov 30, 2023
10ced0a
Remove cache npm
p-offtermatt Nov 30, 2023
8bce148
Fix test-mbt-cov Make instructions
p-offtermatt Nov 30, 2023
d00a1cc
Generate less traces and fix path for testing
p-offtermatt Nov 30, 2023
df7ea65
Fix test path
p-offtermatt Nov 30, 2023
6b99c02
Archive traces in workflow
p-offtermatt Dec 1, 2023
e2ee8a2
Add long version of MBT to makefile
p-offtermatt Dec 1, 2023
0ac3c8a
Use variable instead of true to better signal semantics
p-offtermatt Dec 4, 2023
db9a697
Update testutil/simibc/chain_util.go
p-offtermatt Dec 4, 2023
bf2d8d5
Address comments
p-offtermatt Dec 5, 2023
064188e
Merge branch 'main' into ph/mbt
p-offtermatt Dec 5, 2023
d689142
Add punctuation remoced due to main merge
p-offtermatt Dec 6, 2023
e730ebf
Remove outdated doc line
p-offtermatt Dec 6, 2023
d103bda
Add Quint tests to CI
p-offtermatt Dec 8, 2023
5d97774
Update tests/mbt/model/ccv_model.qnt
p-offtermatt Dec 8, 2023
5fecff1
Address comments
p-offtermatt Dec 8, 2023
90acddc
Add zero check to VotingPowerChangeToEmptyTest
p-offtermatt Dec 8, 2023
1798924
Incorporate Karolos' comments
p-offtermatt Dec 8, 2023
30a79ad
Add spacing between jobs
p-offtermatt Dec 11, 2023
2396038
Update tests/mbt/model/ccv_model.qnt
p-offtermatt Dec 11, 2023
1659892
Address comments
p-offtermatt Dec 11, 2023
21813de
Remove 4 week time advancement
p-offtermatt Dec 11, 2023
a3df827
Upload traces even when test fails
p-offtermatt Dec 11, 2023
e52d186
Fix condition for trace archival
p-offtermatt Dec 11, 2023
b74a09f
Remove unused index
p-offtermatt Dec 11, 2023
e039ef9
Remove outdated for loop
p-offtermatt Dec 11, 2023
b13ead1
Fix if condition for trace upload
p-offtermatt Dec 11, 2023
e7807bf
Add comment about timestamps
p-offtermatt Dec 11, 2023
a052b21
Remove long time advancements
p-offtermatt Dec 11, 2023
60589a1
Address comments
p-offtermatt Dec 11, 2023
82ca137
Make comment clearer
p-offtermatt Dec 11, 2023
6d68920
Update tests/mbt/driver/generate_traces.sh
p-offtermatt Dec 15, 2023
49ba056
Update tests/mbt/run_invariants.sh
p-offtermatt Dec 15, 2023
d04e140
Update tests/mbt/driver/README.md
p-offtermatt Dec 15, 2023
f5f5d6e
Merge branch 'main' into ph/mbt
p-offtermatt Dec 15, 2023
4af62df
Merge branch 'main' into ph/mbt
p-offtermatt Dec 15, 2023
d01e561
Update testutil/simibc/relayed_path.go
p-offtermatt Dec 15, 2023
2a1db2b
Update tests/mbt/driver/generate_more_traces.sh
p-offtermatt Dec 15, 2023
2488377
Remove difftest folder
p-offtermatt Dec 15, 2023
357541f
Merge branch 'ph/mbt' of https://github.com/cosmos/interchain-securit…
p-offtermatt Dec 15, 2023
73ba96f
Minor fixes based on PR comments
p-offtermatt Dec 15, 2023
44e6145
Make timedout status a const
p-offtermatt Dec 18, 2023
7940d0f
Lengthen retention to 6 days
p-offtermatt Dec 18, 2023
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
52 changes: 43 additions & 9 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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:
Expand All @@ -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: 2

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]
Expand All @@ -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 }}
Expand Down Expand Up @@ -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
39 changes: 31 additions & 8 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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:
Expand Down Expand Up @@ -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 ###
###############################################################################
Expand Down
12 changes: 6 additions & 6 deletions TESTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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.
3 changes: 2 additions & 1 deletion app/consumer-democracy/proposals_whitelisting_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,8 @@ import (
)

func TestDemocracyGovernanceWhitelistingKeys(t *testing.T) {
_, valUpdates, _ := testutil.CreateValidators(t, 4)
_, valUpdates, _, err := testutil.CreateValidators(4)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I changed the signature of the CreateValidators function to better suit my needs, so I had to adjust this here

require.NoError(t, err)
ibctesting.DefaultTestingAppInit = icstestingutils.DemocracyConsumerAppIniter(valUpdates)
chain := ibctesting.NewTestChain(t, ibctesting.NewCoordinator(t, 0), "test")
paramKeeper := chain.App.(*appConsumer.App).ParamsKeeper
Expand Down
1 change: 1 addition & 0 deletions go.mod
Original file line number Diff line number Diff line change
Expand Up @@ -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
)
Expand Down
2 changes: 2 additions & 0 deletions go.sum
Original file line number Diff line number Diff line change
Expand Up @@ -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=
Expand Down
128 changes: 0 additions & 128 deletions tests/difference/core/docs/METHOD.md

This file was deleted.

Loading
Loading