Consensys/corset

Optimise Spillage Computation

Opened this issue · 1 comments

(see also #139 and #151)

Currently more spillage is being requested than necessary. For example, in this case:

(defconstraint test1 () (eq! A (next B)))

The tool is reporting a spillage value of 1 because we have a positive shift. However, since padding is only ever added at the beginning of a trace, it is only negative shifts that require spillage (see #139 for details on how to fix this).

In addition, its not clear to me that the above example requires any spillage at all. Spillage seems to me to only be required for computed columns. Therefore, we could report the required spillage for the above as 0. However, its unclear to me exactly how best to implement this optimisation. Presumably, we could do the spillage calculation just on computed columns for example.

Spillage seems to me to only be required for computed columns.

Basically, yes.