Reorganize the curve-specific synthesis framework

This brings in most of the changes that I made when figuring out how to
integrate montgomery into the framework.

The code is a bit slower because the we drop `Print Assumptions` at the
bottom of each synthesis problem, to record that things are closed under
the global context.  If we remove this, we get back the time that we
lost with this commit.

After     | File Name                                                | Before    || Change
---------------------------------------------------------------------------------------------
13m10.63s | Total                                                    | 11m51.91s || +1m18.71s
---------------------------------------------------------------------------------------------
1m15.83s  | Specific/X2555/C128/ladderstep                           | 1m02.57s  || +0m13.25s
1m03.07s  | Specific/X25519/C32/femul                                | 0m54.99s  || +0m08.07s
0m36.49s  | Specific/X25519/C32/fesquare                             | 0m27.77s  || +0m08.72s
1m08.99s  | Specific/X2448/Karatsuba/C64/femul                       | 1m01.88s  || +0m07.10s
0m26.82s  | Specific/X25519/C32/freeze                               | 0m19.81s  || +0m07.01s
2m06.29s  | Specific/X25519/C64/ladderstep                           | 2m00.03s  || +0m06.26s
0m17.48s  | Specific/X25519/C64/femul                                | 0m10.81s  || +0m06.67s
0m14.78s  | Specific/X25519/C64/freeze                               | 0m08.19s  || +0m06.58s
0m14.12s  | Specific/X25519/C64/fesquare                             | 0m07.45s  || +0m06.66s
1m48.54s  | Specific/NISTP256/AMD64/femul                            | 1m51.58s  || -0m03.04s
0m44.50s  | Specific/X2448/Karatsuba/C64/Synthesis                   | 0m43.81s  || +0m00.68s
0m31.40s  | Specific/X25519/C32/Synthesis                            | 0m31.02s  || +0m00.37s
0m25.72s  | Specific/IntegrationTestMontgomeryP256_128               | 0m25.34s  || +0m00.37s
0m18.36s  | Specific/NISTP256/AMD64/fesub                            | 0m18.79s  || -0m00.42s
0m16.45s  | Specific/NISTP256/AMD64/feadd                            | 0m16.40s  || +0m00.05s
0m15.15s  | Specific/NISTP256/AMD64/feopp                            | 0m14.79s  || +0m00.36s
0m12.27s  | Specific/IntegrationTestMontgomeryP256_128_Sub           | 0m11.90s  || +0m00.36s
0m12.06s  | Specific/IntegrationTestMontgomeryP256_128_Add           | 0m11.89s  || +0m00.16s
0m10.93s  | Specific/IntegrationTestMontgomeryP256_128_Opp           | 0m11.39s  || -0m00.46s
0m10.12s  | Specific/X25519/C64/Synthesis                            | 0m09.86s  || +0m00.25s
0m09.86s  | Specific/NISTP256/AMD64/fenz                             | 0m09.54s  || +0m00.32s
0m09.40s  | Specific/IntegrationTestMontgomeryP256_128_Nonzero       | 0m09.16s  || +0m00.24s
0m06.08s  | Specific/X2555/C128/Synthesis                            | 0m05.72s  || +0m00.36s
0m01.06s  | Specific/Framework/SynthesisFramework                    | 0m00.98s  || +0m00.08s
0m01.05s  | Specific/X25519/C32/CurveParameters                      | 0m01.01s  || +0m00.04s
0m00.88s  | Specific/Framework/ReificationTypes                      | 0m00.84s  || +0m00.04s
   N/A    | Specific/Framework/ArithmeticSynthesisFramework          | 0m00.82s  || -0m00.82s
0m00.81s  | Specific/Framework/ArithmeticSynthesis/Karatsuba         |    N/A    || +0m00.81s
0m00.79s  | Specific/Framework/ArithmeticSynthesis/SquareFromMul     |    N/A    || +0m00.79s
0m00.79s  | Specific/Framework/ArithmeticSynthesis/Base              |    N/A    || +0m00.79s
0m00.79s  | Specific/Framework/ArithmeticSynthesis/Freeze            |    N/A    || +0m00.79s
0m00.78s  | Specific/Framework/ArithmeticSynthesis/BasePackage       |    N/A    || +0m00.78s
0m00.76s  | Specific/Framework/IntegrationTestTemporaryMiscCommon    | 0m00.78s  || -0m00.02s
0m00.74s  | Specific/Framework/ArithmeticSynthesis/HelperTactics     |    N/A    || +0m00.74s
0m00.74s  | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage  |    N/A    || +0m00.74s
0m00.73s  | Specific/Framework/ArithmeticSynthesis/FreezePackage     |    N/A    || +0m00.73s
0m00.72s  | Specific/Framework/ReificationTypesPackage               |    N/A    || +0m00.72s
0m00.70s  | Specific/Framework/ArithmeticSynthesis/Defaults          |    N/A    || +0m00.70s
0m00.69s  | Specific/Framework/ArithmeticSynthesis/LadderstepPackage |    N/A    || +0m00.69s
0m00.69s  | Specific/Framework/ArithmeticSynthesis/DefaultsPackage   |    N/A    || +0m00.69s
0m00.68s  | Specific/Framework/ArithmeticSynthesis/Ladderstep        |    N/A    || +0m00.68s
   N/A    | Specific/Framework/LadderstepSynthesisFramework          | 0m00.68s  || -0m00.68s
0m00.42s  | Specific/Framework/IntegrationTestDisplayCommon          | 0m00.39s  || +0m00.02s
0m00.40s  | Specific/X25519/C64/CurveParameters                      | 0m00.44s  || -0m00.03s
0m00.34s  | Specific/Framework/IntegrationTestDisplayCommonTactics   | 0m00.35s  || -0m00.00s
0m00.33s  | Specific/X2555/C128/CurveParameters                      | 0m00.31s  || +0m00.02s
0m00.33s  | Specific/Framework/CurveParameters                       | 0m00.31s  || +0m00.02s
0m00.33s  | Specific/Framework/CurveParametersPackage                |    N/A    || +0m00.33s
0m00.31s  | Specific/X2448/Karatsuba/C64/CurveParameters             | 0m00.32s  || -0m00.01s
0m00.07s  | Specific/Framework/Packages                              |    N/A    || +0m00.07s

40 files changed, 1879 insertions, 981 deletions

diff --git a/_CoqProject b/_CoqProject
index e2619d54b..5bcc76f6c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -239,14 +239,27 @@ src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v
 src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
 src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v
 src/Specific/MontgomeryP256_128.v
-src/Specific/Framework/ArithmeticSynthesisFramework.v
 src/Specific/Framework/CurveParameters.v
+src/Specific/Framework/CurveParametersPackage.v
 src/Specific/Framework/IntegrationTestDisplayCommon.v
 src/Specific/Framework/IntegrationTestDisplayCommonTactics.v
 src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v
-src/Specific/Framework/LadderstepSynthesisFramework.v
+src/Specific/Framework/Packages.v
 src/Specific/Framework/ReificationTypes.v
+src/Specific/Framework/ReificationTypesPackage.v
 src/Specific/Framework/SynthesisFramework.v
