From 187edc3c088bb8bf2ba8aafeaf159a8e981e3fda Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 14 Aug 2026 12:31:56 +0200 Subject: [PATCH 1/7] spec: recursive verification explanation, pt1 --- spec/book.typ | 5 + spec/field.typ | 5 + spec/field_decode.typ | 5 + spec/figures/DEEP-FRI_verification.md | 32 ++ spec/figures/DEEP-FRI_verification.svg | 1 + spec/recursion.typ | 461 +++++++++++++++++++++++++ 6 files changed, 509 insertions(+) create mode 100644 spec/field.typ create mode 100644 spec/field_decode.typ create mode 100644 spec/figures/DEEP-FRI_verification.md create mode 100644 spec/figures/DEEP-FRI_verification.svg create mode 100644 spec/recursion.typ diff --git a/spec/book.typ b/spec/book.typ index 052f134bd..97f58882d 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -55,6 +55,11 @@ ("ecsm.typ", [`ECSM` accelerator], ), ("fext.typ", [Extension field accelerator], ), )), + ("RECURSION", ( + ("recursion.typ", [Recursive verification], ), + ("field.typ", [`Field` VM], ), + ("field_decode.typ", [`Field` `DECODE` table], ), + )), ("MATHEMATICS", ( ("limbs_and_carries.typ", [On limb decomposition and carries], ), )) diff --git a/spec/field.typ b/spec/field.typ new file mode 100644 index 000000000..a8ae3058d --- /dev/null +++ b/spec/field.typ @@ -0,0 +1,5 @@ +#import "/book.typ": book-page + +#show: book-page("field.typ") + +TODO \ No newline at end of file diff --git a/spec/field_decode.typ b/spec/field_decode.typ new file mode 100644 index 000000000..4e83287df --- /dev/null +++ b/spec/field_decode.typ @@ -0,0 +1,5 @@ +#import "/book.typ": book-page + +#show: book-page("field_decode.typ") + +TODO \ No newline at end of file diff --git a/spec/figures/DEEP-FRI_verification.md b/spec/figures/DEEP-FRI_verification.md new file mode 100644 index 000000000..5a80c5cdf --- /dev/null +++ b/spec/figures/DEEP-FRI_verification.md @@ -0,0 +1,32 @@ + + +title Proof verification +note over P,V: established: shared program with\npublic input +note over P: fill tables +P->V: batch-commit tables +group par [DEEP] +P<-V: lincomb challenges +P->V: quotient commitment +P<-V: segment challenges +P->V: segment commitment +P<-V: DEEP point +P->V: DEEP openings +else LogUp +P<-V: LogUp challenges +P->V: batch-commit to LogUp columns +P->V: open sum entries +note over V: checksum +end + +P->V: batch FRI-commit (implicitly) +loop Batch-FRI +P<-V: folding challenge +P->V: folding commitment +end +P->V: FRI low-degree output +note over V: verify low-degreeness +loop FRI-verify +P<-V: FRI-opening challenge +P->V: opening +note over V: verify opening +end \ No newline at end of file diff --git a/spec/figures/DEEP-FRI_verification.svg b/spec/figures/DEEP-FRI_verification.svg new file mode 100644 index 000000000..6adf58fd0 --- /dev/null +++ b/spec/figures/DEEP-FRI_verification.svg @@ -0,0 +1 @@ +title%20Proof%20verification%0Anote%20over%20P%2CV%3A%20established%3A%20shared%20program%20with%5Cnpublic%20input%0Anote%20over%20P%3A%20fill%20tables%0AP-%3EV%3A%20batch-commit%20tables%0Agroup%20par%20%5BDEEP%5D%0AP%3C-V%3A%20lincomb%20challenges%0AP-%3EV%3A%20quotient%20commitment%0AP%3C-V%3A%20segment%20challenges%0AP-%3EV%3A%20segment%20commitment%0AP%3C-V%3A%20DEEP%20point%0AP-%3EV%3A%20DEEP%20openings%0Aelse%20LogUp%0AP%3C-V%3A%20LogUp%20challenges%0AP-%3EV%3A%20batch-commit%20to%20LogUp%20columns%0AP-%3EV%3A%20open%20sum%20entries%0Anote%20over%20V%3A%20checksum%0Aend%0A%0AP-%3EV%3A%20batch%20FRI-commit%0Aloop%20Batch-FRI%0AP%3C-V%3A%20folding%20challenge%0AP-%3EV%3A%20folding%20commitment%0Aend%0AP-%3EV%3A%20FRI%20low-degree%20output%0Anote%20over%20V%3A%20verify%20low-degreeness%0Aloop%20FRI-verify%0AP%3C-V%3A%20FRI-opening%20challenge%0AP-%3EV%3A%20opening%0Anote%20over%20V%3A%20verify%20opening%0AendPVProof verificationestablished: shared program withpublic inputfill tablesbatch-commit tableslincomb challengesquotient commitmentsegment challengessegment commitmentDEEP pointDEEP openingsLogUp challengesbatch-commit to LogUp columnsopen sum entrieschecksumbatch FRI-commit (implicitly)folding challengefolding commitmentFRI low-degree outputverify low-degreenessFRI-opening challengeopeningverify openingpar[DEEP][LogUp]loop[Batch-FRI]loop[FRI-verify] \ No newline at end of file diff --git a/spec/recursion.typ b/spec/recursion.typ new file mode 100644 index 000000000..5dc811b87 --- /dev/null +++ b/spec/recursion.typ @@ -0,0 +1,461 @@ +#import "/book.typ": book-page, et, aside + +#show: book-page("recursion.typ") + + +// Outline +#let binaryVM = raw("binaryVM") +#let fieldVM = raw("fieldVM") + + +#let functionSpace = $PP$ +#let program = $bb(p)$ +#let inputSpace = $II$ +#let input = $bb(i)$ +#let instanceSpace = $XX$ +#let instance = $bb(x)$ +#let instance2 = $bb(y)$ +#let witnessSpace = $WW$ +#let witness = $bb(w)$ +#let proofSpace = $bb(Pi)$ +#let proof = $bb(pi)$ +#let prove = $italic("p")$ +#let verify = $italic("v")$ +#let commit = $italic("c")$ +#let one = $bb(1)$ +#let zero = $bb(0)$ +#let function = $cal(F)$ +#let relation = $cal(R)$ + +#show math.equation.where(block: false): box + += Notation + +Let $functionSpace := {function: inputSpace times witnessSpace mapsto BB}$ denote the set of functions mapping input-witness pairs $(input; witness) in inputSpace times witnessSpace$ to a boolean ${ zero, one } in BB$. +Let relation $relation subset.eq functionSpace times inputSpace =: instanceSpace$ denote the set of all succesfully terminating program instances, i.e., all function-input instances $(program, input) in functionSpace times inputSpace$ for which there exists a witness $witness in witnessSpace$ such that $program\(input; witness) = one$. + +Let there furthermore exist _proving system_ $(prove, verify)$ with prover $prove in { function: instanceSpace times witnessSpace mapsto proofSpace }$ and verifier $verify in { function: instanceSpace times proofSpace mapsto BB}$ such that +$ +forall (instance, witness) in relation times witnessSpace &: PP[verify\(instance, prove\(instance; witness)) = one | instance(witness) = one] = 1 \ +forall instance in instanceSpace without relation, forall proof in proofSpace &: PP[verify\(instance, proof) = one] < epsilon +$ +with $epsilon$ negligibly small. +That is: any valid proof for a terminating program verifiers successfully, while the probability of any proof verifying a unsuccesfully-terminating program is negligible. + += Proof recursion +In our application, the prover wishes to convince the verifier that for some public program-input instance $instance = (program, input) in instanceSpace$ they know a private witness $witness in witnessSpace$ such that $program\(input; witness) = one$. +To this end, the prover uses $prove\(program, input; witness) = prove\(instance; witness)$ to generate proof $proof$ and sends this to the verifier. +They then use $verify(instance, proof)$ to check that the proof is valid, convincing them of the prover's claim. + +When we observe that $verify in functionSpace$, we can now let the prover compute $prove\(verify, instance; prove\(instance; witness)) = proof'$ and send this proof for the verifier to $verify((verify, instance), proof')$, proving that they _know a proof attesting that $instance$ is in the relation_. +This concept, colloquially known as _proof recursion_, can be applied recursively. +This is often beneficial for _succint_ proving systems where proof size (and verification time) typically shrinks 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. + +== Proof traceability +Importantly, the final recursive proof should be _tied_ to both the original instance $instance$, as well as the entire stack of verifiers used along the way. +Without this, the final verifier cannot verify that the received proof attests to the original claim. +We exemplify this in the following triple-nested example: +$ +&prove\([verify, instance'']; prove\([verify, instance']; prove\([verify, instance]; prove\(instance; witness))) = proof'''\ +&verify(instance''', proof''') in BB +$ +which requires $instance''' = [verify, instance''] = [verify, [verify, instance']] = [verify, [verify, [verify, instance]]]$: the original instance, as well as the full stack of verification functions used during recursion. + +It is undesirable for the instance to grow as the level of recursion increases. +To this end, one can construct the modified proving system $(prove', verify')$ such that +$ +forall (instance, witness) in relation times witnessSpace &: PP[verify'\(commit\(instance), prove'\(commit\(instance); instance, witness)) = one | instance(witness) = one] = 1 \ +forall instance in instanceSpace without relation, forall proof in proofSpace &: PP[verify'\(commit\(instance), proof) = one] < epsilon +$ +where $commit\(dot)$ denotes a constant-size cryptographic commitment of the provided value. +Importantly, this allows the instance to be constant size. +It does, however, trade instance size for computation time, as the verifier now has to (pre)compute the $n$th nested commitment to verify an $n$-deep recursion. + +#et( + "design a setup such that the validators does not have to track the entire verification stack, i.e., if a verifier accepts the top level proof for the instance, that must mean that the instance's program was either 1) itself, or 2) the guest (= base level). The tricky thing here is that you'd have to somehow bypass the validator code containing the hash-root of a commitment of itself (which you should not be able to do with cryptographic hash functions)" +) + += Operation-specific verification +#let scratch = $bb(s)$ + +To verify a proof, several checks of different types need to be performed. +For the purposes of this discussion, we distinguish two types of checks: +those that rely primarily on binary arithmetic, and those relying on field arithmetic. + +Emulating either type of arithmetic on a VM designed for the other, typically incurs significant performance overhead. +Yet, recursive proving heavily relies on both types. +With the aim of bypassing a 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 specified binary arithmetic-oriented VM (henceforth referred to as _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 requires the verification algorithm be split as well. +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. + +This architecture solves this by introducing a prover-hinted _communication record_ accessible to both VMs. +In practice, this record will primarily contain values being reinterpreted --- from $FF$ to $ZZ_(2^N)$ and vice-versa --- during verification. +The two halves of the split verification algorithm should be designed to verify the record: for each value on the record, one of the VMs _verifies_ the value to be correct, while the other _assumes_ the value to be correct and resumes the verification algorithm under this assumption. + +To ensure this verification happens correctly, both verification algorithms 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 _algorithm design-time_ and parametrized in terms of the proof only. +Then, both verification algorithm halves should be designed to agree on the interpretation of the proof and communication record, irrespective of the provided proof. + +Note that, as part of check correctness of a proof-of-split-verification, the verifier must now verify that the VMs were given 1) the same proof and communication record, and 2) a synchronized algorithm pair; otherwise the prover could cheat. + +#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. +] + +// #let bool = $#`B`$ +// #let field = $#`F`$ +// #let equal = $#`E`$ +// #let consistency = $#`C`$ + + +// - Let $verify_bool || verify_field := verify$ denote the decomposed verifier. +// $ +// prove\([verify_bool || verify_field, instance]; [proof, scratch]) = proof' +// $ +// $ +// v'(instance, proof) := verify([verify_bool || verify_field, instance], proof) +// $ +// $ +// verify\([verify_bool || verify_field, instance], proof')\ +// // &=verify'\(instance, proof')\ +// &=verify\([verify_bool, instance], proof') times verify\([verify_field, instance], proof')\ +// $ +// $ +// &prove\([verify', [verify_bool || verify_field, instance]]; [proof', scratch'])\ +// &=prove\([verify_bool || verify_field || verify_consistency, [verify, instance]]; proof')\ +// // &=prove\([verify_bool\([verify, instance], dot) times verify_field\([verify, instance], dot); proof')\ +// &=[ +// prove\([verify_bool, [verify, instance]]; proof'), +// prove\([verify_field, [verify, instance]]; proof'), +// prove\([verify_consistency, [verify, instance]]; proof') +// ]\ +// &= [proof'_bool, proof'_field]\ +// &= proof''\ +// &\ \ +// &prove\([verify, [verify, instance]]; proof')\ +// &=prove\([verify_bool || verify_field, [verify, instance]]; proof')\ +// &=[ +// prove\([verify_bool, [verify, instance]]; proof'), +// prove\([verify_field, [verify, instance]]; proof') +// ]\ +// &= [proof'_bool, proof'_field]\ +// &= proof''\ +// &\ \ +// &verify\([verify, [verify, instance]], proof'')\ +// &=verify\([verify_bool || verify_field, [verify, instance]], [proof'_bool, proof'_field])\ +// &=verify\([verify_bool, instance], proof'_bool) times verify\([verify_field, instance], proof'_field)\ +// $ +// --- +// - $prove\((verify_bool, instance); proof) -> proof_bool$ +// - $prove\((verify_field, instance); proof) -> proof_field$ +// - $verify\(((verify_bool, instance),(verify_field, instance)), (proof_bool, proof_field)) $ +// --- +// $ +// &verify'\((verify_bool, verify_field, instance), (proof_bool, proof_field)) \ +// &= verify((verify_bool, instance), proof_bool) times verify\((verify_field, instance), proof_field) +// &\ \ +// &overline(prove)\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field))\ +// &= ( +// prove\((verify'_bool, (verify_bool, verify_field, instance)); (proof_bool, proof_field)), +// prove\((verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field)) +// )\ +// &= (proof^1_bool, proof^1_field) +// &\ \ +// &verify'\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)), (proof'_bool, proof'_field)) +// $ +// - $prove\((verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field)) -> proof'_field$ +// - $verify'\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)), (proof'_bool, proof'_field))$ +// --- +// - $prove\((verify'_bool, (verify'_bool, verify'_field, (verify_bool, verify_field, instance))); (proof'_bool, proof'_field)) -> proof''_bool$ +// - $prove\((verify'_field, (verify'_bool, verify'_field, (verify_bool, verify_field, instance))); (proof'_bool, proof'_field)) -> proof''_field$ +// - $verify\((verify'_bool, verify'_field, (verify'_bool, verify'_field, (verify'_bool, verify'_field, (verify_bool, verify_field, instance)))), (proof''_bool, proof''_field))$ +// --- +// - $prove\((verify_bool, ((verify_bool, instance),(verify_field, instance))); (proof_bool, proof_field)) -> proof_bool'$ +// - $prove\((verify_field, ((verify_bool, instance),(verify_field, instance))); (proof_bool, proof_field)) -> proof_field'$ +// - $verify\(((verify_bool, ((verify_bool, instance),(verify_field, instance))), (verify_field, ((verify_bool, instance),(verify_field, instance)))), (proof_0', proof_1'))$ + + +// - typically, verification algorithms reinterpret data based on the field. +// - expand proof to include prover-provided "scratch space", +// - commit to this "expanded proof" +// - have both VMs use the same expanded proof to +// - verify programs must be tuned such that all values in the scratch space are +// - checked by one of the two VMs and +// - leveraged by other VM to speed up verification. +// - + +// - specific verify programs. + + + += Theory applied +Applying these observations and design requirements to this VM, we present the following design + +- separate field-VM (@field-VM) with its own `DECODE` table (@field-decode). + +== Split Verification Algorithm(s) + +=== Verification of guest program proof +#let FRI = raw("FRI") +#let DEEP = raw("DEEP") +#let LogUp = raw("LogUp") +#let challenges = $bb(C)$ +#let table_commitments = $cal(C)_cal(T)$ +#let logup_commitments = $cal(C)_cal(L)$ +#let DEEP_commitments = $cal(C)_cal(D)$ +#let DEEP_openings = $cal(O)_cal(D)$ +#let FRI_folding_commitments = $cal(C)_cal(F)$ +#let FRI_query_openings = $cal(O)_cal(F)$ +#let proof = $bb(pi)$ +#let expanded_proof = $proof^*$ +#let fs = $#`FiatShamir`$ + +Proof contents: +- #table_commitments: the commitments to all AIR-tables, +- #logup_commitments: the commitments to the #LogUp columns, +- #DEEP_commitments: the #DEEP commitments, +- #DEEP_openings: the #DEEP openings, +- #FRI_folding_commitments: the #FRI folding commitments, and +- #FRI_query_openings: the #FRI query openings. + +#figure(image("figures/DEEP-FRI_verification.svg", height: 75%)) + +On communcation record: +- all the challenges: lincomb, segment, DEEP coordinate, LogUp, folding & query + +Native verification steps: +- binaryVM: + - [B] Derive lincomb challenges from table commitments + public input + - [B] Derive segment challenges from quotient commitments + table commitments + public input + - [B] Derive DEEP point from segment + quotient + table commitments + public input + - [B] Derive LogUp challenges from table commitments + public input + - [B] verify LogUp opening proofs + - [B] derive folding challenges from (everything before) + - [B] derive FRI-query challenges + - [B] verify query proofs +- fieldVM: + - [F] verify opened LogUp sums + - [F] verify low-degreeness of FRI output + - [F] verify query opening validity. + - [F] verify DEEP quotient/segmenting using DEEP-point + +== Verification of verification-proof +TODO + +// = L0 proof +// Let $proof\(g,x) := (#table_commitments, #DEEP_commitments, #DEEP_openings, #FRI_folding_commitments, #FRI_query_openings)$ denote a proof produced by the prover for program $g$ on public input $x$, with +// - #table_commitments the commitments to all AIR-tables, +// - #DEEP_commitments the #DEEP commitments, +// - #DEEP_openings the #DEEP openings, +// - #FRI_folding_commitments the #FRI folding commitments, and +// - #FRI_query_openings the #FRI query openings. + + +// = Verifying an L0 proof +// Let $#fs\(proof) -> challenges$ denote the deterministic map producing the challenges corresponding to a given proof. +// We construct an _expanded proof_ $#expanded_proof := (proof, #fs\(proof)) = (proof, #`prog_comm`, challenges)$ containing the original proof, a commitment to the original guest program (including public parameters), and the challenges required for verification. + +// The program commitment #`prog_comm` can be a commitment to the public information of a specific proof, e.g., the hash of the commitments to the `DECODE` table(s) and all public `PAGE` tables. + +// Next, let us define two verification programs: + +// ``` +// func verify_L0_binary(proof: Proof, prog_comm, challenges) -> Proof: +// commit(prog_comm) # through printing to stdout +// assert challenges == fiatShamir(proof) +// assert verify_FRI_query_proofs(proof, challenges) + +// func verify_L0_field(proof: Proof, _prog_comm, challenges) -> Proof: +// assert verify_DEEP_openings(proof, challenges) +// assert verify_FRI_folding(proof, challenges) +// assert verify_FRI_output_is_low_degree(proof, challenges) +// assert verify_LogUp_equals_zero(proof, challenges) + +// func proof_L0_verification(prog_comm, proof: Proof) -> DoubleProof: +// challenges = fiatShamir_risc5VM(proof) +// input_commitment = commit((prog_comm, proof, challenges)) +// proof0: Proof = risc5VM.prove(verify_L0_binary, input_commitment) +// proof1: Proof = fieldVM.prove(verify_L0_field, input_commitment) +// return (input_commitment, proof0, proof1) +// ``` + +// = Verifying an L1 proof + +// ``` +// func verify_L1_binary(proof: Proof, prog_comm, challenges) -> Proof: +// commit(prog_comm) # through printing to stdout +// assert challenges.c0 == fiatShamir_risc5VM(proof) +// assert challenges.c1 == fiatShamir_fieldVM(proof) +// assert verify_FRI_query_proofs(proof.p0, challenges.c0) +// assert verify_FRI_query_proofs(proof.p1, challenges.c1) + +// func verify_L1_field(proof, prog_comm, challenges) -> Proof: +// assert verify_DEEP_openings(proof.p0, challenges.c0) +// assert verify_DEEP_openings(proof.p1, challenges.c1) +// assert verify_FRI_folding(proof.p0, challenges.c0) +// assert verify_FRI_folding(proof.p1, challenges.c1) +// assert verify_FRI_output_is_low_degree(proof.p0, challenges.c0) +// assert verify_FRI_output_is_low_degree(proof.p1, challenges.c1) + +// # compute verifier contribution to the risc5VM's LogUp +// vc = compute_commitment_contribution(challenges.c0, prog_comm) +// assert verify_LogUp_equals_zero(proof.p0 + vc, challenges.c0) +// assert verify_LogUp_equals_zero(proof.p1, challenges.c1) + +// func proof_L1_verification(_prog_comm, proof: DoubleProof) -> DoubleProof: +// c0 = fiatShamir_risc5VM((proof.input_comm, proof.p0)) +// c1 = fiatShamir_fieldVM((proof.input_comm, proof.p1)) +// challenges = (c0, c1) + +// input_commitment = commit((_prog_comm, proof, challenges)) +// proof0: Proof = risc5VM.prove(verify_L1_binary, input_commitment) +// proof1: Proof = fieldVM.prove(verify_L1_field, input_commitment) +// return (input_commitment, proof0, proof1) +// ``` + + + + + +// = Recursion +// - proof system generates proof +// - proof is still quite large +// - rather than verify the proof itself, have the prover generate proof that the verification of the first proof succeeds, where this new proof is smaller than the first. +// - repeat until the desired proof size is reached +// - at the end, verify this "recursed" proof. +// - this is commonly called "proof recursion" + +// - one important aspect, is that the _recursed proof_ should be tied to the original, base proof. + +// = Recursion components +// Three different configurations +// + prove_guest_program(guest_program) -> proof +// + prove_single_proof_verification(proof) -> double_proof +// + prove_double_proof_verification(double_proof) -> double_proof + +// == Proving a guest program +// -> take guest program +// > generate proof + +// contents of proof: +// - table commitments +// - DEEP commitments +// - DEEP openings +// - FRI folding commitments +// - FRI query openings (= node content + merkle path) + +// == Proving the verification of a proof +// - expand proof to proof_with_challenges +// - commit to proof_with_challenges (e.g., as PAGES tables) +// - binaryVM runs program "verify_binary", with commitment as instance and (proof, challenges) as witness +// - commits to the `commitment` by printing it to `stdout` +// - verifies that: +// - FRI query proofs are valid +// - challenges are correctly derived from the proof transcript +// - fieldVM runs program "verify_field" with commitment as instance and (proof, challenges) as witness: +// - verifies that: +// - DEEP opening is valid +// - FRI folding was done correctly. +// - generate two proofs, with a *shared commitment to the memory init/fini of the commitment* +// -> (shared_commitment, proof_binary_vm, proof_field_vm) + +// == Proving the verification of a double-proof +// - expand proofs to proof_with_challenges +// - commit to proof_with_challenges (e.g., as PAGES tables) +// - binaryVM runs program "verify_binary", with commitment as instance and (proof, challenges) as witness +// - commits to the `commitment` by printing it to `stdout` +// - verifies that: +// - FRI query proofs are valid +// - challenges are correctly derived from the proof transcript +// - fieldVM runs program "verify_field" with commitment as instance and (proof, challenges) as witness: +// - verifies that: +// - DEEP opening is valid +// - FRI folding was done correctly. + + + + + +// // Keys +// #let ProverKey = $KK$ +// #let VerifKey = $VV$ + +// // Spaces +// #let instanceSpace = $XX$ +// #let witnessSpace = $WW$ +// #let outSpace = $BB$ +// #let hashOutSpace = $HH$ +// #let proofSpace = $Pi$ + +// Let $PP: XX times WW mapsto BB$ denote the collection of guest programs mapping a (public) _instance_ $x in XX$ and (private) witness + +// - L0: proof $arrow.l$ prove(guest_program, input) +// - L1: (proof0, proof1) $arrow.l$ prove(verify_proof(proof)) +// - L2+: (proof0, proof1) $arrow.l$ prove(verify_proof(proof)) + +// Level 0: +// - instance: program ELF, public inputs +// - witness: private inputs + +// Proof L0: +// - setup: +// - turn ELF, public inputs into DECODE table +// - comm = commit to DECODE table +// - prover: +// - proof $arrow.l$ prove(comm, witness) + + +// prover: +// - runs prove() + +// Level 0: +// $ +// text("program space: ") +// && PP &:&& instanceSpace times witnessSpace &&mapsto outSpace\ +// text("preprocessor space: ") +// && PP PP &:&& PP times instanceSpace &&mapsto ProverKey times VerifKey\ +// text("L0 prover: ") +// && #`p` &in&& ProverKey times witnessSpace &&mapsto proofSpace\ +// text("L0 verifier: ") +// && #`v` &in&& VerifKey times proofSpace &&mapsto outSpace +// $ + +// Level 1: +// $ +// text("program: ") +// && p' &in&& [hashOutSpace] times [VerifKey times proofSpace times witnessSpace'] &&mapsto outSpace\ +// text("preprocessor: ") +// && #`pp`' &:&& p' times hashOutSpace &&mapsto ProverKey' times VerifKey'\ +// text("L1 prover: ") +// && #`p`' &in&& ProverKey' times [VerifKey times proofSpace times witnessSpace'] &&mapsto proofSpace' := proofSpace times proofSpace\ +// text("L1 verifier: ") +// && #`v`' &in&& VerifKey' times proofSpace' &&mapsto outSpace +// $ + +// Level 2 - $inf$: +// $ +// text("program: ") +// && p_2 &in&& [hashOutSpace] times [VerifKey' times proofSpace' times witnessSpace'] &&mapsto outSpace\ +// text("preprocessor: ") +// && #`pp`_2 &:&& p_2 times hashOutSpace &&mapsto ProverKey' times VerifKey'\ +// text("L2 prover: ") +// && #`p`_2 &in&& ProverKey' times [VerifKey' times proofSpace' times witnessSpace'] &&mapsto proofSpace'\ +// text("L2 verifier: ") +// && #`v`_2 &in&& VerifKey' times proofSpace' &&mapsto outSpace +// $ + +// s.t. $(#`h`, #`vk`, #`π`) mapsto #`H` (#`vk`) = #`h` text("and") #`verify` (#`vk`, #`π`) = 1$ + + +// $ +// #`program<`XX #`>` (WW) mapsto BB +// $ From 89e5cacd95c1cc38d308c16eff90c83fb36b6e4a Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 14 Aug 2026 12:49:20 +0200 Subject: [PATCH 2/7] spec/recursion: put text and figure side-by-side --- spec/recursion.typ | 62 +++++++++++++++++++++++++--------------------- 1 file changed, 34 insertions(+), 28 deletions(-) diff --git a/spec/recursion.typ b/spec/recursion.typ index 5dc811b87..291cbad73 100644 --- a/spec/recursion.typ +++ b/spec/recursion.typ @@ -219,34 +219,40 @@ Applying these observations and design requirements to this VM, we present the f #let expanded_proof = $proof^*$ #let fs = $#`FiatShamir`$ -Proof contents: -- #table_commitments: the commitments to all AIR-tables, -- #logup_commitments: the commitments to the #LogUp columns, -- #DEEP_commitments: the #DEEP commitments, -- #DEEP_openings: the #DEEP openings, -- #FRI_folding_commitments: the #FRI folding commitments, and -- #FRI_query_openings: the #FRI query openings. - -#figure(image("figures/DEEP-FRI_verification.svg", height: 75%)) - -On communcation record: -- all the challenges: lincomb, segment, DEEP coordinate, LogUp, folding & query - -Native verification steps: -- binaryVM: - - [B] Derive lincomb challenges from table commitments + public input - - [B] Derive segment challenges from quotient commitments + table commitments + public input - - [B] Derive DEEP point from segment + quotient + table commitments + public input - - [B] Derive LogUp challenges from table commitments + public input - - [B] verify LogUp opening proofs - - [B] derive folding challenges from (everything before) - - [B] derive FRI-query challenges - - [B] verify query proofs -- fieldVM: - - [F] verify opened LogUp sums - - [F] verify low-degreeness of FRI output - - [F] verify query opening validity. - - [F] verify DEEP quotient/segmenting using DEEP-point +#grid( + columns: (1fr, auto), + column-gutter: 1em, + [ + Proof contents: + - #table_commitments: the commitments to all AIR-tables, + - #logup_commitments: the commitments to the #LogUp columns, + - #DEEP_commitments: the #DEEP commitments, + - #DEEP_openings: the #DEEP openings, + - #FRI_folding_commitments: the #FRI folding commitments, and + - #FRI_query_openings: the #FRI query openings. + + On communcation record: + - all the challenges: lincomb, segment, DEEP coordinate, LogUp, folding & query + + Native verification steps: + - binaryVM: + - [B] Derive lincomb challenges from table commitments + public input + - [B] Derive segment challenges from quotient commitments + table commitments + public input + - [B] Derive DEEP point from segment + quotient + table commitments + public input + - [B] Derive LogUp challenges from table commitments + public input + - [B] verify LogUp opening proofs + - [B] derive folding challenges from (everything before) + - [B] derive FRI-query challenges + - [B] verify query proofs + - fieldVM: + - [F] verify opened LogUp sums + - [F] verify low-degreeness of FRI output + - [F] verify query opening validity. + - [F] verify DEEP quotient/segmenting using DEEP-point + ], + figure(image("figures/DEEP-FRI_verification.svg", height: 90%)) +) + == Verification of verification-proof TODO From 0aab4a4e946eff07686546f0845afc0bccce5d1e Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 21 Aug 2026 11:53:53 +0200 Subject: [PATCH 3/7] spec/recursion: overhaul --- spec/book.typ | 1 + spec/figures/DEEP-FRI_verification.md | 11 +- spec/figures/DEEP-FRI_verification.svg | 2 +- spec/recursion.typ | 620 ++++++++++++++++--------- spec/verifier.typ | 8 + 5 files changed, 426 insertions(+), 216 deletions(-) create mode 100644 spec/verifier.typ diff --git a/spec/book.typ b/spec/book.typ index 97f58882d..847730933 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -13,6 +13,7 @@ ("logup.typ", [`LogUp` argument], ), ("memory.typ", [Memory argument], ), ("streaming.typ", [Streaming prover], ), + ("verifier.typ", [Verification], ) )), ("OVERVIEW", ( ("variables.typ", [Variables], ), diff --git a/spec/figures/DEEP-FRI_verification.md b/spec/figures/DEEP-FRI_verification.md index 5a80c5cdf..997dcaf93 100644 --- a/spec/figures/DEEP-FRI_verification.md +++ b/spec/figures/DEEP-FRI_verification.md @@ -26,7 +26,10 @@ end P->V: FRI low-degree output note over V: verify low-degreeness loop FRI-verify -P<-V: FRI-opening challenge -P->V: opening -note over V: verify opening -end \ No newline at end of file +note over V: sample folding\nchallenges +P<-V: challenges +P->V: openings +note over V: verify openings +note over V: verify folding\nsteps +end +note over V: verify DEEP \ No newline at end of file diff --git a/spec/figures/DEEP-FRI_verification.svg b/spec/figures/DEEP-FRI_verification.svg index 6adf58fd0..24e57a819 100644 --- a/spec/figures/DEEP-FRI_verification.svg +++ b/spec/figures/DEEP-FRI_verification.svg @@ -1 +1 @@ -title%20Proof%20verification%0Anote%20over%20P%2CV%3A%20established%3A%20shared%20program%20with%5Cnpublic%20input%0Anote%20over%20P%3A%20fill%20tables%0AP-%3EV%3A%20batch-commit%20tables%0Agroup%20par%20%5BDEEP%5D%0AP%3C-V%3A%20lincomb%20challenges%0AP-%3EV%3A%20quotient%20commitment%0AP%3C-V%3A%20segment%20challenges%0AP-%3EV%3A%20segment%20commitment%0AP%3C-V%3A%20DEEP%20point%0AP-%3EV%3A%20DEEP%20openings%0Aelse%20LogUp%0AP%3C-V%3A%20LogUp%20challenges%0AP-%3EV%3A%20batch-commit%20to%20LogUp%20columns%0AP-%3EV%3A%20open%20sum%20entries%0Anote%20over%20V%3A%20checksum%0Aend%0A%0AP-%3EV%3A%20batch%20FRI-commit%0Aloop%20Batch-FRI%0AP%3C-V%3A%20folding%20challenge%0AP-%3EV%3A%20folding%20commitment%0Aend%0AP-%3EV%3A%20FRI%20low-degree%20output%0Anote%20over%20V%3A%20verify%20low-degreeness%0Aloop%20FRI-verify%0AP%3C-V%3A%20FRI-opening%20challenge%0AP-%3EV%3A%20opening%0Anote%20over%20V%3A%20verify%20opening%0AendPVProof verificationestablished: shared program withpublic inputfill tablesbatch-commit tableslincomb challengesquotient commitmentsegment challengessegment commitmentDEEP pointDEEP openingsLogUp challengesbatch-commit to LogUp columnsopen sum entrieschecksumbatch FRI-commit (implicitly)folding challengefolding commitmentFRI low-degree outputverify low-degreenessFRI-opening challengeopeningverify openingpar[DEEP][LogUp]loop[Batch-FRI]loop[FRI-verify] \ No newline at end of file +title%20Proof%20verification%0Anote%20over%20P%2CV%3A%20established%3A%20shared%20program%20with%5Cnpublic%20input%0Anote%20over%20P%3A%20fill%20tables%0AP-%3EV%3A%20batch-commit%20tables%0Agroup%20par%20%5BDEEP%5D%0AP%3C-V%3A%20lincomb%20challenges%0AP-%3EV%3A%20quotient%20commitment%0AP%3C-V%3A%20segment%20challenges%0AP-%3EV%3A%20segment%20commitment%0AP%3C-V%3A%20DEEP%20point%0AP-%3EV%3A%20DEEP%20openings%0Aelse%20LogUp%0AP%3C-V%3A%20LogUp%20challenges%0AP-%3EV%3A%20batch-commit%20to%20LogUp%20columns%0AP-%3EV%3A%20open%20sum%20entries%0Anote%20over%20V%3A%20checksum%0Aend%0A%0AP-%3EV%3A%20batch%20FRI-commit%20(implicitly)%0Aloop%20Batch-FRI%0AP%3C-V%3A%20folding%20challenge%0AP-%3EV%3A%20folding%20commitment%0Aend%0AP-%3EV%3A%20FRI%20low-degree%20output%0Anote%20over%20V%3A%20verify%20low-degreeness%0Aloop%20FRI-verify%0Anote%20over%20V%3A%20sample%20folding%5Cnchallenges%0AP%3C-V%3A%20challenges%0AP-%3EV%3A%20openings%0Anote%20over%20V%3A%20verify%20openings%0Anote%20over%20V%3A%20verify%20folding%5Cnsteps%0Aend%0Anote%20over%20V%3A%20verify%20DEEPPVProof verificationestablished: shared program withpublic inputfill tablesbatch-commit tableslincomb challengesquotient commitmentsegment challengessegment commitmentDEEP pointDEEP openingsLogUp challengesbatch-commit to LogUp columnsopen sum entrieschecksumbatch FRI-commit (implicitly)folding challengefolding commitmentFRI low-degree outputverify low-degreenesssample foldingchallengeschallengesopeningsverify openingsverify foldingstepsverify DEEPpar[DEEP][LogUp]loop[Batch-FRI]loop[FRI-verify] \ No newline at end of file diff --git a/spec/recursion.typ b/spec/recursion.typ index 291cbad73..982fee2cd 100644 --- a/spec/recursion.typ +++ b/spec/recursion.typ @@ -8,11 +8,14 @@ #let fieldVM = raw("fieldVM") -#let functionSpace = $PP$ -#let program = $bb(p)$ +#let functionSpace = $cal(F)$ +#let verifierSpace = $cal(V)$ +#let privateFunctionSpace = $hat(cal(F))$ +#let program = $f$ #let inputSpace = $II$ #let input = $bb(i)$ #let instanceSpace = $XX$ +#let instanceCommitmentSpace = $CC$ #let instance = $bb(x)$ #let instance2 = $bb(y)$ #let witnessSpace = $WW$ @@ -21,244 +24,439 @@ #let proof = $bb(pi)$ #let prove = $italic("p")$ #let verify = $italic("v")$ -#let commit = $italic("c")$ +#let commit(x) = $overline(#x)$ +#let comm(x) = $commit(#x)$ #let one = $bb(1)$ #let zero = $bb(0)$ -#let function = $cal(F)$ +#let function = $bb(f)$ #let relation = $cal(R)$ +#let iff = $arrow.double.l.r$ +#let implies = $arrow.double.r$ +#let prob = $PP$ #show math.equation.where(block: false): box = Notation - -Let $functionSpace := {function: inputSpace times witnessSpace mapsto BB}$ denote the set of functions mapping input-witness pairs $(input; witness) in inputSpace times witnessSpace$ to a boolean ${ zero, one } in BB$. -Let relation $relation subset.eq functionSpace times inputSpace =: instanceSpace$ denote the set of all succesfully terminating program instances, i.e., all function-input instances $(program, input) in functionSpace times inputSpace$ for which there exists a witness $witness in witnessSpace$ such that $program\(input; witness) = one$. - -Let there furthermore exist _proving system_ $(prove, verify)$ with prover $prove in { function: instanceSpace times witnessSpace mapsto proofSpace }$ and verifier $verify in { function: instanceSpace times proofSpace mapsto BB}$ such that +Let $BB := { zero, one }$ denote the boolean set and let +$functionSpace := {f: inputSpace times witnessSpace mapsto BB}$ denote +the set of functions mapping the (public) input space $inputSpace$ and (private) +witness space $witnessSpace$ to this set. +We use $instanceSpace := functionSpace times inputSpace = {instance: witnessSpace mapsto BB}$ +to denote the set of functions with the public input "baked in"; +elements in this set are henceforth referred to as _function instances_, or simply _instances_. +We then define $relation subset.eq instanceSpace$ +as the set of all _solvable instances_, +i.e., all instances $instance in instanceSpace$ +for which there exists a witness $witness in witnessSpace$ such that +$instance\(witness) = one$. +Lastly, we introduce the commitment function $c: instanceSpace mapsto instanceCommitmentSpace$. +To simplify notation, we use $commit(instance) = c(instance)$. + +We now assume the existence of _proving system_ $(prove, verify)$ with +prover $prove: instanceSpace times witnessSpace mapsto proofSpace$ and +verifier $verify: instanceCommitmentSpace times proofSpace mapsto BB$ such that $ -forall (instance, witness) in relation times witnessSpace &: PP[verify\(instance, prove\(instance; witness)) = one | instance(witness) = one] = 1 \ -forall instance in instanceSpace without relation, forall proof in proofSpace &: PP[verify\(instance, proof) = one] < epsilon +forall (instance, witness) in relation times witnessSpace &: prob[verify\(commit(instance), prove\(instance; witness)) = one | instance(witness) = one] = 1 \ +forall instance in instanceSpace without relation, forall proof in proofSpace &: prob[verify\(commit(instance), proof) = one] < epsilon $ -with $epsilon$ negligibly small. -That is: any valid proof for a terminating program verifiers successfully, while the probability of any proof verifying a unsuccesfully-terminating program is negligible. +with $epsilon$ negligibly small and $proofSpace$ the proof space. +That is: any valid proof for a solvable instance verifies successfully, +while the probability of any proof verifying an unsolvable instance is negligible. + +Translating this to the purposes of this VM, a prover wishes to convince the verifier +that for some agreed upon program ($program in functionSpace$) 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 relation$). +To this end, the prover uses $prove\((program, input); witness) = prove\(instance; witness)$ +to construct some proof $proof in proofSpace$ and sends this to the verifier. +They then use $verify(comm(instance), proof)$ to check that the proof is valid, +convincing them of the prover's claim. = Proof recursion -In our application, the prover wishes to convince the verifier that for some public program-input instance $instance = (program, input) in instanceSpace$ they know a private witness $witness in witnessSpace$ such that $program\(input; witness) = one$. -To this end, the prover uses $prove\(program, input; witness) = prove\(instance; witness)$ to generate proof $proof$ and sends this to the verifier. -They then use $verify(instance, proof)$ to check that the proof is valid, convincing them of the prover's claim. - -When we observe that $verify in functionSpace$, we can now let the prover compute $prove\(verify, instance; prove\(instance; witness)) = proof'$ and send this proof for the verifier to $verify((verify, instance), proof')$, proving that they _know a proof attesting that $instance$ is in the relation_. -This concept, colloquially known as _proof recursion_, can be applied recursively. -This is often beneficial for _succint_ proving systems where proof size (and verification time) typically shrinks 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. - -== Proof traceability -Importantly, the final recursive proof should be _tied_ to both the original instance $instance$, as well as the entire stack of verifiers used along the way. -Without this, the final verifier cannot verify that the received proof attests to the original claim. -We exemplify this in the following triple-nested example: +Now observe that the verifier $verify$ is itself a function in +$verifierSpace := {hat(f): instanceSpace times proofSpace mapsto BB} subset.eq functionSpace$. +This means that we can use $prove$ to prove that the verification of a proof $proof$ for a given instance $instance$ succeeds: $ -&prove\([verify, instance'']; prove\([verify, instance']; prove\([verify, instance]; prove\(instance; witness))) = proof'''\ -&verify(instance''', proof''') in BB + &prove\(verify(comm(instance), dot); proof) = proof', text("and") + &verify(comm(verify(comm(instance), dot)), proof') = one. $ -which requires $instance''' = [verify, instance''] = [verify, [verify, instance']] = [verify, [verify, [verify, instance]]]$: the original instance, as well as the full stack of verification functions used during recursion. - -It is undesirable for the instance to grow as the level of recursion increases. -To this end, one can construct the modified proving system $(prove', verify')$ such that +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 _succint_ proving systems where proof size +typically shrinks (and verification time therefore 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, $ -forall (instance, witness) in relation times witnessSpace &: PP[verify'\(commit\(instance), prove'\(commit\(instance); instance, witness)) = one | instance(witness) = one] = 1 \ -forall instance in instanceSpace without relation, forall proof in proofSpace &: PP[verify'\(commit\(instance), proof) = one] < epsilon + &prove\(verify(comm(verify(comm(instance), dot)), dot); proof') = proof'', text("and")\ + &verify(comm(verify(comm(verify(comm(instance), dot)), dot)), proof'') = one. $ -where $commit\(dot)$ denotes a constant-size cryptographic commitment of the provided value. -Importantly, this allows the instance to be constant size. -It does, however, trade instance size for computation time, as the verifier now has to (pre)compute the $n$th nested commitment to verify an $n$-deep recursion. - -#et( - "design a setup such that the validators does not have to track the entire verification stack, i.e., if a verifier accepts the top level proof for the instance, that must mean that the instance's program was either 1) itself, or 2) the guest (= base level). The tricky thing here is that you'd have to somehow bypass the validator code containing the hash-root of a commitment of itself (which you should not be able to do with cryptographic hash functions)" -) +we see that the verifier first 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. -= Operation-specific verification -#let scratch = $bb(s)$ - -To verify a proof, several checks of different types need to be performed. -For the purposes of this discussion, we distinguish two types of checks: -those that rely primarily on binary arithmetic, and those relying on field arithmetic. - -Emulating either type of arithmetic on a VM designed for the other, typically incurs significant performance overhead. -Yet, recursive proving heavily relies on both types. -With the aim of bypassing a 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 specified binary arithmetic-oriented VM (henceforth referred to as _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. +A solution to this, is to leverage the following variation to the verification algorithm: +$ + verify': instanceCommitmentSpace^2 times {0, 1} times proofSpace: (c_0, c_1, b, proof) mapsto + cases( + verify(c_0, proof) &text("if") b=0, + verify(c_1(c_0, c_1, dot), proof) &text("if") b=1 + ) +$ +where it is assumed that $comm(function(x_1, x_2, dot))$ can be easily +constructed from $comm(function), comm(x_1)$, and $comm(x_2)$. +By choosing $c_0 = commit(instance)$ and $c_1 = commit(verify')$, the prover can then prove +the base case by selecting $b=0$, and set $b=1$ during further recursion. +Then, when presented with depth-n proof $proof^((n))$ and base instance $instance$, +the verifier executes +$ + verify'(commit(instance), commit(verify'), 1, proof^((n))) + &= verify(verify'(commit(instance), commit(verify'), dot), proof^((n)))\ + &= verify(verify(verify'(commit(instance), commit(verify'), dot dot), dot), proof^((n)))\ + &= verify(verify(verify(dots.c(v(commit(instance), dot), dot), dots.c), dot), dot), proof^((n))). +$ +In other words, we have constructed a verifier $verify'$ which can only verify +the desired base case, or a proof it produced itself. +This means that with successful verification of the ultimate proof $proof^((n))$, +it is also guaranteed that $verify'$ must have been used at every step in the proof recursion. +This solution moreover reduces the verifier overhead on parsing the instance to a minimum, +as both $comm(instance)$ and $comm(verify')$ can typically be precomputed. + +#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. +] -The introduction of this split requires the verification algorithm be split as well. -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. +#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 the 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. -This architecture solves this by introducing a prover-hinted _communication record_ accessible to both VMs. -In practice, this record will primarily contain values being reinterpreted --- from $FF$ to $ZZ_(2^N)$ and vice-versa --- during verification. -The two halves of the split verification algorithm should be designed to verify the record: for each value on the record, one of the VMs _verifies_ the value to be correct, while the other _assumes_ the value to be correct and resumes the verification algorithm under this assumption. - -To ensure this verification happens correctly, both verification algorithms 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 _algorithm design-time_ and parametrized in terms of the proof only. -Then, both verification algorithm halves should be designed to agree on the interpretation of the proof and communication record, irrespective of the provided proof. - -Note that, as part of check correctness of a proof-of-split-verification, the verifier must now verify that the VMs were given 1) the same proof and communication record, and 2) a synchronized algorithm pair; otherwise the prover could cheat. +This 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 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. + 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. ] -// #let bool = $#`B`$ -// #let field = $#`F`$ -// #let equal = $#`E`$ -// #let consistency = $#`C`$ - +In theory, any division of tasks between the two VMs would work. +Yet, it is expected that some division will be more performant than others. +Below, we provide a division that, in theory, is expected to achieve solid performance: + +*Record $record$.* +The record contains all challenges the prover derived using Fiat-Shamir. + +*Tasks for $verify'_b\(c_0, c_1, b, proof, record)$:* ++ assert that $b in {0, 1}$, ++ verify challenges on record $record$ according to Fiat-Shamir, ++ verify the various opening proofs; + - if $b=0$: + verify binary-VM DECODE table (@decode) query opening against $c_0$ + - if $b=1$: + verify binary-VM DECODE table (@decode) query opening against $c_(1,b)$ and + verify field-VM DECODE table (@field-decode) query opening against $c_(1,f)$ ++ `COMMIT` to $c_0$ and $c_1$ (see @commit) + +*Tasks $verify'_f\(c_0, c_1, b, proof, record)$:* ++ verify LogUp openings sum to zero, + - if $b=1$, use $c_0$ and $c_1$ to complete the `COMMIT` balance. ++ verify `DEEP` evaluation ++ verify `FRI` folding ++ verify `FRI` output low degreeness check. + +*Prover.* +The prover performs the following steps: +$ + 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^((n)) &arrow.l prove(verify'_b || verify'_f, (commit(instance), [commit(verify'_b), commit(verify'_f)], 1, proof^((n-1)), record)) +$ -// - Let $verify_bool || verify_field := verify$ denote the decomposed verifier. -// $ -// prove\([verify_bool || verify_field, instance]; [proof, scratch]) = proof' -// $ -// $ -// v'(instance, proof) := verify([verify_bool || verify_field, instance], proof) -// $ -// $ -// verify\([verify_bool || verify_field, instance], proof')\ -// // &=verify'\(instance, proof')\ -// &=verify\([verify_bool, instance], proof') times verify\([verify_field, instance], proof')\ -// $ -// $ -// &prove\([verify', [verify_bool || verify_field, instance]]; [proof', scratch'])\ -// &=prove\([verify_bool || verify_field || verify_consistency, [verify, instance]]; proof')\ -// // &=prove\([verify_bool\([verify, instance], dot) times verify_field\([verify, instance], dot); proof')\ -// &=[ -// prove\([verify_bool, [verify, instance]]; proof'), -// prove\([verify_field, [verify, instance]]; proof'), -// prove\([verify_consistency, [verify, instance]]; proof') -// ]\ -// &= [proof'_bool, proof'_field]\ -// &= proof''\ -// &\ \ -// &prove\([verify, [verify, instance]]; proof')\ -// &=prove\([verify_bool || verify_field, [verify, instance]]; proof')\ -// &=[ -// prove\([verify_bool, [verify, instance]]; proof'), -// prove\([verify_field, [verify, instance]]; proof') -// ]\ -// &= [proof'_bool, proof'_field]\ -// &= proof''\ -// &\ \ -// &verify\([verify, [verify, instance]], proof'')\ -// &=verify\([verify_bool || verify_field, [verify, instance]], [proof'_bool, proof'_field])\ -// &=verify\([verify_bool, instance], proof'_bool) times verify\([verify_field, instance], proof'_field)\ -// $ -// --- -// - $prove\((verify_bool, instance); proof) -> proof_bool$ -// - $prove\((verify_field, instance); proof) -> proof_field$ -// - $verify\(((verify_bool, instance),(verify_field, instance)), (proof_bool, proof_field)) $ -// --- -// $ -// &verify'\((verify_bool, verify_field, instance), (proof_bool, proof_field)) \ -// &= verify((verify_bool, instance), proof_bool) times verify\((verify_field, instance), proof_field) -// &\ \ -// &overline(prove)\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field))\ -// &= ( -// prove\((verify'_bool, (verify_bool, verify_field, instance)); (proof_bool, proof_field)), -// prove\((verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field)) -// )\ -// &= (proof^1_bool, proof^1_field) -// &\ \ -// &verify'\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)), (proof'_bool, proof'_field)) -// $ -// - $prove\((verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field)) -> proof'_field$ -// - $verify'\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)), (proof'_bool, proof'_field))$ -// --- -// - $prove\((verify'_bool, (verify'_bool, verify'_field, (verify_bool, verify_field, instance))); (proof'_bool, proof'_field)) -> proof''_bool$ -// - $prove\((verify'_field, (verify'_bool, verify'_field, (verify_bool, verify_field, instance))); (proof'_bool, proof'_field)) -> proof''_field$ -// - $verify\((verify'_bool, verify'_field, (verify'_bool, verify'_field, (verify'_bool, verify'_field, (verify_bool, verify_field, instance)))), (proof''_bool, proof''_field))$ -// --- -// - $prove\((verify_bool, ((verify_bool, instance),(verify_field, instance))); (proof_bool, proof_field)) -> proof_bool'$ -// - $prove\((verify_field, ((verify_bool, instance),(verify_field, instance))); (proof_bool, proof_field)) -> proof_field'$ -// - $verify\(((verify_bool, ((verify_bool, instance),(verify_field, instance))), (verify_field, ((verify_bool, instance),(verify_field, instance)))), (proof_0', proof_1'))$ - - -// - typically, verification algorithms reinterpret data based on the field. -// - expand proof to include prover-provided "scratch space", -// - commit to this "expanded proof" -// - have both VMs use the same expanded proof to -// - verify programs must be tuned such that all values in the scratch space are -// - checked by one of the two VMs and -// - leveraged by other VM to speed up verification. -// - - -// - specific verify programs. - - - -= Theory applied -Applying these observations and design requirements to this VM, we present the following design - -- separate field-VM (@field-VM) with its own `DECODE` table (@field-decode). - -== Split Verification Algorithm(s) - -=== Verification of guest program proof -#let FRI = raw("FRI") -#let DEEP = raw("DEEP") -#let LogUp = raw("LogUp") -#let challenges = $bb(C)$ -#let table_commitments = $cal(C)_cal(T)$ -#let logup_commitments = $cal(C)_cal(L)$ -#let DEEP_commitments = $cal(C)_cal(D)$ -#let DEEP_openings = $cal(O)_cal(D)$ -#let FRI_folding_commitments = $cal(C)_cal(F)$ -#let FRI_query_openings = $cal(O)_cal(F)$ -#let proof = $bb(pi)$ -#let expanded_proof = $proof^*$ -#let fs = $#`FiatShamir`$ - -#grid( - columns: (1fr, auto), - column-gutter: 1em, - [ - Proof contents: - - #table_commitments: the commitments to all AIR-tables, - - #logup_commitments: the commitments to the #LogUp columns, - - #DEEP_commitments: the #DEEP commitments, - - #DEEP_openings: the #DEEP openings, - - #FRI_folding_commitments: the #FRI folding commitments, and - - #FRI_query_openings: the #FRI query openings. - - On communcation record: - - all the challenges: lincomb, segment, DEEP coordinate, LogUp, folding & query - - Native verification steps: - - binaryVM: - - [B] Derive lincomb challenges from table commitments + public input - - [B] Derive segment challenges from quotient commitments + table commitments + public input - - [B] Derive DEEP point from segment + quotient + table commitments + public input - - [B] Derive LogUp challenges from table commitments + public input - - [B] verify LogUp opening proofs - - [B] derive folding challenges from (everything before) - - [B] derive FRI-query challenges - - [B] verify query proofs - - fieldVM: - - [F] verify opened LogUp sums - - [F] verify low-degreeness of FRI output - - [F] verify query opening validity. - - [F] verify DEEP quotient/segmenting using DEEP-point - ], - figure(image("figures/DEEP-FRI_verification.svg", height: 90%)) -) - - -== Verification of verification-proof -TODO +*Ultimate verification.* +$verify'(commit(instance), [commit(verify'_b), commit(verify'_f)], 1, proof^((n-1))) =? one$ + + + +// // #let bool = $#`B`$ +// // #let field = $#`F`$ +// // #let equal = $#`E`$ +// // #let consistency = $#`C`$ + + +// // - Let $verify_bool || verify_field := verify$ denote the decomposed verifier. +// // $ +// // prove\([verify_bool || verify_field, instance]; [proof, scratch]) = proof' +// // $ +// // $ +// // v'(instance, proof) := verify([verify_bool || verify_field, instance], proof) +// // $ +// // $ +// // verify\([verify_bool || verify_field, instance], proof')\ +// // // &=verify'\(instance, proof')\ +// // &=verify\([verify_bool, instance], proof') times verify\([verify_field, instance], proof')\ +// // $ +// // $ +// // &prove\([verify', [verify_bool || verify_field, instance]]; [proof', scratch'])\ +// // &=prove\([verify_bool || verify_field || verify_consistency, [verify, instance]]; proof')\ +// // // &=prove\([verify_bool\([verify, instance], dot) times verify_field\([verify, instance], dot); proof')\ +// // &=[ +// // prove\([verify_bool, [verify, instance]]; proof'), +// // prove\([verify_field, [verify, instance]]; proof'), +// // prove\([verify_consistency, [verify, instance]]; proof') +// // ]\ +// // &= [proof'_bool, proof'_field]\ +// // &= proof''\ +// // &\ \ +// // &prove\([verify, [verify, instance]]; proof')\ +// // &=prove\([verify_bool || verify_field, [verify, instance]]; proof')\ +// // &=[ +// // prove\([verify_bool, [verify, instance]]; proof'), +// // prove\([verify_field, [verify, instance]]; proof') +// // ]\ +// // &= [proof'_bool, proof'_field]\ +// // &= proof''\ +// // &\ \ +// // &verify\([verify, [verify, instance]], proof'')\ +// // &=verify\([verify_bool || verify_field, [verify, instance]], [proof'_bool, proof'_field])\ +// // &=verify\([verify_bool, instance], proof'_bool) times verify\([verify_field, instance], proof'_field)\ +// // $ +// // --- +// // - $prove\((verify_bool, instance); proof) -> proof_bool$ +// // - $prove\((verify_field, instance); proof) -> proof_field$ +// // - $verify\(((verify_bool, instance),(verify_field, instance)), (proof_bool, proof_field)) $ +// // --- +// // $ +// // &verify'\((verify_bool, verify_field, instance), (proof_bool, proof_field)) \ +// // &= verify((verify_bool, instance), proof_bool) times verify\((verify_field, instance), proof_field) +// // &\ \ +// // &overline(prove)\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field))\ +// // &= ( +// // prove\((verify'_bool, (verify_bool, verify_field, instance)); (proof_bool, proof_field)), +// // prove\((verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field)) +// // )\ +// // &= (proof^1_bool, proof^1_field) +// // &\ \ +// // &verify'\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)), (proof'_bool, proof'_field)) +// // $ +// // - $prove\((verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field)) -> proof'_field$ +// // - $verify'\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)), (proof'_bool, proof'_field))$ +// // --- +// // - $prove\((verify'_bool, (verify'_bool, verify'_field, (verify_bool, verify_field, instance))); (proof'_bool, proof'_field)) -> proof''_bool$ +// // - $prove\((verify'_field, (verify'_bool, verify'_field, (verify_bool, verify_field, instance))); (proof'_bool, proof'_field)) -> proof''_field$ +// // - $verify\((verify'_bool, verify'_field, (verify'_bool, verify'_field, (verify'_bool, verify'_field, (verify_bool, verify_field, instance)))), (proof''_bool, proof''_field))$ +// // --- +// // - $prove\((verify_bool, ((verify_bool, instance),(verify_field, instance))); (proof_bool, proof_field)) -> proof_bool'$ +// // - $prove\((verify_field, ((verify_bool, instance),(verify_field, instance))); (proof_bool, proof_field)) -> proof_field'$ +// // - $verify\(((verify_bool, ((verify_bool, instance),(verify_field, instance))), (verify_field, ((verify_bool, instance),(verify_field, instance)))), (proof_0', proof_1'))$ + + +// // - typically, verification algorithms reinterpret data based on the field. +// // - expand proof to include prover-provided "scratch space", +// // - commit to this "expanded proof" +// // - have both VMs use the same expanded proof to +// // - verify programs must be tuned such that all values in the scratch space are +// // - checked by one of the two VMs and +// // - leveraged by other VM to speed up verification. +// // - + +// // - specific verify programs. + + + +// = Theory applied +// Applying these observations and design requirements to this VM, we present the following design + +// - separate field-VM (@field-VM) with its own `DECODE` table (@field-decode). + +// == Split Verification Algorithm(s) + +// === Verification of guest program proof +// #let FRI = raw("FRI") +// #let DEEP = raw("DEEP") +// #let LogUp = raw("LogUp") +// #let challenges = $bb(C)$ +// #let guestProgramCommitment = $cal(C)_cal(G)$ +// #let tableCommitments = $cal(C)_cal(T)$ +// #let logupCommitments = $cal(C)_cal(L)$ +// #let logupOpenings = $cal(O)_cal(L)$ +// #let quotientCommitments = $cal(C)_cal(Q)$ +// #let deepCommitments = $cal(C)_cal(D)$ +// #let deepOpenings = $cal(O)_cal(D)$ +// #let friFoldingCommitments = $cal(C)_cal(F)$ +// #let friQueryOpenings = $cal(O)_cal(F)$ +// #let proof = $bb(pi)$ +// #let expanded_proof = $proof^*$ +// #let fs = $#`FiatShamir`$ + +// #grid( +// columns: (1fr, auto), +// column-gutter: 1em, +// [ +// Proof contents: +// - #tableCommitments: the commitments to all AIR-tables, +// - #logupCommitments: the #LogUp commitments, +// - #logupOpenings: the #LogUp openings, +// - #deepCommitments: the #DEEP commitments, +// - #deepOpenings: the #DEEP openings, +// - #friFoldingCommitments: the #FRI folding commitments, and +// - #friQueryOpenings: the #FRI query openings. + +// *Native verification*: + +// input: +// - proof +// - public commitment (i.e., program + public input) +// verification steps: +// - derive lincomb challenges +// - derive segment challenges +// - derive DEEP point +// - derive LogUp challenges +// - verify LogUp opening proofs +// - verify LogUp openings sum to zero, +// - derive folding challenges +// - verify low-degreeness of FRI output, +// - derive FRI-query challenges, +// - verify FRI-query proofs, +// - verify folding was done correctly, +// - verify DEEP quotient/segmenting using DEEP-point. + +// *Split verification steps*: +// - communcation record: +// - all the challenges: lincomb, segment, DEEP point, LogUp, folding & query +// - binaryVM: verify +// - recorded lincomb challenges, +// - recorded segment challenges, +// - recorded DEEP point, +// - recorded LogUp challenges, +// - LogUp opening proofs, +// - recorded folding challenges, +// - recorded FRI-query challenges, and +// - FRI-query proofs. +// - fieldVM: verify +// - LogUp openings sum to zero, +// - low-degreeness of FRI output, +// - query opening are valid, +// - DEEP quotient/segmenting using DEEP-point. + +// ], +// figure(image("figures/DEEP-FRI_verification.svg", height: 90%)) +// ) + +// == Transformation +// - COMMIT to any public input +// -> this forces the verifier in the next-layer to include it in verifying this proof. +// - use + +// == Verification of verification-proof +// *Native verification steps*: +// - public input: +// - commitment of guest program + public parameters +// - private input: +// - guest program + public parameters +// - proof that guest program in R +// - steps: +// - commit to guest program: COMMIT to commitment. +// - _all of the above_, where +// - openings of guest program table are verified against that commitment + + + +// #let get = $arrow.l$ +// #let FS = $#`FiatShamir`$ + +// == Verify base +// Input: +// - instance: +// - #guestProgramCommitment: commitment to guest program. +// - proof: +// - #tableCommitments: commitments to all AIR-tables, +// - #logupCommitments: #LogUp commitments, +// - #logupOpenings: #LogUp openings, +// - #quotientCommitments: quotient commitments, +// - #deepCommitments: #DEEP commitments, +// - #deepOpenings: #DEEP openings, +// - #friFoldingCommitments: #FRI folding commitments, and +// - #friQueryOpenings: #FRI query openings. + +// Steps: +// + derive linear combination challenges, +// + derive segment challenges, +// + derive DEEP point, +// + derive LogUp challenges, +// + verify LogUp opening proofs, +// + verify LogUp openings sum to zero, +// + derive folding challenges, +// + verify low-degreeness of FRI output, +// + derive FRI-query challenges, +// + verify FRI-query proofs, +// + verify folding was done correctly, +// + verify DEEP quotient/segmenting using DEEP-point. + + +// - what needs to be done to verify a base proof, (see verification) +// - what extra needs to be done to do this usiing the split verifier, +// - what extra needs to be done to _prove_ this verification. + +// - what needs to be done to verify a recursive proof, +// - what extra needs to be done to do this using the split verifier, +// - what extra needs to be done to _prove_ this verification. // = L0 proof -// Let $proof\(g,x) := (#table_commitments, #DEEP_commitments, #DEEP_openings, #FRI_folding_commitments, #FRI_query_openings)$ denote a proof produced by the prover for program $g$ on public input $x$, with +// Let $proof\(g,x) := (#tableCommitments, #DEEP_commitments, #DEEP_openings, #FRI_folding_commitments, #FRI_query_openings)$ denote a proof produced by the prover for program $g$ on public input $x$, with // - #table_commitments the commitments to all AIR-tables, // - #DEEP_commitments the #DEEP commitments, // - #DEEP_openings the #DEEP openings, diff --git a/spec/verifier.typ b/spec/verifier.typ new file mode 100644 index 000000000..2635bf645 --- /dev/null +++ b/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. +// \ No newline at end of file From 408ab46c37abdd90e78374aaf7fcfab082961674 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 21 Aug 2026 11:55:55 +0200 Subject: [PATCH 4/7] spec/recursion: clean up --- spec/figures/DEEP-FRI_verification.md | 35 -- spec/figures/DEEP-FRI_verification.svg | 1 - spec/recursion.typ | 450 +------------------------ 3 files changed, 9 insertions(+), 477 deletions(-) delete mode 100644 spec/figures/DEEP-FRI_verification.md delete mode 100644 spec/figures/DEEP-FRI_verification.svg diff --git a/spec/figures/DEEP-FRI_verification.md b/spec/figures/DEEP-FRI_verification.md deleted file mode 100644 index 997dcaf93..000000000 --- a/spec/figures/DEEP-FRI_verification.md +++ /dev/null @@ -1,35 +0,0 @@ - - -title Proof verification -note over P,V: established: shared program with\npublic input -note over P: fill tables -P->V: batch-commit tables -group par [DEEP] -P<-V: lincomb challenges -P->V: quotient commitment -P<-V: segment challenges -P->V: segment commitment -P<-V: DEEP point -P->V: DEEP openings -else LogUp -P<-V: LogUp challenges -P->V: batch-commit to LogUp columns -P->V: open sum entries -note over V: checksum -end - -P->V: batch FRI-commit (implicitly) -loop Batch-FRI -P<-V: folding challenge -P->V: folding commitment -end -P->V: FRI low-degree output -note over V: verify low-degreeness -loop FRI-verify -note over V: sample folding\nchallenges -P<-V: challenges -P->V: openings -note over V: verify openings -note over V: verify folding\nsteps -end -note over V: verify DEEP \ No newline at end of file diff --git a/spec/figures/DEEP-FRI_verification.svg b/spec/figures/DEEP-FRI_verification.svg deleted file mode 100644 index 24e57a819..000000000 --- a/spec/figures/DEEP-FRI_verification.svg +++ /dev/null @@ -1 +0,0 @@ -title%20Proof%20verification%0Anote%20over%20P%2CV%3A%20established%3A%20shared%20program%20with%5Cnpublic%20input%0Anote%20over%20P%3A%20fill%20tables%0AP-%3EV%3A%20batch-commit%20tables%0Agroup%20par%20%5BDEEP%5D%0AP%3C-V%3A%20lincomb%20challenges%0AP-%3EV%3A%20quotient%20commitment%0AP%3C-V%3A%20segment%20challenges%0AP-%3EV%3A%20segment%20commitment%0AP%3C-V%3A%20DEEP%20point%0AP-%3EV%3A%20DEEP%20openings%0Aelse%20LogUp%0AP%3C-V%3A%20LogUp%20challenges%0AP-%3EV%3A%20batch-commit%20to%20LogUp%20columns%0AP-%3EV%3A%20open%20sum%20entries%0Anote%20over%20V%3A%20checksum%0Aend%0A%0AP-%3EV%3A%20batch%20FRI-commit%20(implicitly)%0Aloop%20Batch-FRI%0AP%3C-V%3A%20folding%20challenge%0AP-%3EV%3A%20folding%20commitment%0Aend%0AP-%3EV%3A%20FRI%20low-degree%20output%0Anote%20over%20V%3A%20verify%20low-degreeness%0Aloop%20FRI-verify%0Anote%20over%20V%3A%20sample%20folding%5Cnchallenges%0AP%3C-V%3A%20challenges%0AP-%3EV%3A%20openings%0Anote%20over%20V%3A%20verify%20openings%0Anote%20over%20V%3A%20verify%20folding%5Cnsteps%0Aend%0Anote%20over%20V%3A%20verify%20DEEPPVProof verificationestablished: shared program withpublic inputfill tablesbatch-commit tableslincomb challengesquotient commitmentsegment challengessegment commitmentDEEP pointDEEP openingsLogUp challengesbatch-commit to LogUp columnsopen sum entrieschecksumbatch FRI-commit (implicitly)folding challengefolding commitmentFRI low-degree outputverify low-degreenesssample foldingchallengeschallengesopeningsverify openingsverify foldingstepsverify DEEPpar[DEEP][LogUp]loop[Batch-FRI]loop[FRI-verify] \ No newline at end of file diff --git a/spec/recursion.typ b/spec/recursion.typ index 982fee2cd..a7c5b3758 100644 --- a/spec/recursion.typ +++ b/spec/recursion.typ @@ -56,8 +56,10 @@ We now assume the existence of _proving system_ $(prove, verify)$ with prover $prove: instanceSpace times witnessSpace mapsto proofSpace$ and verifier $verify: instanceCommitmentSpace times proofSpace mapsto BB$ such that $ -forall (instance, witness) in relation times witnessSpace &: prob[verify\(commit(instance), prove\(instance; witness)) = one | instance(witness) = one] = 1 \ -forall instance in instanceSpace without relation, forall proof in proofSpace &: prob[verify\(commit(instance), proof) = one] < epsilon +forall (instance, witness) in relation times witnessSpace +&: prob[verify\(commit(instance), prove\(instance; witness)) = one | instance(witness) = one] = 1 \ +forall instance in instanceSpace without relation, forall proof in proofSpace +&: prob[verify\(commit(instance), proof) = one] < epsilon $ with $epsilon$ negligibly small and $proofSpace$ the proof space. That is: any valid proof for a solvable instance verifies successfully, @@ -75,7 +77,8 @@ convincing them of the prover's claim. = Proof recursion Now observe that the verifier $verify$ is itself a function in $verifierSpace := {hat(f): instanceSpace times proofSpace mapsto BB} subset.eq functionSpace$. -This means that we can use $prove$ to prove that the verification of a proof $proof$ for a given instance $instance$ succeeds: +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. @@ -223,443 +226,8 @@ The prover performs the following steps: $ 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^((n)) &arrow.l prove(verify'_b || verify'_f, (commit(instance), [commit(verify'_b), commit(verify'_f)], 1, proof^((n-1)), record)) + proof^((i)) &arrow.l prove(verify'_b || verify'_f, (commit(instance), [commit(verify'_b), commit(verify'_f)], 1, proof^((i-1)), record)) $ -*Ultimate verification.* -$verify'(commit(instance), [commit(verify'_b), commit(verify'_f)], 1, proof^((n-1))) =? one$ - - - -// // #let bool = $#`B`$ -// // #let field = $#`F`$ -// // #let equal = $#`E`$ -// // #let consistency = $#`C`$ - - -// // - Let $verify_bool || verify_field := verify$ denote the decomposed verifier. -// // $ -// // prove\([verify_bool || verify_field, instance]; [proof, scratch]) = proof' -// // $ -// // $ -// // v'(instance, proof) := verify([verify_bool || verify_field, instance], proof) -// // $ -// // $ -// // verify\([verify_bool || verify_field, instance], proof')\ -// // // &=verify'\(instance, proof')\ -// // &=verify\([verify_bool, instance], proof') times verify\([verify_field, instance], proof')\ -// // $ -// // $ -// // &prove\([verify', [verify_bool || verify_field, instance]]; [proof', scratch'])\ -// // &=prove\([verify_bool || verify_field || verify_consistency, [verify, instance]]; proof')\ -// // // &=prove\([verify_bool\([verify, instance], dot) times verify_field\([verify, instance], dot); proof')\ -// // &=[ -// // prove\([verify_bool, [verify, instance]]; proof'), -// // prove\([verify_field, [verify, instance]]; proof'), -// // prove\([verify_consistency, [verify, instance]]; proof') -// // ]\ -// // &= [proof'_bool, proof'_field]\ -// // &= proof''\ -// // &\ \ -// // &prove\([verify, [verify, instance]]; proof')\ -// // &=prove\([verify_bool || verify_field, [verify, instance]]; proof')\ -// // &=[ -// // prove\([verify_bool, [verify, instance]]; proof'), -// // prove\([verify_field, [verify, instance]]; proof') -// // ]\ -// // &= [proof'_bool, proof'_field]\ -// // &= proof''\ -// // &\ \ -// // &verify\([verify, [verify, instance]], proof'')\ -// // &=verify\([verify_bool || verify_field, [verify, instance]], [proof'_bool, proof'_field])\ -// // &=verify\([verify_bool, instance], proof'_bool) times verify\([verify_field, instance], proof'_field)\ -// // $ -// // --- -// // - $prove\((verify_bool, instance); proof) -> proof_bool$ -// // - $prove\((verify_field, instance); proof) -> proof_field$ -// // - $verify\(((verify_bool, instance),(verify_field, instance)), (proof_bool, proof_field)) $ -// // --- -// // $ -// // &verify'\((verify_bool, verify_field, instance), (proof_bool, proof_field)) \ -// // &= verify((verify_bool, instance), proof_bool) times verify\((verify_field, instance), proof_field) -// // &\ \ -// // &overline(prove)\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field))\ -// // &= ( -// // prove\((verify'_bool, (verify_bool, verify_field, instance)); (proof_bool, proof_field)), -// // prove\((verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field)) -// // )\ -// // &= (proof^1_bool, proof^1_field) -// // &\ \ -// // &verify'\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)), (proof'_bool, proof'_field)) -// // $ -// // - $prove\((verify'_field, (verify_bool, verify_field, instance)); (proof_bool, proof_field)) -> proof'_field$ -// // - $verify'\((verify'_bool, verify'_field, (verify_bool, verify_field, instance)), (proof'_bool, proof'_field))$ -// // --- -// // - $prove\((verify'_bool, (verify'_bool, verify'_field, (verify_bool, verify_field, instance))); (proof'_bool, proof'_field)) -> proof''_bool$ -// // - $prove\((verify'_field, (verify'_bool, verify'_field, (verify_bool, verify_field, instance))); (proof'_bool, proof'_field)) -> proof''_field$ -// // - $verify\((verify'_bool, verify'_field, (verify'_bool, verify'_field, (verify'_bool, verify'_field, (verify_bool, verify_field, instance)))), (proof''_bool, proof''_field))$ -// // --- -// // - $prove\((verify_bool, ((verify_bool, instance),(verify_field, instance))); (proof_bool, proof_field)) -> proof_bool'$ -// // - $prove\((verify_field, ((verify_bool, instance),(verify_field, instance))); (proof_bool, proof_field)) -> proof_field'$ -// // - $verify\(((verify_bool, ((verify_bool, instance),(verify_field, instance))), (verify_field, ((verify_bool, instance),(verify_field, instance)))), (proof_0', proof_1'))$ - - -// // - typically, verification algorithms reinterpret data based on the field. -// // - expand proof to include prover-provided "scratch space", -// // - commit to this "expanded proof" -// // - have both VMs use the same expanded proof to -// // - verify programs must be tuned such that all values in the scratch space are -// // - checked by one of the two VMs and -// // - leveraged by other VM to speed up verification. -// // - - -// // - specific verify programs. - - - -// = Theory applied -// Applying these observations and design requirements to this VM, we present the following design - -// - separate field-VM (@field-VM) with its own `DECODE` table (@field-decode). - -// == Split Verification Algorithm(s) - -// === Verification of guest program proof -// #let FRI = raw("FRI") -// #let DEEP = raw("DEEP") -// #let LogUp = raw("LogUp") -// #let challenges = $bb(C)$ -// #let guestProgramCommitment = $cal(C)_cal(G)$ -// #let tableCommitments = $cal(C)_cal(T)$ -// #let logupCommitments = $cal(C)_cal(L)$ -// #let logupOpenings = $cal(O)_cal(L)$ -// #let quotientCommitments = $cal(C)_cal(Q)$ -// #let deepCommitments = $cal(C)_cal(D)$ -// #let deepOpenings = $cal(O)_cal(D)$ -// #let friFoldingCommitments = $cal(C)_cal(F)$ -// #let friQueryOpenings = $cal(O)_cal(F)$ -// #let proof = $bb(pi)$ -// #let expanded_proof = $proof^*$ -// #let fs = $#`FiatShamir`$ - -// #grid( -// columns: (1fr, auto), -// column-gutter: 1em, -// [ -// Proof contents: -// - #tableCommitments: the commitments to all AIR-tables, -// - #logupCommitments: the #LogUp commitments, -// - #logupOpenings: the #LogUp openings, -// - #deepCommitments: the #DEEP commitments, -// - #deepOpenings: the #DEEP openings, -// - #friFoldingCommitments: the #FRI folding commitments, and -// - #friQueryOpenings: the #FRI query openings. - -// *Native verification*: - -// input: -// - proof -// - public commitment (i.e., program + public input) -// verification steps: -// - derive lincomb challenges -// - derive segment challenges -// - derive DEEP point -// - derive LogUp challenges -// - verify LogUp opening proofs -// - verify LogUp openings sum to zero, -// - derive folding challenges -// - verify low-degreeness of FRI output, -// - derive FRI-query challenges, -// - verify FRI-query proofs, -// - verify folding was done correctly, -// - verify DEEP quotient/segmenting using DEEP-point. - -// *Split verification steps*: -// - communcation record: -// - all the challenges: lincomb, segment, DEEP point, LogUp, folding & query -// - binaryVM: verify -// - recorded lincomb challenges, -// - recorded segment challenges, -// - recorded DEEP point, -// - recorded LogUp challenges, -// - LogUp opening proofs, -// - recorded folding challenges, -// - recorded FRI-query challenges, and -// - FRI-query proofs. -// - fieldVM: verify -// - LogUp openings sum to zero, -// - low-degreeness of FRI output, -// - query opening are valid, -// - DEEP quotient/segmenting using DEEP-point. - -// ], -// figure(image("figures/DEEP-FRI_verification.svg", height: 90%)) -// ) - -// == Transformation -// - COMMIT to any public input -// -> this forces the verifier in the next-layer to include it in verifying this proof. -// - use - -// == Verification of verification-proof -// *Native verification steps*: -// - public input: -// - commitment of guest program + public parameters -// - private input: -// - guest program + public parameters -// - proof that guest program in R -// - steps: -// - commit to guest program: COMMIT to commitment. -// - _all of the above_, where -// - openings of guest program table are verified against that commitment - - - -// #let get = $arrow.l$ -// #let FS = $#`FiatShamir`$ - -// == Verify base -// Input: -// - instance: -// - #guestProgramCommitment: commitment to guest program. -// - proof: -// - #tableCommitments: commitments to all AIR-tables, -// - #logupCommitments: #LogUp commitments, -// - #logupOpenings: #LogUp openings, -// - #quotientCommitments: quotient commitments, -// - #deepCommitments: #DEEP commitments, -// - #deepOpenings: #DEEP openings, -// - #friFoldingCommitments: #FRI folding commitments, and -// - #friQueryOpenings: #FRI query openings. - -// Steps: -// + derive linear combination challenges, -// + derive segment challenges, -// + derive DEEP point, -// + derive LogUp challenges, -// + verify LogUp opening proofs, -// + verify LogUp openings sum to zero, -// + derive folding challenges, -// + verify low-degreeness of FRI output, -// + derive FRI-query challenges, -// + verify FRI-query proofs, -// + verify folding was done correctly, -// + verify DEEP quotient/segmenting using DEEP-point. - - -// - what needs to be done to verify a base proof, (see verification) -// - what extra needs to be done to do this usiing the split verifier, -// - what extra needs to be done to _prove_ this verification. - -// - what needs to be done to verify a recursive proof, -// - what extra needs to be done to do this using the split verifier, -// - what extra needs to be done to _prove_ this verification. - -// = L0 proof -// Let $proof\(g,x) := (#tableCommitments, #DEEP_commitments, #DEEP_openings, #FRI_folding_commitments, #FRI_query_openings)$ denote a proof produced by the prover for program $g$ on public input $x$, with -// - #table_commitments the commitments to all AIR-tables, -// - #DEEP_commitments the #DEEP commitments, -// - #DEEP_openings the #DEEP openings, -// - #FRI_folding_commitments the #FRI folding commitments, and -// - #FRI_query_openings the #FRI query openings. - - -// = Verifying an L0 proof -// Let $#fs\(proof) -> challenges$ denote the deterministic map producing the challenges corresponding to a given proof. -// We construct an _expanded proof_ $#expanded_proof := (proof, #fs\(proof)) = (proof, #`prog_comm`, challenges)$ containing the original proof, a commitment to the original guest program (including public parameters), and the challenges required for verification. - -// The program commitment #`prog_comm` can be a commitment to the public information of a specific proof, e.g., the hash of the commitments to the `DECODE` table(s) and all public `PAGE` tables. - -// Next, let us define two verification programs: - -// ``` -// func verify_L0_binary(proof: Proof, prog_comm, challenges) -> Proof: -// commit(prog_comm) # through printing to stdout -// assert challenges == fiatShamir(proof) -// assert verify_FRI_query_proofs(proof, challenges) - -// func verify_L0_field(proof: Proof, _prog_comm, challenges) -> Proof: -// assert verify_DEEP_openings(proof, challenges) -// assert verify_FRI_folding(proof, challenges) -// assert verify_FRI_output_is_low_degree(proof, challenges) -// assert verify_LogUp_equals_zero(proof, challenges) - -// func proof_L0_verification(prog_comm, proof: Proof) -> DoubleProof: -// challenges = fiatShamir_risc5VM(proof) -// input_commitment = commit((prog_comm, proof, challenges)) -// proof0: Proof = risc5VM.prove(verify_L0_binary, input_commitment) -// proof1: Proof = fieldVM.prove(verify_L0_field, input_commitment) -// return (input_commitment, proof0, proof1) -// ``` - -// = Verifying an L1 proof - -// ``` -// func verify_L1_binary(proof: Proof, prog_comm, challenges) -> Proof: -// commit(prog_comm) # through printing to stdout -// assert challenges.c0 == fiatShamir_risc5VM(proof) -// assert challenges.c1 == fiatShamir_fieldVM(proof) -// assert verify_FRI_query_proofs(proof.p0, challenges.c0) -// assert verify_FRI_query_proofs(proof.p1, challenges.c1) - -// func verify_L1_field(proof, prog_comm, challenges) -> Proof: -// assert verify_DEEP_openings(proof.p0, challenges.c0) -// assert verify_DEEP_openings(proof.p1, challenges.c1) -// assert verify_FRI_folding(proof.p0, challenges.c0) -// assert verify_FRI_folding(proof.p1, challenges.c1) -// assert verify_FRI_output_is_low_degree(proof.p0, challenges.c0) -// assert verify_FRI_output_is_low_degree(proof.p1, challenges.c1) - -// # compute verifier contribution to the risc5VM's LogUp -// vc = compute_commitment_contribution(challenges.c0, prog_comm) -// assert verify_LogUp_equals_zero(proof.p0 + vc, challenges.c0) -// assert verify_LogUp_equals_zero(proof.p1, challenges.c1) - -// func proof_L1_verification(_prog_comm, proof: DoubleProof) -> DoubleProof: -// c0 = fiatShamir_risc5VM((proof.input_comm, proof.p0)) -// c1 = fiatShamir_fieldVM((proof.input_comm, proof.p1)) -// challenges = (c0, c1) - -// input_commitment = commit((_prog_comm, proof, challenges)) -// proof0: Proof = risc5VM.prove(verify_L1_binary, input_commitment) -// proof1: Proof = fieldVM.prove(verify_L1_field, input_commitment) -// return (input_commitment, proof0, proof1) -// ``` - - - - - -// = Recursion -// - proof system generates proof -// - proof is still quite large -// - rather than verify the proof itself, have the prover generate proof that the verification of the first proof succeeds, where this new proof is smaller than the first. -// - repeat until the desired proof size is reached -// - at the end, verify this "recursed" proof. -// - this is commonly called "proof recursion" - -// - one important aspect, is that the _recursed proof_ should be tied to the original, base proof. - -// = Recursion components -// Three different configurations -// + prove_guest_program(guest_program) -> proof -// + prove_single_proof_verification(proof) -> double_proof -// + prove_double_proof_verification(double_proof) -> double_proof - -// == Proving a guest program -// -> take guest program -// > generate proof - -// contents of proof: -// - table commitments -// - DEEP commitments -// - DEEP openings -// - FRI folding commitments -// - FRI query openings (= node content + merkle path) - -// == Proving the verification of a proof -// - expand proof to proof_with_challenges -// - commit to proof_with_challenges (e.g., as PAGES tables) -// - binaryVM runs program "verify_binary", with commitment as instance and (proof, challenges) as witness -// - commits to the `commitment` by printing it to `stdout` -// - verifies that: -// - FRI query proofs are valid -// - challenges are correctly derived from the proof transcript -// - fieldVM runs program "verify_field" with commitment as instance and (proof, challenges) as witness: -// - verifies that: -// - DEEP opening is valid -// - FRI folding was done correctly. -// - generate two proofs, with a *shared commitment to the memory init/fini of the commitment* -// -> (shared_commitment, proof_binary_vm, proof_field_vm) - -// == Proving the verification of a double-proof -// - expand proofs to proof_with_challenges -// - commit to proof_with_challenges (e.g., as PAGES tables) -// - binaryVM runs program "verify_binary", with commitment as instance and (proof, challenges) as witness -// - commits to the `commitment` by printing it to `stdout` -// - verifies that: -// - FRI query proofs are valid -// - challenges are correctly derived from the proof transcript -// - fieldVM runs program "verify_field" with commitment as instance and (proof, challenges) as witness: -// - verifies that: -// - DEEP opening is valid -// - FRI folding was done correctly. - - - - - -// // Keys -// #let ProverKey = $KK$ -// #let VerifKey = $VV$ - -// // Spaces -// #let instanceSpace = $XX$ -// #let witnessSpace = $WW$ -// #let outSpace = $BB$ -// #let hashOutSpace = $HH$ -// #let proofSpace = $Pi$ - -// Let $PP: XX times WW mapsto BB$ denote the collection of guest programs mapping a (public) _instance_ $x in XX$ and (private) witness - -// - L0: proof $arrow.l$ prove(guest_program, input) -// - L1: (proof0, proof1) $arrow.l$ prove(verify_proof(proof)) -// - L2+: (proof0, proof1) $arrow.l$ prove(verify_proof(proof)) - -// Level 0: -// - instance: program ELF, public inputs -// - witness: private inputs - -// Proof L0: -// - setup: -// - turn ELF, public inputs into DECODE table -// - comm = commit to DECODE table -// - prover: -// - proof $arrow.l$ prove(comm, witness) - - -// prover: -// - runs prove() - -// Level 0: -// $ -// text("program space: ") -// && PP &:&& instanceSpace times witnessSpace &&mapsto outSpace\ -// text("preprocessor space: ") -// && PP PP &:&& PP times instanceSpace &&mapsto ProverKey times VerifKey\ -// text("L0 prover: ") -// && #`p` &in&& ProverKey times witnessSpace &&mapsto proofSpace\ -// text("L0 verifier: ") -// && #`v` &in&& VerifKey times proofSpace &&mapsto outSpace -// $ - -// Level 1: -// $ -// text("program: ") -// && p' &in&& [hashOutSpace] times [VerifKey times proofSpace times witnessSpace'] &&mapsto outSpace\ -// text("preprocessor: ") -// && #`pp`' &:&& p' times hashOutSpace &&mapsto ProverKey' times VerifKey'\ -// text("L1 prover: ") -// && #`p`' &in&& ProverKey' times [VerifKey times proofSpace times witnessSpace'] &&mapsto proofSpace' := proofSpace times proofSpace\ -// text("L1 verifier: ") -// && #`v`' &in&& VerifKey' times proofSpace' &&mapsto outSpace -// $ - -// Level 2 - $inf$: -// $ -// text("program: ") -// && p_2 &in&& [hashOutSpace] times [VerifKey' times proofSpace' times witnessSpace'] &&mapsto outSpace\ -// text("preprocessor: ") -// && #`pp`_2 &:&& p_2 times hashOutSpace &&mapsto ProverKey' times VerifKey'\ -// text("L2 prover: ") -// && #`p`_2 &in&& ProverKey' times [VerifKey' times proofSpace' times witnessSpace'] &&mapsto proofSpace'\ -// text("L2 verifier: ") -// && #`v`_2 &in&& VerifKey' times proofSpace' &&mapsto outSpace -// $ - -// s.t. $(#`h`, #`vk`, #`π`) mapsto #`H` (#`vk`) = #`h` text("and") #`verify` (#`vk`, #`π`) = 1$ - - -// $ -// #`program<`XX #`>` (WW) mapsto BB -// $ +*Final verification.* +$verify'(commit(instance), [commit(verify'_b), commit(verify'_f)], 1, proof^((n))) =? one$ From ab117fa00bcd61c44581df0b9de11d40eb21fcda Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 21 Aug 2026 12:07:11 +0200 Subject: [PATCH 5/7] spec/recursion: more cleanup --- spec/recursion.typ | 69 ++++++++++++++++++++-------------------------- 1 file changed, 30 insertions(+), 39 deletions(-) diff --git a/spec/recursion.typ b/spec/recursion.typ index a7c5b3758..88d3359c7 100644 --- a/spec/recursion.typ +++ b/spec/recursion.typ @@ -2,34 +2,25 @@ #show: book-page("recursion.typ") - -// Outline -#let binaryVM = raw("binaryVM") -#let fieldVM = raw("fieldVM") - - -#let functionSpace = $cal(F)$ -#let verifierSpace = $cal(V)$ -#let privateFunctionSpace = $hat(cal(F))$ -#let program = $f$ -#let inputSpace = $II$ -#let input = $bb(i)$ -#let instanceSpace = $XX$ -#let instanceCommitmentSpace = $CC$ -#let instance = $bb(x)$ -#let instance2 = $bb(y)$ -#let witnessSpace = $WW$ -#let witness = $bb(w)$ -#let proofSpace = $bb(Pi)$ -#let proof = $bb(pi)$ -#let prove = $italic("p")$ -#let verify = $italic("v")$ +// Spaces and instances +#let (functionSpace, function) = ($cal(F)$, $bb(f)$) +#let (inputSpace, input) = ($II$, $bb(i)$) +#let (instanceSpace, instance) = ($XX$, $bb(x)$) +#let (witnessSpace, witness) = ($WW$, $bb(w)$) +#let (proofSpace, proof) = ($bb(Pi)$, $bb(pi)$) + +#let (commitmentSpace, commitment) = ($CC$, $bb(c)$) #let commit(x) = $overline(#x)$ #let comm(x) = $commit(#x)$ -#let one = $bb(1)$ -#let zero = $bb(0)$ -#let function = $bb(f)$ + +#let program = $f$ #let relation = $cal(R)$ + +#let verifierSpace = $cal(V)$ +#let (prove, verify) = ($italic("p")$, $italic("v")$) + +// Mathematical symbols +#let (zero, one) = ($bb(0)$, $bb(1)$) #let iff = $arrow.double.l.r$ #let implies = $arrow.double.r$ #let prob = $PP$ @@ -49,12 +40,12 @@ as the set of all _solvable instances_, i.e., all instances $instance in instanceSpace$ for which there exists a witness $witness in witnessSpace$ such that $instance\(witness) = one$. -Lastly, we introduce the commitment function $c: instanceSpace mapsto instanceCommitmentSpace$. +Lastly, we introduce the commitment function $c: instanceSpace mapsto commitmentSpace$. To simplify notation, we use $commit(instance) = c(instance)$. We now assume the existence of _proving system_ $(prove, verify)$ with prover $prove: instanceSpace times witnessSpace mapsto proofSpace$ and -verifier $verify: instanceCommitmentSpace times proofSpace mapsto BB$ such that +verifier $verify: commitmentSpace times proofSpace mapsto BB$ such that $ forall (instance, witness) in relation times witnessSpace &: prob[verify\(commit(instance), prove\(instance; witness)) = one | instance(witness) = one] = 1 \ @@ -76,7 +67,7 @@ convincing them of the prover's claim. = Proof recursion Now observe that the verifier $verify$ is itself a function in -$verifierSpace := {hat(f): instanceSpace times proofSpace mapsto BB} subset.eq functionSpace$. +$verifierSpace := {hat(f): commitmentSpace times proofSpace mapsto BB} subset.eq functionSpace$. This means that we can use $prove$ to prove that the verification of a proof $proof$ for a given instance $instance$ succeeds: $ @@ -108,15 +99,15 @@ 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': instanceCommitmentSpace^2 times {0, 1} times proofSpace: (c_0, c_1, b, proof) mapsto + verify': commitmentSpace^2 times {0, 1} times proofSpace: (commitment_0, commitment_1, b, proof) mapsto cases( - verify(c_0, proof) &text("if") b=0, - verify(c_1(c_0, c_1, dot), proof) &text("if") b=1 + verify(commitment_0, proof) &text("if") b=0, + verify(commitment_1(commitment_0, commitment_1, dot), proof) &text("if") b=1 ) $ where it is assumed that $comm(function(x_1, x_2, dot))$ can be easily constructed from $comm(function), comm(x_1)$, and $comm(x_2)$. -By choosing $c_0 = commit(instance)$ and $c_1 = commit(verify')$, the prover can then prove +By choosing $commitment_0 = commit(instance)$ and $commitment_1 = commit(verify')$, the prover can then prove the base case by selecting $b=0$, and set $b=1$ during further recursion. Then, when presented with depth-n proof $proof^((n))$ and base instance $instance$, the verifier executes @@ -203,20 +194,20 @@ Below, we provide a division that, in theory, is expected to achieve solid perfo *Record $record$.* The record contains all challenges the prover derived using Fiat-Shamir. -*Tasks for $verify'_b\(c_0, c_1, b, proof, record)$:* +*Tasks for $verify'_b\(commitment_0, commitment_1, b, proof, record)$:* + assert that $b in {0, 1}$, + verify challenges on record $record$ according to Fiat-Shamir, + verify the various opening proofs; - if $b=0$: - verify binary-VM DECODE table (@decode) query opening against $c_0$ + verify binary-VM DECODE table (@decode) query opening against $commitment_0$ - if $b=1$: - verify binary-VM DECODE table (@decode) query opening against $c_(1,b)$ and - verify field-VM DECODE table (@field-decode) query opening against $c_(1,f)$ -+ `COMMIT` to $c_0$ and $c_1$ (see @commit) + verify binary-VM DECODE table (@decode) query opening against $commitment_(1,b)$ and + verify field-VM DECODE table (@field-decode) query opening against $commitment_(1,f)$ ++ `COMMIT` to $commitment_0$ and $commitment_1$ (see @commit) -*Tasks $verify'_f\(c_0, c_1, b, proof, record)$:* +*Tasks $verify'_f\(commitment_0, commitment_1, b, proof, record)$:* + verify LogUp openings sum to zero, - - if $b=1$, use $c_0$ and $c_1$ to complete the `COMMIT` balance. + - if $b=1$, use $commitment_0$ and $commitment_1$ to complete the `COMMIT` balance. + verify `DEEP` evaluation + verify `FRI` folding + verify `FRI` output low degreeness check. From b430d3d1a96c29fe06abde0ff1a221af457f7fad Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Wed, 26 Aug 2026 10:14:11 +0200 Subject: [PATCH 6/7] Apply suggestions from code review Co-authored-by: Robin Jadoul --- spec/recursion.typ | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/recursion.typ b/spec/recursion.typ index 88d3359c7..00ebe5016 100644 --- a/spec/recursion.typ +++ b/spec/recursion.typ @@ -43,7 +43,7 @@ $instance\(witness) = one$. Lastly, we introduce the commitment function $c: instanceSpace mapsto commitmentSpace$. To simplify notation, we use $commit(instance) = c(instance)$. -We now assume the existence of _proving system_ $(prove, verify)$ with +We now assume the existence of _proof system_ $(prove, verify)$ with prover $prove: instanceSpace times witnessSpace mapsto proofSpace$ and verifier $verify: commitmentSpace times proofSpace mapsto BB$ such that $ @@ -78,8 +78,8 @@ 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 _succint_ proving systems where proof size -typically shrinks (and verification time therefore reduces) as the level of recursion increases. +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. @@ -157,7 +157,7 @@ results of binary arithmetic are used to verify field arithmetical constraints 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. -This architecture enables the required communications by introducing a +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. From f293a728e2bb38bfb05ff4aa5e5346d45bc0757f Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 26 Aug 2026 10:34:05 +0200 Subject: [PATCH 7/7] spec/recursion: address code review comments --- spec/recursion.typ | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/spec/recursion.typ b/spec/recursion.typ index 00ebe5016..d801f6570 100644 --- a/spec/recursion.typ +++ b/spec/recursion.typ @@ -3,13 +3,13 @@ #show: book-page("recursion.typ") // Spaces and instances -#let (functionSpace, function) = ($cal(F)$, $bb(f)$) +#let (functionSpace, function) = ($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)$, $bb(pi)$) -#let (commitmentSpace, commitment) = ($CC$, $bb(c)$) +#let (commitmentSpace, commitment) = ($cal(C)$, $bb(c)$) #let commit(x) = $overline(#x)$ #let comm(x) = $commit(#x)$ @@ -29,7 +29,7 @@ = Notation Let $BB := { zero, one }$ denote the boolean set and let -$functionSpace := {f: inputSpace times witnessSpace mapsto BB}$ denote +$functionSpace := {function: inputSpace times witnessSpace mapsto BB}$ denote the set of functions mapping the (public) input space $inputSpace$ and (private) witness space $witnessSpace$ to this set. We use $instanceSpace := functionSpace times inputSpace = {instance: witnessSpace mapsto BB}$ @@ -40,8 +40,12 @@ as the set of all _solvable instances_, i.e., all instances $instance in instanceSpace$ for which there exists a witness $witness in witnessSpace$ such that $instance\(witness) = one$. -Lastly, we introduce the commitment function $c: instanceSpace mapsto commitmentSpace$. -To simplify notation, we use $commit(instance) = c(instance)$. +Lastly, we introduce the instance commitment function $c: instanceSpace mapsto 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 mapsto proofSpace$ and