Model based testing on integration tests #2072

rnbguy · 2022-04-06T13:19:38Z

Closes: #2070

Description

This PR contains the sources to enable Model Based Testing (MBT) in the integration test framework.

It extends two integration tests using MBT.

Successful token transfer
Unsuccessful token transfer (in case of IBC packet expiration)

Instructions

Next action items,

Create a CI for MBT tests.
Add/Refer instructions to setup apalache as dependency.
Describe the link between TLA+ specifications and Rust code.
Instructions on running apalache on the specifications manually.
Maintain example traces from apalache for manual inspection.

PR author checklist:

Added changelog entry, using unclog.
Added tests: integration (for Hermes) or unit/mock tests (for modules).
Linked to GitHub issue.
Updated code comments and documentation (e.g., docs/).

Reviewer checklist:

Reviewed Files changed in the GitHub PR explorer.
Manually tested (in case integration/unit/mock tests are absent).

adizere · 2022-05-05T15:42:36Z

After sync-ing with the team:

Rano: Estimate there may be another week of work necessary to get it ready for review. The failing tests are due to Apalache most likely, fixable.

it's important to note that the code here (modelator-side) will become obsolete once the more stable version of modelator comes out (v1).

the TLA+ specs still valuable

Adi: Sean Chen, maybe consider familiarizing yourself with the TLA+ specs. We don't expect these will need maintenance, but it's good to have a person who understands that front. This should not block merging, however.

Soares: The two important requiremets are: (1) save traces both on failure & succcess, and (2) get the CI tests to pass (related to Apalache error most likely).

worst case, in case we merge this and it will block us in the future, we can consider feature-flagging the MBT tests or disabling them (unless we actually uncover a bug in the relayer)

rnbguy · 2022-05-05T17:12:45Z

@adizere thanks for the summary ! 👍

I seem to fix the flaky tests. Ran some longer tests, but nothing came up. If everything looks alright, @soareschen and I can close the PR next week 🙂

…test/mbt

adizere · 2022-05-27T11:12:16Z

Wanted to follow-up here and see if the PR is blocked on anything.

The tests are not failing anymore, but a couple of them take too long (~20mins), specifically the integration test with gaia5 and gaia6. I restarted those jobs to see if they are successful.

soareschen · 2022-05-30T09:39:06Z

Sorry that I forgot to follow up on this PR. It can be merged now.

The tests are not failing anymore, but a couple of them take too long (~20mins)

We switched the parallel thread for the CI from 2 to 1, and apparently that makes the test run too slow. I have switched it back to run in 2 threads, and the time taken is now the same as master.

