Excessive Delta Constraints Generated for Permutation

[DavePearce]

This is not a bug, but more of an observation. Given this minimal test for a permutation:

(module test)
(defcolumns A)
(defpermutation (B) ((+ A)))

We end up with a large number of "delta" constraints. Specifically, these:

test.__SRT__Delta_bbe6c9-decomposition :=
__SRT__Delta_bbe6c9 - (1 * __SRT__Delta_0_bbe6c9 + 256 * __SRT__Delta_1_bbe6c9 + 65536 * __SRT__Delta_2_bbe6c9 + 16777216 * __SRT__Delta_3_bbe6c9 + ...)                                      

test.__SRT__Delta_0_bbe6c9-is-byte
__SRT__Delta_0_bbe6c9 < 256

test.__SRT__Delta_1_bbe6c9-is-byte
__SRT__Delta_1_bbe6c9 < 256

test.__SRT__Delta_2_bbe6c9-is-byte
__SRT__Delta_2_bbe6c9 < 256

test.__SRT__Delta_3_bbe6c9-is-byte
__SRT__Delta_3_bbe6c9 < 256

...

There are exactly 16 __SRT__DELTA_XX constraints. I understand that what we have here is a byte decomposition of a u128. But, for this particular example, its just overkill to have this many. Presumably for the intended ZK system, this hardcoded figure makes sense u128 values as often used. But, presumably they are not always. Furthermore, we don't even have a type for the column A so there is no need for a byte decomposition at all.

[DavePearce]

NOTE: __SRT__Delta_3_bbe6c9 < 256 indicates a range constraint.

[delehef]

The permutation proves that the produced columnset (here only one) is indeed sorted according to the given criterion. This implies to prove that the difference between each pair of successive elements in the sorted columns is positive (the other way around if we want descendingly sorted columns).

To this end, we create a xxx_Delta_xxx column, which for each row contains this difference. From there, it is required:

1. to prove that xxx_Delta_xxx is indeed positive everywhere, which is accomplished through a byte-decomposition (spawning the 16 xxx_Delta_i_xxx columns; this could be optimized by reducing the number of such columns as described in issue #7, but has not yet been done);
2. prove that each of these columns is indeed a byte, which is accomplished by the range constraint.

See with @OlivierBBB for the full details of the permutation argument, which is described somewhere in the spec :)

[DavePearce]

An example to illustrate:

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

This should only need one additional column for holding the difference between successive values of Y in the permutation, but currently generates 16 (of which 15 are guaranteed to hold 0).