Have word_by_word_montgonery compute s and c from the prime #486

JasonGross · 2019-01-13T06:48:42Z

This allows us to support primes which are not a power of 2. We also add p484 as an example. To support this, I added a small parser combinator library which can parse arithmetic expressions involving `()^*/+-` and decimal digits. Closes mit-plv#486 Closes mit-plv#342

This allows us to support primes which are not a power of 2. We also add p484 as an example. To support this, I added a small parser combinator library which can parse arithmetic expressions involving `()^*/+-` and decimal digits. N.B. I had to move the definition of the c-files variables up above the c-files target to make it build anything at all. Closes mit-plv#486 Closes mit-plv#342

This allows us to support primes which are not a power of 2. We also add p484 as an example. To support this, I added a small parser combinator library which can parse arithmetic expressions involving `()^*/+-` and decimal digits. Closes mit-plv#486 Closes mit-plv#342

This allows us to support primes which are not a power of 2. We also add p484 as an example. To support this, I added a small parser combinator library which can parse arithmetic expressions involving `()^*/+-` and decimal digits. Closes mit-plv#486 Closes mit-plv#342 After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 22m14.42s | Total | 12m14.76s || +9m59.65s | +81.61% -------------------------------------------------------------------------------------------- 9m41.91s | p484_32.c | N/A || +9m41.90s | ∞ 0m11.51s | p484_64.c | N/A || +0m11.50s | ∞ 3m16.22s | p384_32.c | 3m12.02s || +0m04.19s | +2.18% 4m12.18s | PushButtonSynthesis.vo | 4m10.16s || +0m02.02s | +0.80% 0m45.08s | ExtractionHaskell/word_by_word_montgomery | 0m45.24s || -0m00.16s | -0.35% 0m38.14s | p521_32.c | 0m38.12s || +0m00.02s | +0.05% 0m31.80s | p521_64.c | 0m31.78s || +0m00.01s | +0.06% 0m31.09s | ExtractionHaskell/unsaturated_solinas | 0m30.77s || +0m00.32s | +1.03% 0m24.18s | ExtractionHaskell/saturated_solinas | 0m24.21s || -0m00.03s | -0.12% 0m17.38s | ExtractionOCaml/word_by_word_montgomery | 0m17.35s || +0m00.02s | +0.17% 0m13.39s | secp256k1_32.c | 0m13.59s || -0m00.19s | -1.47% 0m13.14s | p256_32.c | 0m13.04s || +0m00.10s | +0.76% 0m10.58s | ExtractionOCaml/unsaturated_solinas | 0m10.73s || -0m00.15s | -1.39% 0m10.23s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.34s || -0m00.10s | -1.06% 0m07.88s | ExtractionOCaml/saturated_solinas | 0m07.94s || -0m00.06s | -0.75% 0m06.78s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.86s || -0m00.08s | -1.16% 0m06.28s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.42s || -0m00.13s | -2.18% 0m06.00s | p224_32.c | 0m05.97s || +0m00.03s | +0.50% 0m05.50s | p384_64.c | 0m05.35s || +0m00.15s | +2.80% 0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.08s || +0m00.20s | +3.93% 0m05.10s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.98s || +0m00.11s | +2.40% 0m04.12s | ExtractionHaskell/saturated_solinas.hs | 0m04.15s || -0m00.03s | -0.72% 0m02.14s | curve25519_32.c | 0m02.28s || -0m00.13s | -6.14% 0m01.44s | CLI.vo | 0m01.42s || +0m00.02s | +1.40% 0m01.44s | curve25519_64.c | 0m01.57s || -0m00.13s | -8.28% 0m01.14s | StandaloneOCamlMain.vo | 0m01.11s || +0m00.02s | +2.70% 0m01.12s | p256_64.c | 0m00.98s || +0m00.14s | +14.28% 0m01.11s | StandaloneHaskellMain.vo | 0m01.17s || -0m00.05s | -5.12% 0m01.03s | secp256k1_64.c | 0m01.15s || -0m00.11s | -10.43% 0m01.02s | p224_64.c | 0m00.99s || +0m00.03s | +3.03% 0m00.21s | Util/Strings/ParseArithmetic.vo | N/A || +0m00.21s | ∞

ghost · 2019-01-13T19:34:32Z

