From 0ecc4e8287515be9df3388b035a15a792f79541e Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 14 Aug 2026 12:31:56 +0200 Subject: [PATCH 01/16] spec: recursive verification explanation, pt1 --- spec/chapters/field.typ | 1 + spec/chapters/field_decode.typ | 2 + spec/chapters/recursion.typ | 459 +++++++++++++++++++++++++ spec/figures/DEEP-FRI_verification.md | 32 ++ spec/figures/DEEP-FRI_verification.svg | 1 + spec/meta.typ | 5 + 6 files changed, 500 insertions(+) create mode 100644 spec/chapters/field.typ create mode 100644 spec/chapters/field_decode.typ create mode 100644 spec/chapters/recursion.typ create mode 100644 spec/figures/DEEP-FRI_verification.md create mode 100644 spec/figures/DEEP-FRI_verification.svg diff --git a/spec/chapters/field.typ b/spec/chapters/field.typ new file mode 100644 index 000000000..1333ed77b --- /dev/null +++ b/spec/chapters/field.typ @@ -0,0 +1 @@ +TODO diff --git a/spec/chapters/field_decode.typ b/spec/chapters/field_decode.typ new file mode 100644 index 000000000..6921ceac3 --- /dev/null +++ b/spec/chapters/field_decode.typ @@ -0,0 +1,2 @@ + +TODO diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ new file mode 100644 index 000000000..d8d47a9aa --- /dev/null +++ b/spec/chapters/recursion.typ @@ -0,0 +1,459 @@ +#import "/meta.typ": et, aside + + +// 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 +// $ 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/meta.typ b/spec/meta.typ index fc6bc783b..885947d4e 100644 --- a/spec/meta.typ +++ b/spec/meta.typ @@ -52,6 +52,11 @@ ("ecsm", [`ECSM` accelerator], ), ("fext", [Extension field accelerator], ), )), + ("RECURSION", ( + ("recursion", [Recursive verification], ), + ("field", [`Field` VM], ), + ("field_decode", [`Field` `DECODE` table], ), + )), ("MATHEMATICS", ( ("limbs_and_carries", [On limb decomposition and carries], ), )) From c3652e7c39e178c15e9fc1cfd41c4220545ef32e Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 14 Aug 2026 12:49:20 +0200 Subject: [PATCH 02/16] spec/recursion: put text and figure side-by-side --- spec/chapters/recursion.typ | 62 ++++++++++++++++++++----------------- 1 file changed, 34 insertions(+), 28 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index d8d47a9aa..c4fa91471 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -217,34 +217,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 b89ff299ba618e9cc7ba8214a61d2a83cacefec7 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 21 Aug 2026 11:53:53 +0200 Subject: [PATCH 03/16] spec/recursion: overhaul --- spec/book.typ | 236 ++++++++++ spec/chapters/recursion.typ | 620 ++++++++++++++++--------- spec/chapters/verifier.typ | 4 + spec/figures/DEEP-FRI_verification.md | 11 +- spec/figures/DEEP-FRI_verification.svg | 2 +- spec/meta.typ | 1 + 6 files changed, 658 insertions(+), 216 deletions(-) create mode 100644 spec/book.typ create mode 100644 spec/chapters/verifier.typ diff --git a/spec/book.typ b/spec/book.typ new file mode 100644 index 000000000..847730933 --- /dev/null +++ b/spec/book.typ @@ -0,0 +1,236 @@ +#import "@preview/shiroa:0.3.1": * +#import "/templates/page.typ": project +#import "@preview/equate:0.3.2": equate + +#show: book + +#let meta = ( + title: "Lambda VM specification", + authors: ("3MI Labs", "Aligned"), + version: "0.2", + summary: ( + ("PROOF SYSTEM", ( + ("logup.typ", [`LogUp` argument], ), + ("memory.typ", [Memory argument], ), + ("streaming.typ", [Streaming prover], ), + ("verifier.typ", [Verification], ) + )), + ("OVERVIEW", ( + ("variables.typ", [Variables], ), + ("signatures.typ", [Signatures], ), + )), + ("TEMPLATES", ( + ("is_bit.typ", [`IS_BIT` template], ), + ("is_byte.typ", [`IS_BYTE` template], ), + ("sign.typ", [`SIGN` template], ), + ("add.typ", [`ADD`/`SUB` template], ), + ("neg.typ", [`NEG` template], ), + ("reg.typ", [`REG`/`REGW` template], ), + )), + ("CPU", ( + ("decode.typ", [`DECODE` table], ), + ("cpu.typ", [`CPU` chip], ), + ("cpu32.typ", [`CPU32` chip], ), + )), + ("ALU", ( + ("shift.typ", [`SHIFT` chip], ), + ("branch.typ", [`BRANCH` chip], ), + ("lt.typ", [`LT` chip], ), + ("eq.typ", [`EQ` chip], ), + ("mul.typ", [`MUL` chip], ), + ("dvrm.typ", [`DVRM` chip], ), + ("bitwise.typ", [`BITWISE` chips], ), + ("bytewise.typ", [`BYTEWISE` chip], ) + )), + ("MEMORY", ( + ("memw.typ", [`MEMW` chip], ), + ("load.typ", [`LOAD` chip], ), + ("store.typ", [`STORE` chip], ), + )), + ("ECALLS", ( + ("about_ecalls.typ", [About `ECALL`], ), + ("halt.typ", [`HALT` chip], ), + ("commit.typ", [`COMMIT` chip], ), + ("sha256.typ", [`SHA256` accelerator], ), + ("keccak.typ", [`KECCAK` accelerator], ), + ("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], ), + )) + ) +) +#let meta_sections = meta.summary.map(m => m.at(1)).sum() +#book-meta( + title: meta.title, + authors: meta.authors, + summary: prefix-chapter("front.typ", meta.title) + + meta.summary.map( + ((title, sections)) => { + heading(depth: 1, title) + sections.map(((ch, title, _ref)) => chapter(ch, title)).join() + } + ).join() +) + +#let highlights = ( + "aside": ("Aside", rgb("55aaff")), + "attention": ("Attention", rgb("ff2600")), +) + +#let highlight(title, body, ref: none, kind: "aside") = [ + #figure( + caption: title, + supplement: highlights.at(kind).at(0), + kind: kind, + body + )#ref +] + +#let aside = highlight.with(kind: "aside") +#let attention = highlight.with(kind: "attention") + +#let common-formatting(body) = { + set footnote(numbering: "[1]") + show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt) + show ref: equate.with(sub-numbering: true, breakable: true, number-mode: "label") + show selector.or(..highlights.keys().map(k => figure.where(kind: k))): it => { + set figure.caption(position: top) + show figure.caption: cap => block( + inset: (left: 1em, right: 1em, top: .75em, bottom: .75em), + outset: (left: 1em), + width: 100% + 1em, + fill: highlights.at(it.kind).at(1), + stroke: luma(50%), + align(center, strong(text(fill: black, cap))) + ) + block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: luma(50%), breakable: false, align(left, it)) + } + body +} + + +#let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.4em, radius: 20%, stroke: black)[ + #set text(fill: foreground) + *TODO #if name != none { [(#name)] }*: #body +] +#let rj = todo.with(background: teal, name: "Robin") +#let et = todo.with(background: rgb("d4aa3a"), name: "Erik") +#let cdsg = todo.with(background: olive, name: "Cyprien") + + +#let is-shiroa = "x-target" in sys.inputs + +// Strip styling to keep only "pure" content. +// This is useful to avoid errors on the `set document(...)` in `project` +// when invisibly including other chapters to resolve xrefs. +#let strip-all(content) = { + if repr(content.func()) == "sequence" { + for c in content.children { + strip-all(c) + } + } else if repr(content.func()) == "styled" { + strip-all(content.child) + } else { + content + } +} + +#let _toplevel = state("_toplevel", none) +#let _xref-included = state("_xref-included", (:)) + +// Invisibly include another chapter, so that its labels can be resolved +#let xref-include(f) = { + show ref: none + context { + place(hide(box(width: auto, height: 0%, strip-all(include "/" + f)))) + } +} + +// Generate a cross-link for references to other chapters. +// Leaves the ref untouched if it can't be resolved or points to the current chapter. +#let xref(rf) = { + assert(is-shiroa, message: "xref should only be used when compiling for shiroa") + let lbl = rf.target + let found = meta_sections.find(((_, _, tag)) => str(lbl).starts-with(str(tag))) + context if found != none and found.at(0) != _toplevel.final() { + let (ch, title, ref) = found + if ref == lbl { + cross-link("/" + ch, [Chapter #(meta_sections.position(x => x == found) + 1)]) + } else { + // Because shiroa does weird url escaping + let shiroa-label = label(str(lbl).replace(":", "%3A")) + context _xref-included.update(x => x + ((ch): true)) + // The ideal would be to use `rf` directly as content argument to `cross-link`, + // as that would inherit any/all formatting of the ref we want or need. + // Unfortunately the ref link seems to take precedence over the cross-link hyperlink + // when clicking. + // There may still be some way around it by messing with some html output + let link-content = context { + let fig = query(lbl).first() + let counter = if fig.has("counter") { + fig.counter + } else { + counter(fig.func()) + } + + let supplement = if rf.supplement == auto { + fig.fields().at("supplement", default: none) + } else { + rf.supplement + } + [#supplement #numbering(fig.numbering, ..counter.at(lbl))] + } + cross-link("/" + ch, reference: shiroa-label, link-content) + } + } else { + rf + } +} + +#let book-page(file, ..args) = { + if not file.ends-with(".typ") { + file = lower(file) + ".typ" + } + + assert(meta_sections.find(s => s.at(0) == file) != none, message: "Couldn't resolve typst source file " + file) + + if is-shiroa { + (body) => { + show: common-formatting + context _toplevel.update(s => { + if s == none { + file + } else { + s + } + }) + let cond() = _toplevel.final() == file + show ref: it => context if cond() { xref(it) } + let title = context { + // Strip raw, because shiroa already makes the title raw + show raw: it => it.text + meta_sections.find(x => x.at(0) == _toplevel.final()).at(1) + } + project.with(..args, title: title, description: plain-text(meta_sections.find(x => x.at(0) == file).at(1)), cond: cond)([ + #context _xref-included.final().pairs().map(((key, value)) => context if value and cond() { + xref-include(key) + }).join() + #metadata(json("interaction_count.json").sum(default: (:))) + + #let chapter-index = meta_sections.position(x => x.at(0) == file) + 1 + #set heading(numbering: (..args) => [#chapter-index.#numbering("1.1", ..args)]) + #counter(heading).update(0) + + #body + ]) + } + } else { + body => body + } +} diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index c4fa91471..4ccf69b29 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -6,11 +6,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$ @@ -19,244 +22,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/chapters/verifier.typ b/spec/chapters/verifier.typ new file mode 100644 index 000000000..e85903478 --- /dev/null +++ b/spec/chapters/verifier.typ @@ -0,0 +1,4 @@ +// TODO: +// - sigma protocol, layout the various steps +// - Fiat Shamir transformation into non-interactive protocol. +// 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/meta.typ b/spec/meta.typ index 885947d4e..eea8f6e4a 100644 --- a/spec/meta.typ +++ b/spec/meta.typ @@ -10,6 +10,7 @@ ("logup", [`LogUp` argument], ), ("memory", [Memory argument], ), ("streaming", [Streaming prover], ), + ("verifier", [Verification], ), )), ("OVERVIEW", ( ("variables", [Variables], ), From 13f32ce3191bb4803132b7408052260993d7917e Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 21 Aug 2026 11:55:55 +0200 Subject: [PATCH 04/16] spec/recursion: clean up --- spec/chapters/recursion.typ | 450 +------------------------ spec/figures/DEEP-FRI_verification.md | 35 -- spec/figures/DEEP-FRI_verification.svg | 1 - 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/chapters/recursion.typ b/spec/chapters/recursion.typ index 4ccf69b29..fbb822753 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -54,8 +54,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, @@ -73,7 +75,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. @@ -221,443 +224,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$ 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 From bc875f048e691f9d194cba7911fb0d14acef1f06 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 21 Aug 2026 12:07:11 +0200 Subject: [PATCH 05/16] spec/recursion: more cleanup --- spec/chapters/recursion.typ | 69 ++++++++++++++++--------------------- 1 file changed, 30 insertions(+), 39 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index fbb822753..fbfb93ce6 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -1,33 +1,24 @@ #import "/meta.typ": et, aside - -// 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$ @@ -47,12 +38,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 \ @@ -74,7 +65,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: $ @@ -106,15 +97,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 @@ -201,20 +192,20 @@ Below, we provide a division that, in theory, is expected to achieve solid perfo *Record $record$.* The record contains all challenges the prover derived using Fiat-Shamir. -*Tasks for $verify'_b\(c_0, c_1, b, proof, record)$:* +*Tasks for $verify'_b\(commitment_0, commitment_1, b, proof, record)$:* + assert that $b in {0, 1}$, + verify challenges on record $record$ according to Fiat-Shamir, + verify the various opening proofs; - if $b=0$: - verify binary-VM DECODE table (@decode) query opening against $c_0$ + verify binary-VM DECODE table (@decode) query opening against $commitment_0$ - if $b=1$: - verify binary-VM DECODE table (@decode) query opening against $c_(1,b)$ and - verify field-VM DECODE table (@field-decode) query opening against $c_(1,f)$ -+ `COMMIT` to $c_0$ and $c_1$ (see @commit) + verify binary-VM DECODE table (@decode) query opening against $commitment_(1,b)$ and + verify field-VM DECODE table (@field-decode) query opening against $commitment_(1,f)$ ++ `COMMIT` to $commitment_0$ and $commitment_1$ (see @commit) -*Tasks $verify'_f\(c_0, c_1, b, proof, record)$:* +*Tasks $verify'_f\(commitment_0, commitment_1, b, proof, record)$:* + verify LogUp openings sum to zero, - - if $b=1$, use $c_0$ and $c_1$ to complete the `COMMIT` balance. + - if $b=1$, use $commitment_0$ and $commitment_1$ to complete the `COMMIT` balance. + verify `DEEP` evaluation + verify `FRI` folding + verify `FRI` output low degreeness check. From 0fae69977d83c1bdd5a8162afde9f1ec5f503cf4 Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Wed, 26 Aug 2026 10:14:11 +0200 Subject: [PATCH 06/16] Apply suggestions from code review Co-authored-by: Robin Jadoul --- spec/chapters/recursion.typ | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index fbfb93ce6..232d01db1 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -41,7 +41,7 @@ $instance\(witness) = one$. Lastly, we introduce the commitment function $c: instanceSpace mapsto commitmentSpace$. To simplify notation, we use $commit(instance) = c(instance)$. -We now assume the existence of _proving system_ $(prove, verify)$ with +We now assume the existence of _proof system_ $(prove, verify)$ with prover $prove: instanceSpace times witnessSpace mapsto proofSpace$ and verifier $verify: commitmentSpace times proofSpace mapsto BB$ such that $ @@ -76,8 +76,8 @@ This new proof $proof'$ thus attests to _the existence of a proof $proof$ that satisfies the verifier on the given instance $instance$_. This concept, colloquially known as _proof recursion_, can be applied repeatedly. -The technique is specifically beneficial for _succint_ proving systems where proof size -typically shrinks (and verification time therefore reduces) as the level of recursion increases. +The technique is specifically beneficial for _succinct_ proving systems where proof size +typically shrinks (and verification time reduces) as the level of recursion increases. The technique is mostly useful in settings where the extra time spent by the prover is outweighed by the time saved by the verifier(s), e.g., a computationally constrained verifier, or multiple verifiers. @@ -155,7 +155,7 @@ results of binary arithmetic are used to verify field arithmetical constraints and vice-versa --- e.g., hashing merkle leafs containing field elements during FRI-query proof verification. This implies that some form of communication between both VMs is required. -This architecture enables the required communications by introducing a +Our architecture enables the required communications by introducing a prover-hinted _communication record_ $record$ accessible to both VMs. In practice, this record will primarily contain values being reinterpreted --- from $FF$ to $ZZ_(2^64)$ and vice-versa --- during verification. From 741811e7cb1e8d5843aee6a180614758876b0af3 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 26 Aug 2026 10:34:05 +0200 Subject: [PATCH 07/16] spec/recursion: address code review comments --- spec/chapters/recursion.typ | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 232d01db1..ac52176ee 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -1,13 +1,13 @@ #import "/meta.typ": et, aside // Spaces and instances -#let (functionSpace, function) = ($cal(F)$, $bb(f)$) +#let (functionSpace, function) = ($cal(F)$, $f$) #let (inputSpace, input) = ($II$, $bb(i)$) #let (instanceSpace, instance) = ($XX$, $bb(x)$) #let (witnessSpace, witness) = ($WW$, $bb(w)$) #let (proofSpace, proof) = ($bb(Pi)$, $bb(pi)$) -#let (commitmentSpace, commitment) = ($CC$, $bb(c)$) +#let (commitmentSpace, commitment) = ($cal(C)$, $bb(c)$) #let commit(x) = $overline(#x)$ #let comm(x) = $commit(#x)$ @@ -27,7 +27,7 @@ = Notation Let $BB := { zero, one }$ denote the boolean set and let -$functionSpace := {f: inputSpace times witnessSpace mapsto BB}$ denote +$functionSpace := {function: inputSpace times witnessSpace mapsto BB}$ denote the set of functions mapping the (public) input space $inputSpace$ and (private) witness space $witnessSpace$ to this set. We use $instanceSpace := functionSpace times inputSpace = {instance: witnessSpace mapsto BB}$ @@ -38,8 +38,12 @@ as the set of all _solvable instances_, i.e., all instances $instance in instanceSpace$ for which there exists a witness $witness in witnessSpace$ such that $instance\(witness) = one$. -Lastly, we introduce the commitment function $c: instanceSpace mapsto commitmentSpace$. -To simplify notation, we use $commit(instance) = c(instance)$. +Lastly, we introduce the instance commitment function $c: instanceSpace mapsto commitmentSpace$. +Note that this commitment scheme does not involve randomness; it is a determistic scheme. +Randomness is typically required to make a commitment _hiding_. +For the purposes of this discussion, we are not concerned with this property, +as the function will only be used for committing to public information. +To simplify notation, we henceforth use $commit(instance)$ to represent the commitment $c(instance)$ of $instance$. We now assume the existence of _proof system_ $(prove, verify)$ with prover $prove: instanceSpace times witnessSpace mapsto proofSpace$ and From 757131a69457f71182ae913ce5fcc6c04ec98da3 Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Fri, 28 Aug 2026 11:49:04 +0200 Subject: [PATCH 08/16] Apply suggestions from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/chapters/recursion.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index ac52176ee..25e479c93 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -5,7 +5,7 @@ #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 (proofSpace, proof) = ($bb(Pi)$, $pi$) #let (commitmentSpace, commitment) = ($cal(C)$, $bb(c)$) #let commit(x) = $overline(#x)$ From 54ce9246b26a393657839288ce666728069211ab Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 28 Aug 2026 11:48:53 +0200 Subject: [PATCH 09/16] spec/recursion: address review comments --- spec/chapters/recursion.typ | 159 +++++++++++++++++++++--------------- 1 file changed, 93 insertions(+), 66 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 25e479c93..b4b51ebc3 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -11,14 +11,13 @@ #let commit(x) = $overline(#x)$ #let comm(x) = $commit(#x)$ -#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 (zero, one) = ($0$, $1$) #let iff = $arrow.double.l.r$ #let implies = $arrow.double.r$ #let prob = $PP$ @@ -30,14 +29,15 @@ Let $BB := { zero, one }$ denote the boolean set and let $functionSpace := {function: inputSpace times witnessSpace mapsto BB}$ denote the set of functions mapping the (public) input space $inputSpace$ and (private) witness space $witnessSpace$ to this set. -We use $instanceSpace := functionSpace times inputSpace = {instance: witnessSpace mapsto BB}$ -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_. +Function-input pairs $(function, input) in functionSpace times inputSpace$ +are henceforth referred to as _function instances_, or simply _instances_. +Where convenient, we may also denote this as $function(input; dot) in instanceSpace$ +with instance space $instanceSpace$. We then define $relation subset.eq instanceSpace$ as the set of all _solvable instances_, -i.e., all instances $instance in instanceSpace$ +i.e., instances $function(input; dot) in instanceSpace$ for which there exists a witness $witness in witnessSpace$ such that -$instance\(witness) = one$. +$function\(input; witness) = one$. Lastly, we introduce the instance commitment function $c: instanceSpace mapsto commitmentSpace$. Note that this commitment scheme does not involve randomness; it is a determistic scheme. Randomness is typically required to make a commitment _hiding_. @@ -47,24 +47,17 @@ To simplify notation, we henceforth use $commit(instance)$ to represent the comm We now assume the existence of _proof system_ $(prove, verify)$ with prover $prove: instanceSpace times witnessSpace mapsto proofSpace$ and -verifier $verify: commitmentSpace times proofSpace mapsto BB$ such that -$ -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, -while the probability of any proof verifying an unsolvable instance is negligible. +verifier $verify: commitmentSpace times proofSpace mapsto BB$ that is both +_complete_ --- i.e., $verify$ accepts all valid proofs generated by $prove$ --- +and _sound_ --- i.e., one cannot create an acceptable proof for an unsolvable instance. Translating this to the purposes of this VM, a prover wishes to convince the verifier -that for some agreed upon program ($program in functionSpace$) and specified public input ($input in inputSpace$), +that for some agreed upon program ($function 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)$ +(i.e., $(function, input) in relation$). +To this end, the prover uses $prove\(function(input; dot); 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, +They then use $verify(comm(function(input; dot)), proof)$ to check that the proof is valid, convincing them of the prover's claim. = Proof recursion @@ -91,8 +84,8 @@ While recursive proving leads to a decrease in proof size, this is naively trade against an increase in instance complexity. Looking at a depth-two recursive proof, $ - &prove\(verify(comm(verify(comm(instance), dot)), dot); proof') = proof'', text("and")\ - &verify(comm(verify(comm(verify(comm(instance), dot)), dot)), proof'') = one. + &prove\(verify(comm(verify(comm(instance), dot)), dot); proof') = proof'', text("and") + verify(comm(verify(comm(verify(comm(instance), dot)), dot)), proof'') = one $ we see that the verifier first the verifier first has to derive the commitment $comm(verify(comm(verify(comm(instance), dot)), dot))$ @@ -104,27 +97,35 @@ $ verify': commitmentSpace^2 times {0, 1} times proofSpace: (commitment_0, commitment_1, b, proof) mapsto cases( verify(commitment_0, proof) &text("if") b=0, - verify(commitment_1(commitment_0, commitment_1, dot), proof) &text("if") b=1 + 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 $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 +where it is assumed that $comm(function((x_1, x_2); dot))$ can be easily +constructed from $(comm(function), comm(x_1), comm(x_2))$. +Now observe that +$ + verify'(comm(instance), comm(verify'), 0, proof) &= verify(comm(instance), proof), text("and")\ + verify'(comm(instance), comm(verify'), 1, proof) &= verify(comm(verify')((comm(instance), comm(verify')); dot), proof)\ + &= verify(comm(verify'((instance, verify'); dot)), proof). +$ +In other words, by setting $commitment_0 = commit(instance)$ and $commitment_1 = commit(verify')$, +this algorithm can verify a base proof by setting $b=0$ or a recursive proof when selecting $b=1$. +Importantly, the verification of some proof $proof$ using $verify'(comm(instance), comm(verify'), 1, dot)$ +succeeds only if the prover has used $verify'$ at every step in the proof recursion. +This fact is illustrated by the following expansion: $ verify'(commit(instance), commit(verify'), 1, proof^((n))) &= verify(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. +Hence, a recursive proof based on $verify'$ attests that $verify'$ was the +only algorithm used throughout the entire recursion stack. + +Lastly, note that the verification of a recursive proof $proof^((n))$ only +depends on $comm(instance)$, since $comm(verify')$ can be precomputed. +We have thus established a recursive proving system that only requires the base +instance as input to the verification of a recursive proof. #aside([$comm(verify')$ absorption])[ Note that $commit(verify')$ must be provided to $verify'$ as a _parameter_; @@ -190,37 +191,63 @@ effectively synchronizing their interpretation. ] 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\(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 $commitment_0$ - - if $b=1$: - 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\(commitment_0, commitment_1, b, proof, record)$:* -+ verify LogUp openings sum to zero, - - 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. - -*Prover.* -The prover performs the following steps: +Moreover, it is unclear what division will lead to optimal performance. +Yet, it is expected that divisions adhering to these high-level guidelines will +be a good first step towards a performant verifier: ++ have the field-VM perform all verification steps involving field arithmetic, ++ include all verifier-issued challenges required by these verification steps + in the communication record $record$ as field-elements, so that the field-VM does not have to derive them, ++ use the binary-VM to verify the challenges hinted by the communication record are indeed correct. + += Recursive proving and split processing +We lastly provide some notes on applying the recursive proving and split processing to +the verification of a proof in the context of this VM. + +First, we note that in any scenario, the prover has to commit to the program $function$ +being exeucted and the public input $input$ that is provided. +In a non-recursive proof, this is trivially done by committing to the `DECODE` table +representing $function$, and the `PAGE` tables storing the public $input$. +Since these commitments are deterministic, the verifier can locally reconstruct +the commitments and verify any opening proofs against its own version of the commitment. + +When recursing on this process, the prover provides the verifier with this commitment. +We thus have to demonstrate the commitments the prover provides are as expected. +This is achieved by having the verification algorithm `COMMIT` (see @commit) +to the public input it is provided. +This act produces an imbalance in the LogUp-component of the proof-of-verification, +which must be balanced during verification in the _next_ recursion layer. +In later recursions, the verifier must consistently `COMMIT` to its public input +and use the _same_ public input to balance out the LogUp-component of the proof +it is provided. +This solution effectively kicks the can down the road; the final verifier has to +provide the initial input to the program as input to verify the recursive proof. + +Denoted as pseudo-algorithms, we find: + +#set list(marker: [---]) +*Communication record overview:* +- the data required according to the chosen verification split, +- if $b=1$, reconstructed commitment $comm(verify'(comm(instance), comm(verify'); dot))$ + +*$verify'_b\(comm(instance), (comm(verify'_b), comm(verify'_f)), b, proof, record)$:* +- `COMMIT` to $comm(instance)$, $comm(verify'_b),$ and $comm(verify'_f)$ +- assert that $b in {0, 1}$, +- verify proof: + - if $b=0$: execute $verify_b (comm(instance), proof)$ + - if $b=1$: + + construct $comm(verify'(comm(instance), comm(verify'); dot))$ from $(comm(instance), (comm(verify'_b), comm(verify'_f)))$ + + execute $verify_b (comm(verify'(comm(instance), comm(verify'); dot)), proof)$ + +*$verify'_f\(comm(instance), (comm(verify'_b), comm(verify'_f)), b, proof, record)$:* +- verify proof: $verify_b (comm(verify'(comm(instance), comm(verify'); dot)), proof)$ + - if $b=1$, use $comm(instance), comm(verify'_b), comm(verify'_f)$ to complete the `COMMIT` LogUp-balance. + +*Prover:* $ - proof &arrow.l prove(instance, witness)\ - proof' &arrow.l prove(verify'_b || verify'_f, (commit(instance), [commit(verify'_b), commit(verify'_f)], 0, proof, record))\ - proof^((i)) &arrow.l prove(verify'_b || verify'_f, (commit(instance), [commit(verify'_b), commit(verify'_f)], 1, proof^((i-1)), record)) + proof &arrow.l prove(instance, witness)\ + proof' &arrow.l prove(verify'_b || verify'_f, (commit(instance), (commit(verify'_b), commit(verify'_f)), 0, proof, record))\ + proof^((i)) &arrow.l prove(verify'_b || verify'_f, (commit(instance), (commit(verify'_b), commit(verify'_f)), 1, proof^((i-1)), record)) $ *Final verification.* -$verify'(commit(instance), [commit(verify'_b), commit(verify'_f)], 1, proof^((n))) =? one$ +$verify'(commit(instance), (commit(verify'_b), commit(verify'_f)), 1, proof^((n))) =? one$ From a75546f3a8390babad7f0683fac6809f9167b4a3 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 2 Sep 2026 17:13:13 +0200 Subject: [PATCH 10/16] address comments Cyprien --- spec/chapters/recursion.typ | 83 ++++++++++++++++++++----------------- 1 file changed, 44 insertions(+), 39 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index b4b51ebc3..6b86cacaf 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -1,7 +1,7 @@ #import "/meta.typ": et, aside // Spaces and instances -#let (functionSpace, function) = ($cal(F)$, $f$) +#let (programSpace, program) = ($cal(F)$, $f$) #let (inputSpace, input) = ($II$, $bb(i)$) #let (instanceSpace, instance) = ($XX$, $bb(x)$) #let (witnessSpace, witness) = ($WW$, $bb(w)$) @@ -12,6 +12,7 @@ #let comm(x) = $commit(#x)$ #let relation = $cal(R)$ +#let language = $cal(L)$ #let verifierSpace = $cal(V)$ #let (prove, verify) = ($italic("p")$, $italic("v")$) @@ -21,52 +22,54 @@ #let iff = $arrow.double.l.r$ #let implies = $arrow.double.r$ #let prob = $PP$ +#let to = math.arrow.r #show math.equation.where(block: false): box = Notation Let $BB := { zero, one }$ denote the boolean set and let -$functionSpace := {function: inputSpace times witnessSpace mapsto BB}$ denote +$programSpace := {program: inputSpace times witnessSpace to BB}$ denote the set of functions mapping the (public) input space $inputSpace$ and (private) witness space $witnessSpace$ to this set. -Function-input pairs $(function, input) in functionSpace times inputSpace$ +We define instance space $instanceSpace := programSpace times inputSpace = {program: witnessSpace to BB}$; +program-input pairs $(program, input) in instanceSpace$ are henceforth referred to as _function instances_, or simply _instances_. -Where convenient, we may also denote this as $function(input; dot) in instanceSpace$ -with instance space $instanceSpace$. -We then define $relation subset.eq instanceSpace$ -as the set of all _solvable instances_, -i.e., instances $function(input; dot) in instanceSpace$ -for which there exists a witness $witness in witnessSpace$ such that -$function\(input; witness) = one$. -Lastly, we introduce the instance commitment function $c: instanceSpace mapsto commitmentSpace$. -Note that this commitment scheme does not involve randomness; it is a determistic scheme. +Where the individual components of the pair are irrelevant, an instance is +denoted as $instance in instanceSpace$. + +We define relation $relation subset instanceSpace times witnessSpace$ where $((program, input), witness) in relation$ if $program(input, witness) = 1$. +This relation induces the language $language subset instanceSpace$ of _solvable instances_, +where $instance in language$ if there exists a witness $witness$ for which $(instance, witness)in relation$. + +Lastly, we introduce the instance commitment function $c: instanceSpace to commitmentSpace$. +Note that this commitment scheme does not involve randomness; it is a _determistic_ scheme. Randomness is typically required to make a commitment _hiding_. For the purposes of this discussion, we are not concerned with this property, as the function will only be used for committing to public information. To simplify notation, we henceforth use $commit(instance)$ to represent the commitment $c(instance)$ of $instance$. We now assume the existence of _proof system_ $(prove, verify)$ with -prover $prove: instanceSpace times witnessSpace mapsto proofSpace$ and -verifier $verify: commitmentSpace times proofSpace mapsto BB$ that is both +prover $prove: instanceSpace times witnessSpace to proofSpace$ and +verifier $verify: commitmentSpace times proofSpace to BB$ that is both _complete_ --- i.e., $verify$ accepts all valid proofs generated by $prove$ --- and _sound_ --- i.e., one cannot create an acceptable proof for an unsolvable instance. Translating this to the purposes of this VM, a prover wishes to convince the verifier -that for some agreed upon program ($function in functionSpace$) and specified public input ($input in inputSpace$), +that for some agreed upon program ($program in programSpace$) and specified public input ($input in inputSpace$), they know a private input ($witness in witnessSpace$) such that the program terminates successfully -(i.e., $(function, input) in relation$). -To this end, the prover uses $prove\(function(input; dot); witness)$ +(i.e., $(program, input) in language$). +To this end, the prover uses $prove(program(input; dot); witness)$ to construct some proof $proof in proofSpace$ and sends this to the verifier. -They then use $verify(comm(function(input; dot)), proof)$ to check that the proof is valid, +They then use $verify(comm(program(input; dot)), proof)$ to check that the proof is valid, convincing them of the prover's claim. = Proof recursion Now observe that the verifier $verify$ is itself a function in -$verifierSpace := {hat(f): commitmentSpace times proofSpace mapsto BB} subset.eq functionSpace$. +$verifierSpace := {hat(f): commitmentSpace times proofSpace to BB} subset.eq programSpace$. This means that we can use $prove$ to prove that the verification of a proof $proof$ for a given instance $instance$ succeeds: $ - &prove\(verify(comm(instance), dot); proof) = proof', text("and") + &prove(verify(comm(instance), dot); proof) = proof', text("and") &verify(comm(verify(comm(instance), dot)), proof') = one. $ This new proof $proof'$ thus attests to _the existence of a proof $proof$ that @@ -84,40 +87,40 @@ While recursive proving leads to a decrease in proof size, this is naively trade against an increase in instance complexity. Looking at a depth-two recursive proof, $ - &prove\(verify(comm(verify(comm(instance), dot)), dot); proof') = proof'', text("and") + prove(verify(comm(verify(comm(instance), dot)), dot); proof') = proof'', text("and") verify(comm(verify(comm(verify(comm(instance), dot)), dot)), proof'') = one $ -we see that the verifier first the verifier first has to derive the commitment +we see that the verifier first has to derive the commitment $comm(verify(comm(verify(comm(instance), dot)), dot))$ from the given base instance $instance$ before verifying the proof. This increase in verifier computation is undesirable and should be avoided. A solution to this, is to leverage the following variation to the verification algorithm: $ - verify': commitmentSpace^2 times {0, 1} times proofSpace: (commitment_0, commitment_1, b, proof) mapsto + verify': commitmentSpace^2 times {0, 1} times proofSpace: (overline(r), overline(s), b, proof) mapsto cases( - verify(commitment_0, proof) &text("if") b=0, - verify(commitment_1((commitment_0, commitment_1); dot), proof) &text("if") b=1 + verify(overline(r), proof) &text("if") b=0, + verify(overline(s(overline(r), overline(s); dot)), proof) &text("if") b=1, ) $ -where it is assumed that $comm(function((x_1, x_2); dot))$ can be easily -constructed from $(comm(function), comm(x_1), comm(x_2))$. +where it is assumed that $overline(s(overline(r), overline(s); dot)) in commitmentSpace$ can efficiently be constructed from $(overline(r), overline(s)) in commitmentSpace^2$. Now observe that $ verify'(comm(instance), comm(verify'), 0, proof) &= verify(comm(instance), proof), text("and")\ - verify'(comm(instance), comm(verify'), 1, proof) &= verify(comm(verify')((comm(instance), comm(verify')); dot), proof)\ - &= verify(comm(verify'((instance, verify'); dot)), proof). + verify'(comm(instance), comm(verify'), 1, proof) &= verify(comm(verify'((comm(instance), comm(verify')); dot)), proof). $ -In other words, by setting $commitment_0 = commit(instance)$ and $commitment_1 = commit(verify')$, -this algorithm can verify a base proof by setting $b=0$ or a recursive proof when selecting $b=1$. + +In other words, by setting $(commitment_0, commitment_1) = (commit(instance), commit(verify'))$, +this algorithm can verify a base proof by choosing $b=0$ or a recursive proof when selecting $b=1$. Importantly, the verification of some proof $proof$ using $verify'(comm(instance), comm(verify'), 1, dot)$ succeeds only if the prover has used $verify'$ at every step in the proof recursion. This fact is illustrated by the following expansion: $ verify'(commit(instance), commit(verify'), 1, proof^((n))) - &= verify(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))). + &= verify(comm(verify'(commit(instance), commit(verify'), dot)), proof^((n)))\ + &= verify(comm(verify(comm(verify'(comm(instance), comm(verify'), dot)), dot)), proof^((n)))\ + &= verify(comm(verify(comm(verify(comm(verify'(comm(instance), comm(verify'), dot)), dot)), dot)), proof^((n)))\ + &= verify(comm(verify(comm(verify(comm(dots.c (comm(verify(comm(instance), dot) dots.c))), dot)), dot)), proof^((n)))\ $ Hence, a recursive proof based on $verify'$ attests that $verify'$ was the only algorithm used throughout the entire recursion stack. @@ -143,7 +146,7 @@ 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 +Emulating field arithmetic on a binary arithmetic-oriented VM, typically incurs significant computational overhead. With the aim of avoiding this performance penalty, we introduce a field arithmetic-oriented mini-VM (henceforth referred to as the _field-VM_), @@ -203,16 +206,18 @@ be a good first step towards a performant verifier: We lastly provide some notes on applying the recursive proving and split processing to the verification of a proof in the context of this VM. -First, we note that in any scenario, the prover has to commit to the program $function$ +First, we note that in any scenario, the prover has to commit to the program $program$ being exeucted and the public input $input$ that is provided. In a non-recursive proof, this is trivially done by committing to the `DECODE` table -representing $function$, and the `PAGE` tables storing the public $input$. +representing $program$, and the `PAGE` tables storing the public $input$. Since these commitments are deterministic, the verifier can locally reconstruct the commitments and verify any opening proofs against its own version of the commitment. +Note that in this case, the prover may exclude the opened value from any proof strings +pertaining to the `DECODE` and `PAGE` tables, as these are already known to the verifier. When recursing on this process, the prover provides the verifier with this commitment. We thus have to demonstrate the commitments the prover provides are as expected. -This is achieved by having the verification algorithm `COMMIT` (see @commit) +This is achieved by having the verificationan algorithm `COMMIT` (see @commit) to the public input it is provided. This act produces an imbalance in the LogUp-component of the proof-of-verification, which must be balanced during verification in the _next_ recursion layer. @@ -250,4 +255,4 @@ $ $ *Final verification.* -$verify'(commit(instance), (commit(verify'_b), commit(verify'_f)), 1, proof^((n))) =? one$ +$verify'(commit(instance), (commit(verify'_b), commit(verify'_f)), 1, proof^((n))) =^? one$ From cc47599c488d178b83353853d9713871c4d8bd8c Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 15 Sep 2026 14:07:47 +0200 Subject: [PATCH 11/16] complete combination --- spec/chapters/recursion.typ | 508 ++++++++++++++++++++++++++++++------ 1 file changed, 427 insertions(+), 81 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 6b86cacaf..2319a57e0 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -3,7 +3,7 @@ // Spaces and instances #let (programSpace, program) = ($cal(F)$, $f$) #let (inputSpace, input) = ($II$, $bb(i)$) -#let (instanceSpace, instance) = ($XX$, $bb(x)$) +#let (instanceSpace, instance, instance2) = ($XX$, $bb(x)$, $bb(y)$) #let (witnessSpace, witness) = ($WW$, $bb(w)$) #let (proofSpace, proof) = ($bb(Pi)$, $pi$) @@ -11,6 +11,8 @@ #let commit(x) = $overline(#x)$ #let comm(x) = $commit(#x)$ +#let hash = $H$ + #let relation = $cal(R)$ #let language = $cal(L)$ @@ -26,7 +28,9 @@ #show math.equation.where(block: false): box -= Notation +#set list(marker: [---]) + += Proof recursion Let $BB := { zero, one }$ denote the boolean set and let $programSpace := {program: inputSpace times witnessSpace to BB}$ denote the set of functions mapping the (public) input space $inputSpace$ and (private) @@ -63,7 +67,7 @@ to construct some proof $proof in proofSpace$ and sends this to the verifier. They then use $verify(comm(program(input; dot)), proof)$ to check that the proof is valid, convincing them of the prover's claim. -= Proof recursion +== Recursively proving proof verification Now observe that the verifier $verify$ is itself a function in $verifierSpace := {hat(f): commitmentSpace times proofSpace to BB} subset.eq programSpace$. This means that we can use $prove$ to prove that the verification of a proof $proof$ @@ -82,7 +86,7 @@ The technique is mostly useful in settings where the extra time spent by the pro is outweighed by the time saved by the verifier(s), e.g., a computationally constrained verifier, or multiple verifiers. -= Resolving growing instance complexity +== 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, @@ -97,86 +101,77 @@ This increase in verifier computation is undesirable and should be avoided. A solution to this, is to leverage the following variation to the verification algorithm: $ - verify': commitmentSpace^2 times {0, 1} times proofSpace: (overline(r), overline(s), b, proof) mapsto - cases( - verify(overline(r), proof) &text("if") b=0, - verify(overline(s(overline(r), overline(s); dot)), proof) &text("if") b=1, - ) + verify': commitmentSpace^2 times proofSpace: ([comm(x), comm(y)], proof) mapsto + verify(comm(x), proof) or verify(comm(y([comm(x), comm(y)], dot)), proof) $ -where it is assumed that $overline(s(overline(r), overline(s); dot)) in commitmentSpace$ can efficiently be constructed from $(overline(r), overline(s)) in commitmentSpace^2$. -Now observe that +where it is assumed that $comm(y([comm(x), comm(y)], dot)) in commitmentSpace$ can be constructed efficiently from $comm(x), comm(y) in commitmentSpace$. +Now observe that setting $(comm(x), comm(y)) = (commit(instance), commit(verify'))$ yields $ - verify'(comm(instance), comm(verify'), 0, proof) &= verify(comm(instance), proof), text("and")\ - verify'(comm(instance), comm(verify'), 1, proof) &= verify(comm(verify'((comm(instance), comm(verify')); dot)), proof). + verify'([comm(instance), comm(verify')], proof) + = verify(comm(instance), proof) or verify(comm(verify'([comm(instance), comm(verify')], dot)), proof). $ - -In other words, by setting $(commitment_0, commitment_1) = (commit(instance), commit(verify'))$, -this algorithm can verify a base proof by choosing $b=0$ or a recursive proof when selecting $b=1$. -Importantly, the verification of some proof $proof$ using $verify'(comm(instance), comm(verify'), 1, dot)$ -succeeds only if the prover has used $verify'$ at every step in the proof recursion. -This fact is illustrated by the following expansion: +In words, $verify'([comm(instance), comm(verify')], dot)$ only accepts $proof$ if it is either +a) proof of $instance in language$, or +b) proof of the existence of a (different) proof that satisfies $verify'([comm(instance), comm(verify')], dot)$. +We can now recursively expand the expression, yielding $ - verify'(commit(instance), commit(verify'), 1, proof^((n))) - &= verify(comm(verify'(commit(instance), commit(verify'), dot)), proof^((n)))\ - &= verify(comm(verify(comm(verify'(comm(instance), comm(verify'), dot)), dot)), proof^((n)))\ - &= verify(comm(verify(comm(verify(comm(verify'(comm(instance), comm(verify'), dot)), dot)), dot)), proof^((n)))\ - &= verify(comm(verify(comm(verify(comm(dots.c (comm(verify(comm(instance), dot) dots.c))), dot)), dot)), proof^((n)))\ + verify'(commit(instance), commit(verify'), proof) + &= verify(comm(instance), proof) or verify(comm(verify'([comm(instance), comm(verify')], dot)), proof)\ + &= verify(comm(instance), proof) or verify(comm(verify(comm(instance), dot) or verify(comm(verify'([comm(instance), comm(verify')]; dot)), dot)), proof)\ + &= verify(comm(instance), proof) or verify(comm(verify(comm(instance), dot) or verify(comm(verify(comm(instance), dot) or verify(comm(verify'([comm(instance), comm(verify')], dot)), dot)), dot)), proof)\ + &= verify(comm(instance), proof) or verify(comm(verify(comm(instance), dot) or verify(comm(verify(comm(instance), dot) or verify(comm(verify(comm(instance), dot) or verify(comm(verify'([comm(instance), comm(verify')], dot)), dot)), dot)), dot)), proof),\ + &&text(italic("etc.")) $ -Hence, a recursive proof based on $verify'$ attests that $verify'$ was the -only algorithm used throughout the entire recursion stack. - -Lastly, note that the verification of a recursive proof $proof^((n))$ only -depends on $comm(instance)$, since $comm(verify')$ can be precomputed. -We have thus established a recursive proving system that only requires the base -instance as input to the verification of a recursive proof. +This shows us that a prover can use $verify'$ to shrink a proof $proof$ attesting +to $instance in language$ recursively any number of times, such that the ultimate +verification will still pass; verification is _complete_. +Secondly, note that the size of the verification input +$(comm(instance), comm(verify'))$ is _constant_ in the depth of the recursion. +In fact, the size of the verification instance is typically fully determined by +$comm(instance)$, since $comm(verify')$ can often be precomputed. + +It is important to note that we have not proven soundness of this construction. +Specifically, there may exist proofs that _attest to the existence of itself_ in a finite number of recursion steps. +Such a proof would be accepted by $verify'$ even if $instance in.not language$. +In practice, one might be able to prevent this problem by including a recursion-level counter in the proof. #aside([$comm(verify')$ absorption])[ -Note that $commit(verify')$ must be provided to $verify'$ as a _parameter_; -absorbing it into $verify'$ would imply an object containing a cryptographic commitment of itself, -which is theoretically impossible. + Note that $commit(verify')$ must be provided to $verify'$ as a _parameter_; + absorbing it into $verify'$ would imply an object containing a cryptographic + commitment of itself at a static location, which is practically impossible. ] -#et("illustrate that there comes a termination point, i.e., a proof cannot prove itself.") -#et("note shakiness of recursion") += Split verification +#let (record, recordSpace) = ($bb(r)$, $Re$) -= Split processing -#let record = $bb(r)$ +Proof recursion involves executing the verification algorithm _inside_ the VM. In practice, we find that the set of operations utilized for verification differs vastly from those typically performed by guest programs. Specifically, verification primarily involves hashing and (extension) field arithmetic, where especially the second is absent in typical guest programs. -Emulating field arithmetic on a binary arithmetic-oriented VM, typically +Emulating field arithmetic on a binary arithmetic-oriented VM typically incurs significant computational overhead. -With the aim of avoiding this performance penalty, we introduce a field -arithmetic-oriented mini-VM (henceforth referred to as the _field-VM_), -which will act as a _co-processor_ to the established _binary-VM_. -Since both VMs are proven using the same proof system, a unified proof can be -produced for the parallel execution of both VMs. - -The introduction of this split allows the verification algorithm to be split in two halves, -with each VM performing the computations it is fastest at. -The two halves cannot work independently, however. -In the process of verifying proofs of the current proof system (`DEEP-FRI` + `LogUp`), -results of binary arithmetic are used to verify field arithmetical constraints ---- e.g., field challenges extracted from binary hash outputs --- -and vice-versa --- e.g., hashing merkle leafs containing field elements during FRI-query proof verification. -This implies that some form of communication between both VMs is required. - -Our architecture enables the required communications by introducing a -prover-hinted _communication record_ $record$ accessible to both VMs. -In practice, this record will primarily contain values being reinterpreted ---- from $FF$ to $ZZ_(2^64)$ and vice-versa --- during verification. -The two halves of the split verification algorithm are adapted to leverage -the record: for each value on the record, one of the VMs _verifies_ the value to be correct, -while the other _assumes_ its correctness and resumes verification under this assumption. - -To ensure correct verification, both verification-algorithm halves must align -on the interpretation of each value on the proof-record pair. -To this end, the dimensions of the record must be determined at _verification algorithm design-time_ -and parametrized in terms of the proof only. -Then, both verification algorithm halves can be given the same logic to interpret the record, -effectively synchronizing their interpretation. +With the aim of avoiding a performance penalty on this front, we show how one +might split the verification process in two halves, +such that either half can be executed on a VM with an instruction set tailored to its needs. + +== Communication +As a result of executing the two verification-algorithm halves on distinct VMs, +no direct communication between both algorithms is possible. +Yet, practice shows that effective algorithm splits requires some form of communication +between both halves: typically one half performs a verification step to a certain +point, after which the other half continues verification starting from this +intermediate state. + +To achieve communication between two programs running on different VMs, +we introduce the concept of a prover-hinted _communication record_ $record$ +provided as _input_ to both processes. +All values that are to be communicated from one part to another, are stated on this record. +For each value on the record, the "sending" half _verifies_ that it is as expected, +whilst the "receiving" half _assumes_ its correctness and resumes verification under this assumption. +One can now conclude that the proof satisfies the instance +when both algorithm-halves produce the same record for this input. #aside("Coupling")[ As observed, both verification halves must be synchronized to correctly verify a proof. @@ -193,16 +188,357 @@ effectively synchronizing their interpretation. to accelerate hash-verification) while incurring as little design overhead as possible. ] -In theory, any division of tasks between the two VMs would work. -Moreover, it is unclear what division will lead to optimal performance. -Yet, it is expected that divisions adhering to these high-level guidelines will -be a good first step towards a performant verifier: -+ have the field-VM perform all verification steps involving field arithmetic, -+ include all verifier-issued challenges required by these verification steps - in the communication record $record$ as field-elements, so that the field-VM does not have to derive them, -+ use the binary-VM to verify the challenges hinted by the communication record are indeed correct. +More formally, we define +$v_0, v_1: instanceSpace times proofSpace to recordSpace$ as a valid _split_ of verifier $v in verifierSpace$ if +$ + forall (instance, proof) in instanceSpace times proofSpace: v(comm(instance), proof) = 1 iff v_0(comm(instance), proof) = v_1(comm(instance), proof), +$ +where $recordSpace$ denotes the communication record space. +That is, the two halves agree if and only if the instance-proof verifies succesfully. +By applying the Kronecker delta function $delta$ #footnote("https://en.wikipedia.org/wiki/Kronecker_delta"), +we can transform both halves into members of $programSpace$: +$ + tilde(v)_0(comm(instance), [proof, record]) := delta_(v_0(comm(instance), proof),record), #h(3em) + tilde(v)_1(comm(instance), [proof, record]) := delta_(v_1(comm(instance), proof),record). +$ +That is, $tilde(v)_0, tilde(v)_1$ indicate whether the provided record $record in recordSpace$ +would indeed be produced by $v_0$ respectively $v_1$ when provided $instance$ and $proof$. +With this transformation in place, one can express +$ + v(comm(instance), proof) + = tilde(v)_0(comm(instance), [proof, d(comm(instance), proof)]) + dot tilde(v)_1(comm(instance), [proof, d(comm(instance), proof)]). +$ +where $d(comm(instance), proof) := v_0(comm(instance), proof)$ denotes the +record deriviation function. +We introduce the function product $(f || g)(input, witness) := f(input, witness) dot g(input, witness)$ for $f, g in programSpace$. +This then allows us to express +$ + prove(verify(comm(instance), dot); proof) + &= prove((tilde(v)_0 || tilde(v)_1)(comm(instance), dot); [proof, record]) + &= proof', +$ +with $record := d(comm(instance), proof)$. + +Summarizing, we have now expressed recursive verification in terms of a +split verifier, where the same instance-proof-record triple was provided to +both verification halves. +The produced proof $proof'$ now attests to $instance in language$ when +$verify(comm((tilde(v)_0 || tilde(v)_1)(comm(instance), dot)), proof') = 1$. + + +// == Input synchronization +// By partitioning the verification algorithm and executing the parts on different VMs, +// we are now creating two _partial_ proofs. +// For two partials to collectively attest to a statement, they must have been constructed +// for _the same instance-proof-record triple_ $(comm(instance), proof, record)$. +// This means that an algorithm verifying a partitioned proof must check that this is the case, +// in addition to verifying the individual parts to be correct. +// In the context of recursive proving, this verification step must be built into the +// verification algorithm being used. + + + +// - stuff about how interpreting this as communication + +// to split $v'$, we first observe that +// $ +// v^*([instance, instance2], [proof, b]) +// :&= +// $ +// $ +// v'([comm(x), comm(y)], [proof, b]) +// &= Delta_BB (v(comm(x), proof), v(comm(y([comm(x), comm(y)], dot)), proof), b)\ +// &= v(Delta_BB (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof) +// $ +// hence, +// $ +// v'_0([comm(x), comm(y)], [[proof, b], r]) +// &= v_0(Delta_BB (comm(x), comm(y([comm(x), comm(y)], dot)), b), [proof, r])\ +// v'_1([comm(x), comm(y)], [[proof, b], r]) +// &= v_1(Delta_BB (comm(x), comm(y([comm(x), comm(y)], dot)), b), [proof, r])\ +// $ + + + +// - when verifying a proof-of-split-verification, must ensure the same instance-proof-record triple was provided to both VMs +// - typical solution: design the level-1 verification subalgorithms such that they commit to their inputs, and then have the level-2 verification check that both l1 subalgorithms committed to the same value. + +// - in our recursion stack, the level-1 and level-2 verification algorithms are the same. + +// - introduce selectors +// $ +// &Delta_cal(A): cal(A)^2 times BB to cal(A): (x, y, b) mapsto cases(x & text("if") b=0, y & text("if") b=1) +// $ +// - devise verifier that selects a proof hinting what it is. part of proof due to recursion. +// $ +// tilde(verify)(Delta_commitmentSpace (comm(x), comm(y), dot), [proof, b]) +// &:= verify(Delta_commitmentSpace (comm(x), comm(y), b), proof) and b in^? BB +// $ +// $ +// tilde(verify)([comm(x), comm(y)], [proof, b]) +// &:= verify(Delta_commitmentSpace (comm(x), comm(y), b), proof) +// $ +// $ +// tilde(verify)'([comm(x), comm(y)], [proof, b]) := tilde(verify)([comm(x), comm(y([comm(x), comm(y)], dot))], [proof, b]) +// $ +// // $ +// // tilde(verify)'([comm(x), comm(y)], [proof, 0]) +// // &= tilde(verify)([comm(x), comm(y([comm(x), comm(y)], dot))], [proof, 0])\ +// // &= verify(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), 0)], proof) +// // &= verify(comm(x), proof) +// // $ +// // and +// // $ +// // tilde(verify)'([comm(x), comm(y)], [proof, 1]) +// // &= tilde(verify)([comm(x), comm(y([comm(x), comm(y)], dot))], [proof, 1])\ +// // &= verify(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), 1)], proof) +// // &= verify(comm(y([comm(x), comm(y)], dot)), proof) +// // $ +// // hence, +// $ +// &tilde(verify)'([comm(instance), comm(instance2)], [proof, 0]) or tilde(verify)'([comm(instance), comm(instance2)], [proof, 1])\ +// &=tilde(verify)([comm(instance), comm(instance2([comm(instance), comm(instance2)], dot))], [proof, 0]) +// or tilde(verify)([comm(instance), comm(instance2([comm(instance), comm(instance2)], dot))], [proof, 1])\ +// &= verify(Delta_commitmentSpace (comm(instance), comm(instance2([comm(instance), comm(instance2)], dot)), 0), proof) +// or verify(Delta_commitmentSpace (comm(instance), comm(instance2([comm(instance), comm(instance2)], dot)), 1), proof)\ +// &= verify(comm(instance), proof) +// or verify(comm(instance2([comm(instance), comm(instance2)], dot)), proof)\ +// &= verify'([comm(instance), comm(instance2)], proof) +// $ +// in words: whether it is recursion or not is now "hinted" in the proof (and can thus be kept secret in recursive proving) + +// // - use them to modify v' by having the proof hint whether it is base or recursion +// // $ +// // verify^*([comm(x), comm(y)], [proof, b]) +// // :&= Delta_BB (verify(comm(x), proof), verify(comm(y([comm(x), comm(y)], dot)), proof), b)\ +// // &= verify(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof)\ +// // $ +// // - modify for recursive proving: $b$ must become part of the witness +// // $ +// // tilde(verify)(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), dot), [proof, b]) +// // &:= verify(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof) +// // $ +// - introduce concept of function splitting +// $ +// f(x) = 1 iff f_0(x) = f_1(x) +// $ +// - introduce transformation +// $ +// tilde(f)(x, y) = delta_(y = f(x)) +// $ +// - apply transformation to split function +// $ +// verify(x, proof) +// = tilde(v)_0(x, proof, v_1(x, proof)) dot tilde(v)_1(x, proof, v_0(x, proof)) +// $ +// - introduce function combiner +// $ +// dot || dot : programSpace times programSpace to programSpace : (f||g)(x,y) = f(x,y) dot g(x,y) +// $ +// - split $tilde(verify)'$ into $(tilde(verify)'_0, tilde(verify)'_1)$ s.t. +// $ +// tilde(verify)' equiv tilde(verify)'_0 || tilde(verify)'_1 +// $ +// $ +// tilde(verify)'_0([comm(x), comm(y)], [proof, b]) +// &= verify_0(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof)\ +// tilde(verify)'_1([comm(x), comm(y)], [proof, b]) +// &= verify_1(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof)\ +// $ + +// - combine into a single prover +// $ +// &prove(tilde(verify)'_0([comm(x), comm(y)], dot) +// || tilde(verify)'_1([comm(x), comm(y)], dot); [proof, b]) &&= [proof', b]\ +// $ +// that is: prove that both functions are executed on the same input $[proof, b]$. + + +// story: +// - different types of operations +// - typically cannot both be executed efficiently in the same environment +// - hence: split algorithm in parts, such that each part can be executed in a separate VM +// - q1: how to split? +// - design algorithms $v_0$ and $v_1(x, p, r)$ such that there only exists an +// $r$ satisfying $v_0(x, p, r ) = v_1(x, p, r) = 1$ if and only if +// $v(instance, proof) = 1$. Let $g(x, p): language times proofSpace to recordSpace$ +// denote this map for instances in the language. +// - hence, $v(x,p) = v_0(x,p,g(x, p)) dot v_1(x,p,g(x, p))$ +// - in other words, $v(x,p) = 1$ if there exists a record $r = v_0(x, p) = v_1(x, p)$. +// - A practical interpretation of $r$ is to view it as a "communication record" +// between the two halves: one half may verify part of an execution, and pass that +// information on to the other half, and vice versa. Only when both algorithms can +// agree on the same record, is the proof valid. + +// - q2: how to recursively verify a proof of split-verification? +// - assuming a perfect split, it suffices to verify that a) both partial verifiers are satisfied, and that b) both parts were given the same record. +// - this then allows us to make the record part of the witness. +// - verifier must ensure both parts were given the same instance-proof-record triple. + + +// - q3: how to split the prover? +// - new subsection + + +// = Split proving +// #et("describe what to do when proving the different VMs using different proof systems -> inner product argument") +// #let ip(x, y) = $chevron.l #x, #y chevron.r$ +// In the generic setting, input synchronization can be achieved by encapsulating the +// split verification with an _inner product argument_. + + + +// $ +// verify'(comm(instance), comm(instance2), proof) = verify(comm(instance), proof) or verify(comm(instance2(comm(instance), comm(instance2), dot)), proof) +// $ +// $ +// verify(comm(instance), comm(instance2), [proof, b]) +// &= Delta(verify(comm(instance), proof), verify(comm(instance2(comm(instance), comm(instance2), dot)), proof), b)\ +// &= verify'(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), [proof, b])\ +// // &= verify(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), b), proof)\ +// &= verify^*(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), b), proof) and b in^? BB\ +// $ + +// $ +// &verify'_0(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), [proof, b]) +// dot verify'_1(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), [proof, b])\ +// &prove(verify'_0(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), dot) +// || verify'_1(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), dot); [proof, b]) = [proof', b]\ +// &prove(verify'_0(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), dot) +// || verify'_1(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), dot); [proof', b]) = [proof'', b] +// $ + += Split proving +#et("todo") + += Split-recursion +With proof recursion and split verification formalized, we now combine both concepts into a unified system. +To this end, we first introduce the selector function +$ + &Delta_cal(A): cal(A)^2 times BB to cal(A): (x, y, b) mapsto cases(x & text("if") b=0, y & text("if") b=1), +$ +which, given a bit $b in BB$ and two elements $x,y$ of some space $cal(A)$, selects +an element based on the value of $b$. +We can now use this selector to define $verify^*$ --- a variation to $verify'$ --- as follows: +$ + verify^*([comm(x), comm(y)], [proof, b]) + :&= Delta_BB (verify(comm(x), proof), verify(comm(y([comm(x), comm(y)], dot)), proof), b)\ + &= verify(Delta_C (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof). +$ +Note here that one can reconstruct $verify'$ from $verify^*$ as +$ + sum_(b in BB) verify^*([comm(x), comm(y)], [proof, b]) + &=^((triangle)) or.big_(b in BB) verify^*([comm(x), comm(y)], [proof, b])\ + &= verify(Delta_C (comm(x), comm(y([comm(x), comm(y)], dot)), 0), proof) or verify(Delta_C (comm(x), comm(y([comm(x), comm(y)], dot)), 1), proof)\ + &= verify(comm(x), proof) or verify(comm(y([comm(x), comm(y)], dot)), proof)\ + &= verify'(comm(x), comm(y), proof),\ +$ +where $(triangle)$ holds under the assumption that a single proof $proof$ cannot +attest to two distinct instances. +This makes the `OR` operation ($or$) effectively equivalent to the `XOR` operation, +which is equivalent to addition in $BB$. +Hence, $verify^*$ and $verify'$ are effectively equivalent, except that $verify^*$ +has the proof include a bit $b$ indicating whether it is verifying a base proof or recursion proof. + +We now observe that +$ + tilde(verify)^*_0([comm(x), comm(y)], [[proof, b], r]) + &:= tilde(v)_0(Delta_C (comm(x), comm(y([comm(x), comm(y)], dot)), b), [proof, r]),\ + tilde(verify)^*_1([comm(x), comm(y)], [[proof, b], r]) + &:= tilde(v)_1(Delta_C (comm(x), comm(y([comm(x), comm(y)], dot)), b), [proof, r]) +$ +jointly form a valid split of $verify^*$, since +$ + verify^*([comm(x), comm(y)], [proof, b]) + &= verify(Delta_C (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof)\ + &= (tilde(verify)_0 || tilde(verify)_1)(Delta_C (comm(x), comm(y([comm(x), comm(y)], dot)), b), [proof, r])\ + &= (tilde(verify)^*_0 || tilde(verify)^*_1)([comm(x), comm(y)], [[proof, b], r]),\ +$ +when +$r = g([comm(x), comm(y([comm(x), comm(y)], dot))], [proof, b])$. +By selecting $(comm(x), comm(y)) = (comm(instance), comm(tilde(v)^*_0 || tilde(v)^*_1))$, +we now obtain +$ + (tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0 || tilde(verify)^*_1)], [[proof, b], r]) + // &= tilde(verify)^*_0([comm(instance), comm(tilde(verify)^*_0 || tilde(verify)^*_1)], [[proof, b], r]) dot tilde(verify)^*_1([comm(instance), comm(tilde(verify)^*_0 || tilde(verify)^*_1)], [[proof, b], r])\ + &= verify^*([comm(instance), comm(tilde(verify)^*_0 || tilde(verify)^*_1)], [proof, b])\ + &= verify(Delta_commitmentSpace (comm(instance), comm((tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance),comm(tilde(verify)^*_0 || tilde(verify)^*_1)], dot)), b), proof)\ + &= Delta_BB (verify(comm(instance), proof), verify(comm((tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance),comm(tilde(verify)^*_0 || tilde(verify)^*_1)], dot)), proof), b)\ + &= verify(comm(instance), proof) dot (1-b) + verify(comm((tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance),comm(tilde(verify)^*_0 || tilde(verify)^*_1)], dot)), proof) dot b. +$ +i.e., a split verification algorithm that checks whether $proof$ attests a) to $instance in language$ when $b=0$ or b) to the existence of a proof that does when $b=1$. +Importantly, this can be achieved recursively, as +$ + #h(8em) // alignment purposes + &prove(instance; witness) &&to proof_(0),\ + &prove((tilde(verify)^*_0||tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0||tilde(verify)^*_1)], dot); [[proof_(0), 0], r_(0)]) &&to [proof_(1), 1],\ + &prove((tilde(verify)^*_0||tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0||tilde(verify)^*_1)], dot); [[proof_(1), 1], r_(1)]) &&to [proof_(2), 1],\ + &prove((tilde(verify)^*_0||tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0||tilde(verify)^*_1)], dot); [[proof_(2), 1], r_(2)]) &&to [proof_(3), 1], + &&#h(8em)text(italic("etc.")) +$ +with +$ + r_i :&= g(comm((tilde(verify)^*_0||tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0||tilde(verify)^*_1)], dot)), [proof_i, 1-delta_(i,0)]). +$ + += Applied to lambda VM + -= Recursive proving and split processing +When both VMs are proven using the same proof system, the inner product argument is excessive. +Here, the same commitment to $comm((proof, record))$ can be interpreted by both VMs. +It therefore suffices for the verifier to verify both partial proofs against +the same public proof-record commitment. + +base level: +- input: instance, verifier +- witness: proof, record +- output: proof + +$ + verify': commitmentSpace^2 times proofSpace: (comm(x), comm(y), proof) mapsto + verify(comm(x), proof) or verify(comm(y(comm(x), comm(y); dot)), proof) +$ + +how to split $verify'$ into $verify'_0$ and $verify'_1$ + +$ + verify': commitmentSpace^2 times proofSpace: (comm(x), comm(y), proof) mapsto + verify(comm(x), proof) or verify(comm(y(comm(x), comm(y); dot)), proof) +$ + +$ + &verify'_0: (comm(x), comm(y), proof) mapsto + verify_0(comm(x), proof) or verify_0(comm(y(comm(x), comm(y); dot)), proof)\ + &verify'_1: (comm(x), comm(y), proof) mapsto + verify_1(comm(x), proof) or verify_1(comm(y(comm(x), comm(y); dot)), proof)\ +$ + +$ + &verify_0(comm(x), proof)\ + &verify_1(comm(x), proof) +$ + +recursion level: + +$ + &verify'_0\ + &verify'_1\ +$ + + +$ + verify +$ + +TODO: +We assume that these VMs are proven using the same proof system, +yielding a unified proof of the combined execution as a result. + + += Combining recursive proving and split processing + += Applied to LambdaVM We lastly provide some notes on applying the recursive proving and split processing to the verification of a proof in the context of this VM. @@ -217,7 +553,7 @@ pertaining to the `DECODE` and `PAGE` tables, as these are already known to the When recursing on this process, the prover provides the verifier with this commitment. We thus have to demonstrate the commitments the prover provides are as expected. -This is achieved by having the verificationan algorithm `COMMIT` (see @commit) +This is achieved by having the verification algorithm `COMMIT` (see @commit) to the public input it is provided. This act produces an imbalance in the LogUp-component of the proof-of-verification, which must be balanced during verification in the _next_ recursion layer. @@ -229,14 +565,24 @@ provide the initial input to the program as input to verify the recursive proof. Denoted as pseudo-algorithms, we find: -#set list(marker: [---]) += Applied to LambdaVM + + +In theory, any division of tasks between the two VMs would work. +Moreover, it is unclear what division will lead to optimal performance. +Yet, it is expected that divisions adhering to these high-level guidelines will +be a good first step towards a performant verifier: ++ have the field-VM perform all verification steps involving field arithmetic, ++ include all verifier-issued challenges required by these verification steps + in the communication record $record$ as field-elements, so that the field-VM does not have to derive them, ++ use the binary-VM to verify the challenges hinted by the communication record are indeed correct. + *Communication record overview:* - the data required according to the chosen verification split, - if $b=1$, reconstructed commitment $comm(verify'(comm(instance), comm(verify'); dot))$ -*$verify'_b\(comm(instance), (comm(verify'_b), comm(verify'_f)), b, proof, record)$:* +*$verify'_b\(comm(instance), (comm(verify'_b), comm(verify'_f)), proof, record)$:* - `COMMIT` to $comm(instance)$, $comm(verify'_b),$ and $comm(verify'_f)$ -- assert that $b in {0, 1}$, - verify proof: - if $b=0$: execute $verify_b (comm(instance), proof)$ - if $b=1$: From 8c27b72046738fb02f090bc56f760194b3e8d5a2 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 15 Sep 2026 14:08:10 +0200 Subject: [PATCH 12/16] trim excess --- spec/chapters/recursion.typ | 183 ------------------------------------ 1 file changed, 183 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 2319a57e0..0be697036 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -226,189 +226,6 @@ both verification halves. The produced proof $proof'$ now attests to $instance in language$ when $verify(comm((tilde(v)_0 || tilde(v)_1)(comm(instance), dot)), proof') = 1$. - -// == Input synchronization -// By partitioning the verification algorithm and executing the parts on different VMs, -// we are now creating two _partial_ proofs. -// For two partials to collectively attest to a statement, they must have been constructed -// for _the same instance-proof-record triple_ $(comm(instance), proof, record)$. -// This means that an algorithm verifying a partitioned proof must check that this is the case, -// in addition to verifying the individual parts to be correct. -// In the context of recursive proving, this verification step must be built into the -// verification algorithm being used. - - - -// - stuff about how interpreting this as communication - -// to split $v'$, we first observe that -// $ -// v^*([instance, instance2], [proof, b]) -// :&= -// $ -// $ -// v'([comm(x), comm(y)], [proof, b]) -// &= Delta_BB (v(comm(x), proof), v(comm(y([comm(x), comm(y)], dot)), proof), b)\ -// &= v(Delta_BB (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof) -// $ -// hence, -// $ -// v'_0([comm(x), comm(y)], [[proof, b], r]) -// &= v_0(Delta_BB (comm(x), comm(y([comm(x), comm(y)], dot)), b), [proof, r])\ -// v'_1([comm(x), comm(y)], [[proof, b], r]) -// &= v_1(Delta_BB (comm(x), comm(y([comm(x), comm(y)], dot)), b), [proof, r])\ -// $ - - - -// - when verifying a proof-of-split-verification, must ensure the same instance-proof-record triple was provided to both VMs -// - typical solution: design the level-1 verification subalgorithms such that they commit to their inputs, and then have the level-2 verification check that both l1 subalgorithms committed to the same value. - -// - in our recursion stack, the level-1 and level-2 verification algorithms are the same. - -// - introduce selectors -// $ -// &Delta_cal(A): cal(A)^2 times BB to cal(A): (x, y, b) mapsto cases(x & text("if") b=0, y & text("if") b=1) -// $ -// - devise verifier that selects a proof hinting what it is. part of proof due to recursion. -// $ -// tilde(verify)(Delta_commitmentSpace (comm(x), comm(y), dot), [proof, b]) -// &:= verify(Delta_commitmentSpace (comm(x), comm(y), b), proof) and b in^? BB -// $ -// $ -// tilde(verify)([comm(x), comm(y)], [proof, b]) -// &:= verify(Delta_commitmentSpace (comm(x), comm(y), b), proof) -// $ -// $ -// tilde(verify)'([comm(x), comm(y)], [proof, b]) := tilde(verify)([comm(x), comm(y([comm(x), comm(y)], dot))], [proof, b]) -// $ -// // $ -// // tilde(verify)'([comm(x), comm(y)], [proof, 0]) -// // &= tilde(verify)([comm(x), comm(y([comm(x), comm(y)], dot))], [proof, 0])\ -// // &= verify(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), 0)], proof) -// // &= verify(comm(x), proof) -// // $ -// // and -// // $ -// // tilde(verify)'([comm(x), comm(y)], [proof, 1]) -// // &= tilde(verify)([comm(x), comm(y([comm(x), comm(y)], dot))], [proof, 1])\ -// // &= verify(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), 1)], proof) -// // &= verify(comm(y([comm(x), comm(y)], dot)), proof) -// // $ -// // hence, -// $ -// &tilde(verify)'([comm(instance), comm(instance2)], [proof, 0]) or tilde(verify)'([comm(instance), comm(instance2)], [proof, 1])\ -// &=tilde(verify)([comm(instance), comm(instance2([comm(instance), comm(instance2)], dot))], [proof, 0]) -// or tilde(verify)([comm(instance), comm(instance2([comm(instance), comm(instance2)], dot))], [proof, 1])\ -// &= verify(Delta_commitmentSpace (comm(instance), comm(instance2([comm(instance), comm(instance2)], dot)), 0), proof) -// or verify(Delta_commitmentSpace (comm(instance), comm(instance2([comm(instance), comm(instance2)], dot)), 1), proof)\ -// &= verify(comm(instance), proof) -// or verify(comm(instance2([comm(instance), comm(instance2)], dot)), proof)\ -// &= verify'([comm(instance), comm(instance2)], proof) -// $ -// in words: whether it is recursion or not is now "hinted" in the proof (and can thus be kept secret in recursive proving) - -// // - use them to modify v' by having the proof hint whether it is base or recursion -// // $ -// // verify^*([comm(x), comm(y)], [proof, b]) -// // :&= Delta_BB (verify(comm(x), proof), verify(comm(y([comm(x), comm(y)], dot)), proof), b)\ -// // &= verify(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof)\ -// // $ -// // - modify for recursive proving: $b$ must become part of the witness -// // $ -// // tilde(verify)(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), dot), [proof, b]) -// // &:= verify(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof) -// // $ -// - introduce concept of function splitting -// $ -// f(x) = 1 iff f_0(x) = f_1(x) -// $ -// - introduce transformation -// $ -// tilde(f)(x, y) = delta_(y = f(x)) -// $ -// - apply transformation to split function -// $ -// verify(x, proof) -// = tilde(v)_0(x, proof, v_1(x, proof)) dot tilde(v)_1(x, proof, v_0(x, proof)) -// $ -// - introduce function combiner -// $ -// dot || dot : programSpace times programSpace to programSpace : (f||g)(x,y) = f(x,y) dot g(x,y) -// $ -// - split $tilde(verify)'$ into $(tilde(verify)'_0, tilde(verify)'_1)$ s.t. -// $ -// tilde(verify)' equiv tilde(verify)'_0 || tilde(verify)'_1 -// $ -// $ -// tilde(verify)'_0([comm(x), comm(y)], [proof, b]) -// &= verify_0(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof)\ -// tilde(verify)'_1([comm(x), comm(y)], [proof, b]) -// &= verify_1(Delta_commitmentSpace (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof)\ -// $ - -// - combine into a single prover -// $ -// &prove(tilde(verify)'_0([comm(x), comm(y)], dot) -// || tilde(verify)'_1([comm(x), comm(y)], dot); [proof, b]) &&= [proof', b]\ -// $ -// that is: prove that both functions are executed on the same input $[proof, b]$. - - -// story: -// - different types of operations -// - typically cannot both be executed efficiently in the same environment -// - hence: split algorithm in parts, such that each part can be executed in a separate VM -// - q1: how to split? -// - design algorithms $v_0$ and $v_1(x, p, r)$ such that there only exists an -// $r$ satisfying $v_0(x, p, r ) = v_1(x, p, r) = 1$ if and only if -// $v(instance, proof) = 1$. Let $g(x, p): language times proofSpace to recordSpace$ -// denote this map for instances in the language. -// - hence, $v(x,p) = v_0(x,p,g(x, p)) dot v_1(x,p,g(x, p))$ -// - in other words, $v(x,p) = 1$ if there exists a record $r = v_0(x, p) = v_1(x, p)$. -// - A practical interpretation of $r$ is to view it as a "communication record" -// between the two halves: one half may verify part of an execution, and pass that -// information on to the other half, and vice versa. Only when both algorithms can -// agree on the same record, is the proof valid. - -// - q2: how to recursively verify a proof of split-verification? -// - assuming a perfect split, it suffices to verify that a) both partial verifiers are satisfied, and that b) both parts were given the same record. -// - this then allows us to make the record part of the witness. -// - verifier must ensure both parts were given the same instance-proof-record triple. - - -// - q3: how to split the prover? -// - new subsection - - -// = Split proving -// #et("describe what to do when proving the different VMs using different proof systems -> inner product argument") -// #let ip(x, y) = $chevron.l #x, #y chevron.r$ -// In the generic setting, input synchronization can be achieved by encapsulating the -// split verification with an _inner product argument_. - - - -// $ -// verify'(comm(instance), comm(instance2), proof) = verify(comm(instance), proof) or verify(comm(instance2(comm(instance), comm(instance2), dot)), proof) -// $ -// $ -// verify(comm(instance), comm(instance2), [proof, b]) -// &= Delta(verify(comm(instance), proof), verify(comm(instance2(comm(instance), comm(instance2), dot)), proof), b)\ -// &= verify'(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), [proof, b])\ -// // &= verify(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), b), proof)\ -// &= verify^*(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), b), proof) and b in^? BB\ -// $ - -// $ -// &verify'_0(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), [proof, b]) -// dot verify'_1(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), [proof, b])\ -// &prove(verify'_0(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), dot) -// || verify'_1(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), dot); [proof, b]) = [proof', b]\ -// &prove(verify'_0(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), dot) -// || verify'_1(delta(comm(instance), comm(instance2(comm(instance), comm(instance2), dot)), dot), dot); [proof', b]) = [proof'', b] -// $ - = Split proving #et("todo") From 808b2ce57b039966e90546231ba8d5e131aacea4 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 18 Sep 2026 11:05:13 +0200 Subject: [PATCH 13/16] refactor --- spec/chapters/recursion.typ | 257 +++++++++++++++++------------------- 1 file changed, 120 insertions(+), 137 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 0be697036..3e1e37600 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -86,7 +86,7 @@ The technique is mostly useful in settings where the extra time spent by the pro is outweighed by the time saved by the verifier(s), e.g., a computationally constrained verifier, or multiple verifiers. -== Resolving growing instance complexity +== 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, @@ -110,9 +110,9 @@ $ verify'([comm(instance), comm(verify')], proof) = verify(comm(instance), proof) or verify(comm(verify'([comm(instance), comm(verify')], dot)), proof). $ -In words, $verify'([comm(instance), comm(verify')], dot)$ only accepts $proof$ if it is either +In words, $verify'([comm(instance), comm(verify')], dot)$ accepts only if $proof$ is either a) proof of $instance in language$, or -b) proof of the existence of a (different) proof that satisfies $verify'([comm(instance), comm(verify')], dot)$. +b) proof of _the existence of a (different) proof_ that satisfies $verify'([comm(instance), comm(verify')], dot)$. We can now recursively expand the expression, yielding $ verify'(commit(instance), commit(verify'), proof) @@ -131,9 +131,10 @@ In fact, the size of the verification instance is typically fully determined by $comm(instance)$, since $comm(verify')$ can often be precomputed. It is important to note that we have not proven soundness of this construction. -Specifically, there may exist proofs that _attest to the existence of itself_ in a finite number of recursion steps. +For example, there may exist proofs that _attest to the existence of itself_ in a finite number of recursion steps. Such a proof would be accepted by $verify'$ even if $instance in.not language$. In practice, one might be able to prevent this problem by including a recursion-level counter in the proof. +The existence of other soundness gaps are not ruled out by the authors. #aside([$comm(verify')$ absorption])[ Note that $commit(verify')$ must be provided to $verify'$ as a _parameter_; @@ -154,19 +155,32 @@ Emulating field arithmetic on a binary arithmetic-oriented VM typically incurs significant computational overhead. With the aim of avoiding a performance penalty on this front, we show how one might split the verification process in two halves, -such that either half can be executed on a VM with an instruction set tailored to its needs. +such that either half can be executed on a VM with an instruction set tailored to its needs, +while maintaining completeness and soundness of the verification. == Communication -As a result of executing the two verification-algorithm halves on distinct VMs, -no direct communication between both algorithms is possible. +When executing the two verification-algorithm halves on distinct VMs, +no direct communication between both algorithms is possible, +even if both VMs are proven using the same proof system. Yet, practice shows that effective algorithm splits requires some form of communication between both halves: typically one half performs a verification step to a certain point, after which the other half continues verification starting from this intermediate state. +Hence, support for communication is desirable. + +Briefly zooming out, we observe that for two algorithm halves to jointly +verify a proof, it is paramount that both subprograms are provided identical +input. +Moreover, we note that split verification is used in _recursion_ only: +the verifier verifies the ultimate proof _outside_ the VM, where the monolithic +verification algorithm can be executed efficiently. +Furthermore, all input provided during recursion is hinted by the prover, which +has access to the full execution trace before proving, including any information +that would ideally be sent between the two verification halves. To achieve communication between two programs running on different VMs, -we introduce the concept of a prover-hinted _communication record_ $record$ -provided as _input_ to both processes. +we thus introduce the concept of a prover-hinted _communication record_ $record$ +provided as input to both subprocesses. All values that are to be communicated from one part to another, are stated on this record. For each value on the record, the "sending" half _verifies_ that it is as expected, whilst the "receiving" half _assumes_ its correctness and resumes verification under this assumption. @@ -189,7 +203,8 @@ when both algorithm-halves produce the same record for this input. ] More formally, we define -$v_0, v_1: instanceSpace times proofSpace to recordSpace$ as a valid _split_ of verifier $v in verifierSpace$ if +$v_0, v_1: instanceSpace times proofSpace to recordSpace$ as a valid _split_ of +verifier $v in verifierSpace$ if $ forall (instance, proof) in instanceSpace times proofSpace: v(comm(instance), proof) = 1 iff v_0(comm(instance), proof) = v_1(comm(instance), proof), $ @@ -209,8 +224,7 @@ $ = tilde(v)_0(comm(instance), [proof, d(comm(instance), proof)]) dot tilde(v)_1(comm(instance), [proof, d(comm(instance), proof)]). $ -where $d(comm(instance), proof) := v_0(comm(instance), proof)$ denotes the -record deriviation function. +where $d(comm(instance), proof)$ denotes the record deriviation function. We introduce the function product $(f || g)(input, witness) := f(input, witness) dot g(input, witness)$ for $f, g in programSpace$. This then allows us to express $ @@ -273,7 +287,7 @@ $ &= (tilde(verify)^*_0 || tilde(verify)^*_1)([comm(x), comm(y)], [[proof, b], r]),\ $ when -$r = g([comm(x), comm(y([comm(x), comm(y)], dot))], [proof, b])$. +$r = d([comm(x), comm(y([comm(x), comm(y)], dot))], [proof, b])$. By selecting $(comm(x), comm(y)) = (comm(instance), comm(tilde(v)^*_0 || tilde(v)^*_1))$, we now obtain $ @@ -282,7 +296,7 @@ $ &= verify^*([comm(instance), comm(tilde(verify)^*_0 || tilde(verify)^*_1)], [proof, b])\ &= verify(Delta_commitmentSpace (comm(instance), comm((tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance),comm(tilde(verify)^*_0 || tilde(verify)^*_1)], dot)), b), proof)\ &= Delta_BB (verify(comm(instance), proof), verify(comm((tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance),comm(tilde(verify)^*_0 || tilde(verify)^*_1)], dot)), proof), b)\ - &= verify(comm(instance), proof) dot (1-b) + verify(comm((tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance),comm(tilde(verify)^*_0 || tilde(verify)^*_1)], dot)), proof) dot b. + &= verify(comm(instance), proof) dot (1-b) + verify(comm((tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance),comm(tilde(verify)^*_0 || tilde(verify)^*_1)], dot)), proof) dot b, $ i.e., a split verification algorithm that checks whether $proof$ attests a) to $instance in language$ when $b=0$ or b) to the existence of a proof that does when $b=1$. Importantly, this can be achieved recursively, as @@ -296,126 +310,95 @@ $ $ with $ - r_i :&= g(comm((tilde(verify)^*_0||tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0||tilde(verify)^*_1)], dot)), [proof_i, 1-delta_(i,0)]). -$ - -= Applied to lambda VM - - -When both VMs are proven using the same proof system, the inner product argument is excessive. -Here, the same commitment to $comm((proof, record))$ can be interpreted by both VMs. -It therefore suffices for the verifier to verify both partial proofs against -the same public proof-record commitment. - -base level: -- input: instance, verifier -- witness: proof, record -- output: proof - -$ - verify': commitmentSpace^2 times proofSpace: (comm(x), comm(y), proof) mapsto - verify(comm(x), proof) or verify(comm(y(comm(x), comm(y); dot)), proof) -$ - -how to split $verify'$ into $verify'_0$ and $verify'_1$ - -$ - verify': commitmentSpace^2 times proofSpace: (comm(x), comm(y), proof) mapsto - verify(comm(x), proof) or verify(comm(y(comm(x), comm(y); dot)), proof) -$ - -$ - &verify'_0: (comm(x), comm(y), proof) mapsto - verify_0(comm(x), proof) or verify_0(comm(y(comm(x), comm(y); dot)), proof)\ - &verify'_1: (comm(x), comm(y), proof) mapsto - verify_1(comm(x), proof) or verify_1(comm(y(comm(x), comm(y); dot)), proof)\ -$ - -$ - &verify_0(comm(x), proof)\ - &verify_1(comm(x), proof) -$ - -recursion level: - -$ - &verify'_0\ - &verify'_1\ -$ - - -$ - verify -$ - -TODO: -We assume that these VMs are proven using the same proof system, -yielding a unified proof of the combined execution as a result. - - -= Combining recursive proving and split processing - -= Applied to LambdaVM -We lastly provide some notes on applying the recursive proving and split processing to -the verification of a proof in the context of this VM. - -First, we note that in any scenario, the prover has to commit to the program $program$ -being exeucted and the public input $input$ that is provided. -In a non-recursive proof, this is trivially done by committing to the `DECODE` table -representing $program$, and the `PAGE` tables storing the public $input$. -Since these commitments are deterministic, the verifier can locally reconstruct -the commitments and verify any opening proofs against its own version of the commitment. -Note that in this case, the prover may exclude the opened value from any proof strings -pertaining to the `DECODE` and `PAGE` tables, as these are already known to the verifier. - -When recursing on this process, the prover provides the verifier with this commitment. -We thus have to demonstrate the commitments the prover provides are as expected. -This is achieved by having the verification algorithm `COMMIT` (see @commit) -to the public input it is provided. -This act produces an imbalance in the LogUp-component of the proof-of-verification, -which must be balanced during verification in the _next_ recursion layer. -In later recursions, the verifier must consistently `COMMIT` to its public input -and use the _same_ public input to balance out the LogUp-component of the proof -it is provided. -This solution effectively kicks the can down the road; the final verifier has to -provide the initial input to the program as input to verify the recursive proof. - -Denoted as pseudo-algorithms, we find: - -= Applied to LambdaVM - - -In theory, any division of tasks between the two VMs would work. -Moreover, it is unclear what division will lead to optimal performance. -Yet, it is expected that divisions adhering to these high-level guidelines will -be a good first step towards a performant verifier: -+ have the field-VM perform all verification steps involving field arithmetic, -+ include all verifier-issued challenges required by these verification steps - in the communication record $record$ as field-elements, so that the field-VM does not have to derive them, -+ use the binary-VM to verify the challenges hinted by the communication record are indeed correct. - -*Communication record overview:* -- the data required according to the chosen verification split, -- if $b=1$, reconstructed commitment $comm(verify'(comm(instance), comm(verify'); dot))$ - -*$verify'_b\(comm(instance), (comm(verify'_b), comm(verify'_f)), proof, record)$:* -- `COMMIT` to $comm(instance)$, $comm(verify'_b),$ and $comm(verify'_f)$ -- verify proof: - - if $b=0$: execute $verify_b (comm(instance), proof)$ - - if $b=1$: - + construct $comm(verify'(comm(instance), comm(verify'); dot))$ from $(comm(instance), (comm(verify'_b), comm(verify'_f)))$ - + execute $verify_b (comm(verify'(comm(instance), comm(verify'); dot)), proof)$ - -*$verify'_f\(comm(instance), (comm(verify'_b), comm(verify'_f)), b, proof, record)$:* -- verify proof: $verify_b (comm(verify'(comm(instance), comm(verify'); dot)), proof)$ - - if $b=1$, use $comm(instance), comm(verify'_b), comm(verify'_f)$ to complete the `COMMIT` LogUp-balance. - -*Prover:* -$ - proof &arrow.l prove(instance, witness)\ - proof' &arrow.l prove(verify'_b || verify'_f, (commit(instance), (commit(verify'_b), commit(verify'_f)), 0, proof, record))\ - proof^((i)) &arrow.l prove(verify'_b || verify'_f, (commit(instance), (commit(verify'_b), commit(verify'_f)), 1, proof^((i-1)), record)) -$ - -*Final verification.* -$verify'(commit(instance), (commit(verify'_b), commit(verify'_f)), 1, proof^((n))) =^? one$ + r_i :&= d(comm((tilde(verify)^*_0||tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0||tilde(verify)^*_1)], dot)), [proof_i, 1-delta_(i,0)]). +$ + += The theory applied +We now discuss how the split-recursion system is integrated in practice. + +== The split +Let $v$ denote the verification algorithm performing all steps outlined in @verification. +We split $v$ into halves $tilde(v)_f$ and $tilde(v)_b$ such that an efficient +arithmetization is achieved when the former is executed in the _field-VM_ (@field-VM) +and the latter on the _RiscV-VM_ (@decode through @ecall). +Practically speaking, $tilde(v)_f$ is put in charge of all verification steps +involving _field_ arithmetic --- e.g., verifying `FRI` folding, +while $tilde(v)_b$ performs all _binary_ arithmetic --- e.g., challenge derivation +by means of the Fiat-Shamir transformation. + +The communication record primarily exists of the various Fiat-Shamir-derived +challenges required by $tilde(v)_f$ to complete verification. +During execution, $tilde(v)_b$ is in charge of validating these record values, +while $tilde(v)_f$ assumes them to be correct. + +#et([update the communication record overview once @verification is complete.]) + +== Recursive instance verification +In @growing-instance-complexity, it is assumed that one can efficiently construct +the commitment $comm(y([comm(x), comm(y)], dot))$ from $(comm(x), comm(y))$. +We show that this assumption holds in practice. + +First, note that for an instance $program(input, dot)$, the program +$program$ and input $input$ are committed to separately. +Recall that a (split) program is encoded as one or more +`DECODE` (@decode) and/or `FIELD-DECODE` (@field-decode) tables, while the +input $input$ --- and private input $witness$ and record $record$ for that matter +--- are made available to the VMs by means of `PAGE` tables (@streaming:chip:page). +In this proof system, the prover commits to each of these tables individually +by means of sharing _the root of their merkle-tree_. +#footnote([ + To clarify the process: + + every table column is _interpolated_, creating a polynomial that + evaluates to the column entries on specific inputs, + + the polynomial is _encoded_, creating a codeword of polynomial evaluations + over a different, larger domain, + + the codewords are _batched_, turning a list of codewords into a codeword of lists, and + + the batched codeword is _merkle-committed_, yielding the tree root. +]) + +Aside from this proof-system level commitment contraption, we can additionally leverage +the `COMMIT` chip to commit to individual bytes in the input. +Any values sent by the guest program to `std::out` are recorded in this chip's +table, with the table set up such that it causes an imbalance in the interaction logic +of the proof system during proving. +During verification, it can be verified that this imbalance is caused by the +`COMMIT`ments of this public information. + +Leveraging the `COMMIT` chip is mostly useful in situations where revealing full `PAGE` +tables is unnecessarily expensive or cumbersome, e.g., when committing to small +amounts of data or to data scattered across several `PAGE` tables. +One potential limitation is that `COMMIT`ting in this way is at the discretion of the VM's +guest program. +Since the guest program is publically known during recursive verification, +this limitation does not apply here + +Hence, by having $tilde(v)_b ([comm(x), comm(y)], [[proof, b], record])$ `COMMIT` +to the commitments $comm(x)$ and $comm(y)$ it is provided, and using the same commitments +to balance the proof's interaction logic when $b=1$, the ultimate verifier of the +final proof can be confident that the same verification algorithm was used +at every recursion step when verifying +$(comm(x), comm(y)) = (comm(instance), comm(tilde(v)_b || tilde(v)_f))$. + +== Summary + +*Communication record $record$:*\ +The communication record contains all challenges derived from the proof by +means of the Fiat-Shamir transformation. + +*`RiscV-VM` subalgorithm* +$tilde(v)_b ([comm(instance), comm(instance2)], [[proof, b], record])$: +- `COMMIT`s to $comm(instance), comm(instance2)$ by sending both halves to `std::out`. +- derives challenges from $proof$ by means of Fiat-Shamir, and assert that they + match those located in $record$ at the expected location. +- Performs the binary arithmetic steps required to verify that $proof$ attests + to $instance$ (when $b=0$) or $instance2$ (when $b != 0$#footnote[The RiscV-VM's `PAGE` tables only supports byte data. All non-zero data is treated as $b=1$.]), + given the derived challenges. + +*`Field-VM` subalgorithm* +$tilde(v)_f ([comm(instance), comm(instance2)], [[proof, b], record])$: +- Performs the field arithmetic steps required to verify that $proof$ attests + to $instance$ (when $b=0$) or $instance2$ (when $b != 0$), + given the challenges stated on the $record$. + - Importantly, when $b != 0$, assert that the proofs interaction-logic is + balanced out by including $comm(instance), comm(instance2)$ and the + appropriate challenge under `COMMIT`'s domain separator. From 694a6a5b59eeb4a1f55217f08ce59cd4aeed2c0d Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Tue, 22 Sep 2026 14:31:19 +0200 Subject: [PATCH 14/16] Apply batched suggestions from code review Co-authored-by: Robin Jadoul --- spec/chapters/recursion.typ | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 3e1e37600..981f4ef85 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -35,14 +35,14 @@ Let $BB := { zero, one }$ denote the boolean set and let $programSpace := {program: inputSpace times witnessSpace to BB}$ denote the set of functions mapping the (public) input space $inputSpace$ and (private) witness space $witnessSpace$ to this set. -We define instance space $instanceSpace := programSpace times inputSpace = {program: witnessSpace to BB}$; +We define instance space $instanceSpace := programSpace times inputSpace tilde.equiv {program: witnessSpace to BB}$; program-input pairs $(program, input) in instanceSpace$ are henceforth referred to as _function instances_, or simply _instances_. Where the individual components of the pair are irrelevant, an instance is denoted as $instance in instanceSpace$. -We define relation $relation subset instanceSpace times witnessSpace$ where $((program, input), witness) in relation$ if $program(input, witness) = 1$. -This relation induces the language $language subset instanceSpace$ of _solvable instances_, +We define relation $relation subset.eq instanceSpace times witnessSpace$ where $((program, input), witness) in relation$ if $program(input, witness) = 1$. +This relation induces the language $language subset.eq instanceSpace$ of _solvable instances_, where $instance in language$ if there exists a witness $witness$ for which $(instance, witness)in relation$. Lastly, we introduce the instance commitment function $c: instanceSpace to commitmentSpace$. @@ -358,7 +358,7 @@ by means of sharing _the root of their merkle-tree_. Aside from this proof-system level commitment contraption, we can additionally leverage the `COMMIT` chip to commit to individual bytes in the input. -Any values sent by the guest program to `std::out` are recorded in this chip's +Any values sent by the guest program to `stdout` are recorded in this chip's table, with the table set up such that it causes an imbalance in the interaction logic of the proof system during proving. During verification, it can be verified that this imbalance is caused by the @@ -387,7 +387,7 @@ means of the Fiat-Shamir transformation. *`RiscV-VM` subalgorithm* $tilde(v)_b ([comm(instance), comm(instance2)], [[proof, b], record])$: -- `COMMIT`s to $comm(instance), comm(instance2)$ by sending both halves to `std::out`. +- `COMMIT`s to $comm(instance), comm(instance2)$ by sending both halves to `stdout`. - derives challenges from $proof$ by means of Fiat-Shamir, and assert that they match those located in $record$ at the expected location. - Performs the binary arithmetic steps required to verify that $proof$ attests From 97942270541b3c40bb7edf68c3c5685b5a8eaa56 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 22 Sep 2026 14:15:44 +0200 Subject: [PATCH 15/16] spec/recursion: drop book.typ --- spec/book.typ | 236 -------------------------------------------------- 1 file changed, 236 deletions(-) delete mode 100644 spec/book.typ diff --git a/spec/book.typ b/spec/book.typ deleted file mode 100644 index 847730933..000000000 --- a/spec/book.typ +++ /dev/null @@ -1,236 +0,0 @@ -#import "@preview/shiroa:0.3.1": * -#import "/templates/page.typ": project -#import "@preview/equate:0.3.2": equate - -#show: book - -#let meta = ( - title: "Lambda VM specification", - authors: ("3MI Labs", "Aligned"), - version: "0.2", - summary: ( - ("PROOF SYSTEM", ( - ("logup.typ", [`LogUp` argument], ), - ("memory.typ", [Memory argument], ), - ("streaming.typ", [Streaming prover], ), - ("verifier.typ", [Verification], ) - )), - ("OVERVIEW", ( - ("variables.typ", [Variables], ), - ("signatures.typ", [Signatures], ), - )), - ("TEMPLATES", ( - ("is_bit.typ", [`IS_BIT` template], ), - ("is_byte.typ", [`IS_BYTE` template], ), - ("sign.typ", [`SIGN` template], ), - ("add.typ", [`ADD`/`SUB` template], ), - ("neg.typ", [`NEG` template], ), - ("reg.typ", [`REG`/`REGW` template], ), - )), - ("CPU", ( - ("decode.typ", [`DECODE` table], ), - ("cpu.typ", [`CPU` chip], ), - ("cpu32.typ", [`CPU32` chip], ), - )), - ("ALU", ( - ("shift.typ", [`SHIFT` chip], ), - ("branch.typ", [`BRANCH` chip], ), - ("lt.typ", [`LT` chip], ), - ("eq.typ", [`EQ` chip], ), - ("mul.typ", [`MUL` chip], ), - ("dvrm.typ", [`DVRM` chip], ), - ("bitwise.typ", [`BITWISE` chips], ), - ("bytewise.typ", [`BYTEWISE` chip], ) - )), - ("MEMORY", ( - ("memw.typ", [`MEMW` chip], ), - ("load.typ", [`LOAD` chip], ), - ("store.typ", [`STORE` chip], ), - )), - ("ECALLS", ( - ("about_ecalls.typ", [About `ECALL`], ), - ("halt.typ", [`HALT` chip], ), - ("commit.typ", [`COMMIT` chip], ), - ("sha256.typ", [`SHA256` accelerator], ), - ("keccak.typ", [`KECCAK` accelerator], ), - ("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], ), - )) - ) -) -#let meta_sections = meta.summary.map(m => m.at(1)).sum() -#book-meta( - title: meta.title, - authors: meta.authors, - summary: prefix-chapter("front.typ", meta.title) - + meta.summary.map( - ((title, sections)) => { - heading(depth: 1, title) + sections.map(((ch, title, _ref)) => chapter(ch, title)).join() - } - ).join() -) - -#let highlights = ( - "aside": ("Aside", rgb("55aaff")), - "attention": ("Attention", rgb("ff2600")), -) - -#let highlight(title, body, ref: none, kind: "aside") = [ - #figure( - caption: title, - supplement: highlights.at(kind).at(0), - kind: kind, - body - )#ref -] - -#let aside = highlight.with(kind: "aside") -#let attention = highlight.with(kind: "attention") - -#let common-formatting(body) = { - set footnote(numbering: "[1]") - show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt) - show ref: equate.with(sub-numbering: true, breakable: true, number-mode: "label") - show selector.or(..highlights.keys().map(k => figure.where(kind: k))): it => { - set figure.caption(position: top) - show figure.caption: cap => block( - inset: (left: 1em, right: 1em, top: .75em, bottom: .75em), - outset: (left: 1em), - width: 100% + 1em, - fill: highlights.at(it.kind).at(1), - stroke: luma(50%), - align(center, strong(text(fill: black, cap))) - ) - block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: luma(50%), breakable: false, align(left, it)) - } - body -} - - -#let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.4em, radius: 20%, stroke: black)[ - #set text(fill: foreground) - *TODO #if name != none { [(#name)] }*: #body -] -#let rj = todo.with(background: teal, name: "Robin") -#let et = todo.with(background: rgb("d4aa3a"), name: "Erik") -#let cdsg = todo.with(background: olive, name: "Cyprien") - - -#let is-shiroa = "x-target" in sys.inputs - -// Strip styling to keep only "pure" content. -// This is useful to avoid errors on the `set document(...)` in `project` -// when invisibly including other chapters to resolve xrefs. -#let strip-all(content) = { - if repr(content.func()) == "sequence" { - for c in content.children { - strip-all(c) - } - } else if repr(content.func()) == "styled" { - strip-all(content.child) - } else { - content - } -} - -#let _toplevel = state("_toplevel", none) -#let _xref-included = state("_xref-included", (:)) - -// Invisibly include another chapter, so that its labels can be resolved -#let xref-include(f) = { - show ref: none - context { - place(hide(box(width: auto, height: 0%, strip-all(include "/" + f)))) - } -} - -// Generate a cross-link for references to other chapters. -// Leaves the ref untouched if it can't be resolved or points to the current chapter. -#let xref(rf) = { - assert(is-shiroa, message: "xref should only be used when compiling for shiroa") - let lbl = rf.target - let found = meta_sections.find(((_, _, tag)) => str(lbl).starts-with(str(tag))) - context if found != none and found.at(0) != _toplevel.final() { - let (ch, title, ref) = found - if ref == lbl { - cross-link("/" + ch, [Chapter #(meta_sections.position(x => x == found) + 1)]) - } else { - // Because shiroa does weird url escaping - let shiroa-label = label(str(lbl).replace(":", "%3A")) - context _xref-included.update(x => x + ((ch): true)) - // The ideal would be to use `rf` directly as content argument to `cross-link`, - // as that would inherit any/all formatting of the ref we want or need. - // Unfortunately the ref link seems to take precedence over the cross-link hyperlink - // when clicking. - // There may still be some way around it by messing with some html output - let link-content = context { - let fig = query(lbl).first() - let counter = if fig.has("counter") { - fig.counter - } else { - counter(fig.func()) - } - - let supplement = if rf.supplement == auto { - fig.fields().at("supplement", default: none) - } else { - rf.supplement - } - [#supplement #numbering(fig.numbering, ..counter.at(lbl))] - } - cross-link("/" + ch, reference: shiroa-label, link-content) - } - } else { - rf - } -} - -#let book-page(file, ..args) = { - if not file.ends-with(".typ") { - file = lower(file) + ".typ" - } - - assert(meta_sections.find(s => s.at(0) == file) != none, message: "Couldn't resolve typst source file " + file) - - if is-shiroa { - (body) => { - show: common-formatting - context _toplevel.update(s => { - if s == none { - file - } else { - s - } - }) - let cond() = _toplevel.final() == file - show ref: it => context if cond() { xref(it) } - let title = context { - // Strip raw, because shiroa already makes the title raw - show raw: it => it.text - meta_sections.find(x => x.at(0) == _toplevel.final()).at(1) - } - project.with(..args, title: title, description: plain-text(meta_sections.find(x => x.at(0) == file).at(1)), cond: cond)([ - #context _xref-included.final().pairs().map(((key, value)) => context if value and cond() { - xref-include(key) - }).join() - #metadata(json("interaction_count.json").sum(default: (:))) - - #let chapter-index = meta_sections.position(x => x.at(0) == file) + 1 - #set heading(numbering: (..args) => [#chapter-index.#numbering("1.1", ..args)]) - #counter(heading).update(0) - - #body - ]) - } - } else { - body => body - } -} From 5ba52b7d8a55104c48aeb85c6eca2a17f6cb4d76 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 22 Sep 2026 14:26:59 +0200 Subject: [PATCH 16/16] spec/recursion: replace || by `product` --- spec/chapters/recursion.typ | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ index 981f4ef85..009b02942 100644 --- a/spec/chapters/recursion.typ +++ b/spec/chapters/recursion.typ @@ -159,6 +159,8 @@ such that either half can be executed on a VM with an instruction set tailored t while maintaining completeness and soundness of the verification. == Communication +#let product(f, g) = $(#f and #g)$ + When executing the two verification-algorithm halves on distinct VMs, no direct communication between both algorithms is possible, even if both VMs are proven using the same proof system. @@ -225,11 +227,11 @@ $ dot tilde(v)_1(comm(instance), [proof, d(comm(instance), proof)]). $ where $d(comm(instance), proof)$ denotes the record deriviation function. -We introduce the function product $(f || g)(input, witness) := f(input, witness) dot g(input, witness)$ for $f, g in programSpace$. +We introduce the function product $(product(f, g)(input, witness) := f(input, witness) dot g(input, witness)$ for $f, g in programSpace$. This then allows us to express $ prove(verify(comm(instance), dot); proof) - &= prove((tilde(v)_0 || tilde(v)_1)(comm(instance), dot); [proof, record]) + &= prove(product(tilde(v)_0, tilde(v)_1)(comm(instance), dot); [proof, record]) &= proof', $ with $record := d(comm(instance), proof)$. @@ -238,7 +240,7 @@ Summarizing, we have now expressed recursive verification in terms of a split verifier, where the same instance-proof-record triple was provided to both verification halves. The produced proof $proof'$ now attests to $instance in language$ when -$verify(comm((tilde(v)_0 || tilde(v)_1)(comm(instance), dot)), proof') = 1$. +$verify(comm(product(tilde(v)_0, tilde(v)_1)(comm(instance), dot)), proof') = 1$. = Split proving #et("todo") @@ -283,34 +285,33 @@ jointly form a valid split of $verify^*$, since $ verify^*([comm(x), comm(y)], [proof, b]) &= verify(Delta_C (comm(x), comm(y([comm(x), comm(y)], dot)), b), proof)\ - &= (tilde(verify)_0 || tilde(verify)_1)(Delta_C (comm(x), comm(y([comm(x), comm(y)], dot)), b), [proof, r])\ - &= (tilde(verify)^*_0 || tilde(verify)^*_1)([comm(x), comm(y)], [[proof, b], r]),\ + &= product(tilde(verify)_0, tilde(verify)_1)(Delta_C (comm(x), comm(y([comm(x), comm(y)], dot)), b), [proof, r])\ + &= product(tilde(verify)^*_0, tilde(verify)^*_1)([comm(x), comm(y)], [[proof, b], r]),\ $ when $r = d([comm(x), comm(y([comm(x), comm(y)], dot))], [proof, b])$. -By selecting $(comm(x), comm(y)) = (comm(instance), comm(tilde(v)^*_0 || tilde(v)^*_1))$, +By selecting $(comm(x), comm(y)) = (comm(instance), comm(product(tilde(v)^*_0, tilde(v)^*_1)))$, we now obtain $ - (tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0 || tilde(verify)^*_1)], [[proof, b], r]) - // &= tilde(verify)^*_0([comm(instance), comm(tilde(verify)^*_0 || tilde(verify)^*_1)], [[proof, b], r]) dot tilde(verify)^*_1([comm(instance), comm(tilde(verify)^*_0 || tilde(verify)^*_1)], [[proof, b], r])\ - &= verify^*([comm(instance), comm(tilde(verify)^*_0 || tilde(verify)^*_1)], [proof, b])\ - &= verify(Delta_commitmentSpace (comm(instance), comm((tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance),comm(tilde(verify)^*_0 || tilde(verify)^*_1)], dot)), b), proof)\ - &= Delta_BB (verify(comm(instance), proof), verify(comm((tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance),comm(tilde(verify)^*_0 || tilde(verify)^*_1)], dot)), proof), b)\ - &= verify(comm(instance), proof) dot (1-b) + verify(comm((tilde(verify)^*_0 || tilde(verify)^*_1)([comm(instance),comm(tilde(verify)^*_0 || tilde(verify)^*_1)], dot)), proof) dot b, + product(tilde(verify)^*_0, tilde(verify)^*_1)([comm(instance), comm(product(tilde(verify)^*_0, tilde(verify)^*_1))], [[proof, b], r]) + &= verify^*([comm(instance), comm(product(tilde(verify)^*_0, tilde(verify)^*_1))], [proof, b])\ + &= verify(Delta_commitmentSpace (comm(instance), comm(product(tilde(verify)^*_0, tilde(verify)^*_1)([comm(instance),comm(product(tilde(verify)^*_0, tilde(verify)^*_1))], dot)), b), proof)\ + &= Delta_BB (verify(comm(instance), proof), verify(comm(product(tilde(verify)^*_0, tilde(verify)^*_1)([comm(instance),comm(product(tilde(verify)^*_0, tilde(verify)^*_1))], dot)), proof), b)\ + &= verify(comm(instance), proof) dot (1-b) + verify(comm(product(tilde(verify)^*_0, tilde(verify)^*_1)([comm(instance),comm(product(tilde(verify)^*_0, tilde(verify)^*_1))], dot)), proof) dot b, $ i.e., a split verification algorithm that checks whether $proof$ attests a) to $instance in language$ when $b=0$ or b) to the existence of a proof that does when $b=1$. Importantly, this can be achieved recursively, as $ #h(8em) // alignment purposes &prove(instance; witness) &&to proof_(0),\ - &prove((tilde(verify)^*_0||tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0||tilde(verify)^*_1)], dot); [[proof_(0), 0], r_(0)]) &&to [proof_(1), 1],\ - &prove((tilde(verify)^*_0||tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0||tilde(verify)^*_1)], dot); [[proof_(1), 1], r_(1)]) &&to [proof_(2), 1],\ - &prove((tilde(verify)^*_0||tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0||tilde(verify)^*_1)], dot); [[proof_(2), 1], r_(2)]) &&to [proof_(3), 1], + &prove(product(tilde(verify)^*_0, tilde(verify)^*_1)([comm(instance), comm(product(tilde(verify)^*_0, tilde(verify)^*_1))], dot); [[proof_(0), 0], r_(0)]) &&to [proof_(1), 1],\ + &prove(product(tilde(verify)^*_0, tilde(verify)^*_1)([comm(instance), comm(product(tilde(verify)^*_0, tilde(verify)^*_1))], dot); [[proof_(1), 1], r_(1)]) &&to [proof_(2), 1],\ + &prove(product(tilde(verify)^*_0, tilde(verify)^*_1)([comm(instance), comm(product(tilde(verify)^*_0, tilde(verify)^*_1))], dot); [[proof_(2), 1], r_(2)]) &&to [proof_(3), 1], &&#h(8em)text(italic("etc.")) $ with $ - r_i :&= d(comm((tilde(verify)^*_0||tilde(verify)^*_1)([comm(instance), comm(tilde(verify)^*_0||tilde(verify)^*_1)], dot)), [proof_i, 1-delta_(i,0)]). + r_i :&= d(comm(product(tilde(verify)^*_0, tilde(verify)^*_1)([comm(instance), comm(product(tilde(verify)^*_0, tilde(verify)^*_1))], dot)), [proof_i, 1-delta_(i,0)]). $ = The theory applied @@ -377,7 +378,7 @@ to the commitments $comm(x)$ and $comm(y)$ it is provided, and using the same co to balance the proof's interaction logic when $b=1$, the ultimate verifier of the final proof can be confident that the same verification algorithm was used at every recursion step when verifying -$(comm(x), comm(y)) = (comm(instance), comm(tilde(v)_b || tilde(v)_f))$. +$(comm(x), comm(y)) = (comm(instance), comm(product(tilde(v)_b, tilde(v)_f)))$. == Summary