diff options
Diffstat (limited to 'src/Experiments/SpecEd25519.v')
-rw-r--r-- | src/Experiments/SpecEd25519.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v index 4e30313d9..659a0ec66 100644 --- a/src/Experiments/SpecEd25519.v +++ b/src/Experiments/SpecEd25519.v @@ -149,11 +149,11 @@ Local Infix "*" := (E.mul(H0:=curve25519params)). Axiom H : forall n : nat, word n -> word (b + b). Axiom B : point. (* TODO: B = decodePoint (y=4/5, x="positive") *) Axiom B_nonzero : B <> zero. -Axiom l_order_B : l * B = zero. -Axiom point_encoding : canonical encoding of point as word b. -Axiom scalar_encoding : canonical encoding of {n : nat | n < l} as word b. +Axiom l_order_B : E.eq (l * B) zero. +Axiom Eenc : point -> word b. +Axiom Senc : nat -> word b. -Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B point_encoding scalar_encoding := +Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B Eenc Senc := { EdDSA_c_valid := c_valid; EdDSA_n_ge_c := n_ge_c; |