Test generation

[bugarela]

Hello

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]

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

• 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)
• type definition for BigInt is missing
• type definition for HashMap is missing

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]

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]

• 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]

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.