benchmark_internal shows about 2% speedup in each method as a result (64bit).
sage/prove_group_implementations.sage too?
ACK 66a412939351396a6351b062dff820989a63cc56
I re-derived these formulas by manipulating the sage code until it matches the forms in this PR, and then comparing the result with the C implementations.
244@@ -245,6 +245,15 @@ void bench_group_add_affine_var(void* arg, int iters) {
245 }
246 }
247
248+void bench_group_add_zinv_var(void* arg, int iters) {
249+ int i;
250+ bench_inv *data = (bench_inv*)arg;
251+
252+ for (i = 0; i < iters; i++) {
253+ secp256k1_gej_add_zinv_var(&data->gej[0], &data->gej[0], &data->ge[1], &data->fe[0]);
&data->gej[0].y as fe ensure we’re not benchmarking with the same fe over and over?
128 rx = b.X * bzinv2
129 ry = b.Y * bzinv3
130 rz = 1
131 return (constraints(), constraints(zero={b.Infinity : 'b_finite'}, nonzero={a.Infinity : 'a_infinite'}), jacobianpoint(rx, ry, rz))
132+ if branch == 0:
133+ return (constraints(), constraints(nonzero={b.Infinity : 'b_infinite'}), a)
Now that this conditional has been moved, the constraints are off. In the first return, we do not know that b is not infinity (but in the second, we know that a is not infinity, though that shouldn’t be required to prove the formula.) And then the prover finds a bug in the formula because there is no equivalent in the sage code for
0 if (a->infinity) {
1 [...]
2 r->infinity = b->infinity;
Here’s fixed sage code: https://github.com/real-or-random/secp256k1/commits/group_var
I assume the reason for checking b->infinity first was that this is faster if true, and I guess the likelihood of a or b being infinity is comparable. It’s probably not measurable but was there a performance reason for the reordering, or did you just change it because then it looks cleaner? If the latter, we may just leave it as it was.
It was just for consistency across the several methods, but on review ‘b’ is from a lookup table and should never actually be infinity in current usages. So as little as it matters, the check should come after checks that might actually happen (if we can’t just require it to be non-infinity anyway).
I’ve adopted your fixup for the sage script, thanks.
It was just for consistency across the several methods, but on review ‘b’ is from a lookup table and should never actually be infinity in current usages. So as little as it matters, the check should come after checks that might actually happen (if we can’t just require it to be non-infinity anyway).
We could VERIFY_CHECK it. But the branch can probably be predicted then, so I don’t think it hurts (and it’s certainly safer).
fixup! should be squashed but it’s probably also good to change the sage stuff in the same commit as the C code, then C and sage are always consistent.
123 bzinv3 = bzinv2 * bzinv
124 rx = b.X * bzinv2
125 ry = b.Y * bzinv3
126 rz = 1
127+ if branch == 0:
128+ return (constraints(), constraints(nonzero={a.Infinity : 'a_infinite', b.Infinity : 'b_infinite'}), point_at_infinity())
branch == 0 or branch == 1 and not just before? It doesn’t use any of the local variables. Also, why does it exist at all, given that there’s no corresponding branch in the C code?
This branch corresponds to https://github.com/bitcoin-core/secp256k1/blob/2d0e1154c1939e8e7ffb05f64faf3f626fcb7000/src/group_impl.h#L455 in the C code, which is equivalent to
0if (b->infinity) {
1 r ->infinity = 1;
2} else {
3 r ->infinity = 0;
4}
So the mapping then is
(C) a->infinity && b->infinity -> (sage) branch == 0(C) a->infinity && !b->infinity -> (sage) branch == 1When I wrote this I assumed that in sage, we need to write it as an explicit branch because we have no infinity field but instead point_at_infinity() and jacobianpoint(x, y, z) constructors. But now I see that it’s not entirely true. The constructor is actually jacobianpoint(x, y, z, infinity), so there’s a much simpler way that’s closer to the sage code, see the fixup comment at https://github.com/real-or-random/secp256k1/commits/group_var .
@peterdettman Can you pick that commit and squash again?
b ->infinity = 1
You mean r ->infinity = 0? Anyway, I see what you meant to represent with this branch. Your fixup looks good.
279@@ -288,7 +280,7 @@ if __name__ == "__main__":
280 success = True
281 success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_var", 0, 7, 5, formula_secp256k1_gej_add_var)
282 success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_ge_var", 0, 7, 5, formula_secp256k1_gej_add_ge_var)
283- success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_zinv_var", 0, 7, 5, formula_secp256k1_gej_add_zinv_var)
284+ success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_zinv_var", 0, 7, 6, formula_secp256k1_gej_add_zinv_var)
--exhaustive version. But it doesn’t matter as the fixup mentioned above reverts this change here.
- Updated _gej_add_var, _gej_add_ge_var, _gej_add_zinv_var
- 2 fewer _fe_negate in each method
- Updated operation counts and standardize layout
- Added internal benchmark for _gej_add_zinv_var
- Update sage files (fixed by Tim Ruffing)