Factor out parameter-specific code

After    | File Name                                   | Before   || Change
------------------------------------------------------------------------------
6m08.27s | Total                                       | 6m25.95s || -0m17.68s
------------------------------------------------------------------------------
  N/A    | Specific/ArithmeticSynthesisTest32          | 0m39.62s || -0m39.61s
0m38.34s | Specific/X25519/C32/ArithmeticSynthesisTest |   N/A    || +0m38.34s
0m20.46s | Specific/X25519/C32/ReificationTypes        |   N/A    || +0m20.46s
2m31.97s | Specific/X25519/C64/ladderstep              | 2m51.10s || -0m19.12s
  N/A    | Specific/ArithmeticSynthesisTest            | 0m09.54s || -0m09.53s
0m09.50s | Specific/X25519/C64/ArithmeticSynthesisTest |   N/A    || +0m09.50s
1m03.72s | Specific/X25519/C32/femul                   | 1m11.22s || -0m07.50s
0m10.44s | Specific/IntegrationTestFreeze              | 0m17.29s || -0m06.84s
0m34.55s | Specific/X25519/C32/fesquare                | 0m40.47s || -0m05.92s
0m05.50s | Specific/X25519/C64/ReificationTypes        |   N/A    || +0m05.50s
0m12.47s | Specific/X25519/C64/femul                   | 0m13.98s || -0m01.50s
0m08.93s | Specific/X25519/C64/fesquare                | 0m10.67s || -0m01.74s
0m11.14s | Specific/IntegrationTestSub                 | 0m12.06s || -0m00.92s
0m00.50s | Specific/X25519/C32/CurveParameters         |   N/A    || +0m00.50s
0m00.38s | Specific/CurveParameters                    |   N/A    || +0m00.38s
0m00.37s | Specific/X25519/C64/CurveParameters         |   N/A    || +0m00.37s

18 files changed, 1040 insertions, 1019 deletions

diff --git a/_CoqProject b/_CoqProject
index 0adfec1b9..56eeb51ff 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -222,9 +222,8 @@ src/Spec/MontgomeryCurve.v
 src/Spec/MxDH.v
 src/Spec/WeierstrassCurve.v
 src/Spec/Test/X25519.v
-src/Specific/ArithmeticSynthesisTest.v
 src/Specific/ArithmeticSynthesisTest130.v
-src/Specific/ArithmeticSynthesisTest32.v
+src/Specific/CurveParameters.v
 src/Specific/IntegrationTestDisplayCommon.v
 src/Specific/IntegrationTestDisplayCommonTactics.v
 src/Specific/IntegrationTestFreeze.v
@@ -262,10 +261,16 @@ src/Specific/NISTP256/AMD64/fesubDisplay.v
 src/Specific/NISTP256/FancyMachine256/Barrett.v
 src/Specific/NISTP256/FancyMachine256/Core.v
 src/Specific/NISTP256/FancyMachine256/Montgomery.v
+src/Specific/X25519/C32/ArithmeticSynthesisTest.v
+src/Specific/X25519/C32/CurveParameters.v
+src/Specific/X25519/C32/ReificationTypes.v
 src/Specific/X25519/C32/femul.v
 src/Specific/X25519/C32/femulDisplay.v
 src/Specific/X25519/C32/fesquare.v
 src/Specific/X25519/C32/fesquareDisplay.v
+src/Specific/X25519/C64/ArithmeticSynthesisTest.v
+src/Specific/X25519/C64/CurveParameters.v
+src/Specific/X25519/C64/ReificationTypes.v
 src/Specific/X25519/C64/femul.v
 src/Specific/X25519/C64/femulDisplay.v
 src/Specific/X25519/C64/fesquare.v
