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
There was a problem hiding this comment.
It already feels like a lot of bb throughout the document
I know! Once I stumbled across bb on Typst, I fell in love with it 🙈 Let's collaborate on reducing its use to an acceptable level 😉
Do we need these to be bb?
Specifically bb? No. I did feel like it would be useful to distinguish these booleans false/true from normal 0/1, also because some programs use 1 as error state and 0 as success state; I didn't want there to be confusion on what 0/1 meant. I considered bot and top, but was not content with how they looked.
Do you agree that distinguishing them from false/true is valuable? Do you perhaps know of a different useful symbol here?
There was a problem hiding this comment.
I don't think it's strictly needed here to have the separation, as long as it's clearly defined what counts as a "successful" execution. But I'd say top/bot or serif("success")/serif("fail") or the like could probably work as well or better, if you don't want to just to with 0/1
There was a problem hiding this comment.
Refactored it to just 0/1.
| &: 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.
There was a problem hiding this comment.
wdyt of simply rephrasing this in terms of completeness (= proof for solvable instances is accepted) and completeness (= any proof for unsolvable instances is rejected), without the mathematical formulae?
| 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).
There was a problem hiding this comment.
My view on this is as follows:
fis the program with any constants baked in. The commitment offis the merkle commitment of the DECODE table.iare the program settings. The commitment ofiis the merkle commit of the PAGE tables containing public memory.
So, I would say that instance-comm( f(i; ·) ) ≡ (function-comm(f), input-comm(i))
Is this formulation [of commit composition] the case in practice for us?
I believe so, yes
and how does it interact with the absorption remark?
Could you elaborate what you mean by this?
(I haven't refactored the text to work with split instances just yet; would like to reach understanding on the topic before performing the refactor)
There was a problem hiding this comment.
So, I would say that instance-comm( f(i; ·) ) ≡ (function-comm(f), input-comm(i))
My surface reading without this clarification would be to read f(i; ·) as the function with now also i "baked in".
Maybe this needs some in-text clarification.
It can also help a bit to make the definition of bb(X) have a ≅ instead of plain = when reinterpreting it as purely functions taking a witness.
There was a problem hiding this comment.
Could you elaborate what you mean by this?
I mean kinda that I read f(i; ·) as absorbing i into f (as clarified in my previous comment). So you'd end up with some weirdness on how exactly the commitments work there, similar-ish to the circularity of the absorption remark.
There was a problem hiding this comment.
Let me know if the rephrasing works
| *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.
There was a problem hiding this comment.
I'm not content with this section, at all. Indeed, stuff is missing.
I propose we have a full verifier description in verifier.typ (including all the ad-hoc checks you mention) and here only mention how to transform that monolithic verifier into the split/recursive verifier in this section.
wdyt of that split?
There was a problem hiding this comment.
I rewrote this section. Let me know what you think!
Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com>
Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>
2 participants
No description provided.