Support for 128-bit words

I haven't found a good way to genericize the proofs of relatedness
things, mostly because Modules and functors are annoying.

50 files changed, 569 insertions, 571 deletions

diff --git a/src/SpecificGen/GF2213_32Bounded.v b/src/SpecificGen/GF2213_32Bounded.v
index 7aeb5fd45..2947aacfc 100644
--- a/src/SpecificGen/GF2213_32Bounded.v
+++ b/src/SpecificGen/GF2213_32Bounded.v
@@ -78,7 +78,7 @@ Definition postfreezeW : fe2213_32W -> fe2213_32W :=
          (num_limbs := length_fe2213_32)
          modulusW
          ge_modulusW
-         (Interpretations.Word64.neg GF2213_32.int_width)
+         (Interpretations64.WordW.neg GF2213_32.int_width)
       ).
 
 Definition freezeW (f : fe2213_32W) : fe2213_32W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
@@ -117,7 +117,7 @@ Ltac lower_bound_minus_ge_modulus :=
   cbv [ge_modulus Let_In ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne ModularBaseSystemListZOperations.neg];
   repeat break_if; Z.ltb_to_lt; subst; try omega;
     rewrite ?Z.land_0_l; auto;
-    change Interpretations.Word64.word64ToZ with word64ToZ;
+    change Interpretations64.WordW.wordWToZ with word64ToZ;
     etransitivity; try apply Z.land_upper_bound_r; instantiate; try omega;
     apply Z.ones_nonneg; instantiate; vm_compute; discriminate.
 
@@ -136,8 +136,8 @@ Proof.
   destruct_head' and.
   Z.ltb_to_lt.
   cbv [postfreezeW].
-  cbv [conditional_subtract_modulusW Interpretations.Word64.neg].
-  change word64ToZ with Interpretations.Word64.word64ToZ in *.
+  cbv [conditional_subtract_modulusW Interpretations64.WordW.neg].
+  change word64ToZ with Interpretations64.WordW.wordWToZ in *.
   rewrite Hgm.
 
   cbv [modulusW Tuple.map].
@@ -148,12 +148,12 @@ Proof.
 
   split.
   { match goal with
-    |- (_,word64ToZ (_ ^- (Interpretations.Word64.ZToWord64 ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
+    |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  rewrite !Interpretations64.WordW.wordWToZ_sub;
+  rewrite !Interpretations64.WordW.wordWToZ_land;
+  rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
@@ -170,10 +170,10 @@ Proof.
 
 
   unfold_is_bounded.
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  rewrite !Interpretations64.WordW.wordWToZ_sub;
+  rewrite !Interpretations64.WordW.wordWToZ_land;
+  rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
diff --git a/src/SpecificGen/GF2213_32Reflective.v b/src/SpecificGen/GF2213_32Reflective.v
index 840cfe090..1fbf1a1c9 100644
--- a/src/SpecificGen/GF2213_32Reflective.v
+++ b/src/SpecificGen/GF2213_32Reflective.v
@@ -10,9 +10,9 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.MapInterp.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.SpecificGen.GF2213_32Reflective.Common.
@@ -50,10 +50,10 @@ Declare Reduction asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 Ltac asm_interp
   := cbv beta iota delta
@@ -61,10 +61,10 @@ Ltac asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 
 
diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v
index c01957df8..ff4999bcc 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common.v
@@ -4,9 +4,9 @@ Require Export Crypto.SpecificGen.GF2213_32.
 Require Export Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Export Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.InterpWfRel.
@@ -19,7 +19,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
 
-Notation Expr := (Expr base_type Word64.interp_base_type op).
+Notation Expr := (Expr base_type WordW.interp_base_type op).
 
 Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
@@ -45,9 +45,9 @@ Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
-  | (?x :: nil)%list => constr:(Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |})
+  | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
   | (?x :: ?xs)%list => let bs := bounds_from_list xs in
-                        constr:((Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |}, bs))
+                        constr:((Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs))
   end.
 
 Local Ltac make_bounds ls :=
@@ -66,17 +66,16 @@ Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZB
 Proof. make_bounds (Tuple.to_list _ bounds). Defined.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
-  := fun e => curry_binop_fe2213_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_binop_fe2213_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
-  := fun e => curry_unop_fe2213_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe2213_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.word64
-  := fun e => curry_unop_fe2213_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe2213_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.wire_digitsW
-  := fun e => curry_unop_fe2213_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe2213_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> SpecificGen.GF2213_32BoundedCommon.wire_digitsW -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
-  := fun e => curry_unop_wire_digitsW (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_wire_digitsW (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -117,13 +116,13 @@ Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
       let ropZ_sig := ropZ_sigv in
       let ropW := MapInterp (fun _ x => x) ropW' in
-      let ropZ := MapInterp Word64.to_Z ropW' in
-      let ropBounds := MapInterp ZBounds.of_word64 ropW' in
-      let ropBoundedWord64 := MapInterp BoundedWord64.of_word64 ropW' in
+      let ropZ := MapInterp WordW.to_Z ropW' in
+      let ropBounds := MapInterp ZBounds.of_wordW ropW' in
+      let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in
       ropZ = proj1_sig ropZ_sig
-      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Z.interp_op) ropZ)
-      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@ZBounds.interp_op) ropBounds)
-      /\ interp_type_rel_pointwise2 Relations.related_word64 (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Word64.interp_op) ropW))
+      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ)
+      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds)
+      /\ interp_type_rel_pointwise2 Relations.related_wordW (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@WordW.interp_op) ropW))
        (only parsing).
 
 Ltac app_tuples x y :=
@@ -138,7 +137,7 @@ Local Arguments Tuple.map2 : simpl never.
 Local Arguments Tuple.map : simpl never.
 
 Fixpoint args_to_bounded_helperT {n}
-         (v : Tuple.tuple' Word64.word64 n)
+         (v : Tuple.tuple' WordW.wordW n)
          (bounds : Tuple.tuple' (Z * Z) n)
          (pf : List.fold_right
                  andb true
@@ -149,7 +148,7 @@ Fixpoint args_to_bounded_helperT {n}
                        (fun bounds v =>
                           let '(lower, upper) := bounds in ((lower <=? v)%Z && (v <=? upper)%Z)%bool)
                        bounds
-                       (Tuple.map (n:=S n) Word64.word64ToZ v))) = true)
+                       (Tuple.map (n:=S n) WordW.wordWToZ v))) = true)
          (res : Type)
          {struct n}
   : Type.
@@ -161,9 +160,9 @@ Proof.
                                       (Tuple.map2 (n:=S n) _ bounds (Tuple.map (n:=S n) _ v))) = true
                              -> Type)
           with
-          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat Word64.bit_width)%Z, res
+          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat WordW.bit_width)%Z, res
           | S n' => fun v' bounds' pf0 => let t := _ in
-                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
+                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat WordW.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
           end v bounds pf).
   { clear -pf0.
     abstract (
@@ -178,15 +177,15 @@ Defined.
 
 Fixpoint args_to_bounded_helper {n} res
          {struct n}
-  : forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
+  : forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
 Proof.
-  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
-         | 0 => fun v bounds pf f pf' => f {| BoundedWord64.lower := fst bounds ; BoundedWord64.value := v ; BoundedWord64.upper := snd bounds |}
+  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
+         | 0 => fun v bounds pf f pf' => f {| BoundedWord.lower := fst bounds ; BoundedWord.value := v ; BoundedWord.upper := snd bounds |}
          | S n'
            => fun v bounds pf f pf'
               => @args_to_bounded_helper
                    n' res (fst v) (fst bounds) _
-                   (fun ts => f (ts, {| BoundedWord64.lower := fst (snd bounds) ; BoundedWord64.value := snd v ; BoundedWord64.upper := snd (snd bounds) |}))
+                   (fun ts => f (ts, {| BoundedWord.lower := fst (snd bounds) ; BoundedWord.value := snd v ; BoundedWord.upper := snd (snd bounds) |}))
          end.
   { clear -pf pf'.
     unfold Tuple.map2, Tuple.map in pf; simpl in *.
@@ -242,16 +241,16 @@ Local Ltac args_to_bounded x H :=
       ).
 
 Definition unop_args_to_bounded (x : fe2213_32W) (H : is_bounded (fe2213_32WToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpT).
 Proof. args_to_bounded x H. Defined.
 
 Definition unopWireToFE_args_to_bounded (x : wire_digitsW) (H : wire_digits_is_bounded (wire_digitsWToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpWireToFET).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpWireToFET).
 Proof. args_to_bounded x H. Defined.
 Definition binop_args_to_bounded (x : fe2213_32W * fe2213_32W)
            (H : is_bounded (fe2213_32WToZ (fst x)) = true)
            (H' : is_bounded (fe2213_32WToZ (snd x)) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprBinOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprBinOpT).
 Proof.
   let v := app_tuples (unop_args_to_bounded (fst x) H) (unop_args_to_bounded (snd x) H') in
   exact v.
@@ -328,13 +327,13 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   change interp_base_type with (@Z.interp_base_type) in *;
   rewrite <- Heq; clear Heq;
   destruct Hbounds as [ Hbounds0 [Hbounds1 Hbounds2] ];
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 Word64.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_word64_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 WordW.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_wordW_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
   specialize_by repeat first [ progress intros
                              | reflexivity
                              | assumption
                              | progress destruct_head' base_type
-                             | progress destruct_head' BoundedWord64.BoundedWord
+                             | progress destruct_head' BoundedWordW.BoundedWord
                              | progress destruct_head' and
                              | progress repeat apply conj ];
   specialize (Hbounds_left args H0);
@@ -350,7 +349,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWord64.to_word64' BoundedWord64.boundedWordToWord64 BoundedWord64.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_word64_boundsi' Relations.related'_word64_bounds ZBounds.upper ZBounds.lower Application.remove_all_binders Word64.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe2213_32WToZ ?x = _ /\ _ ]
     => destruct x; destruct_head_hnf' prod
@@ -359,7 +358,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
-  change word64ToZ with Word64.word64ToZ in *;
+  change word64ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
@@ -371,7 +370,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
-  change Word64.word64ToZ with word64ToZ in *;
+  change WordW.wordWToZ with word64ToZ in *;
   repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
 
 
@@ -387,10 +386,10 @@ Ltac rexpr_correct :=
     [ | apply @RelWfMapInterp, wf_ropW ].. ];
   auto with interp_related.
 
-Notation rword_of_Z rexprZ_sig := (MapInterp Word64.of_Z (proj1_sig rexprZ_sig)) (only parsing).
+Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing).
 
 Notation compute_bounds opW bounds
-  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_word64) opW)) bounds)
+  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds)
        (only parsing).
 
 
@@ -407,7 +406,7 @@ Module Export PrettyPrinting.
     := fun t : base_type
        => match t return ZBounds.interp_base_type t -> match t with TZ => bounds_on end with
           | TZ => fun x => match x with
-                           | Some {| ZBounds.lower := l ; ZBounds.upper := u |}
+                           | Some {| Bounds.lower := l ; Bounds.upper := u |}
                              => in_range l u
                            | None
                              => overflow
