Optimising Zero Checks

[DavePearce]

Optimising zero checks is important, because these often result in an entirely new column being created. Example:

(if-zero X Y Z)

Gets broken down into:

(1 - (~ X)) * Y
X * Z

Here, (~ X) results in a new column. However, suppose X is known to be binary (i.e. either X=0 or X=1). Then we can avoid the normalisation step.

[DavePearce]

In addition, there are other situations when we can also avoid the normalisation step. Consider this variation:

(defcolumns (X :binary@prove) (Y :binary@prove) Z)
(defconstraint test () (if-zero (+ X Y) Z))

Again, this would compile down to the constraint:

(1 - ~(X+Y)) * Z

This might seem more problematic, since X+Y can have any of three values: 0, 1 or 2. We can still encode this:

(1 - (X+Y) - (X*Y)) * Z

This works for two columns without needed an additional inverse.