-
Notifications
You must be signed in to change notification settings - Fork 144
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.
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
Autocompute s and c in WBW Montgomery #487
Conversation
9b0d23a
to
b2f85e1
Compare
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 | ∞
b2f85e1
to
f3ce695
Compare
overall change lgtm. could even further inline c and I would expect it would wind up mostly unused. but not important so not blocking. I'm feeling uneasy about checking in tens of thousands of lines of generated c code, but I guess that is already happening, so we might as well let this one slip... |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please remove the slow file and merge.
It's too slow to generate each time
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
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.Timing diff:
Perhaps we shouldn't include p484_32 as an example or something? What do you think, @andres-erbsen ?