feat: upgrade go corset to v11

[DavePearce]

No description provided.

[OlivierBBB]

I will say I find the usage of or unfamiliar but it works.

[DavePearce]

Hmmmm, we probably could write it so that it looks exactly like it does in the spec using three cases with the AND for the third case.

[OlivierBBB]

What is the idea behind converting constraints à la

(= X (+ Y (binary-value))

to

(if (binary-value)
    (= X (+ Y 1))
    (= X Y)
)

AFAICT this was done in hub/constraints/instruction-handling/halting/revert.lisp, too. The underlying constraint is different (though equivalent) and has a higher degree:

// old approach
0 = X - Y - (binary-value) // degree = max{ 1, degree (binary-value) }

// new approach
0 = (binary-value) * (X - Y - 1) + (1 - (binary-value)) * (X - Y) // degree = 1 +  degree (binary-value)

Also it deviates from the spec which may end up causing confusion in the future.

[DavePearce]

What is the idea behind converting constraints à la

The issue is to do with the structuring that go-corset imposes. It distinguishes "logical values" from general arithmetic values. For example, (== X 1) returns a logical value (of the bool type) where as say (+ X 1) returns an arithmetic value (of the int type). Constraints require logical values, as do if conditions. So you cannot write this:

(defcolumns (X :i16))
(defconstraint c1 () X)

Instead, you are forced to write this:

(defcolumns (X :i16))
(defconstraint c1 () (== X 0))

Likewise, you cannot mix logical and arithmetical values arbitrarily as you did before. So, you cannot do this:

(defconstraint c1 () (== X (== Y 1))

Because the operands of == are expected to be arithmetic values, not logical values.

Going back to the original constraint, the issue is that remained-constant! returns a logical value, and hence cannot be used in the position it was. So I refactored to avoid that.

Also it deviates from the spec which may end up causing confusion in the future.

Personally, I would suggest that the original presentation is much harder to understand and is a potential source of confusion itself. The logical presentation (whilst potentially less efficient) is much easy to read and follow. So, if it were me, I would just change the spec to match.

[DavePearce]

I should add that in theory go-corset could actually apply the optimisation itself when applicable. However, right now --- it does not.

[DavePearce]

And, the whole purpose of all this is to make explicit when equality is being used (as opposed to -) and, likewise, when logical or and logical and are being used (as opposed to * and +). That is, for field agnosticity.

[DavePearce]

Also, just to clarify. Isn't this the wrong way around:

(= X (+ Y (binary-value))

to

(if (binary-value)
    (= X (+ Y 1))
    (= X Y)
)

Here, when binary-value==0 we want (= X Y) ... right? Anyway, it does't matter as I get the point.

[DavePearce]

Also, just thinking about this comment:

0 = (binary-value) * (X - Y - 1) + (1 - (binary-value)) * (X - Y)

Firstly, see my slack message on linea-arithmetisation about how the original corset tool handles if.

Secondly, assuming we translate as above ... then this will multiply out and simplify when turned into a polynomial, meaning its identical. At least that would be my understanding. Something like this:

0 = bv * (X - Y - 1) + (1 - bv) * (X - Y)
==> bv.X - bv.Y - bv + X - Y - bv.X + bv.Y
==> X - Y - bv

[OlivierBBB]

then this will multiply out and simplify when turned into a polynomial, meaning its identical

This may be the case, I don't know whether corset does such algebraic manipulations under the hood. My assumption was that it doesn't, it just takes takes the constraint as is. We would certainly benefit from go-corset doing this expansion in this particular case.

[OlivierBBB]

So boolean / loobean is gone but we now have numerical and logical columns. I'm ok with that, especially if it simplifies FV work and allows us to talk with AND's and OR's etc ...

[DavePearce]

You got it --- its gone, but not quite gone ;)

[DavePearce]

This may be the case, I don't know whether corset does such algebraic manipulations under the hood.

Go-corset doesn't at the moment (though it could for sure), but I actually think the prover might do this already. They do a fair bit of work simplifying constraints.

[OlivierBBB]

LGTM but I'm confused as to a couple of changes mentioned in comments