Show Constraints Arising from `@prove` ?

[DavePearce]

(see also #91)

A question I'm unsure about is whether or not columns marked with @prove should generate additional constraints. For example:

(defcolumns (BIN :byte@prove))
(defconstraint eg2 () (vanishes! (- 1 BIN)))

Generates the following (according to corset debug):

eg2 :=
1 - BIN

Likewise, this generates the same constraints:

(defcolumns (BIN :binary@prove))
(defconstraint eg2 () (vanishes! (- 1 BIN)))

My understanding previously is that binary@prove should result in a specific binary constraint being added (e.g. BIN * (1-BIN)). Likewise, I assumed that byte@prove would result in a range constraint or a lookup. So, it seems odd that there is nothing being added in both cases above.

[DavePearce]

ALSO: check the effect of perspectives. Specifically, if B belongs to a perspective then B :binary@prove should generate something like P * B * (B - 1).

[DavePearce]

So, for the example above, looking at the generated go output from wizard-iop gives this:

func ZkEVMDefine(build *Builder) {
        //
        // Corset-computed columns
        //
        test__A := build.RegisterCommit("test.A", build.Settings.Traces.Test)
        test__B := build.RegisterCommit("test.B", build.Settings.Traces.Test)
        test__C := build.RegisterCommit("test.C", build.Settings.Traces.Test)

        //
        // Interleaved columns
        //

        //
        // Constraints
        //
        build.GlobalConstraint("test.A-binarity", test__A.AsVariable().Mul(symbolic.NewConstant("1").Sub(test__A.AsVariable())))
        build.GlobalConstraint("test.test2", symbolic.NewConstant("1").Sub(test__A.AsVariable()).Mul(test__B.AsVariable().Sub(test__C.AsVariable())))
}

So, this actually includes the binarity constraint as test.A-binarity.

[DavePearce]

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:

P * A

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

@OlivierBBB This is not what you are expecting, right?

[delehef]

Do not forget the --auto-constraints=nhood when calling corset debug to see the auto-generated type constraints.

[DavePearce]

Great, thanks --- that is what I was looking for. I'm going to close this now and split out a new issue around the perspective binarity constraints.