+src/Specific/Framework/ArithmeticSynthesis/Base.v
+src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
+src/Specific/Framework/ArithmeticSynthesis/Defaults.v
+src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v
+src/Specific/Framework/ArithmeticSynthesis/Freeze.v
+src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
+src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
+src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v
+src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
+src/Specific/Framework/ArithmeticSynthesis/Ladderstep.v
+src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
+src/Specific/Framework/ArithmeticSynthesis/SquareFromMul.v
 src/Specific/NISTP256/AMD64/MontgomeryP256.v
 src/Specific/NISTP256/AMD64/feadd.v
 src/Specific/NISTP256/AMD64/feaddDisplay.v
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Base.v b/src/Specific/Framework/ArithmeticSynthesis/Base.v
new file mode 100644
index 000000000..092c08705
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/Base.v
@@ -0,0 +1,125 @@
+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.Specific.Framework.CurveParameters.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics.
+Require Import Crypto.Util.QUtil.
+Require Import Crypto.Util.Decidable.
+Require Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.CacheTerm.
+
+  (* 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.):  *)
+
+Ltac pose_r bitwidth r :=
+  cache_term_with_type_by
+    positive
+    ltac:(let v := (eval vm_compute in (Z.to_pos (2^bitwidth))) in exact v)
+           r.
+
+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.
+  Local Coercion Z.of_nat : nat >-> Z.
+  Local Coercion Z.pos : positive >-> Z.
+  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_half_sz sz half_sz :=
+  let v := (eval compute in (sz / 2)%nat) in
+  cache_term v half_sz.
+
+Ltac pose_half_sz_nonzero half_sz half_sz_nonzero :=
+  cache_proof_with_type_by
+    (half_sz <> 0%nat)
+    ltac:(cbv; congruence)
+           half_sz_nonzero.
+
+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
+  let v := (eval compute in v) in (* compute away the type arguments *)
+  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 helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chain :=
+  cache_term_with_type_by
+    (forall i (H:In i carry_chain), wt (S i) / wt i <> 0)
+    ltac:(let i := fresh "i" in intros i ?; exact (wt_divides' i))
+           wt_divides_chain.
+Ltac internal_pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains :=
+  lazymatch carry_chains with
+  | ?carry_chain :: nil
+    => helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chains
+  | ?carry_chain :: ?carry_chains
+    => let wt_divides_chains := fresh wt_divides_chains in
+       let wt_divides_chain := fresh wt_divides_chains in
+       let wt_divides_chain := helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chain in
+       let wt_divides_chains := internal_pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains in
+       constr:((wt_divides_chain, wt_divides_chains))
+  end.
+Ltac pose_wt_divides_chains wt carry_chains wt_divides' wt_divides_chains :=
+  let carry_chains := (eval cbv delta [carry_chains] in carry_chains) in
+  internal_pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains.
+
+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.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
new file mode 100644
index 000000000..457c9dc11
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
@@ -0,0 +1,185 @@
+(* This file is autogenerated from Base.v by remake_packages.py *)
+Require Import Crypto.Specific.Framework.CurveParametersPackage.
+Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Base.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+
+Module TAG.
+  Inductive tags := r | m | wt | sz2 | half_sz | half_sz_nonzero | m_enc | coef | coef_mod | sz_nonzero | wt_nonzero | wt_nonneg | wt_divides | wt_divides' | wt_divides_chains | wt_pos | wt_multiples.
+End TAG.
+
+Ltac add_r pkg :=
+  let bitwidth := Tag.get pkg TAG.bitwidth in
+  let r := fresh "r" in
+  let r := pose_r bitwidth r in
+  Tag.update pkg TAG.r r.
+
+Ltac add_m pkg :=
+  let s := Tag.get pkg TAG.s in
+  let c := Tag.get pkg TAG.c in
+  let m := fresh "m" in
+  let m := pose_m s c m in
+  Tag.update pkg TAG.m m.
+
+Ltac add_wt pkg :=
+  let m := Tag.get pkg TAG.m in
+  let sz := Tag.get pkg TAG.sz in
+  let wt := fresh "wt" in
+  let wt := pose_wt m sz wt in
+  Tag.update pkg TAG.wt wt.
+
+Ltac add_sz2 pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let sz2 := fresh "sz2" in
+  let sz2 := pose_sz2 sz sz2 in
+  Tag.update pkg TAG.sz2 sz2.
+
+Ltac add_half_sz pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let half_sz := fresh "half_sz" in
+  let half_sz := pose_half_sz sz half_sz in
+  Tag.update pkg TAG.half_sz half_sz.
+
+Ltac add_half_sz_nonzero pkg :=
+  let half_sz := Tag.get pkg TAG.half_sz in
+  let half_sz_nonzero := fresh "half_sz_nonzero" in
+  let half_sz_nonzero := pose_half_sz_nonzero half_sz half_sz_nonzero in
+  Tag.update pkg TAG.half_sz_nonzero half_sz_nonzero.
+
+Ltac add_m_enc pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let s := Tag.get pkg TAG.s in
+  let c := Tag.get pkg TAG.c in
+  let wt := Tag.get pkg TAG.wt in
+  let m_enc := fresh "m_enc" in
+  let m_enc := pose_m_enc sz s c wt m_enc in
+  Tag.update pkg TAG.m_enc m_enc.
+
+Ltac add_coef pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let wt := Tag.get pkg TAG.wt in
+  let m_enc := Tag.get pkg TAG.m_enc in
+  let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in
+  let coef := fresh "coef" in
+  let coef := pose_coef sz wt m_enc coef_div_modulus coef in
+  Tag.update pkg TAG.coef coef.
+
+Ltac add_coef_mod pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let wt := Tag.get pkg TAG.wt in
+  let m := Tag.get pkg TAG.m in
+  let coef := Tag.get pkg TAG.coef in
+  let coef_mod := fresh "coef_mod" in
+  let coef_mod := pose_coef_mod sz wt m coef coef_mod in
+  Tag.update pkg TAG.coef_mod coef_mod.
+
+Ltac add_sz_nonzero pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let sz_nonzero := fresh "sz_nonzero" in
+  let sz_nonzero := pose_sz_nonzero sz sz_nonzero in
+  Tag.update pkg TAG.sz_nonzero sz_nonzero.
+
+Ltac add_wt_nonzero pkg :=
+  let wt := Tag.get pkg TAG.wt in
+  let wt_nonzero := fresh "wt_nonzero" in
+  let wt_nonzero := pose_wt_nonzero wt wt_nonzero in
+  Tag.update pkg TAG.wt_nonzero wt_nonzero.
+
+Ltac add_wt_nonneg pkg :=
+  let wt := Tag.get pkg TAG.wt in
+  let wt_nonneg := fresh "wt_nonneg" in
+  let wt_nonneg := pose_wt_nonneg wt wt_nonneg in
+  Tag.update pkg TAG.wt_nonneg wt_nonneg.
+
+Ltac add_wt_divides pkg :=
+  let wt := Tag.get pkg TAG.wt in
+  let wt_divides := fresh "wt_divides" in
+  let wt_divides := pose_wt_divides wt wt_divides in
+  Tag.update pkg TAG.wt_divides wt_divides.
+
+Ltac add_wt_divides' pkg :=
+  let wt := Tag.get pkg TAG.wt in
+  let wt_divides := Tag.get pkg TAG.wt_divides in
+  let wt_divides' := fresh "wt_divides'" in
+  let wt_divides' := pose_wt_divides' wt wt_divides wt_divides' in
+  Tag.update pkg TAG.wt_divides' wt_divides'.
+
+Ltac add_wt_divides_chains pkg :=
+  let wt := Tag.get pkg TAG.wt in
+  let carry_chains := Tag.get pkg TAG.carry_chains in
+  let wt_divides' := Tag.get pkg TAG.wt_divides' in
+  let wt_divides_chains := fresh "wt_divides_chains" in
+  let wt_divides_chains := pose_wt_divides_chains wt carry_chains wt_divides' wt_divides_chains in
+  Tag.update pkg TAG.wt_divides_chains wt_divides_chains.
+
+Ltac add_wt_pos pkg :=
+  let wt := Tag.get pkg TAG.wt in
+  let wt_pos := fresh "wt_pos" in
+  let wt_pos := pose_wt_pos wt wt_pos in
+  Tag.update pkg TAG.wt_pos wt_pos.
+
+Ltac add_wt_multiples pkg :=
+  let wt := Tag.get pkg TAG.wt in
+  let wt_multiples := fresh "wt_multiples" in
+  let wt_multiples := pose_wt_multiples wt wt_multiples in
+  Tag.update pkg TAG.wt_multiples wt_multiples.
+
+Ltac add_Base_package pkg :=
+  let pkg := add_r pkg in
+  let pkg := add_m pkg in
+  let pkg := add_wt pkg in
+  let pkg := add_sz2 pkg in
+  let pkg := add_half_sz pkg in
+  let pkg := add_half_sz_nonzero pkg in
+  let pkg := add_m_enc pkg in
+  let pkg := add_coef pkg in
+  let pkg := add_coef_mod pkg in
+  let pkg := add_sz_nonzero pkg in
+  let pkg := add_wt_nonzero pkg in
+  let pkg := add_wt_nonneg pkg in
+  let pkg := add_wt_divides pkg in
+  let pkg := add_wt_divides' pkg in
+  let pkg := add_wt_divides_chains pkg in
+  let pkg := add_wt_pos pkg in
+  let pkg := add_wt_multiples pkg in
+  Tag.strip_local pkg.
+
+
+Module MakeBasePackage (PKG : PrePackage).
+  Module Import MakeBasePackageInternal := MakePackageBase PKG.
+
+  Ltac get_r _ := get TAG.r.
+  Notation r := (ltac:(let v := get_r () in exact v)) (only parsing).
+  Ltac get_m _ := get TAG.m.
+  Notation m := (ltac:(let v := get_m () in exact v)) (only parsing).
+  Ltac get_wt _ := get TAG.wt.
+  Notation wt := (ltac:(let v := get_wt () in exact v)) (only parsing).
+  Ltac get_sz2 _ := get TAG.sz2.
+  Notation sz2 := (ltac:(let v := get_sz2 () in exact v)) (only parsing).
+  Ltac get_half_sz _ := get TAG.half_sz.
+  Notation half_sz := (ltac:(let v := get_half_sz () in exact v)) (only parsing).
+  Ltac get_half_sz_nonzero _ := get TAG.half_sz_nonzero.
+  Notation half_sz_nonzero := (ltac:(let v := get_half_sz_nonzero () in exact v)) (only parsing).
+  Ltac get_m_enc _ := get TAG.m_enc.
+  Notation m_enc := (ltac:(let v := get_m_enc () in exact v)) (only parsing).
+  Ltac get_coef _ := get TAG.coef.
+  Notation coef := (ltac:(let v := get_coef () in exact v)) (only parsing).
+  Ltac get_coef_mod _ := get TAG.coef_mod.
+  Notation coef_mod := (ltac:(let v := get_coef_mod () in exact v)) (only parsing).
+  Ltac get_sz_nonzero _ := get TAG.sz_nonzero.
+  Notation sz_nonzero := (ltac:(let v := get_sz_nonzero () in exact v)) (only parsing).
+  Ltac get_wt_nonzero _ := get TAG.wt_nonzero.
+  Notation wt_nonzero := (ltac:(let v := get_wt_nonzero () in exact v)) (only parsing).
+  Ltac get_wt_nonneg _ := get TAG.wt_nonneg.
+  Notation wt_nonneg := (ltac:(let v := get_wt_nonneg () in exact v)) (only parsing).
+  Ltac get_wt_divides _ := get TAG.wt_divides.
+  Notation wt_divides := (ltac:(let v := get_wt_divides () in exact v)) (only parsing).
+  Ltac get_wt_divides' _ := get TAG.wt_divides'.
+  Notation wt_divides' := (ltac:(let v := get_wt_divides' () in exact v)) (only parsing).
+  Ltac get_wt_divides_chains _ := get TAG.wt_divides_chains.
+  Notation wt_divides_chains := (ltac:(let v := get_wt_divides_chains () in exact v)) (only parsing).
+  Ltac get_wt_pos _ := get TAG.wt_pos.
+  Notation wt_pos := (ltac:(let v := get_wt_pos () in exact v)) (only parsing).
+  Ltac get_wt_multiples _ := get TAG.wt_multiples.
+  Notation wt_multiples := (ltac:(let v := get_wt_multiples () in exact v)) (only parsing).
+End MakeBasePackage.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v
new file mode 100644
index 000000000..db209c9f1
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v
@@ -0,0 +1,187 @@
+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 Crypto.Specific.Framework.CurveParameters.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.PoseTermWithName.
+Require Import Crypto.Util.Tactics.CacheTerm.
+Require Crypto.Util.Tuple.
+
+Local Notation tuple := Tuple.tuple.
+Local Open Scope list_scope.
+Local Open Scope Z_scope.
+Local Infix "^" := tuple : type_scope.
+
+Module Export Exports.
+  Export Coq.setoid_ring.ZArithRing.
+End Exports.
+
+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.
+
+(* Performs a full carry loop (as specified by carry_chain) *)
+Ltac pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains 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 div_mod;
+          pose_proof_tuple wt_divides_chains;
+          let x := make_chained_carries_cps sz wt s c a carry_chains in
+          solve_op_F wt x; reflexivity)
+           carry_sig.
+
+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 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 P_default_mul P_extra_prove_mul_eq 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 P_default_square P_extra_prove_square_eq 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.
+
+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).
+ *)
diff --git a/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v b/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v
new file mode 100644
index 000000000..a83adb29c
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v
@@ -0,0 +1,177 @@
+(* This file is autogenerated from Defaults.v by remake_packages.py *)
+Require Import Crypto.Specific.Framework.CurveParametersPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
+Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Defaults.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+
+Module TAG.
+  Inductive tags := carry_sig | zero_sig | one_sig | a24_sig | add_sig | sub_sig | opp_sig | mul_sig | square_sig | ring.
+End TAG.
+
+Ltac add_carry_sig pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.carry_sig
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let s := Tag.get pkg TAG.s in
+                   let c := Tag.get pkg TAG.c in
+                   let carry_chains := Tag.get pkg TAG.carry_chains in
+                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
+                   let wt_divides_chains := Tag.get pkg TAG.wt_divides_chains in
+                   let carry_sig := fresh "carry_sig" in
+                   let carry_sig := pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains carry_sig in
+                   constr:(carry_sig)).
+Ltac add_zero_sig pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.zero_sig
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let zero_sig := fresh "zero_sig" in
+                   let zero_sig := pose_zero_sig sz m wt zero_sig in
+                   constr:(zero_sig)).
+Ltac add_one_sig pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.one_sig
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let one_sig := fresh "one_sig" in
+                   let one_sig := pose_one_sig sz m wt one_sig in
+                   constr:(one_sig)).
+Ltac add_a24_sig pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.a24_sig
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let a24 := Tag.get pkg TAG.a24 in
+                   let a24_sig := fresh "a24_sig" in
+                   let a24_sig := pose_a24_sig sz m wt a24 a24_sig in
+                   constr:(a24_sig)).
+Ltac add_add_sig pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.add_sig
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
+                   let add_sig := fresh "add_sig" in
+                   let add_sig := pose_add_sig sz m wt wt_nonzero add_sig in
+                   constr:(add_sig)).
+Ltac add_sub_sig pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.sub_sig
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
+                   let coef := Tag.get pkg TAG.coef in
+                   let sub_sig := fresh "sub_sig" in
+                   let sub_sig := pose_sub_sig sz m wt wt_nonzero coef sub_sig in
+                   constr:(sub_sig)).
+Ltac add_opp_sig pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.opp_sig
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
+                   let coef := Tag.get pkg TAG.coef in
+                   let opp_sig := fresh "opp_sig" in
+                   let opp_sig := pose_opp_sig sz m wt wt_nonzero coef opp_sig in
+                   constr:(opp_sig)).
+Ltac add_mul_sig pkg P_default_mul P_extra_prove_mul_eq :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.mul_sig
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let s := Tag.get pkg TAG.s in
+                   let c := Tag.get pkg TAG.c in
+                   let sz2 := Tag.get pkg TAG.sz2 in
+                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
+                   let mul_sig := fresh "mul_sig" in
+                   let mul_sig := pose_mul_sig P_default_mul P_extra_prove_mul_eq sz m wt s c sz2 wt_nonzero mul_sig in
+                   constr:(mul_sig)).
+Ltac add_square_sig pkg P_default_square P_extra_prove_square_eq :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.square_sig
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let s := Tag.get pkg TAG.s in
+                   let c := Tag.get pkg TAG.c in
+                   let sz2 := Tag.get pkg TAG.sz2 in
+                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
+                   let square_sig := fresh "square_sig" in
+                   let square_sig := pose_square_sig P_default_square P_extra_prove_square_eq sz m wt s c sz2 wt_nonzero square_sig in
+                   constr:(square_sig)).
+Ltac add_ring pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.ring
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let wt_divides' := Tag.get pkg TAG.wt_divides' in
+                   let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
+                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
+                   let zero_sig := Tag.get pkg TAG.zero_sig in
+                   let one_sig := Tag.get pkg TAG.one_sig in
+                   let opp_sig := Tag.get pkg TAG.opp_sig in
+                   let add_sig := Tag.get pkg TAG.add_sig in
+                   let sub_sig := Tag.get pkg TAG.sub_sig in
+                   let mul_sig := Tag.get pkg TAG.mul_sig in
+                   let ring := fresh "ring" 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:(ring)).
+Ltac add_Defaults_package pkg P_default_mul P_extra_prove_mul_eq P_default_square P_extra_prove_square_eq :=
+  let pkg := add_carry_sig pkg in
+  let pkg := add_zero_sig pkg in
+  let pkg := add_one_sig pkg in
+  let pkg := add_a24_sig pkg in
+  let pkg := add_add_sig pkg in
+  let pkg := add_sub_sig pkg in
+  let pkg := add_opp_sig pkg in
+  let pkg := add_mul_sig pkg P_default_mul P_extra_prove_mul_eq in
+  let pkg := add_square_sig pkg P_default_square P_extra_prove_square_eq in
+  let pkg := add_ring pkg in
+  Tag.strip_local pkg.
+
+
+Module MakeDefaultsPackage (PKG : PrePackage).
+  Module Import MakeDefaultsPackageInternal := MakePackageBase PKG.
+
+  Ltac get_carry_sig _ := get TAG.carry_sig.
+  Notation carry_sig := (ltac:(let v := get_carry_sig () in exact v)) (only parsing).
+  Ltac get_zero_sig _ := get TAG.zero_sig.
+  Notation zero_sig := (ltac:(let v := get_zero_sig () in exact v)) (only parsing).
+  Ltac get_one_sig _ := get TAG.one_sig.
+  Notation one_sig := (ltac:(let v := get_one_sig () in exact v)) (only parsing).
+  Ltac get_a24_sig _ := get TAG.a24_sig.
+  Notation a24_sig := (ltac:(let v := get_a24_sig () in exact v)) (only parsing).
+  Ltac get_add_sig _ := get TAG.add_sig.
+  Notation add_sig := (ltac:(let v := get_add_sig () in exact v)) (only parsing).
+  Ltac get_sub_sig _ := get TAG.sub_sig.
+  Notation sub_sig := (ltac:(let v := get_sub_sig () in exact v)) (only parsing).
+  Ltac get_opp_sig _ := get TAG.opp_sig.
+  Notation opp_sig := (ltac:(let v := get_opp_sig () in exact v)) (only parsing).
+  Ltac get_mul_sig _ := get TAG.mul_sig.
+  Notation mul_sig := (ltac:(let v := get_mul_sig () in exact v)) (only parsing).
+  Ltac get_square_sig _ := get TAG.square_sig.
+  Notation square_sig := (ltac:(let v := get_square_sig () in exact v)) (only parsing).
+  Ltac get_ring _ := get TAG.ring.
+  Notation ring := (ltac:(let v := get_ring () in exact v)) (only parsing).
+End MakeDefaultsPackage.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Freeze.v b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v
new file mode 100644
index 000000000..02daea678
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v
@@ -0,0 +1,50 @@
+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.Saturated.Freeze.
+Require Crypto.Specific.Framework.CurveParameters.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.Definitions.
+Require Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.CacheTerm.
+
+Module Export Exports.
+  Hint Opaque freeze : uncps.
+  Hint Rewrite freeze_id : uncps.
+End Exports.
+
+Local Open Scope Z_scope.
+Local Infix "^" := Tuple.tuple : type_scope.
+
+(* 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.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
new file mode 100644
index 000000000..9314f369e
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
@@ -0,0 +1,39 @@
+(* This file is autogenerated from Freeze.v by remake_packages.py *)
+Require Import Crypto.Specific.Framework.CurveParametersPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
+Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Freeze.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+
+Module TAG.
+  Inductive tags := freeze_sig.
+End TAG.
+
+Ltac add_freeze_sig pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.freeze_sig
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let c := Tag.get pkg TAG.c in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let bitwidth := Tag.get pkg TAG.bitwidth in
+                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
+                   let wt_pos := Tag.get pkg TAG.wt_pos in
+                   let wt_divides := Tag.get pkg TAG.wt_divides in
+                   let wt_multiples := Tag.get pkg TAG.wt_multiples in
+                   let freeze_sig := fresh "freeze_sig" 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
+                   constr:(freeze_sig)).
+Ltac add_Freeze_package pkg :=
+  let pkg := add_freeze_sig pkg in
+  Tag.strip_local pkg.
+
+
+Module MakeFreezePackage (PKG : PrePackage).
+  Module Import MakeFreezePackageInternal := MakePackageBase PKG.
+
+  Ltac get_freeze_sig _ := get TAG.freeze_sig.
+  Notation freeze_sig := (ltac:(let v := get_freeze_sig () in exact v)) (only parsing).
+End MakeFreezePackage.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v b/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
new file mode 100644
index 000000000..e2bc9e6e0
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
@@ -0,0 +1,65 @@
+Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
+Require Import Crypto.Arithmetic.Core. Import B.
+Require Import Crypto.Util.ZUtil.ModInv.
+Require Import Crypto.Util.Tactics.CacheTerm.
+Require Crypto.Util.Tuple.
+
+Local Notation tuple := Tuple.tuple.
+Local Open Scope list_scope.
+Local Open Scope Z_scope.
+
+Ltac if_cond_else cond tac default id :=
+  lazymatch (eval compute in cond) with
+  | true => tac id
+  | false => default
+  end.
+Ltac if_cond cond tac id := if_cond_else cond tac (0%Z) id.
+
+Ltac pose_modinv modinv_fuel a modulus modinv :=
+  let v := constr:(Option.invert_Some (Z.modinv_fueled modinv_fuel a modulus)) in
+  let v := (eval vm_compute in v) in
+  let v := (eval vm_compute in (v : Z)) in
+  cache_term v modinv.
+Ltac pose_correct_if_Z v mkeqn id :=
+  let T := type of v in
+  let eqn :=
+      lazymatch (eval vm_compute in T) with
+      | Z => mkeqn ()
+      | ?T
+        => let v := (eval vm_compute in v) in
+           lazymatch T with
+           | option _
+             => lazymatch v with
+                | None => constr:(v = v)
+                end
+           | unit
+             => lazymatch v with
+                | tt => constr:(tt = tt)
+                end
+           end
+      end in
+  cache_proof_with_type_by
+    eqn
+    ltac:(vm_compute; reflexivity)
+           id.
+
+Ltac pose_proof_tuple ls :=
+  lazymatch ls with
+  | pair ?x ?y => pose_proof_tuple x; pose_proof_tuple y
+  | ?ls => pose proof ls
+  end.
+
+Ltac make_chained_carries_cps' sz wt s c a carry_chains :=
+  lazymatch carry_chains with
+  | ?carry_chain :: nil
+    => constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain id)
+  | ?carry_chain :: ?carry_chains
+    => let r := fresh "r" in
+       let r' := fresh r in
+       constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain
+                                              (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r
+                                                                                    (fun r' => ltac:(let v := make_chained_carries_cps' sz wt s c r' carry_chains in exact v))))
+  end.
+Ltac make_chained_carries_cps sz wt s c a carry_chains :=
+  let carry_chains := (eval cbv delta [carry_chains] in carry_chains) in
+  make_chained_carries_cps' sz wt s c a carry_chains.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v
new file mode 100644
index 000000000..78cc57d68
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v
@@ -0,0 +1,140 @@
+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 Crypto.Specific.Framework.CurveParameters.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.
+Require Import Crypto.Arithmetic.Karatsuba.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Crypto.Util.Tuple.
+Require Import Crypto.Util.IdfunWithAlt.
+Require Import Crypto.Util.Tactics.VM.
+Require Import Crypto.Util.QUtil.
+Require Import Crypto.Util.ZUtil.ModInv.
+
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.SquareFromMul.
+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.
+Local Infix "^" := Tuple.tuple : type_scope.
+
+(** XXX TODO(jadep) FIXME: Is sqrt(s) the right thing to pass to goldilocks_mul_cps (the original code hard-coded 2^224 *)
+Ltac internal_pose_sqrt_s s sqrt_s :=
+  let v := (eval vm_compute in (Z.log2 s / 2)) in
+  cache_term (2^v) sqrt_s.
+
+Ltac basesystem_partial_evaluation_RHS :=
+  let t0 := (match goal with
+             | |- _ _ ?t => t
+             end) in
+  let t :=
+   eval
+    cbv
+     delta [Positional.to_associational_cps Positional.to_associational
+           Positional.eval Positional.zeros Positional.add_to_nth_cps
+           Positional.add_to_nth Positional.place_cps Positional.place
+           Positional.from_associational_cps Positional.from_associational
+           Positional.carry_cps Positional.carry
+           Positional.chained_carries_cps Positional.chained_carries
+           Positional.sub_cps Positional.sub Positional.split_cps
+           Positional.scmul_cps Positional.unbalanced_sub_cps
+           Positional.negate_snd_cps Positional.add_cps Positional.opp_cps
+           Associational.eval Associational.multerm Associational.mul_cps
+           Associational.mul Associational.split_cps Associational.split
+           Associational.reduce_cps Associational.reduce
+           Associational.carryterm_cps Associational.carryterm
+           Associational.carry_cps Associational.carry
+           Associational.negate_snd_cps Associational.negate_snd div modulo
+           id_tuple_with_alt id_tuple'_with_alt
+           ]
+   in t0
+  in
+  let t := eval pattern @runtime_mul in t in
+  let t := (match t with
+            | ?t _ => t
+            end) in
+  let t := eval pattern @runtime_add in t in
+  let t := (match t with
+            | ?t _ => t
+            end) in
+  let t := eval pattern @runtime_opp in t in
+  let t := (match t with
+            | ?t _ => t
+            end) in
+  let t := eval pattern @runtime_shr in t in
+  let t := (match t with
+            | ?t _ => t
+            end) in
+  let t := eval pattern @runtime_and in t in
+  let t := (match t with
+            | ?t _ => t
+            end) in
+  let t := eval pattern @Let_In in t in
+  let t := (match t with
+            | ?t _ => t
+            end) in
+  let t := eval pattern @id_with_alt in t in
+  let t := (match t with
+            | ?t _ => t
+            end) in
+  let t1 := fresh "t1" in
+  pose (t1 := t);
+   transitivity
+    (t1 (@id_with_alt) (@Let_In) (@runtime_and) (@runtime_shr) (@runtime_opp) (@runtime_add)
+       (@runtime_mul));
+   [ replace_with_vm_compute t1; clear t1 | reflexivity ].
+
+Ltac internal_pose_goldilocks_mul_sig sz wt s c half_sz sqrt_s goldilocks_mul_sig :=
+  cache_term_with_type_by
+    {mul : (Z^sz -> Z^sz -> Z^sz)%type |
+     forall a b : Z^sz,
+       mul a b = goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt sqrt_s a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)}
+    ltac:(eexists; cbv beta zeta; intros;
+          cbv [goldilocks_mul_cps];
+          repeat autounfold;
+          basesystem_partial_evaluation_RHS;
+          do_replace_match_with_destructuring_match_in_goal;
+          reflexivity)
+           goldilocks_mul_sig.
+
+Ltac internal_pose_mul_sig_from_goldilocks_mul_sig sz m wt s c half_sz sqrt_s goldilocks_mul_sig 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
+       Positional.Fdecode (m := m) wt (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:(
+                     goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt sqrt_s a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)) in
+          F_mod_eq;
+          transitivity (Positional.eval wt x); repeat autounfold;
+
+          [
+          | autorewrite with uncps push_id push_basesystem_eval;
+            apply goldilocks_mul_correct; try assumption; cbv; congruence ];
+          cbv [mod_eq]; apply f_equal2;
+          [ | reflexivity ];
+          apply f_equal;
+          etransitivity; [|apply (proj2_sig goldilocks_mul_sig)];
+          cbv [proj1_sig goldilocks_mul_sig];
+          reflexivity)
+           mul_sig.
+
+Ltac pose_mul_sig sz m wt s c half_sz wt_nonzero mul_sig :=
+  let sqrt_s := fresh "sqrt_s" in
+  let goldilocks_mul_sig := fresh "goldilocks_mul_sig" in
+  let sqrt_s := internal_pose_sqrt_s s sqrt_s in
+  let goldilocks_mul_sig := internal_pose_goldilocks_mul_sig sz wt s c half_sz sqrt_s goldilocks_mul_sig in
+  internal_pose_mul_sig_from_goldilocks_mul_sig sz m wt s c half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig.
+
+Ltac pose_square_sig sz m wt mul_sig square_sig :=
+  SquareFromMul.pose_square_sig sz m wt mul_sig square_sig.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v b/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
new file mode 100644
index 000000000..a0d2d3528
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
@@ -0,0 +1,46 @@
+(* This file is autogenerated from Karatsuba.v by remake_packages.py *)
+Require Import Crypto.Specific.Framework.CurveParametersPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage.
+Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Karatsuba.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+
+
+Ltac add_mul_sig pkg :=
+  if_goldilocks
+    pkg
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let s := Tag.get pkg TAG.s in
+                   let c := Tag.get pkg TAG.c in
+                   let half_sz := Tag.get pkg TAG.half_sz in
+                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
+                   let mul_sig := fresh "mul_sig" in
+                   let mul_sig := pose_mul_sig sz m wt s c half_sz wt_nonzero mul_sig in
+                   Tag.update pkg TAG.mul_sig mul_sig)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_square_sig pkg :=
+  if_goldilocks
+    pkg
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let wt := Tag.get pkg TAG.wt in
+                   let mul_sig := Tag.get pkg TAG.mul_sig in
+                   let square_sig := fresh "square_sig" in
+                   let square_sig := pose_square_sig sz m wt mul_sig square_sig in
+                   Tag.update pkg TAG.square_sig square_sig)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_Karatsuba_package pkg :=
+  let pkg := add_mul_sig pkg in
+  let pkg := add_square_sig pkg in
+  Tag.strip_local pkg.
+
+
+Module MakeKaratsubaPackage (PKG : PrePackage).
+  Module Import MakeKaratsubaPackageInternal := MakePackageBase PKG.
+
+End MakeKaratsubaPackage.
diff --git a/src/Specific/Framework/LadderstepSynthesisFramework.v b/src/Specific/Framework/ArithmeticSynthesis/Ladderstep.v
index d6afb31eb..ba3fd9078 100644
--- a/src/Specific/Framework/LadderstepSynthesisFramework.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Ladderstep.v
@@ -46,7 +46,6 @@ Section with_notations.
        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)
