diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-10-10 15:30:20 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-10-10 15:31:19 -0400 |
| commit | f4b071306ee1d51500de9b167acb7c701616ab92 (patch) | |
| tree | 8de8a7234f718d374af548e7a042aef78af691af /src/Spec | |
| parent | 2b7ee7e329e50c39c99d9c17756d6f8ff1a021ae (diff) | |
Filled in point/scalar encoding definitions.
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/Ed25519.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index d7bf50481..a8e95cf9d 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -61,8 +61,12 @@ Section Ed25519. (F.of_Z q 15112221349535400772501151409588531511454012693041857206046113283949847762202, F.of_Z q 4 / F.of_Z q 5). - Axiom Eenc : E -> Word.word b. (* TODO(jadep) *) - Axiom Senc : Fl -> Word.word b. (* TODO(jadep) *) + Definition Fencode {b : nat} {m} : F m -> Word.word b := + 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. (* 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. |