From 3d8afe1c9bd905e3a62523e87a2aa7e5d9f5093d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 21 Jun 2016 23:29:38 -0400 Subject: EdDSA.v: resolve ambiguity based on ed25519.py --- src/Spec/EdDSA.v | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 1ed1a8054..d71f2ad44 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -1,7 +1,5 @@ Require Import Crypto.Spec.Encoding. - -Require Import Crypto.Util.WordUtil. -Require Bedrock.Word. +Require Bedrock.Word Crypto.Util.WordUtil. Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt. Require Coq.Numbers.Natural.Peano.NPeano. Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. @@ -50,13 +48,14 @@ Section EdDSA. Local Notation publickey := (Word.word b) (only parsing). Local Notation signature := (Word.word (b + b)) (only parsing). - - Existing Class le. Local Existing Instance EdDSA_n_le_b. Local Arguments H {n} _. + Local Notation wfirstn n w := (@WordUtil.wfirstn n _ w _) (only parsing). + + Require Import Omega. + Obligation Tactic := simpl; intros; try apply NPeano.Nat.mod_upper_bound; destruct prm; omega. - (* TODO: proofread curveKey and definition of n *) - Definition curveKey (sk:secretkey) : nat := - let x := wfirstn n sk in (* first half of the secret key is a scalar *) + Program Definition curveKey (sk:secretkey) : nat := + let x := wfirstn n (H sk) in (* hash the key, use first "half" for secret scalar *) let x := x - (x mod (2^c)) in (* it is implicitly 0 mod (2^c) *) x + 2^n. (* and the high bit is always set *) @@ -72,7 +71,6 @@ Section EdDSA. let s : nat := curveKey sk in (* secret scalar *) let S : {n|n publickey -> signature -> Prop := -- cgit v1.2.3