diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-19 18:31:29 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-05-20 10:58:45 -0400 |
| commit | 58972e8383e2e4ee9fab27771bccfffefce828d4 (patch) | |
| tree | e8491bc8bbb4309f6d9d5db74f3432e5f2f1622f /src/Util/ZUtil | |
| parent | e2ff36332b09d66968f4fec90e7b811dd816208a (diff) | |
Add adc -> sbb to arithmetic simplifer
After | File Name | Before || Change
---------------------------------------------------------------------------------------
6m14.04s | Total | 6m23.68s || -0m09.63s
---------------------------------------------------------------------------------------
0m26.28s | Compilers/Z/ArithmeticSimplifierWf | 0m48.67s || -0m22.39s
0m25.64s | Compilers/Z/ArithmeticSimplifierInterp | 0m14.14s || +0m11.50s
2m17.60s | Specific/IntegrationTestLadderstep | 2m17.90s || -0m00.30s
0m56.48s | Compilers/Z/Named/RewriteAddToAdcInterp | 0m55.76s || +0m00.71s
0m54.26s | Specific/IntegrationTestLadderstep130 | 0m54.53s || -0m00.27s
0m15.89s | Specific/IntegrationTestFreeze | 0m15.07s || +0m00.82s
0m11.69s | Specific/IntegrationTestMul | 0m11.78s || -0m00.08s
0m10.62s | Specific/ArithmeticSynthesisTest | 0m10.59s || +0m00.02s
0m10.54s | Specific/IntegrationTestSub | 0m10.55s || -0m00.01s
0m08.98s | Specific/IntegrationTestSquare | 0m09.04s || -0m00.05s
0m06.05s | Arithmetic/Saturated | 0m06.02s || +0m00.03s
0m03.04s | Compilers/Z/RewriteAddToAdcInterp | 0m03.00s || +0m00.04s
0m02.60s | Compilers/Z/Bounds/Pipeline/Definition | 0m02.25s || +0m00.35s
0m01.52s | Util/ZUtil/AddGetCarry | 0m01.50s || +0m00.02s
0m00.74s | Arithmetic/MontgomeryReduction/WordByWord/Definition | 0m00.71s || +0m00.03s
0m00.62s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.78s || -0m00.16s
0m00.59s | Compilers/Z/ArithmeticSimplifier | 0m00.42s || +0m00.17s
0m00.57s | Compilers/Z/Bounds/Pipeline | 0m00.60s || -0m00.03s
0m00.34s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.37s || -0m00.02s
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/AddGetCarry.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v index 0208207b3..34f5f2ea8 100644 --- a/src/Util/ZUtil/AddGetCarry.v +++ b/src/Util/ZUtil/AddGetCarry.v @@ -70,4 +70,8 @@ Module Z. reflexivity. Qed. + Lemma sub_with_borrow_to_add_get_carry c x y + : Z.sub_with_borrow c x y = Z.add_with_carry (-c) x (-y). + Proof. reflexivity. Qed. + End Z. |