diff options
Diffstat (limited to 'src/Spec/MontgomeryCurve.v')
| -rw-r--r-- | src/Spec/MontgomeryCurve.v | 181 |
1 files changed, 181 insertions, 0 deletions
diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v new file mode 100644 index 000000000..4e448392f --- /dev/null +++ b/src/Spec/MontgomeryCurve.v @@ -0,0 +1,181 @@ +Require Crypto.Algebra. +Require Crypto.Util.GlobalSettings. + +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 2}. + 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. + Local Notation "- x" := (Fopp x). + Local Notation "x ^ 2" := (x*x) (at level 30). Local Notation "x ^ 3" := (x*x^2) (at level 30). + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "2" := (1+1). Local Notation "3" := (1+2). + + Local Notation "'∞'" := unit : type_scope. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "( x , y )" := (inl (pair x y)). + Local Open Scope core_scope. + + Context {a b: F} {b_nonzero:b <> 0}. + + Definition point := { P | match P with + | (x, y) => b*y^2 = x^3 + a*x^2 + x + | ∞ => True + end }. + Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. + + 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 + end; + subst; try fsatz. + + Program Definition add (P1 P2:point) : point := + exist _ + match coordinates P1, coordinates P2 return _ with + (x1, y1), (x2, y2) => + if Decidable.dec (x1 = x2) + then if Decidable.dec (y1 = - y2) + then ∞ + else (b*(3*x1^2+2*a*x1+1)^2/(2*b*y1)^2-a-x1-x1, (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) + else (b*(y2-y1)^2/(x2-x1)^2-a-x1-x2, (2*x1+x2+a)*(y2-y1)/(x2-x1)-b*(y2-y1)^3/(x2-x1)^3-y1) + | ∞, ∞ => ∞ + | ∞, _ => coordinates P2 + | _, ∞ => coordinates P1 + 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. + + 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}. + + 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. + + Definition eq (P1 P2:point) := + match coordinates P1, coordinates P2 with + | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2 + | ∞, ∞ => True + | _, _ => False + end. + + 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. + + Section AddX. + Lemma homogeneous_x_differential_addition_releations P1 P2 : + match coordinates (add P2 (opp P1)), coordinates P1, coordinates P2, coordinates (add P1 P2) with + | (x, _), (x1, _), (x2, _), (x3, _) => + if Decidable.dec (x1 = x2) + then x3 * (4*x1*(x1^2 + a*x1 + 1)) = (x1^2 - 1)^2 + else x3 * (x*(x1-x2)^2) = (x1*x2 - 1)^2 + | _, _, _, _ => True + 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). + + (* 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 + pair X2 Z2, pair X3 Z3 => + let A := X2+Z2 in + let AA := A^2 in + let B := X2-Z2 in + let BB := B^2 in + let E := AA-BB in + let C := X3+Z3 in + let D := X3-Z3 in + let DA := D*A in + let CB := C*B in + let X5 := (DA+CB)^2 in + let Z5 := X1*(DA-CB)^2 in + 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 *) + Abort. + End AddX. + End MontgomeryCurve. +End M.
\ No newline at end of file |