@@ -66,28 +65,3 @@ Ltac pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig
                  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/ArithmeticSynthesis/LadderstepPackage.v b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
new file mode 100644
index 000000000..dd7b6c541
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
@@ -0,0 +1,38 @@
+(* This file is autogenerated from Ladderstep.v by remake_packages.py *)
+Require Import Crypto.Specific.Framework.CurveParametersPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage.
+Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+
+Module TAG.
+  Inductive tags := Mxzladderstep_sig.
+End TAG.
+
+Ltac add_Mxzladderstep_sig pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.Mxzladderstep_sig
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let wt := Tag.get pkg TAG.wt in
+                   let m := Tag.get pkg TAG.m in
+                   let add_sig := Tag.get pkg TAG.add_sig in
+                   let sub_sig := Tag.get pkg TAG.sub_sig in
+                   let mul_sig := Tag.get pkg TAG.mul_sig in
+                   let square_sig := Tag.get pkg TAG.square_sig in
+                   let carry_sig := Tag.get pkg TAG.carry_sig in
+                   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)).
+Ltac add_Ladderstep_package pkg :=
+  let pkg := add_Mxzladderstep_sig pkg in
+  Tag.strip_local pkg.
+
+
+Module MakeLadderstepPackage (PKG : PrePackage).
+  Module Import MakeLadderstepPackageInternal := MakePackageBase PKG.
+
+  Ltac get_Mxzladderstep_sig _ := get TAG.Mxzladderstep_sig.
+  Notation Mxzladderstep_sig := (ltac:(let v := get_Mxzladderstep_sig () in exact v)) (only parsing).
+End MakeLadderstepPackage.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/SquareFromMul.v b/src/Specific/Framework/ArithmeticSynthesis/SquareFromMul.v
new file mode 100644
index 000000000..8d8946923
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/SquareFromMul.v
@@ -0,0 +1,28 @@
+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 Crypto.Specific.Framework.CurveParameters.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics.
+Require Import Crypto.Util.Tactics.CacheTerm.
+Require Crypto.Util.Tuple.
+
+Local Notation tuple := Tuple.tuple.
+Local Open Scope list_scope.
+Local Open Scope Z_scope.
+Local Infix "^" := tuple : type_scope.
+
+Ltac pose_square_sig sz m wt mul_sig 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
+       Positional.Fdecode (m := m) wt (square a) = (eval a * eval a)%F}
+    ltac:(idtac;
+          let a := fresh "a" in
+          eexists; cbv beta zeta; intros a;
+          rewrite <-(proj2_sig mul_sig);
+          apply f_equal;
+          cbv [proj1_sig mul_sig];
+          reflexivity)
+           square_sig.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py
new file mode 100755
index 000000000..52f5e0f54
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py
@@ -0,0 +1,240 @@
+#!/usr/bin/env python
+from __future__ import with_statement
+import re, os
+import io
+
+PACKAGE_NAMES = [('../CurveParameters.v', [])]
+CP_LIST = ['../CurveParametersPackage.v']
+CP_BASE_LIST = ['../CurveParametersPackage.v', 'BasePackage.v']
+CP_BASE_DEFAULTS_LIST = ['../CurveParametersPackage.v', 'BasePackage.v', 'DefaultsPackage.v']
+CP_BASE_DEFAULTS_FREEZE_LADDERSTEP_LIST = ['../CurveParametersPackage.v', 'BasePackage.v', 'DefaultsPackage.v', 'FreezePackage.v', 'LadderstepPackage.v']
+NORMAL_PACKAGE_NAMES = [('Base.v', (CP_LIST, None)),
+                        ('Defaults.v', (CP_BASE_LIST, 'not_exists')),
+                        ('../ReificationTypes.v', (CP_BASE_LIST, None)),
+                        ('Freeze.v', (CP_BASE_LIST, 'not_exists')),
+                        ('Ladderstep.v', (CP_BASE_DEFAULTS_LIST, 'not_exists')),
+                        ('Karatsuba.v', (CP_BASE_DEFAULTS_LIST, 'goldilocks'))]
+ALL_FILE_NAMES = PACKAGE_NAMES + NORMAL_PACKAGE_NAMES # PACKAGE_CP_NAMES + WITH_CURVE_BASE_NAMES + ['../ReificationTypes.v']
+CONFIGS = ('goldilocks', )
+
+EXCLUDES = ('constr:((wt_divides_chain, wt_divides_chains))', )
+
+contents = {}
+lines = {}
+fns = {}
+
+PY_FILE_NAME = os.path.basename(__file__)
+
+def init_contents(lines=lines, contents=contents):
+    for fname, _ in ALL_FILE_NAMES:
+        with open(fname, 'r') as f:
+            contents[fname] = f.read()
+    lines.update(dict((k, v.split('\n')) for k, v in contents.items()))
+
+def strip_prefix(name, prefix='local_'):
+    if name.startswith(prefix): return name[len(prefix):]
+    return name
+
+def init_fns(lines=lines, fns=fns):
+    header = 'Ltac pose_'
+    for fname, _ in ALL_FILE_NAMES:
+        stripped_lines = [i.strip() for i in lines[fname]]
+        fns[fname] = [(strip_prefix(name, 'local_'), args.strip(), name.startswith('local_'))
+                      for line in stripped_lines
+                      if line.startswith(header)
+                      for name, args in re.findall('Ltac pose_([^ ]*' + ') ([A-Za-z0-9_\' ]*' + ')', line.strip())]
+
+def get_file_root(folder=os.path.dirname(__file__), filename='Makefile'):
+    dir_path = os.path.realpath(folder)
+    while not os.path.isfile(os.path.join(dir_path, filename)) and dir_path != '/':
+        dir_path = os.path.realpath(os.path.join(dir_path, '..'))
+    if not os.path.isfile(os.path.join(dir_path, filename)):
+        print('ERROR: Could not find Makefile in the root of %s' % folder)
+        raise Exception
+    return dir_path
+
+def modname_of_file_name(fname):
+    assert(fname[-2:] == '.v')
+    return 'Crypto.' + os.path.normpath(os.path.relpath(os.path.realpath(fname), os.path.join(root, 'src'))).replace(os.sep, '.')[:-2]
+
+def split_args(name, args_str, indent=''):
+    args = [arg.strip() for arg in args_str.split(' ')]
+    pass_args = [arg for arg in args if arg.startswith('P_')]
+    extract_args = [arg for arg in args if arg not in pass_args and arg != name]
+    if name not in args:
+        print('Error: %s not in %s' % (name, repr(args)))
+        assert(name in args)
+    assert(len(pass_args) + len(extract_args) + 1 == len(args))
+    pass_args_str = ' '.join(pass_args)
+    if pass_args_str != '': pass_args_str += ' '
+    extract_args_str = ''
+    nl_indent = ('\n%(indent)s  ' % locals())
+    if len(extract_args) > 0:
+        extract_args_str = nl_indent + nl_indent.join('let %s := Tag.get pkg TAG.%s in' % (arg, arg) for arg in extract_args)
+    return args, pass_args, extract_args, pass_args_str, extract_args_str
+
+def make_add_from_pose(name, args_str, indent='', only_if=None, local=False):
+    args, pass_args, extract_args, pass_args_str, extract_args_str = split_args(name, args_str, indent=indent)
+    ret = r'''%(indent)sLtac add_%(name)s pkg %(pass_args_str)s:=''' % locals()
+    local_str = ('local_' if local else '')
+    if_not_exists_str = ''
+    body = r'''%(extract_args_str)s
+%(indent)s  let %(name)s := fresh "%(name)s" in
+%(indent)s  ''' % locals()
+    body += r'''let %(name)s := pose_%(local_str)s%(name)s %(args_str)s in
+%(indent)s  ''' % locals()
+    if only_if == 'not_exists':
+        assert(not local)
+        body += 'constr:(%(name)s)' % locals()
+        body = body.strip('\n ').replace('\n', '\n                 ')
+        ret += r'''
+%(indent)s  Tag.update_by_tac_if_not_exists
+%(indent)s    pkg
+%(indent)s    TAG.%(name)s
+%(indent)s    ltac:(fun _ => %(body)s).''' % locals()
+    else:
+        body += r'''Tag.%(local_str)supdate pkg TAG.%(name)s %(name)s''' % locals()
+        if only_if is None:
+            ret += body + '.\n'
+        else:
+            body = body.strip('\n ').replace('\n', '\n                 ')
+            ret += r'''
+%(indent)s  if_%(only_if)s
+%(indent)s    pkg
+%(indent)s    ltac:(fun _ => %(body)s)
+%(indent)s    ltac:(fun _ => pkg)
+%(indent)s    ().''' % locals()
+    return ret
+
+def make_add_all(fname, indent=''):
+    modname, ext = os.path.splitext(os.path.basename(fname))
+    all_items = [(name, split_args(name, args_str, indent=indent)) for name, args_str, local in fns[fname]]
+    all_pass_args = []
+    for name, (args, pass_args, extract_args, pass_args_str, extract_args_str) in all_items:
+        for arg in pass_args:
+            if arg not in all_pass_args: all_pass_args.append(arg)
+    all_pass_args_str = ' '.join(all_pass_args)
+    if all_pass_args_str != '': all_pass_args_str += ' '
+    ret = r'''%(indent)sLtac add_%(modname)s_package pkg %(all_pass_args_str)s:=''' % locals()
+    nl_indent = ('\n%(indent)s  ' % locals())
+    ret += nl_indent + nl_indent.join('let pkg := add_%s pkg %sin' % (name, pass_args_str)
+                                      for name, (args, pass_args, extract_args, pass_args_str, extract_args_str) in all_items)
+    ret += nl_indent + 'Tag.strip_local pkg.\n'
+    return ret
+
+def make_if(name, indent=''):
+    ret = r'''%(indent)sLtac if_%(name)s pkg tac_true tac_false arg :=
+%(indent)s  let %(name)s := Tag.get pkg TAG.%(name)s in
+%(indent)s  let %(name)s := (eval vm_compute in (%(name)s : bool)) in
+%(indent)s  lazymatch %(name)s with
+%(indent)s  | true => tac_true arg
+%(indent)s  | false => tac_false arg
+%(indent)s  end.
+''' % locals()
+    return ret
+
+def write_if_changed(fname, value):
+    if os.path.isfile(fname):
+        with open(fname, 'r') as f:
+            old_value = f.read()
+        if old_value == value: return
+    value = unicode(value)
+    print('Writing %s...' % fname)
+    with io.open(fname, 'w', newline='\n') as f:
+        f.write(value)
+
+def do_replace(fname, headers, new_contents):
+    lines = contents[fname].split('\n')
+    ret = []
+    for line in lines:
+        if any(header in line for header in headers):
+            ret.append(new_contents)
+            break
+        else:
+            ret.append(line)
+    ret = unicode('\n'.join(ret))
+    write_if_changed(fname, ret)
+
+def get_existing_tags(fname, deps):
+    return set(name for dep in deps for name, args, local in fns[dep.replace('Package.v', '.v')])
+
+def make_package(fname, deps, extra_modname_prefix='', extra_imports=None, prefix=None, add_package=True):
+    py_file_name = PY_FILE_NAME
+    existing_tags = get_existing_tags(fname, deps)
+    full_mod = modname_of_file_name(fname)
+    modname, ext = os.path.splitext(os.path.basename(fname))
+    ret = (r'''(* This file is autogenerated from %(modname)s.v by %(py_file_name)s *)
+''' % locals())
+    if extra_imports is not None:
+        ret += extra_imports
+    ret += (r'''Require Export %(full_mod)s.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+''' % locals())
+    if prefix is not None:
+        ret += prefix
+    new_names = [name for name, args, local in fns[fname] if name not in existing_tags and not local]
+    if add_package: # and len(new_names) > 0:
+        ret += (r'''
+
+Module Make%(extra_modname_prefix)s%(modname)sPackage (PKG : PrePackage).
+  Module Import Make%(extra_modname_prefix)s%(modname)sPackageInternal := MakePackageBase PKG.
+''' % locals())
+        for name in new_names:
+            ret += ("\n  Ltac get_%s _ := get TAG.%s." % (name, name))
+            ret += ("\n  Notation %s := (ltac:(let v := get_%s () in exact v)) (only parsing)." % (name, name))
+        ret += ('\nEnd Make%(extra_modname_prefix)s%(modname)sPackage.\n' % locals())
+    return ret
+
+def make_tags(fname, deps):
+    existing_tags = get_existing_tags(fname, deps)
+    new_tags = [name for name, args, local in fns[fname] if name not in existing_tags]
+    if len(new_tags) == 0: return ''
+    names = ' | '.join(new_tags)
+    return r'''Module TAG.
+  Inductive tags := %s.
+End TAG.
+''' % names
+
+def write_package(fname, pkg):
+    pkg_name = fname[:-2] + 'Package.v'
+    write_if_changed(pkg_name, pkg)
+
+def update_CurveParameters(fname='../CurveParameters.v'):
+    endline = contents[fname].strip().split('\n')[-1]
+    assert(endline.startswith('End '))
+    header = '(* Everything below this line autogenerated by %s *)' % PY_FILE_NAME
+    assert(header in contents[fname])
+    ret = '  %s' % header
+    for name, args, local in fns[fname]:
+        ret += '\n' + make_add_from_pose(name, args, indent='  ', local=local)
+    ret += '\n' + make_add_all(fname, indent='  ')
+    ret += endline
+    prefix = ''
+    for name in CONFIGS:
+        prefix += '\n' + make_if(name, indent='')
+    pkg = make_package(fname, [], prefix=prefix)
+    do_replace(fname, (header,), ret)
+    write_package(fname, pkg)
+
+def make_normal_package(fname, deps, only_if=None):
+    prefix = ''
+    extra_imports = ''
+    for dep in deps:
+        extra_imports += 'Require Import %s.\n' % modname_of_file_name(dep)
+    prefix += '\n' + make_tags(fname, deps)
+    for name, args, local in fns[fname]:
+        prefix += '\n' + make_add_from_pose(name, args, indent='', only_if=only_if, local=local)
+    prefix += '\n' + make_add_all(fname, indent='')
+    return make_package(fname, deps, extra_imports=extra_imports, prefix=prefix)
+
+def update_normal_package(fname, deps, only_if=None):
+    pkg = make_normal_package(fname, deps, only_if=only_if)
+    write_package(fname, pkg)
+
+root = get_file_root()
+init_contents()
+init_fns()
+update_CurveParameters()
+for fname, (deps, only_if) in NORMAL_PACKAGE_NAMES:
+    update_normal_package(fname, deps, only_if=only_if)
diff --git a/src/Specific/Framework/ArithmeticSynthesisFramework.v b/src/Specific/Framework/ArithmeticSynthesisFramework.v
deleted file mode 100644
index 342c759fe..000000000
--- a/src/Specific/Framework/ArithmeticSynthesisFramework.v
+++ /dev/null
@@ -1,754 +0,0 @@
-Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
-Require Import Coq.Lists.List. Import ListNotations.
-Require Import Crypto.Arithmetic.Core. Import B.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Arithmetic.Saturated.Freeze.
-Require Crypto.Specific.Framework.CurveParameters.
-Require Import Crypto.Util.Decidable.
-Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.
-Require Import Crypto.Arithmetic.Karatsuba.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Crypto.Util.Tuple.
-Require Import Crypto.Util.IdfunWithAlt.
-Require Import Crypto.Util.Tactics.VM.
-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_chains carry_chains :=
-    let v := P.do_compute P.carry_chains in
-    cache_term v carry_chains.
-
-  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.
-  Ltac pose_goldilocks goldilocks :=
-    cache_term_with_type_by
-      bool
-      ltac:(let v := P.do_compute P.goldilocks in exact v)
-             goldilocks.
-  (* 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 helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chain :=
-    cache_term_with_type_by
-      (forall i (H:In i carry_chain), wt (S i) / wt i <> 0)
-      ltac:(let i := fresh "i" in intros i ?; exact (wt_divides' i))
-             wt_divides_chain.
-  Ltac pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains :=
-    lazymatch carry_chains with
-    | ?carry_chain :: nil
-      => helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chains
-    | ?carry_chain :: ?carry_chains
-      => let wt_divides_chains := fresh wt_divides_chains in
-         let wt_divides_chain := fresh wt_divides_chains in
-         let wt_divides_chain := helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chain in
-         let wt_divides_chains := pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains in
-         constr:((wt_divides_chain, wt_divides_chains))
-    end.
-  Ltac pose_wt_divides_chains wt carry_chains wt_divides' wt_divides_chains :=
-    let carry_chains := (eval cbv delta [carry_chains] in carry_chains) in
-    pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains.
-
-  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_half_sz sz half_sz :=
-    let v := (eval compute in (sz / 2)%nat) in
-    cache_term v half_sz.
-  Ltac pose_half_sz_nonzero half_sz half_sz_nonzero :=
-    cache_proof_with_type_by
-      (half_sz <> 0%nat)
-      ltac:(cbv; congruence)
-             half_sz_nonzero.
-
-  Ltac basesystem_partial_evaluation_RHS :=
-    let t0 := (match goal with
-               | |- _ _ ?t => t
-               end) in
-    let t :=
-     eval
-      cbv
-       delta [Positional.to_associational_cps Positional.to_associational
-             Positional.eval Positional.zeros Positional.add_to_nth_cps
-             Positional.add_to_nth Positional.place_cps Positional.place
-             Positional.from_associational_cps Positional.from_associational
-             Positional.carry_cps Positional.carry
-             Positional.chained_carries_cps Positional.chained_carries
-             Positional.sub_cps Positional.sub Positional.split_cps
-             Positional.scmul_cps Positional.unbalanced_sub_cps
-             Positional.negate_snd_cps Positional.add_cps Positional.opp_cps
-             Associational.eval Associational.multerm Associational.mul_cps
-             Associational.mul Associational.split_cps Associational.split
-             Associational.reduce_cps Associational.reduce
-             Associational.carryterm_cps Associational.carryterm
-             Associational.carry_cps Associational.carry
-             Associational.negate_snd_cps Associational.negate_snd div modulo
-             id_tuple_with_alt id_tuple'_with_alt
-             ]
-     in t0
-    in
-    let t := eval pattern @runtime_mul in t in
-    let t := (match t with
-              | ?t _ => t
-              end) in
-    let t := eval pattern @runtime_add in t in
-    let t := (match t with
-              | ?t _ => t
-              end) in
-    let t := eval pattern @runtime_opp in t in
-    let t := (match t with
-              | ?t _ => t
-              end) in
-    let t := eval pattern @runtime_shr in t in
-    let t := (match t with
-              | ?t _ => t
-              end) in
-    let t := eval pattern @runtime_and in t in
-    let t := (match t with
-              | ?t _ => t
-              end) in
-    let t := eval pattern @Let_In in t in
-    let t := (match t with
-              | ?t _ => t
-              end) in
-    let t := eval pattern @id_with_alt in t in
-    let t := (match t with
-              | ?t _ => t
-              end) in
-    let t1 := fresh "t1" in
-    pose (t1 := t);
-     transitivity
-      (t1 (@id_with_alt) (@Let_In) (@runtime_and) (@runtime_shr) (@runtime_opp) (@runtime_add)
-         (@runtime_mul));
-     [ replace_with_vm_compute t1; clear t1 | reflexivity ].
-
-  (** XXX TODO(jadep) FIXME: Is sqrt(s) the right thing to pass to goldilocks_mul_cps (the original code hard-coded 2^224 *)
-  Ltac pose_sqrt_s s sqrt_s :=
-    let v := (eval vm_compute in (Z.log2 s / 2)) in
-    cache_term (2^v) sqrt_s.
-
-  Ltac pose_goldilocks_mul_sig goldilocks sz wt s c half_sz sqrt_s goldilocks_mul_sig :=
-    lazymatch eval compute in goldilocks with
-    | true
-      => cache_term_with_type_by
-           {mul : (Z^sz -> Z^sz -> Z^sz)%type |
-            forall a b : Z^sz,
-              mul a b = goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt sqrt_s a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)}
-           ltac:(eexists; cbv beta zeta; intros;
-                 cbv [goldilocks_mul_cps];
-                 repeat autounfold;
-                 basesystem_partial_evaluation_RHS;
-                 do_replace_match_with_destructuring_match_in_goal;
-                 reflexivity)
-                  goldilocks_mul_sig
-    | false
-      => goldilocks_mul_sig
-    end.
-
-  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_mul_sig_from_goldilocks_mul_sig sz m wt s c half_sz sqrt_s goldilocks_mul_sig 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
-         Positional.Fdecode (m := m) wt (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:(
-                       goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt sqrt_s a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)) in
-            F_mod_eq;
-            transitivity (Positional.eval wt x); repeat autounfold;
-
-            [
-            | autorewrite with uncps push_id push_basesystem_eval;
-              apply goldilocks_mul_correct; try assumption; cbv; congruence ];
-            cbv [mod_eq]; apply f_equal2;
-            [ | reflexivity ];
-            apply f_equal;
-            etransitivity; [|apply (proj2_sig goldilocks_mul_sig)];
-            cbv [proj1_sig goldilocks_mul_sig];
-            reflexivity)
-             mul_sig.
-
-  Ltac pose_mul_sig_full goldilocks sz m wt s c sz2 half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig :=
-    lazymatch eval compute in goldilocks with
-    | true
-      => pose_mul_sig_from_goldilocks_mul_sig sz m wt s c half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig
-    | false
-      => pose_mul_sig sz m wt s c sz2 wt_nonzero mul_sig
-    end.
-
-  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.
-
-  Ltac pose_square_sig_from_mul_sig sz m wt mul_sig 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
-         Positional.Fdecode (m := m) wt (square a) = (eval a * eval a)%F}
-      ltac:(idtac;
-            let a := fresh "a" in
-            eexists; cbv beta zeta; intros a;
-            rewrite <-(proj2_sig mul_sig);
-            apply f_equal;
-            cbv [proj1_sig mul_sig];
-            reflexivity)
-             square_sig.
-
-  Ltac pose_square_sig_full goldilocks sz m wt s c sz2 wt_nonzero mul_sig square_sig :=
-    lazymatch eval compute in goldilocks with
-    | true
-      => pose_square_sig_from_mul_sig sz m wt mul_sig square_sig
-    | false
-      => pose_square_sig sz m wt s c sz2 wt_nonzero square_sig
-    end.
-
-  Ltac pose_proof_tuple ls :=
-    lazymatch ls with
-    | pair ?x ?y => pose_proof_tuple x; pose_proof_tuple y
-    | ?ls => pose proof ls
-    end.
-
-  Ltac make_chained_carries_cps' sz wt s c a carry_chains :=
-    lazymatch carry_chains with
-    | ?carry_chain :: nil
-      => constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain id)
-    | ?carry_chain :: ?carry_chains
-      => let r := fresh "r" in
-         let r' := fresh r in
-         constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain
-                (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r
-                (fun r' => ltac:(let v := make_chained_carries_cps' sz wt s c r' carry_chains in exact v))))
-    end.
-  Ltac make_chained_carries_cps sz wt s c a carry_chains :=
-    let carry_chains := (eval cbv delta [carry_chains] in carry_chains) in
-    make_chained_carries_cps' sz wt s c a carry_chains.
-  (* Performs a full carry loop (as specified by carry_chain) *)
-  Ltac pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains 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 div_mod;
-            pose_proof_tuple wt_divides_chains;
-            let x := make_chained_carries_cps sz wt s c a carry_chains 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_chains := fresh "carry_chains" in
-    let a24 := fresh "a24" in
-    let coef_div_modulus := fresh "coef_div_modulus" in
-    let goldilocks := fresh "goldilocks" 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_chains := fresh "wt_divides_chains" 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 half_sz := fresh "half_sz" in
-    let half_sz_nonzero := fresh "half_sz_nonzero" in
-    let sqrt_s := fresh "sqrt_s" in
-    let goldilocks_mul_sig := fresh "goldilocks_mul_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_chains := pose_carry_chains carry_chains in
-    let a24 := pose_a24 a24 in
-    let coef_div_modulus := pose_coef_div_modulus coef_div_modulus in
-    let goldilocks := pose_goldilocks goldilocks 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_chains := pose_wt_divides_chains wt carry_chains wt_divides' wt_divides_chains 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 half_sz := pose_half_sz sz half_sz in
-    let half_sz_nonzero := pose_half_sz_nonzero half_sz half_sz_nonzero in
-    let sqrt_s := pose_sqrt_s s sqrt_s in
-    let goldilocks_mul_sig := pose_goldilocks_mul_sig goldilocks sz wt s c half_sz sqrt_s goldilocks_mul_sig in
-    let mul_sig := pose_mul_sig_full goldilocks sz m wt s c sz2 half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig in
-    let square_sig := pose_square_sig_full goldilocks sz m wt s c sz2 wt_nonzero mul_sig square_sig in
-    let carry_sig := pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_chains).
-  Notation carry_chains := (ltac:(let v := get_carry_chains () in exact v)) (only parsing).
-  Ltac get_a24 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_goldilocks _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in goldilocks).
-  Notation goldilocks := (ltac:(let v := get_goldilocks () in exact v)) (only parsing).
-  Ltac get_m _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides_chains).
-  Notation wt_divides_chains := (ltac:(let v := get_wt_divides_chains () in exact v)) (only parsing).
-  Ltac get_zero_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_half_sz _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in half_sz).
-  Notation half_sz := (ltac:(let v := get_half_sz () in exact v)) (only parsing).
-  Ltac get_half_sz_nonzero _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in half_sz_nonzero).
-  Notation half_sz_nonzero := (ltac:(let v := get_half_sz_nonzero () in exact v)) (only parsing).
-  Ltac get_sqrt_s _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sqrt_s).
-  Notation sqrt_s := (ltac:(let v := get_sqrt_s () in exact v)) (only parsing).
-  Ltac get_mul_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, 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
index 2d0bf5152..7078d4bec 100644
--- a/src/Specific/Framework/CurveParameters.v
+++ b/src/Specific/Framework/CurveParameters.v
@@ -1,6 +1,8 @@
 Require Export Coq.ZArith.BinInt.
 Require Export Coq.Lists.List.
 Require Export Crypto.Util.ZUtil.Notations.
