From 7d6041c9b25536fcc0cfe94f1fb311ddd42993dc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 12 Aug 2016 16:25:17 -0700 Subject: 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 --- src/ModularArithmetic/Pow2BaseProofs.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'src/ModularArithmetic') 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. -- cgit v1.2.3