correct assertion for secp256k1_fe_mul_inner #1438

1. 
   roconnor-blockstream commented at 10:41 pm on November 6, 2023: contributor

   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.
2. correct assertion for secp256k1_fe_mul_inner

   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.

   8e2a5fe908
3. real-or-random approved
4. 
   real-or-random commented at 9:59 am on November 7, 2023: contributor

   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
5. roconnor-blockstream cross-referenced this on Nov 7, 2023 from issue Extra validation on top of #73 by sipa
6. real-or-random added the label assurance on Nov 13, 2023
7. real-or-random added the label refactor/smell on Nov 13, 2023
8. Tighten secp256k1_fe_mul_inner's VERIFY_BITS checks

   These changes bring the checks to the same values used at the corresponding positions in secp256k1_fe_sqr_inner.

   dcdda31f2c
9. 
   roconnor-blockstream commented at 5:10 pm on November 14, 2023: contributor

   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.
10. 
    real-or-random commented at 9:05 am on November 16, 2023: contributor

    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.

11. roconnor-blockstream cross-referenced this on Nov 21, 2023 from issue Replace the 64-bit C field implementation by fiat-crypto output by dderjoel
12. 
    real-or-random commented at 2:36 pm on November 24, 2023: contributor

    @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?
13. 
    roconnor-blockstream commented at 4:40 pm on November 24, 2023: contributor

    yes (under the preconditions I give for my specification).
14. 
    roconnor-blockstream commented at 4:45 pm on November 24, 2023: contributor

    untested-but-formally-verified-ACK
15. real-or-random approved
16. 
    real-or-random commented at 8:44 am on November 27, 2023: contributor

    ACK dcdda31f2cda13839a4285d8601118c041b18c13 tested with asm disabled
17. real-or-random merged this on Nov 27, 2023
18. real-or-random closed this on Nov 27, 2023

    ---

19. roconnor-blockstream deleted the branch on Nov 27, 2023

Contributors
roconnor-blockstream real-or-random

Labels
assurance refactor/smell