From 208cd983ebf13233baee79e81c30c302fa763f82 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 14 Oct 2026 11:51:30 +0200 Subject: [PATCH] notes by JP on implementing split proving --- .../0_input_for_3MI.md | 343 +++++++++++++ .../1_proposed_spec_text.md | 453 ++++++++++++++++++ 2 files changed, 796 insertions(+) create mode 100644 spec/notes/01-split-verification-impl/0_input_for_3MI.md create mode 100644 spec/notes/01-split-verification-impl/1_proposed_spec_text.md diff --git a/spec/notes/01-split-verification-impl/0_input_for_3MI.md b/spec/notes/01-split-verification-impl/0_input_for_3MI.md new file mode 100644 index 000000000..3f4cb1188 --- /dev/null +++ b/spec/notes/01-split-verification-impl/0_input_for_3MI.md @@ -0,0 +1,343 @@ +# Two VMs for recursion: what we built, what broke, and what we learned + +*Implementation of the 3MI Field VM (#971) and Recursion (#943) specifications, as merged on October 2. The work is closed; this document is meant as input for the spec. Proposed Typst text for the open sections is in `1_proposed_spec_text.md`.* + +## The short version + +We built the recursion the spec describes: +- the **Lambda VM (RISC-V)** runs the binary half, v_bin: hashing, Fiat–Shamir, Merkle paths and proof of work; +- the **Field VM** runs the field half, v_fld: constraints, composition, DEEP and FRI folds; +- both are **proven together in one proof**, bound by a pseudo-`PAGE`: the spec's *split verification*. + +It runs end to end, from an Ethereum block (a 10-transfer ethrex test block) to a uniform recursion tower at ~111 bits. + +Getting there meant three kinds of work: +- filling in several parts the spec leaves as TODO; +- changing a few things it states; +- closing soundness holes that only appear once the two halves really run apart. + +One finding sums up the design question: **in this two-VM design, the field VM is not the bottleneck; the binary VM is.** +- The Field VM next to algebraic hash chips verifies an epoch proof as fast as a dedicated recursion machine. +- With the hashes on RISC-V, as the spec places them, the same work is ~25× slower. + +The document is in three parts: +- **Part I** follows the spec as written; +- **Part II** covers what the spec leaves as TODO and how we made it work; +- **Part III** covers the experimental branches: a binary-field prover for the hash half, *split proving* across proof systems with Flock (the section the spec leaves as TODO), and BLAKE3. + +A word on names. Lambda's own recursion machine is the **LFM** (Lambda Field Machine): one machine with write-once memory and its own RPX hash chips. It is the baseline throughout. In the implementation it is also the language in which the verifier is first written before being cut into the two halves. + +--- + +## Part I — Following the spec + +### 1. The Field VM on its own + +The first step was the Field VM as written: +- the single `FMA d == a·b + c` instruction over the cubic extension of Goldilocks; +- registers `ZERO`, `PC` and N general-purpose ones; +- both addressing modes; +- input and output hinting; +- the halt self-loop at PC 0, with execution starting at PC 1. + +Assembler, executor, AIR and prover follow the text closely. + +A few pieces the spec does not define had to be decided along the way (the `MEM` table, how it is bound to the statement, hint values). Part II describes them. + +One change was needed in our own framework. The out-mux reads the next row's registers, and the framework only opened the LogUp accumulator at the next row. Every other next-row read was silently checked against zero until those columns were opened as well. + +### 2. Running a real verifier on it + +The next step was real work: the field half of verifying one epoch proof of the Lambda VM, with RPX as the hash. The existing epoch verifier was translated into Field VM programs, one FMA per field operation, with inversions as hints that the FMA checks. + +The first version used 11× the cells of the same arithmetic in the LFM. The gap was structural: +- the explicit `MEM` table; +- per-row decoding; +- every argument being an extension element. + +An optimization campaign closed most of it, taking proving from 9.6 s to 4.5 s (2.8 s with degree 3 at blowup 2) and the gap from ~11× to ~3×: +- N = 2 registers instead of 5, since generated code works through memory; +- chained power-of-two segments instead of one padded table; +- a chunked `DECODE`; +- operand fusion. + +Two ideas did not pay off: a register-free row variant (only 13% of rows could use it) and a third memory argument. + +### 3. The hash half: where the trouble started + +The field half is half the verifier. Two versions of the hash half were built: +- **Option A, not the spec:** the Field VM plus the LFM's RPX hash chips in one proof. It proves an epoch's verification **on par with the LFM itself** (within ±1% over 10 interleaved runs). +- **Option B, the spec:** the Field VM plus a RISC-V program for the hash half. The first version was not viable: a software RPX permutation costs ~73,000 RISC-V cycles, and one production epoch needs 82,323 of them. That is 6.07 G cycles and an extrapolated ~24 h of proving, about 11,000× the LFM. + +Making option B usable took two changes: +- an **RPX precompile** in the Lambda VM; +- replacing the interpreter that ran the cut program with **native code compiled for each proof shape**. In the binary half, the precompile and the compiled code brought the cost to 55–85 cycles per hash. + +Option B then verified an epoch in ~199 s, still about 25× the LFM, while option A stayed at parity. That gap never went away, and it is the main design lesson below. + +### 4. Recursion: the tower that would not shrink + +The Recursion chapter defines `verify*`. It was built as described: +- one program holding the base verifier and the recursive verifier, both run at every level; +- every assertion of the first multiplied by 1 − b and every one of the second by b, with b² = b asserted ungated; +- `comm(x)` committing to the base instance and `comm(y)` to the program. + +Each level is a single proof containing both VMs, as the spec's split verification describes; how the two VMs share data is in Part II. + +**It did not converge.** Verifying one epoch cost 337× the epoch's own cycles, so every level was bigger than the one it verified. What brought it below 1×: + +| Change | Cost of verifying one epoch | +|---|---:| +| Starting point: one Merkle tree and one FRI per table, interpreted v_bin | 337× | +| Native compiled v_bin | 35.5× | +| One Merkle tree per phase over all trace tables, and one FRI | 11.5× | +| No keccak tables in the recursive guest (they were 26% of all hash permutations) | 2.38× | +| Epochs of 2²³ cycles | **0.615×** | + +Two of these deserve a comment: +- **Sharding.** Sharding tables made the cost grow with the epoch size, so a bigger epoch did not help until shards were gone. +- **Batched commitments depart from the spec,** which commits to every table individually (`recursion.typ:347–349`). Program tables (`DECODE`, `FIELD_VM_DECODE`, the address maps) keep their own trees, so the program identity is still a list of roots; trace tables share one tree per phase. The same change on a mainnet block gave −73% proof size and −75% verification time. + +Two more problems came from uniformity: +- **A straight-line verifier depends on the proof shape** (table heights, query counts), so its program id is constant only at a fixed point. The construction emits `verify'` for a shape, proves a level, emits again from that proof, and repeats until the id repeats. +- **Shapes that depend on data break that fixed point.** Three causes appeared: + - branches on query bits; + - the number of memory pages the guest touches; + - a multiplication table that deduplicates operands, while the inactive branch multiplied arbitrary values by its zero gate. + + Fixes: branch-free code; reused guest memory; multiplying by the gate with a mask. + +The tower converged: three levels with one program id, at 7.96 M cycles at Q = 101 and grinding 28, and 7.69 M at Q = 110 once the program tables shared one preprocessed tree. (Q is the number of FRI queries. At blowup 4 each query adds about 2 bits of security and grinding adds its own bits, so Q = 110 with 20 bits of grinding gives ~128 bits, and Q = 80 with 32 bits gives ~111.) + +### 5. From an Ethereum block + +A tower needs a base. A block's proof is a bundle of epoch proofs plus a global proof, and both branches of `verify'` run at every level, so verifying the whole bundle inside `verify'` would make every level pay for it. Instead, an **anchor** program verifies the bundle once, and `verify'` with b = 0 verifies the anchor's proof. + +Two more spec issues showed up here: +- **The chapters disagree on the commitment domain.** The Recursion chapter backs stdout with `PAGE` tables (`recursion.typ:359–394`); the Memory chapter calls that domain unpaged, and the Streaming chapter forbids `PAGE` there. The implementation binds stdout through the COMMIT bus, whose term the verifier recomputes. +- **The node that verifies two proofs sets the security ceiling.** At Q = 80 it sits at 0.973 × 2²³; Q = 110 would need ~10.8 M cycles. + +End to end on `ethrex_10_transfers`, a 10-transfer test block from ethrex (CPU server with 96 cores): +- from the block to the first recursive proof, ~37 min; +- each further level, ~7.5 min; +- every level 8.16 M cycles and ~97 GB of memory, at ~111 bits; +- one program id at every level; the final verifier accepts level k and rejects k + 1. + +For comparison, the same tower with the LFM's hash chips instead of RISC-V (option A) proves a level in ~25–45 s with 15–29 GB, at Q = 110, end to end from a mainnet block. + +### What Part I says about the two-VM design + +Measured on the same CPU server, verifying the same epoch proof: + +| Field half | Hash half | Prove | +|---|---|---:| +| LFM | LFM (one machine) | ~8 s | +| **Field VM** | LFM's RPX chips | **on par** (±1%) | +| **Field VM** | **RISC-V**, as in the spec | **~199 s** (~25×) | + +In the tower the gap is ~10× per level, with ~4× the memory. + +**The Field VM is not the problem.** Inside a monolithic RISC-V verifier, field arithmetic is 70–80% of the cycles; DEEP reconstruction alone is 60–74%. Moving it to the Field VM is exactly right, and the Field VM handles it as well as a dedicated machine. + +What stays on RISC-V is expensive for reasons that have little to do with fields: +- hashing through a precompile; +- byte order: big-endian commitments cost ~300 cycles per Merkle level without a byte-reverse instruction; +- decoding the proof: 41% of a byte-native binary half; +- rebuilding table shapes: 24% of a byte-native binary half. + +**The binary half needs its own design.** Either: +- a hash, precompile ABI and encodings chosen for it (little-endian, bulk absorb, zero-copy proof access, shapes embedded in the verifier); or +- a spec that lets the hash half run on algebraic hash chips next to the Field VM. + +--- + +## Part II — About the TODOs + +These are the parts the spec leaves open or as TODO. Each one turned out to be needed for a sound proof that converges. + +### 6. Split verification in one proof: how the two VMs share data + +**Spec:** the Split verification section (`recursion.typ:145–239`) has the two halves share a record and be proven as one program. The input, private input and record "are made available to the VMs by means of `PAGE` tables" (`recursion.typ:345–346`), but nothing says how the Field VM reads them. (Proving the halves *separately* is split proving, the TODO at `recursion.typ:240`; that is Part III, §12.) + +**Options.** Robin pointed out that the side-by-side Field VM and Lambda VM case "can still be a single proof". For the shared data there were two proposals: +- one commitment serving as both the Field VM's `MEM` and the RISC-V memory initialization. The binary VM would then have to rebuild the field version of the whole input to check it; +- after Robin talked with Erik: an extension-field version for the Field VM and a byte version for the binary VM, in the same proof, bound through LogUp. + +**Taken:** the second, as a **pseudo-`PAGE`**: 24 bytes per cell, three little-endian limbs, mapped to Field VM addresses by a preprocessed `FADDR`, placed in page-aligned private-input pages. Two additions: +- **A second direction, `BACK`,** for values the binary half computes for the Field VM (challenges, query bits). The proposal covered only the shared input. +- **A constraint that each limb is below p.** Without it, the bytes of v + p pass as v; a test shows it. + +**What it surfaced.** Running both halves in one proof exposed soundness holes in our first implementation that nothing in the spec prevents. Each one was confirmed by a test that builds the forged proof: the proof was accepted before the fix and is rejected after it, which also shows the test is not vacuous. The holes: +- query bits decomposed from x + p instead of x, which picks different query positions for the same field element; +- the fourth lane of shared hints, of `BACK` cells and of published words left unchecked when a four-element RPX digest met a three-coordinate cell; +- program constants not bound; +- a hint the Field VM decomposed that the binary half never saw; +- the binary program's identity not bound; +- limbs encoded as v + p. + +### 7. The communication record + +**Spec:** the record "primarily consists of the Fiat–Shamir challenges", and the overview is left to "update once @verification is complete" (`recursion.typ:329–334`). + +**What we found.** The holes in §6 share a cause: **the record must contain every value one half assumes and the other produces, each with one enforced encoding.** Challenges alone are not enough. + +**Options.** Let the record be whatever the cut makes cross, or define it by meaning. + +**Taken:** first the cut, which gave tens of thousands of intermediate cells and tied both halves to one compiler. Then a record where only named values cross, in a layout computed from the proof shape alone: +- **from v_bin to v_fld:** the Fiat–Shamir challenges, in transcript order, and the query bits; +- **from v_fld to v_bin:** the register LDE and the statement words, which v_bin hashes. + +Values both halves can compute from the shared input are computed by both. The emitted verifier is checked against the layout every time it is built. + +On a Q = 80 level, 6,129 named cells cross instead of 32,220 cut-chosen ones, and the level costs 6.8% fewer cycles. This is what lets either half be rewritten or audited on its own. + +### 8. The verification chapter + +**Spec:** `verifier.typ` is a TODO ("sigma protocol, layout the various steps; Fiat–Shamir transformation"). + +**Taken:** one order of transcript steps, followed by both the native verifier and the in-VM one. The record in §7 is derived from it. The proposed text lists the steps. + +### 9. The level counter + +**Spec:** soundness of the construction "is not yet proven"; a recursion-level counter is suggested in an aside (`recursion.typ:131–137`). + +**Taken:** required. Each level publishes `level = 1 + b · level_child`, and the final verifier accepts level k and rejects k + 1. Ten tampers are rejected, among them b = 2, b flipped, wrong commitments, a forged child level and another program of the same shape. + +### 10. Field VM details + +**`MEM`.** The spec asks for "a committed table containing the memory as well as the multiplicities" (`field_vm.typ:16–27`) without defining it. +- *Options:* preprocessed or constrained addresses. +- *Taken, confirmed by Robin:* a chip with one row per address; uniqueness by constraint (`ADDR₀ = 0`, `ADDR' = ADDR + 1`), because with LogUp alone a prover could commit two rows with one address; backfilled by the prover, so write-once in execution. +- *Public cells:* a flag sends them on a bus the verifier closes itself. + +**Hint values.** The spec leaves them as an implementation detail (`field_vm.typ:147`). +- An output hint with `imm₀ ≠ 0` is solved. +- A single linear input hint (as in `INV`) is solved. +- Anything else comes from the host. +- Output hints on `ZERO` and hint collisions are rejected by the executor. + +**Smaller choices:** +- the extension polynomial w³ − 2; +- `DECODE` packed as 11 base-field values instead of extension elements, since the X² coefficient was always zero; +- N = 2 registers; +- segmented execution. + +--- + +## Part III — Experimental implementations + +### 11. A binary-field prover for the hash half (Binius64) + +The Recursion chapter names Flock as a possible prover for the hash half, so the first experiment measured what a binary-field prover does with this hash load. +- **Binius64 and keccak:** 65,536 keccak-f permutations in 2.1–3.0 s. An epoch needs ~70k compressions, so the hash half would take ~2.3–3.2 s, against ~12 minutes for keccak on the RISC-V VM. That is similar to, or a little better than, the LFM's whole epoch, before coupling the two proofs or verifying a binary-field proof in the next layer. +- **Flock and BLAKE3:** Flock was 6–7× faster than Binius64 on the same hash, proving 65,536 BLAKE3 compressions in 0.14 s. + +### 12. Split proving across proof systems (Flock) + +This is the spec's *split proving*, the section left as TODO (`recursion.typ:240`). Robin described it as "the road towards splitting the two parts up entirely, and through that enabling Flock". + +**The idea.** Prove each half in the proof system that suits it: +- the field half in a STARK over Goldilocks, with the Field VM; +- the hash half in Flock, a prover over a binary field that is very fast at bitwise hashes such as BLAKE3. + +Two proofs per step instead of one. + +**One step, in order.** + +```text + verifier of one epoch proof + │ cut + ┌───────┴────────┐ + ▼ ▼ + v_fld v_bin + Field VM Flock circuit + (Goldilocks) (binary field) + │ │ + ▼ ▼ + proof A proof B + │ │ + └─── shared values published in both ───┘ + │ + ▼ + the next level checks they are equal + and verifies both proofs +``` + +1. **Cut.** The verifier is cut as in Part I: field operations to v_fld, hashing, bits and Merkle work to v_bin. +2. **Proof A.** The Field VM runs v_fld and proves it, as a STARK over Goldilocks. +3. **Proof B.** v_bin is written as a Flock circuit and proved: + - all 79,343 BLAKE3 compressions of an epoch; + - the glue around them, as Flock gates: Merkle-path selects, packing and unpacking, bit decompositions with their check that the value is below p, reversed digests; + - prover hints as private witness. + + BLAKE3 is the 6-round variant our executor used, with Flock patched to match. +4. **Publish.** Every value both halves use becomes a public input of both proofs. +5. **Check.** Someone checks that A and B published the same values and verifies both proofs. In the first version a host did the comparison (together with one keccak-f permutation, since Flock has no keccak gate). In the tower, the next level does it. + +**What has to be bound, and why it is so much.** Two kinds of values cross: +- **The record:** values one half computes and the other uses (challenges, query bits, results). For one epoch this was ~94k cells. +- **The proof data both halves read:** ~100k cells. The Field VM folds FRI with the opened values of the proof being verified, but only Flock can check those values against their Merkle roots. So the opened values and Merkle siblings must reach both proofs. They cannot be cut, because they are the proof itself. + +Together that is 194,345 cells per step. Moving work to the side that owns it cut the record: +- assertions to Flock; +- bit decompositions to the Field VM; +- each half its own constants. + +The derived values dropped from ~94k to ~15–25k cells. **The ~94,153 cells of proof data stay:** that is the floor of this design. + +**One step, measured** (a real BLAKE3 epoch): +- Field VM, 0.59 s; Flock, 0.50 s; total **1.10 s**; +- against 5.05 s for the LFM with RPX, ~4.6× faster in prove time (1.4–1.7× once the circuit build is counted). + +**Recursion.** The next level verifies both proofs: the Field VM proof with our verifier, and the Flock proof with Flock's verifier replayed in the circuit. Flock's verification costs ~166k BLAKE3 compressions, and 93% of them go to digesting the published values. Built this way, the tower is sound up to height 2. + +**It does not converge.** The published interface grows with every level: 112,804 cells at level 1 (after the cuts), 972,491 at level 2. A level verifies the previous level's two proofs, and the data it must share between its own two halves is now the previous proofs' data, published values included. So the interface feeds itself. + +The obvious fix is to bind the shared values with one random linear combination instead of publishing them. It is cheap in Goldilocks, but costs ~20 billion constraints per challenge in Flock, where a Goldilocks multiply-add is ~20–30k Boolean constraints. + +**Conclusion:** split proving across fields needs a binding of the shared values whose cost does not grow with them and is cheap in both fields. Until then, split verification in one proof (Part II, §6) is the construction that converges. + +### 13. BLAKE3 + +**6 or 7 rounds.** The code used a 6-round BLAKE3 variant, so the standard 7-round BLAKE3 was compared against it: +- **In the base layer** (proving a block), the seventh round is practically free: +0.4% prove and +3% verify on a mainnet block. BLAKE3 stays ~12% faster than keccak there. +- **Inside a circuit over Goldilocks** (the LFM wrap), the seventh round costs **+17% prove**: every round is cells, 620 M → 695 M. +- **In Flock,** the 6-round variant was used, with Flock patched to match. + +So, if recursion moves to a binary-field prover, standard BLAKE3 has no downside. In a field circuit, 6 rounds save ~17% at the price of a non-standard hash whose security margin is not quantified. + +**In the one-proof tower.** The last experiment asked whether the tower of Part I could use BLAKE3 instead of RPX: +- It runs: three levels with one program id at Q = 1 (4.42 M cycles per level). +- At Q = 4 it needs 7.42 M cycles and 117 GB, and it only fits in memory by recomputing low-degree extensions. A BLAKE3 compression is a 3,268-column table; an RPX permutation, ~330. +- In a binary half generated from our word-lane representation, BLAKE3 cost ~4× RPX. Two compiler fusions cut that 31%, not enough for Q = 80. + +Over plain bytes the picture flips: a Rust binary half over bytes, with a bulk-absorb call, was 4.4× cheaper than RPX in a proxy measurement. **The hash, its precompile calling convention and the digest representation have to be chosen together.** With the RPX tower already at ~111 bits, the BLAKE3 line was closed here. + +--- + +## What we would put in the spec + +Each row is a concrete change proposed for the spec. The Typst text for it, ready to paste, and the evidence behind it are in the attached `1_proposed_spec_text.md`, in the section listed. + +| Proposal | Where in the spec | Section of `1_proposed_spec_text.md` | +|---|---|---| +| Write the verification chapter as an ordered list of transcript steps, from which the record follows | `verifier.typ` (empty, TODO) | §1 | +| Define the communication record as every value that crosses between the halves, named, with producer, consumer, type and a count from the proof shape | `recursion.typ:329–334` (overview TODO) | §2 | +| Say how the two VMs share data when both halves are proven in one proof: the pseudo-`PAGE`, in both directions, with canonical limbs | `recursion.typ`, Split verification (new subsection) | §3, first block | +| State what split proving needs: a binding between the two proofs whose cost does not grow with what crosses | `recursion.typ:240–241` (Split proving TODO) | §3, second block | +| Make the level counter required, and say how b is constrained | `recursion.typ:131–137` | §4 | +| Give every crossing value one enforced encoding (bits, limbs, whole digests, base-field values) | `recursion.typ`, record section | §9 | +| Define the `MEM` table (chip, unique addresses, write-once) and how public cells are bound | `field_vm.typ:16–27` | §7, §8 | +| Allow one tree per phase over all trace tables and one FRI, with program tables committed separately | `recursion.typ:347–349` | §11 | +| Separate instance and program commitments, list what identifies a split program, and require a shape fixed point for a uniform verifier | `recursion.typ:341–357` | §12 | +| Replace "typically shrinks" with a measurable inequality, `C_verify(L) < 2^L` | `recursion.typ:80–85` | §14 | +| Resolve the commitment-domain conflict by binding stdout through the COMMIT bus | `recursion.typ:359–394`, `memory.typ`, `streaming.typ` | §10 | +| Smaller points: the extension polynomial, hint values, restricting the ISA, segments, N as a parameter | `field_vm.typ` | §5, §6, §13 | +| Use one name for `FIELD_VM_DECODE` and fix the index typos in `field_vm.toml` | `recursion.typ:344`, `field_vm.toml` | — (editorial) | + +## Open points for the spec + +- **Where the hash half runs.** On RISC-V, as the spec places it, it is ~25× the cost of algebraic hash chips next to the Field VM (Part I). Keeping it there needs a binary half designed for it; the alternative is to allow algebraic hash chips. +- **Batched trace commitments.** Uniform recursion converged only with one tree per phase and one FRI. Whether that becomes a requirement is open. +- **Proof shapes and the commitment domain.** A straight-line verifier needs a fixed proof shape; whether recursion is meant over fixed or arbitrary shapes is open. So is whether the commitment domain is paged or unpaged, where the chapters disagree. +- **Binding for split proving.** Proving the halves separately (with Flock) needs a cross-field binding whose cost does not grow with what crosses; which construction the spec intends is open. diff --git a/spec/notes/01-split-verification-impl/1_proposed_spec_text.md b/spec/notes/01-split-verification-impl/1_proposed_spec_text.md new file mode 100644 index 000000000..e81d8bcde --- /dev/null +++ b/spec/notes/01-split-verification-impl/1_proposed_spec_text.md @@ -0,0 +1,453 @@ +3MI spec · spec/main 41c3af9a6 · proposals from the Lambda VM implementation + +# Proposed text for the open parts of the Field VM and Recursion chapters + +For every section the spec leaves as TODO or as an implementation detail, and for the gaps we hit building the uniform tower, this page gives what we propose, why (with what we measured or tested), and Typst text ready to paste into the chapter. + +The text follows what is built and tested in the Lambda VM: a uniform recursion tower over RPX, from an Ethereum block (a 10-transfer ethrex test block), at ~111 bits (blowup 4, Q = 80, grinding 32), one program id at every level. Names in `monospace` are the implementation's; the Typst uses the chapters' own notation where it exists. The story behind each proposal is in `0_input_for_3MI.md`. + +## Sections the spec leaves open + +### 1 · The verification chapter TODO + +verifier.typ:1 — "TODO: sigma protocol, layout the various steps; Fiat–Shamir transformation" + +**Proposal** + +Lay out the verifier as the ordered sequence of transcript steps. The recursion chapter needs exactly this list: it fixes the record (section 2) and the cost of each split half. + +**Why** + +Every soundness gap we found in the split was a value one half assumed and the other never produced. Writing the steps once, with what each absorbs and samples, makes the record derivable instead of discovered. The order below is the one our verifier and its in-VM emitter both follow. + +*Paste into verifier.typ* + +``` typst += Verification + +The verifier replays the prover's Fiat–Shamir transcript. Each step absorbs +prover messages and then samples challenges; a challenge is sampled only after +everything it must depend on has been absorbed. + ++ *Statement.* Absorb the instance: the public input and output, the public + Field VM cells and the shared regions. ++ *Shape and commitments.* Absorb the shape (the number of tables and each + table's trace length), then the preprocessed roots, which include the + program's `DECODE` and `FIELD_VM_DECODE` roots, then the main-trace roots. ++ *LogUp challenges.* Sample $z$ and $alpha$, shared by every bus. ++ *Auxiliary commitments.* Absorb the auxiliary-trace roots. ++ *Bus contributions.* Absorb each table's claimed LogUp contribution. ++ *Composition challenges.* Sample one $beta_t$ per table $t$; the composition + polynomial of $t$ is $sum_i beta_t^i dot C_(t,i)$ over its constraints. ++ *Composition commitments.* Absorb the composition roots. ++ *Out-of-domain points.* Sample one point $z_t$ per table, rejecting points in + the trace or evaluation domain. ++ *Out-of-domain claims.* Absorb, per table, the trace values at $z_t$ and at + $omega z_t$ (only the columns read at the next row), then the composition parts. ++ *DEEP challenges.* Sample one $gamma_t$ per table; if an FRI instance batches + several tables, sample $alpha_"fri"$ to combine them. ++ *FRI commit phase.* Per FRI instance and folding layer, sample the folding + challenge $zeta_j$ and absorb the layer root; absorb the final polynomial. ++ *Proof of work.* Check the grinding nonce against the transcript state, then + absorb it. ++ *Queries.* Sample $Q$ query indices as bits of the largest evaluation domain. ++ *Checks.* At $z_t$: each table's constraints against its composition claim. + Per query: every opened leaf against its root; the DEEP value of each table + from its openings and claims; the FRI fold along the query path; the final + polynomial. Last, the LogUp balance: the contributions sum to the term the + public input fixes. + +#aside("Who does what in a split verifier")[ + Steps 1–13 and the Merkle checks are hashing and bit work, for $v_"bin"$; the + constraint, DEEP, FRI-fold and balance checks are field arithmetic, for + $v_"fld"$. Section @split-verification:record lists what crosses. +] +``` + +### 2 · The communication record TODO + +recursion.typ:329–334 — "primarily consists of the Fiat-Shamir-derived challenges … update the communication record overview once @verification is complete." + +**Proposal** + +Define the record as every value one half assumes and the other produces, in a fixed order, with a count computed from the proof shape alone. Challenges are only part of it. + +**Why** + +- With the record defined as "whatever the cut makes cross", seven tamper cases verified forged proofs before each fix: a moved constant, a decomposed hint, three truncated digest lanes, non-canonical query bits and another guest program. +- We rebuilt the split so that only named values cross. On a tower level at Q = 1 the crossing went from 2,674 cells (91% without a meaning) to 2,319 named cells. At Q = 80 it went from 32,220 to 6,129. Cycles per level fell 1.2% at Q = 1 and 6.8% at Q = 80 (6.48 M → 6.04 M cycles on the fixture tower, three fewer tables, 3.4 GB less memory), and the levels keep one program id. +- The counts below are checked against the emitted verifier every time it is built. + +| Entry | Producer → consumer | Type | Count per verified proof | +|----|----|----|----| +| Fiat–Shamir challenges, in transcript order | v_bin → v_fld | extension, canonical | 2 + 3·T + \[α_fri\] + Σ ζ | +| Query bits | v_bin → v_fld | base, 0/1 | Q · log₂\|D_max\| | +| Register LDE | v_fld → v_bin | base, canonical | 2 · \|LDE\| per REGISTER table | +| Statement words (hinted ELF digest and public output) | v_fld → v_bin | base, canonical | 4 + ⌈L/8⌉ | + +T = number of tables, ζ = folding challenges over the FRI instances, L = public-output length in bytes. The register LDE and statement words are the values v_bin hashes that v_fld computes; values both halves can compute from the shared input are computed on both and are not record. + +*Paste into recursion.typ, replaces the paragraph at line 329 and the TODO at 334* + +``` typst +== The communication record + +The record holds every value one verification half assumes and the other +produces. For each entry the producing half verifies it and the consuming +half reads it; nothing else crosses. Values either half can compute from the +shared input alone are computed by both and are not part of the record. + +For a verified proof of $T$ tables, $Q$ queries and FRI folding challenges +$zeta_1, ..., zeta_k$, the record is, in this order: + +#table(columns: 4, + [*Entry*], [*From → to*], [*Type*], [*Count*], + [Fiat–Shamir challenges, transcript order (@verification)], [$v_"bin" -> v_"fld"$], + [extension, canonical], [$2 + 3T + [alpha_"fri"] + k$], + [Query bits, low to high], [$v_"bin" -> v_"fld"$], [bit], [$Q dot log_2 |D_max|$], + [Register LDE, leaf order], [$v_"fld" -> v_"bin"$], [base, canonical], + [$2 |D_"REGISTER"|$], + [Hinted statement as 8-byte words], [$v_"fld" -> v_"bin"$], [base, canonical], + [$4 + ceil(L / 8)$], +) + +The count is a function of the proof shape, so a verifier that knows the +shape knows the record layout. A recursive verifier that verifies two +proofs (@split-recursion) concatenates their records in verification order. + +#aside("Why not only challenges")[ + The consuming half must not trust any value it did not compute. A record + that lists only the challenges leaves every other crossing value + unconstrained in one half; in our implementation each omitted kind of value + admitted a forged proof. +] +``` + +### 3 · Split verification in one proof, and split proving TODO + +recursion.typ:145–239 — "Split verification": the two halves share a record and are proven as one program, `prove(product(verify_0, verify_1))`; recursion.typ:345–346 — the input, private input and record "are made available to the VMs by means of `PAGE` tables"; recursion.typ:240–241 — "= Split proving \#et("todo")" + +**Proposal** + +Two separate additions: + +- **Split verification:** say how the two VMs share data when both halves are proven in one proof. This is the construction Robin and Erik proposed: a 24-byte pseudo-`PAGE` that binds RISC-V memory bytes to Field VM cells. It adds a second direction, `BACK`, and canonical limbs. The spec says the input and record reach the VMs through `PAGE` tables, but not how the Field VM reads them. +- **Split proving (the TODO):** proving the halves separately, possibly in other proof systems. State the requirement we found: a binding between the two proofs whose cost does not grow with what crosses. + +**Why** + +- The one-proof construction is the one behind the uniform tower; Robin indicated the side-by-side Field VM and Lambda VM case "can still be a single proof". +- `BACK` is how the record travels from v_bin to v_fld. +- Without the limb bound, bytes encoding v + p pass as v; there is a test for it. +- What was tried for split proving: the Field VM half as a STARK over Goldilocks and the whole hash half as a Flock proof, two proofs per step. Every shared value was published in both, and the next level checked they matched and verified both proofs. Most of the shared values are the opened values and Merkle siblings of the proof being verified: the Field VM folds them, and only the hash half can authenticate them. They cannot be cut, so the published interface grows with each level (112,804 → 972,491 cells), and it did not converge. A random-linear-combination binding instead costs ~20 billion constraints in Flock. The full account is in `0_input_for_3MI.md`, §12. + +*Paste into recursion.typ, as a new subsection of "Split verification" after "Communication"* + +``` typst +== Proving both halves in one proof + +When both halves run on VMs proven over the same field, the product +$product(verify_0, verify_1)$ is proven as a single proof: one transcript, one +set of commitments, and the LogUp buses of both VMs balanced together. The +halves share the input and the record through _pseudo-`PAGE`_ regions of the +binary VM's memory. + +A region is a sequence of 24-byte cells. Cell $k$ holds three little-endian +64-bit limbs $(l_0, l_1, l_2)$, the coordinates of an extension element in the +basis $(1, X, X^2)$, and is mapped to the Field VM address $"FADDR"_k$. Per byte, +the region takes the place of the memory system's page: it sends the initial +token and receives the final token of that byte. Per cell, it sends +$("FADDR"_k, l_0, l_1, l_2)$ to `FIELD_VM_MEM`, with the limbs read from + +- the *initial* bytes for an `IN` region: values present before $v_"bin"$ runs + (the shared input and the record entries $v_"fld"$ produces), and +- the *final* bytes for a `BACK` region: values $v_"bin"$ writes for $v_"fld"$ + (the record entries $v_"bin"$ produces). + +The region constrains every limb to be below $p$, so the bytes of $v + p$ do +not stand for $v$. It does not range-check bytes: the binary program reads +every byte of an `IN` cell and writes every byte of a `BACK` cell, so each byte +meets a range-checked memory token. + +`FADDR` is preprocessed and its root is part of the program commitment. +Regions are page-aligned and lie in private-input pages. The statement absorbs +the number of regions and each region's base, direction, cell count and +address map; the binary program's public output begins with its program +digest and each region's base and cell count, which the verifier compares. +``` + +*Paste into recursion.typ, replaces the TODO at line 241* + +``` typst += Split proving + +Split proving proves the two halves separately, possibly in different proof +systems (e.g. $v_"bin"$ in a binary field). The proofs then cannot share a +commitment, so the values that cross between the halves (the record, and the +proof data both halves read) must be bound across the two proofs. + +Publishing those values in both proofs does not converge under recursion: each +level's interface contains the previous level's proof data, and it grows with +every level. Split proving requires a binding of the crossing values whose +cost does not grow with them and is cheap to compute in both fields. Until +such a binding is specified, split verification in one proof +(@split-verification:one-proof) is the construction that converges. +``` + +### 4 · Soundness of the recursion: the level counter Open + +recursion.typ:131–137 — "soundness of this construction is not yet proven … one might be able to prevent this … by including a recursion-level counter" + +**Proposal** + +Make the counter part of the construction instead of a suggestion. Also say how the bit b is constrained and how both branches coexist in one program. + +**Why** + +We built it this way. The final verifier accepts level k and rejects k + 1. Ten tampers are rejected: b = 2, b flipped both ways, a wrong comm(x) (twice), a forged child level, a wrong comm(y), another program of the same shape, a moved output, and shared precomputed trees. + +*Paste into recursion.typ, after the verify\* definition* + +``` typst +== Recursion level + +Every recursive proof states its level. $v_"fld"$ asserts $b^2 = b$. Every +assertion of the base verifier is multiplied by $1 - b$ and every assertion of +the recursive verifier by $b$: both run, and the inactive one constrains +nothing. With $b = 1$ the binary half checks that the child's output is +$(comm(x), comm(y), ell_"child")$, and publishes + +$ ell = 1 + b dot ell_"child". $ + +The final verifier checks $comm(x)$, $comm(y)$ and the level it expects; a +proof of level $k$ is rejected at any other level. +``` + +### 5 · Which value a hint takes Implementation detail + +field_vm.typ:146–147 — "provides no information on which value exactly should be hinted … leave this as an implementation detail" + +**Proposal** + +Give executors one default rule, so that two executors of the same program agree on its execution. + +**Why** + +This is what our executor does. It covers every hint the generated verifier uses: inversions are solved linearly, and frame pointers and dereferenced destinations come from the host. + +*Paste into field_vm.typ, after the instruction-notation paragraph* + +``` typst +#aside("Choosing hinted values")[ + An executor chooses hinted values in this order: + + an output hint on a register argument $d = #`imm`_0 dot #`reg` + #`imm`_1$ + with $#`imm`_0 != 0$ is solved for `reg`; + + a single input hint that enters the constraint linearly (as in `INV`) is + solved for its register; + + any other hint (a new frame pointer, a `d` that dereferences memory, an + output hint with $#`imm`_0 = 0$) is supplied by the host. + An output hint on `ZERO` is invalid: $next("ZERO")$ is already fixed by the + result. An instruction whose `d` register the next instruction input-hints + is rejected by the executor. +] +``` + +### 6 · Restricting the design after observed use Future + +field_vm.typ:350–356 — "Depending on observed use, in the future, we can restrict this design…" + +**Proposal** + +Record what a generated STARK verifier actually uses, so the parameters can be chosen from it. + +**Why** + +All measured on the Field VM half of a real epoch verifier: + +- **N = 2 registers:** 2.92 M → 2.39 M cells (−18%). +- **d = 3 at blowup 2:** proving goes from 4.53 s to 2.82 s, but the proof grows from 3.9 MB to 7.3 MB. +- **A register-free row variant:** only 13% of rows could use it, so we discarded it. +- **A third memory argument:** no net gain. + +*Paste into field_vm.typ, appended to "Notes and potential optimizations"* + +``` typst +- Observed on a generated STARK verifier: it works mostly through memory, so + $N = 2$ general-purpose registers suffice and reduce the trace by about a + fifth against $N = 5$. $d = 3$ at blowup 2 proves faster at the price of a + larger proof; the parameters $(d, N, t)$ should be part of the program's + identity rather than fixed globally. +``` + +## Gaps the spec does not cover yet + +### 7 · The MEM table Gap + +field_vm.typ:16–27 — "a committed table containing the memory as well as the multiplicities" + +**Why** + +With LogUp alone, a prover can commit two rows with one address and serve different values to different reads. Robin confirmed both the chip and the backfilling. + +*Paste into field_vm.typ, new section after the ISA* + +``` typst +== The memory table + +`MEM` has one row per address: `ADDR`, an extension `VALUE`, a multiplicity +`MU` and a public flag `PUB`. It receives $(#`ADDR`, #`VALUE`)$ on +`FIELD_VM_MEM` with multiplicity `MU`; an address with non-zero extension +coefficients does not balance. Addresses are unique by construction: +$#`ADDR`_0 = 0$ and $next(#`ADDR`) = #`ADDR` + 1$. + +`MEM` is read-only in the proof and write-once in execution: the prover +backfills it, an instruction whose `d` dereferences an undefined cell defines +it, and reading an undefined cell from `a`, `b` or `c` is an error. +``` + +### 8 · Binding public cells Gap + +**Why** + +The inputs and constants in `MEM` must be fixed by the statement. Shared data goes through the pseudo-PAGE (section 3); constants and published values need their own path. + +*Paste into field_vm.typ, after the memory table* + +``` typst +Rows with $#`PUB` = 1$ send $(#`ADDR`, #`VALUE`)$ on `FIELD_VM_PUBLIC`. The +verifier absorbs the public cells into the transcript, requires their +addresses to be strictly increasing and canonical, and closes the bus itself +against the term those cells determine. +``` + +### 9 · Canonical encodings of what crosses Gap + +**Why** + +Each of these accepted a forged proof before its fix: + +- x and x + p decompose to different query bits; +- a four-element RPX digest truncated to a three-coordinate cell; +- a base value carried with non-zero extension coordinates. + +*Paste into recursion.typ, in the record section* + +``` typst +Every record entry has one canonical encoding, enforced by its producer and +checked where it crosses: +- bits are 0 or 1, and a decomposition of a field element reconstructs a value + strictly below $p$; +- limbs crossing in a pseudo-`PAGE` are below $p$; +- a base-field entry has zero extension coordinates; +- a digest crosses whole: all of its elements, never truncated to fit a cell. +``` + +### 10 · Recursive instance commitment and the commitment domain Gap + +recursion.typ:359–394 vs memory.typ:25–33 and streaming.typ:117–124 + +**Why** + +The recursion chapter says stdout is backed by `PAGE` tables. The memory chapter calls the commitment domain unpaged, and the streaming chapter forbids `PAGE` on unpaged domains. We bind stdout through the COMMIT bus, whose term the verifier recomputes. With batched trace commitments (section 11) there is no per-table `PAGE` root to open anyway. + +*Paste into recursion.typ, replaces the PAGE-opening check at 370–394* + +``` typst +$v_"bin"$ writes $comm(x)$, $comm(y)$ and its level to `stdout`, the +commitment domain, which is unpaged: its bytes reach the verifier as public +output, whose bus term the verifier recomputes. With $b = 1$, $v_"bin"$ checks +that the child's public output, after its header, is +$(comm(x), comm(y), ell_"child")$. +``` + +### 11 · Batched trace commitments and one FRI Gap + +recursion.typ:347–349 — "the prover commits to each of these tables individually" + +**Why** + +- With one tree and one FRI per table, verifying an epoch of 2²¹ cycles costs 409,013 hash permutations, and recursion diverges (35.5× even with a native v_bin). +- With one tree per phase and one FRI it costs about 57,000, and recursion converges. +- On a mainnet block, the same change gives −12% prove time, −73% proof size and −75% verify time. +- Program tables keep their own trees, so the program id is still a list of roots. + +*Paste into recursion.typ, replaces 347–349* + +``` typst +Tables whose content the program fixes (`DECODE`, `FIELD_VM_DECODE` and the +other program-dependent preprocessed tables) are committed individually; +their roots identify the program. Trace tables are committed in one tree per +phase (main, auxiliary, composition) over all heights, and their low-degree +tests combined into one FRI instance, once the shape (table set and heights) +has been absorbed. +``` + +### 12 · Program identity and the two commitment functions Gap + +**Why** + +The spec uses one commitment notation for both instances and programs. A split program is identified by both halves and by the layout of what they share. + +*Paste into recursion.typ, in "Recursive instance verification"* + +``` typst +A split program's identity is the hash of a domain tag, its binary +executable's digest and entry point, and the roots of its program-dependent +tables: `DECODE`, the executable's data pages, the `FIELD_VM_DECODE` chunks and +the pseudo-`PAGE` address maps. Instances and programs are committed with +separate domain tags: +$ comm(x) = H("instance" || "id" || |"out"| || "out"), quad + comm(y) = H("program" || "id"). $ +``` + +### 13 · Field VM parameters left unnamed Gap + +**Why** + +- **The extension polynomial:** it has to be fixed for proofs and programs to be portable. +- **DECODE packing:** the X² coefficient was always zero, so we pack base-field values instead. +- **Segments:** they avoid padding a long run to the next power of two. + +*Paste into field_vm.typ* + +``` typst +- The extension field is $FF_p [w] \/ (w^3 - 2)$. +- The decoding tuple may be packed as base-field values: LogUp weights each + value with its own power of the challenge, so packing into extension + elements is an optimization, not a requirement. +- An execution may be proven in power-of-two segments. Each segment has public + first and last states; a segment that is not the last repeats the next + segment's first step in its last row, so the hand-over is constrained, and + only the last segment pads with the halt state. +``` + +### 14 · When recursion converges Gap + +recursion.typ:80–85 — "the proof size typically shrinks" + +**Why** + +Measured cost of verifying one epoch, as a multiple of the epoch: + +- 337× per table with an interpreted v_bin; +- 35.5× with a native v_bin; +- 11.5× with batched commitments; +- 2.38× with no keccak in the guest; +- 0.615× at 2²³. + +The tower level is at 0.973 × 2²³ at Q = 80. The node that verifies two proofs is the binding case. + +*Paste into recursion.typ, after the shrinking argument* + +``` typst +Recursion converges when the cycles of the recursive verifier, for the proof +shape it verifies and at the target security, fit one epoch: +$ C_"verify"(L) < 2^L. $ +$C_"verify"$ includes every hash permutation, the guest's overhead, the +public input and, for a node that verifies two proofs, both. "Typically +shrinks" is not a guarantee: in our measurements the condition required +batched commitments, no binary-hash tables in the recursive guest, a +compiled $v_"bin"$, and epochs of $2^23$ cycles. +``` + +Prepared by the Lambda VM team, October 2026, against spec/main 41c3af9a6 (Field VM \#971, Recursion \#943). Every number is measured in our implementation unless stated otherwise.