diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-10-27 10:12:54 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-11-04 00:27:28 -0400 |
commit | 6498b3808c81eeb19f5b1b3a3c8797c1c4adc83a (patch) | |
tree | 9566a90388fb9ebb4280d03edb2035f6c91976e5 /src/Spec/Ed25519.v | |
parent | da89fd027e7fc9339cb3f637edf47f6a74c7d589 (diff) |
put EdDSA encoding sign bit at the MSB
Diffstat (limited to 'src/Spec/Ed25519.v')
-rw-r--r-- | src/Spec/Ed25519.v | 9 |
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. |