aboutsummaryrefslogtreecommitdiff
path: root/src/AbstractInterpretationWf.v
Commit message (Collapse)AuthorAge
* Add a couple more identifiers to support eager recGravatar Jason Gross2019-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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%
* Add support for reifying `zrange` and `option`Gravatar Jason Gross2019-02-18
| | | | This is needed to reify statements for the rewriter.
* Add Option.{lift,map,combine}, List.Option.liftGravatar Jason Gross2019-02-11
| | | | These will be useful for extending the AST with `option` types.
* Insert casts before literals during bounds analysisGravatar Jason Gross2019-02-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unless we explicitly say not to. The ability to explicitly say not to is required for, e.g., eta-expansion where we want to replace variable lists of known length with with cons cells indexing into the variable list, but don't want to pollute the code with casts. Uniformity in this way allows rewrite rules to not blow up exponentially (in the number of wildcards); we previously required a separate rewrite rule for each way of choosing between wildcard and literal. To preserve output of the pipeline, we add another pass that just strips the casts off of literals at the end. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 20m27.24s | Total | 22m39.70s || -2m12.46s | -9.74% -------------------------------------------------------------------------------------------- 0m44.27s | Rewriter.vo | 2m11.58s || -1m27.31s | -66.35% 1m15.23s | RewriterRulesInterpGood.vo | 1m50.28s || -0m35.04s | -31.78% 1m40.19s | RewriterRulesGood.vo | 1m58.05s || -0m17.85s | -15.12% 0m26.99s | AbstractInterpretationProofs.vo | 0m16.91s || +0m10.07s | +59.60% 3m15.98s | p384_32.c | 3m07.78s || +0m08.19s | +4.36% 0m42.52s | ExtractionHaskell/word_by_word_montgomery | 0m44.60s || -0m02.07s | -4.66% 0m28.63s | ExtractionHaskell/unsaturated_solinas | 0m31.38s || -0m02.75s | -8.76% 0m21.76s | ExtractionHaskell/saturated_solinas | 0m24.56s || -0m02.79s | -11.40% 0m09.87s | ExtractionOCaml/unsaturated_solinas | 0m11.28s || -0m01.41s | -12.50% 1m59.22s | RewriterWf2.vo | 2m00.09s || -0m00.87s | -0.72% 1m07.03s | Fancy/Montgomery256.vo | 1m07.31s || -0m00.28s | -0.41% 0m52.60s | Fancy/Barrett256.vo | 0m53.16s || -0m00.55s | -1.05% 0m48.17s | RewriterInterpProofs1.vo | 0m48.72s || -0m00.54s | -1.12% 0m40.16s | AbstractInterpretationWf.vo | 0m40.23s || -0m00.07s | -0.17% 0m38.35s | p521_32.c | 0m38.26s || +0m00.09s | +0.23% 0m31.56s | p521_64.c | 0m31.53s || +0m00.02s | +0.09% 0m24.64s | RewriterWf1.vo | 0m24.01s || +0m00.62s | +2.62% 0m23.54s | AbstractInterpretationZRangeProofs.vo | 0m23.64s || -0m00.10s | -0.42% 0m23.48s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m23.26s || +0m00.21s | +0.94% 0m20.92s | SlowPrimeSynthesisExamples.vo | 0m20.62s || +0m00.30s | +1.45% 0m19.92s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m19.80s || +0m00.12s | +0.60% 0m16.60s | ExtractionOCaml/word_by_word_montgomery | 0m17.56s || -0m00.95s | -5.46% 0m14.72s | p448_solinas_64.c | 0m14.66s || +0m00.06s | +0.40% 0m13.70s | secp256k1_32.c | 0m13.45s || +0m00.25s | +1.85% 0m13.68s | p256_32.c | 0m13.33s || +0m00.34s | +2.62% 0m13.28s | CStringification.vo | 0m13.26s || +0m00.01s | +0.15% 0m11.88s | p484_64.c | 0m11.74s || +0m00.14s | +1.19% 0m09.96s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.24s || -0m00.27s | -2.73% 0m07.47s | ExtractionOCaml/saturated_solinas | 0m07.93s || -0m00.46s | -5.80% 0m06.78s | BoundsPipeline.vo | 0m05.96s || +0m00.82s | +13.75% 0m06.72s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.03s || -0m00.31s | -4.40% 0m06.38s | p224_32.c | 0m06.54s || -0m00.16s | -2.44% 0m06.21s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.34s || -0m00.12s | -2.05% 0m05.45s | p384_64.c | 0m05.18s || +0m00.27s | +5.21% 0m04.82s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.84s || -0m00.01s | -0.41% 0m04.80s | ExtractionOCaml/saturated_solinas.ml | 0m05.07s || -0m00.27s | -5.32% 0m03.83s | ExtractionHaskell/saturated_solinas.hs | 0m04.07s || -0m00.24s | -5.89% 0m03.30s | PushButtonSynthesis/Primitives.vo | 0m03.31s || -0m00.01s | -0.30% 0m03.26s | PushButtonSynthesis/SmallExamples.vo | 0m03.24s || +0m00.01s | +0.61% 0m03.08s | PushButtonSynthesis/SaturatedSolinas.vo | 0m02.96s || +0m00.12s | +4.05% 0m02.16s | curve25519_32.c | 0m02.16s || +0m00.00s | +0.00% 0m01.57s | curve25519_64.c | 0m01.47s || +0m00.10s | +6.80% 0m01.40s | CLI.vo | 0m01.32s || +0m00.07s | +6.06% 0m01.27s | PushButtonSynthesis/MontgomeryReduction.vo | 0m01.19s || +0m00.08s | +6.72% 0m01.26s | StandaloneHaskellMain.vo | 0m01.18s || +0m00.08s | +6.77% 0m01.22s | PushButtonSynthesis/BarrettReduction.vo | 0m01.29s || -0m00.07s | -5.42% 0m01.13s | RewriterProofs.vo | 0m01.10s || +0m00.02s | +2.72% 0m01.10s | secp256k1_64.c | 0m01.01s || +0m00.09s | +8.91% 0m01.08s | StandaloneOCamlMain.vo | 0m01.13s || -0m00.04s | -4.42% 0m01.06s | p256_64.c | 0m01.02s || +0m00.04s | +3.92% 0m01.05s | AbstractInterpretation.vo | 0m01.00s || +0m00.05s | +5.00% 0m01.00s | CompilersTestCases.vo | 0m01.08s || -0m00.08s | -7.40% 0m01.00s | p224_64.c | 0m01.00s || +0m00.00s | +0.00%
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 09:14:16 +0000