spec: Recursion

spec/book.typ

@@ -13,6 +13,7 @@
         ("logup.typ", [`LogUp` argument], <logup>),
         ("memory.typ", [Memory argument], <memory>),
         ("streaming.typ", [Streaming prover], <streaming>),
+        ("verifier.typ", [Verification], <verification>)
     )),
     ("OVERVIEW", (
         ("variables.typ", [Variables], <vars>),
@@ -55,6 +56,11 @@
       ("ecsm.typ", [`ECSM` accelerator], <ecsm>),
       ("fext.typ", [Extension field accelerator], <fext>),
     )),
+    ("RECURSION", (
+      ("recursion.typ", [Recursive verification], <recursion>),
+      ("field.typ", [`Field` VM], <field-VM>),
+      ("field_decode.typ", [`Field` `DECODE` table], <field-decode>),
+    )),
     ("MATHEMATICS", (
       ("limbs_and_carries.typ", [On limb decomposition and carries], <limbs>),
     ))

spec/field.typ

@@ -0,0 +1,5 @@
+#import "/book.typ": book-page
+
+#show: book-page("field.typ")
+
+TODO

spec/field_decode.typ

@@ -0,0 +1,5 @@
+#import "/book.typ": book-page
+
+#show: book-page("field_decode.typ")
+
+TODO

spec/recursion.typ

