diff options
Diffstat (limited to 'src/CompleteEdwardsCurve/DoubleAndAdd.v')
| -rw-r--r-- | src/CompleteEdwardsCurve/DoubleAndAdd.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v index d58a06c55..50027349d 100644 --- a/src/CompleteEdwardsCurve/DoubleAndAdd.v +++ b/src/CompleteEdwardsCurve/DoubleAndAdd.v @@ -5,26 +5,26 @@ Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith. Section EdwardsDoubleAndAdd. Context {prm:TwistedEdwardsParams}. - Definition doubleAndAdd (bound n : nat) (P : point) : point := - iter_op unifiedAdd zero N.testbit_nat (N.of_nat n) P bound. + Definition doubleAndAdd (bound n : nat) (P : E.point) : E.point := + iter_op E.add E.zero N.testbit_nat (N.of_nat n) P bound. - Lemma scalarMult_double : forall n P, scalarMult (n + n) P = scalarMult n (P + P)%E. + Lemma scalarMult_double : forall n P, E.mul (n + n) P = E.mul n (P + P)%E. Proof. intros. replace (n + n)%nat with (n * 2)%nat by omega. induction n; simpl; auto. - rewrite twistedAddAssoc. + rewrite E.add_assoc. f_equal; auto. Qed. Lemma doubleAndAdd_spec : forall bound n P, N.size_nat (N.of_nat n) <= bound -> - scalarMult n P = doubleAndAdd bound n P. + E.mul n P = doubleAndAdd bound n P. Proof. induction n; auto; intros; unfold doubleAndAdd; rewrite iter_op_spec with (scToN := fun x => x); ( unfold Morphisms.Proper, Morphisms.respectful, Equivalence.equiv; intros; subst; try rewrite Nat2N.id; - reflexivity || assumption || apply twistedAddAssoc - || rewrite twistedAddComm; apply zeroIsIdentity). + reflexivity || assumption || apply E.add_assoc + || rewrite E.add_comm; apply E.add_0_r). Qed. End EdwardsDoubleAndAdd.
\ No newline at end of file |