Reorgainze synthesis framework files into a Framework folder

8 files changed, 1544 insertions, 0 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesisFramework.v b/src/Specific/Framework/ArithmeticSynthesisFramework.v
new file mode 100644
index 000000000..77624ed41
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesisFramework.v
@@ -0,0 +1,565 @@
+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.Framework.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.
+
+Require Import Crypto.Util.Tactics.PoseTermWithName.
+Require Import Crypto.Util.Tactics.CacheTerm.
+
+Local Notation tuple := Tuple.tuple.
+Local Open Scope list_scope.
+Local Open Scope Z_scope.
+Local Coercion Z.of_nat : nat >-> Z.
+
+Hint Opaque freeze : uncps.
+Hint Rewrite freeze_id : uncps.
+
+Module Export Exports.
+  Export Coq.setoid_ring.ZArithRing.
+End Exports.
+
+Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParameters).
+  Module P := CurveParameters.FillCurveParameters Curve.
+
+  Local Infix "^" := tuple : type_scope.
+
+  (* emacs for adjusting definitions *)
+  (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) : \([A-Za-z0-9_]+\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\4^J  cache_term_with_type_by^J      \2^J      ltac:(let v := P.do_compute \3 in exact v)^J      \1.):  *)
+  (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) : \([A-Za-z0-9_]+\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\4^J  cache_term_with_type_by^J      \2^J      ltac:(let v := P.do_compute \3 in exact v)^J      \1.):  *)
+  (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) : \([A-Za-z0-9_ \.]*\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\4^J  cache_term_with_type_by^J      (\2)^J      ltac:(let v := P.do_compute \3 in exact v)^J      \1.): *)
+  (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\3^J  let v := P.do_compute \2 in cache_term v \1.):  *)
+
+  (* These definitions will need to be passed as Ltac arguments (or
+  cleverly inferred) when things are eventually automated *)
+  Ltac pose_sz sz :=
+    cache_term_with_type_by
+      nat
+      ltac:(let v := P.do_compute P.sz in exact v)
+             sz.
+  Ltac pose_bitwidth bitwidth :=
+    cache_term_with_type_by
+      Z
+      ltac:(let v := P.do_compute P.bitwidth in exact v)
+             bitwidth.
+  Ltac pose_s s := (* don't want to compute, e.g., [2^255] *)
+    cache_term_with_type_by
+      Z
+      ltac:(let v := P.do_unfold P.s in exact v)
+             s.
+  Ltac pose_c c :=
+    cache_term_with_type_by
+      (list B.limb)
+      ltac:(let v := P.do_compute P.c in exact v)
+             c.
+  Ltac pose_carry_chain1 carry_chain1 :=
+    let v := P.do_compute P.carry_chain1 in
+    cache_term v carry_chain1.
+  Ltac pose_carry_chain2 carry_chain2 :=
+    let v := P.do_compute P.carry_chain2 in
+    cache_term v carry_chain2.
+
+  Ltac pose_a24 a24 :=
+    let v := P.do_compute P.a24 in
+    cache_term v a24.
+  Ltac pose_coef_div_modulus coef_div_modulus :=
+    cache_term_with_type_by
+      nat
+      ltac:(let v := P.do_compute P.coef_div_modulus in exact v)
+             coef_div_modulus.
+  (* These definitions are inferred from those above *)
+  Ltac pose_m s c m := (* modulus *)
+    let v := (eval vm_compute in (Z.to_pos (s - Associational.eval c))) in
+    cache_term v m.
+  Section wt.
+    Import QArith Qround.
+    Local Coercion QArith_base.inject_Z : Z >-> Q.
+    Definition wt_gen (m : positive) (sz : nat) (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i).
+  End wt.
+  Ltac pose_wt m sz wt :=
+    let v := (eval cbv [wt_gen] in (wt_gen m sz)) in
+    cache_term v wt.
+  Ltac pose_sz2 sz sz2 :=
+    let v := (eval vm_compute in ((sz * 2) - 1)%nat) in
+    cache_term v sz2.
+  Ltac pose_m_enc sz s c wt m_enc :=
+    let v := (eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c))) in
+    cache_term v m_enc.
+  Ltac pose_coef sz wt m_enc coef_div_modulus coef := (* subtraction coefficient *)
+    let v := (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)) in
+    cache_term v coef.
+
+  Ltac pose_coef_mod sz wt m coef coef_mod :=
+    cache_term_with_type_by
+      (mod_eq m (Positional.eval (n:=sz) wt coef) 0)
+      ltac:(exact eq_refl)
+             coef_mod.
+  Ltac pose_sz_nonzero sz sz_nonzero :=
+    cache_proof_with_type_by
+      (sz <> 0%nat)
+      ltac:(vm_decide_no_check)
+             sz_nonzero.
+  Ltac pose_wt_nonzero wt wt_nonzero :=
+    cache_proof_with_type_by
+      (forall i, wt i <> 0)
+      ltac:(eapply pow_ceil_mul_nat_nonzero; vm_decide_no_check)
+             wt_nonzero.
+  Ltac pose_wt_nonneg wt wt_nonneg :=
+    cache_proof_with_type_by
+      (forall i, 0 <= wt i)
+      ltac:(apply pow_ceil_mul_nat_nonneg; vm_decide_no_check)
+             wt_nonneg.
+  Ltac pose_wt_divides wt wt_divides :=
+    cache_proof_with_type_by
+      (forall i, wt (S i) / wt i > 0)
+      ltac:(apply pow_ceil_mul_nat_divide; vm_decide_no_check)
+             wt_divides.
+  Ltac pose_wt_divides' wt wt_divides wt_divides' :=
+    cache_proof_with_type_by
+      (forall i, wt (S i) / wt i <> 0)
+      ltac:(symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides)
+             wt_divides'.
+  Ltac pose_wt_divides_chain1 wt carry_chain1 wt_divides' wt_divides_chain1 :=
+    cache_term_with_type_by
+      (forall i (H:In i carry_chain1), wt (S i) / wt i <> 0)
+      ltac:(let i := fresh "i" in intros i ?; exact (wt_divides' i))
+             wt_divides_chain1.
+  Ltac pose_wt_divides_chain2 wt carry_chain2 wt_divides' wt_divides_chain2 :=
+    cache_term_with_type_by
+      (forall i (H:In i carry_chain2), wt (S i) / wt i <> 0)
+      ltac:(let i := fresh "i" in intros i ?; exact (wt_divides' i))
+             wt_divides_chain2.
+
+  Local Ltac solve_constant_sig :=
+    idtac;
+    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.
+
+  Ltac pose_zero_sig sz m wt zero_sig :=
+    cache_term_with_type_by
+      { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F}
+      solve_constant_sig
+      zero_sig.
+
+  Ltac pose_one_sig sz m wt one_sig :=
+    cache_term_with_type_by
+      { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F}
+      solve_constant_sig
+      one_sig.
+
+  Ltac pose_a24_sig sz m wt a24 a24_sig :=
+    cache_term_with_type_by
+      { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m P.a24 }
+      solve_constant_sig
+      a24_sig.
+
+  Ltac pose_add_sig sz m wt wt_nonzero add_sig :=
+    cache_term_with_type_by
+      { 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 }
+      ltac:(idtac;
+            let a := fresh "a" in
+            let b := fresh "b" in
+            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)
+             add_sig.
+
+  Ltac pose_sub_sig sz m wt wt_nonzero coef sub_sig :=
+    cache_term_with_type_by
+      {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}
+      ltac:(idtac;
+            let a := fresh "a" in
+            let b := fresh "b" in
+            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)
+             sub_sig.
+
+  Ltac pose_opp_sig sz m wt wt_nonzero coef opp_sig :=
+    cache_term_with_type_by
+      {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)}
+      ltac:(idtac;
+            let a := fresh in
+            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)
+             opp_sig.
+
+  Ltac pose_mul_sig sz m wt s c sz2 wt_nonzero mul_sig :=
+    cache_term_with_type_by
+      {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}
+      ltac:(idtac;
+            let a := fresh "a" in
+            let b := fresh "b" in
+            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)
+             mul_sig.
+
+  Ltac pose_square_sig sz m wt s c sz2 wt_nonzero square_sig :=
+    cache_term_with_type_by
+      {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}
+      ltac:(idtac;
+            let a := fresh "a" in
+            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)
+             square_sig.
+
+  (* Performs a full carry loop (as specified by carry_chain) *)
+  Ltac pose_carry_sig sz m wt s c carry_chain1 carry_chain2 wt_nonzero wt_divides_chain1 wt_divides_chain2 carry_sig :=
+    cache_term_with_type_by
+      {carry : (Z^sz -> Z^sz)%type |
+       forall a : Z^sz,
+         let eval := Positional.Fdecode (m := m) wt in
+         eval (carry a) = eval a}
+      ltac:(idtac;
+            let a := fresh "a" in
+            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)
+             carry_sig.
+
+  Ltac pose_wt_pos wt wt_pos :=
+    cache_proof_with_type_by
+      (forall i, wt i > 0)
+      ltac:(eapply pow_ceil_mul_nat_pos; vm_decide_no_check)
+             wt_pos.
+
+  Ltac pose_wt_multiples wt wt_multiples :=
+    cache_proof_with_type_by
+      (forall i, wt (S i) mod (wt i) = 0)
+      ltac:(apply pow_ceil_mul_nat_multiples; vm_decide_no_check)
+             wt_multiples.
+
+
+  (* kludge to get around name clashes in the following, and the fact
+     that the python script cares about argument names *)
+  Local Ltac rewrite_eval_freeze_with_c c' :=
+    rewrite eval_freeze with (c:=c').
+
+  Ltac pose_freeze_sig sz m wt c m_enc bitwidth wt_nonzero wt_pos wt_divides wt_multiples freeze_sig :=
+    cache_term_with_type_by
+      {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}
+      ltac:(let a := fresh "a" in
+            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)
+             freeze_sig.
+
+  Ltac pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_sig add_sig sub_sig mul_sig ring :=
+    cache_term
+      (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)
+      )
+      ring.
+
+(*
+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).
+*)
+
+  (**
+<<
+#!/usr/bin/env python
+from __future__ import with_statement
+import re
+
+with open('ArithmeticSynthesisFramework.v', 'r') as f:
+    lines = f.readlines()
+
+header = 'Ltac pose_'
+
+fns = [(name, args.strip())
+       for line in lines
+       if line.strip()[:len(header)] == header
+       for name, args in re.findall('Ltac pose_([^ ]*' + ') ([A-Za-z0-9_\' ]*' + ')', line.strip())]
+
+print(r'''  Ltac get_ArithmeticSynthesis_package _ :=
+    %s'''
+    % '\n    '.join('let %s := fresh "%s" in' % (name, name) for name, args in fns))
+print('    ' + '\n    '.join('let %s := pose_%s %s in' % (name, name, args) for name, args in fns))
+print('    constr:((%s)).' % ', '.join(name for name, args in fns))
+print(r'''
+  Ltac make_ArithmeticSynthesis_package _ :=
+    lazymatch goal with
+    | [ |- { T : _ & T } ] => eexists
+    | [ |- _ ] => idtac
+    end;
+    let pkg := get_ArithmeticSynthesis_package () in
+    exact pkg.
+End MakeArithmeticSynthesisTestTactics.
+
+Module Type ArithmeticSynthesisPrePackage.
+  Parameter ArithmeticSynthesis_package' : { T : _ & T }.
+  Parameter ArithmeticSynthesis_package : projT1 ArithmeticSynthesis_package'.
+End ArithmeticSynthesisPrePackage.
+
+Module MakeArithmeticSynthesisTest (AP : ArithmeticSynthesisPrePackage).
+  Ltac get_MakeArithmeticSynthesisTest_package _ := eval hnf in AP.ArithmeticSynthesis_package.
+  Ltac AS_reduce_proj x :=
+    eval cbv beta iota zeta in x.
+''')
+terms = ', '.join(name for name, args in fns)
+for name, args in fns:
+    print("  Ltac get_%s _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(%s) := pkg in %s)." % (name, terms, name))
+    print("  Notation %s := (ltac:(let v := get_%s () in exact v)) (only parsing)." % (name, name))
+print('End MakeArithmeticSynthesisTest.')
+>> **)
+  Ltac get_ArithmeticSynthesis_package _ :=
+    let sz := fresh "sz" in
+    let bitwidth := fresh "bitwidth" in
+    let s := fresh "s" in
+    let c := fresh "c" in
+    let carry_chain1 := fresh "carry_chain1" in
+    let carry_chain2 := fresh "carry_chain2" in
+    let a24 := fresh "a24" in
+    let coef_div_modulus := fresh "coef_div_modulus" in
+    let m := fresh "m" in
+    let wt := fresh "wt" in
+    let sz2 := fresh "sz2" in
+    let m_enc := fresh "m_enc" in
+    let coef := fresh "coef" in
+    let coef_mod := fresh "coef_mod" in
+    let sz_nonzero := fresh "sz_nonzero" in
+    let wt_nonzero := fresh "wt_nonzero" in
+    let wt_nonneg := fresh "wt_nonneg" in
+    let wt_divides := fresh "wt_divides" in
+    let wt_divides' := fresh "wt_divides'" in
+    let wt_divides_chain1 := fresh "wt_divides_chain1" in
+    let wt_divides_chain2 := fresh "wt_divides_chain2" in
+    let zero_sig := fresh "zero_sig" in
+    let one_sig := fresh "one_sig" in
+    let a24_sig := fresh "a24_sig" in
+    let add_sig := fresh "add_sig" in
+    let sub_sig := fresh "sub_sig" in
+    let opp_sig := fresh "opp_sig" in
+    let mul_sig := fresh "mul_sig" in
+    let square_sig := fresh "square_sig" in
+    let carry_sig := fresh "carry_sig" in
+    let wt_pos := fresh "wt_pos" in
+    let wt_multiples := fresh "wt_multiples" in
+    let freeze_sig := fresh "freeze_sig" in
+    let ring := fresh "ring" in
+    let sz := pose_sz sz in
+    let bitwidth := pose_bitwidth bitwidth in
+    let s := pose_s s in
+    let c := pose_c c in
+    let carry_chain1 := pose_carry_chain1 carry_chain1 in
+    let carry_chain2 := pose_carry_chain2 carry_chain2 in
+    let a24 := pose_a24 a24 in
+    let coef_div_modulus := pose_coef_div_modulus coef_div_modulus in
+    let m := pose_m s c m in
+    let wt := pose_wt m sz wt in
+    let sz2 := pose_sz2 sz sz2 in
+    let m_enc := pose_m_enc sz s c wt m_enc in
+    let coef := pose_coef sz wt m_enc coef_div_modulus coef in
+    let coef_mod := pose_coef_mod sz wt m coef coef_mod in
+    let sz_nonzero := pose_sz_nonzero sz sz_nonzero in
+    let wt_nonzero := pose_wt_nonzero wt wt_nonzero in
+    let wt_nonneg := pose_wt_nonneg wt wt_nonneg in
+    let wt_divides := pose_wt_divides wt wt_divides in
+    let wt_divides' := pose_wt_divides' wt wt_divides wt_divides' in
+    let wt_divides_chain1 := pose_wt_divides_chain1 wt carry_chain1 wt_divides' wt_divides_chain1 in
+    let wt_divides_chain2 := pose_wt_divides_chain2 wt carry_chain2 wt_divides' wt_divides_chain2 in
+    let zero_sig := pose_zero_sig sz m wt zero_sig in
+    let one_sig := pose_one_sig sz m wt one_sig in
+    let a24_sig := pose_a24_sig sz m wt a24 a24_sig in
+    let add_sig := pose_add_sig sz m wt wt_nonzero add_sig in
+    let sub_sig := pose_sub_sig sz m wt wt_nonzero coef sub_sig in
+    let opp_sig := pose_opp_sig sz m wt wt_nonzero coef opp_sig in
+    let mul_sig := pose_mul_sig sz m wt s c sz2 wt_nonzero mul_sig in
+    let square_sig := pose_square_sig sz m wt s c sz2 wt_nonzero square_sig in
+    let carry_sig := pose_carry_sig sz m wt s c carry_chain1 carry_chain2 wt_nonzero wt_divides_chain1 wt_divides_chain2 carry_sig in
+    let wt_pos := pose_wt_pos wt wt_pos in
+    let wt_multiples := pose_wt_multiples wt wt_multiples in
+    let freeze_sig := pose_freeze_sig sz m wt c m_enc bitwidth wt_nonzero wt_pos wt_divides wt_multiples freeze_sig in
+    let ring := pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_sig add_sig sub_sig mul_sig ring in
+    constr:((sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring)).
+
+  Ltac make_ArithmeticSynthesis_package _ :=
+    lazymatch goal with
+    | [ |- { T : _ & T } ] => eexists
+    | [ |- _ ] => idtac
+    end;
+    let pkg := get_ArithmeticSynthesis_package () in
+    exact pkg.
+End MakeArithmeticSynthesisTestTactics.
+
+Module Type ArithmeticSynthesisPrePackage.
+  Parameter ArithmeticSynthesis_package' : { T : _ & T }.
+  Parameter ArithmeticSynthesis_package : projT1 ArithmeticSynthesis_package'.
+End ArithmeticSynthesisPrePackage.
+
+Module MakeArithmeticSynthesisTest (AP : ArithmeticSynthesisPrePackage).
+  Ltac get_MakeArithmeticSynthesisTest_package _ := eval hnf in AP.ArithmeticSynthesis_package.
+  Ltac AS_reduce_proj x :=
+    eval cbv beta iota zeta in x.
+
+  Ltac get_sz _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz).
+  Notation sz := (ltac:(let v := get_sz () in exact v)) (only parsing).
+  Ltac get_bitwidth _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in bitwidth).
+  Notation bitwidth := (ltac:(let v := get_bitwidth () in exact v)) (only parsing).
+  Ltac get_s _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in s).
+  Notation s := (ltac:(let v := get_s () in exact v)) (only parsing).
+  Ltac get_c _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in c).
+  Notation c := (ltac:(let v := get_c () in exact v)) (only parsing).
+  Ltac get_carry_chain1 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_chain1).
+  Notation carry_chain1 := (ltac:(let v := get_carry_chain1 () in exact v)) (only parsing).
+  Ltac get_carry_chain2 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_chain2).
+  Notation carry_chain2 := (ltac:(let v := get_carry_chain2 () in exact v)) (only parsing).
+  Ltac get_a24 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in a24).
+  Notation a24 := (ltac:(let v := get_a24 () in exact v)) (only parsing).
+  Ltac get_coef_div_modulus _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef_div_modulus).
+  Notation coef_div_modulus := (ltac:(let v := get_coef_div_modulus () in exact v)) (only parsing).
+  Ltac get_m _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in m).
+  Notation m := (ltac:(let v := get_m () in exact v)) (only parsing).
+  Ltac get_wt _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt).
+  Notation wt := (ltac:(let v := get_wt () in exact v)) (only parsing).
+  Ltac get_sz2 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz2).
+  Notation sz2 := (ltac:(let v := get_sz2 () in exact v)) (only parsing).
+  Ltac get_m_enc _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in m_enc).
+  Notation m_enc := (ltac:(let v := get_m_enc () in exact v)) (only parsing).
+  Ltac get_coef _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef).
+  Notation coef := (ltac:(let v := get_coef () in exact v)) (only parsing).
+  Ltac get_coef_mod _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef_mod).
+  Notation coef_mod := (ltac:(let v := get_coef_mod () in exact v)) (only parsing).
+  Ltac get_sz_nonzero _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz_nonzero).
+  Notation sz_nonzero := (ltac:(let v := get_sz_nonzero () in exact v)) (only parsing).
+  Ltac get_wt_nonzero _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_nonzero).
+  Notation wt_nonzero := (ltac:(let v := get_wt_nonzero () in exact v)) (only parsing).
+  Ltac get_wt_nonneg _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_nonneg).
+  Notation wt_nonneg := (ltac:(let v := get_wt_nonneg () in exact v)) (only parsing).
+  Ltac get_wt_divides _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides).
+  Notation wt_divides := (ltac:(let v := get_wt_divides () in exact v)) (only parsing).
+  Ltac get_wt_divides' _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides').
+  Notation wt_divides' := (ltac:(let v := get_wt_divides' () in exact v)) (only parsing).
+  Ltac get_wt_divides_chain1 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides_chain1).
+  Notation wt_divides_chain1 := (ltac:(let v := get_wt_divides_chain1 () in exact v)) (only parsing).
+  Ltac get_wt_divides_chain2 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides_chain2).
+  Notation wt_divides_chain2 := (ltac:(let v := get_wt_divides_chain2 () in exact v)) (only parsing).
+  Ltac get_zero_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in zero_sig).
+  Notation zero_sig := (ltac:(let v := get_zero_sig () in exact v)) (only parsing).
+  Ltac get_one_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in one_sig).
+  Notation one_sig := (ltac:(let v := get_one_sig () in exact v)) (only parsing).
+  Ltac get_a24_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in a24_sig).
+  Notation a24_sig := (ltac:(let v := get_a24_sig () in exact v)) (only parsing).
+  Ltac get_add_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in add_sig).
+  Notation add_sig := (ltac:(let v := get_add_sig () in exact v)) (only parsing).
+  Ltac get_sub_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sub_sig).
+  Notation sub_sig := (ltac:(let v := get_sub_sig () in exact v)) (only parsing).
+  Ltac get_opp_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in opp_sig).
+  Notation opp_sig := (ltac:(let v := get_opp_sig () in exact v)) (only parsing).
+  Ltac get_mul_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in mul_sig).
+  Notation mul_sig := (ltac:(let v := get_mul_sig () in exact v)) (only parsing).
+  Ltac get_square_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in square_sig).
+  Notation square_sig := (ltac:(let v := get_square_sig () in exact v)) (only parsing).
+  Ltac get_carry_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_sig).
+  Notation carry_sig := (ltac:(let v := get_carry_sig () in exact v)) (only parsing).
+  Ltac get_wt_pos _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_pos).
+  Notation wt_pos := (ltac:(let v := get_wt_pos () in exact v)) (only parsing).
+  Ltac get_wt_multiples _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_multiples).
+  Notation wt_multiples := (ltac:(let v := get_wt_multiples () in exact v)) (only parsing).
+  Ltac get_freeze_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in freeze_sig).
+  Notation freeze_sig := (ltac:(let v := get_freeze_sig () in exact v)) (only parsing).
+  Ltac get_ring _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in ring).
+  Notation ring := (ltac:(let v := get_ring () in exact v)) (only parsing).
+End MakeArithmeticSynthesisTest.
diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v
new file mode 100644
index 000000000..aa679a4d3
--- /dev/null
+++ b/src/Specific/Framework/CurveParameters.v
@@ -0,0 +1,114 @@
+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).
+  Ltac do_compute v :=
+    let v' := (eval vm_compute in v) in v'.
+  Notation compute v
+    := (ltac:(let v' := do_compute 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/Framework/IntegrationTestDisplayCommon.v b/src/Specific/Framework/IntegrationTestDisplayCommon.v
new file mode 100644
index 000000000..a3bf52d85
--- /dev/null
+++ b/src/Specific/Framework/IntegrationTestDisplayCommon.v
@@ -0,0 +1,24 @@
+Require Import Crypto.Util.Sigma.Lift.
+Require Import Crypto.Util.Sigma.Associativity.
+Require Import Crypto.Util.Sigma.MapProjections.
+Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.Eta.
+Require Export Coq.ZArith.ZArith.
+Require Export Crypto.Util.LetIn.
+Require Export Crypto.Util.FixedWordSizes.
+Require Export Crypto.Compilers.Syntax.
+Require Export Crypto.Specific.Framework.IntegrationTestDisplayCommonTactics.
+Require Export Crypto.Compilers.Z.HexNotationConstants.
+Require Export Crypto.Util.Notations.
+Require Export Crypto.Compilers.Z.CNotations.
+
+Global Arguments Pos.to_nat !_ / .
+Global Arguments InterpEta {_ _ _ _ _}.
+Global Set Printing Width 2000000.
+
+Notation "'Interp-η' f x" := (Eta.InterpEta f x) (format "'Interp-η' '//' f '//' x", at level 200, f at next level, x at next level).
+Notation ReturnType := (interp_flat_type _).
+Notation "'let' ( a , b ) := c 'in' d" := (let (a, b) := c in d) (at level 200, d at level 200, format "'let'  ( a ,  b )  :=  c  'in' '//' d").
+
+Require Export Coq.Unicode.Utf8. (* for better line breaks at function display; must come last *)
diff --git a/src/Specific/Framework/IntegrationTestDisplayCommonTactics.v b/src/Specific/Framework/IntegrationTestDisplayCommonTactics.v
new file mode 100644
index 000000000..2b15616fe
--- /dev/null
+++ b/src/Specific/Framework/IntegrationTestDisplayCommonTactics.v
@@ -0,0 +1,149 @@
+Require Import Crypto.Util.Sigma.Lift.
+Require Import Crypto.Util.Sigma.Associativity.
+Require Import Crypto.Util.Sigma.MapProjections.
+Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.Eta.
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.FixedWordSizes.
+Require Import Crypto.Compilers.Syntax.
+Require Export Crypto.Util.Notations.
+
+Global Arguments Pos.to_nat !_ / .
+
+Ltac display_helper_gen f make_hole :=
+  let display_helper f := display_helper_gen f make_hole in
+  let do_make_hole _ :=
+      match goal with
+      | [ |- ?T ] => let h := make_hole T in
+                     refine h
+      end in
+  let t := type of f in
+  lazymatch (eval hnf in t) with
+  | forall _ : ?A, ?B
+    => let x := fresh "x" in
+       lazymatch (eval hnf in A) with
+       | @sig ?A ?P
+         => lazymatch (eval hnf in A) with
+            | sig _
+              => let f' := constr:(fun x : A => f (exist P x ltac:(do_make_hole ()))) in
+                 display_helper f'
+            | _
+              => refine (fun x : A => _);
+                 let f' := constr:(f (exist P x ltac:(do_make_hole ()))) in
+                 display_helper f'
+            end
+       | _
+         => lazymatch A with
+            | prod ?A ?B
+              => let f' := constr:(fun (a : A) (b : B) => f (a, b)%core) in
+                 display_helper f'
+            | _
+              => refine (fun x : A => _);
+                 let f' := constr:(f x) in
+                 display_helper f'
+            end
+       end
+  | @sig ?A _
+    => lazymatch (eval hnf in A) with
+       | sig _ => display_helper (proj1_sig f)
+       | _ => refine (proj1_sig f)
+       end
+  | _
+    => lazymatch t with
+       | prod _ _
+         => let a := fresh "a" in
+            let b := fresh "b" in
+            refine (let (a, b) := f in
+                    pair _ _);
+            [ display_helper a | display_helper b ]
+       | _ => refine f
+       end
+  end.
+Ltac display_helper f := display_helper_gen f ltac:(fun T => open_constr:(_)).
+Ltac display_helper_with_admit f :=
+  constr:(fun admit : forall T, T
+          => ltac:(display_helper_gen f ltac:(fun T => constr:(admit T)))).
+Ltac try_strip_admit f :=
+  lazymatch f with
+  | fun _ : forall T, T => ?P => P
+  | ?P => P
+  end.
+Ltac refine_display f :=
+  let do_red F := (eval cbv [f
+                               proj1_sig fst snd
+                               Tuple.map Tuple.map'
+                               Lift.lift1_sig Lift.lift2_sig Lift.lift3_sig Lift.lift4_sig Lift.lift4_sig_sig
+                               MapProjections.proj2_sig_map Associativity.sig_sig_assoc
+                               sig_conj_by_impl2
+                               sig_eq_trans_exist1 sig_R_trans_exist1 sig_eq_trans_rewrite_fun_exist1
+                               sig_R_trans_rewrite_fun_exist1
+                               adjust_tuple2_tuple2_sig
+                               Tuple.tuple Tuple.tuple'
+                               FixedWordSizes.wordT FixedWordSizes.word_case FixedWordSizes.ZToWord FixedWordSizes.word_case_dep
+                               Bounds.actual_logsz Bounds.round_up_to_in_list Bounds.option_min
+                               List.map List.filter List.fold_right List.fold_left
+                               Nat.leb Nat.min
+                               PeanoNat.Nat.log2 PeanoNat.Nat.log2_iter PeanoNat.Nat.pred
+                               Bounds.bounds_to_base_type
+                               interp_flat_type
+                               Z.leb Z.compare Pos.compare Pos.compare_cont
+                               ZRange.lower ZRange.upper
+                               BinPos.Pos.to_nat PeanoNat.Nat.pow
+                            ] in F) in
+  let ret := display_helper_with_admit (proj1_sig f) in
+  let ret := do_red ret in
+  let ret := lazymatch ret with
+             | context[match ?sz with O => _ | _ => _ end] => (eval cbv [sz] in ret)
+             | _ => ret
+             end in
+  let ret := (eval simpl @Z.to_nat in ret) in
+  let ret := (eval cbv [interp_flat_type] in ret) in
+  let ret := try_strip_admit ret in
+  refine ret.
+Tactic Notation "display" open_constr(f) :=
+  refine_display f.
+Notation display f := (ltac:(let v := f in display v)) (only parsing).
+
+(** Some helper tactics for actually pulling out the expression *)
+Ltac strip_InterpEta term :=
+  let retype e :=
+      lazymatch type of e with
+      | forall var, @Syntax.expr ?base_type_code ?op var ?T
+        => constr:(e : @Syntax.Expr base_type_code op T)
+      | _ => e
+      end in
+  lazymatch term with
+  | fun x : ?T => ?P
+    => let maybe_x := fresh x in
+       let probably_not_x := fresh maybe_x in
+       let not_x := fresh probably_not_x in
+       lazymatch
+         constr:(fun x : T
+                 => match P with
+                    | not_x => ltac:(let v := (eval cbv delta [not_x] in not_x) in
+                                     let v' := strip_InterpEta v in
+                                     exact v')
+                    end)
+       with
+       | fun _ => ?P => retype P
+       | ?P => retype P
+       end
+  | @Eta.InterpEta _ _ _ _ _ ?e
+    => e
+  | @Eta.InterpEta _ _ _ _ _ ?e _
+    => e
+  | let (a, b) := ?f in _
+    => f
+  | _ => let dummy := match goal with
+                      | _ => fail 1 "strip_InterpEta:" term
+                      end in
+         I
+  end.
+
+Ltac extract_Expr f :=
+  let k := constr:(ltac:(refine_display f)) in
+  let k := strip_InterpEta k in
+  k.
+Notation extract_Expr f := (ltac:(let v := f in let v := extract_Expr v in refine v)) (only parsing).
diff --git a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v
new file mode 100644
index 000000000..41bef884c
--- /dev/null
+++ b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v
@@ -0,0 +1,288 @@
+(*** XXX TODO MOVE ALL THINGS IN THIS FILE TO BETTER PLACES *)
+Require Import Coq.ZArith.BinInt.
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Sigma.Lift.
+Require Import Crypto.Util.Sigma.Associativity.
+Require Import Crypto.Util.Sigma.MapProjections.
+Require Import Crypto.Util.Tactics.MoveLetIn.
+Require Import Crypto.Util.Tactics.DestructHead.
+
+Definition adjust_tuple2_tuple2_sig {A P Q}
+           (v : { a : { a : tuple (tuple A 2) 2 | (P (fst (fst a)) /\ P (snd (fst a))) /\ (P (fst (snd a)) /\ P (snd (snd a))) }
+                | Q (exist _ _ (proj1 (proj1 (proj2_sig a))),
+                     exist _ _ (proj2 (proj1 (proj2_sig a))),
+                     (exist _ _ (proj1 (proj2 (proj2_sig a))),
+                      exist _ _ (proj2 (proj2 (proj2_sig a))))) })
+  : { a : tuple (tuple (@sig A P) 2) 2 | Q a }.
+Proof.
+  eexists.
+  exact (proj2_sig v).
+Defined.
+
+(** TODO MOVE ME *)
+(** The [eexists_sig_etransitivity_R R] tactic takes a goal of the form
+    [{ a | R (f a) b }], and splits it into two goals, [R ?b' b] and
+    [{ a | R (f a) ?b' }], where [?b'] is a fresh evar. *)
+Definition sig_R_trans_exist1 {B} (R : B -> B -> Prop) {HT : Transitive R} {A} (f : A -> B)
+           (b b' : B)
+           (pf : R b' b)
+           (y : { a : A | R (f a) b' })
+  : { a : A | R (f a) b }
+  := let 'exist a p := y in exist _ a (transitivity (R:=R) p pf).
+Ltac eexists_sig_etransitivity_R R :=
+  lazymatch goal with
+  | [ |- @sig ?A ?P ]
+    => let RT := type of R in
+       let B := lazymatch (eval hnf in RT) with ?B -> _ => B end in
+       let lem := constr:(@sig_R_trans_exist1 B R _ A _ _ : forall b' pf y, @sig A P) in
+       let lem := open_constr:(lem _) in
+       simple refine (lem _ _)
+  end.
+Tactic Notation "eexists_sig_etransitivity_R" open_constr(R) := eexists_sig_etransitivity_R R.
+(** The [eexists_sig_etransitivity] tactic takes a goal of the form
+      [{ a | f a = b }], and splits it into two goals, [?b' = b] and
+      [{ a | f a = ?b' }], where [?b'] is a fresh evar. *)
+Definition sig_eq_trans_exist1 {A B}
+  := @sig_R_trans_exist1 B (@eq B) _ A.
+Ltac eexists_sig_etransitivity :=
+  lazymatch goal with
+  | [ |- { a : ?A | @?f a = ?b } ]
+    => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in
+       simple refine (lem _ (_ : { a : A | _ }))
+  end.
+Definition sig_R_trans_rewrite_fun_exist1 {B} (R : B -> B -> Prop) {HT : Transitive R}
+{A} (f : A -> B) (b : B) (f' : A -> B)
+           (pf : forall a, R (f a) (f' a))
+           (y : { a : A | R (f' a) b })
+  : { a : A | R (f a) b }
+  := let 'exist a p := y in exist _ a (transitivity (R:=R) (pf a) p).
+Ltac eexists_sig_etransitivity_for_rewrite_fun_R R :=
+  lazymatch goal with
+  | [ |- @sig ?A ?P ]
+    => let RT := type of R in
+       let B := lazymatch (eval hnf in RT) with ?B -> _ => B end in
+       let lem := constr:(@sig_R_trans_rewrite_fun_exist1 B R _ A _ _ : forall f' pf y, @sig A P) in
+       let lem := open_constr:(lem _) in
+       simple refine (lem _ _); cbv beta
+  end.
+Tactic Notation "eexists_sig_etransitivity_for_rewrite_fun_R" open_constr(R)
+  := eexists_sig_etransitivity_for_rewrite_fun_R R.
+Definition sig_eq_trans_rewrite_fun_exist1 {A B} (f f' : A -> B)
+           (b : B)
+           (pf : forall a, f' a = f a)
+           (y : { a : A | f' a = b })
+  : { a : A | f a = b }
+  := let 'exist a p := y in exist _ a (eq_trans (eq_sym (pf a)) p).
+Ltac eexists_sig_etransitivity_for_rewrite_fun :=
+  lazymatch goal with
+  | [ |- { a : ?A | @?f a = ?b } ]
+    => let lem := open_constr:(@sig_eq_trans_rewrite_fun_exist1 A _ f _ b) in
+       simple refine (lem _ _); cbv beta
+  end.
+Definition sig_conj_by_impl2 {A} {P Q : A -> Prop} (H : forall a : A, Q a -> P a)
+           (H' : { a : A | Q a })
+  : { a : A | P a /\ Q a }
+  := let (a, p) := H' in exist _ a (conj (H a p) p).
+
+
+(** [apply_lift_sig] picks out which version of the [liftN_sig] lemma
+    to apply, and builds the appropriate arguments *)
+Ltac make_P_for_apply_lift_sig P :=
+  lazymatch P with
+  | fun (f : ?F) => forall (a : ?A), @?P f a
+    => constr:(fun (a : A)
+               => ltac:(lazymatch constr:(fun (f : F)
+                                          => ltac:(let v := (eval cbv beta in (P f a)) in
+                                                   lazymatch (eval pattern (f a) in v) with
+                                                   | ?k _ => exact k
+                                                   end))
+                        with
+                        | fun _ => ?P
+                          => let v := make_P_for_apply_lift_sig P in
+                             exact v
+                        end))
+  | _ => P
+  end.
+Ltac apply_lift_sig :=
+  let P := lazymatch goal with |- sig ?P => P end in
+  let P := make_P_for_apply_lift_sig P in
+  lazymatch goal with
+  | [ |- { f | forall a b c d e, _ } ]
+    => fail "apply_lift_sig does not yet support ≥ 5 binders"
+  | [ |- { f | forall (a : ?A) (b : ?B) (c : ?C) (d : ?D), _ } ]
+    => apply (@lift4_sig A B C D _ P)
+  | [ |- { f | forall (a : ?A) (b : ?B) (c : ?C), _ } ]
+    => apply (@lift3_sig A B C _ P)
+  | [ |- { f | forall (a : ?A) (b : ?B), _ } ]
+    => apply (@lift2_sig A B _ P)
+  | [ |- { f | forall (a : ?A), _ } ]
+    => apply (@lift1_sig A _ P)
+  | [ |- { f | _ } ]
+    => idtac
+  end.
+Ltac get_proj2_sig_map_arg_helper P :=
+  lazymatch P with
+  | (fun e => ?A -> @?B e)
+    => let B' := get_proj2_sig_map_arg_helper B in
+       uconstr:(A -> B')
+  | _ => uconstr:(_ : Prop)
+  end.
+Ltac get_proj2_sig_map_arg _ :=
+  lazymatch goal with
+  | [ |- { e : ?T | @?E e } ]
+    => let P := get_proj2_sig_map_arg_helper E in
+       uconstr:(fun e : T => P)
+  end.
+Ltac get_phi_for_preglue _ :=
+  lazymatch goal with
+  | [ |- { e | @?E e } ]
+    => lazymatch E with
+       | context[Tuple.map (Tuple.map ?phi) _ = _]
+         => phi
+       | context[?phi _ = _]
+         => phi
+       end
+  end.
+Ltac start_preglue :=
+  apply_lift_sig; intros; cbv beta iota zeta;
+  let phi := get_phi_for_preglue () in
+  let P' := get_proj2_sig_map_arg () in
+  refine (proj2_sig_map (P:=P') _ _);
+  [ let FINAL := fresh "FINAL" in
+    let a := fresh "a" in
+    intros a FINAL;
+    repeat (let H := fresh in intro H; specialize (FINAL H));
+    lazymatch goal with
+    | [ |- ?phi _ = ?RHS ]
+      => refine (@eq_trans _ _ _ RHS FINAL _); cbv [phi]; clear a FINAL
+    | [ |- _ /\ Tuple.map (Tuple.map ?phi) _ = _ ]
+      => split; cbv [phi]; [ refine (proj1 FINAL); shelve | ]
+    end
+  | cbv [phi] ].
+Ltac do_set_sig f_sig :=
+  let fZ := fresh f_sig in
+  set (fZ := proj1_sig f_sig);
+  context_to_dlet_in_rhs fZ;
+  try cbv beta iota delta [proj1_sig f_sig] in fZ;
+  cbv beta delta [fZ]; clear fZ;
+  cbv beta iota delta [fst snd].
+Ltac do_set_sig_1arg f_sig :=
+  let fZ := fresh f_sig in
+  set (fZ := proj1_sig f_sig);
+  context_to_dlet_in_rhs (fZ _);
+  try cbn beta iota delta [proj1_sig f_sig] in fZ;
+  try cbv [f_sig] in fZ;
+  cbv beta delta [fZ]; clear fZ;
+  cbv beta iota delta [fst snd].
+Ltac do_set_sigs _ :=
+  lazymatch goal with
+  | [ |- context[@proj1_sig ?a ?b ?f_sig] ]
+    => let fZ := fresh f_sig in
+       set (fZ := proj1_sig f_sig);
+       context_to_dlet_in_rhs fZ;
+       do_set_sigs (); (* we recurse before unfolding, because that's faster *)
+       try cbv beta iota delta [proj1_sig f_sig] in fZ;
+       cbv beta delta [fZ];
+       cbv beta iota delta [fst snd]
+  | _ => idtac
+  end.
+Ltac trim_after_do_rewrite_with_sig _ :=
+  repeat match goal with
+         | [ |- Tuple.map ?f _ = Tuple.map ?f _ ]
+           => apply f_equal
+         end.
+Ltac do_rewrite_with_sig_no_set_by f_sig by_tac :=
+  let lem := constr:(proj2_sig f_sig) in
+  let lemT := type of lem in
+  let lemT := (eval cbv beta zeta in lemT) in
+  rewrite <- (lem : lemT) by by_tac ();
+  trim_after_do_rewrite_with_sig ().
+Ltac do_rewrite_with_sig_by f_sig by_tac :=
+  do_rewrite_with_sig_no_set_by f_sig by_tac;
+  do_set_sig f_sig.
+Ltac do_rewrite_with_sig_1arg_by f_sig by_tac :=
+  do_rewrite_with_sig_no_set_by f_sig by_tac;
+  do_set_sig_1arg f_sig.
+Ltac do_rewrite_with_sig f_sig := do_rewrite_with_sig_by f_sig ltac:(fun _ => idtac).
+Ltac do_rewrite_with_sig_1arg f_sig := do_rewrite_with_sig_1arg_by f_sig ltac:(fun _ => idtac).
+Ltac do_rewrite_with_1sig_add_carry_by f_sig carry_sig by_tac :=
+  let fZ := fresh f_sig in
+  rewrite <- (proj2_sig f_sig) by by_tac ();
+  symmetry; rewrite <- (proj2_sig carry_sig) by by_tac (); symmetry;
+  pose (fun a => proj1_sig carry_sig (proj1_sig f_sig a)) as fZ;
+  lazymatch goal with
+  | [ |- context G[proj1_sig carry_sig (proj1_sig f_sig ?a)] ]
+    => let G' := context G[fZ a] in change G'
+  end;
+  context_to_dlet_in_rhs fZ; cbv beta delta [fZ];
+  try cbv beta iota delta [proj1_sig f_sig carry_sig];
+  cbv beta iota delta [fst snd].
+Ltac do_rewrite_with_1sig_add_carry f_sig carry_sig := do_rewrite_with_1sig_add_carry_by f_sig carry_sig ltac:(fun _ => idtac).
+Ltac do_rewrite_with_2sig_add_carry_by f_sig carry_sig by_tac :=
+  let fZ := fresh f_sig in
+  rewrite <- (proj2_sig f_sig) by by_tac ();
+  symmetry; rewrite <- (proj2_sig carry_sig) by by_tac (); symmetry;
+  pose (fun a b => proj1_sig carry_sig (proj1_sig f_sig a b)) as fZ;
+  lazymatch goal with
+  | [ |- context G[proj1_sig carry_sig (proj1_sig f_sig ?a ?b)] ]
+    => let G' := context G[fZ a b] in change G'
+  end;
+  context_to_dlet_in_rhs fZ; cbv beta delta [fZ];
+  try cbv beta iota delta [proj1_sig f_sig carry_sig];
+  cbv beta iota delta [fst snd].
+Ltac do_rewrite_with_2sig_add_carry f_sig carry_sig := do_rewrite_with_2sig_add_carry_by f_sig carry_sig ltac:(fun _ => idtac).
+Ltac unmap_map_tuple _ :=
+  repeat match goal with
+         | [ |- context[Tuple.map (n:=?N) (fun x : ?T => ?f (?g x))] ]
+           => 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
+  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)
+      end
+  | try subst_feW () ].
+Ltac fin_preglue :=
+  [ > reflexivity
+  | repeat 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)) ].
+
+Ltac factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t :=
+  let feBW_small := lazymatch goal with |- { f : ?feBW_small | _ } => feBW_small end in
+  Associativity.sig_sig_assoc;
+  apply sig_conj_by_impl2;
+  [ let H := fresh in
+    intros ? H;
+    try lazymatch goal with
+        | [ |- (?eval _ < _)%Z ]
+          => cbv [eval]
+        end;
+    rewrite H; clear H;
+    eapply Z.le_lt_trans;
+      [ apply Z.eq_le_incl, f_equal | apply op_bounded ];
+      [ repeat match goal with
+               | [ |- ?f ?x = ?g ?y ]
+                 => is_evar y; unify x y;
+                    apply (f_equal (fun fg => fg x))
+               end;
+        clear; abstract reflexivity
+      | .. ];
+      op_sig_side_conditions_t ()
+  | 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));
+    cbv [proj1_sig];
+    repeat match goal with
+           | [ H : feBW_small |- _ ] => destruct H as [? _]
+           end ].
diff --git a/src/Specific/Framework/LadderstepSynthesisFramework.v b/src/Specific/Framework/LadderstepSynthesisFramework.v
new file mode 100644
index 000000000..d6afb31eb
--- /dev/null
+++ b/src/Specific/Framework/LadderstepSynthesisFramework.v
@@ -0,0 +1,93 @@
+Require Import Coq.ZArith.BinIntDef.
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Curves.Montgomery.XZ.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Tactics.PoseTermWithName.
+Require Import Crypto.Util.Tactics.CacheTerm.
+
+(** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
+Definition FMxzladderstep {m} := @M.donnaladderstep (F m) F.add F.sub F.mul.
+
+Section with_notations.
+  Context sz (add sub mul : tuple Z sz -> tuple Z sz -> tuple Z sz)
+          (square carry : tuple Z sz -> tuple Z sz).
+  Local Infix "+" := add.
+  Local Notation "a * b" := (carry (mul a b)).
+  Local Notation "x ^ 2" := (carry (square x)).
+  Local Infix "-" := sub.
+  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? *)
+Ltac pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig :=
+  cache_term_with_type_by
+    { 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 (m:=m) (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }
+    ltac:((exists (Mxzladderstep sz (proj1_sig add_sig) (proj1_sig sub_sig) (proj1_sig mul_sig) (proj1_sig square_sig) (proj1_sig carry_sig)));
+          let a24 := fresh "a24" in
+          let x1 := fresh "x1" in
+          let Q := fresh "Q" in
+          let Q' := fresh "Q'" in
+          let eval := fresh "eval" in
+          intros a24 x1 Q Q' eval;
+          cbv [Mxzladderstep FMxzladderstep M.donnaladderstep];
+          destruct Q, Q'; cbv [map map' fst snd Let_In eval];
+          repeat match goal with
+                 | [ |- context[@proj1_sig ?a ?b ?s] ]
+                   => rewrite !(@proj2_sig a b s)
+                 end;
+          reflexivity)
+           Mxzladderstep_sig.
+
+Ltac get_Ladderstep_package sz wt m add_sig sub_sig mul_sig square_sig carry_sig :=
+  let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in
+  let Mxzladderstep_sig := pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig in
+  constr:((Mxzladderstep_sig, tt)).
+Ltac make_Ladderstep_package sz wt m add_sig sub_sig mul_sig square_sig carry_sig :=
+  lazymatch goal with
+  | [ |- { T : _ & T } ] => eexists
+  | [ |- _ ] => idtac
+  end;
+  let pkg := get_Ladderstep_package sz wt m add_sig sub_sig mul_sig square_sig carry_sig in
+  exact pkg.
+
+Module Type LadderstepPrePackage.
+  Parameter Ladderstep_package' : { T : _ & T }.
+  Parameter Ladderstep_package : projT1 Ladderstep_package'.
+End LadderstepPrePackage.
+
+Module MakeLadderstep (LP : LadderstepPrePackage).
+  Ltac get_Ladderstep_package _ := eval hnf in LP.Ladderstep_package.
+  Ltac L_reduce_proj x :=
+    eval cbv beta iota zeta in x.
+  Ltac get_Mxzladderstep_sig _ := let pkg := get_Ladderstep_package () in L_reduce_proj (let '(Mxzladderstep_sig, tt) := pkg in Mxzladderstep_sig).
+  Notation Mxzladderstep_sig := (ltac:(let v := get_Mxzladderstep_sig () in exact v)) (only parsing).
+End MakeLadderstep.
diff --git a/src/Specific/Framework/ReificationTypes.v b/src/Specific/Framework/ReificationTypes.v
new file mode 100644
index 000000000..3a160e04d
--- /dev/null
+++ b/src/Specific/Framework/ReificationTypes.v
@@ -0,0 +1,207 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.romega.ROmega.
+Require Import Coq.micromega.Lia.
+Require Import Coq.Lists.List.
+Local Open Scope Z_scope.
+
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+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.Util.Decidable.
+
+Require Import Crypto.Util.Tactics.PoseTermWithName.
+Require Import Crypto.Util.Tactics.CacheTerm.
+
+Ltac pose_limb_widths wt sz limb_widths :=
+  pose_term_with
+    ltac:(fun _ => (eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz))))
+           limb_widths.
+
+Ltac get_b_of upper_bound_of_exponent :=
+  constr:(fun exp => {| lower := 0 ; upper := upper_bound_of_exponent exp |}%Z). (* 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. *)
+Ltac pose_bounds_exp sz limb_widths bounds_exp :=
+  pose_term_with_type
+    (Tuple.tuple Z sz)
+    ltac:(fun _ => eval compute in
+               (Tuple.from_list sz limb_widths eq_refl))
+           bounds_exp.
+
+Ltac pose_bounds sz b_of bounds_exp bounds :=
+  pose_term_with_type
+    (Tuple.tuple zrange sz)
+    ltac:(fun _ => eval compute in
+               (Tuple.map (fun e => b_of e) bounds_exp))
+           bounds.
+
+Ltac pose_lgbitwidth limb_widths lgbitwidth :=
+  pose_term_with
+    ltac:(fun _ => eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))))
+           lgbitwidth.
+
+Ltac pose_bitwidth lgbitwidth bitwidth :=
+  pose_term_with
+    ltac:(fun _ => eval compute in (2^lgbitwidth)%nat)
+           bitwidth.
+
+Ltac pose_feZ sz feZ :=
+  pose_term_with
+    ltac:(fun _ => constr:(tuple Z sz))
+           feZ.
+
+Ltac pose_feW sz lgbitwidth feW :=
+  cache_term_with_type_by
+    Type
+    ltac:(let v := eval cbv [lgbitwidth] in (tuple (wordT lgbitwidth) sz) in exact v)
+           feW.
+Ltac pose_feW_bounded feW bounds feW_bounded :=
+  cache_term_with_type_by
+    (feW -> Prop)
+    ltac:(let v := eval cbv [bounds] in (fun w : feW => is_bounded_by None bounds (map wordToZ w)) in exact_no_check v)
+           feW_bounded.
+Ltac pose_feBW sz bitwidth bounds feBW :=
+  cache_term_with_type_by
+    Type
+    ltac:(let v := eval cbv [bitwidth bounds] in (BoundedWord sz bitwidth bounds) in exact v)
+           feBW.
+
+Lemma feBW_bounded_helper'
+      sz bitwidth bounds
+      (feBW := BoundedWord sz bitwidth bounds)
+      (wt : nat -> Z)
+      (Hwt : forall i, 0 <= wt i)
+  : forall (a : feBW),
+    B.Positional.eval wt (map lower bounds)
+    <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a)
+    <= B.Positional.eval wt (map upper bounds).
+Proof.
+  let a := fresh "a" in
+  intro a;
+    destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
+  destruct sz as [|sz].
+  { cbv -[Z.le Z.lt Z.mul]; lia. }
+  { cbn [tuple map] in *.
+    revert dependent wt; induction sz as [|sz IHsz]; intros.
+    { cbv -[Z.le Z.lt wordToZ Z.mul Z.pow Z.add lower upper Nat.log2 wordT] in *.
+      repeat match goal with
+             | [ |- context[@wordToZ ?n ?x] ]
+               => generalize dependent (@wordToZ n x); intros
+             | [ H : forall j, 0 <= wt j |- context[wt ?i] ]
+               => pose proof (H i); generalize dependent (wt i); intros
+             end.
+      nia. }
+    { pose proof (Hwt 0%nat).
+      cbn [tuple' map'] in *.
+      destruct a as [a' a], bounds as [bounds b], H as [H [H' _]].
+      cbn [fst snd] in *.
+      setoid_rewrite (@B.Positional.eval_step (S _)).
+      specialize (IHsz bounds a' H (fun i => wt (S i)) (fun i => Hwt _)).
+      nia. } }
+Qed.
+Lemma feBW_bounded_helper
+      sz bitwidth bounds
+      (feBW := BoundedWord sz bitwidth bounds)
+      (wt : nat -> Z)
+      (Hwt : forall i, 0 <= wt i)
+      l u
+  : l <= B.Positional.eval wt (map lower bounds)
+    /\ B.Positional.eval wt (map upper bounds) < u
+    -> forall (a : feBW),
+      l <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < u.
+Proof.
+  intros [Hl Hu] a; split;
+    [ eapply Z.le_trans | eapply Z.le_lt_trans ];
+    [ | eapply feBW_bounded_helper' | eapply feBW_bounded_helper' | ];
+    assumption.
+Qed.
+
+Ltac pose_feBW_bounded wt sz feBW bitwidth bounds m wt_nonneg feBW_bounded :=
+  cache_proof_with_type_by
+    (forall a : feBW, 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m)
+    ltac:(apply (@feBW_bounded_helper sz bitwidth bounds wt wt_nonneg);
+          vm_compute; clear; split; congruence)
+           feBW_bounded.
+
+Ltac pose_phiW feW m wt phiW :=
+  cache_term_with_type_by
+    (feW -> F m)
+    ltac:(exact (fun x : feW => B.Positional.Fdecode wt (Tuple.map wordToZ x)))
+           phiW.
+Ltac pose_phiBW feBW m wt phiBW :=
+  cache_term_with_type_by
+    (feBW -> F m)
+    ltac:(exact (fun x : feBW => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x)))
+           phiBW.
+
+Ltac get_ReificationTypes_package wt sz m wt_nonneg upper_bound_of_exponent :=
+  let limb_widths := fresh "limb_widths" in
+  let bounds_exp := fresh "bounds_exp" in
+  let bounds := fresh "bounds" in
+  let lgbitwidth := fresh "lgbitwidth" in
+  let bitwidth := fresh "bitwidth" in
+  let feZ := fresh "feZ" in
+  let feW := fresh "feW" in
+  let feW_bounded := fresh "feW_bounded" in
+  let feBW := fresh "feBW" in
+  let feBW_bounded := fresh "feBW_bounded" in
+  let phiW := fresh "phiW" in
+  let phiBW := fresh "phiBW" in
+  let limb_widths := pose_limb_widths wt sz limb_widths in
+  let b_of := get_b_of upper_bound_of_exponent in
+  let bounds_exp := pose_bounds_exp sz limb_widths bounds_exp in
+  let bounds := pose_bounds sz b_of bounds_exp bounds in
+  let lgbitwidth := pose_lgbitwidth limb_widths lgbitwidth in
+  let bitwidth := pose_bitwidth lgbitwidth bitwidth in
+  let feZ := pose_feZ sz feZ in
+  let feW := pose_feW sz lgbitwidth feW in
+  let feW_bounded := pose_feW_bounded feW bounds feW_bounded in
+  let feBW := pose_feBW sz bitwidth bounds feBW in
+  let feBW_bounded := pose_feBW_bounded wt sz feBW bitwidth bounds m wt_nonneg feBW_bounded in
+  let phiW := pose_phiW feW m wt phiW in
+  let phiBW := pose_phiBW feBW m wt phiBW in
+  constr:((feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW)).
+Ltac make_ReificationTypes_package wt sz m wt_nonneg upper_bound_of_exponent :=
+  lazymatch goal with
+  | [ |- { T : _ & T } ] => eexists
+  | [ |- _ ] => idtac
+  end;
+  let pkg := get_ReificationTypes_package wt sz m wt_nonneg upper_bound_of_exponent in
+  exact pkg.
+
+Module Type ReificationTypesPrePackage.
+  Parameter ReificationTypes_package' : { T : _ & T }.
+  Parameter ReificationTypes_package : projT1 ReificationTypes_package'.
+End ReificationTypesPrePackage.
+
+Module MakeReificationTypes (RP : ReificationTypesPrePackage).
+  Ltac get_ReificationTypes_package _ := eval hnf in RP.ReificationTypes_package.
+  Ltac RT_reduce_proj x :=
+    eval cbv beta iota zeta in x.
+  (**
+<<
+terms = 'feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW'
+for i in terms.split(', '):
+    print("  Ltac get_%s _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(%s) := pkg in %s)." % (i, terms, i))
+    print("  Notation %s := (ltac:(let v := get_%s () in exact v)) (only parsing)." % (i, i))
+>> *)
+  Ltac get_feZ _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feZ).
+  Notation feZ := (ltac:(let v := get_feZ () in exact v)) (only parsing).
+  Ltac get_feW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feW).
+  Notation feW := (ltac:(let v := get_feW () in exact v)) (only parsing).
+  Ltac get_feW_bounded _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feW_bounded).
+  Notation feW_bounded := (ltac:(let v := get_feW_bounded () in exact v)) (only parsing).
+  Ltac get_feBW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feBW).
+  Notation feBW := (ltac:(let v := get_feBW () in exact v)) (only parsing).
+  Ltac get_feBW_bounded _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feBW_bounded).
+  Notation feBW_bounded := (ltac:(let v := get_feBW_bounded () in exact v)) (only parsing).
+  Ltac get_phiW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in phiW).
+  Notation phiW := (ltac:(let v := get_phiW () in exact v)) (only parsing).
+  Ltac get_phiBW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in phiBW).
+  Notation phiBW := (ltac:(let v := get_phiBW () in exact v)) (only parsing).
+End MakeReificationTypes.
diff --git a/src/Specific/Framework/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v
new file mode 100644
index 000000000..c30024181
--- /dev/null
+++ b/src/Specific/Framework/SynthesisFramework.v
@@ -0,0 +1,104 @@
+Require Import Crypto.Specific.Framework.ArithmeticSynthesisFramework.
+Require Import Crypto.Specific.Framework.ReificationTypes.
+Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework.
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Util.BoundedWord.
+Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon.
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.
+Require Crypto.Specific.Framework.CurveParameters.
+
+Module Export Exports.
+  Export ArithmeticSynthesisFramework.Exports.
+End Exports.
+
+Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters).
+  Module AS := MakeArithmeticSynthesisTestTactics Curve.
+
+  Ltac get_synthesis_package _ :=
+    let arithmetic_synthesis_pkg := AS.get_ArithmeticSynthesis_package () in
+    lazymatch arithmetic_synthesis_pkg with
+    | (?sz, ?bitwidth, ?s, ?c, ?carry_chain1, ?carry_chain2, ?a24, ?coef_div_modulus, ?m, ?wt, ?sz2, ?m_enc, ?coef, ?coef_mod, ?sz_nonzero, ?wt_nonzero, ?wt_nonneg, ?wt_divides, ?wt_divides', ?wt_divides_chain1, ?wt_divides_chain2, ?zero_sig, ?one_sig, ?a24_sig, ?add_sig, ?sub_sig, ?opp_sig, ?mul_sig, ?square_sig, ?carry_sig, ?wt_pos, ?wt_multiples, ?freeze_sig, ?ring)
+      => let reification_types_pkg := get_ReificationTypes_package wt sz m wt_nonneg AS.P.upper_bound_of_exponent in
+         let ladderstep_pkg := get_Ladderstep_package sz wt m add_sig sub_sig mul_sig square_sig carry_sig in
+         constr:((arithmetic_synthesis_pkg, reification_types_pkg, ladderstep_pkg))
+    end.
+  Ltac make_synthesis_package _ :=
+    lazymatch goal with
+    | [ |- { T : _ & _ } ]
+      => first [ eexists (_, _, _)
+               | eexists (_, _)
+               | eexists ]
+    | [ |- _ ] => idtac
+    end;
+    let pkg := get_synthesis_package () in
+    exact pkg.
+End MakeSynthesisTactics.
+
+Local Notation eta2 x := (fst x, snd x) (only parsing).
+Local Notation eta3 x := (eta2 (fst x), snd x) (only parsing).
+
+Notation Synthesis_package'_Type :=
+  { ABC : _ & let '(a, b, c) := eta3 ABC in (a * b * c)%type } (only parsing).
+
+Module Type SynthesisPrePackage.
+  Parameter Synthesis_package' : Synthesis_package'_Type.
+  Parameter Synthesis_package : let '(a, b, c) := eta3 (projT1 Synthesis_package') in (a * b * c)%type.
+End SynthesisPrePackage.
+
+Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : SynthesisPrePackage).
+  Module CP := CurveParameters.FillCurveParameters Curve.
+
+  Module PP <: ReificationTypesPrePackage <: ArithmeticSynthesisPrePackage <: LadderstepPrePackage.
+    Definition ArithmeticSynthesis_package := Eval compute in let '(a, b, c) := P.Synthesis_package in a.
+    Definition ArithmeticSynthesis_package' : { T : _ & T } := existT _ _ ArithmeticSynthesis_package.
+    Definition ReificationTypes_package := Eval compute in let '(a, b, c) := P.Synthesis_package in b.
+    Definition ReificationTypes_package' : { T : _ & T } := existT _ _ ReificationTypes_package.
+    Definition Ladderstep_package := Eval compute in let '(a, b, c) := P.Synthesis_package in c.
+    Definition Ladderstep_package' : { T : _ & T } := existT _ _ Ladderstep_package.
+  End PP.
+  Module RT := MakeReificationTypes PP.
+  Module AS := MakeArithmeticSynthesisTest PP.
+  Module LS := MakeLadderstep PP.
+  Include RT.
+  Include AS.
+  Include LS.
+
+  Ltac synthesize_with_carry do_rewrite get_op_sig :=
+    let carry_sig := get_carry_sig () in
+    let op_sig := get_op_sig () in
+    start_preglue;
+    [ do_rewrite op_sig carry_sig; cbv_runtime
+    | .. ];
+    fin_preglue;
+    refine_reflectively_gen CP.allowable_bit_widths default.
+  Ltac synthesize_2arg_with_carry get_op_sig :=
+    synthesize_with_carry do_rewrite_with_2sig_add_carry get_op_sig.
+  Ltac synthesize_1arg_with_carry get_op_sig :=
+    synthesize_with_carry do_rewrite_with_1sig_add_carry get_op_sig.
+
+  Ltac synthesize_mul _ := synthesize_2arg_with_carry get_mul_sig.
+  Ltac synthesize_add _ := synthesize_2arg_with_carry get_add_sig.
+  Ltac synthesize_sub _ := synthesize_2arg_with_carry get_sub_sig.
+  Ltac synthesize_square _ := synthesize_1arg_with_carry get_square_sig.
+  Ltac synthesize_freeze _ :=
+    let freeze_sig := get_freeze_sig () in
+    let feBW_bounded := get_feBW_bounded () in
+    start_preglue;
+    [ do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime
+    | .. ];
+    fin_preglue;
+    refine_reflectively_gen CP.freeze_allowable_bit_widths anf.
+  Ltac synthesize_xzladderstep _ :=
+    let Mxzladderstep_sig := get_Mxzladderstep_sig () in
+    let a24_sig := get_a24_sig () in
+    start_preglue;
+    [ unmap_map_tuple ();
+      do_rewrite_with_sig_1arg Mxzladderstep_sig;
+      cbv [Mxzladderstep XZ.M.xzladderstep a24_sig]; cbn [proj1_sig];
+      do_set_sigs ();
+      cbv_runtime
+    | .. ];
+    finish_conjoined_preglue ();
+    refine_reflectively_gen CP.allowable_bit_widths default.
+End PackageSynthesis.