diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-02 11:23:10 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-03 00:22:13 -0500 |
| commit | 1f8b428d03c7d448680245f5752004a32ce77c20 (patch) | |
| tree | d954d42e1aa89454cd3a695f0c3eaea8ffe027e0 /_CoqProject | |
| parent | 2238baafd6ad626bbec17b85cbeb79f848475d6e (diff) | |
Prove that convert_bases partitions
Unfortunately, the proof is rather slow :-(
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------------------
22m46.26s | Total | 22m03.36s || +0m42.90s | +3.24%
--------------------------------------------------------------------------------------------------------------------
1m57.06s | Experiments/NewPipeline/Arithmetic.vo | 1m15.08s || +0m41.98s | +55.91%
0m42.39s | p521_32.c | 0m39.92s || +0m02.46s | +6.18%
0m35.40s | p521_64.c | 0m33.02s || +0m02.37s | +7.20%
3m15.80s | p384_32.c | 3m17.10s || -0m01.29s | -0.65%
6m19.46s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m18.91s || +0m00.54s | +0.14%
4m34.80s | Experiments/NewPipeline/Toplevel1.vo | 4m35.56s || -0m00.75s | -0.27%
1m36.64s | Experiments/NewPipeline/Toplevel2.vo | 1m36.64s || +0m00.00s | +0.00%
0m43.22s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m44.18s || -0m00.96s | -2.17%
0m29.24s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m29.83s || -0m00.58s | -1.97%
0m22.83s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m22.87s || -0m00.04s | -0.17%
0m16.11s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m16.73s || -0m00.62s | -3.70%
0m14.24s | p256_32.c | 0m13.75s || +0m00.49s | +3.56%
0m14.22s | secp256k1_32.c | 0m14.19s || +0m00.03s | +0.21%
0m11.01s | p384_64.c | 0m10.50s || +0m00.50s | +4.85%
0m09.71s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.86s || -0m00.14s | -1.52%
0m09.69s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m10.35s || -0m00.66s | -6.37%
0m07.41s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m07.74s || -0m00.33s | -4.26%
0m06.65s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.52s || +0m00.13s | +1.99%
0m06.50s | p224_32.c | 0m06.47s || +0m00.03s | +0.46%
0m06.24s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m06.38s || -0m00.13s | -2.19%
0m05.10s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.97s || +0m00.12s | +2.61%
0m04.82s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m05.04s || -0m00.21s | -4.36%
0m03.95s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m04.02s || -0m00.06s | -1.74%
0m02.31s | curve25519_32.c | 0m02.24s || +0m00.06s | +3.12%
0m02.03s | p224_64.c | 0m01.92s || +0m00.10s | +5.72%
0m01.91s | secp256k1_64.c | 0m02.00s || -0m00.09s | -4.50%
0m01.90s | p256_64.c | 0m01.86s || +0m00.03s | +2.15%
0m01.54s | curve25519_64.c | 0m01.61s || -0m00.07s | -4.34%
0m01.51s | Experiments/NewPipeline/CLI.vo | 0m01.49s || +0m00.02s | +1.34%
0m01.29s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.29s || +0m00.00s | +0.00%
0m01.28s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.32s || -0m00.04s | -3.03%
Diffstat (limited to '_CoqProject')
0 files changed, 0 insertions, 0 deletions