Vero Translate

VCG Translate: Verified Code → Lean 4 Benchmark

Translate the selected items from the upstream source into a compilable Lean 4 project that matches the ratified paradigm documented in reference/BankLedger/. This is curation stage output: produce Impl/, Spec/, Harness.lean, Bundle.lean, Test.lean, root hub, lakefile.toml, lean-toolchain, and manifest.json. Do NOT emit Proof/ — that layer is materialized downstream at pre-agent-gen.

Canonical example: reference/BankLedger/. When uncertain about marker placement, Bundle shape, manifest field names, or docstring style, read those files directly — they are the living contract.

When to use

• After plan stage has produced .vero/plan.json and humans have approved it.
• Pair with the appropriate vero-source-{lang} skill for per-language translation patterns.

Prerequisites

• .vero/plan.json exists with the approved translation plan (schema: docs/pipeline-schema.md).
• Source files accessible.
• Language skill loaded.

Output shape (must match reference/BankLedger/)

<Project>/                         # Lean project root
├── lakefile.toml                  # see "Lakefile" below
├── lean-toolchain                 # leanprover/lean4:v4.29.1
├── manifest.json                  # see docs/pipeline-schema.md
├── <Project>.lean                 # root hub — imports only
└── <Project>/                     # root package dir
    ├── Impl/<Module>.lean         # types, sig abbrevs, reference impls (with markers)
    ├── Spec/<Module>.lean         # frozen specs plus RepoImpl-dependent spec helpers
    ├── Bundle.lean                # structure <Project>Bundle — one field per API
    ├── Harness.lean               # structure RepoImpl + canonical + joint_unsat macro
    └── Test.lean                  # #guard conformance tests against Bank.* directly

Multi-package benchmarks add sibling <OtherPackage>/ dirs, each with their own Impl/, Spec/, Bundle.lean. Harness.lean stays as a benchmark-level singleton.

The !benchmark marker system

Every LLM-editable slot is wrapped in a -- !benchmark @start <key> … / -- !benchmark @end <key> … pair. The @end must repeat the same key and def=<name>.

Active key set (7)

Retired (do not emit): spec, spec_aux, claim_aux, def_aux, def_body, precond*, postcond*.

!solution prefix (new third prefix — only in Proof/Joint.lean)

Multi-line block that lets the LLM submit structured data (the joint-unsat spec list). Translate does not emit Proof/Joint.lean; the pre-agent-gen stage does. Knowledge for reference only.

!curation prefix

