correct assertion for secp256k1_fe_mul_inner #1438
pull roconnor-blockstream wants to merge 2 commits into bitcoin-core:master from roconnor-blockstream:patch-6 changing 1 files +3 −3-
roconnor-blockstream commented at 10:41 pm on November 6, 2023: contributorBased 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.
-
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.
-
real-or-random approved
-
real-or-random commented at 9:59 am on November 7, 2023: contributorutACK https://github.com/bitcoin-core/secp256k1/pull/1438/commits/8e2a5fe908faa2ad0b847b3e5c42662614c8fa88 This computes
c += u0 * (R << 4)
, whereu0
is 56 bits,(R >> 4)
is 33 bits, thereforeu0 * (R << 4)
is 89 bits, andc
before the assignment was 112 bits, soc
after the assignment is at most 113 bits -
roconnor-blockstream cross-referenced this on Nov 7, 2023 from issue Extra validation on top of #73 by sipa
-
real-or-random added the label assurance on Nov 13, 2023
-
real-or-random added the label refactor/smell on Nov 13, 2023
-
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.
-
roconnor-blockstream commented at 5:10 pm on November 14, 2023: contributorAdded a few more changes to make the
VERIFY_BITS
checks insecp256k1_fe_mul_inner
to match the corresponding checks insecp256k1_fe_sqr_inner
. -
real-or-random commented at 9:05 am on November 16, 2023: contributor
utACK dcdda31f2cda13839a4285d8601118c041b18c13
8e2a5fe908faa2ad0b847b3e5c42662614c8fa88: This computes
c += u0 * (R << 4)
, whereu0
is 56 bits,(R >> 4)
is 33 bits, thereforeu0 * (R << 4)
is 89 bits, andc
before the assignment was 112 bits, soc
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 cross-referenced this on Nov 21, 2023 from issue Replace the 64-bit C field implementation by fiat-crypto output by dderjoel
-
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?
-
roconnor-blockstream commented at 4:40 pm on November 24, 2023: contributoryes (under the preconditions I give for my specification).
-
roconnor-blockstream commented at 4:45 pm on November 24, 2023: contributoruntested-but-formally-verified-ACK
-
real-or-random approved
-
real-or-random commented at 8:44 am on November 27, 2023: contributorACK dcdda31f2cda13839a4285d8601118c041b18c13 tested with asm disabled
-
real-or-random merged this on Nov 27, 2023
-
real-or-random closed this on Nov 27, 2023
-
roconnor-blockstream deleted the branch on Nov 27, 2023
github-metadata-mirror
This is a metadata mirror of the GitHub repository bitcoin-core/secp256k1. This site is not affiliated with GitHub. Content is generated from a GitHub metadata backup.
generated: 2024-10-30 03:15 UTC
This is a metadata mirror of the GitHub repository bitcoin-core/secp256k1. This site is not affiliated with GitHub. Content is generated from a GitHub metadata backup.
generated: 2024-10-30 03:15 UTC
This site is hosted by @0xB10C
More mirrored repositories can be found on mirror.b10c.me
More mirrored repositories can be found on mirror.b10c.me