Extra validation on top of #73

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

5dd421bab5

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

sipa commented at 4:07 pm on November 13, 2014: contributor

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

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: contributor

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.

Add overflow analysis to field_10x26_impl.h f8cce95650

sipa commented at 4:53 pm on November 14, 2014: contributor

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

gmaxwell commented at 6:54 pm on November 14, 2014: 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 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

Extra validation on top of #73 #103