* Release v0.15.0 (informalsystems#2234) * Bump crates to v0.15.0 and ibc-proto to v0.18.0 * Include ibc-test-framework in release * Slightly improve main Cargo doc for ibc-test-framework * Fix components names * Update changelog * Update lockfile Co-authored-by: Soares Chen <soares.chen@maybevoid.com> * Add type ascription to fix build when `telemetry` feature is disabled (informalsystems#2235) * Bump once_cell from 1.11.0 to 1.12.0 (informalsystems#2237) * Add `ibc-test-framework` to the main README (informalsystems#2236) * Add `ibc-test-framework` to the main README * Cleanup * Fix `execute_schedule` method leaking operational data (informalsystems#2118) * Pull in upstream changes * Adding integration test for execute_schedule * Adding integration test for execute_schedule * Finish stubbing out execute_schedule test * Call `chains.shutdown` method * Correctly shut down chain * Shut down node b as well * Debugging execute_schedule test * Add Debug derivations * Update integration test so that its flow correctly tests `execute_schedule` * Attempt to perform a second IBC transfer * Remove info's * Increase sleep timeout duration * Incorportate new test framework features * Remove unnecessary `sleep` call * Correctly use new test framework features * Get assertions passing for now * Send two transactions, one in each direction * Add doc comment for test * Improve panic messages * Refactor test so that it is actually testing the desired behavior * Attempt at fixing `execute_schedule` leaky logic * Flesh out doc comments some more * Remove a duplicate function * Make use of OperationalDataTarget enum * Remove redundant enum * Remove some Debug derives * Remove one more debug derive * Add `try_fetch_scheduled_operational_data` back in * Give `do_execute_schedule` a more descriptive name * Improve `execute_schedule_for_target_chain` method's documentation * Add a bunch of clarifying comments * More clarification of comments * Flesh out `OperationalData` docs * Add changelog entry * Incorporate PR feedback Co-authored-by: Adi Seredinschi <adi@informal.systems> * Add `keys balance` command to query the balance for a key (informalsystems#2232) * Added subcommand 'balance' for command 'keys' to output the account balance associated with a given key * Added changelog entry for new command feature * Updated Hermes guide to include the new keys balance command * Improved error log for the CLI command and added doc comment * fixed fmt by running cargo fmt * Refactored query_balance to take key_name parameter. Added JSON output to keys balance command. * Fixed typo in comment in CosmosSdkChain query_balance method * Updated keys balance command to take the key_name as an optional flag Co-authored-by: Luca Joss <luca.joss@arcanite.ch> Co-authored-by: Romain Ruetschi <romain@informal.systems> * Model based testing on integration tests (informalsystems#2072) * ics20 token transfer spec * fixes for tla functions * full spec * update tla specs * mbt driver code * prepare for itf adoption * itf deserializer * description in comments * fix type * hack for apalache v0.20.2 (apalache-mc/apalache#1304) * updated tla spec * example itf.json * code refactor * prepare for mbt * fix and update * updated example * updated trace types * working mbt driver * fix mbt test * added mbt readme * BinaryChainTest over BinaryChannelTest * wait for established channel * added packet state assertions * improved mbt integration * few fixes * Refactor bootstrap chain and foreign client code * Introduce BootstrapChannel/ConnectionOptions * Increase timeout for assert_eventual_wallet_amount for CI * Upgrade Rust to 1.60.0 * Fix fmt in Rust 1.60.0 * Update Rust MSRV to 1.60 * Try running CI integration test single-threaded * Fix variable mixup * Add MBT to CI * Disable failing parse_itf test * Disable test_self_connected_ibc_transfer * Use gaia6 to run MBT test * Debug log on CI * save itf trace on failure * initialize nested maps * updated mbt code * Use new Nix URL * better fix to empty nested maps * Remove stale comments * Fix merge conflicts Co-authored-by: Soares Chen <soares.chen@maybevoid.com> Co-authored-by: Adi Seredinschi <adi@informal.systems> * Bump uuid from 1.0.0 to 1.1.0 (informalsystems#2247) Bumps [uuid](https://github.com/uuid-rs/uuid) from 1.0.0 to 1.1.0. - [Release notes](https://github.com/uuid-rs/uuid/releases) - [Commits](uuid-rs/uuid@1.0.0...1.1.0) --- updated-dependencies: - dependency-name: uuid dependency-type: direct:production update-type: version-update:semver-minor ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> * Add `query channel client` command to query a channel's client state (informalsystems#2248) * Added new CLI command 'query channel client' * Updated Hermes guide to include new query channel client command and updated changelog * Added missing subcommand in Hermes guide, section 7.9.3 Co-authored-by: Luca Joss <luca@informal.systems> * Fix wrong `create channel` command in "Create a new path" page in the guide (informalsystems#2245) Fix wrong `create channel` command in guide Co-authored-by: Adi Seredinschi <adi@informal.systems> * Disable MBT tests on CI due to flakiness (informalsystems#2253) * Complete ICS20 Implementation (informalsystems#1989) * Add ics26 Module trait * newtype for Acknowledgement * Define Router interface * Improve Router trait * Update mock router impl * Test for router API * Disallow duplicate module_ids in MockRouter * Add RouterBuilder for seal-style API * Fix failing test * Fix CI after merge * Chainable RouterBuilder::add_route() * Fix test * Add Router::has_route() trait method * Add comments * Separate mutating/non-mutating trait methods for shadow-paging style API * Make most Module trait methods optional * Default impl for MockModule::on_chan_open_try() * Acknowledgement trait * Extend router test * Simplify OnRechPacketResult using FnOnce() * Cleanup * Use Cow<str> for CapabilityName::new() * Use Cow<str> for CapabilityName::new() * Use newtype ModuleId instead of trait assoc type * Module callbacks' args as refs * Fix mock impl * WIP channel callbacks * Fix ModuleId ctor validation * TypedCapability * Use typed capabilities * Add Router::route_mut() * Implement pre-dispatch channel message validation * Avoid cloning message during channel msg dispatch * Add ChannelReader::lookup_module_by_channel() * Complete ics4 dispatch with callbacks * Fix compile errors from rebase * Fix CI test * Improve mock impl for capabilities * cargo fmt * Set channel version returned from on_chan_open_try() * Implement packet handler verification * Add missing check already received packets on ordered channels * Avoid cloning message during packet msg dispatch * Implement RecvPacket NoOp * cargo fmt and remove unused errors * Make on_recv_packet() Ack result optional * Don't return Result from on_recv_packet() and pass GenericAcknowledgement to on_acknowledgement_packet() * Implement packet callbacks * Allow callbacks to write logs and emit events * Fix test * Add .changelog entry * Add a comment for state rollback expectation from dispatch() * ics26_routing::handler::deliver() takes single message as input * ics26_routing::handler::deliver() returns logs as well * Remove ctx_ro * Callbacks return ModuleOutput<T> * Return HandlerOutputBuilder from channel and packet dispatch fn * Revert "Callbacks return ModuleOutput<T>" This reverts commit 1d430c9. * Address review feedback for comments * Extract ChannelMsg::lookup_module() * Add ICS20 Denom type * Add ICS20 TracePrefix & TracePath type * Define Coin and Decimal types * Impl conversions from/to RawDenomTrace * Make better use of derive-more * Impl conversions for Coin type * Add HashedDenom and polish DenomTrace impl * Define PacketData domain type and conversions * Use Coin domain type in MsgTransfer * Fix usage of Coin type in relayer code * Always panic on decimal arith overflow * Polish generic Signer impl * Implement ICS20 signer type * Coin type with generic Denom param * Use IbcCoin in MsgTransfer and PrefixedCoin in PacketData * Minor refactoring * Fix test_util * Impl AsRef<[u8]> for GenericAcknowledgement * Ics20Context is no longer a supertrait of Ics26Context * Add ICS20 Ack type * Add ICS20 event enum placeholder * Define all ICS20 expected keepers and context * Update send_transfer() for recent context changes * Give mut ref to set_channel_escrow_address() * Define ICS20 callback functions * Fix test build * Move denom derive functions to integration tests * Add version to chan_open_try callback * Rename ChannelId::counter() to sequence() * Add AppModule error variant to ChannelError * Implement validation helpers for callbacks * Define Ics20 callback errors * Implement channel handshake callbacks * Fix clippy errors * Impl Deserialize for PacketData * Manually implement AsRef<str> for Signer * Fix ICS20 Ack success from impl * Add more ICS20 errors * Improve ack type ctor * Add ctor for TracePrefix * Provide denom trace methods to remove prefix and check for empty trace path * Implement conversion from PrefixedCoin to IbcCoin * Add Ics20Reader trait methods to check send/receive enabled * Provided trait method get_channel_escrow_address() * Add BankReader trait for is_blocked_account() * Add FromStr bound for Ics20Context::AccountId * Use IbcCoins in Bank traits * Impl on_recv_packet() for cases where receiver chain is source * Fallible OnRecvPacket::write_fn() * Complete on_recv_packet impl * Fix test build * Fix clippy errors * Implement remaining packet callbacks for ICS20 * Make set_denom_trace() fallible * Don't derive AsRef * Complete send_transfer impl * Manual deserialize impl for Acknowledgement * Add ctor for Acknowledgement * Handle packet-data deserialize error separately * Use U256 for Denom and move bigint.rs to modules/src * Rename Denom to Amount * Cleanup * Fix trait definitions * Use source enum * Fix AccountReader trait * Validate port_id * More refactoring * Rename Signer to Address * Use Address instead of Signer where applicable * Fix send_transfer packet creation * Fix clippy warnings * Define ICS20 events * Extract relay code into separate files * Fix clippy warnings * Make HandlerOutput/Builder generic over events * Define ModuleEvent * Add AppModule variant to IbcEvent * Impl Display for Acknowledgement * Derive serde for ModuleId * Add ModuleId to ModuleEvent * Impl conversion from tuple for ModuleEventAttribute * Impl conversions from ICS20 events to ModuleEvent * Add event for transfer * Remove bech32 validation from Address * Change MsgTransfer receiver type to Address * Extract MockContext IbcStore * Improve conversion from Signer to AccountId * Add deliver method to Module trait * Implement conversions for MsgTransfer to/from Protobuf Any * Store packet result directly in send_transfer() * Make all ICS20 mods public * Make all IbsStore fields public to enable access for app modules * Implement Ics20Context for DummyTransferModule * Fix failing test * Manual Clone impl for MockContext * Fix failing test * Revert "Fix failing test" This reverts commit 40aec61. * Fix MockContext Clone impl * Update trait definitions after merge with master * Replace ModuleOutput with ModuleOutputBuilder in callbacks * Add inout param ModuleOutputBuilder to Ics20 callback handlers * Emit ICS20 receive packet events * Module::deliver() must be able to emit IbcEvents * Allow HandlerOutputBuilder to merge HandlerOutput * Emit transfer event * Add AckStatusEvent * Emit ICS20 ack events * Emit ICS20 timeout events * Remove ABCI error code * Remove #[allow(unused)] * Add log for send transfer * MsgReceipt abstraction * Handle missing IbcEvent to AbciEvent conversions for RecvPacket and TimeoutOnClose events * Implement ModuleEvent to AbciEvent conversion * Make send_transfer() public * Allow empty TracePaths * Fix TracePath multiple prefix parse bug * Fix TracePath empty str parse bug * Improve DenomTrace FromStr * Add denom validation test * Add denom trace and serde tests * TracePath tests * Allow Denom with '/' * Fix HashedDenom FromStr impl for empty hash * Minor refactoring * Add IbcCoin tests * Add .changelog entry * Fix clippy errors * Disallow empty Signer and replace Address with it * Use ToString as trait bound for ICS20 AccountId * Change AccountId trait bound from FromStr to TryFrom<Signer> * Remove Signer::new() * Delete OCap related TODO * Remove the PortKeeper * Remove Module::deliver() * Fix clippy warnings * Rename transfer module * Rename mod relay * Fix tests failing due to empty signer * Rename PORT_ID const to PORT_ID_STR * Fix escrow addr gen * Test cosmos escrow addr gen * Rename receiver account * Remove `has_denom_trace()` * Remove `BankReader::is_blocked_account()` * Remove `AccountId::ToString` bound * Remove `AccountReader` * Mint/burn into user accounts directly * Use `chunks_exact()` instead of `windows().step_by()` * Rename `DenomTrace::has_prefix()` to `trace_starts_with()` * Move trace related methods into `TracePath` * Fix add/remove prefix * Add test for add/remove trace prefix * Set denom trace only if not already set * Use truncate instead of drain in cosmos_adr028_escrow_address() * Rename DenomTrace as PrefixedDenom * Modify all `BankKeeper` methods to use `PrefixedCoin` instead of `IbcCoin` * Rename `Denom` as `BaseDenom` * Impl Into<U256> and checked_add/sub() for Amount * Add more TracePath tests * Test TracePath is_empty() * Remove IbcCoin * Remove HashedDenom and HashedCoin * Fix test compilation * Add comment for send_transfer() * Functions for determining source chain * Minor refactoring * cargo fmt * Derive serde for PacketCommitment and AcknowledgementCommitment * docstring and comment Co-authored-by: Philippe Laferriere <plafer@protonmail.com> * Merge commands `keys add` and `keys restore` into a single command. (informalsystems#2251) * Merged commands 'keys add' and 'keys restore' into a single command, 'keys add'. Improved restoring a key with mnemonic by taking a file containing the mnemonic as input instead of taking the mnemonic as command line input * Updated Hermes guide with new merged 'keys add' command. And updated changelog with improvement * Fixed e2e setup script to take correct flag when adding keys * Fixed small errors in Hermes guide and improved comments for changed 'keys add' command. * Improved Hermes guide section 7.2 * Updated the Hermes guide section 7.2 to match actual features * Bump moka from 0.8.4 to 0.8.5 (informalsystems#2246) Bumps [moka](https://github.com/moka-rs/moka) from 0.8.4 to 0.8.5. - [Release notes](https://github.com/moka-rs/moka/releases) - [Changelog](https://github.com/moka-rs/moka/blob/master/CHANGELOG.md) - [Commits](moka-rs/moka@v0.8.4...v0.8.5) --- updated-dependencies: - dependency-name: moka dependency-type: direct:production update-type: version-update:semver-patch ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: Adi Seredinschi <adi@informal.systems> * fmt * rename LightClientContext to ReaderContext * use host hash function in escrow address * minor fix * minor fix Co-authored-by: Romain Ruetschi <romain@informal.systems> Co-authored-by: Soares Chen <soares.chen@maybevoid.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: Sean Chen <seanchen11235@gmail.com> Co-authored-by: Adi Seredinschi <adi@informal.systems> Co-authored-by: Luca Joss <43531661+ljoss17@users.noreply.github.com> Co-authored-by: Luca Joss <luca.joss@arcanite.ch> Co-authored-by: Ranadeep Biswas <mail@rnbguy.at> Co-authored-by: Luca Joss <luca@informal.systems> Co-authored-by: Shoaib Ahmed <sufialhussaini@gmail.com> Co-authored-by: Philippe Laferriere <plafer@protonmail.com>

* ics20 token transfer spec * fixes for tla functions * full spec * update tla specs * mbt driver code * prepare for itf adoption * itf deserializer * description in comments * fix type * hack for apalache v0.20.2 (apalache-mc/apalache#1304) * updated tla spec * example itf.json * code refactor * prepare for mbt * fix and update * updated example * updated trace types * working mbt driver * fix mbt test * added mbt readme * BinaryChainTest over BinaryChannelTest * wait for established channel * added packet state assertions * improved mbt integration * few fixes * Refactor bootstrap chain and foreign client code * Introduce BootstrapChannel/ConnectionOptions * Increase timeout for assert_eventual_wallet_amount for CI * Upgrade Rust to 1.60.0 * Fix fmt in Rust 1.60.0 * Update Rust MSRV to 1.60 * Try running CI integration test single-threaded * Fix variable mixup * Add MBT to CI * Disable failing parse_itf test * Disable test_self_connected_ibc_transfer * Use gaia6 to run MBT test * Debug log on CI * save itf trace on failure * initialize nested maps * updated mbt code * Use new Nix URL * better fix to empty nested maps * Remove stale comments * Fix merge conflicts Co-authored-by: Soares Chen <soares.chen@maybevoid.com> Co-authored-by: Adi Seredinschi <adi@informal.systems>

rnbguy added 25 commits April 1, 2022 16:52

ics20 token transfer spec

1872a17

fixes for tla functions

8a61317

full spec

3fe2b2f

update tla specs

5ee9add

mbt driver code

fcb99f2

prepare for itf adoption

20f4f04

itf deserializer

b2722c9

description in comments

af21962

fix type

42d242b

hack for apalache v0.20.2 (apalache-mc/apalache#1304)

7cf28b7

updated tla spec

5cfbdb7

example itf.json

abad67a

code refactor

bc19019

prepare for mbt

6e3d282

fix and update

2f4c78c

updated example

bfee963

updated trace types

2c6b91f

working mbt driver

a3c1948

fix mbt test

73c3bfd

added mbt readme

de1feea

BinaryChainTest over BinaryChannelTest

22143bd

wait for established channel

05e0326

added packet state assertions

51c0dbd

improved mbt integration

37117a8

few fixes

aa2b3ef

rnbguy requested a review from soareschen April 6, 2022 13:19

rnbguy requested review from adizere, ancazamfir and romac as code owners April 6, 2022 13:19

romac marked this pull request as draft April 7, 2022 07:08

soareschen self-assigned this Apr 11, 2022

soareschen and others added 9 commits April 11, 2022 14:36

Merge branch 'master' into rnbguy/integration-test/mbt

be68b41

Fix variable mixup

1dc138c

Add MBT to CI

f57fc45

Disable failing parse_itf test

1d3fc7b

Disable test_self_connected_ibc_transfer

8357645

Use gaia6 to run MBT test

3d29281

Debug log on CI

937e1ed

Merge branch 'master' into rnbguy/integration-test/mbt

ca9c9e7

save itf trace on failure

ecd0e16

rnbguy added 2 commits May 5, 2022 18:19

initialize nested maps

b83070e

updated mbt code

14c5598

soareschen and others added 3 commits May 6, 2022 11:12

Merge remote-tracking branch 'origin/master' into rnbguy/integration-…

b0202dc

…test/mbt

Use new Nix URL

67368ab

better fix to empty nested maps

f4bf73b

soareschen added 3 commits May 30, 2022 11:01

Merge branch 'master' into rnbguy/integration-test/mbt

cd5f9c6

Remove stale comments

17c420a

Fix merge conflicts

fdc0cf6

soareschen marked this pull request as ready for review May 30, 2022 09:37

soareschen approved these changes May 30, 2022

View reviewed changes

Merge branch 'master' into rnbguy/integration-test/mbt

1c7fe94

adizere merged commit c6aaa49 into master May 30, 2022

adizere deleted the rnbguy/integration-test/mbt branch May 30, 2022 14:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Model based testing on integration tests #2072

Model based testing on integration tests #2072

rnbguy commented Apr 6, 2022 •

edited

Loading

adizere commented May 5, 2022

rnbguy commented May 5, 2022

adizere commented May 27, 2022

soareschen commented May 30, 2022

Model based testing on integration tests #2072

Model based testing on integration tests #2072

Conversation

rnbguy commented Apr 6, 2022 • edited Loading

Description

Instructions

PR author checklist:

Reviewer checklist:

adizere commented May 5, 2022

rnbguy commented May 5, 2022

adizere commented May 27, 2022

soareschen commented May 30, 2022

rnbguy commented Apr 6, 2022 •

edited

Loading