blob: 248e0af6e6fe26da16b0cd5074004b4803781ec9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
Require Import Zpower ZArith Znumtheory.
Require Import Crypto.Galois.GaloisField.
Require Import Crypto.Curves.PointFormats.
Definition two_255_19 := 2^255 - 19. (* <http://safecurves.cr.yp.to/primeproofs.html> *)
Fact two_255_19_prime : prime two_255_19. Admitted.
Module Modulus25519 <: Modulus.
Definition modulus := exist _ two_255_19 two_255_19_prime.
End Modulus25519.
Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519.
Module Import GFDefs := GaloisField Modulus25519.
Local Open Scope GF_scope.
Definition a : GF := -1.
Definition d : GF := -121665 / 121666.
Lemma a_nonzero : a <> 0.
Proof.
discriminate.
Qed.
Definition sqrt_a: GF := 19681161376707505956807079304988542015446066515923890162744021073123829784752.
Lemma a_square : sqrt_a^2 = a.
Proof.
(* An example of how to use ring properly *)
replace (sqrt_a ^ 2) with (sqrt_a * sqrt_a) by ring.
assert ((inject ((GFToZ sqrt_a) * (GFToZ sqrt_a)))%Z = a).
- apply gf_eq.
(* vm_compute runs out of memory. *)
admit.
- rewrite inject_distr_mul in H.
intuition.
Admitted.
Lemma d_nonsquare : forall x, x * x <> d.
(* <https://en.wikipedia.org/wiki/Euler%27s_criterion> *)
Admitted.
Definition A : GF := 486662.
(* Definition montgomeryOnCurve25519 := montgomeryOnCurve 1 A. *)
(* Module-izing Twisted was a breaking change
Definition m1TwistedOnCurve25519 := twistedOnCurve (0 -1) d.
Definition identityTwisted : twisted := mkTwisted 0 1.
Lemma identityTwistedOnCurve : m1TwistedOnCurve25519 identityTwisted.
unfold m1TwistedOnCurve25519, twistedOnCurve.
simpl; field.
Qed.
*)
Definition basepointY := 4 / 5.
(* True iff this prime is odd *)
Definition char_gt_2: (1+1) <> 0.
Admitted.
End Curve25519Params.
Module Edwards25519 := CompleteTwistedEdwardsCurve Modulus25519 Curve25519Params.
Module Edwards25519Minus1Twisted := Minus1Format Modulus25519 Curve25519Params.
|
