search

informalsystems / cosmwasm-to-quint

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

Test generation #18

Closed bugarela closed 4 months ago

bugarela commented 4 months ago

Hello :octocat:

Closes #3 and closes #4

Sorry the PR is so big, but experimental mode kind of results in this. You might want to pick one snap (i.e. for ctf-02) file to review the behavior only. There are plenty of opportunities to improve the code itself, but I think this is good enough for the experiment.

This has some meaningful changes, besides the big MBT generation:

  1. Use allListsUpTo to generate nondet lists
  2. Rename return -> result because using return in rust MBT is an issue since it is a keyword.
  3. Write files with the generated code instead of printing to STDOUT. This also means that we'll have one Quint file + one MBT file per rust crate
  4. Add quint-lib-files as a compilation asset and write it in the target folder when running - so users won't have to do that manually

I'll rewrite the README next, this has to be ready by Monday. I'll merge it by Monday and make the repo public, so please try to add any input before that. Sorry for the short notice!

ivan-gavran commented 4 months ago

This is a shallow review, checking for functionality only. Checking on CTF-01 Model

Test file There is a number of syntax error that I am not able to interpret correctly. They are mostly about "missing comma", "missing {", but my guess is the root cause may be connected with the fact that pub struct Message is empty. (not sure though)

ivan-gavran commented 4 months ago

One more "presentation" comment: now that the model is not output to the std, the only output is about problems (not found this, not available that). I would suggest adding some text saying "Successfully generated the model in quint and the test in tests"

ivan-gavran commented 4 months ago
  • there are multiple type definitions for Lockup, InstantiateMsg, ContractState, Response and State (some of them in the model file, some of them in the lib and the model file)

It seems that the same problem existed in (newer) version of the main branch. (I guess I worked with some older version where it did not occur.)

bugarela commented 4 months ago

For register: I talked to Ivan and we found that the problems he had were only because of leftovers from previous versions on his local cosmwasm folder. Everything was fixed by a small cleanup and the errors shouldn't happen on a normal contract.