diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-15 15:49:44 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-15 15:53:43 -0700 |
| commit | 322dda59271e397c091a6329139f5b6ed820de7c (patch) | |
| tree | 9b2bd2ead0f36506b26dfd4dbde59bbdd35aa5c8 /src/Util/ZUtil.v | |
| parent | fc7d760073953304f56f9e034ce3d54e3153a3c7 (diff) | |
Support shiftl in Zshift_to_pow
After | File Name | Before || Change
----------------------------------------------------------------------------------
1m50.24s | Total | 1m51.62s || -0m01.37s
----------------------------------------------------------------------------------
0m16.95s | ModularArithmetic/ModularBaseSystemProofs | 0m16.87s || +0m00.07s
0m14.88s | Specific/GF25519 | 0m14.70s || +0m00.18s
0m13.67s | Experiments/SpecEd25519 | 0m13.66s || +0m00.00s
0m08.99s | ModularArithmetic/Pow2BaseProofs | 0m09.51s || -0m00.51s
0m06.83s | ModularArithmetic/Montgomery/ZProofs | 0m06.86s || -0m00.03s
0m04.81s | Testbit | 0m05.06s || -0m00.25s
0m03.77s | BaseSystemProofs | 0m03.92s || -0m00.14s
0m03.53s | ModularArithmetic/Tutorial | 0m03.76s || -0m00.23s
0m03.40s | Util/ZUtil | 0m03.36s || +0m00.04s
0m03.24s | Experiments/SpecificCurve25519 | 0m03.31s || -0m00.06s
0m02.75s | ModularArithmetic/BarrettReduction/ZHandbook | 0m02.80s || -0m00.04s
0m02.21s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.24s || -0m00.03s
0m02.16s | Specific/GF1305 | 0m02.11s || +0m00.05s
0m02.01s | ModularArithmetic/ModularBaseSystemOpt | 0m02.01s || +0m00.00s
0m01.99s | ModularArithmetic/ModularArithmeticTheorems | 0m02.01s || -0m00.01s
0m01.74s | ModularArithmetic/BarrettReduction/ZBounded | 0m01.79s || -0m00.05s
0m01.56s | Encoding/PointEncodingPre | 0m01.59s || -0m00.03s
0m01.23s | ModularArithmetic/BarrettReduction/Z | 0m01.24s || -0m00.01s
0m01.19s | ModularArithmetic/ExtendedBaseVector | 0m01.16s || +0m00.03s
0m01.17s | BaseSystem | 0m01.17s || +0m00.00s
0m01.04s | ModularArithmetic/PrimeFieldTheorems | 0m01.07s || -0m00.03s
0m00.92s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.97s || -0m00.04s
0m00.87s | Util/NumTheoryUtil | 0m00.86s || +0m00.01s
0m00.86s | ModularArithmetic/ModularBaseSystemField | 0m00.86s || +0m00.00s
0m00.85s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.81s || +0m00.03s
0m00.81s | ModularArithmetic/Montgomery/ZBounded | 0m00.87s || -0m00.05s
0m00.70s | Encoding/ModularWordEncodingTheorems | 0m00.74s || -0m00.04s
0m00.65s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.61s || +0m00.04s
0m00.62s | ModularArithmetic/ModularBaseSystemList | 0m00.58s || +0m00.04s
0m00.62s | Encoding/ModularWordEncodingPre | 0m00.65s || -0m00.03s
0m00.57s | ModularArithmetic/ModularBaseSystem | 0m00.54s || +0m00.02s
0m00.56s | Spec/ModularWordEncoding | 0m00.61s || -0m00.04s
0m00.55s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.84s || -0m00.28s
0m00.50s | ModularArithmetic/Pre | 0m00.47s || +0m00.03s
0m00.46s | ModularArithmetic/ZBounded | 0m00.45s || +0m00.01s
0m00.43s | ModularArithmetic/Pow2Base | 0m00.40s || +0m00.02s
0m00.41s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.39s || +0m00.01s
0m00.39s | ModularArithmetic/Montgomery/Z | 0m00.41s || -0m00.01s
0m00.36s | Spec/ModularArithmetic | 0m00.36s || +0m00.00s
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 82e77d0dc..60cb18a67 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -96,7 +96,8 @@ Hint Rewrite <- Z.shiftr_lxor Z.shiftr_land Z.shiftr_lor Z.shiftr_ldiff Z.lnot_s Hint Rewrite Z.shiftr_lxor Z.shiftr_land Z.shiftr_lor Z.shiftr_ldiff Z.lnot_shiftr Z.ldiff_ones_r using zutil_arith : push_Zshift. Hint Rewrite <- Z.shiftr_shiftl_l Z.shiftr_shiftl_r Z.shiftr_shiftr using zutil_arith : push_Zshift. Hint Rewrite Z.shiftr_opp_r Z.shiftl_opp_r Z.shiftr_0_r Z.shiftr_0_l : push_Zshift. -Hint Rewrite Z.shiftr_div_pow2 Z.shiftr_mul_pow2 using zutil_arith : Zshift_to_pow. +Hint Rewrite Z.shiftr_div_pow2 Z.shiftr_mul_pow2 Z.shiftl_opp_r using zutil_arith : Zshift_to_pow. +Hint Rewrite <- Z.shiftr_opp_r using zutil_arith : Zshift_to_pow. Hint Rewrite <- Z.shiftr_div_pow2 Z.shiftr_mul_pow2 using zutil_arith : Zpow_to_shift. (** For the occasional lemma that can remove the use of [Z.div] *) |