diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-24 21:40:48 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-08-25 15:35:00 -0400 |
| commit | 673534439ac5002e995ebcf49ea640692c83f2d8 (patch) | |
| tree | e54fe2fe646521b74559194f7cd8abae1519b3f3 /_CoqProject | |
| parent | 8a76415f12bb3d45e76e258245310161e102a367 (diff) | |
Do almost all ZRange proofs
We haven't done most of the fancy machine operations (and, in fact, most
of that bounds analysis is wrong in theory even if it's correct on the
inputs that we see), but the rest is done.
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------------------
17m45.36s | Total | 17m48.00s || -0m02.63s | -0.24%
--------------------------------------------------------------------------------------------------------------------
4m34.24s | Experiments/NewPipeline/Toplevel1 | 4m36.34s || -0m02.10s | -0.75%
0m21.01s | Experiments/NewPipeline/AbstractInterpretationZRangeProofs | 0m23.78s || -0m02.76s | -11.64%
6m03.20s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 6m01.29s || +0m01.90s | +0.52%
1m44.40s | Experiments/NewPipeline/Toplevel2 | 1m43.68s || +0m00.71s | +0.69%
0m38.53s | p521_32.c | 0m38.56s || -0m00.03s | -0.07%
0m37.22s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m37.36s || -0m00.14s | -0.37%
0m35.10s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m34.95s || +0m00.14s | +0.42%
0m32.10s | p521_64.c | 0m32.20s || -0m00.10s | -0.31%
0m23.75s | p384_32.c | 0m23.76s || -0m00.01s | -0.04%
0m20.06s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m20.38s || -0m00.32s | -1.57%
0m18.77s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m18.77s || +0m00.00s | +0.00%
0m13.63s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m13.52s || +0m00.11s | +0.81%
0m11.74s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m11.72s || +0m00.01s | +0.17%
0m10.38s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m10.40s || -0m00.01s | -0.19%
0m08.66s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.61s || +0m00.05s | +0.58%
0m08.50s | p384_64.c | 0m08.48s || +0m00.01s | +0.23%
0m05.46s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.52s || -0m00.05s | -1.08%
0m05.35s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.40s || -0m00.05s | -0.92%
0m03.98s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.04s || -0m00.06s | -1.48%
0m03.91s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m03.93s || -0m00.02s | -0.50%
0m03.90s | p256_32.c | 0m03.87s || +0m00.02s | +0.77%
0m03.76s | secp256k1_32.c | 0m03.73s || +0m00.02s | +0.80%
0m03.16s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.25s || -0m00.08s | -2.76%
0m02.21s | p224_32.c | 0m02.10s || +0m00.10s | +5.23%
0m02.15s | curve25519_32.c | 0m02.07s || +0m00.08s | +3.86%
0m01.67s | p224_64.c | 0m01.68s || -0m00.01s | -0.59%
0m01.65s | secp256k1_64.c | 0m01.66s || -0m00.01s | -0.60%
0m01.51s | p256_64.c | 0m01.66s || -0m00.14s | -9.03%
0m01.43s | Experiments/NewPipeline/CLI | 0m01.46s || -0m00.03s | -2.05%
0m01.38s | curve25519_64.c | 0m01.39s || -0m00.01s | -0.71%
0m01.28s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.26s || +0m00.02s | +1.58%
0m01.28s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.18s || +0m00.10s | +8.47%
Diffstat (limited to '_CoqProject')
0 files changed, 0 insertions, 0 deletions