Vero Source Lean

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)

Extracting specs from theorems

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

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:

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>; #guards from source #guard/example).