Move more of carry_sig, zero_sig, one_sig, etc to gallina

After    | File Name                                                | Before   || Change
-------------------------------------------------------------------------------------------
8m28.18s | Total                                                    | 8m28.73s || -0m00.55s
-------------------------------------------------------------------------------------------
0m06.23s | Specific/X25519/C64/Synthesis                            | 0m09.93s || -0m03.69s
3m28.42s | Specific/X25519/C64/ladderstep                           | 3m26.20s || +0m02.22s
0m02.19s | Specific/Framework/ArithmeticSynthesis/Defaults          | 0m00.71s || +0m01.48s
2m03.48s | Specific/NISTP256/AMD64/femul                            | 2m04.36s || -0m00.87s
0m24.97s | Specific/X25519/C64/femul                                | 0m24.56s || +0m00.41s
0m24.38s | Specific/NISTP256/AMD64/fesub                            | 0m23.90s || +0m00.48s
0m21.75s | Specific/NISTP256/AMD64/feadd                            | 0m21.87s || -0m00.12s
0m20.38s | Specific/X25519/C64/freeze                               | 0m20.04s || +0m00.33s
0m19.57s | Specific/X25519/C64/fesquare                             | 0m19.83s || -0m00.25s
0m17.47s | Specific/NISTP256/AMD64/feopp                            | 0m17.87s || -0m00.40s
0m15.16s | Specific/NISTP256/AMD64/fenz                             | 0m15.40s || -0m00.24s
0m08.25s | Specific/NISTP256/AMD64/Synthesis                        | 0m08.38s || -0m00.13s
0m04.01s | Specific/Framework/ArithmeticSynthesis/Montgomery        | 0m03.90s || +0m00.10s
0m01.06s | Specific/Framework/ArithmeticSynthesis/Base              | 0m01.06s || +0m00.00s
0m01.01s | Specific/Framework/SynthesisFramework                    | 0m00.95s || +0m00.06s
0m00.90s | Specific/Framework/ArithmeticSynthesis/HelperTactics     | 0m00.90s || +0m00.00s
0m00.86s | Specific/Framework/ArithmeticSynthesis/Freeze            | 0m00.75s || +0m00.10s
0m00.82s | Specific/Framework/MontgomeryReificationTypesPackage     | 0m00.78s || +0m00.03s
0m00.81s | Specific/Framework/ArithmeticSynthesis/Karatsuba         | 0m00.75s || +0m00.06s
0m00.79s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.72s || +0m00.07s
0m00.77s | Specific/Framework/ReificationTypesPackage               | 0m00.76s || +0m00.01s
0m00.75s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.75s || +0m00.00s
0m00.75s | Specific/Framework/ArithmeticSynthesis/FreezePackage     | 0m00.74s || +0m00.01s
0m00.72s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage  | 0m00.72s || +0m00.00s
0m00.69s | Specific/Framework/ArithmeticSynthesis/BasePackage       | 0m00.73s || -0m00.04s
0m00.68s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage   | 0m00.76s || -0m00.07s
0m00.67s | Specific/Framework/ArithmeticSynthesis/SquareFromMul     | 0m00.78s || -0m00.10s
0m00.32s | Specific/Framework/CurveParameters                       | 0m00.31s || +0m00.01s
0m00.32s | Specific/Framework/CurveParametersPackage                | 0m00.33s || -0m00.01s

13 files changed, 508 insertions, 159 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v
index db209c9f1..42c49f46d 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v
@@ -1,12 +1,15 @@
 Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
 Require Import Coq.Lists.List. Import ListNotations.
+Require Import Crypto.Arithmetic.CoreUnfolder.
 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.Specific.Framework.ArithmeticSynthesis.Base.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.PoseTermWithName.
 Require Import Crypto.Util.Tactics.CacheTerm.
 Require Crypto.Util.Tuple.
