---
name: vero-source-lean
description: Load BEFORE curating an existing Lean 4 source repo into the benchmark format. Lean→Lean is mostly extraction, not translation — the source defs become the canonical Impl, the source theorems become the spec obligations. Pair with vero-discover, vero-plan, vero-translate, vero-spec-write, and vero-lean-pitfalls.
---

# VCG Source — Lean

Lean source is the special case: the upstream is already in the target language. The curation work is *not* translation but **extraction + reshaping** to fit the ratified benchmark paradigm.

**Reference the canonical shape** at `reference/BankLedger/`. The end product looks identical to a benchmark curated from Dafny / Verus / Coq — the difference is the path to get there.

## What you're doing

Given a Lean 4 source repo (no `lakefile.toml` at the curation-output path, just `.lean` files), produce a benchmark Lean project with:

1. **APIs** (`Impl/<Module>.lean`): the source's executable defs become `def <Project>.<name> : <Sig> := <body>` wrapped in `!benchmark code def=<name>` markers. The body is the *real* Lean source body — pre-agent-gen will replace it with `sorry` before the LLM sees the benchmark.
2. **Specs** (`Spec/<Module>.lean`): the source's theorems / lemmas become `def spec_<name> (impl : RepoImpl) : Prop := <statement>` definitions. The theorems themselves are dropped — proofs live in `Proof/` (materialized later for gen).
3. **Bundle / Harness / Test**: standard, mirrors BankLedger.

Because Lean→Lean is extraction, every selected theorem/spec must keep
source traceability. Emit or preserve a source map that records the
source declaration, target Lean spec/API, and whether the item was
extracted, compressed, trusted/opaque, or intentionally skipped. Do not
assume one source file maps to exactly one benchmark file.

## Classification (vero-discover)

| Source construct | Output classification |
|---|---|
| `def f : T := body` (top-level executable) | API (`kind=api`) — body becomes `code` marker interior |
| `def _f` / `private def f` / nested `def` inside a non-API | API helper (`kind=api_helper`) |
| `theorem t : P x := proof` | Spec candidate — `P x` is the spec body |
| `lemma t : P x := proof` | Spec candidate (same as theorem) |
| `def P : T → Prop := …` (predicate) | Spec helper (`spec_helpers[]`) — used in spec bodies |
| `structure Foo where ...` | Type — preserved verbatim |
| `inductive Foo := ...` | Type |
| `abbrev FooSig := T → U` | Sig abbrev — passed through as-is |
| `instance : Hashable Foo := …` | Type-class instance — preserved in `global_aux` if unrelated to spec bodies |
| `axiom A : P` | Trusted axiom — added to `manifest.json::trusted_axioms` |
| `opaque f : T → U` | Opaque — preserved in `global_aux` |
| `import …` | Import — preserved at file head |
| `#guard …` / `example …` | Test → `Test.lean` |
| `#eval …` (debug) | Skip; flag with `@review human` |

## Extracting specs from theorems

The single hard part. A typical Lean theorem looks like:

```lean
theorem ledger_create_zero (ledger : Ledger) (id : AccountId) :
    ¬ accountExists id ledger →
    getBalance id (createAccount id ledger) = some 0 := by
  intro h
  …
```

The benchmark spec is the proposition shape, not the proof. Strip the proof (`:= by …`) and reshape into a `RepoImpl` parameter:

```lean
def spec_ledger_create_zero (impl : RepoImpl) : Prop :=
  ∀ (ledger : Ledger) (id : AccountId),
    ¬ impl.bankLedger.accountExists id ledger →
    impl.bankLedger.getBalance id (impl.bankLedger.createAccount id ledger) = some 0
```

Rules:

1. **Every API reference goes through `impl.<repo_impl_field>.<fn>`.** The source uses bare names (`createAccount`); the spec uses bundle-qualified names (`impl.bankLedger.createAccount`).
2. **Theorem `:` becomes `Prop`** (it already was).
3. **Bound parameters become `∀`-quantified** at the spec level (the source theorem's parameters become explicit `∀` in the spec body).
4. **The proof is dropped.** It's regenerated by the LLM during gen.
5. **Spec helpers**: if the theorem statement uses a curator-given predicate (e.g., `def isWellFormed : Ledger → Prop`), preserve that predicate as a `spec_helper_*` in the same `Spec/<Module>.lean` file. Reference it from the spec body.

## Naming

- Theorems prefixed `<module>_<intent>` map to specs `spec_<module>_<intent>`.
- Theorems with verb-style names (e.g., `createAccountZeroBalance`) map to snake_case (`spec_create_account_zero_balance`).
- When the source uses Mathlib-style naming (`createAccount_zero_balance`), preserve and just prefix `spec_`.

## Extraction workflow (translate stage)

For each module:

1. Read `<source>/<Module>.lean`.
2. Identify executable defs (potential APIs) and theorems (potential spec sources).
3. Group APIs into `<Project>/Impl/<Module>.lean`:
   - copy imports + structures + helpers verbatim into `global_aux` and outside-marker context
   - emit `abbrev <Name>Sig := <type>` for each API
   - emit `def <Project>.<name> : <Project>.<Name>Sig := <original-body>` inside `code` marker pair
   - emit `code_aux` marker pair (empty, room for the LLM to add internal helpers)
4. For each chosen theorem (per `select.json`):
   - shape into `def spec_<name> (impl : RepoImpl) : Prop := <body>` in `<Project>/Spec/<Module>.lean`
   - swap bare API references → `impl.<repo_impl_field>.<fn>`
5. Update `manifest.json::packages[].modules[]`:
   - `apis[]` lists the executables; each entry `{ name, sig, type, kind: "api" }`
   - `specs[]` lists the spec names (bare strings)
   - `spec_helpers[]` lists predicate helpers if any
6. `Bundle.lean` + `Harness.lean` + `Test.lean` standard (one bundle field per API; canonical wires through to `<Project>.<api>`; `#guard`s from source `#guard`/`example`).

## No spec synthesis for Lean source

Lean→Lean curation is *honest extraction* of what the upstream source already proves — it must NOT synthesize new specs. The `lean_spec` workflow therefore deliberately omits the `spec_write` stage; the only specs in the curated benchmark are the ones the translate stage extracts from existing source `theorem` / `lemma` / `example` declarations.

If a curator wants additional specs, they should extend the upstream source repo with new theorems first (so the new specs are anchored in real, type-checked claims about the API), then re-run curation. Do not edit the curated benchmark to add specs that don't exist upstream.

Do not turn a source theorem into a benchmark obligation if the extracted
`spec_*` ignores `RepoImpl`, concludes `True`, or only proves a library
helper fact unrelated to the implementation. Classify those as
`spec_helper` / source context unless there is an explicit human
decision to keep a theorem-only obligation.

## Verify before declaring done

1. `lake build` succeeds.
2. Every `apis[]` entry has its `abbrev <Sig>` + `def <Project>.<name>` in the right Impl file.
3. Every `specs[]` entry exists as `def spec_<name> (impl : RepoImpl) : Prop := …` in the right Spec file.
4. `Spec/<Module>.lean` files have NO `theorem` / `lemma` / `example` declarations (the validator's `spec_shape` check enforces this).
5. The source repo's `axiom` declarations are listed in `manifest.json::trusted_axioms`.
6. Translated-source provenance is present in `.vero/source_map.json`,
   `.vero/discover.json`, or another validator-readable artifact.

## What NOT to do

- Don't preserve theorems in `Spec/`. They're not benchmark obligations; they're proofs that the *source* was correct.
- Don't translate Mathlib references unless the curator explicitly authorizes Mathlib in the target benchmark.
- Don't introduce new `instance` blocks for `DecidableEq` unless they're already in the source — the validator's anti-cheat instance check (gen/eval side) rejects suspicious additions.
- Don't conflate `def spec_helper_x` (executable predicate, used in specs) with `def spec_x` (proof obligation). They live in the same Spec file but their manifest classification differs.