Incorrect Padding for Descending Permutation Sorts

[DavePearce]

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]

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]

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:

• (Delta Sign). The problem is, we can't using inverse (i.e. appending) padding for the delta column. Since this currently ranges over both positive and negative signed columns, its only logical to pad at the front. But, this breaks with inverse padding.

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.