-
Notifications
You must be signed in to change notification settings - Fork 2
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from September 20 meeting #35
base: main
Are you sure you want to change the base?
Conversation
daira
commented
Sep 20, 2024
- Define shortcut
$[i, j]$ notation and use it consistently. - Clarifications to the definition of a correctness-preserving translation.
- Make notation in the definition of
$\mathcal{R}_{\mathsf{concrete}}$ more consistent. - Move explanations of the FIND_ROW_MAPPING algorithm to its definition.
- Complete the (informal) proof for FIND_ROW_MAPPING.
Signed-off-by: Daira-Emma Hopwood <daira@jacaranda.org>
…ion. Signed-off-by: Daira-Emma Hopwood <daira@jacaranda.org>
…more consistent. Co-authored-by: Mary Maller <mary.maller@ethereum.org> Co-authored-by: Jack Grigg <thestr4d@gmail.com> Signed-off-by: Daira-Emma Hopwood <daira@jacaranda.org>
Co-authored-by: Mary Maller <mary.maller@ethereum.org> Co-authored-by: Jack Grigg <thestr4d@gmail.com> Signed-off-by: Daira-Emma Hopwood <daira@jacaranda.org>
* Completeness is preserved: given a satisfying instance $x$ and witness $w$ for the abstract circuit, $w' = \mathcal{F}(w)$ is a satisfying witness for the concrete circuit with instance $\mathcal{I}(x)$. | ||
* Knowledge soundness is preserved: given a satisfying instance $x'$ and witness $w'$ for the concrete circuit, we can efficiently compute some satisfying witness $w$ for the abstract circuit with instance $\mathcal{I}^{-1}(x')$. | ||
|
||
We also claim that a correctness-preserving translation in this sense, when used with a concrete proof system that is zero-knowledge, necessarily yields an overall proof system for the abstract relation that is zero-knowledge. That is, informally, no additional information about the abstract witness is revealed beyond the fact that the prover knows such a witness. | ||
|
||
> Aside: we could have required there to be an efficient reverse witness translation function $\mathcal{F}' \mathrel{⦂} \mathbb{F}^{m' \times n'} \rightarrow \mathbb{F}^{m \times n}$ from concrete witnesses to abstract witnesses, and then used $w = \mathcal{F}'(w')$ in the definition of knowledge soundness preservation. We do not take that approach because strictly speaking it would be an overspecification: we do not need the satisfying abstract witness to be *deterministically* and efficiently computable from the concrete witness; we only need it to be efficiently computable. Also, in general $w$ could also depend on the instance $x'$, not just $w'$. In practice, specifying such a function $\mathcal{F}'$ is likely to be the easiest way to prove knowledge soundness preservation. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm open to just requiring this to be a deterministic function
Co-authored-by: Mary Maller <mary.maller@ethereum.org> Co-authored-by: Jack Grigg <thestr4d@gmail.com> Signed-off-by: Daira-Emma Hopwood <daira@jacaranda.org>
60f11a6
to
e82162f
Compare