spec: Recursion by erik-3milabs · Pull Request #943 · yetanotherco/lambda_vm

erik-3milabs · 2026-08-21T10:07:40Z

No description provided.

github-actions · 2026-08-21T10:07:55Z

Kimi Code Review

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

Automated review by Kimi (Moonshot AI)

github-actions · 2026-08-21T10:08:49Z

Codex Code Review

Medium — Recursive verification omits the required commitment (spec/recursion.typ:105). verify accepts a commitmentSpace, but the recursive branch treats commitment_1 as a function; lines 116–118 similarly pass verifier functions directly. Use an explicitly defined specialization operation producing comm(verify'(commitment_0, commitment_1, ·)). As written, the equations are ill-typed and do not establish the claimed recursive chain.

RobinJadoul · 2026-08-28T10:30:15Z

+When recursing on this process, the prover provides the verifier with this commitment.
+We thus have to demonstrate the commitments the prover provides are as expected.
+This is achieved by having the verification algorithm `COMMIT` (see @commit)
+to the public input it is provided.
+This act produces an imbalance in the LogUp-component of the proof-of-verification, 
+which must be balanced during verification in the _next_ recursion layer.
+In later recursions, the verifier must consistently `COMMIT` to its public input
+and use the _same_ public input to balance out the LogUp-component of the proof
+it is provided.
+This solution effectively kicks the can down the road; the final verifier has to
+provide the initial input to the program as input to verify the recursive proof.


We may not have access to COMMIT in a future flock-fieldvm hybrid

Isn't this handled by $\mathbb{c}_1 = \bar{\mathbb{x}}$ already? Since the instance $\mathbb{x}$ includes the public input?

Re 2.

Do you mean that having the guest COMMIT to $\mathbb{c}_1$ is excessive, since there must be a PAGE storing it, and all PAGEs are committed to by the VM?

In that case the verifier will have to add a constraint to that specific PAGE table, constraining that it contains the commitment on the required address 🤔 or were you thinking of a different solution?

There are multiple PAGEs that need to be present to correctly represent the ELF being loaded into memory, so those would be part of $\bar{\mathbb{x}}$ already. And the ELF is the public input part, potentially with the PAGEs for the commitments made by the guest program.
So in the end, we'd need these specific tables to be used already as precomputed tables (which could/would be part of a verification key that can be derived from the ELF once and not computed on every verification).

cdesaintguilhem

Mostly minor comments!

cdesaintguilhem · 2026-09-01T11:26:30Z

+  verify': commitmentSpace^2 times {0, 1} times proofSpace: (commitment_0, commitment_1, b, proof) mapsto
+  cases(
+    verify(commitment_0, proof) &text("if") b=0,
+    verify(commitment_1((commitment_0, commitment_1); dot), proof) &text("if") b=1


I can't parse what commitment_1((commitment_0, commitment_1); dot) is meant to be here.

cdesaintguilhem · 2026-09-01T11:50:33Z

+are henceforth referred to as _function instances_, or simply _instances_.
+Where convenient, we may also denote this as $function(input; dot) in instanceSpace$
+with instance space $instanceSpace$.
+We then define $relation subset.eq instanceSpace$ 


This relation is actually a language.

I rewrote the paragraph, as discussed. Is it correct now?

cdesaintguilhem · 2026-09-01T11:57:54Z

+Since these commitments are deterministic, the verifier can locally reconstruct
+the commitments and verify any opening proofs against its own version of the commitment.


As an optimisation: if the verifier has the DECODE and relevant PAGE tables in the clear, the prover does not even need to provide the corresponding openings as part of the proof string.

The downside would be that you get an increased storage cost in the verifying key, where storing those tables on-chain would be very costly, compared to just merkle roots.

RobinJadoul

I'm wondering whether we should choose for the $f$ function in the proof system to be the ELF proof, or if it should purely be the VM itself, and moving the ELF into public inputs.

Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com>

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>

RobinJadoul

Not paying attention to all possible typography yet, trying to get the last high-level stuff out of the way
I'll try to do another pass later this week, but this is a first go at it

RobinJadoul · 2026-09-21T12:52:57Z

+#let (proofSpace, proof) = ($bb(Pi)$, $pi$)
+
+#let (commitmentSpace, commitment) = ($cal(C)$, $bb(c)$)
+#let commit(x) = $overline(#x)$


Suggested change

#let commit(x) = $overline(#x)$

#let commit(x) = $dash(#x)$

should work better for html export
(except there's some weird rendering issues where at least FF, and seemingly other browsers too, so maybe this should be a later effort to clean up browser rendering a bit, as chromium also seems generally quite bad atm)

I'm leaving it out of the commitment-batch for now, but would be happy to switch once we've established how to fix the html support issue.

RobinJadoul · 2026-09-21T13:01:03Z

+
+== Recursively proving proof verification
+Now observe that the verifier $verify$ is itself a function in 
+$verifierSpace := {hat(f): commitmentSpace times proofSpace to BB} subset.eq programSpace$.


I think that to use the proof as private input, we need to have $\hat{f}$ map from only $\mathcal{C}$, or let $\mathcal{V} \subseteq \mathbb{X}$
The former is probably the more interesting, though that kinda moves the meaning of $\hat{f}$ to "c commits to a satisfiable (/solvable?) instance"

Let's discuss this in person

RobinJadoul · 2026-09-21T13:26:33Z

+For example, there may exist proofs that _attest to the existence of itself_ in a finite number of recursion steps.
+Such a proof would be accepted by $verify'$ even if $instance in.not language$.
+In practice, one might be able to prevent this problem by including a recursion-level counter in the proof.
+The existence of other soundness gaps are not ruled out by the authors.


Feels a bit weird to phrase it like this, maybe something about not providing a full proof of soundness (yet)?

sure. wdyt of

Suggested change

The existence of other soundness gaps are not ruled out by the authors.

The provision of a full soundness proof is deferred.

?

RobinJadoul · 2026-09-21T14:48:11Z

+$program$ and input $input$ are committed to separately.
+Recall that a (split) program is encoded as one or more 
+`DECODE` (@decode) and/or `FIELD-DECODE` (@field-decode) tables, while the 
+input $input$ --- and private input $witness$ and record $record$ for that matter 


Technically, public input is committed private input, but committed values are now available through COMMIT's PAGEs

A) some committed values (namely those COMMITted by the guest program) are available through the COMMIT's PAGEs, right?

B) how would you propose the text be modified? I'm confused by the remark.

RobinJadoul · 2026-09-21T14:50:47Z

+Leveraging the `COMMIT` chip is mostly useful in situations where revealing full `PAGE`
+tables is unnecessarily expensive or cumbersome, e.g., when committing to small 
+amounts of data or to data scattered across several `PAGE` tables.
+One potential limitation is that `COMMIT`ting in this way is at the discretion of the VM's
+guest program.


I think this model of COMMIT is outdated since epoch/L2G system for committing? Though I suppose a COMMIT-domain PAGE table is not strictly different from just providing the same interactions from the verifier.

why would this model be outdated? I don't see how the epoch/L2G system changed this.

RobinJadoul · 2026-09-21T14:52:44Z

+- derives challenges from $proof$ by means of Fiat-Shamir, and assert that they 
+  match those located in $record$ at the expected location.
+- Performs the binary arithmetic steps required to verify that $proof$ attests
+  to $instance$ (when $b=0$) or $instance2$ (when $b != 0$#footnote[The RiscV-VM's `PAGE` tables only supports byte data. All non-zero data is treated as $b=1$.]),


We can assert the bit-ness of b as well, alternatively

You mean by including

x = EQ[b, 0]; y = EQ[b, 1]; z = x + y; z = EQ[z; 1];

in the guest program?

Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com>

erik-3milabs · 2026-09-22T10:17:38Z

+
+== Recursively proving proof verification
+Now observe that the verifier $verify$ is itself a function in 
+$verifierSpace := {hat(f): commitmentSpace times proofSpace to BB} subset.eq programSpace$.


Let's discuss this in person

erik-3milabs · 2026-09-22T10:19:16Z

+For example, there may exist proofs that _attest to the existence of itself_ in a finite number of recursion steps.
+Such a proof would be accepted by $verify'$ even if $instance in.not language$.
+In practice, one might be able to prevent this problem by including a recursion-level counter in the proof.
+The existence of other soundness gaps are not ruled out by the authors.


sure. wdyt of

Suggested change

The existence of other soundness gaps are not ruled out by the authors.

The provision of a full soundness proof is deferred.

?

erik-3milabs · 2026-09-22T10:19:59Z

+For each value on the record, the "sending" half _verifies_ that it is as expected, 
+whilst the "receiving" half _assumes_ its correctness and resumes verification under this assumption.
+One can now conclude that the proof satisfies the instance
+when both algorithm-halves produce the same record for this input.


A)

Suggested change

when both algorithm-halves produce the same record for this input.

when both algorithm-halves accept the same record for this input.

B) let's discuss this in person.

