From 6dc1781b13e14c64a6e209a0981c03203fdd9e70 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 27 Jul 2016 17:18:30 -0700 Subject: Move most notation level declarations into Util This reveals and prevents notation clashes. Notable breakage: - `x {{ y }}` breaks `Context {forall x, {P x} + {~P x}}.` (@jadephilipoom) - `x [[ y ]]` breaks `destruct x as [[a]|[b]].` (@jadephilipoom) - `O :( A , B ): :?: L ::: R` breaks `((1):nat)` and `constr:(nat)` (@varomodt) After | File Name | Before || Change ------------------------------------------------------------------------------------ 3m16.07s | Total | 3m23.63s || -0m07.55s ------------------------------------------------------------------------------------ 0m16.90s | ModularArithmetic/ModularBaseSystemProofs | 0m19.02s || -0m02.12s 0m03.29s | ModularArithmetic/ModularBaseSystemOpt | 0m05.30s || -0m02.00s 0m12.04s | Experiments/SpecEd25519 | 0m13.89s || -0m01.85s 0m36.02s | CompleteEdwardsCurve/ExtendedCoordinates | 0m36.12s || -0m00.09s 0m34.48s | Specific/GF25519 | 0m34.27s || +0m00.20s 0m15.62s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.76s || -0m00.14s 0m07.36s | Specific/GF1305 | 0m07.34s || +0m00.02s 0m06.64s | Algebra | 0m06.14s || +0m00.50s 0m05.12s | WeierstrassCurve/Pre | 0m05.09s || +0m00.03s 0m04.58s | ModularArithmetic/Tutorial | 0m03.83s || +0m00.75s 0m04.46s | BaseSystemProofs | 0m04.33s || +0m00.12s 0m04.26s | ModularArithmetic/Pow2BaseProofs | 0m05.16s || -0m00.90s 0m03.91s | CompleteEdwardsCurve/Pre | 0m04.62s || -0m00.71s 0m02.75s | Assembly/State | 0m03.12s || -0m00.37s 0m02.55s | Experiments/EdDSARefinement | 0m01.85s || +0m00.69s 0m02.46s | Util/ZUtil | 0m02.45s || +0m00.00s 0m01.86s | Assembly/Wordize | 0m02.02s || -0m00.15s 0m01.68s | ModularArithmetic/ModularArithmeticTheorems | 0m01.68s || +0m00.00s 0m01.67s | ModularArithmetic/PrimeFieldTheorems | 0m01.96s || -0m00.29s 0m01.50s | Encoding/PointEncodingPre | 0m02.20s || -0m00.70s 0m01.46s | ModularArithmetic/BarrettReduction/Z | 0m01.02s || +0m00.43s 0m01.26s | BaseSystem | 0m01.21s || +0m00.05s 0m01.24s | Assembly/Pseudize | 0m01.22s || +0m00.02s 0m01.20s | ModularArithmetic/ExtendedBaseVector | 0m01.86s || -0m00.66s 0m01.04s | Util/IterAssocOp | 0m00.74s || +0m00.30s 0m00.96s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.67s || +0m00.28s 0m00.96s | Assembly/Pipeline | 0m00.65s || +0m00.30s 0m00.93s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.98s || -0m00.04s 0m00.93s | ModularArithmetic/ModularBaseSystemField | 0m00.95s || -0m00.01s 0m00.92s | Util/NumTheoryUtil | 0m01.19s || -0m00.26s 0m00.90s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.89s || +0m00.01s 0m00.82s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.95s || -0m00.13s 0m00.81s | Assembly/QhasmEvalCommon | 0m00.86s || -0m00.04s 0m00.80s | Assembly/StringConversion | 0m00.60s || +0m00.20s 0m00.79s | Assembly/Qhasm | 0m00.54s || +0m00.25s 0m00.73s | Assembly/Pseudo | 0m00.98s || -0m00.25s 0m00.72s | Util/AdditionChainExponentiation | 0m00.92s || -0m00.20s 0m00.69s | Experiments/SpecificCurve25519 | 0m00.72s || -0m00.03s 0m00.65s | Spec/ModularWordEncoding | 0m00.85s || -0m00.19s 0m00.65s | ModularArithmetic/ModularBaseSystemList | 0m00.68s || -0m00.03s 0m00.65s | Assembly/PseudoConversion | 0m00.67s || -0m00.02s 0m00.64s | Encoding/ModularWordEncodingPre | 0m00.62s || +0m00.02s 0m00.64s | Spec/EdDSA | 0m00.93s || -0m00.29s 0m00.64s | Testbit | 0m00.94s || -0m00.29s 0m00.63s | Encoding/ModularWordEncodingTheorems | 0m00.66s || -0m00.03s 0m00.62s | Assembly/AlmostQhasm | 0m00.49s || +0m00.13s 0m00.59s | ModularArithmetic/ModularBaseSystem | 0m00.61s || -0m00.02s 0m00.49s | Spec/WeierstrassCurve | 0m00.43s || +0m00.06s 0m00.49s | Assembly/QhasmUtil | 0m00.51s || -0m00.02s 0m00.49s | ModularArithmetic/Pre | 0m00.47s || +0m00.02s 0m00.47s | Assembly/Vectorize | 0m00.51s || -0m00.04s 0m00.46s | Assembly/AlmostConversion | 0m00.44s || +0m00.02s 0m00.42s | ModularArithmetic/Pow2Base | 0m00.42s || +0m00.00s 0m00.41s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.45s || -0m00.04s 0m00.41s | Spec/ModularArithmetic | 0m00.41s || +0m00.00s 0m00.39s | Spec/CompleteEdwardsCurve | 0m00.41s || -0m00.01s 0m00.03s | Util/Notations | 0m00.03s || +0m00.00s --- src/ModularArithmetic/ModularBaseSystemList.v | 4 ++-- src/ModularArithmetic/ModularBaseSystemProofs.v | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v index b46429fcc..c556427b9 100644 --- a/src/ModularArithmetic/ModularBaseSystemList.v +++ b/src/ModularArithmetic/ModularBaseSystemList.v @@ -14,7 +14,7 @@ Local Open Scope Z_scope. Section Defs. Context `{prm :PseudoMersenneBaseParams} (modulus_multiple : digits). Local Notation base := (base_from_limb_widths limb_widths). - Local Notation "u [ i ]" := (nth_default 0 u i) (at level 40). + Local Notation "u [ i ]" := (nth_default 0 u i). Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us). @@ -68,4 +68,4 @@ Section Defs. Otherwise, it's all zeroes, and the subtractions do nothing. *) map2 (fun x y => x - y) us (map (Z.land and_term) modulus_digits). -End Defs. \ No newline at end of file +End Defs. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index a1370d33e..d740cca17 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -208,7 +208,7 @@ Section PseudoMersenneProofs. split; [ intuition | ]. destruct Hcarry_done as [Hnth_nonneg Hshiftr_0]. apply Z.shiftr_eq_0_iff in Hshiftr_0. - destruct Hshiftr_0 as [nth_0 | []]; [ rewrite nth_0; zero_bounds | ]. + destruct Hshiftr_0 as [nth_0 | [] ]; [ rewrite nth_0; zero_bounds | ]. apply Z.log2_lt_pow2; auto. - rewrite nth_default_out_of_bounds by omega. split; zero_bounds. @@ -482,8 +482,8 @@ Section CanonicalizationProofs. Qed. Hint Rewrite @nth_default_carry using (omega || distr_length; omega) : push_nth_default. - Local Notation "u '[' i ']' " := (nth_default 0 u i) (at level 30). - Local Notation "u '{{' i '}}' " := (carry_sequence (make_chain i) u) (at level 30). + Local Notation "u [ i ]" := (nth_default 0 u i). + Local Notation "u {{ i }}" := (carry_sequence (make_chain i) u) (at level 30). (* Can't rely on [Reserved Notation]: https://coq.inria.fr/bugs/show_bug.cgi?id=4970 *) Lemma bound_during_first_loop : forall i n us, length us = length limb_widths -> -- cgit v1.2.3