From 2a321d84d1eceffbe35538c6f7fff2974e034e50 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 22 Feb 2017 14:11:41 -0500 Subject: use [positive] for [F] modulus, char_ge_C instead of char_gt_C --- src/Spec/CompleteEdwardsCurve.v | 2 +- src/Spec/Ed25519.v | 27 ++++----- src/Spec/EdDSA.v | 2 +- src/Spec/ModularArithmetic.v | 16 ++++- src/Spec/ModularWordEncoding.v | 2 +- src/Spec/MontgomeryCurve.v | 131 +++++++++++++++------------------------- src/Spec/WeierstrassCurve.v | 2 +- 7 files changed, 79 insertions(+), 103 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 801b31ffc..daaa2ed74 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -11,7 +11,7 @@ Module E. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one)} + {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)} {Feq_dec:Decidable.DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 02f59c9e5..4fc3afce4 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -12,10 +12,10 @@ Section Ed25519. Local Open Scope Z_scope. - Definition q : BinNums.Z := 2^255 - 19. + Definition q : BinPos.positive := 2^255 - 19. Definition Fq : Type := F q. - Definition l : BinNums.Z := 2^252 + 27742317777372353535851937790883648493. + Definition l : BinPos.positive := 2^252 + 27742317777372353535851937790883648493. Definition Fl : Type := F l. Local Open Scope F_scope. @@ -51,10 +51,10 @@ Section Ed25519. let '(x,y) := E.coordinates P in Fencode (len:=b-1) y ++ bit (sign x). Definition Senc : Fl -> Word.word b := Fencode (len:=b). - Local Instance char_gt_2 : (* TODO: prove this in PrimeFieldTheorems *) - @Ring.char_gt (F.F q) (@eq (F.F q)) (F.of_Z q BinNums.Z0) + Local Instance char_gt_e : (* TODO: prove this in PrimeFieldTheorems *) + @Ring.char_ge (F.F q) (@eq (F.F q)) (F.of_Z q BinNums.Z0) (F.of_Z q (BinNums.Zpos BinNums.xH)) (@F.opp q) - (@F.add q) (@F.sub q) (@F.mul q) (BinNat.N.succ_pos BinNat.N.one). + (@F.add q) (@F.sub q) (@F.mul q) (BinNat.N.succ_pos BinNat.N.two). Proof. intros p ?. edestruct (fun p:p = (BinNat.N.succ_pos BinNat.N.zero) \/ p = (BinNat.N.succ_pos BinNat.N.one) => p); subst. { admit. (* @@ -75,21 +75,18 @@ Section Ed25519. Let mul := E.mul(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d). Let zero := E.zero(nonzero_a:=nonzero_a)(d:=d). - Definition ed25519 (l_order_B: E.eq (mul (BinInt.Z.to_nat l) B)%E zero) : + Definition ed25519 (l_order_B: E.eq(F:=Fq)(Fone:=F.one) (mul (BinInt.Z.to_nat l) B)%E zero) : EdDSA (E:=E) (Eadd:=add) (Ezero:=zero) (EscalarMult:=mul) (B:=B) (Eopp:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.opp(nonzero_a:=nonzero_a)) (* TODO: move defn *) (Eeq:=E.eq) (* TODO: move defn *) (l:=l) (b:=b) (n:=n) (c:=c) (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512). Proof. - split; try exact _. - (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *) - (* timeout 1 match goal with H:?P |- ?P => idtac end. *) - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - exact l_order_B. + split; + match goal with + | |- ?P => match goal with [H:P|-_] => exact H end (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *) + | _ => exact _ + | _ => Crypto.Util.Decidable.vm_decide + end. Qed. End Ed25519. diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index f8581c4c9..67a1014f6 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -33,7 +33,7 @@ Section EdDSA. {H : forall {n}, Word.word n -> Word.word (b + b)} (* main hash function *) {c : nat} (* cofactor E = 2^c *) {n : nat} (* secret keys are (n+1) bits *) - {l : BinInt.Z} (* order of the subgroup of E generated by B *) + {l : BinPos.positive} (* order of the subgroup of E generated by B *) {B : E} (* base point *) diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index a3e80fcf9..ed6a0c4a2 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -2,6 +2,13 @@ Require Coq.ZArith.Znumtheory Coq.Numbers.BinNums. Require Crypto.ModularArithmetic.Pre. +Delimit Scope positive_scope with positive. +Bind Scope positive_scope with BinPos.positive. +Infix "+" := BinPos.Pos.add : positive_scope. +Infix "*" := BinPos.Pos.mul : positive_scope. +Infix "-" := BinPos.Pos.sub : positive_scope. +Infix "^" := BinPos.Pos.pow : positive_scope. + Delimit Scope N_scope with N. Bind Scope N_scope with BinNums.N. Infix "+" := BinNat.N.add : N_scope. @@ -18,17 +25,20 @@ 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. +Global Coercion BinInt.Z.pos : BinPos.positive >-> BinInt.Z. +Global Coercion BinInt.Z.of_N : BinNums.N >-> BinInt.Z. +Global Set Printing Coercions. Module F. - Definition F (m : BinInt.Z) := { z : BinInt.Z | z = z mod m }. - Bind Scope F_scope with F. + Definition F (m : BinPos.positive) := { z : BinInt.Z | z = z mod m }. Local Obligation Tactic := cbv beta; auto using Pre.Z_mod_mod. Program Definition of_Z m (a:BinNums.Z) : F m := a mod m. Definition to_Z {m} (a:F m) : BinNums.Z := proj1_sig a. Section FieldOperations. - Context {m : BinInt.Z}. + Context {m : BinPos.positive}. Definition zero : F m := of_Z m 0. Definition one : F m := of_Z m 1. diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v index 7a9845e7e..5b0bdb545 100644 --- a/src/Spec/ModularWordEncoding.v +++ b/src/Spec/ModularWordEncoding.v @@ -11,7 +11,7 @@ Require Crypto.Encoding.ModularWordEncodingPre. Local Open Scope nat_scope. Section ModularWordEncoding. - Context {m : Z} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. + Context {m : positive} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. Definition Fm_enc (x : F m) : word sz := NToWord sz (Z.to_N (F.to_Z x)). diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v index 5f7246011..2717f6bbc 100644 --- a/src/Spec/MontgomeryCurve.v +++ b/src/Spec/MontgomeryCurve.v @@ -6,7 +6,7 @@ Require Import Crypto.Spec.WeierstrassCurve. Module M. Section MontgomeryCurve. Import BinNat. - Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. @@ -28,20 +28,26 @@ Module M. end }. Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. + Definition eq (P1 P2:point) := + match coordinates P1, coordinates P2 with + | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2 + | ∞, ∞ => True + | _, _ => False + end. + Import Crypto.Util.Tactics Crypto.Algebra.Field. Ltac t := destruct_head' point; destruct_head' sum; destruct_head' prod; break_match; simpl in *; break_match_hyps; trivial; try discriminate; repeat match goal with | |- _ /\ _ => split - | [H:@eq (sum _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H - | [H:@eq (prod _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H + | [H:@Logic.eq (sum _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H + | [H:@Logic.eq (prod _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H end; subst; try fsatz. Program Definition add (P1 P2:point) : point := - exist _ - match coordinates P1, coordinates P2 return _ with + match coordinates P1, coordinates P2 return F*F+∞ with (x1, y1), (x2, y2) => if Decidable.dec (x1 = x2) then if Decidable.dec (y1 = - y2) @@ -51,53 +57,39 @@ Module M. | ∞, ∞ => ∞ | ∞, _ => coordinates P2 | _, ∞ => coordinates P1 - end _. + end. Next Obligation. Proof. t. Qed. Program Definition opp (P:point) : point := - exist _ - match P with - | (x, y) => (x, -y) - | ∞ => ∞ - end _. - Next Obligation. - Proof. t. Qed. + match P return F*F+∞ with + | (x, y) => (x, -y) + | ∞ => ∞ + end. + Next Obligation. Proof. t. Qed. Local Notation "4" := (1+3). Local Notation "16" := (4*4). Local Notation "9" := (3*3). Local Notation "27" := (3*9). - Context {char_gt_27:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 27}. + Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}. Let WeierstrassA := ((3-a^2)/(3*b^2)). Let WeierstrassB := ((2*a^3-9*a)/(27*b^3)). - Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB). - Program Definition MontgomeryOfWeierstrass (P:Wpoint) : point := - exist - _ - match W.coordinates P return _ with - | (x,y) => (b*x-a/3, b*y) - | _ => ∞ - end - _. - Next Obligation. - Proof. subst WeierstrassA; subst WeierstrassB; destruct P; t. Qed. + Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB). - Definition eq (P1 P2:point) := - match coordinates P1, coordinates P2 with - | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2 - | ∞, ∞ => True - | _, _ => False + Program Definition of_Weierstrass (P:Wpoint) : point := + match W.coordinates P return F*F+∞ with + | (x,y) => (b*x-a/3, b*y) + | _ => ∞ end. + Next Obligation. + Proof. clear char_ge_3; subst WeierstrassA; subst WeierstrassB; destruct P; t. Qed. - Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_gt_2 WeierstrassA WeierstrassB). - Lemma MontgomeryOfWeierstrass_add P1 P2 : - eq (MontgomeryOfWeierstrass (W.add P1 P2)) - (add (MontgomeryOfWeierstrass P1) (MontgomeryOfWeierstrass P2)). - Proof. - cbv [WeierstrassA WeierstrassB eq MontgomeryOfWeierstrass W.add add coordinates W.coordinates proj1_sig] in *; t. - Qed. + Lemma of_Weierstrass_add P1 P2 : + eq (of_Weierstrass (W.add P1 P2)) + (add (of_Weierstrass P1) (of_Weierstrass P2)). + Proof. cbv [WeierstrassA WeierstrassB eq of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *; clear char_ge_3; t. Qed. Section AddX. Lemma homogeneous_x_differential_addition_releations P1 P2 : @@ -110,30 +102,20 @@ Module M. end. Proof. t. Qed. - Definition onCurve xy := let 'pair x y := xy in b*y^2 = x^3 + a*x^2 + x. - Definition xzpoint := { xz | let 'pair x z := xz in (z = 0 \/ exists y, onCurve (pair (x/z) y)) }. - Definition xzcoordinates (P:xzpoint) : F*F := proj1_sig P. - Program Definition toxz (P:point) : xzpoint := - exist _ - match coordinates P with - | (x, y) => pair x 1 - | ∞ => pair 1 0 - end _. - Next Obligation. t; [right; exists f0; t | left; reflexivity ]. Qed. - - Definition sig_pair_to_pair_sig {T T' I I'} (xy:{xy | let 'pair x y := xy in I x /\ I' y}) - : prod {x:T | I x} {y:T' | I' y} - := let 'exist (pair x y) (conj pfx pfy) := xy in pair (exist _ x pfx) (exist _ y pfy). + Program Definition to_xz (P:point) : F*F := + match coordinates P with + | (x, y) => pair x 1 + | ∞ => pair 1 0 + end. (* From Explicit Formulas Database by Lange and Bernstein, credited to 1987 Montgomery "Speeding the Pollard and elliptic curve methods of factorization", page 261, fifth and sixth displays, plus common-subexpression elimination, plus assumption Z1=1 *) - Context {a24:F} {a24_correct:4*a24 = a+2}. - Definition xzladderstep (X1:F) (P1 P2:xzpoint) : prod xzpoint xzpoint. refine ( - sig_pair_to_pair_sig (exist _ - match xzcoordinates P1, xzcoordinates P2 return _ with + Context {a24:F} {a24_correct:4*a24 = a+2}. (* TODO: +2 or -2 ? *) + Definition xzladderstep (X1:F) (P1 P2:F*F) : ((F*F)*(F*F)) := + match P1, P2 with pair X2 Z2, pair X3 Z3 => let A := X2+Z2 in let AA := A^2 in @@ -149,32 +131,19 @@ Module M. let X4 := AA*BB in let Z4 := E*(BB + a24*E) in (pair (pair X4 Z4) (pair X5 Z5)) - end _) ). - Proof. - destruct P1, P2; cbv [onCurve xzcoordinates] in *. t; intuition idtac. - { left. fsatz. } - { left. fsatz. } - admit. - admit. - admit. - admit. - { right. - admit. (* the following used to work, but slowly: - exists ((fun x1 y1 x2 y2 => (2*x1+x1+a)*(3*x1^2+2*a*x1+1)/(2*b*y1)-b*(3*x1^2+2*a*x1+1)^3/(2*b*y1)^3-y1) (f1/f2) x0 (f/f0) x). - Algebra.common_denominator_in H. - Algebra.common_denominator_in H0. - Algebra.common_denominator. - abstract Algebra.nsatz. - - idtac. - admit. - admit. - admit. - admit. - admit. *) } - { right. - (* exists ((fun x1 y1 x2 y2 => (2*x1+x2+a)*(y2-y1)/(x2-x1)-b*(y2-y1)^3/(x2-x1)^3-y1) (f1/f2) x0 (f/f0) x). *) - (* XXX: this case is probably not true -- there is not necessarily a guarantee that the output x/z is on curve if [X1] was not the x coordinate of the difference of input points as requored *) + end. + + Require Import Crypto.Util.Tuple. + + (* TODO: look up this lemma statement -- the current one may not be right *) + Lemma xzladderstep_to_xz X1 P1 P2 + (HX1 : match coordinates (add P1 (opp P2)) with (x,y) => X1 = x | _ => False end) + : fieldwise (n:=2) (fieldwise (n:=2) Feq) + (xzladderstep X1 (to_xz P1) (to_xz P2)) + (pair (to_xz (add P1 P2)) (to_xz (add P1 P1))). + destruct P1 as [[[??]|?]?], P2 as [[[??]|?]?]; + cbv [fst snd xzladderstep to_xz add coordinates proj1_sig opp fieldwise fieldwise'] in *; + break_match_hyps; break_match; repeat split; try contradiction. Abort. End AddX. End MontgomeryCurve. diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index d19f3f786..87b5bcffd 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -9,7 +9,7 @@ Module W. * (page 79) *) - Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "x =? y" := (Decidable.dec (Feq x y)) (at level 70, no associativity) : type_scope. Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Decidable.dec (Feq x y))) : bool_scope. -- cgit v1.2.3