Add constraints

[effectfully]

We want to be able to impose various invariants like "an external variable v can't be zero". Perhaps the best way to do this is to have a grammar like this:

Partially implemented in d662c72c3cf610d75533581cacb6c20b395249e0. Currently we only support equality constraints over field elements. The grammar is

i = j; <expr>

There is a problem, though. Consider

if i == 0 then 0 = i; 1 else 1

Here we check whether i is equal to 0 and if it is, then require it to be equal to 0 and return 1. And if i was not 0, then we simply return 1 without requiring anything. This makes perfect sense in this repo, but not downstream, because we do not have any branching downstream. Thus, whenever we enter a local scope, we should ban using constraints there.

Or we can compile 0 = i as

0 = i OR False = (i == 0)

(where OR is the same as or, but defined over constraints rather than boolean values). So we invert the performed check and add it to the constraint to ensure that regardless of how control flow goes, the constraint will be satisfied. This is weird and I don't think we can define OR over constraints, so we just should ban constraints in local scopes.

[effectfully]

In fact, we can probably handle constraints in local scopes actually. So consider

if i == 0 then 0 = i; 1 else 1

We can represent the constraint as

let b = i == 0;
0 * b = i * b

So whenever i is equal to 0 we get 0 = i and 0 = 0 otherwise (which is trivially satisfied).

[effectfully]

Range constraints (and any boolean expressions in general) were added in #28.