From 3c524d0d303681cd5902006d535c34cbcefd5a6a Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 13 Oct 2026 18:15:48 +0200 Subject: [PATCH 1/5] First split-proving draft --- spec/chapters/recursion.typ | 57 +++++++++++++++++++++++++++++++++++-- 1 file changed, 54 insertions(+), 3 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 68e3c104b..499296f40 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -1,4 +1,4 @@ -#import "/meta.typ": et, aside +#import "/meta.typ": et, aside, rj // Spaces and instances #let (programSpace, program) = ($cal(F)$, $f$) @@ -10,6 +10,7 @@ #let (commitmentSpace, commitment) = ($cal(C)$, $bb(c)$) #let commit(x) = $dash(#x)$ #let comm(x) = $commit(#x)$ +#let comm2(x) = $hat(#x)$ #let hash = $H$ @@ -238,9 +239,59 @@ The produced proof $proof'$ now attests to $instance in language$ when $verify(comm(product(verify_0, verify_1)(comm(instance), dot)), proof') = 1$. = Split proving -#et("todo") +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$ +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[ + In practice for most proof systems, this is already available. + For a proof system where it is not available, we let $verify'_(b)$ explicitly verify that this relation holds. +] +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$ + +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). $ +The choice of checksum function, in turn, can depend on the choice of proof systems. +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. + 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$. + +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. +If the proof systems for the split verifier work over different fields, field emulation would need to happen on one side, with the other using native arithmetic, +or both sides could target a common target field that is simpler to emulate in both.#footnote[ + In a practical implementation with flock and the lambda proof system side by side, an inner product in the goldilocks extension field should + be possible in a repetitive binary circuit that fits well in flock's model. +] +Choices for the structure of $z$ include $z = (alpha_1, alpha_2, alpha_3, ..., alpha_(|x|))$, $z = (1, alpha, alpha^2, ..., alpha^(|x| - 1))$ +or even $z = (alpha_1, alpha_1^2, ..., alpha_1^ell, alpha_2, alpha_2^2, ..., alpha_(lr(|x|)/ell)^ell)$, depending on tradeoffs between +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), +one can even use a permutation argument such as in @logup to check equality of the data. + +#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 + be the subsequence of elements of $[pi, r]$ that is read or written by both $verify^*_0$ and $verify^*_1$. +] +#rj[Define these as "a recursion split of $verify$" somehow to avoid more notation pain down below?] -= Split-recursion += Split recursion +#rj[Update everything below to match differing commitments] With proof recursion and split verification formalized, we now combine both concepts into a unified system. To this end, we first introduce the selector function $ From 1032e5178eb557880f4f64c13c7c99e46a07dd6f Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 16 Oct 2026 16:54:09 +0200 Subject: [PATCH 2/5] Update split proving base description --- spec/chapters/recursion.typ | 76 ++++++++++++++++++++----------------- 1 file changed, 42 insertions(+), 34 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 499296f40..106ba0130 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -45,7 +45,7 @@ This relation induces the language $language subset.eq instanceSpace$ of _solvab where $instance in language$ if there exists a witness $witness$ for which $(instance, witness)in relation$. Lastly, we introduce the instance commitment function $c: instanceSpace to commitmentSpace$. -Note that this commitment scheme does not involve randomness; it is a _determistic_ scheme. +Note that this commitment scheme does not involve randomness; it is a _deterministic_ scheme. Randomness is typically required to make a commitment _hiding_. For the purposes of this discussion, we are not concerned with this property, as the function will only be used for committing to public information. @@ -101,7 +101,7 @@ This increase in verifier computation is undesirable and should be avoided. A solution to this, is to leverage the following variation to the verification algorithm: $ verify': commitmentSpace^2 times proofSpace: ([comm(x), comm(y)], proof) mapsto - verify(comm(x), proof) or verify(comm(y([comm(x), comm(y)], dot)), proof) + verify(comm(x), proof) or verify(comm(y([comm(x), comm(y)], dot)), proof), $ where it is assumed that $comm(y([comm(x), comm(y)], dot)) in commitmentSpace$ can be constructed efficiently from $comm(x), comm(y) in commitmentSpace$. Now observe that setting $(comm(x), comm(y)) = (commit(instance), commit(verify'))$ yields @@ -114,7 +114,7 @@ a) proof of $instance in language$, or b) proof of _the existence of a (different) proof_ that satisfies $verify'([comm(instance), comm(verify')], dot)$. We can now recursively expand the expression, yielding $ - verify'(commit(instance), commit(verify'), proof) + verify'([commit(instance), commit(verify')], proof) &= verify(comm(instance), proof) or verify(comm(verify'([comm(instance), comm(verify')], dot)), proof)\ &= verify(comm(instance), proof) or verify(comm(verify(comm(instance), dot) or verify(comm(verify'([comm(instance), comm(verify')]; dot)), dot)), proof)\ &= verify(comm(instance), proof) or verify(comm(verify(comm(instance), dot) or verify(comm(verify(comm(instance), dot) or verify(comm(verify'([comm(instance), comm(verify')], dot)), dot)), dot)), proof)\ @@ -239,59 +239,67 @@ The produced proof $proof'$ now attests to $instance in language$ when $verify(comm(product(verify_0, verify_1)(comm(instance), dot)), proof') = 1$. = Split proving -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$ -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[ - In practice for most proof systems, this is already available. - For a proof system where it is not available, we let $verify'_(b)$ explicitly verify that this relation holds. -] -our goal then becomes to prove the following statements in parallel: +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. +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$ +in the $prove_0$ and $prove_1$ scheme respectively. + +To then coherently prove the original verifier $verify$, our goal becomes: -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$ +1. $verify_0(comm(bb(x)), [proof_0, record_0]) = 1$ +2. $verify_1(comm2(bb(x)), [proof_1, record_1]) = 1$ +3. $[proof_0, record_0] = [proof_1, record_1]$ -The first two statements would follow naturally from proving $verify_(b)$ or the derived $verify'_(b)$. +The first two statements would follow naturally from proving the evaluation of $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). $ +$ verify'_(b)([x, s], w) = verify_(b)(x, w) dot (serif("cksum")(w) =^? s). $ The choice of checksum function, in turn, can depend on the choice of proof systems. 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. - 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$. 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 +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. +In either case, $z$ should not be known to the (recursion) prover before being bound to both $[proof_b, record_b]$ pairs used. If the proof systems for the split verifier work over different fields, field emulation would need to happen on one side, with the other using native arithmetic, -or both sides could target a common target field that is simpler to emulate in both.#footnote[ +or both sides could work in a common target field that is simpler to emulate in both.#footnote[ In a practical implementation with flock and the lambda proof system side by side, an inner product in the goldilocks extension field should be possible in a repetitive binary circuit that fits well in flock's model. ] -Choices for the structure of $z$ include $z = (alpha_1, alpha_2, alpha_3, ..., alpha_(|x|))$, $z = (1, alpha, alpha^2, ..., alpha^(|x| - 1))$ -or even $z = (alpha_1, alpha_1^2, ..., alpha_1^ell, alpha_2, alpha_2^2, ..., alpha_(lr(|x|)/ell)^ell)$, depending on tradeoffs between -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), +Choices for the structure of $z$ include $z = (1, alpha, alpha^2, ..., alpha^(lr(|x|) - 1))$ and $z = (alpha_1, alpha_2, alpha_3, ..., alpha_(|x|))$. +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 +$lr(|x|)/ell$ independent challenges to derive. +To avoid having to prove the derivation of the random challenges, they can be made into a public input.#footnote[ + This requires a succinct description of $z$ (e.g. the single value $alpha$), as otherwise the shrinking + effect of providing $proof$ as private witness is lost. +] +Where needed, multiple independent inner products can be used to amplify soundness. +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. #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$ --- + A larger $[proof, record]$ 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$. + Since values that only one $verify'_(b)$ accesses do not influence $verify'_(1-b)$, the checksummed data need only + be the subsequence of elements of $[proof, record]$ that is accessed by both $verify'_0$ and $verify'_1$. ] -#rj[Define these as "a recursion split of $verify$" somehow to avoid more notation pain down below?] + +Observe that considering considering the proof +$ proof_sans("rec") = s || prove_0(verify'_0([comm(x), s], dot); [proof, record]) || prove_1(verify'_1([comm2(x), s], dot); [proof, record]) $ +still allows us to treat the final output as a single proof, with a well-defined verifier. +As such, it is possible to construct a split verifier for this combined proof system, and enable full split recursion. = Split recursion -#rj[Update everything below to match differing commitments] +#rj[Update everything below to match differing commitments (still needed if we're unifying above?)] With proof recursion and split verification formalized, we now combine both concepts into a unified system. To this end, we first introduce the selector function $ From 30080f2d237c5bd81ae1387526e5d41dd45c0bdc Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 19 Oct 2026 11:39:10 +0200 Subject: [PATCH 3/5] Add reordering remark to aside --- spec/chapters/recursion.typ | 3 +++ 1 file changed, 3 insertions(+) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 106ba0130..ed145a7a3 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -291,6 +291,9 @@ one can even use a permutation argument such as in @logup to check equality of t and as such should be kept as short as possible. Since values that only one $verify'_(b)$ accesses do not influence $verify'_(1-b)$, the checksummed data need only be the subsequence of elements of $[proof, record]$ that is accessed by both $verify'_0$ and $verify'_1$. + + An even stronger version of this additionally allows re-ordering of the elements of this subsequence, + so that one or both of the verifier halves can have a simpler structure or ordering of its checks. ] Observe that considering considering the proof From 1303a250c7b0bc75f5d30b3cefee22c4c072c7b3 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 19 Oct 2026 14:31:33 +0200 Subject: [PATCH 4/5] Update spec/chapters/recursion.typ Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/chapters/recursion.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index ed145a7a3..6059bfe96 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -296,7 +296,7 @@ one can even use a permutation argument such as in @logup to check equality of t so that one or both of the verifier halves can have a simpler structure or ordering of its checks. ] -Observe that considering considering the proof +Observe that considering the proof $ proof_sans("rec") = s || prove_0(verify'_0([comm(x), s], dot); [proof, record]) || prove_1(verify'_1([comm2(x), s], dot); [proof, record]) $ still allows us to treat the final output as a single proof, with a well-defined verifier. As such, it is possible to construct a split verifier for this combined proof system, and enable full split recursion. From acf107a831bce63b154c2a9b41dc11e4856a1ac6 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Thu, 22 Oct 2026 16:14:20 +0200 Subject: [PATCH 5/5] Try to keep the split recursion section intact without getting flooded in notation --- spec/assets/mathml_cleanup.js | 2 +- spec/chapters/recursion.typ | 11 +++++++---- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/spec/assets/mathml_cleanup.js b/spec/assets/mathml_cleanup.js index 33075c56d..e193a20d2 100644 --- a/spec/assets/mathml_cleanup.js +++ b/spec/assets/mathml_cleanup.js @@ -60,7 +60,7 @@ // Fix 3: Replace overlines with a border-top CSS rule for browsers that // do not stretch the top line properly. (e.g. chromium (and forks like Brave)) for (let elem of document.body.querySelectorAll("mover mo:last-child")) { - if (isOverline(elem.textContent) && elem.getBoundingClientRect().width < elem.parentElement.getBoundingClientRect().width * 0.9) { + if (isOverline(elem.textContent) && elem.getBoundingClientRect().width < elem.parentElement.getBoundingClientRect().width * 0.8) { elem.style.display = "none"; elem.parentElement.style.borderTop = "0.06em solid currentColor"; elem.parentElement.style.paddingTop = "0.12em"; diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 6059bfe96..c0a71e064 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -129,7 +129,7 @@ $(comm(instance), comm(verify'))$ is _constant_ in the depth of the recursion. In fact, the size of the verification instance is typically fully determined by $comm(instance)$, since $comm(verify')$ can often be precomputed. -#aside([Soundness])[ +#aside[Soundness][ It is important to note that soundness of this construction is not yet proven. 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$. @@ -137,7 +137,7 @@ $comm(instance)$, since $comm(verify')$ can often be precomputed. a recursion-level counter in the proof. ] -#aside([$comm(verify')$ absorption])[ +#aside[$comm(verify')$ absorption][ Note that $commit(verify')$ must be provided to $verify'$ as a _parameter_; absorbing it into $verify'$ would imply an object containing a cryptographic commitment of itself at a static location, which is practically impossible. @@ -302,7 +302,6 @@ still allows us to treat the final output as a single proof, with a well-defined As such, it is possible to construct a split verifier for this combined proof system, and enable full split recursion. = Split recursion -#rj[Update everything below to match differing commitments (still needed if we're unifying above?)] With proof recursion and split verification formalized, we now combine both concepts into a unified system. To this end, we first introduce the selector function $ @@ -310,7 +309,11 @@ $ $ which, given a bit $b in BB$ and two elements $x,y$ of some space $cal(A)$, selects an element based on the value of $b$. -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. + $ verify^*([comm(x), comm(y)], [proof, b]) :&= Delta_BB (verify(comm(x), proof), verify(comm(y([comm(x), comm(y)], dot)), proof), b)\