spec: Recursion - #943
Conversation
Kimi Code ReviewAutomated review by Kimi (Moonshot AI) |
Codex Code Review
|
| #let (prove, verify) = ($italic("p")$, $italic("v")$) | ||
|
|
||
| // Mathematical symbols | ||
| #let (zero, one) = ($bb(0)$, $bb(1)$) |
There was a problem hiding this comment.
Do we need these to be bb? It already feels like a lot of bb throughout the document
| 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$. |
There was a problem hiding this comment.
commitments may need to be randomized, so with an explicit randomness parameter maybe c(x; r)
There was a problem hiding this comment.
Or maybe we can be content with a deterministic commitment scheme and make explicit that we don't care about/expect it to be hiding.
| 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 |
There was a problem hiding this comment.
| We now assume the existence of _proving system_ $(prove, verify)$ with | |
| We now assume the existence of _proof system_ $(prove, verify)$ with |
| #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)$) |
There was a problem hiding this comment.
maybe just pi instead of bb?
| &: 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 |
There was a problem hiding this comment.
what probability space is this over? For the prover I'm assuming internal randomness, but the verifier should presumably be deterministic
There was a problem hiding this comment.
I think this may be a side-effect of formalizing things as NIZKs, since the common way to express this as an interactive proocol can rely on the random challenges from the verifier for both of these.
For a NIZK, the soundness becomes computationally secure, presumably, so it becomes dependent on the prover somewhere.
|
|
||
| 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. |
There was a problem hiding this comment.
| typically shrinks (and verification time therefore reduces) as the level of recursion increases. | |
| typically shrinks (and verification time reduces) as the level of recursion increases. |
It is not a guaranteed fact that smaller proofs are faster to verify, though typically they would be
| 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 |
There was a problem hiding this comment.
stick to just
| 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)$. |
There was a problem hiding this comment.
Is this formulation the case in practice for us, and how does it interact with the absorption remark? That is, we let the verifier take an instance as argument, which has already absorbed its input, so that part of the formalization seems slightly wrong here. If we keep instance as (f, i) without the reinterpretation as f(i; .) it might work, but then the way we commit should also change a bit to have a commitment to f and potentially plain i (maybe a commitment to i works, but I'm not 100% certain).
| 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 |
There was a problem hiding this comment.
"This" feels like it refers to what already was described, but the record is not an inherent part of introducing a split, so maybe
| This architecture enables the required communications by introducing a | |
| Our architecture enables the required communications by introducing a |
| *Record $record$.* | ||
| The record contains all challenges the prover derived using Fiat-Shamir. | ||
|
|
||
| *Tasks for $verify'_b\(commitment_0, commitment_1, b, proof, record)$:* |
There was a problem hiding this comment.
This is missing a few of the ad-hoc checks, which are (I think) mostly related to memory and paging.
It would probably be a good idea to have an overview of those somewhere central as well.
2 participants
No description provided.