Switch to reflective bounded word in Ed25519

(cc @andres-erbsen)

8 files changed, 77 insertions, 675 deletions

diff --git a/_CoqProject b/_CoqProject
index d442245e7..0489e1b0f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -12,7 +12,6 @@ src/Assembly/Compile.v
 src/Assembly/Conversions.v
 src/Assembly/Evaluables.v
 src/Assembly/GF25519.v
-src/Assembly/GF25519BoundedInstantiation.v
 src/Assembly/HL.v
 src/Assembly/LL.v
 src/Assembly/PhoasCommon.v
@@ -136,7 +135,6 @@ src/Specific/GF1305.v
 src/Specific/GF25519.v
 src/Specific/GF25519Bounded.v
 src/Specific/GF25519BoundedCommon.v
-src/Specific/GF25519BoundedCommonWord.v
 src/Specific/GF25519Reflective.v
 src/Specific/SC25519.v
 src/Specific/FancyMachine256/Barrett.v
diff --git a/src/Assembly/GF25519BoundedInstantiation.v b/src/Assembly/GF25519BoundedInstantiation.v
deleted file mode 100644
index 1c6897343..000000000
--- a/src/Assembly/GF25519BoundedInstantiation.v
+++ /dev/null
@@ -1,139 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Assembly.PhoasCommon.
-Require Import Crypto.Assembly.QhasmCommon.
-Require Import Crypto.Assembly.Compile.
-Require Import Crypto.Assembly.LL.
-Require Import Crypto.Assembly.GF25519.
-Require Import Crypto.Specific.GF25519.
-Require Import Crypto.Specific.GF25519BoundedCommonWord.
-Require Import Crypto.Util.Tactics.
-Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.Tuple.
-
-(* Totally fine to edit these definitions; DO NOT change the type signatures at all *)
-Section Operations.
-  Import Assembly.GF25519.GF25519.
-  Definition wfe: Type := @interp_type (word bits) FE.
-
-  Definition ExprBinOp : Type := GF25519.Binary.
-  Definition ExprUnOp : Type := GF25519.Unary.
-  Axiom ExprUnOpFEToZ : Type.
-  Axiom ExprUnOpWireToFE : Type.
-  Axiom ExprUnOpFEToWire : Type.
-
-  Local Existing Instance WordEvaluable.
-
-  Definition interp_bexpr' (op: ExprBinOp) (x y: tuple (word bits) 10): tuple (word bits) 10 :=
-    let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in
-    let '(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9) := y in
-    op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9.
-
-  Definition interp_uexpr' (op: ExprUnOp) (x: tuple (word bits) 10): tuple (word bits) 10 :=
-    let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in
-    op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
-
-  Definition radd : ExprBinOp := GF25519.add.
-  Definition rsub : ExprBinOp := GF25519.sub.
-  Definition rmul : ExprBinOp := GF25519.mul.
-  Definition ropp : ExprUnOp := GF25519.opp.
-End Operations.
-
-Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
-  := interp_bexpr'.
-Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
-  := interp_uexpr'.
-Axiom interp_uexpr_FEToZ : ExprUnOpFEToZ -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.word64.
-Axiom interp_uexpr_FEToWire : ExprUnOpFEToWire -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.wire_digitsW.
-Axiom interp_uexpr_WireToFE : ExprUnOpWireToFE -> Specific.GF25519BoundedCommonWord.wire_digitsW -> Specific.GF25519BoundedCommonWord.fe25519W.
-Axiom rfreeze : ExprUnOp.
-Axiom rge_modulus : ExprUnOpFEToZ.
-Axiom rpack : ExprUnOpFEToWire.
-Axiom runpack : ExprUnOpWireToFE.
-
-Declare Reduction asm_interp
-  := cbv [id
-            interp_bexpr interp_uexpr interp_bexpr' interp_uexpr'
-            radd rsub rmul ropp (*rfreeze rge_modulus rpack runpack*)
-            GF25519.GF25519.add GF25519.GF25519.sub GF25519.GF25519.mul GF25519.GF25519.opp (* GF25519.GF25519.freeze *)
-            GF25519.GF25519.bits GF25519.GF25519.FE
-            QhasmCommon.liftN QhasmCommon.NArgMap Compile.CompileHL.compile LL.LL.under_lets LL.LL.interp LL.LL.interp_arg LL.LL.match_arg_Prod Conversions.LLConversions.convertExpr Conversions.LLConversions.convertArg Conversions.LLConversions.convertVar PhoasCommon.type_rect PhoasCommon.type_rec PhoasCommon.type_ind PhoasCommon.interp_binop LL.LL.uninterp_arg
-            Evaluables.ezero Evaluables.toT Evaluables.fromT Evaluables.eadd Evaluables.esub Evaluables.emul Evaluables.eshiftr Evaluables.eand Evaluables.eltb Evaluables.eeqb
-            Evaluables.WordEvaluable Evaluables.ZEvaluable].
-
-Definition interp_radd : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
-  := Eval asm_interp in interp_bexpr radd.
-(*Print interp_radd.*)
-Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl.
-Definition interp_rsub : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
-  := Eval asm_interp in interp_bexpr rsub.
-(*Print interp_rsub.*)
-Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl.
-Definition interp_rmul : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
-  := Eval asm_interp in interp_bexpr rmul.
-(*Print interp_rmul.*)
-Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl.
-Definition interp_ropp : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
-  := Eval asm_interp in interp_uexpr ropp.
-(*Print interp_ropp.*)
-Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl.
-Definition interp_rfreeze : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
-  := Eval asm_interp in interp_uexpr rfreeze.
-(*Print interp_rfreeze.*)
-Definition interp_rfreeze_correct : interp_rfreeze = interp_uexpr rfreeze := eq_refl.
-
-Definition interp_rge_modulus : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.word64
-  := Eval asm_interp in interp_uexpr_FEToZ rge_modulus.
-Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl.
-
-Definition interp_rpack : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.wire_digitsW
-  := Eval asm_interp in interp_uexpr_FEToWire rpack.
-Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl.
-
-Definition interp_runpack : Specific.GF25519BoundedCommonWord.wire_digitsW -> Specific.GF25519BoundedCommonWord.fe25519W
-  := Eval asm_interp in interp_uexpr_WireToFE runpack.
-Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl.
-
-Local Notation binop_correct_and_bounded rop op
-  := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
-Local Notation unop_correct_and_bounded rop op
-  := (iunop_correct_and_bounded (interp_uexpr rop) op) (only parsing).
-Local Notation unop_FEToZ_correct rop op
-  := (iunop_FEToZ_correct (interp_uexpr_FEToZ rop) op) (only parsing).
-Local Notation unop_FEToWire_correct_and_bounded rop op
-  := (iunop_FEToWire_correct_and_bounded (interp_uexpr_FEToWire rop) op) (only parsing).
-Local Notation unop_WireToFE_correct_and_bounded rop op
-  := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing).
-
-Local Ltac start_correct_and_bounded_t op op_expr lem :=
-  intros; hnf in *; destruct_head' prod; simpl in * |- ;
-  repeat match goal with H : is_bounded _ = true |- _ => unfold_is_bounded_in H end;
-  repeat match goal with H : wire_digits_is_bounded _ = true |- _ => unfold_is_bounded_in H end;
-  change op with op_expr;
-  rewrite <- lem.
-
-Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add.
-Proof.
-  intros; hnf in *; destruct_head' prod; simpl in * |- .
-  repeat match goal with H : is_bounded _ = true |- _ => unfold_is_bounded_in H end.
-Admitted.
-Lemma rsub_correct_and_bounded : binop_correct_and_bounded rsub carry_sub.
-Proof.
-Admitted.
-Lemma rmul_correct_and_bounded : binop_correct_and_bounded rmul mul.
-Proof.
-Admitted.
-Lemma ropp_correct_and_bounded : unop_correct_and_bounded ropp carry_opp.
-Proof.
-Admitted.
-Lemma rfreeze_correct_and_bounded : unop_correct_and_bounded rfreeze freeze.
-Proof.
-Admitted.
-Lemma rge_modulus_correct_and_bounded : unop_FEToZ_correct rge_modulus ge_modulus.
-Proof.
-Admitted.
-Lemma rpack_correct_and_bounded : unop_FEToWire_correct_and_bounded rpack pack.
-Proof.
-Admitted.
-Lemma runpack_correct_and_bounded : unop_WireToFE_correct_and_bounded runpack unpack.
-Proof.
-Admitted.
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 629a2e576..5657d8503 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -632,21 +632,19 @@ Proof.
          GF25519BoundedCommon.proj1_fe25519W
          PseudoMersenneBaseParams.limb_widths
          GF25519.params25519 length