+Require Import Crypto.Util.Tactics.CacheTerm.
+Require Import Crypto.Util.TagList.
 Require Crypto.Util.Tuple.
 
 Module Export Notations.
@@ -23,7 +25,7 @@ Module Type CurveParameters.
   Parameter carry_chains
     : option (list (list nat)). (* defaults to [seq 0 (pred sz) :: (0 :: 1 :: nil) :: nil] *)
   Parameter a24 : option Z.
-  Parameter coef_div_modulus : nat.
+  Parameter coef_div_modulus : option nat.
 
   Parameter goldilocks : bool.
 
@@ -35,10 +37,15 @@ Module Type CurveParameters.
     : option (list nat). (* defaults to [bitwidth :: 2*bitwidth :: nil] *)
   Parameter freeze_extra_allowable_bit_widths
     : option (list nat). (* defaults to [8 :: nil] *)
+  Parameter modinv_fuel : option nat.
   Ltac extra_prove_mul_eq := idtac.
   Ltac extra_prove_square_eq := idtac.
 End CurveParameters.
 
+Module TAG.
+  Inductive tags := sz | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel.
+End TAG.
+
 Module FillCurveParameters (P : CurveParameters).
   Local Notation defaulted opt_v default
     := (match opt_v with
@@ -56,7 +63,7 @@ Module FillCurveParameters (P : CurveParameters).
   Definition c := P.c.
   Definition carry_chains := defaulted P.carry_chains [seq 0 (pred sz); [0; 1]]%nat.
   Definition a24 := defaulted P.a24 0.
-  Definition coef_div_modulus := P.coef_div_modulus.
+  Definition coef_div_modulus := defaulted P.coef_div_modulus 0%nat.
 
   Definition goldilocks := P.goldilocks.
 
@@ -74,11 +81,23 @@ Module FillCurveParameters (P : CurveParameters).
     end.
 
   Definition upper_bound_of_exponent
-    := defaulted P.upper_bound_of_exponent (fun exp => (2^exp + 2^(exp-3))%Z).
+    := defaulted P.upper_bound_of_exponent
+                 (fun exp => (2^exp + 2^(exp-3))%Z).
+  Local Notation list_8_if_not_exists ls :=
+    (if existsb (Nat.eqb 8) ls
+     then nil
+     else [8]%nat)
+      (only parsing).
   Definition allowable_bit_widths
-    := defaulted P.allowable_bit_widths (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil)%nat.
+    := 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.
+    := defaulted
+         P.freeze_extra_allowable_bit_widths
+         (list_8_if_not_exists allowable_bit_widths)
+         ++ allowable_bit_widths.
+  Definition modinv_fuel := defaulted P.modinv_fuel 10%nat.
 
   (* hack around https://coq.inria.fr/bugs/show_bug.cgi?id=5764 *)
   Ltac do_unfold v' :=
@@ -95,10 +114,11 @@ Module FillCurveParameters (P : CurveParameters).
     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 P_modinv_fuel := P.modinv_fuel in
     let v' := (eval cbv [id
                            List.app
-                           sz bitwidth s c carry_chains a24 coef_div_modulus goldilocks
-                           P_sz P_bitwidth P_s P_c P_carry_chains P_a24 P_coef_div_modulus P_goldilocks
+                           sz bitwidth s c carry_chains a24 coef_div_modulus goldilocks modinv_fuel
+                           P_sz P_bitwidth P_s P_c P_carry_chains P_a24 P_coef_div_modulus P_goldilocks P_modinv_fuel
                            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
@@ -112,4 +132,131 @@ Module FillCurveParameters (P : CurveParameters).
          (only parsing).
   Ltac extra_prove_mul_eq := P.extra_prove_mul_eq.
   Ltac extra_prove_square_eq := P.extra_prove_square_eq.
-End FillCurveParameters.
+
+  Local Notation P_sz := sz.
+  Local Notation P_bitwidth := bitwidth.
+  Local Notation P_s := s.
+  Local Notation P_c := c.
+  Local Notation P_carry_chains := carry_chains.
+  Local Notation P_a24 := a24.
+  Local Notation P_coef_div_modulus := coef_div_modulus.
+  Local Notation P_goldilocks := goldilocks.
+  Local Notation P_upper_bound_of_exponent := upper_bound_of_exponent.
+  Local Notation P_allowable_bit_widths := allowable_bit_widths.
+  Local Notation P_freeze_allowable_bit_widths := freeze_allowable_bit_widths.
+  Local Notation P_modinv_fuel := modinv_fuel.
+
+  Ltac pose_sz sz :=
+    cache_term_with_type_by
+      nat
+      ltac:(let v := do_compute P_sz in exact v)
+             sz.
+  Ltac pose_bitwidth bitwidth :=
+    cache_term_with_type_by
+      Z
+      ltac:(let v := 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 := do_unfold P_s in exact v)
+             s.
+  Ltac pose_c c :=
+    cache_term_with_type_by
+      (list limb)
+      ltac:(let v := do_compute P_c in exact v)
+             c.
+  Ltac pose_carry_chains carry_chains :=
+    let v := do_compute P_carry_chains in
+    cache_term v carry_chains.
+
+  Ltac pose_a24 a24 :=
+    let v := 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 := do_compute P_coef_div_modulus in exact v)
+             coef_div_modulus.
+  Ltac pose_goldilocks goldilocks :=
+    cache_term_with_type_by
+      bool
+      ltac:(let v := do_compute P_goldilocks in exact v)
+             goldilocks.
+
+  Ltac pose_modinv_fuel modinv_fuel :=
+    cache_term_with_type_by
+      nat
+      ltac:(let v := do_compute P_modinv_fuel in exact v)
+             modinv_fuel.
+
+  Ltac pose_upper_bound_of_exponent upper_bound_of_exponent :=
+    cache_term_with_type_by
+      (Z -> Z)
+      ltac:(let v := do_unfold P_upper_bound_of_exponent in exact v)
+             upper_bound_of_exponent.
+
+  (* Everything below this line autogenerated by remake_packages.py *)
+  Ltac add_sz pkg :=
+    let sz := fresh "sz" in
+    let sz := pose_sz sz in
+    Tag.update pkg TAG.sz sz.
+
+  Ltac add_bitwidth pkg :=
+    let bitwidth := fresh "bitwidth" in
+    let bitwidth := pose_bitwidth bitwidth in
+    Tag.update pkg TAG.bitwidth bitwidth.
+
+  Ltac add_s pkg :=
+    let s := fresh "s" in
+    let s := pose_s s in
+    Tag.update pkg TAG.s s.
+
+  Ltac add_c pkg :=
+    let c := fresh "c" in
+    let c := pose_c c in
+    Tag.update pkg TAG.c c.
+
+  Ltac add_carry_chains pkg :=
+    let carry_chains := fresh "carry_chains" in
+    let carry_chains := pose_carry_chains carry_chains in
+    Tag.update pkg TAG.carry_chains carry_chains.
+
+  Ltac add_a24 pkg :=
+    let a24 := fresh "a24" in
+    let a24 := pose_a24 a24 in
+    Tag.update pkg TAG.a24 a24.
+
+  Ltac add_coef_div_modulus pkg :=
+    let coef_div_modulus := fresh "coef_div_modulus" in
+    let coef_div_modulus := pose_coef_div_modulus coef_div_modulus in
+    Tag.update pkg TAG.coef_div_modulus coef_div_modulus.
+
+  Ltac add_goldilocks pkg :=
+    let goldilocks := fresh "goldilocks" in
+    let goldilocks := pose_goldilocks goldilocks in
+    Tag.update pkg TAG.goldilocks goldilocks.
+
+  Ltac add_modinv_fuel pkg :=
+    let modinv_fuel := fresh "modinv_fuel" in
+    let modinv_fuel := pose_modinv_fuel modinv_fuel in
+    Tag.update pkg TAG.modinv_fuel modinv_fuel.
+
+  Ltac add_upper_bound_of_exponent pkg :=
+    let upper_bound_of_exponent := fresh "upper_bound_of_exponent" in
+    let upper_bound_of_exponent := pose_upper_bound_of_exponent upper_bound_of_exponent in
+    Tag.update pkg TAG.upper_bound_of_exponent upper_bound_of_exponent.
+
+  Ltac add_CurveParameters_package pkg :=
+    let pkg := add_sz pkg in
+    let pkg := add_bitwidth pkg in
+    let pkg := add_s pkg in
+    let pkg := add_c pkg in
+    let pkg := add_carry_chains pkg in
+    let pkg := add_a24 pkg in
+    let pkg := add_coef_div_modulus pkg in
+    let pkg := add_goldilocks pkg in
+    let pkg := add_modinv_fuel pkg in
+    let pkg := add_upper_bound_of_exponent pkg in
+    Tag.strip_local pkg.
+End FillCurveParameters.
\ No newline at end of file
diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v
new file mode 100644
index 000000000..782ccdd22
--- /dev/null
+++ b/src/Specific/Framework/CurveParametersPackage.v
@@ -0,0 +1,38 @@
+(* This file is autogenerated from CurveParameters.v by remake_packages.py *)
+Require Export Crypto.Specific.Framework.CurveParameters.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+
+Ltac if_goldilocks pkg tac_true tac_false arg :=
+  let goldilocks := Tag.get pkg TAG.goldilocks in
+  let goldilocks := (eval vm_compute in (goldilocks : bool)) in
+  lazymatch goldilocks with
+  | true => tac_true arg
+  | false => tac_false arg
+  end.
+
+
+Module MakeCurveParametersPackage (PKG : PrePackage).
+  Module Import MakeCurveParametersPackageInternal := MakePackageBase PKG.
+
+  Ltac get_sz _ := get TAG.sz.
+  Notation sz := (ltac:(let v := get_sz () in exact v)) (only parsing).
+  Ltac get_bitwidth _ := get TAG.bitwidth.
+  Notation bitwidth := (ltac:(let v := get_bitwidth () in exact v)) (only parsing).
+  Ltac get_s _ := get TAG.s.
+  Notation s := (ltac:(let v := get_s () in exact v)) (only parsing).
+  Ltac get_c _ := get TAG.c.
+  Notation c := (ltac:(let v := get_c () in exact v)) (only parsing).
+  Ltac get_carry_chains _ := get TAG.carry_chains.
+  Notation carry_chains := (ltac:(let v := get_carry_chains () in exact v)) (only parsing).
+  Ltac get_a24 _ := get TAG.a24.
+  Notation a24 := (ltac:(let v := get_a24 () in exact v)) (only parsing).
+  Ltac get_coef_div_modulus _ := get TAG.coef_div_modulus.
+  Notation coef_div_modulus := (ltac:(let v := get_coef_div_modulus () in exact v)) (only parsing).
+  Ltac get_goldilocks _ := get TAG.goldilocks.
+  Notation goldilocks := (ltac:(let v := get_goldilocks () in exact v)) (only parsing).
+  Ltac get_modinv_fuel _ := get TAG.modinv_fuel.
+  Notation modinv_fuel := (ltac:(let v := get_modinv_fuel () in exact v)) (only parsing).
+  Ltac get_upper_bound_of_exponent _ := get TAG.upper_bound_of_exponent.
+  Notation upper_bound_of_exponent := (ltac:(let v := get_upper_bound_of_exponent () in exact v)) (only parsing).
+End MakeCurveParametersPackage.
diff --git a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v
index 41bef884c..687af2c9c 100644
--- a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v
+++ b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v
@@ -2,9 +2,12 @@
 Require Import Coq.ZArith.BinInt.
 Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.BoundedWord.
 Require Import Crypto.Util.Sigma.Lift.
 Require Import Crypto.Util.Sigma.Associativity.
 Require Import Crypto.Util.Sigma.MapProjections.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.Tactics.MoveLetIn.
 Require Import Crypto.Util.Tactics.DestructHead.
 
@@ -286,3 +289,6 @@ Ltac factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t :=
     repeat match goal with
            | [ H : feBW_small |- _ ] => destruct H as [? _]
            end ].
