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/ModularArithmetic | |
| 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/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 8f115f101..9a31bef59 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -692,8 +692,8 @@ Section BitwiseDecodeEncode. End BitwiseDecodeEncode. Section UniformBase. - Context {width : Z} (limb_width_pos : 0 < width). - Context (limb_widths : list Z) (limb_widths_nonnil : limb_widths <> nil) + Context {width : Z} (limb_width_nonneg : 0 <= width). + Context (limb_widths : list Z) (limb_widths_uniform : forall w, In w limb_widths -> w = width). Local Notation base := (base_from_limb_widths limb_widths). @@ -721,7 +721,6 @@ Section UniformBase. Lemma uniform_limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. Proof. intros. - apply Z.lt_le_incl. replace w with width by (symmetry; auto). assumption. Qed. |