diff options
31 files changed, 217 insertions, 464 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 7c5c8d8cc..02ad4731f 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -142,8 +142,8 @@ Section Algebra. Global Existing Instance field_div_Proper. End AddMul. - Definition char_gt {T} (eq:T->T->Prop) (zero:T) (inj:BinPos.positive->T) C := forall p, BinPos.Pos.le p C -> not (eq (inj p) zero). - Existing Class char_gt. + Definition char_ge {T} (eq:T->T->Prop) (zero:T) (inj:BinPos.positive->T) C := forall p, BinPos.Pos.lt p C -> not (eq (inj p) zero). + Existing Class char_ge. End Algebra. Section ZeroNeqOne. diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v index f3a43f3e3..13a0ffa95 100644 --- a/src/Algebra/Field_test.v +++ b/src/Algebra/Field_test.v @@ -42,7 +42,7 @@ Module _fsatz_test. Lemma division_by_zero_in_hyps_neq_neq (bad:1/0 <> (1+1)/0): 1 <> 0. fsatz. Qed. Import BinNums. - Context {char_gt_15:@Ring.char_gt F eq zero one opp add sub mul 15}. + Context {char_ge_16:@Ring.char_ge F eq zero one opp add sub mul 16}. Local Notation two := (one+one) (only parsing). Local Notation three := (one+one+one) (only parsing). diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v index 8110ad5cd..72414b46e 100644 --- a/src/Algebra/IntegralDomain.v +++ b/src/Algebra/IntegralDomain.v @@ -62,21 +62,21 @@ Module IntegralDomain. Qed. Section WithChar. - Context C (char_gt_C:@Ring.char_gt R eq zero one opp add sub mul C). + Context C (char_ge_C:@Ring.char_ge R eq zero one opp add sub mul C) (HC: Pos.lt xH C). Definition is_factor_nonzero (n:N) : bool := - match n with N0 => false | N.pos p => BinPos.Pos.leb p C end. + match n with N0 => false | N.pos p => BinPos.Pos.ltb p C end. Lemma is_factor_nonzero_correct (n:N) (refl:Logic.eq (is_factor_nonzero n) true) : of_Z (Z.of_N n) <> zero. Proof. - destruct n; [discriminate|]; rewrite Znat.positive_N_Z; apply char_gt_C, Pos.leb_le, refl. + destruct n; [discriminate|]; rewrite Znat.positive_N_Z; apply char_ge_C, Pos.ltb_lt, refl. Qed. Lemma RZN_product_nonzero l (H : forall x : N, List.In x l -> of_Z (Z.of_N x) <> zero) : of_Z (Z.of_N (List.fold_right N.mul 1%N l)) <> zero. Proof. rewrite <-List.Forall_forall in H; induction H; simpl List.fold_right. - { eapply char_gt_C, Pos.le_1_l. } + { eapply char_ge_C; assumption. } { rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism constr:(of_Z). eapply Ring.nonzero_product_iff_nonzero_factor; eauto. } Qed. @@ -106,7 +106,7 @@ Module IntegralDomain. | Coef_mul c1 c2 => andb (is_nonzero c1) (is_nonzero c2) | _ => is_constant_nonzero (CtoZ c) end. - Lemma is_nonzero_correct c (refl:Logic.eq (is_nonzero c) true) : denote c <> zero. + Lemma is_nonzero_correct' c (refl:Logic.eq (is_nonzero c) true) : denote c <> zero. Proof. induction c; repeat match goal with @@ -123,6 +123,17 @@ Module IntegralDomain. end. Qed. End WithChar. + + Lemma is_nonzero_correct + C + (char_ge_C:@Ring.char_ge R eq zero one opp add sub mul C) + c (refl:Logic.eq (andb (Pos.ltb xH C) (is_nonzero C c)) true) + : denote c <> zero. + Proof. + rewrite Bool.andb_true_iff in refl; destruct refl. + eapply @is_nonzero_correct'; try apply Pos.ltb_lt; eauto. + Qed. + End ReflectiveNsatzSideConditionProver. Ltac reify one opp add mul x := @@ -145,9 +156,9 @@ Module IntegralDomain. Ltac solve_constant_nonzero := match goal with | |- not (?eq ?x _) => - let cg := constr:(_:Ring.char_gt (eq:=eq) _) in + let cg := constr:(_:Ring.char_ge (eq:=eq) _) in match type of cg with - @Ring.char_gt ?R eq ?zero ?one ?opp ?add ?sub ?mul ?C => + @Ring.char_ge ?R eq ?zero ?one ?opp ?add ?sub ?mul ?C => let x' := _LargeCharacteristicReflective.reify one opp add mul x in let x' := constr:(@_LargeCharacteristicReflective.denote R one opp add mul x') in change (not (eq x' zero)); diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index f39d730f2..640b12ed9 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -388,11 +388,11 @@ Section of_Z. Qed. End of_Z. -Definition char_gt +Definition char_ge {R eq zero one opp add} {sub:R->R->R} {mul:R->R->R} C := - @Algebra.char_gt R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C. -Existing Class char_gt. + @Algebra.char_ge R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C. +Existing Class char_ge. (*** Tactics for ring equations *) Require Export Coq.setoid_ring.Ring_tac. diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 32303a7bd..408c03337 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -21,7 +21,7 @@ Module E. Section CompleteEdwardsCurveTheorems. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one)} + {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)} {Feq_dec:DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. @@ -109,7 +109,7 @@ Module E. Section Homomorphism. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {Fchar_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one)} + {Fchar_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)} {Feq_dec:DecidableRel Feq}. Context {Fa Fd: F} @@ -152,10 +152,10 @@ Module E. Qed. (* TODO: character respects isomorphism *) - Global Instance Kchar_gt_2 : - @char_gt K Keq Kzero Kone Kopp Kadd Ksub Kmul (BinNat.N.succ_pos BinNat.N.one). + Global Instance Kchar_ge_2 : + @char_ge K Keq Kzero Kone Kopp Kadd Ksub Kmul (BinNat.N.succ_pos BinNat.N.two). Proof. - intros p Hp X; apply (Fchar_gt_2 p Hp). + intros p Hp X; apply (Fchar_ge_3 p Hp). eapply Monoid.is_homomorphism_phi_proper in X. rewrite (homomorphism_zero(zero:=Fzero)(phi:=KtoF)) in X. etransitivity; [|eexact X]; clear X. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index b2dbbc73d..ad0d79c52 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -10,7 +10,7 @@ Module Extended. Section ExtendedCoordinates. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one)} + {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)} {Feq_dec:DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 1d86a8e91..32eae2334 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -17,7 +17,7 @@ Section Edwards. Context (a:F) (a_nonzero : a<>0) (a_square : exists sqrt_a, sqrt_a^2 = a). Context (d:F) (d_nonsquare : forall sqrt_d, sqrt_d^2 <> d). - Context {char_gt_2:@Ring.char_gt F eq zero one opp add sub mul 2}. + Context {char_ge_3:@Ring.char_ge F eq zero one opp add sub mul 3}. Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing). Lemma onCurve_zero : onCurve 0 1. fsatz. Qed. diff --git a/src/EdDSARepChange.v b/src/EdDSARepChange.v index d36f07b9b..e44b634f8 100644 --- a/src/EdDSARepChange.v +++ b/src/EdDSARepChange.v @@ -125,7 +125,6 @@ Section EdDSA. Proof. eexists. pose proof EdDSA_l_odd. - assert (l_pos:(0 < l)%Z) by omega. cbv [verify']. etransitivity. Focus 2. { @@ -140,8 +139,8 @@ Section EdDSA. || rewrite SRepERepMul_correct || rewrite SdecS_correct || rewrite SRepDecModL_correct - || rewrite (@F.of_nat_to_nat _ l_pos _) - || rewrite (@F.of_nat_mod _ l_pos _) + || rewrite (@F.of_nat_to_nat _ _) + || rewrite (@F.of_nat_mod _ _) ). reflexivity. } Unfocus. diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v index fbd9238c1..faf4eecc5 100644 --- a/src/Encoding/ModularWordEncodingPre.v +++ b/src/Encoding/ModularWordEncodingPre.v @@ -9,7 +9,7 @@ Require Import Crypto.Spec.Encoding. Local Open Scope nat_scope. Section ModularWordEncodingPre. - Context {m : Z} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. + Context {m : positive} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. Let Fm_enc (x : F m) : word sz := NToWord sz (Z.to_N (F.to_Z x)). diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v index 215551801..66617ec29 100644 --- a/src/Encoding/ModularWordEncodingTheorems.v +++ b/src/Encoding/ModularWordEncodingTheorems.v @@ -13,7 +13,7 @@ Require Import Crypto.Spec.ModularWordEncoding. Local Open Scope F_scope. Section SignBit. - Context {m : Z} {prime_m : prime m} {two_lt_m : (2 < m)%Z} {sz : nat} {bound_check : (Z.to_nat m < 2 ^ sz)%nat}. + Context {m : positive} {prime_m : prime m} {two_lt_m : (2 < m)%Z} {sz : nat} {bound_check : (Z.to_nat m < 2 ^ sz)%nat}. Lemma sign_bit_parity : forall x, @sign_bit m sz x = Z.odd (F.to_Z x). Proof. diff --git a/src/Encoding/PointEncoding.v b/src/Encoding/PointEncoding.v index 2585a7392..2341cf090 100644 --- a/src/Encoding/PointEncoding.v +++ b/src/Encoding/PointEncoding.v @@ -26,7 +26,7 @@ Require Crypto.Encoding.PointEncodingPre. *) Section PointEncoding. - Context {b : nat} {m : Z} {Fa Fd : F m} {prime_m : Znumtheory.prime m} + Context {b : nat} {m : positive} {Fa Fd : F m} {prime_m : Znumtheory.prime m} {two_lt_m : (2 < m)%Z} {bound_check : (Z.to_nat m < 2 ^ b)%nat}. @@ -66,7 +66,6 @@ Section PointEncoding. {Ksign_correct : forall x, sign x = Ksign (phi x)} {Kenc_correct : forall x, Fencode x = Kenc (phi x)}. - Notation KonCurve := (@E.onCurve _ Keq Kone Kadd Kmul Ka Kd). Context {Kpoint} {Kcoord_to_point : @E.point K Keq Kone Kadd Kmul Ka Kd -> Kpoint} {Kpoint_to_coord : Kpoint -> (K * K)}. @@ -74,8 +73,6 @@ Section PointEncoding. Context {Kpoint_eq : Kpoint -> Kpoint -> Prop} {Kpoint_add : Kpoint -> Kpoint -> Kpoint}. Context {Kpoint_eq_correct : forall p q, Kpoint_eq p q <-> Tuple.fieldwise (n := 2) Keq (Kpoint_to_coord p) (Kpoint_to_coord q)} {Kpoint_eq_Equivalence : Equivalence Kpoint_eq}. - Context {Fprm:@E.twisted_edwards_params (F m) eq F.zero F.one F.opp F.add F.sub F.mul Fa Fd}. - Context {Kprm:@E.twisted_edwards_params K Keq Kzero Kone Kopp Kadd Ksub Kmul Ka Kd}. Context {phi_bijective : forall x y, Keq (phi x) (phi y) <-> x = y}. Lemma phi_onCurve : forall x y, @@ -93,7 +90,7 @@ Section PointEncoding. reflexivity. Qed. - Definition point_phi (P : Fpoint) : Kpoint := Kcoord_to_point (E.ref_phi (fieldK := Kfield) (Ha := phi_a) (Hd := phi_d) P). + Definition point_phi (P : Fpoint) : Kpoint := Kcoord_to_point (E.point_phi (fieldK := Kfield) (Ha := phi_a) (Hd := phi_d) P). Lemma Proper_point_phi : Proper (E.eq ==> Kpoint_eq) point_phi. Proof. @@ -101,7 +98,7 @@ Section PointEncoding. apply Kpoint_eq_correct; cbv [point_phi]. destruct x, y. repeat break_let. - cbv [E.ref_phi]. + cbv [E.point_phi]. rewrite !Kp2c_c2p. apply E.Proper_coordinates in H; cbv [E.coordinates proj1_sig] in H. inversion H; econstructor; cbv [Tuple.fieldwise' fst snd] in *; subst; @@ -113,6 +110,8 @@ Section PointEncoding. let z := Z.of_N (wordToN w) in if Z_lt_dec z m then Some (F.of_Z m z) else None. + (* The following does not build + Context {Kpoint_add_correct : forall P Q, Kpoint_eq (point_phi (Fpoint_add P Q)) (Kpoint_add (point_phi P) (point_phi Q))}. diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v index bbf0f82fd..7f8f185e4 100644 --- a/src/Encoding/PointEncodingPre.v +++ b/src/Encoding/PointEncodingPre.v @@ -19,15 +19,29 @@ Require Export Crypto.Util.FixCoqMistakes. Generalizable All Variables. Section PointEncodingPre. - Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div} {eq_dec:DecidableRel eq}. - Local Infix "==" := eq : type_scope. - Local Notation "a !== b" := (not (a == b)): type_scope. - Local Notation "0" := zero. Local Notation "1" := one. - Local Infix "+" := add. Local Infix "*" := mul. - Local Infix "-" := sub. Local Infix "/" := div. - Local Notation "x ^ 2" := (x*x). - - Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). + Context {F eq zero one opp add sub mul inv div} + {field:@field F eq zero one opp add sub mul inv div} + {char_ge_3 : @Ring.char_ge F eq zero one opp add sub mul (BinNat.N.succ_pos BinNat.N.two)} + {eq_dec:DecidableRel eq}. + Local Infix "==" := eq : type_scope. Local Notation "a !== b" := (not (a == b)) : type_scope. + Local Notation "0" := zero. Local Notation "1" := one. + Local Infix "+" := add. Local Infix "*" := mul. + Local Infix "-" := sub. Local Infix "/" := div. + Local Notation "x ^ 2" := (x*x). + + Context {a d: F} + {nonzero_a : a !== 0} + {square_a : exists sqrt_a, sqrt_a^2 == a} + {nonsquare_d : forall x, x^2 !== d}. + + Local Notation onCurve x y := (a*x^2 + y^2 == 1 + d*x^2*y^2). + Local Notation point := (@E.point F eq one add mul a d). + Local Notation point_eq := (@E.eq F eq one add mul a d). + Local Notation point_zero := (E.zero(nonzero_a:=nonzero_a)(d:=d)). + Local Notation point_add := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)). + Local Notation point_mul := (E.mul(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)). + + Add Field _point_encoding_field : (Field.field_theory_for_stdlib_tactic (T:=F)). Definition F_eqb x y := if eq_dec x y then true else false. Lemma F_eqb_iff : forall x y, F_eqb x y = true <-> x == y. @@ -35,9 +49,6 @@ Section PointEncodingPre. unfold F_eqb; intros; destruct (eq_dec x y); split; auto; discriminate. Qed. - Context {a d:F} {prm:@E.twisted_edwards_params F eq zero one opp add sub mul a d}. - Local Notation point := (@E.point F eq one add mul a d). - Local Notation onCurve := (@E.onCurve F eq one add mul a d). Local Notation solve_for_x2 := (@E.solve_for_x2 F one sub mul div a d). Context {sz : nat} (sz_nonzero : (0 < sz)%nat). @@ -68,10 +79,10 @@ Section PointEncodingPre. onCurve (sqrt (E.solve_for_x2(Fone:=one)(Fsub:=sub)(Fmul:=mul)(Fdiv:=div)(a:=a)(d:=d) y)) y. Proof. intros. - eapply E.solve_correct. + eapply @E.solve_correct; eauto. eapply square_sqrt. symmetry. - eapply E.solve_correct. eassumption. + eapply @E.solve_correct; eauto. Qed. (* TODO : move? *) @@ -84,11 +95,11 @@ Section PointEncodingPre. onCurve (opp (sqrt (solve_for_x2 y))) y. Proof. intros. - apply E.solve_correct. + eapply @E.solve_correct; eauto. etransitivity; [ apply square_opp | ]. eapply square_sqrt. symmetry. - apply E.solve_correct; eassumption. + eapply @E.solve_correct; eauto. Qed. Definition point_enc_coordinates (p : (F * F)) : Word.word (sz+1) := let '(x,y) := p in @@ -152,7 +163,6 @@ Section PointEncodingPre. unfold option_coordinates_eq, option_eq, prod_eq; tauto. Qed. - Definition point_eq (p q : point) : Prop := prod_eq eq eq (proj1_sig p) (proj1_sig q). Definition option_point_eq := option_eq (point_eq). Lemma option_point_eq_iff : forall p q, @@ -222,19 +232,11 @@ Section PointEncodingPre. Ltac congruence_option_coord := exfalso; eauto using option_coordinates_eq_NS. - Lemma onCurve_eq : forall x y, - eq (add (mul a (mul x x)) (mul y y)) - (add one (mul (mul d (mul x x)) (mul y y))) -> - @E.onCurve _ eq one add mul a d x y. - Proof. - tauto. - Qed. - - Definition point_from_xy (xy : F * F) : option point := + Program Definition point_from_xy (xy : F * F) : option point := let '(x,y) := xy in match Decidable.dec (eq (add (mul a (mul x x)) (mul y y)) - (add one (mul (mul d (mul x x)) (mul y y)))) with - | left A => Some (exist _ (x,y) (onCurve_eq x y A)) + (add one (mul (mul d (mul x x)) (mul y y)))) return option point with + | left A => Some (exist _ (x,y) _) | right _ => None end. @@ -293,12 +295,12 @@ Section PointEncodingPre. option_eq point_eq (point_dec w) (Some x) -> option_eq (Tuple.fieldwise (n := 2) eq) (point_dec_coordinates w) (Some (E.coordinates x)). Proof. - unfold point_dec, E.coordinates, point_from_xy, option_rect; intros. - break_match; [ | congruence]. - destruct p. break_match; [ | congruence ]. + cbv [point_dec E.coordinates point_from_xy option_rect]; intros. destruct x as [xy pf]; destruct xy. - cbv [option_eq point_eq] in *. - simpl in *. + break_match; [|congruence]. + destruct p. + break_match; [|congruence]. + cbv [option_eq point_eq E.coordinates Tuple.fieldwise Tuple.fieldwise'] in *. intuition. Qed. @@ -357,13 +359,12 @@ Section PointEncodingPre. pose proof (square_sqrt (solve_for_x2 y) x) as solve_sqrt_ok. forward solve_sqrt_ok. { symmetry. - apply E.solve_correct. - assumption. + eapply @E.solve_correct; eassumption. } match goal with [ H1 : ?P, H2 : ?P -> _ |- _ ] => specialize (H2 H1); clear H1 end. unfold sqrt_ok in solve_sqrt_ok. break_if; [ | congruence]. - assert (solve_for_x2 y == (x ^2)) as solve_correct by (symmetry; apply E.solve_correct; assumption). + assert (solve_for_x2 y == (x ^2)) as solve_correct by (symmetry; eapply @E.solve_correct; eassumption). destruct (eq_dec x 0) as [eq_x_0 | neq_x_0]. + rewrite eq_x_0 in *. assert (0^2 == 0) as zero_square by apply Ring.mul_0_l. @@ -387,7 +388,7 @@ Section PointEncodingPre. rewrite !solve_correct in *. intro. apply neq_x_0. - rewrite H0, zero_square in sqrt_square. + rewrite H, zero_square in sqrt_square. rewrite Ring.zero_product_iff_zero_factor in sqrt_square. tauto. } Unfocus. rewrite wlast_combine. @@ -396,9 +397,9 @@ Section PointEncodingPre. try eapply sign_match with (y := solve_for_x2 y); eauto; try solve [symmetry; auto]; rewrite ?square_opp; auto; intro; apply neq_x_0; rewrite solve_correct in *; - try apply Group.inv_zero_zero in H0; - rewrite H0, zero_square in sqrt_square; - rewrite Ring.zero_product_iff_zero_factor in sqrt_square; tauto. + rewrite ?Group.inv_id_iff in H; + rewrite H, zero_square in sqrt_square; + rewrite Ring.zero_product_iff_zero_factor in sqrt_square; tauto. Qed. Lemma point_encoding_valid : forall p, @@ -429,11 +430,11 @@ Proof. end. exfalso. apply n. - apply option_coordinates_eq_iff in H1; destruct H1. - rewrite H1, H2; assumption. + apply option_coordinates_eq_iff in H0; destruct H0. + rewrite H0, H1; assumption. - rewrite Heqo in H0. + rewrite Heqo in H. congruence_option_coord. Qed. diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 262b20e3e..863300dde 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -31,8 +31,15 @@ Module F. Lemma pow_spec {m} a : F.pow a 0%N = 1%F :> F m /\ forall x, F.pow a (1 + x)%N = F.mul a (F.pow a x). Proof. change (@F.pow m) with (proj1_sig (@F.pow_with_spec m)); destruct (@F.pow_with_spec m); eauto. Qed. + Global Instance char_gt {m} : + @Ring.char_ge + (F m) Logic.eq F.zero F.one F.opp F.add F.sub F.mul + m. + Proof. + Admitted. + Section FandZ. - Context {m:Z}. + Context {m:positive}. Local Open Scope F_scope. Theorem eq_to_Z_iff (x y : F m) : x = y <-> F.to_Z x = F.to_Z y. @@ -145,34 +152,33 @@ Module F. Local Infix "mod" := modulo : nat_scope. Local Open Scope nat_scope. - Context {m} (m_pos: (0 < m)%Z). - Let to_nat_m_nonzero : Z.to_nat m <> 0. - rewrite Z2Nat.inj_lt in m_pos; omega. - Qed. + Context {m:BinPos.positive}. Lemma to_nat_of_nat (n:nat) : F.to_nat (F.of_nat m n) = (n mod (Z.to_nat m))%nat. Proof. unfold F.to_nat, F.of_nat. rewrite F.to_Z_of_Z. - pose proof (mod_Zmod n (Z.to_nat m) to_nat_m_nonzero) as Hmod. - rewrite Z2Nat.id in Hmod by omega. + assert (Pos.to_nat m <> 0)%nat as HA by (pose proof Pos2Nat.is_pos m; omega). + pose proof (mod_Zmod n (Pos.to_nat m) HA) as Hmod. + rewrite positive_nat_Z in Hmod. rewrite <- Hmod. - rewrite <-Nat2Z.id by omega. - reflexivity. + rewrite <-Nat2Z.id, Z2Nat.inj_pos; omega. Qed. Lemma of_nat_to_nat x : F.of_nat m (F.to_nat x) = x. unfold F.to_nat, F.of_nat. - rewrite Z2Nat.id; [ eapply F.of_Z_to_Z | eapply F.to_Z_range; trivial]. + rewrite Z2Nat.id; [ eapply F.of_Z_to_Z | eapply F.to_Z_range; reflexivity]. Qed. + Lemma Pos_to_nat_nonzero p : Pos.to_nat p <> 0%nat. + Admitted. + Lemma of_nat_mod (n:nat) : F.of_nat m (n mod (Z.to_nat m)) = F.of_nat m n. Proof. unfold F.of_nat. - replace (Z.of_nat (n mod Z.to_nat m)) with(Z.of_nat n mod Z.of_nat (Z.to_nat m))%Z - by (symmetry; eapply (mod_Zmod n (Z.to_nat m) to_nat_m_nonzero)). - rewrite Z2Nat.id by omega. - rewrite <-F.of_Z_mod; reflexivity. + rewrite (F.of_Z_mod (Z.of_nat n)), ?mod_Zmod, ?Z2Nat.id; [reflexivity|..]. + { apply Pos2Z.is_nonneg. } + { rewrite Z2Nat.inj_pos. apply Pos_to_nat_nonzero. } Qed. Lemma to_nat_mod (x:F m) (Hm:(0 < m)%Z) : F.to_nat x mod (Z.to_nat m) = F.to_nat x. @@ -192,7 +198,7 @@ Module F. End FandNat. Section RingTacticGadgets. - Context (m:Z). + Context (m:positive). Definition ring_theory : ring_theory 0%F 1%F (@F.add m) (@F.mul m) (@F.sub m) (@F.opp m) eq := Algebra.Ring.ring_theory_for_stdlib_tactic. @@ -252,22 +258,8 @@ Module F. Ltac is_constant t := match t with F.of_Z _ ?x => x | _ => NotConstant end. Ltac is_pow_constant t := Ncst t. - Module Type Modulus. Parameter modulus : Z. End Modulus. - - (* Example of how to instantiate the ring tactic *) - Module RingModulo (Export M : Modulus). - Add Ring _theory : (ring_theory modulus) - (morphism (ring_morph modulus), - constants [is_constant], - div (morph_div_theory modulus), - power_tac (power_theory modulus) [is_pow_constant]). - - Example ring_modulo_example : forall x y z, x*z + z*y = z*(x+y). - Proof. intros. ring. Qed. - End RingModulo. - Section VariousModulo. - Context {m:Z}. + Context {m:positive}. Local Open Scope F_scope. Add Ring _theory : (ring_theory m) @@ -284,7 +276,7 @@ Module F. End VariousModulo. Section Pow. - Context {m:Z}. + Context {m:positive}. Add Ring _theory' : (ring_theory m) (morphism (ring_morph m), constants [is_constant], diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v index fd9483182..428239498 100644 --- a/src/ModularArithmetic/ModularBaseSystemListProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v @@ -164,7 +164,7 @@ Section ModulusDigitsProofs. rewrite encodeZ_spec by eauto using limb_widths_nonnil, limb_widths_good. apply Z.mod_small. cbv [upper_bound]. fold k. - assert (modulus = 2 ^ k - c) by (cbv [c]; ring). + assert (Z.pos modulus = 2 ^ k - c) by (cbv [c]; ring). omega. Qed. @@ -182,7 +182,7 @@ Section ModulusDigitsProofs. | |- _ => progress autorewrite with Ztestbit | |- _ => unique pose proof c_pos | |- _ => unique pose proof modulus_pos - | |- _ => unique assert (modulus = 2 ^ k - c) by (cbv [c]; ring) + | |- _ => unique assert (Z.pos modulus = 2 ^ k - c) by (cbv [c]; ring) | |- _ => break_if | |- _ => rewrite decode_modulus_digits | |- _ => rewrite Z.testbit_pow2_mod @@ -196,7 +196,7 @@ Section ModulusDigitsProofs. specialize_by (eauto || omega); rewrite sum_firstn_succ_default in *; split; zero_bounds; eauto) | |- Z.pow2_mod _ _ = Z.ones _ => apply Z.bits_inj' - | |- Z.testbit modulus ?i = true => transitivity (Z.testbit (2 ^ k - c) i) + | |- Z.testbit (Z.pos modulus) ?i = true => transitivity (Z.testbit (2 ^ k - c) i) | |- _ => congruence end. @@ -496,7 +496,7 @@ Section ConditionalSubtractModulusProofs. specialize_by auto. cbv [upper_bound] in *. fold k in *. - assert (modulus = 2 ^ k - c) by (cbv [c]; ring). + assert (Z.pos modulus = 2 ^ k - c) by (cbv [c]; ring). destruct (Z_le_dec modulus (BaseSystem.decode base u)). + split; try omega. apply Z.lt_le_trans with (m := 2 ^ k); try omega. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 3b0231191..34a331fa1 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -30,12 +30,12 @@ Class CarryChain (limb_widths : list Z) := carry_chain_valid : forall i, In i carry_chain -> (i < length limb_widths)%nat }. - Class SubtractionCoefficient {m : Z} {prm : PseudoMersenneBaseParams m} := { + Class SubtractionCoefficient {m : positive} {prm : PseudoMersenneBaseParams m} := { coeff : tuple Z (length limb_widths); coeff_mod: decode coeff = 0%F }. - Class ExponentiationChain {m : Z} {prm : PseudoMersenneBaseParams m} (exp : Z) := { + Class ExponentiationChain {m : positive} {prm : PseudoMersenneBaseParams m} (exp : Z) := { chain : list (nat * nat); chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N exp }. @@ -85,7 +85,7 @@ Section FieldOperationProofs. + apply F.of_Z_to_Z. + apply bv. + rewrite <-F.mod_to_Z. - match goal with |- appcontext [?a mod modulus] => + match goal with |- appcontext [?a mod (Z.pos modulus)] => pose proof (Z.mod_pos_bound a modulus modulus_pos) end. pose proof lt_modulus_2k. omega. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index abc30056f..6f2970814 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -15,10 +15,11 @@ Require Export Crypto.Util.FixCoqMistakes. Require Crypto.Algebra Crypto.Algebra.Field. Existing Class prime. +Local Open Scope F_scope. Module F. Section Field. - Context (q:Z) {prime_q:prime q}. + Context (q:positive) {prime_q:prime q}. Lemma inv_spec : F.inv 0%F = (0%F : F q) /\ (prime q -> forall x : F q, x <> 0%F -> (F.inv x * x)%F = 1%F). Proof. change (@F.inv q) with (proj1_sig (@F.inv_with_spec q)); destruct (@F.inv_with_spec q); eauto. Qed. @@ -37,33 +38,10 @@ Module F. | _ => split end. Qed. - - Definition field_theory : field_theory 0%F 1%F F.add F.mul F.sub F.opp F.div F.inv eq - := Algebra.Field.field_theory_for_stdlib_tactic. End Field. - (** A field tactic hook that can be imported *) - Module Type PrimeModulus. - Parameter modulus : Z. - Parameter prime_modulus : prime modulus. - End PrimeModulus. - Module FieldModulo (Export M : PrimeModulus). - Module Import RingM := F.RingModulo M. - Add Field _field : (F.field_theory modulus) - (morphism (F.ring_morph modulus), - constants [F.is_constant], - div (F.morph_div_theory modulus), - power_tac (F.power_theory modulus) [F.is_pow_constant]). - End FieldModulo. - Section NumberThoery. - Context {q:Z} {prime_q:prime q} {two_lt_q: 2 < q}. - Local Open Scope F_scope. - Add Field _field : (field_theory q) - (morphism (F.ring_morph q), - constants [F.is_constant], - div (F.morph_div_theory q), - power_tac (F.power_theory q) [F.is_pow_constant]). + Context {q:positive} {prime_q:prime q} {two_lt_q: 2 < q}. (* TODO: move to PrimeFieldTheorems *) Lemma to_Z_1 : @F.to_Z q 1 = 1%Z. @@ -91,16 +69,15 @@ Module F. Global Instance Decidable_square (x:F q) : Decidable (exists y, y*y = x). Proof. destruct (dec (x = 0)). - { left. abstract (exists 0; subst; ring). } + { left. abstract (exists 0; subst; apply Ring.mul_0_l). } { eapply Decidable_iff_to_impl; [eapply euler_criterion; assumption | exact _]. } Defined. End NumberThoery. Section SquareRootsPrime3Mod4. - Context {q:Z} {prime_q: prime q} {q_3mod4 : q mod 4 = 3}. + Context {q:positive} {prime_q: prime q} {q_3mod4 : q mod 4 = 3}. - Local Open Scope F_scope. - Add Field _field2 : (field_theory q) + Add Field _field2 : (Algebra.Field.field_theory_for_stdlib_tactic(T:=F q)) (morphism (F.ring_morph q), constants [F.is_constant], div (F.morph_div_theory q), @@ -114,15 +91,13 @@ Module F. Lemma two_lt_q_3mod4 : 2 < q. Proof. pose proof (prime_ge_2 q _) as two_le_q. - apply Zle_lt_or_eq in two_le_q. - destruct two_le_q; auto. - subst_max. - discriminate. + destruct (Zle_lt_or_eq _ _ two_le_q) as [H|H]; [exact H|]. + rewrite <-H in q_3mod4; discriminate. Qed. Local Hint Resolve two_lt_q_3mod4. - Lemma sqrt_3mod4_correct : forall x, - ((exists y, y*y = x) <-> (sqrt_3mod4 x)*(sqrt_3mod4 x) = x). + Lemma sqrt_3mod4_correct (x:F q) : + ((exists y, y*y = x) <-> (sqrt_3mod4 x)*(sqrt_3mod4 x) = x)%F. Proof. cbv [sqrt_3mod4]; intros. destruct (F.eq_dec x 0); @@ -148,10 +123,9 @@ Module F. End SquareRootsPrime3Mod4. Section SquareRootsPrime5Mod8. - Context {q:Z} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}. - + Context {q:positive} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}. Local Open Scope F_scope. - Add Field _field3 : (field_theory q) + Add Field _field3 : (Algebra.Field.field_theory_for_stdlib_tactic(T:=F q)) (morphism (F.ring_morph q), constants [F.is_constant], div (F.morph_div_theory q), @@ -164,10 +138,8 @@ Module F. Lemma two_lt_q_5mod8 : 2 < q. Proof. pose proof (prime_ge_2 q _) as two_le_q. - apply Zle_lt_or_eq in two_le_q. - destruct two_le_q; auto. - subst_max. - discriminate. + destruct (Zle_lt_or_eq _ _ two_le_q) as [H|H]; [exact H|]. + rewrite <-H in *. discriminate. Qed. Local Hint Resolve two_lt_q_5mod8. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 630fc102e..3a530c377 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -33,7 +33,7 @@ Section PseudoMersenneBaseParamProofs. pose proof (NumTheoryUtil.lt_1_p _ prime_modulus); omega. Qed. Hint Resolve modulus_pos. - Lemma modulus_nonzero : modulus <> 0. + Lemma modulus_nonzero : Z.pos modulus <> 0. pose proof (Znumtheory.prime_ge_2 _ prime_modulus); omega. Qed. @@ -45,7 +45,6 @@ Section PseudoMersenneBaseParamProofs. rewrite Z.mul_add_distr_r, Zplus_mod. unfold c. rewrite Z.sub_sub_distr, Z.sub_diag. - simpl. rewrite Z.mul_comm, Z.mod_add_l; auto using modulus_nonzero. rewrite <- Zplus_mod; auto. Qed. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v index b564bcb05..6f6fd6556 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParams.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v @@ -4,16 +4,16 @@ Require Import Crypto.Util.ListUtil. Require Crypto.BaseSystem. Local Open Scope Z_scope. -Class PseudoMersenneBaseParams (modulus : Z) := { +Class PseudoMersenneBaseParams (modulus : positive) := { limb_widths : list Z; limb_widths_pos : forall w, In w limb_widths -> 0 < w; limb_widths_nonnil : limb_widths <> nil; limb_widths_good : forall i j, (i + j < length limb_widths)%nat -> sum_firstn limb_widths (i + j) <= sum_firstn limb_widths i + sum_firstn limb_widths j; - prime_modulus : Znumtheory.prime modulus; + prime_modulus : Znumtheory.prime (Z.pos modulus); k := sum_firstn limb_widths (length limb_widths); - c := 2 ^ k - modulus; + c := 2 ^ k - (Z.pos modulus); c_pos : 0 < c; limb_widths_match_modulus : forall i j, (i < length limb_widths)%nat -> diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v deleted file mode 100644 index 4ec1ed82c..000000000 --- a/src/ModularArithmetic/Tutorial.v +++ /dev/null @@ -1,196 +0,0 @@ -Require Import Coq.ZArith.BinInt Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems. - - -(* Example for modular arithmetic with a concrete modulus in a section *) -Section Mod24. - (* Set notations + - * / refer to F operations *) - Local Open Scope F_scope. - - (* Specify modulus *) - Let q := 24. - - (* Boilerplate for letting Z numbers be interpreted as field elements *) - Let ZToFq := F.of_Z _ : BinNums.Z -> F q. Hint Unfold ZToFq. - Local Coercion ZToFq : Z >-> F. - Local Coercion F.to_Z : F >-> Z. - - (* Boilerplate for [ring]. Similar boilerplate works for [field] if - the modulus is prime . *) - Add Ring _theory : (F.ring_theory q) - (morphism (F.ring_morph q), - preprocess [unfold ZToFq], - constants [F.is_constant], - div (F.morph_div_theory q), - power_tac (F.power_theory q) [F.is_pow_constant]). - - Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + 2*a*b + b^2. - Proof. - intros. - ring. - Qed. -End Mod24. - -(* Example for modular arithmetic with an abstract modulus in a section *) -Section Modq. - Context {q:Z} {prime_q:prime q}. - Existing Instance prime_q. - - (* Set notations + - * / refer to F operations *) - Local Open Scope F_scope. - - (* Boilerplate for letting Z numbers be interpreted as field elements *) - Let ZToFq := F.of_Z _ : BinNums.Z -> F q. Hint Unfold ZToFq. - Local Coercion ZToFq : Z >-> F. - Local Coercion F.to_Z : F >-> Z. - - (* Boilerplate for [field]. Similar boilerplate works for [ring] if - the modulus is not prime . *) - Add Field _theory' : (F.field_theory q) - (morphism (F.ring_morph q), - preprocess [unfold ZToFq], - constants [F.is_constant], - div (F.morph_div_theory q), - power_tac (F.power_theory q) [F.is_pow_constant]). - - Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + 2*(a/c)*(b/c) + b^2/c^2. - Proof. - intros. - field; trivial. - Qed. -End Modq. - -(*** The old way: Modules ***) - -Module Modulus31 <: F.PrimeModulus. - Definition modulus := 2^5 - 1. - Lemma prime_modulus : prime modulus. - Admitted. -End Modulus31. - -Module Modulus127 <: F.PrimeModulus. - Definition modulus := 2^127 - 1. - Lemma prime_modulus : prime modulus. - Admitted. -End Modulus127. - -Module Example31. - (* Then we can construct a field with that modulus *) - Module Import Field := F.FieldModulo Modulus31. - Import Modulus31. - - (* And pull in the appropriate notations *) - Local Open Scope F_scope. - - (* First, let's solve a ring example*) - Lemma ring_example: forall x: F modulus, x * (F.of_Z _ 2) = x + x. - Proof. - intros. - ring. - Qed. - - (* Unfortunately, the [ring] and [field] tactics need syntactic - (not definitional) equality to recognize the ring in question. - Therefore, it is necessary to explicitly rewrite the modulus - (usually hidden by implicitn arguments) match the one passed to - [FieldModulo]. *) - Lemma ring_example': forall x: F (2^5-1), x * (F.of_Z _ 2) = x + x. - Proof. - intros. - change (2^5-1)%Z with modulus. - ring. - Qed. - - (* Then a field example (we have to know we can't divide by zero!) *) - Lemma field_example: forall x y z: F modulus, z <> 0 -> - x * (y / z) / z = x * y / (z ^ 2). - Proof. - intros; simpl. - field; trivial. - Qed. - - (* Then an example with exponentiation *) - Lemma exp_example: forall x: F modulus, x ^ 2 + F.of_Z _ 2 * x + 1 = (x + 1) ^ 2. - Proof. - intros; simpl. - field; trivial. - Qed. - - (* In general, the rule I've been using is: - - - If our goal looks like x = y: - - + If we need to use assumptions to prove the goal, then before - we apply field, - - * Perform all relevant substitutions (especially subst) - - * If we have something more complex, we're probably going - to have to performe some sequence of "replace X with Y" - and solve out the subgoals manually before we can use - field. - - + Else, just use field directly - - - If we just want to simplify terms and put them into a canonical - form, then field_simplify or ring_simplify should do the trick. - Note, however, that the canonical form has lots of annoying "/1"s - - - Otherwise, do a "replace X with Y" to generate an equality - so that we can use field in the above case - - *) - -End Example31. - -(* Notice that the field tactics work whether we know what the modulus is *) -Module TimesZeroTransparentTestModule. - Module Import Theory := F.FieldModulo Modulus127. - Import Modulus127. - Local Open Scope F_scope. - - Lemma timesZero : forall a : F modulus, a*0 = 0. - intros. - field. - Qed. -End TimesZeroTransparentTestModule. - -(* An opaque modulus causes the field tactic to expand all constants - into matches on the modulus. Goals can still be proven, but with - significant overhead. Consider using an entirely abstract - [Algebra.field] instead. *) - -Module TimesZeroParametricTestModule (M: F.PrimeModulus). - Module Theory := F.FieldModulo M. - Import Theory M. - Local Open Scope F_scope. - - Lemma timesZero : forall a : F modulus, a*0 = 0. - intros. - field. - Qed. - - Lemma realisticFraction : forall x y d : F modulus, 1 <> F.of_Z modulus 0 -> (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x. - Proof. - intros. - field; assumption. - Qed. - - Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus, - 1 <> F.of_Z modulus 0 -> - ZQ <> 0 -> - ZP <> 0 -> - ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 -> - ZP * F.of_Z _ 2 * ZQ * (ZP * ZQ) + XP * YP * F.of_Z _ 2 * d * (XQ * YQ) <> 0 -> - ZP * F.of_Z _ 2 * ZQ * (ZP * ZQ) - XP * YP * F.of_Z _ 2 * d * (XQ * YQ) <> 0 -> - - ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) * - (ZP * F.of_Z _ 2 * ZQ - XP * YP / ZP * F.of_Z _ 2 * d * (XQ * YQ / ZQ)) / - ((ZP * F.of_Z _ 2 * ZQ - XP * YP / ZP * F.of_Z _ 2 * d * (XQ * YQ / ZQ)) * - (ZP * F.of_Z _ 2 * ZQ + XP * YP / ZP * F.of_Z _ 2 * d * (XQ * YQ / ZQ))) = - (XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)). - Proof. - intros. - field; repeat split; assumption. - Qed. -End TimesZeroParametricTestModule. diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 801b31ffc..daaa2ed74 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -11,7 +11,7 @@ Module E. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one)} + {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)} {Feq_dec:Decidable.DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 02f59c9e5..4fc3afce4 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -12,10 +12,10 @@ Section Ed25519. Local Open Scope Z_scope. - Definition q : BinNums.Z := 2^255 - 19. + Definition q : BinPos.positive := 2^255 - 19. Definition Fq : Type := F q. - Definition l : BinNums.Z := 2^252 + 27742317777372353535851937790883648493. + Definition l : BinPos.positive := 2^252 + 27742317777372353535851937790883648493. Definition Fl : Type := F l. Local Open Scope F_scope. @@ -51,10 +51,10 @@ Section Ed25519. let '(x,y) := E.coordinates P in Fencode (len:=b-1) y ++ bit (sign x). Definition Senc : Fl -> Word.word b := Fencode (len:=b). - Local Instance char_gt_2 : (* TODO: prove this in PrimeFieldTheorems *) - @Ring.char_gt (F.F q) (@eq (F.F q)) (F.of_Z q BinNums.Z0) + Local Instance char_gt_e : (* TODO: prove this in PrimeFieldTheorems *) + @Ring.char_ge (F.F q) (@eq (F.F q)) (F.of_Z q BinNums.Z0) (F.of_Z q (BinNums.Zpos BinNums.xH)) (@F.opp q) - (@F.add q) (@F.sub q) (@F.mul q) (BinNat.N.succ_pos BinNat.N.one). + (@F.add q) (@F.sub q) (@F.mul q) (BinNat.N.succ_pos BinNat.N.two). Proof. intros p ?. edestruct (fun p:p = (BinNat.N.succ_pos BinNat.N.zero) \/ p = (BinNat.N.succ_pos BinNat.N.one) => p); subst. { admit. (* @@ -75,21 +75,18 @@ Section Ed25519. Let mul := E.mul(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d). Let zero := E.zero(nonzero_a:=nonzero_a)(d:=d). - Definition ed25519 (l_order_B: E.eq (mul (BinInt.Z.to_nat l) B)%E zero) : + Definition ed25519 (l_order_B: E.eq(F:=Fq)(Fone:=F.one) (mul (BinInt.Z.to_nat l) B)%E zero) : EdDSA (E:=E) (Eadd:=add) (Ezero:=zero) (EscalarMult:=mul) (B:=B) (Eopp:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.opp(nonzero_a:=nonzero_a)) (* TODO: move defn *) (Eeq:=E.eq) (* TODO: move defn *) (l:=l) (b:=b) (n:=n) (c:=c) (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512). Proof. - split; try exact _. - (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *) - (* timeout 1 match goal with H:?P |- ?P => idtac end. *) - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - exact l_order_B. + split; + match goal with + | |- ?P => match goal with [H:P|-_] => exact H end (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *) + | _ => exact _ + | _ => Crypto.Util.Decidable.vm_decide + end. Qed. End Ed25519. diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index f8581c4c9..67a1014f6 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -33,7 +33,7 @@ Section EdDSA. {H : forall {n}, Word.word n -> Word.word (b + b)} (* main hash function *) {c : nat} (* cofactor E = 2^c *) {n : nat} (* secret keys are (n+1) bits *) - {l : BinInt.Z} (* order of the subgroup of E generated by B *) + {l : BinPos.positive} (* order of the subgroup of E generated by B *) {B : E} (* base point *) diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index a3e80fcf9..ed6a0c4a2 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -2,6 +2,13 @@ Require Coq.ZArith.Znumtheory Coq.Numbers.BinNums. Require Crypto.ModularArithmetic.Pre. +Delimit Scope positive_scope with positive. +Bind Scope positive_scope with BinPos.positive. +Infix "+" := BinPos.Pos.add : positive_scope. +Infix "*" := BinPos.Pos.mul : positive_scope. +Infix "-" := BinPos.Pos.sub : positive_scope. +Infix "^" := BinPos.Pos.pow : positive_scope. + Delimit Scope N_scope with N. Bind Scope N_scope with BinNums.N. Infix "+" := BinNat.N.add : N_scope. @@ -18,17 +25,20 @@ Infix "-" := BinInt.Z.sub : Z_scope. Infix "/" := BinInt.Z.div : Z_scope. Infix "^" := BinInt.Z.pow : Z_scope. Infix "mod" := BinInt.Z.modulo (at level 40, no associativity) : Z_scope. + Local Open Scope Z_scope. +Global Coercion BinInt.Z.pos : BinPos.positive >-> BinInt.Z. +Global Coercion BinInt.Z.of_N : BinNums.N >-> BinInt.Z. +Global Set Printing Coercions. Module F. - Definition F (m : BinInt.Z) := { z : BinInt.Z | z = z mod m }. - Bind Scope F_scope with F. + Definition F (m : BinPos.positive) := { z : BinInt.Z | z = z mod m }. Local Obligation Tactic := cbv beta; auto using Pre.Z_mod_mod. Program Definition of_Z m (a:BinNums.Z) : F m := a mod m. Definition to_Z {m} (a:F m) : BinNums.Z := proj1_sig a. Section FieldOperations. - Context {m : BinInt.Z}. + Context {m : BinPos.positive}. Definition zero : F m := of_Z m 0. Definition one : F m := of_Z m 1. diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v index 7a9845e7e..5b0bdb545 100644 --- a/src/Spec/ModularWordEncoding.v +++ b/src/Spec/ModularWordEncoding.v @@ -11,7 +11,7 @@ Require Crypto.Encoding.ModularWordEncodingPre. Local Open Scope nat_scope. Section ModularWordEncoding. - Context {m : Z} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. + Context {m : positive} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. Definition Fm_enc (x : F m) : word sz := NToWord sz (Z.to_N (F.to_Z x)). diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v index 5f7246011..2717f6bbc 100644 --- a/src/Spec/MontgomeryCurve.v +++ b/src/Spec/MontgomeryCurve.v @@ -6,7 +6,7 @@ Require Import Crypto.Spec.WeierstrassCurve. Module M. Section MontgomeryCurve. Import BinNat. - Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. @@ -28,20 +28,26 @@ Module M. end }. Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. + Definition eq (P1 P2:point) := + match coordinates P1, coordinates P2 with + | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2 + | ∞, ∞ => True + | _, _ => False + end. + Import Crypto.Util.Tactics Crypto.Algebra.Field. Ltac t := destruct_head' point; destruct_head' sum; destruct_head' prod; break_match; simpl in *; break_match_hyps; trivial; try discriminate; repeat match goal with | |- _ /\ _ => split - | [H:@eq (sum _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H - | [H:@eq (prod _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H + | [H:@Logic.eq (sum _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H + | [H:@Logic.eq (prod _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H end; subst; try fsatz. Program Definition add (P1 P2:point) : point := - exist _ - match coordinates P1, coordinates P2 return _ with + match coordinates P1, coordinates P2 return F*F+∞ with (x1, y1), (x2, y2) => if Decidable.dec (x1 = x2) then if Decidable.dec (y1 = - y2) @@ -51,53 +57,39 @@ Module M. | ∞, ∞ => ∞ | ∞, _ => coordinates P2 | _, ∞ => coordinates P1 - end _. + end. Next Obligation. Proof. t. Qed. Program Definition opp (P:point) : point := - exist _ - match P with - | (x, y) => (x, -y) - | ∞ => ∞ - end _. - Next Obligation. - Proof. t. Qed. + match P return F*F+∞ with + | (x, y) => (x, -y) + | ∞ => ∞ + end. + Next Obligation. Proof. t. Qed. Local Notation "4" := (1+3). Local Notation "16" := (4*4). Local Notation "9" := (3*3). Local Notation "27" := (3*9). - Context {char_gt_27:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 27}. + Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}. Let WeierstrassA := ((3-a^2)/(3*b^2)). Let WeierstrassB := ((2*a^3-9*a)/(27*b^3)). - Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB). - Program Definition MontgomeryOfWeierstrass (P:Wpoint) : point := - exist - _ - match W.coordinates P return _ with - | (x,y) => (b*x-a/3, b*y) - | _ => ∞ - end - _. - Next Obligation. - Proof. subst WeierstrassA; subst WeierstrassB; destruct P; t. Qed. + Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB). - Definition eq (P1 P2:point) := - match coordinates P1, coordinates P2 with - | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2 - | ∞, ∞ => True - | _, _ => False + Program Definition of_Weierstrass (P:Wpoint) : point := + match W.coordinates P return F*F+∞ with + | (x,y) => (b*x-a/3, b*y) + | _ => ∞ end. + Next Obligation. + Proof. clear char_ge_3; subst WeierstrassA; subst WeierstrassB; destruct P; t. Qed. - Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_gt_2 WeierstrassA WeierstrassB). - Lemma MontgomeryOfWeierstrass_add P1 P2 : - eq (MontgomeryOfWeierstrass (W.add P1 P2)) - (add (MontgomeryOfWeierstrass P1) (MontgomeryOfWeierstrass P2)). - Proof. - cbv [WeierstrassA WeierstrassB eq MontgomeryOfWeierstrass W.add add coordinates W.coordinates proj1_sig] in *; t. - Qed. + Lemma of_Weierstrass_add P1 P2 : + eq (of_Weierstrass (W.add P1 P2)) + (add (of_Weierstrass P1) (of_Weierstrass P2)). + Proof. cbv [WeierstrassA WeierstrassB eq of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *; clear char_ge_3; t. Qed. Section AddX. Lemma homogeneous_x_differential_addition_releations P1 P2 : @@ -110,30 +102,20 @@ Module M. end. Proof. t. Qed. - Definition onCurve xy := let 'pair x y := xy in b*y^2 = x^3 + a*x^2 + x. - Definition xzpoint := { xz | let 'pair x z := xz in (z = 0 \/ exists y, onCurve (pair (x/z) y)) }. - Definition xzcoordinates (P:xzpoint) : F*F := proj1_sig P. - Program Definition toxz (P:point) : xzpoint := - exist _ - match coordinates P with - | (x, y) => pair x 1 - | ∞ => pair 1 0 - end _. - Next Obligation. t; [right; exists f0; t | left; reflexivity ]. Qed. - - Definition sig_pair_to_pair_sig {T T' I I'} (xy:{xy | let 'pair x y := xy in I x /\ I' y}) - : prod {x:T | I x} {y:T' | I' y} - := let 'exist (pair x y) (conj pfx pfy) := xy in pair (exist _ x pfx) (exist _ y pfy). + Program Definition to_xz (P:point) : F*F := + match coordinates P with + | (x, y) => pair x 1 + | ∞ => pair 1 0 + end. (* From Explicit Formulas Database by Lange and Bernstein, credited to 1987 Montgomery "Speeding the Pollard and elliptic curve methods of factorization", page 261, fifth and sixth displays, plus common-subexpression elimination, plus assumption Z1=1 *) - Context {a24:F} {a24_correct:4*a24 = a+2}. - Definition xzladderstep (X1:F) (P1 P2:xzpoint) : prod xzpoint xzpoint. refine ( - sig_pair_to_pair_sig (exist _ - match xzcoordinates P1, xzcoordinates P2 return _ with + Context {a24:F} {a24_correct:4*a24 = a+2}. (* TODO: +2 or -2 ? *) + Definition xzladderstep (X1:F) (P1 P2:F*F) : ((F*F)*(F*F)) := + match P1, P2 with pair X2 Z2, pair X3 Z3 => let A := X2+Z2 in let AA := A^2 in @@ -149,32 +131,19 @@ Module M. let X4 := AA*BB in let Z4 := E*(BB + a24*E) in (pair (pair X4 Z4) (pair X5 Z5)) - end _) ). - Proof. - destruct P1, P2; cbv [onCurve xzcoordinates] in *. t; intuition idtac. - { left. fsatz. } - { left. fsatz. } - admit. - admit. - admit. - admit. - { right. - admit. (* the following used to work, but slowly: - exists ((fun x1 y1 x2 y2 => (2*x1+x1+a)*(3*x1^2+2*a*x1+1)/(2*b*y1)-b*(3*x1^2+2*a*x1+1)^3/(2*b*y1)^3-y1) (f1/f2) x0 (f/f0) x). - Algebra.common_denominator_in H. - Algebra.common_denominator_in H0. - Algebra.common_denominator. - abstract Algebra.nsatz. - - idtac. - admit. - admit. - admit. - admit. - admit. *) } - { right. - (* exists ((fun x1 y1 x2 y2 => (2*x1+x2+a)*(y2-y1)/(x2-x1)-b*(y2-y1)^3/(x2-x1)^3-y1) (f1/f2) x0 (f/f0) x). *) - (* XXX: this case is probably not true -- there is not necessarily a guarantee that the output x/z is on curve if [X1] was not the x coordinate of the difference of input points as requored *) + end. + + Require Import Crypto.Util.Tuple. + + (* TODO: look up this lemma statement -- the current one may not be right *) + Lemma xzladderstep_to_xz X1 P1 P2 + (HX1 : match coordinates (add P1 (opp P2)) with (x,y) => X1 = x | _ => False end) + : fieldwise (n:=2) (fieldwise (n:=2) Feq) + (xzladderstep X1 (to_xz P1) (to_xz P2)) + (pair (to_xz (add P1 P2)) (to_xz (add P1 P1))). + destruct P1 as [[[??]|?]?], P2 as [[[??]|?]?]; + cbv [fst snd xzladderstep to_xz add coordinates proj1_sig opp fieldwise fieldwise'] in *; + break_match_hyps; break_match; repeat split; try contradiction. Abort. End AddX. End MontgomeryCurve. diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index d19f3f786..87b5bcffd 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -9,7 +9,7 @@ Module W. * <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> (page 79) *) - Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "x =? y" := (Decidable.dec (Feq x y)) (at level 70, no associativity) : type_scope. Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Decidable.dec (Feq x y))) : bool_scope. diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index d31a2319f..717417209 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -19,7 +19,7 @@ Local Open Scope Z. (* BEGIN precomputation. *) -Definition modulus : Z := 2^130 - 5. +Definition modulus : positive := (2^130 - 5)%positive. Lemma prime_modulus : prime modulus. Admitted. Definition int_width := 32%Z. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 361cc83a7..0cea13d43 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -22,7 +22,7 @@ Local Open Scope Z. (* BEGIN precomputation. *) -Definition modulus : Z := Eval compute in 2^255 - 19. +Definition modulus : positive := Eval compute in (2^255 - 19)%positive. Definition prime_modulus : prime modulus := Crypto.Spec.Ed25519.prime_q. Definition int_width := 64%Z. Definition freeze_input_bound := 32%Z. diff --git a/src/Specific/SC25519.v b/src/Specific/SC25519.v index 9d8e7caee..033750453 100644 --- a/src/Specific/SC25519.v +++ b/src/Specific/SC25519.v @@ -11,7 +11,7 @@ Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.WordUtil. Import NPeano. -Local Notation modulusv := (2^252 + 27742317777372353535851937790883648493)%Z. +Local Notation modulusv := (2^252 + 27742317777372353535851937790883648493)%positive. Local Coercion Z.of_nat : nat >-> Z. Local Notation eta x := (fst x, snd x). Local Notation eta3 x := (eta (fst x), snd x). diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v index da4c8c214..58ec8b5bf 100644 --- a/src/WeierstrassCurve/Pre.v +++ b/src/WeierstrassCurve/Pre.v @@ -10,7 +10,7 @@ Local Open Scope core_scope. Section Pre. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))} + {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))} {eq_dec: DecidableRel Feq}. Local Infix "=" := Feq. Local Notation "a <> b" := (not (a = b)). Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. diff --git a/src/WeierstrassCurve/WeierstrassCurveTheorems.v b/src/WeierstrassCurve/WeierstrassCurveTheorems.v index bff8c2bc2..aa444c9ee 100644 --- a/src/WeierstrassCurve/WeierstrassCurveTheorems.v +++ b/src/WeierstrassCurve/WeierstrassCurveTheorems.v @@ -9,8 +9,8 @@ Module W. Section W. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {char_gt_3:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))} - {char_gt_11:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 11%positive} (* FIXME: we shouldn't need this *) + {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))} + {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive} (* FIXME: we shouldn't need this *) {Feq_dec:DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. |