Skip to content
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

Open
wants to merge 5 commits into
base: main
Choose a base branch
from

Conversation

daira
Copy link
Collaborator

@daira 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.

daira and others added 4 commits September 20, 2024 17:27
…more

consistent.

Co-authored-by: Mary Maller <[email protected]>
Co-authored-by: Jack Grigg <[email protected]>
Signed-off-by: Daira-Emma Hopwood <[email protected]>
Co-authored-by: Mary Maller <[email protected]>
Co-authored-by: Jack Grigg <[email protected]>
Signed-off-by: Daira-Emma Hopwood <[email protected]>
@daira daira requested review from str4d and mmaller September 20, 2024 16:43
* 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.
Copy link
Collaborator Author

@daira daira Sep 20, 2024

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 $\mathcal{F}'$, since the minor overspecification makes little difference in practice, and it makes the symmetry between completeness and knowledge soundness more apparent. Also we know that the instance elements will be copied to the witness, so there is not really any harm in omitting them from the input to $\mathcal{F}'$. What do yous think?

Co-authored-by: Mary Maller <[email protected]>
Co-authored-by: Jack Grigg <[email protected]>
Signed-off-by: Daira-Emma Hopwood <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant