From 996fe81ecfa5d8dfa89d2d61c1e94fd15fe9a911 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 7 Feb 2016 14:03:23 -0500 Subject: remove a dangling About --- src/Specific/GF25519.v | 1 - 1 file changed, 1 deletion(-) (limited to 'src') diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 732779a1a..7ef2f0aaf 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -289,7 +289,6 @@ Proof. cbv [cap Base25Point5_10limbs.base]. intros. rewrite map_length in *. - About map_nth_default. erewrite map_nth_default; [|assumption]. instantiate (2 := 0%Z). (** For the division of maps of (2 ^ _) over lists, replace it with 2 ^ (_ - _) *) -- cgit v1.2.3 From a9149bcee709930b80e9e5c9b0e6f20cf8174956 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 7 Feb 2016 22:55:06 -0500 Subject: fresh take at specifications using implicit arguments instead of module parameters --- src/CompleteEwardsCurve/Pre.v | 174 +++++++++++++++++++++++++++++++++++++++++ src/ModularArithmetic/Pre.v | 8 ++ src/Spec/CompleteEwardsCurve.v | 49 ++++++++++++ src/Spec/ModularArithmetic.v | 60 ++++++++++++++ 4 files changed, 291 insertions(+) create mode 100644 src/CompleteEwardsCurve/Pre.v create mode 100644 src/ModularArithmetic/Pre.v create mode 100644 src/Spec/CompleteEwardsCurve.v create mode 100644 src/Spec/ModularArithmetic.v (limited to 'src') diff --git a/src/CompleteEwardsCurve/Pre.v b/src/CompleteEwardsCurve/Pre.v new file mode 100644 index 000000000..d66ed8fab --- /dev/null +++ b/src/CompleteEwardsCurve/Pre.v @@ -0,0 +1,174 @@ +Require Import BinInt Znumtheory VerdiTactics. + +Require Import Crypto.Spec.ModularArithmetic. +Local Open Scope F_scope. + +Section Pre. + Context {p : BinInt.Z}. + Context {a : F p}. + Context {d : F p}. + Context {modulus_prime : Znumtheory.prime p}. + Context {modulus_lt_2 : 2 < p}. + Context {a_nonzero : a <> 0}. + Context {a_square : exists sqrt_a, sqrt_a^2 = a}. + Context {d_nonsquare : forall x, x^2 <> d}. + + (* the canonical definitions are in Spec *) + Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2). + Local Notation unifiedAdd' P1' P2' := ( + let '(x1, y1) := P1' in + let '(x2, y2) := P2' in + (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))) + ). + + Lemma char_gt_2 : ZToField 2 <> (0: F p). + intro; find_injection. + pose proof modulus_lt_2. + rewrite (Z.mod_small 2 p), Z.mod_0_l in *; omega. + Qed. + + (* + Ltac whatsNotZero := + repeat match goal with + | [H: ?lhs = ?rhs |- _ ] => + match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end; + assert (lhs <> 0) by (rewrite H; auto) + | [H: ?lhs = ?rhs |- _ ] => + match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end; + assert (rhs <> 0) by (rewrite H; auto) + | [H: (?a^?p)%F <> 0 |- _ ] => + match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; + let Y:=fresh in let Z:=fresh in try ( + assert (p <> 0%N) as Z by (intro Y; inversion Y); + assert (a <> 0) by (eapply root_nonzero; eauto); + clear Z) + | [H: (?a*?b)%F <> 0 |- _ ] => + match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; + assert (a <> 0) by (eapply mul_nonzero_l; eauto) + | [H: (?a*?b)%F <> 0 |- _ ] => + match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end; + assert (b <> 0) by (eapply mul_nonzero_r; eauto) + end. + *) + + Lemma edwardsAddComplete' x1 y1 x2 y2 : + onCurve (x1, y1) -> + onCurve (x2, y2) -> + (d*x1*x2*y1*y2)^2 <> 1. + Proof. (* + intuition; whatsNotZero. + + pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. + destruct a_square as [sqrt_a a_square]. + rewrite <-a_square in *. + + (* Furthermore... *) + pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt. + rewrite H0 in Heqt at 2. + replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2)) + with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field. + rewrite H1 in Heqt. + replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field. + rewrite <-H in Heqt. + + (* main equation for both potentially nonzero denominators *) + case_eq_GF (sqrt_a*x2 + y2) 0; case_eq_GF (sqrt_a*x2 - y2) 0; + try match goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] => + assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 = + f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2) + (d * x1 * x2 * y1 * y2*sqrt_a*(inject 2)*x1*y1)) as Heqw1 by field; + rewrite H1 in *; + replace (1 * y1^2) with (y1^2) in * by field; + rewrite <- Heqt in *; + assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 / + (x1 * y1 * (f (sqrt_a * x2) y2))^2) + by (rewriteAny; field; auto); + match goal with [H: d = (?n^2)/(?l^2) |- _ ] => + destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto) + end + end. + + assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field). + + replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (inject 2 * sqrt_a * x2) in Hc by field. + + (* contradiction: product of nonzero things is zero *) + destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition. + destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition. + apply Ha_nonzero; field. + Qed + *) Admitted. + Lemma edwardsAddCompletePlus x1 y1 x2 y2 : + onCurve (x1, y1) -> + onCurve (x2, y2) -> + (1 + d*x1*x2*y1*y2) <> 0. + Proof. (* + intros; case_eq_GF (d*x1*x2*y1*y2) (0-1)%GF. + - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. + - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H1 by field. + intro; rewrite H2 in H1; intuition. + Qed. + *) Admitted. + + Lemma edwardsAddCompleteMinus x1 y1 x2 y2 : + onCurve (x1, y1) -> + onCurve (x2, y2) -> + (1 - d*x1*x2*y1*y2) <> 0. + Proof. (* + unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (1)%GF. + - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. + - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H1 by field. + intro; rewrite H2 in H1; apply H1; field. + Qed. + *) Admitted. + + Definition zeroOnCurve : onCurve (0, 1). + Admitted. (* field. *) + + Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3 + (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) : + onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3). + Proof. (* + (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1; + * c=1 and an extra a in front of x^2 *) + + injection H; clear H; intros. + + Ltac t x1 y1 x2 y2 := + assert ((a*x2^2 + y2^2)*d*x1^2*y1^2 + = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto); + assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2 + = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field). + t x1 y1 x2 y2; t x2 y2 x1 y1. + + remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 - + (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T. + assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field). + assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +( + (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 * + y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field). + replace 1 with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3. + + match goal with [ |- ?x = 1 ] => replace x with + ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 + + ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 - + d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/ + ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end; try field; auto. + - rewrite <-HT1, <-HT2; field; rewrite HT1. + replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2)) + with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) + by field; simpl; auto. + - replace (1 - (d * x1 * x2 * y1 * y2) ^ 2) + with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) + by field; auto. + Qed. + *) Admitted. + + Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 -> + onCurve (unifiedAdd' P1 P2). + Proof. + intros; destruct P1, P2. + remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r. + eapply unifiedAdd'_onCurve'; eauto. + Qed. +End Pre. \ No newline at end of file diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v new file mode 100644 index 000000000..2c111be32 --- /dev/null +++ b/src/ModularArithmetic/Pre.v @@ -0,0 +1,8 @@ +Require Import Znumtheory BinInt BinNums. + +Lemma Z_mod_mod x m : x mod m = (x mod m) mod m. + symmetry. + destruct (BinInt.Z.eq_dec m 0). + - subst; rewrite !Zdiv.Zmod_0_r; reflexivity. + - apply BinInt.Z.mod_mod; assumption. +Qed. diff --git a/src/Spec/CompleteEwardsCurve.v b/src/Spec/CompleteEwardsCurve.v new file mode 100644 index 000000000..7ebf35988 --- /dev/null +++ b/src/Spec/CompleteEwardsCurve.v @@ -0,0 +1,49 @@ +Require BinInt Znumtheory. + +Require Crypto.CompleteEwardsCurve.Pre. + +Require Import Crypto.Spec.ModularArithmetic. +Local Open Scope F_scope. + +Class TwistedEdwardsParams := { + p : BinInt.Z; + a : F p; + d : F p; + modulus_prime : Znumtheory.prime p; + a_nonzero : a <> 0; + a_square : exists sqrt_a, sqrt_a^2 = a; + d_nonsquare : forall x, x^2 <> d +}. + +Section TwistedEdwardsCurves. + Context `{prm:TwistedEdwardsParams}. + (* Twisted Edwards curves with complete addition laws. References: + * + * + * + *) + Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. + Definition point := { P | onCurve P}. + Definition mkPoint xy proof : point := exist onCurve xy proof. + Definition projX (P:point) : F p := fst (proj1_sig P). + Definition projY (P:point) : F p:= snd (proj1_sig P). + + Definition zero : point := mkPoint (0, 1) Pre.zeroOnCurve. + + (* NOTE: the two matches on P1 can probably be merged, not sure whether good idea... *) + Definition unifiedAdd (P1 P2 : point) : point := + let 'exist P1' pf1 := P1 in + let 'exist P2' pf2 := P2 in + mkPoint + ( let '(x1, y1) := P1' in + let '(x2, y2) := P2' in + (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))) + (Pre.unifiedAdd'_onCurve _ _ pf1 pf2). + Local Infix "+" := unifiedAdd. + + Fixpoint scalarMult (n:nat) (P : point) : point := + match n with + | O => zero + | S n' => P + scalarMult n' P + end. +End TwistedEdwardsCurves. \ No newline at end of file diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v new file mode 100644 index 000000000..7f31161e2 --- /dev/null +++ b/src/Spec/ModularArithmetic.v @@ -0,0 +1,60 @@ +Require Znumtheory BinInt BinNums. + +Require Crypto.ModularArithmetic.Pre. + +Delimit Scope N_scope with N. +Infix "+" := BinNat.N.add : N_scope. +Infix "*" := BinNat.N.mul : N_scope. +Infix "-" := BinNat.N.sub : N_scope. +Infix "/" := BinNat.N.div : N_scope. +Infix "^" := BinNat.N.pow : N_scope. + +Delimit Scope Z_scope with Z. +Infix "+" := BinInt.Z.add : Z_scope. +Infix "*" := BinInt.Z.mul : Z_scope. +Infix "-" := BinInt.Z.sub : Z_scope. +Infix "/" := BinInt.Z.div : Z_scope. +Infix "^" := BinInt.Z.pow : Z_scope. +Infix "mod" := BinInt.Z.modulo (at level 40, no associativity) : Z_scope. +Local Open Scope Z_scope. + +Definition F (modulus : BinInt.Z) := { z : BinInt.Z | z = z mod modulus }. +Section FieldOperations. + Context {m : BinInt.Z}. + + Let Fm := F m. (* TODO: if inlined, coercions say "anomaly please report" *) + Coercion ZToField (a:BinInt.Z) : Fm := exist _ (a mod m) (Pre.Z_mod_mod a m). + Coercion FieldToZ (a:Fm) : BinInt.Z := proj1_sig a. + + Definition add (a b:Fm) : Fm := ZToField (a + b). + Definition mul (a b:Fm) : Fm := ZToField (a * b). + + Parameter opp : Fm -> Fm. + Axiom F_opp_spec : forall (a:Fm), add a (opp a) = 0 /\ opp a = opp a mod m. + Definition sub (a b:Fm) : Fm := add a (opp b). + + Parameter inv : Fm -> Fm. + Axiom F_inv_spec : forall (a:Fm), mul a (inv a) = 1 /\ inv 0 = 0 /\ inv a = inv a mod m. + Definition div (a b:Fm) : Fm := mul a (inv b). + + Parameter pow : Fm -> BinNums.N -> Fm. + Axiom F_pow_spec : forall a, pow a 0%N = 1 /\ forall x y, pow a (x + y)%N = pow a x * pow a y. +End FieldOperations. + +Delimit Scope F_scope with F. +Arguments ZToField {_} _%Z : simpl never. +Arguments add {_} _%F _%F : simpl never. +Arguments mul {_} _%F _%F : simpl never. +Arguments sub {_} _%F _%F : simpl never. +Arguments div {_} _%F _%F : simpl never. +Arguments pow {_} _%F _%N : simpl never. +Arguments inv {_} _%F : simpl never. +Arguments opp {_} _%F : simpl never. +Local Open Scope F_scope. +Infix "+" := add : F_scope. +Infix "*" := mul : F_scope. +Infix "-" := sub : F_scope. +Infix "/" := div : F_scope. +Infix "^" := pow : F_scope. +Notation "0" := (ZToField 0) : F_scope. +Notation "1" := (ZToField 1) : F_scope. -- cgit v1.2.3 From 056018a4ade16f17fca77289d8f6443f31b59496 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 11 Feb 2016 16:32:41 -0500 Subject: Define F m, a replacement for GF with several benefits. - F has a human readable complete specification - F is a parametric type, not a parametric module - Different F instances can be disambiguated by type inference, which is more conventient that notation scopes. - F has significant support for non-prime moduli - It should be relatively easy to port existing GF code to F. Since the repository currently contains code referencing both F and GF, it makes sense to keep the names different for now. Later, F may or may not be renamed to GF. --- _CoqProject | 8 + src/ModularArithmetic/ModularArithmeticTheorems.v | 350 ++++++++++++++++++++++ src/ModularArithmetic/PrimeFieldTheorems.v | 51 ++++ src/ModularArithmetic/Tutorial.v | 108 +++++++ src/Spec/CompleteEwardsCurve.v | 15 +- src/Spec/ModularArithmetic.v | 21 +- 6 files changed, 536 insertions(+), 17 deletions(-) create mode 100644 src/ModularArithmetic/ModularArithmeticTheorems.v create mode 100644 src/ModularArithmetic/PrimeFieldTheorems.v create mode 100644 src/ModularArithmetic/Tutorial.v (limited to 'src') diff --git a/_CoqProject b/_CoqProject index 55b29744f..c1e10953f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,5 @@ -R src Crypto +src/CompleteEwardsCurve/Pre.v src/Curves/PointFormats.v src/Curves/ScalarMult.v src/Galois/BaseSystem.v @@ -9,8 +10,15 @@ src/Galois/GaloisRep.v src/Galois/GaloisTheory.v src/Galois/GaloisTutorial.v src/Galois/ModularBaseSystem.v +src/Galois/ModularBaseSystem.v +src/ModularArithmetic/ModularArithmeticTheorems.v +src/ModularArithmetic/Pre.v +src/ModularArithmetic/PrimeFieldTheorems.v +src/ModularArithmetic/Tutorial.v src/Rep/ECRep.v src/Rep/GaloisRep.v +src/Spec/CompleteEwardsCurve.v +src/Spec/ModularArithmetic.v src/Specific/EdDSA25519.v src/Specific/GF25519.v src/Tactics/VerdiTactics.v diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v new file mode 100644 index 000000000..9bbaac489 --- /dev/null +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -0,0 +1,350 @@ +Require Import Spec.ModularArithmetic. + +Require Import Eqdep_dec. +Require Import Tactics.VerdiTactics. +Require Import BinInt Zdiv Znumtheory NArith. (* import Zdiv before Znumtheory *) +Require Import Coq.Classes.Morphisms Setoid. +Require Export Ring_theory Field_theory Field_tac. + +Theorem F_eq: forall {m} (x y : F m), x = y <-> FieldToZ x = FieldToZ y. +Proof. + destruct x, y; intuition; simpl in *; try congruence. + subst_max. + f_equal. + eapply UIP_dec, Z.eq_dec. +Qed. + +(* Fails iff the input term does some arithmetic with mod'd values. *) +Ltac notFancy E := +match E with +| - (_ mod _) => idtac +| context[_ mod _] => fail 1 +| _ => idtac +end. + +Lemma Zplus_neg : forall n m, n + -m = n - m. +Proof. + auto. +Qed. + +Lemma Zmod_eq : forall a b n, a = b -> a mod n = b mod n. +Proof. + intros; rewrite H; trivial. +Qed. + +(* Remove redundant [mod] operations from the conclusion. *) +Ltac demod := + repeat match goal with + | [ |- context[(?x mod _ + _) mod _] ] => + notFancy x; rewrite (Zplus_mod_idemp_l x) + | [ |- context[(_ + ?y mod _) mod _] ] => + notFancy y; rewrite (Zplus_mod_idemp_r y) + | [ |- context[(?x mod _ - _) mod _] ] => + notFancy x; rewrite (Zminus_mod_idemp_l x) + | [ |- context[(_ - ?y mod _) mod _] ] => + notFancy y; rewrite (Zminus_mod_idemp_r _ y) + | [ |- context[(?x mod _ * _) mod _] ] => + notFancy x; rewrite (Zmult_mod_idemp_l x) + | [ |- context[(_ * (?y mod _)) mod _] ] => + notFancy y; rewrite (Zmult_mod_idemp_r y) + | [ |- context[(?x mod _) mod _] ] => + notFancy x; rewrite (Zmod_mod x) + | _ => rewrite Zplus_neg in * || rewrite Z.sub_diag in * + end. + +(* Remove exists under equals: we do this a lot *) +Ltac eq_remove_proofs := lazymatch goal with +| [ |- @eq (F _) ?a ?b ] => + assert (Q := F_eq a b); + simpl in *; apply Q; clear Q +end. + +Ltac Fdefn := + intros; + unfold unfoldFm; + rewrite ?F_opp_spec; + repeat match goal with [ x : F _ |- _ ] => destruct x end; + try eq_remove_proofs; + demod; + rewrite ?Z.mul_1_l; + intuition; demod; try solve [ f_equal; intuition ]. + +Local Open Scope F_scope. + +Section FEquality. + Context {m:Z}. + + (** Equality **) + Definition F_eqb (x y : F m) : bool := Z.eqb x y. + + Lemma F_eqb_eq x y : F_eqb x y = true -> x = y. + Proof. + unfold F_eqb; Fdefn; apply Z.eqb_eq; trivial. + Qed. + + Lemma F_eqb_complete : forall x y: F m, x = y -> F_eqb x y = true. + Proof. + intros; subst; apply Z.eqb_refl. + Qed. + + Lemma F_eqb_refl : forall x, F_eqb x x = true. + Proof. + intros; apply F_eqb_complete; trivial. + Qed. + + Lemma F_eqb_neq x y : F_eqb x y = false -> x <> y. + Proof. + intuition; subst y. + pose proof (F_eqb_refl x). + congruence. + Qed. + + Lemma F_eqb_neq_complete x y : x <> y -> F_eqb x y = false. + Proof. + intros. + case_eq (F_eqb x y); intros; trivial. + pose proof (F_eqb_eq x y); intuition. + Qed. + + Lemma F_eq_dec : forall x y : F m, {x = y} + {x <> y}. + Proof. + intros; case_eq (F_eqb x y); [left|right]; auto using F_eqb_eq, F_eqb_neq. + Qed. + + Lemma if_F_eq_dec_if_F_eqb : forall {T} x y (a b:T), (if F_eq_dec x y then a else b) = (if F_eqb x y then a else b). + Proof. + intros; intuition; break_if. + - rewrite F_eqb_complete; trivial. + - rewrite F_eqb_neq_complete; trivial. + Defined. +End FEquality. + +Section FandZ. + Local Set Printing Coercions. + Context {m:Z}. + + Lemma ZToField_small_nonzero : forall z, (0 < z < m)%Z -> ZToField z <> (0:F m). + Proof. + intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition. + Qed. + + Lemma ZToField_0 : @ZToField m 0 = 0. + Proof. + Fdefn. + Qed. + + Lemma FieldToZ_ZToField : forall z, FieldToZ (@ZToField m z) = z mod m. + Proof. + Fdefn. + Qed. + + Lemma mod_FieldToZ : forall x, (@FieldToZ m x) mod m = FieldToZ x. + Proof. + Fdefn. + Qed. + + (** ZToField distributes over operations **) + Lemma ZToField_add : forall (x y : Z), + @ZToField m (x + y) = ZToField x + ZToField y. + Proof. + Fdefn. + Qed. + + Lemma FieldToZ_add : forall x y : F m, + FieldToZ (x + y) = ((FieldToZ x + FieldToZ y) mod m)%Z. + Proof. + Fdefn. + Qed. + + Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m -> + b mod m = (- a) mod m. + Admitted. + + Lemma FieldToZ_opp' : forall x, FieldToZ (@opp m x) mod m = -x mod m. + Proof. + intros. + pose proof (FieldToZ_add x (opp x)) as H. + rewrite F_opp_spec, FieldToZ_ZToField in H. + auto using mod_plus_zero_subproof. + Qed. + + Lemma FieldToZ_opp : forall x, FieldToZ (@opp m x) = -x mod m. + Proof. + intros. + pose proof (FieldToZ_opp' x) as H; rewrite mod_FieldToZ in H; trivial. + Qed. + + (* Compatibility between inject and subtraction *) + Lemma ZToField_sub : forall (x y : Z), + @ZToField m (x - y) = ZToField x - ZToField y. + Proof. + repeat progress Fdefn. + rewrite Zplus_mod, FieldToZ_opp', FieldToZ_ZToField. + demod; reflexivity. + Qed. + + (* Compatibility between inject and multiplication *) + Lemma ZToField_mul : forall (x y : Z), + @ZToField m (x * y) = ZToField x * ZToField y. + Proof. + Fdefn. + Qed. + + (* Compatibility between inject and GFtoZ *) + Lemma ZToField_idempotent : forall (x : F m), ZToField x = x. + Proof. + Fdefn. + Qed. + + (* Compatibility between inject and mod *) + Lemma ZToField_mod : forall x, @ZToField m x = ZToField (x mod m). + Proof. + Fdefn. + Qed. +End FandZ. + +Section RingModuloPre. + Context {m:Z}. + (* Substitution to prove all Compats *) + Ltac compat := repeat intro; subst; trivial. + + Instance Fplus_compat : Proper (eq==>eq==>eq) (@add m). + Proof. + compat. + Qed. + + Instance Fminus_compat : Proper (eq==>eq==>eq) (@sub m). + Proof. + compat. + Qed. + + Instance Fmult_compat : Proper (eq==>eq==>eq) (@mul m). + Proof. + compat. + Qed. + + Instance Fopp_compat : Proper (eq==>eq) (@opp m). + Proof. + compat. + Qed. + + Instance Finv_compat : Proper (eq==>eq) (@inv m). + Proof. + compat. + Qed. + + Instance Fdiv_compat : Proper (eq==>eq==>eq) (@div m). + Proof. + compat. + Qed. + + (***** Ring Theory *****) + Definition Fring_theory : ring_theory 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq. + Proof. + constructor; Fdefn. + Qed. + + Lemma pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n. + Proof. + destruct (F_pow_spec x) as [HO HS]. + Admitted. + + (***** Power theory *****) + Lemma Fpower_theory : power_theory 1%F (@mul m) eq id (@pow m). + Proof. + constructor; apply pow_pow_N. + Qed. + + (***** Division Theory *****) + Definition Fquotrem(a b: F m): F m * F m := + let '(q, r) := (Z.quotrem a b) in (ZToField q, ZToField r). + Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) Fquotrem. + Proof. + constructor; intros; unfold Fquotrem, id. + + replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b) by + try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). + + Fdefn; rewrite <-Z.quot_rem'; trivial. + Qed. + + Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m. + Admitted. + + (* Define a "ring morphism" between GF and Z, i.e. an equivalence + * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'. + * + * Doing this allows us to do our coefficient manipulations in Z + * rather than GF, because we know it's equivalent to inject the + * result afterward. + *) + Lemma Fring_morph: + ring_morph 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq + 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb + (@ZToField m). + Proof. + constructor; intros; try Fdefn; unfold id, unfoldFm; + try (apply gf_eq; simpl; intuition). + + - rewrite FieldToZ_opp, FieldToZ_ZToField; demod; trivial. + - rewrite FieldToZ_opp, FieldToZ_ZToField, Z_mod_opp; trivial. + - rewrite (proj1 (Z.eqb_eq x y)); trivial. + Qed. + + (* Redefine our division theory under the ring morphism *) + Lemma Fmorph_div_theory: + div_theory eq Zplus Zmult (@ZToField m) Z.quotrem. + Proof. + constructor; intros; intuition. + replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); + try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). + + eq_remove_proofs; demod; + rewrite <- (Z.quot_rem' a b); + destruct a; simpl; trivial. + Qed. + + Lemma ZToField_1 : @ZToField m 1 = 1. + Proof. + Fdefn. + Qed. +End RingModuloPre. + +Module Type Modulus. + Parameter modulus : Z. +End Modulus. + +Module RingModulo (Export M : Modulus). + (* Add our ring with all the fixin's *) + Definition ring_theory_modulo := @Fring_theory modulus. + Definition ring_morph_modulo := @Fring_morph modulus. + Definition morph_div_theory_modulo := @Fmorph_div_theory modulus. + Definition power_theory_modulo := @Fpower_theory modulus. + + Ltac Fexp_tac t := Ncst t. + + (* Expose the carrier in constants so field can simplify them *) + Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1. + + (* Split up the equation (because field likes /\, then + * change back all of our GFones and GFzeros. *) + Ltac Fpostprocess := + repeat split; + repeat match goal with [ |- context[exist ?a ?b (Pre.Z_mod_mod ?x ?q)] ] => + replace (exist a b (Pre.Z_mod_mod x)) with (@ZToField q x%Z) by reflexivity + end; + rewrite ?ZToField_0, ?ZToField_1. + + (* Tactic to passively convert from GF to Z in special circumstances *) + Ltac Fconstant t := + match t with + | @ZToField _ ?x => x + | _ => NotConstant + end. + + Add Ring GFring_Z : ring_theory_modulo + (morphism ring_morph_modulo, + constants [Fconstant], + div morph_div_theory_modulo, + power_tac power_theory_modulo [Fexp_tac]). +End RingModulo. \ No newline at end of file diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v new file mode 100644 index 000000000..4cdd1192e --- /dev/null +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -0,0 +1,51 @@ +Require Export Spec.ModularArithmetic ModularArithmetic.ModularArithmeticTheorems. +Require Export Ring_theory Field_theory Field_tac. + +Require Import Tactics.VerdiTactics. +Require Import Coq.Classes.Morphisms Setoid. +Require Import BinInt BinNat ZArith Znumtheory NArith. (* import Zdiv before Znumtheory *) +Require Import Eqdep_dec. + +Existing Class prime. + +Section FieldModuloPre. + Context {q:Z} {prime_q:prime q}. + Local Open Scope F_scope. + + Lemma Fq_1_neq_0 : (1:F q) <> (0:F q). + Proof. + pose proof prime_ge_2 q _. + rewrite F_eq, !FieldToZ_ZToField, !Zmod_small by omega; congruence. + Qed. + + Lemma F_mul_inv_l : forall x : F q, inv x * x = 1. + Proof. + intros. + rewrite <-(proj1 (F_inv_spec _ x)). + Fdefn. + Qed. + + (* Add an abstract field (without modifiers) *) + Definition Ffield_theory : field_theory 0%F 1%F (@add q) (@mul q) (@sub q) (@opp q) (@div q) (@inv q) eq. + Proof. + constructor; auto using Fring_theory, Fq_1_neq_0, F_mul_inv_l. + Qed. +End FieldModuloPre. + +Module Type PrimeModulus. + Parameter modulus : Z. + Parameter prime_modulus : prime modulus. +End PrimeModulus. + +Module FieldModulo (Import M : PrimeModulus). + (* Add our field with all the fixin's *) + Module Import RingM := RingModulo M. + Definition field_theory_modulo := @Ffield_theory modulus prime_modulus. + Add Field Ffield_Z : field_theory_modulo + (morphism ring_morph_modulo, + preprocess [Fpreprocess], + postprocess [Fpostprocess], + constants [Fconstant], + div morph_div_theory_modulo, + power_tac power_theory_modulo [Fexp_tac]). +End FieldModulo. \ No newline at end of file diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v new file mode 100644 index 000000000..e84659c9e --- /dev/null +++ b/src/ModularArithmetic/Tutorial.v @@ -0,0 +1,108 @@ +Require Import BinInt Zpower ZArith Znumtheory. +Require Import Spec.ModularArithmetic ModularArithmetic.PrimeFieldTheorems. + +Module Modulus31 <: PrimeModulus. + Definition modulus := 2^5 - 1. + Lemma prime_modulus : prime modulus. + Admitted. +End Modulus31. + +Module Modulus127 <: PrimeModulus. + Definition modulus := 2^127 - 1. + Lemma prime_modulus : prime modulus. + Admitted. +End Modulus127. + +Module Example31. + (* Then we can construct a field with that modulus *) + Module Import Field := FieldModulo Modulus31. + Import Modulus31. + + (* And pull in the appropriate notations *) + Local Open Scope F_scope. + + (* First, let's solve a ring example*) + Lemma ring_example: forall x: F modulus, x * (ZToField 2) = x + x. + Proof. + intros. + ring. + Qed. + + (* Unfortunately, the [ring] and [field] tactics need syntactic + (not definitional) equality to recognize the ring in question. + Therefore, it is necessary to explicitly rewrite the modulus + (usually hidden by implicitn arguments) match the one passed to + [FieldModulo]. *) + Lemma ring_example': forall x: F (2^5-1), x * (ZToField 2) = x + x. + Proof. + intros. + change (2^5-1)%Z with modulus. + ring. + Qed. + + (* Then a field example (we have to know we can't divide by zero!) *) + Lemma field_example: forall x y z: F modulus, z <> 0 -> + x * (y / z) / z = x * y / (z ^ 2). + Proof. + intros; simpl. + field; trivial. + Qed. + + (* Then an example with exponentiation *) + Lemma exp_example: forall x: F modulus, x ^ 2 + ZToField 2 * x + 1 = (x + 1) ^ 2. + Proof. + intros; simpl. + field; trivial. + Qed. + + (* In general, the rule I've been using is: + + - If our goal looks like x = y: + + + If we need to use assumptions to prove the goal, then before + we apply field, + + * Perform all relevant substitutions (especially subst) + + * If we have something more complex, we're probably going + to have to performe some sequence of "replace X with Y" + and solve out the subgoals manually before we can use + field. + + + Else, just use field directly + + - If we just want to simplify terms and put them into a canonical + form, then field_simplify or ring_simplify should do the trick. + Note, however, that the canonical form has lots of annoying "/1"s + + - Otherwise, do a "replace X with Y" to generate an equality + so that we can use field in the above case + + *) + +End Example31. + +(* Notice that the field tactics work whether we know what the modulus is *) +Module TimesZeroTransparentTestModule. + Module Import Theory := FieldModulo Modulus127. + Import Modulus127. + Local Open Scope F_scope. + + Lemma timesZero : forall a : F modulus, a*0 = 0. + intros. + field. + Qed. +End TimesZeroTransparentTestModule. + +(* Or if we don't (i.e. it's opaque) *) +Module TimesZeroParametricTestModule (M: PrimeModulus). + Module Theory := FieldModulo M. + Import Theory M. + Local Open Scope F_scope. + + Lemma timesZero : forall a : F modulus, a*0 = 0. + intros. + field. + Qed. +End TimesZeroParametricTestModule. + diff --git a/src/Spec/CompleteEwardsCurve.v b/src/Spec/CompleteEwardsCurve.v index 7ebf35988..8eeefe03b 100644 --- a/src/Spec/CompleteEwardsCurve.v +++ b/src/Spec/CompleteEwardsCurve.v @@ -6,17 +6,18 @@ Require Import Crypto.Spec.ModularArithmetic. Local Open Scope F_scope. Class TwistedEdwardsParams := { - p : BinInt.Z; - a : F p; - d : F p; - modulus_prime : Znumtheory.prime p; + q : BinInt.Z; + a : F q; + d : F q; + modulus_prime : Znumtheory.prime q; a_nonzero : a <> 0; a_square : exists sqrt_a, sqrt_a^2 = a; d_nonsquare : forall x, x^2 <> d }. Section TwistedEdwardsCurves. - Context `{prm:TwistedEdwardsParams}. + Context {prm:TwistedEdwardsParams}. + (* Twisted Edwards curves with complete addition laws. References: * * @@ -24,9 +25,7 @@ Section TwistedEdwardsCurves. *) Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. Definition point := { P | onCurve P}. - Definition mkPoint xy proof : point := exist onCurve xy proof. - Definition projX (P:point) : F p := fst (proj1_sig P). - Definition projY (P:point) : F p:= snd (proj1_sig P). + Definition mkPoint (xy:F q * F q) (pf:onCurve xy) : point := exist onCurve xy pf. Definition zero : point := mkPoint (0, 1) Pre.zeroOnCurve. diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index 7f31161e2..e2243dfff 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -1,4 +1,4 @@ -Require Znumtheory BinInt BinNums. +Require Znumtheory BinNums. Require Crypto.ModularArithmetic.Pre. @@ -19,29 +19,32 @@ Infix "mod" := BinInt.Z.modulo (at level 40, no associativity) : Z_scope. Local Open Scope Z_scope. Definition F (modulus : BinInt.Z) := { z : BinInt.Z | z = z mod modulus }. +Coercion FieldToZ {m} (a:F m) : BinNums.Z := proj1_sig a. + Section FieldOperations. Context {m : BinInt.Z}. - Let Fm := F m. (* TODO: if inlined, coercions say "anomaly please report" *) - Coercion ZToField (a:BinInt.Z) : Fm := exist _ (a mod m) (Pre.Z_mod_mod a m). - Coercion FieldToZ (a:Fm) : BinInt.Z := proj1_sig a. - + Let Fm := F m. (* Note: if inlined, coercions say "anomaly please report" *) + Coercion unfoldFm (a:Fm) : F m := a. + Coercion ZToField (a:BinNums.Z) : Fm := exist _ (a mod m) (Pre.Z_mod_mod a m). + Definition add (a b:Fm) : Fm := ZToField (a + b). Definition mul (a b:Fm) : Fm := ZToField (a * b). Parameter opp : Fm -> Fm. - Axiom F_opp_spec : forall (a:Fm), add a (opp a) = 0 /\ opp a = opp a mod m. + Axiom F_opp_spec : forall (a:Fm), add a (opp a) = 0. Definition sub (a b:Fm) : Fm := add a (opp b). Parameter inv : Fm -> Fm. - Axiom F_inv_spec : forall (a:Fm), mul a (inv a) = 1 /\ inv 0 = 0 /\ inv a = inv a mod m. + Axiom F_inv_spec : Znumtheory.prime m -> forall (a:Fm), mul a (inv a) = 1 /\ inv 0 = 0. Definition div (a b:Fm) : Fm := mul a (inv b). Parameter pow : Fm -> BinNums.N -> Fm. - Axiom F_pow_spec : forall a, pow a 0%N = 1 /\ forall x y, pow a (x + y)%N = pow a x * pow a y. + Axiom F_pow_spec : forall a, pow a 0%N = 1 /\ forall x, pow a (1 + x)%N = mul a (pow a x). End FieldOperations. Delimit Scope F_scope with F. +Arguments F _%Z. Arguments ZToField {_} _%Z : simpl never. Arguments add {_} _%F _%F : simpl never. Arguments mul {_} _%F _%F : simpl never. @@ -57,4 +60,4 @@ Infix "-" := sub : F_scope. Infix "/" := div : F_scope. Infix "^" := pow : F_scope. Notation "0" := (ZToField 0) : F_scope. -Notation "1" := (ZToField 1) : F_scope. +Notation "1" := (ZToField 1) : F_scope. \ No newline at end of file -- cgit v1.2.3 From 7ce9586da796da9e7656e691f8e63d4f59257649 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 11 Feb 2016 17:57:57 -0500 Subject: port several theorems from GF to F --- src/CompleteEwardsCurve/Pre.v | 25 ++++--- src/ModularArithmetic/ModularArithmeticTheorems.v | 88 +++++++++++++++++------ src/ModularArithmetic/PrimeFieldTheorems.v | 67 ++++++++++++++++- src/Specific/EdDSA25519.v | 3 +- 4 files changed, 150 insertions(+), 33 deletions(-) (limited to 'src') diff --git a/src/CompleteEwardsCurve/Pre.v b/src/CompleteEwardsCurve/Pre.v index d66ed8fab..27f7619dc 100644 --- a/src/CompleteEwardsCurve/Pre.v +++ b/src/CompleteEwardsCurve/Pre.v @@ -1,17 +1,26 @@ Require Import BinInt Znumtheory VerdiTactics. Require Import Crypto.Spec.ModularArithmetic. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Local Open Scope F_scope. Section Pre. - Context {p : BinInt.Z}. - Context {a : F p}. - Context {d : F p}. - Context {modulus_prime : Znumtheory.prime p}. - Context {modulus_lt_2 : 2 < p}. + Context {q : BinInt.Z}. + Context {a : F q}. + Context {d : F q}. + Context {prime_q : Znumtheory.prime q}. + Context {two_lt_q : 2 < q}. Context {a_nonzero : a <> 0}. Context {a_square : exists sqrt_a, sqrt_a^2 = a}. Context {d_nonsquare : forall x, x^2 <> d}. + + Add Field Ffield_Z : (@Ffield_theory q _) + (morphism (@Fring_morph q), + preprocess [Fpreprocess], + postprocess [Fpostprocess], + constants [Fconstant], + div (@Fmorph_div_theory q), + power_tac (@Fpower_theory q) [Fexp_tac]). (* the canonical definitions are in Spec *) Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2). @@ -21,10 +30,10 @@ Section Pre. (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))) ). - Lemma char_gt_2 : ZToField 2 <> (0: F p). + Lemma char_gt_2 : ZToField 2 <> (0: F q). intro; find_injection. - pose proof modulus_lt_2. - rewrite (Z.mod_small 2 p), Z.mod_0_l in *; omega. + pose proof two_lt_q. + rewrite (Z.mod_small 2 q), Z.mod_0_l in *; omega. Qed. (* diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 9bbaac489..f4d3b87ff 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -309,42 +309,84 @@ Section RingModuloPre. Fdefn. Qed. End RingModuloPre. + +Ltac Fconstant t := match t with @ZToField _ ?x => x | _ => NotConstant end. +Ltac Fexp_tac t := Ncst t. +Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1. +Ltac Fpostprocess := repeat split; + repeat match goal with [ |- context[exist ?a ?b (Pre.Z_mod_mod ?x ?q)] ] => + change (exist a b (Pre.Z_mod_mod x)) with (@ZToField q x%Z) end; + rewrite ?ZToField_0, ?ZToField_1. Module Type Modulus. Parameter modulus : Z. End Modulus. +(* Example of how to instantiate the ring tactic *) Module RingModulo (Export M : Modulus). - (* Add our ring with all the fixin's *) Definition ring_theory_modulo := @Fring_theory modulus. Definition ring_morph_modulo := @Fring_morph modulus. Definition morph_div_theory_modulo := @Fmorph_div_theory modulus. Definition power_theory_modulo := @Fpower_theory modulus. - - Ltac Fexp_tac t := Ncst t. - - (* Expose the carrier in constants so field can simplify them *) - Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1. - - (* Split up the equation (because field likes /\, then - * change back all of our GFones and GFzeros. *) - Ltac Fpostprocess := - repeat split; - repeat match goal with [ |- context[exist ?a ?b (Pre.Z_mod_mod ?x ?q)] ] => - replace (exist a b (Pre.Z_mod_mod x)) with (@ZToField q x%Z) by reflexivity - end; - rewrite ?ZToField_0, ?ZToField_1. - - (* Tactic to passively convert from GF to Z in special circumstances *) - Ltac Fconstant t := - match t with - | @ZToField _ ?x => x - | _ => NotConstant - end. Add Ring GFring_Z : ring_theory_modulo (morphism ring_morph_modulo, constants [Fconstant], div morph_div_theory_modulo, power_tac power_theory_modulo [Fexp_tac]). -End RingModulo. \ No newline at end of file +End RingModulo. + +Section VariousModulo. + Context {m:Z}. + + Add Ring GFring_Z : (@Fring_theory m) + (morphism (@Fring_morph m), + constants [Fconstant], + div (@Fmorph_div_theory m), + power_tac (@Fpower_theory m) [Fexp_tac]). + + Lemma F_mul_0_l : forall x : F m, 0 * x = 0. + Proof. + intros; ring. + Qed. + + Lemma F_mul_0_r : forall x : F m, x * 0 = 0. + Proof. + intros; ring. + Qed. + + Lemma F_mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0. + intros; intuition; subst. + assert (0 * b = 0) by ring; intuition. + Qed. + + Lemma F_mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0. + intros; intuition; subst. + assert (a * 0 = 0) by ring; intuition. + Qed. + + Lemma F_pow_distr_mul : forall (x y:F m) z, (0 <= z)%N -> + (x ^ z) * (y ^ z) = (x * y) ^ z. + Proof. + intros. + replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id. + apply natlike_ind with (x := Z.of_N z); simpl; [ ring | | + replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto]. + intros z' z'_nonneg IHz'. + rewrite Z2N.inj_succ by auto. + rewrite <-N.add_1_l. + rewrite !(proj2 (@F_pow_spec m _) _). + rewrite <- IHz'. + ring. + Qed. + + Lemma F_opp_swap : forall x y : F m, opp x = y <-> x = opp y. + Proof. + split; intro; subst; ring. + Qed. + + Lemma F_opp_involutive : forall x : F m, opp (opp x) = x. + Proof. + intros; ring. + Qed. +End VariousModulo. \ No newline at end of file diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 4cdd1192e..b652a8e84 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -48,4 +48,69 @@ Module FieldModulo (Import M : PrimeModulus). constants [Fconstant], div morph_div_theory_modulo, power_tac power_theory_modulo [Fexp_tac]). -End FieldModulo. \ No newline at end of file +End FieldModulo. + +Section VariousModPrime. + Context {q:Z} {prime_q:prime q}. + Local Open Scope F_scope. + Add Field Ffield_Z : (@Ffield_theory q _) + (morphism (@Fring_morph q), + preprocess [Fpreprocess], + postprocess [Fpostprocess], + constants [Fconstant], + div (@Fmorph_div_theory q), + power_tac (@Fpower_theory q) [Fexp_tac]). + + Lemma Fq_mul_eq : forall x y z : F q, z <> 0 -> x * z = y * z -> x = y. + Proof. + intros ? ? ? z_nonzero mul_z_eq. + assert (x * z * inv z = y * z * inv z) as H by (rewrite mul_z_eq; reflexivity). + replace (x * z * inv z) with (x * (z * inv z)) in H by (field; trivial). + replace (y * z * inv z) with (y * (z * inv z)) in H by (field; trivial). + rewrite (proj1 (@F_inv_spec q _ _)) in H. + replace (x * 1) with x in H by field. + replace (y * 1) with y in H by field. + trivial. + Qed. + + Lemma Fq_mul_zero_why : forall a b : F q, a*b = 0 -> a = 0 \/ b = 0. + intros. + assert (Z := F_eq_dec a 0); destruct Z. + + - left; intuition. + + - assert (a * b / a = 0) by + ( rewrite H; field; intuition ). + + replace (a*b/a) with (b) in H0 by (field; trivial). + right; intuition. + Qed. + + Lemma Fq_mul_nonzero_nonzero : forall a b : F q, a <> 0 -> b <> 0 -> a*b <> 0. + intros; intuition; subst. + apply Fq_mul_zero_why in H1. + destruct H1; subst; intuition. + Qed. + Hint Resolve Fq_mul_nonzero_nonzero. + + Lemma F_square_mul : forall x y z : F q, (y <> 0) -> + x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z. + Proof. + intros ? ? ? y_nonzero A. + exists (x / y). + assert ((x / y) ^ 2 = x ^ 2 / y ^ 2) as square_distr_div by (field; trivial). + assert (y ^ 2 <> 0) as y2_nonzero by ( + change (2%N) with (1+(1+0))%N; + rewrite !(proj2 (@F_pow_spec q _) _), !(proj1 (@F_pow_spec q _)); + auto 10 using Fq_mul_nonzero_nonzero, Fq_1_neq_0). + rewrite (Fq_mul_eq _ z (y ^ 2)); auto. + rewrite <- A. + field; trivial. + Qed. + + Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x. + Proof. + intros. + (* TODO(jadep) *) + Admitted. +End VariousModPrime. \ No newline at end of file diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v index 96f997180..6403c8b53 100644 --- a/src/Specific/EdDSA25519.v +++ b/src/Specific/EdDSA25519.v @@ -557,7 +557,8 @@ Module EdDSA25519_Params <: EdDSAParams. I have so far not managed to unify them. *) Lemma point_eq_copy : forall x1 x2 y1 y2, x1 = x2 -> y1 = y2 -> forall p1 p2, mkPoint (x1, y1) p1 = mkPoint (x2, y2) p2. - Admitted. + apply Facts.point_eq. + Qed. Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p. Proof. -- cgit v1.2.3 From 0fe6fb9b908e5c4909ef31a5243d3f9f6a8d083f Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 11 Feb 2016 20:10:39 -0500 Subject: port some Edwards curve stuff from GF to F --- src/CompleteEwardsCurve/Pre.v | 80 ++++++++++++++++-------------- src/ModularArithmetic/PrimeFieldTheorems.v | 28 ++++++++++- 2 files changed, 69 insertions(+), 39 deletions(-) (limited to 'src') diff --git a/src/CompleteEwardsCurve/Pre.v b/src/CompleteEwardsCurve/Pre.v index 27f7619dc..16001ab16 100644 --- a/src/CompleteEwardsCurve/Pre.v +++ b/src/CompleteEwardsCurve/Pre.v @@ -35,58 +35,59 @@ Section Pre. pose proof two_lt_q. rewrite (Z.mod_small 2 q), Z.mod_0_l in *; omega. Qed. + + Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end. + Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end. - (* Ltac whatsNotZero := repeat match goal with | [H: ?lhs = ?rhs |- _ ] => match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (lhs <> 0) by (rewrite H; auto) + assert (lhs <> 0) by (rewrite H; auto using Fq_1_neq_0) | [H: ?lhs = ?rhs |- _ ] => match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (rhs <> 0) by (rewrite H; auto) + assert (rhs <> 0) by (rewrite H; auto using Fq_1_neq_0) | [H: (?a^?p)%F <> 0 |- _ ] => match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; let Y:=fresh in let Z:=fresh in try ( assert (p <> 0%N) as Z by (intro Y; inversion Y); - assert (a <> 0) by (eapply root_nonzero; eauto); + assert (a <> 0) by (eapply Fq_root_nonzero; eauto using Fq_1_neq_0); clear Z) | [H: (?a*?b)%F <> 0 |- _ ] => match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (a <> 0) by (eapply mul_nonzero_l; eauto) + assert (a <> 0) by (eapply F_mul_nonzero_l; eauto using Fq_1_neq_0) | [H: (?a*?b)%F <> 0 |- _ ] => match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (b <> 0) by (eapply mul_nonzero_r; eauto) + assert (b <> 0) by (eapply F_mul_nonzero_r; eauto using Fq_1_neq_0) end. - *) - + Lemma edwardsAddComplete' x1 y1 x2 y2 : onCurve (x1, y1) -> onCurve (x2, y2) -> (d*x1*x2*y1*y2)^2 <> 1. - Proof. (* - intuition; whatsNotZero. + Proof. + intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero. pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. - destruct a_square as [sqrt_a a_square]. - rewrite <-a_square in *. + destruct a_square as [sqrt_a a_square']. + rewrite <-a_square' in *. (* Furthermore... *) pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt. - rewrite H0 in Heqt at 2. + rewrite Hc2 in Heqt at 2. replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2)) with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field. - rewrite H1 in Heqt. + rewrite Hcontra in Heqt. replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field. - rewrite <-H in Heqt. + rewrite <-Hc1 in Heqt. (* main equation for both potentially nonzero denominators *) - case_eq_GF (sqrt_a*x2 + y2) 0; case_eq_GF (sqrt_a*x2 - y2) 0; - try match goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] => + destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0); + try lazymatch goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] => assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 = f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2) - (d * x1 * x2 * y1 * y2*sqrt_a*(inject 2)*x1*y1)) as Heqw1 by field; - rewrite H1 in *; + (d * x1 * x2 * y1 * y2*sqrt_a*(ZToField 2)*x1*y1)) as Heqw1 by field; + rewrite Hcontra in Heqw1; replace (1 * y1^2) with (y1^2) in * by field; rewrite <- Heqt in *; assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 / @@ -99,45 +100,45 @@ Section Pre. assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field). - replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (inject 2 * sqrt_a * x2) in Hc by field. + replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field. (* contradiction: product of nonzero things is zero *) - destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition. - destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition. + destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition. + destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition. apply Ha_nonzero; field. - Qed - *) Admitted. + Qed. + Lemma edwardsAddCompletePlus x1 y1 x2 y2 : onCurve (x1, y1) -> onCurve (x2, y2) -> (1 + d*x1*x2*y1*y2) <> 0. - Proof. (* - intros; case_eq_GF (d*x1*x2*y1*y2) (0-1)%GF. + Proof. + intros Hc1 Hc2; simpl in Hc1, Hc2. + intros; destruct (F_eq_dec (d*x1*x2*y1*y2) (0-1)) as [H|H]. - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. - - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H1 by field. - intro; rewrite H2 in H1; intuition. + - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field. + intro Hz; rewrite Hz in H; intuition. Qed. - *) Admitted. Lemma edwardsAddCompleteMinus x1 y1 x2 y2 : onCurve (x1, y1) -> onCurve (x2, y2) -> (1 - d*x1*x2*y1*y2) <> 0. - Proof. (* - unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (1)%GF. + Proof. + intros Hc1 Hc2. destruct (F_eq_dec (d*x1*x2*y1*y2) 1) as [H|H]. - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. - - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H1 by field. - intro; rewrite H2 in H1; apply H1; field. + - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field. + intro Hz; rewrite Hz in H; apply H; field. Qed. - *) Admitted. Definition zeroOnCurve : onCurve (0, 1). - Admitted. (* field. *) + simpl. field. + Qed. Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3 (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) : onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3). - Proof. (* + Proof. (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1; * c=1 and an extra a in front of x^2 *) @@ -156,7 +157,7 @@ Section Pre. assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +( (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 * y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field). - replace 1 with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3. + replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3. match goal with [ |- ?x = 1 ] => replace x with ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 + @@ -166,7 +167,10 @@ Section Pre. - rewrite <-HT1, <-HT2; field; rewrite HT1. replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2)) with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) - by field; simpl; auto. + by field; simpl. + SearchAbout pow 0. + eauto using F_mul_nonzero_l, F_mul_nonzero_r. + SearchAbout pow 0. - replace (1 - (d * x1 * x2 * y1 * y2) ^ 2) with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) by field; auto. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index b652a8e84..338903b26 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -93,7 +93,7 @@ Section VariousModPrime. Qed. Hint Resolve Fq_mul_nonzero_nonzero. - Lemma F_square_mul : forall x y z : F q, (y <> 0) -> + Lemma Fq_square_mul : forall x y z : F q, (y <> 0) -> x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z. Proof. intros ? ? ? y_nonzero A. @@ -107,6 +107,32 @@ Section VariousModPrime. rewrite <- A. field; trivial. Qed. + + Lemma Fq_root_zero : forall (x: F q) (p: N), x^p = 0 -> x = 0. + induction p using N.peano_ind; + rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)). + - intros; destruct Fq_1_neq_0; auto. + - intro H; destruct (Fq_mul_zero_why x (x^p) H); auto. + Qed. + + Lemma Fq_root_nonzero : forall (x:F q) p, x^p <> 0 -> (p <> 0)%N -> x <> 0. + induction p using N.peano_ind; + rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)). + - intuition. + - destruct (N.eq_dec p 0); intro H; intros; subst. + + rewrite (proj1 (@F_pow_spec q _)) in H; replace (x*1) with (x) in H by ring; trivial. + + apply IHp; auto. intro Hz; rewrite Hz in *. apply H, F_mul_0_r. + Qed. + + Lemma Fq_pow_nonzero : forall (x : F q) p, x <> 0 -> x^p <> 0. + Proof. + induction p using N.peano_ind; + rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)). + - intuition. auto using Fq_1_neq_0. + - intros H Hc. destruct (Fq_mul_zero_why _ _ Hc). + + intuition. + + apply IHp; auto. + Qed. Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x. Proof. -- cgit v1.2.3 From 41b48a78924a9689b9ab838eb74b1d14f267cdfe Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 11 Feb 2016 21:42:15 -0500 Subject: make field on F automatically clean up the constant-vomit it expands --- src/CompleteEwardsCurve/Pre.v | 17 ++++++++--------- src/ModularArithmetic/ModularArithmeticTheorems.v | 2 +- 2 files changed, 9 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/CompleteEwardsCurve/Pre.v b/src/CompleteEwardsCurve/Pre.v index 16001ab16..e4dc140e1 100644 --- a/src/CompleteEwardsCurve/Pre.v +++ b/src/CompleteEwardsCurve/Pre.v @@ -163,19 +163,18 @@ Section Pre. ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 + ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 - d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/ - ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end; try field; auto. + ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end. - rewrite <-HT1, <-HT2; field; rewrite HT1. replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2)) + with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) by field. + auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero, + edwardsAddCompleteMinus, edwardsAddCompletePlus. + - field; replace (1 - (d * x1 * x2 * y1 * y2) ^ 2) with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) - by field; simpl. - SearchAbout pow 0. - eauto using F_mul_nonzero_l, F_mul_nonzero_r. - SearchAbout pow 0. - - replace (1 - (d * x1 * x2 * y1 * y2) ^ 2) - with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) - by field; auto. + by field; + auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero, + edwardsAddCompleteMinus, edwardsAddCompletePlus. Qed. - *) Admitted. Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index f4d3b87ff..474cd03e1 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -315,7 +315,7 @@ Ltac Fexp_tac t := Ncst t. Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1. Ltac Fpostprocess := repeat split; repeat match goal with [ |- context[exist ?a ?b (Pre.Z_mod_mod ?x ?q)] ] => - change (exist a b (Pre.Z_mod_mod x)) with (@ZToField q x%Z) end; + change (exist a b (Pre.Z_mod_mod x q)) with (@ZToField q x%Z) end; rewrite ?ZToField_0, ?ZToField_1. Module Type Modulus. -- cgit v1.2.3 From 34875f01c422e5665a73f076e7e17b9c7e1d5aa0 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 12 Feb 2016 14:44:48 -0500 Subject: port some edwards curve theorems --- _CoqProject | 5 +- .../CompleteEdwardsCurveTheorems.v | 52 ++++++ src/CompleteEdwardsCurve/Pre.v | 186 +++++++++++++++++++++ src/CompleteEwardsCurve/Pre.v | 186 --------------------- src/Curves/PointFormats.v | 52 +----- src/ModularArithmetic/ModularArithmeticTheorems.v | 30 ++++ src/ModularArithmetic/PrimeFieldTheorems.v | 7 +- src/ModularArithmetic/Tutorial.v | 7 + src/Spec/CompleteEdwardsCurve.v | 52 ++++++ src/Spec/CompleteEwardsCurve.v | 48 ------ 10 files changed, 338 insertions(+), 287 deletions(-) create mode 100644 src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v create mode 100644 src/CompleteEdwardsCurve/Pre.v delete mode 100644 src/CompleteEwardsCurve/Pre.v create mode 100644 src/Spec/CompleteEdwardsCurve.v delete mode 100644 src/Spec/CompleteEwardsCurve.v (limited to 'src') diff --git a/_CoqProject b/_CoqProject index c1e10953f..02a3c797d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,5 +1,6 @@ -R src Crypto -src/CompleteEwardsCurve/Pre.v +src/CompleteEdwardsCurve/Pre.v +src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/Curves/PointFormats.v src/Curves/ScalarMult.v src/Galois/BaseSystem.v @@ -17,7 +18,7 @@ src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/Tutorial.v src/Rep/ECRep.v src/Rep/GaloisRep.v -src/Spec/CompleteEwardsCurve.v +src/Spec/CompleteEdwardsCurve.v src/Spec/ModularArithmetic.v src/Specific/EdDSA25519.v src/Specific/GF25519.v diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v new file mode 100644 index 000000000..90f5907fd --- /dev/null +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -0,0 +1,52 @@ +Require Export Crypto.Spec.CompleteEdwardsCurve. + +Require Import Crypto.CompleteEdwardsCurve.Pre. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Eqdep_dec. +Require Import Crypto.Tactics.VerdiTactics. + +Section CompleteEdwardsCurveTheorems. + Context {prm:TwistedEdwardsParams}. + Existing Instance prime_q. + Add Field Ffield_Z : (@Ffield_theory q _) + (morphism (@Fring_morph q), + preprocess [idtac], + postprocess [try exact Fq_1_neq_0; try assumption], + constants [Fconstant], + div (@Fmorph_div_theory q), + power_tac (@Fpower_theory q) [Fexp_tac]). + + Lemma point_eq : forall p1 p2, p1 = p2 -> forall pf1 pf2, + mkPoint p1 pf1 = mkPoint p2 pf2. + Proof. + destruct p1, p2; intros; find_injection; intros; subst; apply f_equal. + apply UIP_dec, F_eq_dec. (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *) + Qed. + Hint Resolve point_eq. + + Ltac Edefn := unfold unifiedAdd, zero; intros; + repeat match goal with + | [ p : point |- _ ] => + let x := fresh "x" p in + let y := fresh "y" p in + let pf := fresh "pf" p in + destruct p as [[x y] pf]; unfold onCurve in pf + | _ => eapply point_eq, f_equal2 + | _ => eapply point_eq + end. + Lemma twistedAddComm : forall A B, (A+B = B+A)%E. + Proof. + Edefn; f_equal; field. + Qed. + + Lemma twistedAddAssoc : forall A B C, A+(B+C) = (A+B)+C. + Proof. + (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *) + Admitted. + + Lemma zeroIsIdentity : forall P, (P + zero = P)%E. + Proof. + Edefn; repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r, + ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; exact eq_refl. + Qed. +End CompleteEdwardsCurveTheorems. \ No newline at end of file diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v new file mode 100644 index 000000000..e4dc140e1 --- /dev/null +++ b/src/CompleteEdwardsCurve/Pre.v @@ -0,0 +1,186 @@ +Require Import BinInt Znumtheory VerdiTactics. + +Require Import Crypto.Spec.ModularArithmetic. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Local Open Scope F_scope. + +Section Pre. + Context {q : BinInt.Z}. + Context {a : F q}. + Context {d : F q}. + Context {prime_q : Znumtheory.prime q}. + Context {two_lt_q : 2 < q}. + Context {a_nonzero : a <> 0}. + Context {a_square : exists sqrt_a, sqrt_a^2 = a}. + Context {d_nonsquare : forall x, x^2 <> d}. + + Add Field Ffield_Z : (@Ffield_theory q _) + (morphism (@Fring_morph q), + preprocess [Fpreprocess], + postprocess [Fpostprocess], + constants [Fconstant], + div (@Fmorph_div_theory q), + power_tac (@Fpower_theory q) [Fexp_tac]). + + (* the canonical definitions are in Spec *) + Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2). + Local Notation unifiedAdd' P1' P2' := ( + let '(x1, y1) := P1' in + let '(x2, y2) := P2' in + (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))) + ). + + Lemma char_gt_2 : ZToField 2 <> (0: F q). + intro; find_injection. + pose proof two_lt_q. + rewrite (Z.mod_small 2 q), Z.mod_0_l in *; omega. + Qed. + + Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end. + Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end. + + Ltac whatsNotZero := + repeat match goal with + | [H: ?lhs = ?rhs |- _ ] => + match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end; + assert (lhs <> 0) by (rewrite H; auto using Fq_1_neq_0) + | [H: ?lhs = ?rhs |- _ ] => + match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end; + assert (rhs <> 0) by (rewrite H; auto using Fq_1_neq_0) + | [H: (?a^?p)%F <> 0 |- _ ] => + match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; + let Y:=fresh in let Z:=fresh in try ( + assert (p <> 0%N) as Z by (intro Y; inversion Y); + assert (a <> 0) by (eapply Fq_root_nonzero; eauto using Fq_1_neq_0); + clear Z) + | [H: (?a*?b)%F <> 0 |- _ ] => + match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; + assert (a <> 0) by (eapply F_mul_nonzero_l; eauto using Fq_1_neq_0) + | [H: (?a*?b)%F <> 0 |- _ ] => + match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end; + assert (b <> 0) by (eapply F_mul_nonzero_r; eauto using Fq_1_neq_0) + end. + + Lemma edwardsAddComplete' x1 y1 x2 y2 : + onCurve (x1, y1) -> + onCurve (x2, y2) -> + (d*x1*x2*y1*y2)^2 <> 1. + Proof. + intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero. + + pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. + destruct a_square as [sqrt_a a_square']. + rewrite <-a_square' in *. + + (* Furthermore... *) + pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt. + rewrite Hc2 in Heqt at 2. + replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2)) + with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field. + rewrite Hcontra in Heqt. + replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field. + rewrite <-Hc1 in Heqt. + + (* main equation for both potentially nonzero denominators *) + destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0); + try lazymatch goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] => + assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 = + f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2) + (d * x1 * x2 * y1 * y2*sqrt_a*(ZToField 2)*x1*y1)) as Heqw1 by field; + rewrite Hcontra in Heqw1; + replace (1 * y1^2) with (y1^2) in * by field; + rewrite <- Heqt in *; + assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 / + (x1 * y1 * (f (sqrt_a * x2) y2))^2) + by (rewriteAny; field; auto); + match goal with [H: d = (?n^2)/(?l^2) |- _ ] => + destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto) + end + end. + + assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field). + + replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field. + + (* contradiction: product of nonzero things is zero *) + destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition. + destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition. + apply Ha_nonzero; field. + Qed. + + Lemma edwardsAddCompletePlus x1 y1 x2 y2 : + onCurve (x1, y1) -> + onCurve (x2, y2) -> + (1 + d*x1*x2*y1*y2) <> 0. + Proof. + intros Hc1 Hc2; simpl in Hc1, Hc2. + intros; destruct (F_eq_dec (d*x1*x2*y1*y2) (0-1)) as [H|H]. + - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. + - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field. + intro Hz; rewrite Hz in H; intuition. + Qed. + + Lemma edwardsAddCompleteMinus x1 y1 x2 y2 : + onCurve (x1, y1) -> + onCurve (x2, y2) -> + (1 - d*x1*x2*y1*y2) <> 0. + Proof. + intros Hc1 Hc2. destruct (F_eq_dec (d*x1*x2*y1*y2) 1) as [H|H]. + - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. + - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field. + intro Hz; rewrite Hz in H; apply H; field. + Qed. + + Definition zeroOnCurve : onCurve (0, 1). + simpl. field. + Qed. + + Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3 + (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) : + onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3). + Proof. + (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1; + * c=1 and an extra a in front of x^2 *) + + injection H; clear H; intros. + + Ltac t x1 y1 x2 y2 := + assert ((a*x2^2 + y2^2)*d*x1^2*y1^2 + = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto); + assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2 + = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field). + t x1 y1 x2 y2; t x2 y2 x1 y1. + + remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 - + (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T. + assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field). + assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +( + (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 * + y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field). + replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3. + + match goal with [ |- ?x = 1 ] => replace x with + ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 + + ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 - + d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/ + ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end. + - rewrite <-HT1, <-HT2; field; rewrite HT1. + replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2)) + with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) by field. + auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero, + edwardsAddCompleteMinus, edwardsAddCompletePlus. + - field; replace (1 - (d * x1 * x2 * y1 * y2) ^ 2) + with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) + by field; + auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero, + edwardsAddCompleteMinus, edwardsAddCompletePlus. + Qed. + + Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 -> + onCurve (unifiedAdd' P1 P2). + Proof. + intros; destruct P1, P2. + remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r. + eapply unifiedAdd'_onCurve'; eauto. + Qed. +End Pre. \ No newline at end of file diff --git a/src/CompleteEwardsCurve/Pre.v b/src/CompleteEwardsCurve/Pre.v deleted file mode 100644 index e4dc140e1..000000000 --- a/src/CompleteEwardsCurve/Pre.v +++ /dev/null @@ -1,186 +0,0 @@ -Require Import BinInt Znumtheory VerdiTactics. - -Require Import Crypto.Spec.ModularArithmetic. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Local Open Scope F_scope. - -Section Pre. - Context {q : BinInt.Z}. - Context {a : F q}. - Context {d : F q}. - Context {prime_q : Znumtheory.prime q}. - Context {two_lt_q : 2 < q}. - Context {a_nonzero : a <> 0}. - Context {a_square : exists sqrt_a, sqrt_a^2 = a}. - Context {d_nonsquare : forall x, x^2 <> d}. - - Add Field Ffield_Z : (@Ffield_theory q _) - (morphism (@Fring_morph q), - preprocess [Fpreprocess], - postprocess [Fpostprocess], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - - (* the canonical definitions are in Spec *) - Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2). - Local Notation unifiedAdd' P1' P2' := ( - let '(x1, y1) := P1' in - let '(x2, y2) := P2' in - (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))) - ). - - Lemma char_gt_2 : ZToField 2 <> (0: F q). - intro; find_injection. - pose proof two_lt_q. - rewrite (Z.mod_small 2 q), Z.mod_0_l in *; omega. - Qed. - - Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end. - Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end. - - Ltac whatsNotZero := - repeat match goal with - | [H: ?lhs = ?rhs |- _ ] => - match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (lhs <> 0) by (rewrite H; auto using Fq_1_neq_0) - | [H: ?lhs = ?rhs |- _ ] => - match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (rhs <> 0) by (rewrite H; auto using Fq_1_neq_0) - | [H: (?a^?p)%F <> 0 |- _ ] => - match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; - let Y:=fresh in let Z:=fresh in try ( - assert (p <> 0%N) as Z by (intro Y; inversion Y); - assert (a <> 0) by (eapply Fq_root_nonzero; eauto using Fq_1_neq_0); - clear Z) - | [H: (?a*?b)%F <> 0 |- _ ] => - match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (a <> 0) by (eapply F_mul_nonzero_l; eauto using Fq_1_neq_0) - | [H: (?a*?b)%F <> 0 |- _ ] => - match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (b <> 0) by (eapply F_mul_nonzero_r; eauto using Fq_1_neq_0) - end. - - Lemma edwardsAddComplete' x1 y1 x2 y2 : - onCurve (x1, y1) -> - onCurve (x2, y2) -> - (d*x1*x2*y1*y2)^2 <> 1. - Proof. - intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero. - - pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. - destruct a_square as [sqrt_a a_square']. - rewrite <-a_square' in *. - - (* Furthermore... *) - pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt. - rewrite Hc2 in Heqt at 2. - replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2)) - with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field. - rewrite Hcontra in Heqt. - replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field. - rewrite <-Hc1 in Heqt. - - (* main equation for both potentially nonzero denominators *) - destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0); - try lazymatch goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] => - assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 = - f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2) - (d * x1 * x2 * y1 * y2*sqrt_a*(ZToField 2)*x1*y1)) as Heqw1 by field; - rewrite Hcontra in Heqw1; - replace (1 * y1^2) with (y1^2) in * by field; - rewrite <- Heqt in *; - assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 / - (x1 * y1 * (f (sqrt_a * x2) y2))^2) - by (rewriteAny; field; auto); - match goal with [H: d = (?n^2)/(?l^2) |- _ ] => - destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto) - end - end. - - assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field). - - replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field. - - (* contradiction: product of nonzero things is zero *) - destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition. - destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition. - apply Ha_nonzero; field. - Qed. - - Lemma edwardsAddCompletePlus x1 y1 x2 y2 : - onCurve (x1, y1) -> - onCurve (x2, y2) -> - (1 + d*x1*x2*y1*y2) <> 0. - Proof. - intros Hc1 Hc2; simpl in Hc1, Hc2. - intros; destruct (F_eq_dec (d*x1*x2*y1*y2) (0-1)) as [H|H]. - - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. - - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field. - intro Hz; rewrite Hz in H; intuition. - Qed. - - Lemma edwardsAddCompleteMinus x1 y1 x2 y2 : - onCurve (x1, y1) -> - onCurve (x2, y2) -> - (1 - d*x1*x2*y1*y2) <> 0. - Proof. - intros Hc1 Hc2. destruct (F_eq_dec (d*x1*x2*y1*y2) 1) as [H|H]. - - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. - - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field. - intro Hz; rewrite Hz in H; apply H; field. - Qed. - - Definition zeroOnCurve : onCurve (0, 1). - simpl. field. - Qed. - - Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3 - (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) : - onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3). - Proof. - (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1; - * c=1 and an extra a in front of x^2 *) - - injection H; clear H; intros. - - Ltac t x1 y1 x2 y2 := - assert ((a*x2^2 + y2^2)*d*x1^2*y1^2 - = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto); - assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2 - = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field). - t x1 y1 x2 y2; t x2 y2 x1 y1. - - remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 - - (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T. - assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field). - assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +( - (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 * - y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field). - replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3. - - match goal with [ |- ?x = 1 ] => replace x with - ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 + - ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 - - d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/ - ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end. - - rewrite <-HT1, <-HT2; field; rewrite HT1. - replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2)) - with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) by field. - auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero, - edwardsAddCompleteMinus, edwardsAddCompletePlus. - - field; replace (1 - (d * x1 * x2 * y1 * y2) ^ 2) - with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) - by field; - auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero, - edwardsAddCompleteMinus, edwardsAddCompletePlus. - Qed. - - Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 -> - onCurve (unifiedAdd' P1 P2). - Proof. - intros; destruct P1, P2. - remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r. - eapply unifiedAdd'_onCurve'; eauto. - Qed. -End Pre. \ No newline at end of file diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 8137abc4c..2ea04cde5 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -137,56 +137,8 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam - Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0. - intros. - - induction p; inversion H. - - revert H H1; generalize x; induction p; intros. - - - simpl in H; apply mul_zero_why in H; destruct H; intuition. - - + subst; intuition. - - + apply IHp in H. - rewrite H1. - simpl in H1. - apply mul_zero_why in H1; destruct H1; intuition. - rewrite H0 in H. - apply mul_zero_why in H; destruct H; intuition. - - simpl; intuition. - - - simpl in H1; apply IHp in H1; simpl; intuition. - simpl in H; rewrite H in H1; rewrite H. - apply mul_zero_why in H1; destruct H1; intuition. - - - simpl in H; subst; intuition. - - Qed. - - Lemma root_nonzero : forall x p, x^p <> 0 -> (p <> 0)%N -> x <> 0. - intros; intuition. - - induction p. - - - apply H; intuition. - - - apply H. - rewrite H1 in *. - induction p. - - + simpl. - field. - - + simpl in *. - replace (0 * 0) with 0 in * by field. - apply IHp; intuition. - induction p; inversion H2. - - + simpl; intuition. - - Qed. + Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0. Admitted. + Lemma root_nonzero : forall x p, x^p <> 0 -> (p <> 0)%N -> x <> 0. Admitted. Lemma char_gt_2 : inject 2 <> 0. intro H; inversion H; clear H. diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 474cd03e1..6c79e6891 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -389,4 +389,34 @@ Section VariousModulo. Proof. intros; ring. Qed. + + Lemma F_add_0_r : forall x : F m, (x + 0)%F = x. + Proof. + intros; ring. + Qed. + + Lemma F_add_0_l : forall x : F m, (0 + x)%F = x. + Proof. + intros; ring. + Qed. + + Lemma F_sub_0_r : forall x : F m, (x - 0)%F = x. + Proof. + intros; ring. + Qed. + + Lemma F_sub_0_l : forall x : F m, (0 - x)%F = opp x. + Proof. + intros; ring. + Qed. + + Lemma F_mul_1_r : forall x : F m, (x * 1)%F = x. + Proof. + intros; ring. + Qed. + + Lemma F_mul_1_l : forall x : F m, (1 * x)%F = x. + Proof. + intros; ring. + Qed. End VariousModulo. \ No newline at end of file diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 338903b26..6a862fb3b 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -56,7 +56,7 @@ Section VariousModPrime. Add Field Ffield_Z : (@Ffield_theory q _) (morphism (@Fring_morph q), preprocess [Fpreprocess], - postprocess [Fpostprocess], + postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], constants [Fconstant], div (@Fmorph_div_theory q), power_tac (@Fpower_theory q) [Fexp_tac]). @@ -133,6 +133,11 @@ Section VariousModPrime. + intuition. + apply IHp; auto. Qed. + + Lemma F_div_1_r : forall x : F q, (x/1)%F = x. + Proof. + intros; field. (* TODO: Warning: Collision between bound variables ... *) + Qed. Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x. Proof. diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v index e84659c9e..a4cbcb5ca 100644 --- a/src/ModularArithmetic/Tutorial.v +++ b/src/ModularArithmetic/Tutorial.v @@ -104,5 +104,12 @@ Module TimesZeroParametricTestModule (M: PrimeModulus). intros. field. Qed. + + Lemma realisticFraction : forall x y d : F modulus, (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x. + Proof. + intros. + field; try exact Fq_1_neq_0. + Qed. + End TimesZeroParametricTestModule. diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v new file mode 100644 index 000000000..3586e1f95 --- /dev/null +++ b/src/Spec/CompleteEdwardsCurve.v @@ -0,0 +1,52 @@ +Require BinInt Znumtheory. + +Require Crypto.CompleteEdwardsCurve.Pre. + +Require Import Crypto.Spec.ModularArithmetic. +Local Open Scope F_scope. + +Class TwistedEdwardsParams := { + q : BinInt.Z; + a : F q; + d : F q; + prime_q : Znumtheory.prime q; + two_lt_q : BinInt.Z.lt 2 q; + nonzero_a : a <> 0; + square_a : exists sqrt_a, sqrt_a^2 = a; + nonsquare_d : forall x, x^2 <> d +}. + +Section TwistedEdwardsCurves. + Context {prm:TwistedEdwardsParams}. + + (* Twisted Edwards curves with complete addition laws. References: + * + * + * + *) + Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. + Definition point := { P | onCurve P}. + Definition mkPoint (xy:F q * F q) (pf:onCurve xy) : point := exist onCurve xy pf. + + Definition zero : point := mkPoint (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q). + + (* NOTE: the two matches on P1 can probably be merged, not sure whether good idea... *) + Definition unifiedAdd (P1 P2 : point) : point := + let 'exist P1' pf1 := P1 in + let 'exist P2' pf2 := P2 in + mkPoint + ( let '(x1, y1) := P1' in + let '(x2, y2) := P2' in + (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))) + (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2). + + Fixpoint scalarMult (n:nat) (P : point) : point := + match n with + | O => zero + | S n' => unifiedAdd P (scalarMult n' P) + end. +End TwistedEdwardsCurves. + +Delimit Scope E_scope with E. +Infix "+" := unifiedAdd : E_scope. +Infix "*" := scalarMult : E_scope. \ No newline at end of file diff --git a/src/Spec/CompleteEwardsCurve.v b/src/Spec/CompleteEwardsCurve.v deleted file mode 100644 index 8eeefe03b..000000000 --- a/src/Spec/CompleteEwardsCurve.v +++ /dev/null @@ -1,48 +0,0 @@ -Require BinInt Znumtheory. - -Require Crypto.CompleteEwardsCurve.Pre. - -Require Import Crypto.Spec.ModularArithmetic. -Local Open Scope F_scope. - -Class TwistedEdwardsParams := { - q : BinInt.Z; - a : F q; - d : F q; - modulus_prime : Znumtheory.prime q; - a_nonzero : a <> 0; - a_square : exists sqrt_a, sqrt_a^2 = a; - d_nonsquare : forall x, x^2 <> d -}. - -Section TwistedEdwardsCurves. - Context {prm:TwistedEdwardsParams}. - - (* Twisted Edwards curves with complete addition laws. References: - * - * - * - *) - Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. - Definition point := { P | onCurve P}. - Definition mkPoint (xy:F q * F q) (pf:onCurve xy) : point := exist onCurve xy pf. - - Definition zero : point := mkPoint (0, 1) Pre.zeroOnCurve. - - (* NOTE: the two matches on P1 can probably be merged, not sure whether good idea... *) - Definition unifiedAdd (P1 P2 : point) : point := - let 'exist P1' pf1 := P1 in - let 'exist P2' pf2 := P2 in - mkPoint - ( let '(x1, y1) := P1' in - let '(x2, y2) := P2' in - (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))) - (Pre.unifiedAdd'_onCurve _ _ pf1 pf2). - Local Infix "+" := unifiedAdd. - - Fixpoint scalarMult (n:nat) (P : point) : point := - match n with - | O => zero - | S n' => P + scalarMult n' P - end. -End TwistedEdwardsCurves. \ No newline at end of file -- cgit v1.2.3 From 1a51bcb7bc1811553dfa658a04bb6d0764825fd6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 12 Feb 2016 16:47:41 -0500 Subject: document field issue re-appearing --- .../CompleteEdwardsCurveTheorems.v | 6 +- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 130 +++++++++++++++++++++ .../ExtendedCoordinatesIssue.v | 40 +++++++ src/ModularArithmetic/Tutorial.v | 18 ++- src/Spec/CompleteEdwardsCurve.v | 11 +- 5 files changed, 196 insertions(+), 9 deletions(-) create mode 100644 src/CompleteEdwardsCurve/ExtendedCoordinates.v create mode 100644 src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v (limited to 'src') diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 90f5907fd..b1be7dd63 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -24,19 +24,19 @@ Section CompleteEdwardsCurveTheorems. Qed. Hint Resolve point_eq. - Ltac Edefn := unfold unifiedAdd, zero; intros; + Ltac Edefn := unfold unifiedAdd, unifiedAdd', zero; intros; repeat match goal with | [ p : point |- _ ] => let x := fresh "x" p in let y := fresh "y" p in let pf := fresh "pf" p in destruct p as [[x y] pf]; unfold onCurve in pf - | _ => eapply point_eq, f_equal2 + | _ => eapply point_eq, (f_equal2 pair) | _ => eapply point_eq end. Lemma twistedAddComm : forall A B, (A+B = B+A)%E. Proof. - Edefn; f_equal; field. + Edefn; apply f_equal2; ring. Qed. Lemma twistedAddAssoc : forall A B C, A+(B+C) = (A+B)+C. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v new file mode 100644 index 000000000..d2cd753fe --- /dev/null +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -0,0 +1,130 @@ +Require Import Crypto.CompleteEdwardsCurve.Pre. +Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.Tactics.VerdiTactics. + +Section ExtendedCoordinates. + Local Open Scope F_scope. + Context {prm:TwistedEdwardsParams}. + Existing Instance prime_q. + + Add Field GFfield_Z : (@Ffield_theory q _) + (morphism (@Fring_morph q), + preprocess [Fpreprocess], + postprocess [Fpostprocess], + constants [Fconstant], + div (@Fmorph_div_theory q), + power_tac (@Fpower_theory q) [Fexp_tac]). + + + (** [extended] represents a point on an elliptic curve using extended projective + * Edwards coordinates with twist a=-1 (see ). *) + Record extended := mkExtended {extendedX : F q; + extendedY : F q; + extendedZ : F q; + extendedT : F q}. + Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). + + Definition twistedToExtended (P : (F q*F q)) : extended := + let '(x, y) := P in (x, y, 1, x*y). + Definition extendedToTwisted (P : extended) : F q * F q := + let '(X, Y, Z, T) := P in ((X/Z), (Y/Z)). + Definition rep (P:extended) (rP:(F q*F q)) : Prop := + let '(X, Y, Z, T) := P in + extendedToTwisted P = rP /\ + Z <> 0 /\ + T = X*Y/Z. + Local Hint Unfold twistedToExtended extendedToTwisted rep. + Local Notation "P '~=' rP" := (rep P rP) (at level 70). + + Ltac extended_tac := + repeat progress (autounfold; unfold onCurve, unifiedAdd, unifiedAdd', rep in *; intros); + repeat match goal with + | [ p : (F q*F q)%type |- _ ] => + let x := fresh "x" p in + let y := fresh "y" p in + destruct p as [x y] + | [ p : extended |- _ ] => + let X := fresh "X" p in + let Y := fresh "Y" p in + let Z := fresh "Z" p in + let T := fresh "T" p in + destruct p as [X Y Z T] + | [ H: _ /\ _ |- _ ] => destruct H + | [ |- _ /\ _ ] => split + | [ H: @eq (F q * F q)%type _ _ |- _ ] => invcs H + | [ H: @eq F q ?x _ |- _ ] => isVar x; rewrite H; clear H + | [ |- @eq (F q * F q)%type _ _] => apply f_equal2 + | _ => progress rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r, + ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r + | _ => progress eauto using Fq_1_neq_0 + | [ H: a = _ |- _ ] => rewrite H + | [ |- @eq (F q) _ _] => fail; field (*FIXME*) + end. + + Lemma twistedToExtended_rep : forall P, twistedToExtended P ~= P. + Proof. + extended_tac. + Qed. + + Lemma extendedToTwisted_rep : forall P rP, P ~= rP -> extendedToTwisted P = rP. + Proof. + extended_tac. + Qed. + + Section TwistMinus1. + Context (a_eq_minus1 : a = opp 1). + (** Second equation from section 3.1, also and *) + Definition unifiedAddM1 (P1 P2 : extended) : extended := + let '(X1, Y1, Z1, T1) := P1 in + let '(X2, Y2, Z2, T2) := P2 in + let A := (Y1-X1)*(Y2-X2) in + let B := (Y1+X1)*(Y2+X2) in + let C := T1*ZToField 2*d*T2 in + let D := Z1*ZToField 2 *Z2 in + let E := B-A in + let F := D-C in + let G := D+C in + let H := B+A in + let X3 := E*F in + let Y3 := G*H in + let T3 := E*H in + let Z3 := F*G in + (X3, Y3, Z3, T3). + Local Hint Unfold unifiedAdd. + + Lemma unifiedAdd_repM1: forall P Q rP rQ, onCurve rP -> onCurve rQ -> + P ~= rP -> Q ~= rQ -> (unifiedAddM1 P Q) ~= (unifiedAdd' rP rQ). + Proof. + intros P Q rP rQ HoP HoQ HrP HrQ. + pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d) as HoR; simpl in HoR. + extended_tac. + field. + + (* If we we had reasoning modulo associativity and commutativity, + * the following tactic would probably solve all 10 goals here: + repeat match goal with [H1: @eq GF _ _, H2: @eq GF _ _ |- _ ] => + let H := fresh "H" in ( + pose proof (edwardsAddCompletePlus _ _ _ _ H1 H2) as H; + match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end + ) || ( + pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as H; + match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end + ); repeat apply mul_nonzero_nonzero; auto 10 + end. + *) + + - replace (Z0 * Z * Z0 * Z + d * X0 * X * Y0 * Y) with (Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. + - replace (Z0 * inject 2 * Z * (Z0 * Z) + X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. + - replace (Z0 * inject 2 * Z * (Z0 * Z) - X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. + - replace (Z0 * Z * Z0 * Z - d * X0 * X * Y0 * Y) with (Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. + - replace (Z0 * inject 2 * Z * (Z0 * Z) + X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. + - replace (Z0 * inject 2 * Z * (Z0 * Z) - X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. + - replace (Z0 * Z * Z0 * Z - d * X0 * X * Y0 * Y) with (Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto). + repeat apply mul_nonzero_nonzero. + + replace (Z0 * 2 * Z - X0 * Y0 / Z0 * 2 * d * (X * Y / Z)) with (2*Z*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. + + replace (Z0 * 2 * Z + X0 * Y0 / Z0 * 2 * d * (X * Y / Z)) with (2*Z*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. + - replace (Z0 * inject 2 * Z * (Z0 * Z) + X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 + d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. + - replace (Z0 * inject 2 * Z * (Z0 * Z) - X0 * Y0 * inject 2 * d * (X * Y)) with (2*Z*Z*Z0*Z0* (1 - d * (X / Z) * (X0 / Z0) * (Y / Z) * (Y0 / Z0))) by (field; auto); auto 10. + Qed. +End ExtendedCoordinates. \ No newline at end of file diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v new file mode 100644 index 000000000..b9baf1498 --- /dev/null +++ b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v @@ -0,0 +1,40 @@ +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.CompleteEdwardsCurve.Pre. + +Section ExtendedCoordinates. + Local Open Scope F_scope. + + (* + Context {prm:TwistedEdwardsParams}. (* DOESN'T WORK *) + *) + Context {q:BinInt.Z} {prime_q:Znumtheory.prime q}. (* WORKS OKAY-ish *) + + Check q : BinInt.Z. + Check prime_q : Znumtheory.prime q. + Existing Instance prime_q. + + Add Field Ffield_Z : (@Ffield_theory q _) + (morphism (@Fring_morph q), + preprocess [Fpreprocess], + postprocess [Fpostprocess], + constants [Fconstant], + div (@Fmorph_div_theory q), + power_tac (@Fpower_theory q) [Fexp_tac]). + + Lemma biggerFraction : forall XP YP ZP XQ YQ ZQ d : F q, + ZQ <> 0 -> + ZP <> 0 -> + ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 -> + ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 -> + ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 -> + + ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) * + (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) / + ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) * + (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))) = + (XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)). + Proof. + intros. + field; assumption. + Qed. +End ExtendedCoordinates. \ No newline at end of file diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v index a4cbcb5ca..ae2b63bad 100644 --- a/src/ModularArithmetic/Tutorial.v +++ b/src/ModularArithmetic/Tutorial.v @@ -110,6 +110,22 @@ Module TimesZeroParametricTestModule (M: PrimeModulus). intros. field; try exact Fq_1_neq_0. Qed. - + + Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus, + ZQ <> 0 -> + ZP <> 0 -> + ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 -> + ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 -> + ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 -> + + ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) * + (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) / + ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) * + (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))) = + (XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)). + Proof. + intros. + field; assumption. + Qed. End TimesZeroParametricTestModule. diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 3586e1f95..23e201405 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -30,14 +30,15 @@ Section TwistedEdwardsCurves. Definition zero : point := mkPoint (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q). - (* NOTE: the two matches on P1 can probably be merged, not sure whether good idea... *) + Definition unifiedAdd' P1' P2' := + let '(x1, y1) := P1' in + let '(x2, y2) := P2' in + (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). + Definition unifiedAdd (P1 P2 : point) : point := let 'exist P1' pf1 := P1 in let 'exist P2' pf2 := P2 in - mkPoint - ( let '(x1, y1) := P1' in - let '(x2, y2) := P2' in - (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))) + mkPoint (unifiedAdd' P1' P2') (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2). Fixpoint scalarMult (n:nat) (P : point) : point := -- cgit v1.2.3 From d188b32664886d7757cd6016c85a32180fcffbdf Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 12 Feb 2016 17:11:15 -0500 Subject: fix imports --- src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v index b9baf1498..37bc8cca5 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v @@ -1,5 +1,5 @@ Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.CompleteEdwardsCurve.Pre. +Require Import Crypto.Spec.CompleteEdwardsCurve. Section ExtendedCoordinates. Local Open Scope F_scope. -- cgit v1.2.3 From 6c993ee91855ee8c19c292cd164ab24a7c1012f8 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 12 Feb 2016 22:22:36 -0500 Subject: workaround field with typeclass modulus --- .../ExtendedCoordinatesIssue.v | 24 ++++++++++------------ 1 file changed, 11 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v index 37bc8cca5..8d24f2cd2 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v @@ -4,22 +4,19 @@ Require Import Crypto.Spec.CompleteEdwardsCurve. Section ExtendedCoordinates. Local Open Scope F_scope. - (* - Context {prm:TwistedEdwardsParams}. (* DOESN'T WORK *) - *) - Context {q:BinInt.Z} {prime_q:Znumtheory.prime q}. (* WORKS OKAY-ish *) - - Check q : BinInt.Z. - Check prime_q : Znumtheory.prime q. - Existing Instance prime_q. + Context {prm:TwistedEdwardsParams}. + Context {p:BinInt.Z} {p_eq_q:p = q}. + Lemma prime_p : Znumtheory.prime p. + rewrite p_eq_q; exact prime_q. + Qed. - Add Field Ffield_Z : (@Ffield_theory q _) - (morphism (@Fring_morph q), + Add Field Ffield_Z : (@Ffield_theory p prime_p) + (morphism (@Fring_morph p), preprocess [Fpreprocess], postprocess [Fpostprocess], constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). + div (@Fmorph_div_theory p), + power_tac (@Fpower_theory p) [Fexp_tac]). Lemma biggerFraction : forall XP YP ZP XQ YQ ZQ d : F q, ZQ <> 0 -> @@ -34,7 +31,8 @@ Section ExtendedCoordinates. (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))) = (XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)). Proof. + rewrite <-p_eq_q. intros. - field; assumption. + abstract (field; assumption). Qed. End ExtendedCoordinates. \ No newline at end of file -- cgit v1.2.3