From 187edc3c088bb8bf2ba8aafeaf159a8e981e3fda Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 14 Aug 2026 12:31:56 +0200 Subject: [PATCH 1/5] 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/5] 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/5] 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/5] 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/5] 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.