Optionally output circuit to solve with Z3 theorem prover

[jonasnick]

Based on #2.

Initially I imagined that if the solver could find a solution quickly if we remove any single constraint, but doesn't find a solution with all constraints, then this would at least give some indication that the circuit does something right.

On my laptop, Z3 can solve just fine as long as there are fewer than 600 constraints. Beyond that, the memory requirements grow quickly (and I didn't give it a lot of time). But perhaps this is worth investigating in the future.

[jonasnick]

Using Z3 with a smaller curve (P = 47, N1 = 59, N2 = 37) I verified (see See https://github.com/sipa/purify/commit/d195ee1522e63c375fa9da001e60f0d8a76d0187) that

1. There is no valid wire assignment with a different output
2. Any valid wire assignment must include a representation of the dlogs of U1 and U2 or their negation in the first wires

I didn't work with a much smaller curve because the incomplete addition formula does not seem to be applicable (getting division by 0 with P <= 13).

[real-or-random]

Using Z3 with a smaller curve (P = 47, N1 = 59, N2 = 37) I verified (see See d195ee1) that

1. There is no valid wire assignment with a different output

2. Any valid wire assignment must include a representation of the dlogs of `U1` and `U2` or their negation in the first wires

That's crazy shit! We should add this to the paper. :)

I didn't work with a much smaller curve because the incomplete addition formula does not seem to be applicable (getting division by 0 with P <= 13).

Hm, can you elaborate? At least as how I understand it, we should never hit the missing cases in the addition, and I don't see how this depends on the size of the curve. (And if it does, maybe we forgot to state an assumption in the paper.)

[jonasnick]

Hm, can you elaborate?

I'm assuming that's because the order is too small for the "recipe" in section 5.1 of the paper. Perhaps @sipa knows more.

[sipa]

I would suspect that it works for any curve. If there is a problem, it may be that the python code I wrote makes some implicit assumptions.

[real-or-random]

Random thought: What can indeed happen is that one of the precomputed points in the lookup table in the circuit is infinity. That should not be an issue in practice since this will be caught already when building the circuit, and it happens only with negligible probability (at least on honest inputs). But I don't think we talk about this case in the paper currently.

[sipa]

@real-or-random That can't be it, the elements in the lookup table are multiples of the input point; as the group size is prime, the only way to obtain infinity from a multiplication is when either the input point is infinity (guaranteed by the hash-to-curve not to be the case), or the scalar is a multiple of the group order (guaranteed not to be the case as we simply only build a table up to N/2).

I looked into it a bit more, and it seems it's mostly an issue with the circuit code in purify.py. It'd try to build an "addition where we only care about the X coordinate output" for the last table lookup, except there was only a single table lookup for such small curves, resulting in nothing to add up. I've pushed a fix.