diff --git a/README.md b/README.md index 4591de8..4c9414b 100644 --- a/README.md +++ b/README.md @@ -1,36 +1,66 @@ -# scribe +
-``` +
                _ _
   ___  ___ _ __(_) |__   ___
  / __|/ __| '__| | '_ \ / _ \
  \__ \ (__| |  | | |_) |  __/
  |___/\___|_|  |_|_.__/ \___|
-```
+
-an llm proof-completion loop for zk gadgets, with the lean kernel as oracle. +### an LLM proof-completion loop for ZK circuit gadgets, with the Lean 4 kernel as the oracle -## what it does +[![CI](https://img.shields.io/github/actions/workflow/status/LucidSamuel/scribe/ci.yml?branch=main&label=CI&logo=github)](https://github.com/LucidSamuel/scribe/actions/workflows/ci.yml) +[![Docker](https://img.shields.io/github/actions/workflow/status/LucidSamuel/scribe/docker.yml?branch=main&label=Docker&logo=docker)](https://github.com/LucidSamuel/scribe/actions/workflows/docker.yml) +[![License: MIT](https://img.shields.io/badge/license-MIT-blue.svg)](./LICENSE-MIT) +[![Lean 4](https://img.shields.io/badge/Lean-4.30.0--rc2-1f425f.svg)](https://leanprover.github.io/) +[![Rust](https://img.shields.io/badge/Rust-stable-orange.svg?logo=rust)](https://www.rust-lang.org/) +[![proofs: kernel-checked](https://img.shields.io/badge/proofs-kernel--checked-success.svg)](#proven-gadgets) -1. **gadget-ir**: a minimal IR for polynomial constraints over a prime field. -2. **lean-emit**: reads the IR, emits a Lean 4 file with the theorem statement and `sorry`. -3. **proof-pilot**: drives an LLM backend in a loop: edit proof → compile the target Lean file → read errors → repeat. stops when the kernel accepts or budget is exhausted. -4. **halva-bridge**: combines Halva's halo2 extraction with a user specification and optionally sends the resulting theorem to proof-pilot. -5. **scribe-cli**: top-level `scribe` binary with `verify` and `demo` subcommands (see below). +[Getting Started](#getting-started) · +[Usage](#usage) · +[Proven Gadgets](#proven-gadgets) · +[Architecture](docs/architecture.md) · +[Why](docs/why.md) -the lean kernel is the oracle. proof-pilot builds the Lake project and then compiles the exact target file, including files outside the default Lake target. the llm cannot fake acceptance with `sorry` or `axiom`, which are blocked by proof-pilot, the pre-commit hook, and CI. +
-## quickstart +--- -### docker (fastest) +## Background -the published image bundles Rust binaries, the Lean toolchain, and pre-cached Mathlib oleans. +Zero-knowledge circuits are notoriously hard to get right: a single under-constrained gate is a soundness bug that no amount of testing reliably catches. **scribe** turns the soundness of a ZK gadget into a theorem and proves it using a large language model to *write* the proof and the **Lean 4 kernel** to *check* it. -``` +> [!IMPORTANT] +> The Lean kernel is the oracle, not the LLM. `proof-pilot` builds the Lake project and then compiles the exact target file. The model cannot fake acceptance with `sorry`, `axiom`, or `native_decide` — these are blocked in three independent places: `proof-pilot` itself, a pre-commit hook, and CI. + +Three properties make this trustworthy: + +- **Sound by construction.** Every proof in this repo is checked by the Lean 4 kernel. `#print axioms` on each theorem shows only the standard axioms: no `sorryAx`, no custom assumptions. +- **Automated.** An LLM drives a closed feedback loop, edit the proof, compile, read the errors (or structured LSP goal states), repeat until the kernel accepts or the budget runs out. +- **Real circuits.** The `halva-bridge` consumes actual Halva-style halo2 extraction output and proves soundness against a human-written specification. + +## How It Works + +scribe is a small Rust workspace. The pipeline runs IR → Lean scaffold → LLM proof loop → kernel-accepted `.lean`: + +1. **`gadget-ir`**: a minimal IR for polynomial constraints over a prime field (TOML → struct). +2. **`lean-emit`**: reads the IR and emits a Lean 4 file with the theorem statement and a `sorry`. +3. **`proof-pilot`**: drives an LLM backend in a loop: edit the proof → compile the target file → read the errors → repeat. Stops when the kernel accepts or the budget is exhausted. +4. **`halva-bridge`**: combines a Halva halo2 extraction with a user specification and (optionally) sends the resulting theorem to `proof-pilot`. +5. **`scribe-cli`**: the top-level `scribe` binary, with `verify`, `init`, and `demo` subcommands. + +## Getting Started + +### Docker (fastest) + +The published image bundles the Rust binaries, the Lean toolchain, and pre-cached Mathlib oleans, so there is no ~30-minute cold Mathlib build. + +```sh # five-minute demo: dry-run the range-check gadget proof (no API key needed) docker run --rm ghcr.io/lucidsamuel/scribe:latest scribe demo -# verify a Halva extractor project against a user spec (requires ANTHROPIC_API_KEY) +# verify a Halva extraction against a user spec (requires ANTHROPIC_API_KEY) docker run --rm \ -e ANTHROPIC_API_KEY="$ANTHROPIC_API_KEY" \ -v "$(pwd)":/workspace \ @@ -39,97 +69,37 @@ docker run --rm \ --halva-output /workspace/extracted.lean \ --spec-file /workspace/spec.lean \ --output /workspace/Proof.lean - -# build locally -docker build -t scribe:dev . ``` -see the [docker section](#docker) below for more. +See the [Docker](#docker) section for tags and local builds. -### rust +### From source -``` -cargo check --workspace -cargo test --workspace -``` - -### lean - -requires [elan](https://github.com/leanprover/elan) (lean version manager). +> [!NOTE] +> The Rust workspace builds with a stable toolchain. The Lean side requires [elan](https://github.com/leanprover/elan) (the Lean version manager); the pinned toolchain is `leanprover/lean4:v4.30.0-rc2`. -``` -# install elan (mac) -curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh +```sh +# Rust workspace +cargo check --workspace +cargo test --workspace +# Lean proofs +curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh # install elan (mac/linux) cd lean -lake exe cache get -lake build +lake exe cache get # fetch pre-built Mathlib oleans +lake build # should exit 0 with no warnings — every gadget proof is complete ``` -`lake build` should exit 0 with no warnings. all six gadget proofs are complete. - -### emit a scaffold +> [!TIP] +> Running `scribe`, `proof-pilot`, or `halva-bridge` against a live model needs a backend. The default backend shells out to the `claude` CLI; pass `--backend openai|anthropic|...` plus `--api-key` / `--model` to use a hosted API instead. Run any binary with `--help` for the full flag list. -``` -cargo run -p lean-emit -- examples/poseidon-sbox/gadget.toml -``` - -### proof loop +## Usage -``` -cargo run -p proof-pilot -- lean/ZkGadgets/AutoProof.lean \ - --lake-dir lean \ - --max-iters 10 \ - --transcript transcript.log -``` - -proof-pilot calls `claude -p` with the file + build errors, extracts the proof from the response, patches the file, and repeats until both the project build and exact target compilation pass clean or the budget is exhausted. - -additional proof-pilot flags (v2): - -- `--notes NOTES.md` — write a `NOTES.md` learning log after the session; each iteration records concrete tactics tried and cites worked examples from `lean/ZkGadgets/`. -- `--save-transcript session.json` — save a versioned JSON transcript recording the full iteration history, toolchain string, and Mathlib rev. -- `--replay session.json` — deterministically replay a saved transcript; refuses on toolchain mismatch unless `--allow-toolchain-mismatch` is passed. -- `--lsp` — use the Lean language server for structured diagnostics (goal states + hypotheses) instead of raw `lake build` text. - -by default it uses `prompts/lean-prover.md` as the system prompt; pass `--system-prompt ` to override it. - -see [transcripts/poseidon-sbox.md](transcripts/poseidon-sbox.md) for an example session closing the Poseidon S-box proof in 2 iterations. - -### bridge a Halva extraction - -``` -cargo run -p halva-bridge -- examples/halva-range-check/extracted.lean \ - --spec-file examples/halva-range-check/spec.lean \ - --output lean/ZkGadgets/HalvaRangeCheck.lean -``` - -Use `--prove` to launch proof-pilot after scaffolding. Structured specifications can use `--spec ` with repeatable `--extra-import ` flags. Run `halva-bridge --help` for the backend and proof-loop options. - -The same flow scales to harder circuits. `examples/halva-fibonacci/` and `examples/halva-binary-number/` are real Halva extractions (`cargo run --example fib` / `--example scroll-binary-number` from the Halva repo) bridged to proven soundness theorems — exercising copy constraints and multi-gate circuits respectively, neither of which the range-check example touches. - -## scribe verify - -`scribe verify` is the single-command path from a Halva extractor project to a kernel-checked proof. - -**scoping note:** `scribe verify --circuit` operates on a Halva *extractor project* — you still author the Halva extractor program that runs against your halo2 circuit. `scribe init --circuit` can generate that project skeleton, but scribe does not read raw halo2 Rust source directly. the command is: extractor-project-output → Lean scaffold → LLM proof loop → kernel-accepted `.lean` file. - -## scribe init - -`scribe init --circuit` creates the editable Halva extractor project that `scribe verify --circuit` expects. - -``` -scribe init \ - --circuit path/to/raw-halo2-circuit-crate \ - --output path/to/halva-extractor-project \ - [--name MyCircuit] \ - [--halva-git https://github.com//.git] \ - [--halva-rev REV] -``` +### `scribe verify` -The generated project contains `Cargo.toml`, `src/main.rs`, and a README. Fill in `src/main.rs` to instantiate your circuit, call Halva, and print the extracted Lean to stdout; then pass that generated project to `scribe verify --circuit`. If `--halva-git` is omitted, the generated `Cargo.toml` leaves the Halva dependency as an explicit TODO instead of guessing a repository URL. +The single-command path from a Halva extraction (or extractor project) to a kernel-checked proof. -``` +```sh # from a pre-extracted Halva .lean file + a user spec snippet scribe verify \ --halva-output extracted.lean \ @@ -143,134 +113,154 @@ scribe verify \ # from a Halva extractor project directory (runs the extractor, then verifies) scribe verify \ - --circuit path/to/halva-extractor-project \ + --circuit path/to/halva-extractor-project \ --spec-file spec.lean \ --output lean/ZkGadgets/MyCircuit.lean ``` -both forms run proof-pilot by default and exit 0 only when the Lean kernel accepts the proof. the output `.lean` file is the artifact; no `sorry` or `axiom` survive. pass `--no-prove` to only emit the scaffold (which still contains `sorry`) and skip the proof loop. +Both forms run `proof-pilot` by default and exit `0` only when the Lean kernel accepts the proof. The output `.lean` file is the artifact; no `sorry` or `axiom` survive. Pass `--no-prove` to emit only the scaffold (which still contains `sorry`) and skip the proof loop. -## scribe demo +> [!NOTE] +> **Scope.** `scribe verify --circuit` operates on a Halva *extractor project* — you still author the small extractor program that runs against your halo2 circuit. scribe does not read raw halo2 Rust source directly. The chain is: extractor-project output → Lean scaffold → LLM proof loop → kernel-accepted `.lean`. -`scribe demo` is the five-minute first-run experience for the range-check gadget (chosen because it is legible to non-hash ZK engineers). three tiers: +### `scribe init` -| flag | what it does | -|---|---| -| _(none)_ | dry-run: walks through the pipeline conceptually and shows the gadget description — no Lean toolchain or API key required | -| `--verify` | runs `lake build` on the pre-computed `lean/ZkGadgets/RangeCheck.lean` proof (needs Lean; **no** API key); this tier runs in CI | -| `--live` | runs the full LLM proof loop on a fresh scaffold (needs Lean **and** an API key / backend) | +Generates the editable Halva extractor project that `scribe verify --circuit` expects. +```sh +scribe init \ + --circuit path/to/raw-halo2-circuit-crate \ + --output path/to/halva-extractor-project \ + [--name MyCircuit] \ + [--halva-git https://github.com//.git] \ + [--halva-rev REV] ``` -# dry-run (no Lean or API key needed) -scribe demo -# kernel-check the pre-computed range-check proof (needs Lean, no API key) -scribe demo --verify +The generated project contains `Cargo.toml`, `src/main.rs`, and a README. Fill in `src/main.rs` to instantiate your circuit, call Halva, and print the extracted Lean to stdout — then pass that project to `scribe verify --circuit`. If `--halva-git` is omitted, the generated `Cargo.toml` leaves the Halva dependency as an explicit TODO rather than guessing a repository URL. + +### `scribe demo` + +The five-minute first-run experience, built around the range-check gadget (legible to non-hash ZK engineers). Three tiers: -# run the live LLM proof loop on a fresh scaffold (needs Lean + API key) -scribe demo --live --backend claude +| Tier | What it does | Requirements | +|---|---|---| +| `scribe demo` | Dry-run: walks through the pipeline and shows the gadget description | none | +| `scribe demo --verify` | Runs `lake build` on the pre-computed `RangeCheck.lean` proof | Lean (no API key) | +| `scribe demo --live` | Runs the full LLM proof loop on a fresh scaffold | Lean **and** an API key / backend | + +```sh +scribe demo # dry-run, no Lean or API key +scribe demo --verify # kernel-check the pre-computed proof +scribe demo --live --backend claude # full LLM proof loop on a fresh scaffold ``` -the dry-run output leads with a plain-English gadget description: -> *range-check gadget: proves that a field element x satisfies 0 ≤ x < 256 by decomposing x into 8 boolean bits and checking their weighted sum.* +### Running the loop directly -## docker +```sh +# emit a scaffold from an IR file +cargo run -p lean-emit -- examples/poseidon-sbox/gadget.toml -the `ghcr.io/lucidsamuel/scribe` image is built on every push to `main` and on version tags, via `.github/workflows/docker.yml`. it bundles: +# run the proof loop on a target file +cargo run -p proof-pilot -- lean/ZkGadgets/AutoProof.lean \ + --lake-dir lean \ + --max-iters 10 \ + --transcript transcript.log +``` -- Rust release binaries: `scribe`, `proof-pilot`, `halva-bridge` -- elan + Lean toolchain pinned to `leanprover/lean4:v4.30.0-rc2` -- pre-cached Mathlib oleans (avoids the ~30-minute cold Mathlib build) +`proof-pilot` calls the model with the file + build errors, extracts the proof from the response, patches the file, and repeats until both the project build and the exact target compilation pass clean. Useful flags: -target image size is approximately 3.2 GB (Mathlib oleans account for ~2.5 GB of that). +- `--notes NOTES.md` — write a learning log; each iteration records the tactics tried and cites worked examples from `lean/ZkGadgets/`. +- `--save-transcript session.json` — save a versioned JSON transcript (iteration history, toolchain string, Mathlib rev). +- `--replay session.json` — deterministically replay a transcript; refuses on toolchain mismatch unless `--allow-toolchain-mismatch`. +- `--lsp` — use the Lean language server for structured diagnostics (goal states + hypotheses) instead of raw `lake build` text. +- `--system-prompt ` — override the default system prompt (`prompts/lean-prover.md`). -``` -# pull latest -docker pull ghcr.io/lucidsamuel/scribe:latest +See [`transcripts/poseidon-sbox.md`](transcripts/poseidon-sbox.md) for a session that closes the Poseidon S-box proof in 2 iterations. -# demo (no LLM call) -docker run --rm ghcr.io/lucidsamuel/scribe:latest scribe demo +## The Halva Bridge -# verify with your own files -docker run --rm \ - -e ANTHROPIC_API_KEY="$ANTHROPIC_API_KEY" \ - -v "$(pwd)":/workspace \ - ghcr.io/lucidsamuel/scribe:latest \ - scribe verify \ - --halva-output /workspace/extracted.lean \ - --spec-file /workspace/spec.lean \ - --output /workspace/Proof.lean +`halva-bridge` turns a real halo2 extraction into a proven soundness theorem. It parses Halva's `meets_constraints` output, merges in a user `Spec` + `soundness` theorem, and hands the result to `proof-pilot`. -# build locally (from repo root) -docker build -t scribe:dev . -docker run --rm scribe:dev scribe --help +```sh +cargo run -p halva-bridge -- examples/halva-range-check/extracted.lean \ + --spec-file examples/halva-range-check/spec.lean \ + --output lean/ZkGadgets/HalvaRangeCheck.lean ``` -tags: `latest` (main branch), `sha-` (per-commit), `v` (releases). +Use `--prove` to launch `proof-pilot` after scaffolding. Structured specs can use `--spec ` with repeatable `--extra-import ` flags; run `halva-bridge --help` for the backend and proof-loop options. + +The same flow scales to harder circuits. `examples/halva-fibonacci/` and `examples/halva-binary-number/` are real extractions (`cargo run --example fib` / `--example scroll-binary-number` in the Halva repo) bridged to proven theorems — exercising **copy constraints** and **multi-gate** circuits respectively, neither of which the range-check example touches. -## gadgets +## Proven Gadgets -| gadget | constraints | soundness claim | +Every theorem below is complete and kernel-checked (`lake build` is green, with no `sorry` / `axiom` / `native_decide`). + +| Gadget | Constraints | Soundness claim | |---|---|---| -| 8-bit range check | 9 (8 boolean + decomposition) | `∃ k : Fin 256, k.val = x` | +| 8-bit range check | 9 (8 boolean + decomposition) | `ZMod.val x < 256` (requires `p > 256`) | | conditional select | 2 (boolean + mux) | `(b = 0 ∧ z = y) ∨ (b = 1 ∧ z = x)` | | poseidon s-box | 3 (squaring chain) | `y = x ^ 5` | | non-zero check | 1 (inverse) | `x ≠ 0` | | edwards addition | 2 (baby jubjub add) | output point on curve | -| Halva polynomial range check | 1 (10-factor polynomial) | selected value is in `Fin 10` | -| Halva Fibonacci | 1 add gate + 17 copy constraints | output instance cell `= 21·f(0) + 34·f(1)` | -| Halva binary number | 4 (2 boolean + recomposition + range) | enabled rows hold bits `b₀,b₁` with value `= 2·b₀ + b₁`, never both set | +| **Halva** polynomial range check | 1 (10-factor polynomial) | `ZMod.val advice < 10` on enabled rows (requires `P > 10`) | +| **Halva** Fibonacci | 1 add gate + 17 copy constraints | output instance cell `= 21·f(0) + 34·f(1)` | +| **Halva** binary number | 4 (2 boolean + recomposition + range) | bits `b₀,b₁` with value `= 2·b₀ + b₁`, never both set | -## git hooks +## Docker -reject commits that add `sorry`, `axiom`, or `native_decide` to lean files: +The `ghcr.io/lucidsamuel/scribe` image is built on every push to `main` and on version tags (`.github/workflows/docker.yml`). It bundles: +- Rust release binaries: `scribe`, `proof-pilot`, `halva-bridge` +- elan + the Lean toolchain pinned to `leanprover/lean4:v4.30.0-rc2` +- pre-cached Mathlib oleans (~2.5 GB of the ~3.2 GB image) + +```sh +docker pull ghcr.io/lucidsamuel/scribe:latest +docker run --rm ghcr.io/lucidsamuel/scribe:latest scribe demo + +# build locally (from repo root) +docker build -t scribe:dev . +docker run --rm scribe:dev scribe --help ``` -git config core.hooksPath .githooks -``` -## project structure +Tags: `latest` (main branch), `sha-` (per-commit), `v` (releases). + +## Project Structure ``` crates/ gadget-ir/ constraint system IR + TOML deserialization lean-emit/ IR → Lean 4 scaffold with sorry - proof-pilot/ LLM proof loop (patcher, lean runner, session logging, transcript) + proof-pilot/ LLM proof loop (patcher, lean runner, session logging, transcript, replay) halva-bridge/ Halva extraction + semantic specification bridge - scribe-cli/ top-level `scribe` binary (verify + demo subcommands) -lean/ - ZkGadgets/ - Field.lean field helper lemmas (proven) - RangeCheck.lean 8-bit range check soundness (proven) - ConditionalSelect.lean conditional select soundness (proven) - PoseidonSbox.lean poseidon s-box x^5 soundness (proven) - NonzeroCheck.lean field nonzero check soundness (proven) - EdwardsAddition.lean baby jubjub addition closure (proven) - HalvaRangeCheck.lean Halva range-check extraction soundness (proven) - HalvaFibonacci.lean Halva Fibonacci extraction soundness — copy constraints (proven) - HalvaBinaryNumber.lean Halva binary-number extraction soundness — 4 gates (proven) -examples/ - range-check/ 8-bit range check (9 witnesses, 9 constraints) - conditional-select/ conditional select (4 witnesses, 2 constraints) - poseidon-sbox/ poseidon s-box x^5 (4 witnesses, 3 constraints) - nonzero-check/ field inverse (2 witnesses, 1 constraint) - edwards-addition/ baby jubjub point addition (6 witnesses, 2 constraints) - halva-range-check/ real Halva extraction + user specification - halva-fibonacci/ real Halva extraction (add gate + copy constraints) + spec - halva-binary-number/ real Halva extraction (4 gates, fixed-column enable) + spec -transcripts/ - poseidon-sbox.md example proof-pilot session (autonomous closure in 2 iterations) -docs/ - architecture.md data flow + crate descriptions - why.md motivation + scribe-cli/ top-level `scribe` binary (verify + init + demo) + bench/ ZKGadgetEval benchmark suite +lean/ZkGadgets/ the proven theorems (Field + 8 gadgets) +examples/ IR / extraction + spec inputs for every gadget +transcripts/ example proof-pilot sessions +prompts/ system prompt(s) for the proof loop +docs/ architecture.md, why.md ``` -## docs +## Documentation + +- [**architecture.md**](docs/architecture.md) — data flow, crate descriptions, how the pieces connect. +- [**why.md**](docs/why.md) — motivation: why formally verify ZK circuits, and why an LLM loop. +- [**poseidon-sbox transcript**](transcripts/poseidon-sbox.md) — a real session closing a proof in 2 iterations. + +## Contributing + +Contributions are welcome — please open an issue or PR on [GitHub](https://github.com/LucidSamuel/scribe). + +Before committing, enable the git hook that rejects any `sorry`, `axiom`, or `native_decide` added to Lean files: + +```sh +git config core.hooksPath .githooks +``` -- [architecture.md](docs/architecture.md) — data flow, crate descriptions, how the pieces connect -- [why.md](docs/why.md) — motivation: why formal verification of zk circuits, why an llm loop -- [poseidon-sbox transcript](transcripts/poseidon-sbox.md) — example proof-pilot session closing a proof in 2 iterations +> [!CAUTION] +> CI runs `cargo check` + `cargo test --workspace`, `lake build`, and a `sorry`/`axiom`/`native_decide` scan over `lean/ZkGadgets`. A green local `lake build` and `cargo test` are the bar before opening a PR; running `cargo fmt` and `cargo clippy` first is good practice. -## license +## License -MIT +Licensed under the [MIT License](./LICENSE-MIT). diff --git a/examples/halva-range-check/spec.lean b/examples/halva-range-check/spec.lean index a7e0737..4ecfc19 100644 --- a/examples/halva-range-check/spec.lean +++ b/examples/halva-range-check/spec.lean @@ -3,12 +3,17 @@ import Mathlib.Algebra.Field.ZMod import Mathlib.Tactic.LinearCombination -/-- Specification: when the range-check selector is enabled at a row, - the advice value in that row is in [0, 10). - Requires the prime P > 10 so that ZMod P casts are injective on Fin 10. -/ +/-- Specification: when the range-check selector is enabled at a row, the advice + value in that row is genuinely in [0, 10) — its canonical natural representative + `ZMod.val` is `< 10`. + + This is the honest, non-vacuous statement. The form + `∃ k : Fin 10, (k.val : ZMod P) = advice` is vacuous when `P ≤ 10` (the casts of + `0..9` then cover all of `ZMod P`), so it is provable without ever using `hp`. + `ZMod.val advice < 10` cannot be proved without `hp : P > 10`. -/ def Spec (c: ValidCircuit P P_Prime) (hp: P > 10): Prop := ∀ row : ℕ, c.get_selector 0 row = 1 → - ∃ k : Fin 10, (k.val : ZMod P) = c.get_advice 0 row + ZMod.val (c.get_advice 0 row) < 10 /-- Soundness: if the circuit meets all halo2 constraints (extracted by Halva), then it satisfies the range-check specification. diff --git a/lean/ZkGadgets.lean b/lean/ZkGadgets.lean index eb89140..6b11a31 100644 --- a/lean/ZkGadgets.lean +++ b/lean/ZkGadgets.lean @@ -1,3 +1,4 @@ +import ZkGadgets.Audit import ZkGadgets.Field import ZkGadgets.RangeCheck import ZkGadgets.ConditionalSelect diff --git a/lean/ZkGadgets/Audit.lean b/lean/ZkGadgets/Audit.lean new file mode 100644 index 0000000..3d8d876 --- /dev/null +++ b/lean/ZkGadgets/Audit.lean @@ -0,0 +1,99 @@ +import Lean + +/-! +# Spec audit — hypothesis-liveness checks (verdict engine, C1) + +The Lean kernel checks that a *proof* is correct, but nothing checks that the +*statement* is meaningful. This module is the deterministic core of a "verdict +engine": a refuter that complements the (single-sided) proof loop by flagging +degenerate statements a kernel-accepted proof would otherwise hide. + +It implements **C1, hypothesis-liveness**, which catches two real regression +classes that both shipped in this repo at one point: + +* **Decorative hypothesis** — a statement carries an explicit hypothesis its proof + never uses (e.g. a bound passed to a `Spec` but ignored). `#audit_uses` flags it. +* **Dropped side-condition** — an intended hypothesis never reaches the signature + (e.g. a `variable (hp : p > 256)` the theorem never references, so Lean omits it). + `#audit_requires` guards a load-bearing condition by name. + +Both commands fail the build (`logError`) when they fire, so they act as live CI +gates next to a theorem. The remaining checks — finite-model non-vacuity probes +(C2), antecedent satisfiability (C3), and an adversarial refuter (C4) — are future +work and not implemented here. +-/ + +open Lean Elab Command Meta + +namespace ScribeAudit + +/-- The names of a declaration's **explicit, proposition-typed** binders that do not + occur in its proof term — i.e. hypotheses the proof never uses. A non-empty + result is a "decorative hypothesis" smell. -/ +def unusedHyps (declName : Name) : MetaM (Array Name) := do + let info ← getConstInfo declName + -- `ConstantInfo.value?` excludes theorems, so match explicitly. + let value ← match info with + | .thmInfo ti => pure ti.value + | .defnInfo di => pure di.value + | _ => throwError "audit: '{declName}' has no proof term to inspect" + lambdaTelescope value fun args body => do + let mut unused : Array Name := #[] + for arg in args do + let fvarId := arg.fvarId! + let ldecl ← fvarId.getDecl + -- only consider explicit hypotheses; skip implicits and instance arguments + if ldecl.binderInfo.isExplicit && (← isProp ldecl.type) then + unless body.hasAnyFVar (· == fvarId) do + unused := unused.push ldecl.userName + return unused + +/-- Render a declaration's type as a flat string for substring checks. -/ +def signatureString (declName : Name) : MetaM String := do + let info ← getConstInfo declName + return toString (← ppExpr info.type) + +end ScribeAudit + +/-- `#audit_uses thm` fails the build if `thm` has an explicit hypothesis its proof + never uses (a decorative / possibly-vacuous hypothesis). Silent on success, so it + works as a live regression gate placed next to a theorem. -/ +elab "#audit_uses " id:ident : command => do + liftTermElabM do + let declName ← realizeGlobalConstNoOverload id + let unused ← ScribeAudit.unusedHyps declName + unless unused.isEmpty do + let names := String.intercalate ", " (unused.toList.map toString) + logError m!"audit ✗ {declName}: unused (possibly decorative) hypotheses: {names}" + +/-- `#audit_requires thm "needle"` fails the build unless `needle` appears in `thm`'s + signature. Use it to pin a load-bearing side-condition (e.g. `"p > 256"`) so that + silently dropping it — the classic vacuous-spec regression — turns the build red. -/ +elab "#audit_requires " id:ident needle:str : command => do + liftTermElabM do + let declName ← realizeGlobalConstNoOverload id + let sig ← ScribeAudit.signatureString declName + let needleStr := needle.getString + unless (sig.splitOn needleStr).length ≥ 2 do + logError m!"audit ✗ {declName}: required hypothesis '{needleStr}' is absent from the signature — it may have been dropped" + +namespace ScribeAudit.SelfTest + +-- The decoy below deliberately ignores a hypothesis; that is the property under test. +set_option linter.unusedVariables false + +-- A hypothesis the proof never uses: must be reported. +private theorem decoy_decorative (n : Nat) (hbig : n > 5) : n = n := rfl +-- A hypothesis the proof genuinely uses: must not be reported. +private theorem decoy_live (n : Nat) (h : n = 0) : n = 0 := h + +-- Deterministic unit test of the detection logic (independent of message wording). +run_cmd liftTermElabM do + let bad ← ScribeAudit.unusedHyps ``decoy_decorative + unless bad == #[`hbig] do + throwError "audit self-test failed: expected [hbig] unused, got {bad}" + let good ← ScribeAudit.unusedHyps ``decoy_live + unless good.isEmpty do + throwError "audit self-test failed: expected no unused hyps, got {good}" + +end ScribeAudit.SelfTest diff --git a/lean/ZkGadgets/HalvaRangeCheck.lean b/lean/ZkGadgets/HalvaRangeCheck.lean index c43732d..df7eb73 100644 --- a/lean/ZkGadgets/HalvaRangeCheck.lean +++ b/lean/ZkGadgets/HalvaRangeCheck.lean @@ -4,6 +4,7 @@ import Mathlib.Data.ZMod.Defs import Mathlib.Data.ZMod.Basic import Mathlib.Algebra.Field.ZMod import Mathlib.Tactic.LinearCombination +import ZkGadgets.Audit set_option linter.unusedVariables false @@ -113,12 +114,19 @@ def meets_constraints (c: ValidCircuit P P_Prime): Prop := all_shuffles c ∧ ∀ col row: ℕ, (row < c.n ∧ row ≥ c.usable_rows) → c.1.Instance col row = c.1.InstanceUnassigned col row -/-- Specification: when the range-check selector is enabled at a row, - the advice value in that row is in [0, 10). - Requires the prime P > 10 so that ZMod P casts are injective on Fin 10. -/ +/-- Specification: when the range-check selector is enabled at a row, the advice + value in that row is genuinely in [0, 10) — i.e. its canonical natural + representative `ZMod.val` is `< 10`. + + This is the honest, non-vacuous statement. The earlier form + `∃ k : Fin 10, (k.val : ZMod P) = advice` is vacuous when `P ≤ 10` (the casts of + `0..9` then cover all of `ZMod P`), so it is provable without ever using `hp` — + making `hp` decorative. `ZMod.val advice < 10` cannot be proved without `hp`: + the bound `P > 10` is exactly what forces `ZMod.val` to agree with the small + integer the advice cell encodes. -/ def Spec (c: ValidCircuit P P_Prime) (hp: P > 10): Prop := ∀ row : ℕ, c.get_selector 0 row = 1 → - ∃ k : Fin 10, (k.val : ZMod P) = c.get_advice 0 row + ZMod.val (c.get_advice 0 row) < 10 /-- Soundness: if the circuit meets all halo2 constraints (extracted by Halva), then it satisfies the range-check specification. @@ -127,15 +135,16 @@ theorem soundness (c: ValidCircuit P P_Prime) (hp: P > 10) (h: meets_constraints c): Spec c hp := by haveI : Fact (Nat.Prime P) := ⟨P_Prime⟩ intro row hsel - unfold meets_constraints at h - obtain ⟨_, _, _, _, _, _, hgates, _⟩ := h - unfold all_gates gate_0 at hgates - have hgate := hgates row - simp only [hsel, one_mul] at hgate - set v := c.get_advice 0 row with hv - -- Product of 10 factors = 0; since ZMod P is a field (prime P), split on which factor is 0 - rcases mul_eq_zero.mp hgate with h | h - · rcases mul_eq_zero.mp h with h | h + -- The gate forces the advice value to be one of the field elements 0..9. + have hex : ∃ k : Fin 10, ((k.val : ℕ) : ZMod P) = c.get_advice 0 row := by + unfold meets_constraints at h + obtain ⟨_, _, _, _, _, _, hgates, _⟩ := h + unfold all_gates gate_0 at hgates + have hgate := hgates row + simp only [hsel, one_mul] at hgate + set v := c.get_advice 0 row with hv + -- Product of 10 factors = 0; since ZMod P is a field (prime P), split on which factor is 0 + rcases mul_eq_zero.mp hgate with h | h · rcases mul_eq_zero.mp h with h | h · rcases mul_eq_zero.mp h with h | h · rcases mul_eq_zero.mp h with h | h @@ -143,28 +152,45 @@ theorem soundness (c: ValidCircuit P P_Prime) (hp: P > 10) · rcases mul_eq_zero.mp h with h | h · rcases mul_eq_zero.mp h with h | h · rcases mul_eq_zero.mp h with h | h - · -- v = 0 - exact ⟨⟨0, by omega⟩, by simpa using h.symm⟩ - · -- 1 + -v = 0 → v = 1 - have hv1 : v = 1 := by linear_combination -h - exact ⟨⟨1, by omega⟩, by simpa using hv1.symm⟩ - · -- 2 + -v = 0 → v = 2 - have hv2 : v = 2 := by linear_combination -h - exact ⟨⟨2, by omega⟩, by simpa using hv2.symm⟩ - · have hv3 : v = 3 := by linear_combination -h - exact ⟨⟨3, by omega⟩, by simpa using hv3.symm⟩ - · have hv4 : v = 4 := by linear_combination -h - exact ⟨⟨4, by omega⟩, by simpa using hv4.symm⟩ - · have hv5 : v = 5 := by linear_combination -h - exact ⟨⟨5, by omega⟩, by simpa using hv5.symm⟩ - · have hv6 : v = 6 := by linear_combination -h - exact ⟨⟨6, by omega⟩, by simpa using hv6.symm⟩ - · have hv7 : v = 7 := by linear_combination -h - exact ⟨⟨7, by omega⟩, by simpa using hv7.symm⟩ - · have hv8 : v = 8 := by linear_combination -h - exact ⟨⟨8, by omega⟩, by simpa using hv8.symm⟩ - · have hv9 : v = 9 := by linear_combination -h - exact ⟨⟨9, by omega⟩, by simpa using hv9.symm⟩ + · rcases mul_eq_zero.mp h with h | h + · -- v = 0 + exact ⟨⟨0, by omega⟩, by simpa using h.symm⟩ + · -- 1 + -v = 0 → v = 1 + have hv1 : v = 1 := by linear_combination -h + exact ⟨⟨1, by omega⟩, by simpa using hv1.symm⟩ + · -- 2 + -v = 0 → v = 2 + have hv2 : v = 2 := by linear_combination -h + exact ⟨⟨2, by omega⟩, by simpa using hv2.symm⟩ + · have hv3 : v = 3 := by linear_combination -h + exact ⟨⟨3, by omega⟩, by simpa using hv3.symm⟩ + · have hv4 : v = 4 := by linear_combination -h + exact ⟨⟨4, by omega⟩, by simpa using hv4.symm⟩ + · have hv5 : v = 5 := by linear_combination -h + exact ⟨⟨5, by omega⟩, by simpa using hv5.symm⟩ + · have hv6 : v = 6 := by linear_combination -h + exact ⟨⟨6, by omega⟩, by simpa using hv6.symm⟩ + · have hv7 : v = 7 := by linear_combination -h + exact ⟨⟨7, by omega⟩, by simpa using hv7.symm⟩ + · have hv8 : v = 8 := by linear_combination -h + exact ⟨⟨8, by omega⟩, by simpa using hv8.symm⟩ + · have hv9 : v = 9 := by linear_combination -h + exact ⟨⟨9, by omega⟩, by simpa using hv9.symm⟩ + -- Convert membership in {0..9} to the honest bound. This step needs `hp : P > 10`: + -- without it `ZMod.val` of the cast could wrap around and exceed 10. + obtain ⟨k, hk⟩ := hex + have hkP : (k.val : ℕ) < P := by have := k.isLt; omega + rw [← hk, ZMod.val_natCast_of_lt hkP] + exact k.isLt + +/-- Non-vacuity witness: the bound `ZMod.val advice < 10` is a genuine restriction. + In `ZMod 11` (prime, > 10) the element `10` refutes it, so the spec is not + `True` in disguise and the `P > 10` hypothesis is load-bearing. -/ +example : ¬ ((10 : ZMod 11).val < 10) := by decide end RangeCheck + +-- Verdict-engine guards (C1): the `P > 10` bound must stay in the signature, and the +-- soundness proof must actually use it (it was decorative before the non-vacuity fix). +#audit_requires RangeCheck.soundness "P > 10" +#audit_uses RangeCheck.soundness diff --git a/lean/ZkGadgets/RangeCheck.lean b/lean/ZkGadgets/RangeCheck.lean index 23d5ee2..57ba632 100644 --- a/lean/ZkGadgets/RangeCheck.lean +++ b/lean/ZkGadgets/RangeCheck.lean @@ -1,4 +1,5 @@ import ZkGadgets.Field +import ZkGadgets.Audit import Mathlib.Data.ZMod.Basic import Mathlib.Data.Fin.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic @@ -11,17 +12,27 @@ Constraint system: b_i * (b_i - 1) = 0 for i in [0, 8) (each bit is boolean) sum (b_i * 2^i) = x (bit decomposition) -Soundness: if the constraints hold and p > 256, then x is in [0, 256). +Soundness: if the constraints hold and p > 256, then `x` is genuinely a byte, +i.e. its canonical natural representative is in [0, 256). + +The conclusion is `ZMod.val x < 256`, NOT `∃ k : Fin 256, (k.val : ZMod p) = x`. +The existential is vacuous whenever `p ≤ 256` (every field element is then the cast +of some byte), so it would state something strictly weaker than "x is a byte" and +could be proved without ever using `hp`. `ZMod.val x < 256` cannot be proved without +`hp` — the bound `p > 256` is what makes `ZMod.val` agree with the integer value. -/ -variable (p : ℕ) [Fact (Nat.Prime p)] (hp : p > 256) +variable (p : ℕ) [Fact (Nat.Prime p)] theorem range_check_8bit_sound + -- `hp` is an explicit, load-bearing hypothesis: the proof fails without it, and + -- `#check @range_check_8bit_sound` shows it in the signature (it is not dropped). + (hp : p > 256) (x : ZMod p) (bits : Fin 8 → ZMod p) (h_bit : ∀ i : Fin 8, bits i * (bits i - 1) = 0) (h_decomp : (∑ i : Fin 8, bits i * (2 : ZMod p) ^ (i : ℕ)) = x) : - ∃ k : Fin 256, (k.val : ZMod p) = x := by + ZMod.val x < 256 := by -- Each bit is 0 or 1 in ZMod p have h01 : ∀ i, bits i = 0 ∨ bits i = 1 := fun i => bit_boolean p (bits i) (h_bit i) -- Natural representative for each bit @@ -40,9 +51,25 @@ theorem range_check_8bit_sound exact Nat.mul_le_mul_right _ (hle i) · simp only [Fin.sum_univ_succ, Fin.sum_univ_zero, Fin.val_zero, Fin.val_succ] omega - -- Provide the Fin 256 witness - exact ⟨⟨∑ i : Fin 8, nb i * 2 ^ (i : ℕ), hlt⟩, by + -- x is the cast of the natural weighted sum N, with N < 256. + have hxN : x = ((∑ i : Fin 8, nb i * 2 ^ (i : ℕ) : ℕ) : ZMod p) := by rw [← h_decomp] push_cast congr 1; ext i - rw [hcast i]⟩ + rw [hcast i] + -- N < 256 < p (this is where `hp` is used), so `ZMod.val` of the cast is exactly N. + have hNp : (∑ i : Fin 8, nb i * 2 ^ (i : ℕ)) < p := by omega + rw [hxN, ZMod.val_natCast_of_lt hNp] + exact hlt + +/-- Non-vacuity witness: the byte bound `ZMod.val x < 256` is a genuine restriction, + not `True` in disguise. In `ZMod 257` (prime, > 256) the element `256` refutes the + conclusion — so the soundness theorem is saying something real, and dropping the + constraints (or the `p > 256` hypothesis) would make it false. This is the kind of + refutation a spec-level search should always be able to find for an honest spec. -/ +example : ¬ ((256 : ZMod 257).val < 256) := by decide + +-- Verdict-engine guards (C1): fail the build if the `p > 256` bound is ever dropped +-- from the signature, or if the proof stops using a declared hypothesis. +#audit_requires range_check_8bit_sound "p > 256" +#audit_uses range_check_8bit_sound