diff --git a/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v b/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v
index be248d708..23becba34 100644
--- a/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -18,7 +18,7 @@ Lemma ExprBinOp_correct_and_bounded
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded xy Hx Hy in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -31,9 +31,9 @@ Lemma ExprBinOp_correct_and_bounded
           let Hx := let (Hx, Hy) := Hxy in Hx in
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => binop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v
index 3d52bcf78..250a64400 100644
--- a/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOp_correct_and_bounded
                    (Hx : is_bounded (fe2213_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOp_correct_and_bounded
                    (x := eta_fe2213_32W x)
                    (Hx : is_bounded (fe2213_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v
index a08efcfd8..2dcae7edd 100644
--- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (Hx : is_bounded (fe2213_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (x := eta_fe2213_32W x)
                    (Hx : is_bounded (fe2213_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToWire_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v
index 1f3a5f8a0..ef997e3f9 100644
--- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (Hx : is_bounded (fe2213_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (x := eta_fe2213_32W x)
                    (Hx : is_bounded (fe2213_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToZ_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v
index 727936a13..4342ef865 100644
--- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (x := eta_wire_digitsW x)
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopWireToFE_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF2519_32Bounded.v b/src/SpecificGen/GF2519_32Bounded.v
index b49228967..ca448e458 100644
--- a/src/SpecificGen/GF2519_32Bounded.v
+++ b/src/SpecificGen/GF2519_32Bounded.v
@@ -78,7 +78,7 @@ Definition postfreezeW : fe2519_32W -> fe2519_32W :=
          (num_limbs := length_fe2519_32)
          modulusW
          ge_modulusW
-         (Interpretations.Word64.neg GF2519_32.int_width)
+         (Interpretations64.WordW.neg GF2519_32.int_width)
       ).
 
 Definition freezeW (f : fe2519_32W) : fe2519_32W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
@@ -117,7 +117,7 @@ Ltac lower_bound_minus_ge_modulus :=
   cbv [ge_modulus Let_In ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne ModularBaseSystemListZOperations.neg];
   repeat break_if; Z.ltb_to_lt; subst; try omega;
     rewrite ?Z.land_0_l; auto;
-    change Interpretations.Word64.word64ToZ with word64ToZ;
+    change Interpretations64.WordW.wordWToZ with word64ToZ;
     etransitivity; try apply Z.land_upper_bound_r; instantiate; try omega;
     apply Z.ones_nonneg; instantiate; vm_compute; discriminate.
 
@@ -136,8 +136,8 @@ Proof.
   destruct_head' and.
   Z.ltb_to_lt.
   cbv [postfreezeW].
-  cbv [conditional_subtract_modulusW Interpretations.Word64.neg].
-  change word64ToZ with Interpretations.Word64.word64ToZ in *.
+  cbv [conditional_subtract_modulusW Interpretations64.WordW.neg].
+  change word64ToZ with Interpretations64.WordW.wordWToZ in *.
   rewrite Hgm.
 
   cbv [modulusW Tuple.map].
@@ -148,12 +148,12 @@ Proof.
 
   split.
   { match goal with
-    |- (_,word64ToZ (_ ^- (Interpretations.Word64.ZToWord64 ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
+    |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  rewrite !Interpretations64.WordW.wordWToZ_sub;
+  rewrite !Interpretations64.WordW.wordWToZ_land;
+  rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
@@ -170,10 +170,10 @@ Proof.
 
 
   unfold_is_bounded.
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  rewrite !Interpretations64.WordW.wordWToZ_sub;
+  rewrite !Interpretations64.WordW.wordWToZ_land;
+  rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
diff --git a/src/SpecificGen/GF2519_32Reflective.v b/src/SpecificGen/GF2519_32Reflective.v
index 964d0f608..ca7b86e5f 100644
--- a/src/SpecificGen/GF2519_32Reflective.v
+++ b/src/SpecificGen/GF2519_32Reflective.v
@@ -10,9 +10,9 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.MapInterp.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.SpecificGen.GF2519_32Reflective.Common.
@@ -50,10 +50,10 @@ Declare Reduction asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe2519_32W curry_unop_fe2519_32W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 Ltac asm_interp
   := cbv beta iota delta
@@ -61,10 +61,10 @@ Ltac asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe2519_32W curry_unop_fe2519_32W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 
 
diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v
index 16a7dd72c..aac5d8fb9 100644
--- a/src/SpecificGen/GF2519_32Reflective/Common.v
+++ b/src/SpecificGen/GF2519_32Reflective/Common.v
@@ -4,9 +4,9 @@ Require Export Crypto.SpecificGen.GF2519_32.
 Require Export Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Export Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.InterpWfRel.
@@ -19,7 +19,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
 
-Notation Expr := (Expr base_type Word64.interp_base_type op).
+Notation Expr := (Expr base_type WordW.interp_base_type op).
 
 Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
@@ -45,9 +45,9 @@ Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
-  | (?x :: nil)%list => constr:(Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |})
+  | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
   | (?x :: ?xs)%list => let bs := bounds_from_list xs in
-                        constr:((Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |}, bs))
+                        constr:((Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs))
   end.
 
 Local Ltac make_bounds ls :=
@@ -66,17 +66,16 @@ Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZB
 Proof. make_bounds (Tuple.to_list _ bounds). Defined.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
-  := fun e => curry_binop_fe2519_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_binop_fe2519_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
-  := fun e => curry_unop_fe2519_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe2519_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.word64
-  := fun e => curry_unop_fe2519_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe2519_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.wire_digitsW
-  := fun e => curry_unop_fe2519_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe2519_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> SpecificGen.GF2519_32BoundedCommon.wire_digitsW -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
-  := fun e => curry_unop_wire_digitsW (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_wire_digitsW (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -117,13 +116,13 @@ Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
       let ropZ_sig := ropZ_sigv in
       let ropW := MapInterp (fun _ x => x) ropW' in
-      let ropZ := MapInterp Word64.to_Z ropW' in
-      let ropBounds := MapInterp ZBounds.of_word64 ropW' in
-      let ropBoundedWord64 := MapInterp BoundedWord64.of_word64 ropW' in
+      let ropZ := MapInterp WordW.to_Z ropW' in
+      let ropBounds := MapInterp ZBounds.of_wordW ropW' in
+      let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in
       ropZ = proj1_sig ropZ_sig
-      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Z.interp_op) ropZ)
-      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@ZBounds.interp_op) ropBounds)
-      /\ interp_type_rel_pointwise2 Relations.related_word64 (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Word64.interp_op) ropW))
+      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ)
+      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds)
+      /\ interp_type_rel_pointwise2 Relations.related_wordW (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@WordW.interp_op) ropW))
        (only parsing).
 
 Ltac app_tuples x y :=
@@ -138,7 +137,7 @@ Local Arguments Tuple.map2 : simpl never.
 Local Arguments Tuple.map : simpl never.
 
 Fixpoint args_to_bounded_helperT {n}
-         (v : Tuple.tuple' Word64.word64 n)
+         (v : Tuple.tuple' WordW.wordW n)
          (bounds : Tuple.tuple' (Z * Z) n)
          (pf : List.fold_right
                  andb true
@@ -149,7 +148,7 @@ Fixpoint args_to_bounded_helperT {n}
                        (fun bounds v =>
                           let '(lower, upper) := bounds in ((lower <=? v)%Z && (v <=? upper)%Z)%bool)
                        bounds
-                       (Tuple.map (n:=S n) Word64.word64ToZ v))) = true)
+                       (Tuple.map (n:=S n) WordW.wordWToZ v))) = true)
          (res : Type)
          {struct n}
   : Type.
@@ -161,9 +160,9 @@ Proof.
                                       (Tuple.map2 (n:=S n) _ bounds (Tuple.map (n:=S n) _ v))) = true
                              -> Type)
           with
-          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat Word64.bit_width)%Z, res
+          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat WordW.bit_width)%Z, res
           | S n' => fun v' bounds' pf0 => let t := _ in
-                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
+                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat WordW.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
           end v bounds pf).
   { clear -pf0.
     abstract (
@@ -178,15 +177,15 @@ Defined.
 
 Fixpoint args_to_bounded_helper {n} res
          {struct n}
-  : forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
+  : forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
 Proof.
-  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
-         | 0 => fun v bounds pf f pf' => f {| BoundedWord64.lower := fst bounds ; BoundedWord64.value := v ; BoundedWord64.upper := snd bounds |}
+  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
+         | 0 => fun v bounds pf f pf' => f {| BoundedWord.lower := fst bounds ; BoundedWord.value := v ; BoundedWord.upper := snd bounds |}
          | S n'
            => fun v bounds pf f pf'
               => @args_to_bounded_helper
                    n' res (fst v) (fst bounds) _
-                   (fun ts => f (ts, {| BoundedWord64.lower := fst (snd bounds) ; BoundedWord64.value := snd v ; BoundedWord64.upper := snd (snd bounds) |}))
+                   (fun ts => f (ts, {| BoundedWord.lower := fst (snd bounds) ; BoundedWord.value := snd v ; BoundedWord.upper := snd (snd bounds) |}))
          end.
   { clear -pf pf'.
     unfold Tuple.map2, Tuple.map in pf; simpl in *.
@@ -242,16 +241,16 @@ Local Ltac args_to_bounded x H :=
       ).
 
 Definition unop_args_to_bounded (x : fe2519_32W) (H : is_bounded (fe2519_32WToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpT).
 Proof. args_to_bounded x H. Defined.
 
 Definition unopWireToFE_args_to_bounded (x : wire_digitsW) (H : wire_digits_is_bounded (wire_digitsWToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpWireToFET).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpWireToFET).
 Proof. args_to_bounded x H. Defined.
 Definition binop_args_to_bounded (x : fe2519_32W * fe2519_32W)
            (H : is_bounded (fe2519_32WToZ (fst x)) = true)
            (H' : is_bounded (fe2519_32WToZ (snd x)) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprBinOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprBinOpT).
 Proof.
   let v := app_tuples (unop_args_to_bounded (fst x) H) (unop_args_to_bounded (snd x) H') in
   exact v.
@@ -328,13 +327,13 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   change interp_base_type with (@Z.interp_base_type) in *;
   rewrite <- Heq; clear Heq;
   destruct Hbounds as [ Hbounds0 [Hbounds1 Hbounds2] ];
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 Word64.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_word64_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 WordW.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_wordW_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
   specialize_by repeat first [ progress intros
                              | reflexivity
                              | assumption
                              | progress destruct_head' base_type
-                             | progress destruct_head' BoundedWord64.BoundedWord
+                             | progress destruct_head' BoundedWordW.BoundedWord
                              | progress destruct_head' and
                              | progress repeat apply conj ];
   specialize (Hbounds_left args H0);
@@ -350,7 +349,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWord64.to_word64' BoundedWord64.boundedWordToWord64 BoundedWord64.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_word64_boundsi' Relations.related'_word64_bounds ZBounds.upper ZBounds.lower Application.remove_all_binders Word64.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe2519_32WToZ ?x = _ /\ _ ]
     => destruct x; destruct_head_hnf' prod
@@ -359,7 +358,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
-  change word64ToZ with Word64.word64ToZ in *;
+  change word64ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
@@ -371,7 +370,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
-  change Word64.word64ToZ with word64ToZ in *;
+  change WordW.wordWToZ with word64ToZ in *;
   repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
 
 
@@ -387,10 +386,10 @@ Ltac rexpr_correct :=
     [ | apply @RelWfMapInterp, wf_ropW ].. ];
   auto with interp_related.
 
-Notation rword_of_Z rexprZ_sig := (MapInterp Word64.of_Z (proj1_sig rexprZ_sig)) (only parsing).
+Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing).
 
 Notation compute_bounds opW bounds
-  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_word64) opW)) bounds)
+  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds)
        (only parsing).
 
 
@@ -407,7 +406,7 @@ Module Export PrettyPrinting.
     := fun t : base_type
        => match t return ZBounds.interp_base_type t -> match t with TZ => bounds_on end with
           | TZ => fun x => match x with
-                           | Some {| ZBounds.lower := l ; ZBounds.upper := u |}
+                           | Some {| Bounds.lower := l ; Bounds.upper := u |}
                              => in_range l u
                            | None
                              => overflow
