diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-11-01 15:41:37 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-11-11 11:55:00 -0500 |
| commit | db9921705a8038507335117ecaaeace1f3ac0b80 (patch) | |
| tree | f053b4b931c3203d623d22beb195e3f01388c47f /src/Util | |
| parent | 56c498de53c503222806dfc2399a117802d1b290 (diff) | |
Update the post-bounds rewrite rules
They are all proven, and they work!
To make this possible, we had to make casting commute with negation.
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------------------
32m30.13s | Total | 32m17.70s || +0m12.42s | +0.64%
--------------------------------------------------------------------------------------------------------------------
1m38.96s | Experiments/NewPipeline/RewriterRulesGood.vo | 1m23.70s || +0m15.26s | +18.23%
4m44.45s | Experiments/NewPipeline/Toplevel1.vo | 4m58.41s || -0m13.95s | -4.67%
2m08.47s | Experiments/NewPipeline/RewriterRulesInterpGood.vo | 1m56.27s || +0m12.19s | +10.49%
6m36.50s | p384_32.c | 6m42.34s || -0m05.84s | -1.45%
6m19.09s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m15.11s || +0m03.97s | +1.06%
1m24.28s | Experiments/NewPipeline/Rewriter.vo | 1m20.87s || +0m03.40s | +4.21%
0m40.26s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m43.07s || -0m02.81s | -6.52%
1m57.38s | Experiments/NewPipeline/RewriterWf2.vo | 1m59.36s || -0m01.98s | -1.65%
1m40.57s | Experiments/NewPipeline/Toplevel2.vo | 1m41.68s || -0m01.11s | -1.09%
0m42.80s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m41.59s || +0m01.20s | +2.90%
0m25.06s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m26.26s || -0m01.20s | -4.56%
0m18.78s | p256_32.c | 0m17.12s || +0m01.66s | +9.69%
0m18.49s | secp256k1_32.c | 0m17.05s || +0m01.43s | +8.44%
0m15.98s | Experiments/NewPipeline/RewriterWf1.vo | 0m17.00s || -0m01.01s | -5.99%
0m08.04s | p224_32.c | 0m07.03s || +0m01.00s | +14.36%
0m39.70s | p521_32.c | 0m40.46s || -0m00.75s | -1.87%
0m33.03s | p521_64.c | 0m33.98s || -0m00.94s | -2.79%
0m23.34s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m22.79s || +0m00.55s | +2.41%
0m18.64s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m17.70s || +0m00.94s | +5.31%
0m14.98s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m14.20s || +0m00.78s | +5.49%
0m11.58s | p384_64.c | 0m11.49s || +0m00.08s | +0.78%
0m09.16s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.29s || -0m00.12s | -1.39%
0m06.04s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.01s || +0m00.03s | +0.49%
0m05.80s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.85s || -0m00.04s | -0.85%
0m04.74s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.36s || +0m00.37s | +8.71%
0m04.57s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.91s || -0m00.33s | -6.92%
0m03.66s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.55s || +0m00.11s | +3.09%
0m02.24s | curve25519_32.c | 0m02.29s || -0m00.04s | -2.18%
0m02.04s | p224_64.c | 0m01.86s || +0m00.17s | +9.67%
0m01.98s | secp256k1_64.c | 0m02.45s || -0m00.47s | -19.18%
0m01.97s | p256_64.c | 0m01.88s || +0m00.09s | +4.78%
0m01.49s | curve25519_64.c | 0m01.55s || -0m00.06s | -3.87%
0m01.40s | Experiments/NewPipeline/CLI.vo | 0m01.49s || -0m00.09s | -6.04%
0m01.30s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.34s || -0m00.04s | -2.98%
0m01.26s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.31s || -0m00.05s | -3.81%
0m01.10s | Experiments/NewPipeline/CompilersTestCases.vo | 0m01.12s || -0m00.02s | -1.78%
0m01.00s | Experiments/NewPipeline/RewriterProofs.vo | 0m00.97s || +0m00.03s | +3.09%
Diffstat (limited to 'src/Util')
0 files changed, 0 insertions, 0 deletions