diff options
| -rw-r--r-- | .gitignore | 12 | ||||
| -rw-r--r-- | AUTHORS | 16 | ||||
| -rw-r--r-- | CONTRIBUTORS | 28 | ||||
| -rw-r--r-- | LICENSE | 2 | ||||
| -rw-r--r-- | _CoqProject | 3 | ||||
| -rw-r--r-- | crypto-defects.md | 20 | ||||
| -rw-r--r-- | src/Algebra.v | 193 | ||||
| -rw-r--r-- | src/BaseSystem.v | 3 | ||||
| -rw-r--r-- | src/BaseSystemProofs.v | 8 | ||||
| -rw-r--r-- | src/Encoding/ModularWordEncodingTheorems.v | 6 | ||||
| -rw-r--r-- | src/ModularArithmetic/BarrettReduction/Z.v | 118 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 8 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 28 | ||||
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 4 | ||||
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 4 | ||||
| -rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 10 | ||||
| -rw-r--r-- | src/Spec/WeierstrassCurve.v | 84 | ||||
| -rw-r--r-- | src/Testbit.v | 10 | ||||
| -rw-r--r-- | src/Util/NatUtil.v | 8 | ||||
| -rw-r--r-- | src/Util/NumTheoryUtil.v | 16 | ||||
| -rw-r--r-- | src/Util/Tactics.v | 9 | ||||
| -rw-r--r-- | src/Util/ZUtil.v | 1091 | ||||
| -rw-r--r-- | src/WeierstrassCurve/Pre.v | 57 |
23 files changed, 1274 insertions, 464 deletions
diff --git a/.gitignore b/.gitignore index f88b441c8..b8cf1d4bc 100644 --- a/.gitignore +++ b/.gitignore @@ -1,10 +1,14 @@ -.#* -*~ *# *.aux *.d *.glob -Makefile.bak -Makefile.coq *.vio *.vo +*~ +.#* +Makefile.bak +Makefile.coq +csdp.cache +lia.cache +nlia.cache +nra.cache diff --git a/AUTHORS b/AUTHORS new file mode 100644 index 000000000..31d71c211 --- /dev/null +++ b/AUTHORS @@ -0,0 +1,16 @@ +# This is the official list of fiat-crypto authors for copyright purposes. +# This file is distinct from the CONTRIBUTORS files. +# See the latter for an explanation. + +# Names should be added to this file as one of +# Organization's name +# Individual's name <submission email address> +# Individual's name <submission email address> <email2> <emailN> +# See CONTRIBUTORS for the meaning of multiple email addresses. + +# Please keep the list sorted. + +Andres Erbsen <andreser@mit.edu> +Google Inc. +Jade Philipoom <jadep@mit.edu> <jade.philipoom@gmail.com> +Massachusetts Institute of Technology diff --git a/CONTRIBUTORS b/CONTRIBUTORS new file mode 100644 index 000000000..905edafd1 --- /dev/null +++ b/CONTRIBUTORS @@ -0,0 +1,28 @@ +# This is the official list of people have contributed code to the +# fiat-crypto repository. +# +# The AUTHORS file lists the copyright holders; this file +# lists people. For example, Google employees are listed here +# but not in AUTHORS, because Google holds the copyright. +# +# When adding J Random Contributor's name to this file, +# either J's name or J's organization's name should be +# added to the AUTHORS file, depending on who holds the copyright. +# +# Names should be added to this file like so: +# Individual's name <submission email address> +# Individual's name <submission email address> <email2> <emailN> +# +# An entry with multiple email addresses specifies that the +# first address should be used in the submit logs and +# that the other addresses should be recognized as the +# same person. + +# Please keep the list sorted. + +Adam Chlipala <adamc@csail.mit.edu> <adam@chlipala.net> +Andres Erbsen <andreser@mit.edu> +Daniel Ziegler <dmz@mit.edu> +Jade Philipoom <jadep@mit.edu> <jade.philipoom@gmail.com> +Jason Gross <jgross@mit.edu> <jagro@google.com> <jasongross9@gmail.com> +Robert Sloan <rsloan@mit.edu> <varomodt@gmail.com> <rsloan@sumologic.com> @@ -1,6 +1,6 @@ The MIT License (MIT) -Copyright (c) 2015 Programming Languages and Verification Group at MIT CSAIL +Copyright (c) 2015-2016 the fiat-crypto authors (see the AUTHORS file). Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal diff --git a/_CoqProject b/_CoqProject index 55973017b..f3f07e840 100644 --- a/_CoqProject +++ b/_CoqProject @@ -45,11 +45,13 @@ src/ModularArithmetic/PseudoMersenneBaseParamProofs.v src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/PseudoMersenneBaseRep.v src/ModularArithmetic/Tutorial.v +src/ModularArithmetic/BarrettReduction/Z.v src/Spec/CompleteEdwardsCurve.v src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v +src/Spec/WeierstrassCurve.v src/Specific/GF1305.v src/Specific/GF25519.v src/Tactics/Nsatz.v @@ -68,3 +70,4 @@ src/Util/Tuple.v src/Util/Unit.v src/Util/WordUtil.v src/Util/ZUtil.v +src/WeierstrassCurve/Pre.v diff --git a/crypto-defects.md b/crypto-defects.md new file mode 100644 index 000000000..f8cf52053 --- /dev/null +++ b/crypto-defects.md @@ -0,0 +1,20 @@ +Here is an incomplete list of defects in cryptographic implementations. We +should make sure our verification rules out the possibility of similar mistakes +appearing in our code. + +| Reference | Specification | Implementation | Defect | +| ------------------------------------------------------------------- | --------------------------- | --------------------------- | ------------- | +| [openssl#3607](https://rt.openssl.org/Ticket/Display.html?id=3607) | P256 field element squaring | 64-bit Montgomery form, AMD64 | limb overflow | +| [go#13515](https://github.com/golang/go/issues/13515) | Modular exponentiation | uintptr-sized Montgomery form, Go | carry handling | +| [NaCl ed25519 (p. 2)](https://tweetnacl.cr.yp.to/tweetnacl-20131229.pdf) | F25519 mul, square | 64-bit pseudo-Mersenne, AMD64 | carry handling | +| [openssl#0c687d7e](https://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=dc3c5067cd90f3f2159e5d53c57b92730c687d7e;ds=sidebyside) | Poly1305 | 32-bit pseudo-Mersenne, x86 and ARM | bad truncation | +| [openssl#ef5c9b11](https://github.com/openssl/openssl/commit/29851264f11ccc70c6c0140d7e3d8d93ef5c9b11) | Modular exponentiation | 64-bit Montgomery form, AMD64 | carry handling | +| [nettle#09e3ce4d](https://git.lysator.liu.se/nettle/nettle/commit/c71d2c9d20eeebb985e3872e4550137209e3ce4d) | secp-256r1 modular reduction | | carry handling | +| [socat#7](http://www.dest-unreach.org/socat/contrib/socat-secadv7.html) | DH in Z*p | irrelevant | non-prime p | +| [invalid-curve](http://euklid.org/pdf/ECC_Invalid_Curve.pdf) | NIST ECDH | irrelevant | not onCurve | +| [donna#8edc799f](https://github.com/agl/curve25519-donna/commit/2647eeba59fb628914c79ce691df794a8edc799f) | F25519 internal to wire | 32-bit pseudo-Mersenne, C | non-canonical | +| [end-to-end#340](https://github.com/google/end-to-end/issues/340) | Curve25519 library | twisted Edwards coordinates | (0, 1) = ∞ | +| [CVE-2006-4339](https://web.archive.org/web/20071010042708/http://www.imc.org/ietf-openpgp/mail-archive/msg14307.html) | RSA-PKCS-1 sig. verification | irrelevant | padding check | +| [CVE-2014-3570](https://www.openssl.org/news/secadv/20150108.txt) | Bignum squaring | | | + +Not covered in the above list: memory mismanagement (buffer overrun, use-after-free, uninitialized read, null dereference), timing attacks (branch, cache, instruction). While these issues are very important, there are good programming disciplines for avoiding them without verifying intricate details of the computation. diff --git a/src/Algebra.v b/src/Algebra.v index eca1b2bb1..62b216b92 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -711,36 +711,26 @@ Ltac deduplicate_nonfraction_pieces mul := => subst x0 x1 end. -Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac cont := +Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div cont := idtac; let one_arg_recr := fun op v => set_nonfraction_pieces_on - v eq zero opp add sub mul inv div nonzero_tac + v eq zero opp add sub mul inv div ltac:(fun x => cont (op x)) in let two_arg_recr := fun op v0 v1 => set_nonfraction_pieces_on - v0 eq zero opp add sub mul inv div nonzero_tac + v0 eq zero opp add sub mul inv div ltac:(fun x => set_nonfraction_pieces_on - v1 eq zero opp add sub mul inv div nonzero_tac + v1 eq zero opp add sub mul inv div ltac:(fun y => cont (op x y))) in lazymatch T with | eq ?x ?y => two_arg_recr eq x y | appcontext[div] => lazymatch T with - | div ?numerator ?denominator - => let d := fresh "d" in - pose denominator as d; - cut (not (eq d zero)); - [ intro; - set_nonfraction_pieces_on - numerator eq zero opp add sub mul inv div nonzero_tac - ltac:(fun numerator' - => cont (div numerator' d)) - | subst d; nonzero_tac ] | opp ?x => one_arg_recr opp x | inv ?x => one_arg_recr inv x | add ?x ?y => two_arg_recr add x y @@ -753,32 +743,32 @@ Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac con pose T as x; cont x end. -Ltac set_nonfraction_pieces_in_by H nonzero_tac := +Ltac set_nonfraction_pieces_in H := idtac; let fld := guess_field in lazymatch type of fld with | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div => let T := type of H in set_nonfraction_pieces_on - T eq zero opp add sub mul inv div nonzero_tac + T eq zero opp add sub mul inv div ltac:(fun T' => change T' in H); deduplicate_nonfraction_pieces mul end. -Ltac set_nonfraction_pieces_by nonzero_tac := +Ltac set_nonfraction_pieces := idtac; let fld := guess_field in lazymatch type of fld with | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div => let T := get_goal in set_nonfraction_pieces_on - T eq zero opp add sub mul inv div nonzero_tac + T eq zero opp add sub mul inv div ltac:(fun T' => change T'); deduplicate_nonfraction_pieces mul end. -Ltac set_nonfraction_pieces_in H := - set_nonfraction_pieces_in_by H ltac:(try (intro; field_nonzero_mul_split; try tauto)). -Ltac set_nonfraction_pieces := - set_nonfraction_pieces_by ltac:(try (intro; field_nonzero_mul_split; tauto)). +Ltac default_conservative_common_denominator_nonzero_tac := + repeat apply conj; + try first [ assumption + | intro; field_nonzero_mul_split; tauto ]. Ltac conservative_common_denominator_in H := idtac; let fld := guess_field in @@ -789,10 +779,9 @@ Ltac conservative_common_denominator_in H := lazymatch type of H with | appcontext[div] => set_nonfraction_pieces_in H; - [ common_denominator_in H; - [ - | repeat apply conj; try assumption.. ] - | .. ]; + common_denominator_in H; + [ + | default_conservative_common_denominator_nonzero_tac.. ]; repeat match goal with H := _ |- _ => subst H end | ?T => fail 0 "no division in" H ":" T end. @@ -806,10 +795,9 @@ Ltac conservative_common_denominator := lazymatch goal with | |- appcontext[div] => set_nonfraction_pieces; - [ common_denominator; - [ - | repeat apply conj; try assumption.. ] - | .. ]; + common_denominator; + [ + | default_conservative_common_denominator_nonzero_tac.. ]; repeat match goal with H := _ |- _ => subst H end | |- ?G => fail 0 "no division in goal" G @@ -846,14 +834,30 @@ Ltac conservative_common_denominator_inequality := | let HG := fresh in intros HG; apply H'; conservative_common_denominator_in HG; [ eexact HG | .. ] ]. +Ltac conservative_common_denominator_hyps := + try match goal with + | [H: _ |- _ ] + => progress conservative_common_denominator_in H; + [ conservative_common_denominator_hyps + | .. ] + end. + +Ltac conservative_common_denominator_inequality_hyps := + try match goal with + | [H: _ |- _ ] + => progress conservative_common_denominator_inequality_in H; + [ conservative_common_denominator_inequality_hyps + | .. ] + end. + Ltac conservative_common_denominator_all := try conservative_common_denominator; - [ repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_in H; [] end + [ try conservative_common_denominator_hyps | .. ]. Ltac conservative_common_denominator_inequality_all := try conservative_common_denominator_inequality; - [ repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_inequality_in H; [] end + [ try conservative_common_denominator_inequality_hyps | .. ]. Ltac conservative_common_denominator_equality_inequality_all := @@ -878,19 +882,41 @@ Ltac field_simplify_eq_hyps := Ltac field_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq. -(** Clear duplicate hypotheses, and hypotheses of the form [R x x] for a reflexive relation [R] *) +(** Clear duplicate hypotheses, and hypotheses of the form [R x x] for a reflexive relation [R], and similarly for symmetric relations *) Ltac clear_algebraic_duplicates_step R := match goal with | [ H : R ?x ?x |- _ ] => clear H end. +Ltac clear_algebraic_duplicates_step_S R := + match goal with + | [ H : R ?x ?y, H' : R ?y ?x |- _ ] + => clear H + | [ H : not (R ?x ?y), H' : not (R ?y ?x) |- _ ] + => clear H + | [ H : (R ?x ?y -> False)%type, H' : (R ?y ?x -> False)%type |- _ ] + => clear H + | [ H : not (R ?x ?y), H' : (R ?y ?x -> False)%type |- _ ] + => clear H + end. Ltac clear_algebraic_duplicates_guarded R := let test_reflexive := constr:(_ : Reflexive R) in repeat clear_algebraic_duplicates_step R. +Ltac clear_algebraic_duplicates_guarded_S R := + let test_symmetric := constr:(_ : Symmetric R) in + repeat clear_algebraic_duplicates_step_S R. Ltac clear_algebraic_duplicates := clear_duplicates; repeat match goal with - | [ H : ?R ?x ?x |- _ ] => clear_algebraic_duplicates_guarded R + | [ H : ?R ?x ?x |- _ ] => progress clear_algebraic_duplicates_guarded R + | [ H : ?R ?x ?y, H' : ?R ?y ?x |- _ ] + => progress clear_algebraic_duplicates_guarded_S R + | [ H : not (?R ?x ?y), H' : not (?R ?y ?x) |- _ ] + => progress clear_algebraic_duplicates_guarded_S R + | [ H : not (?R ?x ?y), H' : (?R ?y ?x -> False)%type |- _ ] + => progress clear_algebraic_duplicates_guarded_S R + | [ H : (?R ?x ?y -> False)%type, H' : (?R ?y ?x -> False)%type |- _ ] + => progress clear_algebraic_duplicates_guarded_S R end. (*** Inequalities over fields *) @@ -1006,16 +1032,43 @@ Ltac nsatz_inequality_to_equality := | [ H : not (?R ?x ?zero) |- False ] => apply H | [ H : (?R ?x ?zero -> False)%type |- False ] => apply H end. +(** Clean up tactic handling side-conditions *) +Ltac super_nsatz_post_clean_inequalities := + repeat (apply conj || split_field_inequalities); + try assumption; + prensatz_contradict; nsatz_inequality_to_equality; + try nsatz. +Ltac nsatz_equality_to_inequality_by_decide_equality := + lazymatch goal with + | [ H : not (?R _ _) |- ?R _ _ ] => idtac + | [ H : (?R _ _ -> False)%type |- ?R _ _ ] => idtac + | [ |- ?R _ _ ] => fail 0 "No hypothesis exists which negates the relation" R + | [ |- ?G ] => fail 0 "The goal is not a binary relation:" G + end; + lazymatch goal with + | [ |- ?R ?x ?y ] + => destruct (@dec (R x y) _); [ assumption | exfalso ] + end. (** Handles inequalities and fractions *) -Ltac super_nsatz := +Ltac super_nsatz_internal nsatz_alternative := (* [nsatz] gives anomalies on duplicate hypotheses, so we strip them *) clear_algebraic_duplicates; prensatz_contradict; (* Each goal left over by [prensatz_contradict] is separate (and there might not be any), so we handle them all separately *) [ try conservative_common_denominator_equality_inequality_all; - [ try nsatz_inequality_to_equality; try nsatz - | repeat (apply conj || split_field_inequalities); try assumption; prensatz_contradict; nsatz_inequality_to_equality; try nsatz.. ].. ]. + [ try nsatz_inequality_to_equality; + try first [ nsatz; + (* [nstaz] might leave over side-conditions; we handle them if they are inequalities *) + try super_nsatz_post_clean_inequalities + | nsatz_alternative ] + | super_nsatz_post_clean_inequalities.. ].. ]. + +Ltac super_nsatz := + super_nsatz_internal + (* if [nsatz] fails, we try turning the goal equality into an inequality and trying again *) + ltac:(nsatz_equality_to_inequality_by_decide_equality; + super_nsatz_internal idtac). Section ExtraLemmas. Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. @@ -1023,13 +1076,11 @@ Section ExtraLemmas. Local Notation "0" := zero. Local Notation "1" := one. Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Example _only_two_square_roots_test x y : x * x = y * y -> x <> opp y -> x = y. + Proof. intros; super_nsatz. Qed. + Lemma only_two_square_roots' x y : x * x = y * y -> x <> y -> x <> opp y -> False. - Proof. - intros. - canonicalize_field_equalities; canonicalize_field_inequalities. - assert (H' : (x + y) * (x - y) <> 0) by (apply mul_nonzero_nonzero; assumption). - apply H'; nsatz. - Qed. + Proof. intros; super_nsatz. Qed. Lemma only_two_square_roots x y z : x * x = z -> y * y = z -> x <> y -> x <> opp y -> False. Proof. @@ -1051,17 +1102,37 @@ Section ExtraLemmas. End ExtraLemmas. (** We look for hypotheses of the form [x^2 = y^2] and [x^2 = z] together with [y^2 = z], and prove that [x = y] or [x = opp y] *) -Ltac pose_proof_only_two_square_roots x y H := +Ltac pose_proof_only_two_square_roots x y H eq opp mul := not constr_eq x y; - match goal with - | [ H' : ?eq (?mul x x) (?mul y y) |- _ ] - => pose proof (only_two_square_roots'_choice x y H') as H - | [ H0 : ?eq (?mul x x) ?z, H1 : ?eq (?mul y y) ?z |- _ ] - => pose proof (only_two_square_roots_choice x y z H0 H1) as H + lazymatch x with + | opp ?x' => pose_proof_only_two_square_roots x' y H eq opp mul + | _ + => lazymatch y with + | opp ?y' => pose_proof_only_two_square_roots x y' H eq opp mul + | _ + => match goal with + | [ H' : eq x y |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq y x |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq x (opp y) |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq y (opp x) |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq (opp x) y |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq (opp y) x |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq (mul x x) (mul y y) |- _ ] + => pose proof (only_two_square_roots'_choice x y H') as H + | [ H0 : eq (mul x x) ?z, H1 : eq (mul y y) ?z |- _ ] + => pose proof (only_two_square_roots_choice x y z H0 H1) as H + end + end end. -Ltac reduce_only_two_square_roots x y := +Ltac reduce_only_two_square_roots x y eq opp mul := let H := fresh in - pose_proof_only_two_square_roots x y H; + pose_proof_only_two_square_roots x y H eq opp mul; destruct H; try setoid_subst y. Ltac pre_clean_only_two_square_roots := @@ -1075,21 +1146,25 @@ Ltac post_clean_only_two_square_roots x y := | [ H : (?R ?x ?x -> False)%type |- _ ] => exfalso; apply H; reflexivity end); try setoid_subst x; try setoid_subst y. -Ltac only_two_square_roots_step := +Ltac only_two_square_roots_step eq opp mul := match goal with - | [ H : not (?eq ?x (?opp ?y)) |- _ ] + | [ H : not (eq ?x (opp ?y)) |- _ ] (* this one comes first, because it the procedure is asymmetric with respect to [x] and [y], and this order is more likely to lead to solving goals by contradiction. *) - => is_var x; is_var y; reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y - | [ H : ?eq (?mul ?x ?x) (?mul ?y ?y) |- _ ] - => reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y - | [ H : ?eq (?mul ?x ?x) ?z, H' : ?eq (?mul ?y ?y) ?z |- _ ] - => reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y + => is_var x; is_var y; reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y + | [ H : eq (mul ?x ?x) (mul ?y ?y) |- _ ] + => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y + | [ H : eq (mul ?x ?x) ?z, H' : eq (mul ?y ?y) ?z |- _ ] + => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y end. Ltac only_two_square_roots := pre_clean_only_two_square_roots; - repeat only_two_square_roots_step. + let fld := guess_field in + lazymatch type of fld with + | @field ?F ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div + => repeat only_two_square_roots_step eq opp mul + end. Section Example. Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. diff --git a/src/BaseSystem.v b/src/BaseSystem.v index a37932de0..0ad6c0a03 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -120,7 +120,7 @@ Section PolynomialBaseCoefs. rewrite in_map_iff in *. destruct H; destruct H. subst. - apply pos_pow_nat_pos. + apply Z.pos_pow_nat_pos. Qed. Lemma poly_base_defn : forall i, (i < length poly_base)%nat -> @@ -145,7 +145,6 @@ Section PolynomialBaseCoefs. with (Z.pos b1); auto. rewrite Z_div_mult_full; auto. apply Z.pow_nonzero; intuition. - pose proof (Zgt_pos_0 b1); omega. Qed. Lemma poly_base_good: diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index a0372c60b..eb7f31ba6 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -84,7 +84,7 @@ Section BaseSystemProofs. intros. rewrite nth_default_eq. destruct (nth_in_or_default i base d). - + auto using positive_is_nonzero, base_positive. + + auto using Z.positive_is_nonzero, base_positive. + congruence. Qed. @@ -94,7 +94,7 @@ Section BaseSystemProofs. intros. rewrite nth_default_eq. destruct (nth_in_or_default i base d). - + rewrite <-gt_lt_symmetry; auto using base_positive. + + apply Z.gt_lt; auto using base_positive. + congruence. Qed. @@ -191,7 +191,7 @@ Section BaseSystemProofs. Lemma nth_error_base_nonzero : forall n x, nth_error base n = Some x -> x <> 0. Proof. - eauto using (@nth_error_value_In Z), Zgt0_neq0, base_positive. + eauto using (@nth_error_value_In Z), Z.gt0_neq0, base_positive. Qed. Hint Rewrite plus_0_r. @@ -594,7 +594,7 @@ Section BaseSystemProofs. specialize (H1 i H2); rewrite (Znumtheory.Zmod_div_mod _ _ _ (nth_default_base_pos _ H _) (nth_default_base_pos _ H _) H0) end. - rewrite <-Z.div_mod by (apply positive_is_nonzero, gt_lt_symmetry; auto using nth_default_base_pos). + rewrite <-Z.div_mod by (apply Z.positive_is_nonzero, Z.lt_gt; auto using nth_default_base_pos). reflexivity. Qed. diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v index 41b75e216..033e99665 100644 --- a/src/Encoding/ModularWordEncodingTheorems.v +++ b/src/Encoding/ModularWordEncodingTheorems.v @@ -43,12 +43,12 @@ Section SignBit. pose proof (F_opp_spec x) as opp_spec_x. apply F_eq in opp_spec_x. rewrite FieldToZ_add in opp_spec_x. - rewrite <-opp_spec_x, Z_odd_mod in sign_zero by (pose proof prime_ge_2 m prime_m; omega). - replace (Z.odd m) with true in sign_zero by (destruct (ZUtil.prime_odd_or_2 m prime_m); auto || omega). + rewrite <-opp_spec_x, Z.odd_mod in sign_zero by (pose proof prime_ge_2 m prime_m; omega). + replace (Z.odd m) with true in sign_zero by (destruct (Z.prime_odd_or_2 m prime_m); auto || omega). rewrite Z.odd_add, F_FieldToZ_add_opp, Z.div_same, Bool.xorb_true_r in sign_zero by assumption || omega. apply Bool.xorb_eq. rewrite <-Bool.negb_xorb_l. assumption. Qed. -End SignBit.
\ No newline at end of file +End SignBit. diff --git a/src/ModularArithmetic/BarrettReduction/Z.v b/src/ModularArithmetic/BarrettReduction/Z.v new file mode 100644 index 000000000..8b472d5d8 --- /dev/null +++ b/src/ModularArithmetic/BarrettReduction/Z.v @@ -0,0 +1,118 @@ +(*** Barrett Reduction *) +(** This file implements Barrett Reduction on [Z]. We follow Wikipedia. *) +Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. +Require Import Crypto.Util.ZUtil Crypto.Util.Tactics. + +Local Open Scope Z_scope. + +Section barrett. + Context (n a : Z) + (n_reasonable : n <> 0). + (** Quoting Wikipedia <https://en.wikipedia.org/wiki/Barrett_reduction>: *) + (** In modular arithmetic, Barrett reduction is a reduction + algorithm introduced in 1986 by P.D. Barrett. A naive way of + computing *) + (** [c = a mod n] *) + (** would be to use a fast division algorithm. Barrett reduction is + an algorithm designed to optimize this operation assuming [n] is + constant, and [a < n²], replacing divisions by + multiplications. *) + + (** * General idea *) + Section general_idea. + (** Let [m = 1 / n] be the inverse of [n] as a floating point + number. Then *) + (** [a mod n = a - ⌊a m⌋ n] *) + (** where [⌊ x ⌋] denotes the floor function. The result is exact, + as long as [m] is computed with sufficient accuracy. *) + + (* [/] is [Z.div], which means truncated division *) + Local Notation "⌊am⌋" := (a / n) (only parsing). + + Theorem naive_barrett_reduction_correct + : a mod n = a - ⌊am⌋ * n. + Proof. + apply Zmod_eq_full; assumption. + Qed. + End general_idea. + + (** * Barrett algorithm *) + Section barrett_algorithm. + (** Barrett algorithm is a fixed-point analog which expresses + everything in terms of integers. Let [k] be the smallest + integer such that [2ᵏ > n]. Think of [n] as representing the + fixed-point number [n 2⁻ᵏ]. We precompute [m] such that [m = + ⌊4ᵏ / n⌋]. Then [m] represents the fixed-point number + [m 2⁻ᵏ ≈ (n 2⁻ᵏ)⁻¹]. *) + (** N.B. We don't need [k] to be the smallest such integer. *) + Context (k : Z) + (k_good : n < 2 ^ k) + (m : Z) + (m_good : m = 4^k / n). (* [/] is [Z.div], which is truncated *) + (** Wikipedia neglects to mention non-negativity, but we need it. + It might be possible to do with a relaxed assumption, such as + the sign of [a] and the sign of [n] being the same; but I + figured it wasn't worth it. *) + Context (n_pos : 0 < n) (* or just [0 <= n], since we have [n <> 0] above *) + (a_nonneg : 0 <= a). + + Lemma k_nonnegative : 0 <= k. + Proof. + destruct (Z_lt_le_dec k 0); try assumption. + rewrite !Z.pow_neg_r in * by lia; lia. + Qed. + + (** Now *) + Let q := (m * a) / 4^k. + Let r := a - q * n. + (** Because of the floor function (in Coq, because [/] means + truncated division), [q] is an integer and [r ≡ a mod n]. *) + Theorem barrett_reduction_equivalent + : r mod n = a mod n. + Proof. + subst r q m. + rewrite <- !Z.add_opp_r, !Zopp_mult_distr_l, !Z_mod_plus_full by assumption. + reflexivity. + Qed. + + Lemma qn_small + : q * n <= a. + Proof. + pose proof k_nonnegative; subst q r m. + assert (0 <= 2^(k-1)) by zero_bounds. + Z.simplify_fractions_le. + Qed. + + (** Also, if [a < n²] then [r < 2n]. *) + (** N.B. It turns out that it is sufficient to assume [a < 4ᵏ]. *) + Context (a_small : a < 4^k). + Lemma r_small : r < 2 * n. + Proof. + Hint Rewrite (Z.div_small a (4^k)) (Z.mod_small a (4^k)) using lia : zsimplify. + Hint Rewrite (Z.mul_div_eq' a n) using lia : zstrip_div. + cut (r + 1 <= 2 * n); [ lia | ]. + pose proof k_nonnegative; subst r q m. + assert (0 <= 2^(k-1)) by zero_bounds. + assert (4^k <> 0) by auto with zarith lia. + assert (a mod n < n) by auto with zarith lia. + pose proof (Z.mod_pos_bound (a * 4^k / n) (4^k)). + transitivity (a - (a * 4 ^ k / n - a) / 4 ^ k * n + 1). + { rewrite <- (Z.mul_comm a); auto 6 with zarith lia. } + rewrite (Z_div_mod_eq (_ * 4^k / n) (4^k)) by lia. + autorewrite with push_Zmul push_Zopp zsimplify zstrip_div. + break_match; auto with lia. + Qed. + + (** In that case, we have *) + Theorem barrett_reduction_small + : a mod n = if r <? n + then r + else r - n. + Proof. + pose proof r_small. pose proof qn_small. + destruct (r <? n) eqn:rlt; Z.ltb_to_lt. + { symmetry; apply (Zmod_unique a n q); subst r; lia. } + { symmetry; apply (Zmod_unique a n (q + 1)); subst r; lia. } + Qed. + End barrett_algorithm. +End barrett. diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index bb9b1674e..ce11b157b 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -22,7 +22,7 @@ Definition Z_div_opt := Eval compute in Z.div. Definition Z_pow_opt := Eval compute in Z.pow. Definition Z_opp_opt := Eval compute in Z.opp. Definition Z_shiftl_opt := Eval compute in Z.shiftl. -Definition Z_shiftl_by_opt := Eval compute in Z_shiftl_by. +Definition Z_shiftl_by_opt := Eval compute in Z.shiftl_by. Definition nth_default_opt {A} := Eval compute in @nth_default A. Definition set_nth_opt {A} := Eval compute in @set_nth A. @@ -502,11 +502,11 @@ Section Multiplication. cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros ext_base reduce]. rewrite <- mul'_opt_correct. change @base with base_opt. - rewrite map_shiftl by apply k_nonneg. + rewrite Z.map_shiftl by apply k_nonneg. rewrite c_subst. rewrite k_subst. change @map with @map_opt. - change @Z_shiftl_by with @Z_shiftl_by_opt. + change @Z.shiftl_by with @Z_shiftl_by_opt. reflexivity. Defined. @@ -671,4 +671,4 @@ Section Canonicalization. auto using freeze_opt_preserves_rep. Qed. -End Canonicalization.
\ No newline at end of file +End Canonicalization. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 75806f570..29612d900 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -170,7 +170,7 @@ Section PseudoMersenneProofs. rewrite Z.sub_sub_distr, Z.sub_diag. simpl. rewrite Z.mul_comm. - rewrite mod_mult_plus; auto using modulus_nonzero. + rewrite Z.mod_add_l; auto using modulus_nonzero. rewrite <- Zplus_mod; auto. Qed. @@ -390,8 +390,8 @@ Section CarryProofs. rewrite nth_default_base_succ by omega. rewrite Z.mul_assoc. rewrite (Z.mul_comm _ (2 ^ log_cap i)). - rewrite mul_div_eq; try ring. - apply gt_lt_symmetry. + rewrite Z.mul_div_eq; try ring. + apply Z.gt_lt_iff. apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg. Qed. @@ -423,7 +423,7 @@ Section CarryProofs. rewrite <- Z.add_opp_l, <- Z.opp_sub_distr. unfold pow2_mod. rewrite Z.land_ones by apply log_cap_nonneg. - rewrite <- mul_div_eq by (apply gt_lt_symmetry; apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg). + rewrite <- Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg). rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. rewrite Zopp_mult_distr_r. rewrite Z.mul_comm. @@ -570,7 +570,7 @@ Section CanonicalizationProofs. Lemma max_bound_pos : forall i, (i < length base)%nat -> 0 < max_bound i. Proof. - unfold max_bound, log_cap; intros; apply Z_ones_pos_pos. + unfold max_bound, log_cap; intros; apply Z.ones_pos_pos. apply limb_widths_pos. rewrite nth_default_eq. apply nth_In. @@ -580,7 +580,7 @@ Section CanonicalizationProofs. Lemma max_bound_nonneg : forall i, 0 <= max_bound i. Proof. - unfold max_bound; intros; auto using Z_ones_nonneg. + unfold max_bound; intros; auto using Z.ones_nonneg. Qed. Local Hint Resolve max_bound_nonneg. @@ -939,7 +939,7 @@ Section CanonicalizationProofs. apply Z.add_le_mono. + apply carry_bounds_0_upper; auto; omega. + apply Z.mul_le_mono_pos_l; auto using c_pos. - apply Z_shiftr_ones; auto; + apply Z.shiftr_ones; auto; [ | pose proof (B_compat_log_cap (pred (length base))); omega ]. split. - apply carry_bounds_lower; auto; omega. @@ -978,7 +978,7 @@ Section CanonicalizationProofs. + rewrite <-max_bound_log_cap, <-Z.add_1_l. apply Z.add_le_mono. - rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. - apply Z_div_floor; auto. + apply Z.div_floor; auto. destruct i. * simpl. eapply Z.le_lt_trans; [ apply carry_full_bounds_0; auto | ]. @@ -1061,7 +1061,7 @@ Section CanonicalizationProofs. + rewrite <-max_bound_log_cap, <-Z.add_1_l. rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. apply Z.add_le_mono. - - apply Z_div_floor; auto. + - apply Z.div_floor; auto. eapply Z.le_lt_trans; [ eapply carry_full_2_bounds_0; eauto | ]. replace (Z.succ 1) with (2 ^ 1) by ring. rewrite <-max_bound_log_cap. @@ -1267,7 +1267,7 @@ Section CanonicalizationProofs. Lemma max_ones_nonneg : 0 <= max_ones. Proof. unfold max_ones. - apply Z_ones_nonneg. + apply Z.ones_nonneg. pose proof limb_widths_nonneg. induction limb_widths. cbv; congruence. @@ -1282,19 +1282,19 @@ Section CanonicalizationProofs. unfold max_ones. intros ? ? x_range. rewrite Z.land_comm. - rewrite Z.land_ones by apply Z_le_fold_right_max_initial. + rewrite Z.land_ones by apply Z.le_fold_right_max_initial. apply Z.mod_small. split; try omega. eapply Z.lt_le_trans; try eapply x_range. apply Z.pow_le_mono_r; try omega. rewrite log_cap_eq. destruct (lt_dec i (length limb_widths)). - + apply Z_le_fold_right_max. + + apply Z.le_fold_right_max. - apply limb_widths_nonneg. - rewrite nth_default_eq. auto using nth_In. + rewrite nth_default_out_of_bounds by omega. - apply Z_le_fold_right_max_initial. + apply Z.le_fold_right_max_initial. Qed. Lemma full_isFull'_true : forall j us, (length us = length base) -> @@ -1802,7 +1802,7 @@ Section CanonicalizationProofs. + match goal with |- (?a ?= ?b) = (?c ?= ?d) => rewrite (Z.compare_antisym b a); rewrite (Z.compare_antisym d c) end. apply CompOpp_inj; rewrite !CompOpp_involutive. - apply gt_lt_symmetry in Hgt. + apply Z.gt_lt_iff in Hgt. etransitivity; try apply Z_compare_decode_step_lt; auto; omega. Qed. diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 23393d7ef..1504ca0df 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -97,7 +97,7 @@ Section Pow2BaseProofs. Proof. intros. repeat rewrite nth_default_base by omega. - apply mod_same_pow. + apply Z.mod_same_pow. split; [apply sum_firstn_limb_widths_nonneg | ]. destruct (NPeano.Nat.eq_dec i 0); subst. + case_eq limb_widths; intro; unfold sum_firstn; simpl; try omega; intros l' lw_eq. @@ -199,7 +199,7 @@ Section BitwiseDecodeEncode. intros. simpl; f_equal. match goal with H : bounded _ _ |- _ => - rewrite Z_lor_shiftl by (auto; unfold bounded in H; specialize (H i); assumption) end. + rewrite Z.lor_shiftl by (auto; unfold bounded in H; specialize (H i); assumption) end. rewrite Z.shiftl_mul_pow2 by auto. ring. Qed. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 2021e8514..a2f606f30 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -460,8 +460,8 @@ Section SquareRootsPrime5Mod8. apply Z2N.inj_iff; try zero_bounds. rewrite <- Z.mul_cancel_l with (p := 2) by omega. ring_simplify. - rewrite mul_div_eq by omega. - rewrite mul_div_eq by omega. + rewrite Z.mul_div_eq by omega. + rewrite Z.mul_div_eq by omega. rewrite (Zmod_div_mod 2 8 q) by (try omega; apply Zmod_divide; omega || auto). rewrite q_5mod8. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 50c1f3ea6..c07da850f 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -42,7 +42,7 @@ Section PseudoMersenneBaseParamProofs. rewrite (Z.mul_comm r). subst r. assert (i + j - length base < length base)%nat by omega. - rewrite mul_div_eq by (apply gt_lt_symmetry; apply Z.mul_pos_pos; + rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.mul_pos_pos; [ | subst b; unfold base; rewrite nth_default_base; try assumption ]; zero_bounds; auto using sum_firstn_limb_widths_nonneg, limb_widths_nonneg). rewrite (Zminus_0_l_reverse (b i * b j)) at 1. @@ -51,7 +51,7 @@ Section PseudoMersenneBaseParamProofs. unfold base; repeat rewrite nth_default_base by auto. do 2 rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. symmetry. - apply mod_same_pow. + apply Z.mod_same_pow. split. + apply Z.add_nonneg_nonneg; auto using sum_firstn_limb_widths_nonneg. + rewrite base_length, base_from_limb_widths_length in * by auto. @@ -65,7 +65,7 @@ Section PseudoMersenneBaseParamProofs. destruct In_b_base as [i nth_err_b]. apply nth_error_subst in nth_err_b; [ | auto ]. rewrite nth_err_b. - apply gt_lt_symmetry. + apply Z.gt_lt_iff. apply Z.pow_pos_nonneg; omega || auto using sum_firstn_limb_widths_nonneg. Qed. @@ -84,10 +84,10 @@ Section PseudoMersenneBaseParamProofs. unfold base in *. repeat rewrite nth_default_base by (omega || auto). rewrite (Z.mul_comm _ (2 ^ (sum_firstn limb_widths (i+j)))). - rewrite mul_div_eq by (apply gt_lt_symmetry; zero_bounds; + rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; zero_bounds; auto using sum_firstn_limb_widths_nonneg). rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. - rewrite mod_same_pow; try ring. + rewrite Z.mod_same_pow; try ring. split; [ auto using sum_firstn_limb_widths_nonneg | ]. apply limb_widths_good. rewrite <- base_length; assumption. diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v new file mode 100644 index 000000000..7ec5d99ec --- /dev/null +++ b/src/Spec/WeierstrassCurve.v @@ -0,0 +1,84 @@ +Require Crypto.WeierstrassCurve.Pre. + +Module E. + Section WeierstrassCurves. + (* Short Weierstrass curves with addition laws. References: + * <https://hyperelliptic.org/EFD/g1p/auto-shortw.html> + * <https://cr.yp.to/talks/2007.06.07/slides.pdf> + * See also: + * <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> (page 79) + *) + + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Infix "=?" := Algebra.eq_dec (at level 70, no associativity) : type_scope. + Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Algebra.eq_dec x y)) : bool_scope. + Local Infix "+" := Fadd. Local Infix "*" := Fmul. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. + Local Notation "- x" := (Fopp x). + Local Notation "x ^ 2" := (x*x) (at level 30). Local Notation "x ^ 3" := (x*x^2) (at level 30). + Local Notation "'∞'" := unit : type_scope. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "2" := (1+1). Local Notation "3" := (1+2). Local Notation "4" := (1+3). + Local Notation "8" := (1+(1+(1+(1+4)))). Local Notation "12" := (1+(1+(1+(1+8)))). + Local Notation "16" := (1+(1+(1+(1+12)))). Local Notation "20" := (1+(1+(1+(1+16)))). + Local Notation "24" := (1+(1+(1+(1+20)))). Local Notation "27" := (1+(1+(1+24))). + + Local Notation "( x , y )" := (inl (pair x y)). + Local Open Scope core_scope. + + Context {a b: F}. + + (** N.B. We may require more conditions to prove that points form + a group under addition (associativity, in particular. If + that's the case, more fields will be added to this class. *) + Class weierstrass_params := + { + char_gt_2 : 2 <> 0; + char_ne_3 : 3 <> 0; + nonzero_discriminant : -(16) * (4 * a^3 + 27 * b^2) <> 0 + }. + Context `{weierstrass_params}. + + Definition point := { P | match P with + | (x, y) => y^2 = x^3 + a*x + b + | ∞ => True + end }. + Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. + + (** The following points are indeed on the curve -- see [WeierstrassCurve.Pre] for proof *) + Local Obligation Tactic := + try solve [ Program.Tactics.program_simpl + | intros; apply (Pre.unifiedAdd'_onCurve _ _ (proj2_sig _) (proj2_sig _)) ]. + + Program Definition zero : point := ∞. + + Program Definition add (P1 P2:point) : point + := exist + _ + (match coordinates P1, coordinates P2 return _ with + | (x1, y1), (x2, y2) => + if x1 =? x2 then + if y2 =? -y1 then ∞ + else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, + (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) + else ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, + (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) + | ∞, ∞ => ∞ + | ∞, _ => coordinates P2 + | _, ∞ => coordinates P1 + end) + _. + + Fixpoint mul (n:nat) (P : point) : point := + match n with + | O => zero + | S n' => add P (mul n' P) + end. + End WeierstrassCurves. +End E. + +Delimit Scope E_scope with E. +Infix "+" := E.add : E_scope. +Infix "*" := E.mul : E_scope. diff --git a/src/Testbit.v b/src/Testbit.v index 545c3cbce..f9de9092b 100644 --- a/src/Testbit.v +++ b/src/Testbit.v @@ -107,7 +107,7 @@ Proof. rewrite <- nth_default_eq in uniform. erewrite nth_error_value_eq_nth_default in uniform; eauto. subst. - destruct r; [ | apply pos_pow_nat_pos | pose proof (Zlt_neg_0 p) ] ; omega. + destruct r; [ | apply Z.pos_pow_nat_pos | pose proof (Zlt_neg_0 p) ] ; omega. + intros. rewrite nth_default_eq. rewrite uniform; auto. @@ -151,7 +151,7 @@ Proof. induction us; boring. rewrite <- (IHus base) by (omega || eauto using no_overflow_tail). rewrite decode_cons by (eapply uniform_base_BaseVector; eauto; - rewrite gt_lt_symmetry; apply Z_pow_gt0; omega). + rewrite Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega). simpl. f_equal. + symmetry. eapply no_overflow_cons; eauto. @@ -174,12 +174,12 @@ Proof. auto using Z.land_0_l. + destruct i; simpl. - rewrite nth_default_cons. - rewrite Z.shiftr_0_r, Z_land_add_land by omega. + rewrite Z.shiftr_0_r, Z.land_add_land by omega. symmetry; eapply no_overflow_cons; eauto. - rewrite nth_default_cons_S. erewrite IHus; eauto using no_overflow_tail. remember (i * limb_width)%nat as k. - rewrite Z_shiftr_add_shiftl_high; rewrite ?Nat2Z.inj_add; + rewrite Z.shiftr_add_shiftl_high; rewrite ?Nat2Z.inj_add; repeat f_equal; try omega. rewrite Z.land_ones by apply Nat2Z.is_nonneg. apply Z.mod_pos_bound. zero_bounds. @@ -191,7 +191,7 @@ Lemma unfold_bits_testbit : forall limb_width us n, (0 < limb_width)%nat -> Proof. unfold testbit; intros. erewrite unfold_bits_indexing; eauto. - rewrite <- Z_testbit_low by + rewrite <- Z.testbit_low by (split; try apply Nat2Z.inj_lt; pose proof (mod_bound_pos n limb_width); omega). rewrite Z.shiftr_spec by apply Nat2Z.is_nonneg. f_equal. diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index bc2c8425b..0cdfd784f 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,4 +1,5 @@ Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. +Require Import Coq.micromega.Psatz. Import Nat. Local Open Scope nat_scope. @@ -78,3 +79,10 @@ Proof. [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ]. Qed. + +Lemma pow_nonzero a k : a <> 0 -> a ^ k <> 0. +Proof. + intro; induction k; simpl; nia. +Qed. + +Hint Resolve pow_nonzero : arith. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 10ce148b0..c16b87639 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -66,7 +66,7 @@ Qed. Lemma p_odd : Z.odd p = true. Proof. - pose proof (prime_odd_or_2 p prime_p). + pose proof (Z.prime_odd_or_2 p prime_p). destruct H; auto. Qed. @@ -124,12 +124,12 @@ Proof. assert (b mod p <> 0) as b_nonzero. { intuition. rewrite <- Z.pow_2_r in a_square. - rewrite mod_exp_0 in a_square by prime_bound. + rewrite Z.mod_exp_0 in a_square by prime_bound. rewrite <- a_square in a_nonzero. auto. } pose proof (squared_fermat_little b b_nonzero). - rewrite mod_pow in * by prime_bound. + rewrite Z.mod_pow in * by prime_bound. rewrite <- a_square. rewrite Z.mod_mod; prime_bound. Qed. @@ -172,10 +172,10 @@ Proof. intros. destruct (exists_primitive_root_power) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto. destruct (gpow_y a a_range) as [j [j_range pow_y_j]]; clear gpow_y. - rewrite mod_pow in pow_a_x by prime_bound. + rewrite Z.mod_pow in pow_a_x by prime_bound. replace a with (a mod p) in pow_y_j by (apply Z.mod_small; omega). rewrite <- pow_y_j in pow_a_x. - rewrite <- mod_pow in pow_a_x by prime_bound. + rewrite <- Z.mod_pow in pow_a_x by prime_bound. rewrite <- Z.pow_mul_r in pow_a_x by omega. assert (p - 1 | j * x) as divide_mul_j_x. { rewrite <- phi_is_order in y_order. @@ -193,13 +193,13 @@ Proof. rewrite <- Z_div_plus by omega. rewrite Z.mul_comm. rewrite x_id_inv in divide_mul_j_x; auto. - apply (divide_mul_div _ j 2) in divide_mul_j_x; + apply (Z.divide_mul_div _ j 2) in divide_mul_j_x; try (apply prime_pred_divide2 || prime_bound); auto. rewrite <- Zdivide_Zdiv_eq by (auto || omega). rewrite Zplus_diag_eq_mult_2. replace (a mod p) with a in pow_y_j by (symmetry; apply Z.mod_small; omega). rewrite Z_div_mult by omega; auto. - apply divide2_even_iff. + apply Z.divide2_even_iff. apply prime_pred_even. Qed. @@ -281,7 +281,7 @@ Lemma div2_p_1mod4 : forall (p : Z) (prime_p : prime p) (neq_p_2: p <> 2), (p / 2) * 2 + 1 = p. Proof. intros. - destruct (prime_odd_or_2 p prime_p); intuition. + destruct (Z.prime_odd_or_2 p prime_p); intuition. rewrite <- Zdiv2_div. pose proof (Zdiv2_odd_eqn p); break_if; congruence || omega. Qed. diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index abfc2499c..304ae3c20 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -229,6 +229,15 @@ Ltac destruct_sig_matcher HT := Ltac destruct_sig := destruct_all_matches destruct_sig_matcher. Ltac destruct_sig' := destruct_all_matches' destruct_sig_matcher. +(** try to specialize all non-dependent hypotheses using [tac] *) +Ltac specialize_by' tac := + idtac; + match goal with + | [ H : ?A -> ?B |- _ ] => let H' := fresh in assert (H' : A) by tac; specialize (H H'); clear H' + end. + +Ltac specialize_by tac := repeat specialize_by' tac. + (** If [tac_in H] operates in [H] and leaves side-conditions before the original goal, then [side_conditions_before_to_side_conditions_after tac_in H] does diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 5ea174577..6a452169c 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1,206 +1,250 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. -Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. +Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil. Require Import Coq.Lists.List. Import Nat. Local Open Scope Z. -Lemma gt_lt_symmetry: forall n m, n > m <-> m < n. -Proof. - intros; split; omega. -Qed. +Hint Extern 1 => lia : lia. +Hint Extern 1 => lra : lra. +Hint Extern 1 => nia : nia. +Hint Extern 1 => omega : omega. +Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l : zarith. +Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) : zarith. + +(** Only hints that are always safe to apply (i.e., reversible), and + which can reasonably be said to "simplify" the goal, should go in + this database. *) +Create HintDb zsimplify discriminated. +Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r : zsimplify. +Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add using lia : zsimplify. + +(** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *) +Create HintDb push_Zopp discriminated. +Create HintDb pull_Zopp discriminated. +Hint Rewrite Z.div_opp_l_nz Z.div_opp_l_z using lia : pull_Zopp. +Hint Rewrite Z.mul_opp_l : pull_Zopp. +Hint Rewrite <- Z.opp_add_distr : pull_Zopp. +Hint Rewrite <- Z.div_opp_l_nz Z.div_opp_l_z using lia : push_Zopp. +Hint Rewrite <- Z.mul_opp_l : push_Zopp. +Hint Rewrite Z.opp_add_distr : push_Zopp. + +Create HintDb push_Zmul discriminated. +Create HintDb pull_Zmul discriminated. +Hint Rewrite Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : push_Zmul. +Hint Rewrite <- Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : pull_Zmul. + +(** For the occasional lemma that can remove the use of [Z.div] *) +Create HintDb zstrip_div. +Hint Rewrite Z.div_small_iff using lia : zstrip_div. + +(** It's not clear that [mod] is much easier for [lia] than [Z.div], + so we separate out the transformations between [mod] and [div]. + We'll put, e.g., [mul_div_eq] into it below. *) +Create HintDb zstrip_div. + +Module Z. + Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0. + Proof. intros; omega. Qed. + + Hint Resolve positive_is_nonzero : zarith. + + Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 -> + a / b > 0. + Proof. + intros; rewrite Z.gt_lt_iff. + apply Z.div_str_pos. + split; intuition. + apply Z.divide_pos_le; try (apply Zmod_divide); omega. + Qed. -Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0. -Proof. - intros; omega. -Qed. -Hint Resolve positive_is_nonzero. + Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m. + Proof. intros; subst; auto. Qed. -Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 -> - a / b > 0. -Proof. - intros; rewrite gt_lt_symmetry. - apply Z.div_str_pos. - split; intuition. - apply Z.divide_pos_le; try (apply Zmod_divide); omega. -Qed. + Hint Resolve elim_mod : zarith. -Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m. -Proof. - intros; subst; auto. -Qed. -Hint Resolve elim_mod. + Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b. + Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Hint Rewrite mod_add_l using lia : zsimplify. -Lemma mod_mult_plus: forall a b c, (b <> 0) -> (a * b + c) mod b = c mod b. -Proof. - intros. - rewrite Zplus_mod. - rewrite Z.mod_mul; auto; simpl. - rewrite Zmod_mod; auto. -Qed. + Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b. + Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a. + Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. + Hint Rewrite mod_add' mod_add_l' using lia : zsimplify. -Lemma pos_pow_nat_pos : forall x n, - Z.pos x ^ Z.of_nat n > 0. - do 2 (intros; induction n; subst; simpl in *; auto with zarith). - rewrite <- Pos.add_1_r, Zpower_pos_is_exp. - apply Zmult_gt_0_compat; auto; reflexivity. -Qed. + Lemma pos_pow_nat_pos : forall x n, + Z.pos x ^ Z.of_nat n > 0. + Proof. + do 2 (intros; induction n; subst; simpl in *; auto with zarith). + rewrite <- Pos.add_1_r, Zpower_pos_is_exp. + apply Zmult_gt_0_compat; auto; reflexivity. + Qed. -Lemma Z_div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a. - intros. rewrite Z.mul_comm. apply Z.div_mul; auto. -Qed. + Lemma div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a. + Proof. intros. rewrite Z.mul_comm. apply Z.div_mul; auto. Qed. + Hint Rewrite div_mul' using lia : zsimplify. -Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0. - intuition. -Qed. + (** TODO: Should we get rid of this duplicate? *) + Notation gt0_neq0 := positive_is_nonzero (only parsing). -Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> - ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. -Proof. - intros; induction n; try reflexivity. - rewrite Nat2Z.inj_succ. - rewrite pow_succ_r by apply le_0_n. - rewrite Z.pow_succ_r by apply Zle_0_nat. - rewrite IHn. - rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg. -Qed. + Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> + ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. + Proof. + intros; induction n; try reflexivity. + rewrite Nat2Z.inj_succ. + rewrite pow_succ_r by apply le_0_n. + rewrite Z.pow_succ_r by apply Zle_0_nat. + rewrite IHn. + rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg. + Qed. -Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 -> - a ^ x mod m = 0. -Proof. - intros. - replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega). - induction (Z.to_nat x). { - simpl in *; omega. - } { - rewrite Nat2Z.inj_succ in *. - rewrite Z.pow_succ_r by omega. - rewrite Z.mul_mod by omega. - case_eq n; intros. { - subst. simpl. - rewrite Zmod_1_l by omega. - rewrite H1. - apply Zmod_0_l. + Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n. + Proof with auto using Zle_0_nat, Z.pow_nonneg. + intros; apply Z2Nat.inj... + rewrite <- pow_Z2N_Zpow, !Nat2Z.id... + Qed. + + Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 -> + a ^ x mod m = 0. + Proof. + intros. + replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega). + induction (Z.to_nat x). { + simpl in *; omega. } { - subst. - rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega). - rewrite H1. - auto. + rewrite Nat2Z.inj_succ in *. + rewrite Z.pow_succ_r by omega. + rewrite Z.mul_mod by omega. + case_eq n; intros. { + subst. simpl. + rewrite Zmod_1_l by omega. + rewrite H1. + apply Zmod_0_l. + } { + subst. + rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega). + rewrite H1. + auto. + } } - } -Qed. + Qed. -Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) -> - a ^ b mod m = (a mod m) ^ b mod m. -Proof. - intros; rewrite <- (Z2Nat.id b) by auto. - induction (Z.to_nat b); auto. - rewrite Nat2Z.inj_succ. - do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg. - rewrite Z.mul_mod by auto. - rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto. - rewrite <- IHn by auto. - rewrite Z.mod_mod by auto. - reflexivity. -Qed. + Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) -> + a ^ b mod m = (a mod m) ^ b mod m. + Proof. + intros; rewrite <- (Z2Nat.id b) by auto. + induction (Z.to_nat b); auto. + rewrite Nat2Z.inj_succ. + do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg. + rewrite Z.mul_mod by auto. + rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto. + rewrite <- IHn by auto. + rewrite Z.mod_mod by auto. + reflexivity. + Qed. -Ltac Zdivide_exists_mul := let k := fresh "k" in -match goal with -| [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H] -| [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides -end; (omega || auto). + Ltac divide_exists_mul := let k := fresh "k" in + match goal with + | [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H] + | [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides + end; (omega || auto). -Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0), - (a | b * (a / c)) -> (c | a) -> (c | b). -Proof. - intros ? ? ? ? ? divide_a divide_c_a; do 2 Zdivide_exists_mul. - rewrite divide_c_a in divide_a. - rewrite Z_div_mul' in divide_a by auto. - replace (b * k) with (k * b) in divide_a by ring. - replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring. - rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition). - eapply Zdivide_intro; eauto. -Qed. + Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0), + (a | b * (a / c)) -> (c | a) -> (c | b). + Proof. + intros ? ? ? ? ? divide_a divide_c_a; do 2 divide_exists_mul. + rewrite divide_c_a in divide_a. + rewrite div_mul' in divide_a by auto. + replace (b * k) with (k * b) in divide_a by ring. + replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring. + rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition). + eapply Zdivide_intro; eauto. + Qed. -Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true. -Proof. - intro; split. { - intro divide2_n. - Zdivide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega]. - rewrite divide2_n. - apply Z.even_mul. - } { - intro n_even. - pose proof (Zmod_even n). - rewrite n_even in H. - apply Zmod_divide; omega || auto. - } -Qed. + Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true. + Proof. + intro; split. { + intro divide2_n. + divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega]. + rewrite divide2_n. + apply Z.even_mul. + } { + intro n_even. + pose proof (Zmod_even n). + rewrite n_even in H. + apply Zmod_divide; omega || auto. + } + Qed. -Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true. -Proof. - intros. - apply Decidable.imp_not_l; try apply Z.eq_decidable. - intros p_neq2. - pose proof (Zmod_odd p) as mod_odd. - destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto. - rewrite p_not_odd in mod_odd. - apply Zmod_divides in mod_odd; try omega. - destruct mod_odd as [c c_id]. - rewrite Z.mul_comm in c_id. - apply Zdivide_intro in c_id. - apply prime_divisors in c_id; auto. - destruct c_id; [omega | destruct H; [omega | destruct H; auto]]. - pose proof (prime_ge_2 p prime_p); omega. -Qed. + Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true. + Proof. + intros. + apply Decidable.imp_not_l; try apply Z.eq_decidable. + intros p_neq2. + pose proof (Zmod_odd p) as mod_odd. + destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto. + rewrite p_not_odd in mod_odd. + apply Zmod_divides in mod_odd; try omega. + destruct mod_odd as [c c_id]. + rewrite Z.mul_comm in c_id. + apply Zdivide_intro in c_id. + apply prime_divisors in c_id; auto. + destruct c_id; [omega | destruct H; [omega | destruct H; auto]]. + pose proof (prime_ge_2 p prime_p); omega. + Qed. -Lemma mul_div_eq : (forall a m, m > 0 -> m * (a / m) = (a - a mod m))%Z. -Proof. - intros. - rewrite (Z_div_mod_eq a m) at 2 by auto. - ring. -Qed. + Lemma mul_div_eq : forall a m, m > 0 -> m * (a / m) = (a - a mod m). + Proof. + intros. + rewrite (Z_div_mod_eq a m) at 2 by auto. + ring. + Qed. -Ltac prime_bound := match goal with -| [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega -end. + Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z. + Proof. + intros. + rewrite (Z_div_mod_eq a m) at 2 by auto. + ring. + Qed. -Lemma Zlt_minus_lt_0 : forall n m, m < n -> 0 < n - m. -Proof. - intros; omega. -Qed. + Hint Rewrite mul_div_eq mul_div_eq' using lia : zdiv_to_mod. + Hint Rewrite <- mul_div_eq' using lia : zmod_to_div. + Ltac prime_bound := match goal with + | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega + end. -Lemma Z_testbit_low : forall n x i, (0 <= i < n) -> - Z.testbit x i = Z.testbit (Z.land x (Z.ones n)) i. -Proof. - intros. - rewrite Z.land_ones by omega. - symmetry. - apply Z.mod_pow2_bits_low. - omega. -Qed. + Lemma testbit_low : forall n x i, (0 <= i < n) -> + Z.testbit x i = Z.testbit (Z.land x (Z.ones n)) i. + Proof. + intros. + rewrite Z.land_ones by omega. + symmetry. + apply Z.mod_pow2_bits_low. + omega. + Qed. -Lemma Z_testbit_add_shiftl_low : forall i a b n, (0 <= i < n) -> - Z.testbit (a + Z.shiftl b n) i = Z.testbit a i. -Proof. - intros. - erewrite Z_testbit_low; eauto. - rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega. - rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega). - apply Z.mod_pow2_bits_low. - omega. -Qed. + Lemma testbit_add_shiftl_low : forall i, (0 <= i) -> forall a b n, (i < n) -> + Z.testbit (a + Z.shiftl b n) i = Z.testbit a i. + Proof. + intros. + erewrite Z.testbit_low; eauto. + rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega. + rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega). + auto using Z.mod_pow2_bits_low. + Qed. -Lemma Z_mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0. -Proof. - intros. - apply Z.div_small. - auto using Z.mod_pos_bound. -Qed. + Lemma mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0. + Proof. + intros. + apply Z.div_small. + auto using Z.mod_pos_bound. + Qed. + Hint Rewrite mod_div_eq0 using lia : zsimplify. -Lemma Z_shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n -> +Lemma shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n -> Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr b (m - n). Proof. intros. @@ -212,7 +256,7 @@ Proof. f_equal; ring. Qed. -Lemma Z_shiftr_add_shiftl_low : forall n m a b, 0 <= m <= n -> 0 <= a < 2 ^ n -> +Lemma shiftr_add_shiftl_low : forall n m a b, 0 <= m <= n -> 0 <= a < 2 ^ n -> Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr a m + Z.shiftr b (m - n). Proof. intros. @@ -223,7 +267,7 @@ Proof. repeat f_equal; ring. Qed. -Lemma Z_testbit_add_shiftl_high : forall i, (0 <= i) -> forall a b n, (0 <= n <= i) -> +Lemma testbit_add_shiftl_high : forall i, (0 <= i) -> forall a b n, (0 <= n <= i) -> 0 <= a < 2 ^ n -> Z.testbit (a + Z.shiftl b n) i = Z.testbit b (i - n). Proof. @@ -233,7 +277,7 @@ Proof. replace a with 0 by omega; f_equal; ring | ]); try omega. rewrite <-Z.add_1_r at 1. rewrite <-Z.shiftr_spec by assumption. replace (Z.succ x - n) with (x - (n - 1)) by ring. - rewrite Z_shiftr_add_shiftl_low, <-Z.shiftl_opp_r with (a := b) by omega. + rewrite shiftr_add_shiftl_low, <-Z.shiftl_opp_r with (a := b) by omega. rewrite <-H1 with (a := Z.shiftr a 1); try omega; [ repeat f_equal; ring | ]. rewrite Z.shiftr_div_pow2 by omega. split; apply Z.div_pos || apply Z.div_lt_upper_bound; @@ -242,89 +286,81 @@ Proof. replace (1 + (n - 1)) with n by ring; omega. Qed. -Lemma Z_land_add_land : forall n m a b, (m <= n)%nat -> - Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)). -Proof. - intros. - rewrite !Z.land_ones by apply Nat2Z.is_nonneg. - rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg. - replace (b * 2 ^ Z.of_nat n) with - ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by - (rewrite (le_plus_minus m n) at 2; try assumption; - rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring). - rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega). - symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega). - rewrite (le_plus_minus m n) by assumption. - rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg. - apply Z.divide_factor_l. -Qed. - -Lemma Z_pow_gt0 : forall a, 0 < a -> forall b, 0 <= b -> 0 < a ^ b. -Proof. - intros until 1. - apply natlike_ind; try (simpl; omega). - intros. - rewrite Z.pow_succ_r by assumption. - apply Z.mul_pos_pos; assumption. -Qed. + Lemma land_add_land : forall n m a b, (m <= n)%nat -> + Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)). + Proof. + intros. + rewrite !Z.land_ones by apply Nat2Z.is_nonneg. + rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg. + replace (b * 2 ^ Z.of_nat n) with + ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by + (rewrite (le_plus_minus m n) at 2; try assumption; + rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring). + rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega). + symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega). + rewrite (le_plus_minus m n) by assumption. + rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg. + apply Z.divide_factor_l. + Qed. -Lemma div_pow2succ : forall n x, (0 <= x) -> - n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x). -Proof. - intros. - rewrite Z.pow_succ_r, Z.mul_comm by auto. - rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega). - rewrite Zdiv2_div. - reflexivity. -Qed. + Lemma div_pow2succ : forall n x, (0 <= x) -> + n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x). + Proof. + intros. + rewrite Z.pow_succ_r, Z.mul_comm by auto. + rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega). + rewrite Zdiv2_div. + reflexivity. + Qed. -Lemma shiftr_succ : forall n x, - Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1. -Proof. - intros. - rewrite Z.shiftr_shiftr by omega. - reflexivity. -Qed. + Lemma shiftr_succ : forall n x, + Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1. + Proof. + intros. + rewrite Z.shiftr_shiftr by omega. + reflexivity. + Qed. -Definition Z_shiftl_by n a := Z.shiftl a n. + Definition shiftl_by n a := Z.shiftl a n. -Lemma Z_shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z_shiftl_by n a. -Proof. - intros. - unfold Z_shiftl_by. - rewrite Z.shiftl_mul_pow2 by assumption. - apply Z.mul_comm. -Qed. + Lemma shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z.shiftl_by n a. + Proof. + intros. + unfold Z.shiftl_by. + rewrite Z.shiftl_mul_pow2 by assumption. + apply Z.mul_comm. + Qed. -Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z_shiftl_by n) l. -Proof. - intros; induction l; auto using Z_shiftl_by_mul_pow2. - simpl. - rewrite IHl. - f_equal. - apply Z_shiftl_by_mul_pow2. - assumption. -Qed. + Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z.shiftl_by n) l. + Proof. + intros; induction l; auto using Z.shiftl_by_mul_pow2. + simpl. + rewrite IHl. + f_equal. + apply Z.shiftl_by_mul_pow2. + assumption. + Qed. -Lemma Z_odd_mod : forall a b, (b <> 0)%Z -> - Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a. -Proof. - intros. - rewrite Zmod_eq_full by assumption. - rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul. - case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r. -Qed. + Lemma odd_mod : forall a b, (b <> 0)%Z -> + Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a. + Proof. + intros. + rewrite Zmod_eq_full by assumption. + rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul. + case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r. + Qed. -Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0. -Proof. - intros. - replace b with (b - c + c) by ring. - rewrite Z.pow_add_r by omega. - apply Z_mod_mult. -Qed. + Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0. + Proof. + intros. + replace b with (b - c + c) by ring. + rewrite Z.pow_add_r by omega. + apply Z_mod_mult. + Qed. + Hint Rewrite mod_same_pow using lia : zsimplify. - Lemma Z_ones_succ : forall x, (0 <= x) -> + Lemma ones_succ : forall x, (0 <= x) -> Z.ones (Z.succ x) = 2 ^ x + Z.ones x. Proof. unfold Z.ones; intros. @@ -335,14 +371,14 @@ Qed. rewrite Z.pow_succ_r; omega. Qed. - Lemma Z_div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c. + Lemma div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c. Proof. intros. apply Z.lt_succ_r. apply Z.div_lt_upper_bound; try omega. Qed. - Lemma Z_shiftr_1_r_le : forall a b, a <= b -> + Lemma shiftr_1_r_le : forall a b, a <= b -> Z.shiftr a 1 <= Z.shiftr b 1. Proof. intros. @@ -350,7 +386,7 @@ Qed. apply Z.div_le_mono; omega. Qed. - Lemma Z_ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1. + Lemma ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1. Proof. induction i; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega. intros. @@ -364,7 +400,7 @@ Qed. f_equal. omega. Qed. - Lemma Z_shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) -> + Lemma shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) -> Z.shiftr a i <= Z.ones (n - i) \/ n <= i. Proof. intros until 1. @@ -378,17 +414,17 @@ Qed. left. rewrite shiftr_succ. replace (n - Z.succ x) with (Z.pred (n - x)) by omega. - rewrite Z_ones_pred by omega. - apply Z_shiftr_1_r_le. + rewrite Z.ones_pred by omega. + apply Z.shiftr_1_r_le. assumption. Qed. - Lemma Z_shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) -> + Lemma shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) -> Z.shiftr a i <= Z.ones (n - i) . Proof. intros a n i G G0 G1. destruct (Z_le_lt_eq_dec i n G1). - + destruct (Z_shiftr_ones' a n G i G0); omega. + + destruct (Z.shiftr_ones' a n G i G0); omega. + subst; rewrite Z.sub_diag. destruct (Z_eq_dec a 0). - subst; rewrite Z.shiftr_0_l; reflexivity. @@ -396,7 +432,7 @@ Qed. apply Z.log2_lt_pow2; omega. Qed. - Lemma Z_shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1. + Lemma shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1. Proof. intros a ? ? [a_nonneg a_upper_bound]. apply Z_le_lt_eq_dec in a_upper_bound. @@ -412,107 +448,17 @@ Qed. omega. Qed. -(* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *) -Ltac zero_bounds' := - repeat match goal with - | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg - | [ |- 0 <= _ - _] => apply Z.le_0_sub - | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg - | [ |- 0 <= _ / _] => apply Z.div_pos - | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg - | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg - | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds']; - try solve [apply Z.add_nonneg_pos; zero_bounds'] - | [ |- 0 < _ - _] => apply Z.lt_0_sub - | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split - | [ |- 0 < _ / _] => apply Z.div_str_pos - | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg - end; try omega; try prime_bound; auto. - -Ltac zero_bounds := try omega; try prime_bound; zero_bounds'. - -Lemma Z_ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. -Proof. - apply natlike_ind. - + unfold Z.ones. simpl; omega. - + intros. - rewrite Z_ones_succ by assumption. - zero_bounds. -Qed. - -Lemma Z_ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. -Proof. - intros. - unfold Z.ones. - rewrite Z.shiftl_1_l. - apply Z.lt_succ_lt_pred. - apply Z.pow_gt_1; omega. -Qed. - -Lemma N_le_1_l : forall p, (1 <= N.pos p)%N. -Proof. - destruct p; cbv; congruence. -Qed. - -Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N. -Proof. - induction a; destruct b; intros; try solve [cbv; congruence]; - simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl; - try (apply N_le_1_l || apply N.le_0_l); intro land_eq; - rewrite land_eq in *; unfold N.le, N.compare in *; - rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO; - try assumption. - destruct (p ?=a)%positive; cbv; congruence. -Qed. - -Lemma Z_land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> - Z.land a b <= a. -Proof. - intros. - destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence]. - cbv [Z.land]. - rewrite <-N2Z.inj_pos, <-N2Z.inj_le. - auto using Pos_land_upper_bound_l. -Qed. - -Lemma Z_land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) -> - Z.land a b <= b. -Proof. - intros. - rewrite Z.land_comm. - auto using Z_land_upper_bound_l. -Qed. - -Lemma Z_le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) -> - In x l -> x <= fold_right Z.max low l. -Proof. - induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ]. - simpl. - destruct (in_inv In_list); subst. - + apply Z.le_max_l. - + etransitivity. - - apply IHl; auto; intuition. - - apply Z.le_max_r. -Qed. - -Lemma Z_le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l. -Proof. - induction l; intros; try reflexivity. - etransitivity; [ apply IHl | apply Z.le_max_r ]. -Qed. - - (* TODO : move to ZUtil *) - Lemma Z_lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> + Lemma lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> Z.lor a (Z.shiftl b n) = a + (Z.shiftl b n). Proof. intros. apply Z.bits_inj'; intros t ?. rewrite Z.lor_spec, Z.shiftl_spec by assumption. destruct (Z_lt_dec t n). - + rewrite Z_testbit_add_shiftl_low by omega. + + rewrite testbit_add_shiftl_low by omega. rewrite Z.testbit_neg_r with (n := t - n) by omega. apply Bool.orb_false_r. - + rewrite Z_testbit_add_shiftl_high by omega. + + rewrite testbit_add_shiftl_high by omega. replace (Z.testbit a t) with false; [ apply Bool.orb_false_l | ]. symmetry. apply Z.testbit_false; try omega. @@ -520,3 +466,446 @@ Qed. split; try eapply Z.lt_le_trans with (m := 2 ^ n); try omega. apply Z.pow_le_mono_r; omega. Qed. + + (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *) + Ltac zero_bounds' := + repeat match goal with + | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg + | [ |- 0 <= _ - _] => apply Z.le_0_sub + | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg + | [ |- 0 <= _ / _] => apply Z.div_pos + | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg + | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg + | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds']; + try solve [apply Z.add_nonneg_pos; zero_bounds'] + | [ |- 0 < _ - _] => apply Z.lt_0_sub + | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split + | [ |- 0 < _ / _] => apply Z.div_str_pos + | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg + end; try omega; try prime_bound; auto. + + Ltac zero_bounds := try omega; try prime_bound; zero_bounds'. + + Hint Extern 1 => progress zero_bounds : zero_bounds. + + Lemma ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. + Proof. + apply natlike_ind. + + unfold Z.ones. simpl; omega. + + intros. + rewrite Z.ones_succ by assumption. + zero_bounds. + Qed. + + Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. + Proof. + intros. + unfold Z.ones. + rewrite Z.shiftl_1_l. + apply Z.lt_succ_lt_pred. + apply Z.pow_gt_1; omega. + Qed. + + Lemma N_le_1_l : forall p, (1 <= N.pos p)%N. + Proof. + destruct p; cbv; congruence. + Qed. + + Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N. + Proof. + induction a; destruct b; intros; try solve [cbv; congruence]; + simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl; + try (apply N_le_1_l || apply N.le_0_l); intro land_eq; + rewrite land_eq in *; unfold N.le, N.compare in *; + rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO; + try assumption. + destruct (p ?=a)%positive; cbv; congruence. + Qed. + + Lemma land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> + Z.land a b <= a. + Proof. + intros. + destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence]. + cbv [Z.land]. + rewrite <-N2Z.inj_pos, <-N2Z.inj_le. + auto using Pos_land_upper_bound_l. + Qed. + + Lemma land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) -> + Z.land a b <= b. + Proof. + intros. + rewrite Z.land_comm. + auto using Z.land_upper_bound_l. + Qed. + + Lemma le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) -> + In x l -> x <= fold_right Z.max low l. + Proof. + induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ]. + simpl. + destruct (in_inv In_list); subst. + + apply Z.le_max_l. + + etransitivity. + - apply IHl; auto; intuition. + - apply Z.le_max_r. + Qed. + + Lemma le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l. + Proof. + induction l; intros; try reflexivity. + etransitivity; [ apply IHl | apply Z.le_max_r ]. + Qed. + + Ltac ltb_to_lt := + repeat match goal with + | [ H : (?x <? ?y) = ?b |- _ ] + => let H' := fresh in + rename H into H'; + pose proof (Zlt_cases x y) as H; + rewrite H' in H; + clear H' + end. + + Ltac compare_to_sgn := + repeat match goal with + | [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H + | _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff + end. + + Local Ltac replace_to_const c := + repeat match goal with + | [ H : ?x = ?x |- _ ] => clear H + | [ H : ?x = c, H' : context[?x] |- _ ] => rewrite H in H' + | [ H : c = ?x, H' : context[?x] |- _ ] => rewrite <- H in H' + | [ H : ?x = c |- context[?x] ] => rewrite H + | [ H : c = ?x |- context[?x] ] => rewrite <- H + end. + + Lemma lt_div_0 n m : n / m < 0 <-> ((n < 0 < m \/ m < 0 < n) /\ 0 < -(n / m)). + Proof. + Z.compare_to_sgn; rewrite Z.sgn_opp; simpl. + pose proof (Zdiv_sgn n m) as H. + pose proof (Z.sgn_spec (n / m)) as H'. + repeat first [ progress intuition + | progress simpl in * + | congruence + | lia + | progress replace_to_const (-1) + | progress replace_to_const 0 + | progress replace_to_const 1 + | match goal with + | [ x : Z |- _ ] => destruct x + end ]. + Qed. + + Lemma two_times_x_minus_x x : 2 * x - x = x. + Proof. lia. Qed. + + Lemma mul_div_le x y z + (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z) + (Hyz : y <= z) + : x * y / z <= x. + Proof. + transitivity (x * z / z); [ | rewrite Z.div_mul by lia; lia ]. + apply Z_div_le; nia. + Qed. + + Lemma div_mul_diff a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * a / b - c * (a / b) <= c. + Proof. + pose proof (Z.mod_pos_bound a b). + etransitivity; [ | apply (mul_div_le c (a mod b) b); lia ]. + rewrite (Z_div_mod_eq a b) at 1 by lia. + rewrite Z.mul_add_distr_l. + replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia. + rewrite Z.div_add_l by lia. + lia. + Qed. + + Lemma div_mul_le_le a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c. + Proof. + pose proof (Z.div_mul_diff a b c); split; try apply Z.div_mul_le; lia. + Qed. + + Lemma div_mul_le_le_offset a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b). + Proof. + pose proof (Z.div_mul_le_le a b c); lia. + Qed. + + Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.div_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith. + + (** * [Z.simplify_fractions_le] *) + (** The culmination of this series of tactics, + [Z.simplify_fractions_le], will use the fact that [a * (b / c) <= + (a * b) / c], and do some reasoning modulo associativity and + commutativity in [Z] to perform such a reduction. It may leave + over goals if it cannot prove that some denominators are non-zero. + If the rewrite [a * (b / c)] → [(a * b) / c] is safe to do on the + LHS of the goal, this tactic should not turn a solvable goal into + an unsolvable one. + + After running, the tactic does some basic rewriting to simplify + fractions, e.g., that [a * b / b = a]. *) + Ltac split_sums_step := + match goal with + | [ |- _ + _ <= _ ] + => etransitivity; [ eapply Z.add_le_mono | ] + | [ |- _ - _ <= _ ] + => etransitivity; [ eapply Z.sub_le_mono | ] + end. + Ltac split_sums := + try (split_sums_step; [ split_sums.. | ]). + Ltac pre_reorder_fractions_step := + match goal with + | [ |- context[?x / ?y * ?z] ] + => rewrite (Z.mul_comm (x / y) z) + | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in + match LHS with + | context G[?x * (?y / ?z)] + => let G' := context G[(x * y) / z] in + transitivity G' + end + end. + Ltac pre_reorder_fractions := + try first [ split_sums_step; [ pre_reorder_fractions.. | ] + | pre_reorder_fractions_step; [ .. | pre_reorder_fractions ] ]. + Ltac split_comparison := + match goal with + | [ |- ?x <= ?x ] => reflexivity + | [ H : _ >= _ |- _ ] + => apply Z.ge_le_iff in H + | [ |- ?x * ?y <= ?z * ?w ] + => lazymatch goal with + | [ H : 0 <= x |- _ ] => idtac + | [ H : x < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec x 0) + end; + [ .. + | lazymatch goal with + | [ H : 0 <= y |- _ ] => idtac + | [ H : y < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec y 0) + end; + [ .. + | apply Zmult_le_compat; [ | | assumption | assumption ] ] ] + | [ |- ?x / ?y <= ?z / ?y ] + => lazymatch goal with + | [ H : 0 < y |- _ ] => idtac + | [ H : y <= 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec 0 y) + end; + [ apply Z_div_le; [ apply Z.gt_lt_iff; assumption | ] + | .. ] + | [ |- ?x / ?y <= ?x / ?z ] + => lazymatch goal with + | [ H : 0 <= x |- _ ] => idtac + | [ H : x < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec x 0) + end; + [ .. + | lazymatch goal with + | [ H : 0 < z |- _ ] => idtac + | [ H : z <= 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec 0 z) + end; + [ apply Z.div_le_compat_l; [ assumption | split; [ assumption | ] ] + | .. ] ] + | [ |- _ + _ <= _ + _ ] + => apply Z.add_le_mono + | [ |- _ - _ <= _ - _ ] + => apply Z.sub_le_mono + | [ |- ?x * (?y / ?z) <= (?x * ?y) / ?z ] + => apply Z.div_mul_le + end. + Ltac split_comparison_fin_step := + match goal with + | _ => assumption + | _ => lia + | _ => progress subst + | [ H : ?n * ?m < 0 |- _ ] + => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]] + | [ H : ?n / ?m < 0 |- _ ] + => apply (proj1 (lt_div_0 n m)) in H; destruct H as [[[??]|[??]]?] + | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ] + => assert (0 <= x^y) by zero_bounds; lia + | [ H : (?x^?y) < 0 |- _ ] + => assert (0 <= x^y) by zero_bounds; lia + | [ H : (?x^?y) <= 0 |- _ ] + => let H' := fresh in + assert (H' : 0 <= x^y) by zero_bounds; + assert (x^y = 0) by lia; + clear H H' + | [ H : _^_ = 0 |- _ ] + => apply Z.pow_eq_0_iff in H; destruct H as [?|[??]] + | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ] + => assert (x = 0) by lia; clear H H' + | [ |- ?x <= ?y ] => is_evar x; reflexivity + | [ |- ?x <= ?y ] => is_evar y; reflexivity + end. + Ltac split_comparison_fin := repeat split_comparison_fin_step. + Ltac simplify_fractions_step := + match goal with + | _ => rewrite Z.div_mul by (try apply Z.pow_nonzero; zero_bounds) + | [ |- context[?x * ?y / ?x] ] + => rewrite (Z.mul_comm x y) + | [ |- ?x <= ?x ] => reflexivity + end. + Ltac simplify_fractions := repeat simplify_fractions_step. + Ltac simplify_fractions_le := + pre_reorder_fractions; + [ repeat split_comparison; split_comparison_fin; zero_bounds.. + | simplify_fractions ]. + + Lemma log2_nonneg' n a : n <= 0 -> n <= Z.log2 a. + Proof. + intros; transitivity 0; auto with zarith. + Qed. + + Hint Resolve log2_nonneg' : zarith. + + (** We create separate databases for two directions of transformations + involving [Z.log2]; combining them leads to loops. *) + (* for hints that take in hypotheses of type [log2 _], and spit out conclusions of type [_ ^ _] *) + Create HintDb hyp_log2. + + (* for hints that take in hypotheses of type [_ ^ _], and spit out conclusions of type [log2 _] *) + Create HintDb concl_log2. + + Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2. + Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2. + + Lemma le_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z. + Proof. + destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia. + Qed. + + Lemma div_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y. + Proof. + intros; rewrite Z.div_div, (Z.mul_comm y x), <- Z.div_div, Z.div_same by lia. + reflexivity. + Qed. + + Hint Rewrite div_x_y_x using lia : zsimplify. + + Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0. + Proof. + split; intro H'; apply Z.mod_opp_l_z in H'; rewrite ?Z.opp_involutive in H'; assumption. + Qed. + + Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. + Proof. lia. Qed. + + Hint Rewrite <- mod_opp_l_z_iff using lia : zsimplify. + Hint Rewrite opp_eq_0_iff : zsimplify. + + Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X. + Proof. lia. Qed. + + Lemma div_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1). + Proof. + destruct (Z_zerop (a mod b)); autorewrite with zsimplify push_Zopp; reflexivity. + Qed. + + Lemma div_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1). + Proof. + destruct (Z_zerop (a mod b)); autorewrite with zsimplify pull_Zopp; lia. + Qed. + + Hint Rewrite Z.div_opp_l_complete using lia : pull_Zopp. + Hint Rewrite Z.div_opp_l_complete' using lia : push_Zopp. + + Lemma div_opp a : a <> 0 -> -a / a = -1. + Proof. + intros; autorewrite with pull_Zopp zsimplify; lia. + Qed. + + Hint Rewrite Z.div_opp using lia : zsimplify. + + Lemma div_sub_1_0 x : x > 0 -> (x - 1) / x = 0. + Proof. auto with zarith lia. Qed. + + Hint Rewrite div_sub_1_0 using lia : zsimplify. + + Lemma sub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0. + Proof. + intros H0 H1; pose proof (Z.sub_pos_bound a b X H0 H1). + assert (Hn : -X <= a - b) by lia. + assert (Hp : a - b <= X - 1) by lia. + split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ]; + instantiate; autorewrite with zsimplify; try reflexivity. + Qed. + + Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) + (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith. + + Lemma sub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a <? b then -1 else 0. + Proof. + intros H0 H1; pose proof (Z.sub_pos_bound_div a b X H0 H1). + destruct (a <? b) eqn:?; Z.ltb_to_lt. + { cut ((a - b) / X <> 0); [ lia | ]. + autorewrite with zstrip_div; auto with zarith lia. } + { autorewrite with zstrip_div; auto with zarith lia. } + Qed. + + Lemma add_opp_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (-b + a) / X = if a <? b then -1 else 0. + Proof. + rewrite !(Z.add_comm (-_)), !Z.add_opp_r. + apply Z.sub_pos_bound_div_eq. + Qed. + + Hint Rewrite Z.sub_pos_bound_div_eq Z.add_opp_pos_bound_div_eq using lia : zstrip_div. + + Lemma div_small_sym a b : 0 <= a < b -> 0 = a / b. + Proof. intros; symmetry; apply Z.div_small; assumption. Qed. + + Lemma mod_small_sym a b : 0 <= a < b -> a = a mod b. + Proof. intros; symmetry; apply Z.mod_small; assumption. Qed. + + Hint Resolve div_small_sym mod_small_sym : zarith. + + Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b. + Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed. + + Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b. + Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed. + + Hint Rewrite div_add_l' div_add' using lia : zsimplify. + + Lemma div_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b. + Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed. + + Lemma div_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b. + Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l'. Qed. + + Lemma div_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b. + Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l. Qed. + + Lemma div_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b. + Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l'. Qed. + + Hint Rewrite Z.div_add_sub Z.div_add_sub' Z.div_add_sub_l Z.div_add_sub_l' using lia : zsimplify. + + Lemma div_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k. + Proof. + intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. + autorewrite with zsimplify; reflexivity. + Qed. + + Lemma div_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k. + Proof. + intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. + autorewrite with zsimplify; reflexivity. + Qed. + + Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using lia : zsimplify. +End Z. + +Module Export BoundsTactics. + Ltac prime_bound := Z.prime_bound. + Ltac zero_bounds := Z.zero_bounds. +End BoundsTactics. diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v new file mode 100644 index 000000000..060d2f479 --- /dev/null +++ b/src/WeierstrassCurve/Pre.v @@ -0,0 +1,57 @@ +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. +Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Local Open Scope core_scope. + +Generalizable All Variables. +Section Pre. + Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}. + Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)). + 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" := (opp x). + Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2). + Local Notation "'∞'" := unit : type_scope. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "2" := (1+1). Local Notation "3" := (1+2). + Local Notation "( x , y )" := (inl (pair x y)). + + Add Field WeierstrassCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). + Add Ring WeierstrassCurveRing : (Ring.ring_theory_for_stdlib_tactic (T:=F)). + + Context {a:F}. + Context {b:F}. + + (* the canonical definitions are in Spec *) + Definition onCurve (P:F*F + ∞) := match P with + | (x, y) => y^2 = x^3 + a*x + b + | ∞ => True + end. + Definition unifiedAdd' (P1' P2':F*F + ∞) : F*F + ∞ := + match P1', P2' with + | (x1, y1), (x2, y2) + => if x1 =? x2 then + if y2 =? -y1 then + ∞ + else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, + (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) + else + ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, + (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) + | ∞, ∞ => ∞ + | ∞, _ => P2' + | _, ∞ => P1' + end. + + Lemma unifiedAdd'_onCurve : forall P1 P2, + onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). + Proof. + unfold onCurve, unifiedAdd'; intros [[x1 y1]|] [[x2 y2]|] H1 H2; + break_match; trivial; setoid_subst_rel eq; only_two_square_roots; + field_algebra; nsatz_contradict. + Qed. +End Pre. |