## Algorithm Details for Ecne

The algorithm begins by finding instances of the trusted functions inside the input R1CS file, which allows us to turn the R1CS into _special constraints_ and _reduced constraints_. The reduced constraints are still in R1CS form (e.g. $z = x * y$, whereas the special constraints are in function form (i.e. $y_3 = f(y_1, y_2)$)

Then, we apply a series of rules to the reduced constraints, and the special constraints whenever appropriate as well. The rules on reduced constraints are as follows. Remember that we are working over a finite field!

- (Rule 1) If $cx = <unique>$, and $c \neq 0$ is a constant, then $x$ is also uniquely determined.
- (Rule 2a) If $(x-a) * (x-b) = 0$, then $x = [a, b]$. Namely, if $\{a,b\} = \{0,1\}$, then $0 \le x \le 1$ as well.
- (Rule 2b) If $a*x + b = 0$, then $x = -b/a$.
- (Rule 3) If $z = 2^0 x_0 + 2^1 x_1 + \ldots + 2^n x_n$, and $x_0, x_1, ... x_n$ are all in $[0,1]$, then $z \in [0, 2^{n+1}]$. Furthermore, if $z$ is uniquely determined, so are $x_0, x_1, ... x_n$.
- (Rule 4a) If $x = y$, then all properties from $x$ are copied to $y$.
- (Rule 4b) If $1 = x + y$, and $x \in [0,1]$ (or $y \in [0,1]$), then the other variable is also in $[0,1]$. Furthermore, if $x$ is uniquely determined, $y$ is uniquely determined as well.
- (Rule 5) If $z = x_0 + a_1 x_1 + \ldots + a_n x_n$, and $a_i \mid a_{i+1}$, and $x_i < a_{i+1} / a_i$ (and $x_n$ is less than $p / a_n - 1$, where $p$ is the prime of the finite field), then one can bound $z$ similarly to Rule 3, and if $z$ is uniquely determined, then $x_0, x_1, ... x_n$ are also uniquely determined.
- (Rule 6) This is a rule called the AllButOneZero rule, and considers groups of variables, all but at most one of which are zero. It's best illustrated with an example. If $y_1$ is uniquely determined, and
$x_1 * y_1 = 0$
$x_2 * (y_1 - 1) = 0$
$x_3 * (y_1 - 2) = 0$
$x_1 + x_2 + x_3 = z$
Then assuming that $z$ is uniquely determined as well, we can uniquely determine $x_1, x_2, x_3$.
- (Rule 7) If $Ax = b$, where $A$ is a constant square matrix with nonzero determinant, and $b$ is a uniquely determined vector, then $x$ is uniquely determined as well.

These deduction rules are implemented by maintaining information on each variable in the `VariableState` object.