diff --git a/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v b/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v
index d2bce7c3f..095c7a8c6 100644
--- a/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -18,7 +18,7 @@ Lemma ExprBinOp_correct_and_bounded
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded xy Hx Hy in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -31,9 +31,9 @@ Lemma ExprBinOp_correct_and_bounded
           let Hx := let (Hx, Hy) := Hxy in Hx in
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => binop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v
index d651e6118..f2e091570 100644
--- a/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOp_correct_and_bounded
                    (Hx : is_bounded (fe2519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOp_correct_and_bounded
                    (x := eta_fe2519_32W x)
                    (Hx : is_bounded (fe2519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v
index 10dc0866e..cf8a85d6f 100644
--- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (Hx : is_bounded (fe2519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (x := eta_fe2519_32W x)
                    (Hx : is_bounded (fe2519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToWire_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v
index ec00c6233..7d70c1234 100644
--- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (Hx : is_bounded (fe2519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (x := eta_fe2519_32W x)
                    (Hx : is_bounded (fe2519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToZ_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v
index 6ca61afe9..22e68fcf5 100644
--- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (x := eta_wire_digitsW x)
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopWireToFE_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF25519_32Bounded.v b/src/SpecificGen/GF25519_32Bounded.v
index 264d7c3d3..7dddfe2c5 100644
--- a/src/SpecificGen/GF25519_32Bounded.v
+++ b/src/SpecificGen/GF25519_32Bounded.v
@@ -78,7 +78,7 @@ Definition postfreezeW : fe25519_32W -> fe25519_32W :=
          (num_limbs := length_fe25519_32)
          modulusW
          ge_modulusW
-         (Interpretations.Word64.neg GF25519_32.int_width)
+         (Interpretations64.WordW.neg GF25519_32.int_width)
       ).
 
 Definition freezeW (f : fe25519_32W) : fe25519_32W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
@@ -117,7 +117,7 @@ Ltac lower_bound_minus_ge_modulus :=
   cbv [ge_modulus Let_In ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne ModularBaseSystemListZOperations.neg];
   repeat break_if; Z.ltb_to_lt; subst; try omega;
     rewrite ?Z.land_0_l; auto;
-    change Interpretations.Word64.word64ToZ with word64ToZ;
+    change Interpretations64.WordW.wordWToZ with word64ToZ;
     etransitivity; try apply Z.land_upper_bound_r; instantiate; try omega;
     apply Z.ones_nonneg; instantiate; vm_compute; discriminate.
 
@@ -136,8 +136,8 @@ Proof.
   destruct_head' and.
   Z.ltb_to_lt.
   cbv [postfreezeW].
-  cbv [conditional_subtract_modulusW Interpretations.Word64.neg].
-  change word64ToZ with Interpretations.Word64.word64ToZ in *.
+  cbv [conditional_subtract_modulusW Interpretations64.WordW.neg].
+  change word64ToZ with Interpretations64.WordW.wordWToZ in *.
   rewrite Hgm.
 
   cbv [modulusW Tuple.map].
@@ -148,12 +148,12 @@ Proof.
 
   split.
   { match goal with
-    |- (_,word64ToZ (_ ^- (Interpretations.Word64.ZToWord64 ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
+    |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  rewrite !Interpretations64.WordW.wordWToZ_sub;
+  rewrite !Interpretations64.WordW.wordWToZ_land;
+  rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
@@ -170,10 +170,10 @@ Proof.
 
 
   unfold_is_bounded.
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  rewrite !Interpretations64.WordW.wordWToZ_sub;
+  rewrite !Interpretations64.WordW.wordWToZ_land;
+  rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
diff --git a/src/SpecificGen/GF25519_32Reflective.v b/src/SpecificGen/GF25519_32Reflective.v
index 0459f10ab..e4e17b47f 100644
--- a/src/SpecificGen/GF25519_32Reflective.v
+++ b/src/SpecificGen/GF25519_32Reflective.v
@@ -10,9 +10,9 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.MapInterp.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.SpecificGen.GF25519_32Reflective.Common.
@@ -50,10 +50,10 @@ Declare Reduction asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe25519_32W curry_unop_fe25519_32W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 Ltac asm_interp
   := cbv beta iota delta
@@ -61,10 +61,10 @@ Ltac asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe25519_32W curry_unop_fe25519_32W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 
 
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v
index 4105b4173..96958f330 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common.v
@@ -4,9 +4,9 @@ Require Export Crypto.SpecificGen.GF25519_32.
 Require Export Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Export Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.InterpWfRel.
@@ -19,7 +19,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
 
-Notation Expr := (Expr base_type Word64.interp_base_type op).
+Notation Expr := (Expr base_type WordW.interp_base_type op).
 
 Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
@@ -45,9 +45,9 @@ Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
-  | (?x :: nil)%list => constr:(Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |})
+  | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
   | (?x :: ?xs)%list => let bs := bounds_from_list xs in
-                        constr:((Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |}, bs))
+                        constr:((Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs))
   end.
 
 Local Ltac make_bounds ls :=
@@ -66,17 +66,16 @@ Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZB
 Proof. make_bounds (Tuple.to_list _ bounds). Defined.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
-  := fun e => curry_binop_fe25519_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_binop_fe25519_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
-  := fun e => curry_unop_fe25519_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe25519_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.word64
-  := fun e => curry_unop_fe25519_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe25519_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.wire_digitsW
-  := fun e => curry_unop_fe25519_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe25519_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> SpecificGen.GF25519_32BoundedCommon.wire_digitsW -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
-  := fun e => curry_unop_wire_digitsW (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_wire_digitsW (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -117,13 +116,13 @@ Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
       let ropZ_sig := ropZ_sigv in
       let ropW := MapInterp (fun _ x => x) ropW' in
-      let ropZ := MapInterp Word64.to_Z ropW' in
-      let ropBounds := MapInterp ZBounds.of_word64 ropW' in
-      let ropBoundedWord64 := MapInterp BoundedWord64.of_word64 ropW' in
+      let ropZ := MapInterp WordW.to_Z ropW' in
+      let ropBounds := MapInterp ZBounds.of_wordW ropW' in
+      let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in
       ropZ = proj1_sig ropZ_sig
-      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Z.interp_op) ropZ)
-      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@ZBounds.interp_op) ropBounds)
-      /\ interp_type_rel_pointwise2 Relations.related_word64 (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Word64.interp_op) ropW))
+      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ)
+      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds)
+      /\ interp_type_rel_pointwise2 Relations.related_wordW (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@WordW.interp_op) ropW))
        (only parsing).
 
 Ltac app_tuples x y :=
@@ -138,7 +137,7 @@ Local Arguments Tuple.map2 : simpl never.
 Local Arguments Tuple.map : simpl never.
 
 Fixpoint args_to_bounded_helperT {n}
-         (v : Tuple.tuple' Word64.word64 n)
+         (v : Tuple.tuple' WordW.wordW n)
          (bounds : Tuple.tuple' (Z * Z) n)
          (pf : List.fold_right
                  andb true
@@ -149,7 +148,7 @@ Fixpoint args_to_bounded_helperT {n}
                        (fun bounds v =>
                           let '(lower, upper) := bounds in ((lower <=? v)%Z && (v <=? upper)%Z)%bool)
                        bounds
-                       (Tuple.map (n:=S n) Word64.word64ToZ v))) = true)
+                       (Tuple.map (n:=S n) WordW.wordWToZ v))) = true)
          (res : Type)
          {struct n}
   : Type.
@@ -161,9 +160,9 @@ Proof.
                                       (Tuple.map2 (n:=S n) _ bounds (Tuple.map (n:=S n) _ v))) = true
                              -> Type)
           with
-          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat Word64.bit_width)%Z, res
+          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat WordW.bit_width)%Z, res
           | S n' => fun v' bounds' pf0 => let t := _ in
-                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
+                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat WordW.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
           end v bounds pf).
   { clear -pf0.
     abstract (
@@ -178,15 +177,15 @@ Defined.
 
 Fixpoint args_to_bounded_helper {n} res
          {struct n}
-  : forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
+  : forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
 Proof.
-  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
-         | 0 => fun v bounds pf f pf' => f {| BoundedWord64.lower := fst bounds ; BoundedWord64.value := v ; BoundedWord64.upper := snd bounds |}
+  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
+         | 0 => fun v bounds pf f pf' => f {| BoundedWord.lower := fst bounds ; BoundedWord.value := v ; BoundedWord.upper := snd bounds |}
          | S n'
            => fun v bounds pf f pf'
               => @args_to_bounded_helper
                    n' res (fst v) (fst bounds) _
-                   (fun ts => f (ts, {| BoundedWord64.lower := fst (snd bounds) ; BoundedWord64.value := snd v ; BoundedWord64.upper := snd (snd bounds) |}))
+                   (fun ts => f (ts, {| BoundedWord.lower := fst (snd bounds) ; BoundedWord.value := snd v ; BoundedWord.upper := snd (snd bounds) |}))
          end.
   { clear -pf pf'.
     unfold Tuple.map2, Tuple.map in pf; simpl in *.
@@ -242,16 +241,16 @@ Local Ltac args_to_bounded x H :=
       ).
 
 Definition unop_args_to_bounded (x : fe25519_32W) (H : is_bounded (fe25519_32WToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpT).
 Proof. args_to_bounded x H. Defined.
 
 Definition unopWireToFE_args_to_bounded (x : wire_digitsW) (H : wire_digits_is_bounded (wire_digitsWToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpWireToFET).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpWireToFET).
 Proof. args_to_bounded x H. Defined.
 Definition binop_args_to_bounded (x : fe25519_32W * fe25519_32W)
            (H : is_bounded (fe25519_32WToZ (fst x)) = true)
            (H' : is_bounded (fe25519_32WToZ (snd x)) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprBinOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprBinOpT).
 Proof.
   let v := app_tuples (unop_args_to_bounded (fst x) H) (unop_args_to_bounded (snd x) H') in
   exact v.
@@ -328,13 +327,13 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   change interp_base_type with (@Z.interp_base_type) in *;
   rewrite <- Heq; clear Heq;
   destruct Hbounds as [ Hbounds0 [Hbounds1 Hbounds2] ];
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 Word64.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_word64_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 WordW.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_wordW_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
   specialize_by repeat first [ progress intros
                              | reflexivity
                              | assumption
                              | progress destruct_head' base_type
-                             | progress destruct_head' BoundedWord64.BoundedWord
+                             | progress destruct_head' BoundedWordW.BoundedWord
                              | progress destruct_head' and
                              | progress repeat apply conj ];
   specialize (Hbounds_left args H0);
@@ -350,7 +349,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWord64.to_word64' BoundedWord64.boundedWordToWord64 BoundedWord64.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_word64_boundsi' Relations.related'_word64_bounds ZBounds.upper ZBounds.lower Application.remove_all_binders Word64.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe25519_32WToZ ?x = _ /\ _ ]
     => destruct x; destruct_head_hnf' prod
@@ -359,7 +358,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
-  change word64ToZ with Word64.word64ToZ in *;
+  change word64ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
@@ -371,7 +370,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
-  change Word64.word64ToZ with word64ToZ in *;
+  change WordW.wordWToZ with word64ToZ in *;
   repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
 
 
@@ -387,10 +386,10 @@ Ltac rexpr_correct :=
     [ | apply @RelWfMapInterp, wf_ropW ].. ];
   auto with interp_related.
 
-Notation rword_of_Z rexprZ_sig := (MapInterp Word64.of_Z (proj1_sig rexprZ_sig)) (only parsing).
+Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing).
 
 Notation compute_bounds opW bounds
-  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_word64) opW)) bounds)
+  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds)
        (only parsing).
 
 
@@ -407,7 +406,7 @@ Module Export PrettyPrinting.
     := fun t : base_type
        => match t return ZBounds.interp_base_type t -> match t with TZ => bounds_on end with
           | TZ => fun x => match x with
-                           | Some {| ZBounds.lower := l ; ZBounds.upper := u |}
+                           | Some {| Bounds.lower := l ; Bounds.upper := u |}
                              => in_range l u
                            | None
                              => overflow
