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

Remove witness handling / as prover code as much as possible from circuits #241

Open
L-as opened this issue Dec 19, 2024 · 3 comments
Open

Comments

@L-as
Copy link
Collaborator

L-as commented Dec 19, 2024

Prover functions should take a function that returns a field as witness, i.e., all provers should have the following type:

type witness = unit -> field
type prover =
  Pickles.Side_loaded.Verification_key.t option -> (* left side loaded vk *)
  Pickles.Side_loaded.Proof.t option -> (* left recursively verified proof *)
  Pickles.Side_loaded.Verification_key.t option -> (* right side loaded vk *)
  Pickles.Side_loaded.Proof.t option -> (* right recursively verified proof *)
  witness ->
  Pickles.Side_loaded.Proof.t

The point is that all witness handling should be done outside the code defining the circuits, to prevent polluting the mind with thoughts about code that doesn't affect the security of the protocol.

Right now we've mixed the two to an uncomfortable degree. Really we we're supposed to use handlers/requests/responses,
but even that is suboptimal, since you end up defining requests for the sake of making proving easier.

In some sense this is the same as what is proposed above but we allow only one kind of request of the following form

type _ Request.t += Get_witness : field Request.t

Of course, you can make a wrapping library for the circuit that defines a more convenient way of passing in the witnesses.
That helper library would have many of the definitions we would have moved out of the circuits by doing this change.

In the circuits we would use a new function in place of exists:

val new_exists : ('var, 't) Typ.t -> 'var Checked.t

To assist with figuring out the order of the witnesses, new_exists could get the line number and file name of each place it's used and print it.

The whole interface of the zeko_circuits library should be something like:

sig
  val prove_inner_sync : prover
  val prove_inner_action_witness : prover
  val inner_vk : Pickles.Side_loaded.Verification_key.t
  (* ... *)
end

Compile_simple.compile should also not provide the circuit with an 'input probably and instead make the circuit
rely on the above-mentioned new_exists exclusively.

Of course in practice we'd replace all of the Pickles types above with our own,
such that we can provide a dummy interface that doesn't use crypto.

@L-as
Copy link
Collaborator Author

L-as commented Jan 9, 2025

This would also involve deleting v.ml and not using its functionality.

@L-as
Copy link
Collaborator Author

L-as commented Jan 18, 2025

I've reconsidered this a bit.

We shouldn't expose the prover functions. We should instead expose the circuits, without any types, and let the user code compile and do everything else.

Recursive proofs like-wise would have to be handled by the user. However, we would have a way of grouping rules into a single "ruleset", such that when compiling circuits, recursive proofs aren't used for the wrong circuit.

@L-as
Copy link
Collaborator Author

L-as commented Jan 18, 2025

Also, exists should take a string, and when providing the witness for the circuit,
it should be such that you should provide a list of fields, along with the "name" for it.

It will be checked that the length and name matches.
Thus, the prover will have no more information, and must still provide everything in the correct order,
but the debuggability is a bit better.

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

No branches or pull requests

1 participant