Find and replace functions that compute "are all equal zero"

[chriseth]

Searches the constraints to find a set of input columns and one output column such that (semantically, not syntactically), the ouput is zero if and only if all the inputs are zero (and output is one otherwise). Then it tries to replace the involved constraints and auxiliary columns by a better version of that function.

[chriseth]

The code starting here should be equivalent to

a_is_zero * a = 0;
a_is_zero = 1 - a_inv * a;
b_is_zero * b = 0;
b_is_zero = 1 - b_inv * b;
c_is_zero * c = 0;
c_is_zero = 1 - c_inv * c;
d_is_zero * d = 0;
d_is_zero = 1 - d_inv * d;

cmp_result_0 = a_is_zero * b_is_zero * c_is_zero * d_is_zero;
cmp_result_0 * (1 - cmp_result_0) = 0;

(where a corresponds to b__0_0, b corresponds to b__1_0 etc.)

these are 13 columns, while the present code also has 13 columns, but performs two bitwise lookups.

[chriseth]

If we allow two bitwise lookups, we get

// Bus 6 (BITWISE_LOOKUP)
mult=is_valid, args=[a, b, ab, 0, 1]
mult=is_valid, args=[c, d, cd, 0, 1]

ab_is_zero * ab = 0;
ab_is_zero = 1 - ab_inv * ab;
cd_is_zero * cd = 0;
cd_is_zero = 1 - cd_inv * cd;

result = ab_is_zero * cd_is_zero;
result * (1 - result) = 0;

Which has only 11 columns. Adding another bitwise lookup we get to

mult=is_valid, args=[a, b, ab, 0, 1]
mult=is_valid, args=[c, d, cd, 0, 1]
mult=is_valid, args=[abcd, ab, cd, 0, 1]
result * abcd = 0;
result = 1 - abcd_inv * abcd;

which only has 9 columns.

Maybe it also makes sense to subtract 5 from the columns (4 inputs, one output), because those will likely be consumed by the preceding and following instructions. Then we would have

two lookups: from 8 to 6
three lookups: from 8 to 4

[chriseth]

Actually it's even simpler.
We know that 0 <= a, b, c, d <= 255. Because of that, if we define x = a + b + c + d, then 0 <= x <= 0x3fc which is less than half the modulus. This means that x is zero if and only if all of a, b, c, d are zero.

Now the system reads:

x = a + b + c + d
result * x = 0
result = 1 - x_inv * x

Of course, we can always inline x, and thus we have only one additional column, zero lookups and 6 columns in total.

[chriseth]

The slight problem here is that we might need witgen for x_inv.

[chriseth]

Now on to how to detect that we indeed are working with an "is equal zero" condition. Let's try to detect the pattern.

Property we want to check:

1. if b__*_0 are all zero, then cmp_result must be one.
2. if cmp_result is one, then all b__*_0 must be zero.
3. cmp_result is either one or zero.

The third property is easy to check. Once we have that, we can see if setting all b__*_0 to zero and cmp_result to zero leads to a contradiction and this establishes 1). The second could be more tricky to check.

[chriseth]

TODO: Check that with byte range constraints we can infer

-((b__3_0 - b_msb_f_0) * (b__3_0 - b_msb_f_0 - 256)) = 0
=> b__3_0 = b_msb_f_0   OR b__3_0 = b_msb_f_0 + 256, but the latter cannot happen due to range constraints
=> b__3_0 = b_msb_f_0

[chriseth]

