aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v
Commit message (Collapse)AuthorAge
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
|
* new pipeline: refactor glue, split into more filesGravatar Jason Gross2019-01-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP Try to remove assumption that s = weight n After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 14m03.04s | Total | 20m54.46s || -6m51.41s | -32.79% -------------------------------------------------------------------------------------------------------------------- 0m01.18s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m18.83s || -6m17.64s | -99.68% N/A | Experiments/NewPipeline/Toplevel1.vo | 4m36.32s || -4m36.31s | -100.00% 4m17.06s | Experiments/NewPipeline/PushButtonSynthesis.vo | N/A || +4m17.06s | ∞ 1m28.64s | Experiments/NewPipeline/Toplevel2.vo | 1m38.21s || -0m09.57s | -9.74% 3m10.57s | p384_32.c | 3m18.05s || -0m07.48s | -3.77% 0m06.36s | Experiments/NewPipeline/BoundsPipeline.vo | N/A || +0m06.36s | ∞ 0m06.16s | Experiments/NewPipeline/COperationSpecifications.vo | N/A || +0m06.16s | ∞ 0m05.66s | p384_64.c | 0m10.80s || -0m05.14s | -47.59% 0m38.24s | p521_32.c | 0m41.31s || -0m03.07s | -7.43% 0m31.64s | p521_64.c | 0m33.94s || -0m02.29s | -6.77% 0m45.06s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m43.83s || +0m01.23s | +2.80% 0m30.57s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m29.56s || +0m01.01s | +3.41% 0m13.52s | secp256k1_32.c | 0m14.60s || -0m01.08s | -7.39% 0m01.00s | p256_64.c | 0m02.03s || -0m01.02s | -50.73% 0m24.19s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m23.62s || +0m00.57s | +2.41% 0m16.66s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m16.40s || +0m00.26s | +1.58% 0m13.34s | p256_32.c | 0m14.00s || -0m00.66s | -4.71% 0m10.40s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m10.08s || +0m00.32s | +3.17% 0m10.11s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.81s || +0m00.29s | +3.05% 0m07.84s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m07.66s || +0m00.17s | +2.34% 0m07.09s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.62s || +0m00.46s | +7.09% 0m06.89s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m06.42s || +0m00.46s | +7.32% 0m06.26s | p224_32.c | 0m06.54s || -0m00.28s | -4.28% 0m05.24s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.99s || +0m00.25s | +5.01% 0m04.96s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.94s || +0m00.01s | +0.40% 0m04.19s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m04.10s || +0m00.09s | +2.19% 0m02.13s | curve25519_32.c | 0m02.30s || -0m00.16s | -7.39% 0m01.46s | curve25519_64.c | 0m01.65s || -0m00.18s | -11.51% 0m01.44s | Experiments/NewPipeline/CLI.vo | 0m01.37s || +0m00.06s | +5.10% 0m01.31s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.30s || +0m00.01s | +0.76% 0m01.26s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.25s || +0m00.01s | +0.80% 0m01.15s | secp256k1_64.c | 0m01.91s || -0m00.76s | -39.79% 0m01.03s | p224_64.c | 0m02.02s || -0m00.99s | -49.00% 0m00.44s | Experiments/NewPipeline/PushButtonSynthesis/ReificationCache.vo | N/A || +0m00.44s | ∞
* Revert "Disable very very slow printing"Gravatar Jason Gross2018-11-07
| | | | | | | | | | | | | This reverts commit 5cb258c09a602be3a6414b9c70fc7e1ab4b178b8. Since we fixed adjust_s, we don't actually need to remove the print statement, as it only takes 3 minutes rather than 50. After | File Name | Before || Change | % Change --------------------------------------------------------------------------------------------------- 6m12.87s | Total | 3m27.44s || +2m45.43s | +79.74% --------------------------------------------------------------------------------------------------- 6m12.88s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 3m27.45s || +2m45.43s | +79.74%
* Disable very very slow printingGravatar Jason Gross2018-11-06
| | | | | | | | | | | The number of lines of code in the synthesized p256 mulmod went from 2253 to 7575, and the time of printing went from about 161 s to about 3653 s. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------------- 5m25.05s | Total | 66m04.61s || -60m39.56s | -91.80% ----------------------------------------------------------------------------------------------------- 5m25.05s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 66m04.62s || -60m39.56s | -91.80%
* Import prim token notations before using themGravatar Jason Gross2018-08-24
| | | | | | | | | | | This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. c.f. https://github.com/coq/coq/pull/8064#issuecomment-415493362 Almost all changes were made via https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169#file-fix-py
* Better error message printingGravatar Jason Gross2018-07-12
| | | | When printing the bounds analysis tree, try harder to convert to C
* Remove useless dependencyGravatar Jason Gross2018-07-12
|
* Fix missing argGravatar Jason Gross2018-07-03
|
* Comment out some code that's too slowGravatar Jason Gross2018-07-03
|
* synthesize squareGravatar Jason Gross2018-07-03
|
* WIPGravatar Jason Gross2018-07-03
|
* New pipeline, split among filesGravatar Jason Gross2018-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 02:45:51 +0000