[Fix] Fix circuit for cast lossy field to group. #2133
Conversation
This resolves the underconstraining bug that was found in that circuit. The fix involves the creation of two new circuits, which are more general and may have other uses: - A circuit for square roots flagged nondeterministic, which return both square roots, in no specified order (hence 'nondeterministic'), if the input is a non-zero square, and returns an error flag set if the input is not a square. - A circuit for turning an x coordinate into the (unique, if it exists) point in the subgroup with that x coordinate, with an error flag set if there is no such point in the subgroup. This circuit makes use of the previous one to solve the curve equation, i.e. to find whether and where x intersects the elliptic curve. The new circuit for cast lossy field to group is realized by using the latter circuit to attempt to find the point in the subgroup with the given value as x coordinate. If none exists, we return the generator if the input is 0, otherwise the result of Elligator-2 is returned, which is always a subgroup point. The use of the new circuits for flagged operations eliminate the underconstraining without eliminating desired solutions (which would happen by enforcing constraints without taking flags into account).
Since this is a flagged operation, it must never fail.
|
As additional "testing", I inspected part of the constraints in the samples (generated by @bendyarm) of these new circuits, and they look reasonable to me. I only inspected part of the constraints because there are literally thousands. Eventually we'll check all of them mechanically in the theorem prover, but I wanted to do a preliminary sanity checks on these new and slightly complicated circuits. |
| let point1_times_order = order_bits_be_constants.mul(point1); | ||
| let point2_times_order = order_bits_be_constants.mul(point2); |
There was a problem hiding this comment.
Can we implement a version of Group::enforce_in_group as Group::is_in_group that returns a boolean?
There was a problem hiding this comment.
Not that I know. If we impose the enforce_in_group constraints directly on the point (x, y) to check, clearly we get unsatisfiable constraints when (x, y) is not in the group. If we postulate a new/separate point (x', y') in the group (using the enforce_in_group constraints), the trouble is how to enforce the right connection between (x, y), (x', y'), and the boolean result r. Just saying that (r = 1) <==> (x = x' & y = y') is underconstrained, because even if (x, y) is in the group, I can pick a different (x', y') also in the group (because the group has more than one point) and set r = 0 (another possible solution being x = x' and y = y' and r = 1 of course).
There was a problem hiding this comment.
I'm not saying it's impossible. Maybe there's something clever, but if there is it has not occurred to any of us yet.
There was a problem hiding this comment.
Looking at enforce_in_group it seems like it's possible to change the enforce_* into is_*, but I don't know what the issue is.
There was a problem hiding this comment.
I looked this morning at ProvableHQ/snarkVM-fork@fix/cast-lossy-field-to-group...feat/is-in-group (which does that) but I see an underconstraining problem similar to above. I'll DM-forward you the details.
|
@howardwu The CI failure may be due to a change in the constraint count: But I'm not seeing explicit numbers to change in that code; presumably they are calculated, but I'm not familiar with that part of the code. |
|
The CI failure is just an S3 failure. I've triggered a re-run of CI |
|
Re-targeted to |
Co-authored-by: Alessandro Coglio <[email protected]> Signed-off-by: d0cd <[email protected]>
Co-authored-by: Alessandro Coglio <[email protected]> Signed-off-by: d0cd <[email protected]>
Co-authored-by: Alessandro Coglio <[email protected]> Signed-off-by: d0cd <[email protected]>
Co-authored-by: Alessandro Coglio <[email protected]> Signed-off-by: d0cd <[email protected]>
[Refactor] Adds some tests and contains some documentation suggestions for the `fix/cast-lossy-field-to-group` PR
| @@ -63,6 +63,65 @@ impl<E: Environment> Field<E> { | |||
| } | |||
| } | |||
|
|
|||
| impl<E: Environment> Field<E> { | |||
| /// Returns both square roots of `self` and a `Boolean` flag, which is set iff `self` is not a square. | |||
There was a problem hiding this comment.
| /// Returns both square roots of `self` and a `Boolean` flag, which is set iff `self` is not a square. | |
| /// Returns both square roots of `self` and a `Boolean` flag, which is set iff `self` is not a square. | |
| /// The roots are returned in the order specified below by this function, | |
| /// but the generated constraints do not impose an order | |
| /// (this is where the `nondeterministic` part of this function name refers to). |
howardwu
changed the title
This resolves the underconstraining bug that was found in that circuit.
The fix involves the creation of two new circuits, which are more general and may have other uses:
The new circuit for cast lossy field to group is realized by using the latter circuit to attempt to find the point in the subgroup with the given value as x coordinate. If none exists, we return the generator if the input is 0, otherwise the result of Elligator-2 is returned, which is always a subgroup point.
The use of the new circuits for flagged operations eliminate the underconstraining without eliminating desired solutions (which would happen by enforcing constraints without taking flags into account).
This PR is draft because I still need to add tests for the two new circuits, but the implementation can be already reviewed.