informalsystems / cosmwasm-to-quint

Semi-automated modelling and Model-Based Testing for CosmWasm contracts
Apache License 2.0
14 stars 1 forks source link

Add snapshot tests for CTF contracts #12

Closed bugarela closed 6 months ago

bugarela commented 6 months ago

Hello :octocat:

PS: big diff because of snapshots - no need to review those at this time, as this is just a snapshot of the current results of the tool.

Closes #6

I was really feeling a need for regression tests on this, so I can make changes without ruining what is already working. So this adds a testing setup that I think will be perfect for the current situation:

  1. By using the rustc_utils crate, and copying the run definition from https://github.com/cognitive-engineering-lab/rustc_plugin/blob/main/crates/rustc_plugin/tests/test_example.rs, I'm able to run the cargo cosmwasm-to-quint cli command for a folder from the rust integration test
  2. By using the insta crate, I can automatically create and review snapshots for the expected result, so it's super easy to check what changed in the behavior after updating the translator itself. Those snaphots will make the PR diffs larger, but I think they will be helpful to the understanding of the PR changes.

I wanted to add the cosmwasm-ctf repository as a submodule to avoid polluting this repo, but I actually need one change to the original CTF contracts: updating the Cargo.lock file for each contract to be compatible with the nightly version of rustc, which is required by this project. So I made a fork (on my personal account, so it doesn't draw unnecessary attention for being listed under informal's organization, and also doesn't use a repository slot from the enterprise account) with that change, and I'm using that fork as a submodule here.

I'll add a CI action in a followup