erik-3milabs · 2026-09-22T10:20:24Z

+]
+
+More formally, we define
+$v_0, v_1: instanceSpace times proofSpace to recordSpace$ as a valid _split_ of 


like this, you mean, right?

Suggested change

$v_0, v_1: instanceSpace times proofSpace to recordSpace$ as a valid _split_ of

$v_0, v_1: commitmentSpace times proofSpace to recordSpace$ as a valid _split_ of

erik-3milabs · 2026-09-22T10:23:41Z

+$
+where $recordSpace$ denotes the communication record space.
+That is, the two halves agree if and only if the instance-proof verifies succesfully.
+By applying the Kronecker delta function $delta$ #footnote("https://en.wikipedia.org/wiki/Kronecker_delta"),


I included it, as I've encountered a wild variety of notation for the delta function and wanted to point the reader to the exact definition I'm using here. We could alternatively derive it in the document and keep it self-contained. wdyt?

erik-3milabs · 2026-09-22T10:27:25Z

+Leveraging the `COMMIT` chip is mostly useful in situations where revealing full `PAGE`
+tables is unnecessarily expensive or cumbersome, e.g., when committing to small 
+amounts of data or to data scattered across several `PAGE` tables.
+One potential limitation is that `COMMIT`ting in this way is at the discretion of the VM's
+guest program.


