diff options
Diffstat (limited to 'src/Spec/Test/X25519.v')
| -rw-r--r-- | src/Spec/Test/X25519.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Spec/Test/X25519.v b/src/Spec/Test/X25519.v index a4fed8dd4..97b3a5fe0 100644 --- a/src/Spec/Test/X25519.v +++ b/src/Spec/Test/X25519.v @@ -1,6 +1,9 @@ (* Test vectors from <https://tools.ietf.org/html/rfc7748#section-5.2>, with hex values converted to decimal using python like this: > int.from_bytes(binascii.unhexlify('deadbeef'), 'little') *) +Require Import Coq.NArith.BinNatDef. +Require Import Coq.ZArith.BinIntDef. +Require Import Coq.PArith.BinPosDef. Require Import Spec.ModularArithmetic Spec.MxDH Crypto.Util.Decidable. Definition F := F (2^255 - 19). Definition a : F := F.of_Z _ 486662. |