Extend split-recursion to multiple proof systems by RobinJadoul · Pull Request #1018 · yetanotherco/lambda_vm

RobinJadoul · 2026-10-13T16:17:00Z

No description provided.

github-actions · 2026-10-13T16:17:13Z

Kimi Code Review

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

Automated review by Kimi (Moonshot AI)

github-actions · 2026-10-13T16:17:50Z

Codex Code Review

Medium — Incorrect challenge-binding requirement (recursion.typ:271): The specification requires committing to [x, r] before revealing z, but the checksum compares witnesses [π, r]. Binding the public instance x leaves π adaptable after the challenge, invalidating the random-checksum soundness argument. Require both witness commitments c₀ and c₁ to be fixed before deriving the same z, and include both in the Fiat–Shamir transcript.

The diff changes only the specification; no executable-code issues were found.

erik-3milabs

general remarks:

replace pi by proof
replace r by record
you're opted to write $v(x; w)$ rather than $v(x,w)$. This is, however, contrary to all other notation in this document. Not saying it is wrong, but it should be clarified somewhere

erik-3milabs · 2026-10-14T07:28:30Z

+we will write $comm(x)$ and $comm2(x)$ as the (deterministic) commitments to $x$
+in the proof system of $verify_0$ and $verify_1$ respectively.
+
+If we write $verify'_(b)([c_x, c_w]; w)$ to be an adaptation of $verify_(b)(c_x; w)$ that additionally gives has a public commitment to the private witness,#footnote[


$v_b$ is not yet defined at this point. Or do you mean to use it as a variable that can be either 0 or 1? Eitherway, we should probably define this. Also, I don't know if $b$ is the right choice here.

Also, $v'$ was already used in 36.1.2, so we're somewhat overloading things here.

b is indeed just a generic bit here

erik-3milabs · 2026-10-14T07:31:12Z

+we will write $comm(x)$ and $comm2(x)$ as the (deterministic) commitments to $x$
+in the proof system of $verify_0$ and $verify_1$ respectively.
+
+If we write $verify'_(b)([c_x, c_w]; w)$ to be an adaptation of $verify_(b)(c_x; w)$ that additionally gives has a public commitment to the private witness,#footnote[


Suggested change

If we write $verify'_(b)([c_x, c_w]; w)$ to be an adaptation of $verify_(b)(c_x; w)$ that additionally gives has a public commitment to the private witness,#footnote[

If we write $verify'_(b)([c_x, c_w]; w)$ to be an adaptation of $verify_(b)(c_x; w)$ that is additionally given a public commitment to the private witness,#footnote[

?

erik-3milabs · 2026-10-14T07:49:41Z

+
+The first two statements would follow naturally from proving $verify_(b)$ or the derived $verify'_(b)$.
+To integrate the last statement, we introduce a "checksum" of the witness, which will be checked by both halves of the split:
+$ verify^*_(b)([x, s]; w) = verify'_(b)(x; w) dot (serif("cksum")(w) =^? s). $


$v^*$ is used for a different purpose later on: we're overloading here.

erik-3milabs · 2026-10-14T07:51:34Z

+
+- $serif("cksum")(x) = serif("Hash")(x)$: compute a hash in both halves, at the cost of needing to evaluate a hash in a proof system that is likely not a good fit for that hash.
+- $serif("cksum")(x) = comm2(x)$: recompute the commitment $comm2(x)$ as part of $verify^*_0$, and let $verify^*_1$ simply check that the checksum equals the public commitment.
+  In practice, this would come at the cost of evaluating a Reed-Solomon blowup over the field of $verify_0$ and computing a merkle tree, both inside $verify^*_0$.


In practice, this would come at the cost of evaluating a Reed-Solomon blowup over the field of [...]

This is an implementation detail not described anywhere else in the document.

Fair, it is mostly meant as a remark to argue why it's not a good/performant approach

erik-3milabs · 2026-10-14T07:54:05Z

+Finally, we consider the instantiation $serif("chsum")(x) = chevron.l x, z chevron.r$ for a random zero-evader $z$.
+This could be implemented by having an additional public input provided to $verify^*_(b)$, or by having $verify^*_(b)$ itself
+derive it from the public inputs and context as a Fiat-Shamir challenge.
+In either case, $z$ should not be known to the (recursion) prover before being bound to $[x, r]$ via its public commitment.


shouldn't the prover also commit to the proof it will be verifying first?

erik-3milabs · 2026-10-14T08:43:11Z

+the verification cost of computing $z$ and the soundness error of the zero-evader.
+Where needed, multiple independent $z$ can be used to amplify soundnes.
+In settings where both $verify^*_(b)$ are in the same proof system, with the same commitment scheme, but different representations of the committed data
+(e.g. representing $pi$ as a sequence of committed bytes and as a sequence of extension field elemens),


Suggested change

(e.g. representing $pi$ as a sequence of committed bytes and as a sequence of extension field elemens),

(e.g. representing $pi$ as a sequence of committed bytes and as a sequence of extension field elements),

erik-3milabs · 2026-10-14T08:46:46Z

+  A larger $[pi, r]$ comes at a cost --- whether a cost of soundness or a cost of deriving more independent random $alpha_i$ ---
+  and as such should be kept as short as possible.
+  Since values that only one $verify^*_(b)$ reads or writes cannot lead to a differing result, the checksummed data need only
+  be the subsequence of elements of $[pi, r]$ that is read or written by both $verify^*_0$ and $verify^*_1$.


Suggested change

be the subsequence of elements of $[pi, r]$ that is read or written by both $verify^*_0$ and $verify^*_1$.

