Open DavePearce opened 3 months ago
(see #183)
This is an inefficiency, but I have labelled it as a bug here as it really should be fixed. Consider:
(module test) (defcolumns (P :binary@prove)) (defperspective p1 P ((A :binary@prove))) (defperspective p2 P ((B :binary)))
Here, a single binary constraint is given for the underlying column:
test.B-binarity := col#3 * (1 - col#3)
Now consider this:
(module test) (defcolumns (P :binary@prove)) (defperspective p1 P ((A :binary@prove))) (defperspective p2 P ((B :binary@prove)))
In this case, we get two binarity constraints:
test.A-binarity := col#2 * (1 - col#2) test.B-binarity := col#3 * (1 - col#3)
Which we can see in the final define.go are really generated:
define.go
test__A_xor_B := build.RegisterCommit("test.A_xor_B", build.Settings.Traces.Test) test__A_xor_B := build.RegisterCommit("test.A_xor_B", build.Settings.Traces.Test) test__P1 := build.RegisterCommit("test.P1", build.Settings.Traces.Test) test__P2 := build.RegisterCommit("test.P2", build.Settings.Traces.Test) // // Constraints // build.GlobalConstraint("test.A-binarity", test__A_xor_B.AsVariable().Mul(symbolic.NewConstant("1").Sub(test__A_xor_B.AsVariable()))) build.GlobalConstraint("test.B-binarity", test__A_xor_B.AsVariable().Mul(symbolic.NewConstant("1").Sub(test__A_xor_B.AsVariable()))) build.GlobalConstraint("test.P1-binarity", test__P1.AsVariable().Mul(symbolic.NewConstant("1").Sub(test__P1.AsVariable()))) build.GlobalConstraint("test.P2-binarity", test__P2.AsVariable().Mul(symbolic.NewConstant("1").Sub(test__P2.AsVariable()))) build.GlobalConstraint("test.c1", test__P1.AsVariable().Mul(test__A_xor_B.AsVariable().Sub(symbolic.NewConstant("10"))))
Probably the same as #186
Hmmm, this is actually quite tricky to implement correctly.
(see #183)
This is an inefficiency, but I have labelled it as a bug here as it really should be fixed. Consider:
Here, a single binary constraint is given for the underlying column:
Now consider this:
In this case, we get two binarity constraints:
Which we can see in the final
define.go
are really generated: