From 405f5840e5d9097b034a05d5eeab5ae6ba5757a3 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 10 Oct 2016 11:23:06 -0400 Subject: Spec.Ed25519: fix exponent field modulus --- src/Spec/Ed25519.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Spec') diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 150e3f388..bdafa10fe 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -11,7 +11,7 @@ Section Ed25519. Definition q : BinNums.Z := 2^255 - 19. Definition Fq : Type := F q. - Definition l : BinNums.Z := 252 + 27742317777372353535851937790883648493. + Definition l : BinNums.Z := 2^252 + 27742317777372353535851937790883648493. Definition Fl : Type := F l. Local Open Scope F_scope. -- cgit v1.2.3