Skip to content

Commit 6f4c068

Browse files
alexanderlhicksalexanderlhicks
committed
Document Felt drop-in roadmap and Phase 10 bootstrap
1 parent 42db1ae commit 6f4c068

7 files changed

Lines changed: 213 additions & 6 deletions

File tree

‎README.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,12 @@ This verifies that llzk-lean's Lake metadata uses the accepted
3232
`project-llzk/veir` remote, that `rev` and `inputRev` identify the accepted
3333
commit, and that `.lake/packages/VeIR` is clean at that commit.
3434

35+
The Felt drop-in replacement plan is tracked in
36+
[`docs/drop-in-roadmap.md`](docs/drop-in-roadmap.md), with the project-wide
37+
roadmap in the companion llzk-lean checkout at
38+
`../llzk-lean/docs/drop-in-roadmap.md`.
39+
Phase 9 and Phase 10 planning files live under [`docs/phases/`](docs/phases/).
40+
3541
| VeIR Features | Complete | Verified |
3642
|-------------------------------------------------------|------------| ---------|
3743
| MLIR core data structures (block, operation, region) | ✅ | 🔒 |

‎Veir/GlobalOpInfo.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -444,7 +444,7 @@ def OperationPtr.hasSideEffects (op : OperationPtr) (ctx : IRContext OpCode) : B
444444
if opCode.isTerminator then true else
445445
match opCode with
446446
-- These dialects are pure
447-
| .arith _ | .comb _ | .mod_arith _ | .datapath _ => false
447+
| .arith _ | .comb _ | .mod_arith _ | .datapath _ | .felt _ => false
448448
| .builtin .unrealized_conversion_cast => false
449449
| .hw .constant => false
450450
-- RISC-V is pure register arithmetic except the memory ops

‎Veir/Passes/Felt/Proofs.lean‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,11 +5,10 @@ import Veir.Data.Felt.Basic
55
66
Each pattern in `Combine.lean` is paired with an algebraic identity
77
here, proven over `Felt p := ZMod p`. This file proves the *arithmetic
8-
identity only*; it does NOT prove that the IR rewrite preserves program
9-
semantics or well-formedness. The pass-side rewriter preconditions are
10-
discharged with `sorry` in `Combine.lean`, so the bar this file clears
11-
is the algebraic theorem, not the transformation. See `REVIEW.md`
12-
(finding VC2) for the full trust-boundary writeup.
8+
identity only*. The executable rewrite preconditions are discharged in
9+
`Veir/Passes/Felt/RewriteLemmas.lean`, but that still establishes IR
10+
well-formedness of the rewrite, not whole-program semantic preservation.
11+
See `REVIEW.md` and `FOLLOWUP.md` for the current trust-boundary writeup.
1312
1413
Phase E.5 (2026-05-19) upgraded the proof model from `abbrev Felt
1514
:= Int` to `abbrev Felt p := ZMod p`. Each theorem now universally

