Fixed CS for ECPAIRING
#620
Conversation
| (begin | ||
| (if-not-zero IS_ECPAIRING_DATA (eq! CS_ECPAIRING ACCPC)) | ||
| (if-not-zero IS_ECPAIRING_RESULT (eq! CS_ECPAIRING (* SUCCESS_BIT (- 1 TRIVIAL_PAIRING)))) | ||
| (if-zero (is_ecpairing) (vanishes! CS_ECPAIRING)) |
There was a problem hiding this comment.
I don't know if this is already the case in the definition but we should (force-bool (is_ecpairing)) at some point.
There was a problem hiding this comment.
Should we turn
(defun (is_ecpairing)
(+ IS_ECPAIRING_DATA IS_ECPAIRING_RESULT))
into
(defun (is_ecpairing)
(force-bool (+ IS_ECPAIRING_DATA IS_ECPAIRING_RESULT)))
?
| @@ -735,7 +739,12 @@ | |||
| (eq! CS_ECMUL (* ICP (is_ecmul)))) | |||
|
|
|||
| (defconstraint ecpairing-circuit-selector () | |||
| (eq! CS_ECPAIRING ACCPC)) | |||
There was a problem hiding this comment.
I'm confused why this constraint didn't blow up in the past. Don't we constrain ACCPC to be zero when it's not pairing data ?
There was a problem hiding this comment.
For me ACCPC was about acceptable pairs of points for the pairing circuit, at least that's what I remember the acronym to mean from yesterday's discussion @lorenzogentile404.
There was a problem hiding this comment.
I believe it was not blowing up as it was underconstrained. That is, along pairing data it was correctly forced to be 1 for acceptable pairs. However, along pairing result rows, when SUCCESS_BIT was 1, ACCPC could have been anything.
There was a problem hiding this comment.
This is what we had, and actually still have.
There was a problem hiding this comment.
Shouldn't it be the case that ACCPC can only be nonzero along is_ecpairing_data ?
No description provided.