Skip to content
This repository has been archived by the owner on Apr 9, 2024. It is now read-only.

Add a field or a method to indicate what are the initial witnesses needed to solve a circuit #62

Closed
kevaundray opened this issue Jan 20, 2023 · 2 comments
Labels
enhancement New feature or request

Comments

@kevaundray
Copy link
Contributor

kevaundray commented Jan 20, 2023

Problem

A circuit is solvable if it is given an initial set of witness values. There is currently no way to validate this and upstream users of ACIR will need to somehow validate this or not validate it and hope that this is the case.

Another usecase is that an optimisation pass may wish to modify witnesses and it would be good to know which of the initial witnesses are always constants for example -- ie we can then pass information back to the user stating that the circuit is only solvable if their fourth initial witness value is always 5 for example.

Solution

We can add a field into ACIR which indicates these set of values. Moreover, we could avoid having a large set of values by allowing one to indicate a contiguous range, ie Range(0, 500) would mean that the first 500 witnesses are needed in order for this circuit to be solvable.

Example:

enum InitialWitnesses {
    Range(usize, usize),
    Values(Vec<InitialWitnesses>),
    Value(usize)
}

Alternatives considered

(Describe any alternative solutions you have considered.)

Additional context

(If applicable.)

@kevaundray kevaundray added the enhancement New feature or request label Jan 20, 2023
@guipublic
Copy link
Contributor

Ideally, an ACIR circuit should specify:

  • the inputs to the circuit
  • the public inputs
  • the outputs

Not taking into account any noir specificities, the simplest would be to require the inputs to be the first witnesses.
So in that case a range or the number of inputs is enough.
The public inputs would be a subset of the inputs, and in order to be flexible, we could use the provided InitialWitnesses enum to define them.
My rational is that inputs can potentially be very big, while public inputs are usually kept small, by providing them out-of-band and using hash of the public inputs when they are required to be big.
Finally, the outputs are a list with eventual duplicates from the public inputs.

Note that inputs and outputs can be deduced from the circuit, but not the public inputs. An alternative could be to simply tag public inputs as 'pub' in the ACIR gates and deduce the above lists from the circuit.

@kevaundray
Copy link
Contributor Author

I think the outputs is a separate issue, though it seems that we are on the same page with regards to initial witnesses.

This issue is solely related to specifying the inputs needed to allow the circuit to be solvable, ie the inputs which cannot be computed from other inputs.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

3 participants