diff --git a/src/Specific/ArithmeticSynthesisTest32.v b/src/Specific/ArithmeticSynthesisTest32.v
deleted file mode 100644
index 880652374..000000000
--- a/src/Specific/ArithmeticSynthesisTest32.v
+++ /dev/null
@@ -1,466 +0,0 @@
-Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
-Require Import Coq.Lists.List. Import ListNotations.
-Require Import Crypto.Arithmetic.Core. Import B.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Arithmetic.Saturated.Freeze.
-Require Import Crypto.Util.Decidable.
-Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Crypto.Util.Tuple.
-Require Import Crypto.Util.QUtil.
-Local Notation tuple := Tuple.tuple.
-Local Open Scope list_scope.
-Local Open Scope Z_scope.
-Local Coercion Z.of_nat : nat >-> Z.
-
-(***
-Modulus : 2^255-19
-Base: 25/26
-***)
-Section Ops25p5.
-  Local Infix "^" := tuple : type_scope.
-
-  (* These definitions will need to be passed as Ltac arguments (or
-  cleverly inferred) when things are eventually automated *)
-  Definition sz := 10%nat.
-  Definition bitwidth := 32.
-  Definition s : Z := 2^255.
-  Definition c : list B.limb := [(1, 19)].
-  Definition carry_chain1 := Eval vm_compute in (seq 0 (pred sz)).
-  Definition carry_chain2 := [0;1]%nat.
-
-  Definition a24 := 121665%Z.
-  Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
-  (* These definitions are inferred from those above *)
-  Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *)
-  Section wt.
-    Import QArith Qround.
-    Local Coercion QArith_base.inject_Z : Z >-> Q.
-    Definition wt (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i).
-  End wt.
-  Definition sz2 := Eval vm_compute in ((sz * 2) - 1)%nat.
-  Definition m_enc :=
-    Eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c)).
-  Definition coef := (* subtraction coefficient *)
-    Eval vm_compute in
-      ((fix addm (acc: Z^sz) (ctr : nat) : Z^sz :=
-         match ctr with
-         | O => acc
-         | S n => addm (Positional.add_cps wt acc m_enc id) n
-         end) (Positional.zeros sz) coef_div_modulus).
-  Definition coef_mod : mod_eq m (Positional.eval (n:=sz) wt coef) 0 := eq_refl.
-  Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed.
-  Lemma wt_nonzero i : wt i <> 0.
-  Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed.
-  Lemma wt_divides i : wt (S i) / wt i > 0.
-  Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed.
-  Lemma wt_divides' i : wt (S i) / wt i <> 0.
-  Proof. symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides. Qed.
-  Definition wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0 := wt_divides' i.
-  Definition wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0 := wt_divides' i.
-
-  Local Ltac solve_constant_sig :=
-    lazymatch goal with
-    | [ |- { c : Z^?sz | Positional.Fdecode (m:=?M) ?wt c = ?v } ]
-      => let t := (eval vm_compute in
-                      (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt (F.to_Z (m:=M) v))) in
-         (exists t; vm_decide)
-    end.
-
-  Definition zero_sig :
-    { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F}.
-  Proof.
-    solve_constant_sig.
-  Defined.
-
-  Definition one_sig :
-    { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F}.
-  Proof.
-    solve_constant_sig.
-  Defined.
-
-  Definition a24_sig :
-    { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m a24 }.
-  Proof.
-    solve_constant_sig.
-  Defined.
-
-  Definition add_sig :
-    { add : (Z^sz -> Z^sz -> Z^sz)%type |
-               forall a b : Z^sz,
-                 let eval := Positional.Fdecode (m:=m) wt in
-                 eval (add a b) = (eval a  + eval b)%F }.
-  Proof.
-    eexists; cbv beta zeta; intros a b.
-    pose proof wt_nonzero.
-    let x := constr:(
-        Positional.add_cps (n := sz) wt a b id) in
-    solve_op_F wt x. reflexivity.
-  Defined.
-
-  Definition sub_sig :
-    {sub : (Z^sz -> Z^sz -> Z^sz)%type |
-               forall a b : Z^sz,
-                 let eval := Positional.Fdecode (m:=m) wt in
-                 eval (sub a b) = (eval a - eval b)%F}.
-  Proof.
-    eexists; cbv beta zeta; intros a b.
-    pose proof wt_nonzero.
-    let x := constr:(
-         Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in
-    solve_op_F wt x. reflexivity.
-  Defined.
-
-  Definition opp_sig :
-    {opp : (Z^sz -> Z^sz)%type |
-               forall a : Z^sz,
-                 let eval := Positional.Fdecode (m := m) wt in
-                 eval (opp a) = F.opp (eval a)}.
-  Proof.
-    eexists; cbv beta zeta; intros a.
-    pose proof wt_nonzero.
-    let x := constr:(
-         Positional.opp_cps (n:=sz) (coef := coef) wt a id) in
-    solve_op_F wt x. reflexivity.
-  Defined.
-
-  Definition mul_sig :
-    {mul : (Z^sz -> Z^sz -> Z^sz)%type |
-               forall a b : Z^sz,
-                 let eval := Positional.Fdecode (m := m) wt in
-                 eval (mul a b) = (eval a  * eval b)%F}.
-  Proof.
-    eexists; cbv beta zeta; intros a b.
-    pose proof wt_nonzero.
-    let x := constr:(
-         Positional.mul_cps (n:=sz) (m:=sz2) wt a b
-                            (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in
-    solve_op_F wt x.
-    instantiate (1 := fun a b =>
-      (* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
-      let '(in_9, in_8, in_7, in_6, in_5, in_4, in_3, in_2, in_1, in_0) := a in
-      let '(in2_9, in2_8, in2_7, in2_6, in2_5, in2_4, in2_3, in2_2, in2_1, in2_0) := b in
-      dlet output_0 := in2_0 * in_0 in
-dlet output_1 :=       in2_0 * in_1 +
-                    in2_1 * in_0 in
-dlet output_2 :=  2 *  in2_1 * in_1 +
-                    in2_0 * in_2 +
-                    in2_2 * in_0 in
-dlet output_3 :=       in2_1 * in_2 +
-                    in2_2 * in_1 +
-                    in2_0 * in_3 +
-                    in2_3 * in_0 in
-dlet output_4 :=       in2_2 * in_2 +
-               2 * (in2_1 * in_3 +
-                    in2_3 * in_1) +
-                    in2_0 * in_4 +
-                    in2_4 * in_0 in
-dlet output_5 :=       in2_2 * in_3 +
-                    in2_3 * in_2 +
-                    in2_1 * in_4 +
-                    in2_4 * in_1 +
-                    in2_0 * in_5 +
-                    in2_5 * in_0 in
-dlet output_6 :=  2 * (in2_3 * in_3 +
-                    in2_1 * in_5 +
-                    in2_5 * in_1) +
-                    in2_2 * in_4 +
-                    in2_4 * in_2 +
-                    in2_0 * in_6 +
-                    in2_6 * in_0 in
-dlet output_7 :=       in2_3 * in_4 +
-                    in2_4 * in_3 +
-                    in2_2 * in_5 +
-                    in2_5 * in_2 +
-                    in2_1 * in_6 +
-                    in2_6 * in_1 +
-                    in2_0 * in_7 +
-                    in2_7 * in_0 in
-dlet output_8 :=       in2_4 * in_4 +
-               2 * (in2_3 * in_5 +
-                    in2_5 * in_3 +
-                    in2_1 * in_7 +
-                    in2_7 * in_1) +
-                    in2_2 * in_6 +
-                    in2_6 * in_2 +
-                    in2_0 * in_8 +
-                    in2_8 * in_0 in
-dlet output_9 :=       in2_4 * in_5 +
-                    in2_5 * in_4 +
-                    in2_3 * in_6 +
-                    in2_6 * in_3 +
-                    in2_2 * in_7 +
-                    in2_7 * in_2 +
-                    in2_1 * in_8 +
-                    in2_8 * in_1 +
-                    in2_0 * in_9 +
-                    in2_9 * in_0 in
-dlet output_10 := 2 * (in2_5 * in_5 +
-                    in2_3 * in_7 +
-                    in2_7 * in_3 +
-                    in2_1 * in_9 +
-                    in2_9 * in_1) +
-                    in2_4 * in_6 +
-                    in2_6 * in_4 +
-                    in2_2 * in_8 +
-                    in2_8 * in_2 in
-dlet output_11 :=      in2_5 * in_6 +
-                    in2_6 * in_5 +
-                    in2_4 * in_7 +
-                    in2_7 * in_4 +
-                    in2_3 * in_8 +
-                    in2_8 * in_3 +
-                    in2_2 * in_9 +
-                    in2_9 * in_2 in
-dlet output_12 :=      in2_6 * in_6 +
-               2 * (in2_5 * in_7 +
-                    in2_7 * in_5 +
-                    in2_3 * in_9 +
-                    in2_9 * in_3) +
-                    in2_4 * in_8 +
-                    in2_8 * in_4 in
-dlet output_13 :=      in2_6 * in_7 +
-                    in2_7 * in_6 +
-                    in2_5 * in_8 +
-                    in2_8 * in_5 +
-                    in2_4 * in_9 +
-                    in2_9 * in_4 in
-dlet output_14 := 2 * (in2_7 * in_7 +
-                    in2_5 * in_9 +
-                    in2_9 * in_5) +
-                    in2_6 * in_8 +
-                    in2_8 * in_6 in
-dlet output_15 :=      in2_7 * in_8 +
-                    in2_8 * in_7 +
-                    in2_6 * in_9 +
-                    in2_9 * in_6 in
-dlet output_16 :=      in2_8 * in_8 +
-               2 * (in2_7 * in_9 +
-                    in2_9 * in_7) in
-dlet output_17 :=      in2_8 * in_9 +
-                    in2_9 * in_8 in
-dlet output_18 := 2 *  in2_9 * in_9 in
-dlet output_8 := output_8 + output_18 << 4 in
-dlet output_8 := output_8 + output_18 << 1 in
-dlet output_8 := output_8 + output_18 in
-dlet output_7 := output_7 + output_17 << 4 in
-dlet output_7 := output_7 + output_17 << 1 in
-dlet output_7 := output_7 + output_17 in
-dlet output_6 := output_6 + output_16 << 4 in
-dlet output_6 := output_6 + output_16 << 1 in
-dlet output_6 := output_6 + output_16 in
-dlet output_5 := output_5 + output_15 << 4 in
-dlet output_5 := output_5 + output_15 << 1 in
-dlet output_5 := output_5 + output_15 in
-dlet output_4 := output_4 + output_14 << 4 in
-dlet output_4 := output_4 + output_14 << 1 in
-dlet output_4 := output_4 + output_14 in
-dlet output_3 := output_3 + output_13 << 4 in
-dlet output_3 := output_3 + output_13 << 1 in
-dlet output_3 := output_3 + output_13 in
-dlet output_2 := output_2 + output_12 << 4 in
-dlet output_2 := output_2 + output_12 << 1 in
-dlet output_2 := output_2 + output_12 in
-dlet output_1 := output_1 + output_11 << 4 in
-dlet output_1 := output_1 + output_11 << 1 in
-dlet output_1 := output_1 + output_11 in
-dlet output_0 := output_0 + output_10 << 4 in
-dlet output_0 := output_0 + output_10 << 1 in
-dlet output_0 := output_0 + output_10 in
-(output_9, output_8, output_7, output_6, output_5, output_4, output_3, output_2, output_1, output_0)
-    ).
-    break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring.
-  Defined.
-
-  Definition square_sig :
-    {square : (Z^sz -> Z^sz)%type |
-               forall a : Z^sz,
-                 let eval := Positional.Fdecode (m := m) wt in
-                 eval (square a) = (eval a  * eval a)%F}.
-  Proof.
-    eexists; cbv beta zeta; intros a.
-    pose proof wt_nonzero.
-    let x := constr:(
-         Positional.mul_cps (n:=sz) (m:=sz2) wt a a
-                            (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in
-    solve_op_F wt x.
-    instantiate (1 := fun a =>
-      (* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
-      let '(in_9, in_8, in_7, in_6, in_5, in_4, in_3, in_2, in_1, in_0) := a in
-dlet output_0 :=       in_0 * in_0 in
-dlet output_1 :=  2 *  in_0 * in_1 in
-dlet output_2 :=  2 * (in_1 * in_1 +
-                    in_0 * in_2) in
-dlet output_3 :=  2 * (in_1 * in_2 +
-                    in_0 * in_3) in
-dlet output_4 :=       in_2 * in_2 +
-               4 *  in_1 * in_3 +
-               2 *  in_0 * in_4 in
-dlet output_5 :=  2 * (in_2 * in_3 +
-                    in_1 * in_4 +
-                    in_0 * in_5) in
-dlet output_6 :=  2 * (in_3 * in_3 +
-                    in_2 * in_4 +
-                    in_0 * in_6 +
-               2 *  in_1 * in_5) in
-dlet output_7 :=  2 * (in_3 * in_4 +
-                    in_2 * in_5 +
-                    in_1 * in_6 +
-                    in_0 * in_7) in
-dlet output_8 :=       in_4 * in_4 +
-               2 * (in_2 * in_6 +
-                    in_0 * in_8 +
-               2 * (in_1 * in_7 +
-                    in_3 * in_5)) in
-dlet output_9 :=  2 * (in_4 * in_5 +
-                    in_3 * in_6 +
-                    in_2 * in_7 +
-                    in_1 * in_8 +
-                    in_0 * in_9) in
-dlet output_10 := 2 * (in_5 * in_5 +
-                    in_4 * in_6 +
-                    in_2 * in_8 +
-               2 * (in_3 * in_7 +
-                    in_1 * in_9)) in
-dlet output_11 := 2 * (in_5 * in_6 +
-                    in_4 * in_7 +
-                    in_3 * in_8 +
-                    in_2 * in_9) in
-dlet output_12 :=      in_6 * in_6 +
-               2 * (in_4 * in_8 +
-               2 * (in_5 * in_7 +
-                    in_3 * in_9)) in
-dlet output_13 := 2 * (in_6 * in_7 +
-                    in_5 * in_8 +
-                    in_4 * in_9) in
-dlet output_14 := 2 * (in_7 * in_7 +
-                    in_6 * in_8 +
-               2 *  in_5 * in_9) in
-dlet output_15 := 2 * (in_7 * in_8 +
-                    in_6 * in_9) in
-dlet output_16 :=      in_8 * in_8 +
-               4 *  in_7 * in_9 in
-dlet output_17 := 2 *  in_8 * in_9 in
-dlet output_18 := 2 *  in_9 * in_9 in
-dlet output_8 := output_8 + output_18 << 4 in
-dlet output_8 := output_8 + output_18 << 1 in
-dlet output_8 := output_8 + output_18 in
-dlet output_7 := output_7 + output_17 << 4 in
-dlet output_7 := output_7 + output_17 << 1 in
-dlet output_7 := output_7 + output_17 in
-dlet output_6 := output_6 + output_16 << 4 in
-dlet output_6 := output_6 + output_16 << 1 in
-dlet output_6 := output_6 + output_16 in
-dlet output_5 := output_5 + output_15 << 4 in
-dlet output_5 := output_5 + output_15 << 1 in
-dlet output_5 := output_5 + output_15 in
-dlet output_4 := output_4 + output_14 << 4 in
-dlet output_4 := output_4 + output_14 << 1 in
-dlet output_4 := output_4 + output_14 in
-dlet output_3 := output_3 + output_13 << 4 in
-dlet output_3 := output_3 + output_13 << 1 in
-dlet output_3 := output_3 + output_13 in
-dlet output_2 := output_2 + output_12 << 4 in
-dlet output_2 := output_2 + output_12 << 1 in
-dlet output_2 := output_2 + output_12 in
-dlet output_1 := output_1 + output_11 << 4 in
-dlet output_1 := output_1 + output_11 << 1 in
-dlet output_1 := output_1 + output_11 in
-dlet output_0 := output_0 + output_10 << 4 in
-dlet output_0 := output_0 + output_10 << 1 in
-dlet output_0 := output_0 + output_10 in
-(output_9, output_8, output_7, output_6, output_5, output_4, output_3, output_2, output_1, output_0)
-    ).
-    break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring.
-  Defined.
-
-  (* Performs a full carry loop (as specified by carry_chain) *)
-  Definition carry_sig :
-    {carry : (Z^sz -> Z^sz)%type |
-               forall a : Z^sz,
-                 let eval := Positional.Fdecode (m := m) wt in
-                 eval (carry a) = eval a}.
-  Proof.
-    eexists; cbv beta zeta; intros a.
-    pose proof wt_nonzero. pose proof wt_divides_chain1.
-    pose proof div_mod. pose proof wt_divides_chain2.
-    let x := constr:(
-               Positional.chained_carries_cps (n:=sz) (div:=div)(modulo:=modulo) wt a carry_chain1
-                  (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r
-                  (fun rrr => Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt rrr carry_chain2 id
-             ))) in
-    solve_op_F wt x. reflexivity.
-  Defined.
-
-  Section PreFreeze.
-    Lemma wt_pos i : wt i > 0.
-    Proof. eapply pow_ceil_mul_nat_pos; vm_decide. Qed.
-
-    Lemma wt_multiples i : wt (S i) mod (wt i) = 0.
-    Proof. apply pow_ceil_mul_nat_multiples; vm_decide. Qed.
-  End PreFreeze.
-
-  Hint Opaque freeze : uncps.
-  Hint Rewrite freeze_id : uncps.
-
-  Definition freeze_sig :
-    {freeze : (Z^sz -> Z^sz)%type |
-     forall a : Z^sz,
-         (0 <= Positional.eval wt a < 2 * Z.pos m)->
-                 let eval := Positional.Fdecode (m := m) wt in
-                 eval (freeze a) = eval a}.
-  Proof.
-    eexists; cbv beta zeta; intros a ?.
-    pose proof wt_nonzero. pose proof wt_pos.
-    pose proof div_mod. pose proof wt_divides.
-    pose proof wt_multiples.
-    pose proof div_correct. pose proof modulo_correct.
-    let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in
-    F_mod_eq;
-      transitivity (Positional.eval wt x); repeat autounfold;
-        [ | autorewrite with uncps push_id push_basesystem_eval;
-            rewrite eval_freeze with (c:=c);
-            try eassumption; try omega; try reflexivity;
-            try solve [auto using B.Positional.select_id,
-                       B.Positional.eval_select, zselect_correct];
-            vm_decide].
-   cbv[mod_eq]; apply f_equal2;
-     [  | reflexivity ]; apply f_equal.
-   cbv - [runtime_opp runtime_add runtime_mul runtime_shr runtime_and Let_In Z.add_get_carry Z.zselect].
-   reflexivity.
-  Defined.
-
-  Definition ring_25p5 :=
-    (Ring.ring_by_isomorphism
-         (F := F m)
-         (H := Z^sz)
-         (phi := Positional.Fencode wt)
-         (phi' := Positional.Fdecode wt)
-         (zero := proj1_sig zero_sig)
-         (one := proj1_sig one_sig)
-         (opp := proj1_sig opp_sig)
-         (add := proj1_sig add_sig)
-         (sub := proj1_sig sub_sig)
-         (mul := proj1_sig mul_sig)
-         (phi'_zero := proj2_sig zero_sig)
-         (phi'_one := proj2_sig one_sig)
-         (phi'_opp := proj2_sig opp_sig)
-         (Positional.Fdecode_Fencode_id
-            (sz_nonzero := sz_nonzero)
-            (div_mod := div_mod)
-            wt eq_refl wt_nonzero wt_divides')
-         (Positional.eq_Feq_iff wt)
-         (proj2_sig add_sig)
-         (proj2_sig sub_sig)
-         (proj2_sig mul_sig)
-      ).
-
-(*
-Eval cbv [proj1_sig add_sig] in (proj1_sig add_sig).
-Eval cbv [proj1_sig sub_sig] in (proj1_sig sub_sig).
-Eval cbv [proj1_sig opp_sig] in (proj1_sig opp_sig).
-Eval cbv [proj1_sig mul_sig] in (proj1_sig mul_sig).
-Eval cbv [proj1_sig carry_sig] in (proj1_sig carry_sig).
-*)
-
-End Ops25p5.
diff --git a/src/Specific/CurveParameters.v b/src/Specific/CurveParameters.v
new file mode 100644
index 000000000..79282757d
--- /dev/null
+++ b/src/Specific/CurveParameters.v
@@ -0,0 +1,112 @@
+Require Export Coq.ZArith.BinInt.
+Require Export Coq.Lists.List.
+Require Export Crypto.Util.ZUtil.Notations.
+Require Crypto.Util.Tuple.
+
+Module Export Notations.
+  Export ListNotations.
+
+  Open Scope list_scope.
+  Open Scope Z_scope.
+
+  Notation limb := (Z * Z)%type.
+  Infix "^" := Tuple.tuple : type_scope.
+End Notations.
+
+(* These definitions will need to be passed as Ltac arguments (or
+   cleverly inferred) when things are eventually automated *)
+Module Type CurveParameters.
+  Parameter sz : nat.
+  Parameter bitwidth : Z.
+  Parameter s : Z.
+  Parameter c : list limb.
+  Parameter carry_chain1
+    : option (list nat). (* defaults to [seq 0 (pred sz)] *)
+  Parameter carry_chain2
+    : option (list nat). (* defaults to [0 :: 1 :: nil] *)
+  Parameter a24 : Z.
+  Parameter coef_div_modulus : nat.
+
+  Parameter mul_code : option (Z^sz -> Z^sz -> Z^sz).
+  Parameter square_code : option (Z^sz -> Z^sz).
+  Parameter upper_bound_of_exponent
+    : option (Z -> Z). (* defaults to [fun exp => 2^exp + 2^(exp-3)] *)
+  Parameter allowable_bit_widths
+    : option (list nat). (* defaults to [bitwidth :: 2*bitwidth :: nil] *)
+  Parameter freeze_extra_allowable_bit_widths
+    : option (list nat). (* defaults to [8 :: nil] *)
+  Ltac extra_prove_mul_eq := idtac.
+  Ltac extra_prove_square_eq := idtac.
+End CurveParameters.
+
+Module FillCurveParameters (P : CurveParameters).
+  Local Notation defaulted opt_v default
+    := (match opt_v with
+        | Some v => v
+        | None => default
+        end).
+  Notation compute v
+    := (ltac:(let v' := v in let v' := (eval vm_compute in v') in exact v'))
+         (only parsing).
+  Definition sz := P.sz.
+  Definition bitwidth := P.bitwidth.
+  Definition s := P.s.
+  Definition c := P.c.
+  Definition carry_chain1 := defaulted P.carry_chain1 (seq 0 (pred sz)).
+  Definition carry_chain2 := defaulted P.carry_chain2 (0 :: 1 :: nil)%nat.
+  Definition a24 := P.a24.
+  Definition coef_div_modulus := P.coef_div_modulus.
+
+  Ltac default_mul :=
+    lazymatch (eval hnf in P.mul_code) with
+    | None => reflexivity
+    | Some ?mul_code
+      => instantiate (1:=mul_code)
+    end.
+  Ltac default_square :=
+    lazymatch (eval hnf in P.square_code) with
+    | None => reflexivity
+    | Some ?square_code
+      => instantiate (1:=square_code)
+    end.
+
+  Definition upper_bound_of_exponent
+    := defaulted P.upper_bound_of_exponent (fun exp => (2^exp + 2^(exp-3))%Z).
+  Definition allowable_bit_widths
+    := defaulted P.allowable_bit_widths (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil)%nat.
+  Definition freeze_allowable_bit_widths
+    := defaulted P.freeze_extra_allowable_bit_widths [8]%nat ++ allowable_bit_widths.
+
+  (* hack around https://coq.inria.fr/bugs/show_bug.cgi?id=5764 *)
+  Ltac do_unfold v' :=
+    let P_sz := P.sz in
+    let P_bitwidth := P.bitwidth in
+    let P_s := P.s in
+    let P_c := P.c in
+    let P_carry_chain1 := P.carry_chain1 in
+    let P_carry_chain2 := P.carry_chain2 in
+    let P_a24 := P.a24 in
+    let P_coef_div_modulus := P.coef_div_modulus in
+    let P_mul_code := P.mul_code in
+    let P_square_code := P.square_code in
+    let P_upper_bound_of_exponent := P.upper_bound_of_exponent in
+    let P_allowable_bit_widths := P.allowable_bit_widths in
+    let P_freeze_extra_allowable_bit_widths := P.freeze_extra_allowable_bit_widths in
+    let v' := (eval cbv [id
+                           List.app
+                           sz bitwidth s c carry_chain1 carry_chain2 a24 coef_div_modulus
+                           P_sz P_bitwidth P_s P_c P_carry_chain1 P_carry_chain2 P_a24 P_coef_div_modulus
+                           P_mul_code P_square_code
+                           upper_bound_of_exponent allowable_bit_widths freeze_allowable_bit_widths
+                           P_upper_bound_of_exponent P_allowable_bit_widths P_freeze_extra_allowable_bit_widths
+                           pred seq]
+                in v') in
+    v'.
+  Notation unfold v
+    := (ltac:(let v' := v in
+              let v' := do_unfold v' in
+              exact v'))
+         (only parsing).
+  Ltac extra_prove_mul_eq := P.extra_prove_mul_eq.
+  Ltac extra_prove_square_eq := P.extra_prove_square_eq.
+End FillCurveParameters.
diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v
index 18cee5114..ebfab0c69 100644
--- a/src/Specific/IntegrationTestFreeze.v
+++ b/src/Specific/IntegrationTestFreeze.v
@@ -1,74 +1,27 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
+Require Import Crypto.Specific.X25519.C64.ReificationTypes.
+Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Specific.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Tactics.MoveLetIn.
-Require Import Crypto.Util.Tactics.DestructHead.
-Import ListNotations.
-
+Require Import Crypto.Util.BoundedWord.
 Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
-
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
-Section BoundedField25p5.
-  Local Coercion Z.of_nat : nat >-> Z.
-
-  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-  Let length_lw := Eval compute in List.length limb_widths.
+Local Definition phi : feBW -> F m :=
+  fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
 
-  Local Notation b_of exp := {| lower := 0 ; upper := 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] *)
-  (* The definition [bounds_exp] is a tuple-version of the
-     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
-     the approximate base-2 exponent of the bounds on the limb in that
-     position. *)
-  Let bounds_exp : Tuple.tuple Z length_lw
-    := Eval compute in
-        Tuple.from_list length_lw limb_widths eq_refl.
-  Let bounds : Tuple.tuple zrange length_lw
-    := Eval compute in
-        Tuple.map (fun e => b_of e) bounds_exp.
-
-  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
-  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
-  Let feZ : Type := tuple Z sz.
-  Let feW : Type := tuple (wordT lgbitwidth) sz.
-  Let feBW : Type := BoundedWord sz bitwidth bounds.
-  Let phi : feBW -> F m :=
-    fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
-  Lemma feBW_bounded (a : feBW)
-    : 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m.
-  Proof.
-    destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
-    revert H.
-    cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt]; cbn [fst snd].
-    repeat match goal with
-           | [ |- context[wt ?n] ]
-             => let v := (eval compute in (wt n)) in change (wt n) with v
-           end.
-    intro; destruct_head'_and.
-    omega.
-  Qed.
-
-  (* TODO : change this to field once field isomorphism happens *)
-  Definition freeze :
-    { freeze : feBW -> feBW
-    | forall a, phi (freeze a) = phi a }.
-  Proof.
-    start_preglue.
-    do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime.
-    all:fin_preglue.
-    (* jgross start here! *)
-    (*Set Ltac Profiling.*)
-    Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *)
-    (*Show Ltac Profile.*)
-    (* total time:      5.680s
+(* TODO : change this to field once field isomorphism happens *)
+Definition freeze :
+  { freeze : feBW -> feBW
+  | forall a, phi (freeze a) = phi a }.
+Proof.
+  start_preglue.
+  do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime.
+  all:fin_preglue.
+  (* jgross start here! *)
+  (*Set Ltac Profiling.*)
+  Time refine_reflectively_gen P.freeze_allowable_bit_widths anf. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *)
+  (*Show Ltac Profile.*)
+  (* total time:      5.680s
 
  tactic                                   local  total   calls       max
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
@@ -108,7 +61,5 @@ Section BoundedField25p5.
   └Glue.zrange_to_reflective -----------   0.1%   3.3%       1    0.188s
   └Glue.zrange_to_reflective_goal ------   2.0%   2.4%       1    0.136s
 
-*)
-  Time Defined. (* Finished transaction in 3.607 secs (3.607u,0.s) (successful) *)
-
-End BoundedField25p5.
+   *)
+Time Defined. (* Finished transaction in 3.607 secs (3.607u,0.s) (successful) *)
diff --git a/src/Specific/IntegrationTestSub.v b/src/Specific/IntegrationTestSub.v
index 7599c99e1..f88dc51d9 100644
--- a/src/Specific/IntegrationTestSub.v
+++ b/src/Specific/IntegrationTestSub.v
@@ -1,71 +1,27 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
+Require Import Crypto.Specific.X25519.C64.ReificationTypes.
+Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Specific.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Tactics.MoveLetIn.
-Import ListNotations.
-
+Require Import Crypto.Util.BoundedWord.
 Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
-
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
-Section BoundedField25p5.
-  Local Coercion Z.of_nat : nat >-> Z.
-
-  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-  Let length_lw := Eval compute in List.length limb_widths.
+Local Definition phi : feBW -> F m :=
+  fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
 
-  Local Notation b_of exp := {| lower := 0 ; upper := 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] *)
-  (* The definition [bounds_exp] is a tuple-version of the
-     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
-     the approximate base-2 exponent of the bounds on the limb in that
-     position. *)
-  Let bounds_exp : Tuple.tuple Z length_lw
-    := Eval compute in
-        Tuple.from_list length_lw limb_widths eq_refl.
-  Let bounds : Tuple.tuple zrange length_lw
-    := Eval compute in
-        Tuple.map (fun e => b_of e) bounds_exp.
-
-  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
-  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
-  Let feZ : Type := tuple Z sz.
-  Let feW : Type := tuple (wordT lgbitwidth) sz.
-  Let feBW : Type := BoundedWord sz bitwidth bounds.
-  Let phi : feBW -> F m :=
-    fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
-  (* TODO : change this to field once field isomorphism happens *)
-  Definition sub :
-    { sub : feBW -> feBW -> feBW
-    | forall a b, phi (sub a b) = F.sub (phi a) (phi b) }.
-  Proof.
-    lazymatch goal with
-    | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
-      => apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
-    end.
-    intros a b.
-    eexists_sig_etransitivity. all:cbv [phi].
-    rewrite <- (proj2_sig sub_sig).
-    symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
-    set (carry_subZ := fun a b => proj1_sig carry_sig (proj1_sig sub_sig a b)).
-    change (proj1_sig carry_sig (proj1_sig sub_sig ?a ?b)) with (carry_subZ a b).
-    context_to_dlet_in_rhs carry_subZ.
-    cbv beta iota delta [carry_subZ proj1_sig sub_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
-    reflexivity.
-    sig_dlet_in_rhs_to_context.
-    apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
-    (* jgross start here! *)
-    (*Set Ltac Profiling.*)
-    Time refine_reflectively. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
-    (*Show Ltac Profile.*)
-    (* total time:     19.632s
+(* TODO : change this to field once field isomorphism happens *)
+Definition sub :
+  { sub : feBW -> feBW -> feBW
+  | forall a b, phi (sub a b) = F.sub (phi a) (phi b) }.
+Proof.
+  start_preglue.
+  do_rewrite_with_2sig_add_carry sub_sig carry_sig; cbv_runtime.
+  all:fin_preglue.
+  (* jgross start here! *)
+  (*Set Ltac Profiling.*)
+  Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
+  (*Show Ltac Profile.*)
+  (* total time:     19.632s
 
  tactic                                   local  total   calls       max
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
@@ -106,7 +62,5 @@ Section BoundedField25p5.
  │ ├─ReflectiveTactics.abstract_cbv_inte   2.7%   3.3%       1    0.648s
  │ └─ReflectiveTactics.abstract_cbv_rhs    2.0%   2.7%       1    0.532s
  └─Glue.refine_to_reflective_glue ------   0.0%   2.2%       1    0.436s
-*)
-  Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
-
-End BoundedField25p5.
+   *)
+Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/IntegrationTestTemporaryMiscCommon.v
index 4aae7ee0a..083e82207 100644
--- a/src/Specific/IntegrationTestTemporaryMiscCommon.v
+++ b/src/Specific/IntegrationTestTemporaryMiscCommon.v
@@ -237,23 +237,18 @@ Ltac unmap_map_tuple _ :=
            => rewrite <- (Tuple.map_map (n:=N) f g
                           : pointwise_relation _ eq _ (Tuple.map (n:=N) (fun x : T => f (g x))))
          end.
+Ltac get_feW_bounded boundedT :=
+  lazymatch boundedT with
+  | and ?X ?Y => get_feW_bounded X
+  | ?feW_bounded _ => feW_bounded
+  end.
 Ltac subst_feW _ :=
   let T := lazymatch goal with |- @sig ?T _ => T end in
   let boundedT := lazymatch goal with |- { e | ?A -> _ } => A end in
-  match goal with
-  | [ feW := _ : Type |- _ ]
-    => match goal with
-       | [ feW_bounded := _ : feW -> Prop |- _ ]
-         => lazymatch T with
-            | context[feW] => idtac
-            end;
-            lazymatch boundedT with
-            | context[feW_bounded _] => idtac
-            end;
-            subst feW feW_bounded
-       end
-  end;
-  cbv beta.
+  let feW_bounded := get_feW_bounded boundedT in
+  let feW := lazymatch type of feW_bounded with ?feW -> Prop => feW end in
+  cbv [feW feW_bounded];
+  try clear feW feW_bounded.
 Ltac finish_conjoined_preglue _ :=
   [ > match goal with
       | [ FINAL : _ /\ ?e |- _ ] => is_evar e; refine (proj2 FINAL)
diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/X25519/C32/ArithmeticSynthesisTest.v
index b3148efdb..6b1d5ee11 100644
--- a/src/Specific/ArithmeticSynthesisTest.v
+++ b/src/Specific/X25519/C32/ArithmeticSynthesisTest.v
@@ -3,6 +3,8 @@ Require Import Coq.Lists.List. Import ListNotations.
 Require Import Crypto.Arithmetic.Core. Import B.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Arithmetic.Saturated.Freeze.
+Require Crypto.Specific.CurveParameters.
+Require Import Crypto.Specific.X25519.C32.CurveParameters.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
@@ -13,24 +15,22 @@ Local Open Scope list_scope.
 Local Open Scope Z_scope.
 Local Coercion Z.of_nat : nat >-> Z.
 
-(***
-Modulus : 2^255-19
-Base: 51
-***)
-Section Ops51.
+Module P := CurveParameters.FillCurveParameters Curve.
+
+Section Ops.
   Local Infix "^" := tuple : type_scope.
 
   (* These definitions will need to be passed as Ltac arguments (or
   cleverly inferred) when things are eventually automated *)
-  Definition sz := 5%nat.
-  Definition bitwidth := 64.
-  Definition s : Z := 2^255.
-  Definition c : list B.limb := [(1, 19)].
-  Definition carry_chain1 := Eval vm_compute in (seq 0 (pred sz)).
-  Definition carry_chain2 := [0;1]%nat.
-
-  Definition a24 := 121665%Z.
-  Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
+  Definition sz : nat := P.compute P.sz.
+  Definition bitwidth : Z := P.compute P.bitwidth.
+  Definition s : Z := P.unfold P.s. (* don't want to compute, e.g., [2^255] *)
+  Definition c : list B.limb := P.compute P.c.
+  Definition carry_chain1 := P.compute P.carry_chain1.
+  Definition carry_chain2 := P.compute P.carry_chain2.
+
+  Definition a24 := P.compute P.a24.
+  Definition coef_div_modulus : nat := P.compute P.coef_div_modulus.
   (* These definitions are inferred from those above *)
   Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *)
   Section wt.
@@ -136,28 +136,9 @@ Section Ops51.
          Positional.mul_cps (n:=sz) (m:=sz2) wt a b
                             (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in
     solve_op_F wt x.
-    instantiate (1 := fun a b =>
-      (* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
-      let '(r4, r3, r2, r1, r0) := a in
-      let '(s4, s3, s2, s1, s0) := b in
-      dlet t0  :=  r0 * s0 in
-      dlet t1  :=  r0 * s1 + r1 * s0 in
-      dlet t2  :=  r0 * s2 + r2 * s0 + r1 * s1 in
-      dlet t3  :=  r0 * s3 + r3 * s0 + r1 * s2 + r2 * s1 in
-      dlet t4  :=  r0 * s4 + r4 * s0 + r3 * s1 + r1 * s3 + r2 * s2 in
-
-      dlet r4' := r4*19 in
-      dlet r1' := r1*19 in
-      dlet r2' := r2*19 in
-      dlet r3' := r3*19 in
-
-      dlet t0 := t0 + r4' * s1 + r1' * s4 + r2' * s3 + r3' * s2 in
-      dlet t1 := t1 + r4' * s2 + r2' * s4 + r3' * s3 in
-      dlet t2 := t2 + r4' * s3 + r3' * s4 in
-      dlet t3 := t3 + r4' * s4 in
-      (t4, t3, t2, t1, t0)
-    ).
-    break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); ring.
+    P.default_mul;
+      P.extra_prove_mul_eq;
+      break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring.
   Defined.
 
   Definition square_sig :
@@ -172,22 +153,9 @@ Section Ops51.
          Positional.mul_cps (n:=sz) (m:=sz2) wt a a
                             (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in
     solve_op_F wt x.
-    instantiate (1 := fun a =>
-      (* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
-      let '(r4, r3, r2, r1, r0) := a in
-      dlet d0 := r0 * 2 in
-      dlet d1 := r1 * 2 in
-      dlet d2 := r2 * 2 * 19 in
-      dlet d419 := r4 * 19 in
-      dlet d4 := d419 * 2 in
-      dlet t0 := r0 * r0 + d4 * r1 + d2 * r3        in
-      dlet t1 := d0 * r1 + d4 * r2 + r3 * (r3 * 19) in
-      dlet t2 := d0 * r2 + r1 * r1 + d4 * r3        in
-      dlet t3 := d0 * r3 + d1 * r2 + r4 * d419      in
-      dlet t4 := d0 * r4 + d1 * r3 + r2 * r2        in
-      (t4, t3, t2, t1, t0)
-    ).
-    break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); ring.
+    P.default_square;
+      P.extra_prove_square_eq;
+      break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring.
   Defined.
 
   (* Performs a full carry loop (as specified by carry_chain) *)
@@ -246,7 +214,7 @@ Section Ops51.
    reflexivity.
   Defined.
 
-  Definition ring_51 :=
+  Definition ring :=
     (Ring.ring_by_isomorphism
          (F := F m)
          (H := Z^sz)
@@ -279,4 +247,4 @@ Eval cbv [proj1_sig mul_sig] in (proj1_sig mul_sig).
 Eval cbv [proj1_sig carry_sig] in (proj1_sig carry_sig).
 *)
 
-End Ops51.
+End Ops.
diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v
new file mode 100644
index 000000000..8e7848bc1
--- /dev/null
+++ b/src/Specific/X25519/C32/CurveParameters.v
@@ -0,0 +1,249 @@
+Require Import Crypto.Specific.CurveParameters.
+Require Import Crypto.Util.LetIn.
+
+(***
+Modulus : 2^255-19
+Base: 25.5
+***)
+
+Module Curve <: CurveParameters.
+  Definition sz : nat := 10%nat.
+  Definition bitwidth : Z := 32.
+  Definition s : Z := 2^255.
+  Definition c : list limb := [(1, 19)].
+  Definition carry_chain1 := Eval vm_compute in Some (seq 0 (pred sz)).
+  Definition carry_chain2 := Some [0;1]%nat.
+
+  Definition a24 := 121665%Z.
+  Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
+
+  Definition mul_code : option (Z^sz -> Z^sz -> Z^sz)
+    := Some (fun a b =>
+      (* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
+      let '(in_9, in_8, in_7, in_6, in_5, in_4, in_3, in_2, in_1, in_0) := a in
+      let '(in2_9, in2_8, in2_7, in2_6, in2_5, in2_4, in2_3, in2_2, in2_1, in2_0) := b in
+      dlet output_0 := in2_0 * in_0 in
+dlet output_1 :=       in2_0 * in_1 +
+                    in2_1 * in_0 in
+dlet output_2 :=  2 *  in2_1 * in_1 +
+                    in2_0 * in_2 +
+                    in2_2 * in_0 in
+dlet output_3 :=       in2_1 * in_2 +
+                    in2_2 * in_1 +
+                    in2_0 * in_3 +
+                    in2_3 * in_0 in
+dlet output_4 :=       in2_2 * in_2 +
+               2 * (in2_1 * in_3 +
+                    in2_3 * in_1) +
+                    in2_0 * in_4 +
+                    in2_4 * in_0 in
+dlet output_5 :=       in2_2 * in_3 +
+                    in2_3 * in_2 +
+                    in2_1 * in_4 +
+                    in2_4 * in_1 +
+                    in2_0 * in_5 +
+                    in2_5 * in_0 in
+dlet output_6 :=  2 * (in2_3 * in_3 +
+                    in2_1 * in_5 +
+                    in2_5 * in_1) +
+                    in2_2 * in_4 +
+                    in2_4 * in_2 +
+                    in2_0 * in_6 +
+                    in2_6 * in_0 in
+dlet output_7 :=       in2_3 * in_4 +
+                    in2_4 * in_3 +
+                    in2_2 * in_5 +
+                    in2_5 * in_2 +
+                    in2_1 * in_6 +
+                    in2_6 * in_1 +
+                    in2_0 * in_7 +
+                    in2_7 * in_0 in
+dlet output_8 :=       in2_4 * in_4 +
+               2 * (in2_3 * in_5 +
+                    in2_5 * in_3 +
+                    in2_1 * in_7 +
+                    in2_7 * in_1) +
+                    in2_2 * in_6 +
+                    in2_6 * in_2 +
+                    in2_0 * in_8 +
+                    in2_8 * in_0 in
+dlet output_9 :=       in2_4 * in_5 +
+                    in2_5 * in_4 +
+                    in2_3 * in_6 +
+                    in2_6 * in_3 +
+                    in2_2 * in_7 +
+                    in2_7 * in_2 +
+                    in2_1 * in_8 +
+                    in2_8 * in_1 +
+                    in2_0 * in_9 +
+                    in2_9 * in_0 in
+dlet output_10 := 2 * (in2_5 * in_5 +
+                    in2_3 * in_7 +
+                    in2_7 * in_3 +
+                    in2_1 * in_9 +
+                    in2_9 * in_1) +
+                    in2_4 * in_6 +
+                    in2_6 * in_4 +
+                    in2_2 * in_8 +
+                    in2_8 * in_2 in
+dlet output_11 :=      in2_5 * in_6 +
+                    in2_6 * in_5 +
+                    in2_4 * in_7 +
+                    in2_7 * in_4 +
+                    in2_3 * in_8 +
+                    in2_8 * in_3 +
+                    in2_2 * in_9 +
+                    in2_9 * in_2 in
+dlet output_12 :=      in2_6 * in_6 +
+               2 * (in2_5 * in_7 +
+                    in2_7 * in_5 +
+                    in2_3 * in_9 +
+                    in2_9 * in_3) +
+                    in2_4 * in_8 +
+                    in2_8 * in_4 in
+dlet output_13 :=      in2_6 * in_7 +
+                    in2_7 * in_6 +
+                    in2_5 * in_8 +
+                    in2_8 * in_5 +
+                    in2_4 * in_9 +
+                    in2_9 * in_4 in
+dlet output_14 := 2 * (in2_7 * in_7 +
+                    in2_5 * in_9 +
+                    in2_9 * in_5) +
+                    in2_6 * in_8 +
+                    in2_8 * in_6 in
+dlet output_15 :=      in2_7 * in_8 +
+                    in2_8 * in_7 +
+                    in2_6 * in_9 +
+                    in2_9 * in_6 in
+dlet output_16 :=      in2_8 * in_8 +
+               2 * (in2_7 * in_9 +
+                    in2_9 * in_7) in
+dlet output_17 :=      in2_8 * in_9 +
+                    in2_9 * in_8 in
+dlet output_18 := 2 *  in2_9 * in_9 in
+dlet output_8 := output_8 + output_18 << 4 in
+dlet output_8 := output_8 + output_18 << 1 in
+dlet output_8 := output_8 + output_18 in
+dlet output_7 := output_7 + output_17 << 4 in
+dlet output_7 := output_7 + output_17 << 1 in
+dlet output_7 := output_7 + output_17 in
+dlet output_6 := output_6 + output_16 << 4 in
+dlet output_6 := output_6 + output_16 << 1 in
+dlet output_6 := output_6 + output_16 in
+dlet output_5 := output_5 + output_15 << 4 in
+dlet output_5 := output_5 + output_15 << 1 in
+dlet output_5 := output_5 + output_15 in
+dlet output_4 := output_4 + output_14 << 4 in
+dlet output_4 := output_4 + output_14 << 1 in
+dlet output_4 := output_4 + output_14 in
+dlet output_3 := output_3 + output_13 << 4 in
+dlet output_3 := output_3 + output_13 << 1 in
+dlet output_3 := output_3 + output_13 in
+dlet output_2 := output_2 + output_12 << 4 in
+dlet output_2 := output_2 + output_12 << 1 in
+dlet output_2 := output_2 + output_12 in
+dlet output_1 := output_1 + output_11 << 4 in
+dlet output_1 := output_1 + output_11 << 1 in
+dlet output_1 := output_1 + output_11 in
+dlet output_0 := output_0 + output_10 << 4 in
+dlet output_0 := output_0 + output_10 << 1 in
+dlet output_0 := output_0 + output_10 in
+(output_9, output_8, output_7, output_6, output_5, output_4, output_3, output_2, output_1, output_0)
+            ).
+
+  Definition square_code : option (Z^sz -> Z^sz)
+    := Some (fun a =>
+      (* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
+      let '(in_9, in_8, in_7, in_6, in_5, in_4, in_3, in_2, in_1, in_0) := a in
+dlet output_0 :=       in_0 * in_0 in
+dlet output_1 :=  2 *  in_0 * in_1 in
+dlet output_2 :=  2 * (in_1 * in_1 +
+                    in_0 * in_2) in
+dlet output_3 :=  2 * (in_1 * in_2 +
+                    in_0 * in_3) in
+dlet output_4 :=       in_2 * in_2 +
+               4 *  in_1 * in_3 +
+               2 *  in_0 * in_4 in
+dlet output_5 :=  2 * (in_2 * in_3 +
+                    in_1 * in_4 +
+                    in_0 * in_5) in
+dlet output_6 :=  2 * (in_3 * in_3 +
+                    in_2 * in_4 +
+                    in_0 * in_6 +
+               2 *  in_1 * in_5) in
+dlet output_7 :=  2 * (in_3 * in_4 +
+                    in_2 * in_5 +
+                    in_1 * in_6 +
+                    in_0 * in_7) in
+dlet output_8 :=       in_4 * in_4 +
+               2 * (in_2 * in_6 +
+                    in_0 * in_8 +
+               2 * (in_1 * in_7 +
+                    in_3 * in_5)) in
+dlet output_9 :=  2 * (in_4 * in_5 +
+                    in_3 * in_6 +
+                    in_2 * in_7 +
+                    in_1 * in_8 +
+                    in_0 * in_9) in
+dlet output_10 := 2 * (in_5 * in_5 +
+                    in_4 * in_6 +
+                    in_2 * in_8 +
+               2 * (in_3 * in_7 +
+                    in_1 * in_9)) in
+dlet output_11 := 2 * (in_5 * in_6 +
+                    in_4 * in_7 +
+                    in_3 * in_8 +
+                    in_2 * in_9) in
+dlet output_12 :=      in_6 * in_6 +
+               2 * (in_4 * in_8 +
+               2 * (in_5 * in_7 +
+                    in_3 * in_9)) in
+dlet output_13 := 2 * (in_6 * in_7 +
+                    in_5 * in_8 +
+                    in_4 * in_9) in
+dlet output_14 := 2 * (in_7 * in_7 +
+                    in_6 * in_8 +
+               2 *  in_5 * in_9) in
+dlet output_15 := 2 * (in_7 * in_8 +
+                    in_6 * in_9) in
+dlet output_16 :=      in_8 * in_8 +
+               4 *  in_7 * in_9 in
+dlet output_17 := 2 *  in_8 * in_9 in
+dlet output_18 := 2 *  in_9 * in_9 in
+dlet output_8 := output_8 + output_18 << 4 in
+dlet output_8 := output_8 + output_18 << 1 in
+dlet output_8 := output_8 + output_18 in
+dlet output_7 := output_7 + output_17 << 4 in
+dlet output_7 := output_7 + output_17 << 1 in
+dlet output_7 := output_7 + output_17 in
+dlet output_6 := output_6 + output_16 << 4 in
+dlet output_6 := output_6 + output_16 << 1 in
+dlet output_6 := output_6 + output_16 in
+dlet output_5 := output_5 + output_15 << 4 in
+dlet output_5 := output_5 + output_15 << 1 in
+dlet output_5 := output_5 + output_15 in
+dlet output_4 := output_4 + output_14 << 4 in
+dlet output_4 := output_4 + output_14 << 1 in
+dlet output_4 := output_4 + output_14 in
+dlet output_3 := output_3 + output_13 << 4 in
+dlet output_3 := output_3 + output_13 << 1 in
+dlet output_3 := output_3 + output_13 in
+dlet output_2 := output_2 + output_12 << 4 in
+dlet output_2 := output_2 + output_12 << 1 in
+dlet output_2 := output_2 + output_12 in
+dlet output_1 := output_1 + output_11 << 4 in
+dlet output_1 := output_1 + output_11 << 1 in
+dlet output_1 := output_1 + output_11 in
+dlet output_0 := output_0 + output_10 << 4 in
+dlet output_0 := output_0 + output_10 << 1 in
+dlet output_0 := output_0 + output_10 in
+(output_9, output_8, output_7, output_6, output_5, output_4, output_3, output_2, output_1, output_0)
+            ).
+
+  Definition upper_bound_of_exponent : option (Z -> Z) := None.
+  Definition allowable_bit_widths : option (list nat) := None.
+  Definition freeze_extra_allowable_bit_widths : option (list nat) := None.
+  Ltac extra_prove_mul_eq := idtac.
+  Ltac extra_prove_square_eq := idtac.
+End Curve.
diff --git a/src/Specific/X25519/C32/ReificationTypes.v b/src/Specific/X25519/C32/ReificationTypes.v
new file mode 100644
index 000000000..83ea345e5
--- /dev/null
+++ b/src/Specific/X25519/C32/ReificationTypes.v
@@ -0,0 +1,51 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
+Local Open Scope Z_scope.
+
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Util.FixedWordSizes.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Specific.X25519.C32.ArithmeticSynthesisTest.
+
+Section BoundedField.
+  Local Coercion Z.of_nat : nat >-> Z.
+
+  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
+  Let length_lw := Eval compute in List.length limb_widths.
+
+  Local Notation b_of exp := {| lower := 0 ; upper := P.upper_bound_of_exponent exp |}%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] *)
+  (* The definition [bounds_exp] is a tuple-version of the
+     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
+     the approximate base-2 exponent of the bounds on the limb in that
+     position. *)
+  Let bounds_exp : Tuple.tuple Z length_lw
+    := Eval compute in
+        Tuple.from_list length_lw limb_widths eq_refl.
+  Let bounds : Tuple.tuple zrange length_lw
+    := Eval compute in
+        Tuple.map (fun e => b_of e) bounds_exp.
+
+  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
+  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
+  Let feZ : Type := tuple Z sz.
+  Definition feW : Type := Eval cbv [lgbitwidth] in tuple (wordT lgbitwidth) sz.
+  Definition feW_bounded : feW -> Prop
+    := Eval cbv [bounds] in fun w => is_bounded_by None bounds (map wordToZ w).
+  Definition feBW : Type := Eval cbv [bitwidth bounds] in BoundedWord sz bitwidth bounds.
+
+  Lemma feBW_bounded (a : feBW)
+    : 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m.
+  Proof.
+    destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
+    revert H.
+    cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt]; cbn [fst snd].
+    repeat match goal with
+           | [ |- context[wt ?n] ]
+             => let v := (eval compute in (wt n)) in change (wt n) with v
+           end.
+    intro; destruct_head'_and.
+    omega.
+  Qed.
+End BoundedField.
diff --git a/src/Specific/X25519/C32/femul.v b/src/Specific/X25519/C32/femul.v
index 19959f19e..9d69dc9f3 100644
--- a/src/Specific/X25519/C32/femul.v
+++ b/src/Specific/X25519/C32/femul.v
@@ -1,59 +1,27 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
+Require Import Crypto.Specific.X25519.C32.ReificationTypes.
+Require Import Crypto.Specific.X25519.C32.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Specific.ArithmeticSynthesisTest32.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Tactics.MoveLetIn.
-Import ListNotations.
-
+Require Import Crypto.Util.BoundedWord.
 Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
-
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
-Section BoundedField25p5.
-  Local Coercion Z.of_nat : nat >-> Z.
-
-  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-  Let length_lw := Eval compute in List.length limb_widths.
+Local Definition phi : feBW -> F m :=
+  fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
 
-  Local Notation b_of exp := {| lower := 0 ; upper := 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] *)
-  (* The definition [bounds_exp] is a tuple-version of the
-     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
-     the approximate base-2 exponent of the bounds on the limb in that
-     position. *)
-  Let bounds_exp : Tuple.tuple Z length_lw
-    := Eval compute in
-        Tuple.from_list length_lw limb_widths eq_refl.
-  Let bounds : Tuple.tuple zrange length_lw
-    := Eval compute in
-        Tuple.map (fun e => b_of e) bounds_exp.
-
-  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
-  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
-  Let feZ : Type := tuple Z sz.
-  Let feW : Type := tuple (wordT lgbitwidth) sz.
-  Let feBW : Type := BoundedWord sz bitwidth bounds.
-  Let phi : feBW -> F m :=
-    fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
-  (* TODO : change this to field once field isomorphism happens *)
-  Definition mul :
-    { mul : feBW -> feBW -> feBW
-    | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }.
-  Proof.
-    start_preglue.
-    do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime.
-    all:fin_preglue.
-    (* jgross start here! *)
-    (*Set Ltac Profiling.*)
-    Time refine_reflectively32. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
-    (*Show Ltac Profile.*)
-    (* total time:     19.632s
+(* TODO : change this to field once field isomorphism happens *)
+Definition mul :
+  { mul : feBW -> feBW -> feBW
+  | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }.
+Proof.
+  start_preglue.
+  do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime.
+  all:fin_preglue.
+  (* jgross start here! *)
+  (*Set Ltac Profiling.*)
+  Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
+  (*Show Ltac Profile.*)
+  (* total time:     19.632s
 
  tactic                                   local  total   calls       max
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
@@ -94,7 +62,5 @@ Section BoundedField25p5.
  │ ├─ReflectiveTactics.abstract_cbv_inte   2.7%   3.3%       1    0.648s
  │ └─ReflectiveTactics.abstract_cbv_rhs    2.0%   2.7%       1    0.532s
  └─Glue.refine_to_reflective_glue ------   0.0%   2.2%       1    0.436s
-*)
-  Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
-
-End BoundedField25p5.
+   *)
+Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
diff --git a/src/Specific/X25519/C32/fesquare.v b/src/Specific/X25519/C32/fesquare.v
index 00bf7c08b..32dc4acf9 100644
--- a/src/Specific/X25519/C32/fesquare.v
+++ b/src/Specific/X25519/C32/fesquare.v
@@ -1,59 +1,27 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
+Require Import Crypto.Specific.X25519.C32.ReificationTypes.
+Require Import Crypto.Specific.X25519.C32.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Specific.ArithmeticSynthesisTest32.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Tactics.MoveLetIn.
-Import ListNotations.
-
+Require Import Crypto.Util.BoundedWord.
 Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
-
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
-Section BoundedField25p5.
-  Local Coercion Z.of_nat : nat >-> Z.
-
-  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-  Let length_lw := Eval compute in List.length limb_widths.
+Local Definition phi : feBW -> F m :=
+  fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
 
-  Local Notation b_of exp := {| lower := 0 ; upper := 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] *)
-  (* The definition [bounds_exp] is a tuple-version of the
-     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
-     the approximate base-2 exponent of the bounds on the limb in that
-     position. *)
-  Let bounds_exp : Tuple.tuple Z length_lw
-    := Eval compute in
-        Tuple.from_list length_lw limb_widths eq_refl.
-  Let bounds : Tuple.tuple zrange length_lw
-    := Eval compute in
-        Tuple.map (fun e => b_of e) bounds_exp.
-
-  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
-  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
-  Let feZ : Type := tuple Z sz.
-  Let feW : Type := tuple (wordT lgbitwidth) sz.
-  Let feBW : Type := BoundedWord sz bitwidth bounds.
-  Let phi : feBW -> F m :=
-    fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
-  (* TODO : change this to field once field isomorphism happens *)
-  Definition square :
-    { square : feBW -> feBW
-    | forall a, phi (square a) = F.mul (phi a) (phi a) }.
-  Proof.
-    start_preglue.
-    do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime.
-    all:fin_preglue.
-    (* jgross start here! *)
-    (*Set Ltac Profiling.*)
-    Time refine_reflectively32. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
-    (*Show Ltac Profile.*)
-    (* total time:     19.632s
+(* TODO : change this to field once field isomorphism happens *)
+Definition square :
+  { square : feBW -> feBW
+  | forall a, phi (square a) = F.mul (phi a) (phi a) }.
+Proof.
+  start_preglue.
+  do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime.
+  all:fin_preglue.
+  (* jgross start here! *)
+  (*Set Ltac Profiling.*)
+  Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
+  (*Show Ltac Profile.*)
+  (* total time:     19.632s
 
  tactic                                   local  total   calls       max
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
@@ -94,7 +62,5 @@ Section BoundedField25p5.
  │ ├─ReflectiveTactics.abstract_cbv_inte   2.7%   3.3%       1    0.648s
  │ └─ReflectiveTactics.abstract_cbv_rhs    2.0%   2.7%       1    0.532s
  └─Glue.refine_to_reflective_glue ------   0.0%   2.2%       1    0.436s
-*)
-  Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
-
-End BoundedField25p5.
+   *)
+Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
diff --git a/src/Specific/X25519/C64/ArithmeticSynthesisTest.v b/src/Specific/X25519/C64/ArithmeticSynthesisTest.v
new file mode 100644
index 000000000..f4ef43f20
--- /dev/null
+++ b/src/Specific/X25519/C64/ArithmeticSynthesisTest.v
@@ -0,0 +1,250 @@
+Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
+Require Import Coq.Lists.List. Import ListNotations.
+Require Import Crypto.Arithmetic.Core. Import B.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Arithmetic.Saturated.Freeze.
+Require Crypto.Specific.CurveParameters.
+Require Import Crypto.Specific.X25519.C64.CurveParameters.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Crypto.Util.Tuple.
+Require Import Crypto.Util.QUtil.
+Local Notation tuple := Tuple.tuple.
+Local Open Scope list_scope.
+Local Open Scope Z_scope.
+Local Coercion Z.of_nat : nat >-> Z.
+
+Module P := CurveParameters.FillCurveParameters Curve.
+
+Section Ops.
+  Local Infix "^" := tuple : type_scope.
+
+  (* These definitions will need to be passed as Ltac arguments (or
+  cleverly inferred) when things are eventually automated *)
+  Definition sz : nat := P.compute P.sz.
+  Definition bitwidth : Z := P.compute P.bitwidth.
+  Definition s : Z := P.unfold P.s. (* don't want to compute, e.g., [2^255] *)
+  Definition c : list B.limb := P.compute P.c.
+  Definition carry_chain1 := P.compute P.carry_chain1.
+  Definition carry_chain2 := P.compute P.carry_chain2.
+
+  Definition a24 := P.compute P.a24.
+  Definition coef_div_modulus : nat := P.compute P.coef_div_modulus.
+  (* These definitions are inferred from those above *)
+  Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *)
+  Section wt.
+    Import QArith Qround.
+    Local Coercion QArith_base.inject_Z : Z >-> Q.
+    Definition wt (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i).
+  End wt.
+  Definition sz2 := Eval vm_compute in ((sz * 2) - 1)%nat.
+  Definition m_enc :=
+    Eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c)).
+  Definition coef := (* subtraction coefficient *)
+    Eval vm_compute in
+      ((fix addm (acc: Z^sz) (ctr : nat) : Z^sz :=
+         match ctr with
+         | O => acc
+         | S n => addm (Positional.add_cps wt acc m_enc id) n
+        end) (Positional.zeros sz) coef_div_modulus).
+  Definition coef_mod : mod_eq m (Positional.eval (n:=sz) wt coef) 0 := eq_refl.
+  Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed.
+  Lemma wt_nonzero i : wt i <> 0.
+  Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed.
+  Lemma wt_divides i : wt (S i) / wt i > 0.
+  Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed.
+  Lemma wt_divides' i : wt (S i) / wt i <> 0.
+  Proof. symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides. Qed.
+  Definition wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0 := wt_divides' i.
+  Definition wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0 := wt_divides' i.
+
+  Local Ltac solve_constant_sig :=
+    lazymatch goal with
+    | [ |- { c : Z^?sz | Positional.Fdecode (m:=?M) ?wt c = ?v } ]
+      => let t := (eval vm_compute in
+                      (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt (F.to_Z (m:=M) v))) in
+         (exists t; vm_decide)
+    end.
+
+  Definition zero_sig :
+    { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F}.
+  Proof.
+    solve_constant_sig.
+  Defined.
+
+  Definition one_sig :
+    { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F}.
+  Proof.
+    solve_constant_sig.
+  Defined.
+
+  Definition a24_sig :
+    { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m a24 }.
+  Proof.
+    solve_constant_sig.
+  Defined.
+
+  Definition add_sig :
+    { add : (Z^sz -> Z^sz -> Z^sz)%type |
+               forall a b : Z^sz,
+                 let eval := Positional.Fdecode (m:=m) wt in
+                 eval (add a b) = (eval a  + eval b)%F }.
+  Proof.
+    eexists; cbv beta zeta; intros a b.
+    pose proof wt_nonzero.
+    let x := constr:(
+        Positional.add_cps (n := sz) wt a b id) in
+    solve_op_F wt x. reflexivity.
+  Defined.
+
+  Definition sub_sig :
+    {sub : (Z^sz -> Z^sz -> Z^sz)%type |
+               forall a b : Z^sz,
+                 let eval := Positional.Fdecode (m:=m) wt in
+                 eval (sub a b) = (eval a - eval b)%F}.
+  Proof.
+    eexists; cbv beta zeta; intros a b.
+    pose proof wt_nonzero.
+    let x := constr:(
+         Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in
+    solve_op_F wt x. reflexivity.
+  Defined.
+
+  Definition opp_sig :
+    {opp : (Z^sz -> Z^sz)%type |
+               forall a : Z^sz,
+                 let eval := Positional.Fdecode (m := m) wt in
+                 eval (opp a) = F.opp (eval a)}.
+  Proof.
+    eexists; cbv beta zeta; intros a.
+    pose proof wt_nonzero.
+    let x := constr:(
+         Positional.opp_cps (n:=sz) (coef := coef) wt a id) in
+    solve_op_F wt x. reflexivity.
+  Defined.
+
+  Definition mul_sig :
+    {mul : (Z^sz -> Z^sz -> Z^sz)%type |
+               forall a b : Z^sz,
+                 let eval := Positional.Fdecode (m := m) wt in
+                 eval (mul a b) = (eval a  * eval b)%F}.
+  Proof.
+    eexists; cbv beta zeta; intros a b.
+    pose proof wt_nonzero.
+    let x := constr:(
+         Positional.mul_cps (n:=sz) (m:=sz2) wt a b
+                            (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in
+    solve_op_F wt x.
+    P.default_mul;
+      P.extra_prove_mul_eq;
+      break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring.
+  Defined.
+
+  Definition square_sig :
+    {square : (Z^sz -> Z^sz)%type |
+               forall a : Z^sz,
+                 let eval := Positional.Fdecode (m := m) wt in
+                 eval (square a) = (eval a  * eval a)%F}.
+  Proof.
+    eexists; cbv beta zeta; intros a.
+    pose proof wt_nonzero.
+    let x := constr:(
+         Positional.mul_cps (n:=sz) (m:=sz2) wt a a
+                            (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in
+    solve_op_F wt x.
+    P.default_square;
+      P.extra_prove_square_eq;
+      break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring.
+  Defined.
+
+  (* Performs a full carry loop (as specified by carry_chain) *)
+  Definition carry_sig :
+    {carry : (Z^sz -> Z^sz)%type |
+               forall a : Z^sz,
+                 let eval := Positional.Fdecode (m := m) wt in
+                 eval (carry a) = eval a}.
+  Proof.
+    eexists; cbv beta zeta; intros a.
+    pose proof wt_nonzero. pose proof wt_divides_chain1.
+    pose proof div_mod. pose proof wt_divides_chain2.
+    let x := constr:(
+               Positional.chained_carries_cps (n:=sz) (div:=div)(modulo:=modulo) wt a carry_chain1
+                  (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r
+                  (fun rrr => Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt rrr carry_chain2 id
+             ))) in
+    solve_op_F wt x. reflexivity.
+  Defined.
+
+  Section PreFreeze.
+    Lemma wt_pos i : wt i > 0.
+    Proof. eapply pow_ceil_mul_nat_pos; vm_decide. Qed.
+
+    Lemma wt_multiples i : wt (S i) mod (wt i) = 0.
+    Proof. apply pow_ceil_mul_nat_multiples; vm_decide. Qed.
+  End PreFreeze.
+
+  Hint Opaque freeze : uncps.
+  Hint Rewrite freeze_id : uncps.
+
+  Definition freeze_sig :
+    {freeze : (Z^sz -> Z^sz)%type |
+     forall a : Z^sz,
+         (0 <= Positional.eval wt a < 2 * Z.pos m)->
+                 let eval := Positional.Fdecode (m := m) wt in
+                 eval (freeze a) = eval a}.
+  Proof.
+    eexists; cbv beta zeta; intros a ?.
+    pose proof wt_nonzero. pose proof wt_pos.
+    pose proof div_mod. pose proof wt_divides.
+    pose proof wt_multiples.
+    pose proof div_correct. pose proof modulo_correct.
+    let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in
+    F_mod_eq;
+      transitivity (Positional.eval wt x); repeat autounfold;
+        [ | autorewrite with uncps push_id push_basesystem_eval;
+            rewrite eval_freeze with (c:=c);
+            try eassumption; try omega; try reflexivity;
+            try solve [auto using B.Positional.select_id,
+                       B.Positional.eval_select, zselect_correct];
+            vm_decide].
+   cbv[mod_eq]; apply f_equal2;
+     [  | reflexivity ]; apply f_equal.
+   cbv - [runtime_opp runtime_add runtime_mul runtime_shr runtime_and Let_In Z.add_get_carry Z.zselect].
+   reflexivity.
+  Defined.
+
+  Definition ring :=
+    (Ring.ring_by_isomorphism
+         (F := F m)
+         (H := Z^sz)
+         (phi := Positional.Fencode wt)
+         (phi' := Positional.Fdecode wt)
+         (zero := proj1_sig zero_sig)
+         (one := proj1_sig one_sig)
+         (opp := proj1_sig opp_sig)
+         (add := proj1_sig add_sig)
+         (sub := proj1_sig sub_sig)
+         (mul := proj1_sig mul_sig)
+         (phi'_zero := proj2_sig zero_sig)
+         (phi'_one := proj2_sig one_sig)
+         (phi'_opp := proj2_sig opp_sig)
+         (Positional.Fdecode_Fencode_id
+            (sz_nonzero := sz_nonzero)
+            (div_mod := div_mod)
+            wt eq_refl wt_nonzero wt_divides')
+         (Positional.eq_Feq_iff wt)
+         (proj2_sig add_sig)
+         (proj2_sig sub_sig)
+         (proj2_sig mul_sig)
+      ).
+
+(*
+Eval cbv [proj1_sig add_sig] in (proj1_sig add_sig).
+Eval cbv [proj1_sig sub_sig] in (proj1_sig sub_sig).
+Eval cbv [proj1_sig opp_sig] in (proj1_sig opp_sig).
+Eval cbv [proj1_sig mul_sig] in (proj1_sig mul_sig).
+Eval cbv [proj1_sig carry_sig] in (proj1_sig carry_sig).
+*)
+
+End Ops.
diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v
new file mode 100644
index 000000000..1e15eea24
--- /dev/null
+++ b/src/Specific/X25519/C64/CurveParameters.v
@@ -0,0 +1,65 @@
+Require Import Crypto.Specific.CurveParameters.
+Require Import Crypto.Util.LetIn.
+
+(***
+Modulus : 2^255-19
+Base: 51
+***)
+
+Module Curve <: CurveParameters.
+  Definition sz : nat := 5%nat.
+  Definition bitwidth : Z := 64.
+  Definition s : Z := 2^255.
+  Definition c : list limb := [(1, 19)].
+  Definition carry_chain1 := Eval vm_compute in Some (seq 0 (pred sz)).
+  Definition carry_chain2 := Some [0;1]%nat.
+
+  Definition a24 := 121665%Z.
+  Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
+
+  Definition mul_code : option (Z^sz -> Z^sz -> Z^sz)
+    := Some (fun a b =>
+      (* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
+      let '(r4, r3, r2, r1, r0) := a in
+      let '(s4, s3, s2, s1, s0) := b in
+      dlet t0  :=  r0 * s0 in
+      dlet t1  :=  r0 * s1 + r1 * s0 in
+      dlet t2  :=  r0 * s2 + r2 * s0 + r1 * s1 in
+      dlet t3  :=  r0 * s3 + r3 * s0 + r1 * s2 + r2 * s1 in
+      dlet t4  :=  r0 * s4 + r4 * s0 + r3 * s1 + r1 * s3 + r2 * s2 in
+
+      dlet r4' := r4*19 in
+      dlet r1' := r1*19 in
+      dlet r2' := r2*19 in
+      dlet r3' := r3*19 in
+
+      dlet t0 := t0 + r4' * s1 + r1' * s4 + r2' * s3 + r3' * s2 in
+      dlet t1 := t1 + r4' * s2 + r2' * s4 + r3' * s3 in
+      dlet t2 := t2 + r4' * s3 + r3' * s4 in
+      dlet t3 := t3 + r4' * s4 in
+      (t4, t3, t2, t1, t0)
+            ).
+
+  Definition square_code : option (Z^sz -> Z^sz)
+    := Some (fun a =>
+      (* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
+      let '(r4, r3, r2, r1, r0) := a in
+      dlet d0 := r0 * 2 in
+      dlet d1 := r1 * 2 in
+      dlet d2 := r2 * 2 * 19 in
+      dlet d419 := r4 * 19 in
+      dlet d4 := d419 * 2 in
+      dlet t0 := r0 * r0 + d4 * r1 + d2 * r3        in
+      dlet t1 := d0 * r1 + d4 * r2 + r3 * (r3 * 19) in
+      dlet t2 := d0 * r2 + r1 * r1 + d4 * r3        in
+      dlet t3 := d0 * r3 + d1 * r2 + r4 * d419      in
+      dlet t4 := d0 * r4 + d1 * r3 + r2 * r2        in
+      (t4, t3, t2, t1, t0)
+            ).
+
+  Definition upper_bound_of_exponent : option (Z -> Z) := None.
+  Definition allowable_bit_widths : option (list nat) := None.
+  Definition freeze_extra_allowable_bit_widths : option (list nat) := None.
+  Ltac extra_prove_mul_eq := idtac.
+  Ltac extra_prove_square_eq := idtac.
+End Curve.
diff --git a/src/Specific/X25519/C64/ReificationTypes.v b/src/Specific/X25519/C64/ReificationTypes.v
new file mode 100644
index 000000000..6050404c8
--- /dev/null
+++ b/src/Specific/X25519/C64/ReificationTypes.v
@@ -0,0 +1,51 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
+Local Open Scope Z_scope.
+
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Util.FixedWordSizes.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest.
+
+Section BoundedField.
+  Local Coercion Z.of_nat : nat >-> Z.
+
+  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
+  Let length_lw := Eval compute in List.length limb_widths.
+
+  Local Notation b_of exp := {| lower := 0 ; upper := P.upper_bound_of_exponent exp |}%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] *)
+  (* The definition [bounds_exp] is a tuple-version of the
+     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
+     the approximate base-2 exponent of the bounds on the limb in that
+     position. *)
+  Let bounds_exp : Tuple.tuple Z length_lw
+    := Eval compute in
+        Tuple.from_list length_lw limb_widths eq_refl.
+  Let bounds : Tuple.tuple zrange length_lw
+    := Eval compute in
+        Tuple.map (fun e => b_of e) bounds_exp.
+
+  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
+  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
+  Let feZ : Type := tuple Z sz.
+  Definition feW : Type := Eval cbv [lgbitwidth] in tuple (wordT lgbitwidth) sz.
+  Definition feW_bounded : feW -> Prop
+    := Eval cbv [bounds] in fun w => is_bounded_by None bounds (map wordToZ w).
+  Definition feBW : Type := Eval cbv [bitwidth bounds] in BoundedWord sz bitwidth bounds.
+
+  Lemma feBW_bounded (a : feBW)
+    : 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m.
+  Proof.
+    destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
+    revert H.
+    cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt]; cbn [fst snd].
+    repeat match goal with
+           | [ |- context[wt ?n] ]
+             => let v := (eval compute in (wt n)) in change (wt n) with v
+           end.
+    intro; destruct_head'_and.
+    omega.
+  Qed.
+End BoundedField.
diff --git a/src/Specific/X25519/C64/femul.v b/src/Specific/X25519/C64/femul.v
index 155bcf9e1..aad541ff6 100644
--- a/src/Specific/X25519/C64/femul.v
+++ b/src/Specific/X25519/C64/femul.v
@@ -1,59 +1,27 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
+Require Import Crypto.Specific.X25519.C64.ReificationTypes.
+Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Specific.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Tactics.MoveLetIn.
-Import ListNotations.
-
+Require Import Crypto.Util.BoundedWord.
 Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
-
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
-Section BoundedField25p5.
-  Local Coercion Z.of_nat : nat >-> Z.
-
-  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-  Let length_lw := Eval compute in List.length limb_widths.
+Local Definition phi : feBW -> F m :=
+  fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
 
-  Local Notation b_of exp := {| lower := 0 ; upper := 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] *)
-  (* The definition [bounds_exp] is a tuple-version of the
-     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
-     the approximate base-2 exponent of the bounds on the limb in that
-     position. *)
-  Let bounds_exp : Tuple.tuple Z length_lw
-    := Eval compute in
-        Tuple.from_list length_lw limb_widths eq_refl.
-  Let bounds : Tuple.tuple zrange length_lw
-    := Eval compute in
-        Tuple.map (fun e => b_of e) bounds_exp.
-
-  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
-  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
-  Let feZ : Type := tuple Z sz.
-  Let feW : Type := tuple (wordT lgbitwidth) sz.
-  Let feBW : Type := BoundedWord sz bitwidth bounds.
-  Let phi : feBW -> F m :=
-    fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
-  (* TODO : change this to field once field isomorphism happens *)
-  Definition mul :
-    { mul : feBW -> feBW -> feBW
-    | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }.
-  Proof.
-    start_preglue.
-    do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime.
-    all:fin_preglue.
-    (* jgross start here! *)
-    (*Set Ltac Profiling.*)
-    Time refine_reflectively. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
-    (*Show Ltac Profile.*)
-    (* total time:     19.632s
+(* TODO : change this to field once field isomorphism happens *)
+Definition mul :
+  { mul : feBW -> feBW -> feBW
+  | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }.
+Proof.
+  start_preglue.
+  do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime.
+  all:fin_preglue.
+  (* jgross start here! *)
+  (*Set Ltac Profiling.*)
+  Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
+  (*Show Ltac Profile.*)
+  (* total time:     19.632s
 
  tactic                                   local  total   calls       max
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
@@ -94,7 +62,5 @@ Section BoundedField25p5.
  │ ├─ReflectiveTactics.abstract_cbv_inte   2.7%   3.3%       1    0.648s
  │ └─ReflectiveTactics.abstract_cbv_rhs    2.0%   2.7%       1    0.532s
  └─Glue.refine_to_reflective_glue ------   0.0%   2.2%       1    0.436s
-*)
-  Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
-
-End BoundedField25p5.
+   *)
+Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
diff --git a/src/Specific/X25519/C64/fesquare.v b/src/Specific/X25519/C64/fesquare.v
index 0bba90c68..a88ea6e24 100644
--- a/src/Specific/X25519/C64/fesquare.v
+++ b/src/Specific/X25519/C64/fesquare.v
@@ -1,59 +1,27 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
+Require Import Crypto.Specific.X25519.C64.ReificationTypes.
+Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Specific.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Tactics.MoveLetIn.
-Import ListNotations.
-
+Require Import Crypto.Util.BoundedWord.
 Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
-
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
-Section BoundedField25p5.
-  Local Coercion Z.of_nat : nat >-> Z.
-
-  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-  Let length_lw := Eval compute in List.length limb_widths.
+Local Definition phi : feBW -> F m :=
+  fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
 
-  Local Notation b_of exp := {| lower := 0 ; upper := 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] *)
-  (* The definition [bounds_exp] is a tuple-version of the
-     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
-     the approximate base-2 exponent of the bounds on the limb in that
-     position. *)
-  Let bounds_exp : Tuple.tuple Z length_lw
-    := Eval compute in
-        Tuple.from_list length_lw limb_widths eq_refl.
-  Let bounds : Tuple.tuple zrange length_lw
-    := Eval compute in
-        Tuple.map (fun e => b_of e) bounds_exp.
-
-  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
-  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
-  Let feZ : Type := tuple Z sz.
-  Let feW : Type := tuple (wordT lgbitwidth) sz.
-  Let feBW : Type := BoundedWord sz bitwidth bounds.
-  Let phi : feBW -> F m :=
-    fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
-  (* TODO : change this to field once field isomorphism happens *)
-  Definition square :
-    { square : feBW -> feBW
-    | forall a, phi (square a) = F.mul (phi a) (phi a) }.
-  Proof.
-    start_preglue.
-    do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime.
-    all:fin_preglue.
-    (* jgross start here! *)
-    (*Set Ltac Profiling.*)
-    Time refine_reflectively. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
-    (*Show Ltac Profile.*)
-    (* total time:     19.632s
+(* TODO : change this to field once field isomorphism happens *)
+Definition square :
+  { square : feBW -> feBW
+  | forall a, phi (square a) = F.mul (phi a) (phi a) }.
+Proof.
+  start_preglue.
+  do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime.
+  all:fin_preglue.
+  (* jgross start here! *)
+  (*Set Ltac Profiling.*)
+  Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
+  (*Show Ltac Profile.*)
+  (* total time:     19.632s
 
  tactic                                   local  total   calls       max
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
@@ -94,7 +62,5 @@ Section BoundedField25p5.
  │ ├─ReflectiveTactics.abstract_cbv_inte   2.7%   3.3%       1    0.648s
  │ └─ReflectiveTactics.abstract_cbv_rhs    2.0%   2.7%       1    0.532s
  └─Glue.refine_to_reflective_glue ------   0.0%   2.2%       1    0.436s
-*)
-  Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
-
-End BoundedField25p5.
+   *)
+Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v
index 7b9062a6b..62f728dd5 100644
--- a/src/Specific/X25519/C64/ladderstep.v
+++ b/src/Specific/X25519/C64/ladderstep.v
@@ -1,146 +1,118 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
 Require Import Coq.Classes.Morphisms.
-Local Open Scope Z_scope.
 
+Require Import Crypto.Specific.X25519.C64.ReificationTypes.
+Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Specific.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
+Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.
+
+Require Import Crypto.Util.FixedWordSizes.
+Require Import Coq.ZArith.BinIntDef.
+Require Import Crypto.Curves.Montgomery.XZ.
+Require Import Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift.
+Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Tactics.MoveLetIn.
 Require Import Crypto.Util.Tactics.SetEvars.
 Require Import Crypto.Util.Tactics.SubstEvars.
 Require Import Crypto.Util.Tactics.ETransitivity.
-Require Import Crypto.Curves.Montgomery.XZ.
-Import ListNotations.
-
-Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
-
-Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-
-Section BoundedField25p5.
-  Local Coercion Z.of_nat : nat >-> Z.
-
-  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-  Let length_lw := Eval compute in List.length limb_widths.
-
-  Local Notation b_of exp := {| lower := 0 ; upper := 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] *)
-  (* The definition [bounds_exp] is a tuple-version of the
-     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
-     the approximate base-2 exponent of the bounds on the limb in that
-     position. *)
-  Let bounds_exp : Tuple.tuple Z length_lw
-    := Eval compute in
-        Tuple.from_list length_lw limb_widths eq_refl.
-  Let bounds : Tuple.tuple zrange length_lw
-    := Eval compute in
-        Tuple.map (fun e => b_of e) bounds_exp.
-
-  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
-  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
-  Let feZ : Type := tuple Z sz.
-  Let feW : Type := tuple (wordT lgbitwidth) sz.
-  Let feW_bounded : feW -> Prop
-    := fun w => is_bounded_by None bounds (map wordToZ w).
-  Let feBW : Type := BoundedWord sz bitwidth bounds.
-  Let phi : feW -> F m :=
-    fun x => B.Positional.Fdecode wt (Tuple.map wordToZ x).
+Require Import Crypto.Util.Notations.
 
-  (** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
-  Definition FMxzladderstep := @M.donnaladderstep (F m) F.add F.sub F.mul.
+Local Definition phi : feW -> F m :=
+  fun x => B.Positional.Fdecode wt (Tuple.map wordToZ x).
 
-  Section with_notations.
-    Local Infix "+" := (proj1_sig add_sig).
-    Local Notation "a * b" := (proj1_sig carry_sig (proj1_sig mul_sig a b)).
-    Local Notation "x ^ 2" := (proj1_sig carry_sig (proj1_sig square_sig x)).
-    Local Infix "-" := (proj1_sig sub_sig).
-    Definition Mxzladderstep a24 x1 Q Q'
-      := match Q, Q' with
-         | (x, z), (x', z') =>
-           dlet origx := x in
-           dlet x := x + z in
-           dlet z := origx - z in
-           dlet origx' := x' in
-           dlet x' := x' + z' in
-           dlet z' := origx' - z' in
-           dlet xx' := x' * z in
-           dlet zz' := x * z' in
-           dlet origx' := xx' in
-           dlet xx' := xx' + zz' in
-           dlet zz' := origx' - zz' in
-           dlet x3 := xx'^2 in
-           dlet zzz' := zz'^2 in
-           dlet z3 := zzz' * x1 in
-           dlet xx := x^2 in
-           dlet zz := z^2 in
-           dlet x2 := xx * zz in
-           dlet zz := xx - zz in
-           dlet zzz := zz * a24 in
-           dlet zzz := zzz + xx in
-           dlet z2 := zz * zzz in
-           ((x2, z2), (x3, z3))%core
-         end.
-  End with_notations.
+(** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
+Definition FMxzladderstep := @M.donnaladderstep (F m) F.add F.sub F.mul.
 
+Section with_notations.
+  Local Infix "+" := (proj1_sig add_sig).
+  Local Notation "a * b" := (proj1_sig carry_sig (proj1_sig mul_sig a b)).
+  Local Notation "x ^ 2" := (proj1_sig carry_sig (proj1_sig square_sig x)).
+  Local Infix "-" := (proj1_sig sub_sig).
+  Definition Mxzladderstep a24 x1 Q Q'
+    := match Q, Q' with
+       | (x, z), (x', z') =>
+         dlet origx := x in
+         dlet x := x + z in
+         dlet z := origx - z in
+         dlet origx' := x' in
+         dlet x' := x' + z' in
+         dlet z' := origx' - z' in
+         dlet xx' := x' * z in
+         dlet zz' := x * z' in
+         dlet origx' := xx' in
+         dlet xx' := xx' + zz' in
+         dlet zz' := origx' - zz' in
+         dlet x3 := xx'^2 in
+         dlet zzz' := zz'^2 in
+         dlet z3 := zzz' * x1 in
+         dlet xx := x^2 in
+         dlet zz := z^2 in
+         dlet x2 := xx * zz in
+         dlet zz := xx - zz in
+         dlet zzz := zz * a24 in
+         dlet zzz := zzz + xx in
+         dlet z2 := zz * zzz in
+         ((x2, z2), (x3, z3))%core
+       end.
+End with_notations.
 
-  (** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
-  Definition Mxzladderstep_sig
-    : { xzladderstep : tuple Z sz -> tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz * (tuple Z sz * tuple Z sz)
-      | forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }.
-  Proof.
-    exists Mxzladderstep.
-    intros a24 x1 Q Q' eval.
-    cbv [Mxzladderstep FMxzladderstep M.donnaladderstep].
-    destruct Q, Q'; cbv [map map' fst snd Let_In eval].
-    repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig square_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig).
-    reflexivity.
-  Defined.
 
-  (* TODO : change this to field once field isomorphism happens *)
-  Definition xzladderstep :
-    { xzladderstep : feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW)
-    | forall x1 Q Q',
-        let xz := xzladderstep x1 Q Q' in
-        let eval := B.Positional.Fdecode wt in
-        feW_bounded x1
-        -> feW_bounded (fst Q) /\ feW_bounded (snd Q)
-        -> feW_bounded (fst Q') /\ feW_bounded (snd Q')
-        -> ((feW_bounded (fst (fst xz)) /\ feW_bounded (snd (fst xz)))
-            /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz))))
-           /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }.
-  Proof.
-    start_preglue.
-    unmap_map_tuple ().
-    do_rewrite_with_sig_1arg Mxzladderstep_sig.
-    cbv [Mxzladderstep M.xzladderstep a24_sig]; cbn [proj1_sig].
-    do_set_sigs ().
-    cbv_runtime.
-    all:finish_conjoined_preglue ().
-    (* jgross start here! *)
-    Set Ltac Profiling.
-    (*
-    Time Glue.refine_to_reflective_glue (64::128::nil)%nat%list.
-    Time ReflectiveTactics.refine_with_pipeline_correct default.
-    { Time ReflectiveTactics.do_reify. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. }
-    { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. }
-    { Time SubstLet.subst_let; clear; abstract vm_cast_no_check (eq_refl true). }
-    { Time SubstLet.subst_let; clear; vm_compute; reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. }
-    { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. }
-    { Time abstract ReflectiveTactics.handle_bounds_from_hyps. }
-    { Time abstract ReflectiveTactics.handle_boundedness_side_condition. }
-     *)
-    Time refine_reflectively.
-    Show Ltac Profile.
-  Time Defined.
+(** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
+Definition Mxzladderstep_sig
+  : { xzladderstep : tuple Z sz -> tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz * (tuple Z sz * tuple Z sz)
+    | forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }.
+Proof.
+  exists Mxzladderstep.
+  intros a24 x1 Q Q' eval.
+  cbv [Mxzladderstep FMxzladderstep M.donnaladderstep].
+  destruct Q, Q'; cbv [map map' fst snd Let_In eval].
+  repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig square_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig).
+  reflexivity.
+Defined.
 
-Time End BoundedField25p5.
+(* TODO : change this to field once field isomorphism happens *)
+Definition xzladderstep :
+  { xzladderstep : feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW)
+  | forall x1 Q Q',
+      let xz := xzladderstep x1 Q Q' in
+      let eval := B.Positional.Fdecode wt in
+      feW_bounded x1
+      -> feW_bounded (fst Q) /\ feW_bounded (snd Q)
+      -> feW_bounded (fst Q') /\ feW_bounded (snd Q')
+      -> ((feW_bounded (fst (fst xz)) /\ feW_bounded (snd (fst xz)))
+          /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz))))
+         /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }.
+Proof.
+  start_preglue.
+  unmap_map_tuple ().
+  do_rewrite_with_sig_1arg Mxzladderstep_sig.
+  cbv [Mxzladderstep M.xzladderstep a24_sig]; cbn [proj1_sig].
+  do_set_sigs ().
+  cbv_runtime.
+  all:finish_conjoined_preglue ().
+  (* jgross start here! *)
+  Set Ltac Profiling.
+  (*
+  Time Glue.refine_to_reflective_glue P.allowable_bit_widths.
+  Time ReflectiveTactics.refine_with_pipeline_correct default.
+  { Time ReflectiveTactics.do_reify. }
+  { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+  { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+  { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+  { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+  { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+  { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. }
+  { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. }
+  { Time SubstLet.subst_let; clear; abstract vm_cast_no_check (eq_refl true). }
+  { Time SubstLet.subst_let; clear; vm_compute; reflexivity. }
+  { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. }
+  { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. }
+  { Time abstract ReflectiveTactics.handle_bounds_from_hyps. }
+  { Time abstract ReflectiveTactics.handle_boundedness_side_condition. }
+   *)
+  Time refine_reflectively_gen P.allowable_bit_widths default.
+  Show Ltac Profile.
+Time Defined.
diff --git a/src/Specific/X25519/C64/ladderstepDisplay.log b/src/Specific/X25519/C64/ladderstepDisplay.log
index 73c47fa40..56c67eeb2 100644
--- a/src/Specific/X25519/C64/ladderstepDisplay.log
+++ b/src/Specific/X25519/C64/ladderstepDisplay.log
@@ -1,4 +1,4 @@
-λ x x0 x1 x2 x3 : word64 * word64 * word64 * word64 * word64,
+λ x x0 x1 x2 x3 : ReificationTypes.feW,
 let (a, b) := Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x15, x16, x14, x12, x10, (x25, x26, x24, x22, x20, (x33, x34, x32, x30, x28)), (x43, x44, x42, x40, x38, (x51, x52, x50, x48, x46)))%core,
@@ -367,4 +367,4 @@ let (a, b) := Interp-η
 (let (a0, b0) := a in
 (a0, b0), let (a0, b0) := b in
 (a0, b0))%core
-     : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * (word64 * word64 * word64 * word64 * word64) * (word64 * word64 * word64 * word64 * word64 * (word64 * word64 * word64 * word64 * word64))
+     : ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW * ReificationTypes.feW * (ReificationTypes.feW * ReificationTypes.feW)