diff options
| author |  varomodt <varomodt@localhost.localdomain> | 2016-01-09 13:43:53 -0500 |
|---|---|---|
| committer | varomodt <varomodt@localhost.localdomain> | 2016-01-09 13:43:53 -0500 |
| commit | f5127ba5bb5c1b932b51f9b3d43a18aa566a6d26 (patch) | |
| tree | 44938bc996c9604322a84391399743af9993a5c0 /src/Specific | |
| parent | bb4c8e7d281279eb9aeb44c5d0de5be1d022028c (diff) | |
simple refactor of makefile; comments
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/EdDSA25519.v | 12 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 2 |
2 files changed, 10 insertions, 4 deletions
diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v index 26c45a713..32ae4dde7 100644 --- a/src/Specific/EdDSA25519.v +++ b/src/Specific/EdDSA25519.v @@ -1,6 +1,6 @@ Require Import ZArith.ZArith Zpower ZArith Znumtheory. Require Import NPeano. -Require Import Galois.EdDSA Galois GaloisTheory. +Require Import Crypto.Galois.EdDSA Crypto.Galois.GaloisField. Require Import Crypto.Curves.PointFormats. Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil. Require Import Bedrock.Word. @@ -65,7 +65,8 @@ Module EdDSA25519_Params <: EdDSAParams. unfold n, b; omega. Qed. - Module Import GFDefs := GaloisDefs Modulus_q. + Module GFDefs := GaloisField Modulus_q. + Import GFDefs. Local Open Scope GF_scope. Definition a := GFopp 1%GF. @@ -105,7 +106,7 @@ Module EdDSA25519_Params <: EdDSAParams. rewrite H1; reflexivity. Qed. - Lemma a_square : exists x, (x * x = a)%GF. + Lemma a_square_old : exists x, (x * x = a)%GF. Proof. intros. pose proof (minus1_square_1mod4 q (proj2_sig q) q_1mod4). @@ -119,15 +120,20 @@ Module EdDSA25519_Params <: EdDSAParams. (* TODO *) Parameter d : GF. + Parameter sqrt_a : GF. Axiom d_nonsquare : forall x, x^2 <> d. + Axiom a_square: (sqrt_a^2 = a)%GF. + Axiom char_gt_2: (1+1 <> 0)%GF. Module CurveParameters <: TwistedEdwardsParams Modulus_q. Module GFDefs := GFDefs. Definition a : GF := a. + Definition sqrt_a := sqrt_a. Definition a_nonzero := a_nonzero. Definition a_square := a_square. Definition d := d. Definition d_nonsquare := d_nonsquare. + Definition char_gt_2 := char_gt_2. End CurveParameters. Module Facts := CompleteTwistedEdwardsFacts Modulus_q CurveParameters. Module Import Curve := Facts.Curve. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 51f1b14c8..4b06e5230 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -139,7 +139,7 @@ end. Section GF25519Base25Point5Formula. Import GF25519Base25Point5. - Import GF. + Import Field. Hint Rewrite Z.mul_0_l |