-         Tuple.to_list Tuple.to_list'] in *.
-  (* TODO (jgross) : this should probably be Ltac'ed *)
-  assert (n = 0 \/ n = 1 \/ n = 2 \/ n = 3 \/ n = 4 \/ n = 5 \/ n = 6 \/ n = 7 \/ n = 8 \/ n = 9) by omega.
-  repeat match goal with H : _ \/ _ |- _ => destruct H end;
-    subst; cbv [nth_default nth_error pred];
-      match goal with |- appcontext [if ?x then _ else _] =>
-                      destruct x end; try congruence;
-        cbv - [GF25519BoundedCommon.proj_word Z.le Z.lt] in *;
-  match goal with
-  |- appcontext [GF25519BoundedCommon.proj_word ?b] =>
-  let A := fresh "H" in
-  pose proof (@GF25519BoundedCommon.word_bounded _ _ b) as A;
-    rewrite Bool.andb_true_iff in A; destruct A end;
-  rewrite !Z.leb_le in *;
-  omega.
+         Tuple.to_list Tuple.to_list' nth_default] in *.
+  repeat match goal with
+         | [ |- appcontext[nth_error _ ?n] ]
+           => is_var n; destruct n; simpl @nth_error; cbv beta iota
+         end;
+    simpl in *; unfold Z.pow_pos; simpl; try omega;
+      match goal with
+        |- appcontext [GF25519BoundedCommon.proj_word ?b] =>
+        let A := fresh "H" in
+        pose proof (@GF25519BoundedCommon.word_bounded _ _ b) as A;
+          rewrite Bool.andb_true_iff in A; destruct A end;
+      rewrite !Z.leb_le in *;
+      omega.
 Qed.
 
 Lemma feSign_correct : forall x,
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index d9194610b..b0a3f512a 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -7,7 +7,7 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
 Require Import Crypto.Specific.GF25519.
 Require Import Crypto.Specific.GF25519BoundedCommon.
-(*Require Import Crypto.Assembly.GF25519BoundedInstantiation.*)
+Require Import Crypto.Specific.GF25519Reflective.
 Require Import Bedrock.Word Crypto.Util.WordUtil.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
 Require Import Crypto.Tactics.VerdiTactics.
@@ -45,11 +45,15 @@ Local Ltac define_unop_WireToFE f opW blem :=
   abstract bounded_wire_digits_t opW blem.
 
 Local Opaque Let_In.
-(*Local Arguments interp_radd / _ _.
+Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb.
+Local Arguments interp_radd / _ _.
 Local Arguments interp_rsub / _ _.
 Local Arguments interp_rmul / _ _.
 Local Arguments interp_ropp / _.
 Local Arguments interp_rfreeze / _.
+Local Arguments interp_rge_modulus / _.
+Local Arguments interp_rpack / _.
+Local Arguments interp_runpack / _.
 Definition addW (f g : fe25519W) : fe25519W := Eval simpl in interp_radd f g.
 Definition subW (f g : fe25519W) : fe25519W := Eval simpl in interp_rsub f g.
 Definition mulW (f g : fe25519W) : fe25519W := Eval simpl in interp_rmul f g.
@@ -57,15 +61,7 @@ Definition oppW (f : fe25519W) : fe25519W := Eval simpl in interp_ropp f.
 Definition freezeW (f : fe25519W) : fe25519W := Eval simpl in interp_rfreeze f.
 Definition ge_modulusW (f : fe25519W) : word64 := Eval simpl in interp_rge_modulus f.
 Definition packW (f : fe25519W) : wire_digitsW := Eval simpl in interp_rpack f.
-Definition unpackW (f : wire_digitsW) : fe25519W := Eval simpl in interp_runpack f.*)
-Definition addW (f g : fe25519W) : fe25519W := Eval cbv beta delta [carry_add] in carry_add f g.
-Definition subW (f g : fe25519W) : fe25519W := Eval cbv beta delta [carry_sub] in carry_sub f g.
-Definition mulW (f g : fe25519W) : fe25519W := Eval cbv beta delta [mul] in mul f g.
-Definition oppW (f : fe25519W) : fe25519W := Eval cbv beta delta [carry_opp] in carry_opp f.
-Definition freezeW (f : fe25519W) : fe25519W := Eval cbv beta delta [freeze] in freeze f.
-Definition ge_modulusW (f : fe25519W) : word64 := Eval cbv beta delta [ge_modulus] in ge_modulus f.
-Definition packW (f : fe25519W) : wire_digitsW := Eval cbv beta delta [pack] in pack f.
-Definition unpackW (f : wire_digitsW) : fe25519W := Eval cbv beta delta [unpack] in unpack f.
+Definition unpackW (f : wire_digitsW) : fe25519W := Eval simpl in interp_runpack f.
 
 Local Transparent Let_In.
 Definition powW (f : fe25519W) chain := fold_chain_opt (proj1_fe25519W one) mulW chain [f].
@@ -78,21 +74,21 @@ Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb :=
   intros; apply rop_cb; assumption.
 
 Lemma addW_correct_and_bounded : ibinop_correct_and_bounded addW carry_add.
-Proof. (*port_correct_and_bounded interp_radd_correct addW interp_radd radd_correct_and_bounded. Qed.*) Admitted.
+Proof. port_correct_and_bounded interp_radd_correct addW interp_radd radd_correct_and_bounded. Qed.
 Lemma subW_correct_and_bounded : ibinop_correct_and_bounded subW carry_sub.
-Proof. (*port_correct_and_bounded interp_rsub_correct subW interp_rsub rsub_correct_and_bounded. Qed.*) Admitted.
+Proof. port_correct_and_bounded interp_rsub_correct subW interp_rsub rsub_correct_and_bounded. Qed.
 Lemma mulW_correct_and_bounded : ibinop_correct_and_bounded mulW mul.
-Proof. (*port_correct_and_bounded interp_rmul_correct mulW interp_rmul rmul_correct_and_bounded. Qed.*) Admitted.
+Proof. port_correct_and_bounded interp_rmul_correct mulW interp_rmul rmul_correct_and_bounded. Qed.
 Lemma oppW_correct_and_bounded : iunop_correct_and_bounded oppW carry_opp.
-Proof. (*port_correct_and_bounded interp_ropp_correct oppW interp_ropp ropp_correct_and_bounded. Qed.*) Admitted.
+Proof. port_correct_and_bounded interp_ropp_correct oppW interp_ropp ropp_correct_and_bounded. Qed.
 Lemma freezeW_correct_and_bounded : iunop_correct_and_bounded freezeW freeze.
-Proof. (*port_correct_and_bounded interp_rfreeze_correct freezeW interp_rfreeze rfreeze_correct_and_bounded. Qed.*) Admitted.
+Proof. port_correct_and_bounded interp_rfreeze_correct freezeW interp_rfreeze rfreeze_correct_and_bounded. Qed.
 Lemma ge_modulusW_correct : iunop_FEToZ_correct ge_modulusW ge_modulus.
-Proof. (*port_correct_and_bounded interp_rge_modulus_correct ge_modulusW interp_rge_modulus rge_modulus_correct_and_bounded. Qed.*) Admitted.
+Proof. port_correct_and_bounded interp_rge_modulus_correct ge_modulusW interp_rge_modulus rge_modulus_correct_and_bounded. Qed.
 Lemma packW_correct_and_bounded : iunop_FEToWire_correct_and_bounded packW pack.
-Proof. (*port_correct_and_bounded interp_rpack_correct packW interp_rpack rpack_correct_and_bounded. Qed.*) Admitted.
+Proof. port_correct_and_bounded interp_rpack_correct packW interp_rpack rpack_correct_and_bounded. Qed.
 Lemma unpackW_correct_and_bounded : iunop_WireToFE_correct_and_bounded unpackW unpack.
-Proof. (*port_correct_and_bounded interp_runpack_correct unpackW interp_runpack runpack_correct_and_bounded. Qed.*) Admitted.
+Proof. port_correct_and_bounded interp_runpack_correct unpackW interp_runpack runpack_correct_and_bounded. Qed.
 
 Lemma powW_correct_and_bounded chain : iunop_correct_and_bounded (fun x => powW x chain) (fun x => pow x chain).
 Proof.
@@ -100,8 +96,7 @@ Proof.
   intro x; intros; apply (fold_chain_opt_gen fe25519WToZ is_bounded [x]).
   { reflexivity. }
   { reflexivity. }
-  { intros; progress rewrite <- ?mul_correct,
-            <- ?(fun X Y => proj1 (mulW_correct_and_bounded _ _ X Y)) by assumption.
+  { intros; progress rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded _ _ X Y)) by assumption.
     apply mulW_correct_and_bounded; assumption. }
   { intros; rewrite (fun X Y => proj1 (mulW_correct_and_bounded _ _ X Y)) by assumption; reflexivity. }
   { intros [|?]; autorewrite with simpl_nth_default;
@@ -204,7 +199,8 @@ Proof.
       apply Proper_Let_In_nd_changebody_eq; intros.
       set_evars.
       change sqrt_m1 with (fe25519WToZ sqrt_m1W).
-      rewrite <- !(fun X Y => proj1 (mulW_correct_and_bounded _ _ X Y)), <- eqbW_correct, (pull_bool_if fe25519WToZ)
+      rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded a a X Y)),
+      <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe25519WToZ)
         by repeat match goal with
                   | _ => progress subst
                   | [ |- is_bounded (fe25519WToZ ?op) = true ]
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v
index 900b2d564..29bc1af5d 100644
--- a/src/Specific/GF25519BoundedCommon.v
+++ b/src/Specific/GF25519BoundedCommon.v
@@ -21,14 +21,14 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.
 Local Open Scope Z.
 
 (* BEGIN aliases for word extraction *)
