informalsystems / informalsystems/FuzzMo
[adapter generation] Align in-context examples & generation targets between model and adapter generation
- Dominant language
- Rust
- Stars
- 0
- Forks
- 0
- PR merge metrics
- No merged PRs in 30d
Description
## Current state
The expected outline of Quint models differs between model and adapter generation.
Adapter generation is currently based on older Quint models for CTF contracts.
The major differences are in how Quint models are divided into modules and files.
For example, adapter generation expects all constants to be defined in a separate `constants.qnt` file, while model generation does not consider this file.
There are other such subtle differences that need to be addressed.
To see the concrete differences in model formats, look at the following two data directories.
1. Adapter generation: https://github.com/informalsystems/FuzzMo/tree/main/data/adapter_generation/CTF/quint
2. Model generation: https://github.com/informalsystems/FuzzMo/tree/main/data/model_generation/quint_examples
## The problem
Only CTF-01, CTF-02, and CTF-07 have been prepared for use as in-context examples and generation targets for adapter generation and repair.
In comparison, model generation also uses CTF-05 (and soon CTF-04, [PR](https://github.com/informalsystems/FuzzMo/pull/2)).
The reason for this is that we have two versions of Quint models for CTF-01, 02, and 07 (used for adapter generation and model generation), while a Quint model for CTF-05 was made only for model generation.
The difference in format is the most significant blocker for connecting model generation and adapter generation.
## Proposed solution
The examples (CosmWasm contracts, Quint models) must be unified between adapter and model generation, so the same set can be used in both cases. To this end, a unified format for in-context example contracts needs to be established. This is related to the UX and development towards a proper tool, as it will help applying the tool on real-world examples.
Model generation uses a newer "format" which more closely follows CosmWasm code and is produced in the mechanical phase of model generation. Therefore, adapter generation should be modified to use it too. Older models can then be archived and we can stop using them.
Contributor guide
Research direction
Compare the examples in data/adapter_generation/CTF/quint with data/model_generation/quint_examples, focusing on differences in module and file layout such as constants.qnt. Define a unified format based on the newer model-generation format, update adapter generation to use it, and archive the older models so both generation paths share the same examples and targets.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- rust
- Domain
- blockchain
- Issue type
- Refactor
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 30/100