Inefficient Register Allocation

[DavePearce]

Consider an example like this:

(module test)
(defcolumns (P :binary@prove))
(defperspective p1 P ((A :i8)))
(defperspective p2 P ((B :i16)))

We can see the register allocation performed by Corset:

   0             test.P      𝟙   1                                       r0/test.Pι1
   1             test.p1/A   𝟠   1                                       r1/test.Aι1
   2             test.p2/B  i8   1                                       r2/test.Bι1

The key is that it will not allocate A and B to the same underlying column (i.e. register) because they nominally have different types. In fact, it is safe to do this because they are not being proven. However, there are flow on effects of allowing them to be allocated together: trace files need to use the maximum width of any column allocated to a register; the inspector will have to do the same.

Overall, its not clear to me whether or not this optimisation will add any significant value. But it is worth considering at least. Note also that i8@prove and byte@prove will not be allocated together either.

[DavePearce]

Another case of inefficiency is the following:

(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)

However, if we do this then we get something surprising:

(module test)
(defcolumns (P :binary@prove))
(defperspective p1 P ((A :binary@prove)))
(defperspective p2 P ((B :binary@prove)))

Then, 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 generated:

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"))))

[delehef]

Overall, its not clear to me whether or not this optimisation will add any significant value.

That was a design choice that was supposed to help with value validity checking while importing traces. When debugging safeguards will become less important than traces size, it will be the time to implement your proposition.

[DavePearce]

That was a design choice that was supposed to help with value validity checking while importing traces.

Yeah, overall now that I've dug through it and understand what's going on I think its working pretty well. I'm not sure we'll need much more optimisation. Its seems to be a lot of binary fields in particular which need to be allocated together, and as it currently works they should be!