diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-09 19:50:04 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-09 19:57:42 -0400 |
commit | ca5402e5c10d5283869229c2765349a553033a98 (patch) | |
tree | 68204f64bd4b30d1932b5b69708223184fcbb7c9 | |
parent | 1eb3ce168f8ec11821c14bf856cdd0725b236cc0 (diff) |
Add a Ztestbit_full database
After | File Name | Before || Change
---------------------------------------------------------------------------------------------
6m00.58s | Total | 6m23.23s || -0m22.64s
---------------------------------------------------------------------------------------------
0m35.50s | ModularArithmetic/Conversion | 0m39.25s || -0m03.75s
1m35.19s | Test/Curve25519SpecTestVectors | 1m38.04s || -0m02.84s
0m06.69s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | 0m08.83s || -0m02.13s
0m27.51s | ModularArithmetic/ModularBaseSystemProofs | 0m28.99s || -0m01.47s
0m08.13s | Encoding/PointEncoding | 0m09.64s || -0m01.50s
0m05.25s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | 0m06.96s || -0m01.71s
0m22.82s | ModularArithmetic/Pow2BaseProofs | 0m23.37s || -0m00.55s
0m20.17s | EdDSARepChange | 0m20.89s || -0m00.71s
0m14.41s | Specific/GF25519 | 0m14.81s || -0m00.40s
0m13.08s | Util/ZUtil | 0m13.30s || -0m00.22s
0m10.31s | Testbit | 0m10.50s || -0m00.18s
0m09.57s | ModularArithmetic/Montgomery/ZProofs | 0m09.74s || -0m00.16s
0m08.46s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.68s || -0m00.21s
0m08.16s | BoundedArithmetic/Double/Proofs/Multiply | 0m09.02s || -0m00.85s
0m07.64s | Specific/GF1305 | 0m07.94s || -0m00.30s
0m04.01s | ModularArithmetic/Tutorial | 0m03.61s || +0m00.39s
0m03.91s | BaseSystemProofs | 0m04.01s || -0m00.09s
0m03.86s | ModularArithmetic/BarrettReduction/ZHandbook | 0m04.40s || -0m00.54s
0m03.46s | ModularArithmetic/ModularBaseSystemListProofs | 0m03.65s || -0m00.18s
0m03.37s | BoundedArithmetic/InterfaceProofs | 0m03.98s || -0m00.60s
0m03.28s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.78s || -0m00.50s
0m02.86s | Encoding/PointEncodingPre | 0m03.22s || -0m00.36s
0m02.78s | BoundedArithmetic/Double/Proofs/Decode | 0m03.25s || -0m00.47s
0m02.78s | ModularArithmetic/ModularArithmeticTheorems | 0m03.42s || -0m00.64s
0m02.31s | ModularArithmetic/ModularBaseSystemOpt | 0m02.38s || -0m00.06s
0m02.26s | Specific/FancyMachine256/Barrett | 0m02.80s || -0m00.54s
0m02.22s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.54s || -0m00.31s
0m02.07s | Specific/FancyMachine256/Montgomery | 0m02.31s || -0m00.24s
0m01.83s | ModularArithmetic/Montgomery/ZBounded | 0m02.12s || -0m00.29s
0m01.78s | Specific/FancyMachine256/Core | 0m01.78s || +0m00.00s
0m01.70s | ModularArithmetic/PrimeFieldTheorems | 0m01.38s || +0m00.32s
0m01.52s | ModularArithmetic/BarrettReduction/Z | 0m01.88s || -0m00.35s
0m01.38s | BaseSystem | 0m01.40s || -0m00.02s
0m01.24s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.16s || +0m00.08s
0m01.10s | ModularArithmetic/ExtendedBaseVector | 0m01.20s || -0m00.09s
0m01.05s | Util/NumTheoryUtil | 0m01.01s || +0m00.04s
0m00.88s | Experiments/EncodingLemmas | 0m00.93s || -0m00.05s
0m00.86s | BoundedArithmetic/Double/Proofs/LoadImmediate | 0m00.92s || -0m00.06s
0m00.84s | BoundedArithmetic/Double/Proofs/BitwiseOr | 0m01.19s || -0m00.35s
0m00.80s | Encoding/ModularWordEncodingPre | 0m00.61s || +0m00.19s
0m00.78s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.75s || +0m00.03s
0m00.71s | BoundedArithmetic/X86ToZLike | 0m00.89s || -0m00.18s
0m00.67s | Encoding/ModularWordEncodingTheorems | 0m00.72s || -0m00.04s
0m00.62s | BoundedArithmetic/Interface | 0m00.66s || -0m00.04s
0m00.62s | Spec/EdDSA | 0m00.59s || +0m00.03s
0m00.61s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.74s || -0m00.13s
0m00.61s | Spec/ModularWordEncoding | 0m00.69s || -0m00.07s
0m00.61s | ModularArithmetic/ModularBaseSystemList | 0m00.65s || -0m00.04s
0m00.60s | BoundedArithmetic/Double/Core | 0m00.49s || +0m00.10s
0m00.60s | Spec/Ed25519 | 0m00.50s || +0m00.09s
0m00.58s | ModularArithmetic/ModularBaseSystem | 0m00.62s || -0m00.04s
0m00.55s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.63s || -0m00.07s
0m00.53s | BoundedArithmetic/Double/Proofs/SelectConditional | 0m00.62s || -0m00.08s
0m00.51s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.55s || -0m00.04s
0m00.50s | BoundedArithmetic/StripCF | 0m00.51s || -0m00.01s
0m00.50s | BoundedArithmetic/ArchitectureToZLike | 0m00.48s || +0m00.02s
0m00.49s | ModularArithmetic/Pre | 0m00.47s || +0m00.02s
0m00.49s | BoundedArithmetic/Double/Repeated/Core | 0m00.48s || +0m00.01s
0m00.48s | ModularArithmetic/ZBounded | 0m00.50s || -0m00.02s
0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.54s || -0m00.08s
0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.54s || -0m00.08s
0m00.44s | ModularArithmetic/Pow2Base | 0m00.49s || -0m00.04s
0m00.40s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.44s || -0m00.03s
0m00.38s | ModularArithmetic/Montgomery/Z | 0m00.44s || -0m00.06s
0m00.35s | Spec/ModularArithmetic | 0m00.36s || -0m00.01s
-rw-r--r-- | src/Util/ZUtil.v | 48 |
1 files changed, 46 insertions, 2 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 8d482d1ee..c98b63554 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -203,8 +203,10 @@ Ltac zify_nat_op ::= end. Create HintDb Ztestbit discriminated. -Hint Rewrite Z.testbit_0_l : Ztestbit. -Hint Rewrite Z.land_spec Z.lor_spec Z.shiftl_spec Z.shiftr_spec using zutil_arith : Ztestbit. +Create HintDb Ztestbit_full discriminated. +Hint Rewrite Z.testbit_0_l Z.land_spec Z.lor_spec : Ztestbit. +Hint Rewrite Z.testbit_0_l Z.land_spec Z.lor_spec : Ztestbit_full. +Hint Rewrite Z.shiftl_spec Z.shiftr_spec using zutil_arith : Ztestbit. Hint Rewrite Z.testbit_neg_r using zutil_arith : Ztestbit. Hint Rewrite Bool.andb_true_r Bool.andb_false_r Bool.orb_true_r Bool.orb_false_r Bool.andb_true_l Bool.andb_false_l Bool.orb_true_l Bool.orb_false_l : Ztestbit. @@ -247,6 +249,22 @@ Module Z. Qed. Hint Rewrite ones_spec using zutil_arith : Ztestbit. + Lemma ones_spec_full : forall n m, Z.testbit (Z.ones n) m + = if Z_lt_dec m 0 + then false + else if Z_lt_dec n 0 + then true + else if Z_lt_dec m n then true else false. + Proof. + intros. + repeat (break_if || autorewrite with Ztestbit); try reflexivity; try omega. + unfold Z.ones. + rewrite <- Z.shiftr_opp_r, Z.shiftr_eq_0 by (simpl; omega); simpl. + destruct m; simpl in *; try reflexivity. + exfalso; auto using Zlt_neg_0. + Qed. + Hint Rewrite ones_spec_full : Ztestbit_full. + Lemma testbit_pow2_mod : forall a n i, 0 <= n -> Z.testbit (Z.pow2_mod a n) i = if Z_lt_dec i n then Z.testbit a i else false. Proof. @@ -261,6 +279,20 @@ Module Z. Qed. Hint Rewrite testbit_pow2_mod using zutil_arith : Ztestbit. + Lemma testbit_pow2_mod_full : forall a n i, + Z.testbit (Z.pow2_mod a n) i = if Z_lt_dec n 0 + then if Z_lt_dec i 0 then false else Z.testbit a i + else if Z_lt_dec i n then Z.testbit a i else false. + Proof. + intros; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ]. + unfold pow2_mod. + autorewrite with Ztestbit_full; + repeat break_match; + autorewrite with Ztestbit; + reflexivity. + Qed. + Hint Rewrite testbit_pow2_mod_full : Ztestbit_full. + Lemma bits_above_pow2 a n : 0 <= a < 2^n -> Z.testbit a n = false. Proof. intros. @@ -824,6 +856,17 @@ Module Z. Qed. Hint Rewrite shiftl_spec_full : Ztestbit. + Lemma shiftr_spec_full a n m + : Z.testbit (a << n) m = if Z_lt_dec m n + then false + else if Z_le_dec 0 m + then Z.testbit a (m - n) + else false. + Proof. + repeat break_match; auto using Z.shiftl_spec_low, Z.shiftl_spec, Z.testbit_neg_r with omega. + Qed. + Hint Rewrite shiftl_spec_full : Ztestbit. + (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *) Ltac zero_bounds' := repeat match goal with @@ -2817,4 +2860,5 @@ Ltac Ztestbit := => rewrite (Z.bits_above_pow2 x y) by zutil_arith | [ |- context[Z.testbit ?x ?y] ] => rewrite (Z.bits_above_log2 x y) by zutil_arith + | _ => progress autorewrite with Ztestbit_full end. |