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/Testbit.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/Testbit.v') 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 -- cgit v1.2.3