Extra validation on top of #73 #103
pull sipa wants to merge 4 commits into bitcoin-core:master from sipa:opt-mul-sqr changing 2 files +854 −334-
sipa commented at 3:53 pm on November 13, 2014: contributor
-
Rewrite mul/sqr for 32bit/64bit
- interleave calculation of the lower and upper partial product ranges, and reduction - less registers needed, more opportunities for parallel ops
-
Add equalities relating input and output variables fa0d620668
-
Add overflow analysis to field_5x52_int128_impl.h a51859871a
-
sipa renamed this:
Extra '
Extra validation on top of #73
on Nov 13, 2014 -
gmaxwell commented at 8:33 pm on November 13, 2014: contributor
Using the same preconditions as before (the code doesn’t have dynamic checks yet), I get:
S_r[0..1] ∈ [0..67108863] [2] ∈ [0..68157440] [3..8] ∈ [0..67108863] [9] ∈ [0..4194303]
for secp256k1_fe_mul_inner
and
S_r[0..1] ∈ [0..67108863] [2] ∈ [0..68157440] [3..8] ∈ [0..67108863] [9] ∈ [0..4194303]
secp256k1_fe_sqr_inner
And no overflows.
Can you add the dynamic checks too? After all, frame-c only proves it correct. :P At least of the input values, since those are axiomatic to this analysis.
-
sipa commented at 1:45 pm on November 14, 2014: contributor@peterdettman still seems to be around 4% slower when compiled with CFLAGS="-O2 -m32" –enable-endomorphism –with-field=32bit than the original version. The 64bit version is very significantly faster.
-
sipa commented at 3:12 pm on November 14, 2014: contributorWith CFLAGS="-O3 -march=native -m32" –enable-endomorphism it’s faster, and the decrease with -O2 isn’t so bad, and I like having code with somewhat better assurances for correctness than we had.
-
Add overflow analysis to field_10x26_impl.h f8cce95650
-
gmaxwell commented at 6:04 pm on November 14, 2014: contributor
Yep, line numbers don’t match because I restated them as the ACSL assertions, but they all pass. I also checked by off-by-one-bit-ing a few of them and checked that they failed when I did so.
For the multiply inner: aq.c:79:[value] Assertion got status valid. aq.c:81:[value] Assertion got status valid. aq.c:86:[value] Assertion got status valid. aq.c:98:[value] Assertion got status valid. aq.c:102:[value] Assertion got status valid. aq.c:104:[value] Assertion got status valid. aq.c:106:[value] Assertion got status valid. aq.c:110:[value] Assertion got status valid. aq.c:112:[value] Assertion got status valid. aq.c:119:[value] Assertion got status valid. aq.c:130:[value] Assertion got status valid. aq.c:134:[value] Assertion got status valid. aq.c:136:[value] Assertion got status valid. aq.c:138:[value] Assertion got status valid. aq.c:142:[value] Assertion got status valid. aq.c:144:[value] Assertion got status valid. aq.c:152:[value] Assertion got status valid. aq.c:162:[value] Assertion got status valid. aq.c:166:[value] Assertion got status valid. aq.c:168:[value] Assertion got status valid. aq.c:170:[value] Assertion got status valid. aq.c:174:[value] Assertion got status valid. aq.c:176:[value] Assertion got status valid. aq.c:185:[value] Assertion got status valid. aq.c:194:[value] Assertion got status valid. aq.c:198:[value] Assertion got status valid. aq.c:200:[value] Assertion got status valid. aq.c:205:[value] Assertion got status valid. aq.c:207:[value] Assertion got status valid. aq.c:217:[value] Assertion got status valid. aq.c:225:[value] Assertion got status valid. aq.c:229:[value] Assertion got status valid. aq.c:231:[value] Assertion got status valid. aq.c:236:[value] Assertion got status valid. aq.c:238:[value] Assertion got status valid. aq.c:249:[value] Assertion got status valid. aq.c:256:[value] Assertion got status valid. aq.c:260:[value] Assertion got status valid. aq.c:262:[value] Assertion got status valid. aq.c:267:[value] Assertion got status valid. aq.c:269:[value] Assertion got status valid. aq.c:281:[value] Assertion got status valid. aq.c:287:[value] Assertion got status valid. aq.c:291:[value] Assertion got status valid. aq.c:293:[value] Assertion got status valid. aq.c:298:[value] Assertion got status valid. aq.c:300:[value] Assertion got status valid. aq.c:314:[value] Assertion got status valid. aq.c:319:[value] Assertion got status valid. aq.c:323:[value] Assertion got status valid. aq.c:325:[value] Assertion got status valid. aq.c:328:[value] Assertion got status valid. aq.c:332:[value] Assertion got status valid. aq.c:334:[value] Assertion got status valid. aq.c:349:[value] Assertion got status valid. aq.c:353:[value] Assertion got status valid. aq.c:357:[value] Assertion got status valid. aq.c:359:[value] Assertion got status valid. aq.c:362:[value] Assertion got status valid. aq.c:367:[value] Assertion got status valid. aq.c:371:[value] Assertion got status valid. aq.c:375:[value] Assertion got status valid. aq.c:379:[value] Assertion got status valid. aq.c:383:[value] Assertion got status valid. aq.c:388:[value] Assertion got status valid. aq.c:390:[value] Assertion got status valid. aq.c:395:[value] Assertion got status valid. aq.c:399:[value] Assertion got status valid. aq.c:401:[value] Assertion got status valid. aq.c:408:[value] Assertion got status valid. aq.c:412:[value] Assertion got status valid. aq.c:414:[value] Assertion got status valid. aq.c:418:[value] Assertion got status valid. aq.c:420:[value] Assertion got status valid. aq.c:425:[value] Assertion got status valid. aq.c:427:[value] Assertion got status valid. aq.c:429:[value] Assertion got status valid. aq.c:433:[value] Assertion got status valid. aq.c:437:[value] Assertion got status valid.
-
gmaxwell commented at 6:49 pm on November 14, 2014: contributor
And for the sqr:
aqq.c:49:[value] Assertion got status valid. aqq.c:51:[value] Assertion got status valid. aqq.c:56:[value] Assertion got status valid. aqq.c:64:[value] Assertion got status valid. aqq.c:68:[value] Assertion got status valid. aqq.c:70:[value] Assertion got status valid. aqq.c:72:[value] Assertion got status valid. aqq.c:76:[value] Assertion got status valid. aqq.c:78:[value] Assertion got status valid. aqq.c:84:[value] Assertion got status valid. aqq.c:91:[value] Assertion got status valid. aqq.c:95:[value] Assertion got status valid. aqq.c:97:[value] Assertion got status valid. aqq.c:99:[value] Assertion got status valid. aqq.c:103:[value] Assertion got status valid. aqq.c:105:[value] Assertion got status valid. aqq.c:112:[value] Assertion got status valid. aqq.c:119:[value] Assertion got status valid. aqq.c:123:[value] Assertion got status valid. aqq.c:125:[value] Assertion got status valid. aqq.c:127:[value] Assertion got status valid. aqq.c:131:[value] Assertion got status valid. aqq.c:133:[value] Assertion got status valid. aqq.c:140:[value] Assertion got status valid. aqq.c:146:[value] Assertion got status valid. aqq.c:150:[value] Assertion got status valid. aqq.c:152:[value] Assertion got status valid. aqq.c:157:[value] Assertion got status valid. aqq.c:159:[value] Assertion got status valid. aqq.c:167:[value] Assertion got status valid. aqq.c:173:[value] Assertion got status valid. aqq.c:177:[value] Assertion got status valid. aqq.c:179:[value] Assertion got status valid. aqq.c:184:[value] Assertion got status valid. aqq.c:186:[value] Assertion got status valid. aqq.c:194:[value] Assertion got status valid. aqq.c:199:[value] Assertion got status valid. aqq.c:203:[value] Assertion got status valid. aqq.c:205:[value] Assertion got status valid. aqq.c:210:[value] Assertion got status valid. aqq.c:212:[value] Assertion got status valid. aqq.c:221:[value] Assertion got status valid. aqq.c:226:[value] Assertion got status valid. aqq.c:230:[value] Assertion got status valid. aqq.c:232:[value] Assertion got status valid. aqq.c:237:[value] Assertion got status valid. aqq.c:239:[value] Assertion got status valid. aqq.c:249:[value] Assertion got status valid. aqq.c:253:[value] Assertion got status valid. aqq.c:257:[value] Assertion got status valid. aqq.c:259:[value] Assertion got status valid. aqq.c:262:[value] Assertion got status valid. aqq.c:266:[value] Assertion got status valid. aqq.c:268:[value] Assertion got status valid. aqq.c:279:[value] Assertion got status valid. aqq.c:283:[value] Assertion got status valid. aqq.c:287:[value] Assertion got status valid. aqq.c:289:[value] Assertion got status valid. aqq.c:292:[value] Assertion got status valid. aqq.c:297:[value] Assertion got status valid. aqq.c:301:[value] Assertion got status valid. aqq.c:305:[value] Assertion got status valid. aqq.c:309:[value] Assertion got status valid. aqq.c:313:[value] Assertion got status valid. aqq.c:318:[value] Assertion got status valid. aqq.c:320:[value] Assertion got status valid. aqq.c:325:[value] Assertion got status valid. aqq.c:329:[value] Assertion got status valid. aqq.c:331:[value] Assertion got status valid. aqq.c:338:[value] Assertion got status valid. aqq.c:342:[value] Assertion got status valid. aqq.c:344:[value] Assertion got status valid. aqq.c:348:[value] Assertion got status valid. aqq.c:350:[value] Assertion got status valid. aqq.c:355:[value] Assertion got status valid. aqq.c:357:[value] Assertion got status valid. aqq.c:359:[value] Assertion got status valid. aqq.c:363:[value] Assertion got status valid. aqq.c:367:[value] Assertion got status valid.
-
sipa merged this on Nov 15, 2014
-
sipa closed this on Nov 15, 2014
-
sipa referenced this in commit 21288f2d05 on Nov 15, 2014
-
gmaxwell cross-referenced this on Nov 15, 2014 from issue Rewrite mul/sqr for 32bit/64bit by peterdettman
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 09:15 UTC
More mirrored repositories can be found on mirror.b10c.me