+
+Ltac op_sig_side_conditions_t _ :=
+  try (hnf; rewrite <- (ZRange.is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption.
diff --git a/src/Specific/Framework/Packages.v b/src/Specific/Framework/Packages.v
new file mode 100644
index 000000000..14b02b766
--- /dev/null
+++ b/src/Specific/Framework/Packages.v
@@ -0,0 +1,12 @@
+Require Import Crypto.Util.TagList.
+
+Module Type PrePackage.
+  Parameter package : Tag.Context.
+End PrePackage.
+
+Module MakePackageBase (PKG : PrePackage).
+  Ltac get_package _ := eval hnf in PKG.package.
+  Ltac get key :=
+    let pkg := get_package () in
+    Tag.get pkg key.
+End MakePackageBase.
diff --git a/src/Specific/Framework/ReificationTypes.v b/src/Specific/Framework/ReificationTypes.v
index 3a160e04d..872005958 100644
--- a/src/Specific/Framework/ReificationTypes.v
+++ b/src/Specific/Framework/ReificationTypes.v
@@ -15,7 +15,7 @@ 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 :=
+Ltac pose_local_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.
@@ -26,31 +26,40 @@ Ltac get_b_of upper_bound_of_exponent :=
 (* 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 :=
+Ltac pose_local_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 :=
+Ltac pose_local_bounds sz upper_bound_of_exponent bounds_exp bounds :=
+  let b_of := get_b_of upper_bound_of_exponent in
   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 :=
+Ltac pose_bound1 r bound1 :=
+  cache_term_with_type_by
+    zrange
+    ltac:(exact {| lower := 0 ; upper := Z.pos r-1 |})
+           bound1.
+
+Ltac pose_local_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 :=
+Ltac pose_local_adjusted_bitwidth' lgbitwidth adjusted_bitwidth' :=
   pose_term_with
     ltac:(fun _ => eval compute in (2^lgbitwidth)%nat)
-           bitwidth.
+           adjusted_bitwidth'.
+Ltac pose_adjusted_bitwidth adjusted_bitwidth' adjusted_bitwidth :=
+  cache_term adjusted_bitwidth' adjusted_bitwidth.
 
-Ltac pose_feZ sz feZ :=
+Ltac pose_local_feZ sz feZ :=
   pose_term_with
     ltac:(fun _ => constr:(tuple Z sz))
            feZ.
@@ -65,20 +74,20 @@ Ltac pose_feW_bounded feW bounds feW_bounded :=
     (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 :=
+Ltac pose_feBW sz adjusted_bitwidth' bounds feBW :=
   cache_term_with_type_by
     Type
-    ltac:(let v := eval cbv [bitwidth bounds] in (BoundedWord sz bitwidth bounds) in exact v)
+    ltac:(let v := eval cbv [adjusted_bitwidth' bounds] in (BoundedWord sz adjusted_bitwidth' bounds) in exact v)
            feBW.
 
 Lemma feBW_bounded_helper'
-      sz bitwidth bounds
-      (feBW := BoundedWord sz bitwidth bounds)
+      sz adjusted_bitwidth' bounds
+      (feBW := BoundedWord sz adjusted_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 (BoundedWordToZ sz adjusted_bitwidth' bounds a)
     <= B.Positional.eval wt (map upper bounds).
 Proof.
   let a := fresh "a" in
@@ -105,15 +114,15 @@ Proof.
       nia. } }
 Qed.
 Lemma feBW_bounded_helper
-      sz bitwidth bounds
-      (feBW := BoundedWord sz bitwidth bounds)
+      sz adjusted_bitwidth' bounds
+      (feBW := BoundedWord sz adjusted_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.
+      l <= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a) < u.
 Proof.
   intros [Hl Hu] a; split;
     [ eapply Z.le_trans | eapply Z.le_lt_trans ];
@@ -121,10 +130,10 @@ Proof.
     assumption.
 Qed.
 
-Ltac pose_feBW_bounded wt sz feBW bitwidth bounds m wt_nonneg feBW_bounded :=
+Ltac pose_feBW_bounded wt sz feBW adjusted_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);
+    (forall a : feBW, 0 <= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a) < 2 * Z.pos m)
+    ltac:(apply (@feBW_bounded_helper sz adjusted_bitwidth' bounds wt wt_nonneg);
           vm_compute; clear; split; congruence)
            feBW_bounded.
 
@@ -138,70 +147,3 @@ Ltac pose_phiBW feBW m wt phiBW :=
     (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/ReificationTypesPackage.v b/src/Specific/Framework/ReificationTypesPackage.v
new file mode 100644
index 000000000..4a868856e
--- /dev/null
+++ b/src/Specific/Framework/ReificationTypesPackage.v
@@ -0,0 +1,151 @@
+(* This file is autogenerated from ReificationTypes.v by remake_packages.py *)
+Require Import Crypto.Specific.Framework.CurveParametersPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
+Require Export Crypto.Specific.Framework.ReificationTypes.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+
+Module TAG.
+  Inductive tags := limb_widths | bounds_exp | bounds | bound1 | lgbitwidth | adjusted_bitwidth' | adjusted_bitwidth | feZ | feW | feW_bounded | feBW | feBW_bounded | phiW | phiBW.
+End TAG.
+
+Ltac add_limb_widths pkg :=
+  let wt := Tag.get pkg TAG.wt in
+  let sz := Tag.get pkg TAG.sz in
+  let limb_widths := fresh "limb_widths" in
+  let limb_widths := pose_local_limb_widths wt sz limb_widths in
+  Tag.local_update pkg TAG.limb_widths limb_widths.
+
+Ltac add_bounds_exp pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let limb_widths := Tag.get pkg TAG.limb_widths in
+  let bounds_exp := fresh "bounds_exp" in
+  let bounds_exp := pose_local_bounds_exp sz limb_widths bounds_exp in
+  Tag.local_update pkg TAG.bounds_exp bounds_exp.
+
+Ltac add_bounds pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let upper_bound_of_exponent := Tag.get pkg TAG.upper_bound_of_exponent in
+  let bounds_exp := Tag.get pkg TAG.bounds_exp in
+  let bounds := fresh "bounds" in
+  let bounds := pose_local_bounds sz upper_bound_of_exponent bounds_exp bounds in
+  Tag.local_update pkg TAG.bounds bounds.
+
+Ltac add_bound1 pkg :=
+  let r := Tag.get pkg TAG.r in
+  let bound1 := fresh "bound1" in
+  let bound1 := pose_bound1 r bound1 in
+  Tag.update pkg TAG.bound1 bound1.
+
+Ltac add_lgbitwidth pkg :=
+  let limb_widths := Tag.get pkg TAG.limb_widths in
+  let lgbitwidth := fresh "lgbitwidth" in
+  let lgbitwidth := pose_local_lgbitwidth limb_widths lgbitwidth in
+  Tag.local_update pkg TAG.lgbitwidth lgbitwidth.
+
+Ltac add_adjusted_bitwidth' pkg :=
+  let lgbitwidth := Tag.get pkg TAG.lgbitwidth in
+  let adjusted_bitwidth' := fresh "adjusted_bitwidth'" in
+  let adjusted_bitwidth' := pose_local_adjusted_bitwidth' lgbitwidth adjusted_bitwidth' in
+  Tag.local_update pkg TAG.adjusted_bitwidth' adjusted_bitwidth'.
+
+Ltac add_adjusted_bitwidth pkg :=
+  let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
+  let adjusted_bitwidth := fresh "adjusted_bitwidth" in
+  let adjusted_bitwidth := pose_adjusted_bitwidth adjusted_bitwidth' adjusted_bitwidth in
+  Tag.update pkg TAG.adjusted_bitwidth adjusted_bitwidth.
+
+Ltac add_feZ pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let feZ := fresh "feZ" in
+  let feZ := pose_local_feZ sz feZ in
+  Tag.local_update pkg TAG.feZ feZ.
+
+Ltac add_feW pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let lgbitwidth := Tag.get pkg TAG.lgbitwidth in
+  let feW := fresh "feW" in
+  let feW := pose_feW sz lgbitwidth feW in
+  Tag.update pkg TAG.feW feW.
+
+Ltac add_feW_bounded pkg :=
+  let feW := Tag.get pkg TAG.feW in
+  let bounds := Tag.get pkg TAG.bounds in
+  let feW_bounded := fresh "feW_bounded" in
+  let feW_bounded := pose_feW_bounded feW bounds feW_bounded in
+  Tag.update pkg TAG.feW_bounded feW_bounded.
+
+Ltac add_feBW pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
+  let bounds := Tag.get pkg TAG.bounds in
+  let feBW := fresh "feBW" in
+  let feBW := pose_feBW sz adjusted_bitwidth' bounds feBW in
+  Tag.update pkg TAG.feBW feBW.
+
+Ltac add_feBW_bounded pkg :=
+  let wt := Tag.get pkg TAG.wt in
+  let sz := Tag.get pkg TAG.sz in
+  let feBW := Tag.get pkg TAG.feBW in
+  let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
+  let bounds := Tag.get pkg TAG.bounds in
+  let m := Tag.get pkg TAG.m in
+  let wt_nonneg := Tag.get pkg TAG.wt_nonneg in
+  let feBW_bounded := fresh "feBW_bounded" in
+  let feBW_bounded := pose_feBW_bounded wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded in
+  Tag.update pkg TAG.feBW_bounded feBW_bounded.
+
+Ltac add_phiW pkg :=
+  let feW := Tag.get pkg TAG.feW in
+  let m := Tag.get pkg TAG.m in
+  let wt := Tag.get pkg TAG.wt in
+  let phiW := fresh "phiW" in
+  let phiW := pose_phiW feW m wt phiW in
+  Tag.update pkg TAG.phiW phiW.
+
+Ltac add_phiBW pkg :=
+  let feBW := Tag.get pkg TAG.feBW in
+  let m := Tag.get pkg TAG.m in
+  let wt := Tag.get pkg TAG.wt in
+  let phiBW := fresh "phiBW" in
+  let phiBW := pose_phiBW feBW m wt phiBW in
+  Tag.update pkg TAG.phiBW phiBW.
+
+Ltac add_ReificationTypes_package pkg :=
+  let pkg := add_limb_widths pkg in
+  let pkg := add_bounds_exp pkg in
+  let pkg := add_bounds pkg in
+  let pkg := add_bound1 pkg in
+  let pkg := add_lgbitwidth pkg in
+  let pkg := add_adjusted_bitwidth' pkg in
+  let pkg := add_adjusted_bitwidth pkg in
+  let pkg := add_feZ pkg in
+  let pkg := add_feW pkg in
+  let pkg := add_feW_bounded pkg in
+  let pkg := add_feBW pkg in
+  let pkg := add_feBW_bounded pkg in
+  let pkg := add_phiW pkg in
+  let pkg := add_phiBW pkg in
+  Tag.strip_local pkg.
+
+
+Module MakeReificationTypesPackage (PKG : PrePackage).
+  Module Import MakeReificationTypesPackageInternal := MakePackageBase PKG.
+
+  Ltac get_bound1 _ := get TAG.bound1.
+  Notation bound1 := (ltac:(let v := get_bound1 () in exact v)) (only parsing).
+  Ltac get_adjusted_bitwidth _ := get TAG.adjusted_bitwidth.
+  Notation adjusted_bitwidth := (ltac:(let v := get_adjusted_bitwidth () in exact v)) (only parsing).
+  Ltac get_feW _ := get TAG.feW.
+  Notation feW := (ltac:(let v := get_feW () in exact v)) (only parsing).
+  Ltac get_feW_bounded _ := get TAG.feW_bounded.
+  Notation feW_bounded := (ltac:(let v := get_feW_bounded () in exact v)) (only parsing).
+  Ltac get_feBW _ := get TAG.feBW.
+  Notation feBW := (ltac:(let v := get_feBW () in exact v)) (only parsing).
+  Ltac get_feBW_bounded _ := get TAG.feBW_bounded.
+  Notation feBW_bounded := (ltac:(let v := get_feBW_bounded () in exact v)) (only parsing).
+  Ltac get_phiW _ := get TAG.phiW.
+  Notation phiW := (ltac:(let v := get_phiW () in exact v)) (only parsing).
+  Ltac get_phiBW _ := get TAG.phiBW.
+  Notation phiBW := (ltac:(let v := get_phiBW () in exact v)) (only parsing).
+End MakeReificationTypesPackage.
diff --git a/src/Specific/Framework/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v
index 9c80efaa0..617a36212 100644
--- a/src/Specific/Framework/SynthesisFramework.v
+++ b/src/Specific/Framework/SynthesisFramework.v
@@ -1,72 +1,76 @@
-Require Import Crypto.Specific.Framework.ArithmeticSynthesisFramework.
-Require Import Crypto.Specific.Framework.ReificationTypes.
-Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.FreezePackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.KaratsubaPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.LadderstepPackage.
+Require Import Crypto.Specific.Framework.CurveParametersPackage.
+Require Import Crypto.Specific.Framework.ReificationTypesPackage.
+Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.BoundedWord.
+Require Import Crypto.Util.TagList.
+Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon.
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-Require Crypto.Specific.Framework.CurveParameters.
 
 Module Export Exports.
-  Export ArithmeticSynthesisFramework.Exports.
+  Export ArithmeticSynthesis.Defaults.Exports.
+  Export ArithmeticSynthesis.Freeze.Exports.
 End Exports.
 
-Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters).
-  Module AS := MakeArithmeticSynthesisTestTactics Curve.
+(* Alisases for exporting *)
+Module Type PrePackage := PrePackage.
+Module Tag.
+  Notation Context := Tag.Context (only parsing).
+End Tag.
 
-  Ltac get_synthesis_package _ :=
-    let arithmetic_synthesis_pkg := AS.get_ArithmeticSynthesis_package () in
-    lazymatch arithmetic_synthesis_pkg with
-    | (?sz, ?bitwidth, ?s, ?c, ?carry_chains, ?a24, ?coef_div_modulus, ?goldilocks, ?m, ?wt, ?sz2, ?m_enc, ?coef, ?coef_mod, ?sz_nonzero, ?wt_nonzero, ?wt_nonneg, ?wt_divides, ?wt_divides', ?wt_divides_chains, ?zero_sig, ?one_sig, ?a24_sig, ?add_sig, ?sub_sig, ?opp_sig, ?half_sz, ?half_sz_nonzero, ?sqrt_s, ?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))
-    | _ => let dummy := match goal with
-                        | _ => fail "Did you update get_ArithmeticSynthesis_package but forget to update get_synthesis_package?"
-                        end in
-           constr:(I : I)
-    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.
+Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters).
+  Module P := FillCurveParameters Curve.
 
-Local Notation eta2 x := (fst x, snd x) (only parsing).
-Local Notation eta3 x := (eta2 (fst x), snd x) (only parsing).
+  Ltac add_Synthesis_package pkg :=
+    let P_default_mul _ := P.default_mul in
+    let P_extra_prove_mul_eq _ := P.extra_prove_mul_eq in
+    let P_default_square _ := P.default_square in
+    let P_extra_prove_square_eq _ := P.extra_prove_square_eq in
+    let pkg := P.add_CurveParameters_package pkg in
+    let pkg := add_Base_package pkg in
+    let pkg := add_ReificationTypes_package pkg in
+    let pkg := add_Karatsuba_package pkg in
+    (* N.B. freeze is a "default" and must come after anything that may disable it *)
+    let pkg := add_Freeze_package pkg in
+    (* N.B. the Defaults must come after other possible ways of adding the _sig lemmas *)
+    let pkg := add_Defaults_package pkg P_default_mul P_extra_prove_mul_eq P_default_square P_extra_prove_square_eq in
+    (* N.B. Ladderstep must come after Defaults *)
+    let pkg := add_Ladderstep_package pkg in
+    pkg.
 
-Notation Synthesis_package'_Type :=
-  { ABC : _ & let '(a, b, c) := eta3 ABC in (a * b * c)%type } (only parsing).
+  Ltac get_Synthesis_package _ :=
+    let pkg := constr:(Tag.empty) in
+    add_Synthesis_package pkg.
 
-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.
+  Ltac make_Synthesis_package _ :=
+    let pkg := get_Synthesis_package () in
+    exact pkg.
+End MakeSynthesisTactics.
 
-Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : SynthesisPrePackage).
-  Module CP := CurveParameters.FillCurveParameters Curve.
+Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePackage).
+  Module P := 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.
+  Module CP := MakeCurveParametersPackage PKG.
+  Module BP := MakeBasePackage PKG.
+  Module DP := MakeDefaultsPackage PKG.
+  Module RP := MakeReificationTypesPackage PKG.
+  Module FP := MakeFreezePackage PKG.
+  Module LP := MakeLadderstepPackage PKG.
+  Module KP := MakeKaratsubaPackage PKG.
+  Include CP.
+  Include BP.
+  Include DP.
+  Include RP.
+  Include FP.
+  Include LP.
+  Include KP.
 
   Ltac synthesize_with_carry do_rewrite get_op_sig :=
     let carry_sig := get_carry_sig () in
@@ -75,7 +79,7 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis
     [ do_rewrite op_sig carry_sig; cbv_runtime
     | .. ];
     fin_preglue;
-    refine_reflectively_gen CP.allowable_bit_widths default.
+    refine_reflectively_gen P.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 :=
@@ -84,6 +88,7 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis
   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_opp _ := synthesize_1arg_with_carry get_opp_sig.
   Ltac synthesize_square _ := synthesize_1arg_with_carry get_square_sig.
   Ltac synthesize_freeze _ :=
     let freeze_sig := get_freeze_sig () in
@@ -92,7 +97,7 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis
     [ 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.
+    refine_reflectively_gen P.freeze_allowable_bit_widths anf.
   Ltac synthesize_xzladderstep _ :=
     let Mxzladderstep_sig := get_Mxzladderstep_sig () in
     let a24_sig := get_a24_sig () in
@@ -104,5 +109,6 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis
       cbv_runtime
     | .. ];
     finish_conjoined_preglue ();
-    refine_reflectively_gen CP.allowable_bit_widths default.
+    refine_reflectively_gen P.allowable_bit_widths default.
+
 End PackageSynthesis.
diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py
index 56c91e577..aeaef91db 100755
--- a/src/Specific/Framework/make_curve.py
+++ b/src/Specific/Framework/make_curve.py
@@ -1,6 +1,6 @@
 #!/usr/bin/env python
 from __future__ import with_statement
-import json, sys, os, math, re, shutil
+import json, sys, os, math, re, shutil, io
 
 def compute_bitwidth(base):
     return 2**int(math.ceil(math.log(base, 2)))
@@ -175,12 +175,13 @@ def nested_list_to_string(v):
         assert(False)
 
 def make_curve_parameters(parameters):
-    def fix_option(term):
+    def fix_option(term, scope_string=''):
         if not isinstance(term, str) and not isinstance(term, unicode):
             return term
         if term[:len('Some ')] != 'Some ' and term != 'None':
-            if ' ' in term: return 'Some (%s)' % term
-            return 'Some %s' % term
+            if ' ' in term and (term[0] + term[-1]) not in ('()', '[]'):
+                return 'Some (%s)%s' % (term, scope_string)
+            return 'Some %s%s' % (term, scope_string)
         return term
     replacements = dict(parameters)
     assert(all(ch in '0123456789^+- ' for ch in parameters['modulus']))
@@ -208,9 +209,13 @@ def make_curve_parameters(parameters):
                                          parameters.get(op + '_code', None),
                                          nargs,
                                          sz)
-    for k in ('upper_bound_of_exponent', 'allowable_bit_widths', 'freeze_extra_allowable_bit_widths'):
-        if k not in replacements.keys():
-            replacements[k] = 'None'
+    replacements['coef_div_modulus_raw'] = replacements.get('coef_div_modulus', '0')
+    for k, scope_string in (('upper_bound_of_exponent', ''),
+                            ('allowable_bit_widths', '%nat'),
+                            ('freeze_extra_allowable_bit_widths', '%nat'),
+                            ('coef_div_modulus', '%nat'),
+                            ('modinv_fuel', '%nat')):
+        replacements[k] = fix_option(nested_list_to_string(replacements.get(k, 'None')), scope_string=scope_string)
     for k in ('s', 'c', 'goldilocks'):
         replacements[k] = nested_list_to_string(replacements[k])
     for k in ('extra_prove_mul_eq', 'extra_prove_square_eq'):
@@ -232,7 +237,7 @@ Module Curve <: CurveParameters.
   Definition carry_chains : option (list (list nat)) := Eval vm_compute in %(carry_chains)s.
 
   Definition a24 : option Z := %(a24)s.
-  Definition coef_div_modulus : nat := %(coef_div_modulus)s%%nat. (* add %(coef_div_modulus)s*modulus before subtracting *)
+  Definition coef_div_modulus : option nat := %(coef_div_modulus)s. (* add %(coef_div_modulus_raw)s*modulus before subtracting *)
 
   Definition goldilocks : bool := %(goldilocks)s.
 
@@ -245,6 +250,7 @@ Module Curve <: CurveParameters.
   Definition upper_bound_of_exponent : option (Z -> Z) := %(upper_bound_of_exponent)s.
   Definition allowable_bit_widths : option (list nat) := %(allowable_bit_widths)s.
   Definition freeze_extra_allowable_bit_widths : option (list nat) := %(freeze_extra_allowable_bit_widths)s.
+  Definition modinv_fuel : option nat := %(modinv_fuel)s.
   Ltac extra_prove_mul_eq := %(extra_prove_mul_eq)s.
   Ltac extra_prove_square_eq := %(extra_prove_square_eq)s.
 End Curve.
@@ -257,12 +263,9 @@ Require Import %s.CurveParameters.
 
 Module Import T := MakeSynthesisTactics Curve.
 
-Module P <: SynthesisPrePackage.
-  Definition Synthesis_package' : Synthesis_package'_Type.
-  Proof. make_synthesis_package (). Defined.
-
-  Definition Synthesis_package
-    := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'.
+Module P <: PrePackage.
+  Definition package : Tag.Context.
+  Proof. make_Synthesis_package (). Defined.
 End P.
 
 Module Export S := PackageSynthesis Curve P.
@@ -282,6 +285,8 @@ Proof.
   Time synthesize_%(arg)s ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions %(arg)s.
 """ % {'prefix':prefix, 'arg':fearg[2:]}
     elif fearg in ('fesquare',):
         return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
@@ -296,6 +301,8 @@ Proof.
   Time synthesize_square ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions square.
 """ % {'prefix':prefix}
     elif fearg in ('freeze',):
         return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
@@ -310,11 +317,29 @@ Proof.
   Time synthesize_freeze ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions freeze.
 """ % {'prefix':prefix}
+    elif fearg in ('feopp',):
+        return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import %(prefix)s.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition %(arg)s :
+  { %(arg)s : feBW -> feBW
+  | forall a, phiBW (%(arg)s a) = F.%(arg)s (phiBW a) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_%(arg)s ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions %(arg)s.
+""" % {'prefix':prefix, 'arg':fearg[2:]}
     elif fearg in ('ladderstep', 'xzladderstep'):
         return r"""Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep.
 Require Import %(prefix)s.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
@@ -334,6 +359,8 @@ Proof.
   synthesize_xzladderstep ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions xzladderstep.
 """ % {'prefix':prefix}
     else:
         print('ERROR: Unsupported operation: %s' % fearg)
@@ -343,10 +370,12 @@ Time Defined.
 def make_display_arg(fearg, prefix):
     file_name = fearg
     function_name = fearg
-    if fearg in ('femul', 'fesub', 'feadd', 'fesquare'):
+    if fearg in ('femul', 'fesub', 'feadd', 'fesquare', 'feopp'):
         function_name = fearg[2:]
     elif fearg in ('freeze', 'xzladderstep'):
         pass
+    elif fearg in ('fenz',):
+        function_name = 'nonzero'
     elif fearg in ('ladderstep', ):
         function_name = 'xzladderstep'
     else:
@@ -404,12 +433,16 @@ def main(*args):
             if open(fname, 'r').read() == outputs[k]:
                 continue
         new_files.append(fname)
-        with open(fname, 'w') as f:
-            f.write(outputs[k])
+        with io.open(fname, 'w', newline='\n') as f:
+            f.write(unicode(outputs[k]))
             if fname[-len('compiler.sh'):] == 'compiler.sh':
                 mode = os.fstat(f.fileno()).st_mode
                 mode |= 0o111
-                os.fchmod(f.fileno(), mode & 0o7777)
+                mode &= 0o7777
+                if 'fchmod' in os.__dict__.keys():
+                    os.fchmod(f.fileno(), mode)
+                else:
+                    os.chmod(f.name, mode)
     if len(new_files) > 0:
         print('git add ' + ' '.join('"%s"' % i for i in new_files))
 
diff --git a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v
index aa8fd5614..9fe08de2c 100644
--- a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v
+++ b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v
@@ -14,7 +14,7 @@ Module Curve <: CurveParameters.
   Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [[3; 7]; [0; 4; 1; 5; 2; 6; 3; 7]; [4; 0]]%nat.
 
   Definition a24 : option Z := None.
-  Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *)
+  Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *)
 
   Definition goldilocks : bool := true.
 