-Definition word64 := Z.
+Definition word64 := Word.word 64.
 Coercion word64ToZ (x : word64) : Z
-  := x.
-Coercion ZToWord64 (x : Z) : word64 := x.
-Definition w64eqb (x y : word64) := Z.eqb x y.
+  := Z.of_N (wordToN x).
+Coercion ZToWord64 (x : Z) : word64 := NToWord _ (Z.to_N x).
+Definition w64eqb (x y : word64) := weqb x y.
 
 Lemma word64eqb_Zeqb x y : (word64ToZ x =? word64ToZ y)%Z = w64eqb x y.
-Proof. reflexivity. Qed.
+Proof. apply wordeqb_Zeqb. Qed.
 
 Arguments word64 : simpl never.
 Global Opaque word64.
@@ -468,12 +468,28 @@ Definition decode (x : fe25519) : F modulus
 
 Lemma proj1_fe25519_encode x
   : proj1_fe25519 (encode x) = ModularBaseSystem.encode x.
-Proof. reflexivity. Qed.
+Proof.
+  cbv [encode].
+  generalize (encode_bounded x); generalize (ModularBaseSystem.encode x).
+  intros y pf; intros; hnf in y; destruct_head_hnf' prod.
+  cbv [proj1_fe25519 exist_fe25519 proj1_fe25519W Build_bounded_word Build_bounded_word' fe25519WToZ proj_word].
+  unfold_is_bounded_in pf.
+  destruct_head' and.
+  Z.ltb_to_lt.
+  rewrite ?ZToWord64ToZ by (rewrite unfold_Pow2_64; cbv [Pow2_64]; omega).
+  reflexivity.
+Qed.
 
 Lemma decode_exist_fe25519 x pf
   : decode (exist_fe25519 x pf) = ModularBaseSystem.decode x.
 Proof.
-  hnf in x; destruct_head' prod; reflexivity.
+  hnf in x; destruct_head' prod.
+  cbv [decode proj1_fe25519 exist_fe25519 proj1_fe25519W Build_bounded_word Build_bounded_word' fe25519WToZ proj_word].
+  unfold_is_bounded_in pf.
+  destruct_head' and.
+  Z.ltb_to_lt.
+  rewrite ?ZToWord64ToZ by (rewrite unfold_Pow2_64; cbv [Pow2_64]; omega).
+  reflexivity.
 Qed.
 
 Definition div (f g : fe25519) : fe25519
diff --git a/src/Specific/GF25519BoundedCommonWord.v b/src/Specific/GF25519BoundedCommonWord.v
deleted file mode 100644
index 40720ddaa..000000000
--- a/src/Specific/GF25519BoundedCommonWord.v
+++ /dev/null
@@ -1,473 +0,0 @@
-Require Import Crypto.BaseSystem.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
-Require Import Crypto.ModularArithmetic.ModularBaseSystem.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
-Require Import Crypto.Specific.GF25519.
-Require Import Bedrock.Word Crypto.Util.WordUtil.
-Require Import Coq.Lists.List Crypto.Util.ListUtil.
-Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.Util.ZUtil.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.Tactics.
-Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.Decidable.
-Require Import Crypto.Algebra.
-Import ListNotations.
-Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
-Local Open Scope Z.
-
-(* BEGIN aliases for word extraction *)
-Definition word64 := Word.word 64.
-Coercion word64ToZ (x : word64) : Z
-  := Z.of_N (wordToN x).
-Coercion ZToWord64 (x : Z) : word64 := NToWord _ (Z.to_N x).
-Definition w64eqb (x y : word64) := weqb x y.
-
-Lemma word64eqb_Zeqb x y : (word64ToZ x =? word64ToZ y)%Z = w64eqb x y.
-Proof. apply wordeqb_Zeqb. Qed.
-
-(* END aliases for word extraction *)
-
-Local Arguments Z.pow_pos !_ !_ / .
-Lemma ZToWord64ToZ x : 0 <= x < 2^64 -> word64ToZ (ZToWord64 x) = x.
-Proof.
-  intros; unfold word64ToZ, ZToWord64.
-  rewrite ?wordToN_NToWord_idempotent, ?N2Z.id, ?Z2N.id
-    by (omega || apply N2Z.inj_lt; rewrite ?N2Z.id, ?Z2N.id by omega; simpl in *; omega).
-  reflexivity.
-Qed.
-
-(* BEGIN precomputation. *)
-Local Notation b_of exp := (0, 2^exp + 2^(exp-3))%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
-Record bounded_word (lower upper : Z) :=
-  Build_bounded_word'
-    { proj_word :> word64;
-      word_bounded : andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true }.
-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)
-  : bounded_word lower upper
-  := Build_bounded_word'
-       proj_word
-       (match andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z as b return b = true -> b = true with
-        | true => fun _ => eq_refl
-        | false => fun x => x
-        end word_bounded).
-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).
-Lemma word_to_unbounded_helper {x e : nat} : (x < pow2 e)%nat -> (Z.of_nat e <= 64)%Z -> ((0 <=? word64ToZ (ZToWord64 (Z.of_nat x))) && (word64ToZ (ZToWord64 (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^64) by auto with zarith.
-  rewrite !ZToWord64ToZ by omega.
-  match goal with
-  | [ |- context[andb ?x ?y] ]
-    => destruct x eqn:?, y eqn:?; try reflexivity; Z.ltb_to_lt
-  end;
-    intros; omega.
-Qed.
-Definition word_to_unbounded_word {sz} (x : word sz) : (Z.of_nat sz <=? 64)%Z = true -> unbounded_word (Z.of_nat sz).
-Proof.
-  refine (fun pf => Build_bounded_word (Z.of_N (wordToN x)) _).
-  abstract (rewrite wordToN_nat, nat_N_Z; Z.ltb_to_lt; apply (word_to_unbounded_helper (wordToNat_bound x)); simpl; omega).
-Defined.
-Definition word32_to_unbounded_word (x : word 32) : unbounded_word 32.
-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.
-Definition bounds : list (Z * Z)
-  := Eval compute in
-      [b_of 25; b_of 26; b_of 25; b_of 26; b_of 25; b_of 26; b_of 25; b_of 26; b_of 25; b_of 26].
-Definition wire_digit_bounds : list (Z * Z)
-  := Eval compute in
-      List.repeat (0, 2^32-1)%Z 7 ++ ((0,2^31-1)%Z :: nil).
-
-Definition fe25519W := Eval cbv -[word64] in (tuple word64 (length limb_widths)).
-Definition wire_digitsW := Eval cbv -[word64] in (tuple word64 8).
-Definition fe25519WToZ (x : fe25519W) : Specific.GF25519.fe25519
-  := let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in
-     (x0 : Z, x1 : Z, x2 : Z, x3 : Z, x4 : Z, x5 : Z, x6 : Z, x7 : Z, x8 : Z, x9 : Z).
-Definition fe25519ZToW (x : Specific.GF25519.fe25519) : fe25519W
-  := let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in
-     (x0 : word64, x1 : word64, x2 : word64, x3 : word64, x4 : word64, x5 : word64, x6 : word64, x7 : word64, x8 : word64, x9 : word64).
-Definition wire_digitsWToZ (x : wire_digitsW) : Specific.GF25519.wire_digits
-  := let '(x0, x1, x2, x3, x4, x5, x6, x7) := x in
-     (x0 : Z, x1 : Z, x2 : Z, x3 : Z, x4 : Z, x5 : Z, x6 : Z, x7 : Z).
-Definition wire_digitsZToW (x : Specific.GF25519.wire_digits) : wire_digitsW
-  := let '(x0, x1, x2, x3, x4, x5, x6, x7) := x in
-     (x0 : word64, x1 : word64, x2 : word64, x3 : word64, x4 : word64, x5 : word64, x6 : word64, x7 : word64).
-
-Definition app_7 {T} (f : wire_digitsW) (P : wire_digitsW -> T) : T.
-Proof.
-  cbv [wire_digitsW] in *.
-  set (f0 := f).
-  repeat (let g := fresh "g" in destruct f as [f g]).
-  apply P.
-  apply f0.
-Defined.
-
-Definition app_7_correct {T} f (P : wire_digitsW -> T) : app_7 f P = P f.
-Proof.
-  intros.
-  cbv [wire_digitsW] in *.
-  destruct_head' prod.
-  reflexivity.
-Qed.
-
-Definition app_10 {T} (f : fe25519W) (P : fe25519W -> T) : T.
-Proof.
-  cbv [fe25519W] in *.
-  set (f0 := f).
-  repeat (let g := fresh "g" in destruct f as [f g]).
-  apply P.
-  apply f0.
-Defined.
-
-Definition app_10_correct {T} f (P : fe25519W -> T) : app_10 f P = P f.
-Proof.
-  intros.
-  cbv [fe25519W] in *.
-  destruct_head' prod.
-  reflexivity.
-Qed.
-
-Definition appify2 {T} (op : fe25519W -> fe25519W -> T) (f g : fe25519W) :=
-  app_10 f (fun f0 => (app_10 g (fun g0 => op f0 g0))).
-
-Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g.
-Proof.
-  intros. cbv [appify2].
-  etransitivity; apply app_10_correct.
-Qed.
-
-Definition uncurry_unop_fe25519W {T} (op : fe25519W -> T)
-  := Eval cbv -[word64] in Tuple.uncurry (n:=length_fe25519) op.
-Definition curry_unop_fe25519W {T} op : fe25519W -> T
-  := Eval cbv -[word64] in fun f => app_10 f (Tuple.curry (n:=length_fe25519) op).
-Definition uncurry_binop_fe25519W {T} (op : fe25519W -> fe25519W -> T)
-  := Eval cbv -[word64] in uncurry_unop_fe25519W (fun f => uncurry_unop_fe25519W (op f)).
-Definition curry_binop_fe25519W {T} op : fe25519W -> fe25519W -> T
-  := Eval cbv -[word64] in appify2 (fun f => curry_unop_fe25519W (curry_unop_fe25519W op f)).
-
-Definition uncurry_unop_wire_digitsW {T} (op : wire_digitsW -> T)
-  := Eval cbv -[word64] 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_7 f (Tuple.curry (n:=length wire_widths) op).
-
-
-Definition fe25519 :=
-  Eval cbv [fst snd] in
-    let sanity := eq_refl : length bounds = length limb_widths in
-    (word_of 25 * word_of 26 * word_of 25 * word_of 26 * word_of 25 * word_of 26 * word_of 25 * word_of 26 * word_of 25 * word_of 26)%type.
-Definition wire_digits :=
-  Eval cbv [fst snd Tuple.tuple Tuple.tuple'] in
-    (unbounded_word 32 * unbounded_word 32 * unbounded_word 32 * unbounded_word 32
-     * unbounded_word 32 * unbounded_word 32 * unbounded_word 32 * unbounded_word 31)%type.
-Definition proj1_fe25519W (x : fe25519) : fe25519W
-  := let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in
-     (proj_word x0, proj_word x1, proj_word x2, proj_word x3, proj_word x4,
-      proj_word x5, proj_word x6, proj_word x7, proj_word x8, proj_word x9).
-Coercion proj1_fe25519 (x : fe25519) : Specific.GF25519.fe25519
-  := fe25519WToZ (proj1_fe25519W x).
-Definition is_bounded (x : Specific.GF25519.fe25519) : bool
-  := let res := Tuple.map2
-                  (fun bounds v =>
-                     let '(lower, upper) := bounds in
-                     (lower <=? v) && (v <=? upper))%bool%Z
-                  (Tuple.from_list _ (List.rev bounds) eq_refl) x in
-     List.fold_right andb true (Tuple.to_list _ res).
-
-Lemma is_bounded_proj1_fe25519 (x : fe25519) : is_bounded (proj1_fe25519 x) = true.
-Proof.
-  refine (let '(Build_bounded_word' x0 p0, Build_bounded_word' x1 p1, Build_bounded_word' x2 p2, Build_bounded_word' x3 p3, Build_bounded_word' x4 p4,
-                Build_bounded_word' x5 p5, Build_bounded_word' x6 p6, Build_bounded_word' x7 p7, Build_bounded_word' x8 p8, Build_bounded_word' x9 p9)
-            as x := x return is_bounded (proj1_fe25519 x) = true in
-          _).
-  cbv [is_bounded proj1_fe25519 proj1_fe25519W fe25519WToZ to_list length bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj_word].
-  apply fold_right_andb_true_iff_fold_right_and_True.
-  cbv [fold_right List.map].
-  cbv beta in *.
-  repeat split; assumption.
-Qed.
-
-Definition proj1_wire_digitsW (x : wire_digits) : wire_digitsW
-  := let '(x0, x1, x2, x3, x4, x5, x6, x7) := x in
-     (proj_word x0, proj_word x1, proj_word x2, proj_word x3, proj_word x4,
-      proj_word x5, proj_word x6, proj_word x7).
-Coercion proj1_wire_digits (x : wire_digits) : Specific.GF25519.wire_digits
-  := wire_digitsWToZ (proj1_wire_digitsW x).
-Definition wire_digits_is_bounded (x : Specific.GF25519.wire_digits) : bool
-  := let res := Tuple.map2
-                  (fun bounds v =>
-                     let '(lower, upper) := bounds in
-                     (lower <=? v) && (v <=? upper))%bool%Z
-                  (Tuple.from_list _ (List.rev wire_digit_bounds) eq_refl) x in
-     List.fold_right andb true (Tuple.to_list _ res).
-
-Lemma is_bounded_proj1_wire_digits (x : wire_digits) : wire_digits_is_bounded (proj1_wire_digits x) = true.
-Proof.
-  refine (let '(Build_bounded_word' x0 p0, Build_bounded_word' x1 p1, Build_bounded_word' x2 p2, Build_bounded_word' x3 p3, Build_bounded_word' x4 p4,
-                Build_bounded_word' x5 p5, Build_bounded_word' x6 p6, Build_bounded_word' x7 p7)
-            as x := x return wire_digits_is_bounded (proj1_wire_digits x) = true in
-          _).
-  cbv [wire_digits_is_bounded proj1_wire_digits proj1_wire_digitsW wire_digitsWToZ to_list length wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj_word].
-  apply fold_right_andb_true_iff_fold_right_and_True.
-  cbv [fold_right List.map].
-  cbv beta in *.
-  repeat split; assumption.
-Qed.
-
-(** TODO: Turn this into a lemma to speed up proofs *)
-Ltac unfold_is_bounded_in H :=
-  unfold is_bounded, wire_digits_is_bounded, fe25519WToZ, wire_digitsWToZ in H;
-  cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app] in H;
-  rewrite !Bool.andb_true_iff in H.
-
-Definition Pow2_64 := Eval compute in 2^64.
-Definition unfold_Pow2_64 : 2^64 = Pow2_64 := eq_refl.
-
-Definition exist_fe25519W (x : fe25519W) : is_bounded (fe25519WToZ x) = true -> fe25519.
-Proof.
-  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) as x := x return is_bounded (fe25519WToZ x) = true -> fe25519 in
-          fun H => (fun H' => (Build_bounded_word x0 _, Build_bounded_word x1 _, Build_bounded_word x2 _, Build_bounded_word x3 _, Build_bounded_word x4 _,
-                               Build_bounded_word x5 _, Build_bounded_word x6 _, Build_bounded_word x7 _, Build_bounded_word x8 _, Build_bounded_word x9 _))
-                     (let H' := proj1 (@fold_right_andb_true_iff_fold_right_and_True _) H in
-                      _));
-    [
-    | | | | | | | | |
-    | clearbody H'; clear H x;
-      unfold_is_bounded_in H';
-      exact H' ];
-    destruct_head and; auto;
-      rewrite_hyp !*; reflexivity.
-Defined.
-
-Definition exist_fe25519' (x : Specific.GF25519.fe25519) : is_bounded x = true -> fe25519.
-Proof.
-  intro H; apply (exist_fe25519W (fe25519ZToW x)).
-  abstract (
-      hnf in x; destruct_head prod;
-      pose proof H as H';
-      unfold_is_bounded_in H;
-      destruct_head and;
-      Z.ltb_to_lt;
-      rewrite !ZToWord64ToZ by (simpl; omega);
-      assumption
-    ).
-Defined.
-
-Definition exist_fe25519 (x : Specific.GF25519.fe25519) : is_bounded x = true -> fe25519.
-Proof.
-  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) as x := x return is_bounded x = true -> fe25519 in
-          fun H => _).
-  let v := constr:(exist_fe25519' (x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) H) in
-  let rec do_refine v :=
-      first [ let v' := (eval cbv [exist_fe25519W fe25519ZToW exist_fe25519' proj_word Build_bounded_word snd fst] in (proj_word v)) in
-              refine (Build_bounded_word v' _); abstract exact (word_bounded v)
-            | let v' := (eval cbv [exist_fe25519W fe25519ZToW exist_fe25519' proj_word Build_bounded_word snd fst] in (proj_word (snd v))) in
-              refine (_, Build_bounded_word v' _);
-              [ do_refine (fst v) | abstract exact (word_bounded (snd v)) ] ] in
-  do_refine v.
-Defined.
-
-Lemma proj1_fe25519_exist_fe25519W x pf : proj1_fe25519 (exist_fe25519W x pf) = fe25519WToZ x.
-Proof.
-  revert pf.
-  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) as x := x return forall pf : is_bounded (fe25519WToZ x) = true, proj1_fe25519 (exist_fe25519W x pf) = fe25519WToZ x in
-          fun pf => _).
-  reflexivity.
-Qed.
-Lemma proj1_fe25519W_exist_fe25519 x pf : proj1_fe25519W (exist_fe25519 x pf) = fe25519ZToW x.
-Proof.
-  revert pf.
-  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) as x := x return forall pf : is_bounded x = true, proj1_fe25519W (exist_fe25519 x pf) = fe25519ZToW x in
-          fun pf => _).
-  reflexivity.
-Qed.
-Lemma proj1_fe25519_exist_fe25519 x pf : proj1_fe25519 (exist_fe25519 x pf) = x.
-Proof.
-  revert pf.
-  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) as x := x return forall pf : is_bounded x = true, proj1_fe25519 (exist_fe25519 x pf) = x in
-          fun pf => _).
-  cbv [proj1_fe25519 exist_fe25519 proj1_fe25519W fe25519WToZ proj_word Build_bounded_word].
-  unfold_is_bounded_in pf.
-  destruct_head and.
-  Z.ltb_to_lt.
-  rewrite !ZToWord64ToZ by (rewrite unfold_Pow2_64; cbv [Pow2_64]; omega).
-  reflexivity.
-Qed.
-
-Definition exist_wire_digitsW (x : wire_digitsW) : wire_digits_is_bounded (wire_digitsWToZ x) = true -> wire_digits.
-Proof.
-  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7) as x := x return wire_digits_is_bounded (wire_digitsWToZ x) = true -> wire_digits in
-          fun H => (fun H' => (Build_bounded_word x0 _, Build_bounded_word x1 _, Build_bounded_word x2 _, Build_bounded_word x3 _, Build_bounded_word x4 _,
-                               Build_bounded_word x5 _, Build_bounded_word x6 _, Build_bounded_word x7 _))
-                     (let H' := proj1 (@fold_right_andb_true_iff_fold_right_and_True _) H in
-                      _));
-    [
-    | | | | | | |
-    | clearbody H'; clear H x;
-      unfold_is_bounded_in H';
-      exact H' ];
-    destruct_head and; auto;
-      rewrite_hyp !*; reflexivity.
-Defined.
-
-Definition exist_wire_digits' (x : Specific.GF25519.wire_digits) : wire_digits_is_bounded x = true -> wire_digits.
-Proof.
-  intro H; apply (exist_wire_digitsW (wire_digitsZToW x)).
-  abstract (
-      hnf in x; destruct_head prod;
-      pose proof H as H';
-      unfold_is_bounded_in H;
-      destruct_head and;
-      Z.ltb_to_lt;
-      rewrite !ZToWord64ToZ by (simpl; omega);
-      assumption
-    ).
-Defined.
-
-Definition exist_wire_digits (x : Specific.GF25519.wire_digits) : wire_digits_is_bounded x = true -> wire_digits.
-Proof.
-  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7) as x := x return wire_digits_is_bounded x = true -> wire_digits in
-          fun H => _).
-  let v := constr:(exist_wire_digits' (x0, x1, x2, x3, x4, x5, x6, x7) H) in
-  let rec do_refine v :=
-      first [ let v' := (eval cbv [exist_wire_digitsW wire_digitsZToW exist_wire_digits' proj_word Build_bounded_word snd fst] in (proj_word v)) in
-              refine (Build_bounded_word v' _); abstract exact (word_bounded v)
-            | let v' := (eval cbv [exist_wire_digitsW wire_digitsZToW exist_wire_digits' proj_word Build_bounded_word snd fst] in (proj_word (snd v))) in
-              refine (_, Build_bounded_word v' _);
-              [ do_refine (fst v) | abstract exact (word_bounded (snd v)) ] ] in
-  do_refine v.
-Defined.
-
-Lemma proj1_wire_digits_exist_wire_digitsW x pf : proj1_wire_digits (exist_wire_digitsW x pf) = wire_digitsWToZ x.
-Proof.
-  revert pf.
-  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7) as x := x return forall pf : wire_digits_is_bounded (wire_digitsWToZ x) = true, proj1_wire_digits (exist_wire_digitsW x pf) = wire_digitsWToZ x in
-          fun pf => _).
-  reflexivity.
-Qed.
-Lemma proj1_wire_digitsW_exist_wire_digits x pf : proj1_wire_digitsW (exist_wire_digits x pf) = wire_digitsZToW x.
-Proof.
-  revert pf.
-  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7) as x := x return forall pf : wire_digits_is_bounded x = true, proj1_wire_digitsW (exist_wire_digits x pf) = wire_digitsZToW x in
-          fun pf => _).
-  reflexivity.
-Qed.
-Lemma proj1_wire_digits_exist_wire_digits x pf : proj1_wire_digits (exist_wire_digits x pf) = x.
-Proof.
-  revert pf.
-  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7) as x := x return forall pf : wire_digits_is_bounded x = true, proj1_wire_digits (exist_wire_digits x pf) = x in
-          fun pf => _).
-  cbv [proj1_wire_digits exist_wire_digits proj1_wire_digitsW wire_digitsWToZ proj_word Build_bounded_word].
-  unfold_is_bounded_in pf.
-  destruct_head and.
-  Z.ltb_to_lt.
-  rewrite !ZToWord64ToZ by (rewrite unfold_Pow2_64; cbv [Pow2_64]; omega).
-  reflexivity.
-Qed.
-
-(* END precomputation *)
-
-(* Precompute constants *)
-
-Definition one := Eval vm_compute in exist_fe25519 Specific.GF25519.one_ eq_refl.
-
-Definition zero := Eval vm_compute in exist_fe25519 Specific.GF25519.zero_ eq_refl.
-
-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)
-      (Hid : id = F id')
-      (Hop_bounded : forall x y, is_bounded (F x) = true
-                                 -> is_bounded (F y) = true
-                                 -> is_bounded (op (F x) (F y)) = true)
-      (Hop : forall x y, is_bounded (F x) = true
-                         -> is_bounded (F y) = true
-                         -> op (F x) (F y) = F (op' x y))
-      (Hls_bounded : forall n, is_bounded (F (nth_default id' ls n)) = true)
-  : F (fold_chain_opt id' op' chain ls)
-    = fold_chain_opt id op chain (List.map F ls)
-    /\ is_bounded (F (fold_chain_opt id' op' chain ls)) = true.
-Proof.
-  rewrite !fold_chain_opt_correct.
-  revert dependent ls; induction chain as [|x xs IHxs]; intros.
-  { pose proof (Hls_bounded 0%nat).
-    destruct ls; simpl; split; trivial; congruence. }
-  { destruct x; simpl; unfold Let_In; simpl.
-    rewrite (fun ls pf => proj1 (IHxs ls pf)) at 1; simpl.
-    { do 2 f_equal.
-      rewrite <- Hop, Hid by auto.
-      rewrite !map_nth_default_always.
-      split; try reflexivity.
-      apply (IHxs (_::_)).
-      intros [|?]; autorewrite with simpl_nth_default; auto.
-      rewrite <- Hop; auto. }
-    { intros [|?]; simpl;
-        autorewrite with simpl_nth_default; auto.
-      rewrite <- Hop; auto. } }
-Qed.
-
-Lemma encode_bounded x : is_bounded (encode x) = true.
-Proof.
-  pose proof (bounded_encode x).
-  generalize dependent (encode x).
-  intro t; compute in t; intros.
-  destruct_head prod.
-  unfold Pow2Base.bounded in H.
-  pose proof (H 0%nat); pose proof (H 1%nat); pose proof (H 2%nat);
-    pose proof (H 3%nat); pose proof (H 4%nat); pose proof (H 5%nat);
-      pose proof (H 6%nat); pose proof (H 7%nat); pose proof (H 8%nat);
-        pose proof (H 9%nat); clear H.
-  simpl in *.
-  cbv [Z.pow_pos Z.mul Pos.mul Pos.iter nth_default nth_error value] in *.
-  unfold is_bounded.
-  apply fold_right_andb_true_iff_fold_right_and_True.
-  cbv [is_bounded proj1_fe25519 to_list length bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj_word fold_right].
-  repeat split; rewrite !Bool.andb_true_iff, !Z.leb_le; omega.
-Qed.
-
-Definition encode (x : F modulus) : fe25519
-  := exist_fe25519 (encode x) (encode_bounded x).
-
-Definition decode (x : fe25519) : F modulus
-  := ModularBaseSystem.decode (proj1_fe25519 x).
-
-Definition div (f g : fe25519) : fe25519
-  := exist_fe25519 (div (proj1_fe25519 f) (proj1_fe25519 g)) (encode_bounded _).
-
-Definition eq (f g : fe25519) : Prop := eq (proj1_fe25519 f) (proj1_fe25519 g).
-
-
-Notation ibinop_correct_and_bounded irop op
-  := (forall x y,
-         is_bounded (fe25519WToZ x) = true
-         -> is_bounded (fe25519WToZ y) = true
-         -> fe25519WToZ (irop x y) = op (fe25519WToZ x) (fe25519WToZ y)
-            /\ is_bounded (fe25519WToZ (irop x y)) = true) (only parsing).
-Notation iunop_correct_and_bounded irop op
-  := (forall x,
-         is_bounded (fe25519WToZ x) = true
-         -> fe25519WToZ (irop x) = op (fe25519WToZ x)
-            /\ is_bounded (fe25519WToZ (irop x)) = true) (only parsing).
-Notation iunop_FEToZ_correct irop op
-  := (forall x,
-         is_bounded (fe25519WToZ x) = true
-         -> word64ToZ (irop x) = op (fe25519WToZ x)) (only parsing).
-Notation iunop_FEToWire_correct_and_bounded irop op
-  := (forall x,
-         is_bounded (fe25519WToZ x) = true
-         -> wire_digitsWToZ (irop x) = op (fe25519WToZ x)
-            /\ wire_digits_is_bounded (wire_digitsWToZ (irop x)) = true) (only parsing).
-Notation iunop_WireToFE_correct_and_bounded irop op
-  := (forall x,
-         wire_digits_is_bounded (wire_digitsWToZ x) = true
-         -> fe25519WToZ (irop x) = op (wire_digitsWToZ x)
-            /\ is_bounded (fe25519WToZ (irop x)) = true) (only parsing).
diff --git a/src/Specific/GF25519Reflective.v b/src/Specific/GF25519Reflective.v
index c66f64f48..f80bc492b 100644
--- a/src/Specific/GF25519Reflective.v
+++ b/src/Specific/GF25519Reflective.v
@@ -6,7 +6,7 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
 Require Export Crypto.Specific.GF25519.
-Require Import Crypto.Specific.GF25519BoundedCommonWord.
+Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.MapInterp.
@@ -45,45 +45,51 @@ Declare Reduction asm_interp
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rfreeze rge_modulus rpack runpack
             curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW
-            Interp Word64.interp_op interp interp_flat_type Word64.interp_base_type interpf interp_flat_type fst snd].
+            Word64.interp_op Word64.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            Interp interp interp_flat_type interpf interp_flat_type fst snd].
 Ltac asm_interp
   := cbv beta iota delta
          [id
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
             radd rsub rmul ropp rfreeze rge_modulus rpack runpack
             curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW
-            Interp Word64.interp_op interp interp_flat_type Word64.interp_base_type interpf interp_flat_type fst snd].
+            Word64.interp_op Word64.interp_base_type
+            Z.interp_op Z.interp_base_type
+            Z.Syntax.interp_op Z.Syntax.interp_base_type
+            Interp interp interp_flat_type interpf interp_flat_type fst snd].
 
-Definition interp_radd : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
+Definition interp_radd : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
   := Eval asm_interp in interp_bexpr radd.
 (*Print interp_radd.*)
 Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl.
-Definition interp_rsub : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
+Definition interp_rsub : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
   := Eval asm_interp in interp_bexpr rsub.
 (*Print interp_rsub.*)
 Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl.
-Definition interp_rmul : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
+Definition interp_rmul : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
   := Eval asm_interp in interp_bexpr rmul.
 (*Print interp_rmul.*)
 Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl.
-Definition interp_ropp : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
+Definition interp_ropp : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
   := Eval asm_interp in interp_uexpr ropp.
 (*Print interp_ropp.*)
 Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl.
-Definition interp_rfreeze : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
+Definition interp_rfreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
   := Eval asm_interp in interp_uexpr rfreeze.
 (*Print interp_rfreeze.*)
 Definition interp_rfreeze_correct : interp_rfreeze = interp_uexpr rfreeze := eq_refl.
 
-Definition interp_rge_modulus : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.word64
+Definition interp_rge_modulus : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64
   := Eval asm_interp in interp_uexpr_FEToZ rge_modulus.
 Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl.
 
-Definition interp_rpack : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.wire_digitsW
+Definition interp_rpack : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.wire_digitsW
   := Eval asm_interp in interp_uexpr_FEToWire rpack.
 Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl.
 
-Definition interp_runpack : Specific.GF25519BoundedCommonWord.wire_digitsW -> Specific.GF25519BoundedCommonWord.fe25519W
+Definition interp_runpack : Specific.GF25519BoundedCommon.wire_digitsW -> Specific.GF25519BoundedCommon.fe25519W
   := Eval asm_interp in interp_uexpr_WireToFE runpack.
 Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl.
 
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index 1d4922962..951ce89cf 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/Common.v
@@ -1,5 +1,5 @@
 Require Export Crypto.Specific.GF25519.
-Require Import Crypto.Specific.GF25519BoundedCommonWord.
+Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Z.Interpretations.
@@ -37,15 +37,15 @@ Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT.
 Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET.
 Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
 
-Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
+Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
   := fun e => curry_binop_fe25519W (Interp (@Word64.interp_op) e).
-Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
+Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
   := fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e).
-Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.word64
+Definition interp_uexpr_FEToZ : ExprUnOpFEToZ -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64
   := fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e).
-Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.wire_digitsW
+Definition interp_uexpr_FEToWire : ExprUnOpFEToWire -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.wire_digitsW
   := fun e => curry_unop_fe25519W (Interp (@Word64.interp_op) e).
-Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> Specific.GF25519BoundedCommonWord.wire_digitsW -> Specific.GF25519BoundedCommonWord.fe25519W
+Definition interp_uexpr_WireToFE : ExprUnOpWireToFE -> Specific.GF25519BoundedCommon.wire_digitsW -> Specific.GF25519BoundedCommon.fe25519W
   := fun e => curry_unop_wire_digitsW (Interp (@Word64.interp_op) e).
 
 Notation binop_correct_and_bounded rop op