Find a better approach for the ZK determinism problem

[lvella]

Each output in a ZK circuit is represented by 2 variables even and odd. To test for determinism, we assemble the following polynomial that can't be satisfied if any even is different from its corresponding odd (a is a newly introduced variable):

(a[0]*(even[0] - odd[0]) - 1) * (a[1]*(even[1] - odd[1]) - 1) * ... * (a[n-1]*(even[n-1] - odd[n-1]) - 1) = 0

The obvious problem with this approach is that the number of terms in this polynomial grows exponentially with n, making it impractical for anything with more than a few outputs.

This encoding must obviously be fixed. The way Picus does it is that the solver is executed n times, one time for each output variable. Maybe there is a better way, I can think of some alternatives, like:

• running for 2 or 3 output variables at a time;
• doing a full GB without the different output constraints, and checking if each (even[i] - odd[i]) individually belongs to the radical ideal;
• maybe it is feasible to split the huge polynomial above into n+1 small polynomials, one for each output: a[i]*(even[i] - odd[i]) - b[i], and one multiplying all b[i] together (we would still have a very high degree polynomial). I think polynomial b[0]*b[1]*...*b[n-1] can only be zero if at least one even[i] != odd[i].

[lvella]

Another idea is to build a tree of degree 2 polynomials.

[lvella]

In branch parallel_or I fixed this using the first idea: running for a few output variables at a time. I also went further and ran them in parallel, over different processes. Now I believe this is a very silly idea, and would prefer to test each set of output variables sequentially, and save parallelism for issue #12.