Expose Basic Gate (for AND gadget) #190
Conversation
ocaml/lib/snarky_bindings.ml
Outdated
| let basic sl l sr r so o sm sc = | ||
| Impl.with_label "generic_gate" (fun () -> | ||
| Impl.assert_ | ||
| { annotation = Some __LOC__ | ||
| ; basic = | ||
| Kimchi_backend_common.Plonk_constraint_system.Plonk_constraint.T | ||
| (Basic { l = (sl, l); r = (sr, r); o = (so, o); m = sm; c = sc }) | ||
| } ) |
There was a problem hiding this comment.
I exposed Basic and configured the gate in TS insetead of implementing and_equation as in the OCaml code.
- Is this the right approach?
- Are the argument names appropriate?
- Is there anything else I should expose while I'm here?
There was a problem hiding this comment.
1a) Yes it's the right approach to expose the generic gate in it's most general form and not specialized to the "and" logic. We definitely want this in o1js!
1b) I don't think we need it for the "and" gadget though. o1js creates the right generic gates when you do .add() and mul() and so on, which we could use for "and" (will comment on the other PR)
2) I think so. I guess sl means "the selector for the left input" etc?
3) No I think this is good, although I think we should out of principle make an effort to expose all gates to o1js, but that can be a separate PR
There was a problem hiding this comment.
1b) Ahhhh! My assumption was that that would be less efficient than doing what I did, but I think I understand now. I gather from Anaïs that when I call .add(), it goes on to a stack, and then once there is enough on the stack for us to generate an efficient constraint we do so. Is that correct? (Don't worry about tying it all out here if not; maybe we can just do a short call sometime and I will make a list of questions).
2) Correct!
There was a problem hiding this comment.
Yeah what Anais wrote is true but she probably didn't know that a simple Field.mul() also flushes that stack into a constraint, so we don't need that complicated way of specifying the gate
ocaml/lib/snarky_bindings.ml
Outdated
| let basic sl l sr r so o sm sc = | ||
| Impl.with_label "generic_gate" (fun () -> | ||
| Impl.assert_ | ||
| { annotation = Some __LOC__ | ||
| ; basic = | ||
| Kimchi_backend_common.Plonk_constraint_system.Plonk_constraint.T | ||
| (Basic { l = (sl, l); r = (sr, r); o = (so, o); m = sm; c = sc }) | ||
| } ) |
There was a problem hiding this comment.
1a) Yes it's the right approach to expose the generic gate in it's most general form and not specialized to the "and" logic. We definitely want this in o1js!
1b) I don't think we need it for the "and" gadget though. o1js creates the right generic gates when you do .add() and mul() and so on, which we could use for "and" (will comment on the other PR)
2) I think so. I guess sl means "the selector for the left input" etc?
3) No I think this is good, although I think we should out of principle make an effort to expose all gates to o1js, but that can be a separate PR
Summary
This PR exposes the generic constraint to our JS bindings via a function called
Basicand is part of the work necessary for the AND gadget.Context
The AND gadget behaves similarly to the
&operator in JavaScript and does not require a new custom gate. Instead, it uses the XOR gate and one generic gate. See OCaml implementation for context.Tested
This work is tested in the upper layers of o1js with unit and e2e tests built on top of the exposed gate constraint.
AND gadget PR in o1js repo: o1-labs/o1js#1193
closes: o1-labs/o1js#1140