From 71c819fcb46b4d0c58ac611dca059fd0c90a29f4 Mon Sep 17 00:00:00 2001 From: Alexander Hicks Date: Thu, 11 Jun 2026 14:30:12 +0100 Subject: [PATCH] Document Felt drop-in roadmap and Phase 10 bootstrap --- README.md | 9 +- docs/README.md | 20 +- docs/drop-in-roadmap.md | 332 ++++++++++++++++++ docs/future-c-drop-in.md | 16 +- docs/harness/SOURCES.md | 5 + docs/phases/PHASE-09-drop-in-roadmap.md | 70 ++++ .../PHASE-10-toolchain-replacement-spike.md | 98 ++++++ docs/strategy-e-certificates.md | 2 +- reviews/PHASE-10/evidence/README.md | 5 + reviews/PHASE-10/evidence/toolchain-smoke.md | 42 +++ scripts/harness/phase10-toolchain-smoke.sh | 77 ++++ 11 files changed, 663 insertions(+), 13 deletions(-) create mode 100644 docs/drop-in-roadmap.md create mode 100644 docs/phases/PHASE-09-drop-in-roadmap.md create mode 100644 docs/phases/PHASE-10-toolchain-replacement-spike.md create mode 100644 reviews/PHASE-10/evidence/README.md create mode 100644 reviews/PHASE-10/evidence/toolchain-smoke.md create mode 100755 scripts/harness/phase10-toolchain-smoke.sh diff --git a/README.md b/README.md index 82140cb..4629ac4 100644 --- a/README.md +++ b/README.md @@ -26,7 +26,7 @@ LLZK's Felt dialect: and Mathlib out of LLZK's runtime trusted base. The current proof basis is the clean VEIR commit -[`d4cc1bf2d31beeca17eb2e8c9c7181d04af013a3`](docs/harness/PINS.md), +[`d899d95004d4bd988c8456d686c33b11a7a5eb4a`](docs/harness/PINS.md), selected from `project-llzk/veir` branch `felt-review-structural-close` and pinned through Lake metadata. @@ -55,10 +55,15 @@ documented under [`docs/`](docs/): dependency state. - [`docs/harness/CURRENT.md`](docs/harness/CURRENT.md) — active phase and acceptance rule for the harness. +- [`docs/drop-in-roadmap.md`](docs/drop-in-roadmap.md) — single roadmap + for the Felt drop-in replacement goal, including coverage, toolchain, + proof/certificate, assumptions, and TCB requirements. +- [`scripts/harness/phase10-toolchain-smoke.sh`](scripts/harness/phase10-toolchain-smoke.sh) + — Phase 10 bootstrap smoke for the current external-driver replacement path. - [`docs/future-b-extraction.md`](docs/future-b-extraction.md) — Future: extract VEIR's verified rewriter to C++. - [`docs/future-c-drop-in.md`](docs/future-c-drop-in.md) — Future: - drop-in replacement for LLZK's Felt dialect. + full replacement of the `llzk-opt` binary. - [`docs/future-d-ffi-plugin.md`](docs/future-d-ffi-plugin.md) — Future: FFI plugin for the Lean rewriter. - [`docs/future-f-folders-only.md`](docs/future-f-folders-only.md) — diff --git a/docs/README.md b/docs/README.md index 8863589..232e3a8 100644 --- a/docs/README.md +++ b/docs/README.md @@ -21,9 +21,19 @@ LLZK maintainers. - [Dependency pins](harness/PINS.md). Exact VEIR commit, allowed modes, update procedure, rollback procedure, and forbidden hidden state. - [Harness gates](harness/GATES.md). Strict checks required before claiming - Phase 1 acceptance. -- [Phase 1 — reproducible pins](phases/PHASE-01-pins-and-repro.md). Current - phase plan and review requirements. + phase acceptance. +- [Phase 8 — field preconditions](phases/PHASE-08-strategy-a-field-preconditions.md). + Current completed implementation milestone. +- [Phase 9 — drop-in roadmap and claim reset](phases/PHASE-09-drop-in-roadmap.md). + Completed planning baseline after the Phase 8 merge. +- [Phase 10 — toolchain replacement spike](phases/PHASE-10-toolchain-replacement-spike.md). + Bootstrap phase for the external-driver smoke and profile split. + +## Drop-in roadmap + +- [Felt drop-in replacement roadmap](drop-in-roadmap.md). The current + project-wide plan for moving from Phase 8 assurance infrastructure toward + a high-assurance replacement for the C++ Felt dialect path. ## Documented future options @@ -35,8 +45,8 @@ LLZK maintainers. - [Strategy D — Lean MLIR dialect plugin via FFI](future-d-ffi-plugin.md). LLZK loads a Lean `.so` as the dialect implementation. - [Strategy C — Full replacement of `llzk-opt`](future-c-drop-in.md). - `veir-opt` replaces `llzk-opt`. Multi-year scope; documented here - for completeness rather than as an active plan. + `veir-opt` replaces all of `llzk-opt`. Multi-year scope; documented here + for completeness rather than as the current Felt-only roadmap. ## Picking among them diff --git a/docs/drop-in-roadmap.md b/docs/drop-in-roadmap.md new file mode 100644 index 0000000..8f5f91a --- /dev/null +++ b/docs/drop-in-roadmap.md @@ -0,0 +1,332 @@ +# Felt Drop-In Replacement Roadmap + +Last reviewed: 2026-06-11 + +Status: planning baseline after Phase 8. This document is not acceptance +evidence by itself. + +## Goal + +The final goal is a high-assurance replacement for the C++ LLZK Felt dialect +path. In this roadmap, "drop-in replacement" means: + +- existing Felt workloads can use the VEIR-backed path without changing their + source programs; +- the selected VEIR pass profile produces output accepted by the same downstream + LLZK consumers as the C++ path; +- every intended semantic difference from the C++ path is explicit, reviewed, + and gated, with a rollback path; +- the assurance claim says exactly what was checked, what was proved, and what + remains trusted. + +This is not the same as immediately replacing all of `llzk-opt`. Full +`llzk-opt` replacement remains Strategy C and is still a multi-year, +LLZK-wide project. The active target is narrower: make the Felt dialect +implementation and Felt-affecting canonicalization path replaceable first. + +## Replacement Profiles + +The project has two related but distinct replacement profiles. + +**C++-parity profile.** This is the adoption baseline. It should reproduce +the accepted C++ LLZK Felt behavior closely enough that existing callers can +opt in, compare results, bisect regressions, and fall back without ambiguity. +Parity does not mean the C++ behavior is ideal; it is the stable contract used +to make replacement low-risk. + +**Enhanced VEIR profile.** This is the value case. It can run verified +canonicalizations that C++ LLZK does not currently perform, provided each +intentional output difference is explicitly accepted, covered by differential +tests, tied to executable VEIR semantics, and checked for downstream +compatibility. + +Current `EXPECTED-DIVERGE` cases are therefore not automatically bad. They are +classified evidence. A divergence is a blocker for the parity profile unless +it is disabled there; the same divergence may be promoted to an enhanced-profile +feature once its semantic and toolchain claims are reviewed. + +## Current Baseline + +- `project-llzk/veir#1` is merged into `main` at merge commit + `45d31a20b4ff10498f7caba3c8b635553cc93dea`; the merged head was + `42db1ae3cbe76ca6c917501acc8e92a4f01cbc75`. +- `opencompl/veir#829` is closed unmerged. The working integration target is + the `project-llzk/veir` fork. +- llzk-lean's accepted VEIR dependency pin is + `d899d95004d4bd988c8456d686c33b11a7a5eb4a`. +- The accepted LLZK source basis is `project-llzk/llzk-lib` commit + `db922857bc5a88a9107627ef6b36a8b5e57bc5c2`. +- The clean-pin canonical differential corpus currently records + `21 pass (incl. expected-diverge), 0 fail`: 10 positive PASS cases, 10 + canonical `EXPECTED-DIVERGE` cases, and 1 `EXPECTED-LLZK-FAIL`. +- VEIR currently has 15 Felt rewrite patterns over 5 accepted Felt operations: + `const`, `add`, `sub`, `mul`, and `neg`. +- The accepted LLZK Felt dialect has 18 operations. VEIR still lacks semantic + models, interpreter cases, and folder parity for `pow`, `div`, `uintdiv`, + `sintdiv`, `umod`, `smod`, `inv`, `bit_and`, `bit_or`, `bit_xor`, + `bit_not`, `shl`, and `shr`. +- Strategy E certificates currently cover 2 of 15 VEIR Felt rewrite patterns. + The C++ checker has a live JSON loader and polarity dispatcher, but the real + MLIR matcher and `LLZKVerifyRewritesPass` are not implemented. + +## Repository Responsibilities + +`veir` provides the executable and proof-side implementation: + +- LLZK Felt IR representation, parser/printer support, verifier shape checks, + and the `felt-combine` pass. +- Lean proofs for arithmetic identities and IR structural rewrite + well-formedness for the current 15 patterns. +- The standalone Felt runtime-value proof-of-concept in + `Veir/Passes/Felt/InterpModel.lean`. +- The canonical diff driver `scripts/llzk-diff.sh`. + +`veir` does not currently provide complete 18-operation semantics, a +C++-matching Felt canonicalization profile, a whole-program semantic theorem, +or a toolchain integration point that can replace the C++ Felt path directly. + +`llzk-lean` provides the assurance and integration harness: + +- exact source-truth and pin gates for the LLZK source and consumed VEIR proof + basis; +- the differential corpus, expected-divergence polarity, and clean-pin + canonical evidence path; +- the certificate schema, emitter, committed certificate snapshot, and C++ + checker prototype; +- review artifacts and non-claim documentation. + +`llzk-lean` does not implement the Felt dialect itself and does not modify +upstream `llzk-lib` at runtime. + +## Drop-In Definition Of Done + +The Felt replacement is ready only when all of the following are true: + +1. **Toolchain path selected.** There is a reviewed invocation path, either an + out-of-tree replacement driver, an LLZK pass plugin, or an upstreamed + `llzk-opt` integration. The path must define how existing callers opt into + the VEIR-backed Felt implementation and how they fall back to C++. +2. **Replacement profiles are separated.** VEIR exposes a C++-parity profile + for low-risk adoption and an enhanced VEIR profile for verified + improvements. The current stronger algebraic-only `felt-combine` rewrites + that LLZK does not perform must be disabled in the parity profile or + promoted through explicit enhanced-profile acceptance. +3. **Full source coverage ledger.** Every accepted LLZK Felt op, type, + attribute, trait, verifier rule, and folder behavior has a row mapping + LLZK source to VEIR implementation, differential coverage, proof status, and + known assumptions. +4. **Differential coverage is complete for the target surface.** The harness + mirrors `llzk-lib/test/Dialect/Felt/` and representative project workloads, + including positive, no-fire, verifier-reject, and expected-failure cases. + Acceptance evidence has no tool skips. +5. **Runtime semantics are stated correctly.** Proof statements are tied to + the executable matchers, side conditions, result constructors, field + registry behavior, and runtime values. Arithmetic identities alone are + documented only as supporting lemmas. +6. **Certificate route assessed by prototype.** At least one aligned C++/VEIR + fold, initially `constant_fold_add`, is validated through a real MLIR + matcher and rewrite listener. The prototype must state whether certificates + add enough assurance to justify expanding Strategy E. +7. **Trusted base published.** The roadmap, harness docs, and repo READMEs list + every trusted component and caveat: Lean kernel, Mathlib, VEIR IR model, + runtime guards, LLZK source commit, field registry mirror, normalizer, + `llzk-opt` binary, C++ checker, MLIR/LLVM APIs, and any wrapper or plugin. + +## Roadmap + +### Phase 9: Roadmap and Claim Reset + +Deliverables: + +- Make this roadmap the single source of truth for the drop-in objective. +- Update stale top-level pin and proof-boundary wording. +- Define the profile policy: C++ parity is the adoption baseline; enhanced + VEIR is the improvement track. +- Keep Phase 8 as the last completed implementation milestone; do not claim + Phase 9 implementation acceptance until new evidence exists. +- Bootstrap Phase 10 with a concrete toolchain smoke, while keeping the + existing Phase 8 freshness gate intact until Phase 10 has real evidence. + +Exit criteria: + +- Both repos point to the roadmap. +- Current accepted pins and non-claims are consistent in live docs. +- The roadmap distinguishes parity failures from intentional enhanced-profile + improvements. + +### Phase 10: Toolchain Replacement Spike + +Deliverables: + +- Decide the first executable integration shape: + external `veir-opt`/wrapper, MLIR pass plugin, or upstream `llzk-opt` pass. +- Exercise the existing lower-first wrapper as the initial external-driver + spike, so LLZK custom assembly is lowered through `llzk-opt` before VEIR + runs the selected Felt profile. +- Define the exact command sequence equivalent to the C++ path currently + tested as `llzk-opt --canonicalize --mlir-print-op-generic`. +- Add a smoke wrapper that runs both the aligned fold path and the no-fire + precondition path over LLZK custom assembly. +- Record which profile is being exercised. The bootstrap smoke uses the + current enhanced `felt-combine,dce` path until a C++-parity profile exists. + +Exit criteria: + +- One command runs both paths over the same input and records comparable output. +- The command documents which side owns parsing, lowering, canonicalization, + and printing. +- The next implementation issue is precise: either introduce the parity profile + in VEIR, or explicitly accept a current enhanced-profile divergence. + +### Phase 11: Full Coverage Ledger + +Deliverables: + +- Replace the current 18-row operation gap ledger with a drop-in matrix: + syntax, verifier, trait, folder, parser/printer, differential, proof, and + certificate status. +- Extract all C++ Felt folder cases from `Ops.cpp` and `FeltFoldTests.cpp`, + including divide-by-zero no-fold cases, signed integer behavior, bitwidth + behavior, `NotFieldNative` gating, and field-registry preconditions. + +Exit criteria: + +- Each C++ fold has a corresponding VEIR implementation status and at least one + planned positive/no-fire corpus case. +- Missing coverage is quantified, not described narratively. + +### Phase 12: LLZK-Parity VEIR Profile + +Deliverables: + +- Split the VEIR Felt pass surface into a C++-parity profile and a stronger + verified-optimization profile. +- Port missing constant-fold behavior for the 13 unimplemented operations, in + priority order: `inv`/`div`, `pow`, unsigned/signed div/mod, shifts, bit ops. +- Model LLZK's field registry, registered-field requirement, zero-divisor + no-fold behavior, signed representative conversion, bitwidth, and + `NotFieldNative` scope rules. + +Exit criteria: + +- The parity profile does not produce the 10 current nonconstant algebraic + expected divergences unless those divergences are promoted through explicit + acceptance review. +- Every implemented folder has matching differential tests against the C++ + source behavior. + +### Phase 13: Corpus Expansion and Dashboard + +Deliverables: + +- Mirror all `llzk-lib/test/Dialect/Felt/` inputs or generic equivalents. +- Add representative workload corpora from `llzk-benchmarks` where Felt + operations appear in realistic contexts. +- Generate a coverage dashboard from the corpus and ledger. + +Exit criteria: + +- Clean-pin canonical differential evidence has no skips and no unreviewed + failures. +- Dashboard reports coverage by LLZK op, C++ folder, VEIR pattern, and known + expected divergence. + +### Phase 14: Proof-Certificate Prototype + +Deliverables: + +- Implement the MLIR-backed matcher for the current certificate schema. +- Wire a minimal rewrite-listener prototype for one aligned fold, starting with + `constant_fold_add`. +- Replace hand-authored cert shape for the prototype with VEIR-side metadata or + another auditable derivation mechanism. + +Exit criteria: + +- A real LLZK/MLIR rewrite event is accepted or rejected by the checker using + the committed cert snapshot. +- The prototype report states what assurance the certificate adds beyond the + differential harness and what remains in the TCB. + +### Phase 15: Proof Statement Hardening + +Deliverables: + +- Extend value-level runtime lemmas beyond `right_identity_zero_add` to every + parity folder that will ship in the drop-in profile. +- Prove or document bridges between canonical `Nat` runtime values, + `ZMod p` supporting lemmas, and LLZK's `Field::reduce` behavior. +- Keep whole-program `interpret(after) = interpret(before)` out of the + critical path unless separately funded; if pursued, state its dependency on + VEIR dominance assumptions. + +Exit criteria: + +- Each proof-backed runtime claim cites the executable pattern or folder, the + side conditions, the field-registry assumptions, and the exact theorem layer. +- No public claim relies on a ring identity without tying it to the compiler + operation that actually runs. + +### Phase 16: Drop-In Readiness Review + +Deliverables: + +- Run the selected toolchain path on the full differential corpus and selected + benchmark workloads. +- Publish the final TCB and assumptions list. +- Decide whether the integration should remain a project-llzk fork feature, + land as an out-of-tree plugin, or be proposed upstream to LLZK maintainers. + +Exit criteria: + +- A reviewer can reproduce the replacement run from a clean checkout and see + exactly which evidence supports each claim. +- The rollback path to the C++ Felt dialect remains documented and tested. + +## Certificate Route Assessment + +Proof certificates are useful only where they validate runtime behavior that +actually occurs in the replacement path. They add assurance by checking every +covered rewrite event against a small structural contract. They do not prove +complete compiler equivalence, they do not cover operations without certs, and +they do not replace differential coverage. + +The initial certificate proof of concept should therefore stay narrow: + +- choose one aligned fold whose C++ and VEIR behavior already agree, preferably + `constant_fold_add`; +- implement the real MLIR matcher and listener; +- demonstrate one accepted good rewrite and one rejected bad rewrite; +- document the extra trusted code introduced by the checker. + +If the prototype is clear and small, expand to the rest of the C++-parity +folders. If it becomes large or ambiguous, continue with differential coverage +and value-level proofs instead of forcing Strategy E into the critical path. + +## Trusted Base And Assumptions + +Current trusted components: + +- Accepted LLZK Felt source at `db922857bc5a88a9107627ef6b36a8b5e57bc5c2`, + including `Ops.td`, `Ops.cpp`, `FeltFoldTests.cpp`, and `Field.cpp`. +- Accepted VEIR pin `d899d95004d4bd988c8456d686c33b11a7a5eb4a` for current + llzk-lean evidence. +- Lean kernel, imported Mathlib facts, and any axioms reported by + `#print axioms`. +- VEIR's IR model, parser/printer, verifier, pass manager, pattern rewriter, + and defensive runtime guards. +- The differential normalizer and its documented cosmetic rewrites. +- The selected `llzk-opt` binary and LLVM/MLIR toolchain used for evidence. +- For Strategy E, the C++ JSON parser, cert loader, matcher, listener wiring, + schema policy, and MLIR APIs. + +Assumptions to keep explicit: + +- The LLZK source commit is the behavioral ground truth until the accepted + source pin moves. +- Field names and primes must match the accepted LLZK registry. +- Bare or unknown Felt fields are not interpreted as concrete field elements. +- Differential equality is observational evidence over the selected corpus, not + a proof for all programs. +- Value-level proofs justify runtime values under stated side conditions; they + are not automatically whole-program semantic preservation theorems. diff --git a/docs/future-c-drop-in.md b/docs/future-c-drop-in.md index 5e45c45..8c8bc39 100644 --- a/docs/future-c-drop-in.md +++ b/docs/future-c-drop-in.md @@ -1,4 +1,9 @@ -# Strategy C — Full replacement of llzk-opt (future, dialect-narrow does not apply) +# Strategy C — Full replacement of llzk-opt (future, LLZK-wide) + +For the active Felt-only drop-in goal, see +[`drop-in-roadmap.md`](drop-in-roadmap.md). This Strategy C document is about +replacing the entire `llzk-opt` binary and all dialect/backend surfaces, not the +narrower Felt dialect replacement path. ## Concrete picture @@ -33,10 +38,11 @@ Everything LLZK does, but in Lean. Independent of LLZK going forward. MLIR-text exchange format the existing C++ backends parse (~3-4 months each backend, conservatively, without verification). -**Felt-only**: doesn't apply at the dialect level. You can't binary- -replace one dialect — the surrounding tool wants the dialect's C++ -headers. The dialect-narrow equivalent of "replacement" is Strategy D -or B applied to that dialect. +**Felt-only**: does not mean replacing the `llzk-opt` binary. The practical +Felt-only target is a replacement path for the Felt dialect implementation and +Felt-affecting canonicalization/folding behavior, with explicit integration +through a wrapper, plugin, or upstream pass. That path is now tracked in the +drop-in roadmap. ## Why this is documented, not pursued diff --git a/docs/harness/SOURCES.md b/docs/harness/SOURCES.md index ef16e61..7c24458 100644 --- a/docs/harness/SOURCES.md +++ b/docs/harness/SOURCES.md @@ -30,6 +30,11 @@ Last reviewed: 2026-06-10 | `docs/phases/PHASE-06-strategy-a-divergence-burndown.md` | local file, 2026-06-10 | Completed Phase 6 divergence burn-down objective, artifacts, gates, and done criteria | | `docs/phases/PHASE-07-strategy-a-modular-reduction.md` | local file, 2026-06-10 | Completed Phase 7 registered-field modular-reduction objective, artifacts, gates, and done criteria | | `docs/phases/PHASE-08-strategy-a-field-preconditions.md` | local file, 2026-06-10 | Active Phase 8 field-precondition objective, artifacts, gates, and done criteria | +| `docs/drop-in-roadmap.md` | local file, 2026-06-11 | Planning baseline for the Felt drop-in replacement objective; not phase acceptance evidence | +| `docs/phases/PHASE-09-drop-in-roadmap.md` | local file, 2026-06-11 | Completed roadmap and claim-reset planning phase; not implementation acceptance evidence | +| `docs/phases/PHASE-10-toolchain-replacement-spike.md` | local file, 2026-06-11 | Phase 10 bootstrap plan for the external-driver toolchain spike; not Phase 8 acceptance evidence | +| `scripts/harness/phase10-toolchain-smoke.sh` | local file, 2026-06-11 | Phase 10 bootstrap smoke for the lower-first external-driver replacement path; not clean-pin acceptance evidence by itself | +| Phase 10 toolchain smoke evidence | `reviews/PHASE-10/evidence/toolchain-smoke.md` | Bootstrap workspace evidence for the external-driver path and Felt side-effect/DCE fix; not Phase 8 acceptance evidence | | `differential/run-differential.sh` | local file, 2026-06-09 | llzk-lean corpus wrapper around the consumed VeIR diff script | | `differential/corpus/` | local files, 2026-06-09 | Current Strategy A corpus and expected-divergence classification | | Consumed VeIR `scripts/llzk-diff.sh` | `.lake/packages/VeIR/scripts/llzk-diff.sh` at accepted pin | Default clean dependency driver with canonicalization support; Phase 6 canonical mode runs `felt-combine,dce`, the accepted Phase 7 pin includes registered-field fold-result reduction, and the accepted Phase 8 pin skips folds whose field name does not resolve | diff --git a/docs/phases/PHASE-09-drop-in-roadmap.md b/docs/phases/PHASE-09-drop-in-roadmap.md new file mode 100644 index 0000000..e30f58e --- /dev/null +++ b/docs/phases/PHASE-09-drop-in-roadmap.md @@ -0,0 +1,70 @@ +# Phase 9: Drop-In Roadmap And Claim Reset + +Status: completed; superseded by Phase 10 bootstrap +Last reviewed: 2026-06-11 +Repository: llzk-lean +Companion phase file: ../../../veir/docs/phases/PHASE-09-drop-in-roadmap.md + +## Objective + +Turn the post-Phase-8 state into a single drop-in replacement roadmap with +clear claims, repository responsibilities, profile boundaries, assumptions, +and trusted-base caveats. + +This phase is documentation and planning work. It does not claim new Felt +operation coverage, new runtime certificate coverage, or a new accepted +differential baseline. + +## Starting State + +- llzk-lean HEAD at bootstrap: + `aa0ceebf6952cd7027d889b5184dba4061687960`. +- Workspace VeIR HEAD at bootstrap: + `42db1ae3cbe76ca6c917501acc8e92a4f01cbc75`. +- `project-llzk/veir#1` is merged into `main` at merge commit + `45d31a20b4ff10498f7caba3c8b635553cc93dea`. +- `opencompl/veir#829` is closed unmerged. +- Phase 8 remains the last completed implementation milestone. +- The clean-pin canonical corpus remains + `21 pass (incl. expected-diverge), 0 fail`. + +## Claim Reset + +- The active goal is a high-assurance replacement for the C++ LLZK Felt + dialect path, not a full `llzk-opt` binary replacement. +- C++ parity is the adoption and debugging baseline. +- Enhanced VEIR is the improvement path. It may intentionally differ from C++ + LLZK when the difference is reviewed, covered, semantically justified, and + downstream-compatible. +- Arithmetic identities are supporting lemmas only. Runtime claims must cite + executable matchers, side conditions, result constructors, field registry + behavior, and concrete runtime values. + +## Non-Goals + +- Do not mark Phase 9 as a new implementation acceptance phase. +- Do not update the clean VEIR dependency pin. +- Do not reclassify any `EXPECTED-DIVERGE` corpus case. +- Do not claim that the certificate route proves compiler equivalence. + +## Artifacts Created Or Updated + +- `docs/drop-in-roadmap.md`: canonical project-wide roadmap. +- `README.md` and `docs/README.md`: pointers to the roadmap. +- `docs/future-c-drop-in.md`: clarified as full `llzk-opt` replacement, not + the current Felt-only target. +- `docs/strategy-e-certificates.md`: updated current proof-basis language. +- `docs/harness/SOURCES.md`: records the roadmap as planning context, not + phase acceptance evidence. + +## Gates + +- Existing Phase 8 freshness gate must still pass unchanged. +- No new Phase 9 implementation gate exists. + +## Done Criteria + +- Both repos point to the roadmap. +- Profile policy distinguishes C++ parity from enhanced VEIR improvements. +- Public docs state the current non-claims and trusted-base assumptions. +- Phase 10 has a concrete bootstrap target. diff --git a/docs/phases/PHASE-10-toolchain-replacement-spike.md b/docs/phases/PHASE-10-toolchain-replacement-spike.md new file mode 100644 index 0000000..b6b534b --- /dev/null +++ b/docs/phases/PHASE-10-toolchain-replacement-spike.md @@ -0,0 +1,98 @@ +# Phase 10: Toolchain Replacement Spike + +Status: bootstrap; not harness-active +Last reviewed: 2026-06-11 +Repository: llzk-lean +Companion phase file: ../../../veir/docs/phases/PHASE-10-toolchain-replacement-spike.md + +## Objective + +Select and exercise the first executable replacement path for the Felt +drop-in effort, while preserving the distinction between the C++-parity +profile and the enhanced VEIR profile. + +The first spike is an external-driver path. LLZK still owns custom-assembly +parsing and lowering to generic MLIR; VEIR owns the Felt canonicalization pass +under test; LLZK remains the comparison oracle for the C++ path. + +## Starting State + +- Phase 8 is the last accepted implementation milestone. +- Phase 9 completed the roadmap and claim reset. +- The differential wrapper already lowers `.llzk` inputs with + `llzk-opt --mlir-print-op-generic` before invoking VEIR. +- The canonical comparison path currently runs: + - C++ LLZK: `llzk-opt --canonicalize --mlir-print-op-generic`; + - VEIR: `veir-opt -p=felt-combine,dce`. +- The current VEIR path is the enhanced profile. A C++-parity profile still + needs to be implemented or configured in VEIR. + +## Profile Policy + +- **C++-parity profile:** adoption baseline. Divergences from C++ LLZK block + this profile unless explicitly disabled or fixed. +- **Enhanced VEIR profile:** improvement path. Divergences from C++ LLZK may + be accepted only with differential evidence, executable semantic claims, and + downstream compatibility review. + +Phase 10 should not treat the stronger current `felt-combine` behavior as a +problem by default. It should classify each difference as either a parity +blocker or an enhanced-profile candidate. + +## Non-Goals + +- Do not claim full Felt semantic parity. +- Do not claim replacement of the whole `llzk-opt` binary. +- Do not make the certificate route critical-path until the + `constant_fold_add` prototype proves useful. +- Do not reclassify expected divergences without exact evidence and review. + +## Artifacts To Create Or Update + +- `scripts/harness/phase10-toolchain-smoke.sh`: one-command smoke for the + external-driver spike. +- `docs/drop-in-roadmap.md`: roadmap and profile policy. +- `docs/harness/SOURCES.md`: Phase 10 bootstrap source rows. +- Phase 10 evidence under `reviews/PHASE-10/evidence/` once smoke runs are + recorded. + +## Gates To Implement + +- Toolchain smoke: + `scripts/harness/phase10-toolchain-smoke.sh`. +- Existing Phase 8 freshness: + `scripts/harness/check-doc-freshness.sh`. +- Targeted VEIR proof build after proof/doc edits: + `lake build Veir.Passes.Felt.Proofs` from the VEIR repository. + +## Bootstrap Execution + +The first Phase 10 smoke run exposed a workspace VEIR regression relative to +the accepted clean pin: after the upstream DCE side-effect API change, Felt +operations were conservatively treated as side-effecting, so +`veir-opt -p=felt-combine,dce` folded `registered_add_fold.llzk` but did not +erase the now-dead input constants. The clean dependency pin still passed. + +The bootstrap fix is in VeIR `Veir/GlobalOpInfo.lean`: Felt operations are now +classified as side-effect-free for DCE. After rebuilding workspace `veir-opt`, +`scripts/harness/phase10-toolchain-smoke.sh` passes over the aligned fold and +no-fire precondition cases. + +## Review Requirements + +- Record exactly which command owns parsing, lowering, canonicalization, and + printing. +- Identify whether the smoke exercised the clean dependency pin or workspace + VEIR. +- Mark each observed divergence as parity blocker, enhanced-profile candidate, + or unrelated tooling issue. + +## Done Criteria + +- One command runs the external-driver smoke over LLZK custom assembly and + reports comparable output for both paths. +- The first VEIR implementation task is precise: add/configure the parity + profile, or promote a named current divergence into the enhanced profile + through review. +- Phase 10 evidence remains separate from Phase 8 acceptance evidence until + the harness gates are deliberately advanced. diff --git a/docs/strategy-e-certificates.md b/docs/strategy-e-certificates.md index aa0d176..a3c1569 100644 --- a/docs/strategy-e-certificates.md +++ b/docs/strategy-e-certificates.md @@ -21,7 +21,7 @@ pattern: identifier, LHS shape, RHS shape, side conditions, and the name of the Lean theorem that justifies it. The current certificate proof basis is pinned to VEIR commit -`d4cc1bf2d31beeca17eb2e8c9c7181d04af013a3` from +`d899d95004d4bd988c8456d686c33b11a7a5eb4a` from `project-llzk/veir`. Under that pin, the Lean catalog scan still finds 15 Felt pattern definitions, with 2 covered by the hand-authored certificate catalog and 13 reported as uncovered. The pin gate is a diff --git a/reviews/PHASE-10/evidence/README.md b/reviews/PHASE-10/evidence/README.md new file mode 100644 index 0000000..d63ba4e --- /dev/null +++ b/reviews/PHASE-10/evidence/README.md @@ -0,0 +1,5 @@ +# Phase 10 Evidence + +This directory records bootstrap evidence for the Phase 10 toolchain +replacement spike. It is not Phase 8 acceptance evidence and does not update +the clean dependency pin. diff --git a/reviews/PHASE-10/evidence/toolchain-smoke.md b/reviews/PHASE-10/evidence/toolchain-smoke.md new file mode 100644 index 0000000..eccb921 --- /dev/null +++ b/reviews/PHASE-10/evidence/toolchain-smoke.md @@ -0,0 +1,42 @@ +# Phase 10 Toolchain Smoke + +Date: 2026-06-11 + +Command: + +```bash +scripts/harness/phase10-toolchain-smoke.sh +``` + +Tool ownership recorded by the smoke: + +- Lowering owner: `llzk-opt --mlir-print-op-generic`. +- C++ canonical path: `llzk-opt --canonicalize --mlir-print-op-generic`. +- VEIR canonical path: `veir-opt -p=felt-combine,dce`. +- Current profile under smoke: enhanced VEIR `felt-combine,dce`. + +Initial finding: + +- The workspace VEIR path diverged on + `differential/corpus/felt/registered_add_fold.llzk`: `felt-combine` folded + the add, but DCE did not erase the now-dead input constants. +- The clean pinned dependency passed the same input, so this was a workspace + regression relative to the accepted Phase 8 proof basis. +- Root cause: after the upstream DCE side-effect API change, Felt operations + were not listed as pure and defaulted to side-effecting. + +Fix: + +- `Veir/GlobalOpInfo.lean` now marks `.felt _` as side-effect-free for DCE. +- The smoke wrapper refreshes workspace `veir-opt` before using the neighboring + VEIR checkout. + +Final result: + +```text +WORKSPACE-VEIR-OPT: lake build veir-opt succeeded for /home/alh/LLZK/veir +SMOKE-PASS: parse-print aligned fold: differential/corpus/felt/registered_add_fold.llzk +SMOKE-PASS: canonical aligned fold: differential/corpus/felt/registered_add_fold.llzk +SMOKE-PASS: parse-print no-fire precondition: differential/corpus/felt/unspecified_add_fold.llzk +SMOKE-PASS: canonical no-fire precondition: differential/corpus/felt/unspecified_add_fold.llzk +``` diff --git a/scripts/harness/phase10-toolchain-smoke.sh b/scripts/harness/phase10-toolchain-smoke.sh new file mode 100755 index 0000000..0822d4e --- /dev/null +++ b/scripts/harness/phase10-toolchain-smoke.sh @@ -0,0 +1,77 @@ +#!/usr/bin/env bash +# Phase 10 bootstrap smoke for the external-driver Felt replacement path. +# +# This is not acceptance evidence by itself. It records the first executable +# shape: LLZK lowers custom assembly to generic MLIR, then LLZK and VEIR run +# comparable parse/print and canonicalization paths over that same input. + +set -uo pipefail + +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)" +DEFAULT_LLZK_OPT="/nix/store/awcw2wiypa02sl5vx4xm06qwji68xz3h-llzk-debug-2.0.0/bin/llzk-opt" +WORKSPACE_VEIR_DIR="" +if [[ -d "${ROOT}/../veir" ]]; then + WORKSPACE_VEIR_DIR="$(cd "${ROOT}/../veir" && pwd)" +fi +STATUS=0 + +if [[ -z "${LLZK_OPT:-}" && -x "${DEFAULT_LLZK_OPT}" ]]; then + export LLZK_OPT="${DEFAULT_LLZK_OPT}" +fi + +if [[ -z "${LLZK_OPT:-}" ]]; then + echo "ERROR: LLZK_OPT is unset and the accepted default llzk-opt was not found." >&2 + echo "Set LLZK_OPT=/path/to/llzk-opt and rerun." >&2 + exit 2 +fi + +if [[ -z "${VEIR_DIFF:-}" && -n "${WORKSPACE_VEIR_DIR}" && + -x "${WORKSPACE_VEIR_DIR}/scripts/llzk-diff.sh" ]]; then + export VEIR_DIFF="${WORKSPACE_VEIR_DIR}/scripts/llzk-diff.sh" +fi + +if [[ -n "${WORKSPACE_VEIR_DIR}" && + "${VEIR_DIFF:-}" == "${WORKSPACE_VEIR_DIR}/scripts/llzk-diff.sh" && + -z "${VEIR_OPT:-}" ]]; then + build_log="$(mktemp -t phase10-veir-opt-build-XXXXXX)" || exit 2 + if (cd "${WORKSPACE_VEIR_DIR}" && lake build veir-opt >"${build_log}" 2>&1); then + rm -f "${build_log}" + else + echo "ERROR: failed to refresh workspace veir-opt with 'lake build veir-opt'" >&2 + sed 's/^/ /' "${build_log}" >&2 + rm -f "${build_log}" + exit 2 + fi + export VEIR_OPT="${WORKSPACE_VEIR_DIR}/.lake/build/bin/veir-opt" + echo "WORKSPACE-VEIR-OPT: lake build veir-opt succeeded for ${WORKSPACE_VEIR_DIR}" +fi + +run_case() { + local label="$1" + local input="$2" + shift 2 + + echo + echo "== ${label}: ${input} ==" + if "${ROOT}/differential/run-differential.sh" "$@" "${ROOT}/${input}"; then + echo "SMOKE-PASS: ${label}: ${input}" + else + echo "SMOKE-FAIL: ${label}: ${input}" >&2 + STATUS=1 + fi +} + +echo "Phase 10 external-driver smoke" +echo "LLZK_OPT=${LLZK_OPT}" +echo "VEIR_DIFF=${VEIR_DIFF:-}" +echo "lowering owner: llzk-opt --mlir-print-op-generic" +echo "C++ canonical path: llzk-opt --canonicalize --mlir-print-op-generic" +echo "VEIR canonical path: veir-opt -p=felt-combine,dce" +echo "current profile under smoke: enhanced VEIR felt-combine,dce" + +run_case "parse-print aligned fold" "differential/corpus/felt/registered_add_fold.llzk" +run_case "canonical aligned fold" "differential/corpus/felt/registered_add_fold.llzk" --canonicalize +run_case "parse-print no-fire precondition" "differential/corpus/felt/unspecified_add_fold.llzk" +run_case "canonical no-fire precondition" "differential/corpus/felt/unspecified_add_fold.llzk" --canonicalize + +exit "${STATUS}"