@@ -0,0 +1,260 @@
+#import "/book.typ": book-page, et, aside
+
+#show: book-page("recursion.typ")
+
+// Spaces and instances
+#let (programSpace, program) = ($cal(F)$, $f$)
+#let (inputSpace, input) = ($II$, $bb(i)$)
+#let (instanceSpace, instance) = ($XX$, $bb(x)$)
+#let (witnessSpace, witness) = ($WW$, $bb(w)$)
+#let (proofSpace, proof) = ($bb(Pi)$, $pi$)
+
+#let (commitmentSpace, commitment) = ($cal(C)$, $bb(c)$)
+#let commit(x) = $overline(#x)$
+#let comm(x) = $commit(#x)$
+
+#let relation = $cal(R)$
+#let language = $cal(L)$
+
+#let verifierSpace = $cal(V)$
+#let (prove, verify) = ($italic("p")$, $italic("v")$)
+
+// Mathematical symbols
+#let (zero, one) = ($0$, $1$)
+#let iff = $arrow.double.l.r$
+#let implies = $arrow.double.r$
+#let prob = $PP$
+#let to = math.arrow.r
+
+#show math.equation.where(block: false): box
+
+= Notation
+Let $BB := { zero, one }$ denote the boolean set and let 
+$programSpace := {program: inputSpace times witnessSpace to BB}$ denote 
+the set of functions mapping the (public) input space $inputSpace$ and (private) 
+witness space $witnessSpace$ to this set.
+We define instance space $instanceSpace := programSpace times inputSpace = {program: witnessSpace to BB}$;
+program-input pairs $(program, input) in instanceSpace$ 
+are henceforth referred to as _function instances_, or simply _instances_.
+Where the individual components of the pair are irrelevant, an instance is 
+denoted as $instance in instanceSpace$.
+
+We define relation $relation subset instanceSpace times witnessSpace$ where $((program, input), witness) in relation$ if $program(input, witness) = 1$.
+This relation induces the language $language subset instanceSpace$ of _solvable instances_,
+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.
+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. 
+To simplify notation, we henceforth use $commit(instance)$ to represent the commitment $c(instance)$ of $instance$.
+
+We now assume the existence of _proof system_ $(prove, verify)$ with 
+prover $prove: instanceSpace times witnessSpace to proofSpace$ and 
+verifier $verify: commitmentSpace times proofSpace to BB$ that is both
+_complete_ --- i.e., $verify$ accepts all valid proofs generated by $prove$ --- 
+and _sound_ --- i.e., one cannot create an acceptable proof for an unsolvable instance.
+
+Translating this to the purposes of this VM, a prover wishes to convince the verifier 
+that for some agreed upon program ($program in programSpace$) and specified public input ($input in inputSpace$),
+they know a private input ($witness in witnessSpace$) such that the program terminates successfully 
+(i.e., $(program, input) in language$).
+To this end, the prover uses $prove(program(input; dot); witness)$ 
+to construct some proof $proof in proofSpace$ and sends this to the verifier.
+They then use $verify(comm(program(input; dot)), proof)$ to check that the proof is valid, 
+convincing them of the prover's claim.
+
+= Proof recursion
+Now observe that the verifier $verify$ is itself a function in 
+$verifierSpace := {hat(f): commitmentSpace times proofSpace to BB} subset.eq programSpace$.
+This means that we can use $prove$ to prove that the verification of a proof $proof$ 
+for a given instance $instance$ succeeds:
+$
+  &prove(verify(comm(instance), dot); proof) = proof', text("and")
+  &verify(comm(verify(comm(instance), dot)), proof') = one.
+$
+This new proof $proof'$ thus attests to _the existence of a proof $proof$ that 
+satisfies the verifier on the given instance $instance$_.
+
+This concept, colloquially known as _proof recursion_, can be applied repeatedly.
+The technique is specifically beneficial for _succinct_ proving systems where proof size
+typically shrinks (and verification time reduces) as the level of recursion increases.
+The technique is mostly useful in settings where the extra time spent by the prover
+is outweighed by the time saved by the verifier(s), 
+e.g., a computationally constrained verifier, or multiple verifiers.
+
+= Resolving growing instance complexity
+While recursive proving leads to a decrease in proof size, this is naively traded off
+against an increase in instance complexity.
+Looking at a depth-two recursive proof,
+$
+  prove(verify(comm(verify(comm(instance), dot)), dot); proof') = proof'', text("and")
+  verify(comm(verify(comm(verify(comm(instance), dot)), dot)), proof'') = one
+$
+we see that the verifier first has to derive the commitment
+$comm(verify(comm(verify(comm(instance), dot)), dot))$
+from the given base instance $instance$ before verifying the proof.
+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 {0, 1} times proofSpace: (overline(r), overline(s), b, proof) mapsto
+  cases(
+    verify(overline(r), proof) &text("if") b=0,
+    verify(overline(s(overline(r), overline(s); dot)), proof) &text("if") b=1,
+  )
+$
+where it is assumed that $overline(s(overline(r), overline(s); dot)) in commitmentSpace$ can efficiently be constructed from $(overline(r), overline(s)) in commitmentSpace^2$.
+Now observe that
+$
+  verify'(comm(instance), comm(verify'), 0, proof) &= verify(comm(instance), proof), text("and")\
+  verify'(comm(instance), comm(verify'), 1, proof) &= verify(comm(verify'((comm(instance), comm(verify')); dot)), proof).
+$
+
+In other words, by setting $(commitment_0, commitment_1) = (commit(instance), commit(verify'))$,
+this algorithm can verify a base proof by choosing $b=0$ or a recursive proof when selecting $b=1$.
+Importantly, the verification of some proof $proof$ using $verify'(comm(instance), comm(verify'), 1, dot)$ 
+succeeds only if the prover has used $verify'$ at every step in the proof recursion.
+This fact is illustrated by the following expansion:
+$
+  verify'(commit(instance), commit(verify'), 1, proof^((n)))
+  &= verify(comm(verify'(commit(instance), commit(verify'), dot)), proof^((n)))\
+  &= verify(comm(verify(comm(verify'(comm(instance), comm(verify'), dot)), dot)), proof^((n)))\
+  &= verify(comm(verify(comm(verify(comm(verify'(comm(instance), comm(verify'), dot)), dot)), dot)), proof^((n)))\
+  &= verify(comm(verify(comm(verify(comm(dots.c (comm(verify(comm(instance), dot) dots.c))), dot)), dot)), proof^((n)))\
+$
+Hence, a recursive proof based on $verify'$ attests that $verify'$ was the
+only algorithm used throughout the entire recursion stack.
+
+Lastly, note that the verification of a recursive proof $proof^((n))$ only 
+depends on $comm(instance)$, since $comm(verify')$ can be precomputed.
+We have thus established a recursive proving system that only requires the base
+instance as input to the verification of a recursive proof.
+
+#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, 
+which is theoretically impossible.
+]
+
+#et("illustrate that there comes a termination point, i.e., a proof cannot prove itself.")
+#et("note shakiness of recursion")
+
+= Split processing
+#let record = $bb(r)$
+In practice, we find that the set of operations utilized for verification differs vastly from
+those typically performed by guest programs.
+Specifically, verification primarily involves hashing and (extension) field arithmetic, 
+where especially the second is absent in typical guest programs.
+
+Emulating field arithmetic on a binary arithmetic-oriented VM, typically
+incurs significant computational overhead.
+With the aim of avoiding this performance penalty, we introduce a field 
+arithmetic-oriented mini-VM (henceforth referred to as the _field-VM_),
+which will act as a _co-processor_ to the established _binary-VM_.
+Since both VMs are proven using the same proof system, a unified proof can be 
+produced for the parallel execution of both VMs.
+
+The introduction of this split allows the verification algorithm to be split in two halves,
+with each VM performing the computations it is fastest at.
+The two halves cannot work independently, however.
+In the process of verifying proofs of the current proof system (`DEEP-FRI` + `LogUp`),
+results of binary arithmetic are used to verify field arithmetical constraints 
+--- e.g., field challenges extracted from binary hash outputs --- 
+and vice-versa --- e.g., hashing merkle leafs containing field elements during FRI-query proof verification.
+This implies that some form of communication between both VMs is required.
+
+Our architecture enables the required communications by introducing a 
+prover-hinted _communication record_ $record$ accessible to both VMs.
+In practice, this record will primarily contain values being reinterpreted 
+--- from $FF$ to $ZZ_(2^64)$ and vice-versa --- during verification.
+The two halves of the split verification algorithm are adapted to leverage
+the record: for each value on the record, one of the VMs _verifies_ the value to be correct, 
+while the other _assumes_ its correctness and resumes verification under this assumption.
+
+To ensure correct verification, both verification-algorithm halves must align
+on the interpretation of each value on the proof-record pair.
+To this end, the dimensions of the record must be determined at _verification algorithm design-time_ 
+and parametrized in terms of the proof only.
+Then, both verification algorithm halves can be given the same logic to interpret the record, 
+effectively synchronizing their interpretation.
+
+#aside("Coupling")[
+  As observed, both verification halves must be synchronized to correctly verify a proof.
+  This implies that some coupling between both halves must exist.
+  This design utilizes little coupling in the VM design, instead forcing 
+  the guest programs to solve synchronization, as a result introducing the coupling there. 
+
+  This no-coupling VM design permits one of the two halves to transition to a 
+  different proof system (e.g., moving to Flock 
+  #footnote(link(
+    "https://eprint.iacr.org/2026/1329", 
+    "Flock: Fast Proving for Batch Boolean Computations. src: https://eprint.iacr.org/2026/1329"
+  )) 
+  to accelerate hash-verification) while incurring as little design overhead as possible.
+]
+
+In theory, any division of tasks between the two VMs would work.
+Moreover, it is unclear what division will lead to optimal performance.
+Yet, it is expected that divisions adhering to these high-level guidelines will 
+be a good first step towards a performant verifier:
++ have the field-VM perform all verification steps involving field arithmetic,
++ include all verifier-issued challenges required by these verification steps 
+  in the communication record $record$ as field-elements, so that the field-VM does not have to derive them,
++ use the binary-VM to verify the challenges hinted by the communication record are indeed correct.
+
+= Recursive proving and split processing
+We lastly provide some notes on applying the recursive proving and split processing to
+the verification of a proof in the context of this VM.
+
+First, we note that in any scenario, the prover has to commit to the program $program$
+being exeucted and the public input $input$ that is provided.
+In a non-recursive proof, this is trivially done by committing to the `DECODE` table
+representing $program$, and the `PAGE` tables storing the public $input$.
+Since these commitments are deterministic, the verifier can locally reconstruct
+the commitments and verify any opening proofs against its own version of the commitment.
+Note that in this case, the prover may exclude the opened value from any proof strings
+pertaining to the `DECODE` and `PAGE` tables, as these are already known to the verifier.
+
+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)
+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.
+
+Denoted as pseudo-algorithms, we find:
+
+#set list(marker: [---])
+*Communication record overview:*
+- the data required according to the chosen verification split,
+- if $b=1$, reconstructed commitment $comm(verify'(comm(instance), comm(verify'); dot))$
+
+*$verify'_b\(comm(instance), (comm(verify'_b), comm(verify'_f)), b, proof, record)$:*
+- `COMMIT` to $comm(instance)$, $comm(verify'_b),$ and $comm(verify'_f)$ 
+- assert that $b in {0, 1}$,
+- verify proof:
+  - if $b=0$: execute $verify_b (comm(instance), proof)$
+  - if $b=1$:
+    + construct $comm(verify'(comm(instance), comm(verify'); dot))$ from $(comm(instance), (comm(verify'_b), comm(verify'_f)))$
+    + 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)$
+  - if $b=1$, use $comm(instance), comm(verify'_b), comm(verify'_f)$ to complete the `COMMIT` LogUp-balance.
+
+*Prover:*
+$
+  proof &arrow.l prove(instance, witness)\
+  proof' &arrow.l prove(verify'_b || verify'_f, (commit(instance), (commit(verify'_b), commit(verify'_f)), 0, proof, record))\
+  proof^((i)) &arrow.l prove(verify'_b || verify'_f, (commit(instance), (commit(verify'_b), commit(verify'_f)), 1, proof^((i-1)), record))
+$
+
+*Final verification.*
+$verify'(commit(instance), (commit(verify'_b), commit(verify'_f)), 1, proof^((n))) =^? one$

spec/verifier.typ

@@ -0,0 +1,8 @@
+#import "/book.typ": book-page
+
+#show: book-page("verifier.typ")
+
+// TODO:
+// - sigma protocol, layout the various steps
+// - Fiat Shamir transformation into non-interactive protocol.
+//