Save negations in var-time group addition #1056

I guess it does not matter but maybe use something like &data->gej[0].y as fe ensure we're not benchmarking with the same fe over and over?

Done.

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

    if (a->infinity) {
        [...]
        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).

Why is this branch inside this block 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

if (b->infinity) {
    r ->infinity = 1;
} else {
    r ->infinity = 0;
}

So the mapping then is

• (C) a->infinity && b->infinity -> (sage) branch == 0
• (C) a->infinity && !b->infinity -> (sage) branch == 1

When 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.

yes... edited my comment to fix.

Anyway, I forgot to make the corresponding change below for the --exhaustive version. But it doesn't matter as the fixup mentioned above reverts this change here.