Vero Plan

VCG Plan: Emit plan.json

Write a detailed translation plan as JSON, pinning every Lean signature the TRANSLATE stage will emit. The plan is reviewed by a human before translate executes.

This stage does NOT write any Lean code. It writes .vero/plan.json (authoritative machine-readable contract) and .vero/plan/questions.md (human-facing questions, if any).

Canonical example: reference/BankLedger/manifest.json + reference/BankLedger/ — the manifest is what translate produces; this stage produces the richer plan.json that translate consumes to produce it.

When to use

• After .vero/select.json is approved by the human.
• Before the TRANSLATE stage runs.

Inputs

Output: .vero/plan.json

Full schema: docs/pipeline-schema.md (plan.json section). Minimum required structure:

{
  "version": 1,
  "api_namespace": "Bank",
  "packages": [
    {
      "name": "BankLedger",
      "is_root": true,
      "bundle_type": "BankLedgerBundle",
      "repo_impl_field": "bankLedger",
      "modules": [
        {
          "name": "Account",
          "upstream_files": ["src/account.rs"],
          "types": [
            {
              "name": "AccountId",
              "lean_form": "abbrev AccountId := Nat",
              "is_foundation": true
            }
          ],
          "apis": [
            {
              "upstream_name": "create_account",
              "lean_name": "createAccount",
              "sig_abbrev": "CreateAccountSig",
              "lean_type": "AccountId → Ledger → Ledger",
              "opaque": false,
              "nl_description": "Add a new account with the given id to the ledger."
            }
          ],
          "spec_helpers": [
            {
              "name": "toSeq",
              "lean_name": "toSeq",
              "lean_form": "def toSeq : Ledger → List (AccountId × Balance)\n  | []            => []\n  | a :: rest     => (a.id, a.balance) :: toSeq rest",
              "nl_description": "Flatten a ledger to a list of (id, balance) pairs; used by specs to state list-level properties."
            }
          ],
          "specs": [
            {
              "name": "spec_create_zero_balance",
              "nl_description": "Creating a new account gives it zero balance.",
              "lean_form": "∀ (id : AccountId) (ledger : Ledger), impl.bankLedger.accountExists id ledger = false → impl.bankLedger.getBalance id (impl.bankLedger.createAccount id ledger) = some 0",
              "apis_referenced": ["createAccount", "accountExists", "getBalance"],
              "spec_helpers_referenced": [],
              "curator_intended_truth": "prove"
            }
          ]
        }
      ]
    }
  ],
  "test_cases": [
    {
      "name": "guard_create_zero_balance",
      "nl_description": "After creating an account it has balance 0.",
      "lean_form": "#guard getBalance 1 (createAccount 1 []) == some 0"
    }
  ]
}

Category mapping from select.json:

Field-by-field guidance

Top-level:

• version: always 1 for now.
• api_namespace: one Lean namespace for the public API (e.g. "Bank" for BankLedger). Soft convention; may be null for multi-namespace projects.
• packages: exactly one entry has is_root: true — its name must match config.project_name. Multi-package projects add non-root entries.

Per-package:

• name: e.g. "BankLedger". Becomes the package directory name.
• bundle_type: PascalCase, typically "<Name>Bundle".
• repo_impl_field: lowerCamelCase of name, the field inside structure RepoImpl.

Per-module:

• name: PascalCase module name ("Account", "Transaction").
• upstream_files: list of source files this module consolidates.

types[]:

• name: Lean type name.
• lean_form: full Lean declaration text (the curator inspects this verbatim). "abbrev X := …", "structure X where …", or "inductive X where …".
• is_foundation: true if this type must live in the foundation Impl file (the one every other Impl imports).
• source_id, source_file, source_line, upstream_name, and source_signature: provenance for the exact upstream declaration.

apis[]:

• upstream_name: source-side name (create_account in Rust).
• lean_name: Lean-side name after casing (createAccount).
• sig_abbrev: PascalCase abbrev, conventionally <LeanName>Sig with first letter uppercased (CreateAccountSig).
• lean_type: the type body — exactly what goes after := in abbrev <sig_abbrev> := <type>. Use Unicode arrows (→), not ASCII.
• opaque: true for FFI / external functions — translate emits opaque + axioms instead of a translated reference implementation slot.
• nl_description: one-sentence English summary. Used later by vero-validate for spec-intent alignment.
• source_id, source_file, source_line, and source_signature: provenance for the exact upstream declaration.

specs[]:

• name: must start with spec_.
• nl_description: one-sentence English summary of what the spec asserts.
• lean_form: the body of def spec_<…> (impl : RepoImpl) : Prop := …. Access APIs via impl.<repo_impl_field>.<lean_name> — never bare impl.<lean_name> (RepoImpl is one-level-nested).
• apis_referenced: list of lean_names the spec touches. Helps the validator's spec_completeness check.
• curator_intended_truth: "prove" | "disprove" | "unsat" | "sat" | "unknown". Curator's ground-truth label for coverage scoring; may be "unknown" if undecided.
• source_id, source_file, source_line, source_theorem, and source_signature: provenance for the exact upstream theorem/lemma.

Source-provenance rule (hard requirement). Every translated plan item in types[], apis[], api_helpers[], spec_helpers[], specs[], and ref_impls[] must be backed by a real upstream source item. Prefer the exact source_id from .vero/source_index.json; also carry source_file, source_line, and the source signature when available. Do not create generated source ids, blank source files, sentinel predicates, token wrappers, placeholder helpers, or review marker definitions to preserve an item whose Lean translation is not known. If a selected item cannot be faithfully translated now, do not emit it as a translated/scored item; move it to review-only/untranslated metadata with a reason.

Disposition vocabulary (hard requirement). Use only unclassified, provided, scored, hidden, dropped, axiomatized, or opaque. Use provided for fixed source-backed vocabulary that is translated and supplied to the benchmark, such as types and spec helpers. Do not write given; it is a deprecated synonym and will be normalized or rejected by validation.

requires_human_review and equivalence_status: "unclear" are not allowed inside translated/scored item lists. They mean the item is not ready to translate. Keep such items out of types[], apis[], api_helpers[], spec_helpers[], and specs[] until a faithful Lean form is available.

Reference implementations (no separate field). The reference implementation of each non-opaque API is written directly inside the code marker in Impl/<Module>.lean by the TRANSLATE stage — not in a separate Bank.Ref namespace, not in a ref_impls[] plan field. Pre-agent-gen replaces marker content with sorry before the LLM sees the benchmark. This keeps one source of truth and lets #guard tests hit real code at curation / build time.

test_cases[]: #guard assertions against Bank.* directly. Each with an English description and the Lean form. Prefer boundary cases (empty inputs, duplicates, partial-function failure paths).

Output: .vero/plan/questions.md (optional)

If any decision is genuinely ambiguous (the source doesn't commit to a shape), write a bulleted list of questions for the human:

## Questions

- `pop` — source uses `requires s.nonEmpty`. Map to `Option (Stack α)` or
  `(s : Stack α) → s.size > 0 → Stack α`? Recommendation: `Option`
  (simpler, works with `#guard`).

The human answers inline by editing the file; re-run vero-plan on resume to pick up the answers.