diff --git a/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v b/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v
index 837229900..f254a2d3a 100644
--- a/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -18,7 +18,7 @@ Lemma ExprBinOp_correct_and_bounded
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded xy Hx Hy in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -31,9 +31,9 @@ Lemma ExprBinOp_correct_and_bounded
           let Hx := let (Hx, Hy) := Hxy in Hx in
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => binop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v
index 864efb92b..246dcbf70 100644
--- a/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOp_correct_and_bounded
                    (Hx : is_bounded (fe25519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOp_correct_and_bounded
                    (x := eta_fe25519_32W x)
                    (Hx : is_bounded (fe25519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v
index 68efe5b86..a940a0c8b 100644
--- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (Hx : is_bounded (fe25519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (x := eta_fe25519_32W x)
                    (Hx : is_bounded (fe25519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToWire_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v
index 6b9864d6f..b7ec2c6a5 100644
--- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (Hx : is_bounded (fe25519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (x := eta_fe25519_32W x)
                    (Hx : is_bounded (fe25519_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToZ_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v
index 09ac72cdc..34e0896f1 100644
--- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (x := eta_wire_digitsW x)
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopWireToFE_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF25519_64Bounded.v b/src/SpecificGen/GF25519_64Bounded.v
index 35ad2ee01..71b859d32 100644
--- a/src/SpecificGen/GF25519_64Bounded.v
+++ b/src/SpecificGen/GF25519_64Bounded.v
@@ -46,7 +46,7 @@ Local Ltac define_unop_WireToFE f opW blem :=
   abstract bounded_wire_digits_t opW blem.
 
 Local Opaque Let_In.
-Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64.
+Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord128.
 Local Arguments interp_radd / _ _.
 Local Arguments interp_rsub / _ _.
 Local Arguments interp_rmul / _ _.
@@ -60,12 +60,12 @@ Definition subW (f g : fe25519_64W) : fe25519_64W := Eval simpl in interp_rsub f
 Definition mulW (f g : fe25519_64W) : fe25519_64W := Eval simpl in interp_rmul f g.
 Definition oppW (f : fe25519_64W) : fe25519_64W := Eval simpl in interp_ropp f.
 Definition prefreezeW (f : fe25519_64W) : fe25519_64W := Eval simpl in interp_rprefreeze f.
-Definition ge_modulusW (f : fe25519_64W) : word64 := Eval simpl in interp_rge_modulus f.
+Definition ge_modulusW (f : fe25519_64W) : word128 := Eval simpl in interp_rge_modulus f.
 Definition packW (f : fe25519_64W) : wire_digitsW := Eval simpl in interp_rpack f.
 Definition unpackW (f : wire_digitsW) : fe25519_64W := Eval simpl in interp_runpack f.
 
 Definition modulusW :=
-  Eval cbv - [ZToWord64] in (Tuple.map ZToWord64 (Tuple.from_list_default 0%Z length_fe25519_64 GF25519_64.modulus_digits_)).
+  Eval cbv - [ZToWord128] in (Tuple.map ZToWord128 (Tuple.from_list_default 0%Z length_fe25519_64 GF25519_64.modulus_digits_)).
 
 Definition postfreeze : GF25519_64.fe25519_64 -> GF25519_64.fe25519_64 :=
   GF25519_64.postfreeze.
@@ -78,7 +78,7 @@ Definition postfreezeW : fe25519_64W -> fe25519_64W :=
          (num_limbs := length_fe25519_64)
          modulusW
          ge_modulusW
-         (Interpretations.Word64.neg GF25519_64.int_width)
+         (Interpretations128.WordW.neg GF25519_64.int_width)
       ).
 
 Definition freezeW (f : fe25519_64W) : fe25519_64W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
@@ -117,7 +117,7 @@ Ltac lower_bound_minus_ge_modulus :=
   cbv [ge_modulus Let_In ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne ModularBaseSystemListZOperations.neg];
   repeat break_if; Z.ltb_to_lt; subst; try omega;
     rewrite ?Z.land_0_l; auto;
-    change Interpretations.Word64.word64ToZ with word64ToZ;
+    change Interpretations128.WordW.wordWToZ with word128ToZ;
     etransitivity; try apply Z.land_upper_bound_r; instantiate; try omega;
     apply Z.ones_nonneg; instantiate; vm_compute; discriminate.
 
@@ -136,8 +136,8 @@ Proof.
   destruct_head' and.
   Z.ltb_to_lt.
   cbv [postfreezeW].
-  cbv [conditional_subtract_modulusW Interpretations.Word64.neg].
-  change word64ToZ with Interpretations.Word64.word64ToZ in *.
+  cbv [conditional_subtract_modulusW Interpretations128.WordW.neg].
+  change word128ToZ with Interpretations128.WordW.wordWToZ in *.
   rewrite Hgm.
 
   cbv [modulusW Tuple.map].
@@ -148,12 +148,12 @@ Proof.
 
   split.
   { match goal with
-    |- (_,word64ToZ (_ ^- (Interpretations.Word64.ZToWord64 ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
+    |- (_,word128ToZ (_ ^- (Interpretations128.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord128 with Interpretations128.WordW.ZToWordW in *.
+  rewrite !Interpretations128.WordW.wordWToZ_sub;
+  rewrite !Interpretations128.WordW.wordWToZ_land;
+  rewrite !Interpretations128.WordW.wordWToZ_ZToWordW;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
@@ -170,10 +170,10 @@ Proof.
 
 
   unfold_is_bounded.
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord128 with Interpretations128.WordW.ZToWordW in *.
+  rewrite !Interpretations128.WordW.wordWToZ_sub;
+  rewrite !Interpretations128.WordW.wordWToZ_land;
+  rewrite !Interpretations128.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
@@ -235,7 +235,7 @@ Proof.
   hnf in f, g; destruct_head' prod.
   eexists.
   cbv [GF25519_64.fieldwiseb fe25519_64WToZ].
-  rewrite ?word64eqb_Zeqb.
+  rewrite ?word128eqb_Zeqb.
   reflexivity.
 Defined.
 
@@ -288,7 +288,7 @@ Qed.
 
 Definition sqrt_m1W' : fe25519_64W :=
   Eval vm_compute in fe25519_64ZToW sqrt_m1.
-Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe25519_64W_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe25519_64W_word64ize sqrt_m1W'.
+Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe25519_64W_word128ize word128ize andb opt.word128ToZ opt.word128ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe25519_64W_word128ize sqrt_m1W'.
 
 Definition GF25519_64sqrt x : GF25519_64.fe25519_64 :=
   dlet powx := powW (fe25519_64ZToW x) (chain GF25519_64.sqrt_ec) in
@@ -366,7 +366,7 @@ Definition opp (f : fe25519_64) : fe25519_64.
 Proof. define_unop f oppW oppW_correct_and_bounded. Defined.
 Definition freeze (f : fe25519_64) : fe25519_64.
 Proof. define_unop f freezeW freezeW_correct_and_bounded. Defined.
-Definition ge_modulus (f : fe25519_64) : word64.
+Definition ge_modulus (f : fe25519_64) : word128.
 Proof. define_unop_FEToZ f ge_modulusW. Defined.
 Definition pack (f : fe25519_64) : wire_digits.
 Proof. define_unop_FEToWire f packW packW_correct_and_bounded. Defined.
@@ -407,7 +407,7 @@ Lemma opp_correct (f : fe25519_64) : proj1_fe25519_64 (opp f) = carry_opp (proj1
 Proof. op_correct_t opp oppW_correct_and_bounded. Qed.
 Lemma freeze_correct (f : fe25519_64) : proj1_fe25519_64 (freeze f) = GF25519_64.freeze (proj1_fe25519_64 f).
 Proof. op_correct_t freeze freezeW_correct_and_bounded. Qed.
-Lemma ge_modulus_correct (f : fe25519_64) : word64ToZ (ge_modulus f) = GF25519_64.ge_modulus (proj1_fe25519_64 f).
+Lemma ge_modulus_correct (f : fe25519_64) : word128ToZ (ge_modulus f) = GF25519_64.ge_modulus (proj1_fe25519_64 f).
 Proof. op_correct_t ge_modulus ge_modulusW_correct. Qed.
 Lemma pack_correct (f : fe25519_64) : proj1_wire_digits (pack f) = GF25519_64.pack (proj1_fe25519_64 f).
 Proof. op_correct_t pack packW_correct_and_bounded. Qed.
diff --git a/src/SpecificGen/GF25519_64BoundedCommon.v b/src/SpecificGen/GF25519_64BoundedCommon.v
index e6a3b6c20..b14612f07 100644
--- a/src/SpecificGen/GF25519_64BoundedCommon.v
+++ b/src/SpecificGen/GF25519_64BoundedCommon.v
@@ -38,50 +38,50 @@ Definition wire_digit_bounds : tuple (Z * Z) (length wire_widths)
 (* END common curve-specific definitions *)
 
 (* BEGIN aliases for word extraction *)
-Definition word64 := Word.word bit_width.
-Coercion word64ToZ (x : word64) : Z := Z.of_N (wordToN x).
-Coercion ZToWord64 (x : Z) : word64 := NToWord _ (Z.to_N x).
-Definition NToWord64 : N -> word64 := NToWord _.
-Definition word64ize (x : word64) : word64
-  := Eval cbv [wordToN N.succ_double N.double] in NToWord64 (wordToN x).
-Definition w64eqb (x y : word64) := weqb x y.
-
-Global Arguments NToWord64 : simpl never.
-Arguments word64 : simpl never.
+Definition word128 := Word.word bit_width.
+Coercion word128ToZ (x : word128) : Z := Z.of_N (wordToN x).
+Coercion ZToWord128 (x : Z) : word128 := NToWord _ (Z.to_N x).
+Definition NToWord128 : N -> word128 := NToWord _.
+Definition word128ize (x : word128) : word128
+  := Eval cbv [wordToN N.succ_double N.double] in NToWord128 (wordToN x).
+Definition w128eqb (x y : word128) := weqb x y.
+
+Global Arguments NToWord128 : simpl never.
+Arguments word128 : simpl never.
 Arguments bit_width : simpl never.
-Global Opaque word64.
+Global Opaque word128.
 Global Opaque bit_width.
 
 (* END aliases for word extraction *)
 
 (* BEGIN basic types *)
 Module Type WordIsBounded.
-  Parameter is_boundedT : forall (lower upper : Z), word64 -> bool.
-  Parameter Build_is_boundedT : forall {lower upper} {proj_word : word64},
+  Parameter is_boundedT : forall (lower upper : Z), word128 -> bool.
+  Parameter Build_is_boundedT : forall {lower upper} {proj_word : word128},
       andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true -> is_boundedT lower upper proj_word = true.
-  Parameter project_is_boundedT : forall {lower upper} {proj_word : word64},
+  Parameter project_is_boundedT : forall {lower upper} {proj_word : word128},
       is_boundedT lower upper proj_word = true -> andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true.
 End WordIsBounded.
 
 Module Import WordIsBoundedDefault : WordIsBounded.
-  Definition is_boundedT : forall (lower upper : Z), word64 -> bool
+  Definition is_boundedT : forall (lower upper : Z), word128 -> bool
     := fun lower upper proj_word => andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z.
-  Definition Build_is_boundedT {lower upper} {proj_word : word64}
+  Definition Build_is_boundedT {lower upper} {proj_word : word128}
     : andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true -> is_boundedT lower upper proj_word = true
     := fun x => x.
-  Definition project_is_boundedT {lower upper} {proj_word : word64}
+  Definition project_is_boundedT {lower upper} {proj_word : word128}
     : is_boundedT lower upper proj_word = true -> andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true
     := fun x => x.
 End WordIsBoundedDefault.
 
 Definition bounded_word (lower upper : Z)
-  := { proj_word : word64 | is_boundedT lower upper proj_word = true }.
+  := { proj_word : word128 | is_boundedT lower upper proj_word = true }.
 Local Notation word_of exp := (bounded_word (fst (b_of exp)) (snd (b_of exp))).
 Local Notation unbounded_word sz := (bounded_word 0 (2^sz-1)%Z).
 
-Local Opaque word64.
-Definition fe25519_64W := Eval cbv (*-[word64]*) in (tuple word64 length_fe25519_64).
-Definition wire_digitsW := Eval cbv (*-[word64]*) in (tuple word64 (length wire_widths)).
+Local Opaque word128.
+Definition fe25519_64W := Eval cbv (*-[word128]*) in (tuple word128 length_fe25519_64).
+Definition wire_digitsW := Eval cbv (*-[word128]*) in (tuple word128 (length wire_widths)).
 Definition fe25519_64 :=
   Eval cbv -[bounded_word Z.pow Z.sub Z.add] in
     hlist (fun e => word_of e) bounds_exp.
@@ -203,25 +203,25 @@ Defined.
 Definition eta_wire_digitsW (x : wire_digitsW) : wire_digitsW
   := Eval cbv [proj1_sig eta_wire_digitsW_sig] in proj1_sig (eta_wire_digitsW_sig x).
 
-Local Transparent word64.
-Lemma word64ize_id x : word64ize x = x.
+Local Transparent word128.
+Lemma word128ize_id x : word128ize x = x.
 Proof. apply NToWord_wordToN. Qed.
-Local Opaque word64.
+Local Opaque word128.
 
-Lemma word64eqb_Zeqb x y : (word64ToZ x =? word64ToZ y)%Z = w64eqb x y.
+Lemma word128eqb_Zeqb x y : (word128ToZ x =? word128ToZ y)%Z = w128eqb x y.
 Proof. apply wordeqb_Zeqb. Qed.
 
 Local Arguments Z.pow_pos !_ !_ / .
-Lemma word64ToZ_ZToWord64 x : 0 <= x < 2^Z.of_nat bit_width -> word64ToZ (ZToWord64 x) = x.
+Lemma word128ToZ_ZToWord128 x : 0 <= x < 2^Z.of_nat bit_width -> word128ToZ (ZToWord128 x) = x.
 Proof.
-  intros; unfold word64ToZ, ZToWord64.
+  intros; unfold word128ToZ, ZToWord128.
   rewrite wordToN_NToWord_idempotent, Z2N.id
     by (omega || apply N2Z.inj_lt; rewrite <- ?(N_nat_Z (Npow2 _)), ?Npow2_nat, ?Zpow_pow2, ?N2Z.id, ?Z2N.id, ?Z2Nat.id by omega; omega).
   reflexivity.
 Qed.
-Lemma ZToWord64_word64ToZ x : ZToWord64 (word64ToZ x) = x.
+Lemma ZToWord128_word128ToZ x : ZToWord128 (word128ToZ x) = x.
 Proof.
-  intros; unfold word64ToZ, ZToWord64.
+  intros; unfold word128ToZ, ZToWord128.
   rewrite N2Z.id, NToWord_wordToN; reflexivity.
 Qed.
 
@@ -236,7 +236,7 @@ Definition Build_bounded_word' {lower upper} proj_word word_bounded : bounded_wo
 Arguments proj_word {_ _} _.
 Arguments word_bounded {_ _} _.
 Arguments Build_bounded_word' {_ _} _ _.
-Definition Build_bounded_word {lower upper} (proj_word : word64) (word_bounded : andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true)
+Definition Build_bounded_word {lower upper} (proj_word : word128) (word_bounded : andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true)
   : bounded_word lower upper
   := Build_bounded_word'
        proj_word
@@ -244,13 +244,13 @@ Definition Build_bounded_word {lower upper} (proj_word : word64) (word_bounded :
         | true => fun _ => eq_refl
         | false => fun x => x
         end word_bounded).
-Lemma word_to_unbounded_helper {x e : nat} : (x < pow2 e)%nat -> (Z.of_nat e <= Z.of_nat bit_width)%Z -> ((0 <=? word64ToZ (ZToWord64 (Z.of_nat x))) && (word64ToZ (ZToWord64 (Z.of_nat x)) <=? 2 ^ (Z.of_nat e) - 1))%bool = true.
+Lemma word_to_unbounded_helper {x e : nat} : (x < pow2 e)%nat -> (Z.of_nat e <= Z.of_nat bit_width)%Z -> ((0 <=? word128ToZ (ZToWord128 (Z.of_nat x))) && (word128ToZ (ZToWord128 (Z.of_nat x)) <=? 2 ^ (Z.of_nat e) - 1))%bool = true.
 Proof.
   rewrite pow2_id; intro H; apply Nat2Z.inj_lt in H; revert H.
   rewrite Z.pow_Zpow; simpl Z.of_nat.
   intros H H'.
   assert (2^Z.of_nat e <= 2^Z.of_nat bit_width) by auto with zarith.
-  rewrite ?word64ToZ_ZToWord64 by omega.
+  rewrite ?word128ToZ_ZToWord128 by omega.
   match goal with
   | [ |- context[andb ?x ?y] ]
     => destruct x eqn:?, y eqn:?; try reflexivity; Z.ltb_to_lt
@@ -267,26 +267,26 @@ Proof. apply (word_to_unbounded_word x); reflexivity. Defined.
 Definition word31_to_unbounded_word (x : word 31) : unbounded_word 31.
 Proof. apply (word_to_unbounded_word x); reflexivity. Defined.
 
-Local Opaque word64.
+Local Opaque word128.
 Declare Reduction app_tuple_map := cbv [app_wire_digitsW app_fe25519_64W app_fe25519_64 HList.mapt HList.mapt' Tuple.map on_tuple List.map List.app length_fe25519_64 List.length wire_widths Tuple.from_list Tuple.from_list' Tuple.to_list Tuple.to_list' fst snd].
 Definition fe25519_64WToZ (x : fe25519_64W) : SpecificGen.GF25519_64.fe25519_64
   := Eval app_tuple_map in
-      app_fe25519_64W x (Tuple.map (fun v : word64 => v : Z)).
+      app_fe25519_64W x (Tuple.map (fun v : word128 => v : Z)).
 Definition fe25519_64ZToW (x : SpecificGen.GF25519_64.fe25519_64) : fe25519_64W
   := Eval app_tuple_map in
-      app_fe25519_64W x (Tuple.map (fun v : Z => v : word64)).
+      app_fe25519_64W x (Tuple.map (fun v : Z => v : word128)).
 Definition wire_digitsWToZ (x : wire_digitsW) : SpecificGen.GF25519_64.wire_digits
   := Eval app_tuple_map in
-      app_wire_digitsW x (Tuple.map (fun v : word64 => v : Z)).
+      app_wire_digitsW x (Tuple.map (fun v : word128 => v : Z)).
 Definition wire_digitsZToW (x : SpecificGen.GF25519_64.wire_digits) : wire_digitsW
   := Eval app_tuple_map in
-      app_wire_digitsW x (Tuple.map (fun v : Z => v : word64)).
-Definition fe25519_64W_word64ize (x : fe25519_64W) : fe25519_64W
+      app_wire_digitsW x (Tuple.map (fun v : Z => v : word128)).
+Definition fe25519_64W_word128ize (x : fe25519_64W) : fe25519_64W
   := Eval app_tuple_map in
-      app_fe25519_64W x (Tuple.map word64ize).
-Definition wire_digitsW_word64ize (x : wire_digitsW) : wire_digitsW
+      app_fe25519_64W x (Tuple.map word128ize).
+Definition wire_digitsW_word128ize (x : wire_digitsW) : wire_digitsW
   := Eval app_tuple_map in
-      app_wire_digitsW x (Tuple.map word64ize).
+      app_wire_digitsW x (Tuple.map word128ize).
 
 (** TODO: Turn this into a lemma to speed up proofs *)
 Ltac unfold_is_bounded_in H :=
@@ -300,17 +300,17 @@ Ltac unfold_is_bounded :=
   rewrite ?Bool.andb_true_iff.
 
 Local Transparent bit_width.
-Definition Pow2_64 := Eval compute in 2^Z.of_nat bit_width.
-Definition unfold_Pow2_64 : 2^Z.of_nat bit_width = Pow2_64 := eq_refl.
+Definition Pow2_128 := Eval compute in 2^Z.of_nat bit_width.
+Definition unfold_Pow2_128 : 2^Z.of_nat bit_width = Pow2_128 := eq_refl.
 Local Opaque bit_width.
 
 Local Ltac prove_lt_bit_width :=
-  rewrite unfold_Pow2_64; cbv [Pow2_64]; omega.
+  rewrite unfold_Pow2_128; cbv [Pow2_128]; omega.
 
 Lemma fe25519_64ZToW_WToZ (x : fe25519_64W) : fe25519_64ZToW (fe25519_64WToZ x) = x.
 Proof.
   hnf in x; destruct_head' prod; cbv [fe25519_64WToZ fe25519_64ZToW].
-  rewrite !ZToWord64_word64ToZ; reflexivity.
+  rewrite !ZToWord128_word128ToZ; reflexivity.
 Qed.
 
 Lemma fe25519_64WToZ_ZToW x : is_bounded x = true -> fe25519_64WToZ (fe25519_64ZToW x) = x.
@@ -319,36 +319,36 @@ Proof.
   intro H.
   unfold_is_bounded_in H; destruct_head' and.
   Z.ltb_to_lt.
-  rewrite !word64ToZ_ZToWord64 by prove_lt_bit_width.
+  rewrite !word128ToZ_ZToWord128 by prove_lt_bit_width.
   reflexivity.
 Qed.
 
-Lemma fe25519_64W_word64ize_id x : fe25519_64W_word64ize x = x.
+Lemma fe25519_64W_word128ize_id x : fe25519_64W_word128ize x = x.
 Proof.
   hnf in x; destruct_head' prod.
-  cbv [fe25519_64W_word64ize];
-    repeat apply f_equal2; apply word64ize_id.
+  cbv [fe25519_64W_word128ize];
+    repeat apply f_equal2; apply word128ize_id.
 Qed.
-Lemma wire_digitsW_word64ize_id x : wire_digitsW_word64ize x = x.
+Lemma wire_digitsW_word128ize_id x : wire_digitsW_word128ize x = x.
 Proof.
   hnf in x; destruct_head' prod.
-  cbv [wire_digitsW_word64ize];
-    repeat apply f_equal2; apply word64ize_id.
+  cbv [wire_digitsW_word128ize];
+    repeat apply f_equal2; apply word128ize_id.
 Qed.
 
 Definition uncurry_unop_fe25519_64W {T} (op : fe25519_64W -> T)
-  := Eval cbv (*-[word64]*) in Tuple.uncurry (n:=length_fe25519_64) op.
+  := Eval cbv (*-[word128]*) in Tuple.uncurry (n:=length_fe25519_64) op.
 Definition curry_unop_fe25519_64W {T} op : fe25519_64W -> T
-  := Eval cbv (*-[word64]*) in fun f => app_fe25519_64W f (Tuple.curry (n:=length_fe25519_64) op).
+  := Eval cbv (*-[word128]*) in fun f => app_fe25519_64W f (Tuple.curry (n:=length_fe25519_64) op).
 Definition uncurry_binop_fe25519_64W {T} (op : fe25519_64W -> fe25519_64W -> T)
-  := Eval cbv (*-[word64]*) in uncurry_unop_fe25519_64W (fun f => uncurry_unop_fe25519_64W (op f)).
+  := Eval cbv (*-[word128]*) in uncurry_unop_fe25519_64W (fun f => uncurry_unop_fe25519_64W (op f)).
 Definition curry_binop_fe25519_64W {T} op : fe25519_64W -> fe25519_64W -> T
-  := Eval cbv (*-[word64]*) in appify2 (fun f => curry_unop_fe25519_64W (curry_unop_fe25519_64W op f)).
+  := Eval cbv (*-[word128]*) in appify2 (fun f => curry_unop_fe25519_64W (curry_unop_fe25519_64W op f)).
 
 Definition uncurry_unop_wire_digitsW {T} (op : wire_digitsW -> T)
-  := Eval cbv (*-[word64]*) in Tuple.uncurry (n:=length wire_widths) op.
+  := Eval cbv (*-[word128]*) in Tuple.uncurry (n:=length wire_widths) op.
 Definition curry_unop_wire_digitsW {T} op : wire_digitsW -> T
-  := Eval cbv (*-[word64]*) in fun f => app_wire_digitsW f (Tuple.curry (n:=length wire_widths) op).
+  := Eval cbv (*-[word128]*) in fun f => app_wire_digitsW f (Tuple.curry (n:=length wire_widths) op).
 
 
 Definition proj1_fe25519_64W (x : fe25519_64) : fe25519_64W
@@ -417,7 +417,7 @@ Local Ltac make_exist'' x exist_W ZToW :=
       unfold_is_bounded_in H;
       destruct_head' and; simpl in *;
       Z.ltb_to_lt;
-      rewrite ?word64ToZ_ZToWord64 by prove_lt_bit_width;
+      rewrite ?word128ToZ_ZToWord128 by prove_lt_bit_width;
       assumption
     ).
 Local Ltac make_exist' x app_W_dep exist'' exist_W ZToW :=
@@ -459,7 +459,7 @@ Proof.
   unfold_is_bounded_in pf.
   destruct_head' and.
   Z.ltb_to_lt.
-  rewrite ?word64ToZ_ZToWord64 by prove_lt_bit_width.
+  rewrite ?word128ToZ_ZToWord128 by prove_lt_bit_width.
   reflexivity.
 Qed.
 
@@ -491,18 +491,18 @@ Proof.
   unfold_is_bounded_in pf.
   destruct_head' and.
   Z.ltb_to_lt.
-  rewrite ?word64ToZ_ZToWord64 by prove_lt_bit_width.
+  rewrite ?word128ToZ_ZToWord128 by prove_lt_bit_width.
   reflexivity.
 Qed.
 
 Module opt.
-  Definition word64ToZ := Eval vm_compute in word64ToZ.
-  Definition word64ToN := Eval vm_compute in @wordToN bit_width.
-  Definition NToWord64 := Eval vm_compute in NToWord64.
+  Definition word128ToZ := Eval vm_compute in word128ToZ.
+  Definition word128ToN := Eval vm_compute in @wordToN bit_width.
+  Definition NToWord128 := Eval vm_compute in NToWord128.
   Definition bit_width := Eval vm_compute in bit_width.
   Definition Zleb := Eval cbv [Z.leb] in Z.leb.
   Definition andb := Eval vm_compute in andb.
-  Definition word64ize := Eval vm_compute in word64ize.
+  Definition word128ize := Eval vm_compute in word128ize.
 End opt.
 
 Local Transparent bit_width.
@@ -512,35 +512,35 @@ Local Ltac do_change lem :=
     => let x' := (eval vm_compute in x) in
        let z' := (eval vm_compute in z) in
        lazymatch y with
-       | word64ToZ (word64ize ?v)
-         => let y' := constr:(opt.word64ToZ (opt.word64ize v)) in
+       | word128ToZ (word128ize ?v)
+         => let y' := constr:(opt.word128ToZ (opt.word128ize v)) in
             let L' := context L[andb (opt.Zleb x' y') (opt.Zleb y' z')] in
             do_change L'
        end
   | _ => lem
   end.
-Definition fe25519_64_word64ize (x : fe25519_64) : fe25519_64.
+Definition fe25519_64_word128ize (x : fe25519_64) : fe25519_64.
 Proof.
   set (x' := x).
   hnf in x; destruct_head' prod.
-  let lem := constr:(exist_fe25519_64W (fe25519_64W_word64ize (proj1_fe25519_64W x'))) in
-  let lem := (eval cbv [proj1_fe25519_64W x' fe25519_64W_word64ize proj_word exist_fe25519_64W Build_bounded_word' Build_bounded_word] in lem) in
+  let lem := constr:(exist_fe25519_64W (fe25519_64W_word128ize (proj1_fe25519_64W x'))) in
+  let lem := (eval cbv [proj1_fe25519_64W x' fe25519_64W_word128ize proj_word exist_fe25519_64W Build_bounded_word' Build_bounded_word] in lem) in
   let lem := do_change lem in
   refine (lem _);
-    change (is_bounded (fe25519_64WToZ (fe25519_64W_word64ize (proj1_fe25519_64W x'))) = true);
-    abstract (rewrite fe25519_64W_word64ize_id; apply is_bounded_proj1_fe25519_64).
+    change (is_bounded (fe25519_64WToZ (fe25519_64W_word128ize (proj1_fe25519_64W x'))) = true);
+    abstract (rewrite fe25519_64W_word128ize_id; apply is_bounded_proj1_fe25519_64).
 Defined.
-Definition wire_digits_word64ize (x : wire_digits) : wire_digits.
+Definition wire_digits_word128ize (x : wire_digits) : wire_digits.
 Proof.
   set (x' := x).
   hnf in x; destruct_head' prod.
-  let lem := constr:(exist_wire_digitsW (wire_digitsW_word64ize (proj1_wire_digitsW x'))) in
-  let lem := (eval cbv [proj1_wire_digitsW x' wire_digitsW_word64ize proj_word exist_wire_digitsW Build_bounded_word Build_bounded_word'] in lem) in
+  let lem := constr:(exist_wire_digitsW (wire_digitsW_word128ize (proj1_wire_digitsW x'))) in
+  let lem := (eval cbv [proj1_wire_digitsW x' wire_digitsW_word128ize proj_word exist_wire_digitsW Build_bounded_word Build_bounded_word'] in lem) in
   let lem := do_change lem in
-  let lem := (eval cbv [word64ize opt.word64ize andb Z.leb Z.compare CompOpp Pos.compare] in lem) in
+  let lem := (eval cbv [word128ize opt.word128ize andb Z.leb Z.compare CompOpp Pos.compare] in lem) in
   refine (lem _);
-    change (wire_digits_is_bounded (wire_digitsWToZ (wire_digitsW_word64ize (proj1_wire_digitsW x'))) = true);
-    abstract (rewrite wire_digitsW_word64ize_id; apply is_bounded_proj1_wire_digits).
+    change (wire_digits_is_bounded (wire_digitsWToZ (wire_digitsW_word128ize (proj1_wire_digitsW x'))) = true);
+    abstract (rewrite wire_digitsW_word128ize_id; apply is_bounded_proj1_wire_digits).
 Defined.
 
 Lemma is_bounded_to_nth_default x (H : is_bounded x = true)
@@ -566,10 +566,10 @@ Qed.
 (* Precompute constants *)
 
 Definition one' := Eval vm_compute in exist_fe25519_64 SpecificGen.GF25519_64.one_ eq_refl.
-Definition one := Eval cbv [one' fe25519_64_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe25519_64_word64ize one'.
+Definition one := Eval cbv [one' fe25519_64_word128ize word128ize andb opt.word128ToZ opt.word128ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe25519_64_word128ize one'.
 
 Definition zero' := Eval vm_compute in exist_fe25519_64 SpecificGen.GF25519_64.zero_ eq_refl.
-Definition zero := Eval cbv [zero' fe25519_64_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe25519_64_word64ize zero'.
+Definition zero := Eval cbv [zero' fe25519_64_word128ize word128ize andb opt.word128ToZ opt.word128ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in fe25519_64_word128ize zero'.
 
 Lemma fold_chain_opt_gen {A B} (F : A -> B) is_bounded ls id' op' id op chain
       (Hid_bounded : is_bounded (F id') = true)
@@ -642,7 +642,7 @@ Proof.
   unfold_is_bounded_in pf.
   destruct_head' and.
   Z.ltb_to_lt.
-  rewrite ?word64ToZ_ZToWord64 by prove_lt_bit_width.
+  rewrite ?word128ToZ_ZToWord128 by prove_lt_bit_width.
   reflexivity.
 Qed.
 
@@ -654,7 +654,7 @@ Proof.
   unfold_is_bounded_in pf.
   destruct_head' and.
   Z.ltb_to_lt.
-  rewrite ?word64ToZ_ZToWord64 by prove_lt_bit_width.
+  rewrite ?word128ToZ_ZToWord128 by prove_lt_bit_width.
   reflexivity.
 Qed.
 
@@ -678,7 +678,7 @@ Notation iunop_correct_and_bounded irop op
 Notation iunop_FEToZ_correct irop op
   := (forall x,
          is_bounded (fe25519_64WToZ x) = true
-         -> word64ToZ (irop x) = op (fe25519_64WToZ x)) (only parsing).
+         -> word128ToZ (irop x) = op (fe25519_64WToZ x)) (only parsing).
 Notation iunop_FEToWire_correct_and_bounded irop op
   := (forall x,
          is_bounded (fe25519_64WToZ x) = true
diff --git a/src/SpecificGen/GF25519_64Reflective.v b/src/SpecificGen/GF25519_64Reflective.v
index 095def252..69d3ea34a 100644
--- a/src/SpecificGen/GF25519_64Reflective.v
+++ b/src/SpecificGen/GF25519_64Reflective.v
@@ -10,9 +10,9 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.MapInterp.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations128.
+Require Crypto.Reflection.Z.Interpretations128.Relations.
+Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.SpecificGen.GF25519_64Reflective.Common.
@@ -41,8 +41,8 @@ Definition rge_modulus : ExprUnOpFEToZ := Eval vm_compute in rge_modulusW.
 Definition rpack : ExprUnOpFEToWire := Eval vm_compute in rpackW.
 Definition runpack : ExprUnOpWireToFE := Eval vm_compute in runpackW.
 
-Definition rword64ize {t} (x : Expr t) : Expr t
-  := MapInterp (fun t => match t with TZ => word64ize end) x.
+Definition rword128ize {t} (x : Expr t) : Expr t
+  := MapInterp (fun t => match t with TZ => word128ize end) x.
 
 Declare Reduction asm_interp
   := cbv beta iota delta
@@ -50,10 +50,10 @@ Declare Reduction asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 Ltac asm_interp
   := cbv beta iota delta
@@ -61,44 +61,44 @@ Ltac asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 
 
 Definition interp_radd : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
-  := Eval asm_interp in interp_bexpr (rword64ize radd).
+  := Eval asm_interp in interp_bexpr (rword128ize radd).
 (*Print interp_radd.*)
 Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl.
 Definition interp_rsub : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
-  := Eval asm_interp in interp_bexpr (rword64ize rsub).
+  := Eval asm_interp in interp_bexpr (rword128ize rsub).
 (*Print interp_rsub.*)
 Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl.
 Definition interp_rmul : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
-  := Eval asm_interp in interp_bexpr (rword64ize rmul).
+  := Eval asm_interp in interp_bexpr (rword128ize rmul).
 (*Print interp_rmul.*)
 Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl.
 Definition interp_ropp : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
-  := Eval asm_interp in interp_uexpr (rword64ize ropp).
+  := Eval asm_interp in interp_uexpr (rword128ize ropp).
 (*Print interp_ropp.*)
 Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl.
 Definition interp_rprefreeze : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
-  := Eval asm_interp in interp_uexpr (rword64ize rprefreeze).
+  := Eval asm_interp in interp_uexpr (rword128ize rprefreeze).
 (*Print interp_rprefreeze.*)
 Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl.
 
-Definition interp_rge_modulus : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.word64
-  := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus).
+Definition interp_rge_modulus : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.word128
+  := Eval asm_interp in interp_uexpr_FEToZ (rword128ize rge_modulus).
 Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl.
 
 Definition interp_rpack : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.wire_digitsW
-  := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack).
+  := Eval asm_interp in interp_uexpr_FEToWire (rword128ize rpack).
 Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl.
 
 Definition interp_runpack : SpecificGen.GF25519_64BoundedCommon.wire_digitsW -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
-  := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack).
+  := Eval asm_interp in interp_uexpr_WireToFE (rword128ize runpack).
 Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl.
 
 Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add.
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v
index 444edcde4..0811a71cc 100644
--- a/src/SpecificGen/GF25519_64Reflective/Common.v
+++ b/src/SpecificGen/GF25519_64Reflective/Common.v
@@ -4,9 +4,9 @@ Require Export Crypto.SpecificGen.GF25519_64.
 Require Export Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations128.
+Require Crypto.Reflection.Z.Interpretations128.Relations.
+Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Export Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.InterpWfRel.
@@ -19,7 +19,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
 
-Notation Expr := (Expr base_type Word64.interp_base_type op).
+Notation Expr := (Expr base_type WordW.interp_base_type op).
 
 Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
@@ -45,9 +45,9 @@ Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
-  | (?x :: nil)%list => constr:(Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |})
+  | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
   | (?x :: ?xs)%list => let bs := bounds_from_list xs in
-                        constr:((Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |}, bs))
+                        constr:((Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs))
   end.
 
 Local Ltac make_bounds ls :=
@@ -66,17 +66,16 @@ Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZB
 Proof. make_bounds (Tuple.to_list _ bounds). Defined.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
-  := fun e => curry_binop_fe25519_64W (Interp (@Word64.interp_op) e).
+  := fun e => curry_binop_fe25519_64W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
-  := fun e => curry_unop_fe25519_64W (Interp (@Word64.interp_op) e).
-Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.word64
-  := fun e => curry_unop_fe25519_64W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe25519_64W (Interp (@WordW.interp_op) e).
+Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.word128
+  := fun e => curry_unop_fe25519_64W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.wire_digitsW
-  := fun e => curry_unop_fe25519_64W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe25519_64W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> SpecificGen.GF25519_64BoundedCommon.wire_digitsW -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
-  := fun e => curry_unop_wire_digitsW (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_wire_digitsW (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -117,13 +116,13 @@ Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
       let ropZ_sig := ropZ_sigv in
       let ropW := MapInterp (fun _ x => x) ropW' in
-      let ropZ := MapInterp Word64.to_Z ropW' in
-      let ropBounds := MapInterp ZBounds.of_word64 ropW' in
-      let ropBoundedWord64 := MapInterp BoundedWord64.of_word64 ropW' in
+      let ropZ := MapInterp WordW.to_Z ropW' in
+      let ropBounds := MapInterp ZBounds.of_wordW ropW' in
+      let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in
       ropZ = proj1_sig ropZ_sig
-      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Z.interp_op) ropZ)
-      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@ZBounds.interp_op) ropBounds)
-      /\ interp_type_rel_pointwise2 Relations.related_word64 (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Word64.interp_op) ropW))
+      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ)
+      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds)
+      /\ interp_type_rel_pointwise2 Relations.related_wordW (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@WordW.interp_op) ropW))
        (only parsing).
 
 Ltac app_tuples x y :=
@@ -138,7 +137,7 @@ Local Arguments Tuple.map2 : simpl never.
 Local Arguments Tuple.map : simpl never.
 
 Fixpoint args_to_bounded_helperT {n}
-         (v : Tuple.tuple' Word64.word64 n)
+         (v : Tuple.tuple' WordW.wordW n)
          (bounds : Tuple.tuple' (Z * Z) n)
          (pf : List.fold_right
                  andb true
@@ -149,7 +148,7 @@ Fixpoint args_to_bounded_helperT {n}
                        (fun bounds v =>
                           let '(lower, upper) := bounds in ((lower <=? v)%Z && (v <=? upper)%Z)%bool)
                        bounds
-                       (Tuple.map (n:=S n) Word64.word64ToZ v))) = true)
+                       (Tuple.map (n:=S n) WordW.wordWToZ v))) = true)
          (res : Type)
          {struct n}
   : Type.
@@ -161,9 +160,9 @@ Proof.
                                       (Tuple.map2 (n:=S n) _ bounds (Tuple.map (n:=S n) _ v))) = true
                              -> Type)
           with
-          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat Word64.bit_width)%Z, res
+          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat WordW.bit_width)%Z, res
           | S n' => fun v' bounds' pf0 => let t := _ in
-                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
+                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat WordW.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
           end v bounds pf).
   { clear -pf0.
     abstract (
@@ -178,15 +177,15 @@ Defined.
 
 Fixpoint args_to_bounded_helper {n} res
          {struct n}
-  : forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
+  : forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
 Proof.
-  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
-         | 0 => fun v bounds pf f pf' => f {| BoundedWord64.lower := fst bounds ; BoundedWord64.value := v ; BoundedWord64.upper := snd bounds |}
+  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
+         | 0 => fun v bounds pf f pf' => f {| BoundedWord.lower := fst bounds ; BoundedWord.value := v ; BoundedWord.upper := snd bounds |}
          | S n'
            => fun v bounds pf f pf'
               => @args_to_bounded_helper
                    n' res (fst v) (fst bounds) _
-                   (fun ts => f (ts, {| BoundedWord64.lower := fst (snd bounds) ; BoundedWord64.value := snd v ; BoundedWord64.upper := snd (snd bounds) |}))
+                   (fun ts => f (ts, {| BoundedWord.lower := fst (snd bounds) ; BoundedWord.value := snd v ; BoundedWord.upper := snd (snd bounds) |}))
          end.
   { clear -pf pf'.
     unfold Tuple.map2, Tuple.map in pf; simpl in *.
@@ -242,16 +241,16 @@ Local Ltac args_to_bounded x H :=
       ).
 
 Definition unop_args_to_bounded (x : fe25519_64W) (H : is_bounded (fe25519_64WToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpT).
 Proof. args_to_bounded x H. Defined.
 
 Definition unopWireToFE_args_to_bounded (x : wire_digitsW) (H : wire_digits_is_bounded (wire_digitsWToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpWireToFET).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpWireToFET).
 Proof. args_to_bounded x H. Defined.
 Definition binop_args_to_bounded (x : fe25519_64W * fe25519_64W)
            (H : is_bounded (fe25519_64WToZ (fst x)) = true)
            (H' : is_bounded (fe25519_64WToZ (snd x)) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprBinOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprBinOpT).
 Proof.
   let v := app_tuples (unop_args_to_bounded (fst x) H) (unop_args_to_bounded (snd x) H') in
   exact v.
@@ -328,13 +327,13 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   change interp_base_type with (@Z.interp_base_type) in *;
   rewrite <- Heq; clear Heq;
   destruct Hbounds as [ Hbounds0 [Hbounds1 Hbounds2] ];
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 Word64.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_word64_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 WordW.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_wordW_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
   specialize_by repeat first [ progress intros
                              | reflexivity
                              | assumption
                              | progress destruct_head' base_type
-                             | progress destruct_head' BoundedWord64.BoundedWord
+                             | progress destruct_head' BoundedWordW.BoundedWord
                              | progress destruct_head' and
                              | progress repeat apply conj ];
   specialize (Hbounds_left args H0);
@@ -350,7 +349,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWord64.to_word64' BoundedWord64.boundedWordToWord64 BoundedWord64.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_word64_boundsi' Relations.related'_word64_bounds ZBounds.upper ZBounds.lower Application.remove_all_binders Word64.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe25519_64WToZ ?x = _ /\ _ ]
     => destruct x; destruct_head_hnf' prod
@@ -359,7 +358,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
-  change word64ToZ with Word64.word64ToZ in *;
+  change word128ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
@@ -371,7 +370,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
-  change Word64.word64ToZ with word64ToZ in *;
+  change WordW.wordWToZ with word128ToZ in *;
   repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
 
 
@@ -387,10 +386,10 @@ Ltac rexpr_correct :=
     [ | apply @RelWfMapInterp, wf_ropW ].. ];
   auto with interp_related.
 
-Notation rword_of_Z rexprZ_sig := (MapInterp Word64.of_Z (proj1_sig rexprZ_sig)) (only parsing).
+Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing).
 
 Notation compute_bounds opW bounds
-  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_word64) opW)) bounds)
+  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds)
        (only parsing).
 
 
@@ -407,7 +406,7 @@ Module Export PrettyPrinting.
     := fun t : base_type
        => match t return ZBounds.interp_base_type t -> match t with TZ => bounds_on end with
           | TZ => fun x => match x with
-                           | Some {| ZBounds.lower := l ; ZBounds.upper := u |}
+                           | Some {| Bounds.lower := l ; Bounds.upper := u |}
                              => in_range l u
                            | None
                              => overflow
diff --git a/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v b/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v
index cd4a5031b..c8872efc5 100644
--- a/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations128.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -18,7 +18,7 @@ Lemma ExprBinOp_correct_and_bounded
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded xy Hx Hy in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -31,9 +31,9 @@ Lemma ExprBinOp_correct_and_bounded
           let Hx := let (Hx, Hy) := Hxy in Hx in
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => binop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v
index bfc3c3cc1..f6a71740a 100644
--- a/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations128.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOp_correct_and_bounded
                    (Hx : is_bounded (fe25519_64WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOp_correct_and_bounded
                    (x := eta_fe25519_64W x)
                    (Hx : is_bounded (fe25519_64WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v
index f615067c6..7bd176749 100644
--- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations128.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (Hx : is_bounded (fe25519_64WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (x := eta_fe25519_64W x)
                    (Hx : is_bounded (fe25519_64WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToWire_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v
index 079a0729c..d6b8bb2c7 100644
--- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations128.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (Hx : is_bounded (fe25519_64WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (x := eta_fe25519_64W x)
                    (Hx : is_bounded (fe25519_64WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToZ_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v
index c58f70e91..baadad3c3 100644
--- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations128.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (x := eta_wire_digitsW x)
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopWireToFE_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF41417_32Bounded.v b/src/SpecificGen/GF41417_32Bounded.v
index 53ee754f2..be7cf5714 100644
--- a/src/SpecificGen/GF41417_32Bounded.v
+++ b/src/SpecificGen/GF41417_32Bounded.v
@@ -78,7 +78,7 @@ Definition postfreezeW : fe41417_32W -> fe41417_32W :=
          (num_limbs := length_fe41417_32)
          modulusW
          ge_modulusW
-         (Interpretations.Word64.neg GF41417_32.int_width)
+         (Interpretations64.WordW.neg GF41417_32.int_width)
       ).
 
 Definition freezeW (f : fe41417_32W) : fe41417_32W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
@@ -117,7 +117,7 @@ Ltac lower_bound_minus_ge_modulus :=
   cbv [ge_modulus Let_In ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne ModularBaseSystemListZOperations.neg];
   repeat break_if; Z.ltb_to_lt; subst; try omega;
     rewrite ?Z.land_0_l; auto;
-    change Interpretations.Word64.word64ToZ with word64ToZ;
+    change Interpretations64.WordW.wordWToZ with word64ToZ;
     etransitivity; try apply Z.land_upper_bound_r; instantiate; try omega;
     apply Z.ones_nonneg; instantiate; vm_compute; discriminate.
 
@@ -136,8 +136,8 @@ Proof.
   destruct_head' and.
   Z.ltb_to_lt.
   cbv [postfreezeW].
-  cbv [conditional_subtract_modulusW Interpretations.Word64.neg].
-  change word64ToZ with Interpretations.Word64.word64ToZ in *.
+  cbv [conditional_subtract_modulusW Interpretations64.WordW.neg].
+  change word64ToZ with Interpretations64.WordW.wordWToZ in *.
   rewrite Hgm.
 
   cbv [modulusW Tuple.map].
@@ -148,12 +148,12 @@ Proof.
 
   split.
   { match goal with
-    |- (_,word64ToZ (_ ^- (Interpretations.Word64.ZToWord64 ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
+    |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  rewrite !Interpretations64.WordW.wordWToZ_sub;
+  rewrite !Interpretations64.WordW.wordWToZ_land;
+  rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
@@ -170,10 +170,10 @@ Proof.
 
 
   unfold_is_bounded.
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  rewrite !Interpretations64.WordW.wordWToZ_sub;
+  rewrite !Interpretations64.WordW.wordWToZ_land;
+  rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
diff --git a/src/SpecificGen/GF41417_32Reflective.v b/src/SpecificGen/GF41417_32Reflective.v
index d85e22870..d89b5d87b 100644
--- a/src/SpecificGen/GF41417_32Reflective.v
+++ b/src/SpecificGen/GF41417_32Reflective.v
@@ -10,9 +10,9 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.MapInterp.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.SpecificGen.GF41417_32Reflective.Common.
@@ -50,10 +50,10 @@ Declare Reduction asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe41417_32W curry_unop_fe41417_32W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 Ltac asm_interp
   := cbv beta iota delta
@@ -61,10 +61,10 @@ Ltac asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe41417_32W curry_unop_fe41417_32W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 
 
diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v
index 517c66d8a..68de90117 100644
--- a/src/SpecificGen/GF41417_32Reflective/Common.v
+++ b/src/SpecificGen/GF41417_32Reflective/Common.v
@@ -4,9 +4,9 @@ Require Export Crypto.SpecificGen.GF41417_32.
 Require Export Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Export Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.InterpWfRel.
@@ -19,7 +19,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
 
-Notation Expr := (Expr base_type Word64.interp_base_type op).
+Notation Expr := (Expr base_type WordW.interp_base_type op).
 
 Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
@@ -45,9 +45,9 @@ Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
-  | (?x :: nil)%list => constr:(Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |})
+  | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
   | (?x :: ?xs)%list => let bs := bounds_from_list xs in
-                        constr:((Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |}, bs))
+                        constr:((Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs))
   end.
 
 Local Ltac make_bounds ls :=
@@ -66,17 +66,16 @@ Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZB
 Proof. make_bounds (Tuple.to_list _ bounds). Defined.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
-  := fun e => curry_binop_fe41417_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_binop_fe41417_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
-  := fun e => curry_unop_fe41417_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe41417_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.word64
-  := fun e => curry_unop_fe41417_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe41417_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.wire_digitsW
-  := fun e => curry_unop_fe41417_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe41417_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> SpecificGen.GF41417_32BoundedCommon.wire_digitsW -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
-  := fun e => curry_unop_wire_digitsW (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_wire_digitsW (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -117,13 +116,13 @@ Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
       let ropZ_sig := ropZ_sigv in
       let ropW := MapInterp (fun _ x => x) ropW' in
-      let ropZ := MapInterp Word64.to_Z ropW' in
-      let ropBounds := MapInterp ZBounds.of_word64 ropW' in
-      let ropBoundedWord64 := MapInterp BoundedWord64.of_word64 ropW' in
+      let ropZ := MapInterp WordW.to_Z ropW' in
+      let ropBounds := MapInterp ZBounds.of_wordW ropW' in
+      let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in
       ropZ = proj1_sig ropZ_sig
-      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Z.interp_op) ropZ)
-      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@ZBounds.interp_op) ropBounds)
-      /\ interp_type_rel_pointwise2 Relations.related_word64 (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Word64.interp_op) ropW))
+      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ)
+      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds)
+      /\ interp_type_rel_pointwise2 Relations.related_wordW (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@WordW.interp_op) ropW))
        (only parsing).
 
 Ltac app_tuples x y :=
@@ -138,7 +137,7 @@ Local Arguments Tuple.map2 : simpl never.
 Local Arguments Tuple.map : simpl never.
 
 Fixpoint args_to_bounded_helperT {n}
-         (v : Tuple.tuple' Word64.word64 n)
+         (v : Tuple.tuple' WordW.wordW n)
          (bounds : Tuple.tuple' (Z * Z) n)
          (pf : List.fold_right
                  andb true
@@ -149,7 +148,7 @@ Fixpoint args_to_bounded_helperT {n}
                        (fun bounds v =>
                           let '(lower, upper) := bounds in ((lower <=? v)%Z && (v <=? upper)%Z)%bool)
                        bounds
-                       (Tuple.map (n:=S n) Word64.word64ToZ v))) = true)
+                       (Tuple.map (n:=S n) WordW.wordWToZ v))) = true)
          (res : Type)
          {struct n}
   : Type.
@@ -161,9 +160,9 @@ Proof.
                                       (Tuple.map2 (n:=S n) _ bounds (Tuple.map (n:=S n) _ v))) = true
                              -> Type)
           with
-          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat Word64.bit_width)%Z, res
+          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat WordW.bit_width)%Z, res
           | S n' => fun v' bounds' pf0 => let t := _ in
-                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
+                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat WordW.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
           end v bounds pf).
   { clear -pf0.
     abstract (
@@ -178,15 +177,15 @@ Defined.
 
 Fixpoint args_to_bounded_helper {n} res
          {struct n}
-  : forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
+  : forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
 Proof.
-  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
-         | 0 => fun v bounds pf f pf' => f {| BoundedWord64.lower := fst bounds ; BoundedWord64.value := v ; BoundedWord64.upper := snd bounds |}
+  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
+         | 0 => fun v bounds pf f pf' => f {| BoundedWord.lower := fst bounds ; BoundedWord.value := v ; BoundedWord.upper := snd bounds |}
          | S n'
            => fun v bounds pf f pf'
               => @args_to_bounded_helper
                    n' res (fst v) (fst bounds) _
-                   (fun ts => f (ts, {| BoundedWord64.lower := fst (snd bounds) ; BoundedWord64.value := snd v ; BoundedWord64.upper := snd (snd bounds) |}))
+                   (fun ts => f (ts, {| BoundedWord.lower := fst (snd bounds) ; BoundedWord.value := snd v ; BoundedWord.upper := snd (snd bounds) |}))
          end.
   { clear -pf pf'.
     unfold Tuple.map2, Tuple.map in pf; simpl in *.
@@ -242,16 +241,16 @@ Local Ltac args_to_bounded x H :=
       ).
 
 Definition unop_args_to_bounded (x : fe41417_32W) (H : is_bounded (fe41417_32WToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpT).
 Proof. args_to_bounded x H. Defined.
 
 Definition unopWireToFE_args_to_bounded (x : wire_digitsW) (H : wire_digits_is_bounded (wire_digitsWToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpWireToFET).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpWireToFET).
 Proof. args_to_bounded x H. Defined.
 Definition binop_args_to_bounded (x : fe41417_32W * fe41417_32W)
            (H : is_bounded (fe41417_32WToZ (fst x)) = true)
            (H' : is_bounded (fe41417_32WToZ (snd x)) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprBinOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprBinOpT).
 Proof.
   let v := app_tuples (unop_args_to_bounded (fst x) H) (unop_args_to_bounded (snd x) H') in
   exact v.
@@ -328,13 +327,13 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   change interp_base_type with (@Z.interp_base_type) in *;
   rewrite <- Heq; clear Heq;
   destruct Hbounds as [ Hbounds0 [Hbounds1 Hbounds2] ];
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 Word64.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_word64_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 WordW.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_wordW_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
   specialize_by repeat first [ progress intros
                              | reflexivity
                              | assumption
                              | progress destruct_head' base_type
-                             | progress destruct_head' BoundedWord64.BoundedWord
+                             | progress destruct_head' BoundedWordW.BoundedWord
                              | progress destruct_head' and
                              | progress repeat apply conj ];
   specialize (Hbounds_left args H0);
@@ -350,7 +349,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWord64.to_word64' BoundedWord64.boundedWordToWord64 BoundedWord64.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_word64_boundsi' Relations.related'_word64_bounds ZBounds.upper ZBounds.lower Application.remove_all_binders Word64.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe41417_32WToZ ?x = _ /\ _ ]
     => destruct x; destruct_head_hnf' prod
@@ -359,7 +358,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
-  change word64ToZ with Word64.word64ToZ in *;
+  change word64ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
@@ -371,7 +370,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
-  change Word64.word64ToZ with word64ToZ in *;
+  change WordW.wordWToZ with word64ToZ in *;
   repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
 
 
@@ -387,10 +386,10 @@ Ltac rexpr_correct :=
     [ | apply @RelWfMapInterp, wf_ropW ].. ];
   auto with interp_related.
 
-Notation rword_of_Z rexprZ_sig := (MapInterp Word64.of_Z (proj1_sig rexprZ_sig)) (only parsing).
+Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing).
 
 Notation compute_bounds opW bounds
-  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_word64) opW)) bounds)
+  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds)
        (only parsing).
 
 
@@ -407,7 +406,7 @@ Module Export PrettyPrinting.
     := fun t : base_type
        => match t return ZBounds.interp_base_type t -> match t with TZ => bounds_on end with
           | TZ => fun x => match x with
-                           | Some {| ZBounds.lower := l ; ZBounds.upper := u |}
+                           | Some {| Bounds.lower := l ; Bounds.upper := u |}
                              => in_range l u
                            | None
                              => overflow
diff --git a/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v b/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v
index 93a83cf51..3542dc9cf 100644
--- a/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -18,7 +18,7 @@ Lemma ExprBinOp_correct_and_bounded
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded xy Hx Hy in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -31,9 +31,9 @@ Lemma ExprBinOp_correct_and_bounded
           let Hx := let (Hx, Hy) := Hxy in Hx in
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => binop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v
index c616b1a77..7d86a5e95 100644
--- a/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOp_correct_and_bounded
                    (Hx : is_bounded (fe41417_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOp_correct_and_bounded
                    (x := eta_fe41417_32W x)
                    (Hx : is_bounded (fe41417_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v
index 7391e98bf..a008c50bb 100644
--- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (Hx : is_bounded (fe41417_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (x := eta_fe41417_32W x)
                    (Hx : is_bounded (fe41417_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToWire_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v
index 6d991dbb4..700581bad 100644
--- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (Hx : is_bounded (fe41417_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (x := eta_fe41417_32W x)
                    (Hx : is_bounded (fe41417_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToZ_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v
index bb91ea89f..d04d44d32 100644
--- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (x := eta_wire_digitsW x)
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopWireToFE_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF5211_32Bounded.v b/src/SpecificGen/GF5211_32Bounded.v
index 74480a0d1..c879a3b19 100644
--- a/src/SpecificGen/GF5211_32Bounded.v
+++ b/src/SpecificGen/GF5211_32Bounded.v
@@ -78,7 +78,7 @@ Definition postfreezeW : fe5211_32W -> fe5211_32W :=
          (num_limbs := length_fe5211_32)
          modulusW
          ge_modulusW
-         (Interpretations.Word64.neg GF5211_32.int_width)
+         (Interpretations64.WordW.neg GF5211_32.int_width)
       ).
 
 Definition freezeW (f : fe5211_32W) : fe5211_32W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
@@ -117,7 +117,7 @@ Ltac lower_bound_minus_ge_modulus :=
   cbv [ge_modulus Let_In ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne ModularBaseSystemListZOperations.neg];
   repeat break_if; Z.ltb_to_lt; subst; try omega;
     rewrite ?Z.land_0_l; auto;
-    change Interpretations.Word64.word64ToZ with word64ToZ;
+    change Interpretations64.WordW.wordWToZ with word64ToZ;
     etransitivity; try apply Z.land_upper_bound_r; instantiate; try omega;
     apply Z.ones_nonneg; instantiate; vm_compute; discriminate.
 
@@ -136,8 +136,8 @@ Proof.
   destruct_head' and.
   Z.ltb_to_lt.
   cbv [postfreezeW].
-  cbv [conditional_subtract_modulusW Interpretations.Word64.neg].
-  change word64ToZ with Interpretations.Word64.word64ToZ in *.
+  cbv [conditional_subtract_modulusW Interpretations64.WordW.neg].
+  change word64ToZ with Interpretations64.WordW.wordWToZ in *.
   rewrite Hgm.
 
   cbv [modulusW Tuple.map].
@@ -148,12 +148,12 @@ Proof.
 
   split.
   { match goal with
-    |- (_,word64ToZ (_ ^- (Interpretations.Word64.ZToWord64 ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
+    |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  rewrite !Interpretations64.WordW.wordWToZ_sub;
+  rewrite !Interpretations64.WordW.wordWToZ_land;
+  rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
@@ -170,10 +170,10 @@ Proof.
 
 
   unfold_is_bounded.
-  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
-  rewrite !Interpretations.Word64.word64ToZ_sub;
-  rewrite !Interpretations.Word64.word64ToZ_land;
-  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  rewrite !Interpretations64.WordW.wordWToZ_sub;
+  rewrite !Interpretations64.WordW.wordWToZ_land;
+  rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
diff --git a/src/SpecificGen/GF5211_32Reflective.v b/src/SpecificGen/GF5211_32Reflective.v
index 332d5c7e9..415fcad74 100644
--- a/src/SpecificGen/GF5211_32Reflective.v
+++ b/src/SpecificGen/GF5211_32Reflective.v
@@ -10,9 +10,9 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.MapInterp.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.SpecificGen.GF5211_32Reflective.Common.
@@ -50,10 +50,10 @@ Declare Reduction asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe5211_32W curry_unop_fe5211_32W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 Ltac asm_interp
   := cbv beta iota delta
@@ -61,10 +61,10 @@ Ltac asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe5211_32W curry_unop_fe5211_32W curry_unop_wire_digitsW
-            Word64.interp_op Word64.interp_base_type
+            WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 
 
diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v
index a2b9a7c63..ec776afd9 100644
--- a/src/SpecificGen/GF5211_32Reflective/Common.v
+++ b/src/SpecificGen/GF5211_32Reflective/Common.v
@@ -4,9 +4,9 @@ Require Export Crypto.SpecificGen.GF5211_32.
 Require Export Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Interpretations.
-Require Crypto.Reflection.Z.Interpretations.Relations.
-Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Crypto.Reflection.Z.Interpretations64.Relations.
+Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
 Require Import Crypto.Reflection.Z.Reify.
 Require Export Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.InterpWfRel.
@@ -19,7 +19,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
 
-Notation Expr := (Expr base_type Word64.interp_base_type op).
+Notation Expr := (Expr base_type WordW.interp_base_type op).
 
 Local Ltac make_type_from uncurried_op :=
   let T := (type of uncurried_op) in
@@ -45,9 +45,9 @@ Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
-  | (?x :: nil)%list => constr:(Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |})
+  | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |})
   | (?x :: ?xs)%list => let bs := bounds_from_list xs in
-                        constr:((Some {| ZBounds.lower := fst x ; ZBounds.upper := snd x |}, bs))
+                        constr:((Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs))
   end.
 
 Local Ltac make_bounds ls :=
@@ -66,17 +66,16 @@ Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZB
 Proof. make_bounds (Tuple.to_list _ bounds). Defined.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
-  := fun e => curry_binop_fe5211_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_binop_fe5211_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
-  := fun e => curry_unop_fe5211_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe5211_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.word64
-  := fun e => curry_unop_fe5211_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe5211_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.wire_digitsW
-  := fun e => curry_unop_fe5211_32W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe5211_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> SpecificGen.GF5211_32BoundedCommon.wire_digitsW -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
-  := fun e => curry_unop_wire_digitsW (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_wire_digitsW (Interp (@WordW.interp_op) e).
 
 Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
@@ -117,13 +116,13 @@ Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
       let ropZ_sig := ropZ_sigv in
       let ropW := MapInterp (fun _ x => x) ropW' in
-      let ropZ := MapInterp Word64.to_Z ropW' in
-      let ropBounds := MapInterp ZBounds.of_word64 ropW' in
-      let ropBoundedWord64 := MapInterp BoundedWord64.of_word64 ropW' in
+      let ropZ := MapInterp WordW.to_Z ropW' in
+      let ropBounds := MapInterp ZBounds.of_wordW ropW' in
+      let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in
       ropZ = proj1_sig ropZ_sig
-      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Z.interp_op) ropZ)
-      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@ZBounds.interp_op) ropBounds)
-      /\ interp_type_rel_pointwise2 Relations.related_word64 (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Word64.interp_op) ropW))
+      /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ)
+      /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds)
+      /\ interp_type_rel_pointwise2 Relations.related_wordW (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@WordW.interp_op) ropW))
        (only parsing).
 
 Ltac app_tuples x y :=
@@ -138,7 +137,7 @@ Local Arguments Tuple.map2 : simpl never.
 Local Arguments Tuple.map : simpl never.
 
 Fixpoint args_to_bounded_helperT {n}
-         (v : Tuple.tuple' Word64.word64 n)
+         (v : Tuple.tuple' WordW.wordW n)
          (bounds : Tuple.tuple' (Z * Z) n)
          (pf : List.fold_right
                  andb true
@@ -149,7 +148,7 @@ Fixpoint args_to_bounded_helperT {n}
                        (fun bounds v =>
                           let '(lower, upper) := bounds in ((lower <=? v)%Z && (v <=? upper)%Z)%bool)
                        bounds
-                       (Tuple.map (n:=S n) Word64.word64ToZ v))) = true)
+                       (Tuple.map (n:=S n) WordW.wordWToZ v))) = true)
          (res : Type)
          {struct n}
   : Type.
@@ -161,9 +160,9 @@ Proof.
                                       (Tuple.map2 (n:=S n) _ bounds (Tuple.map (n:=S n) _ v))) = true
                              -> Type)
           with
-          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat Word64.bit_width)%Z, res
+          | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat WordW.bit_width)%Z, res
           | S n' => fun v' bounds' pf0 => let t := _ in
-                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
+                                        forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat WordW.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res
           end v bounds pf).
   { clear -pf0.
     abstract (
@@ -178,15 +177,15 @@ Defined.
 
 Fixpoint args_to_bounded_helper {n} res
          {struct n}
-  : forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
+  : forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res.
 Proof.
-  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
-         | 0 => fun v bounds pf f pf' => f {| BoundedWord64.lower := fst bounds ; BoundedWord64.value := v ; BoundedWord64.upper := snd bounds |}
+  refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWordW.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with
+         | 0 => fun v bounds pf f pf' => f {| BoundedWord.lower := fst bounds ; BoundedWord.value := v ; BoundedWord.upper := snd bounds |}
          | S n'
            => fun v bounds pf f pf'
               => @args_to_bounded_helper
                    n' res (fst v) (fst bounds) _
-                   (fun ts => f (ts, {| BoundedWord64.lower := fst (snd bounds) ; BoundedWord64.value := snd v ; BoundedWord64.upper := snd (snd bounds) |}))
+                   (fun ts => f (ts, {| BoundedWord.lower := fst (snd bounds) ; BoundedWord.value := snd v ; BoundedWord.upper := snd (snd bounds) |}))
          end.
   { clear -pf pf'.
     unfold Tuple.map2, Tuple.map in pf; simpl in *.
@@ -242,16 +241,16 @@ Local Ltac args_to_bounded x H :=
       ).
 
 Definition unop_args_to_bounded (x : fe5211_32W) (H : is_bounded (fe5211_32WToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpT).
 Proof. args_to_bounded x H. Defined.
 
 Definition unopWireToFE_args_to_bounded (x : wire_digitsW) (H : wire_digits_is_bounded (wire_digitsWToZ x) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpWireToFET).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprUnOpWireToFET).
 Proof. args_to_bounded x H. Defined.
 Definition binop_args_to_bounded (x : fe5211_32W * fe5211_32W)
            (H : is_bounded (fe5211_32WToZ (fst x)) = true)
            (H' : is_bounded (fe5211_32WToZ (snd x)) = true)
-  : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprBinOpT).
+  : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for ExprBinOpT).
 Proof.
   let v := app_tuples (unop_args_to_bounded (fst x) H) (unop_args_to_bounded (snd x) H') in
   exact v.
@@ -328,13 +327,13 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   change interp_base_type with (@Z.interp_base_type) in *;
   rewrite <- Heq; clear Heq;
   destruct Hbounds as [ Hbounds0 [Hbounds1 Hbounds2] ];
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 Word64.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
-  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_word64_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj_from_option2 WordW.to_Z pf Hbounds2 Hbounds0) as Hbounds_left;
+  pose proof (fun pf => Relations.uncurry_interp_type_rel_pointwise2_proj1_from_option2 Relations.related_wordW_boundsi' pf Hbounds1 Hbounds2) as Hbounds_right;
   specialize_by repeat first [ progress intros
                              | reflexivity
                              | assumption
                              | progress destruct_head' base_type
-                             | progress destruct_head' BoundedWord64.BoundedWord
+                             | progress destruct_head' BoundedWordW.BoundedWord
                              | progress destruct_head' and
                              | progress repeat apply conj ];
   specialize (Hbounds_left args H0);
@@ -350,7 +349,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWord64.to_word64' BoundedWord64.boundedWordToWord64 BoundedWord64.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_word64_boundsi' Relations.related'_word64_bounds ZBounds.upper ZBounds.lower Application.remove_all_binders Word64.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe5211_32WToZ ?x = _ /\ _ ]
     => destruct x; destruct_head_hnf' prod
@@ -359,7 +358,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
-  change word64ToZ with Word64.word64ToZ in *;
+  change word64ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
   cbv [fst snd
@@ -371,7 +370,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
-  change Word64.word64ToZ with word64ToZ in *;
+  change WordW.wordWToZ with word64ToZ in *;
   repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
 
 
@@ -387,10 +386,10 @@ Ltac rexpr_correct :=
     [ | apply @RelWfMapInterp, wf_ropW ].. ];
   auto with interp_related.
 
-Notation rword_of_Z rexprZ_sig := (MapInterp Word64.of_Z (proj1_sig rexprZ_sig)) (only parsing).
+Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing).
 
 Notation compute_bounds opW bounds
-  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_word64) opW)) bounds)
+  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds)
        (only parsing).
 
 
@@ -407,7 +406,7 @@ Module Export PrettyPrinting.
     := fun t : base_type
        => match t return ZBounds.interp_base_type t -> match t with TZ => bounds_on end with
           | TZ => fun x => match x with
-                           | Some {| ZBounds.lower := l ; ZBounds.upper := u |}
+                           | Some {| Bounds.lower := l ; Bounds.upper := u |}
                              => in_range l u
                            | None
                              => overflow
diff --git a/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v b/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v
index a6a6e0f28..ccaefeb38 100644
--- a/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -18,7 +18,7 @@ Lemma ExprBinOp_correct_and_bounded
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded xy Hx Hy in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -31,9 +31,9 @@ Lemma ExprBinOp_correct_and_bounded
           let Hx := let (Hx, Hy) := Hxy in Hx in
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => binop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v
index 9a1d5bdef..4c8c024ef 100644
--- a/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOp_correct_and_bounded
                    (Hx : is_bounded (fe5211_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOp_correct_and_bounded
                    (x := eta_fe5211_32W x)
                    (Hx : is_bounded (fe5211_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unop_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v
index 14f3d3dd7..4abf5e85f 100644
--- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (Hx : is_bounded (fe5211_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (x := eta_fe5211_32W x)
                    (Hx : is_bounded (fe5211_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToWire_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v
index ab44167a6..821f6529c 100644
--- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (Hx : is_bounded (fe5211_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (x := eta_fe5211_32W x)
                    (Hx : is_bounded (fe5211_32WToZ x) = true),
           let args := unop_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopFEToZ_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v
index 9948ea3a0..9284bf40f 100644
--- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v
@@ -1,6 +1,6 @@
 Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
-Require Import Crypto.Reflection.Z.Interpretations.
+Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapInterp.
@@ -15,7 +15,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -25,9 +25,9 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (x := eta_wire_digitsW x)
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx in
-          let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in
+          let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
           with
           | Some bounds => unopWireToFE_bounds_good bounds = true
           | None => False
diff --git a/src/SpecificGen/copy_bounds.sh b/src/SpecificGen/copy_bounds.sh
index ec7821d19..0c73ac268 100755
--- a/src/SpecificGen/copy_bounds.sh
+++ b/src/SpecificGen/copy_bounds.sh
@@ -6,6 +6,10 @@ cd "$DIR"
 
 FILENAME="$1"
 V_FILE_STEM="${FILENAME%.*}"
+BIT_WIDTH=64
+case "$V_FILE_STEM" in
+    *_64) BIT_WIDTH=128;;
+esac
 
 if [ -z "$V_FILE_STEM" ]; then
     echo "USAGE: $0 JSON_FILE"
@@ -17,5 +21,5 @@ for ORIG in $(git ls-files "../Specific/**GF25519*.v" | grep -v "../Specific/GF2
     echo "$NEW"
     NEW_DIR="$(dirname "$NEW")"
     mkdir -p "$NEW_DIR" || exit $?
-    cat "$ORIG" | sed s'/Specific/SpecificGen/g' | sed s"/25519/${V_FILE_STEM}/g" > "$NEW" || exit $?
+    cat "$ORIG" | sed s"/64/${BIT_WIDTH}/g" | sed s'/Specific/SpecificGen/g' | sed s"/25519/${V_FILE_STEM}/g" > "$NEW" || exit $?
 done