Consensys / corset

13 stars 13 forks source link

Inefficient Handling of Sorted Permutations? #199

Open DavePearce opened 4 months ago

DavePearce commented 4 months ago

There is something that struck me looking at the documentation for Corset. Specifically, this example:

(defpermutation (A' B' C') ((↓ A) (↑ B) C))

Where the documentation says:

Here, A', B', and C' are defined as a sorted permutation of the columns A, B, and C, in increasing order of A values, then in decreasing order of B values, and independently of C values.

In fact it seems that, for columns which are not given a sign (e.g. C above), Corset defaults to giving the a positive sign. As such, it then generates constraints to enforce this using deltas. It seems that some of those constraints may be unnecessary. Of course the delta column will always exist, but some of the other columns presumably don't need to?

delehef commented 4 months ago

It seems that some of those constraints may be unnecessary.

IIUC, not enforcing the constraints on the delat would mean that the column C may be re-ordered in whatever fashion; which is probably not the behavior expected by the user.

One could remove the default-to-positive and enforce an explicit sorting criterion for each and every column, but I don't think that no criterion at all would be a good thing.