‎docs/drop-in-roadmap.md‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
# VeIR Felt Drop-In Roadmap Role
2+
3+
Last reviewed: 2026-06-11
4+
5+
This repo is the implementation side of the Felt drop-in replacement effort.
6+
The project-wide roadmap lives in the companion repository at
7+
`../llzk-lean/docs/drop-in-roadmap.md` in the shared workspace.
8+
9+
## Current Role
10+
11+
VEIR currently provides:
12+
13+
- LLZK Felt IR representation, parser/printer support, verifier shape checks,
14+
and the `felt-combine` pass.
15+
- Fifteen Felt rewrite patterns over `const`, `add`, `sub`, `mul`, and `neg`.
16+
- Lean arithmetic proofs and sorry-free structural rewrite precondition proofs
17+
for those 15 patterns.
18+
- A standalone value-level Felt interpreter proof-of-concept in
19+
`Veir/Passes/Felt/InterpModel.lean`.
20+
- The differential driver `scripts/llzk-diff.sh`, consumed by llzk-lean's
21+
clean-pin harness.
22+
23+
VEIR does not yet provide a complete drop-in Felt replacement:
24+
25+
- 13 accepted LLZK Felt operations still lack semantic models and interpreter
26+
cases in VEIR.
27+
- The current `felt-combine` pass includes verified algebraic rewrites that the
28+
C++ LLZK canonicalizer does not perform. Those are useful verified
29+
optimizations, but they must be separated from the C++-parity adoption
30+
profile.
31+
- There is no whole-program rewrite semantic theorem.
32+
- There is no direct `llzk-opt` replacement integration point.
33+
34+
## Replacement Profiles
35+
36+
VEIR should expose two Felt profiles for the drop-in work:
37+
38+
- **C++-parity profile.** Adoption and regression baseline. This profile should
39+
match the accepted LLZK C++ folder/canonicalization behavior as closely as
40+
possible so users can opt in, compare, and fall back cleanly.
41+
- **Enhanced VEIR profile.** Improvement path. This profile may run additional
42+
verified rewrites from `felt-combine`, but every intentional divergence from
43+
C++ LLZK must have differential evidence, executable side conditions,
44+
semantic justification, and downstream compatibility review.
45+
46+
The current nonconstant algebraic divergences are not automatically defects.
47+
They are blockers only for the parity profile. They become compelling
48+
enhanced-profile features only after their runtime semantics and replacement
49+
toolchain behavior are tied down.
50+
51+
## VeIR Work Required For Drop-In
52+
53+
1. **Add profile separation.** Keep `felt-combine` as the stronger verified
54+
optimization pass, but add or configure a C++-parity profile that matches
55+
the C++ Felt folder behavior first.
56+
2. **Port the missing folder semantics.** Implement the C++ fold behavior for
57+
`pow`, `div`, `uintdiv`, `sintdiv`, `umod`, `smod`, `inv`, `bit_and`,
58+
`bit_or`, `bit_xor`, `bit_not`, `shl`, and `shr`, including no-fold side
59+
conditions.
60+
3. **Model runtime side conditions.** Field registry lookup, registered-field
61+
preconditions, signed representative conversion, bitwidth, division by zero,
62+
and `NotFieldNative` scope must be executable conditions, not prose.
63+
4. **Attach auditable rewrite metadata.** If Strategy E continues, certificate
64+
shapes and side conditions should be derived from or colocated with the
65+
executable patterns so llzk-lean does not hand-maintain a parallel catalog.
66+
5. **Strengthen semantic statements.** Arithmetic identities in
67+
`Veir/Passes/Felt/Proofs.lean` are supporting lemmas. Drop-in claims need
68+
value-level runtime lemmas tied to the operations, matchers, result
69+
constructors, and side conditions that actually run.
70+
71+
## Non-Claims
72+
73+
The current VeIR fork does not claim:
74+
75+
- full LLZK Felt semantic parity;
76+
- complete coverage of all C++ Felt folders;
77+
- runtime LLZK rewrite verification;
78+
- replacement of all of `llzk-opt`;
79+
- whole-program semantic preservation for `felt-combine`.
80+
81+
Those claims become available only through the roadmap gates in the companion
82+
`llzk-lean` document.

‎docs/harness/SOURCES.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,10 @@ Last reviewed: 2026-06-10
3030
| `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 |
3131
| `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 |
3232
| `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 |
33+
| `docs/drop-in-roadmap.md` | local file, 2026-06-11 | VeIR-side planning baseline for the Felt drop-in replacement objective; not phase acceptance evidence |
34+
| `docs/phases/PHASE-09-drop-in-roadmap.md` | local file, 2026-06-11 | Completed roadmap and claim-reset planning phase; not implementation acceptance evidence |
35+
| `docs/phases/PHASE-10-toolchain-replacement-spike.md` | local file, 2026-06-11 | Phase 10 bootstrap plan for profile separation and the external-driver toolchain spike; not Phase 8 acceptance evidence |
36+
| `Veir/GlobalOpInfo.lean` | local file, 2026-06-11 | Phase 10 side-effect metadata fix: Felt operations are pure for DCE so `felt-combine,dce` can erase unused Felt constants/arithmetic |
3337
| `scripts/llzk-diff.sh` | local file, 2026-06-10 | VeIR side LLZK/VeIR differential driver; supports parse/print mode and Phase 6 `felt-combine,dce` canonicalization mode |
3438
| Companion `llzk-lean/differential/run-differential.sh` | local file, 2026-06-09 | Corpus wrapper around the consumed VeIR diff script |
3539
| Companion `llzk-lean/differential/corpus/` | local files, 2026-06-09 | Current Strategy A corpus and expected-divergence classification |

‎docs/phases/PHASE-09-drop-in-roadmap.md‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
# Phase 9: Drop-In Roadmap And Claim Reset
2+
3+
Status: completed; superseded by Phase 10 bootstrap
4+
Last reviewed: 2026-06-11
5+
Repository: veir
6+
Companion phase file: ../../../llzk-lean/docs/phases/PHASE-09-drop-in-roadmap.md
7+
8+
## Objective
9+
10+
Align the VeIR implementation-side claims with the project-wide Felt drop-in
11+
roadmap after Phase 8 landed in the `project-llzk/veir` fork.
12+
13+
## Starting State
14+
15+
- Workspace VeIR HEAD at bootstrap:
16+
`42db1ae3cbe76ca6c917501acc8e92a4f01cbc75`.
17+
- `project-llzk/veir#1` is merged into `main` at merge commit
18+
`45d31a20b4ff10498f7caba3c8b635553cc93dea`.
19+
- `opencompl/veir#829` is closed unmerged.
20+
- VEIR has 15 Felt rewrite patterns over `const`, `add`, `sub`, `mul`, and
21+
`neg`.
22+
- VEIR does not yet expose a separate C++-parity Felt profile.
23+
24+
## Claim Reset
25+
26+
- Current `felt-combine` is the enhanced VEIR profile seed.
27+
- A separate C++-parity profile is needed for low-risk adoption and debugging.
28+
- Current nonconstant algebraic divergences are parity blockers, but may become
29+
enhanced-profile features if semantic and downstream claims are established.
30+
- Arithmetic identities in `Veir/Passes/Felt/Proofs.lean` are supporting
31+
lemmas, not whole-program semantic-preservation claims.
32+
33+
## Non-Goals
34+
35+
- Do not claim complete LLZK Felt semantic parity.
36+
- Do not claim whole-program semantic preservation for `felt-combine`.
37+
- Do not replace all of `llzk-opt`.
38+
39+
## Artifacts Created Or Updated
40+
41+
- `docs/drop-in-roadmap.md`: VeIR-side role in the project-wide roadmap.
42+
- `README.md`: pointer to the roadmap.
43+
- `Veir/Passes/Felt/Proofs.lean`: proof-boundary comment corrected.
44+
- `docs/harness/SOURCES.md`: records the roadmap as planning context, not
45+
phase acceptance evidence.
46+
47+
## Done Criteria
48+
49+
- VEIR docs distinguish C++ parity from enhanced VEIR improvements.
50+
- VEIR docs state current non-claims.
51+
- Phase 10 has a concrete implementation-side target.