argh, it's p434 ( 2^216 * 3^137 − 1, which is unofficial, see https://eprint.iacr.org/2018/313.pdf), if you'd like to add tests for real-world-crypto use p503 (2^250 * 3^159) which is slightly slower than p434 or the stronger p751 (2^372*3^239). However it's still the same issue (for p503: Values not provably equal (s ≠ 2^log2(s) (needed for from_bytes)) : expected 13175843156907117380839252916199345042492186767578363998445663477035843932020761233518914911546024351608607150390087656982982306331019593961154237431808 = 13093562431584567480052758787310396608866568184172259157933165472384535185618698219533080369303616628603546736510240284036869026183541572213314110357504)

JasonGross · 2019-01-13T19:42:32Z

Have you tried it with #487? That shouldn't come up anymore.

ghost · 2019-01-13T20:12:25Z

I applied the PR's diff manually, now I'm getting:

./src/ExtractionOCaml/word_by_word_montgomery 'p503' '2^250*3^159' '1,1' '64' mul
Fatal error: exception Stack_overflow

🤔

JasonGross · 2019-01-14T04:20:23Z

That's the wrong input format. You told it to synthesize with bitwidth 1. Try

./src/ExtractionOCaml/word_by_word_montgomery 'p503' '2^250*3^159-1' '64' mul

ghost · 2019-01-14T06:46:31Z

ah, I didn't notice the input format had changed. Now it works, including from/to_bytes, thanks!

This allows us to support primes which are not a power of 2. We also add p484 as an example. To support this, I added a small parser combinator library which can parse arithmetic expressions involving `()^*/+-` and decimal digits. Closes #486 Closes #342 After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 22m14.42s | Total | 12m14.76s || +9m59.65s | +81.61% -------------------------------------------------------------------------------------------- 9m41.91s | p484_32.c | N/A || +9m41.90s | ∞ 0m11.51s | p484_64.c | N/A || +0m11.50s | ∞ 3m16.22s | p384_32.c | 3m12.02s || +0m04.19s | +2.18% 4m12.18s | PushButtonSynthesis.vo | 4m10.16s || +0m02.02s | +0.80% 0m45.08s | ExtractionHaskell/word_by_word_montgomery | 0m45.24s || -0m00.16s | -0.35% 0m38.14s | p521_32.c | 0m38.12s || +0m00.02s | +0.05% 0m31.80s | p521_64.c | 0m31.78s || +0m00.01s | +0.06% 0m31.09s | ExtractionHaskell/unsaturated_solinas | 0m30.77s || +0m00.32s | +1.03% 0m24.18s | ExtractionHaskell/saturated_solinas | 0m24.21s || -0m00.03s | -0.12% 0m17.38s | ExtractionOCaml/word_by_word_montgomery | 0m17.35s || +0m00.02s | +0.17% 0m13.39s | secp256k1_32.c | 0m13.59s || -0m00.19s | -1.47% 0m13.14s | p256_32.c | 0m13.04s || +0m00.10s | +0.76% 0m10.58s | ExtractionOCaml/unsaturated_solinas | 0m10.73s || -0m00.15s | -1.39% 0m10.23s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.34s || -0m00.10s | -1.06% 0m07.88s | ExtractionOCaml/saturated_solinas | 0m07.94s || -0m00.06s | -0.75% 0m06.78s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.86s || -0m00.08s | -1.16% 0m06.28s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.42s || -0m00.13s | -2.18% 0m06.00s | p224_32.c | 0m05.97s || +0m00.03s | +0.50% 0m05.50s | p384_64.c | 0m05.35s || +0m00.15s | +2.80% 0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.08s || +0m00.20s | +3.93% 0m05.10s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.98s || +0m00.11s | +2.40% 0m04.12s | ExtractionHaskell/saturated_solinas.hs | 0m04.15s || -0m00.03s | -0.72% 0m02.14s | curve25519_32.c | 0m02.28s || -0m00.13s | -6.14% 0m01.44s | CLI.vo | 0m01.42s || +0m00.02s | +1.40% 0m01.44s | curve25519_64.c | 0m01.57s || -0m00.13s | -8.28% 0m01.14s | StandaloneOCamlMain.vo | 0m01.11s || +0m00.02s | +2.70% 0m01.12s | p256_64.c | 0m00.98s || +0m00.14s | +14.28% 0m01.11s | StandaloneHaskellMain.vo | 0m01.17s || -0m00.05s | -5.12% 0m01.03s | secp256k1_64.c | 0m01.15s || -0m00.11s | -10.43% 0m01.02s | p224_64.c | 0m00.99s || +0m00.03s | +3.03% 0m00.21s | Util/Strings/ParseArithmetic.vo | N/A || +0m00.21s | ∞

