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.

8 files changed, 77 insertions, 78 deletions

diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index 778c3b3ed..3936d70c2 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -78,7 +78,7 @@ Definition postfreezeW : fe25519W -> fe25519W :=
          (num_limbs := length_fe25519)
          modulusW
          ge_modulusW
-         (Interpretations.Word64.neg GF25519.int_width)
+         (Interpretations64.WordW.neg GF25519.int_width)
       ).
 
 Definition freezeW (f : fe25519W) : fe25519W := 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/Specific/GF25519Reflective.v b/src/Specific/GF25519Reflective.v
index 5e306d61d..a7ca684fb 100644
--- a/src/Specific/GF25519Reflective.v
+++ b/src/Specific/GF25519Reflective.v
@@ -10,9 +10,9 @@ Require Import Crypto.Specific.GF25519BoundedCommon.
 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.Specific.GF25519Reflective.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_fe25519W curry_unop_fe25519W 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_fe25519W curry_unop_fe25519W 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/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index 8b500b42b..c6750fa3c 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/Common.v
@@ -4,9 +4,9 @@ Require Export Crypto.Specific.GF25519.
 Require Export Crypto.Specific.GF25519BoundedCommon.
 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 -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := fun e => curry_binop_fe25519W (Interp (@Word64.interp_op) e).
+  := fun e => curry_binop_fe25519W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe25519W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64
-  := fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe25519W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.wire_digitsW
-  := fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e).
+  := fun e => curry_unop_fe25519W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> Specific.GF25519BoundedCommon.wire_digitsW -> Specific.GF25519BoundedCommon.fe25519W
-  := 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 : fe25519W) (H : is_bounded (fe25519WToZ 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 : fe25519W * fe25519W)
            (H : is_bounded (fe25519WToZ (fst x)) = true)
            (H' : is_bounded (fe25519WToZ (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
   | [ |- fe25519WToZ ?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/Specific/GF25519Reflective/CommonBinOp.v b/src/Specific/GF25519Reflective/CommonBinOp.v
index 32dae16e6..b325a56eb 100644
--- a/src/Specific/GF25519Reflective/CommonBinOp.v
+++ b/src/Specific/GF25519Reflective/CommonBinOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.Specific.GF25519Reflective.Common.
 Require Import Crypto.Specific.GF25519BoundedCommon.
-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/Specific/GF25519Reflective/CommonUnOp.v b/src/Specific/GF25519Reflective/CommonUnOp.v
index eac381b50..10390798b 100644
--- a/src/Specific/GF25519Reflective/CommonUnOp.v
+++ b/src/Specific/GF25519Reflective/CommonUnOp.v
@@ -1,6 +1,6 @@
 Require Export Crypto.Specific.GF25519Reflective.Common.
 Require Import Crypto.Specific.GF25519BoundedCommon.
-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 (fe25519WToZ 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_fe25519W x)
                    (Hx : is_bounded (fe25519WToZ 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/Specific/GF25519Reflective/CommonUnOpFEToWire.v b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
index 2fa1d2ee3..2531e6184 100644
--- a/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
+++ b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
@@ -1,6 +1,6 @@
 Require Export Crypto.Specific.GF25519Reflective.Common.
 Require Import Crypto.Specific.GF25519BoundedCommon.
-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 (fe25519WToZ 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_fe25519W x)
                    (Hx : is_bounded (fe25519WToZ 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/Specific/GF25519Reflective/CommonUnOpFEToZ.v b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
index 7528cfc2d..06d53a1e1 100644
--- a/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
+++ b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
@@ -1,6 +1,6 @@
 Require Export Crypto.Specific.GF25519Reflective.Common.
 Require Import Crypto.Specific.GF25519BoundedCommon.
-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 (fe25519WToZ 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_fe25519W x)
                    (Hx : is_bounded (fe25519WToZ 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/Specific/GF25519Reflective/CommonUnOpWireToFE.v b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
index d61807413..d0c46d1ed 100644
--- a/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
+++ b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
@@ -1,6 +1,6 @@
 Require Export Crypto.Specific.GF25519Reflective.Common.
 Require Import Crypto.Specific.GF25519BoundedCommon.
-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