put EdDSA encoding sign bit at the MSB

1 files changed, 6 insertions, 3 deletions

diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index a8e95cf9d..d6873607f 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -61,12 +61,15 @@ Section Ed25519.
     (F.of_Z q 15112221349535400772501151409588531511454012693041857206046113283949847762202,
      F.of_Z q 4 / F.of_Z q 5).
 
-  Definition Fencode {b : nat} {m} : F m -> Word.word b :=
+  Local Infix "++" := Word.combine.
+  Local Notation bit b := (Word.WS b Word.WO : Word.word 1).
+
+  Definition Fencode {len} {m} : F m -> Word.word len :=
     fun x : F m => (Word.NToWord _ (BinIntDef.Z.to_N (F.to_Z x))).
   Definition sign (x : F q) : bool := BinIntDef.Z.testbit (F.to_Z x) 0.
   Definition Eenc : E -> Word.word b := fun P =>
-    let '(x,y) := E.coordinates P in Word.WS (sign x) (Fencode y).
-  Definition Senc : Fl -> Word.word b := Fencode.
+    let '(x,y) := E.coordinates P in Fencode (len:=b-1) y ++ bit (sign x).
+  Definition Senc : Fl -> Word.word b := Fencode (len:=b).
 
   (* TODO(andreser): prove this after we have fast scalar multplication *)
   Axiom B_order_l : CompleteEdwardsCurveTheorems.E.eq (BinInt.Z.to_nat l * B)%E E.zero.