@@ -29,32 +32,317 @@ Ltac solve_constant_sig :=
        (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
+Local Ltac solve_constant_local_sig :=
+  idtac;
+  lazymatch goal with
+  | [ |- { c : Z^?sz | Positional.Fdecode (m:=?M) ?wt c = ?v } ]
+    => (exists (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt (F.to_Z (m:=M) v)));
+       lazymatch goal with
+       | [ sz_nonzero : sz <> 0%nat, sz_le_log2_m : Z.of_nat sz <= Z.log2_up (Z.pos M) |- _ ]
+         => clear -sz_nonzero sz_le_log2_m
+       end
+  end;
+  abstract (
+      setoid_rewrite Positional.Fdecode_Fencode_id;
+      [ reflexivity
+      | auto using wt_gen0_1, wt_gen_nonzero, wt_gen_divides', div_mod.. ]
+    ).
+
+Section gen.
+  Context (m : positive)
+          (sz : nat)
+          (s : Z)
+          (c : list limb)
+          (carry_chains : list (list nat))
+          (coef : Z^sz)
+          (mul_code : option (Z^sz -> Z^sz -> Z^sz))
+          (square_code : option (Z^sz -> Z^sz))
+          (sz_nonzero : sz <> 0%nat)
+          (s_nonzero : s <> 0)
+          (sz_le_log2_m : Z.of_nat sz <= Z.log2_up (Z.pos m)).
+
+  Local Notation wt := (wt_gen m sz).
+  Local Notation sz2 := (sz2' sz).
+  Local Notation wt_divides' := (wt_gen_divides' m sz sz_nonzero sz_le_log2_m).
+  Local Notation wt_nonzero := (wt_gen_nonzero m sz).
+
+  (* side condition needs cbv [Positional.mul_cps Positional.reduce_cps]. *)
+  Context (mul_code_correct
+           : match mul_code with
+             | None => True
+             | Some v
+               => forall a b,
+                 v a b
+                 = Positional.mul_cps (n:=sz) (m:=sz2) wt a b
+                                      (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)
+             end)
+          (square_code_correct
+           : match square_code with
+             | None => True
+             | Some v
+               => forall a,
+                 v a
+                 = Positional.mul_cps (n:=sz) (m:=sz2) wt a a
+                                      (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)
+             end).
+
+  Context (coef_mod : mod_eq m (Positional.eval wt coef) 0)
+          (m_correct : Z.pos m = s - Associational.eval c).
+
+
+  (* Performs a full carry loop (as specified by carry_chain) *)
+  Definition carry_sig'
+    : { carry : (Z^sz -> Z^sz)%type
+      | forall a : Z^sz,
+          let eval := Positional.Fdecode (m := m) wt in
+          eval (carry a) = eval a }.
+  Proof.
+    let a := fresh "a" in
+    eexists; cbv beta zeta; intros a.
+    pose proof (wt_gen0_1 m sz).
+    pose proof wt_nonzero; pose proof div_mod.
+    pose proof (wt_gen_divides_chains m sz sz_nonzero sz_le_log2_m carry_chains).
+    pose proof wt_divides'.
+    let x := constr:(chained_carries' sz wt s c a carry_chains) in
+    presolve_op_F constr:(wt) x;
+      [ cbv [chained_carries_cps' chained_carries_cps'_step];
+        autorewrite with pattern_runtime;
+        reflexivity
+      | ].
+    { cbv [chained_carries'].
+      change a with (id a) at 2.
+      revert a; induction carry_chains as [|carry_chain carry_chains' IHcarry_chains];
+        [ reflexivity | destruct_head_hnf' and ]; intros.
+      rewrite step_chained_carries_cps'.
+      destruct (length carry_chains') eqn:Hlenc.
+      { destruct carry_chains'; [ | simpl in Hlenc; congruence ].
+        destruct_head'_and;
+          autorewrite with uncps push_id push_basesystem_eval;
+          reflexivity. }
+      { repeat autounfold;
+          autorewrite with uncps push_id push_basesystem_eval.
+        unfold chained_carries'.
+        rewrite IHcarry_chains by auto.
+        repeat autounfold; autorewrite with uncps push_id push_basesystem_eval.
+        rewrite Positional.eval_carry by auto.
+        rewrite Positional.eval_chained_carries by auto; reflexivity. } }
+  Defined.
+
+  Definition constant_sig' v
+    : { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = v}.
+  Proof. solve_constant_local_sig. Defined.
+
+  Definition zero_sig'
+    : { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F}
+    := Eval hnf in constant_sig' _.
+
+  Definition one_sig'
+    : { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 1%F}
+    := Eval hnf in constant_sig' _.
+
+  Definition add_sig'
+    : { add : (Z^sz -> Z^sz -> Z^sz)%type
+      | forall a b : Z^sz,
+          let eval := Positional.Fdecode (m:=m) wt in
+          eval (add a b) = (eval a + eval b)%F }.
+  Proof.
+    eexists; cbv beta zeta; intros a b.
+    pose proof wt_nonzero.
+    pose proof (wt_gen0_1 m sz).
+    let x := constr:(
+               Positional.add_cps (n := sz) wt a b id) in
+    presolve_op_F constr:(wt) x;
+      [ autorewrite with pattern_runtime; reflexivity | ].
+    reflexivity.
+  Defined.
+
+  Definition sub_sig'
+    : { sub : (Z^sz -> Z^sz -> Z^sz)%type
+      | forall a b : Z^sz,
+          let eval := Positional.Fdecode (m:=m) wt in
+          eval (sub a b) = (eval a - eval b)%F }.
+  Proof.
+    let a := fresh "a" in
+    let b := fresh "b" in
+    eexists; cbv beta zeta; intros a b.
+    pose proof wt_nonzero.
+    pose proof (wt_gen0_1 m sz).
+    let x := constr:(
+               Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in
+    presolve_op_F constr:(wt) x;
+      [ autorewrite with pattern_runtime; reflexivity | ].
+    reflexivity.
+  Defined.
+
+  Definition opp_sig'
+    : { opp : (Z^sz -> Z^sz)%type
+      | forall a : Z^sz,
+          let eval := Positional.Fdecode (m := m) wt in
+          eval (opp a) = F.opp (eval a) }.
+  Proof.
+    eexists; cbv beta zeta; intros a.
+    pose proof wt_nonzero.
+    pose proof (wt_gen0_1 m sz).
+    let x := constr:(
+               Positional.opp_cps (n:=sz) (coef := coef) wt a id) in
+    presolve_op_F constr:(wt) x;
+      [ autorewrite with pattern_runtime; reflexivity | ].
+    reflexivity.
+  Defined.
+
+  Definition mul_sig'
+    : { mul : (Z^sz -> Z^sz -> Z^sz)%type
+      | forall a b : Z^sz,
+          let eval := Positional.Fdecode (m := m) wt in
+          eval (mul a b) = (eval a * eval b)%F }.
+  Proof.
+    eexists; cbv beta zeta; intros a b.
+    pose proof wt_nonzero.
+    pose proof (wt_gen0_1 m sz).
+    pose proof (sz2'_nonzero sz sz_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
+    presolve_op_F constr:(wt) x; [ | reflexivity ].
+    let rhs := match goal with |- _ = ?rhs => rhs end in
+    transitivity (match mul_code with
+                  | None => rhs
+                  | Some v => v a b
+                  end);
+      [ reflexivity | ].
+    destruct mul_code; try reflexivity.
+    transitivity (Positional.mul_cps (n:=sz) (m:=sz2) wt a b
+                                     (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)); [ | reflexivity ].
+    auto.
+  Defined.
+
+  Definition square_sig'
+    : { square : (Z^sz -> Z^sz)%type
+      | forall a : Z^sz,
+          let eval := Positional.Fdecode (m := m) wt in
+          eval (square a) = (eval a * eval a)%F }.
+  Proof.
+    eexists; cbv beta zeta; intros a.
+    pose proof wt_nonzero.
+    pose proof (wt_gen0_1 m sz).
+    pose proof (sz2'_nonzero sz sz_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
+    presolve_op_F constr:(wt) x; [ | reflexivity ].
+    let rhs := match goal with |- _ = ?rhs => rhs end in
+    transitivity (match square_code with
+                  | None => rhs
+                  | Some v => v a
+                  end);
+      [ reflexivity | ].
+    destruct square_code; try reflexivity.
+    transitivity (Positional.mul_cps (n:=sz) (m:=sz2) wt a a
+                                     (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)); [ | reflexivity ].
+    auto.
+  Defined.
+
+  Let ring_pkg : { T : _ & T }.
+  Proof.
+    eexists.
+    refine (fun zero_sig one_sig add_sig sub_sig mul_sig opp_sig
+            => 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 := _)
+                 (phi'_one := _)
+                 (phi'_opp := _)
+                 (Positional.Fdecode_Fencode_id
+                    (sz_nonzero := sz_nonzero)
+                    (div_mod := div_mod)
+                    wt (wt_gen0_1 m sz) wt_nonzero wt_divides')
+                 (Positional.eq_Feq_iff wt)
+                 _ _ _);
+      lazymatch goal with
+      | [ |- context[@proj1_sig ?A ?P ?x] ]
+        => pattern (@proj1_sig A P x);
+             exact (@proj2_sig A P x)
+      end.
+  Defined.
+
+  Definition ring' zero_sig one_sig add_sig sub_sig mul_sig opp_sig
+    := Eval cbv [ring_pkg projT2] in
+        projT2 ring_pkg zero_sig one_sig add_sig sub_sig mul_sig opp_sig.
+End gen.
+
+Ltac internal_solve_code_correct P_tac :=
+  hnf;
+  lazymatch goal with
+  | [ |- True ] => constructor
+  | _
+    => cbv [Positional.mul_cps Positional.reduce_cps];
+       intros;
+       autorewrite with pattern_runtime;
+       repeat autounfold;
+       autorewrite with pattern_runtime;
+       basesystem_partial_evaluation_RHS;
+       P_tac ();
+       break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring
+  end.
+
+Ltac pose_mul_code_correct P_extra_prove_mul_eq sz sz2 wt s c mul_code mul_code_correct :=
+  cache_proof_with_type_by
+    (match mul_code with
+     | None => True
+     | Some v
+       => forall a b,
+         v a b
+         = Positional.mul_cps (n:=sz) (m:=sz2) wt a b
+                              (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)
+     end)
+    ltac:(internal_solve_code_correct P_extra_prove_mul_eq)
+           mul_code_correct.
+
+Ltac pose_square_code_correct P_extra_prove_square_eq sz sz2 wt s c square_code square_code_correct :=
+  cache_proof_with_type_by
+    (match square_code with
+     | None => True
+     | Some v
+       => forall a,
+         v a
+         = Positional.mul_cps (n:=sz) (m:=sz2) wt a a
+                              (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)
+     end)
+    ltac:(internal_solve_code_correct P_extra_prove_square_eq)
+           square_code_correct.
+
+Ltac cache_sig_with_type_by_existing_sig ty existing_sig id :=
+  cache_sig_with_type_by_existing_sig_helper
+    ltac:(fun _ => cbv [carry_sig' constant_sig' zero_sig' one_sig' add_sig' sub_sig' mul_sig' square_sig' opp_sig'])
+           ty existing_sig id.
+
+Ltac pose_carry_sig sz m wt s c carry_chains carry_sig :=
+  cache_sig_with_type_by_existing_sig
     {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
+    (carry_sig' m sz s c carry_chains)
+    carry_sig.
+
+Ltac pose_zero_sig sz m wt sz_nonzero sz_le_log2_m zero_sig :=
+  cache_vm_sig_with_type
     { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F}
-    solve_constant_sig
+    (zero_sig' m sz sz_nonzero sz_le_log2_m)
     zero_sig.
 
-Ltac pose_one_sig sz m wt one_sig :=
-  cache_term_with_type_by
+Ltac pose_one_sig sz m wt sz_nonzero sz_le_log2_m one_sig :=
+  cache_vm_sig_with_type
     { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F}
-    solve_constant_sig
+    (one_sig' m sz sz_nonzero sz_le_log2_m)
     one_sig.
 
 Ltac pose_a24_sig sz m wt a24 a24_sig :=
@@ -63,93 +351,50 @@ Ltac pose_a24_sig sz m wt a24 a24_sig :=
     solve_constant_sig
     a24_sig.
 
-Ltac pose_add_sig sz m wt wt_nonzero add_sig :=
-  cache_term_with_type_by
+Ltac pose_add_sig sz m wt sz_nonzero add_sig :=
+  cache_sig_with_type_by_existing_sig
     { add : (Z^sz -> Z^sz -> Z^sz)%type |
       forall a b : Z^sz,
         let eval := Positional.Fdecode (m:=m) wt in
         eval (add a b) = (eval a + eval b)%F }
-    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
+    (add_sig' m sz sz_nonzero)
+    add_sig.
+
+Ltac pose_sub_sig sz m wt coef sub_sig :=
+  cache_sig_with_type_by_existing_sig
     {sub : (Z^sz -> Z^sz -> Z^sz)%type |
      forall a b : Z^sz,
        let eval := Positional.Fdecode (m:=m) wt in
        eval (sub a b) = (eval a - eval b)%F}
-    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
+    (sub_sig' m sz coef)
+    sub_sig.
+
+Ltac pose_opp_sig sz m wt coef opp_sig :=
+  cache_sig_with_type_by_existing_sig
     {opp : (Z^sz -> Z^sz)%type |
      forall a : Z^sz,
        let eval := Positional.Fdecode (m := m) wt in
        eval (opp a) = F.opp (eval a)}
-    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.
-
+    (opp_sig' m sz coef)
+    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
+Ltac pose_mul_sig sz m wt s c mul_code sz_nonzero s_nonzero mul_code_correct mul_sig :=
+  cache_sig_with_type_by_existing_sig
     {mul : (Z^sz -> Z^sz -> Z^sz)%type |
      forall a b : Z^sz,
        let eval := Positional.Fdecode (m := m) wt in
        eval (mul a b) = (eval a * eval b)%F}
-    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
+    (mul_sig' m sz s c mul_code sz_nonzero s_nonzero mul_code_correct)
+    mul_sig.
+
+Ltac pose_square_sig sz m wt s c square_code sz_nonzero s_nonzero square_code_correct square_sig :=
+  cache_sig_with_type_by_existing_sig
     {square : (Z^sz -> Z^sz)%type |
      forall a : Z^sz,
        let eval := Positional.Fdecode (m := m) wt in
        eval (square a) = (eval a * eval a)%F}
-    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.
+    (square_sig' m sz s c square_code sz_nonzero s_nonzero square_code_correct)
+    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
diff --git a/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v b/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v
index a83adb29c..4a037f34a 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v
@@ -6,9 +6,35 @@ 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.
+  Inductive tags := mul_code_correct | square_code_correct | carry_sig | zero_sig | one_sig | a24_sig | add_sig | sub_sig | opp_sig | mul_sig | square_sig | ring.
 End TAG.
 
+Ltac add_mul_code_correct pkg P_extra_prove_mul_eq :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.mul_code_correct
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let sz2 := Tag.get pkg TAG.sz2 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 mul_code := Tag.get pkg TAG.mul_code in
+                   let mul_code_correct := fresh "mul_code_correct" in
+                   let mul_code_correct := pose_mul_code_correct P_extra_prove_mul_eq sz sz2 wt s c mul_code mul_code_correct in
+                   constr:(mul_code_correct)).
+Ltac add_square_code_correct pkg P_extra_prove_square_eq :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.square_code_correct
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let sz2 := Tag.get pkg TAG.sz2 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 square_code := Tag.get pkg TAG.square_code in
+                   let square_code_correct := fresh "square_code_correct" in
+                   let square_code_correct := pose_square_code_correct P_extra_prove_square_eq sz sz2 wt s c square_code square_code_correct in
+                   constr:(square_code_correct)).
 Ltac add_carry_sig pkg :=
   Tag.update_by_tac_if_not_exists
     pkg
@@ -19,10 +45,8 @@ Ltac add_carry_sig pkg :=
                    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
+                   let carry_sig := pose_carry_sig sz m wt s c carry_chains carry_sig in
                    constr:(carry_sig)).
 Ltac add_zero_sig pkg :=
   Tag.update_by_tac_if_not_exists
@@ -31,8 +55,10 @@ Ltac add_zero_sig 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 sz_nonzero := Tag.get pkg TAG.sz_nonzero in
+                   let sz_le_log2_m := Tag.get pkg TAG.sz_le_log2_m in
                    let zero_sig := fresh "zero_sig" in
-                   let zero_sig := pose_zero_sig sz m wt zero_sig in
+                   let zero_sig := pose_zero_sig sz m wt sz_nonzero sz_le_log2_m zero_sig in
                    constr:(zero_sig)).
 Ltac add_one_sig pkg :=
   Tag.update_by_tac_if_not_exists
@@ -41,8 +67,10 @@ Ltac add_one_sig 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 sz_nonzero := Tag.get pkg TAG.sz_nonzero in
+                   let sz_le_log2_m := Tag.get pkg TAG.sz_le_log2_m in
                    let one_sig := fresh "one_sig" in
-                   let one_sig := pose_one_sig sz m wt one_sig in
+                   let one_sig := pose_one_sig sz m wt sz_nonzero sz_le_log2_m one_sig in
                    constr:(one_sig)).
 Ltac add_a24_sig pkg :=
   Tag.update_by_tac_if_not_exists
@@ -62,9 +90,9 @@ Ltac add_add_sig 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 wt_nonzero := Tag.get pkg TAG.wt_nonzero in
+                   let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
                    let add_sig := fresh "add_sig" in
-                   let add_sig := pose_add_sig sz m wt wt_nonzero add_sig in
+                   let add_sig := pose_add_sig sz m wt sz_nonzero add_sig in
                    constr:(add_sig)).
 Ltac add_sub_sig pkg :=
   Tag.update_by_tac_if_not_exists
@@ -73,10 +101,9 @@ Ltac add_sub_sig 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 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
+                   let sub_sig := pose_sub_sig sz m wt coef sub_sig in
                    constr:(sub_sig)).
 Ltac add_opp_sig pkg :=
   Tag.update_by_tac_if_not_exists
@@ -85,12 +112,11 @@ Ltac add_opp_sig 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 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
+                   let opp_sig := pose_opp_sig sz m wt coef opp_sig in
                    constr:(opp_sig)).
-Ltac add_mul_sig pkg P_default_mul P_extra_prove_mul_eq :=
+Ltac add_mul_sig pkg :=
   Tag.update_by_tac_if_not_exists
     pkg
     TAG.mul_sig
@@ -99,12 +125,14 @@ Ltac add_mul_sig pkg P_default_mul P_extra_prove_mul_eq :=
                    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_code := Tag.get pkg TAG.mul_code in
+                   let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
+                   let s_nonzero := Tag.get pkg TAG.s_nonzero in
+                   let mul_code_correct := Tag.get pkg TAG.mul_code_correct 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
+                   let mul_sig := pose_mul_sig sz m wt s c mul_code sz_nonzero s_nonzero mul_code_correct mul_sig in
                    constr:(mul_sig)).
-Ltac add_square_sig pkg P_default_square P_extra_prove_square_eq :=
+Ltac add_square_sig pkg :=
   Tag.update_by_tac_if_not_exists
     pkg
     TAG.square_sig
@@ -113,10 +141,12 @@ Ltac add_square_sig pkg P_default_square P_extra_prove_square_eq :=
                    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_code := Tag.get pkg TAG.square_code in
+                   let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
+                   let s_nonzero := Tag.get pkg TAG.s_nonzero in
+                   let square_code_correct := Tag.get pkg TAG.square_code_correct 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
+                   let square_sig := pose_square_sig sz m wt s c square_code sz_nonzero s_nonzero square_code_correct square_sig in
                    constr:(square_sig)).
 Ltac add_ring pkg :=
   Tag.update_by_tac_if_not_exists
@@ -137,7 +167,9 @@ Ltac add_ring pkg :=
                    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 :=
+Ltac add_Defaults_package pkg P_extra_prove_mul_eq P_extra_prove_square_eq :=
+  let pkg := add_mul_code_correct pkg P_extra_prove_mul_eq in
+  let pkg := add_square_code_correct pkg P_extra_prove_square_eq in
   let pkg := add_carry_sig pkg in
   let pkg := add_zero_sig pkg in
   let pkg := add_one_sig pkg in
@@ -145,15 +177,19 @@ Ltac add_Defaults_package pkg P_default_mul P_extra_prove_mul_eq P_default_squar
   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_mul_sig pkg in
+  let pkg := add_square_sig pkg in
   let pkg := add_ring pkg in
-  Tag.strip_local pkg.
+  Tag.strip_subst_local pkg.
 
 
 Module MakeDefaultsPackage (PKG : PrePackage).
   Module Import MakeDefaultsPackageInternal := MakePackageBase PKG.
 
+  Ltac get_mul_code_correct _ := get TAG.mul_code_correct.
+  Notation mul_code_correct := (ltac:(let v := get_mul_code_correct () in exact v)) (only parsing).
+  Ltac get_square_code_correct _ := get TAG.square_code_correct.
+  Notation square_code_correct := (ltac:(let v := get_square_code_correct () in exact v)) (only parsing).
   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.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Freeze.v b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v
index 02daea678..a32f9e220 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Freeze.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v
@@ -1,8 +1,13 @@
 Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
 Require Import Coq.Lists.List. Import ListNotations.
+Require Import Crypto.Arithmetic.CoreUnfolder.
+Require Import Crypto.Arithmetic.Saturated.CoreUnfolder.
+Require Import Crypto.Arithmetic.Saturated.FreezeUnfolder.
 Require Import Crypto.Arithmetic.Core. Import B.
 Require Import Crypto.Arithmetic.Saturated.Freeze.
 Require Crypto.Specific.Framework.CurveParameters.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Base.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.Definitions.
 Require Crypto.Util.Tuple.
@@ -16,35 +21,57 @@ 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)
+Ltac freeze_preunfold :=
+  cbv [freeze freeze_cps Wrappers.Columns.unbalanced_sub_cps Wrappers.Columns.conditional_add_cps Core.Columns.from_associational_cps Core.Columns.nils Core.Columns.cons_to_nth_cps Core.Columns.compact_cps Wrappers.Columns.add_cps Core.Columns.compact_step_cps Core.Columns.compact_digit_cps].
+
+Section gen.
+  Context (m : positive)
+          (sz : nat)
+          (c : list limb)
+          (bitwidth : Z)
+          (m_enc : Z^sz)
+          (sz_nonzero : sz <> 0%nat)
+          (sz_le_log2_m : Z.of_nat sz <= Z.log2_up (Z.pos m)).
+
+  Local Notation wt := (wt_gen m sz).
+  Local Notation sz2 := (sz2' sz).
+  Local Notation wt_divides' := (wt_gen_divides' m sz sz_nonzero sz_le_log2_m).
+  Local Notation wt_nonzero := (wt_gen_nonzero m sz).
+
+  Context (c_small : 0 < Associational.eval c < wt sz)
+          (m_enc_bounded : Tuple.map (BinInt.Z.land (Z.ones bitwidth)) m_enc = m_enc)
+          (m_enc_correct : Positional.eval wt m_enc = Z.pos m)
+          (m_correct_wt : Z.pos m = wt sz - Associational.eval c).
+
+  Definition freeze_sig'
+    : { freeze : (Z^sz -> Z^sz)%type |
+        forall a : Z^sz,
+          (0 <= Positional.eval wt a < 2 * Z.pos m)->
+          let eval := Positional.Fdecode (m := m) wt in
+          eval (freeze a) = eval a }.
+  Proof.
+    eexists; cbv beta zeta; (intros a ?).
+    pose proof wt_nonzero; pose proof (wt_gen_pos m sz).
+    pose proof (wt_gen0_1 m sz).
+    pose proof div_mod; pose proof (wt_gen_divides m sz sz_nonzero sz_le_log2_m).
+    pose proof (wt_gen_multiples m sz).
+    pose proof div_correct; pose proof modulo_correct.
+    pose proof (wt_gen_divides_chain m sz sz_nonzero sz_le_log2_m).
+    let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in
+    presolve_op_F constr:(wt) x;
+      [ autorewrite with pattern_runtime; reflexivity | ].
+    rewrite eval_freeze with (c := c);
+      try eassumption; try omega; try reflexivity.
+  Defined.
+End gen.
+
+Ltac pose_freeze_sig wt m sz c bitwidth m_enc sz_nonzero sz_le_log2_m freeze_sig :=
+  cache_sig_with_type_by_existing_sig_helper
+    ltac:(fun _ => cbv [freeze_sig'])
+           {freeze : (Z^sz -> Z^sz)%type |
+            forall a : Z^sz,
+              (0 <= Positional.eval wt a < 2 * Z.pos m)->
+              let eval := Positional.Fdecode (m := m) wt in
+              eval (freeze a) = eval a}
+           (freeze_sig' m sz c bitwidth m_enc sz_nonzero sz_le_log2_m)
            freeze_sig.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
index 9314f369e..885bfde09 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
@@ -13,22 +13,20 @@ 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
+    ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
                    let m := Tag.get pkg TAG.m in
-                   let wt := Tag.get pkg TAG.wt in
+                   let sz := Tag.get pkg TAG.sz 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 m_enc := Tag.get pkg TAG.m_enc in
+                   let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
+                   let sz_le_log2_m := Tag.get pkg TAG.sz_le_log2_m 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
+                   let freeze_sig := pose_freeze_sig wt m sz c bitwidth m_enc sz_nonzero sz_le_log2_m freeze_sig in
                    constr:(freeze_sig)).
 Ltac add_Freeze_package pkg :=
   let pkg := add_freeze_sig pkg in
-  Tag.strip_local pkg.
+  Tag.strip_subst_local pkg.
 
 
 Module MakeFreezePackage (PKG : PrePackage).
diff --git a/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v b/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
index 45f2df9be..a3e929a9c 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
@@ -1,7 +1,9 @@
 Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Crypto.Arithmetic.Saturated.Wrappers.
 Require Import Crypto.Util.ZUtil.ModInv.
 Require Import Crypto.Util.Tactics.CacheTerm.
+Require Import Crypto.Util.Decidable.
 Require Crypto.Util.Tuple.
 
 Local Notation tuple := Tuple.tuple.
@@ -122,3 +124,46 @@ Hint Rewrite chained_carries'_id : uncps.
 Ltac make_chained_carries_cps sz wt s c a carry_chains :=
   (eval cbv [chained_carries_cps' chained_carries_cps'_step carry_chains] in
       (chained_carries_cps' sz wt s c a carry_chains id)).
+
+Ltac specialize_existing_sig existing_sig :=
+  lazymatch type of existing_sig with
+  | ?T -> _
+    => let H := fresh "existing_sig_subproof" in
+       let H := cache_proof_with_type_by
+                  T
+                  ltac:(vm_decide_no_check)
+                         H in
+       specialize_existing_sig (existing_sig H)
+  | _ => existing_sig
+  end.
+
+Ltac cache_sig_with_type_by_existing_sig_helper cbv_tac ty existing_sig id :=
+  let existing_sig := specialize_existing_sig existing_sig in
+  cache_sig_with_type_by
+    ty
+    ltac:(eexists; intros; etransitivity;
+          [ apply f_equal
+          | solve [ eapply (proj2_sig existing_sig); eassumption ] ];
+          do 2 (cbv [proj1_sig
+                       chained_carries_cps' chained_carries_cps'_step
+                       Positional.mul_cps Positional.reduce_cps];
+                cbv_tac ());
+          repeat autounfold;
+          let next_step _ := basesystem_partial_evaluation_RHS_gen Wrappers.basesystem_partial_evaluation_unfolder in
+          lazymatch goal with
+          | [ |- _ = match ?code with
+                     | None => _
+                     | _ => _
+                     end ]
+            => let c := (eval hnf in code) in
+               change code with c;
+               cbv beta iota;
+               lazymatch c with
+               | None => next_step ()
+               | _ => idtac
+               end
+          | _ => next_step ()
+          end;
+          do_replace_match_with_destructuring_match_in_goal;
+          reflexivity)
+           id.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v b/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
index a0d2d3528..264effeb1 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
@@ -37,7 +37,7 @@ Ltac add_square_sig pkg :=
 Ltac add_Karatsuba_package pkg :=
   let pkg := add_mul_sig pkg in
   let pkg := add_square_sig pkg in
-  Tag.strip_local pkg.
+  Tag.strip_subst_local pkg.
 
 
 Module MakeKaratsubaPackage (PKG : PrePackage).
diff --git a/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
index dd7b6c541..200ad593a 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
@@ -27,7 +27,7 @@ Ltac add_Mxzladderstep_sig pkg :=
                    constr:(Mxzladderstep_sig)).
 Ltac add_Ladderstep_package pkg :=
   let pkg := add_Mxzladderstep_sig pkg in
-  Tag.strip_local pkg.
+  Tag.strip_subst_local pkg.
 
 
 Module MakeLadderstepPackage (PKG : PrePackage).
diff --git a/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v
index 4980f09b9..5ade26d76 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v
@@ -407,7 +407,7 @@ Ltac add_Montgomery_package pkg :=
   let pkg := add_carry_sig pkg in
   let pkg := add_freeze_sig pkg in
   let pkg := add_Mxzladderstep_sig pkg in
-  Tag.strip_local pkg.
+  Tag.strip_subst_local pkg.
 
 
 Module MakeMontgomeryPackage (PKG : PrePackage).
diff --git a/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py
index d5726ac34..568877838 100755
--- a/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py
+++ b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py
@@ -121,7 +121,7 @@ def make_add_all(fname, indent=''):
     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'
+    ret += nl_indent + 'Tag.strip_subst_local pkg.\n'
     return ret
 
 def make_if(name, indent=''):
diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v
index 472349180..8911dccfc 100644
--- a/src/Specific/Framework/CurveParameters.v
+++ b/src/Specific/Framework/CurveParameters.v
@@ -332,5 +332,5 @@ Module Export CurveParameters.
     let pkg := add_modinv_fuel pkg in
     let pkg := add_mul_code pkg in
     let pkg := add_square_code pkg in
-    Tag.strip_local pkg.
+    Tag.strip_subst_local pkg.
 End CurveParameters.
diff --git a/src/Specific/Framework/MontgomeryReificationTypesPackage.v b/src/Specific/Framework/MontgomeryReificationTypesPackage.v
index 5b440f0e8..6f9364d6e 100644
--- a/src/Specific/Framework/MontgomeryReificationTypesPackage.v
+++ b/src/Specific/Framework/MontgomeryReificationTypesPackage.v
@@ -75,7 +75,7 @@ Ltac add_MontgomeryReificationTypes_package pkg :=
   let pkg := add_feBW_of_feBW_small pkg in
   let pkg := add_phiM pkg in
   let pkg := add_phiM_small pkg in
-  Tag.strip_local pkg.
+  Tag.strip_subst_local pkg.
 
 
 Module MakeMontgomeryReificationTypesPackage (PKG : PrePackage).
diff --git a/src/Specific/Framework/ReificationTypesPackage.v b/src/Specific/Framework/ReificationTypesPackage.v
index 2a5e8e85b..f0703b4ac 100644
--- a/src/Specific/Framework/ReificationTypesPackage.v
+++ b/src/Specific/Framework/ReificationTypesPackage.v
@@ -126,7 +126,7 @@ Ltac add_ReificationTypes_package pkg :=
   let pkg := add_feBW_bounded pkg in
   let pkg := add_phiW pkg in
   let pkg := add_phiBW pkg in
-  Tag.strip_local pkg.
+  Tag.strip_subst_local pkg.
 
 
 Module MakeReificationTypesPackage (PKG : PrePackage).
diff --git a/src/Specific/Framework/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v
index 9c930567e..b45931430 100644
--- a/src/Specific/Framework/SynthesisFramework.v
+++ b/src/Specific/Framework/SynthesisFramework.v
@@ -30,13 +30,11 @@ End Tag.
 Module Export MakeSynthesisTactics.
   Ltac add_Synthesis_package pkg curve extra_prove_mul_eq extra_prove_square_eq :=
     let CP := get_fill_CurveParameters curve in
-    let P_default_mul _ := default_mul CP in
     let P_extra_prove_mul_eq := extra_prove_mul_eq in
-    let P_default_square _ := default_square CP in
     let P_extra_prove_square_eq := extra_prove_square_eq in
     let pkg := Tag.local_update pkg TAG.CP CP in
     let pkg := add_CurveParameters_package pkg in
-    let pkg := Tag.strip_local pkg in
+    let pkg := Tag.strip_subst_local pkg in
     let pkg := add_Base_package pkg in
     let pkg := add_ReificationTypes_package pkg in
     let pkg := add_Karatsuba_package pkg in
@@ -45,7 +43,7 @@ Module Export MakeSynthesisTactics.
     (* N.B. freeze is a "default" and must come after montgomery, which disables 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
+    let pkg := add_Defaults_package pkg P_extra_prove_mul_eq P_extra_prove_square_eq in
     (* N.B. Ladderstep must come after Defaults *)
     let pkg := add_Ladderstep_package pkg in
     pkg.