informalsystems / informalsystems/FuzzMo
[adapter generation] Adapter generation is not robust in terms of project file structure
- 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
Assessment
This issue has not been assessed yet.