be the subsequence of elements of $[pi, r]$ that is accessed by both $verify^*_0$ and $verify^*_1$.

or "interacted"?
Reason I'm proposing this, is to avoid the ambiguous interpretation that one need only include values that are either read by both or written by both (where in practice we see values being "written" by one and read by the other)

erik-3milabs · 2026-10-14T08:52:06Z

+To enable recursion from a split verifier, we start by considering that each part of the split may
+be prove in a different proof system, and with a different commitment scheme.


Suggested change

To enable recursion from a split verifier, we start by considering that each part of the split may

be prove in a different proof system, and with a different commitment scheme.

To enable recursion from a split verifier, we start by considering that either part may

be proven in a different proof system, each using a different commitment scheme.

erik-3milabs · 2026-10-14T08:52:58Z

+For a split verifier $(verify_0, verify_1, d_verify)$ to be recursively proven,
+we will write $comm(x)$ and $comm2(x)$ as the (deterministic) commitments to $x$


Suggested change

For a split verifier $(verify_0, verify_1, d_verify)$ to be recursively proven,

we will write $comm(x)$ and $comm2(x)$ as the (deterministic) commitments to $x$

We write $comm(x)$ and $comm2(x)$ as the (deterministic) commitments to $x$

erik-3milabs · 2026-10-14T09:04:39Z

+our goal then becomes to prove the following statements in parallel:
+
+1. $verify'_0([comm(bb(x)), c_0]; [pi, r]) = 1$
+2. $verify'_1([comm2(bb(x)), c_1]; [pi, r]) = 1$
+3. $exists pi, r: comm([pi, r]) = c_0 and comm2([pi, r]) = c_1$


This doesn't flow right for me just yet. At this point we have just introduced $v'_i$ as taking one more argument than $v_i$ (but haven't bound it to anything). As a result, step 3 feels useless: we have to ensure the commitments given to both $v'_i$ match the same thing. But both $v'_i$ don't actually do anything with that parameter at this point?

Perhaps we should start with

$v_0(x, [\pi, r]) = 1$

$v_1(x, [\pi', r']) = 1$

show that $(\pi, r) = (\pi', r')$

then introduce $v'_b([x, s], [\pi, r]) = v_b(x, [\pi, r]) = 1 \wedge comm_b(x, \pi, r) = s$

and then transition to

$v' _0([x, s0], [\pi, r]) = 1$

$v'_1([x, s1], [\pi', r']) = 1$

$\exists \pi, r: comm_0(x, pi, r) = s0 \wedge comm_1(x, pi, r) = s1$

wdyt?

but haven't bound it to anything

I felt like that was implied by the (informal) definition of the v'_b, and that elaborating that more formally would needlessly take up extra space.

erik-3milabs · 2026-10-14T09:09:12Z

+#aside[Minimizing the length of $z$][
+  A larger $[pi, r]$ comes at a cost --- whether a cost of soundness or a cost of deriving more independent random $alpha_i$ ---
+  and as such should be kept as short as possible.
+  Since values that only one $verify^*_(b)$ reads or writes cannot lead to a differing result, the checksummed data need only


Clarify what you mean by "differing result". What result?

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

…d in notation

First split-proving draft

3c524d0

RobinJadoul requested a review from erik-3milabs October 13, 2026 16:17

RobinJadoul self-assigned this Oct 13, 2026

RobinJadoul added the spec Updates and improvements to the spec document label Oct 13, 2026

erik-3milabs reviewed Oct 14, 2026

View reviewed changes

Update split proving base description

1032e51

RobinJadoul requested a review from erik-3milabs October 16, 2026 14:54

Add reordering remark to aside

30080f2

erik-3milabs approved these changes Oct 19, 2026

View reviewed changes

Comment thread spec/chapters/recursion.typ Outdated

Update spec/chapters/recursion.typ

1303a25

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

erik-3milabs self-requested a review October 19, 2026 12:47

Try to keep the split recursion section intact without getting floode…

acf107a

…d in notation

	If we write $verify'_(b)([c_x, c_w]; w)$ to be an adaptation of $verify_(b)(c_x; w)$ that additionally gives has a public commitment to the private witness,#footnote[
	If we write $verify'_(b)([c_x, c_w]; w)$ to be an adaptation of $verify_(b)(c_x; w)$ that is additionally given a public commitment to the private witness,#footnote[

	(e.g. representing $pi$ as a sequence of committed bytes and as a sequence of extension field elemens),
	(e.g. representing $pi$ as a sequence of committed bytes and as a sequence of extension field elements),

	be the subsequence of elements of $[pi, r]$ that is read or written by both $verify^_0$ and $verify^_1$.
	be the subsequence of elements of $[pi, r]$ that is accessed by both $verify^_0$ and $verify^_1$.

		To enable recursion from a split verifier, we start by considering that each part of the split may
		be prove in a different proof system, and with a different commitment scheme.

		For a split verifier $(verify_0, verify_1, d_verify)$ to be recursively proven,
		we will write $comm(x)$ and $comm2(x)$ as the (deterministic) commitments to $x$

	For a split verifier $(verify_0, verify_1, d_verify)$ to be recursively proven,
	we will write $comm(x)$ and $comm2(x)$ as the (deterministic) commitments to $x$
	We write $comm(x)$ and $comm2(x)$ as the (deterministic) commitments to $x$

Conversation

RobinJadoul commented Oct 13, 2026

Uh oh!

github-actions Bot commented Oct 13, 2026

Kimi Code Review

Uh oh!

github-actions Bot commented Oct 13, 2026

Codex Code Review

Uh oh!

erik-3milabs 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!

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!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants