5 files changed, 590 insertions, 108 deletions

diff --git a/src/Specific/X25519/C32/ArithmeticSynthesisTest.v b/src/Specific/X25519/C32/ArithmeticSynthesisTest.v
new file mode 100644
index 000000000..6b1d5ee11
--- /dev/null
+++ b/src/Specific/X25519/C32/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.C32.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/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) *)