From bacfa270c0c492ef8518d360d87e46cee292474f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 12 Mar 2019 22:55:21 -0400 Subject: Factor out rewriter rules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Move rewrite rule definitions, and the proofs about them, into separate files. We don't yet make use of the separate interp proofs of rewrite rules; the next step is to refactor the interp proof machinery so that we can easily prove the relevant interp relations, given the equality proofs in `src/RewriterRulesProofs.v` After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 23m01.93s | Total | 22m37.08s || +0m24.84s | +1.83% -------------------------------------------------------------------------------------------- 0m24.10s | RewriterRulesProofs.vo | N/A || +0m24.10s | ∞ 1m12.13s | Rewriter.vo | 1m20.61s || -0m08.48s | -10.51% 0m41.17s | ExtractionHaskell/unsaturated_solinas | 0m37.57s || +0m03.60s | +9.58% 1m42.40s | Fancy/Barrett256.vo | 1m40.22s || +0m02.18s | +2.17% 0m45.56s | p521_32.c | 0m48.16s || -0m02.59s | -5.39% 0m14.48s | ExtractionOCaml/word_by_word_montgomery.ml | 0m12.47s || +0m02.00s | +16.11% 1m48.48s | RewriterWf2.vo | 1m46.70s || +0m01.77s | +1.66% 0m15.06s | ExtractionOCaml/unsaturated_solinas | 0m14.06s || +0m01.00s | +7.11% 0m06.26s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.29s || -0m01.03s | -14.12% 0m04.71s | ExtractionHaskell/saturated_solinas.hs | 0m06.05s || -0m01.33s | -22.14% 3m22.17s | p384_32.c | 3m23.06s || -0m00.88s | -0.43% 1m57.31s | RewriterRulesInterpGood.vo | 1m56.61s || +0m00.70s | +0.60% 1m35.20s | RewriterRulesGood.vo | 1m35.80s || -0m00.59s | -0.62% 0m57.50s | ExtractionHaskell/word_by_word_montgomery | 0m56.53s || +0m00.96s | +1.71% 0m45.71s | RewriterInterpProofs1.vo | 0m46.13s || -0m00.42s | -0.91% 0m39.66s | p521_64.c | 0m38.90s || +0m00.75s | +1.95% 0m36.22s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.42s || -0m00.20s | -0.54% 0m34.39s | Fancy/Montgomery256.vo | 0m34.45s || -0m00.06s | -0.17% 0m33.16s | RewriterWf1.vo | 0m32.96s || +0m00.19s | +0.60% 0m32.21s | ExtractionHaskell/saturated_solinas | 0m31.53s || +0m00.67s | +2.15% 0m26.94s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.20s || -0m00.25s | -0.95% 0m25.89s | SlowPrimeSynthesisExamples.vo | 0m25.59s || +0m00.30s | +1.17% 0m23.37s | ExtractionOCaml/word_by_word_montgomery | 0m22.90s || +0m00.47s | +2.05% 0m21.19s | PushButtonSynthesis/BarrettReduction.vo | 0m20.79s || +0m00.40s | +1.92% 0m18.30s | p256_32.c | 0m18.54s || -0m00.23s | -1.29% 0m18.29s | p448_solinas_64.c | 0m18.58s || -0m00.28s | -1.56% 0m17.92s | secp256k1_32.c | 0m18.41s || -0m00.48s | -2.66% 0m14.06s | p434_64.c | 0m13.92s || +0m00.14s | +1.00% 0m11.61s | ExtractionOCaml/saturated_solinas | 0m11.57s || +0m00.03s | +0.34% 0m08.90s | p224_32.c | 0m09.12s || -0m00.21s | -2.41% 0m08.49s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.85s || -0m00.35s | -4.06% 0m08.45s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.62s || -0m00.16s | -1.97% 0m08.02s | p384_64.c | 0m07.04s || +0m00.97s | +13.92% 0m07.01s | ExtractionOCaml/saturated_solinas.ml | 0m06.57s || +0m00.43s | +6.69% 0m06.67s | BoundsPipeline.vo | 0m06.87s || -0m00.20s | -2.91% 0m03.39s | PushButtonSynthesis/Primitives.vo | 0m03.44s || -0m00.04s | -1.45% 0m03.36s | PushButtonSynthesis/SmallExamples.vo | 0m03.38s || -0m00.02s | -0.59% 0m03.23s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.21s || +0m00.02s | +0.62% 0m03.04s | curve25519_32.c | 0m02.68s || +0m00.35s | +13.43% 0m02.74s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.55s || +0m00.19s | +7.45% 0m02.19s | curve25519_64.c | 0m01.81s || +0m00.37s | +20.99% 0m01.72s | secp256k1_64.c | 0m01.46s || +0m00.26s | +17.80% 0m01.56s | p256_64.c | 0m01.22s || +0m00.34s | +27.86% 0m01.49s | p224_64.c | 0m01.56s || -0m00.07s | -4.48% 0m01.32s | CLI.vo | 0m01.32s || +0m00.00s | +0.00% 0m01.14s | StandaloneHaskellMain.vo | 0m01.08s || +0m00.05s | +5.55% 0m01.06s | CompilersTestCases.vo | 0m01.04s || +0m00.02s | +1.92% 0m01.06s | StandaloneOCamlMain.vo | 0m01.12s || -0m00.06s | -5.35% 0m01.00s | RewriterProofs.vo | 0m01.13s || -0m00.12s | -11.50% 0m00.64s | RewriterRules.vo | N/A || +0m00.64s | ∞ --- _CoqProject | 2 ++ 1 file changed, 2 insertions(+) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 8fadf2f12..8c26d122b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -37,8 +37,10 @@ src/MiscCompilerPassesProofs.v src/Rewriter.v src/RewriterInterpProofs1.v src/RewriterProofs.v +src/RewriterRules.v src/RewriterRulesGood.v src/RewriterRulesInterpGood.v +src/RewriterRulesProofs.v src/RewriterWf1.v src/RewriterWf2.v src/SlowPrimeSynthesisExamples.v -- cgit v1.2.3