From f8f1b283f8e75bfec0430c3d048358ec1db21af4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 9 Aug 2018 18:06:40 -0400 Subject: Finish and enable rule-specific rewriter wf proofs After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 21m00.81s | Total | 18m22.02s || +2m38.79s | +14.40% -------------------------------------------------------------------------------------------------------------------- 3m52.84s | Experiments/NewPipeline/RewriterRulesGood | 1m15.03s || +2m37.81s | +210.32% 1m42.05s | Experiments/NewPipeline/Toplevel2 | 1m38.76s || +0m03.29s | +3.33% 6m00.91s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m58.65s || +0m02.26s | +0.63% 0m20.72s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m22.36s || -0m01.64s | -7.33% 0m13.79s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m15.45s || -0m01.66s | -10.74% 4m31.85s | Experiments/NewPipeline/Toplevel1 | 4m32.73s || -0m00.87s | -0.32% 0m39.20s | p521_32.c | 0m39.40s || -0m00.19s | -0.50% 0m37.30s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m37.02s || +0m00.27s | +0.75% 0m34.47s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m35.06s || -0m00.59s | -1.68% 0m32.64s | p521_64.c | 0m32.90s || -0m00.25s | -0.79% 0m23.65s | p384_32.c | 0m23.64s || +0m00.00s | +0.04% 0m18.84s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m18.62s || +0m00.21s | +1.18% 0m10.50s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m10.46s || +0m00.03s | +0.38% 0m08.62s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.57s || +0m00.04s | +0.58% 0m08.46s | p384_64.c | 0m08.44s || +0m00.02s | +0.23% 0m05.52s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.36s || +0m00.15s | +2.98% 0m05.45s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.44s || +0m00.00s | +0.18% 0m03.94s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m03.98s || -0m00.04s | -1.00% 0m03.88s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.09s || -0m00.20s | -5.13% 0m03.85s | secp256k1_32.c | 0m03.78s || +0m00.07s | +1.85% 0m03.77s | p256_32.c | 0m03.84s || -0m00.06s | -1.82% 0m03.33s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.13s || +0m00.20s | +6.38% 0m02.15s | p224_32.c | 0m02.27s || -0m00.12s | -5.28% 0m02.14s | curve25519_32.c | 0m02.21s || -0m00.06s | -3.16% 0m01.66s | p256_64.c | 0m01.53s || +0m00.12s | +8.49% 0m01.63s | secp256k1_64.c | 0m01.51s || +0m00.11s | +7.94% 0m01.53s | p224_64.c | 0m01.56s || -0m00.03s | -1.92% 0m01.43s | curve25519_64.c | 0m01.43s || +0m00.00s | +0.00% 0m01.30s | Experiments/NewPipeline/CLI | 0m01.41s || -0m00.10s | -7.80% 0m01.28s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.21s || +0m00.07s | +5.78% 0m01.20s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.23s || -0m00.03s | -2.43% 0m00.92s | Experiments/NewPipeline/RewriterProofs | 0m00.96s || -0m00.03s | -4.16% --- src/Experiments/NewPipeline/RewriterRulesGood.v | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'src/Experiments') diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v index 3bdfa9913..ef087686a 100644 --- a/src/Experiments/NewPipeline/RewriterRulesGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesGood.v @@ -554,20 +554,16 @@ Module Compilers. Lemma nbe_rewrite_rules_good : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules. Proof. - (* Time start_good (@nbe_cps_id) (@nbe_rewrite_rules). Time all: repeat repeat good_t_step. - *) - Admitted. + Qed. Lemma arith_rewrite_rules_good max_const : rewrite_rules_goodT (arith_rewrite_rules max_const) (arith_rewrite_rules max_const). Proof. - (* Time start_good (@arith_cps_id) (@arith_rewrite_rules). Time all: repeat good_t_step. - *) - Admitted. + Qed. Lemma fancy_rewrite_rules_good (invert_low invert_high : Z -> Z -> option Z) -- cgit v1.2.3