Strategy: For every boolean column (we hope it is "result", let's call it result for now), we check the following:

Does setting it to one value (result = v) imply that some other columns have to be zero? Let cols be those columns. Then check if the converse holds: set cols all to zero and set result = 1 - v. If we get a contradiction, we know that result = v if and only if all of cols are zero. This means we have a way to compute result from those columns.

Now the goal is to find a better constraint system that encodes the same function.

First, we try to reduce the number of inputs variables: For every variable v in cols, tentatively remove it from the set, set all remaining variables to zero and set result = 1- v and try to get a contradiction. If we still get a contradiction, this variable is redundant, we can remove it from the set. At the end, we arrive at a non-redundant set of variables we call inputs and a set of variables we call redundant, with the following property: result = v implies inputs = 0, redudant = 0 and inputs = 0 implies result = v.

[chriseth]

These four constraints are actually equivalent to the one in line 26 and the reason is quite interesting - we could turn this into an optimization step:
Because of line 21, the first factor in the four constraints is binary. The second factors are byte-constrained because they are read from memory. This means each of the expression in the four constraints are byte range constrained. Now the interesting observation is that x = 0, y = 0 is equivalent to x + y = 0 if x and y are non-negative and the sum does not wrap. So we can turn the set of these four constraints into a single constraint by adding them, and we arrive exactly at the constraint in line 26.

Note that the observation that we can use a sum to express a conjunction is actually used by this "check equal zero" optimization step as well. So we could maybe split it into two steps, with the advantage that it would also work in case the values are not byte-constrained (which is the case for "check equal X" for some other constant X, because there the values are essentially y - X, and thus they can get negative)

[Schaeff]

Can we use the fact that x = 0, y = 0 is equivalent to x**2 + y**2 if the sum doesnt wrap (with no condition on x and y being non negative)?

[chriseth]

For that we also need that the squares do not wrap and especially the result would not be equivalent to the constraint in line 26. Or did you have something else in mind?

[chriseth]

Here we have another chance of optimization: We have two binary-constrained inputs to the bitwise lookup, we can just do that with a single algebraic constraint.

[chriseth]

Oh wow, this one is redundant as well, isn't it?

[chriseth]

These should be removed by #3012

[leonardoalt]

Tests failing

[chriseth]

This now fails after the bus interaction var refactoring because we now have

b__0_0 - BusInteractionField(5, 4) = 0
b__0_0 - BusInteractionField(6, 4) = 0

And we remove b__0_0 because it determined to be an inner variable. The bus interaction field variables are the register receives and sends. Since we delete b__0_0, the connection is lost.

[chriseth]

Furthermore, we determine the inputs to be the 8 bus interaction variables, not just 4. So this is an example of "the constraints further restrict the inputs".

[chriseth]

It at least contains v so I think this can be removed again.

[Schaeff]

clippy is failing

[georgwiese]

Cool! I'll have to have another look tomorrow (got through half of equal_zero_cheks.rs, until the end of try_replace_equal_zero_check).

High-level, the questions I have so far:

• Did you consider running this only on the instruction circuits (with PC lookup variables bound to the right values)? I feel like this could reduce complexity, increase efficiency and yield the same results.
• What is the performance impact of this?

[georgwiese]

I don't understand the second sentence.

[chriseth]

Tried to say it differently.

[georgwiese]

I think these should be in openvm/tests/apc_builder_pseudo_instructions.rs?

[georgwiese]

Could we receive a name here, and use it instead of "new_var"? Would make it easier to read the snapshots.

[chriseth]

What do you mean? A name that depends on the other names? Are you proposing to make it a variant of the output variable?

[georgwiese]

I mean changing it to

    let mut new_var = |name| {
        let id = var_allocator.issue_next_poly_id();
        AlgebraicReference {
            name: format!("{name}_{id}").into(),
            id,
        }
    };

and calling it as new_var("sum_inv"). This way we wouldn't have column names like new_var_29 in the snapshots.

[georgwiese]

Could be a constant

[georgwiese]

This block could be extracted into a function.

[georgwiese]

I think by definition of variables_to_remove, the bus interactions removed here are guaranteed to be stateless, right? Maybe we can add an assertion?

[georgwiese]

Would it make sense to split try_replace_equal_zero_check (which is quite long) into try_find_equal_zero_subcircuit and replace_equal_zero_subcircuit?

[georgwiese]

Do we expect this to happen? Or is this a sanity check?

[chriseth]

Yes, this is important.

[georgwiese]

Cool! Looking at the second half, I'm wondering the same thing as yesterday: Do we need check_redundancy? It is a significant amount of code (including is_satisfiable, which is only called from there) and seems a bit ad-hoc. If it is just a sanity check, I'd propose moving it to a separate module (indicating that this code is not essential for soundness) and asserting that it always returns true, instead of silently failing.

[georgwiese]

Please add to the docstring that we assume that inputs are nonzero and can be summed without overflow. Maybe also worth asserting this again here?

[ShuangWu121]

Suggested change

	value: T,
	binary_value: T,

It looks a bit more descriptive to me.

[ShuangWu121]

Does this function solve all the unknown variables in the system, or only some of them?

[chriseth]

It runs the solver, whatever it will determine it will return. But note that the solver has run before on that system, so it will usually only return results that can be obtained given the new assignments.

[ShuangWu121]

I found this name a bit confusing at first — I initially thought it meant the reachable variables excluding the blocking ones, but then I realized it actually includes reachable blocking variables and just stops the search from continuing through them. Just wanted to mention this in case others might read it the same way.

[chriseth]

@georgwiese yes, check_redundancy is vital. Otherwise we might remove more constraints than we want to. What could happen is that the constraints we remove restrict the set of possible inputs. I think we should talk about that in person because I also feel that there still might be a bug in the code wrt that.