@@ -27,6 +27,7 @@ Module Curve <: CurveParameters.
   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.
+  Definition modinv_fuel : option nat := None.
   Ltac extra_prove_mul_eq := idtac.
   Ltac extra_prove_square_eq := idtac.
 End Curve.
diff --git a/src/Specific/X2448/Karatsuba/C64/Synthesis.v b/src/Specific/X2448/Karatsuba/C64/Synthesis.v
index 8ea8aa5c9..500671c90 100644
--- a/src/Specific/X2448/Karatsuba/C64/Synthesis.v
+++ b/src/Specific/X2448/Karatsuba/C64/Synthesis.v
@@ -3,12 +3,9 @@ Require Import Crypto.Specific.X2448.Karatsuba.C64.CurveParameters.
 
 Module Import T := MakeSynthesisTactics Curve.
 
-Module P <: SynthesisPrePackage.
-  Definition Synthesis_package' : Synthesis_package'_Type.
-  Proof. make_synthesis_package (). Defined.
-
-  Definition Synthesis_package
-    := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'.
+Module P <: PrePackage.
+  Definition package : Tag.Context.
+  Proof. make_Synthesis_package (). Defined.
 End P.
 
 Module Export S := PackageSynthesis Curve P.
diff --git a/src/Specific/X2448/Karatsuba/C64/femul.v b/src/Specific/X2448/Karatsuba/C64/femul.v
index 2f890a88f..07dd9b26d 100644
--- a/src/Specific/X2448/Karatsuba/C64/femul.v
+++ b/src/Specific/X2448/Karatsuba/C64/femul.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_mul ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions mul.
diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v
index e8a46ea9e..6324acfca 100644
--- a/src/Specific/X25519/C32/CurveParameters.v
+++ b/src/Specific/X25519/C32/CurveParameters.v
@@ -14,7 +14,7 @@ Module Curve <: CurveParameters.
   Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat.
 
   Definition a24 : option Z := Some 121665.