why would this model be outdated? I don't see how the epoch/L2G system changed this.

erik-3milabs · 2026-09-22T10:29:12Z

+- derives challenges from $proof$ by means of Fiat-Shamir, and assert that they 
+  match those located in $record$ at the expected location.
+- Performs the binary arithmetic steps required to verify that $proof$ attests
+  to $instance$ (when $b=0$) or $instance2$ (when $b != 0$#footnote[The RiscV-VM's `PAGE` tables only supports byte data. All non-zero data is treated as $b=1$.]),


You mean by including

x = EQ[b, 0]; y = EQ[b, 1]; z = x + y; z = EQ[z; 1];

in the guest program?

erik-3milabs · 2026-09-22T10:29:44Z

hmmm, this should be removed, no?

erik-3milabs · 2026-09-22T12:17:43Z

+#let (proofSpace, proof) = ($bb(Pi)$, $pi$)
+
+#let (commitmentSpace, commitment) = ($cal(C)$, $bb(c)$)
+#let commit(x) = $overline(#x)$


I'm leaving it out of the commitment-batch for now, but would be happy to switch once we've established how to fix the html support issue.

erik-3milabs · 2026-09-22T12:30:27Z

+$program$ and input $input$ are committed to separately.
+Recall that a (split) program is encoded as one or more 
+`DECODE` (@decode) and/or `FIELD-DECODE` (@field-decode) tables, while the 
+input $input$ --- and private input $witness$ and record $record$ for that matter 


A) some committed values (namely those COMMITted by the guest program) are available through the COMMIT's PAGEs, right?

B) how would you propose the text be modified? I'm confused by the remark.

erik-3milabs requested review from RobinJadoul and cdesaintguilhem August 21, 2026 10:07

erik-3milabs self-assigned this Aug 21, 2026

erik-3milabs added the spec Updates and improvements to the spec document label Aug 21, 2026

RobinJadoul reviewed Aug 24, 2026

View reviewed changes

erik-3milabs requested a review from RobinJadoul August 28, 2026 09:50

RobinJadoul reviewed Aug 28, 2026

View reviewed changes

cdesaintguilhem reviewed Sep 1, 2026

View reviewed changes

erik-3milabs force-pushed the spec/recursion branch from ff44161 to f92d469 Compare September 2, 2026 16:00

erik-3milabs requested review from RobinJadoul and cdesaintguilhem September 2, 2026 16:09

RobinJadoul reviewed Sep 3, 2026

View reviewed changes

Comment thread spec/chapters/recursion.typ Outdated

Comment thread spec/chapters/recursion.typ Outdated

erik-3milabs added 2 commits September 8, 2026 11:25

spec: recursive verification explanation, pt1

0ecc4e8

spec/recursion: put text and figure side-by-side

c3652e7

RobinJadoul force-pushed the spec/recursion branch 3 times, most recently from 8e0d8f7 to 82dcc54 Compare September 8, 2026 09:38

erik-3milabs and others added 8 commits September 8, 2026 11:39

spec/recursion: overhaul

b89ff29

spec/recursion: clean up

13f32ce

spec/recursion: more cleanup

bc875f0

Apply suggestions from code review

0fae699

Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com>

spec/recursion: address code review comments

741811e

Apply suggestions from code review

757131a

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>

spec/recursion: address review comments

54ce924

address comments Cyprien

a75546f

RobinJadoul force-pushed the spec/recursion branch from 82dcc54 to a75546f Compare September 8, 2026 09:40

erik-3milabs added 2 commits September 18, 2026 11:06

complete combination

cc47599

trim excess

8c27b72

refactor

808b2ce

erik-3milabs requested a review from RobinJadoul September 18, 2026 09:09

RobinJadoul reviewed Sep 21, 2026

View reviewed changes

Apply batched suggestions from code review

694a6a5

Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com>

erik-3milabs commented Sep 22, 2026

View reviewed changes

erik-3milabs added 2 commits September 22, 2026 14:32

spec/recursion: drop book.typ

9794227

spec/recursion: replace || by product

5ba52b7

		Since these commitments are deterministic, the verifier can locally reconstruct
		the commitments and verify any opening proofs against its own version of the commitment.

	The existence of other soundness gaps are not ruled out by the authors.
	The provision of a full soundness proof is deferred.

	when both algorithm-halves produce the same record for this input.
	when both algorithm-halves accept the same record for this input.

	$v_0, v_1: instanceSpace times proofSpace to recordSpace$ as a valid _split_ of
	$v_0, v_1: commitmentSpace times proofSpace to recordSpace$ as a valid _split_ of

Conversation

erik-3milabs commented Aug 21, 2026

Uh oh!

github-actions Bot commented Aug 21, 2026

Kimi Code Review

Uh oh!

github-actions Bot commented Aug 21, 2026

Codex Code Review

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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!

Uh oh!

Uh oh!

cdesaintguilhem left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

RobinJadoul left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

RobinJadoul left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

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!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

erik-3milabs Sep 22, 2026 •

edited

Loading