Add an API to construct a Halo 2 circuit from a set of constraints

[str4d]

At RWC I was chatting with Wei Dai, who mentioned (I think? I talked to a lot of people) that Anoma (was it?) are working on a specification called Vampir (? I'm bad at taking notes, okay) which is an attempt at defining an Intermediate Representation for constraint languages. IIRC the idea is that programs get compiled into general polynomial constraints between some set of defined variables, and then those constraints can be passed to a backend that e.g. splits them apart into R1CS form.

It would be neat if halo2_proofs could interoperate with this IR. The simplest way to perform the integration would be to treat each constraint as a single Gate, create a Selector for each Gate, and create a separate Region for each Gate. All of this would be implemented as a single chip, to which the variables and constraints would be provided. Then it can just create the Regions in the order that the constraints are provided, and the existing floor planning logic will be sufficient to optimise the layout.

The main issues that occur to me:

• It would be nice if the IR could identify selectors or other fixed values. In the meantime, we'd extract every additive or multiplicative constant in each constraint for assignment in a fixed cell, and would only use selectors to toggle the entire constraints.
• Configuration. Currently we don't have full floor planning implemented (only vertical laying out), so without #195 we'd need some kind of macro to create the Circuit implementation. But I'm not convinced we could do so dynamically (because Circuit::configure takes no runtime arguments), which means the caller would need to precisely specify how many fixed, advice, and instance columns to create (and how many selectors we'd need).
• Constraint shape. I suspect the best trade-off will be to query cells in a rectangular shape, using more columns than rows (in order to use fewer, more common rotations), but maybe this can be a tunable parameter that the caller provides.
• For the initial implementation we'd just use the constraints exactly as provided, so we'd rely on the caller to control the maximum degree of the circuit.
• AFAICT this IR wouldn't enable us to leverage any lookup arguments. We would make heavy use of equality constraints, so we'd probably just have every single advice column be equality-enabled.

[joebebel]

No notes needed, you got it pretty accurate. There is even a spec and some examples in progress at: https://specs.anoma.net/master/architecture/j-group/vampir/vampir.html

There may be some bridging needed between Halo 2 terminology/concepts, but it's manageable.

In the long run, the hope is that circuits can be written in a strongly-typed, formally-verifiable language like Juvix and compiled very efficiently to the proving system backend.

I think integrating lookup arguments is very high on the wish list. (Indeed, I'd rather target PLONK/Halo2 style backends than R1CS, but they're not mutually exclusive). Under the design philosophy section, there's some ideas how this might work, in particular how the IR can potentially represent the intent of the circuit, and convert to lookups automatically.

[jMyles]

Brilliant presentation at Zero-Knowledge summit. The visual and spacial metaphor for the circuits and gadgets is quite elegant.

I have no specific thoughts on a Halo 2 API, except to say that it's a very interesting issue.

[softminus]

Brilliant presentation at Zero-Knowledge summit. The visual and spacial metaphor for the circuits and gadgets is quite elegant.

Is there video of the presentation / PDF of the slides? I wasn't able to attend and I'm interested (I'm looking into seeing how techniques from the ASIC/FPGA logic synthesis / place-and-route world can be applicable for targeting Halo2/PLONK-style backends)

[Janmajayamall]

Brilliant presentation at Zero-Knowledge summit. The visual and spacial metaphor for the circuits and gadgets is quite elegant.

Is there video of the presentation / PDF of the slides? I wasn't able to attend and I'm interested (I'm looking into seeing how techniques from the ASIC/FPGA logic synthesis / place-and-route world can be applicable for targeting Halo2/PLONK-style backends)

I believe they are referring to this https://www.youtube.com/watch?v=V1RgGn1GtqM&list=PLj80z0cJm8QFnY6VLVa84nr-21DNvjWH7&index=13 or this https://www.youtube.com/watch?v=aU2ICVrST10