-  Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *)
+  Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *)
 
   Definition goldilocks : bool := false.
 
@@ -245,6 +245,7 @@ Module Curve <: CurveParameters.
   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.
+  Definition modinv_fuel : option nat := None.
   Ltac extra_prove_mul_eq := idtac.
   Ltac extra_prove_square_eq := idtac.
 End Curve.
diff --git a/src/Specific/X25519/C32/Synthesis.v b/src/Specific/X25519/C32/Synthesis.v
index 3b9b35078..0b3336b20 100644
--- a/src/Specific/X25519/C32/Synthesis.v
+++ b/src/Specific/X25519/C32/Synthesis.v
@@ -3,12 +3,9 @@ Require Import Crypto.Specific.X25519.C32.CurveParameters.
 
 Module Import T := MakeSynthesisTactics Curve.
 
-Module P <: SynthesisPrePackage.
-  Definition Synthesis_package' : Synthesis_package'_Type.
-  Proof. make_synthesis_package (). Defined.
-
-  Definition Synthesis_package
-    := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'.
+Module P <: PrePackage.
+  Definition package : Tag.Context.
+  Proof. make_Synthesis_package (). Defined.
 End P.
 
 Module Export S := PackageSynthesis Curve P.
diff --git a/src/Specific/X25519/C32/femul.v b/src/Specific/X25519/C32/femul.v
index 81bf1f255..bc62814e9 100644
--- a/src/Specific/X25519/C32/femul.v
+++ b/src/Specific/X25519/C32/femul.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_mul ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions mul.
diff --git a/src/Specific/X25519/C32/fesquare.v b/src/Specific/X25519/C32/fesquare.v
index 3fa837bd2..2bea3bf8b 100644
--- a/src/Specific/X25519/C32/fesquare.v
+++ b/src/Specific/X25519/C32/fesquare.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_square ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions square.
diff --git a/src/Specific/X25519/C32/freeze.v b/src/Specific/X25519/C32/freeze.v
index 9af1e8e0f..bac5a019f 100644
--- a/src/Specific/X25519/C32/freeze.v
+++ b/src/Specific/X25519/C32/freeze.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_freeze ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions freeze.
diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v
index 54c578a08..78db9dd8e 100644
--- a/src/Specific/X25519/C64/CurveParameters.v
+++ b/src/Specific/X25519/C64/CurveParameters.v
@@ -14,7 +14,7 @@ Module Curve <: CurveParameters.
   Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat.
 
   Definition a24 : option Z := Some 121665.
