informalsystems / informalsystems/FuzzMo

[adapter generation] Align in-context examples & generation targets between model and adapter generation

Open
#10 0 comments 0 reactions 0 assignees View on GitHub
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

Open the contributing 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.