diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 4 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 61 | ||||
| -rw-r--r-- | src/Util/Tactics.v | 40 | ||||
| -rw-r--r-- | src/Util/ZUtil.v | 136 |
4 files changed, 216 insertions, 25 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 5923a7279..0ce214bbd 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -1205,6 +1205,8 @@ Section Conversion. let bitsA := Z.pow2_mod ((inp # digitA) >> indexA) dist in convert' inp (i + Z.to_nat dist)%nat (update_nth digitB (update_by_concat_bits indexB bitsA) out). Proof. + generalize limb_widthsA_nonneg; intros _. (* don't drop this from the proof in 8.4 *) + generalize limb_widthsB_nonneg; intros _. (* don't drop this from the proof in 8.4 *) repeat match goal with | |- _ => progress intros | |- appcontext [bit_index (Z.of_nat ?i)] => @@ -1212,7 +1214,7 @@ Section Conversion. | H : forall x : Z, In x ?lw -> 0 <= x |- appcontext [bit_index ?lw ?i] => unique pose proof (bit_index_not_done lw i) | H : forall x : Z, In x ?lw -> 0 <= x |- appcontext [bit_index ?lw ?i] => - unique pose proof (rem_bits_in_digit_le_rem_bits lw H i) + unique assert (0 <= i < bitsIn lw -> i + (lw # digit_index lw i - bit_index lw i) <= bitsIn lw) by auto using rem_bits_in_digit_le_rem_bits | |- _ => rewrite Z2Nat.id | |- _ => rewrite Nat2Z.inj_add | |- (Z.to_nat _ < Z.to_nat _)%nat => apply Z2Nat.inj_lt diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 9e5cf1f67..257b388c8 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -110,7 +110,7 @@ Proof. reflexivity. Qed. -Definition appify2 {T} (op : fe25519 -> fe25519 -> T) (f g : fe25519) := +Definition appify2 {T} (op : fe25519 -> fe25519 -> T) (f g : fe25519) := app_10 f (fun f0 => (app_10 g (fun g0 => op f0 g0))). Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g. @@ -163,19 +163,29 @@ Proof. cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. - cbv. - autorewrite with zsimplify. + cbv. (* N.B. The slow part of this is computing with [Z_div_opt]. + It would be much faster if we could take advantage of + the form of [base_from_limb_widths] when doing + division, so we could do subtraction instead. *) + autorewrite with zsimplify_fast. reflexivity. Defined. Definition mul_simpl (f g : fe25519) : fe25519 := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in - proj1_sig (mul_simpl_sig f g). + let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in + let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in + proj1_sig (mul_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) + (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). Definition mul_simpl_correct (f g : fe25519) - : mul_simpl f g = carry_mul_opt k_ c_ f g := - Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in - proj2_sig (mul_simpl_sig f g). + : mul_simpl f g = carry_mul_opt k_ c_ f g. +Proof. + pose proof (proj2_sig (mul_simpl_sig f g)). + cbv [fe25519] in *. + repeat match goal with p : (_ * Z)%type |- _ => destruct p end. + assumption. +Qed. Definition mul_sig (f g : fe25519) : { fg : fe25519 | fg = carry_mul_opt k_ c_ f g}. @@ -220,21 +230,26 @@ Proof. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [pack_opt]. - repeat ( - rewrite <-convert'_opt_correct; - cbv - [from_list_default_opt Pow2BaseProofs.convert']; - repeat progress rewrite ?Z.shiftl_0_r, ?Z.shiftr_0_r, ?Z.land_0_l, ?Z.lor_0_l, ?Z.land_same_r). + repeat (rewrite <-convert'_opt_correct; + cbv - [from_list_default_opt Pow2BaseProofs.convert']). + repeat progress rewrite ?Z.shiftl_0_r, ?Z.shiftr_0_r, ?Z.land_0_l, ?Z.lor_0_l, ?Z.land_same_r. cbv [from_list_default_opt]. reflexivity. Defined. Definition pack_simpl (f : fe25519) := Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in - proj1_sig (pack_simpl_sig f). + let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in + proj1_sig (pack_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). Definition pack_simpl_correct (f : fe25519) - : pack_simpl f = pack_opt params25519 wire_widths_nonneg bits_eq f - := Eval cbv beta iota delta [proj2_sig pack_simpl_sig] in proj2_sig (pack_simpl_sig f). + : pack_simpl f = pack_opt params25519 wire_widths_nonneg bits_eq f. +Proof. + pose proof (proj2_sig (pack_simpl_sig f)). + cbv [fe25519] in *. + repeat match goal with p : (_ * Z)%type |- _ => destruct p end. + assumption. +Qed. Definition pack_sig (f : fe25519) : { f' | f' = pack_opt params25519 wire_widths_nonneg bits_eq f }. @@ -262,19 +277,25 @@ Proof. cbv [unpack_opt]. repeat ( rewrite <-convert'_opt_correct; - cbv - [from_list_default_opt Pow2BaseProofs.convert']; - repeat progress rewrite ?Z.shiftl_0_r, ?Z.shiftr_0_r, ?Z.land_0_l, ?Z.lor_0_l, ?Z.land_same_r). + cbv - [from_list_default_opt Pow2BaseProofs.convert']). + repeat progress rewrite ?Z.shiftl_0_r, ?Z.shiftr_0_r, ?Z.land_0_l, ?Z.lor_0_l, ?Z.land_same_r. cbv [from_list_default_opt]. reflexivity. Defined. Definition unpack_simpl (f : wire_digits) : fe25519 := Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in - proj1_sig (unpack_simpl_sig f). + let '(f0, f1, f2, f3, f4, f5, f6, f7) := f in + proj1_sig (unpack_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7)). Definition unpack_simpl_correct (f : wire_digits) - : unpack_simpl f = unpack_opt params25519 wire_widths_nonneg bits_eq f - := Eval cbv beta iota delta [proj2_sig unpack_simpl_sig] in proj2_sig (unpack_simpl_sig f). + : unpack_simpl f = unpack_opt params25519 wire_widths_nonneg bits_eq f. +Proof. + pose proof (proj2_sig (unpack_simpl_sig f)). + cbv [wire_digits] in *. + repeat match goal with p : (_ * Z)%type |- _ => destruct p end. + assumption. +Qed. Definition unpack_sig (f : wire_digits) : { f' | f' = unpack_opt params25519 wire_widths_nonneg bits_eq f }. @@ -299,4 +320,4 @@ Definition unpack_correct (f : wire_digits) zero one eq -*)
\ No newline at end of file +*) diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 880f5824a..be777512c 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -20,6 +20,13 @@ Ltac head expr := Ltac head_hnf expr := let expr' := eval hnf in expr in head expr'. +(** [contains x expr] succeeds iff [x] appears in [expr] *) +Ltac contains search_for in_term := + idtac; + lazymatch in_term with + | appcontext[search_for] => idtac + end. + (* [pose proof defn], but only if no hypothesis of the same type exists. most useful for proofs of a proposition *) Tactic Notation "unique" "pose" "proof" constr(defn) := @@ -391,3 +398,36 @@ Ltac eforward_step H := end. Ltac forward H := try (forward_step H; [ forward H | .. ]). Ltac eforward H := try (eforward_step H; [ eforward H | .. ]). + +(** [simplify_projections] reduces terms of the form [fst (_, _)] (for + any projection from [prod], [sig], [sigT], or [and]) *) +Ltac pre_simplify_projection proj proj' uproj' := + pose proj as proj'; + pose proj as uproj'; + unfold proj in uproj'; + change proj with proj'. +Ltac do_simplify_projection_2Targ_4carg_step proj proj' uproj' construct := + change proj' with uproj' at 1; + lazymatch goal with + | [ |- appcontext[uproj' _ _ (construct _ _ _ _)] ] + => unfold uproj' + | _ => change uproj' with proj + end. +Ltac do_simplify_projection_2Targ_4carg proj proj' uproj' construct := + repeat do_simplify_projection_2Targ_4carg_step proj proj' uproj' construct. +Ltac simplify_projection_2Targ_4carg proj construct := + let proj' := fresh "proj" in + let uproj' := fresh "proj" in + pre_simplify_projection proj proj' uproj'; + do_simplify_projection_2Targ_4carg proj proj' uproj' construct; + clear proj' uproj'. + +Ltac simplify_projections := + repeat (simplify_projection_2Targ_4carg @fst @pair + || simplify_projection_2Targ_4carg @snd @pair + || simplify_projection_2Targ_4carg @proj1_sig @exist + || simplify_projection_2Targ_4carg @proj2_sig @exist + || simplify_projection_2Targ_4carg @projT1 @existT + || simplify_projection_2Targ_4carg @projT2 @existT + || simplify_projection_2Targ_4carg @proj1 @conj + || simplify_projection_2Targ_4carg @proj2 @conj). diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 3a96aa51e..cbee05474 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -3,6 +3,7 @@ Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms. Require Import Coq.Structures.Equalities. Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. Require Import Coq.Lists.List. Require Export Crypto.Util.FixCoqMistakes. @@ -18,10 +19,11 @@ 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 Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r : 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. +Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg : 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)) (fun a b pf => proj1 (Z.pow_gt_1 a b pf)) : zarith. -Ltac zutil_arith := solve [ omega | lia ]. +Ltac zutil_arith := solve [ omega | lia | auto with nocore ]. +Ltac zutil_arith_more_inequalities := solve [ zutil_arith | auto with 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 @@ -36,6 +38,7 @@ 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_ 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 Z.div_0_l Z.mod_mod Z.mod_small Z_mod_zero_opp_full Z.mod_1_l using zutil_arith : zsimplify. Hint Rewrite <- Z.opp_eq_mul_m1 Z.one_succ Z.two_succ : zsimplify. Hint Rewrite <- Z.div_mod using zutil_arith : zsimplify. +Hint Rewrite (fun x y => proj2 (Z.eqb_neq x y)) using assumption : zsimplify. (** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *) Create HintDb push_Zopp discriminated. @@ -102,7 +105,7 @@ Hint Rewrite <- Z.shiftr_lxor Z.shiftr_land Z.shiftr_lor Z.shiftr_ldiff Z.lnot_s Hint Rewrite Z.shiftr_lxor Z.shiftr_land Z.shiftr_lor Z.shiftr_ldiff Z.lnot_shiftr Z.ldiff_ones_r Z.shiftl_lxor Z.shiftl_land Z.shiftl_lor Z.shiftl_ldiff using zutil_arith : push_Zshift. Hint Rewrite <- Z.shiftr_shiftl_l Z.shiftr_shiftl_r Z.shiftr_shiftr Z.shiftl_shiftl using zutil_arith : push_Zshift. Hint Rewrite Z.shiftr_opp_r Z.shiftl_opp_r Z.shiftr_0_r Z.shiftr_0_l Z.shiftl_0_r Z.shiftl_0_l : push_Zshift. -Hint Rewrite Z.shiftl_1_l Z.shiftr_div_pow2 Z.shiftr_mul_pow2 Z.shiftl_mul_pow2 Z.shiftl_div_pow2 using zutil_arith : Zshift_to_pow. +Hint Rewrite Z.shiftl_1_l Z.shiftr_div_pow2 Z.shiftr_mul_pow2 Z.shiftl_mul_pow2 Z.shiftl_div_pow2 Z.opp_involutive using zutil_arith : Zshift_to_pow. Hint Rewrite <- Z.shiftr_opp_r using zutil_arith : Zshift_to_pow. Hint Rewrite <- Z.shiftr_div_pow2 Z.shiftr_mul_pow2 Z.shiftl_mul_pow2 Z.shiftl_div_pow2 using zutil_arith : Zpow_to_shift. @@ -110,6 +113,8 @@ Hint Rewrite <- Z.shiftr_div_pow2 Z.shiftr_mul_pow2 Z.shiftl_mul_pow2 Z.shiftl_d Create HintDb zstrip_div. Hint Rewrite Z.div_small_iff using zutil_arith : zstrip_div. +Hint Rewrite <- Z.shiftr_div_pow2 Z.shiftr_mul_pow2 Z.shiftl_mul_pow2 Z.shiftl_div_pow2 using zutil_arith : convert_to_Ztestbit. + (** 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. *) @@ -218,6 +223,7 @@ Module Z. unfold Z.pow2_mod. rewrite Z.land_ones; auto. Qed. + Hint Rewrite <- Z.pow2_mod_spec using zutil_arith : convert_to_Ztestbit. Lemma ones_spec : forall n m, 0 <= n -> 0 <= m -> Z.testbit (Z.ones n) m = if Z_lt_dec m n then true else false. Proof. @@ -271,6 +277,13 @@ Module Z. apply Z.min_case_strong; intros; repeat progress (try break_if; autorewrite with Ztestbit zsimplify; try reflexivity). Qed. + Lemma pow2_mod_pos_bound a b : 0 < b -> 0 <= Z.pow2_mod a b < 2^b. + Proof. + intros; rewrite Z.pow2_mod_spec by omega. + auto with zarith. + Qed. + Hint Resolve pow2_mod_pos_bound : zarith. + Lemma land_same_r : forall a b, (a & b) & b = a & b. Proof. intros; apply Z.bits_inj'; intros. @@ -724,6 +737,7 @@ Module Z. split; try eapply Z.lt_le_trans with (m := 2 ^ n); try omega. apply Z.pow_le_mono_r; omega. Qed. + Hint Rewrite <- Z.lor_shiftl using zutil_arith : convert_to_Ztestbit. (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *) Ltac zero_bounds' := @@ -1617,6 +1631,18 @@ Module Z. Proof. intros; rewrite (mod_small_n 1) by lia; lia. Qed. Hint Rewrite mod_small_1 using zutil_arith : zsimplify. + Lemma mul_mod_distr_r_full a b c : (a * c) mod (b * c) = (a mod b * c). + Proof. + destruct (Z_zerop b); [ | destruct (Z_zerop c) ]; subst; + autorewrite with zsimplify; auto using Z.mul_mod_distr_r. + Qed. + + Lemma mul_mod_distr_l_full a b c : (c * a) mod (c * b) = c * (a mod b). + Proof. + destruct (Z_zerop b); [ | destruct (Z_zerop c) ]; subst; + autorewrite with zsimplify; auto using Z.mul_mod_distr_l. + Qed. + Lemma leb_add_same x y : (x <=? y + x) = (0 <=? y). Proof. destruct (x <=? y + x) eqn:?, (0 <=? y) eqn:?; ltb_to_lt; try reflexivity; omega. Qed. Hint Rewrite leb_add_same : zsimplify. @@ -1661,6 +1687,108 @@ Module Z. Proof. lia. Qed. Hint Rewrite simplify_twice_sub_add : zsimplify. + Lemma simplify_2XmX X : 2 * X - X = X. + Proof. omega. Qed. + Hint Rewrite simplify_2XmX : zsimplify. + + Lemma move_R_pX x y z : x + y = z -> x = z - y. + Proof. omega. Qed. + Lemma move_R_mX x y z : x - y = z -> x = z + y. + Proof. omega. Qed. + Lemma move_R_Xp x y z : y + x = z -> x = z - y. + Proof. omega. Qed. + Lemma move_R_Xm x y z : y - x = z -> x = y - z. + Proof. omega. Qed. + Lemma move_L_pX x y z : z = x + y -> z - y = x. + Proof. omega. Qed. + Lemma move_L_mX x y z : z = x - y -> z + y = x. + Proof. omega. Qed. + Lemma move_L_Xp x y z : z = y + x -> z - y = x. + Proof. omega. Qed. + Lemma move_L_Xm x y z : z = y - x -> y - z = x. + Proof. omega. Qed. + + (** [linear_substitute x] attempts to maipulate equations using only + addition and subtraction to put [x] on the left, and then + eliminates [x]. Currently, it only handles equations where [x] + appears once; it does not yet handle equations like [x - x + x = + 5]. *) + Ltac linear_solve_for_in_step for_var H := + let LHS := match type of H with ?LHS = ?RHS => LHS end in + let RHS := match type of H with ?LHS = ?RHS => RHS end in + first [ match RHS with + | ?a + ?b + => first [ contains for_var b; apply move_L_pX in H + | contains for_var a; apply move_L_Xp in H ] + | ?a - ?b + => first [ contains for_var b; apply move_L_mX in H + | contains for_var a; apply move_L_Xm in H ] + | for_var + => progress symmetry in H + end + | match LHS with + | ?a + ?b + => first [ not contains for_var b; apply move_R_pX in H + | not contains for_var a; apply move_R_Xp in H ] + | ?a - ?b + => first [ not contains for_var b; apply move_R_mX in H + | not contains for_var a; apply move_R_Xm in H ] + end ]. + Ltac linear_solve_for_in for_var H := repeat linear_solve_for_in_step for_var H. + Ltac linear_solve_for for_var := + match goal with + | [ H : for_var = _ |- _ ] => idtac + | [ H : context[for_var] |- _ ] + => linear_solve_for_in for_var H; + lazymatch type of H with + | for_var = _ => idtac + | ?T => fail 0 "Could not fully solve for" for_var "in" T "(hypothesis" H ")" + end + end. + Ltac linear_substitute for_var := linear_solve_for for_var; subst for_var. + Ltac linear_substitute_all := + repeat match goal with + | [ v : Z |- _ ] => linear_substitute v + end. + + (** [div_mod_to_quot_rem] replaces [x / y] and [x mod y] with new + variables [q] and [r] while simultaneously adding facts that + uniquely specify [q] and [r] to the context (roughly, that [y * + q + r = x] and that [0 <= r < y]. *) + Ltac div_mod_to_quot_rem_inequality_solver := + zutil_arith_more_inequalities. + Ltac generalize_div_eucl x y := + let H := fresh in + let H' := fresh in + assert (H' : y <> 0) by div_mod_to_quot_rem_inequality_solver; + generalize (Z.div_mod x y H'); clear H'; + assert (H' : 0 < y) by div_mod_to_quot_rem_inequality_solver; + generalize (Z.mod_pos_bound x y H'); clear H'; + let q := fresh "q" in + let r := fresh "r" in + set (q := x / y); + set (r := x mod y); + clearbody q r. + + Ltac div_mod_to_quot_rem_step := + match goal with + | [ |- context[?x / ?y] ] => generalize_div_eucl x y + | [ |- context[?x mod ?y] ] => generalize_div_eucl x y + end. + + Ltac div_mod_to_quot_rem := repeat div_mod_to_quot_rem_step; intros. + + (** [rewrite_mod_small] is a better version of [rewrite Z.mod_small + by rewrite_mod_small_solver]; it backtracks across occurences + that the solver fails to solve the side-conditions on. *) + Ltac rewrite_mod_small_solver := + zutil_arith_more_inequalities. + Ltac rewrite_mod_small := + repeat match goal with + | [ |- context[?x mod ?y] ] + => rewrite (Z.mod_small x y) by rewrite_mod_small_solver + end. + Local Ltac simplify_div_tac := intros; autorewrite with zsimplify; rewrite <- ?Z_div_plus_full_l, <- ?Z_div_plus_full by assumption; try (apply f_equal2; [ | reflexivity ]); |