| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
Rather than using Forall2 in some places and a combination of length,
combine, and In in others, we now primarily use Forall2.
There is probably some dead tactic code as a result of this that I just
haven't bothered to clean up.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After | File Name | Before || Change | % Change
-----------------------------------------------------------------------------------------------------------
31m53.77s | Total | 32m03.39s || -0m09.62s | -0.50%
-----------------------------------------------------------------------------------------------------------
3m14.32s | p384_32.c | 3m17.09s || -0m02.77s | -1.40%
0m18.13s | secp256k1_32.c | 0m20.29s || -0m02.16s | -10.64%
1m56.46s | RewriterRulesGood.vo | 1m58.15s || -0m01.68s | -1.43%
1m47.38s | Fancy/Barrett256.vo | 1m48.40s || -0m01.02s | -0.94%
0m55.66s | AbstractInterpretationWf.vo | 0m54.26s || +0m01.39s | +2.58%
0m46.39s | p521_32.c | 0m44.46s || +0m01.92s | +4.34%
0m41.97s | ExtractionHaskell/unsaturated_solinas | 0m43.02s || -0m01.05s | -2.44%
0m29.71s | ExtractionHaskell/saturated_solinas | 0m30.81s || -0m01.09s | -3.57%
0m15.02s | ExtractionOCaml/unsaturated_solinas | 0m13.40s || +0m01.61s | +12.08%
0m06.21s | ExtractionOCaml/saturated_solinas.ml | 0m07.39s || -0m01.17s | -15.96%
2m50.82s | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m50.03s || +0m00.78s | +0.46%
2m37.53s | Fancy/Compiler.vo | 2m37.78s || -0m00.25s | -0.15%
2m02.37s | RewriterWf2.vo | 2m01.63s || +0m00.74s | +0.60%
1m48.26s | RewriterRulesInterpGood.vo | 1m48.36s || -0m00.10s | -0.09%
0m57.65s | ExtractionHaskell/word_by_word_montgomery | 0m58.06s || -0m00.41s | -0.70%
0m55.33s | RewriterInterpProofs1.vo | 0m56.16s || -0m00.82s | -1.47%
0m41.18s | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m40.54s || +0m00.64s | +1.57%
0m40.34s | p521_64.c | 0m40.14s || +0m00.20s | +0.49%
0m37.24s | Fancy/Montgomery256.vo | 0m37.94s || -0m00.69s | -1.84%
0m36.23s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.49s || -0m00.26s | -0.71%
0m36.23s | UnderLetsProofs.vo | 0m37.19s || -0m00.96s | -2.58%
0m35.05s | AbstractInterpretationProofs.vo | 0m34.69s || +0m00.35s | +1.03%
0m30.73s | AbstractInterpretationZRangeProofs.vo | 0m30.15s || +0m00.58s | +1.92%
0m28.92s | LanguageWf.vo | 0m28.74s || +0m00.18s | +0.62%
0m27.29s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.12s || +0m00.16s | +0.62%
0m26.70s | PushButtonSynthesis/MontgomeryReductionReificationCache.vo | 0m26.88s || -0m00.17s | -0.66%
0m25.49s | RewriterWf1.vo | 0m25.30s || +0m00.18s | +0.75%
0m25.03s | SlowPrimeSynthesisExamples.vo | 0m24.13s || +0m00.90s | +3.72%
0m22.83s | ExtractionOCaml/word_by_word_montgomery | 0m22.92s || -0m00.09s | -0.39%
0m20.14s | p448_solinas_64.c | 0m20.16s || -0m00.01s | -0.09%
0m19.64s | p256_32.c | 0m19.47s || +0m00.17s | +0.87%
0m16.09s | p434_64.c | 0m16.00s || +0m00.08s | +0.56%
0m15.98s | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m15.93s || +0m00.05s | +0.31%
0m13.45s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.60s || -0m00.15s | -1.10%
0m11.14s | ExtractionOCaml/saturated_solinas | 0m11.11s || +0m00.03s | +0.27%
0m09.60s | p224_32.c | 0m09.30s || +0m00.29s | +3.22%
0m09.21s | ExtractionHaskell/word_by_word_montgomery.hs | 0m09.87s || -0m00.65s | -6.68%
0m08.44s | p384_64.c | 0m08.62s || -0m00.17s | -2.08%
0m08.22s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.21s || -0m00.99s | -10.74%
0m07.01s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.69s || -0m00.68s | -8.84%
0m06.80s | BoundsPipeline.vo | 0m06.73s || +0m00.06s | +1.04%
0m05.68s | Fancy/Prod.vo | 0m05.76s || -0m00.08s | -1.38%
0m05.44s | ExtractionHaskell/saturated_solinas.hs | 0m06.42s || -0m00.97s | -15.26%
0m05.28s | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m05.92s || -0m00.63s | -10.81%
0m03.67s | MiscCompilerPassesProofs.vo | 0m03.62s || +0m00.04s | +1.38%
0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.64s || -0m00.10s | -2.74%
0m03.45s | PushButtonSynthesis/SmallExamples.vo | 0m03.45s || +0m00.00s | +0.00%
0m03.24s | PushButtonSynthesis/BarrettReduction.vo | 0m03.21s || +0m00.03s | +0.93%
0m03.19s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.18s || +0m00.00s | +0.31%
0m03.02s | curve25519_32.c | 0m03.32s || -0m00.29s | -9.03%
0m02.78s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.86s || -0m00.08s | -2.79%
0m02.10s | curve25519_64.c | 0m01.93s || +0m00.17s | +8.80%
0m01.62s | p256_64.c | 0m01.63s || -0m00.00s | -0.61%
0m01.52s | secp256k1_64.c | 0m01.44s || +0m00.08s | +5.55%
0m01.38s | p224_64.c | 0m01.70s || -0m00.32s | -18.82%
0m01.34s | CLI.vo | 0m01.42s || -0m00.07s | -5.63%
0m01.16s | StandaloneHaskellMain.vo | 0m01.14s || +0m00.02s | +1.75%
0m01.15s | RewriterProofs.vo | 0m01.14s || +0m00.01s | +0.87%
0m01.00s | StandaloneOCamlMain.vo | 0m01.19s || -0m00.18s | -15.96%
0m00.59s | PushButtonSynthesis/LegacySynthesisTactics.vo | 0m00.68s || -0m00.09s | -13.23%
0m00.43s | PushButtonSynthesis/ReificationCache.vo | 0m00.53s || -0m00.10s | -18.86%
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This will allow us to write rewrite rules that eagerly evaluate
recursion principles on the RHS.
After | File Name | Before || Change | % Change
-----------------------------------------------------------------------------------------------------------
35m52.89s | Total | 35m21.19s || +0m31.69s | +1.49%
-----------------------------------------------------------------------------------------------------------
1m03.44s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m52.51s || +0m10.92s | +20.81%
0m42.76s | UnderLetsProofs.vo | 0m37.59s || +0m05.16s | +13.75%
1m50.02s | RewriterRulesInterpGood.vo | 1m46.65s || +0m03.37s | +3.15%
3m14.40s | p384_32.c | 3m16.54s || -0m02.13s | -1.08%
1m53.47s | RewriterRulesGood.vo | 1m56.16s || -0m02.68s | -2.31%
0m34.80s | AbstractInterpretationZRangeProofs.vo | 0m32.33s || +0m02.46s | +7.63%
0m22.80s | ExtractionOCaml/word_by_word_montgomery | 0m20.53s || +0m02.26s | +11.05%
2m55.61s | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m53.77s || +0m01.84s | +1.05%
2m37.56s | Fancy/Compiler.vo | 2m39.51s || -0m01.94s | -1.22%
1m47.71s | Fancy/Barrett256.vo | 1m46.42s || +0m01.29s | +1.21%
0m59.28s | ExtractionHaskell/word_by_word_montgomery | 0m57.33s || +0m01.95s | +3.40%
0m42.71s | LanguageInversion.vo | 0m40.75s || +0m01.96s | +4.80%
0m40.95s | ExtractionHaskell/unsaturated_solinas | 0m39.76s || +0m01.19s | +2.99%
0m32.88s | AbstractInterpretationProofs.vo | 0m31.38s || +0m01.50s | +4.78%
0m28.98s | PushButtonSynthesis/MontgomeryReductionReificationCache.vo | 0m27.08s || +0m01.90s | +7.01%
0m17.39s | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m18.95s || -0m01.55s | -8.23%
0m12.51s | GENERATEDIdentifiersWithoutTypes.vo | 0m11.11s || +0m01.40s | +12.60%
0m12.30s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.84s || -0m01.53s | -11.12%
0m07.16s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.67s || +0m01.49s | +26.27%
0m05.84s | ExtractionHaskell/saturated_solinas.hs | 0m04.84s || +0m01.00s | +20.66%
2m01.25s | RewriterWf2.vo | 2m01.06s || +0m00.18s | +0.15%
1m22.67s | Rewriter.vo | 1m22.48s || +0m00.18s | +0.23%
0m54.42s | AbstractInterpretationWf.vo | 0m55.26s || -0m00.83s | -1.52%
0m53.40s | RewriterInterpProofs1.vo | 0m52.85s || +0m00.54s | +1.04%
0m46.26s | p521_32.c | 0m46.58s || -0m00.32s | -0.68%
0m44.94s | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m45.20s || -0m00.26s | -0.57%
0m40.17s | p521_64.c | 0m39.49s || +0m00.67s | +1.72%
0m37.93s | Fancy/Montgomery256.vo | 0m37.31s || +0m00.61s | +1.66%
0m36.59s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.22s || +0m00.37s | +1.02%
0m30.06s | ExtractionHaskell/saturated_solinas | 0m29.33s || +0m00.73s | +2.48%
0m29.61s | LanguageWf.vo | 0m29.48s || +0m00.12s | +0.44%
0m26.76s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.77s || -0m00.00s | -0.03%
0m26.23s | SlowPrimeSynthesisExamples.vo | 0m26.36s || -0m00.12s | -0.49%
0m25.30s | RewriterWf1.vo | 0m25.47s || -0m00.16s | -0.66%
0m20.01s | p448_solinas_64.c | 0m19.97s || +0m00.04s | +0.20%
0m19.56s | p256_32.c | 0m20.04s || -0m00.48s | -2.39%
0m19.28s | secp256k1_32.c | 0m18.86s || +0m00.42s | +2.22%
0m16.08s | CStringification.vo | 0m15.70s || +0m00.37s | +2.42%
0m16.04s | p434_64.c | 0m15.20s || +0m00.83s | +5.52%
0m13.39s | ExtractionOCaml/unsaturated_solinas | 0m13.13s || +0m00.25s | +1.98%
0m09.57s | p224_32.c | 0m08.95s || +0m00.62s | +6.92%
0m09.27s | ExtractionOCaml/saturated_solinas | 0m10.22s || -0m00.95s | -9.29%
0m08.70s | p384_64.c | 0m07.93s || +0m00.76s | +9.70%
0m08.43s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.07s || -0m00.64s | -7.05%
0m07.44s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.35s || -0m00.90s | -10.89%
0m06.97s | ExtractionOCaml/saturated_solinas.ml | 0m07.28s || -0m00.31s | -4.25%
0m06.81s | BoundsPipeline.vo | 0m06.78s || +0m00.02s | +0.44%
0m06.72s | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m06.85s || -0m00.12s | -1.89%
0m05.77s | Fancy/Prod.vo | 0m06.07s || -0m00.30s | -4.94%
0m04.06s | MiscCompilerPassesProofs.vo | 0m03.84s || +0m00.21s | +5.72%
0m03.71s | PushButtonSynthesis/Primitives.vo | 0m03.34s || +0m00.37s | +11.07%
0m03.34s | PushButtonSynthesis/SmallExamples.vo | 0m03.26s || +0m00.08s | +2.45%
0m03.16s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || -0m00.06s | -1.86%
0m03.15s | PushButtonSynthesis/BarrettReduction.vo | 0m03.29s || -0m00.14s | -4.25%
0m02.84s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.90s || -0m00.06s | -2.06%
0m02.79s | curve25519_32.c | 0m02.92s || -0m00.12s | -4.45%
0m02.12s | curve25519_64.c | 0m02.13s || -0m00.00s | -0.46%
0m01.70s | secp256k1_64.c | 0m01.55s || +0m00.14s | +9.67%
0m01.64s | p256_64.c | 0m01.23s || +0m00.40s | +33.33%
0m01.57s | p224_64.c | 0m01.68s || -0m00.10s | -6.54%
0m01.36s | Language.vo | 0m01.33s || +0m00.03s | +2.25%
0m01.33s | CLI.vo | 0m01.32s || +0m00.01s | +0.75%
0m01.26s | AbstractInterpretation.vo | 0m01.25s || +0m00.01s | +0.80%
0m01.13s | RewriterProofs.vo | 0m01.18s || -0m00.05s | -4.23%
0m01.13s | StandaloneOCamlMain.vo | 0m01.04s || +0m00.08s | +8.65%
0m01.10s | CompilersTestCases.vo | 0m01.16s || -0m00.05s | -5.17%
0m01.04s | StandaloneHaskellMain.vo | 0m01.18s || -0m00.13s | -11.86%
0m00.76s | MiscCompilerPasses.vo | 0m00.74s || +0m00.02s | +2.70%
0m00.60s | PushButtonSynthesis/LegacySynthesisTactics.vo | 0m00.66s || -0m00.06s | -9.09%
0m00.46s | UnderLets.vo | 0m00.48s || -0m00.01s | -4.16%
0m00.44s | PushButtonSynthesis/ReificationCache.vo | 0m00.52s || -0m00.08s | -15.38%
|
|
|
|
| |
This is needed to reify statements for the rewriter.
|
|
|
|
| |
These will be useful for extending the AST with `option` types.
|
|
|