informalsystems / informalsystems/FuzzMo

[adapter generation] Adapter generation is not robust in terms of project file structure

Open
#11 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

Adapter generation and repair depend on a specific Cargo workspace setup and file structure that was inherited from the CTF (Capture The Flag) contracts we use as in-context examples.

This issue is closely related to [ [adapter generation] Align in-context examples & generation targets between model and adapter generation #10 ](https://github.com/informalsystems/FuzzMo/issues/10).

## The problem

This makes adapter generation and repair non-robust in the sense that generating and repairing an adapter for a new contract requires the user to modify the `src/lib.rs` file of the contract (to include the generated adapter module), and modifying other contracts' `lib.rs` files (to exclude their generated adapters, in case they contain errors).
This is the case because Cargo will attempt to compile and run all tests in [the directory where example contracts for adapter generation are kept](https://github.com/informalsystems/FuzzMo/tree/main/data/adapter_generation/CTF), resulting in a broken repair process unless the user intervenes in the described way (by modifying `lib.rs` files so that only the desired adapter is considered).

## Proposed solution no. 1

Isolate the contract and the generated adapter into a separate Cargo workspace (use `work_dir`).

## Proposed solution no. 2

Call Cargo in a smarter way.
Maybe there is a way to provide a regex/pattern to ignore other contracts and their errors.

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.