Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Extra validation on top of #73 #103

Merged
merged 4 commits into from
Nov 15, 2014
Merged

Extra validation on top of #73 #103

merged 4 commits into from
Nov 15, 2014

Conversation

sipa
Copy link
Contributor

@sipa sipa commented Nov 13, 2014

No description provided.

peterdettman and others added 3 commits November 13, 2014 04:46
@peterdettman @sipa
Rewrite mul/sqr for 32bit/64bit
5dd421b 
- interleave calculation of the lower and upper partial product ranges, and reduction
- less registers needed, more opportunities for parallel ops
@sipa
Add equalities relating input and output variables
fa0d620
@sipa
Add overflow analysis to field_5x52_int128_impl.h
a518598
@sipa sipa changed the title Extra ' Extra validation on top of #73 Nov 13, 2014
@sipa
Copy link
Contributor Author

sipa commented Nov 13, 2014

@gmaxwell Can you do frama-c analysis on the 32-bit version?

@gmaxwell
Copy link
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
Copy link
Contributor Author

sipa commented Nov 14, 2014

@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
Copy link
Contributor Author

sipa commented Nov 14, 2014

With 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.

@sipa
Copy link
Contributor Author

sipa commented Nov 14, 2014

@gmaxwell Added. Can you get frama-c to also check those VERIFY_BITS assertions? Note that I needed a few more accurate limits in the 32-bit version (checked with a VERIFY_CHECK).

@gmaxwell
Copy link
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
Copy link
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.

@gmaxwell
Copy link
Contributor

ACK.

@sipa perhaps diff the ASM your compiler generates for O3 vs O2 and see if you can see some obvious difference that could be triggered from the source?

@sipa sipa merged commit f8cce95 into bitcoin-core:master Nov 15, 2014
sipa added a commit that referenced this pull request Nov 15, 2014
@sipa
Merge pull request #103
21288f2 
f8cce95 Add overflow analysis to field_10x26_impl.h (Pieter Wuille)
a518598 Add overflow analysis to field_5x52_int128_impl.h (Pieter Wuille)
fa0d620 Add equalities relating input and output variables (Pieter Wuille)
5dd421b Rewrite mul/sqr for 32bit/64bit (Peter Dettman)
@gmaxwell gmaxwell mentioned this pull request Nov 15, 2014
Closed
roconnor-blockstream
roconnor-blockstream reviewed Nov 6, 2023
View reviewed changes
src/field_5x52_int128_impl.h
VERIFY_BITS(u0, 56);
// [d 0 t4+(u0<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0]
c += (__int128)u0 * (R >> 4);
VERIFY_BITS(c, 115);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ought to be VERIFY_BITS(c, 113);

Copy link
Contributor Author

@sipa sipa Nov 6, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you open an issue (or submit a PR to fix it)?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

#1438

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@roconnor-blockstream roconnor-blockstream roconnor-blockstream left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@sipa @gmaxwell @roconnor-blockstream @peterdettman