Single-line curator-only annotations. Stripped before the benchmark is presented to the LLM. Only in Impl/* after curation. Forms:

-- !curation @review v<N> [<x| >] <name> — <loc>, <kind>, <notes>
-- !curation @human: <note>
-- !curation @question <target>: <q>
-- !curation @answer: <a>
-- !curation @v<N> [...] <name> — <notes> [RESOLVED|NOTED|ANSWERED|KEPT]

Marker positioning rules (hard)

• imports — immediately after the actual import statements, BEFORE the module docstring. At file top if no imports.
• global_aux — after the module docstring, before the body.
• code_aux — file-level, immediately before its code slot.
• proof_aux — file-level, BEFORE the theorem or macro invocation. Never between by and the proof body.
• claim — in Joint.lean only; wraps the LLM's live macro invocation (its content is discarded at eval).

def=<name> conventions

• code / code_aux — the Lean function dot-tail (createAccount).
• proof / proof_aux — full theorem name (prove_<spec>, disprove_<spec>, unsat_<spec>, sat_<spec>).
• claim — joint_unsatisfiability (there is exactly one joint slot per benchmark).

Balance

Every @start has a matching @end with the same key and def=. No nesting. Commented markers (inside /- … -/ or -- -- !benchmark) are ignored by the extractor. def=<name> is unique within (file, key).

File templates — canonical shape

lakefile.toml

name = "{Project}"
version = "0.1.0"
defaultTargets = ["{Project}"]

[[lean_lib]]
name = "{Project}"
srcDir = "."
leanOptions = [{ name = "autoImplicit", value = false }]

The old [package] form is gone.

lean-toolchain

leanprover/lean4:v4.29.1

Override only if the upstream source forces a different version.

Root hub <Project>.lean

import {Project}.Impl.<Module1>
import {Project}.Impl.<Module2>
...
import {Project}.Bundle
import {Project}.Harness
import {Project}.Spec.<Module1>
import {Project}.Spec.<Module2>
...
import {Project}.Test

Do not import any Proof/ directory — that's a downstream artifact.

Impl/<Module>.lean template

import {Project}.Impl.<DepModule>

-- !benchmark @start imports
-- !benchmark @end imports

/-!
# {Project}.Impl.<Module>

<One-paragraph description.>

DO NOT MODIFY types or signatures — these are the fixed vocabulary.
Implement only the function bodies.
-/

-- !benchmark @start global_aux
-- !benchmark @end global_aux

-- ── Types (no markers — fixed vocabulary) ─────────────
...

namespace Bank

-- ── API signatures (no markers — fixed vocabulary) ────
abbrev CreateAccountSig := AccountId → Ledger → Ledger
...

end Bank

-- ── Reference implementations (LLM task slots) ──────────

-- !benchmark @start code_aux def=createAccount
-- !benchmark @end code_aux def=createAccount

-- !curation @review v1 [ ] createAccount — Impl/<Module>, code, reference impl
def Bank.createAccount : Bank.CreateAccountSig :=
-- !benchmark @start code def=createAccount
  fun id ledger =>
    if ledger.any (fun a => a.id == id) then ledger
    else ⟨id, 0⟩ :: ledger
-- !benchmark @end code def=createAccount

The body inside the code marker is the curator's reference implementation — real working code, not sorry. Pre-agent-gen replaces it with sorry when emitting the LLM-facing benchmark. See Non-Negotiables below.

Types live in the foundation Impl file (the one every other Impl imports — typically Impl/Account.lean for the root-most types). There is no central Sig.lean or Types.lean.

Spec/<Module>.lean template (frozen, no markers)

import {Project}.Harness

/-!
# {Project}.Spec.<Module>

Specifications for <subsystem>. Each `spec_*` is a property over an
arbitrary `impl : RepoImpl`. Spec helpers that mention `RepoImpl` also
live here, before the specs.

DO NOT MODIFY — this file is frozen curator-given content.
-/

/-- <natural-language description> -/
def spec_<name> (impl : RepoImpl) : Prop :=
  ∀ …, impl.<pkg>.<fn> … = …

Specs access API functions via impl.<pkg>.<fn> where <pkg> is the field name in RepoImpl (e.g. impl.bankLedger.createAccount). No markers at all — the Spec layer is entirely frozen.

Bundle.lean template

import {Project}.Impl.<Module1>
import {Project}.Impl.<Module2>
...

/-!
# {Project}.Bundle

Per-package implementation bundle for the `{Project}` root package.
Collects all API signatures into one structure.

DO NOT MODIFY — benchmark infrastructure.
-/

structure {Project}Bundle where
  createAccount : Bank.CreateAccountSig
  closeAccount  : Bank.CloseAccountSig
  ...

Bundle struct name is <Project>Bundle (PascalCase). One field per API sig, field name matches the API's Lean name (camelCase).

Harness.lean template

import {Project}.Bundle

/-!
# {Project}.Harness

Benchmark harness: `RepoImpl` structure (one field per package),
`canonical` instance wiring, and the `joint_unsat` macro.

DO NOT MODIFY — benchmark infrastructure.
-/

structure RepoImpl where
  {pkg} : {Project}Bundle

def canonical : RepoImpl where
  {pkg} := {
    createAccount := Bank.createAccount
    closeAccount  := Bank.closeAccount
    ...
  }

/-- `joint_unsat spec_A spec_B [spec_C …] by <proof>` generates the
    ∧-conjunction unsat theorem. Variadic; no sort / no dedup — anti-cheat
    is enforced at `!solution` extraction during evaluation. -/
syntax "joint_unsat" ident ident ident* "by" tacticSeq : command

open Lean in
macro_rules
  | `(joint_unsat $s1 $s2 $[$rest]* by $proof) => do
    let specs := #[s1, s2] ++ rest
    let name := specs.foldl (init := `joint_unsat) fun acc s => Name.append acc s.getId
    let mut body ← `($(specs[0]!) impl)
    for s in specs[1:] do
      body ← `($body ∧ $s impl)
    `(theorem $(mkIdent name) : ¬ ∃ impl : RepoImpl, $body := by $proof)

For single-package benchmarks (typical), RepoImpl has exactly one field named lowerCamelCase(<Project>). For multi-package benchmarks it has one field per package.

No other macros. The retired solo_unsat / sat_witness macros are gone; per-module proof obligations materialize as plain theorem statements downstream.

Test.lean template

import {Project}.Impl.<Module1>
...

/-!
# {Project}.Test

`#guard` conformance tests. Guards run against `Bank.*` directly —
the curator's reference implementations live INSIDE the `code` markers
in `Impl/*.lean`. Before the LLM sees the benchmark, pre-agent-gen
replaces marker content with `sorry`; these guards catch regressions
in the reference impls themselves, not in LLM submissions.

DO NOT MODIFY — infrastructure.
-/

open Bank

#guard accountExists 1 [] == false
#guard getBalance 1 (createAccount 1 []) == some 0
#guard (transfer 1 2 30 [⟨1, 100⟩, ⟨2, 50⟩]).map totalAssets == some 150
...

No markers in Test.lean. No Bank.Ref namespace — that's been retired (2026-04-20). The reference implementation is whatever the curator wrote inside each code marker.

manifest.json (derived from the tree)

At the end of translate, emit / update the manifest per the shape in reference/BankLedger/manifest.json (full schema: docs/pipeline-schema.md). Top-level:

{
  "benchmark_id": "...",
  "description": null,
  "lean_version": "4.29.1",
  "modes_supported": ["proof", "codeproof"],
  "source": { "kind": "translated", "language": "...", "repo_url": "...", "commit_hash": "...", "path": "..." },
  "curation": { "date": "..." },
  "root_package": "{Project}",
  "files": {
    "root_hub": "{Project}.lean",
    "harness": "{Project}/Harness.lean",
    "test":    "{Project}/Test.lean",
    "lakefile": "lakefile.toml"
  },
  "packages": [
    {
      "name": "{Project}",
      "bundle": "{Project}/Bundle.lean",
      "bundle_type": "{Project}Bundle",
      "repo_impl_field": "{lowerCamelCase}",
      "modules": [
        {
          "name": "<Module>",
          "impl": "{Project}/Impl/<Module>.lean",
          "spec": "{Project}/Spec/<Module>.lean",
          "apis": [
            { "name": "createAccount", "sig": "CreateAccountSig", "type": "AccountId → Ledger → Ledger" }
          ],
          "specs": ["spec_create_zero_balance", "..."]
        }
      ]
    }
  ]
}

apis[].type is the body of the abbrev <Sig> := <type> in the Impl file (exact text, including spaces around →). specs[] are the spec names found in Spec/<Module>.lean.

Workflow (plan-driven, one file per Write, build per file)

plan.json is the contract. Translate walks plan.packages[].modules[] and emits exactly the files the plan names, one at a time. Do NOT improvise a module that isn't in the plan, and do NOT skip one that is. Do NOT write multiple Lean files before running lake build.

Non-negotiable write discipline.

• One Write per file. Never batch-emit several .lean files in a single turn.
• After each Write, run cd <project> && lake build and wait for it to succeed before moving to the next file.
• If a file is larger than ~150 lines of body (e.g. an Impl/ module with 8+ APIs), split its emission into: (a) Write skeleton with types + sig abbrevs + marker-wrapped API definitions, lake build, (b) Edit to fill each API's reference impl one at a time. This keeps the file buildable after every step.
• Announce each Write in one sentence: "Writing Impl/Merkle.lean — 3 types, 5 APIs, 12 code slots." Then perform the Write. Then announce the build outcome.

Phase 1 — Scaffolding (one Write each)

lakefile.toml, lean-toolchain, empty root hub, empty manifest.json. Build the empty scaffold. That's four Writes and one lake build.

Phase 2 — Impl modules (iterate plan.packages[].modules[])

For each module M in plan.json, in dependency order (foundation module first):

1. Look up the four per-module lists in plan.json:
   • M.types — fully-defined types, emit without markers
   • M.spec_helpers — curator-given vocabulary for specs; emit each as a fully-defined def / inductive / predicate using lean_form verbatim. No markers, not in Bundle. Helpers that mention RepoImpl or impl.<pkg> must live in Spec/<Module>.lean before the specs; pure helpers live in Impl/<Module>.lean.
   • M.api_helpers (optional, usually empty) — fully-defined helpers the curator wants to hand to the LLM. No markers, not in Bundle.
   • M.apis — sig abbrevs + reference implementation defs, each wrapped in !benchmark code / code_aux markers, field contributed to Bundle.
2. Write <Project>/Impl/<M.name>.lean in this order, top to bottom:

   imports
   `-- !benchmark @start imports`  … `-- !benchmark @end imports`
   docstring
   types (no markers)
   pure spec helpers (no markers)
   api helpers (no markers, if any)
   namespace Bank
     API sig abbrevs (no markers)
   end Bank
   `-- !benchmark @start global_aux` … `-- !benchmark @end global_aux`
   one `code_aux` + `code` marker pair per API (with reference impl
   body inside each `code` marker)

3. lake build. Fix errors before proceeding.
4. Announce: "Module <M.name> built. T types, H spec helpers, N API slots emitted. Moving on to <next>."

No module is emitted before its dependencies build clean.