-  Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *)
+  Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *)
 
   Definition goldilocks : bool := false.
 
@@ -62,6 +62,7 @@ Module Curve <: CurveParameters.
   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.
+  Definition modinv_fuel : option nat := None.
   Ltac extra_prove_mul_eq := idtac.
   Ltac extra_prove_square_eq := idtac.
 End Curve.
diff --git a/src/Specific/X25519/C64/Synthesis.v b/src/Specific/X25519/C64/Synthesis.v
index 3c3bac04d..2ea78caba 100644
--- a/src/Specific/X25519/C64/Synthesis.v
+++ b/src/Specific/X25519/C64/Synthesis.v
@@ -3,12 +3,9 @@ Require Import Crypto.Specific.X25519.C64.CurveParameters.
 
 Module Import T := MakeSynthesisTactics Curve.
 
-Module P <: SynthesisPrePackage.
-  Definition Synthesis_package' : Synthesis_package'_Type.
-  Proof. make_synthesis_package (). Defined.
-
-  Definition Synthesis_package
-    := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'.
+Module P <: PrePackage.
+  Definition package : Tag.Context.
+  Proof. make_Synthesis_package (). Defined.
 End P.
 
 Module Export S := PackageSynthesis Curve P.
diff --git a/src/Specific/X25519/C64/femul.v b/src/Specific/X25519/C64/femul.v
index 1e015ddd9..7292df912 100644
--- a/src/Specific/X25519/C64/femul.v
+++ b/src/Specific/X25519/C64/femul.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_mul ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions mul.
diff --git a/src/Specific/X25519/C64/fesquare.v b/src/Specific/X25519/C64/fesquare.v
index cfad2d111..fa692f559 100644
--- a/src/Specific/X25519/C64/fesquare.v
+++ b/src/Specific/X25519/C64/fesquare.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_square ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions square.
diff --git a/src/Specific/X25519/C64/freeze.v b/src/Specific/X25519/C64/freeze.v
index ef826dba5..2c7fe8b85 100644
--- a/src/Specific/X25519/C64/freeze.v
+++ b/src/Specific/X25519/C64/freeze.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_freeze ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions freeze.
diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v
index adb20912e..fc62c9317 100644
--- a/src/Specific/X25519/C64/ladderstep.v
+++ b/src/Specific/X25519/C64/ladderstep.v
@@ -1,6 +1,6 @@
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep.
 Require Import Crypto.Specific.X25519.C64.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
@@ -20,3 +20,5 @@ Proof.
   synthesize_xzladderstep ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions xzladderstep.
diff --git a/src/Specific/X2555/C128/CurveParameters.v b/src/Specific/X2555/C128/CurveParameters.v
index 40c57e8e0..bb4384cc2 100644
--- a/src/Specific/X2555/C128/CurveParameters.v
+++ b/src/Specific/X2555/C128/CurveParameters.v
@@ -14,7 +14,7 @@ Module Curve <: CurveParameters.
   Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat.
 
   Definition a24 : option Z := Some (121665 (* XXX TODO(andreser) FIXME?  Is this right for this curve? *)).
-  Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *)
+  Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *)
 
   Definition goldilocks : bool := false.
 
@@ -27,6 +27,7 @@ Module Curve <: CurveParameters.
   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.
+  Definition modinv_fuel : option nat := None.
   Ltac extra_prove_mul_eq := idtac.
   Ltac extra_prove_square_eq := idtac.
 End Curve.
diff --git a/src/Specific/X2555/C128/Synthesis.v b/src/Specific/X2555/C128/Synthesis.v
index f88491af2..1fa3b4a6c 100644
--- a/src/Specific/X2555/C128/Synthesis.v
+++ b/src/Specific/X2555/C128/Synthesis.v
@@ -3,12 +3,9 @@ Require Import Crypto.Specific.X2555.C128.CurveParameters.
 
 Module Import T := MakeSynthesisTactics Curve.
 
-Module P <: SynthesisPrePackage.
-  Definition Synthesis_package' : Synthesis_package'_Type.
-  Proof. make_synthesis_package (). Defined.
-
-  Definition Synthesis_package
-    := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'.
+Module P <: PrePackage.
+  Definition package : Tag.Context.
+  Proof. make_Synthesis_package (). Defined.
 End P.
 
 Module Export S := PackageSynthesis Curve P.
diff --git a/src/Specific/X2555/C128/ladderstep.v b/src/Specific/X2555/C128/ladderstep.v
index b1d83df4a..902b6c1b0 100644
--- a/src/Specific/X2555/C128/ladderstep.v
+++ b/src/Specific/X2555/C128/ladderstep.v
@@ -1,6 +1,6 @@
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep.
 Require Import Crypto.Specific.X2555.C128.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
@@ -20,3 +20,5 @@ Proof.
   synthesize_xzladderstep ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions xzladderstep.