diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Algebra/Group.v | 18 | ||||
| -rw-r--r-- | src/Algebra/ScalarMult.v | 164 | ||||
| -rw-r--r-- | src/Arithmetic/ModularArithmeticTheorems.v | 74 | ||||
| -rw-r--r-- | src/Arithmetic/PrimeFieldTheorems.v | 6 | ||||
| -rw-r--r-- | src/Curves/Edwards/AffineProofs.v | 7 | ||||
| -rw-r--r-- | src/Primitives/EdDSARepChange.v | 85 | ||||
| -rw-r--r-- | src/Spec/EdDSA.v | 50 | ||||
| -rw-r--r-- | src/Util/AdditionChainExponentiation.v | 35 | ||||
| -rw-r--r-- | src/Util/IterAssocOp.v | 179 |
10 files changed, 215 insertions, 404 deletions
diff --git a/_CoqProject b/_CoqProject index d5fddbc2a..8e6b344c2 100644 --- a/_CoqProject +++ b/_CoqProject @@ -251,7 +251,6 @@ src/Util/HProp.v src/Util/IdfunWithAlt.v src/Util/IffT.v src/Util/Isomorphism.v -src/Util/IterAssocOp.v src/Util/LetIn.v src/Util/LetInMonad.v src/Util/ListUtil.v diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v index 01325de3f..76c53bcb1 100644 --- a/src/Algebra/Group.v +++ b/src/Algebra/Group.v @@ -1,5 +1,5 @@ Require Import Coq.Classes.Morphisms Crypto.Util.Relations (*Crypto.Util.Tactics*). -Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. +Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Monoid. Section BasicProperties. Context {T eq op id inv} `{@group T eq op id inv}. @@ -86,22 +86,6 @@ Section Homomorphism. apply inv_unique. rewrite <- Monoid.homomorphism, left_inverse, homomorphism_id; reflexivity. Qed. - - Section ScalarMultHomomorphism. - Context {MUL} {MUL_is_scalarmult:@ScalarMult.is_scalarmult G EQ OP ID MUL }. - Context {mul} {mul_is_scalarmult:@ScalarMult.is_scalarmult H eq op id mul }. - Lemma homomorphism_scalarmult n P : phi (MUL n P) = mul n (phi P). - Proof using Type*. eapply ScalarMult.homomorphism_scalarmult, homomorphism_id. Qed. - - Import ScalarMult. - Lemma opp_mul : forall n P, inv (mul n P) = mul n (inv P). - Proof using groupH mul_is_scalarmult. - induction n; intros. - { rewrite !scalarmult_0_l, inv_id; reflexivity. } - { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1. - rewrite scalarmult_add_l, scalarmult_1_l, inv_op, scalarmult_S_l, cancel_left; eauto. } - Qed. - End ScalarMultHomomorphism. End Homomorphism. Section GroupByIsomorphism. diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v index 99c1f6bbf..e81f81c2f 100644 --- a/src/Algebra/ScalarMult.v +++ b/src/Algebra/ScalarMult.v @@ -1,91 +1,167 @@ +Require Import Coq.ZArith.BinInt Coq.omega.Omega Crypto.Util.ZUtil.Peano. Require Import Coq.Classes.Morphisms. -Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Monoid. - -Module Import ModuloCoq8485. - Import NPeano Nat. - Infix "mod" := modulo. -End ModuloCoq8485. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Group. +Local Open Scope Z_scope. Section ScalarMultProperties. - Context {G eq add zero} `{monoidG:@monoid G eq add zero}. - Context {mul:nat->G->G}. + Context {G eq add zero opp} `{groupG:@group G eq add zero opp}. + Context {mul:Z->G->G}. Local Infix "=" := eq : type_scope. Local Infix "=" := eq. Local Infix "+" := add. Local Infix "*" := mul. Class is_scalarmult := { scalarmult_0_l : forall P, 0 * P = zero; - scalarmult_S_l : forall n P, S n * P = P + n * P; + scalarmult_succ_l_nn : forall n P, 0 <= n -> Z.succ n * P = P + n * P; + scalarmult_pred_l_np : forall n P, n <= 0 -> Z.pred n * P = opp P + n * P; scalarmult_Proper : Proper (Logic.eq==>eq==>eq) mul }. Global Existing Instance scalarmult_Proper. Context `{mul_is_scalarmult:is_scalarmult}. - Fixpoint scalarmult_ref (n:nat) (P:G) {struct n} := - match n with - | O => zero - | S n' => add P (scalarmult_ref n' P) - end. + Lemma scalarmult_succ_l n P : Z.succ n * P = P + n * P. + Proof. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + repeat (rewrite ?scalarmult_0_l, ?scalarmult_succ_l_nn, ?scalarmult_pred_l_np, ?left_identity, ?right_identity, ?Z.succ_pred, ?Z.pred_succ, ?associative, ?right_inverse, ?left_inverse by omega); reflexivity. + Qed. + + Lemma scalarmult_pred_l n P : Z.pred n * P = opp P + n * P. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + repeat (rewrite ?scalarmult_0_l, ?scalarmult_succ_l_nn, ?scalarmult_pred_l_np, ?left_identity, ?right_identity, ?Z.succ_pred, ?Z.pred_succ, ?associative, ?right_inverse, ?left_inverse by omega); reflexivity. + Qed. + + Definition scalarmult_ref (n:Z) (P:G) : G := + Z.peano_rect + (fun _ => G) + (zero) + (fun _ => add P) + (fun _ => add (opp P)) + n + . Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref. - Proof using monoidG. - repeat intro; subst. - match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end. - repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity. + Proof using groupG. + intros n n' H; subst n'; + induction n using Z.peano_rect_strong; + cbv [Proper respectful] in *; + intros; + cbv [scalarmult_ref] in *; break_match; try reflexivity; + rewrite ?Z.peano_rect_succ, ?Z.peano_rect_pred in * by omega; + rewrite IHn by eassumption; + match goal with H : _ = _ |- _ => rewrite H; reflexivity end. + Qed. + + Lemma scalarmult_ext n P : mul n P = scalarmult_ref n P. + Proof using Type*. + revert P. + destruct mul_is_scalarmult. + induction n using Z.peano_rect_strong; intros; + cbv [scalarmult_ref] in *; break_match; + rewrite ?Z.peano_rect_succ, ?Z.peano_rect_pred, ?Z.succ'_succ, ?Z.pred'_pred in *; + try rewrite <-IHn; try match goal with [H:_|-_] => eapply H end; omega. + Qed. + + Lemma scalarmult_1_l P : 1*P = P. + Proof using Type*. + intros. change 1 with (Z.succ 0). + rewrite scalarmult_succ_l, scalarmult_0_l, right_identity; reflexivity. + Qed. + + Lemma scalarmult_opp1_l P : -1*P = opp P. + change (-1) with (Z.pred 0). + rewrite scalarmult_pred_l, scalarmult_0_l, right_identity; reflexivity. + Qed. + + Lemma scalarmult_add_l (n m:Z) (P:G) : ((n + m)%Z * P = n * P + m * P). + Proof using Type*. + revert P. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + rewrite ?Z.add_0_l, ?Z.add_succ_l, ?Z.add_pred_l; + rewrite ?scalarmult_0_l, ?scalarmult_succ_l, ?scalarmult_pred_l, ?left_identity, <-?associative, <-?IHn; try reflexivity. Qed. - Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P. + Lemma scalarmult_opp_l (n:Z) (P:G) : (-n) * P = opp (n*P). Proof using Type*. - induction n as [|n IHn]; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l). + revert P. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega. + { change (-0) with (0). rewrite !scalarmult_0_l, inv_id; reflexivity. } + { rewrite scalarmult_succ_l_nn, inv_op, <-IHn by omega. + replace (-Z.succ n) with (-n + (- 1))%Z by auto with zarith. + rewrite scalarmult_add_l, scalarmult_opp1_l; reflexivity. } + { rewrite scalarmult_pred_l_np, inv_op, <-IHn, inv_inv by omega. + replace (- Z.pred n) with (-n+1)%Z by auto with zarith. + rewrite scalarmult_add_l, scalarmult_1_l; reflexivity. } Qed. - Lemma scalarmult_1_l : forall P, 1*P = P. - Proof using Type*. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed. + Lemma scalarmult_zero_r (n:Z) : n * zero = zero. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + rewrite ?scalarmult_0_l, ?scalarmult_succ_l_nn, ?scalarmult_pred_l_np, ?IHn, ?inv_id, ?left_identity by omega; + try reflexivity. + Qed. - Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P). + Lemma scalarmult_assoc (n m : Z) P : n * (m * P) = (m * n)%Z * P. Proof using Type*. - induction n as [|n IHn]; intros; - rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity. + revert P. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega. + { rewrite Z.mul_0_r, 2scalarmult_0_l by omega; reflexivity. } + { rewrite scalarmult_succ_l, IHn by omega. + rewrite (Z.mul_comm m (Z.succ n)), Z.mul_succ_l, (Z.mul_comm n m), (Z.add_comm (m*n) m). + rewrite scalarmult_add_l. reflexivity. } + { rewrite scalarmult_pred_l, IHn by omega. + rewrite (Z.mul_comm m (Z.pred n)), Z.mul_pred_l, (Z.mul_comm n m), <-Z.add_opp_l. + rewrite scalarmult_add_l, scalarmult_opp_l. reflexivity. } Qed. - Lemma scalarmult_zero_r : forall m, m * zero = zero. - Proof using Type*. induction m as [|? IHm]; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed. + Lemma scalarmult_sub_l (a b:Z) (P:G) : (a - b)*P = a*P + opp(b*P). + Proof using Type*. + rewrite <-Z.add_opp_r, scalarmult_add_l, scalarmult_opp_l; reflexivity. + Qed. - Lemma scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P. + Lemma scalarmult_opp_r (n:Z) (P:G) : n*opp P = opp (n * P). Proof using Type*. - induction n as [|n IHn]; intros. - { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. } - { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. - rewrite IHn. reflexivity. } + revert P. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + rewrite <-?Z.add_1_l, <-?Z.sub_1_r; + [|rewrite Z.add_comm at 1|rewrite <-Z.add_opp_l; rewrite Z.add_comm at 1]; + repeat (rewrite ?scalarmult_0_l, ?scalarmult_opp_l, ?scalarmult_add_l, ?inv_id, ?inv_op, ?inv_inv, ?IHn, ?scalarmult_1_l); + reflexivity. Qed. Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero. Proof using Type*. intros ? ? Hl ?. rewrite <-scalarmult_assoc, Hl, scalarmult_zero_r. reflexivity. Qed. - Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B. + Lemma scalarmult_mod_order : forall l B, l <> 0 -> l*B = zero -> forall n, n mod l * B = n * B. Proof using Type*. intros l B Hnz Hmod n. - rewrite (NPeano.Nat.div_mod n l Hnz) at 2. + rewrite (Z.div_mod n l Hnz) at 2. rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity. Qed. + End ScalarMultProperties. Section ScalarMultHomomorphism. - Context {G EQ ADD ZERO} {monoidG:@monoid G EQ ADD ZERO}. - Context {H eq add zero} {monoidH:@monoid H eq add zero}. + Context {G EQ ADD ZERO OPP} {groupG:@group G EQ ADD ZERO OPP}. + Context {H eq add zero opp} {groupH:@group H eq add zero opp}. Local Infix "=" := eq : type_scope. Local Infix "=" := eq : eq_scope. - Context {MUL} {MUL_is_scalarmult:@is_scalarmult G EQ ADD ZERO MUL }. - Context {mul} {mul_is_scalarmult:@is_scalarmult H eq add zero mul }. + Context {MUL} {MUL_is_scalarmult:@is_scalarmult G EQ ADD ZERO OPP MUL}. + Context {mul} {mul_is_scalarmult:@is_scalarmult H eq add zero opp mul}. Context {phi} {homom:@Monoid.is_homomorphism G EQ ADD H eq add phi}. - Context (phi_ZERO:phi ZERO = zero). Lemma homomorphism_scalarmult : forall n P, phi (MUL n P) = mul n (phi P). Proof using Type*. - setoid_rewrite scalarmult_ext. - induction n as [|n IHn]; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + rewrite ?scalarmult_0_l, ?scalarmult_succ_l, ?scalarmult_pred_l by omega. + { apply homomorphism_id. } + { rewrite <-IHn. rewrite Monoid.homomorphism. reflexivity. } + { rewrite <-IHn. rewrite Monoid.homomorphism, Group.homomorphism_inv. reflexivity. } Qed. End ScalarMultHomomorphism. -Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero} - : @is_scalarmult G eq add zero (@scalarmult_ref G add zero). -Proof. split; try exact _; intros; reflexivity. Qed. +Global Instance scalarmult_ref_is_scalarmult {G eq add zero opp} {groupG:@group G eq add zero opp} + : @is_scalarmult G eq add zero opp (@scalarmult_ref G add zero opp). +Proof. + split; try exact _; cbv [scalarmult_ref] in *; intros; + rewrite <-?Z.succ'_succ, <-?Z.pred'_pred, ?Z.peano_rect_succ, ?Z.peano_rect_pred in * by omega; + reflexivity. +Qed.
\ No newline at end of file diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v index 77186674f..88f25ec60 100644 --- a/src/Arithmetic/ModularArithmeticTheorems.v +++ b/src/Arithmetic/ModularArithmeticTheorems.v @@ -6,7 +6,7 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArit Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac. -Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring Crypto.Algebra.Field. +Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.ScalarMult Crypto.Algebra.Ring Crypto.Algebra.Field. Require Import Crypto.Util.Decidable Crypto.Util.ZUtil. Require Export Crypto.Util.FixCoqMistakes. @@ -184,7 +184,6 @@ Module F. Lemma to_nat_mod (x:F m) (Hm:(0 < m)%Z) : F.to_nat x mod (Z.to_nat m) = F.to_nat x. Proof using Type. - unfold F.to_nat. rewrite <-F.mod_to_Z at 2. apply Z.mod_to_nat; [assumption|]. @@ -287,17 +286,6 @@ Module F. power_tac (power_theory m) [is_pow_constant]). Local Open Scope F_scope. - Import Algebra.ScalarMult. - Global Instance pow_is_scalarmult - : is_scalarmult (G:=F m) (eq:=eq) (add:=F.mul) (zero:=1%F) (mul := fun n x => x ^ (N.of_nat n)). - Proof using Type. - split; [ intro P | intros n P | ]; rewrite ?Nat2N.inj_succ, <-?N.add_1_l; - match goal with - | [x:F m |- _ ] => solve [destruct (@pow_spec m P); auto] - | |- Proper _ _ => solve_proper - end. - Qed. - (* TODO: move this somewhere? *) Create HintDb nat2N discriminated. Hint Rewrite Nat2N.inj_iff @@ -311,36 +299,60 @@ Module F. Nat2N.inj_div2 Nat2N.inj_max Nat2N.inj_min Nat2N.id : nat2N. - Ltac pow_to_scalarmult_ref := - repeat (autorewrite with nat2N; - match goal with - | |- context [ (_^?n)%F ] => - rewrite <-(N2Nat.id n); generalize (N.to_nat n); clear n; - intro n - | |- context [ (_^N.of_nat ?n)%F ] => - let rw := constr:(scalarmult_ext(zero:=F.of_Z m 1) n) in - setoid_rewrite rw (* rewriting moduloa reduction *) - end). - Lemma pow_0_r (x:F m) : x^0 = 1. - Proof using Type. pow_to_scalarmult_ref. apply scalarmult_0_l. Qed. + Proof using Type. destruct (F.pow_spec x); auto. Qed. + + Lemma pow_succ_r (x:F m) n : x^(N.succ n) = x * x^n. + Proof using Type. + rewrite <-N.add_1_l; + destruct (F.pow_spec x); auto. + Qed. Lemma pow_add_r (x:F m) (a b:N) : x^(a+b) = x^a * x^b. - Proof using Type. pow_to_scalarmult_ref; apply scalarmult_add_l. Qed. + Proof using Type. + destruct (F.pow_spec x) as [A B]. + induction a as [|a IHa] using N.peano_ind; + rewrite ?N.add_succ_l, ?pow_0_r, ?pow_succ_r, ?N.add_0_l, ?IHa; try ring. + Qed. Lemma pow_0_l (n:N) : n <> 0%N -> 0^n = 0 :> F m. - Proof using Type. pow_to_scalarmult_ref; destruct n; simpl; intros; [congruence|ring]. Qed. + Proof using Type. + induction n as [|a IHa] using N.peano_ind; [contradiction|]. + rewrite <-N.add_1_l, pow_add_r; intros; ring. + Qed. + + Lemma pow_1_l (n:N) : 1^n = 1 :> F m. + Proof using Type. + induction n as [|n IHn] using N.peano_ind; + rewrite ?pow_0_r, ?pow_succ_r, ?pow_add_r, ?pow_1_l, ?IHn; ring. + Qed. + + Lemma pow_mul_l (x y:F m) (n:N) : (x*y)^n = x^n * y^n. + Proof using Type. + induction n as [|n IHn] using N.peano_ind; + repeat (rewrite ?pow_0_r, ?pow_succ_r, ?pow_1_l, <-?N.add_1_l, ?N.mul_add_distr_r, ?pow_add_r, ?N.mul_1_l, ?IHn); try ring. + Qed. Lemma pow_pow_l (x:F m) (a b:N) : (x^a)^b = x^(a*b). - Proof using Type. pow_to_scalarmult_ref. apply scalarmult_assoc. Qed. + Proof using Type. + induction a as [|a IHa] using N.peano_ind; + repeat (rewrite ?pow_0_r, ?pow_succ_r, ?pow_1_l, <-?N.add_1_l, ?N.mul_add_distr_r, ?pow_add_r, ?N.mul_1_l, ?pow_mul_l, ?IHa); + try ring. + Qed. Lemma pow_1_r (x:F m) : x^1 = x. - Proof using Type. pow_to_scalarmult_ref; simpl; ring. Qed. + Proof using Type. + change 1%N with (N.succ 0); repeat rewrite ?pow_succ_r, ?pow_0_r; ring. + Qed. Lemma pow_2_r (x:F m) : x^2 = x*x. - Proof using Type. pow_to_scalarmult_ref; simpl; ring. Qed. + Proof using Type. + change 1%N with (N.succ (N.succ 0)); repeat rewrite ?pow_succ_r, ?pow_0_r; ring. + Qed. Lemma pow_3_r (x:F m) : x^3 = x*x*x. - Proof using Type. pow_to_scalarmult_ref; simpl; ring. Qed. + Proof using Type. + change 1%N with (N.succ (N.succ (N.succ 0))); repeat rewrite ?pow_succ_r, ?pow_0_r; ring. + Qed. End Pow. End F. diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v index 3d6260bba..2184d20c6 100644 --- a/src/Arithmetic/PrimeFieldTheorems.v +++ b/src/Arithmetic/PrimeFieldTheorems.v @@ -251,9 +251,8 @@ Module F. {phi'_opp : forall a : H, Logic.eq (phi' (opp a)) (F.opp (phi' a))} {phi'_add : forall a b : H, Logic.eq (phi' (add a b)) (F.add (phi' a) (phi' b))} {phi'_sub : forall a b : H, Logic.eq (phi' (sub a b)) (F.sub (phi' a) (phi' b))} - {phi'_mul : forall a b : H, Logic.eq (phi' (mul a b)) (F.mul (phi' a) (phi' b))} - {P:Type} {pow : H -> P -> H} {NtoP:N->P} - {pow_is_scalarmult:ScalarMult.is_scalarmult(G:=H)(eq:=eq)(add:=mul)(zero:=one)(mul:=fun (n:nat) (k:H) => pow k (NtoP (N.of_nat n)))}. + {phi'_mul : forall a b : H, Logic.eq (phi' (mul a b)) (F.mul (phi' a) (phi' b))}. + (* TODO: revive this once we figure out how to spec the pow impl Definition inv (x:H) := pow x (NtoP (Z.to_N (q - 2)%Z)). Definition div x y := mul (inv y) x. @@ -289,6 +288,7 @@ Module F. /\ @Ring.is_homomorphism H eq one add mul (F q) Logic.eq F.one F.add F.mul phi'. Proof using Type*. eapply @Field.field_and_homomorphism_from_redundant_representation; assumption || exact _ || exact inv_proof || exact div_proof. Qed. + *) End IsomorphicRings. End Iso. End F. diff --git a/src/Curves/Edwards/AffineProofs.v b/src/Curves/Edwards/AffineProofs.v index 8e69b78fe..ec67c25b2 100644 --- a/src/Curves/Edwards/AffineProofs.v +++ b/src/Curves/Edwards/AffineProofs.v @@ -1,6 +1,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Algebra.Hierarchy Crypto.Util.Decidable. +Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.ScalarMult Crypto.Util.Decidable. Require Import Coq.Logic.Eqdep_dec. Require Import Coq.Classes.Morphisms. Require Import Coq.Relations.Relation_Definitions. @@ -12,7 +12,7 @@ Require Import Crypto.Util.Tactics.SetoidSubst. Require Export Crypto.Util.FixCoqMistakes. Module E. - Import Group ScalarMult Ring Field CompleteEdwardsCurve.E. + Import Group Ring Field CompleteEdwardsCurve.E. Notation onCurve_zero := Pre.onCurve_zero. Notation denominator_nonzero := Pre.denominator_nonzero. @@ -91,9 +91,6 @@ Module E. induction n; (reflexivity || eapply (_:Proper (eq==>eq==>eq) add); eauto). Qed. - Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul. - Proof using Type. split; intros; (reflexivity || exact _). Qed. - Section PointCompression. Local Notation "x ^ 2" := (x*x). diff --git a/src/Primitives/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v index 1c6282fb9..041220310 100644 --- a/src/Primitives/EdDSARepChange.v +++ b/src/Primitives/EdDSARepChange.v @@ -17,9 +17,9 @@ Import Notations. Section EdDSA. Context `{prm:EdDSA}. - Local Infix "==" := Eeq. Local Infix "+" := Eadd. Local Infix "*" := EscalarMult. + Local Infix "==" := Eeq. Local Infix "+" := Eadd. Local Infix "*" := ZEmul. - Local Notation valid := (@valid E Eeq Eadd EscalarMult b H l B Eenc Senc). + Local Notation valid := (@valid E Eeq Eadd ZEmul b H l B Eenc Senc). Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M). Proof using Type. cbv [sign public Spec.EdDSA.valid]; intros; subst; @@ -28,7 +28,7 @@ Section EdDSA. | |- _ /\ _ => eapply conj | |- _ => reflexivity end. - rewrite F.to_nat_of_nat, scalarmult_mod_order, scalarmult_add_l, cancel_left, scalarmult_mod_order, NPeano.Nat.mul_comm, scalarmult_assoc; + rewrite F.to_Z_of_Z, scalarmult_mod_order, scalarmult_add_l, cancel_left, scalarmult_mod_order, Z.mul_comm, scalarmult_assoc; try solve [ reflexivity | setoid_rewrite (*unify 0*) (Z2Nat.inj_iff _ 0); pose proof EdDSA_l_odd; omega | pose proof EdDSA_l_odd; omega @@ -43,7 +43,7 @@ Section EdDSA. set_evars. setoid_rewrite <-(symmetry_iff(R:=Eeq)) at 1. setoid_rewrite <-eq_r_opp_r_inv. - setoid_rewrite opp_mul. + setoid_rewrite <-scalarmult_opp_r. subst_evars. reflexivity. Defined. @@ -66,11 +66,11 @@ Section EdDSA. setoid_rewrite combine_eq_iff. setoid_rewrite and_comm at 4. setoid_rewrite and_assoc. repeat setoid_rewrite exists_and_indep_l. setoid_rewrite (and_rewrite_l Eenc (split1 b b sig) - (fun x y => x == _ * B + wordToNat (H _ (y ++ Eenc _ ++ message)) mod _ * Eopp _)); setoid_rewrite eq_enc_S_iff. + (fun x y => x == _ * B + Z.of_nat (wordToNat (H _ (y ++ Eenc _ ++ message))) mod _ * Eopp _)); setoid_rewrite eq_enc_S_iff. setoid_rewrite (@exists_and_equiv_r _ _ _ _ _ _). setoid_rewrite <- (fun A => and_rewriteleft_l (fun x => x) (Eenc A) (fun pk EencA => exists a, Sdec (split2 b b sig) = Some a /\ - Eenc (_ * B + wordToNat (H (b + (b + mlen)) (split1 b b sig ++ EencA ++ message)) mod _ * Eopp A) + Eenc (_ * B + Z.of_nat (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ EencA ++ message))) mod _ * Eopp A) = split1 b b sig)). setoid_rewrite (eq_enc_E_iff pk). setoid_rewrite <-weqb_true_iff. setoid_rewrite <-option_rect_false_returns_true_iff_eq. @@ -78,22 +78,7 @@ Section EdDSA. (intros ? ? Hxy; unfold option_rect; break_match; rewrite <-?Hxy; reflexivity). subst_evars. - (* TODO: generalize this higher order reflexivity *) - match goal with - |- ?f ?mlen ?msg ?pk ?sig = true <-> ?term = true - => let term := eval pattern sig in term in - let term := eval pattern pk in term in - let term := eval pattern msg in term in - let term := match term with - (fun msg => (fun pk => (fun sig => @?body msg pk sig) sig) pk) msg => - body - end in - let term := eval pattern mlen in term in - let term := match term with - (fun mlen => @?body mlen) mlen => body - end in - unify f term; reflexivity - end. + eapply reflexivity. Defined. Definition verify' {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool := Eval cbv [proj1_sig verify'_sig] in proj1_sig verify'_sig mlen message pk sig. @@ -114,10 +99,10 @@ Section EdDSA. Context {SRep SRepEq} `{@Equivalence SRep SRepEq} {S2Rep:F l->SRep}. - Context {SRepDecModL} {SRepDecModL_correct: forall (w:word (b+b)), SRepEq (S2Rep (F.of_nat _ (wordToNat w))) (SRepDecModL w)}. + Context {SRepDecModL} {SRepDecModL_correct: forall (w:word (b+b)), SRepEq (S2Rep (F.of_Z _ (Z.of_nat (wordToNat w)))) (SRepDecModL w)}. Context {SRepERepMul:SRep->Erep->Erep} - {SRepERepMul_correct:forall n P, ErepEq (EToRep ((n mod Z.to_nat l)*P)) (SRepERepMul (S2Rep (F.of_nat _ n)) (EToRep P))} + {SRepERepMul_correct:forall n P, ErepEq (EToRep ((n mod l)*P)) (SRepERepMul (S2Rep (F.of_Z _ n)) (EToRep P))} {Proper_SRepERepMul: Proper (SRepEq==>ErepEq==>ErepEq) SRepERepMul}. Context {SRepDec: word b -> option SRep} @@ -134,7 +119,7 @@ Section EdDSA. etransitivity. Focus 2. { eapply Proper_option_rect_nd_changebody; [intro|reflexivity]. eapply Proper_option_rect_nd_changebody; [intro|reflexivity]. - rewrite <-F.to_nat_mod by omega. + rewrite <-F.mod_to_Z by omega. repeat ( rewrite ERepEnc_correct || rewrite homomorphism @@ -143,8 +128,8 @@ Section EdDSA. || rewrite SRepERepMul_correct || rewrite SdecS_correct || rewrite SRepDecModL_correct - || rewrite (@F.of_nat_to_nat _ _) - || rewrite (@F.of_nat_mod _ _) + || rewrite (@F.of_Z_to_Z _ _) + || rewrite (@F.mod_to_Z _ _) ). reflexivity. } Unfocus. @@ -233,32 +218,11 @@ Section EdDSA. Let n_le_bpb : (n <= b+b)%nat. destruct prm. omega. Qed. - Definition splitSecretPrngCurve (sk:word b) : SRep * word b := - dlet hsk := H _ sk in - dlet curveKey := SRepDecModLShort (clearlow c (@wfirstn n _ hsk n_le_bpb) ++ wones 1) in - dlet prngKey := split2 b b hsk in - (curveKey, prngKey). - - Lemma splitSecretPrngCurve_correct sk : + (* TODO: change impl to basesystem *) + Context (splitSecretPrngCurve : forall (sk:word b), SRep * word b). + Context (splitSecretPrngCurve_correct : forall sk, let (s, r) := splitSecretPrngCurve sk in - SRepEq s (S2Rep (F.of_nat l (curveKey sk))) /\ r = prngKey (H:=H) sk. - Proof using H0 SRepDecModLShort_correct. - cbv [splitSecretPrngCurve EdDSA.curveKey EdDSA.prngKey Let_In]; split; - repeat ( - reflexivity - || rewrite <-SRepDecModLShort_correct - || rewrite wordToNat_split1 - || rewrite wordToNat_wfirstn - || rewrite wordToNat_combine - || rewrite wordToNat_clearlow - || rewrite (eq_refl:wordToNat (wones 1) = 1) - || rewrite mult_1_r - || rewrite setbit_high by - ( pose proof (Nat.pow_nonzero 2 n); specialize_by discriminate; - set (x := wordToNat (H b sk)); - assert (x mod 2 ^ n < 2^n)%nat by (apply Nat.mod_bound_pos; omega); omega) - ). - Qed. + SRepEq s (S2Rep (F.of_Z l (curveKey sk))) /\ r = prngKey (H:=H) sk). Definition sign (pk sk : word b) {mlen} (msg:word mlen) := dlet sp := splitSecretPrngCurve sk in @@ -267,18 +231,13 @@ Section EdDSA. dlet r := SRepDecModL (H _ (p ++ msg)) in dlet R := SRepERepMul r ErepB in dlet S := SRepAdd r (SRepMul (SRepDecModL (H _ (ERepEnc R ++ pk ++ msg))) s) in - ERepEnc R ++ SRepEnc S. - - Lemma to_nat_l_nonzero : Z.to_nat l <> 0. - Proof using n_le_bpb. + ERepEnc R ++ SRepEnc S. - intro Hx; change 0 with (Z.to_nat 0) in Hx. - destruct prm; rewrite Z2Nat.inj_iff in Hx; omega. - Qed. + Lemma Z_l_nonzero : Z.pos l <> 0%Z. discriminate. Qed. Lemma sign_correct (pk sk : word b) {mlen} (msg:word mlen) : sign pk sk msg = EdDSA.sign pk sk msg. - Proof using Agroup Ahomom ERepEnc_correct ErepB_correct H0 Proper_ERepEnc Proper_SRepAdd Proper_SRepERepMul Proper_SRepEnc Proper_SRepMul SRepAdd_correct SRepDecModLShort_correct SRepDecModL_correct SRepERepMul_correct SRepEnc_correct SRepMul_correct. + Proof using Agroup Ahomom ERepEnc_correct ErepB_correct H0 Proper_ERepEnc Proper_SRepAdd Proper_SRepERepMul Proper_SRepEnc Proper_SRepMul SRepAdd_correct SRepDecModLShort_correct SRepDecModL_correct SRepERepMul_correct SRepEnc_correct SRepMul_correct splitSecretPrngCurve_correct. cbv [sign EdDSA.sign Let_In]. let H := fresh "H" in @@ -292,8 +251,8 @@ Section EdDSA. || rewrite SRepEnc_correct || rewrite SRepDecModL_correct || rewrite SRepERepMul_correct - || rewrite (F.of_nat_add (m:=l)) - || rewrite (F.of_nat_mul (m:=l)) + || rewrite (F.of_Z_add (m:=l)) + || rewrite (F.of_Z_mul (m:=l)) || rewrite SRepAdd_correct || rewrite SRepMul_correct || rewrite ErepB_correct @@ -301,7 +260,7 @@ Section EdDSA. || rewrite <-curveKey_correct || eapply (f_equal2 (fun a b => a ++ b)) || f_equiv - || rewrite <-(@scalarmult_mod_order _ _ _ _ _ _ _ _ B to_nat_l_nonzero EdDSA_l_order_B) + || rewrite <-(scalarmult_mod_order l B Z_l_nonzero EdDSA_l_order_B), SRepERepMul_correct ). Qed. End ChangeRep. diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 82a9ba6cc..db350e4e0 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -1,33 +1,19 @@ Require Bedrock.Word Crypto.Util.WordUtil. +Require Crypto.Algebra.Hierarchy Algebra.ScalarMult. Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt. Require Coq.Numbers.Natural.Peano.NPeano. -Require Crypto.Algebra.ScalarMult. - -Require Import Omega. (* TODO: remove this import when we drop 8.4 *) Require Import Crypto.Spec.ModularArithmetic. -(** In Coq 8.4, we have [NPeano.pow] and [NPeano.modulo]. In Coq 8.5, - they are [Nat.pow] and [Nat.modulo]. To allow this file to work - with both versions, we create a module where we (locally) import - both [NPeano] and [Nat], and define the notations with unqualified - names. By importing the module, we get access to the notations - without importing [NPeano] and [Nat] in the top-level of this - file. *) - -Module Import Notations. - Import NPeano Nat. - - Infix "^" := pow. - Infix "mod" := modulo (at level 40, no associativity). - Infix "++" := Word.combine. - Notation setbit := setbit. -End Notations. +Local Infix "-" := BinInt.Z.sub. +Local Infix "^" := BinInt.Z.pow. +Local Infix "mod" := BinInt.Z.modulo. +Local Infix "++" := Word.combine. +Local Notation setbit := BinInt.Z.setbit. -Generalizable All Variables. Section EdDSA. Class EdDSA (* <https://eprint.iacr.org/2015/677.pdf> *) - {E Eeq Eadd Ezero Eopp} {EscalarMult} (* the underllying elliptic curve operations *) + {E Eeq Eadd Ezero Eopp} {ZEmul} (* the underllying elliptic curve operations *) {b : nat} (* public keys are k bits, signatures are 2*k bits *) {H : forall {n}, Word.word n -> Word.word (b + b)} (* main hash function *) @@ -42,7 +28,7 @@ Section EdDSA. := { EdDSA_group:@Algebra.Hierarchy.group E Eeq Eadd Ezero Eopp; - EdDSA_scalarmult:@Algebra.ScalarMult.is_scalarmult E Eeq Eadd Ezero EscalarMult; + EdDSA_scalarmult:@Algebra.ScalarMult.is_scalarmult E Eeq Eadd Ezero Eopp ZEmul; EdDSA_c_valid : c = 2 \/ c = 3; @@ -53,7 +39,7 @@ Section EdDSA. EdDSA_l_prime : Znumtheory.prime l; EdDSA_l_odd : BinInt.Z.lt 2 l; - EdDSA_l_order_B : Eeq (EscalarMult (BinInt.Z.to_nat l) B) Ezero + EdDSA_l_order_B : Eeq (ZEmul l B) Ezero }. Global Existing Instance EdDSA_group. Global Existing Instance EdDSA_scalarmult. @@ -61,7 +47,7 @@ Section EdDSA. Context `{prm:EdDSA}. Local Coercion Word.wordToNat : Word.word >-> nat. - Local Coercion BinInt.Z.to_nat : BinInt.Z >-> nat. + Local Coercion BinInt.Z.of_nat : nat >-> BinInt.Z. Local Notation secretkey := (Word.word b) (only parsing). Local Notation publickey := (Word.word b) (only parsing). Local Notation signature := (Word.word (b + b)) (only parsing). @@ -69,27 +55,27 @@ Section EdDSA. Local Arguments H {n} _. Local Notation wfirstn n w := (@WordUtil.wfirstn n _ w _) (only parsing). - Local Obligation Tactic := destruct prm; simpl; intros; omega. + Local Obligation Tactic := destruct prm; simpl; intros; Omega.omega. - Program Definition curveKey (sk:secretkey) : nat := + Program Definition curveKey (sk:secretkey) : BinInt.Z := 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) *) setbit x n. (* and the high bit is always set *) Local Infix "+" := Eadd. - Local Infix "*" := EscalarMult. + Local Infix "*" := ZEmul. Definition prngKey (sk:secretkey) : Word.word b := Word.split2 b b (H sk). Definition public (sk:secretkey) : publickey := Eenc (curveKey sk*B). Program Definition sign (A_:publickey) sk {n} (M : Word.word n) := - let r : nat := H (prngKey sk ++ M) in (* secret nonce *) - let R : E := r * B in (* commitment to nonce *) - let s : nat := curveKey sk in (* secret scalar *) - let S : F l := F.nat_mod l (r + H (Eenc R ++ A_ ++ M) * s) in + let r := H (prngKey sk ++ M) in (* secret nonce *) + let R := r * B in (* commitment to nonce *) + let s := curveKey sk in (* secret scalar *) + let S := F.of_Z l (r + H (Eenc R ++ A_ ++ M) * s) in Eenc R ++ Senc S. Definition valid {n} (message : Word.word n) pubkey signature := exists A S R, Eenc A = pubkey /\ Eenc R ++ Senc S = signature /\ - Eeq (F.to_nat S * B) (R + (H (Eenc R ++ Eenc A ++ message) mod l) * A). + Eeq (F.to_Z S * B) (R + (H (Eenc R ++ Eenc A ++ message) mod l) * A). End EdDSA. diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index f35c4e9ea..8de191eda 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -6,6 +6,12 @@ Require Import Crypto.Util.Option. Require Import Crypto.Util.Tactics.BreakMatch. Section AddChainExp. + (* TODO: rewrite this. + - use CPS and Loop + - use an inner loop for repeated squaring + - connect to something that abstracts over F.pow, Z.pow, N.pow NOT scalarmult + *) + Function fold_chain {T} (id:T) (op:T->T->T) (is:list (nat*nat)) (acc:list T) {struct is} : T := match is with | nil => @@ -27,33 +33,4 @@ Section AddChainExp. (0, 2); (* 30 = 24 + 6 *) (0, 6)] (* 31 = 30 + 1 *) [1] = 31. reflexivity. Qed. - - Context {G eq op id} {monoid:@Algebra.Hierarchy.monoid G eq op id}. - Context {scalarmult} {is_scalarmult:@ScalarMult.is_scalarmult G eq op id scalarmult}. - Local Infix "=" := eq : type_scope. - Local Open Scope N_scope. - Local Notation "n * P" := (scalarmult (N.to_nat n) P) (only parsing). - - Lemma fold_chain_exp' : forall (x:G) is acc ref - (H:forall i, nth_default id acc i = (nth_default 0 ref i) * x) - (Hl:Logic.eq (length acc) (length ref)), - fold_chain id op is acc = (fold_chain 0 N.add is ref) * x. - Proof using Type*. - intro x; induction is; intros acc ref H Hl; simpl @fold_chain. - { repeat break_match; specialize (H 0%nat); rewrite ?nth_default_cons, ?nth_default_cons_S in H; - solve [ simpl length in *; discriminate | apply H | rewrite scalarmult_0_l; reflexivity ]. } - { repeat break_match. eapply IHis; intros; [|auto with distr_length]; []. - match goal with - [H:context [nth_default _ ?l _] |- context[nth_default _ (?h::?l) ?i] ] - => destruct i; rewrite ?nth_default_cons, ?nth_default_cons_S; - solve [ apply H | rewrite !H, <-scalarmult_add_l, Nnat.N2Nat.inj_add; reflexivity ] - end. } - Qed. - - Lemma fold_chain_exp x is: fold_chain id op is [x] = (fold_chain 0 N.add is [1]) * x. - Proof using Type*. - eapply fold_chain_exp'; trivial; intros i. - destruct i as [|i]; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil; - rewrite ?scalarmult_1_l, ?scalarmult_0_l; reflexivity. - Qed. End AddChainExp. diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v deleted file mode 100644 index 4d9365e4d..000000000 --- a/src/Util/IterAssocOp.v +++ /dev/null @@ -1,179 +0,0 @@ -Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. -Require Import Coq.NArith.NArith Coq.PArith.BinPosDef. -Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. -Require Import Crypto.Util.NUtil. -Require Import Crypto.Util.Tactics.BreakMatch. - -Local Open Scope equiv_scope. - -Generalizable All Variables. -Section IterAssocOp. - Context {T eq op id} {moinoid : @Algebra.Hierarchy.monoid T eq op id} (testbit : nat -> bool). - Local Infix "===" := eq. Local Infix "===" := eq : type_scope. - - Local Notation nat_iter_op := (ScalarMult.scalarmult_ref (add:=op) (zero:=id)). - - Lemma nat_iter_op_plus m n a : - op (nat_iter_op m a) (nat_iter_op n a) === nat_iter_op (m + n) a. - Proof using Type*. symmetry; eapply ScalarMult.scalarmult_add_l. Qed. - - Definition N_iter_op n a := - match n with - | 0%N => id - | Npos p => Pos.iter_op op p a - end. - - Lemma Pos_iter_op_succ : forall p a, Pos.iter_op op (Pos.succ p) a === op a (Pos.iter_op op p a). - Proof using Type*. - induction p as [p IHp|p IHp|]; intros; simpl; rewrite ?Algebra.Hierarchy.associative, ?IHp; reflexivity. - Qed. - - Lemma N_iter_op_succ : forall n a, N_iter_op (N.succ n) a === op a (N_iter_op n a). - Proof using Type*. - destruct n; simpl; intros; rewrite ?Pos_iter_op_succ, ?Algebra.Hierarchy.right_identity; reflexivity. - Qed. - - Lemma N_iter_op_is_nat_iter_op : forall n a, N_iter_op n a === nat_iter_op (N.to_nat n) a. - Proof using Type*. - induction n as [|n IHn] using N.peano_ind; intros; rewrite ?N2Nat.inj_succ, ?N_iter_op_succ, ?IHn; reflexivity. - Qed. - - Context {sel:bool->T->T->T} {sel_correct:forall b x y, sel b x y = if b then y else x}. - - Fixpoint funexp {A} (f : A -> A) (a : A) (exp : nat) : A := - match exp with - | O => a - | S exp' => f (funexp f a exp') - end. - - Definition test_and_op a (state : nat * T) := - let '(i, acc) := state in - let acc2 := op acc acc in - let acc2a := op a acc2 in - match i with - | O => (0, acc) - | S i' => (i', sel (testbit i') acc2 acc2a) - end. - - Definition iter_op bound a : T := - snd (funexp (test_and_op a) (bound, id) bound). - - (* correctness reference *) - Context {x:N} {testbit_correct : forall i, testbit i = N.testbit_nat x i}. - - Definition test_and_op_inv a (s : nat * T) := - snd s === nat_iter_op (N.to_nat (N.shiftr_nat x (fst s))) a. - - Lemma test_and_op_inv_step : forall a s, - test_and_op_inv a s -> - test_and_op_inv a (test_and_op a s). - Proof using Type*. - destruct s as [i acc]. - unfold test_and_op_inv, test_and_op; simpl; intro Hpre. - destruct i; [ apply Hpre | ]. - simpl. - rewrite N.shiftr_succ. - rewrite sel_correct. - case_eq (testbit i); intro testbit_eq; simpl; - rewrite testbit_correct in testbit_eq; rewrite testbit_eq; - rewrite Hpre, <- plus_n_O, nat_iter_op_plus; reflexivity. - Qed. - - Lemma test_and_op_inv_holds : forall a i s, - test_and_op_inv a s -> - test_and_op_inv a (funexp (test_and_op a) s i). - Proof using Type*. - induction i; intros; auto; simpl; apply test_and_op_inv_step; auto. - Qed. - - Lemma funexp_test_and_op_index : forall a x acc y, - fst (funexp (test_and_op a) (x, acc) y) = x - y. - Proof using Type. - induction y as [|? IHy]; simpl; rewrite <- ?Minus.minus_n_O; try reflexivity. - match goal with |- context[funexp ?a ?b ?c] => destruct (funexp a b c) as [i acc'] end. - simpl in IHy. - unfold test_and_op. - destruct i; rewrite Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity. - Qed. - - Lemma iter_op_termination : forall a bound, - N.size_nat x <= bound -> - test_and_op_inv a - (funexp (test_and_op a) (bound, id) bound) -> - iter_op bound a === nat_iter_op (N.to_nat x) a. - Proof using moinoid. - unfold test_and_op_inv, iter_op; simpl; intros ? ? ? Hinv. - rewrite Hinv, funexp_test_and_op_index, Minus.minus_diag. - reflexivity. - Qed. - - Lemma iter_op_correct : forall a bound, N.size_nat x <= bound -> - iter_op bound a === nat_iter_op (N.to_nat x) a. - Proof using Type*. - intros. - apply iter_op_termination; auto. - apply test_and_op_inv_holds. - unfold test_and_op_inv. - simpl. - rewrite N.shiftr_size by auto. - reflexivity. - Qed. -End IterAssocOp. - -Require Import Coq.Classes.Morphisms. -(*Require Import Crypto.Util.Tactics.*) -Require Import Crypto.Util.Relations. - -Global Instance Proper_funexp {T R} {Equivalence_R:Equivalence R} - : Proper ((R==>R) ==> R ==> Logic.eq ==> R) (@funexp T). -Proof. - repeat intro; subst. - match goal with [n0 : nat |- _ ] => rename n0 into n; induction n as [|n IHn] end; [solve [trivial]|]. - match goal with - [H: (_ ==> _)%signature _ _ |- _ ] => - etransitivity; solve [eapply (H _ _ IHn)|reflexivity] - end. -Qed. - -Global Instance Proper_test_and_op {T R} {Equivalence_R:@Equivalence T R} : - Proper ((R==>R==>R) - ==> pointwise_relation _ Logic.eq - ==> (Logic.eq==>R==>R==>R) - ==> R - ==> (fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)) - ==> (fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)) - ) (@test_and_op T). -Proof. - repeat match goal with - | _ => intro - | _ => split - | [p:prod _ _ |- _ ] => destruct p - | [p:and _ _ |- _ ] => destruct p - | _ => progress (cbv [fst snd test_and_op pointwise_relation respectful] in * ) - | _ => progress subst - | _ => progress break_match - | _ => solve [ congruence | eauto 99 ] - end. -Qed. - -Global Instance Proper_iter_op {T R} {Equivalence_R:@Equivalence T R} : - Proper ((R==>R==>R) - ==> R - ==> pointwise_relation _ Logic.eq - ==> (Logic.eq==>R==>R==>R) - ==> Logic.eq - ==> R - ==> R) - (@iter_op T). -Proof. - repeat match goal with - | _ => solve [ reflexivity | congruence | eauto 99 ] - | [ R : _ |- _ ] - => progress eapply (Proper_funexp (R:=(fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)))) - | _ => progress eapply Proper_test_and_op - | _ => progress split - | _ => progress (cbv [fst snd pointwise_relation respectful] in * ) - | _ => intro - end. -Qed. |