Fix misnamed references in Specific/ (broke after saturated arithetic reorg)

12 files changed, 176 insertions, 153 deletions

diff --git a/src/Specific/IntegrationTestMontgomeryP256_128.v b/src/Specific/IntegrationTestMontgomeryP256_128.v
index 2283a3801..00f751908 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128.v
+++ b/src/Specific/IntegrationTestMontgomeryP256_128.v
@@ -6,6 +6,8 @@ Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Specific.MontgomeryP256_128.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -31,8 +33,8 @@ Section BoundedField25p5.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
   Let feBW : Type := BoundedWord sz bitwidth bounds.
   Let eval : feBW -> Z :=
-    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
-  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+    fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
   Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
   Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
   Let phi : feBW -> F m :=
@@ -62,7 +64,7 @@ Section BoundedField25p5.
     eexists_sig_etransitivity.
     set (mulmodZ := proj1_sig mulmod_256).
     context_to_dlet_in_rhs mulmodZ; cbv [mulmodZ].
-    cbv beta iota delta [mulmod_256 mulmod_256'' mulmod_256' proj1_sig Saturated.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    cbv beta iota delta [mulmod_256 mulmod_256'' mulmod_256' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
     reflexivity.
     sig_dlet_in_rhs_to_context.
     apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v b/src/Specific/IntegrationTestMontgomeryP256_128_Add.v
index 459edf1a6..367f63a0b 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_Add.v
@@ -6,6 +6,8 @@ Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Specific.MontgomeryP256_128.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -31,8 +33,8 @@ Section BoundedField25p5.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
   Let feBW : Type := BoundedWord sz bitwidth bounds.
   Let eval : feBW -> Z :=
-    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
-  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+    fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
   Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
   Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
   Let phi : feBW -> F m :=
@@ -62,7 +64,7 @@ Section BoundedField25p5.
     eexists_sig_etransitivity.
     set (addZ := proj1_sig add).
     context_to_dlet_in_rhs addZ; cbv [addZ].
-    cbv beta iota delta [add add' proj1_sig Saturated.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    cbv beta iota delta [add add' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
     reflexivity.
     sig_dlet_in_rhs_to_context.
     apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
index bc14eeaad..6adeac3f9 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
@@ -6,6 +6,8 @@ Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Specific.MontgomeryP256_128.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -35,8 +37,8 @@ Section BoundedField25p5.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
   Let feBW : Type := BoundedWord sz bitwidth bounds.
   Let eval : feBW -> Z :=
-    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
-  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+    fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
   Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
   Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
   Let phi : feBW -> F m :=
@@ -78,7 +80,7 @@ Section BoundedField25p5.
     eexists_sig_etransitivity.
     set (nonzeroZ := proj1_sig nonzero).
     context_to_dlet_in_rhs nonzeroZ; cbv [nonzeroZ].
-    cbv beta iota delta [nonzero nonzero' proj1_sig Saturated.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    cbv beta iota delta [nonzero nonzero' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
     reflexivity.
     sig_dlet_in_rhs_to_context.
     match goal with
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v b/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v
index a8215c03d..1a609d7b4 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v
@@ -6,6 +6,8 @@ Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Specific.MontgomeryP256_128.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -31,8 +33,8 @@ Section BoundedField25p5.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
   Let feBW : Type := BoundedWord sz bitwidth bounds.
   Let eval : feBW -> Z :=
-    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
-  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+    fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
   Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
   Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
   Let phi : feBW -> F m :=
@@ -62,7 +64,7 @@ Section BoundedField25p5.
     eexists_sig_etransitivity.
     set (oppZ := proj1_sig opp).
     context_to_dlet_in_rhs oppZ; cbv [oppZ].
-    cbv beta iota delta [opp opp' proj1_sig Saturated.T lift1_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    cbv beta iota delta [opp opp' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
     reflexivity.
     sig_dlet_in_rhs_to_context.
     apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
index 98cb22343..916659ab5 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
@@ -6,6 +6,8 @@ Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Specific.MontgomeryP256_128.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -31,8 +33,8 @@ Section BoundedField25p5.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
   Let feBW : Type := BoundedWord sz bitwidth bounds.
   Let eval : feBW -> Z :=
-    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
-  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+    fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
   Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
   Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
   Let phi : feBW -> F m :=
@@ -62,7 +64,7 @@ Section BoundedField25p5.
     eexists_sig_etransitivity.
     set (subZ := proj1_sig sub).
     context_to_dlet_in_rhs subZ; cbv [subZ].
-    cbv beta iota delta [sub sub' proj1_sig Saturated.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    cbv beta iota delta [sub sub' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
     reflexivity.
     sig_dlet_in_rhs_to_context.
     apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v
index 323be5533..9c0336503 100644
--- a/src/Specific/MontgomeryP256_128.v
+++ b/src/Specific/MontgomeryP256_128.v
@@ -2,6 +2,8 @@ Require Import Coq.micromega.Lia.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Proofs.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Util.Sigma.Lift.
 Require Import Coq.ZArith.BinInt.
 Require Import Coq.PArith.BinPos.
@@ -22,9 +24,9 @@ Definition r' := Eval vm_compute in Zpow_facts.Zpow_mod (Z.pos r) (Z.pos m - 2)
 Definition r'_correct := eq_refl : ((Z.pos r * r') mod (Z.pos m) = 1)%Z.
 Definition m' : Z := Eval vm_compute in Option.invert_Some (Z.modinv_fueled 10 (-Z.pos m) (Z.pos r)).
 Definition m'_correct := eq_refl : ((Z.pos m * m') mod (Z.pos r) = (-1) mod Z.pos r)%Z.
-Definition m_p256 := eq_refl (Z.pos m) <: Z.pos m = Saturated.eval (n:=sz) (Z.pos r) p256.
+Definition m_p256 := eq_refl (Z.pos m) <: Z.pos m = MontgomeryAPI.eval (n:=sz) (Z.pos r) p256.
 
-Lemma r'_pow_correct : ((r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz) mod Saturated.eval (n:=sz) (Z.pos r) p256 = 1)%Z.
+Lemma r'_pow_correct : ((r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 = 1)%Z.
 Proof. vm_compute; reflexivity. Qed.
 
 Definition mulmod_256' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
@@ -44,44 +46,44 @@ Proof.
        fst snd length List.seq List.hd List.app
        redc pre_redc_cps redc_cps redc_loop_cps redc_body_cps
        Positional.to_associational_cps
-       Saturated.divmod_cps
-       Saturated.conditional_sub_cps
-       Saturated.scmul_cps
-       Saturated.uweight
-       Saturated.Columns.mul_cps
-       Saturated.Associational.mul_cps
+       MontgomeryAPI.divmod_cps
+       MontgomeryAPI.conditional_sub_cps
+       MontgomeryAPI.scmul_cps
+       uweight
+       MontgomeryAPI.Columns.mul_cps
+       MontgomeryAPI.Associational.mul_cps
        (*Z.of_nat Pos.of_succ_nat  Nat.pred
        Z.pow Z.pow_pos Z.mul Pos.iter Pos.mul Pos.succ*)
        Tuple.hd Tuple.append Tuple.tl Tuple.hd' Tuple.tl' CPSUtil.Tuple.left_tl_cps CPSUtil.Tuple.left_hd_cps CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps
        CPSUtil.Tuple.map2_cps
-       Saturated.Columns.from_associational_cps
-       Saturated.Associational.multerm_cps
-       Saturated.Positional.sat_add_cps
-       Saturated.Positional.sat_sub_cps
-       Saturated.Positional.chain_op_cps
-       Saturated.Positional.chain_op'_cps
-       Saturated.Columns.compact_cps
-       Saturated.Columns.compact_step_cps
-       Saturated.Columns.compact_digit_cps
-       Saturated.drop_high_cps
-       Saturated.add_cps
-       Saturated.add_S1_cps
-       Saturated.Columns.add_cps
-       Saturated.Columns.cons_to_nth_cps
+       MontgomeryAPI.Columns.from_associational_cps
+       MontgomeryAPI.Associational.multerm_cps
+       MontgomeryAPI.Positional.sat_add_cps
+       MontgomeryAPI.Positional.sat_sub_cps
+       MontgomeryAPI.Positional.chain_op_cps
+       MontgomeryAPI.Positional.chain_op'_cps
+       MontgomeryAPI.Columns.compact_cps
+       MontgomeryAPI.Columns.compact_step_cps
+       MontgomeryAPI.Columns.compact_digit_cps
+       MontgomeryAPI.drop_high_cps
+       MontgomeryAPI.add_cps
+       MontgomeryAPI.add_S1_cps
+       MontgomeryAPI.Columns.add_cps
+       MontgomeryAPI.Columns.cons_to_nth_cps
        Nat.pred
-       Saturated.join0
-       Saturated.join0_cps CPSUtil.Tuple.left_append_cps
+       MontgomeryAPI.join0
+       MontgomeryAPI.join0_cps CPSUtil.Tuple.left_append_cps
        CPSUtil.Tuple.mapi_with_cps
        id
-       Positional.zeros Saturated.zero Saturated.Columns.nils Tuple.repeat Tuple.append
+       Positional.zeros MontgomeryAPI.zero MontgomeryAPI.Columns.nils Tuple.repeat Tuple.append
        Positional.place_cps
        CPSUtil.Tuple.mapi_with'_cps Tuple.hd Tuple.hd' Tuple.tl Tuple.tl' CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps fst snd
        Z.of_nat fst snd Z.pow Z.pow_pos Pos.of_succ_nat Z.div Z.mul Pos.mul Z.modulo Z.div_eucl Z.pos_div_eucl Z.leb Z.compare Pos.compare_cont Pos.compare Z.pow_pos Pos.iter Z.mul Pos.succ Z.ltb Z.gtb Z.geb Z.div Z.sub Z.pos_sub Z.add Z.opp Z.double
        Decidable.dec Decidable.dec_eq_Z Z.eq_dec Z_rec Z_rec Z_rect
-       Positional.zeros Saturated.zero Saturated.Columns.nils Tuple.repeat Tuple.append
+       Positional.zeros MontgomeryAPI.zero MontgomeryAPI.Columns.nils Tuple.repeat Tuple.append
        (*
-       Saturated.Associational.multerm_cps
-       Saturated.Columns.from_associational_cps Positional.place_cps Saturated.Columns.cons_to_nth_cps Saturated.Columns.nils
+       MontgomeryAPI.Associational.multerm_cps
+       MontgomeryAPI.Columns.from_associational_cps Positional.place_cps MontgomeryAPI.Columns.cons_to_nth_cps MontgomeryAPI.Columns.nils
 Tuple.append
 Tuple.from_list Tuple.from_list'
 Tuple.from_list_default Tuple.from_list_default'
@@ -89,7 +91,7 @@ Tuple.hd
 Tuple.repeat
 Tuple.tl
 Tuple.tuple *)
-       (* Saturated.add_cps Saturated.divmod_cps Saturated.drop_high_cps Saturated.scmul_cps Saturated.zero Saturated.Columns.mul_cps Saturated.Columns.add_cps Saturated.uweight Saturated.T *)
+       (* MontgomeryAPI.add_cps MontgomeryAPI.divmod_cps MontgomeryAPI.drop_high_cps MontgomeryAPI.scmul_cps MontgomeryAPI.zero MontgomeryAPI.Columns.mul_cps MontgomeryAPI.Columns.add_cps uweight MontgomeryAPI.T *)
             (*
             CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps'
 Positional.zeros
@@ -112,9 +114,9 @@ Defined.
 
 Definition mulmod_256'' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
                         | forall (A B : Tuple.tuple Z sz),
-                            Saturated.small (Z.pos r) A -> Saturated.small (Z.pos r) B ->
-                            let eval := Saturated.eval (Z.pos r) in
-                            (Saturated.small (Z.pos r) (f A B)
+                            small (Z.pos r) A -> small (Z.pos r) B ->
+                            let eval := MontgomeryAPI.eval (Z.pos r) in
+                            (small (Z.pos r) (f A B)
                              /\ (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)
                              /\ (eval (f A B) mod Z.pos m
                                  = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z
@@ -129,10 +131,10 @@ Proof.
           | _ => assumption
           | [ |- _ = _ :> Z ] => vm_compute; reflexivity
           | _ => reflexivity
-          | [ |- Saturated.small (Z.pos r) p256 ]
+          | [ |- small (Z.pos r) p256 ]
             => hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or;
                subst; try lia
-          | [ |- Saturated.eval (Z.pos r) p256 <> 0%Z ]
+          | [ |- MontgomeryAPI.eval (Z.pos r) p256 <> 0%Z ]
             => vm_compute; lia
           end
     ).
@@ -185,10 +187,10 @@ Defined.
 Import ModularArithmetic.
 
 (*Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                        | forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                                 (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
-                            Saturated.small (Z.pos r) (f A B)
-                            /\ (let eval := Saturated.eval (Z.pos r) in
+                        | forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                                 (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+                            small (Z.pos r) (f A B)
+                            /\ (let eval := MontgomeryAPI.eval (Z.pos r) in
                                 0 <= eval (f A B) < Z.pos r^Z.of_nat sz
                                 /\ (eval (f A B) mod Z.pos m
                                     = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z
@@ -200,13 +202,13 @@ Definition montgomery_to_F (v : Z) : F m
   := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F.
 
 Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                        | let eval := Saturated.eval (Z.pos r) in
-                          (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                                  (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                        | let eval := MontgomeryAPI.eval (Z.pos r) in
+                          (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                               montgomery_to_F (eval (f A B))
                               = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F)
-                          /\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                                     (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                          /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                                     (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                                  (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }.
 Proof.
   exists (proj1_sig mulmod_256'').
@@ -230,25 +232,25 @@ Local Ltac t_fin :=
            | _ => assumption
            | [ |- _ = _ :> Z ] => vm_compute; reflexivity
            | _ => reflexivity
-           | [ |- Saturated.small (Z.pos r) p256 ]
+           | [ |- small (Z.pos r) p256 ]
              => hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or;
                 subst; try lia
-           | [ |- Saturated.eval (Z.pos r) p256 <> 0%Z ]
+           | [ |- MontgomeryAPI.eval (Z.pos r) p256 <> 0%Z ]
              => vm_compute; lia
            | [ |- and _ _ ] => split
-           | [ |- (0 <= Saturated.eval (Z.pos r) _)%Z ] => apply Saturated.eval_small
+           | [ |- (0 <= MontgomeryAPI.eval (Z.pos r) _)%Z ] => apply MontgomeryAPI.eval_small
            end.. ].
 
 Definition add : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := Saturated.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                 | let eval := MontgomeryAPI.eval (Z.pos r) in
+                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                         (eval A < eval p256
                          -> eval B < eval p256
                          -> montgomery_to_F (eval (f A B))
                             = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                               (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                            (eval A < eval p256
                             -> eval B < eval p256
                             -> 0 <= eval (f A B) < eval p256)))%Z }.
@@ -265,15 +267,15 @@ Proof.
 Defined.
 
 Definition sub : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := Saturated.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                 | let eval := MontgomeryAPI.eval (Z.pos r) in
+                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                         (eval A < eval p256
                          -> eval B < eval p256
                          -> montgomery_to_F (eval (f A B))
                             = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                         (eval A < eval p256
                          -> eval B < eval p256
                          -> 0 <= eval (f A B) < eval p256)))%Z }.
@@ -290,12 +292,12 @@ Proof.
 Defined.
 
 Definition opp : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := Saturated.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A),
+                 | let eval := MontgomeryAPI.eval (Z.pos r) in
+                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
                         (eval A < eval p256
                          -> montgomery_to_F (eval (f A))
                             = (F.opp (montgomery_to_F (eval A)))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A),
+                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
                            (eval A < eval p256
                             -> 0 <= eval (f A) < eval p256)))%Z }.
 Proof.
@@ -311,8 +313,8 @@ Proof.
 Defined.
 
 Definition nonzero : { f:Tuple.tuple Z sz -> Z
-                     | let eval := Saturated.eval (Z.pos r) in
-                       forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A),
+                     | let eval := MontgomeryAPI.eval (Z.pos r) in
+                       forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
                          (eval A < eval p256
                           -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
 Proof.
@@ -320,14 +322,14 @@ Proof.
   abstract (
       intros eval A H **; rewrite (proj2_sig nonzero'), (@eval_nonzero r) by (eassumption || reflexivity);
       subst eval;
-      unfold montgomery_to_F, Saturated.uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul;
+      unfold montgomery_to_F, uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul;
       rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256;
       let H := fresh in
       split; intro H;
       [ rewrite H; autorewrite with zsimplify_const; reflexivity
-      | cut ((Saturated.eval (Z.pos r) A * (r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz)) mod Saturated.eval (n:=sz) (Z.pos r) p256 = 0)%Z;
+      | cut ((MontgomeryAPI.eval (Z.pos r) A * (r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz)) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 = 0)%Z;
         [ rewrite Z.mul_mod, r'_pow_correct; autorewrite with zsimplify_const; pull_Zmod; [ | vm_compute; congruence ];
-          rewrite Z.mod_small; [ trivial | split; try assumption; apply Saturated.eval_small; try assumption; lia ]
+          rewrite Z.mod_small; [ trivial | split; try assumption; apply MontgomeryAPI.eval_small; try assumption; lia ]
         | rewrite Z.mul_assoc, Z.mul_mod, H by (vm_compute; congruence); autorewrite with zsimplify_const; reflexivity ] ]
     ).
 Defined.
diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.v b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.v
index 0cd6661f3..d600869bd 100644
--- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.v
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.v
@@ -6,6 +6,8 @@ Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -31,8 +33,8 @@ Section BoundedField25p5.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
   Let feBW : Type := BoundedWord sz bitwidth bounds.
   Let eval : feBW -> Z :=
-    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
-  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+    fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
   Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
   Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
   Let phi : feBW -> F m :=
@@ -62,7 +64,7 @@ Section BoundedField25p5.
     eexists_sig_etransitivity.
     set (mulmodZ := proj1_sig mulmod_256).
     context_to_dlet_in_rhs mulmodZ; cbv [mulmodZ].
-    cbv beta iota delta [mulmod_256 mulmod_256'' mulmod_256' proj1_sig Saturated.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
+    cbv beta iota delta [mulmod_256 mulmod_256'' mulmod_256' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
     reflexivity.
     sig_dlet_in_rhs_to_context.
     apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Add.v b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Add.v
index 9c24ae7bc..1ea0fbc35 100644
--- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Add.v
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Add.v
@@ -2,10 +2,11 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.Lists.List.
 Local Open Scope Z_scope.
 
-Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -31,8 +32,8 @@ Section BoundedField25p5.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
   Let feBW : Type := BoundedWord sz bitwidth bounds.
   Let eval : feBW -> Z :=
-    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
-  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+    fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
   Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
   Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
   Let phi : feBW -> F m :=
@@ -62,7 +63,7 @@ Section BoundedField25p5.
     eexists_sig_etransitivity.
     set (addZ := proj1_sig add).
     context_to_dlet_in_rhs addZ; cbv [addZ].
-    cbv beta iota delta [add add' proj1_sig Saturated.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    cbv beta iota delta [add add' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
     reflexivity.
     sig_dlet_in_rhs_to_context.
     apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Nonzero.v b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Nonzero.v
index 5f0d15b18..cfea6e957 100644
--- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Nonzero.v
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Nonzero.v
@@ -6,6 +6,8 @@ Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -35,8 +37,8 @@ Section BoundedField25p5.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
   Let feBW : Type := BoundedWord sz bitwidth bounds.
   Let eval : feBW -> Z :=
-    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
-  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+    fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
   Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
   Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
   Let phi : feBW -> F m :=
@@ -78,7 +80,7 @@ Section BoundedField25p5.
     eexists_sig_etransitivity.
     set (nonzeroZ := proj1_sig nonzero).
     context_to_dlet_in_rhs nonzeroZ; cbv [nonzeroZ].
-    cbv beta iota delta [nonzero nonzero' proj1_sig Saturated.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    cbv beta iota delta [nonzero nonzero' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
     reflexivity.
     sig_dlet_in_rhs_to_context.
     match goal with
diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Opp.v b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Opp.v
index 6527162a0..ef4ea6aa6 100644
--- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Opp.v
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Opp.v
@@ -6,6 +6,8 @@ Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -31,8 +33,8 @@ Section BoundedField25p5.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
   Let feBW : Type := BoundedWord sz bitwidth bounds.
   Let eval : feBW -> Z :=
-    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
-  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+    fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
   Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
   Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
   Let phi : feBW -> F m :=
@@ -62,7 +64,7 @@ Section BoundedField25p5.
     eexists_sig_etransitivity.
     set (oppZ := proj1_sig opp).
     context_to_dlet_in_rhs oppZ; cbv [oppZ].
-    cbv beta iota delta [opp opp' proj1_sig Saturated.T lift1_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    cbv beta iota delta [opp opp' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
     reflexivity.
     sig_dlet_in_rhs_to_context.
     apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Sub.v b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Sub.v
index ffe973b85..d01471804 100644
--- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Sub.v
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Sub.v
@@ -6,6 +6,8 @@ Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -31,8 +33,8 @@ Section BoundedField25p5.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
   Let feBW : Type := BoundedWord sz bitwidth bounds.
   Let eval : feBW -> Z :=
-    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
-  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+    fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
   Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
   Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
   Let phi : feBW -> F m :=
@@ -62,7 +64,7 @@ Section BoundedField25p5.
     eexists_sig_etransitivity.
     set (subZ := proj1_sig sub).
     context_to_dlet_in_rhs subZ; cbv [subZ].
-    cbv beta iota delta [sub sub' proj1_sig Saturated.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    cbv beta iota delta [sub sub' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
     reflexivity.
     sig_dlet_in_rhs_to_context.
     apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
diff --git a/src/Specific/NISTP256/AMD64/MontgomeryP256.v b/src/Specific/NISTP256/AMD64/MontgomeryP256.v
index ae5a3cb43..e709cc3ea 100644
--- a/src/Specific/NISTP256/AMD64/MontgomeryP256.v
+++ b/src/Specific/NISTP256/AMD64/MontgomeryP256.v
@@ -2,6 +2,8 @@ Require Import Coq.micromega.Lia.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Proofs.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
 Require Import Crypto.Util.Sigma.Lift.
 Require Import Coq.ZArith.BinInt.
 Require Import Coq.PArith.BinPos.
@@ -22,9 +24,9 @@ Definition r' := Eval vm_compute in Zpow_facts.Zpow_mod (Z.pos r) (Z.pos m - 2)
 Definition r'_correct := eq_refl : ((Z.pos r * r') mod (Z.pos m) = 1)%Z.
 Definition m' : Z := Eval vm_compute in Option.invert_Some (Z.modinv_fueled 10 (-Z.pos m) (Z.pos r)).
 Definition m'_correct := eq_refl : ((Z.pos m * m') mod (Z.pos r) = (-1) mod Z.pos r)%Z.
-Definition m_p256 := eq_refl (Z.pos m) <: Z.pos m = Saturated.eval (n:=sz) (Z.pos r) p256.
+Definition m_p256 := eq_refl (Z.pos m) <: Z.pos m = MontgomeryAPI.eval (n:=sz) (Z.pos r) p256.
 
-Lemma r'_pow_correct : ((r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz) mod Saturated.eval (n:=sz) (Z.pos r) p256 = 1)%Z.
+Lemma r'_pow_correct : ((r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 = 1)%Z.
 Proof. vm_compute; reflexivity. Qed.
 
 Definition mulmod_256' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
@@ -44,37 +46,37 @@ Proof.
        fst snd length List.seq List.hd List.app
        redc redc_cps redc_loop_cps redc_body_cps
        Positional.to_associational_cps
-       Saturated.divmod_cps
-       Saturated.scmul_cps
-       Saturated.uweight
-       Saturated.Columns.mul_cps
-       Saturated.Associational.mul_cps
+       MontgomeryAPI.divmod_cps
+       MontgomeryAPI.scmul_cps
+       uweight
+       MontgomeryAPI.Columns.mul_cps
+       MontgomeryAPI.Associational.mul_cps
        (*Z.of_nat Pos.of_succ_nat  Nat.pred
        Z.pow Z.pow_pos Z.mul Pos.iter Pos.mul Pos.succ*)
        Tuple.hd Tuple.append Tuple.tl Tuple.hd' Tuple.tl' CPSUtil.Tuple.left_tl_cps CPSUtil.Tuple.left_hd_cps CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps
-       Saturated.Columns.from_associational_cps
-       Saturated.Associational.multerm_cps
-       Saturated.Columns.compact_cps
-       Saturated.Columns.compact_step_cps
-       Saturated.Columns.compact_digit_cps
-       Saturated.drop_high_cps
-       Saturated.add_cps
-       Saturated.Columns.add_cps
-       Saturated.Columns.cons_to_nth_cps
+       MontgomeryAPI.Columns.from_associational_cps
+       MontgomeryAPI.Associational.multerm_cps
+       MontgomeryAPI.Columns.compact_cps
+       MontgomeryAPI.Columns.compact_step_cps
+       MontgomeryAPI.Columns.compact_digit_cps
+       MontgomeryAPI.drop_high_cps
+       MontgomeryAPI.add_cps
+       MontgomeryAPI.Columns.add_cps
+       MontgomeryAPI.Columns.cons_to_nth_cps
        Nat.pred
-       Saturated.join0
-       Saturated.join0_cps CPSUtil.Tuple.left_append_cps
+       MontgomeryAPI.join0
+       MontgomeryAPI.join0_cps CPSUtil.Tuple.left_append_cps
        CPSUtil.Tuple.mapi_with_cps
        id
-       Positional.zeros Saturated.zero Saturated.Columns.nils Tuple.repeat Tuple.append
+       Positional.zeros MontgomeryAPI.zero MontgomeryAPI.Columns.nils Tuple.repeat Tuple.append
        Positional.place_cps
        CPSUtil.Tuple.mapi_with'_cps Tuple.hd Tuple.hd' Tuple.tl Tuple.tl' CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps fst snd
        Z.of_nat fst snd Z.pow Z.pow_pos Pos.of_succ_nat Z.div Z.mul Pos.mul Z.modulo Z.div_eucl Z.pos_div_eucl Z.leb Z.compare Pos.compare_cont Pos.compare Z.pow_pos Pos.iter Z.mul Pos.succ Z.ltb Z.gtb Z.geb Z.div Z.sub Z.pos_sub Z.add Z.opp Z.double
        Decidable.dec Decidable.dec_eq_Z Z.eq_dec Z_rec Z_rec Z_rect
-       Positional.zeros Saturated.zero Saturated.Columns.nils Tuple.repeat Tuple.append
+       Positional.zeros MontgomeryAPI.zero MontgomeryAPI.Columns.nils Tuple.repeat Tuple.append
        (*
-       Saturated.Associational.multerm_cps
-       Saturated.Columns.from_associational_cps Positional.place_cps Saturated.Columns.cons_to_nth_cps Saturated.Columns.nils
+       MontgomeryAPI.Associational.multerm_cps
+       MontgomeryAPI.Columns.from_associational_cps Positional.place_cps MontgomeryAPI.Columns.cons_to_nth_cps MontgomeryAPI.Columns.nils
 Tuple.append
 Tuple.from_list Tuple.from_list'
 Tuple.from_list_default Tuple.from_list_default'
@@ -82,7 +84,7 @@ Tuple.hd
 Tuple.repeat
 Tuple.tl
 Tuple.tuple *)
-       (* Saturated.add_cps Saturated.divmod_cps Saturated.drop_high_cps Saturated.scmul_cps Saturated.zero Saturated.Columns.mul_cps Saturated.Columns.add_cps Saturated.uweight Saturated.T *)
+       (* MontgomeryAPI.add_cps MontgomeryAPI.divmod_cps MontgomeryAPI.drop_high_cps MontgomeryAPI.scmul_cps MontgomeryAPI.zero MontgomeryAPI.Columns.mul_cps MontgomeryAPI.Columns.add_cps uweight MontgomeryAPI.T *)
             (*
             CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps'
 Positional.zeros
@@ -106,9 +108,9 @@ Defined.
 
 Definition mulmod_256'' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
                         | forall (A B : Tuple.tuple Z sz),
-                            Saturated.small (Z.pos r) A -> Saturated.small (Z.pos r) B ->
-                            let eval := Saturated.eval (Z.pos r) in
-                            (Saturated.small (Z.pos r) (f A B)
+                            small (Z.pos r) A -> small (Z.pos r) B ->
+                            let eval := MontgomeryAPI.eval (Z.pos r) in
+                            (small (Z.pos r) (f A B)
                              /\ (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)
                              /\ (eval (f A B) mod Z.pos m
                                  = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z
@@ -123,10 +125,10 @@ Proof.
           | _ => assumption
           | [ |- _ = _ :> Z ] => vm_compute; reflexivity
           | _ => reflexivity
-          | [ |- Saturated.small (Z.pos r) p256 ]
+          | [ |- small (Z.pos r) p256 ]
             => hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or;
                subst; try lia
-          | [ |- Saturated.eval (Z.pos r) p256 <> 0%Z ]
+          | [ |- MontgomeryAPI.eval (Z.pos r) p256 <> 0%Z ]
             => vm_compute; lia
           end
     ).
@@ -179,10 +181,10 @@ Defined.
 Import ModularArithmetic.
 
 (*Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                        | forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                                 (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
-                            Saturated.small (Z.pos r) (f A B)
-                            /\ (let eval := Saturated.eval (Z.pos r) in
+                        | forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                                 (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+                            small (Z.pos r) (f A B)
+                            /\ (let eval := MontgomeryAPI.eval (Z.pos r) in
                                 0 <= eval (f A B) < Z.pos r^Z.of_nat sz
                                 /\ (eval (f A B) mod Z.pos m
                                     = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z
@@ -194,13 +196,13 @@ Definition montgomery_to_F (v : Z) : F m
   := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F.
 
 Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                        | let eval := Saturated.eval (Z.pos r) in
-                          (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                                  (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                        | let eval := MontgomeryAPI.eval (Z.pos r) in
+                          (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                               montgomery_to_F (eval (f A B))
                               = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F)
-                          /\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                                     (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                          /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                                     (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                                  (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }.
 Proof.
   exists (proj1_sig mulmod_256'').
@@ -224,25 +226,25 @@ Local Ltac t_fin :=
            | _ => assumption
            | [ |- _ = _ :> Z ] => vm_compute; reflexivity
            | _ => reflexivity
-           | [ |- Saturated.small (Z.pos r) p256 ]
+           | [ |- small (Z.pos r) p256 ]
              => hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or;
                 subst; try lia
-           | [ |- Saturated.eval (Z.pos r) p256 <> 0%Z ]
+           | [ |- MontgomeryAPI.eval (Z.pos r) p256 <> 0%Z ]
              => vm_compute; lia
            | [ |- and _ _ ] => split
-           | [ |- (0 <= Saturated.eval (Z.pos r) _)%Z ] => apply Saturated.eval_small
+           | [ |- (0 <= MontgomeryAPI.eval (Z.pos r) _)%Z ] => apply MontgomeryAPI.eval_small
            end.. ].
 
 Definition add : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := Saturated.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                 | let eval := MontgomeryAPI.eval (Z.pos r) in
+                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                         (eval A < eval p256
                          -> eval B < eval p256
                          -> montgomery_to_F (eval (f A B))
                             = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                               (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                            (eval A < eval p256
                             -> eval B < eval p256
                             -> 0 <= eval (f A B) < eval p256)))%Z }.
@@ -259,15 +261,15 @@ Proof.
 Defined.
 
 Definition sub : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := Saturated.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                 | let eval := MontgomeryAPI.eval (Z.pos r) in
+                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                         (eval A < eval p256
                          -> eval B < eval p256
                          -> montgomery_to_F (eval (f A B))
                             = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
                         (eval A < eval p256
                          -> eval B < eval p256
                          -> 0 <= eval (f A B) < eval p256)))%Z }.
@@ -284,12 +286,12 @@ Proof.
 Defined.
 
 Definition opp : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := Saturated.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A),
+                 | let eval := MontgomeryAPI.eval (Z.pos r) in
+                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
                         (eval A < eval p256
                          -> montgomery_to_F (eval (f A))
                             = (F.opp (montgomery_to_F (eval A)))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A),
+                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
                            (eval A < eval p256
                             -> 0 <= eval (f A) < eval p256)))%Z }.
 Proof.
@@ -305,8 +307,8 @@ Proof.
 Defined.
 
 Definition nonzero : { f:Tuple.tuple Z sz -> Z
-                     | let eval := Saturated.eval (Z.pos r) in
-                       forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A),
+                     | let eval := MontgomeryAPI.eval (Z.pos r) in
+                       forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
                          (eval A < eval p256
                           -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
 Proof.
@@ -314,14 +316,14 @@ Proof.
   abstract (
       intros eval A H **; rewrite (proj2_sig nonzero'), (@eval_nonzero r) by (eassumption || reflexivity);
       subst eval;
-      unfold montgomery_to_F, Saturated.uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul;
+      unfold montgomery_to_F, uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul;
       rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256;
       let H := fresh in
       split; intro H;
       [ rewrite H; autorewrite with zsimplify_const; reflexivity
-      | cut ((Saturated.eval (Z.pos r) A * (r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz)) mod Saturated.eval (n:=sz) (Z.pos r) p256 = 0)%Z;
+      | cut ((MontgomeryAPI.eval (Z.pos r) A * (r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz)) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 = 0)%Z;
         [ rewrite Z.mul_mod, r'_pow_correct; autorewrite with zsimplify_const; pull_Zmod; [ | vm_compute; congruence ];
-          rewrite Z.mod_small; [ trivial | split; try assumption; apply Saturated.eval_small; try assumption; lia ]
+          rewrite Z.mod_small; [ trivial | split; try assumption; apply MontgomeryAPI.eval_small; try assumption; lia ]
         | rewrite Z.mul_assoc, Z.mul_mod, H by (vm_compute; congruence); autorewrite with zsimplify_const; reflexivity ] ]
     ).
 Defined.