diff options
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v')
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v | 582 |
1 files changed, 0 insertions, 582 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v deleted file mode 100644 index 3dd7fc0b3..000000000 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v +++ /dev/null @@ -1,582 +0,0 @@ -(*** Word-By-Word Montgomery Multiplication Proofs *) -Require Import Coq.Arith.Arith. -Require Import Coq.ZArith.BinInt Coq.ZArith.ZArith Coq.ZArith.Zdiv Coq.micromega.Lia. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.NatUtil. -Require Import Crypto.Arithmetic.ModularArithmeticTheorems Crypto.Spec.ModularArithmetic. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Definition. -Require Import Crypto.Algebra.Ring. -Require Import Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.ZUtil.Modulo. -Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.Tactics.SetEvars. -Require Import Crypto.Util.Tactics.SubstEvars. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.BreakMatch. -Local Open Scope Z_scope. - -Section WordByWordMontgomery. - Context - {T : nat -> Type} - {eval : forall {n}, T n -> Z} - {zero : forall {n}, T n} - {divmod : forall {n}, T (S n) -> T n * Z} (* returns lowest limb and all-but-lowest-limb *) - {r : positive} - {r_big : r > 1} - {R : positive} - {R_numlimbs : nat} - {R_correct : R = r^Z.of_nat R_numlimbs :> Z} - {small : forall {n}, T n -> Prop} - {eval_zero : forall n, eval (@zero n) = 0} - {small_zero : forall n, small (@zero n)} - {eval_div : forall n v, small v -> eval (fst (@divmod n v)) = eval v / r} - {eval_mod : forall n v, small v -> snd (@divmod n v) = eval v mod r} - {small_div : forall n v, small v -> small (fst (@divmod n v))} - {scmul : forall {n}, Z -> T n -> T (S n)} (* uses double-output multiply *) - {eval_scmul: forall n a v, small v -> 0 <= a < r -> 0 <= eval v < R -> eval (@scmul n a v) = a * eval v} - {small_scmul : forall n a v, small v -> 0 <= a < r -> 0 <= eval v < R -> small (@scmul n a v)} - {addT : forall {n}, T n -> T n -> T (S n)} (* joins carry *) - {eval_addT : forall n a b, eval (@addT n a b) = eval a + eval b} - {small_addT : forall n a b, small a -> small b -> small (@addT n a b)} - {addT' : forall {n}, T (S n) -> T n -> T (S (S n))} (* joins carry *) - {eval_addT' : forall n a b, eval (@addT' n a b) = eval a + eval b} - {small_addT' : forall n a b, small a -> small b -> small (@addT' n a b)} - {drop_high : T (S (S R_numlimbs)) -> T (S R_numlimbs)} (* drops the highest limb *) - {eval_drop_high : forall v, small v -> eval (drop_high v) = eval v mod (r * r^Z.of_nat R_numlimbs)} - {small_drop_high : forall v, small v -> small (drop_high v)} - (N : T R_numlimbs) (Npos : positive) (Npos_correct: eval N = Z.pos Npos) - (small_N : small N) - (N_lt_R : eval N < R) - {conditional_sub : T (S R_numlimbs) -> T R_numlimbs} (* computes [arg - N] if [N <= arg], and drops high bit *) - {eval_conditional_sub : forall v, small v -> 0 <= eval v < eval N + R -> eval (conditional_sub v) = eval v + if eval N <=? eval v then -eval N else 0} - {small_conditional_sub : forall v, small v -> 0 <= eval v < eval N + R -> small (conditional_sub v)} - {sub_then_maybe_add : T R_numlimbs -> T R_numlimbs -> T R_numlimbs} (* computes [a - b + if (a - b) <? 0 then N else 0] *) - {eval_sub_then_maybe_add : forall a b, small a -> small b -> 0 <= eval a < eval N -> 0 <= eval b < eval N -> eval (sub_then_maybe_add a b) = eval a - eval b + if eval a - eval b <? 0 then eval N else 0} - {small_sub_then_maybe_add : forall a b, small (sub_then_maybe_add a b)} - (B : T R_numlimbs) - (B_bounds : 0 <= eval B < R) - (small_B : small B) - ri (ri_correct : r*ri mod (eval N) = 1 mod (eval N)) - (k : Z) (k_correct : k * eval N mod r = (-1) mod r). - - Create HintDb push_eval discriminated. - Local Ltac t_small := - repeat first [ assumption - | apply small_addT - | apply small_addT' - | apply small_div - | apply small_drop_high - | apply small_zero - | apply small_scmul - | apply small_conditional_sub - | apply small_sub_then_maybe_add - | apply Z_mod_lt - | rewrite Z.mul_split_mod - | solve [ auto with zarith ] - | lia - | progress autorewrite with push_eval - | progress autounfold with word_by_word_montgomery - | match goal with - | [ H : and _ _ |- _ ] => destruct H - end ]. - Hint Rewrite - eval_zero - eval_div - eval_mod - eval_addT - eval_addT' - eval_scmul - eval_drop_high - eval_conditional_sub - eval_sub_then_maybe_add - using (repeat autounfold with word_by_word_montgomery; t_small) - : push_eval. - - Local Arguments eval {_} _. - Local Arguments small {_} _. - Local Arguments divmod {_} _. - - (* Recurse for a as many iterations as A has limbs, varying A := A, S := 0, r, bounds *) - Section Iteration. - Context (pred_A_numlimbs : nat) - (A : T (S pred_A_numlimbs)) - (S : T (S R_numlimbs)) - (small_A : small A) - (small_S : small S) - (S_nonneg : 0 <= eval S). - (* Given A, B < R, we want to compute A * B / R mod N. R = bound 0 * ... * bound (n-1) *) - - Local Coercion eval : T >-> Z. - - Local Notation a := (@WordByWord.Abstract.Dependent.Definition.a T (@divmod) pred_A_numlimbs A). - Local Notation A' := (@WordByWord.Abstract.Dependent.Definition.A' T (@divmod) pred_A_numlimbs A). - Local Notation S1 := (@WordByWord.Abstract.Dependent.Definition.S1 T (@divmod) R_numlimbs scmul addT pred_A_numlimbs B A S). - Local Notation s := (@WordByWord.Abstract.Dependent.Definition.s T (@divmod) R_numlimbs scmul addT pred_A_numlimbs B A S). - Local Notation q := (@WordByWord.Abstract.Dependent.Definition.q T (@divmod) r R_numlimbs scmul addT pred_A_numlimbs B k A S). - Local Notation S2 := (@WordByWord.Abstract.Dependent.Definition.S2 T (@divmod) r R_numlimbs scmul addT addT' N pred_A_numlimbs B k A S). - Local Notation S3 := (@WordByWord.Abstract.Dependent.Definition.S3 T (@divmod) r R_numlimbs scmul addT addT' N pred_A_numlimbs B k A S). - Local Notation S4 := (@WordByWord.Abstract.Dependent.Definition.S4 T (@divmod) r R_numlimbs scmul addT addT' drop_high N pred_A_numlimbs B k A S). - - Lemma S3_bound - : eval S < eval N + eval B - -> eval S3 < eval N + eval B. - Proof. - assert (Hmod : forall a b, 0 < b -> a mod b <= b - 1) - by (intros x y; pose proof (Z_mod_lt x y); omega). - intro HS. - unfold S3, S2, S1. - autorewrite with push_eval; []. - eapply Z.le_lt_trans. - { transitivity ((N+B-1 + (r-1)*B + (r-1)*N) / r); - [ | set_evars; ring_simplify_subterms; subst_evars; reflexivity ]. - Z.peel_le; repeat apply Z.add_le_mono; repeat apply Z.mul_le_mono_nonneg; try lia; - repeat autounfold with word_by_word_montgomery; rewrite ?Z.mul_split_mod; - autorewrite with push_eval; - try Z.zero_bounds; - auto with lia. } - rewrite (Z.mul_comm _ r), <- Z.add_sub_assoc, <- Z.add_opp_r, !Z.div_add_l' by lia. - autorewrite with zsimplify. - simpl; omega. - Qed. - - Lemma small_A' - : small A'. - Proof. - repeat autounfold with word_by_word_montgomery; auto. - Qed. - - Lemma small_S3 - : small S3. - Proof. repeat autounfold with word_by_word_montgomery; t_small. Qed. - - Lemma S3_nonneg : 0 <= eval S3. - Proof. - repeat autounfold with word_by_word_montgomery; rewrite ?Z.mul_split_mod; - autorewrite with push_eval; []. - rewrite ?Npos_correct; Z.zero_bounds; lia. - Qed. - - Lemma S4_nonneg : 0 <= eval S4. - Proof. unfold S4; rewrite eval_drop_high by apply small_S3; Z.zero_bounds. Qed. - - Lemma S4_bound - : eval S < eval N + eval B - -> eval S4 < eval N + eval B. - Proof. - intro H; pose proof (S3_bound H); pose proof S3_nonneg. - unfold S4. - rewrite eval_drop_high by apply small_S3. - rewrite Z.mod_small by nia. - assumption. - Qed. - - Lemma small_S4 - : small S4. - Proof. repeat autounfold with word_by_word_montgomery; t_small. Qed. - - Lemma S1_eq : eval S1 = S + a*B. - Proof. - cbv [S1 a A']. - repeat autorewrite with push_eval. - reflexivity. - Qed. - - Lemma S2_mod_N : (eval S2) mod N = (S + a*B) mod N. - Proof. - cbv [S2]; autorewrite with push_eval zsimplify. rewrite S1_eq. reflexivity. - Qed. - - Lemma S2_mod_r : S2 mod r = 0. - Proof. - cbv [S2 q s]; autorewrite with push_eval. - assert (r > 0) by lia. - assert (Hr : (-(1 mod r)) mod r = r - 1 /\ (-(1)) mod r = r - 1). - { destruct (Z.eq_dec r 1) as [H'|H']. - { rewrite H'; split; reflexivity. } - { rewrite !Z_mod_nz_opp_full; rewrite ?Z.mod_mod; Z.rewrite_mod_small; [ split; reflexivity | omega.. ]. } } - autorewrite with pull_Zmod. - replace 0 with (0 mod r) by apply Zmod_0_l. - eapply F.eq_of_Z_iff. - rewrite Z.mul_split_mod. - repeat rewrite ?F.of_Z_add, ?F.of_Z_mul, <-?F.of_Z_mod. - rewrite <-Algebra.Hierarchy.associative. - replace ((F.of_Z r k * F.of_Z r (eval N))%F) with (F.opp (m:=r) F.one). - { cbv [F.of_Z F.add]; simpl. - apply path_sig_hprop; [ intro; exact HProp.allpath_hprop | ]. - simpl. - rewrite (proj1 Hr), Z.mul_sub_distr_l. - push_Zmod; pull_Zmod. - autorewrite with zsimplify; reflexivity. } - { rewrite <- F.of_Z_mul. - rewrite F.of_Z_mod. - rewrite k_correct. - cbv [F.of_Z F.add F.opp F.one]; simpl. - change (-(1)) with (-1) in *. - apply path_sig_hprop; [ intro; exact HProp.allpath_hprop | ]; simpl. - rewrite (proj1 Hr), (proj2 Hr); Z.rewrite_mod_small; reflexivity. } - Qed. - - Lemma S3_mod_N - : S3 mod N = (S + a*B)*ri mod N. - Proof. - cbv [S3]; autorewrite with push_eval cancel_pair. - pose proof fun a => Z.div_to_inv_modulo N a r ri eq_refl ri_correct as HH; - cbv [Z.equiv_modulo] in HH; rewrite HH; clear HH. - etransitivity; [rewrite (fun a => Z.mul_mod_l a ri N)| - rewrite (fun a => Z.mul_mod_l a ri N); reflexivity]. - rewrite <-S2_mod_N; repeat (f_equal; []); autorewrite with push_eval. - autorewrite with push_Zmod; - rewrite S2_mod_r; - autorewrite with zsimplify. - reflexivity. - Qed. - - Lemma S4_mod_N - (Hbound : eval S < eval N + eval B) - : S4 mod N = (S + a*B)*ri mod N. - Proof. - pose proof (S3_bound Hbound); pose proof S3_nonneg. - unfold S4; autorewrite with push_eval. - rewrite (Z.mod_small _ (r * _)) by nia. - apply S3_mod_N. - Qed. - End Iteration. - - Local Notation redc_body := (@redc_body T (@divmod) r R_numlimbs scmul addT addT' drop_high N B k). - Local Notation redc_loop := (@redc_loop T (@divmod) r R_numlimbs scmul addT addT' drop_high N B k). - Local Notation pre_redc A := (@pre_redc T zero (@divmod) r R_numlimbs scmul addT addT' drop_high N _ A B k). - Local Notation redc A := (@redc T zero (@divmod) r R_numlimbs scmul addT addT' drop_high conditional_sub N _ A B k). - - Section body. - Context (pred_A_numlimbs : nat) - (A_S : T (S pred_A_numlimbs) * T (S R_numlimbs)). - Let A:=fst A_S. - Let S:=snd A_S. - Let A_a:=divmod A. - Let a:=snd A_a. - Context (small_A : small A) - (small_S : small S) - (S_bound : 0 <= eval S < eval N + eval B). - - Lemma small_fst_redc_body : small (fst (redc_body A_S)). - Proof. destruct A_S; apply small_A'; assumption. Qed. - Lemma small_snd_redc_body : small (snd (redc_body A_S)). - Proof. destruct A_S; unfold redc_body; apply small_S4; assumption. Qed. - Lemma snd_redc_body_nonneg : 0 <= eval (snd (redc_body A_S)). - Proof. destruct A_S; apply S4_nonneg; assumption. Qed. - - Lemma snd_redc_body_mod_N - : (eval (snd (redc_body A_S))) mod (eval N) = (eval S + a*eval B)*ri mod (eval N). - Proof. destruct A_S; apply S4_mod_N; auto; omega. Qed. - - Lemma fst_redc_body - : (eval (fst (redc_body A_S))) = eval (fst A_S) / r. - Proof. - destruct A_S; simpl; repeat autounfold with word_by_word_montgomery; simpl. - autorewrite with push_eval. - reflexivity. - Qed. - - Lemma fst_redc_body_mod_N - : (eval (fst (redc_body A_S))) mod (eval N) = ((eval (fst A_S) - a)*ri) mod (eval N). - Proof. - rewrite fst_redc_body. - etransitivity; [ eapply Z.div_to_inv_modulo; try eassumption; lia | ]. - unfold a, A_a, A. - autorewrite with push_eval. - reflexivity. - Qed. - - Lemma redc_body_bound - : eval S < eval N + eval B - -> eval (snd (redc_body A_S)) < eval N + eval B. - Proof. - destruct A_S; apply S4_bound; unfold S in *; cbn [snd] in *; try assumption; try omega. - Qed. - End body. - - Local Arguments Z.pow !_ !_. - Local Arguments Z.of_nat !_. - Local Ltac induction_loop count IHcount - := induction count as [|count IHcount]; intros; cbn [redc_loop] in *; [ | (*rewrite redc_loop_comm_body in * *) ]. - Lemma redc_loop_good count A_S - (Hsmall : small (fst A_S) /\ small (snd A_S)) - (Hbound : 0 <= eval (snd A_S) < eval N + eval B) - : (small (fst (redc_loop count A_S)) /\ small (snd (redc_loop count A_S))) - /\ 0 <= eval (snd (redc_loop count A_S)) < eval N + eval B. - Proof. - induction_loop count IHcount; auto; []. - change (id (0 <= eval B < R)) in B_bounds (* don't let [destruct_head'_and] loop *). - destruct_head'_and. - repeat first [ apply conj - | apply small_fst_redc_body - | apply small_snd_redc_body - | apply redc_body_bound - | apply snd_redc_body_nonneg - | apply IHcount - | solve [ auto ] ]. - Qed. - - Lemma small_redc_loop count A_S - (Hsmall : small (fst A_S) /\ small (snd A_S)) - (Hbound : 0 <= eval (snd A_S) < eval N + eval B) - : small (fst (redc_loop count A_S)) /\ small (snd (redc_loop count A_S)). - Proof. apply redc_loop_good; assumption. Qed. - - Lemma redc_loop_bound count A_S - (Hsmall : small (fst A_S) /\ small (snd A_S)) - (Hbound : 0 <= eval (snd A_S) < eval N + eval B) - : 0 <= eval (snd (redc_loop count A_S)) < eval N + eval B. - Proof. apply redc_loop_good; assumption. Qed. - - Local Ltac handle_IH_small := - repeat first [ apply redc_loop_good - | apply small_fst_redc_body - | apply small_snd_redc_body - | apply redc_body_bound - | apply snd_redc_body_nonneg - | apply conj - | progress cbn [fst snd] - | progress destruct_head' and - | solve [ auto ] ]. - - Lemma fst_redc_loop count A_S - (Hsmall : small (fst A_S) /\ small (snd A_S)) - (Hbound : 0 <= eval (snd A_S) < eval N + eval B) - : eval (fst (redc_loop count A_S)) = eval (fst A_S) / r^(Z.of_nat count). - Proof. - induction_loop count IHcount. - { simpl; autorewrite with zsimplify; reflexivity. } - { rewrite IHcount, fst_redc_body by handle_IH_small. - change (1 + R_numlimbs)%nat with (S R_numlimbs) in *. - rewrite Zdiv_Zdiv by Z.zero_bounds. - rewrite <- (Z.pow_1_r r) at 1. - rewrite <- Z.pow_add_r by lia. - replace (1 + Z.of_nat count) with (Z.of_nat (S count)) by lia. - reflexivity. } - Qed. - - Lemma fst_redc_loop_mod_N count A_S - (Hsmall : small (fst A_S) /\ small (snd A_S)) - (Hbound : 0 <= eval (snd A_S) < eval N + eval B) - : eval (fst (redc_loop count A_S)) mod (eval N) - = (eval (fst A_S) - eval (fst A_S) mod r^Z.of_nat count) - * ri^(Z.of_nat count) mod (eval N). - Proof. - rewrite fst_redc_loop by assumption. - destruct count. - { simpl; autorewrite with zsimplify; reflexivity. } - { etransitivity; - [ eapply Z.div_to_inv_modulo; - try solve [ eassumption - | apply Z.lt_gt, Z.pow_pos_nonneg; lia ] - | ]. - { erewrite <- Z.pow_mul_l, <- Z.pow_1_l. - { apply Z.pow_mod_Proper; [ eassumption | reflexivity ]. } - { lia. } } - reflexivity. } - Qed. - - Local Arguments Z.pow : simpl never. - Lemma snd_redc_loop_mod_N count A_S - (Hsmall : small (fst A_S) /\ small (snd A_S)) - (Hbound : 0 <= eval (snd A_S) < eval N + eval B) - : (eval (snd (redc_loop count A_S))) mod (eval N) - = ((eval (snd A_S) + (eval (fst A_S) mod r^(Z.of_nat count))*eval B)*ri^(Z.of_nat count)) mod (eval N). - Proof. - induction_loop count IHcount. - { simpl; autorewrite with zsimplify; reflexivity. } - { rewrite IHcount by handle_IH_small. - push_Zmod; rewrite snd_redc_body_mod_N, fst_redc_body by handle_IH_small; pull_Zmod. - autorewrite with push_eval; []. - match goal with - | [ |- ?x mod ?N = ?y mod ?N ] - => change (Z.equiv_modulo N x y) - end. - destruct A_S as [A S]. - cbn [fst snd]. - change (Z.pos (Pos.of_succ_nat ?n)) with (Z.of_nat (Datatypes.S n)). - rewrite !Z.mul_add_distr_r. - rewrite <- !Z.mul_assoc. - replace (ri * ri^(Z.of_nat count)) with (ri^(Z.of_nat (Datatypes.S count))) - by (change (Datatypes.S count) with (1 + count)%nat; - autorewrite with push_Zof_nat; rewrite Z.pow_add_r by lia; simpl Z.succ; rewrite Z.pow_1_r; nia). - rewrite <- !Z.add_assoc. - apply Z.add_mod_Proper; [ reflexivity | ]. - unfold Z.equiv_modulo; push_Zmod; rewrite (Z.mul_mod_l (_ mod r) _ (eval N)). - rewrite Z.mod_pull_div by auto with zarith lia. - push_Zmod. - erewrite Z.div_to_inv_modulo; - [ - | apply Z.lt_gt; lia - | eassumption ]. - pull_Zmod. - match goal with - | [ |- ?x mod ?N = ?y mod ?N ] - => change (Z.equiv_modulo N x y) - end. - repeat first [ rewrite <- !Z.pow_succ_r, <- !Nat2Z.inj_succ by lia - | rewrite (Z.mul_comm _ ri) - | rewrite (Z.mul_assoc _ ri _) - | rewrite (Z.mul_comm _ (ri^_)) - | rewrite (Z.mul_assoc _ (ri^_) _) ]. - repeat first [ rewrite <- Z.mul_assoc - | rewrite <- Z.mul_add_distr_l - | rewrite (Z.mul_comm _ (eval B)) - | rewrite !Nat2Z.inj_succ, !Z.pow_succ_r by lia; - rewrite <- Znumtheory.Zmod_div_mod by (apply Z.divide_factor_r || Z.zero_bounds) - | rewrite Zplus_minus - | rewrite (Z.mul_comm r (r^_)) - | reflexivity ]. } - Qed. - - Lemma pre_redc_bound A_numlimbs (A : T A_numlimbs) - (small_A : small A) - : 0 <= eval (pre_redc A) < eval N + eval B. - Proof. - unfold pre_redc. - apply redc_loop_good; simpl; autorewrite with push_eval; - rewrite ?Npos_correct; auto; lia. - Qed. - - Lemma small_pre_redc A_numlimbs (A : T A_numlimbs) - (small_A : small A) - : small (pre_redc A). - Proof. - unfold pre_redc. - apply redc_loop_good; simpl; autorewrite with push_eval; - rewrite ?Npos_correct; auto; lia. - Qed. - - Lemma pre_redc_mod_N A_numlimbs (A : T A_numlimbs) (small_A : small A) (A_bound : 0 <= eval A < r ^ Z.of_nat A_numlimbs) - : (eval (pre_redc A)) mod (eval N) = (eval A * eval B * ri^(Z.of_nat A_numlimbs)) mod (eval N). - Proof. - unfold pre_redc. - rewrite snd_redc_loop_mod_N; cbn [fst snd]; - autorewrite with push_eval zsimplify; - [ | rewrite ?Npos_correct; auto; lia.. ]. - Z.rewrite_mod_small. - reflexivity. - Qed. - - Lemma redc_mod_N A_numlimbs (A : T A_numlimbs) (small_A : small A) (A_bound : 0 <= eval A < r ^ Z.of_nat A_numlimbs) - : (eval (redc A)) mod (eval N) = (eval A * eval B * ri^(Z.of_nat A_numlimbs)) mod (eval N). - Proof. - pose proof (@small_pre_redc _ A small_A). - pose proof (@pre_redc_bound _ A small_A). - unfold redc. - autorewrite with push_eval; []. - break_innermost_match; - try rewrite Z.add_opp_r, Zminus_mod, Z_mod_same_full; - autorewrite with zsimplify_fast; - apply pre_redc_mod_N; auto. - Qed. - - Lemma redc_bound_tight A_numlimbs (A : T A_numlimbs) - (small_A : small A) - : 0 <= eval (redc A) < eval N + eval B + if eval N <=? eval (pre_redc A) then -eval N else 0. - Proof. - pose proof (@small_pre_redc _ A small_A). - pose proof (@pre_redc_bound _ A small_A). - unfold redc. - rewrite eval_conditional_sub by t_small. - break_innermost_match; Z.ltb_to_lt; omega. - Qed. - - Lemma redc_bound_N A_numlimbs (A : T A_numlimbs) - (small_A : small A) - : eval B < eval N -> 0 <= eval (redc A) < eval N. - Proof. - pose proof (@small_pre_redc _ A small_A). - pose proof (@pre_redc_bound _ A small_A). - unfold redc. - rewrite eval_conditional_sub by t_small. - break_innermost_match; Z.ltb_to_lt; omega. - Qed. - - Lemma redc_bound A_numlimbs (A : T A_numlimbs) - (small_A : small A) - (A_bound : 0 <= eval A < r ^ Z.of_nat A_numlimbs) - : 0 <= eval (redc A) < R. - Proof. - pose proof (@small_pre_redc _ A small_A). - pose proof (@pre_redc_bound _ A small_A). - unfold redc. - rewrite eval_conditional_sub by t_small. - break_innermost_match; Z.ltb_to_lt; try omega. - Qed. - - Lemma small_redc A_numlimbs (A : T A_numlimbs) - (small_A : small A) - (A_bound : 0 <= eval A < r ^ Z.of_nat A_numlimbs) - : small (redc A). - Proof. - pose proof (@small_pre_redc _ A small_A). - pose proof (@pre_redc_bound _ A small_A). - unfold redc. - apply small_conditional_sub; [ apply small_pre_redc | .. ]; auto; omega. - Qed. - - Local Notation add := (@add T R_numlimbs addT conditional_sub). - Local Notation sub := (@sub T R_numlimbs sub_then_maybe_add). - Local Notation opp := (@opp T (@zero) R_numlimbs sub_then_maybe_add). - - Section add_sub. - Context (Av Bv : T R_numlimbs) - (small_Av : small Av) - (small_Bv : small Bv) - (Av_bound : 0 <= eval Av < eval N) - (Bv_bound : 0 <= eval Bv < eval N). - - Local Ltac do_clear := - clear dependent B; clear dependent k; clear dependent ri; clear dependent Npos. - - Lemma small_add : small (add Av Bv). - Proof. do_clear; unfold add; t_small. Qed. - Lemma small_sub : small (sub Av Bv). - Proof. do_clear; unfold sub; t_small. Qed. - Lemma small_opp : small (opp Av). - Proof. clear dependent Bv; do_clear; unfold opp, sub; t_small. Qed. - - Lemma eval_add : eval (add Av Bv) = eval Av + eval Bv + if (eval N <=? eval Av + eval Bv) then -eval N else 0. - Proof. do_clear; unfold add; autorewrite with push_eval; reflexivity. Qed. - Lemma eval_sub : eval (sub Av Bv) = eval Av - eval Bv + if (eval Av - eval Bv <? 0) then eval N else 0. - Proof. do_clear; unfold sub; autorewrite with push_eval; reflexivity. Qed. - Lemma eval_opp : eval (opp Av) = (if (eval Av =? 0) then 0 else eval N) - eval Av. - Proof. - clear dependent Bv; do_clear; unfold opp, sub; autorewrite with push_eval. - break_innermost_match; Z.ltb_to_lt; lia. - Qed. - - Local Ltac t_mod_N := - repeat first [ progress break_innermost_match - | reflexivity - | let H := fresh in intro H; rewrite H; clear H - | progress autorewrite with zsimplify_const - | rewrite Z.add_opp_r - | progress (push_Zmod; pull_Zmod) ]. - - Lemma eval_add_mod_N : eval (add Av Bv) mod eval N = (eval Av + eval Bv) mod eval N. - Proof. generalize eval_add; clear. t_mod_N. Qed. - Lemma eval_sub_mod_N : eval (sub Av Bv) mod eval N = (eval Av - eval Bv) mod eval N. - Proof. generalize eval_sub; clear. t_mod_N. Qed. - Lemma eval_opp_mod_N : eval (opp Av) mod eval N = (-eval Av) mod eval N. - Proof. generalize eval_opp; clear; t_mod_N. Qed. - - Lemma add_bound : 0 <= eval (add Av Bv) < eval N. - Proof. do_clear; generalize eval_add; break_innermost_match; Z.ltb_to_lt; lia. Qed. - Lemma sub_bound : 0 <= eval (sub Av Bv) < eval N. - Proof. do_clear; generalize eval_sub; break_innermost_match; Z.ltb_to_lt; lia. Qed. - Lemma opp_bound : 0 <= eval (opp Av) < eval N. - Proof. do_clear; generalize eval_opp; break_innermost_match; Z.ltb_to_lt; lia. Qed. - End add_sub. -End WordByWordMontgomery. |