remove old pipeline

6 files changed, 0 insertions, 1658 deletions

diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v
deleted file mode 100644
index 2ea623b0b..000000000
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v
+++ /dev/null
@@ -1,61 +0,0 @@
-(*** Word-By-Word Montgomery Multiplication *)
-(** This file implements Montgomery Form, Montgomery Reduction, and
-    Montgomery Multiplication on an abstract [T].  See
-    https://github.com/mit-plv/fiat-crypto/issues/157 for a discussion
-    of the algorithm; note that it may be that none of the algorithms
-    there exactly match what we're doing here. *)
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.ZUtil.Definitions.
-
-Local Open Scope Z_scope.
-
-Section WordByWordMontgomery.
-  Local Coercion Z.pos : positive >-> Z.
-  Context
-    {T : Type}
-    {eval : T -> Z}
-    {numlimbs : T -> nat}
-    {zero : nat -> T}
-    {divmod : T -> T * Z} (* returns lowest limb and all-but-lowest-limb *)
-    {r : positive}
-    {scmul : Z -> T -> T} (* uses double-output multiply *)
-    {R : positive}
-    {add : T -> T -> T} (* joins carry *)
-    {drop_high : T -> T} (* drops the highest limb *)
-    (N : T).
-
-  (* Recurse for a as many iterations as A has limbs, varying A := A, S := 0, r, bounds *)
-  Section Iteration.
-    Context (B : T) (k : Z).
-    Context (A S : T).
-    (* Given A, B < R, we want to compute A * B / R mod N. R = bound 0 * ... * bound (n-1) *)
-    Local Definition A_a := dlet p := divmod A in p. Local Definition A' := fst A_a. Local Definition a := snd A_a.
-    Local Definition S1 := add S (scmul a B).
-    Local Definition s := snd (divmod S1).
-    Local Definition q := fst (Z.mul_split r s k).
-    Local Definition S2 := add S1 (scmul q N).
-    Local Definition S3 := fst (divmod S2).
-    Local Definition S4 := drop_high S3.
-  End Iteration.
-
-  Section loop.
-    Context (A B : T) (k : Z) (S' : T).
-
-    Definition redc_body : T * T -> T * T
-      := fun '(A, S') => (A' A, S4 B k A S').
-
-    Fixpoint redc_loop (count : nat) : T * T -> T * T
-      := match count with
-         | O => fun A_S => A_S
-         | S count' => fun A_S => redc_loop count' (redc_body A_S)
-         end.
-
-    Definition redc : T
-      := snd (redc_loop (numlimbs A) (A, zero (1 + numlimbs B))).
-  End loop.
-End WordByWordMontgomery.
-
-Create HintDb word_by_word_montgomery.
-Hint Unfold S4 S3 S2 q s S1 a A' A_a Let_In : word_by_word_montgomery.
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition.v
deleted file mode 100644
index cff906465..000000000
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition.v
+++ /dev/null
@@ -1,81 +0,0 @@
-(*** Word-By-Word Montgomery Multiplication *)
-(** This file implements Montgomery Form, Montgomery Reduction, and
-    Montgomery Multiplication on an abstract [T : ℕ → Type].  See
-    https://github.com/mit-plv/fiat-crypto/issues/157 for a discussion
-    of the algorithm; note that it may be that none of the algorithms
-    there exactly match what we're doing here. *)
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.ZUtil.Definitions.
-
-Local Open Scope Z_scope.
-
-Section WordByWordMontgomery.
-  Local Coercion Z.pos : positive >-> Z.
-  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 : positive}
-    {R_numlimbs : nat}
-    {scmul : forall {n}, Z -> T n -> T (S n)} (* uses double-output multiply *)
-    {addT : forall {n}, T n -> T n -> T (S n)} (* joins carry *)
-    {addT' : forall {n}, T (S n) -> T n -> T (S (S n))} (* joins carry *)
-    {drop_high : T (S (S R_numlimbs)) -> T (S R_numlimbs)} (* drops the highest limb *)
-    {conditional_sub : T (S R_numlimbs) -> T R_numlimbs} (* computes [arg - N] if [N <= arg], and drops high bit *)
-    {sub_then_maybe_add : T R_numlimbs -> T R_numlimbs -> T R_numlimbs} (* computes [a - b + if (a - b) <? 0 then N else 0] *)
-    (N : T R_numlimbs).
-
-  (* Recurse for a as many iterations as A has limbs, varying A := A, S := 0, r, bounds *)
-  Section Iteration.
-    Context (pred_A_numlimbs : nat)
-            (B : T R_numlimbs) (k : Z)
-            (A : T (S pred_A_numlimbs))
-            (S : T (S R_numlimbs)).
-    (* Given A, B < R, we want to compute A * B / R mod N. R = bound 0 * ... * bound (n-1) *)
-    Local Definition A_a := dlet p := divmod _ A in p. Local Definition A' := fst A_a. Local Definition a := snd A_a.
-    Local Definition S1 := addT _ S (scmul _ a B).
-    Local Definition s := snd (divmod _ S1).
-    Local Definition q := fst (Z.mul_split r s k).
-    Local Definition S2 := addT' _ S1 (scmul _ q N).
-    Local Definition S3 := fst (divmod _ S2).
-    Local Definition S4 := drop_high S3.
-  End Iteration.
-
-  Section loop.
-    Context (A_numlimbs : nat)
-            (A : T A_numlimbs)
-            (B : T R_numlimbs)
-            (k : Z)
-            (S' : T (S R_numlimbs)).
-
-    Definition redc_body {pred_A_numlimbs} : T (S pred_A_numlimbs) * T (S R_numlimbs)
-                                             -> T pred_A_numlimbs * T (S R_numlimbs)
-      := fun '(A, S') => (A' _ A, S4 _ B k A S').
-
-    Fixpoint redc_loop (count : nat) : T count * T (S R_numlimbs) -> T O * T (S R_numlimbs)
-      := match count return T count * _ -> _ with
-         | O => fun A_S => A_S
-         | S count' => fun A_S => redc_loop count' (redc_body A_S)
-         end.
-
-    Definition pre_redc : T (S R_numlimbs)
-      := snd (redc_loop A_numlimbs (A, zero (1 + R_numlimbs))).
-
-    Definition redc : T R_numlimbs
-      := conditional_sub pre_redc.
-  End loop.
-
-  Definition add (A B : T R_numlimbs) : T R_numlimbs
-    := conditional_sub (addT _ A B).
-  Definition sub (A B : T R_numlimbs) : T R_numlimbs
-    := sub_then_maybe_add A B.
-  Definition opp (A : T R_numlimbs) : T R_numlimbs
-    := sub (zero _) A.
-End WordByWordMontgomery.
-
-Create HintDb word_by_word_montgomery.
-Hint Unfold S4 S3 S2 q s S1 a A' A_a Let_In : word_by_word_montgomery.
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.
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v
deleted file mode 100644
index 9eabc5ce4..000000000
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v
+++ /dev/null
@@ -1,497 +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.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.
-Local Open Scope Z_scope.
-
-Section WordByWordMontgomery.
-  Context
-    {T : Type}
-    {eval : T -> Z}
-    {numlimbs : T -> nat}
-    {zero : nat -> T}
-    {divmod : T -> T * 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 : T -> Prop}
-    {eval_zero : forall n, eval (zero n) = 0}
-    {numlimbs_zero : forall n, numlimbs (zero n) = n}
-    {eval_div : forall v, small v -> eval (fst (divmod v)) = eval v / r}
-    {eval_mod : forall v, small v -> snd (divmod v) = eval v mod r}
-    {small_div : forall v, small v -> small (fst (divmod v))}
-    {numlimbs_div : forall v, numlimbs (fst (divmod v)) = pred (numlimbs v)}
-    {scmul : Z -> T -> T} (* uses double-output multiply *)
-    {eval_scmul: forall a v, 0 <= a < r -> 0 <= eval v < R -> eval (scmul a v) = a * eval v}
-    {numlimbs_scmul : forall a v, 0 <= a < r -> numlimbs (scmul a v) = S (numlimbs v)}
-    {add : T -> T -> T} (* joins carry *)
-    {eval_add : forall a b, eval (add a b) = eval a + eval b}
-    {small_add : forall a b, small (add a b)}
-    {numlimbs_add : forall a b, numlimbs (add a b) = Datatypes.S (max (numlimbs a) (numlimbs b))}
-    {drop_high : T -> T} (* drops things after [S R_numlimbs] *)
-    {eval_drop_high : forall v, small v -> eval (drop_high v) = eval v mod (r * r^Z.of_nat R_numlimbs)}
-    {numlimbs_drop_high : forall v, numlimbs (drop_high v) = min (numlimbs v) (S R_numlimbs)}
-    (N : T) (Npos : positive) (Npos_correct: eval N = Z.pos Npos)
-    (N_lt_R : eval N < R)
-    (B : T)
-    (B_bounds : 0 <= eval B < R)
-    ri (ri_correct : r*ri mod (eval N) = 1 mod (eval N)).
-  Context (k : Z) (k_correct : k * eval N mod r = (-1) mod r).
-
-  Create HintDb push_numlimbs discriminated.
-  Create HintDb push_eval discriminated.
-  Local Ltac t_small :=
-    repeat first [ assumption
-                 | apply small_add
-                 | apply small_div
-                 | apply Z_mod_lt
-                 | rewrite Z.mul_split_mod
-                 | solve [ auto with zarith ]
-                 | lia
-                 | progress autorewrite with push_eval
-                 | progress autorewrite with push_numlimbs ].
-  Hint Rewrite
-       eval_zero
-       eval_div
-       eval_mod
-       eval_add
-       eval_scmul
-       eval_drop_high
-       using (repeat autounfold with word_by_word_montgomery; t_small)
-    : push_eval.
-  Hint Rewrite
-       numlimbs_zero
-       numlimbs_div
-       numlimbs_add
-       numlimbs_scmul
-       numlimbs_drop_high
-       using (repeat autounfold with word_by_word_montgomery; t_small)
-    : push_numlimbs.
-  Hint Rewrite <- Max.succ_max_distr pred_Sn Min.succ_min_distr : push_numlimbs.
-
-
-  (* Recurse for a as many iterations as A has limbs, varying A := A, S := 0, r, bounds *)
-  Section Iteration.
-    Context (A S : T)
-            (small_A : small A)
-            (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.Definition.a T divmod A).
-    Local Notation A' := (@WordByWord.Abstract.Definition.A' T divmod A).
-    Local Notation S1 := (@WordByWord.Abstract.Definition.S1 T divmod scmul add B A S).
-    Local Notation S2 := (@WordByWord.Abstract.Definition.S2 T divmod r scmul add N B k A S).
-    Local Notation S3 := (@WordByWord.Abstract.Definition.S3 T divmod r scmul add N B k A S).
-    Local Notation S4 := (@WordByWord.Abstract.Definition.S4 T divmod r scmul add drop_high N 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, WordByWord.Abstract.Definition.S2, WordByWord.Abstract.Definition.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.
-      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 numlimbs_S4 : numlimbs S4 = min (max (1 + numlimbs S) (1 + max (1 + numlimbs B) (numlimbs N))) (1 + R_numlimbs).
-    Proof.
-      cbn [plus].
-      repeat autounfold with word_by_word_montgomery; rewrite Z.mul_split_mod.
-      repeat autorewrite with push_numlimbs.
-      change Init.Nat.max with Nat.max.
-      rewrite <- ?(Max.max_assoc (numlimbs S)).
-      reflexivity.
-    Qed.
-
-    Lemma S1_eq : eval S1 = S + a*B.
-    Proof.
-      cbv [S1 a WordByWord.Abstract.Definition.A'].
-      repeat autorewrite with push_eval.
-      reflexivity.
-    Qed.
-
-    Lemma S2_mod_N : (eval S2) mod N = (S + a*B) mod N.
-    Proof.
-      cbv [S2 WordByWord.Abstract.Definition.q WordByWord.Abstract.Definition.s]; autorewrite with push_eval zsimplify. rewrite S1_eq. reflexivity.
-    Qed.
-
-    Lemma S2_mod_r : S2 mod r = 0.
-      cbv [S2 WordByWord.Abstract.Definition.q WordByWord.Abstract.Definition.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 scmul add drop_high N B k).
-  Local Notation redc_loop := (@redc_loop T divmod r scmul add drop_high N B k).
-  Local Notation redc A := (@redc T numlimbs zero divmod r scmul add drop_high N A B k).
-
-  Lemma redc_loop_comm_body count
-    : forall A_S, redc_loop count (redc_body A_S) = redc_body (redc_loop count A_S).
-  Proof.
-    induction count as [|count IHcount]; try reflexivity.
-    simpl; intro; rewrite IHcount; reflexivity.
-  Qed.
-
-  Section body.
-    Context (A_S : T * T).
-    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)
-            (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 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; unfold WordByWord.Abstract.Definition.A', WordByWord.Abstract.Definition.A_a, Let_In, a, A_a, A; 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.
-
-    Lemma numlimbs_redc_body : numlimbs (snd (redc_body A_S))
-                               = min (max (1 + numlimbs (snd A_S)) (1 + max (1 + numlimbs B) (numlimbs N))) (1 + R_numlimbs).
-    Proof. destruct A_S; apply numlimbs_S4; assumption. 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 A_S count
-        (Hsmall : small (fst A_S))
-        (Hbound : 0 <= eval (snd A_S) < eval N + eval B)
-    : small (fst (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 redc_body_bound
-                 | apply snd_redc_body_nonneg
-                 | solve [ auto ] ].
-  Qed.
-
-  Lemma redc_loop_bound A_S count
-        (Hsmall : small (fst 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 t_min_max_step _ :=
-    match goal with
-    | [ |- context[Init.Nat.max ?x ?y] ]
-      => first [ rewrite (Max.max_l x y) by omega
-               | rewrite (Max.max_r x y) by omega ]
-    | [ |- context[Init.Nat.min ?x ?y] ]
-      => first [ rewrite (Min.min_l x y) by omega
-               | rewrite (Min.min_r x y) by omega ]
-    | _ => progress change Init.Nat.max with Nat.max
-    | _ => progress change Init.Nat.min with Nat.min
-    end.
-
-  Lemma numlimbs_redc_loop A_S count
-        (Hsmall : small (fst A_S))
-        (Hbound : 0 <= eval (snd A_S) < eval N + eval B)
-        (Hnumlimbs : (R_numlimbs <= numlimbs (snd A_S))%nat)
-    : numlimbs (snd (redc_loop count A_S))
-      = match count with
-        | O => numlimbs (snd A_S)
-        | S _ => 1 + R_numlimbs
-        end%nat.
-  Proof.
-    assert (Hgen
-            : numlimbs (snd (redc_loop count A_S))
-              = match count with
-                | O => numlimbs (snd A_S)
-                | S _ => min (max (count + numlimbs (snd A_S)) (1 + max (1 + numlimbs B) (numlimbs N))) (1 + R_numlimbs)
-                end).
-    { induction_loop count IHcount; [ reflexivity | ].
-      rewrite numlimbs_redc_body by (try apply redc_loop_good; auto).
-      rewrite IHcount; clear IHcount.
-      destruct count; [ reflexivity | ].
-      destruct (Compare_dec.le_lt_dec (1 + max (1 + numlimbs B) (numlimbs N)) (S count + numlimbs (snd A_S))),
-      (Compare_dec.le_lt_dec (1 + R_numlimbs) (S count + numlimbs (snd A_S))),
-      (Compare_dec.le_lt_dec (1 + R_numlimbs) (1 + max (1 + numlimbs B) (numlimbs N)));
-        repeat first [ reflexivity
-                     | t_min_max_step ()
-                     | progress autorewrite with push_numlimbs
-                     | rewrite Nat.min_comm, Nat.min_max_distr ]. }
-    rewrite Hgen; clear Hgen.
-    destruct count; [ reflexivity | ].
-    repeat apply Max.max_case_strong; apply Min.min_case_strong; omega.
-  Qed.
-
-
-  Lemma fst_redc_loop A_S count
-        (Hsmall : small (fst 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 fst_redc_body, IHcount
-        by (apply redc_loop_good; auto).
-      rewrite Zdiv_Zdiv by Z.zero_bounds.
-      rewrite <- (Z.pow_1_r r) at 2.
-      rewrite <- Z.pow_add_r by lia.
-      replace (Z.of_nat count + 1) with (Z.of_nat (S count)) by (simpl; lia).
-      reflexivity. }
-  Qed.
-
-  Lemma fst_redc_loop_mod_N A_S count
-        (Hsmall : small (fst 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 A_S count
-        (Hsmall : small (fst 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. }
-    { simpl; rewrite snd_redc_body_mod_N
-        by (apply redc_loop_good; auto).
-      push_Zmod; rewrite IHcount; pull_Zmod.
-      autorewrite with push_eval; [ | apply redc_loop_good; auto.. ]; [].
-      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^(Z.of_nat count) * ri) 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 fst_redc_loop by (try apply redc_loop_good; auto; omega).
-      cbn [fst].
-      rewrite Z.mod_pull_div by lia.
-      erewrite Z.div_to_inv_modulo;
-        [
-        | 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 ] ].
-      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
-                   | reflexivity ]. }
-  Qed.
-
-  Lemma redc_bound A
-        (small_A : small A)
-    : 0 <= eval (redc A) < eval N + eval B.
-  Proof.
-    unfold redc.
-    apply redc_loop_good; simpl; autorewrite with push_eval;
-      rewrite ?Npos_correct; auto; lia.
-  Qed.
-
-  Lemma numlimbs_redc_gen A (small_A : small A) (Hnumlimbs : (R_numlimbs <= numlimbs B)%nat)
-    : numlimbs (redc A)
-      = match numlimbs A with
-        | O => S (numlimbs B)
-        | _ => S R_numlimbs
-        end.
-  Proof.
-    unfold redc; rewrite numlimbs_redc_loop by (cbn [fst snd]; t_small);
-      cbn [snd]; rewrite ?numlimbs_zero.
-    reflexivity.
-  Qed.
-  Lemma numlimbs_redc A (small_A : small A) (Hnumlimbs : R_numlimbs = numlimbs B)
-    : numlimbs (redc A) = S (numlimbs B).
-  Proof. rewrite numlimbs_redc_gen; subst; auto; destruct (numlimbs A); reflexivity. Qed.
-
-  Lemma redc_mod_N A (small_A : small A) (A_bound : 0 <= eval A < r ^ Z.of_nat (numlimbs A))
-    : (eval (redc A)) mod (eval N) = (eval A * eval B * ri^(Z.of_nat (numlimbs A))) mod (eval N).
-  Proof.
-    unfold 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.
-End WordByWordMontgomery.
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
deleted file mode 100644
index fd4869f23..000000000
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
+++ /dev/null
@@ -1,108 +0,0 @@
-(*** Word-By-Word Montgomery Multiplication *)
-(** This file implements Montgomery Form, Montgomery Reduction, and
-    Montgomery Multiplication on an abstract [ℤⁿ].  See
-    https://github.com/mit-plv/fiat-crypto/issues/157 for a discussion
-    of the algorithm; note that it may be that none of the algorithms
-    there exactly match what we're doing here. *)
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Arithmetic.Saturated.MontgomeryAPI.
-Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Definition.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.CPS.
-
-Local Open Scope Z_scope.
-
-Section WordByWordMontgomery.
-  Local Coercion Z.pos : positive >-> Z.
-  (** TODO: pick better names for the arguments to this definition. *)
-  Context
-    {r : positive}
-    {R_numlimbs : nat}
-    (N : T R_numlimbs).
-
-  Local Notation scmul := (@scmul (Z.pos r)).
-  Local Notation addT' := (@MontgomeryAPI.add_S1 (Z.pos r)).
-  Local Notation addT := (@MontgomeryAPI.add (Z.pos r)).
-  Local Notation conditional_sub_cps := (fun V => @conditional_sub_cps (Z.pos r) _ V N _).
-  Local Notation conditional_sub := (fun V => @conditional_sub (Z.pos r) _ V N).
-  Local Notation sub_then_maybe_add_cps :=
-    (fun V1 V2 => @sub_then_maybe_add_cps (Z.pos r) R_numlimbs (Z.pos r - 1) V1 V2 N).
-  Local Notation sub_then_maybe_add := (fun V1 V2 => @sub_then_maybe_add (Z.pos r) R_numlimbs (Z.pos r - 1) V1 V2 N).
-
-  Definition redc_body_no_cps (B : T R_numlimbs) (k : Z) {pred_A_numlimbs} (A_S : T (S pred_A_numlimbs) * T (S R_numlimbs))
-    : T pred_A_numlimbs * T (S R_numlimbs)
-    := @redc_body T (@divmod) r R_numlimbs (@scmul) (@addT) (@addT') (@drop_high (S R_numlimbs)) N B k _ A_S.
-  Definition redc_loop_no_cps (B : T R_numlimbs) (k : Z) (count : nat) (A_S : T count * T (S R_numlimbs))
-    : T 0 * T (S R_numlimbs)
-    := @redc_loop T (@divmod) r R_numlimbs (@scmul) (@addT) (@addT') (@drop_high (S R_numlimbs)) N B k count A_S.
-  Definition pre_redc_no_cps {A_numlimbs} (A : T A_numlimbs) (B : T R_numlimbs) (k : Z) : T (S R_numlimbs)
-    := @pre_redc T (@zero) (@divmod) r R_numlimbs (@scmul) (@addT) (@addT') (@drop_high (S R_numlimbs)) N _ A B k.
-  Definition redc_no_cps {A_numlimbs} (A : T A_numlimbs) (B : T R_numlimbs) (k : Z) : T R_numlimbs
-    := @redc T (@zero) (@divmod) r R_numlimbs (@scmul) (@addT) (@addT') (@drop_high (S R_numlimbs)) conditional_sub N _ A B k.
-
-  Definition redc_body_cps {pred_A_numlimbs} (A : T (S pred_A_numlimbs)) (B : T R_numlimbs) (k : Z) (S' : T (S R_numlimbs))
-             {cpsT} (rest : T pred_A_numlimbs * T (S R_numlimbs) -> cpsT)
-    : cpsT
-    := divmod_cps A (fun '(A, a) =>
-       @scmul_cps r _ a B _ (fun aB => @add_cps r _ S' aB _ (fun S1 =>
-       divmod_cps S1 (fun '(_, s) =>
-       Z.mul_split_cps' r s k (fun mul_split_r_s_k =>
-       dlet q := fst mul_split_r_s_k in
-       @scmul_cps r _ q N _ (fun qN => @add_S1_cps r _ S1 qN _ (fun S2 =>
-       divmod_cps S2 (fun '(S3, _) =>
-       @drop_high_cps (S R_numlimbs) S3 _ (fun S4 => rest (A, S4)))))))))).
-
-  Section loop.
-    Context {A_numlimbs} (A : T A_numlimbs) (B : T R_numlimbs) (k : Z) {cpsT : Type}.
-    Fixpoint redc_loop_cps (count : nat) (rest : T 0 * T (S R_numlimbs) -> cpsT) : T count * T (S R_numlimbs) -> cpsT
-      := match count with
-         | O => rest
-         | S count' => fun '(A, S') => redc_body_cps A B k S' (redc_loop_cps count' rest)
-         end.
-
-    Definition pre_redc_cps (rest : T (S R_numlimbs) -> cpsT) : cpsT
-      := redc_loop_cps A_numlimbs (fun '(A, S') => rest S') (A, zero).
-
-    Definition redc_cps (rest : T R_numlimbs -> cpsT) : cpsT
-      := pre_redc_cps (fun v => conditional_sub_cps v rest).
-  End loop.
-
-  Definition redc_body {pred_A_numlimbs} (A : T (S pred_A_numlimbs)) (B : T R_numlimbs) (k : Z) (S' : T (S R_numlimbs))
-    : T pred_A_numlimbs * T (S R_numlimbs)
-    := redc_body_cps A B k S' id.
-  Definition redc_loop (B : T R_numlimbs) (k : Z) (count : nat) : T count * T (S R_numlimbs) -> T 0 * T (S R_numlimbs)
-    := redc_loop_cps B k count id.
-  Definition pre_redc {A_numlimbs} (A : T A_numlimbs) (B : T R_numlimbs) (k : Z) : T (S R_numlimbs)
-    := pre_redc_cps A B k id.
-  Definition redc {A_numlimbs} (A : T A_numlimbs) (B : T R_numlimbs) (k : Z) : T R_numlimbs
-    := redc_cps A B k id.
-
-  Definition add_no_cps (A B : T R_numlimbs) : T R_numlimbs
-    := @add T R_numlimbs (@addT) (@conditional_sub) A B.
-  Definition sub_no_cps (A B : T R_numlimbs) : T R_numlimbs
-    := @sub T R_numlimbs (@sub_then_maybe_add) A B.
-  Definition opp_no_cps (A : T R_numlimbs) : T R_numlimbs
-    := @opp T (@zero) R_numlimbs (@sub_then_maybe_add) A.
-
-  Definition add_cps (A B : T R_numlimbs) {cpsT} (rest : T R_numlimbs -> cpsT) : cpsT
-    := @add_cps r _ A B
-                _ (fun v => conditional_sub_cps v rest).
-  Definition add (A B : T R_numlimbs) : T R_numlimbs
-    := add_cps A B id.
-  Definition sub_cps (A B : T R_numlimbs) {cpsT} (rest : T R_numlimbs -> cpsT) : cpsT
-    := @sub_then_maybe_add_cps A B _ rest.
-  Definition sub (A B : T R_numlimbs) : T R_numlimbs
-    := sub_cps A B id.
-  Definition opp_cps (A : T R_numlimbs) {cpsT} (rest : T R_numlimbs -> cpsT) : cpsT
-    := sub_cps zero A rest.
-  Definition opp (A : T R_numlimbs) : T R_numlimbs
-    := opp_cps A id.
-  Definition nonzero_cps (A : T R_numlimbs) {cpsT} (f : Z -> cpsT) : cpsT
-    := @nonzero_cps R_numlimbs A cpsT f.
-  Definition nonzero (A : T R_numlimbs) : Z
-    := nonzero_cps A id.
-End WordByWordMontgomery.
-
-Hint Opaque redc pre_redc redc_body redc_loop add sub opp nonzero : uncps.
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
deleted file mode 100644
index 35c9e377b..000000000
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
+++ /dev/null
@@ -1,329 +0,0 @@
-(*** Word-By-Word Montgomery Multiplication Proofs *)
-Require Import Coq.ZArith.BinInt.
-Require Import Coq.micromega.Lia.
-Require Import Crypto.Arithmetic.Saturated.UniformWeight.
-Require Import Crypto.Arithmetic.Saturated.MontgomeryAPI.
-Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Definition.
-Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Proofs.
-Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
-Require Import Crypto.Util.Tactics.BreakMatch.
-
-Local Open Scope Z_scope.
-Local Coercion Z.pos : positive >-> Z.
-Section WordByWordMontgomery.
-  (** XXX TODO: pick better names for things like [R_numlimbs] *)
-  Context (r : positive)
-          (R_numlimbs : nat).
-  Local Notation small := (@small (Z.pos r)).
-  Local Notation eval := (@eval (Z.pos r)).
-  Local Notation addT' := (@MontgomeryAPI.add_S1 (Z.pos r)).
-  Local Notation addT := (@MontgomeryAPI.add (Z.pos r)).
-  Local Notation scmul := (@scmul (Z.pos r)).
-  Local Notation eval_zero := (@eval_zero (Z.pos r)).
-  Local Notation small_zero := (@small_zero r (Zorder.Zgt_pos_0 _)).
-  Local Notation small_scmul := (fun n a v _ _ _ => @small_scmul r (Zorder.Zgt_pos_0 _) n a v).
-  Local Notation eval_join0 := (@eval_zero (Z.pos r) (Zorder.Zgt_pos_0 _)).
-  Local Notation eval_div := (@eval_div (Z.pos r) (Zorder.Zgt_pos_0 _)).
-  Local Notation eval_mod := (@eval_mod (Z.pos r)).
-  Local Notation small_div := (@small_div (Z.pos r)).
-  Local Notation eval_scmul := (fun n a v smallv abound vbound => @eval_scmul (Z.pos r) (Zorder.Zgt_pos_0 _) n a v smallv abound).
-  Local Notation eval_addT := (@eval_add_same (Z.pos r) (Zorder.Zgt_pos_0 _)).
-  Local Notation eval_addT' := (@eval_add_S1 (Z.pos r) (Zorder.Zgt_pos_0 _)).
-  Local Notation drop_high := (@drop_high (S R_numlimbs)).
-  Local Notation small_drop_high := (@small_drop_high (Z.pos r) (S R_numlimbs)).
-  Context (A_numlimbs : nat)
-          (N : T R_numlimbs)
-          (A : T A_numlimbs)
-          (B : T R_numlimbs)
-          (k : Z).
-  Context ri
-          (r_big : r > 1)
-          (small_A : small A)
-          (ri_correct : r*ri mod (eval N) = 1 mod (eval N))
-          (small_N : small N)
-          (small_B : small B)
-          (N_nonzero : eval N <> 0)
-          (N_mask : Tuple.map (Z.land (Z.pos r - 1)) N = N)
-          (k_correct : k * eval N mod r = (-1) mod r).
-  Let R : positive := match (Z.pos r ^ Z.of_nat R_numlimbs)%Z with
-                      | Z.pos R => R
-                      | _ => 1%positive
-                      end.
-  Let Npos : positive := match eval N with
-                         | Z.pos N => N
-                         | _ => 1%positive
-                         end.
-  Local Lemma R_correct : Z.pos R = Z.pos r ^ Z.of_nat R_numlimbs.
-  Proof.
-    assert (0 < r^Z.of_nat R_numlimbs) by (apply Z.pow_pos_nonneg; lia).
-    subst R; destruct (Z.pos r ^ Z.of_nat R_numlimbs) eqn:?; [ | reflexivity | ];
-      lia.
-  Qed.
-  Local Lemma small_addT : forall n a b, small a -> small b -> small (@addT n a b).
-  Proof.
-    intros; apply MontgomeryAPI.small_add; auto; lia.
-  Qed.
-  Local Lemma small_addT' : forall n a b, small a -> small b -> small (@addT' n a b).
-  Proof.
-    intros; apply MontgomeryAPI.small_add_S1; auto; lia.
-  Qed.
-
-  Local Notation conditional_sub_cps := (fun V : T (S R_numlimbs) => @conditional_sub_cps (Z.pos r) _ V N _).
-  Local Notation conditional_sub := (fun V : T (S R_numlimbs) => @conditional_sub (Z.pos r) _ V N).
-  Local Notation eval_conditional_sub' := (fun V small_V V_bound => @eval_conditional_sub (Z.pos r) (Zorder.Zgt_pos_0 _) _  V N small_V small_N V_bound).
-
-  Local Lemma 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.
-  Proof. rewrite R_correct; exact eval_conditional_sub'. Qed.
-  Local Notation small_conditional_sub' := (fun V small_V V_bound => @small_conditional_sub (Z.pos r) (Zorder.Zgt_pos_0 _) _ V N small_V small_N V_bound).
-  Local Lemma small_conditional_sub
-    : forall v : T (S R_numlimbs), small v -> 0 <= eval v < eval N + R -> small (conditional_sub v).
-  Proof. rewrite R_correct; exact small_conditional_sub'. Qed.
-
-  Local Lemma A_bound : 0 <= eval A < Z.pos r ^ Z.of_nat A_numlimbs.
-  Proof. apply eval_small; auto; lia. Qed.
-  Local Lemma B_bound' : 0 <= eval B < r^Z.of_nat R_numlimbs.
-  Proof. apply eval_small; auto; lia. Qed.
-  Local Lemma N_bound' : 0 <= eval N < r^Z.of_nat R_numlimbs.
-  Proof. apply eval_small; auto; lia. Qed.
-  Local Lemma N_bound : 0 < eval N < r^Z.of_nat R_numlimbs.
-  Proof. pose proof N_bound'; lia. Qed.
-  Local Lemma Npos_correct: eval N = Z.pos Npos.
-  Proof. pose proof N_bound; subst Npos; destruct (eval N); [ | reflexivity | ]; lia. Qed.
-  Local Lemma N_lt_R : eval N < R.
-  Proof. rewrite R_correct; apply N_bound. Qed.
-  Local Lemma B_bound : 0 <= eval B < R.
-  Proof. rewrite R_correct; apply B_bound'. Qed.
-  Local Lemma eval_drop_high : forall v, small v -> eval (drop_high v) = eval v mod (r * r^Z.of_nat R_numlimbs).
-  Proof.
-    intros; erewrite eval_drop_high by (eassumption || lia).
-    f_equal; unfold uweight.
-    rewrite Znat.Nat2Z.inj_succ, Z.pow_succ_r by lia; reflexivity.
-  Qed.
-
-  Local Notation redc_body_no_cps := (@redc_body_no_cps r R_numlimbs N).
-  Local Notation redc_body_cps := (@redc_body_cps r R_numlimbs N).
-  Local Notation redc_body := (@redc_body r R_numlimbs N).
-  Local Notation redc_loop_no_cps := (@redc_loop_no_cps r R_numlimbs N B k).
-  Local Notation redc_loop_cps := (@redc_loop_cps r R_numlimbs N B k).
-  Local Notation redc_loop := (@redc_loop r R_numlimbs N B k).
-  Local Notation pre_redc_no_cps := (@pre_redc_no_cps r R_numlimbs N A_numlimbs A B k).
-  Local Notation pre_redc_cps := (@pre_redc_cps r R_numlimbs N A_numlimbs A B k).
-  Local Notation pre_redc := (@pre_redc r R_numlimbs N A_numlimbs A B k).
-  Local Notation redc_no_cps := (@redc_no_cps r R_numlimbs N A_numlimbs A B k).
-  Local Notation redc_cps := (@redc_cps r R_numlimbs N A_numlimbs A B k).
-  Local Notation redc := (@redc r R_numlimbs N A_numlimbs A B k).
-
-  Definition redc_no_cps_bound : 0 <= eval redc_no_cps < R
-    := @redc_bound T (@eval) (@zero) (@divmod) r r_big R R_numlimbs R_correct (@small) eval_zero small_zero eval_div eval_mod small_div (@scmul) eval_scmul small_scmul (@addT) eval_addT small_addT (@addT') eval_addT' small_addT' drop_high eval_drop_high small_drop_high N Npos Npos_correct small_N N_lt_R conditional_sub eval_conditional_sub B B_bound small_B ri k A_numlimbs A small_A A_bound.
-  Definition redc_no_cps_bound_N : eval B < eval N -> 0 <= eval redc_no_cps < eval N
-    := @redc_bound_N T (@eval) (@zero) (@divmod) r r_big R R_numlimbs R_correct (@small) eval_zero small_zero eval_div eval_mod small_div (@scmul) eval_scmul small_scmul (@addT) eval_addT small_addT (@addT') eval_addT' small_addT' drop_high eval_drop_high small_drop_high N Npos Npos_correct small_N N_lt_R conditional_sub eval_conditional_sub B B_bound small_B ri k A_numlimbs A small_A.
-  Definition redc_no_cps_mod_N
-    : (eval redc_no_cps) mod (eval N) = (eval A * eval B * ri^(Z.of_nat A_numlimbs)) mod (eval N)
-    := @redc_mod_N T (@eval) (@zero) (@divmod) r r_big R R_numlimbs R_correct (@small) eval_zero small_zero eval_div eval_mod small_div (@scmul) eval_scmul small_scmul (@addT) eval_addT small_addT (@addT') eval_addT' small_addT' drop_high eval_drop_high small_drop_high N Npos Npos_correct small_N N_lt_R conditional_sub eval_conditional_sub B B_bound small_B ri ri_correct k k_correct A_numlimbs A small_A A_bound.
-  Definition small_redc_no_cps
-    : small redc_no_cps
-    := @small_redc T (@eval) (@zero) (@divmod) r r_big R R_numlimbs R_correct (@small) eval_zero small_zero eval_div eval_mod small_div (@scmul) eval_scmul small_scmul (@addT) eval_addT small_addT (@addT') eval_addT' small_addT' drop_high eval_drop_high small_drop_high N Npos Npos_correct small_N N_lt_R conditional_sub small_conditional_sub B B_bound small_B ri k A_numlimbs A small_A A_bound.
-
-  Lemma redc_body_cps_id pred_A_numlimbs (A' : T (S pred_A_numlimbs)) (S' : T (S R_numlimbs)) {cpsT} f
-    : @redc_body_cps pred_A_numlimbs A' B k S' cpsT f = f (redc_body A' B k S').
-  Proof.
-    unfold redc_body, redc_body_cps, LetIn.Let_In.
-    repeat first [ reflexivity
-                 | break_innermost_match_step
-                 | progress autorewrite with uncps ].
-  Qed.
-
-  Lemma redc_loop_cps_id (count : nat) (A_S : T count * T (S R_numlimbs)) {cpsT} f
-    : @redc_loop_cps cpsT count f A_S = f (redc_loop count A_S).
-  Proof.
-    unfold redc_loop.
-    revert A_S f.
-    induction count as [|count IHcount].
-    { reflexivity. }
-    { intros [A' S']; simpl; intros.
-      etransitivity; rewrite @redc_body_cps_id; [ rewrite IHcount | ]; reflexivity. }
-  Qed.
-  Lemma pre_redc_cps_id {cpsT} f : @pre_redc_cps cpsT f = f pre_redc.
-  Proof.
-    unfold pre_redc, pre_redc_cps.
-    etransitivity; rewrite redc_loop_cps_id; [ | reflexivity ]; break_innermost_match;
-      reflexivity.
-  Qed.
-  Lemma redc_cps_id {cpsT} f : @redc_cps cpsT f = f redc.
-  Proof.
-    unfold redc, redc_cps.
-    etransitivity; rewrite pre_redc_cps_id; [ | reflexivity ];
-      autorewrite with uncps;
-      reflexivity.
-  Qed.
-
-  Lemma redc_body_id_no_cps pred_A_numlimbs A' S'
-    : @redc_body pred_A_numlimbs A' B k S' = redc_body_no_cps B k (A', S').
-  Proof.
-    unfold redc_body, redc_body_cps, redc_body_no_cps, Abstract.Dependent.Definition.redc_body, LetIn.Let_In, id.
-    repeat autounfold with word_by_word_montgomery.
-    repeat first [ reflexivity
-                 | progress cbn [fst snd id]
-                 | progress autorewrite with uncps
-                 | break_innermost_match_step
-                 | f_equal; [] ].
-  Qed.
-  Lemma redc_loop_cps_id_no_cps count A_S
-    : redc_loop count A_S = redc_loop_no_cps count A_S.
-  Proof.
-    unfold redc_loop_no_cps, id.
-    revert A_S.
-    induction count as [|count IHcount]; simpl; [ reflexivity | ].
-    intros [A' S']; unfold redc_loop; simpl.
-    rewrite redc_body_cps_id, redc_loop_cps_id, IHcount, redc_body_id_no_cps.
-    reflexivity.
-  Qed.
-  Lemma pre_redc_cps_id_no_cps : pre_redc = pre_redc_no_cps.
-  Proof.
-    unfold pre_redc, pre_redc_cps, pre_redc_no_cps, Abstract.Dependent.Definition.pre_redc.
-    rewrite redc_loop_cps_id, (surjective_pairing (redc_loop _ _)).
-    rewrite redc_loop_cps_id_no_cps; reflexivity.
-  Qed.
-  Lemma redc_cps_id_no_cps : redc = redc_no_cps.
-  Proof.
-    unfold redc, redc_no_cps, redc_cps, Abstract.Dependent.Definition.redc.
-    rewrite pre_redc_cps_id, pre_redc_cps_id_no_cps.
-    autorewrite with uncps; reflexivity.
-  Qed.
-
-  Lemma redc_bound : 0 <= eval redc < R.
-  Proof. rewrite redc_cps_id_no_cps; apply redc_no_cps_bound. Qed.
-  Lemma redc_bound_N : eval B < eval N -> 0 <= eval redc < eval N.
-  Proof. rewrite redc_cps_id_no_cps; apply redc_no_cps_bound_N. Qed.
-  Lemma redc_mod_N
-    : (eval redc) mod (eval N) = (eval A * eval B * ri^(Z.of_nat A_numlimbs)) mod (eval N).
-  Proof. rewrite redc_cps_id_no_cps; apply redc_no_cps_mod_N. Qed.
-  Lemma small_redc
-    : small redc.
-  Proof. rewrite redc_cps_id_no_cps; apply small_redc_no_cps. Qed.
-
-  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 Notation add_no_cps := (@add_no_cps r R_numlimbs N Av Bv).
-    Local Notation add_cps := (@add_cps r R_numlimbs N Av Bv).
-    Local Notation add := (@add r R_numlimbs N Av Bv).
-    Local Notation sub_no_cps := (@sub_no_cps r R_numlimbs N Av Bv).
-    Local Notation sub_cps := (@sub_cps r R_numlimbs N Av Bv).
-    Local Notation sub := (@sub r R_numlimbs N Av Bv).
-    Local Notation opp_no_cps := (@opp_no_cps r R_numlimbs N Av).
-    Local Notation opp_cps := (@opp_cps r R_numlimbs N Av).
-    Local Notation opp := (@opp r R_numlimbs N Av).
-    Local Notation sub_then_maybe_add_cps :=
-       (fun p q => @sub_then_maybe_add_cps (Z.pos r) R_numlimbs (Z.pos r - 1) p q N).
-    Local Notation sub_then_maybe_add :=
-      (fun p q => @sub_then_maybe_add (Z.pos r) R_numlimbs (Z.pos r - 1) p q N).
-    Local Notation eval_sub_then_maybe_add :=
-      (fun p q smp smq => @eval_sub_then_maybe_add (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) p q N smp smq small_N N_mask).
-    Local Notation small_sub_then_maybe_add :=
-      (fun p q => @small_sub_then_maybe_add (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) p q N).
-
-    Definition add_no_cps_bound : 0 <= eval add_no_cps < eval N
-      := @add_bound T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@eval_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound.
-    Definition sub_no_cps_bound : 0 <= eval sub_no_cps < eval N
-      := @sub_bound T (@eval) r R R_numlimbs (@small) N (@sub_then_maybe_add) (@eval_sub_then_maybe_add) Av Bv small_Av small_Bv Av_bound Bv_bound.
-    Definition opp_no_cps_bound : 0 <= eval opp_no_cps < eval N
-      := @opp_bound T (@eval) (@zero) r R R_numlimbs (@small) (@eval_zero) (@small_zero) N (@sub_then_maybe_add) (@eval_sub_then_maybe_add) Av small_Av Av_bound.
-
-    Definition small_add_no_cps : small add_no_cps
-      := @small_add T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@small_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound.
-    Definition small_sub_no_cps : small sub_no_cps
-      := @small_sub T R_numlimbs (@small) (@sub_then_maybe_add) (@small_sub_then_maybe_add) Av Bv.
-    Definition small_opp_no_cps : small opp_no_cps
-      := @small_opp T (@zero) R_numlimbs (@small) (@sub_then_maybe_add) (@small_sub_then_maybe_add) Av.
-
-    Definition eval_add_no_cps : eval add_no_cps = eval Av + eval Bv + (if eval N <=? eval Av + eval Bv then - eval N else 0)
-      := @eval_add T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@eval_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound.
-    Definition eval_sub_no_cps : eval sub_no_cps = eval Av - eval Bv + (if eval Av - eval Bv <? 0 then eval N else 0)
-      := @eval_sub T (@eval) R_numlimbs (@small) N (@sub_then_maybe_add) (@eval_sub_then_maybe_add) Av Bv small_Av small_Bv Av_bound Bv_bound.
-    Definition eval_opp_no_cps : eval opp_no_cps = (if eval Av =? 0 then 0 else eval N) - eval Av
-      := @eval_opp T (@eval) (@zero) r R R_numlimbs (@small) (@eval_zero) (@small_zero) N (@sub_then_maybe_add ) (@eval_sub_then_maybe_add) Av small_Av Av_bound.
-
-    Definition eval_add_no_cps_mod_N : eval add_no_cps mod eval N = (eval Av + eval Bv) mod eval N
-      := @eval_add_mod_N T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@eval_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound.
-    Definition eval_sub_no_cps_mod_N : eval sub_no_cps mod eval N = (eval Av - eval Bv) mod eval N
-      := @eval_sub_mod_N T (@eval) R_numlimbs (@small) N (@sub_then_maybe_add) (@eval_sub_then_maybe_add) Av Bv small_Av small_Bv Av_bound Bv_bound.
-    Definition eval_opp_no_cps_mod_N : eval opp_no_cps mod eval N = (-eval Av) mod eval N
-      := @eval_opp_mod_N T (@eval) (@zero) r R R_numlimbs (@small) (@eval_zero) (@small_zero) N (@sub_then_maybe_add) (@eval_sub_then_maybe_add) Av small_Av Av_bound.
-
-    Lemma add_cps_id_no_cps : add = add_no_cps.
-    Proof.
-      unfold add_no_cps, add, add_cps, Abstract.Dependent.Definition.add; autorewrite with uncps; reflexivity.
-    Qed.
-    Lemma sub_cps_id_no_cps : sub = sub_no_cps.
-    Proof.
-      unfold sub_no_cps, sub, sub_cps, Abstract.Dependent.Definition.sub; autorewrite with uncps; reflexivity.
-    Qed.
-    Lemma opp_cps_id_no_cps : opp = opp_no_cps.
-    Proof.
-      unfold opp, opp_cps, opp_no_cps, Abstract.Dependent.Definition.opp, sub_no_cps, sub, sub_cps, Abstract.Dependent.Definition.sub; autorewrite with uncps; reflexivity.
-    Qed.
-
-    Lemma add_cps_id {cpsT} f : @add_cps cpsT f = f add.
-    Proof. unfold add, add_cps; autorewrite with uncps; reflexivity. Qed.
-    Lemma sub_cps_id {cpsT} f : @sub_cps cpsT f = f sub.
-    Proof. unfold sub, sub_cps; autorewrite with uncps. reflexivity. Qed.
-    Lemma opp_cps_id {cpsT} f : @opp_cps cpsT f = f opp.
-    Proof. unfold opp, opp_cps, sub, sub_cps; autorewrite with uncps. reflexivity. Qed.
-
-    Local Ltac do_rewrite :=
-      first [ rewrite add_cps_id_no_cps
-            | rewrite sub_cps_id_no_cps
-            | rewrite opp_cps_id_no_cps ].
-    Local Ltac do_apply :=
-      first [ apply add_no_cps_bound
-            | apply sub_no_cps_bound
-            | apply opp_no_cps_bound
-            | apply small_add_no_cps
-            | apply small_sub_no_cps
-            | apply small_opp_no_cps
-            | apply eval_add_no_cps
-            | apply eval_sub_no_cps
-            | apply eval_opp_no_cps
-            | apply eval_add_no_cps_mod_N
-            | apply eval_sub_no_cps_mod_N
-            | apply eval_opp_no_cps_mod_N ].
-    Local Ltac t := do_rewrite; do_apply.
-
-    Lemma add_bound : 0 <= eval add < eval N. Proof. t. Qed.
-    Lemma sub_bound : 0 <= eval sub < eval N. Proof. t. Qed.
-    Lemma opp_bound : 0 <= eval opp < eval N. Proof. t. Qed.
-
-    Lemma small_add : small add. Proof. t. Qed.
-    Lemma small_sub : small sub. Proof. t. Qed.
-    Lemma small_opp : small opp. Proof. t. Qed.
-
-    Lemma eval_add : eval add = eval Av + eval Bv + (if eval N <=? eval Av + eval Bv then - eval N else 0).
-    Proof. t. Qed.
-    Lemma eval_sub : eval sub = eval Av - eval Bv + (if eval Av - eval Bv <? 0 then eval N else 0).
-    Proof. t. Qed.
-    Lemma eval_opp : eval opp = (if eval Av =? 0 then 0 else eval N) - eval Av.
-    Proof. t. Qed.
-
-    Lemma eval_add_mod_N : eval add mod eval N = (eval Av + eval Bv) mod eval N.
-    Proof. t. Qed.
-    Lemma eval_sub_mod_N : eval sub mod eval N = (eval Av - eval Bv) mod eval N.
-    Proof. t. Qed.
-    Lemma eval_opp_mod_N : eval opp mod eval N = (-eval Av) mod eval N.
-    Proof. t. Qed.
-  End add_sub.
-
-  Section nonzero.
-    Lemma nonzero_cps_id Av {cpsT} f : @nonzero_cps R_numlimbs Av cpsT f = f (@nonzero R_numlimbs Av).
-    Proof. unfold nonzero, nonzero_cps; autorewrite with uncps; reflexivity. Qed.
-
-    Lemma eval_nonzero Av : small Av -> @nonzero R_numlimbs Av = 0 <-> eval Av = 0.
-    Proof. apply eval_nonzero; lia. Qed.
-  End nonzero.
-End WordByWordMontgomery.
-
-Hint Rewrite redc_body_cps_id redc_loop_cps_id pre_redc_cps_id redc_cps_id add_cps_id sub_cps_id opp_cps_id : uncps.