Discussion: split proving implementation by erik-3milabs · Pull Request #1019 · yetanotherco/lambda_vm

erik-3milabs · 2026-10-14T09:55:37Z

This PR is introduced with the single aim of discussing two markdown files generated during the implementation of the FieldVM (#971) and split verification (#943); there is no plan to merge this PR.

github-actions · 2026-10-14T09:55:52Z

Kimi Code Review

⚠️ Review failed: Kimi API request failed with status 401

Automated review by Kimi (Moonshot AI)

github-actions · 2026-10-14T09:56:32Z

Codex Code Review

No actionable issues found in the PR diff. It adds only two documentation files with implementation notes and proposed specification text; no executable code changes.

erik-3milabs · 2026-10-14T10:08:15Z

+- 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.


We have not spec'd out how the FieldVM should interact with an algebraic hash chip. How was this implemented?

erik-3milabs · 2026-10-14T10:12:26Z

+
+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.


What is meant here by "framework"? The code?

[...] open the LogUp accumulator at the next row. [...]

What does it mean to "open the LogUp accumulator"?

erik-3milabs · 2026-10-14T10:14:41Z

+- 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.


Could you expand on these two ideas?

erik-3milabs · 2026-10-14T10:18:13Z

+- **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.


The FieldVM was designed such that it could support branching and conditionals, allows us to create a single verification program that can accommodate proofs and instances of different shapes and sides. Having a 'dynamic' program should also prevent having to chunk the (FIELD_)DECODE table, as previously mentioned.

Why is this a straight-line program instead?

erik-3milabs · 2026-10-14T12:16:50Z

+
+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:


In my understanding, this subsection is all about the LFM (Lamda Field Machine). I'm therefore reading this as

The first version [of the LFM] used 11x the cells of the same arithmetic in the LFM

That does not make sense. So what is being compared here?

erik-3milabs · 2026-10-16T06:51:46Z

+
+**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.


Perhaps there is room for optimization by reordering things?

erik-3milabs · 2026-10-16T06:54:56Z

+**`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.


How does the flag work?

What is the "them" being sent?

What do you consider as "public cells" in this context?

erik-3milabs · 2026-10-16T06:55:59Z

+
+**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;


erik-3milabs · 2026-10-16T06:58:06Z

+- **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.


What is the Flock+Keccak performance?

erik-3milabs · 2026-10-16T07:04:19Z

+
+**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.


cdesaintguilhem · 2026-10-16T08:55:00Z

+
+### 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.


This step is described as implementing the "field half of verifying one epoch" which should not including any hashing operations, so what is meant by "with RPX as the hash"?

Also, I understood "the existing epoch verifier" to be a RISC-V program that verifies all the components of an epoch proof, so which parts of it were translated into "Field VM programs" for this step?

cdesaintguilhem · 2026-10-16T09:03:16Z

+### 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).


From the addition of RPX hash chips, I assume that RPX was selected as the hash function for the Merkle trees of the base layer, which is not something that is explicitly mentioned anywhere. Do we have data on the relative performance of the LFM proving RPX versus Keccak or Blake? What motivated the choice to add RPX into the experiments?

cdesaintguilhem · 2026-10-16T09:04:43Z

+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).


These two lines together imply that Option A was building the "hash half" with the "Field VM"; is that correct?

cdesaintguilhem · 2026-10-16T09:06:37Z

+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.


Also, if Option B was to use a RISC-V program for the hash half, why was RPX kept as the choice of hash function? Was Option B tried with other hash functions instead?

cdesaintguilhem · 2026-10-16T09:08:31Z

+- 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.


still about 25x the LFM

As written in this comment, the "LFM" is a bit of an ambiguous term.

cdesaintguilhem · 2026-10-16T09:14:40Z

+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.


Once experimental results above are clarified, maybe some of this is still relevant for the design of the hashing half.

notes by JP on implementing split proving

208cd98

RobinJadoul marked this pull request as draft October 14, 2026 12:14

erik-3milabs commented Oct 16, 2026

View reviewed changes

cdesaintguilhem reviewed Oct 16, 2026

View reviewed changes

jotabulacios mentioned this pull request Oct 21, 2026

Field vm/3mi whir #1026

Draft


		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.


		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:


		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.

		- 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.


		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.


		### 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 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).

Conversation

erik-3milabs commented Oct 14, 2026

Uh oh!

github-actions Bot commented Oct 14, 2026

Kimi Code Review

Uh oh!

github-actions Bot commented Oct 14, 2026

Codex Code Review

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants