Add ICS07 client upgrade to the MBT tests #1274
Conversation
- used cleaner LT, GT operators etc - still having the typeOK problem
(at least as correct as anything can work in this spec)
Fix compile errors
- Narrowed it down to the fact that chain states are being stored in a map keyed off the revision, but upgrading the chain changes the revision. This will need to be modified and checked to see if it makes sense.
string+revision to stop errors where a chain context cannot be found because the revision number has changed, making the old key invalid
|
More on the state space / test time thing. "rust-stable" CI tests on this PR took 13m 43s On my local, @adizere told me we try not to merge stuff that makes the tests take longer than 10m. I assume he was talking about the tests on Github CI. This PR exceeds that by about 3 minutes, so I will need to try to fix that. |
Yes, the GitHub CI. More context on this: our current CI takes on average 11 minutes; the longest task is the E2E tests and the next most time intensive task is the Rust tests, which can take 10min. This is not very often a bottleneck, but we would prefer to not increase the delay further -- and if it were a low-hanging fruit we would reduce that time. |
|
CI time for Rust / test-stable (pull_request) is down to 10m 47s- can this be merged? To get any lower, I think I would need to rewrite the TLA+ spec. |
jtremback
changed the title
|
IMHO, we could have a dedicated workflow in the future (for long-running and cross-chain tests) that is only triggered on release -> https://docs.github.com/en/actions/reference/workflow-syntax-for-github-actions#onevent_nametypes |
There was a problem hiding this comment.
Great stuff, @jtremback! Test suite running time looks good to me, although we don't have much margin yet wrt the E2E test suite running time, but we can address that in time.
* got rust compiling with new modelator, problems with the spec * everything works, but I had to delete an assert I don't understand * WIP using height tuple with fields for block height and revision * - corrected some small stuff around height comparisons - used cleaner LT, GT operators etc - still having the typeOK problem * correct tendermint height comparisons again * upgrade tla spec seems to work correctly (at least as correct as anything can work in this spec) * WIP starting on upgrade to rust code * fix TypeOk in spec * correct apalache type def * restore original typo * switch from tuple to record * Finally fixed confusing "No test trace found" error * Work towards synchronizing terminology between rust and tla Fix compile errors * WIP diagnosing upgrade test not passing - Narrowed it down to the fact that chain states are being stored in a map keyed off the revision, but upgrading the chain changes the revision. This will need to be modified and checked to see if it makes sense. * clean up rust todos and dbg's * correct tla bug where chain height instead of revision is updated * make chain revision in rust tests always 1 * key self.contexts hashmap off of chain id string instead of string+revision to stop errors where a chain context cannot be found because the revision number has changed, making the old key invalid * getting non-running tests to run * fix warnings * cut down state space * reduce state space further * bring back a few states * tweak the state filtering and add a changelog * Link .changelog entry to issue * Reorder imports and fix Clippy warning Co-authored-by: Romain Ruetschi <romain@informal.systems>
Closes #1311
Description
This PR adds capability to model a client upgrade to the TLA+ testing spec. It also makes some modifications to the rust MBT tests to run this capability as an MBT test.
Changes in the spec:
Heightwith a record containingRevisionHeightandRevisionNumber, as specified in ICS07.ICS07_UpgradeClientoperator which:Changes in the Rust:
Heightwithibc::Height.IbcTestRunner.contextshashmap with a chainID that does not include the revision number. This allows tests to keep working when the revision number changes.Caveats: The state space has become much bigger from the addition of multiple possible revision numbers. Some of the MBT tests now take minutes to run. We may not want to merge this PR until this is fixed. An easy fix that occurs to me is making Modelator cache TLA+ traces and invalidate this cache when the TLA+ file changes. I will also probably spend some time trying to restrict the state space of this model.
For contributor use:
unclog.docs/) and code comments.Files changedin the Github PR explorer.