diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-09 18:06:40 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-08-13 13:13:58 -0400 |
| commit | f8f1b283f8e75bfec0430c3d048358ec1db21af4 (patch) | |
| tree | f27a4d9b59e31dd512786cb0e3b89593a6c303ff /src/Experiments | |
| parent | a22af596b7136910f521eb0a79af20e88c8b5dd1 (diff) | |
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%
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesGood.v | 8 |
1 files changed, 2 insertions, 6 deletions
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) |