Witgen: Can't reason about range constraints on expressions

[georgwiese]

Consider this example:

namespace main(4);
    // Two bit-constrained witness columns
    // In practice, bit1 is always one (but this is not constrained)
    col witness bit1(i) query Query::Hint(1);
    col witness bit2;
    bit1 * (bit1 - 1) = 0;
    bit2 * (bit2 - 1) = 0;

    // Constrain their sum to be binary as well.
    // This ensures that at most one of the two bits is set.
    // Therefore, bit2 is always zero.
    let bit_sum = bit1 + bit2;
    bit_sum * (bit_sum - 1) = 0;

    // Some witness that depends on bit2.
    col witness foo;
    foo = bit2 * 42 + (1 - bit2) * 43;

Given that bit1 = 1 is set via a hint, the witness should be fully determined:

• Because bit2 and bit_sum are binary, bit2 must be zero
• bit2 uniquely determines foo

However, because bit_sum is just an expression, the binary range constraint is not stored with it, and witgen never figures out bit2.

To work around this, we can materialize bit_sum. The following works:

    let bit_sum;
    bit_sum * (bit_sum - 1) = 0;

[georgwiese]

The following works

This is true after #2120.