Consensys / corset

4 stars 10 forks source link

Missing Binarity Constraints for Perspectives #101

Open DavePearce opened 1 month ago

DavePearce commented 1 month ago

Considering perspectives now. This is my test example:

(module test)
(defcolumns A (P :binary@prove))
(defperspective perp P ((B :binary@prove)))
(defconstraint test (:perspective perp) (vanishes! A))

This currently shows these constraints from corset debug -c --auto-constraints=nhood:

test.test :=
P * A

test.P-binarity :=
col#0 * (1 - col#0)

test.B-binarity :=
col#2 * (1 - col#2)

And for wizard-iop we get this:

build.GlobalConstraint("test.B-binarity", test__B.AsVariable().Mul(symbolic.NewConstant("1").Sub(test__B.AsVariable())))
build.GlobalConstraint("test.P-binarity", test__P.AsVariable().Mul(symbolic.NewConstant("1").Sub(test__P.AsVariable())))
build.GlobalConstraint("test.test", test__P.AsVariable().Mul(test__A.AsVariable()))

Which I translate as:

B * (1 - B)
P * (1 - P)
P * A