From af5141847d7888e502e90b56646959fbf1070b76 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 16 Feb 2017 23:56:47 -0500 Subject: WIP --- src/Spec/CompleteEdwardsCurve.v | 47 +++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 25 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 770a2d02d..801b31ffc 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -9,40 +9,37 @@ 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} {Feq_dec:Decidable.DecidableRel Feq}. + 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)} + {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. Local Infix "+" := Fadd. Local Infix "*" := Fmul. - Local Infix "-" := Fsub. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "x ^ 2" := (x*x) (at level 30). - Local Notation "n / d" := (fst (Fdiv n d, (_:(d <> 0)))). (* force nonzero d *) - - Context {a d: F}. - Class twisted_edwards_params := - { - char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one); - nonzero_a : a <> 0; - square_a : exists sqrt_a, sqrt_a^2 = a; - nonsquare_d : forall x, x^2 <> d - }. - Context `{twisted_edwards_params}. (* TODO: name me *) - - Definition point := { P | let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2 }. - Definition coordinates (P:point) : (F*F) := proj1_sig P. + + Context {a d: F} + {nonzero_a : a <> 0} + {square_a : exists sqrt_a, sqrt_a^2 = a} + {nonsquare_d : forall x, x^2 <> d}. + + Definition point := { xy | let '(x, y) := xy in a*x^2 + y^2 = 1 + d*x^2*y^2 }. + Definition coordinates (P:point) : (F*F) := let (xy, xy_onCurve_proof) := P in xy. Definition eq (P Q:point) := - fst (coordinates P) = fst (coordinates Q) /\ - snd (coordinates P) = snd (coordinates Q). + match coordinates P, coordinates Q with + (x1,y1), (x2,y2) => x1 = x2 /\ y1 = y2 + end. Program Definition zero : point := (0, 1). - Next Obligation. destruct H; eauto using Pre.onCurve_zero. Qed. + Next Obligation. eauto using Pre.onCurve_zero. Qed. Program Definition add (P1 P2:point) : point := - let x1y1 := coordinates P1 in let x1 := fst x1y1 in let y1 := snd x1y1 in - let x2y2 := coordinates P2 in let x2 := fst x2y2 in let y2 := snd x2y2 in - (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). - Next Obligation. destruct P1 as [[??]?], P2 as [[??]?], H. eauto using Pre.denominator_nonzero_x. Qed. - Next Obligation. destruct P1 as [[??]?], P2 as [[??]?], H; eauto using Pre.denominator_nonzero_y. Qed. - Next Obligation. destruct P1 as [[??]?], P2 as [[??]?], H; eauto using Pre.onCurve_add. Qed. + match coordinates P1, coordinates P2 return (F*F) with + (x1, y1), (x2, y2) => + (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))) + end. + Next Obligation. destruct P1 as [[??]?], P2 as [[??]?]; eapply Pre.onCurve_add; eauto. Qed. Fixpoint mul (n:nat) (P : point) : point := match n with -- cgit v1.2.3