Understanding Sorting Constraints

[DavePearce]

Here's my example:

(defcolumns X)
(defpermutation (Y) ((+ X)))

From this, we get a bunch of stuff:

X_intrld_Y
[Y] perm. [X]

__SRT__Eq_57cec4-is-binary :=
__SRT__Eq_57cec4 * (1 - __SRT__Eq_57cec4)

__SRT__at_0_57cec4-is-binary :=
__SRT__at_0_57cec4 * (1 - __SRT__at_0_57cec4)

__SRT__Delta_57cec4-decomposition :=
__SRT__Delta_57cec4 - (1 * __SRT__Delta_0_57cec4 + 256 * __SRT__Delta_1_57cec4 + 65536 * ...

__SRT__Delta_0_57cec4-is-byte
__SRT__Delta_0_57cec4 < 256

__SRT__Delta_1_57cec4-is-byte
__SRT__Delta_1_57cec4 < 256

...

__SRT__at_0_57cec4-0 :=
1 * (1 - __SRT__at_0_57cec4) * (Y - Y₋₁)

__SRT__at_0_57cec4-1 :=
1 * __SRT__at_0_57cec4 * (1 - (Y - Y₋₁) * C/INV[(- Y Y₋₁)])

Eq_@_57cec4 :=
1 - (__SRT__Eq_57cec4 + __SRT__at_0_57cec4)

__SRT__Eq_i_57cec4 :=
(1 - __SRT__Eq_57cec4) * (__SRT__Delta_57cec4 - 1 * __SRT__at_0_57cec4 * (Y - Y₋₁))

...

To better understand this, I'm going to simplify it by consider a restricted case where we are interested only in sorting 16bit columns. My translation is:

at_0 < 2
Eq < 2
Delta == (Delta_1 * 256) + Delta_0
Delta_0 < 256
Delta_1 < 256
if at_0 == 0 then Y[i] == Y[i-1]
if at_0 == 1 then (Y[i] - Y[i-1]) / (Y[i] - Y[i-1]) == 1
if Eq == 0 then Delta == at_0*(Y[i] - Y[i-1])
Eq + at_0 == 1

But, its not clear to me what the Eq and at_0 booleans are for? Seems like the Delta column is enough to ensure the sortedness constraint for Y. Also, seems that at_0 == (1 - Eq). And, I see that Eq==1 means Y[i] == Y[i-1] and Eq==0 means Y[i] != Y[i-1].

@delehef Any thoughts / comments on this?

[DavePearce]

Ideas:

• Maybe the goal of the Eq field is to enable a strict sorting where e.g. Eq is never 1 ?
• Or perhaps its related to the lexicographic ordering when we have a permutation constraint across multiple columns?

[DavePearce]

Ok, looks like the latter point may be the explanation. Let's examine a two column permutation, such as this:

(defcolumns (X :byte) (Y :byte))
(defpermutation (A B) ((+ X) Y))

Then, we get constraints roughly equivalent to this:

at_0 < 2
at_1 < 2
Eq < 2
Delta == (Delta_1 * 256) + Delta_0
Delta_0 < 256
Delta_1 < 256
if at_0 == 0 then A[i] == A[i-1]
if at_0 != 0 then (A[i] - A[i-1]) / (A[i] - A[i-1]) == 1
if at_0 == 0 && at_1 == 0 then B[i] == B[i-1]
if at_0 == 0 && at_1 != 0 then (B[i] - B[i-1]) / (B[i] - B[i-1]) == 1
if Eq == 0 then Delta == at_0*(A[i] - A[i-1]) + at_1*(B[i] - B[i-1])
Eq + at_0 + at_1 == 1

Hmmmmm, Ok I'm starting to get it now ... Delta is the difference between one of the available columns.

[DavePearce]

Seems like we can optimise e.g. this line:

if at_0 == 0 && at_1 == 0 then B[i] == B[i-1]

into this:

if Eq==1 then B[i] == B[i-1]

[DavePearce]

Here's a slightly more high-level translation of our example above:

at_0 : binary
at_1 : binary
Eq  : binary
Delta == (Delta_1 * 256) + Delta_0
Delta_0 < 256
Delta_1 < 256
if at_0 == 0 then A[i] == A[i-1] else A[i] != A[i-1]
if at_1 == 0 then B[i] == B[i-1] else B[i] != B[i-1]
if Eq == 0 then (Delta == A[i] - A[i-1])) || (Delta == B[i] - B[i-1])
Eq + at_0 + at_1 == 1

A sensible property here is that Eq == 0 ==> Delta != 0.

[delehef]

Yep, I think you got it. You should really raise the issue here with @OlivierBBB, he designed the system.

W.r.t. reducing the number of @ columns for e.g. byte columns, I believe you can only do it if you prove somewhere that the underlying column values will never consume more bytes than the number of @ columns, otherwise you may open yourself to attacks where the highest part of the values is not taken into account in the sort verification.

[DavePearce]

@delehef Thanks! Interesting comment regarding the number of columns. I suppose for a byte@prove column that is straightforward. Otherwise, we have to be sure (e.g. verify it :)

[DavePearce]

Also, on a separate note, I guess that wrap around for the BLS12_377 can occur if we are multiplying two 128 bit values because that can potentially require 256 bits of space (but we have, what, 254 bits?).