diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-12 16:25:17 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-12 16:48:18 -0700 |
| commit | 7d6041c9b25536fcc0cfe94f1fb311ddd42993dc (patch) | |
| tree | 9577259264ca646d2c26c20f01b6f1c067648642 /src/Testbit.v | |
| parent | bfccc241c5bbbdd479d06c1db05834b1e719e8f6 (diff) | |
Weaker UniformBase assumptions
After | File Name | Before || Change
----------------------------------------------------------------------------------
0m59.51s | Total | 0m59.14s || +0m00.37s
----------------------------------------------------------------------------------
0m16.46s | ModularArithmetic/ModularBaseSystemProofs | 0m16.45s || +0m00.01s
0m14.41s | Specific/GF25519 | 0m14.36s || +0m00.05s
0m08.35s | ModularArithmetic/Pow2BaseProofs | 0m08.58s || -0m00.23s
0m04.71s | Testbit | 0m04.33s || +0m00.37s
0m03.41s | Experiments/SpecificCurve25519 | 0m03.31s || +0m00.10s
0m02.09s | Specific/GF1305 | 0m02.05s || +0m00.04s
0m02.02s | ModularArithmetic/ModularBaseSystemOpt | 0m02.09s || -0m00.06s
0m01.71s | ModularArithmetic/BarrettReduction/ZBounded | 0m01.70s || +0m00.01s
0m01.15s | ModularArithmetic/ExtendedBaseVector | 0m01.16s || -0m00.01s
0m00.91s | ModularArithmetic/Montgomery/ZBounded | 0m00.84s || +0m00.07s
0m00.90s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.92s || -0m00.02s
0m00.86s | ModularArithmetic/ModularBaseSystemField | 0m00.90s || -0m00.04s
0m00.69s | ModularArithmetic/ModularBaseSystemList | 0m00.61s || +0m00.07s
0m00.65s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.66s || -0m00.01s
0m00.61s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.04s
0m00.59s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.62s || -0m00.03s
Diffstat (limited to 'src/Testbit.v')
| -rw-r--r-- | src/Testbit.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Testbit.v b/src/Testbit.v index 6bc693fae..c7e698e04 100644 --- a/src/Testbit.v +++ b/src/Testbit.v @@ -33,7 +33,7 @@ Section Testbit. | H : ~ (_ = _ :> nat) |- _ => unique pose proof (fun x => H (Nat2Z.inj _ _ x)) | H : (_ = _ :> nat) |- _ => unique pose proof (proj2 (Nat2Z.inj_iff _ _) H) end. - + Lemma testbit_spec' : forall a b us, (0 <= b < width) -> bounded limb_widths us -> (length us = length limb_widths)%nat -> Z.testbit (nth_default 0 us a) b = Z.testbit (decode base us) (Z.of_nat a * width + b). @@ -42,6 +42,8 @@ Section Testbit. | |- _ => progress intros | |- _ => progress autorewrite with push_nth_default Ztestbit zsimplify in * | |- _ => progress change (Z.of_nat 0) with 0 in * + | [ H : In ?x ?ls, H' : forall x', In x' ?ls -> x' = _ |- _ ] + => is_var x; apply H' in H | |- _ => rewrite Nat2Z.inj_succ, Z.mul_succ_l | |- _ => rewrite nth_default_out_of_bounds by omega | |- _ => rewrite nth_default_uniform_base by omega |