aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Encoding/PointEncoding.v43
-rw-r--r--src/Experiments/Ed25519.v53
2 files changed, 66 insertions, 30 deletions
diff --git a/src/Encoding/PointEncoding.v b/src/Encoding/PointEncoding.v
index 39bb8c973..b005ce3df 100644
--- a/src/Encoding/PointEncoding.v
+++ b/src/Encoding/PointEncoding.v
@@ -64,9 +64,11 @@ Section PointEncoding.
{Kenc_correct : forall x, Fencode x = Kenc (phi x)}.
Notation KonCurve := (@Pre.onCurve _ Keq Kone Kadd Kmul Ka Kd).
- Context {Kpoint} {Kcoord_to_point : forall P, KonCurve P -> Kpoint}
+ Context {Kpoint}
+ {Kcoord_to_point : @E.point K Keq Kone Kadd Kmul Ka Kd -> Kpoint}
{Kpoint_to_coord : Kpoint -> (K * K)}.
- Context {Kp2c_c2p : forall P pf, Tuple.fieldwise (n := 2) Keq (Kpoint_to_coord (Kcoord_to_point P pf)) P}.
+ Context {Kp2c_c2p : forall pt : E.point, Tuple.fieldwise (n := 2) Keq (Kpoint_to_coord (Kcoord_to_point pt)) (E.coordinates pt)}.
+ Check Kp2c_c2p.
Context {Kpoint_eq : Kpoint -> Kpoint -> Prop} {Kpoint_add : Kpoint -> Kpoint -> Kpoint}.
Context {Kpoint_eq_correct : forall p q, Kpoint_eq p q <-> Tuple.fieldwise (n := 2) Keq (Kpoint_to_coord p) (Kpoint_to_coord q)} {Kpoint_eq_Equivalence : Equivalence Kpoint_eq}.
@@ -89,12 +91,7 @@ Section PointEncoding.
reflexivity.
Qed.
- Definition point_phi (P : Fpoint) : Kpoint.
- Proof.
- destruct P as [[fx fy]].
- apply (Kcoord_to_point (phi fx, phi fy)).
- apply phi_onCurve; auto.
- Defined.
+ Definition point_phi (P : Fpoint) : Kpoint := Kcoord_to_point (E.ref_phi (fieldK := Kfield) (Ha := phi_a) (Hd := phi_d) P).
Lemma Proper_point_phi : Proper (E.eq ==> Kpoint_eq) point_phi.
Proof.
@@ -102,6 +99,7 @@ Section PointEncoding.
apply Kpoint_eq_correct; cbv [point_phi].
destruct x, y.
repeat break_let.
+ cbv [E.ref_phi].
rewrite !Kp2c_c2p.
apply E.Proper_coordinates in H; cbv [E.coordinates proj1_sig] in H.
inversion H; econstructor; cbv [Tuple.fieldwise' fst snd] in *; subst;
@@ -144,9 +142,10 @@ Section PointEncoding.
destruct P as [[fx fy]]; cbv [E.coordinates proj1_sig].
break_match.
match goal with
- H: Kpoint_to_coord (Kcoord_to_point (?x, ?y) ?pf) = (_,_) |- _ => let A := fresh "H" in
- pose proof (Kp2c_c2p (x,y) pf) as A; rewrite Heqp in A;
+ H: Kpoint_to_coord (Kcoord_to_point ?x) = (_,_) |- _ => let A := fresh "H" in
+ pose proof (Kp2c_c2p x) as A; rewrite Heqp in A;
inversion A; cbv [fst snd Tuple.fieldwise'] in * end.
+ cbv [E.coordinates E.ref_phi proj1_sig] in *.
f_equal; rewrite ?H0, ?H1; auto.
Qed.
@@ -191,7 +190,7 @@ Section PointEncoding.
let '(x,y) := xy in
match Decidable.dec (Keq (Kadd (Kmul Ka (Kmul x x)) (Kmul y y))
(Kadd Kone (Kmul (Kmul Kd (Kmul x x)) (Kmul y y)))) with
- | left A => Some (Kcoord_to_point (x,y) (onCurve_eq x y A))
+ | left A => Some (Kcoord_to_point (exist _ (x,y) (onCurve_eq x y A)))
| right _ => None
end.
@@ -383,6 +382,7 @@ Section PointEncoding.
repeat break_match; try tauto; try reflexivity.
simpl.
apply Kpoint_eq_correct.
+ cbv [point_phi E.ref_phi].
rewrite !Kp2c_c2p.
reflexivity.
Qed.
@@ -400,13 +400,20 @@ Section PointEncoding.
rewrite H, H0 in k'.
break_match; try congruence.
simpl. apply Kpoint_eq_correct.
- repeat ( break_match;
- match goal with
- H: Kpoint_to_coord (Kcoord_to_point (?x, ?y) ?pf) = (_,_) |- _ => let A := fresh "H" in
- pose proof (Kp2c_c2p (x,y) pf) as A; rewrite H in A;
- inversion A; cbv [fst snd Tuple.fieldwise'] in * end;
- intuition;
- repeat match goal with H : Keq _ _ |- _ => rewrite H end; try reflexivity).
+ repeat break_match.
+ do 2 match goal with
+ H: Kpoint_to_coord (Kcoord_to_point ?pt) = (_,_) |- _ =>
+ let A := fresh "H" in
+ pose proof (Kp2c_c2p pt) as A; rewrite H in A;
+ cbv [E.coordinates proj1_sig] in *; inversion A;
+ clear A H
+ end.
+ split;
+ repeat match goal with
+ | |- _ => assumption
+ | |- _ => symmetry; assumption
+ | |- _ => etransitivity; [ eassumption | ]
+ end.
} {
pose proof n as k'.
rewrite H, H0 in k'.
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index ee2af2a3c..ff060d0ca 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -86,15 +86,14 @@ Proof.
reflexivity.
Qed.
-Let EToRep := PointEncoding.point_phi
- (Kfield := GF25519.field25519)
- (phi_homomorphism := GF25519.homomorphism_F25519_encode)
- (Kpoint := Erep)
- (phi_a := phi_a)
- (phi_d := phi_d)
- (Kcoord_to_point := coord_to_extended)
- (phi_bijective := encode_eq_iff)
-.
+Let EToRep :=
+ PointEncoding.point_phi
+ (Kfield := GF25519.field25519)
+ (phi_homomorphism := GF25519.homomorphism_F25519_encode)
+ (Kpoint := Erep)
+ (phi_a := phi_a)
+ (phi_d := phi_d)
+ (Kcoord_to_point := ExtendedCoordinates.Extended.from_twisted (prm := twedprm_ERep) (field := GF25519.field25519)).
Let ZNWord sz x := Word.NToWord sz (BinInt.Z.to_N x).
Let WordNZ {sz} (w : Word.word sz) := BinInt.Z.of_N (Word.wordToN w).
@@ -206,6 +205,7 @@ Admitted.
Lemma Proper_feEnc : Proper (ModularBaseSystem.eq ==> eq) feEnc.
Admitted.
+(*
Lemma ext_to_coord_coord_to_ext : forall (P : GF25519.fe25519 * GF25519.fe25519)
(pf : Pre.onCurve P),
Tuple.fieldwise (n := 2)
@@ -221,19 +221,45 @@ Proof.
(field := GF25519.field25519) (a := a) (d := d)).
apply ExtendedCoordinates.Extended.to_twisted_from_twisted.
Qed.
+ *)
+(*
+Lemma to_twist
+ ed_from_twisted_coordinates_eq :
+ forall pt : E,
+ Tuple.fieldwise ModularBaseSystem.eq (n := 2)
+ ((fun P0 : Erep =>
+ CompleteEdwardsCurve.E.coordinates
+ (ExtendedCoordinates.Extended.to_twisted (field := GF25519.field25519) P0))
+ (ExtendedCoordinates.Extended.from_twisted (field := PrimeFieldTheorems.F.field_modulo GF25519.modulus) pt))
+ (CompleteEdwardsCurve.E.coordinates pt).
+Proof.
+ intros.
+ pose proof ExtendedCoordinates.Extended.to_twisted_from_twisted.
+ specialize (H0 pt).
+*)
Lemma ERepEnc_correct P : Eenc P = ERepEnc (EToRep P).
Proof.
cbv [Eenc ERepEnc EToRep sign Fencode].
+ Check (PointEncoding.Kencode_point_correct
+ (Ksign_correct := feSign_correct)
+ (Kenc_correct := feEnc_correct)
+ (Proper_Ksign := Proper_feSign)
+ (Proper_Kenc := Proper_feEnc)).
transitivity (PointEncoding.encode_point (b := 255) P);
- [ | apply (PointEncoding.Kencode_point_correct
+ [ | eapply (PointEncoding.Kencode_point_correct
(Ksign_correct := feSign_correct)
(Kenc_correct := feEnc_correct)
- (Kp2c_c2p := ext_to_coord_coord_to_ext)
(Proper_Ksign := Proper_feSign)
(Proper_Kenc := Proper_feEnc))
].
reflexivity.
+ Grab Existential Variables.
+ intros.
+ eapply @CompleteEdwardsCurveTheorems.E.Proper_coordinates.
+ { apply GF25519.field25519. }
+ { exact _. }
+ { apply ExtendedCoordinates.Extended.to_twisted_from_twisted. }
Qed.
Lemma ext_eq_correct : forall p q : Erep,
@@ -449,7 +475,10 @@ Let ERepDec :=
GF25519.mul
ModularBaseSystem.div
_ a d feSign
- _ coord_to_extended
+ _ (ExtendedCoordinates.Extended.from_twisted
+ (field := GF25519.field25519)
+ (prm := twedprm_ERep)
+ )
feDec GF25519.sqrt
).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 02:02:30 +0000