Consensys / corset

15 stars 13 forks source link

Incorrect Padding for Descending Permutation Sorts #198

Open DavePearce opened 5 months ago

DavePearce commented 5 months ago

Minimal example to recreate:

(module m1)
(defcolumns X)
(defpermutation (Y) ((- X)))

With this example trace:

{ "m1": { "X": [123] } }

Then, running corset compute --trace test.json --out test.out test.lisp gives this:

{"columns":{
"m1.Y":{
"values":["0x0123","0x00"],
"padding_strategy": {"action": "prepend", "value": "123"}
}
,"m1.X":{
"values":["0x00","0x0123"],
"padding_strategy": {"action": "prepend", "value": "0"}
}
...

This does not look right to me. Specifically, the padding_strategy for Y will mean it is no longer a permutation of X. The logical option here is to have an append padding strategy, but I'm unsure whether or not this is permissible.

@OlivierBBB FYI

DavePearce commented 5 months ago

This is less of a problem when the first column of a permutation is positively signed. For example, something like this:

(module m1)
(defcolumns A B)
(defpermutation (X Y) ((+ A) (- B)))

Then for a trace like this:

{ "m1": { "A": [1,1,2,3], "B": [40,56,65,90] } }

This is accepted correctly because a spillage value of 0 for A ensures we can accept a padded trace like this:

{ "m1": { "A": [0,0,1,1,2,3], "B": [0,0,40,56,65,90] } }

However, we can still construct a problematic trace such as:

{ "m1": { "A": [0,0,0,0], "B": [40,56,65,90] } }

Here, again, we are given an incorrect spillage value for B.

DavePearce commented 5 months ago

The logical option here is to have an append padding strategy, but I'm unsure whether or not this is permissible.

Some updates on this point specifically. Yes, we can choose to append at the end or the beginning (let's call this the padding sign of a column). However, I did not make this work for permutation sorts. Specifically, at a minimum because of this:

The easiest solution then is to enforce a requirement that we must have a leftmost positively signed column for a permutation sort and, furthermore, no trace prior to expansion can have 0 for that column.

Overall, my feeling is that it actually would just make sense to remove sorting direction altogether. That way, there is no confusion.