diff options
| -rw-r--r-- | src/Spec/Ed25519.v | 11 | ||||
| -rw-r--r-- | src/Util/Tuple.v | 4 |
2 files changed, 11 insertions, 4 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 51b1b0831..d7bf50481 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -55,11 +55,18 @@ Section Ed25519. (F:=Fq) (Feq:=Logic.eq) (Fone:=F.one) (Fadd:=F.add) (Fmul:=F.mul) (a:=a) (d:=d). - Axiom B : E. (* TODO(andreser) *) + Local Obligation Tactic := Decidable.vm_decide. (* to prove that B is on curve *) + + Program Definition B : E := + (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) *) + (* 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. + Require Import Crypto.Util.Decidable. Definition ed25519 : EdDSA (E:=E) (Eadd:=E.add) (Ezero:=E.zero) (EscalarMult:=E.mul) (B:=B) @@ -67,5 +74,5 @@ Section Ed25519. (Eeq:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.eq) (* TODO: move defn *) (l:=l) (b:=b) (n:=n) (c:=c) (Eenc:=Eenc) (Senc:=Senc) (H:=H). - Admitted. + Proof. split; try exact _; try exact B_order_l; vm_decide. Qed. End Ed25519.
\ No newline at end of file diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 6ef7a0ca4..bcfc7be5b 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -142,12 +142,12 @@ Proof. { exact _. } { intros ??. exact _. } -Qed. +Defined. Global Instance dec_fieldwise {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise A A n RA) | 10. Proof. destruct n; unfold fieldwise; exact _. -Qed. +Defined. Fixpoint fieldwiseb' {A B} (n:nat) (R:A->B->bool) (a:tuple' A n) (b:tuple' B n) {struct n} : bool. destruct n; simpl @tuple' in *. |