diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-10-12 20:41:31 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-10-12 20:46:00 -0400 |
| commit | c25319ab990ba5cff403e413d38e9381c18783b8 (patch) | |
| tree | 59ed868005f0446340da8230008408ef11f47acb /src/Experiments | |
| parent | 03795fba88904cd4161ed9920aacad0c099ce6c4 (diff) | |
defined sign operation on field elements
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index a904dc537..6bafde3c4 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -7,8 +7,12 @@ Require Crypto.Encoding.PointEncoding. Import Morphisms. Context {H: forall n : nat, Word.word n -> Word.word (b + b)}. -(* TODO : define feSign *) -Context {feSign : GF25519.fe25519 -> bool}. + +Definition feSign (x : GF25519.fe25519) : bool := + let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in + BinInt.Z.testbit x0 0. + +(* TODO *) Context {feSign_correct : forall x, PointEncoding.sign x = feSign (ModularBaseSystem.encode x)}. Context {Proper_feSign : Proper (ModularBaseSystem.eq ==> eq) feSign}. |