‎docs/phases/PHASE-10-toolchain-replacement-spike.md‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
# Phase 10: Toolchain Replacement Spike
2+
3+
Status: bootstrap; not harness-active
4+
Last reviewed: 2026-06-11
5+
Repository: veir
6+
Companion phase file: ../../../llzk-lean/docs/phases/PHASE-10-toolchain-replacement-spike.md
7+
8+
## Objective
9+
10+
Support the first executable Felt replacement spike and define the VEIR pass
11+
surface needed for both the C++-parity profile and the enhanced VEIR profile.
12+
13+
## Starting State
14+
15+
- The current external-driver smoke uses `scripts/llzk-diff.sh`.
16+
- `.llzk` custom assembly is lowered through LLZK before VEIR runs.
17+
- Canonical smoke currently exercises `veir-opt -p=felt-combine,dce`.
18+
- `felt-combine` is stronger than the C++ LLZK canonicalizer for current
19+
nonconstant algebraic rewrites.
20+
21+
## Required Implementation Direction
22+
23+
- Add or configure a C++-parity Felt profile that omits enhanced algebraic
24+
rewrites not performed by C++ LLZK.
25+
- Keep the enhanced `felt-combine` profile available as the improvement path.
26+
- Make profile selection explicit in scripts/docs so differential evidence
27+
states which profile was exercised.
28+
- Continue tying proof claims to executable rewrite conditions rather than to
29+
standalone arithmetic identities.
30+
31+
## Non-Goals
32+
33+
- Do not weaken the current enhanced `felt-combine` profile just to obtain
34+
parity.
35+
- Do not make undocumented output differences part of the replacement claim.
36+
- Do not claim parser/frontend replacement while LLZK still owns lowering.
37+
38+
## Gates To Implement
39+
40+
- llzk-lean Phase 10 smoke:
41+
`scripts/harness/phase10-toolchain-smoke.sh`.
42+
- Targeted proof build after proof/doc edits:
43+
`lake build Veir.Passes.Felt.Proofs`.
44+
- Later implementation gate: a profile-selectable `veir-opt` invocation whose
45+
parity mode avoids the current nonconstant algebraic expected divergences.
46+
47+
## Bootstrap Finding
48+
49+
The first llzk-lean Phase 10 smoke found that workspace VEIR, unlike the
50+
accepted llzk-lean clean pin, no longer removed dead Felt constants after
51+
`felt-combine` folded `registered_add_fold.llzk`. The cause was the newer DCE
52+
side-effect API: Felt operations were not listed as pure and therefore defaulted
53+
to side-effecting.
54+
55+
`Veir/GlobalOpInfo.lean` now marks `.felt _` as side-effect-free, which restores
56+
the expected `felt-combine,dce` behavior for Felt constants and arithmetic in
57+
the external-driver smoke.
58+
59+
## Done Criteria
60+
61+
- VEIR can be invoked in a documented Phase 10 smoke path.
62+
- The parity/enhanced profile split is represented in VEIR implementation or
63+
command-line configuration.
64+
- Any promoted enhanced-profile divergence has differential evidence,
65+
semantic justification, and downstream compatibility notes.

0 commit comments

Comments
 (0)