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-24T11:58:26Z

+*Record $record$.*
+The record contains all challenges the prover derived using Fiat-Shamir.
+
+*Tasks for $verify'_b\(commitment_0, commitment_1, b, proof, record)$:*


This is missing a few of the ad-hoc checks, which are (I think) mostly related to memory and paging.
It would probably be a good idea to have an overview of those somewhere central as well.

I'm not content with this section, at all. Indeed, stuff is missing.
I propose we have a full verifier description in verifier.typ (including all the ad-hoc checks you mention) and here only mention how to transform that monolithic verifier into the split/recursive verifier in this section.

wdyt of that split?

Works for me

I rewrote this section. Let me know what you think!

I think the offloading to the original v_f and v_b should work to kick the can down the road and have a full description elsewhere 👍

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

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

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

RobinJadoul · 2026-08-28T10:36:11Z

+$
+
+*Final verification.*
+$verify'(commit(instance), (commit(verify'_b), commit(verify'_f)), 1, proof^((n))) =? one$


We may be able to get rid of the b argument by having the statement being proven the OR of both options:
I know a proof that is either accepted for the original statement OR for the recursion function.
I suppose this is essentially absorbing this bit into the proof or witness, but it cleans up the final verification and allows proofs without compressing to be used without any further change.

I like the idea, but am not confident that it works well in practice. Specifically, for the ultimate verifier to confirm the proof, they would have to execute both v(x, proof) and v(v'(x, v', proof) to determine whether one of the two is true.

I think a better approach would be to absorb b into the proof. From a notation perspective, this still gets rid of the b, but now you have a bit which allows you to select the right verification configuration.

Sure, turning it from a hint into an explicit value inside the proof should work fine

Maybe the theoretical part is actual nicer represented as an OR statement (not sure, but it avoids making assumptions on the structure of the proof), but we can have the bit inside the proof in practice, making it convenient in the implementation too.

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.

RobinJadoul · 2026-09-03T10:29:24Z

+
+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 verificationan  algorithm `COMMIT` (see @commit)


Suggested change

This is achieved by having the verificationan algorithm `COMMIT` (see @commit)

This is achieved by having the verification algorithm `COMMIT` (see @commit)

RobinJadoul · 2026-09-03T10:31:00Z

+    + execute $verify_b (comm(verify'(comm(instance), comm(verify'); dot)), proof)$
+
+*$verify'_f\(comm(instance), (comm(verify'_b), comm(verify'_f)), b, proof, record)$:*
+- verify proof: $verify_b (comm(verify'(comm(instance), comm(verify'); dot)), proof)$


Suggested change

- verify proof: $verify_b (comm(verify'(comm(instance), comm(verify'); dot)), proof)$

- verify proof: $verify_f (comm(verify'(comm(instance), comm(verify'); dot)), proof)$

erik-3milabs added 5 commits August 14, 2026 12:39

spec: recursive verification explanation, pt1

187edc3

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

89e5cac

spec/recursion: overhaul

0aab4a4

spec/recursion: clean up

408ab46

spec/recursion: more cleanup

ab117fa

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 and others added 4 commits August 26, 2026 10:14

Apply suggestions from code review

b430d3d

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

spec/recursion: address code review comments

f293a72

Apply suggestions from code review

2a62ec8

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

spec/recursion: address review comments

6220a57

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

address comments Cyprien

f92d469

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

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

	This is achieved by having the verificationan algorithm `COMMIT` (see @commit)
	This is achieved by having the verification algorithm `COMMIT` (see @commit)

	- verify proof: $verify_b (comm(verify'(comm(instance), comm(verify'); dot)), proof)$
	- verify proof: $verify_f (comm(verify'(comm(instance), comm(verify'); dot)), proof)$

Uh oh!

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!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants