diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-11-06 21:03:39 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-11-06 22:39:04 -0500 |
| commit | 7ae2244439e0f8e72fcbbbb276aaa5f240509cb9 (patch) | |
| tree | 6cd6ec4455418d64ced9e77064dd245e9f7cb569 /src/Specific/GF25519.v | |
| parent | 3dfd82f6493b8b38656b01b33a64921d01e6bdf6 (diff) | |
move B_order_l and prime_q
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 0a487b1e2..2c0365fd2 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -14,6 +14,7 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Decidable. Require Import Crypto.Algebra. +Require Crypto.Spec.Ed25519. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. Local Open Scope Z. @@ -21,7 +22,7 @@ Local Open Scope Z. (* BEGIN precomputation. *) Definition modulus : Z := Eval compute in 2^255 - 19. -Lemma prime_modulus : prime modulus. Admitted. +Definition prime_modulus : prime modulus := Crypto.Spec.Ed25519.prime_q. Definition int_width := 64%Z. Definition freeze_input_bound := 32%Z. |