From 3febea4ed8fdb255c634acbeb3705c88baa89303 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 20 Jun 2016 03:50:08 -0400 Subject: Remove anything incompatible with new algebraic hierarcy - PointEncoding (these will hopefully come back soon) - EdDSAProofs (not a priority to bring back, but not hard either) - Ed25519 spec bits and pieces which were not finished anyway --- src/Encoding/PointEncodingPre.v | 275 ----------------------------------- src/Encoding/PointEncodingTheorems.v | 207 -------------------------- 2 files changed, 482 deletions(-) delete mode 100644 src/Encoding/PointEncodingPre.v delete mode 100644 src/Encoding/PointEncodingTheorems.v (limited to 'src/Encoding') diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v deleted file mode 100644 index 73ced869b..000000000 --- a/src/Encoding/PointEncodingPre.v +++ /dev/null @@ -1,275 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import Coq.Program.Equality. -Require Import Crypto.Encoding.EncodingTheorems. -Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Bedrock.Word. -Require Import Crypto.Encoding.ModularWordEncodingTheorems. -Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.Util.ZUtil. - -Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.ModularArithmetic. - -Local Open Scope F_scope. - -Section PointEncoding. - Context {prm: TwistedEdwardsParams} {sz : nat} {sz_nonzero : (0 < sz)%nat} - {bound_check : (Z.to_nat q < 2 ^ sz)%nat} {q_5mod8 : (q mod 8 = 5)%Z} - {sqrt_minus1_valid : (@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1} - {FqEncoding : canonical encoding of (F q) as (word sz)} - {sign_bit : F q -> bool} {sign_bit_zero : sign_bit 0 = false} - {sign_bit_opp : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x)}. - Existing Instance prime_q. - - Add Field Ffield : (@Ffield_theory q _) - (morphism (@Fring_morph q), - preprocess [Fpreprocess], - postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - - Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F. - - Lemma solve_sqrt_valid : forall p, E.onCurve p -> - sqrt_valid (E.solve_for_x2 (snd p)). - Proof. - intros ? onCurve_xy. - destruct p as [x y]; simpl. - rewrite (E.solve_correct x y) in onCurve_xy. - rewrite <- onCurve_xy. - unfold sqrt_valid. - eapply sqrt_mod_q_valid; eauto. - unfold isSquare; eauto. - Grab Existential Variables. eauto. - Qed. - - Lemma solve_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) -> - E.onCurve (sqrt_mod_q (E.solve_for_x2 y), y). - Proof. - intros. - unfold sqrt_valid in *. - apply E.solve_correct; auto. - Qed. - - Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) -> - E.onCurve (opp (sqrt_mod_q (E.solve_for_x2 y)), y). - Proof. - intros y sqrt_valid_x2. - unfold sqrt_valid in *. - apply E.solve_correct. - rewrite <- sqrt_valid_x2 at 2. - ring. - Qed. - - Definition point_enc_coordinates (p : (F q * F q)) : Word.word (S sz) := let '(x,y) := p in - Word.WS (sign_bit x) (enc y). - - Let point_enc (p : E.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in - Word.WS (sign_bit x) (enc y). - - Definition point_dec_coordinates (sign_bit : F q -> bool) (w : Word.word (S sz)) : option (F q * F q) := - match dec (Word.wtl w) with - | None => None - | Some y => let x2 := E.solve_for_x2 y in - let x := sqrt_mod_q x2 in - if F_eq_dec (x ^ 2) x2 - then - let p := (if Bool.eqb (whd w) (sign_bit x) then x else opp x, y) in - if (andb (F_eqb x 0) (whd w)) - then None (* special case for 0, since its opposite has the same sign; if the sign bit of 0 is 1, produce None.*) - else Some p - else None - end. - - Ltac inversion_Some_eq := match goal with [H: Some ?x = Some ?y |- _] => inversion H; subst end. - - Lemma point_dec_coordinates_onCurve : forall w p, point_dec_coordinates sign_bit w = Some p -> E.onCurve p. - Proof. - unfold point_dec_coordinates; intros. - edestruct dec; [ | congruence]. - break_if; [ | congruence]. - break_if; [ congruence | ]. - break_if; inversion_Some_eq; auto using solve_onCurve, solve_opp_onCurve. - Qed. - - Lemma prod_eq_dec : forall {A} (A_eq_dec : forall a a' : A, {a = a'} + {a <> a'}) - (x y : (A * A)), {x = y} + {x <> y}. - Proof. - decide equality. - Qed. - - Lemma option_eq_dec : forall {A} (A_eq_dec : forall a a' : A, {a = a'} + {a <> a'}) - (x y : option A), {x = y} + {x <> y}. - Proof. - decide equality. - Qed. - - Definition point_dec' w p : option E.point := - match (option_eq_dec (prod_eq_dec F_eq_dec) (point_dec_coordinates sign_bit w) (Some p)) with - | left EQ => Some (exist _ p (point_dec_coordinates_onCurve w p EQ)) - | right _ => None (* this case is never reached *) - end. - - Definition point_dec (w : word (S sz)) : option E.point := - match (point_dec_coordinates sign_bit w) with - | Some p => point_dec' w p - | None => None - end. - - Lemma point_coordinates_encoding_canonical : forall w p, - point_dec_coordinates sign_bit w = Some p -> point_enc_coordinates p = w. - Proof. - unfold point_dec_coordinates, point_enc_coordinates; intros ? ? coord_dec_Some. - case_eq (dec (wtl w)); [ intros ? dec_Some | intros dec_None; rewrite dec_None in *; congruence ]. - destruct p. - rewrite (shatter_word w). - f_equal; rewrite dec_Some in *; - do 2 (break_if; try congruence); inversion coord_dec_Some; subst. - + destruct (F_eq_dec (sqrt_mod_q (E.solve_for_x2 f1)) 0%F) as [sqrt_0 | ?]. - - rewrite sqrt_0 in *. - apply sqrt_mod_q_root_0 in sqrt_0; try assumption. - rewrite sqrt_0 in *. - break_if; [symmetry; auto using Bool.eqb_prop | ]. - rewrite sign_bit_zero in *. - simpl in Heqb; rewrite Heqb in *. - discriminate. - - break_if. - symmetry; auto using Bool.eqb_prop. - rewrite <- sign_bit_opp by assumption. - destruct (whd w); inversion Heqb0; break_if; auto. - + inversion coord_dec_Some; subst. - auto using encoding_canonical. -Qed. - - Lemma point_encoding_canonical : forall w x, point_dec w = Some x -> point_enc x = w. - Proof. - (* - unfold point_enc; intros. - unfold point_dec in *. - assert (point_dec_coordinates w = Some (proj1_sig x)). { - set (y := point_dec_coordinates w) in *. - revert H. - dependent destruction y. intros. - rewrite H0 in H. - *) - Admitted. - -Lemma point_dec_coordinates_correct w - : option_map (@proj1_sig _ _) (point_dec w) = point_dec_coordinates sign_bit w. -Proof. - unfold point_dec, option_map. - do 2 break_match; try congruence; unfold point_dec' in *; - break_match; try congruence. - inversion_Some_eq. - reflexivity. -Qed. - -Lemma y_decode : forall p, dec (wtl (point_enc_coordinates p)) = Some (snd p). -Proof. - intros. - destruct p as [x y]; simpl. - exact (encoding_valid y). -Qed. - -Lemma sign_bit_opp_eq_iff : forall x y, y <> 0 -> - (sign_bit x <> sign_bit y <-> sign_bit x = sign_bit (opp y)). -Proof. - split; intro sign_mismatch; case_eq (sign_bit x); case_eq (sign_bit y); - try congruence; intros y_sign x_sign; rewrite <- sign_bit_opp in * by auto; - rewrite y_sign, x_sign in *; reflexivity || discriminate. -Qed. - -Lemma sign_bit_squares : forall x y, y <> 0 -> x ^ 2 = y ^ 2 -> - sign_bit x = sign_bit y -> x = y. -Proof. - intros ? ? y_nonzero squares_eq sign_match. - destruct (sqrt_solutions _ _ squares_eq) as [? | eq_opp]; auto. - assert (sign_bit x = sign_bit (opp y)) as sign_mismatch by (f_equal; auto). - apply sign_bit_opp_eq_iff in sign_mismatch; auto. - congruence. -Qed. - -Lemma sign_bit_match : forall x x' y : F q, E.onCurve (x, y) -> E.onCurve (x', y) -> - sign_bit x = sign_bit x' -> x = x'. -Proof. - intros ? ? ? onCurve_x onCurve_x' sign_match. - apply E.solve_correct in onCurve_x. - apply E.solve_correct in onCurve_x'. - destruct (F_eq_dec x' 0). - + subst. - rewrite Fq_pow_zero in onCurve_x' by congruence. - rewrite <- onCurve_x' in *. - eapply Fq_root_zero; eauto. - + apply sign_bit_squares; auto. - rewrite onCurve_x, onCurve_x'. - reflexivity. -Qed. - -Lemma point_encoding_coordinates_valid : forall p, E.onCurve p -> - point_dec_coordinates sign_bit (point_enc_coordinates p) = Some p. -Proof. - intros p onCurve_p. - unfold point_dec_coordinates. - rewrite y_decode. - pose proof (solve_sqrt_valid p onCurve_p) as solve_sqrt_valid_p. - destruct p as [x y]. - unfold sqrt_valid in *. - simpl. - replace (E.solve_for_x2 y) with (x ^ 2 : F q) in * by (apply E.solve_correct; assumption). - case_eq (F_eqb x 0); intro eqb_x_0. - + apply F_eqb_eq in eqb_x_0; rewrite eqb_x_0 in *. - rewrite !Fq_pow_zero, sqrt_mod_q_of_0, Fq_pow_zero by congruence. - rewrite if_F_eq_dec_if_F_eqb, sign_bit_zero. - reflexivity. - + assert (sqrt_mod_q (x ^ 2) <> 0) by (intro false_eq; apply sqrt_mod_q_root_0 in false_eq; try assumption; - apply Fq_root_zero in false_eq; rewrite false_eq, F_eqb_refl in eqb_x_0; congruence). - replace (F_eqb (sqrt_mod_q (x ^ 2)) 0) with false by (symmetry; - apply F_eqb_neq_complete; assumption). - break_if. - - simpl. - f_equal. - break_if. - * rewrite Bool.eqb_true_iff in Heqb. - pose proof (solve_onCurve y solve_sqrt_valid_p). - f_equal. - apply (sign_bit_match _ _ y); auto. - apply E.solve_correct in onCurve_p; rewrite onCurve_p in *. - assumption. - * rewrite Bool.eqb_false_iff in Heqb. - pose proof (solve_opp_onCurve y solve_sqrt_valid_p). - f_equal. - apply sign_bit_opp_eq_iff in Heqb; try assumption. - apply (sign_bit_match _ _ y); auto. - apply E.solve_correct in onCurve_p. - rewrite onCurve_p; auto. - - simpl in solve_sqrt_valid_p. - replace (E.solve_for_x2 y) with (x ^ 2 : F q) in * by (apply E.solve_correct; assumption). - congruence. -Qed. - -Lemma point_dec'_valid : forall p, - point_dec' (point_enc_coordinates (proj1_sig p)) (proj1_sig p) = Some p. -Proof. - unfold point_dec'; intros. - break_match. - + f_equal. - destruct p. - apply E.point_eq. - reflexivity. - + rewrite point_encoding_coordinates_valid in n by apply (proj2_sig p). - congruence. -Qed. - -Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p. -Proof. - intros. - unfold point_dec. - replace (point_enc p) with (point_enc_coordinates (proj1_sig p)) by reflexivity. - break_match; rewrite point_encoding_coordinates_valid in * by apply (proj2_sig p); try congruence. - inversion_Some_eq. - eapply point_dec'_valid. -Qed. - -End PointEncoding. diff --git a/src/Encoding/PointEncodingTheorems.v b/src/Encoding/PointEncodingTheorems.v deleted file mode 100644 index ccea1d81b..000000000 --- a/src/Encoding/PointEncodingTheorems.v +++ /dev/null @@ -1,207 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import Coq.Program.Equality. -Require Import Crypto.Encoding.EncodingTheorems. -Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Bedrock.Word. -Require Import Crypto.Tactics.VerdiTactics. - -Require Import Crypto.Spec.Encoding Crypto.Spec.ModularArithmetic Crypto.Spec.CompleteEdwardsCurve. - -Local Open Scope F_scope. - -Section PointEncoding. - Context {prm: CompleteEdwardsCurve.TwistedEdwardsParams} {sz : nat} - {FqEncoding : canonical encoding of ModularArithmetic.F (CompleteEdwardsCurve.q) as Word.word sz} - {q_5mod8 : (CompleteEdwardsCurve.q mod 8 = 5)%Z} - {sqrt_minus1_valid : (@ZToField CompleteEdwardsCurve.q 2 ^ BinInt.Z.to_N (CompleteEdwardsCurve.q / 4)) ^ 2 = opp 1}. - Existing Instance CompleteEdwardsCurve.prime_q. - - Add Field Ffield : (@PrimeFieldTheorems.Ffield_theory CompleteEdwardsCurve.q _) - (morphism (@ModularArithmeticTheorems.Fring_morph CompleteEdwardsCurve.q), - preprocess [ModularArithmeticTheorems.Fpreprocess], - postprocess [ModularArithmeticTheorems.Fpostprocess; try exact PrimeFieldTheorems.Fq_1_neq_0; try assumption], - constants [ModularArithmeticTheorems.Fconstant], - div (@ModularArithmeticTheorems.Fmorph_div_theory CompleteEdwardsCurve.q), - power_tac (@ModularArithmeticTheorems.Fpower_theory CompleteEdwardsCurve.q) [ModularArithmeticTheorems.Fexp_tac]). - - Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F. - - Lemma solve_sqrt_valid : forall (p : E.point), - sqrt_valid (E.solve_for_x2 (snd (proj1_sig p))). - Proof. - intros. - destruct p as [[x y] onCurve_xy]; simpl. - rewrite (E.solve_correct x y) in onCurve_xy. - rewrite <- onCurve_xy. - unfold sqrt_valid. - eapply sqrt_mod_q_valid; eauto. - unfold isSquare; eauto. - Grab Existential Variables. eauto. - Qed. - - Lemma solve_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) -> - E.onCurve (sqrt_mod_q (E.solve_for_x2 y), y). - Proof. - intros. - unfold sqrt_valid in *. - apply E.solve_correct; auto. - Qed. - - Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) -> - E.onCurve (opp (sqrt_mod_q (E.solve_for_x2 y)), y). - Proof. - intros y sqrt_valid_x2. - unfold sqrt_valid in *. - apply E.solve_correct. - rewrite <- sqrt_valid_x2 at 2. - ring. - Qed. - -Definition sign_bit (x : F q) := (wordToN (enc (opp x)) None - | Some y => let x2 := E.solve_for_x2 y in - let x := sqrt_mod_q x2 in - if F_eq_dec (x ^ 2) x2 - then - let p := (if Bool.eqb (whd w) (sign_bit x) then x else opp x, y) in - Some p - else None - end. - -Definition point_dec (w : word (S sz)) : option E.point := - match dec (wtl w) with - | None => None - | Some y => let x2 := E.solve_for_x2 y in - let x := sqrt_mod_q x2 in - match (F_eq_dec (x ^ 2) x2) with - | right _ => None - | left EQ => if Bool.eqb (whd w) (sign_bit x) - then Some (exist _ (x, y) (solve_onCurve y EQ)) - else Some (exist _ (opp x, y) (solve_opp_onCurve y EQ)) - end - end. - -Lemma point_dec_coordinates_correct w - : option_map (@proj1_sig _ _) (point_dec w) = point_dec_coordinates w. -Proof. - unfold point_dec, point_dec_coordinates. - edestruct dec; [ | reflexivity ]. - edestruct @F_eq_dec; [ | reflexivity ]. - edestruct @Bool.eqb; reflexivity. -Qed. - -Lemma y_decode : forall p, dec (wtl (point_enc p)) = Some (snd (proj1_sig p)). -Proof. - intros. - destruct p as [[x y] onCurve_p]; simpl. - exact (encoding_valid y). -Qed. - - -Lemma wordToN_enc_neq_opp : forall x, x <> 0 -> (wordToN (enc (opp x)) <> wordToN (enc x))%N. -Proof. - intros x x_nonzero. - intro false_eq. - apply x_nonzero. - apply F_eq_opp_zero; try apply two_lt_q. - apply wordToN_inj in false_eq. - apply encoding_inj in false_eq. - auto. -Qed. - -Lemma sign_bit_opp_negb : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x). -Proof. - intros x x_nonzero. - unfold sign_bit. - rewrite <- N.leb_antisym. - rewrite N.ltb_compare, N.leb_compare. - rewrite F_opp_involutive. - case_eq (wordToN (enc x) ?= wordToN (enc (opp x)))%N; auto. - intro wordToN_enc_eq. - pose proof (wordToN_enc_neq_opp x x_nonzero). - apply N.compare_eq_iff in wordToN_enc_eq. - congruence. -Qed. - -Lemma sign_bit_opp : forall x y, y <> 0 -> - (sign_bit x <> sign_bit y <-> sign_bit x = sign_bit (opp y)). -Proof. - split; intro sign_mismatch; case_eq (sign_bit x); case_eq (sign_bit y); - try congruence; intros y_sign x_sign; rewrite <- sign_bit_opp_negb in * by auto; - rewrite y_sign, x_sign in *; reflexivity || discriminate. -Qed. - -Lemma sign_bit_squares : forall x y, y <> 0 -> x ^ 2 = y ^ 2 -> - sign_bit x = sign_bit y -> x = y. -Proof. - intros ? ? y_nonzero squares_eq sign_match. - destruct (sqrt_solutions _ _ squares_eq) as [? | eq_opp]; auto. - assert (sign_bit x = sign_bit (opp y)) as sign_mismatch by (f_equal; auto). - apply sign_bit_opp in sign_mismatch; auto. - congruence. -Qed. - -Lemma sign_bit_match : forall x x' y : F q, E.onCurve (x, y) -> E.onCurve (x', y) -> - sign_bit x = sign_bit x' -> x = x'. -Proof. - intros ? ? ? onCurve_x onCurve_x' sign_match. - apply E.solve_correct in onCurve_x. - apply E.solve_correct in onCurve_x'. - destruct (F_eq_dec x' 0). - + subst. - rewrite Fq_pow_zero in onCurve_x' by congruence. - rewrite <- onCurve_x' in *. - eapply Fq_root_zero; eauto. - + apply sign_bit_squares; auto. - rewrite onCurve_x, onCurve_x'. - reflexivity. -Qed. - -Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p. -Proof. - intros. - unfold point_dec. - rewrite y_decode. - pose proof solve_sqrt_valid p as solve_sqrt_valid_p. - unfold sqrt_valid in *. - destruct p as [[x y] onCurve_p]. - simpl in *. - destruct (F_eq_dec ((sqrt_mod_q (E.solve_for_x2 y)) ^ 2) (E.solve_for_x2 y)); intuition. - break_if; f_equal; apply E.point_eq. - + rewrite Bool.eqb_true_iff in Heqb. - pose proof (solve_onCurve y solve_sqrt_valid_p). - f_equal. - apply (sign_bit_match _ _ y); auto. - + rewrite Bool.eqb_false_iff in Heqb. - pose proof (solve_opp_onCurve y solve_sqrt_valid_p). - f_equal. - apply sign_bit_opp in Heqb. - apply (sign_bit_match _ _ y); auto. - intro eq_zero. - apply E.solve_correct in onCurve_p. - rewrite eq_zero in *. - rewrite Fq_pow_zero in solve_sqrt_valid_p by congruence. - rewrite <- solve_sqrt_valid_p in onCurve_p. - apply Fq_root_zero in onCurve_p. - rewrite onCurve_p in Heqb; auto. -Qed. - -(* Waiting on canonicalization *) -Lemma point_encoding_canonical : forall (x_enc : word (S sz)) (x : E.point), -point_dec x_enc = Some x -> point_enc x = x_enc. -Admitted. - -Instance point_encoding : canonical encoding of E.point as (word (S sz)) := { - enc := point_enc; - dec := point_dec; - encoding_valid := point_encoding_valid; - encoding_canonical := point_encoding_canonical -}. - -End PointEncoding. -- cgit v1.2.3 From 0ae5f6871b29d20f48b5df6dab663b5a44162d01 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 20 Jun 2016 15:07:03 -0400 Subject: remove trailing whitespace from src/ --- .../CompleteEdwardsCurveTheorems.v | 34 +++++++++++----------- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 10 +++---- src/CompleteEdwardsCurve/Pre.v | 22 +++++++------- src/Encoding/EncodingTheorems.v | 2 +- src/Encoding/ModularWordEncodingTheorems.v | 2 +- .../DerivationsOptionRectLetInEncoding.v | 6 ++-- src/ModularArithmetic/ExtendedBaseVector.v | 10 +++---- src/ModularArithmetic/ModularBaseSystem.v | 14 ++++----- src/ModularArithmetic/ModularBaseSystemOpt.v | 14 ++++----- src/ModularArithmetic/ModularBaseSystemProofs.v | 30 +++++++++---------- .../PseudoMersenneBaseParamProofs.v | 14 ++++----- src/Spec/CompleteEdwardsCurve.v | 6 ++-- src/Spec/EdDSA.v | 2 +- src/Util/ListUtil.v | 16 +++++----- 14 files changed, 91 insertions(+), 91 deletions(-) (limited to 'src/Encoding') 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 -- cgit v1.2.3