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/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 6 +++--- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 14 +++++++------- 2 files changed, 10 insertions(+), 10 deletions(-) (limited to 'src/CompleteEdwardsCurve') diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index dbfdb023e..716d72b3e 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -34,7 +34,7 @@ Module E. let x := fresh "x" p in let y := fresh "y" p in let pf := fresh "pf" p in - destruct p as [[x y] pf] + destruct p as [ [x y] pf] end. Local Obligation Tactic := intros; destruct_points; simpl; super_nsatz. @@ -155,7 +155,7 @@ Module E. Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ ( let (x, y) := coordinates P in (phi x, phi y)) _. Next Obligation. - destruct P as [[? ?] ?]; simpl. + destruct P as [ [? ?] ?]; simpl. rewrite_strat bottomup hints field_homomorphism. eauto using is_homomorphism_phi_proper; assumption. Qed. @@ -171,7 +171,7 @@ Module E. | |- _ => intro | |- _ /\ _ => split | [H: _ /\ _ |- _ ] => destruct H - | [p: point |- _ ] => destruct p as [[??]?] + | [p: point |- _ ] => destruct p as [ [??]?] | |- context[point_phi] => setoid_rewrite point_phi_correct | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp ref_phi] in * | |- Keq ?x ?x => reflexivity diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index ac3523889..6b28173e3 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -39,8 +39,8 @@ Module Extended. | |- Proper _ _ => intro | _ => progress intros | [ H: _ /\ _ |- _ ] => destruct H - | [ p:E.point |- _ ] => destruct p as [[??]?] - | [ p:point |- _ ] => destruct p as [[[[??]?]?]?] + | [ p:E.point |- _ ] => destruct p as [ [??] ? ] + | [ p:point |- _ ] => destruct p as [ [ [ [??] ? ] ? ] ? ] | _ => progress autounfold with bash in * | |- _ /\ _ => split | _ => solve [neq01] @@ -98,7 +98,7 @@ Module Extended. let (x, y) := E.coordinates (E.add (to_twisted P) (to_twisted Q)) in (fieldwise (n:=2) Feq) (x, y) (X/Z, Y/Z). Proof. - destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]]. + destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ]. pose proof edwardsAddCompletePlus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ. pose proof edwardsAddCompleteMinus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ. bash. @@ -110,7 +110,7 @@ Module Extended. intros. pose proof (add_coordinates_correct P Q) as Hrep. pose proof Pre.unifiedAdd'_onCurve(a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) (E.coordinates (to_twisted P)) (E.coordinates (to_twisted Q)) as Hon. - destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]]. + destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ]. pose proof edwardsAddCompletePlus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ as Hnz1. pose proof edwardsAddCompleteMinus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ as Hnz2. autounfold with bash in *; simpl in *. @@ -122,7 +122,7 @@ Module Extended. Lemma to_twisted_add P Q : E.eq (to_twisted (add P Q)) (E.add (to_twisted P) (to_twisted Q)). Proof. pose proof (add_coordinates_correct P Q) as Hrep. - destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]]. + destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ]. autounfold with bash in *; simpl in *. destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB. split; reflexivity. @@ -230,7 +230,7 @@ Module Extended. Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ ( let '(X, Y, Z, T) := coordinates P in (phi X, phi Y, phi Z, phi T)) _. Next Obligation. - destruct P as [[[[] ?] ?] [? [? ?]]]; unfold onCurve in *; simpl. + destruct P as [ [ [ [ ] ? ] ? ] [ ? [ ? ? ] ] ]; unfold onCurve in *; simpl. (rewrite_strat bottomup hints field_homomorphism); try assumption. eauto 10 using is_homomorphism_phi_proper, phi_nonzero. Qed. @@ -246,7 +246,7 @@ Module Extended. | |- _ => intro | |- _ /\ _ => split | [H: _ /\ _ |- _ ] => destruct H - | [p: point |- _ ] => destruct p as [[[[] ?] ?] [? [? ?]]] + | [p: point |- _ ] => destruct p as [ [ [ [ ] ? ] ? ] [ ? [ ? ? ] ] ] | |- context[point_phi] => setoid_rewrite point_phi_correct | |- _ => progress cbv [fst snd coordinates proj1_sig eq to_twisted E.eq E.coordinates fieldwise fieldwise' add add_coordinates ref_phi] in * | |- Keq ?x ?x => reflexivity -- cgit v1.2.3