correct assertion for secp256k1_fe_mul_inner #1438

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.

utACK https://github.com/bitcoin-core/secp256k1/pull/1438/commits/8e2a5fe908faa2ad0b847b3e5c42662614c8fa88 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

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.

utACK dcdda31f2cda13839a4285d8601118c041b18c13

8e2a5fe908faa2ad0b847b3e5c42662614c8fa88: 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 dcdda31f2cda13839a4285d8601118c041b18c13: 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.

@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?

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

untested-but-formally-verified-ACK

ACK dcdda31f2cda13839a4285d8601118c041b18c13 tested with asm disabled