ghost · 2019-02-05T21:01:10Z

argh, it's p434 ( 2^216 * 3^137 − 1, which is unofficial, see https://eprint.iacr.org/2018/313.pdf)

ping on that typo, I had a PR to change the Makefile and rename the file and functions/comments prepared, but I wasn't sure if it would interfere with upcomming changes :-)

JasonGross · 2019-02-05T21:42:50Z

Feel free to submit a PR with p434 added to the Makefile and adding the generated .c file as well. If you do this, please mention how long it takes to run; I don't think we should add any new examples that take more than a minute or two on a powerful machine. Unless you see a reason not to, I think we should leave the existing examples as they are.

JasonGross · 2019-02-05T21:43:54Z

interfere with upcomming changes

All of the changes I'm currently working on should not impact the generated C code.

ghost · 2019-02-05T21:55:00Z

It‘s just a typo in the name of the curve, no need to regenerate the c file and no perf impact, the prime remains the same.

JasonGross · 2019-02-06T04:38:09Z

Ah, then, sure, feel free to submit the PR fixing that.

…

On Tue, Feb 5, 2019, 16:55 Daniel Hirche ***@***.***> wrote: It‘s just a typo in the name of the curve, no need to regenerate the c file and no perf impact, the prime remains the same. — You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub <#486 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAYLLCylBACjfdx0Neg_FUoqTxaDmeX-ks5vKf20gaJpZM4Z9A1B> .

Renamed the generated file and function names / comments within, update Makefile. This fixes a typo in the name of the curve, the prime remains the same, see #486 (comment)

JasonGross self-assigned this Jan 13, 2019

JasonGross mentioned this issue Jan 13, 2019

Autocompute s and c in WBW Montgomery #487

Merged

This comment has been minimized.

Sign in to view

JasonGross mentioned this issue Jan 14, 2019

Better error resilience to bitwidth 1 #488

Closed

JasonGross closed this as completed in #487 Jan 14, 2019

ghost mentioned this issue Feb 6, 2019

Rename p484_64.c to p434_64.c (fix typo) #518

Merged

JasonGross pushed a commit that referenced this issue Feb 12, 2019

Rename p484_64.c to p434_64.c (fix typo)

8708ece

Renamed the generated file and function names / comments within, update Makefile. This fixes a typo in the name of the curve, the prime remains the same, see #486 (comment)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Have word_by_word_montgonery compute s and c from the prime #486

Have word_by_word_montgonery compute s and c from the prime #486

JasonGross commented Jan 13, 2019

ghost commented Jan 13, 2019 •

edited by ghost

Loading

JasonGross commented Jan 13, 2019

ghost commented Jan 13, 2019

This comment has been minimized.

JasonGross commented Jan 14, 2019 •

edited

Loading

ghost commented Jan 14, 2019

ghost commented Feb 5, 2019

JasonGross commented Feb 5, 2019

JasonGross commented Feb 5, 2019

ghost commented Feb 5, 2019

JasonGross commented Feb 6, 2019 via email

Have word_by_word_montgonery compute s and c from the prime #486

Have word_by_word_montgonery compute s and c from the prime #486

Comments

JasonGross commented Jan 13, 2019

ghost commented Jan 13, 2019 • edited by ghost Loading

JasonGross commented Jan 13, 2019

ghost commented Jan 13, 2019

This comment has been minimized.

JasonGross commented Jan 14, 2019 • edited Loading

ghost commented Jan 14, 2019

ghost commented Feb 5, 2019

JasonGross commented Feb 5, 2019

JasonGross commented Feb 5, 2019

ghost commented Feb 5, 2019

JasonGross commented Feb 6, 2019 via email

ghost commented Jan 13, 2019 •

edited by ghost

Loading

JasonGross commented Jan 14, 2019 •

edited

Loading