From 5357fe92e65712a3e2506fe0a939b358d14183d7 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 21 Sep 2016 20:45:01 -0400 Subject: alternative signing derivation cleanup --- src/Spec/EdDSA.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/Spec') diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 2971bfef8..f8581c4c9 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -21,6 +21,7 @@ Module Import Notations. Infix "^" := pow. Infix "mod" := modulo (at level 40, no associativity). Infix "++" := Word.combine. + Notation setbit := setbit. End Notations. Generalizable All Variables. @@ -73,7 +74,7 @@ Section EdDSA. Program Definition curveKey (sk:secretkey) : nat := let x := wfirstn n (H sk) in (* hash the key, use first "half" for secret scalar *) let x := x - (x mod (2^c)) in (* it is implicitly 0 mod (2^c) *) - x + 2^n. (* and the high bit is always set *) + setbit x n. (* and the high bit is always set *) Local Infix "+" := Eadd. Local Infix "*" := EscalarMult. -- cgit v1.2.3