diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-09-21 20:45:01 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-09-22 10:44:07 -0400 |
| commit | 5357fe92e65712a3e2506fe0a939b358d14183d7 (patch) | |
| tree | ea0328c53e10620d9a46cd13606a5b6646ce7d6f /src/Spec/EdDSA.v | |
| parent | fd5cba50d8743149e7ca4e386716126f2fc03e63 (diff) | |
alternative signing derivation
cleanup
Diffstat (limited to 'src/Spec/EdDSA.v')
| -rw-r--r-- | src/Spec/EdDSA.v | 3 |
1 files changed, 2 insertions, 1 deletions
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. |