diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-20 18:50:55 -0500 |
|---|---|---|
| committer |  Andres Erbsen <andreser@mit.edu> | 2019-01-05 03:40:45 -0500 |
| commit | a1f2b8bb005c580d75574dd8e5b057cf12f9bcc7 (patch) | |
| tree | 8cd5ddd19de561a05fe283321fc2010b3663443f /_CoqProject | |
| parent | 1f8b428d03c7d448680245f5752004a32ce77c20 (diff) | |
new pipeline: refactor glue, split into more files
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 | ∞
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/_CoqProject b/_CoqProject index ce927e75e..77482ceb2 100644 --- a/_CoqProject +++ b/_CoqProject @@ -251,7 +251,9 @@ src/Experiments/NewPipeline/AbstractInterpretationProofs.v src/Experiments/NewPipeline/AbstractInterpretationWf.v src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v src/Experiments/NewPipeline/Arithmetic.v +src/Experiments/NewPipeline/BoundsPipeline.v src/Experiments/NewPipeline/CLI.v +src/Experiments/NewPipeline/COperationSpecifications.v src/Experiments/NewPipeline/CStringification.v src/Experiments/NewPipeline/CompilersTestCases.v src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v @@ -261,6 +263,7 @@ src/Experiments/NewPipeline/LanguageInversion.v src/Experiments/NewPipeline/LanguageWf.v src/Experiments/NewPipeline/MiscCompilerPasses.v src/Experiments/NewPipeline/MiscCompilerPassesProofs.v +src/Experiments/NewPipeline/PushButtonSynthesis.v src/Experiments/NewPipeline/Rewriter.v src/Experiments/NewPipeline/RewriterInterpProofs1.v src/Experiments/NewPipeline/RewriterProofs.v @@ -271,7 +274,6 @@ src/Experiments/NewPipeline/RewriterWf2.v src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v src/Experiments/NewPipeline/StandaloneHaskellMain.v src/Experiments/NewPipeline/StandaloneOCamlMain.v -src/Experiments/NewPipeline/Toplevel1.v src/Experiments/NewPipeline/Toplevel2.v src/Experiments/NewPipeline/UnderLets.v src/Experiments/NewPipeline/UnderLetsProofs.v @@ -281,6 +283,7 @@ src/Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.v src/Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.v src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.v src/Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.v +src/Experiments/NewPipeline/PushButtonSynthesis/ReificationCache.v src/LegacyArithmetic/ArchitectureToZLike.v src/LegacyArithmetic/ArchitectureToZLikeProofs.v src/LegacyArithmetic/BarretReduction.v |