diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-16 00:24:19 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-16 16:51:11 -0500 |
| commit | 4441785fb44b88bb6943ddbf639d872c8c903281 (patch) | |
| tree | 880ac538d950628dd526bb63580201f2093c59f0 /src/Rewriter.v | |
| parent | 60bade02ccd577550bfcd5974d3c62a3d40e751a (diff) | |
Constant-propogate 0+x and x+0 after bounds
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
21m22.67s | Total | 21m28.24s || -0m05.56s | -0.43%
--------------------------------------------------------------------------------------------
4m09.95s | PushButtonSynthesis.vo | 4m14.76s || -0m04.81s | -1.88%
3m07.95s | p384_32.c | 3m11.17s || -0m03.21s | -1.68%
2m06.43s | Rewriter.vo | 2m06.15s || +0m00.28s | +0.22%
1m55.83s | RewriterWf2.vo | 1m56.15s || -0m00.32s | -0.27%
1m52.36s | RewriterRulesGood.vo | 1m52.34s || +0m00.01s | +0.01%
1m46.52s | RewriterRulesInterpGood.vo | 1m45.70s || +0m00.82s | +0.77%
0m46.56s | RewriterInterpProofs1.vo | 0m46.72s || -0m00.15s | -0.34%
0m45.04s | ExtractionHaskell/word_by_word_montgomery | 0m45.33s || -0m00.28s | -0.63%
0m39.17s | p521_32.c | 0m39.07s || +0m00.10s | +0.25%
0m32.40s | p521_64.c | 0m32.64s || -0m00.24s | -0.73%
0m31.13s | ExtractionHaskell/unsaturated_solinas | 0m30.88s || +0m00.25s | +0.80%
0m24.20s | ExtractionHaskell/saturated_solinas | 0m24.27s || -0m00.07s | -0.28%
0m23.72s | RewriterWf1.vo | 0m23.42s || +0m00.29s | +1.28%
0m17.52s | ExtractionOCaml/word_by_word_montgomery | 0m17.10s || +0m00.41s | +2.45%
0m13.39s | secp256k1_32.c | 0m13.29s || +0m00.10s | +0.75%
0m13.08s | p256_32.c | 0m13.26s || -0m00.17s | -1.35%
0m11.49s | p484_64.c | 0m11.18s || +0m00.31s | +2.77%
0m10.68s | ExtractionOCaml/unsaturated_solinas | 0m10.64s || +0m00.03s | +0.37%
0m10.11s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.10s || +0m00.00s | +0.09%
0m07.96s | ExtractionOCaml/saturated_solinas | 0m07.95s || +0m00.00s | +0.12%
0m06.81s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.76s || +0m00.04s | +0.73%
0m06.30s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.26s || +0m00.04s | +0.63%
0m06.07s | p224_32.c | 0m05.94s || +0m00.12s | +2.18%
0m06.06s | BoundsPipeline.vo | 0m06.08s || -0m00.02s | -0.32%
0m05.46s | p384_64.c | 0m05.30s || +0m00.16s | +3.01%
0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.18s || +0m00.10s | +1.93%
0m04.97s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.99s || -0m00.02s | -0.40%
0m04.13s | ExtractionHaskell/saturated_solinas.hs | 0m04.10s || +0m00.03s | +0.73%
0m02.34s | curve25519_32.c | 0m02.21s || +0m00.12s | +5.88%
0m01.59s | curve25519_64.c | 0m01.47s || +0m00.12s | +8.16%
0m01.46s | CLI.vo | 0m01.48s || -0m00.02s | -1.35%
0m01.15s | secp256k1_64.c | 0m01.03s || +0m00.11s | +11.65%
0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88%
0m01.14s | StandaloneHaskellMain.vo | 0m01.09s || +0m00.04s | +4.58%
0m01.14s | StandaloneOCamlMain.vo | 0m01.12s || +0m00.01s | +1.78%
0m01.09s | p256_64.c | 0m00.98s || +0m00.11s | +11.22%
0m01.06s | p224_64.c | 0m01.00s || +0m00.06s | +6.00%
Diffstat (limited to 'src/Rewriter.v')
| -rw-r--r-- | src/Rewriter.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Rewriter.v b/src/Rewriter.v index 8bbf13173..fb14b31f0 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -1793,6 +1793,13 @@ Module Compilers. ; make_rewriteo (??') (fun r v => ##(lower r) when lower r =? upper r) ; make_rewriteo + (#?ℤ +' ??') + (fun rp z rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? ZRange.normalize rp)%zrange) + ; make_rewriteo + (??' +' #?ℤ ) + (fun rp rv v z => cst rv v when (z =? 0) && (ZRange.normalize rv <=? ZRange.normalize rp)%zrange) + + ; make_rewriteo (#?ℤ - (-'??')) (fun z rnv rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? -ZRange.normalize rnv)%zrange) ; make_rewriteo (#?ℤ - ?? ) (fun z v => -v when z =? 0) |