diff options
-rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 34 | ||||
-rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 10 | ||||
-rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 22 | ||||
-rw-r--r-- | src/Encoding/EncodingTheorems.v | 2 | ||||
-rw-r--r-- | src/Encoding/ModularWordEncodingTheorems.v | 2 | ||||
-rw-r--r-- | src/Experiments/DerivationsOptionRectLetInEncoding.v | 6 | ||||
-rw-r--r-- | src/ModularArithmetic/ExtendedBaseVector.v | 10 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 14 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 14 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 30 | ||||
-rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 14 | ||||
-rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 6 | ||||
-rw-r--r-- | src/Spec/EdDSA.v | 2 | ||||
-rw-r--r-- | src/Util/ListUtil.v | 16 |
14 files changed, 91 insertions, 91 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 89984027f..99029a671 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -23,10 +23,10 @@ Module E. Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d). Add Field _edwards_curve_theorems_field : (field_theory_for_stdlib_tactic (H:=field)). - + Definition eq (P Q:point) := fieldwise (n:=2) Feq (coordinates P) (coordinates Q). Infix "=" := eq : E_scope. - + (* TODO: decide whether we still want something like this, then port Local Ltac t := unfold point_eqb; @@ -41,41 +41,41 @@ Module E. | [H: _ |- _ ] => apply F_eqb_eq in H | _ => rewrite F_eqb_refl end; eauto. - + Lemma point_eqb_sound : forall p1 p2, point_eqb p1 p2 = true -> p1 = p2. Proof. t. Qed. - + Lemma point_eqb_complete : forall p1 p2, p1 = p2 -> point_eqb p1 p2 = true. Proof. t. Qed. - + Lemma point_eqb_neq : forall p1 p2, point_eqb p1 p2 = false -> p1 <> p2. Proof. intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition. apply point_eqb_complete in H0; congruence. Qed. - + Lemma point_eqb_neq_complete : forall p1 p2, p1 <> p2 -> point_eqb p1 p2 = false. Proof. intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition. apply point_eqb_sound in Hneq. congruence. Qed. - + Lemma point_eqb_refl : forall p, point_eqb p p = true. Proof. t. Qed. - + Definition point_eq_dec (p1 p2:E.point) : {p1 = p2} + {p1 <> p2}. destruct (point_eqb p1 p2) eqn:H; match goal with | [ H: _ |- _ ] => apply point_eqb_sound in H | [ H: _ |- _ ] => apply point_eqb_neq in H end; eauto. Qed. - + Lemma point_eqb_correct : forall p1 p2, point_eqb p1 p2 = if point_eq_dec p1 p2 then true else false. Proof. intros. destruct (point_eq_dec p1 p2); eauto using point_eqb_complete, point_eqb_neq_complete. @@ -86,7 +86,7 @@ Module E. Lemma decide_and : forall P Q, {P}+{not P} -> {Q}+{not Q} -> {P/\Q}+{not(P/\Q)}. Proof. intros; repeat match goal with [H:{_}+{_}|-_] => destruct H end; intuition. Qed. - Ltac destruct_points := + Ltac destruct_points := repeat match goal with | [ p : point |- _ ] => let x := fresh "x" p in @@ -104,7 +104,7 @@ Module E. Local Hint Resolve nonsquare_d. Local Hint Resolve @edwardsAddCompletePlus. Local Hint Resolve @edwardsAddCompleteMinus. - + Program Definition opp (P:point) : point := exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _. Solve All Obligations using intros; destruct_points; simpl; field_algebra. @@ -158,14 +158,14 @@ Module E. Section PointCompression. Local Notation "x ^2" := (x*x). Definition solve_for_x2 (y : F) := ((y^2 - 1) / (d * (y^2) - a)). - + Lemma a_d_y2_nonzero : forall y, d * y^2 - a <> 0. Proof. intros ? eq_zero. destruct square_a as [sqrt_a sqrt_a_id]; rewrite <- sqrt_a_id in eq_zero. destruct (eq_dec y 0); [apply nonzero_a|apply nonsquare_d with (sqrt_a/y)]; field_algebra. Qed. - + Lemma solve_correct : forall x y, onCurve (x, y) <-> (x^2 = solve_for_x2 y). Proof. unfold solve_for_x2; simpl; split; intros; field_algebra; auto using a_d_y2_nonzero. @@ -189,10 +189,10 @@ Module E. Create HintDb field_homomorphism discriminated. Hint Rewrite <- homomorphism_one - homomorphism_add - homomorphism_sub - homomorphism_mul - homomorphism_div + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div Ha Hd : field_homomorphism. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 49c5d5041..25af83a0a 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -127,7 +127,7 @@ Module Extended. destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB. split; reflexivity. Qed. - + Global Instance Proper_add : Proper (eq==>eq==>eq) add. Proof. unfold eq. intros x y H x0 y0 H0. @@ -204,10 +204,10 @@ Module Extended. Create HintDb field_homomorphism discriminated. Hint Rewrite <- homomorphism_one - homomorphism_add - homomorphism_sub - homomorphism_mul - homomorphism_div + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div Ha Hd Hdd diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 397a6259c..5314ee37c 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -16,14 +16,14 @@ Section Pre. Context {a:F} {a_nonzero : a<>0} {a_square : exists sqrt_a, sqrt_a^2 = a}. Context {d:F} {d_nonsquare : forall sqrt_d, sqrt_d^2 <> d}. Context {char_gt_2 : 1+1 <> 0}. - + (* the canonical definitions are in Spec *) Definition onCurve (P:F*F) := let (x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. Definition unifiedAdd' (P1' P2':F*F) : F*F := let (x1, y1) := P1' in let (x2, y2) := P2' in pair (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2))) (((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). - + Ltac use_sqrt_a := destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *. Lemma edwardsAddComplete' x1 y1 x2 y2 : @@ -44,13 +44,13 @@ Section Pre. Lemma edwardsAddCompletePlus x1 y1 x2 y2 : onCurve (x1, y1) -> onCurve (x2, y2) -> (1 + d*x1*x2*y1*y2) <> 0. Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed. - + Lemma edwardsAddCompleteMinus x1 y1 x2 y2 : onCurve (x1, y1) -> onCurve (x2, y2) -> (1 - d*x1*x2*y1*y2) <> 0. Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed. - + Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. field_algebra. Qed. - + Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). Proof. @@ -71,7 +71,7 @@ Section RespectsFieldHomomorphism. Let phip := fun (P':F*F) => let (x, y) := P' in (phi x, phi y). - Let eqp := fun (P1' P2':K*K) => + Let eqp := fun (P1' P2':K*K) => let (x1, y1) := P1' in let (x2, y2) := P2' in and (eq x1 x2) (eq y1 y2). @@ -79,11 +79,11 @@ Section RespectsFieldHomomorphism. Create HintDb field_homomorphism discriminated. Hint Rewrite homomorphism_one - homomorphism_add - homomorphism_sub - homomorphism_mul - homomorphism_div - a_ok + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div + a_ok d_ok : field_homomorphism. diff --git a/src/Encoding/EncodingTheorems.v b/src/Encoding/EncodingTheorems.v index 52ac91ada..c6f48a0ab 100644 --- a/src/Encoding/EncodingTheorems.v +++ b/src/Encoding/EncodingTheorems.v @@ -2,7 +2,7 @@ Require Import Crypto.Spec.Encoding. Section EncodingTheorems. Context {A B : Type} {E : canonical encoding of A as B}. - + Lemma encoding_inj : forall x y, enc x = enc y -> x = y. Proof. intros. diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v index 7251ac1e6..41b75e216 100644 --- a/src/Encoding/ModularWordEncodingTheorems.v +++ b/src/Encoding/ModularWordEncodingTheorems.v @@ -24,7 +24,7 @@ Section SignBit. assert (m < 1)%Z by (apply Z2Nat.inj_lt; try omega; assumption). omega. + assert (0 < m)%Z as m_pos by (pose proof prime_ge_2 m prime_m; omega). - pose proof (FieldToZ_range x m_pos). + pose proof (FieldToZ_range x m_pos). destruct (FieldToZ x); auto. - destruct p; auto. - pose proof (Pos2Z.neg_is_neg p); omega. diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index 9a6873bba..33fdb5a17 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -46,7 +46,7 @@ Lemma Let_In_Proper_changevalue {A B} RA {RB} (f:A->B) {Proper_f:Proper (RA==>RB : Proper (RA ==> RB) (fun x => Let_In x f). Proof. intuition. Qed. -Ltac fold_identity_lambdas := +Ltac fold_identity_lambdas := repeat match goal with | [ H: appcontext [fun x => ?f x] |- _ ] => change (fun x => f x) with f in * | |- appcontext [fun x => ?f x] => change (fun x => f x) with f in * @@ -285,7 +285,7 @@ Proof. intros. pose proof (eqb_eq_dec' eqb eqb_iff a b). destruct (eqb a b); eauto. -Qed. +Qed. Lemma eqb_compare_encodings {T} {B} {encoding:canonical encoding of T as B} (T_eqb:T->T->bool) (T_eqb_iff : forall a b:T, (T_eqb a b = true) <-> a = b) @@ -308,7 +308,7 @@ Proof. pose proof encoding_valid. congruence. Qed. Lemma compare_without_decoding {T B} (encoding_T_B:canonical encoding of T as B) (T_eqb:T->T->bool) (T_eqb_iff:forall a b, T_eqb a b = true <-> a = b) (B_eqb:B->B->bool) (B_eqb_iff:forall a b, B_eqb a b = true <-> a = b) - (P_:B) (Q:T) : + (P_:B) (Q:T) : option_rect (fun _ : option T => bool) (fun P : T => T_eqb P Q) false diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index 2e65df9bd..9ed7d065e 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -22,19 +22,19 @@ Section ExtendedBaseVector. * * (x \dot base) * (y \dot base) = (z \dot ext_base) * - * Then we can separate z into its first and second halves: + * Then we can separate z into its first and second halves: * * (z \dot ext_base) = (z1 \dot base) + (2 ^ k) * (z2 \dot base) * * Now, if we want to reduce the product modulo 2 ^ k - c: - * + * * (z \dot ext_base) mod (2^k-c)= (z1 \dot base) + (2 ^ k) * (z2 \dot base) mod (2^k-c) * (z \dot ext_base) mod (2^k-c)= (z1 \dot base) + c * (z2 \dot base) mod (2^k-c) * * This sum may be short enough to express using base; if not, we can reduce again. *) Definition ext_base := base ++ (map (Z.mul (2^k)) base). - + Lemma ext_base_positive : forall b, In b ext_base -> b > 0. Proof. unfold ext_base. intros b In_b_base. @@ -76,14 +76,14 @@ Section ExtendedBaseVector. intuition. Qed. - Lemma map_nth_default_base_high : forall n, (n < (length base))%nat -> + Lemma map_nth_default_base_high : forall n, (n < (length base))%nat -> nth_default 0 (map (Z.mul (2 ^ k)) base) n = (2 ^ k) * (nth_default 0 base n). Proof. intros. erewrite map_nth_default; auto. Qed. - + Lemma base_good_over_boundary : forall (i : nat) (l : (i < length base)%nat) diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 9c6a58f9a..ca8c19d18 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -11,9 +11,9 @@ Local Open Scope Z_scope. Section PseudoMersenneBase. Context `{prm :PseudoMersenneBaseParams}. - + Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us). - + Definition rep (us : digits) (x : F modulus) := (length us = length base)%nat /\ decode us = x. Local Notation "u '~=' x" := (rep u x) (at level 70). Local Hint Unfold rep. @@ -35,13 +35,13 @@ Section PseudoMersenneBase. End PseudoMersenneBase. Section CarryBasePow2. - Context `{prm :PseudoMersenneBaseParams}. + Context `{prm :PseudoMersenneBaseParams}. Definition log_cap i := nth_default 0 limb_widths i. Definition add_to_nth n (x:Z) xs := set_nth n (x + nth_default 0 xs n) xs. - + Definition pow2_mod n i := Z.land n (Z.ones i). Definition carry_simple i := fun us => @@ -54,7 +54,7 @@ Section CarryBasePow2. let us' := set_nth i (pow2_mod di (log_cap i)) us in add_to_nth 0 (c * (Z.shiftr di (log_cap i))) us'. - Definition carry i : digits -> digits := + Definition carry i : digits -> digits := if eq_nat_dec i (pred (length base)) then carry_and_reduce i else carry_simple i. @@ -110,12 +110,12 @@ Section Canonicalization. end. Definition and_term us := if isFull us then max_ones else 0. - + Definition freeze us := let us' := carry_full (carry_full (carry_full us)) in let and_term := and_term us' in (* [and_term] is all ones if us' is full, so the subtractions subtract q overall. 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 Canonicalization. diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index c0e942ece..116fe10e5 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -76,7 +76,7 @@ Ltac construct_params prime_modulus len k := | abstract apply prime_modulus | abstract brute_force_indices lw]. -Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits := +Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits := match limb_widths with | nil => nil | x :: tail => @@ -91,7 +91,7 @@ Ltac subst_precondition := match goal with | [H : ?P, H' : ?P -> _ |- _] => specialize (H' H); clear H end. -Ltac kill_precondition H := +Ltac kill_precondition H := forward H; [abstract (try exact eq_refl; clear; cbv; intros; repeat break_or_hyp; intuition)|]; subst_precondition. @@ -207,7 +207,7 @@ Section Carries. cbv [carry_sequence]. transitivity (fold_right carry_opt_cps f (List.rev is) us). Focus 2. - { + { assert (forall i, In i (rev is) -> i < length base)%nat as Hr. { subst. intros. rewrite <- in_rev in *. auto. } remember (rev is) as ris eqn:Heq. @@ -239,7 +239,7 @@ Section Carries. cbv [carry_sequence]. transitivity (fold_right carry_opt_cps id (List.rev is) us). Focus 2. - { + { assert (forall i, In i (rev is) -> i < length base)%nat as Hr. { subst. intros. rewrite <- in_rev in *. auto. } remember (rev is) as ris eqn:Heq. @@ -273,7 +273,7 @@ Section Carries. rewrite carry_sequence_opt_cps_correct by assumption. apply carry_sequence_rep; eauto using rep_length. Qed. - + Lemma full_carry_chain_bounds : forall i, In i full_carry_chain -> (i < length base)%nat. Proof. unfold full_carry_chain; rewrite <-base_length; intros. @@ -502,7 +502,7 @@ Section Multiplication. rewrite map_shiftl by apply k_nonneg. rewrite c_subst. rewrite k_subst. - change @map with @map_opt. + change @map with @map_opt. change @Z_shiftl_by with @Z_shiftl_by_opt. reflexivity. Defined. @@ -640,7 +640,7 @@ Section Canonicalization. := proj2_sig (freeze_opt_sig us). Lemma freeze_opt_canonical: forall us vs x, - @pre_carry_bounds _ _ int_width us -> PseudoMersenneBaseRep.rep us x -> + @pre_carry_bounds _ _ int_width us -> PseudoMersenneBaseRep.rep us x -> @pre_carry_bounds _ _ int_width vs -> PseudoMersenneBaseRep.rep vs x -> freeze_opt us = freeze_opt vs. Proof. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 562c7d6d4..0462b0f37 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -418,7 +418,7 @@ Section CarryProofs. End CarryProofs. Section CanonicalizationProofs. - Context `{prm : PseudoMersenneBaseParams} (lt_1_length_base : (1 < length base)%nat) + Context `{prm : PseudoMersenneBaseParams} (lt_1_length_base : (1 < length base)%nat) {B} (B_pos : 0 < B) (B_compat : forall w, In w limb_widths -> w <= B) (c_pos : 0 < c) (* on the first reduce step, we add at most one bit of width to the first digit *) @@ -783,7 +783,7 @@ Section CanonicalizationProofs. add_set_nth; [ zero_bounds | ]; apply IHj; auto; omega. Qed. - Ltac carry_seq_lower_bound := + Ltac carry_seq_lower_bound := repeat (intros; eapply carry_sequence_bounds_lower; eauto; carry_length_conditions). Lemma carry_bounds_lower : forall i us j, (0 < i <= j)%nat -> (length us = length base) -> @@ -988,7 +988,7 @@ Section CanonicalizationProofs. split; (destruct (eq_nat_dec i 0); subst; [ cbv [make_chain carry_sequence fold_right carry_simple]; add_set_nth | eapply carry_full_2_bounds_succ; eauto; omega]). - + zero_bounds. + + zero_bounds. - eapply carry_full_2_bounds_0; eauto. - eapply carry_full_bounds; eauto; carry_length_conditions. carry_seq_lower_bound. @@ -1097,7 +1097,7 @@ Section CanonicalizationProofs. [ apply Z.sub_le_mono_r; subst x; apply carry_full_2_bounds_0; auto; ring_simplify | ]; omega. + rewrite carry_unaffected_low by carry_length_conditions. - assert (0 < S i < length base)%nat by omega. + assert (0 < S i < length base)%nat by omega. intuition; right. apply carry_carry_done_done; try solve [carry_length_conditions]. assumption. @@ -1123,7 +1123,7 @@ Section CanonicalizationProofs. unfold carry, carry_and_reduce; break_if; try omega; intros. add_set_nth. split. - + zero_bounds. + + zero_bounds. - eapply carry_full_2_bounds_same; eauto; omega. - eapply carry_carry_full_2_bounds_0_lower; eauto; omega. + pose proof (carry_carry_full_2_bounds_0_upper us (pred (length base))). @@ -1138,12 +1138,12 @@ Section CanonicalizationProofs. ring_simplify. apply carry_full_2_bounds_same; auto. - match goal with H0 : (pred (length base) < length base)%nat, - H : carry_done _ |- _ => + H : carry_done _ |- _ => destruct (H (pred (length base)) H0) as [Hcd1 Hcd2]; rewrite Hcd2 by omega end. ring_simplify. apply shiftr_eq_0_max_bound; auto. assert (0 < length base)%nat as zero_lt_length by omega. - match goal with H : carry_done _ |- _ => + match goal with H : carry_done _ |- _ => destruct (H 0%nat zero_lt_length) end. assumption. Qed. @@ -1277,7 +1277,7 @@ Section CanonicalizationProofs. Local Hint Resolve carry_full_3_length. Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2, - nth_default d (map2 f ls1 ls2) i = + nth_default d (map2 f ls1 ls2) i = if lt_dec i (min (length ls1) (length ls2)) then f (nth_default d1 ls1 i) (nth_default d2 ls2 i) else d. @@ -1487,7 +1487,7 @@ Section CanonicalizationProofs. replace (S (length base - 1)) with (length base) by omega. reflexivity. Qed. - + Lemma carry_done_modulus_digits : carry_done modulus_digits. Proof. apply carry_done_bounds; [apply modulus_digits_length | ]. @@ -1660,7 +1660,7 @@ Section CanonicalizationProofs. Proof. unfold isFull; intros; auto using isFull'_true_iff. Qed. - + Definition minimal_rep us := BaseSystem.decode base us = (BaseSystem.decode base us) mod modulus. Fixpoint compare' us vs i := @@ -1813,7 +1813,7 @@ Section CanonicalizationProofs. intros. destruct (Z_dec (nth_default 0 us n) (nth_default 0 vs n)) as [[?|Hgt]|?]; try congruence. + etransitivity; try apply Z_compare_decode_step_lt; auto. - + match goal with |- (?a ?= ?b) = (?c ?= ?d) => + + match goal with |- (?a ?= ?b) = (?c ?= ?d) => rewrite (Z.compare_antisym b a); rewrite (Z.compare_antisym d c) end. apply CompOpp_inj; rewrite !CompOpp_involutive. apply gt_lt_symmetry in Hgt. @@ -1923,11 +1923,11 @@ Section CanonicalizationProofs. - rewrite nth_default_modulus_digits in *. repeat (break_if; try omega). * subst. - match goal with H : isFull' _ _ _ = true |- _ => + match goal with H : isFull' _ _ _ = true |- _ => apply isFull'_lower_bound_0 in H end. apply Z.compare_ge_iff. omega. - * match goal with H : isFull' _ _ _ = true |- _ => + * match goal with H : isFull' _ _ _ = true |- _ => apply isFull'_true_iff in H; try assumption; destruct H as [? eq_max_bound] end. specialize (eq_max_bound j). omega. @@ -2065,7 +2065,7 @@ Section CanonicalizationProofs. us = vs. Proof. intros. - match goal with Hrep1 : rep _ ?x, Hrep2 : rep _ ?x |- _ => + match goal with Hrep1 : rep _ ?x, Hrep2 : rep _ ?x |- _ => pose proof (rep_decode_mod _ _ _ Hrep1 Hrep2) as eqmod end. repeat match goal with Hmin : minimal_rep ?us |- _ => unfold minimal_rep in Hmin; rewrite <- Hmin in eqmod; clear Hmin end. @@ -2076,7 +2076,7 @@ Section CanonicalizationProofs. Qed. Lemma freeze_canonical : forall us vs x, - pre_carry_bounds us -> rep us x -> + pre_carry_bounds us -> rep us x -> pre_carry_bounds vs -> rep vs x -> freeze us = freeze vs. Proof. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 10bbdf33d..49b1875ce 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -32,7 +32,7 @@ Section PseudoMersenneBaseParamProofs. unfold value in *. congruence. Qed. - + Lemma base_from_limb_widths_step : forall i b w, (S i < length base)%nat -> nth_error base i = Some b -> nth_error limb_widths i = Some w -> @@ -45,7 +45,7 @@ Section PseudoMersenneBaseParamProofs. case_eq i; intros; subst. + subst; apply nth_error_first in nth_err_w. apply nth_error_first in nth_err_b; subst. - apply map_nth_error. + apply map_nth_error. case_eq l; intros; subst; [simpl in *; omega | ]. unfold base_from_limb_widths; fold base_from_limb_widths. reflexivity. @@ -65,7 +65,7 @@ Section PseudoMersenneBaseParamProofs. apply nth_error_first in H. subst; eauto. Qed. - + Lemma sum_firstn_succ : forall l i x, nth_error l i = Some x -> sum_firstn l (S i) = x + sum_firstn l i. @@ -117,7 +117,7 @@ Section PseudoMersenneBaseParamProofs. induction i; intros. + unfold base, sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity. intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega. - + + + assert (i < length base)%nat as lt_i_length by omega. specialize (IHi lt_i_length). rewrite base_length in lt_i_length. @@ -138,7 +138,7 @@ Section PseudoMersenneBaseParamProofs. apply limb_widths_nonneg. eapply nth_error_value_In; eauto. Qed. - + Lemma nth_default_base : forall d i, (i < length base)%nat -> nth_default d base i = 2 ^ (sum_firstn limb_widths i). Proof. @@ -178,7 +178,7 @@ Section PseudoMersenneBaseParamProofs. + rewrite base_length in *; apply limb_widths_match_modulus; assumption. Qed. - Lemma base_succ : forall i, ((S i) < length base)%nat -> + Lemma base_succ : forall i, ((S i) < length base)%nat -> nth_default 0 base (S i) mod nth_default 0 base i = 0. Proof. intros. @@ -226,7 +226,7 @@ Section PseudoMersenneBaseParamProofs. Proof. unfold base; case_eq limb_widths; intros; [pose proof limb_widths_nonnil; congruence | reflexivity]. Qed. - + Lemma base_good : forall i j : nat, (i + j < length base)%nat -> let b := nth_default 0 base in diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 5df36e295..88388ee0a 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -24,12 +24,12 @@ Module E. nonsquare_d : forall x, x^2 <> d }. Context `{twisted_edwards_params}. - + Definition point := { P | let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2 }. Definition coordinates (P:point) : (F*F) := proj1_sig P. Program Definition zero : point := (0, 1). - + Program Definition add (P1 P2:point) : point := exist _ ( let (x1, y1) := coordinates P1 in let (x2, y2) := coordinates P2 in @@ -47,7 +47,7 @@ Module E. end. End TwistedEdwardsCurves. End E. - + Delimit Scope E_scope with E. Infix "+" := E.add : E_scope. Infix "*" := E.mul : E_scope.
\ No newline at end of file diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index bd8a095dd..2c7097207 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -26,7 +26,7 @@ Section EdDSA. {PointEncoding : canonical encoding of E as Word.word b} (* wire format *) {FlEncoding : canonical encoding of { n | n < l } as Word.word b} := - { + { EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp; EdDSA_c_valid : c = 2 \/ c = 3; diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 9a9ce9a06..0426c0834 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -18,7 +18,7 @@ Proof. intros. induction n; boring. Qed. -Ltac nth_tac' := +Ltac nth_tac' := intros; simpl in *; unfold error,value in *; repeat progress (match goal with | [ |- context[nth_error nil ?n] ] => rewrite nth_error_nil_error | [ H: ?x = Some _ |- context[match ?x with Some _ => ?a | None => ?a end ] ] => destruct x @@ -79,10 +79,10 @@ Proof. reflexivity. nth_tac'. pose proof (nth_error_error_length A n l H0). - omega. + omega. Qed. -Ltac nth_tac := +Ltac nth_tac := repeat progress (try nth_tac'; try (match goal with | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H | [ H: nth_error (seq _ _) _ = Some _ |- _ ] => rewrite nth_error_seq in H @@ -191,7 +191,7 @@ Proof. Qed. Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T), - set_nth n x xs = + set_nth n x xs = if lt_dec n (length xs) then splice_nth n x xs else xs. @@ -210,7 +210,7 @@ Lemma combine_set_nth : forall {A B} n (x:A) xs (ys:list B), end. Proof. (* TODO(andreser): this proof can totally be automated, but requires writing ltac that vets multiple hypotheses at once *) - induction n, xs, ys; nth_tac; try rewrite IHn; nth_tac; + induction n, xs, ys; nth_tac; try rewrite IHn; nth_tac; try (f_equal; specialize (IHn x xs ys ); rewrite H in IHn; rewrite <- IHn); try (specialize (nth_error_value_length _ _ _ _ H); omega). assert (Some b0=Some b1) as HA by (rewrite <-H, <-H0; auto). @@ -330,7 +330,7 @@ Proof. intros. rewrite firstn_app_inleft; auto using firstn_all; omega. Qed. - + Lemma skipn_app_sharp : forall {A} n (l l': list A), length l = n -> skipn n (l ++ l') = l'. @@ -422,7 +422,7 @@ Proof. right; repeat eexists; auto. } Qed. - + Lemma nil_length0 : forall {T}, length (@nil T) = 0%nat. Proof. auto. @@ -512,7 +512,7 @@ Ltac nth_error_inbounds := match goal with | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => case_eq (nth_error xs i); - match goal with + match goal with | [ |- forall _, nth_error xs i = Some _ -> _ ] => let x := fresh "x" in let H := fresh "H" in |