diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/BoundedIterOp.v | 94 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/DoubleAndAdd.v | 52 |
3 files changed, 10 insertions, 137 deletions
diff --git a/_CoqProject b/_CoqProject index 1d65a7564..04b25dd6c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,7 +1,6 @@ -R src Crypto src/BaseSystem.v src/BaseSystemProofs.v -src/BoundedIterOp.v src/EdDSAProofs.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/DoubleAndAdd.v diff --git a/src/BoundedIterOp.v b/src/BoundedIterOp.v deleted file mode 100644 index bd4f7d66e..000000000 --- a/src/BoundedIterOp.v +++ /dev/null @@ -1,94 +0,0 @@ -Require Import Crypto.Tactics.VerdiTactics. -Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith. - -Definition testbit_rev p i bound := Pos.testbit_nat p (bound - i). - -Lemma testbit_rev_succ : forall p i b, (i < S b) -> - testbit_rev p i (S b) = - match p with - | xI p' => testbit_rev p' i b - | xO p' => testbit_rev p' i b - | 1%positive => false - end. -Proof. - unfold testbit_rev; intros; destruct p; rewrite <- minus_Sn_m by omega; auto. -Qed. - -(* implements Pos.iter_op only using testbit, not destructing the positive *) -Definition iter_op {A} (op : A -> A -> A) (zero : A) (bound : nat) (p : positive) := - fix iter (i : nat) (a : A) {struct i} : A := - match i with - | O => zero - | S i' => let ret := iter i' (op a a) in - if testbit_rev p i bound - then op a ret - else ret - end. - -Lemma iter_op_step : forall {A} op z b p i (a : A), (i < S b) -> - iter_op op z (S b) p i a = - match p with - | xI p' => iter_op op z b p' i a - | xO p' => iter_op op z b p' i a - | 1%positive => z - end. -Proof. - destruct p; unfold iter_op; (induction i; [ auto |]); intros; rewrite testbit_rev_succ by omega; rewrite IHi by omega; reflexivity. -Qed. - -Lemma pos_size_gt0 : forall p, 0 < Pos.size_nat p. -Proof. - destruct p; intros; auto; try apply Lt.lt_0_Sn. -Qed. -Hint Resolve pos_size_gt0. - -Lemma iter_op_spec : forall b p {A} op z (a : A) (zero_id : forall x : A, op x z = x), (Pos.size_nat p <= b) -> - iter_op op z b p b a = Pos.iter_op op p a. -Proof. - induction b; intros; [pose proof (pos_size_gt0 p); omega |]. - destruct p; simpl; rewrite iter_op_step by omega; unfold testbit_rev; rewrite Minus.minus_diag; try rewrite IHb; simpl in *; auto; omega. -Qed. - -Lemma xO_neq1 : forall p, (1 < p~0)%positive. -Proof. - induction p; auto; apply Pos.lt_succ_diag_r. -Qed. - -Lemma xI_neq1 : forall p, (1 < p~1)%positive. -Proof. - induction p; auto; eapply Pos.lt_trans; apply Pos.lt_succ_diag_r. -Qed. - -Lemma xI_is_succ : forall n p, Pos.of_succ_nat n = p~1%positive -> - (Pos.to_nat (2 * p))%nat = n. -Proof. - induction n; intros; try discriminate. - rewrite <- Pnat.Nat2Pos.id by apply NPeano.Nat.neq_succ_0. - rewrite Pnat.Pos2Nat.inj_iff. - rewrite <- Pos.of_nat_succ. - apply Pos.succ_inj. - rewrite <- Pos.xI_succ_xO. - auto. -Qed. - -Lemma xO_is_succ : forall n p, Pos.of_succ_nat n = p~0%positive -> - Pos.to_nat (Pos.pred_double p) = n. -Proof. - induction n; intros; try discriminate. - rewrite Pos.pred_double_spec. - rewrite <- Pnat.Pos2Nat.inj_iff in *. - rewrite Pnat.Pos2Nat.inj_xO in *. - rewrite Pnat.SuccNat2Pos.id_succ in *. - rewrite Pnat.Pos2Nat.inj_pred by apply xO_neq1. - rewrite <- NPeano.Nat.succ_inj_wd. - rewrite Pnat.Pos2Nat.inj_xO. - omega. -Qed. - -Lemma size_of_succ : forall n, - Pos.size_nat (Pos.of_nat n) <= Pos.size_nat (Pos.of_nat (S n)). -Proof. - intros; induction n; [simpl; auto|]. - apply Pos.size_nat_monotone. - apply Pos.lt_succ_diag_r. -Qed. diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v index 84c1289f6..d04cefc3d 100644 --- a/src/CompleteEdwardsCurve/DoubleAndAdd.v +++ b/src/CompleteEdwardsCurve/DoubleAndAdd.v @@ -1,15 +1,12 @@ Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.BoundedIterOp. +Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Util.IterAssocOp. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith. Section EdwardsDoubleAndAdd. Context {prm:TwistedEdwardsParams}. - Definition doubleAndAdd (b n : nat) (P : point) : point := - match N.of_nat n with - | 0%N => zero - | N.pos p => iter_op unifiedAdd zero b p b P - end. + Definition doubleAndAdd (n : nat) (P : point) : point := + iter_op unifiedAdd zero N.testbit_nat (N.of_nat n) P (N.size_nat (N.of_nat n)). Lemma scalarMult_double : forall n P, scalarMult (n + n) P = scalarMult n (P + P)%E. Proof. @@ -29,43 +26,14 @@ Section EdwardsDoubleAndAdd. auto. Qed. - Lemma doubleAndAdd_spec : forall n b P, (Pos.size_nat (Pos.of_nat n) <= b) -> - scalarMult n P = doubleAndAdd b n P. + + Lemma doubleAndAdd_spec : forall n P, scalarMult n P = doubleAndAdd n P. Proof. induction n; auto; intros. - unfold doubleAndAdd; simpl. - rewrite Pos.of_nat_succ. - rewrite iter_op_spec by (auto using zeroIsIdentity). - case_eq (Pos.of_nat (S n)); intros. { - simpl; f_equal. - rewrite (IHn b) by (pose proof (size_of_succ n); omega). - unfold doubleAndAdd. - rewrite H0 in H. - rewrite <- Pos.of_nat_succ in H0. - rewrite <- (xI_is_succ n p) by apply H0. - rewrite Znat.positive_nat_N; simpl. - rewrite iter_op_spec; auto using zeroIsIdentity. - } { - simpl; f_equal. - rewrite (IHn b) by (pose proof (size_of_succ n); omega). - unfold doubleAndAdd. - rewrite <- (xO_is_succ n p) by (rewrite Pos.of_nat_succ; auto). - rewrite Znat.positive_nat_N; simpl. - rewrite <- Pos.succ_pred_double in H0. - rewrite H0 in H. - rewrite iter_op_spec by (auto using zeroIsIdentity; - pose proof (Pos.lt_succ_diag_r (Pos.pred_double p)); - apply Pos.size_nat_monotone in H1; omega; auto). - rewrite <- iter_op_double. - rewrite Pos.add_diag. - rewrite <- Pos.succ_pred_double. - rewrite Pos.iter_op_succ by apply twistedAddAssoc; auto. - } { - rewrite <- Pnat.Pos2Nat.inj_iff in H0. - rewrite Pnat.Nat2Pos.id in H0 by auto. - rewrite Pnat.Pos2Nat.inj_1 in H0. - assert (n = 0)%nat by omega; subst. - auto using zeroIsIdentity. - } + 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 || apply twistedAddAssoc || rewrite twistedAddComm; apply zeroIsIdentity). Qed. End EdwardsDoubleAndAdd.
\ No newline at end of file |