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

erik-3milabs

This is the core comment of this review.

erik-3milabs · 2026-10-23T06:33:01Z

+we will write $comm(x)$ and $comm2(x)$ for a (deterministic) commitment to $x$
+in the $prove_0$ and $prove_1$ scheme respectively.
+
+To then coherently prove the original verifier $verify$, our goal becomes:


Suggested change

To then coherently prove the original verifier $verify$, our goal becomes:

To then coherently prove the original verifier $verify$, our goal becomes to prove that:

erik-3milabs · 2026-10-23T06:35:25Z

+- $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.
+
+Finally, we consider the instantiation $serif("chsum")(x) = chevron.l x, z chevron.r$ for a random zero-evader $z$.


Suggested change

Finally, we consider the instantiation $serif("chsum")(x) = chevron.l x, z chevron.r$ for a random zero-evader $z$.

Finally, we consider the instantiation $serif("cksum")(x) = chevron.l x, z chevron.r$ for a random zero-evader $z$.

erik-3milabs · 2026-10-23T06:39:04Z

+The former has a soundness loss linear in the size of $x$, while the latter will require more computational
+work to derive independent challenges inside of the verifier.
+As a tradeoff, one could consider the mixture of both, through 
+$z = (alpha_1, alpha_1^2, ..., alpha_1^ell, alpha_2, alpha_2^2, ..., alpha_(lr(|x|)/ell)^ell)$, with a soundness loss $ell$ but only


re:

... with a soundness loss $ell$ ...

is this $ell$ bits? or bits linear in $ell$? Or something else? The absence of a unit is a touch confusing to me.

Maybe "soundness error $\frac\ell{|\mathbf{F}|}$ is more clear

erik-3milabs · 2026-10-23T06:47:11Z

+As such, it is possible to construct a split verifier for this combined proof system, and enable full split recursion.
+
+= Split recursion
 With proof recursion and split verification formalized, we now combine both concepts into a unified system.


Suggested change

With proof recursion and split verification formalized, we now combine both concepts into a unified system.

With proof recursion, split proving, and split verification formalized, we now combine the three concepts into a unified system.

erik-3milabs · 2026-10-23T08:31:14Z

+We consider the case for a valid split verifier $(verify_0, verify_1, d_verify)$
+with proof functions $prove_0$ and $prove_1$.
+Since these proof systems can potentially use different commitments,
+we will write $comm(x)$ and $comm2(x)$ for a (deterministic) commitment to $x$


This overloads $\stackrel{-}{x}$.

I think this is a problem. Later on, you write

With the right choice of proof system and commitment scheme $comm(x)$, ...

I think you want this to convey that $\stackrel{-}{x} := (\stackrel{-}{x}, \hat{x})$. The recursive definition might stump the reader, right at a crucial step that already requires some mental gymnastics to understand.

erik-3milabs · 2026-10-23T12:23:35Z


 = Split proving
-#et("todo")
+To enable recursion with a split verifier, we start by considering that each part of the split may


We don't need split proving to achieve recursion w/ a split verifier.

Suggested change

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

To accelerate recursion with a split verifier, we now discuss how each part of the split may

erik-3milabs · 2026-10-26T08:37:58Z

+We briefly present a few trivial instantiations, before bringing the cost down further.
+
+- $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.


$v^*_b$ is not defined.

erik-3milabs · 2026-10-26T13:34:04Z

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


Why are we suddenly talking about witness and using $w$, rather than proof and $\pi$?

erik-3milabs · 2026-10-26T13:42:48Z

+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 $proof$ as a sequence of committed bytes and as a sequence of extension field elements),
+one can even use a permutation argument such as in @logup to check equality of the data.


This subsection starts as

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

These sentences here related to a different situation, namely that of a single proof system. Yet, below, (after the aside) we continue with the split proof system discussion.

So, either:

we don't start by considering [...], but we just consider [...] (and these sentences are superfluous), or

we do in fact start with a split proof system, and this is a return to the joint proof system (which would be a weird order. Why not start with this?), but then the next paragraph should be moved up above here.

It is even different, and I don't get it.

Maybe s/considering/realizing at the start?
The start is justifying why we're introducing two potentially distinct proof systems into the discussion, whereas this sentence is clarifying what can we can do if they are not distinct.

erik-3milabs · 2026-10-26T14:04:26Z

-We can now use this selector to define $verify^*$ --- a variation to $verify'$ --- as follows:
+We can now use this selector to define $verify^*$ as a variation on $verify'$.
+With the right choice of proof system and commitment scheme $comm(x)$, $verify'$ and by extension
+$verify^*$ can be applied directly to a proof string $pi$ that is either the output of a base proof,
+or a recursive proof that is potentially split as in the previous section.


I have given it some thought, and think I know why this doesn't work as we would like it to: the split-proving section is missing some stuff.

The story up to this point has been:

we start this chapter with introducing recursion,

we bypass a growing instance, by introducing $v'$,

split verification: we show how to convert a verifier into a split verifier.

split proving: we show how to accelerate a split verifier by means of proving each split in different VMs

I would now expect this section to combine $v'$ and split-verification+split-proving. But that doesn't happen.

In fact, we don't yet have the tools to do this: the $v'$-transformation shows how to morph the verifier of a proof system $(p,v)$ into one that can prove that one of two instances is satisfied. In the split proving section, we just pull two proof system provers p0 and p1 out of thin air and don't introduce the accompanying verifiers $v0$ and $v1$ (note: I'm overloading notation here). Neither do we show how one can merge $v0$ and $v1$ into the single verifier $V$ (that can verify proofs that consist of two halves from different proof systems).

Only once we have established those things, can we

apply the $v'$ transformation to $V$ (allowing it to verify two instances), creating $V'$, and

then split $V'$ into $(V_0', V_1', d_{V'})$

before we arrive at a split verifier that can verify proofs for two instances using two verifiers proven by two distinct provers.

Right now, we're essentially asking the reader to take all those mental steps in these two sentences. That is too much.

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 Resolved

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

erik-3milabs reviewed Oct 26, 2026

View reviewed changes

	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$

	To then coherently prove the original verifier $verify$, our goal becomes:
	To then coherently prove the original verifier $verify$, our goal becomes to prove that:

	Finally, we consider the instantiation $serif("chsum")(x) = chevron.l x, z chevron.r$ for a random zero-evader $z$.
	Finally, we consider the instantiation $serif("cksum")(x) = chevron.l x, z chevron.r$ for a random zero-evader $z$.

	With proof recursion and split verification formalized, we now combine both concepts into a unified system.
	With proof recursion, split proving, and split verification formalized, we now combine the three concepts into a unified system.

	To enable recursion with a split verifier, we start by considering that each part of the split may
	To accelerate recursion with a split verifier, we now discuss how each part of the split may

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

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!

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!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants