correct assertion for secp256k1_fe_mul_inner

[roconnor-blockstream]

Based on the surrounding asserts, 112 bits before this line, and 61 bits after this line, this assertion should be 113 bits. Notably the commensurate line in secp256k1_fe_sqr_inner is correctly assert to be 113 bits.

[real-or-random]

utACK 8e2a5fe This computes c += u0 * (R << 4), where u0 is 56 bits, (R >> 4) is 33 bits, therefore u0 * (R << 4) is 89 bits, and c before the assignment was 112 bits, so c after the assignment is at most 113 bits

[roconnor-blockstream]

Added a few more changes to make the VERIFY_BITS checks in secp256k1_fe_mul_inner to match the corresponding checks in secp256k1_fe_sqr_inner.

[real-or-random]

utACK dcdda31

8e2a5fe: This computes c += u0 * (R << 4), where u0 is 56 bits, (R >> 4) is 33 bits, therefore u0 * (R << 4) is 89 bits, and c before the assignment was 112 bits, so c after the assignment is at most 113 bits
dcdda31: We're adding values of bit sizes (64, 108, 112, 112, 108). Combining as (((64, 108), 112), (112, 108)) yields ((109, 112), (112, 108)), then (113, 113), and then 114.

[real-or-random]

@roconnor-blockstream When you say that you integrated this PR in your formal verification efforts, I assume this means that the proven statement includes the guarantee that these assertions hold?

[roconnor-blockstream]

yes (under the preconditions I give for my specification).

[roconnor-blockstream]

untested-but-formally-verified-ACK

[real-or-random]

ACK dcdda31 tested with asm disabled