Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update Curves/Weierstrass #1953

Merged
merged 3 commits into from
Sep 5, 2024
Merged

Update Curves/Weierstrass #1953

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2ae1c17
faster Weierstrass point doubling using coordinate halving
andres-erbsen Aug 19, 2024
7be3973
update Weierstrass Affine, Jacobian with Proper, add laws
andres-erbsen Sep 4, 2024
6f13372
update CoZ
andres-erbsen Sep 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
66 changes: 59 additions & 7 deletions src/Curves/Weierstrass/Affine.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,20 +1,72 @@
Require Import Crypto.Spec.WeierstrassCurve.
Require Import Crypto.Algebra.Field.
Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.SetoidSubst.
Import RelationClasses Morphisms.

Module W.
Section W.
Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
{field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
{Feq_dec:DecidableRel Feq}.
Local Infix "+" := Fadd. Local Infix "-" := Fsub.
Local Infix "*" := Fmul. Local Infix "/" := Fdiv.
Local Notation "x ^ 2" := (x*x) (at level 30).
Local Notation point := (@W.point F Feq Fadd Fmul a b).

Program Definition opp (P:@W.point F Feq Fadd Fmul a b) : @W.point F Feq Fadd Fmul a b
:= match W.coordinates P return F*F+_ with
| inl (x1, y1) => inl (x1, Fopp y1)
| inr tt => inr tt
end.
Next Obligation.
cbv [W.coordinates]; break_match; trivial; fsatz.
Definition opp (P : point) : point. refine (exist _ (
match W.coordinates P with
| inl (x1, y1) => inl (x1, Fopp y1)
| inr tt => inr tt
end) _).
Proof. abstract (cbv [W.coordinates]; break_match; trivial; fsatz). Defined.

Global Instance Equivalence_eq : Equivalence (@W.eq _ Feq Fadd Fmul a b).
Proof.
cbv [W.eq W.coordinates]; split; repeat intros [ [ []|[] ] ?]; intuition try solve
[contradiction | apply reflexivity | apply symmetry; trivial | eapply transitivity; eauto 1].
Qed.

Global Instance Proper_opp : Proper (W.eq ==> W.eq) opp.
Proof.
repeat (intros [ [[]|[] ]?] || intro); cbv [W.coordinates opp W.eq] in *;
repeat (try destruct_head' @and; try case dec as []; try contradiction; try split); trivial.
setoid_subst_rel Feq; reflexivity.
Qed.

(* Weierstraß Elliptic Curves and Side-Channel Attacks
by Eric Brier and Marc Joye, 2002 *)
Definition add' (P1 P2 : point) : point. refine (exist _
match W.coordinates P1, W.coordinates P2 with
| inl (x1, y1), inl (x2, y2) =>
if dec (Feq y1 (Fopp y2)) then
if dec (Feq x1 x2) then inr tt
else let k := (y2-y1)/(x2-x1) in
let x3 := k^2-x1-x2 in
let y3 := k*(x1-x3)-y1 in
inl (x3, y3)
else let k := ((x1^2 + x1*x2 + x2^2 + a)/(y1+y2)) in
let x3 := k^2-x1-x2 in
let y3 := k*(x1-x3)-y1 in
inl (x3, y3)
| inr tt, inr tt => inr tt
| inr tt, _ => W.coordinates P2
| _, inr tt => W.coordinates P1
end _).
Proof. abstract (cbv [W.coordinates]; break_match; trivial; fsatz). Defined.

Lemma add'_correct char_ge_3 : forall P Q : point, W.eq (W.add' P Q) (W.add(char_ge_3:=char_ge_3) P Q).
Proof. intros [ [[]|]?] [ [[]|]?]; cbv [W.coordinates W.add W.add' W.eq]; break_match; try split; try fsatz. Qed.

Global Instance Proper_add' : Proper (W.eq ==> W.eq ==> W.eq) add'.
Proof.
repeat (intros [ [[]|[] ]?] || intro); cbv [W.coordinates W.add' W.eq] in *;
repeat (try destruct_head' @and; try case dec as []; try contradiction; try split); trivial.
Time par : fsatz. (* setoid_subst_rel is slower *)
Qed.

Global Instance Proper_add {char_ge_3} :
Proper (W.eq ==> W.eq ==> W.eq) (@W.add _ Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv _ _ char_ge_3 a b).
Proof. repeat intro. rewrite <-2add'_correct. apply Proper_add'; trivial. Qed.
End W.
End W.
87 changes: 54 additions & 33 deletions src/Curves/Weierstrass/Jacobian/CoZ.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ Module Jacobian.
Local Infix "+" := Fadd. Local Infix "-" := Fsub.
Local Infix "*" := Fmul. Local Infix "/" := Fdiv.
Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x^2*x).
Local Notation "2" := (1+1). Local Notation "4" := (2+2).
Local Notation "2" := (1+1). Local Notation "4" := (1+1+1+1).
Local Notation "8" := (4+4). Local Notation "27" := (4*4 + 4+4 +1+1+1).
Local Notation Wpoint := (@W.point F Feq Fadd Fmul a b).
Context {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive}
Expand Down Expand Up @@ -67,8 +67,8 @@ Module Jacobian.
| _ => progress destruct_head'_sum
| _ => progress destruct_head'_bool
| _ => progress destruct_head'_or
| H: context[@dec ?P ?pf] |- _ => destruct (@dec P pf)
| |- context[@dec ?P ?pf] => destruct (@dec P pf)
| H: context[@dec ?P ?pf] |- _ => destruct (@dec P pf) || destruct (@dec P pf) at 1
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@JasonGross this is because dependent occurrences and destructable occurranes of the same expression. Do you know a more systematic fix from the top of your head?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't it be "at 1 in H" or similar?

A more systematic fix: H: context C[@dec ?P ?pf] |- _ => destruct (@dec P pf) || (let p := fresh in pose (@dec P pf) as p; let C' := context C[p] in change C' in (type of H); destruct p)
Maybe too painful though

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is the idea that change works fine for changing some but not all occurrences?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, change + context will select only one occurrence at a time. This won't work if you need to simultaneously destruct in two or more occurrences though

| |- context[@dec ?P ?pf] => destruct (@dec P pf) || destruct (@dec P pf) at 1
| |- ?P => lazymatch type of P with Prop => split end
end.
Ltac prept := repeat prept_step.
Expand Down Expand Up @@ -405,36 +405,57 @@ Module Jacobian.
end;
fsatz ].

Hint Unfold Jacobian.double negb andb : points_as_coordinates.
Hint Unfold W.eq W.add Jacobian.to_affine Jacobian.of_affine Jacobian.add Jacobian.add_impl Jacobian.opp : points_as_coordinates.

(* These could go into Jacobian.v *)
Global Instance Proper_opp : Proper (eq ==> eq) opp. Proof. faster_t_noclear. Qed.
Local Hint Unfold W.add W.add' W.zero W.opp : points_as_coordinates.
Local Hint Unfold Jacobian.double Jacobian.double_impl negb andb : points_as_coordinates.
Local Hint Unfold Jacobian.to_affine Jacobian.to_affine_impl Jacobian.of_affine Jacobian.of_affine_impl Jacobian.add Jacobian.add_impl Jacobian.opp : points_as_coordinates.

Lemma of_affine_add P Q
: eq (of_affine (W.add P Q)) (add (of_affine P) (of_affine Q)).
Proof. t. Qed.

Lemma add_opp (P : point) :
z_of (add P (opp P)) = 0.
Proof. faster_t_noclear. Qed.
Proof. rewrite Jacobian.eq_iff, Jacobian.to_affine_add, 3Jacobian.to_affine_of_affine; reflexivity. Qed.

Lemma add_comm (P Q : point) :
eq (add P Q) (add Q P).
Proof. faster_t_noclear. Qed.
Proof.
pose proof W.commutative_group(discriminant_nonzero:=discriminant_nonzero) _.
rewrite Jacobian.eq_iff, 2Jacobian.to_affine_add.
rewrite Hierarchy.commutative. reflexivity.
Qed.

Lemma add_zero_l (P Q : point) (H : z_of P = 0) :
eq (add P Q) Q.
Proof. faster_t. Qed.
Proof.
pose proof W.commutative_group(discriminant_nonzero:=discriminant_nonzero) _.
rewrite Jacobian.eq_iff, Jacobian.to_affine_add.
rewrite (proj1 (Jacobian.iszero_iff P)), Hierarchy.left_identity; [reflexivity|].
case P as [ [ []?] ?]; cbv [Jacobian.iszero z_of proj1_sig snd] in *; trivial.
Qed.

Lemma add_zero_r (P Q : point) (H : z_of Q = 0) :
eq (add P Q) P.
Proof. faster_t. Qed.
Proof. rewrite add_comm, add_zero_l; trivial; reflexivity. Qed.

Lemma add_double (P Q : point) :
eq P Q ->
eq (add P Q) (double P).
Proof. faster_t_noclear. Qed.
Proof.
rewrite 2Jacobian.eq_iff, Jacobian.to_affine_add, Jacobian.to_affine_double.
intros ->; reflexivity.
Qed.

Lemma add_opp_same_r (P : point) :
eq (add P (opp P)) (of_affine W.zero).
Proof.
pose proof W.commutative_group(discriminant_nonzero:=discriminant_nonzero) _.
rewrite Jacobian.eq_iff, Jacobian.to_affine_add, Jacobian.to_affine_of_affine, Jacobian.to_affine_opp.
rewrite Hierarchy.right_inverse. reflexivity.
Qed.

Lemma z_of_eq_zero (P : point) : eq P (of_affine W.zero) -> z_of P = 0.
Proof. prept. match goal with H : 0 <> 0 |- _ => case (H ltac:(reflexivity)) end. Qed.

Lemma z_of_add_opp_same_r (P : point) :
z_of (add P (opp P)) = 0.
Proof. apply z_of_eq_zero, add_opp_same_r. Qed.

(* This uses assumptions not present in Jacobian.v,
namely char_ge_12 and discriminant_nonzero. *)
Expand Down Expand Up @@ -465,7 +486,7 @@ Module Jacobian.

Lemma opp_co_z (P : point) :
co_z P (opp P).
Proof. unfold co_z; faster_t. Qed.
Proof. unfold co_z. prept. Qed.

Program Definition make_co_z (P Q : point) (HQaff : z_of Q = 1) : point*point :=
match proj1_sig P, proj1_sig Q return (F*F*F)*(F*F*F) with
Expand All @@ -479,8 +500,8 @@ Module Jacobian.
let t2 := t3 * t2 in
(P, (t1, t2, t3))
end.
Next Obligation. Proof. faster_t. Qed.
Next Obligation. Proof. faster_t. Qed.
Next Obligation. Proof. prept. Qed.
Next Obligation. Proof. prept. par: faster_t. Qed.

Hint Unfold is_point co_z make_co_z : points_as_coordinates.

Expand Down Expand Up @@ -520,17 +541,17 @@ Module Jacobian.
let t5 := t5 - t2 in
((t4, t5, t3), (t1, t2, t3))
end.
Next Obligation. Proof. faster_t_noclear. Qed.
Next Obligation. Proof. faster_t. Qed.
Next Obligation. Proof. prept. all : faster_t_noclear. Qed.
Next Obligation. Proof. prept. all : faster_t. Qed.

Hint Unfold zaddu : points_as_coordinates.
Hint Unfold zaddu Jacobian.add_nz_nz : points_as_coordinates.

(* ZADDU(P, Q) = (P + Q, P) if P <> Q, Q <> -P *)
Lemma zaddu_correct (P Q : point) (H : co_z P Q)
(Hneq : x_of P <> x_of Q):
let '(R1, R2) := zaddu P Q H in
eq (add P Q) R1 /\ eq P R2 /\ co_z R1 R2.
Proof. faster_t_noclear. Qed.
Proof. prept. par : faster_t_noclear. Qed.

Lemma zaddu_correct_alt (P Q : point) (H : co_z P Q) :
let '(R1, R2) := zaddu P Q H in
Expand All @@ -546,7 +567,7 @@ Module Jacobian.
Lemma zaddu_correct0 (P : point) :
let '(R1, R2) := zaddu P (opp P) (opp_co_z P) in
z_of R1 = 0 /\ co_z R1 R2.
Proof. faster_t_noclear. Qed.
Proof. prept. all : faster_t_noclear. Qed.

(* Scalar Multiplication on Weierstraß Elliptic Curves from Co-Z Arithmetic *)
(* Goundar, Joye, Miyaji, Rivain, Vanelli *)
Expand Down Expand Up @@ -587,16 +608,16 @@ Module Jacobian.
let t2 := t2 + t6 in
((t1, t2, t3), (t4, t5, t3))
end.
Next Obligation. Proof. faster_t_noclear. Qed.
Next Obligation. Proof. faster_t_noclear. Qed.
Next Obligation. Proof. prept. all : faster_t_noclear. Qed.
Next Obligation. Proof. prept. all : faster_t_noclear. Qed.

Hint Unfold zaddc : points_as_coordinates.
(* ZADDC(P, Q) = (P + Q, P - Q) if P <> Q, Q <> -P *)
Lemma zaddc_correct (P Q : point) (H : co_z P Q)
(Hneq : x_of P <> x_of Q):
let '(R1, R2) := zaddc P Q H in
eq (add P Q) R1 /\ eq (add P (opp Q)) R2 /\ co_z R1 R2.
Proof. faster_t_noclear. Qed.
Proof. prept. par : faster_t_noclear. Qed.

Lemma zaddc_correct_alt (P Q : point) (H : co_z P Q) :
let '(R1, R2) := zaddc P Q H in
Expand Down Expand Up @@ -735,7 +756,7 @@ Module Jacobian.
rewrite add_assoc, add_comm. reflexivity.
- rewrite <- A2, <- B1, <- B2.
rewrite (add_comm P Q).
rewrite add_assoc. rewrite add_zero_r; [reflexivity|apply add_opp].
rewrite add_assoc. rewrite add_zero_r; [reflexivity|apply z_of_add_opp_same_r].
Qed.

Lemma zdau_naive_correct_alt (P Q : point) (H : co_z P Q)
Expand All @@ -756,7 +777,7 @@ Module Jacobian.
rewrite add_assoc, add_comm. reflexivity.
- rewrite <- A2, <- B1, <- B2.
rewrite (add_comm P Q).
rewrite add_assoc. rewrite add_zero_r; [reflexivity|apply add_opp].
rewrite add_assoc. rewrite add_zero_r; [reflexivity|apply z_of_add_opp_same_r].
Qed.

(* Scalar Multiplication on Weierstraß Elliptic Curves from Co-Z Arithmetic *)
Expand Down Expand Up @@ -816,16 +837,16 @@ Module Jacobian.
let t5 := t7 - t5 in
((t1, t2, t3), (t4, t5, t3))
end.
Next Obligation. Proof. faster_t_noclear. Qed.
Next Obligation. Proof. faster_t_noclear. Qed.
Next Obligation. Proof. prept. par:setoid_subst_rel Feq; faster_t_noclear. Qed.
Next Obligation. Proof. prept. par:faster_t_noclear. Qed.

Hint Unfold zdau : points_as_coordinates.

Lemma zdau_naive_eq_zdau (P Q : point) (H : co_z P Q) :
let '(R1, R2) := zdau_naive P Q H in
let '(S1, S2) := zdau P Q H in
eq R1 S1 /\ eq R2 S2.
Proof. faster_t. all: try fsatz. Qed.
Proof. prept. par : faster_t; try fsatz. Qed.

(* Direct proof is intensive, which is why we need the naive implementation *)
Lemma zdau_correct (P Q : point) (H : co_z P Q)
Expand Down
Loading
Loading