Add a dummy karatsuba parameter

Currently unused, but adding it here in preparation for removing
reification (which will allow easy support of karatsuba separate from
goldilocks).

326 files changed, 354 insertions, 5 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py
index d21ad2d9e..d9812fd94 100755
--- a/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py
+++ b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py
@@ -17,7 +17,7 @@ NORMAL_PACKAGE_NAMES = [('Base.v', (CP_LIST, None)),
                         ('Montgomery.v', (CP_BASE_DEFAULTS_FREEZE_LADDERSTEP_LIST, 'montgomery')),
                         ('../MontgomeryReificationTypes.v', (CP_BASE_LIST + ['MontgomeryPackage.v', '../ReificationTypesPackage.v'], 'montgomery'))]
 ALL_FILE_NAMES = PACKAGE_NAMES + NORMAL_PACKAGE_NAMES # PACKAGE_CP_NAMES + WITH_CURVE_BASE_NAMES + ['../ReificationTypes.v']
-CONFIGS = ('goldilocks', 'montgomery', 'freeze', 'ladderstep')
+CONFIGS = ('goldilocks', 'karatsuba', 'montgomery', 'freeze', 'ladderstep')
 
 EXCLUDES = ('constr:((wt_divides_chain, wt_divides_chains))', )
 
diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v
index ec080491d..3b31d9339 100644
--- a/src/Specific/Framework/CurveParameters.v
+++ b/src/Specific/Framework/CurveParameters.v
@@ -12,7 +12,7 @@ Local Set Primitive Projections.
 Module Export Notations := RawCurveParameters.Notations.
 
 Module TAG. (* namespacing *)
-  Inductive tags := CP | sz | base | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | freeze | ladderstep | upper_bound_of_exponent_tight | upper_bound_of_exponent_loose | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel | mul_code | square_code.
+  Inductive tags := CP | sz | base | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | karatsuba | montgomery | freeze | ladderstep | upper_bound_of_exponent_tight | upper_bound_of_exponent_loose | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel | mul_code | square_code.
 End TAG.
 
 Module Export CurveParameters.
@@ -42,6 +42,7 @@ Module Export CurveParameters.
       coef_div_modulus : nat;
 
       goldilocks : bool;
+      karatsuba : bool;
       montgomery : bool;
       freeze : bool;
       ladderstep : bool;
@@ -65,6 +66,7 @@ Module Export CurveParameters.
               a24
               coef_div_modulus
               goldilocks
+              karatsuba
               montgomery
               freeze
               ladderstep
@@ -102,6 +104,7 @@ Module Export CurveParameters.
         let base := RawCurveParameters.base CP in
         let bitwidth := RawCurveParameters.bitwidth CP in
         let montgomery := RawCurveParameters.montgomery CP in
+        let karatsuba := defaulted (RawCurveParameters.karatsuba CP) false in
         let s := RawCurveParameters.s CP in
         let c := RawCurveParameters.c CP in
         let freeze
@@ -142,6 +145,7 @@ Module Export CurveParameters.
           coef_div_modulus := defaulted (RawCurveParameters.coef_div_modulus CP) 0%nat;
 
           goldilocks := goldilocks;
+          karatsuba := karatsuba;
           montgomery := montgomery;
           freeze := freeze;
           ladderstep := RawCurveParameters.ladderstep CP;
@@ -177,6 +181,7 @@ Module Export CurveParameters.
           a24 := ?a24';
           coef_div_modulus := ?coef_div_modulus';
           goldilocks := ?goldilocks';
+          karatsuba := ?karatsuba';
           montgomery := ?montgomery';
           freeze := ?freeze';
           ladderstep := ?ladderstep';
@@ -193,6 +198,7 @@ Module Export CurveParameters.
          let bitwidth' := do_compute bitwidth' in
          let carry_chains' := do_compute carry_chains' in
          let goldilocks' := do_compute goldilocks' in
+         let karatsuba' := do_compute karatsuba' in
          let montgomery' := do_compute montgomery' in
          let freeze' := do_compute freeze' in
          let ladderstep' := do_compute ladderstep' in
@@ -209,6 +215,7 @@ Module Export CurveParameters.
                     a24 := a24';
                     coef_div_modulus := coef_div_modulus';
                     goldilocks := goldilocks';
+                    karatsuba := karatsuba';
                     montgomery := montgomery';
                     freeze := freeze';
                     ladderstep := ladderstep';
@@ -221,8 +228,6 @@ Module Export CurveParameters.
                     modinv_fuel := modinv_fuel'
                   |})
     end.
-  (*existsb Nat.eqb List.app seq pred Z_add_red Z_sub_red Z_mul_red Z_div_red Z_pow_red Z_eqb_red
-                     Z.to_nat Pos.to_nat Pos.iter_op Nat.add Nat.mul orb andb] in*)
   Notation fill_CurveParameters CP := ltac:(let v := get_fill_CurveParameters CP in exact v) (only parsing).
 
   Ltac internal_pose_of_CP CP proj id :=
@@ -246,6 +251,8 @@ Module Export CurveParameters.
     internal_pose_of_CP CP CurveParameters.coef_div_modulus coef_div_modulus.
   Ltac pose_goldilocks CP goldilocks :=
     internal_pose_of_CP CP CurveParameters.goldilocks goldilocks.
+  Ltac pose_karatsuba CP karatsuba :=
+    internal_pose_of_CP CP CurveParameters.karatsuba karatsuba.
   Ltac pose_montgomery CP montgomery :=
     internal_pose_of_CP CP CurveParameters.montgomery montgomery.
   Ltac pose_freeze CP freeze :=
@@ -322,6 +329,12 @@ Module Export CurveParameters.
     let goldilocks := pose_goldilocks CP goldilocks in
     Tag.update pkg TAG.goldilocks goldilocks.
 
+  Ltac add_karatsuba pkg :=
+    let CP := Tag.get pkg TAG.CP in
+    let karatsuba := fresh "karatsuba" in
+    let karatsuba := pose_karatsuba CP karatsuba in
+    Tag.update pkg TAG.karatsuba karatsuba.
+
   Ltac add_montgomery pkg :=
     let CP := Tag.get pkg TAG.CP in
     let montgomery := fresh "montgomery" in
@@ -392,6 +405,7 @@ Module Export CurveParameters.
     let pkg := add_a24 pkg in
     let pkg := add_coef_div_modulus pkg in
     let pkg := add_goldilocks pkg in
+    let pkg := add_karatsuba pkg in
     let pkg := add_montgomery pkg in
     let pkg := add_freeze pkg in
     let pkg := add_ladderstep pkg in
diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v
index 836e75489..954080ad6 100644
--- a/src/Specific/Framework/CurveParametersPackage.v
+++ b/src/Specific/Framework/CurveParametersPackage.v
@@ -11,6 +11,14 @@ Ltac if_goldilocks pkg tac_true tac_false arg :=
   | false => tac_false arg
   end.
 
+Ltac if_karatsuba pkg tac_true tac_false arg :=
+  let karatsuba := Tag.get pkg TAG.karatsuba in
+  let karatsuba := (eval vm_compute in (karatsuba : bool)) in
+  lazymatch karatsuba with
+  | true => tac_true arg
+  | false => tac_false arg
+  end.
+
 Ltac if_montgomery pkg tac_true tac_false arg :=
   let montgomery := Tag.get pkg TAG.montgomery in
   let montgomery := (eval vm_compute in (montgomery : bool)) in
@@ -57,6 +65,8 @@ Module MakeCurveParametersPackage (PKG : PrePackage).
   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_karatsuba _ := get TAG.karatsuba.
+  Notation karatsuba := (ltac:(let v := get_karatsuba () in exact v)) (only parsing).
   Ltac get_montgomery _ := get TAG.montgomery.
   Notation montgomery := (ltac:(let v := get_montgomery () in exact v)) (only parsing).
   Ltac get_freeze _ := get TAG.freeze.
diff --git a/src/Specific/Framework/RawCurveParameters.v b/src/Specific/Framework/RawCurveParameters.v
index ae3040b10..5ff22d2f1 100644
--- a/src/Specific/Framework/RawCurveParameters.v
+++ b/src/Specific/Framework/RawCurveParameters.v
@@ -31,6 +31,7 @@ Record CurveParameters :=
     coef_div_modulus : option nat;
 
     goldilocks : option bool; (* defaults to true iff the prime ([s-c]) is of the form [2²ᵏ - 2ᵏ - 1] *)
+    karatsuba : option bool; (* defaults to false, currently unused *)
     montgomery : bool;
     freeze : option bool; (* defaults to true iff [s = 2^(base * sz)] *)
     ladderstep : bool;
@@ -58,6 +59,7 @@ Declare Reduction cbv_RawCurveParameters
             a24
             coef_div_modulus
             goldilocks
+            karatsuba
             montgomery
             freeze
             ladderstep
diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py
index ae913d957..b652090b8 100755
--- a/src/Specific/Framework/make_curve.py
+++ b/src/Specific/Framework/make_curve.py
@@ -235,12 +235,13 @@ def make_curve_parameters(parameters):
                             ('freeze_extra_allowable_bit_widths', '%nat'),
                             ('coef_div_modulus', '%nat'),
                             ('modinv_fuel', '%nat'),
+                            ('karatsuba', ''),
                             ('goldilocks', '')):
         replacements[k] = fix_option(nested_list_to_string(replacements.get(k, 'None')), scope_string=scope_string)
     for k in ('montgomery', ):
         if k not in replacements.keys():
             replacements[k] = False
-    for k in ('s', 'c', 'goldilocks', 'montgomery'):
+    for k in ('s', 'c', 'karatsuba', 'goldilocks', 'montgomery'):
         replacements[k] = nested_list_to_string(replacements[k])
     for k in ('extra_prove_mul_eq', 'extra_prove_square_eq'):
         if k not in replacements.keys():
@@ -266,6 +267,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := %(coef_div_modulus)s;
 
     goldilocks := %(goldilocks)s;
+    karatsuba := %(karatsuba)s;
     montgomery := %(montgomery)s;
     freeze := %(freeze)s;
     ladderstep := %(ladderstep)s;
diff --git a/src/Specific/NISTP256/AMD128/CurveParameters.v b/src/Specific/NISTP256/AMD128/CurveParameters.v
index f3c1cc5b1..f994c8a6d 100644
--- a/src/Specific/NISTP256/AMD128/CurveParameters.v
+++ b/src/Specific/NISTP256/AMD128/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/NISTP256/AMD64/CurveParameters.v b/src/Specific/NISTP256/AMD64/CurveParameters.v
index 90846add3..446f0cad8 100644
--- a/src/Specific/NISTP256/AMD64/CurveParameters.v
+++ b/src/Specific/NISTP256/AMD64/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v
index e9da717e8..b22d3a967 100644
--- a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v
+++ b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v
index 0ab20d299..8b13a268c 100644
--- a/src/Specific/X25519/C32/CurveParameters.v
+++ b/src/Specific/X25519/C32/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v
index 6a209e169..2be1510b9 100644
--- a/src/Specific/X25519/C64/CurveParameters.v
+++ b/src/Specific/X25519/C64/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := true;
diff --git a/src/Specific/X2555/C128/CurveParameters.v b/src/Specific/X2555/C128/CurveParameters.v
index 52fc70a7f..1171f7583 100644
--- a/src/Specific/X2555/C128/CurveParameters.v
+++ b/src/Specific/X2555/C128/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some false;
     ladderstep := true;
diff --git a/src/Specific/montgomery32_2e127m1/CurveParameters.v b/src/Specific/montgomery32_2e127m1/CurveParameters.v
index 75fe9dd48..119c9782f 100644
--- a/src/Specific/montgomery32_2e127m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e127m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e129m25/CurveParameters.v b/src/Specific/montgomery32_2e129m25/CurveParameters.v
index 901f55520..07048d8db 100644
--- a/src/Specific/montgomery32_2e129m25/CurveParameters.v
+++ b/src/Specific/montgomery32_2e129m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e130m5/CurveParameters.v b/src/Specific/montgomery32_2e130m5/CurveParameters.v
index c7ed5cdcd..4dfc2991f 100644
--- a/src/Specific/montgomery32_2e130m5/CurveParameters.v
+++ b/src/Specific/montgomery32_2e130m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e137m13/CurveParameters.v b/src/Specific/montgomery32_2e137m13/CurveParameters.v
index d617a49ed..941f2eebd 100644
--- a/src/Specific/montgomery32_2e137m13/CurveParameters.v
+++ b/src/Specific/montgomery32_2e137m13/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e140m27/CurveParameters.v b/src/Specific/montgomery32_2e140m27/CurveParameters.v
index 987d6de82..541761b3b 100644
--- a/src/Specific/montgomery32_2e140m27/CurveParameters.v
+++ b/src/Specific/montgomery32_2e140m27/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e141m9/CurveParameters.v b/src/Specific/montgomery32_2e141m9/CurveParameters.v
index 7dc18363b..341a4a51e 100644
--- a/src/Specific/montgomery32_2e141m9/CurveParameters.v
+++ b/src/Specific/montgomery32_2e141m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e150m3/CurveParameters.v b/src/Specific/montgomery32_2e150m3/CurveParameters.v
index cd35d2b26..761ac9131 100644
--- a/src/Specific/montgomery32_2e150m3/CurveParameters.v
+++ b/src/Specific/montgomery32_2e150m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e150m5/CurveParameters.v b/src/Specific/montgomery32_2e150m5/CurveParameters.v
index eef36a4c5..906516faa 100644
--- a/src/Specific/montgomery32_2e150m5/CurveParameters.v
+++ b/src/Specific/montgomery32_2e150m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e152m17/CurveParameters.v b/src/Specific/montgomery32_2e152m17/CurveParameters.v
index 5101eb3b7..9192d3590 100644
--- a/src/Specific/montgomery32_2e152m17/CurveParameters.v
+++ b/src/Specific/montgomery32_2e152m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e158m15/CurveParameters.v b/src/Specific/montgomery32_2e158m15/CurveParameters.v
index 1df08ae58..282dd6dba 100644
--- a/src/Specific/montgomery32_2e158m15/CurveParameters.v
+++ b/src/Specific/montgomery32_2e158m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e165m25/CurveParameters.v b/src/Specific/montgomery32_2e165m25/CurveParameters.v
index 5ae8ac893..8d3c00d6d 100644
--- a/src/Specific/montgomery32_2e165m25/CurveParameters.v
+++ b/src/Specific/montgomery32_2e165m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e166m5/CurveParameters.v b/src/Specific/montgomery32_2e166m5/CurveParameters.v
index a3ec5f4db..b75c925d1 100644
--- a/src/Specific/montgomery32_2e166m5/CurveParameters.v
+++ b/src/Specific/montgomery32_2e166m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e171m19/CurveParameters.v b/src/Specific/montgomery32_2e171m19/CurveParameters.v
index 9d477e915..54b82b346 100644
--- a/src/Specific/montgomery32_2e171m19/CurveParameters.v
+++ b/src/Specific/montgomery32_2e171m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e174m17/CurveParameters.v b/src/Specific/montgomery32_2e174m17/CurveParameters.v
index 107db915b..4084ea061 100644
--- a/src/Specific/montgomery32_2e174m17/CurveParameters.v
+++ b/src/Specific/montgomery32_2e174m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e174m3/CurveParameters.v b/src/Specific/montgomery32_2e174m3/CurveParameters.v
index 125c648ad..722991370 100644
--- a/src/Specific/montgomery32_2e174m3/CurveParameters.v
+++ b/src/Specific/montgomery32_2e174m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e189m25/CurveParameters.v b/src/Specific/montgomery32_2e189m25/CurveParameters.v
index 4ea8fbb44..c6dffce9b 100644
--- a/src/Specific/montgomery32_2e189m25/CurveParameters.v
+++ b/src/Specific/montgomery32_2e189m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e190m11/CurveParameters.v b/src/Specific/montgomery32_2e190m11/CurveParameters.v
index 7ea0a144f..17ea93c10 100644
--- a/src/Specific/montgomery32_2e190m11/CurveParameters.v
+++ b/src/Specific/montgomery32_2e190m11/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e191m19/CurveParameters.v b/src/Specific/montgomery32_2e191m19/CurveParameters.v
index 5e64355a0..173cd0e0e 100644
--- a/src/Specific/montgomery32_2e191m19/CurveParameters.v
+++ b/src/Specific/montgomery32_2e191m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e192m2e64m1/CurveParameters.v b/src/Specific/montgomery32_2e192m2e64m1/CurveParameters.v
index 22f865980..76ebb9d37 100644
--- a/src/Specific/montgomery32_2e192m2e64m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e192m2e64m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e194m33/CurveParameters.v b/src/Specific/montgomery32_2e194m33/CurveParameters.v
index e3186171e..f0ea8cc22 100644
--- a/src/Specific/montgomery32_2e194m33/CurveParameters.v
+++ b/src/Specific/montgomery32_2e194m33/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e196m15/CurveParameters.v b/src/Specific/montgomery32_2e196m15/CurveParameters.v
index 43429db37..be8378ba9 100644
--- a/src/Specific/montgomery32_2e196m15/CurveParameters.v
+++ b/src/Specific/montgomery32_2e196m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e198m17/CurveParameters.v b/src/Specific/montgomery32_2e198m17/CurveParameters.v
index dda6ddbbd..18f056404 100644
--- a/src/Specific/montgomery32_2e198m17/CurveParameters.v
+++ b/src/Specific/montgomery32_2e198m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e205m45x2e198m1/CurveParameters.v b/src/Specific/montgomery32_2e205m45x2e198m1/CurveParameters.v
index 13457af69..d3ff2f8a7 100644
--- a/src/Specific/montgomery32_2e205m45x2e198m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e205m45x2e198m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e206m5/CurveParameters.v b/src/Specific/montgomery32_2e206m5/CurveParameters.v
index 40cbcef4a..8b51bfd39 100644
--- a/src/Specific/montgomery32_2e206m5/CurveParameters.v
+++ b/src/Specific/montgomery32_2e206m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e212m29/CurveParameters.v b/src/Specific/montgomery32_2e212m29/CurveParameters.v
index 756a7e8a0..eb3018b24 100644
--- a/src/Specific/montgomery32_2e212m29/CurveParameters.v
+++ b/src/Specific/montgomery32_2e212m29/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e213m3/CurveParameters.v b/src/Specific/montgomery32_2e213m3/CurveParameters.v
index 5d0407398..b54fe904f 100644
--- a/src/Specific/montgomery32_2e213m3/CurveParameters.v
+++ b/src/Specific/montgomery32_2e213m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e216m2e108m1/CurveParameters.v b/src/Specific/montgomery32_2e216m2e108m1/CurveParameters.v
index 51f408fc9..aac012bf0 100644
--- a/src/Specific/montgomery32_2e216m2e108m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e216m2e108m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e221m3/CurveParameters.v b/src/Specific/montgomery32_2e221m3/CurveParameters.v
index 3e72c5d78..433140906 100644
--- a/src/Specific/montgomery32_2e221m3/CurveParameters.v
+++ b/src/Specific/montgomery32_2e221m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e222m117/CurveParameters.v b/src/Specific/montgomery32_2e222m117/CurveParameters.v
index 005371b70..fdfdf452e 100644
--- a/src/Specific/montgomery32_2e222m117/CurveParameters.v
+++ b/src/Specific/montgomery32_2e222m117/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e224m2e96p1/CurveParameters.v b/src/Specific/montgomery32_2e224m2e96p1/CurveParameters.v
index 3977932bc..5777d34fe 100644
--- a/src/Specific/montgomery32_2e224m2e96p1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e224m2e96p1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e226m5/CurveParameters.v b/src/Specific/montgomery32_2e226m5/CurveParameters.v
index 43ae803f3..d42852590 100644
--- a/src/Specific/montgomery32_2e226m5/CurveParameters.v
+++ b/src/Specific/montgomery32_2e226m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e230m27/CurveParameters.v b/src/Specific/montgomery32_2e230m27/CurveParameters.v
index d89b2ff97..180742861 100644
--- a/src/Specific/montgomery32_2e230m27/CurveParameters.v
+++ b/src/Specific/montgomery32_2e230m27/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e235m15/CurveParameters.v b/src/Specific/montgomery32_2e235m15/CurveParameters.v
index 3bf3a9e8c..cc45478d6 100644
--- a/src/Specific/montgomery32_2e235m15/CurveParameters.v
+++ b/src/Specific/montgomery32_2e235m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e243m9/CurveParameters.v b/src/Specific/montgomery32_2e243m9/CurveParameters.v
index 4ebad3775..f02ed60ce 100644
--- a/src/Specific/montgomery32_2e243m9/CurveParameters.v
+++ b/src/Specific/montgomery32_2e243m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e251m9/CurveParameters.v b/src/Specific/montgomery32_2e251m9/CurveParameters.v
index 37968f690..243ea3437 100644
--- a/src/Specific/montgomery32_2e251m9/CurveParameters.v
+++ b/src/Specific/montgomery32_2e251m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e254m127x2e240m1/CurveParameters.v b/src/Specific/montgomery32_2e254m127x2e240m1/CurveParameters.v
index 996c182d8..04f2fa3e6 100644
--- a/src/Specific/montgomery32_2e254m127x2e240m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e254m127x2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e255m19/CurveParameters.v b/src/Specific/montgomery32_2e255m19/CurveParameters.v
index 3831df381..2912d73c2 100644
--- a/src/Specific/montgomery32_2e255m19/CurveParameters.v
+++ b/src/Specific/montgomery32_2e255m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e255m2e4m2e1m1/CurveParameters.v b/src/Specific/montgomery32_2e255m2e4m2e1m1/CurveParameters.v
index 5d67b538e..dcd1c1e56 100644
--- a/src/Specific/montgomery32_2e255m2e4m2e1m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e255m2e4m2e1m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e255m765/CurveParameters.v b/src/Specific/montgomery32_2e255m765/CurveParameters.v
index 4949a8177..531d00bbb 100644
--- a/src/Specific/montgomery32_2e255m765/CurveParameters.v
+++ b/src/Specific/montgomery32_2e255m765/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e256m189/CurveParameters.v b/src/Specific/montgomery32_2e256m189/CurveParameters.v
index 0c083a960..c673cf6d9 100644
--- a/src/Specific/montgomery32_2e256m189/CurveParameters.v
+++ b/src/Specific/montgomery32_2e256m189/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/CurveParameters.v b/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/CurveParameters.v
index 7ff9ca3d1..f8b2b996d 100644
--- a/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e256m2e32m977/CurveParameters.v b/src/Specific/montgomery32_2e256m2e32m977/CurveParameters.v
index 719e9d147..5badbfc52 100644
--- a/src/Specific/montgomery32_2e256m2e32m977/CurveParameters.v
+++ b/src/Specific/montgomery32_2e256m2e32m977/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e256m88x2e240m1/CurveParameters.v b/src/Specific/montgomery32_2e256m88x2e240m1/CurveParameters.v
index cdd462cc8..6045bed0c 100644
--- a/src/Specific/montgomery32_2e256m88x2e240m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e256m88x2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e266m3/CurveParameters.v b/src/Specific/montgomery32_2e266m3/CurveParameters.v
index 5ebc3275c..77b84da50 100644
--- a/src/Specific/montgomery32_2e266m3/CurveParameters.v
+++ b/src/Specific/montgomery32_2e266m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e285m9/CurveParameters.v b/src/Specific/montgomery32_2e285m9/CurveParameters.v
index 9f4a1e1f2..a17478355 100644
--- a/src/Specific/montgomery32_2e285m9/CurveParameters.v
+++ b/src/Specific/montgomery32_2e285m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e291m19/CurveParameters.v b/src/Specific/montgomery32_2e291m19/CurveParameters.v
index 51e62d28b..5d1b126a1 100644
--- a/src/Specific/montgomery32_2e291m19/CurveParameters.v
+++ b/src/Specific/montgomery32_2e291m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e321m9/CurveParameters.v b/src/Specific/montgomery32_2e321m9/CurveParameters.v
index 770bdfef8..492ecac0f 100644
--- a/src/Specific/montgomery32_2e321m9/CurveParameters.v
+++ b/src/Specific/montgomery32_2e321m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e322m2e161m1/CurveParameters.v b/src/Specific/montgomery32_2e322m2e161m1/CurveParameters.v
index 6b6b8cb29..7486ca425 100644
--- a/src/Specific/montgomery32_2e322m2e161m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e322m2e161m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e336m17/CurveParameters.v b/src/Specific/montgomery32_2e336m17/CurveParameters.v
index 7861a8c37..231b9ddf7 100644
--- a/src/Specific/montgomery32_2e336m17/CurveParameters.v
+++ b/src/Specific/montgomery32_2e336m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e336m3/CurveParameters.v b/src/Specific/montgomery32_2e336m3/CurveParameters.v
index bdb087598..a03d11c28 100644
--- a/src/Specific/montgomery32_2e336m3/CurveParameters.v
+++ b/src/Specific/montgomery32_2e336m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e338m15/CurveParameters.v b/src/Specific/montgomery32_2e338m15/CurveParameters.v
index dd1fc6389..acab46614 100644
--- a/src/Specific/montgomery32_2e338m15/CurveParameters.v
+++ b/src/Specific/montgomery32_2e338m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e369m25/CurveParameters.v b/src/Specific/montgomery32_2e369m25/CurveParameters.v
index 70aa368fe..0ebd0e29c 100644
--- a/src/Specific/montgomery32_2e369m25/CurveParameters.v
+++ b/src/Specific/montgomery32_2e369m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e379m19/CurveParameters.v b/src/Specific/montgomery32_2e379m19/CurveParameters.v
index 3d8ebe7ab..ffaec84e8 100644
--- a/src/Specific/montgomery32_2e379m19/CurveParameters.v
+++ b/src/Specific/montgomery32_2e379m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e382m105/CurveParameters.v b/src/Specific/montgomery32_2e382m105/CurveParameters.v
index 6c59d1e8f..fde7808fe 100644
--- a/src/Specific/montgomery32_2e382m105/CurveParameters.v
+++ b/src/Specific/montgomery32_2e382m105/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e383m187/CurveParameters.v b/src/Specific/montgomery32_2e383m187/CurveParameters.v
index 3f800a4dc..df9b2f250 100644
--- a/src/Specific/montgomery32_2e383m187/CurveParameters.v
+++ b/src/Specific/montgomery32_2e383m187/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e383m31/CurveParameters.v b/src/Specific/montgomery32_2e383m31/CurveParameters.v
index 80d62d2ef..12f10af41 100644
--- a/src/Specific/montgomery32_2e383m31/CurveParameters.v
+++ b/src/Specific/montgomery32_2e383m31/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e383m421/CurveParameters.v b/src/Specific/montgomery32_2e383m421/CurveParameters.v
index 6416e0b7d..678e5243e 100644
--- a/src/Specific/montgomery32_2e383m421/CurveParameters.v
+++ b/src/Specific/montgomery32_2e383m421/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/CurveParameters.v b/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/CurveParameters.v
index 5de1894c4..e1d8d7f74 100644
--- a/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e384m317/CurveParameters.v b/src/Specific/montgomery32_2e384m317/CurveParameters.v
index d85590b0a..01b7f54d7 100644
--- a/src/Specific/montgomery32_2e384m317/CurveParameters.v
+++ b/src/Specific/montgomery32_2e384m317/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e384m5x2e368m1/CurveParameters.v b/src/Specific/montgomery32_2e384m5x2e368m1/CurveParameters.v
index 360b956c8..f220253fa 100644
--- a/src/Specific/montgomery32_2e384m5x2e368m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e384m5x2e368m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e384m79x2e376m1/CurveParameters.v b/src/Specific/montgomery32_2e384m79x2e376m1/CurveParameters.v
index c8c22c351..cf5e93859 100644
--- a/src/Specific/montgomery32_2e384m79x2e376m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e384m79x2e376m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e389m21/CurveParameters.v b/src/Specific/montgomery32_2e389m21/CurveParameters.v
index 48e1266e1..53d697165 100644
--- a/src/Specific/montgomery32_2e389m21/CurveParameters.v
+++ b/src/Specific/montgomery32_2e389m21/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e401m31/CurveParameters.v b/src/Specific/montgomery32_2e401m31/CurveParameters.v
index 4912cb0ca..131704a25 100644
--- a/src/Specific/montgomery32_2e401m31/CurveParameters.v
+++ b/src/Specific/montgomery32_2e401m31/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e413m21/CurveParameters.v b/src/Specific/montgomery32_2e413m21/CurveParameters.v
index e730df107..dade6d2e9 100644
--- a/src/Specific/montgomery32_2e413m21/CurveParameters.v
+++ b/src/Specific/montgomery32_2e413m21/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e414m17/CurveParameters.v b/src/Specific/montgomery32_2e414m17/CurveParameters.v
index 46f7ec5fb..cbe200a23 100644
--- a/src/Specific/montgomery32_2e414m17/CurveParameters.v
+++ b/src/Specific/montgomery32_2e414m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e416m2e208m1/CurveParameters.v b/src/Specific/montgomery32_2e416m2e208m1/CurveParameters.v
index 0a5932aab..199f2b1c8 100644
--- a/src/Specific/montgomery32_2e416m2e208m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e416m2e208m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e444m17/CurveParameters.v b/src/Specific/montgomery32_2e444m17/CurveParameters.v
index b52d70bf8..9911b3666 100644
--- a/src/Specific/montgomery32_2e444m17/CurveParameters.v
+++ b/src/Specific/montgomery32_2e444m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e448m2e224m1/CurveParameters.v b/src/Specific/montgomery32_2e448m2e224m1/CurveParameters.v
index d0cc8df99..87cb9da35 100644
--- a/src/Specific/montgomery32_2e448m2e224m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e448m2e224m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e450m2e225m1/CurveParameters.v b/src/Specific/montgomery32_2e450m2e225m1/CurveParameters.v
index cf698ea7c..ad40479c6 100644
--- a/src/Specific/montgomery32_2e450m2e225m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e450m2e225m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e452m3/CurveParameters.v b/src/Specific/montgomery32_2e452m3/CurveParameters.v
index 7a3659893..bc18572bd 100644
--- a/src/Specific/montgomery32_2e452m3/CurveParameters.v
+++ b/src/Specific/montgomery32_2e452m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e468m17/CurveParameters.v b/src/Specific/montgomery32_2e468m17/CurveParameters.v
index 6fee6b869..3f2a2d057 100644
--- a/src/Specific/montgomery32_2e468m17/CurveParameters.v
+++ b/src/Specific/montgomery32_2e468m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e480m2e240m1/CurveParameters.v b/src/Specific/montgomery32_2e480m2e240m1/CurveParameters.v
index a85b7147f..df2d34dd7 100644
--- a/src/Specific/montgomery32_2e480m2e240m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e480m2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e488m17/CurveParameters.v b/src/Specific/montgomery32_2e488m17/CurveParameters.v
index 37d6e3161..7e8ed034f 100644
--- a/src/Specific/montgomery32_2e488m17/CurveParameters.v
+++ b/src/Specific/montgomery32_2e488m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e489m21/CurveParameters.v b/src/Specific/montgomery32_2e489m21/CurveParameters.v
index 4537a31e4..f73876229 100644
--- a/src/Specific/montgomery32_2e489m21/CurveParameters.v
+++ b/src/Specific/montgomery32_2e489m21/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e495m31/CurveParameters.v b/src/Specific/montgomery32_2e495m31/CurveParameters.v
index 535bec5ff..bcaa3e33b 100644
--- a/src/Specific/montgomery32_2e495m31/CurveParameters.v
+++ b/src/Specific/montgomery32_2e495m31/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e510m290x2e496m1/CurveParameters.v b/src/Specific/montgomery32_2e510m290x2e496m1/CurveParameters.v
index 76315ccf3..8dd31f795 100644
--- a/src/Specific/montgomery32_2e510m290x2e496m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e510m290x2e496m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e511m187/CurveParameters.v b/src/Specific/montgomery32_2e511m187/CurveParameters.v
index 8b8319dce..466621f72 100644
--- a/src/Specific/montgomery32_2e511m187/CurveParameters.v
+++ b/src/Specific/montgomery32_2e511m187/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e511m481/CurveParameters.v b/src/Specific/montgomery32_2e511m481/CurveParameters.v
index b042acef5..549de6e98 100644
--- a/src/Specific/montgomery32_2e511m481/CurveParameters.v
+++ b/src/Specific/montgomery32_2e511m481/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e512m491x2e496m1/CurveParameters.v b/src/Specific/montgomery32_2e512m491x2e496m1/CurveParameters.v
index 3a70a2371..1ae4f17f9 100644
--- a/src/Specific/montgomery32_2e512m491x2e496m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e512m491x2e496m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e512m569/CurveParameters.v b/src/Specific/montgomery32_2e512m569/CurveParameters.v
index 7dd0ecf4f..cb83eba64 100644
--- a/src/Specific/montgomery32_2e512m569/CurveParameters.v
+++ b/src/Specific/montgomery32_2e512m569/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery32_2e521m1/CurveParameters.v b/src/Specific/montgomery32_2e521m1/CurveParameters.v
index f85fdf99c..92329b455 100644
--- a/src/Specific/montgomery32_2e521m1/CurveParameters.v
+++ b/src/Specific/montgomery32_2e521m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e127m1/CurveParameters.v b/src/Specific/montgomery64_2e127m1/CurveParameters.v
index 76fe26261..fb2a5146e 100644
--- a/src/Specific/montgomery64_2e127m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e127m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e129m25/CurveParameters.v b/src/Specific/montgomery64_2e129m25/CurveParameters.v
index f29d3a47f..a9a854de9 100644
--- a/src/Specific/montgomery64_2e129m25/CurveParameters.v
+++ b/src/Specific/montgomery64_2e129m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e130m5/CurveParameters.v b/src/Specific/montgomery64_2e130m5/CurveParameters.v
index f4db6e74e..b4ff2f97e 100644
--- a/src/Specific/montgomery64_2e130m5/CurveParameters.v
+++ b/src/Specific/montgomery64_2e130m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e137m13/CurveParameters.v b/src/Specific/montgomery64_2e137m13/CurveParameters.v
index 587b5b617..2e161dd87 100644
--- a/src/Specific/montgomery64_2e137m13/CurveParameters.v
+++ b/src/Specific/montgomery64_2e137m13/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e140m27/CurveParameters.v b/src/Specific/montgomery64_2e140m27/CurveParameters.v
index 8059e3cea..7ff1f6a0f 100644
--- a/src/Specific/montgomery64_2e140m27/CurveParameters.v
+++ b/src/Specific/montgomery64_2e140m27/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e141m9/CurveParameters.v b/src/Specific/montgomery64_2e141m9/CurveParameters.v
index 432d9c85c..1d4146465 100644
--- a/src/Specific/montgomery64_2e141m9/CurveParameters.v
+++ b/src/Specific/montgomery64_2e141m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e150m3/CurveParameters.v b/src/Specific/montgomery64_2e150m3/CurveParameters.v
index 23dd867c2..9fa7b1f6b 100644
--- a/src/Specific/montgomery64_2e150m3/CurveParameters.v
+++ b/src/Specific/montgomery64_2e150m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e150m5/CurveParameters.v b/src/Specific/montgomery64_2e150m5/CurveParameters.v
index 77e360ad5..249d46427 100644
--- a/src/Specific/montgomery64_2e150m5/CurveParameters.v
+++ b/src/Specific/montgomery64_2e150m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e152m17/CurveParameters.v b/src/Specific/montgomery64_2e152m17/CurveParameters.v
index 8279ff761..581741f40 100644
--- a/src/Specific/montgomery64_2e152m17/CurveParameters.v
+++ b/src/Specific/montgomery64_2e152m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e158m15/CurveParameters.v b/src/Specific/montgomery64_2e158m15/CurveParameters.v
index a26b25caa..82c1baba1 100644
--- a/src/Specific/montgomery64_2e158m15/CurveParameters.v
+++ b/src/Specific/montgomery64_2e158m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e165m25/CurveParameters.v b/src/Specific/montgomery64_2e165m25/CurveParameters.v
index fc3cd2eb7..3915190cb 100644
--- a/src/Specific/montgomery64_2e165m25/CurveParameters.v
+++ b/src/Specific/montgomery64_2e165m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e166m5/CurveParameters.v b/src/Specific/montgomery64_2e166m5/CurveParameters.v
index 14b88460a..b80118c5e 100644
--- a/src/Specific/montgomery64_2e166m5/CurveParameters.v
+++ b/src/Specific/montgomery64_2e166m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e171m19/CurveParameters.v b/src/Specific/montgomery64_2e171m19/CurveParameters.v
index ba69d191a..776c36f1e 100644
--- a/src/Specific/montgomery64_2e171m19/CurveParameters.v
+++ b/src/Specific/montgomery64_2e171m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e174m17/CurveParameters.v b/src/Specific/montgomery64_2e174m17/CurveParameters.v
index 37a0fef2a..73ad4b3fe 100644
--- a/src/Specific/montgomery64_2e174m17/CurveParameters.v
+++ b/src/Specific/montgomery64_2e174m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e174m3/CurveParameters.v b/src/Specific/montgomery64_2e174m3/CurveParameters.v
index 5ca7e71d0..fe20134ec 100644
--- a/src/Specific/montgomery64_2e174m3/CurveParameters.v
+++ b/src/Specific/montgomery64_2e174m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e189m25/CurveParameters.v b/src/Specific/montgomery64_2e189m25/CurveParameters.v
index 4d140e788..6f8159a72 100644
--- a/src/Specific/montgomery64_2e189m25/CurveParameters.v
+++ b/src/Specific/montgomery64_2e189m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e190m11/CurveParameters.v b/src/Specific/montgomery64_2e190m11/CurveParameters.v
index 72be2d66e..18a845f0f 100644
--- a/src/Specific/montgomery64_2e190m11/CurveParameters.v
+++ b/src/Specific/montgomery64_2e190m11/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e191m19/CurveParameters.v b/src/Specific/montgomery64_2e191m19/CurveParameters.v
index d0acf117b..54d7d6487 100644
--- a/src/Specific/montgomery64_2e191m19/CurveParameters.v
+++ b/src/Specific/montgomery64_2e191m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e192m2e64m1/CurveParameters.v b/src/Specific/montgomery64_2e192m2e64m1/CurveParameters.v
index c0e328181..bdd7fe851 100644
--- a/src/Specific/montgomery64_2e192m2e64m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e192m2e64m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e194m33/CurveParameters.v b/src/Specific/montgomery64_2e194m33/CurveParameters.v
index 7269d8689..2b450282c 100644
--- a/src/Specific/montgomery64_2e194m33/CurveParameters.v
+++ b/src/Specific/montgomery64_2e194m33/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e196m15/CurveParameters.v b/src/Specific/montgomery64_2e196m15/CurveParameters.v
index edd16e09e..f876ce2bf 100644
--- a/src/Specific/montgomery64_2e196m15/CurveParameters.v
+++ b/src/Specific/montgomery64_2e196m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e198m17/CurveParameters.v b/src/Specific/montgomery64_2e198m17/CurveParameters.v
index ec3e96771..16c39e743 100644
--- a/src/Specific/montgomery64_2e198m17/CurveParameters.v
+++ b/src/Specific/montgomery64_2e198m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e205m45x2e198m1/CurveParameters.v b/src/Specific/montgomery64_2e205m45x2e198m1/CurveParameters.v
index 459a50f6d..69690d6d5 100644
--- a/src/Specific/montgomery64_2e205m45x2e198m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e205m45x2e198m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e206m5/CurveParameters.v b/src/Specific/montgomery64_2e206m5/CurveParameters.v
index cfbc549d6..b96f6d0a6 100644
--- a/src/Specific/montgomery64_2e206m5/CurveParameters.v
+++ b/src/Specific/montgomery64_2e206m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e212m29/CurveParameters.v b/src/Specific/montgomery64_2e212m29/CurveParameters.v
index 65d3893f3..569504adc 100644
--- a/src/Specific/montgomery64_2e212m29/CurveParameters.v
+++ b/src/Specific/montgomery64_2e212m29/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e213m3/CurveParameters.v b/src/Specific/montgomery64_2e213m3/CurveParameters.v
index b94c40f3c..f260326b0 100644
--- a/src/Specific/montgomery64_2e213m3/CurveParameters.v
+++ b/src/Specific/montgomery64_2e213m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e216m2e108m1/CurveParameters.v b/src/Specific/montgomery64_2e216m2e108m1/CurveParameters.v
index 6c28b53ab..945150d91 100644
--- a/src/Specific/montgomery64_2e216m2e108m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e216m2e108m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e221m3/CurveParameters.v b/src/Specific/montgomery64_2e221m3/CurveParameters.v
index d56417476..2eb4ee31e 100644
--- a/src/Specific/montgomery64_2e221m3/CurveParameters.v
+++ b/src/Specific/montgomery64_2e221m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e222m117/CurveParameters.v b/src/Specific/montgomery64_2e222m117/CurveParameters.v
index 32a0d0ae4..894baebcb 100644
--- a/src/Specific/montgomery64_2e222m117/CurveParameters.v
+++ b/src/Specific/montgomery64_2e222m117/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e224m2e96p1/CurveParameters.v b/src/Specific/montgomery64_2e224m2e96p1/CurveParameters.v
index 7b7032e2c..e28cc7788 100644
--- a/src/Specific/montgomery64_2e224m2e96p1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e224m2e96p1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e226m5/CurveParameters.v b/src/Specific/montgomery64_2e226m5/CurveParameters.v
index dc9f2e818..3e97cd422 100644
--- a/src/Specific/montgomery64_2e226m5/CurveParameters.v
+++ b/src/Specific/montgomery64_2e226m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e230m27/CurveParameters.v b/src/Specific/montgomery64_2e230m27/CurveParameters.v
index 4451ac5f5..488698c86 100644
--- a/src/Specific/montgomery64_2e230m27/CurveParameters.v
+++ b/src/Specific/montgomery64_2e230m27/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e235m15/CurveParameters.v b/src/Specific/montgomery64_2e235m15/CurveParameters.v
index 4d8baaad6..bf979d13d 100644
--- a/src/Specific/montgomery64_2e235m15/CurveParameters.v
+++ b/src/Specific/montgomery64_2e235m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e243m9/CurveParameters.v b/src/Specific/montgomery64_2e243m9/CurveParameters.v
index b4980469f..51d5b0a88 100644
--- a/src/Specific/montgomery64_2e243m9/CurveParameters.v
+++ b/src/Specific/montgomery64_2e243m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e251m9/CurveParameters.v b/src/Specific/montgomery64_2e251m9/CurveParameters.v
index 30e0510f6..0f61ec8c0 100644
--- a/src/Specific/montgomery64_2e251m9/CurveParameters.v
+++ b/src/Specific/montgomery64_2e251m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e254m127x2e240m1/CurveParameters.v b/src/Specific/montgomery64_2e254m127x2e240m1/CurveParameters.v
index 0b8b1b3d8..34d6d4b0c 100644
--- a/src/Specific/montgomery64_2e254m127x2e240m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e254m127x2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e255m19/CurveParameters.v b/src/Specific/montgomery64_2e255m19/CurveParameters.v
index 76b2cb5be..a82c6a4f3 100644
--- a/src/Specific/montgomery64_2e255m19/CurveParameters.v
+++ b/src/Specific/montgomery64_2e255m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e255m2e4m2e1m1/CurveParameters.v b/src/Specific/montgomery64_2e255m2e4m2e1m1/CurveParameters.v
index 7d97f2d40..caefcd321 100644
--- a/src/Specific/montgomery64_2e255m2e4m2e1m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e255m2e4m2e1m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e255m765/CurveParameters.v b/src/Specific/montgomery64_2e255m765/CurveParameters.v
index 93fa1e31c..24ae9e3d8 100644
--- a/src/Specific/montgomery64_2e255m765/CurveParameters.v
+++ b/src/Specific/montgomery64_2e255m765/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e256m189/CurveParameters.v b/src/Specific/montgomery64_2e256m189/CurveParameters.v
index f9c59d753..c6844835e 100644
--- a/src/Specific/montgomery64_2e256m189/CurveParameters.v
+++ b/src/Specific/montgomery64_2e256m189/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1/CurveParameters.v b/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1/CurveParameters.v
index 1bbcf4b87..1d1a9e4a7 100644
--- a/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e256m2e32m977/CurveParameters.v b/src/Specific/montgomery64_2e256m2e32m977/CurveParameters.v
index c8b8bca34..0c0b5f720 100644
--- a/src/Specific/montgomery64_2e256m2e32m977/CurveParameters.v
+++ b/src/Specific/montgomery64_2e256m2e32m977/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e256m88x2e240m1/CurveParameters.v b/src/Specific/montgomery64_2e256m88x2e240m1/CurveParameters.v
index 7a8872bfb..e0f31c209 100644
--- a/src/Specific/montgomery64_2e256m88x2e240m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e256m88x2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e266m3/CurveParameters.v b/src/Specific/montgomery64_2e266m3/CurveParameters.v
index 64000bd7a..fb791dd86 100644
--- a/src/Specific/montgomery64_2e266m3/CurveParameters.v
+++ b/src/Specific/montgomery64_2e266m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e285m9/CurveParameters.v b/src/Specific/montgomery64_2e285m9/CurveParameters.v
index c4063ee2f..2fa34e17e 100644
--- a/src/Specific/montgomery64_2e285m9/CurveParameters.v
+++ b/src/Specific/montgomery64_2e285m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e291m19/CurveParameters.v b/src/Specific/montgomery64_2e291m19/CurveParameters.v
index 5cab89ec4..8067dfdd2 100644
--- a/src/Specific/montgomery64_2e291m19/CurveParameters.v
+++ b/src/Specific/montgomery64_2e291m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e321m9/CurveParameters.v b/src/Specific/montgomery64_2e321m9/CurveParameters.v
index e28b0caf9..040e23d2d 100644
--- a/src/Specific/montgomery64_2e321m9/CurveParameters.v
+++ b/src/Specific/montgomery64_2e321m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e322m2e161m1/CurveParameters.v b/src/Specific/montgomery64_2e322m2e161m1/CurveParameters.v
index 3a639c9e4..340e7f55a 100644
--- a/src/Specific/montgomery64_2e322m2e161m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e322m2e161m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e336m17/CurveParameters.v b/src/Specific/montgomery64_2e336m17/CurveParameters.v
index 1210bd46d..b0d15fb57 100644
--- a/src/Specific/montgomery64_2e336m17/CurveParameters.v
+++ b/src/Specific/montgomery64_2e336m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e336m3/CurveParameters.v b/src/Specific/montgomery64_2e336m3/CurveParameters.v
index ef476746f..eb90a6f99 100644
--- a/src/Specific/montgomery64_2e336m3/CurveParameters.v
+++ b/src/Specific/montgomery64_2e336m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e338m15/CurveParameters.v b/src/Specific/montgomery64_2e338m15/CurveParameters.v
index 0912f474d..2aca237b6 100644
--- a/src/Specific/montgomery64_2e338m15/CurveParameters.v
+++ b/src/Specific/montgomery64_2e338m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e369m25/CurveParameters.v b/src/Specific/montgomery64_2e369m25/CurveParameters.v
index 6478b3708..5cddeef19 100644
--- a/src/Specific/montgomery64_2e369m25/CurveParameters.v
+++ b/src/Specific/montgomery64_2e369m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e379m19/CurveParameters.v b/src/Specific/montgomery64_2e379m19/CurveParameters.v
index 5c8f456da..47dad6280 100644
--- a/src/Specific/montgomery64_2e379m19/CurveParameters.v
+++ b/src/Specific/montgomery64_2e379m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e382m105/CurveParameters.v b/src/Specific/montgomery64_2e382m105/CurveParameters.v
index 436d88ff7..3a16d34a1 100644
--- a/src/Specific/montgomery64_2e382m105/CurveParameters.v
+++ b/src/Specific/montgomery64_2e382m105/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e383m187/CurveParameters.v b/src/Specific/montgomery64_2e383m187/CurveParameters.v
index 36c4d99c1..cc4e4efae 100644
--- a/src/Specific/montgomery64_2e383m187/CurveParameters.v
+++ b/src/Specific/montgomery64_2e383m187/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e383m31/CurveParameters.v b/src/Specific/montgomery64_2e383m31/CurveParameters.v
index 1ee40b3d6..da9efc880 100644
--- a/src/Specific/montgomery64_2e383m31/CurveParameters.v
+++ b/src/Specific/montgomery64_2e383m31/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e383m421/CurveParameters.v b/src/Specific/montgomery64_2e383m421/CurveParameters.v
index fae00b805..65b26ddae 100644
--- a/src/Specific/montgomery64_2e383m421/CurveParameters.v
+++ b/src/Specific/montgomery64_2e383m421/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e384m2e128m2e96p2e32m1/CurveParameters.v b/src/Specific/montgomery64_2e384m2e128m2e96p2e32m1/CurveParameters.v
index af15a9e48..406a8de00 100644
--- a/src/Specific/montgomery64_2e384m2e128m2e96p2e32m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e384m2e128m2e96p2e32m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e384m317/CurveParameters.v b/src/Specific/montgomery64_2e384m317/CurveParameters.v
index 5eb7c760f..9616800d3 100644
--- a/src/Specific/montgomery64_2e384m317/CurveParameters.v
+++ b/src/Specific/montgomery64_2e384m317/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e384m5x2e368m1/CurveParameters.v b/src/Specific/montgomery64_2e384m5x2e368m1/CurveParameters.v
index 7d246de33..6642c8a5b 100644
--- a/src/Specific/montgomery64_2e384m5x2e368m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e384m5x2e368m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e384m79x2e376m1/CurveParameters.v b/src/Specific/montgomery64_2e384m79x2e376m1/CurveParameters.v
index 52bfaf504..67ec75679 100644
--- a/src/Specific/montgomery64_2e384m79x2e376m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e384m79x2e376m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e389m21/CurveParameters.v b/src/Specific/montgomery64_2e389m21/CurveParameters.v
index acac04ddd..a7a960cdf 100644
--- a/src/Specific/montgomery64_2e389m21/CurveParameters.v
+++ b/src/Specific/montgomery64_2e389m21/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e401m31/CurveParameters.v b/src/Specific/montgomery64_2e401m31/CurveParameters.v
index 00acfe820..1f1900525 100644
--- a/src/Specific/montgomery64_2e401m31/CurveParameters.v
+++ b/src/Specific/montgomery64_2e401m31/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e413m21/CurveParameters.v b/src/Specific/montgomery64_2e413m21/CurveParameters.v
index 33b627edd..072b07875 100644
--- a/src/Specific/montgomery64_2e413m21/CurveParameters.v
+++ b/src/Specific/montgomery64_2e413m21/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e414m17/CurveParameters.v b/src/Specific/montgomery64_2e414m17/CurveParameters.v
index 60512c1f1..cd6d8ee68 100644
--- a/src/Specific/montgomery64_2e414m17/CurveParameters.v
+++ b/src/Specific/montgomery64_2e414m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e416m2e208m1/CurveParameters.v b/src/Specific/montgomery64_2e416m2e208m1/CurveParameters.v
index aac9ae3c3..15fb68dac 100644
--- a/src/Specific/montgomery64_2e416m2e208m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e416m2e208m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e444m17/CurveParameters.v b/src/Specific/montgomery64_2e444m17/CurveParameters.v
index 369f6d89b..fa0acb741 100644
--- a/src/Specific/montgomery64_2e444m17/CurveParameters.v
+++ b/src/Specific/montgomery64_2e444m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e448m2e224m1/CurveParameters.v b/src/Specific/montgomery64_2e448m2e224m1/CurveParameters.v
index b2877bf4e..c61e96569 100644
--- a/src/Specific/montgomery64_2e448m2e224m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e448m2e224m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e450m2e225m1/CurveParameters.v b/src/Specific/montgomery64_2e450m2e225m1/CurveParameters.v
index 2011f85a2..69aefbd94 100644
--- a/src/Specific/montgomery64_2e450m2e225m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e450m2e225m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e452m3/CurveParameters.v b/src/Specific/montgomery64_2e452m3/CurveParameters.v
index 6d66fd5a0..9dd11515b 100644
--- a/src/Specific/montgomery64_2e452m3/CurveParameters.v
+++ b/src/Specific/montgomery64_2e452m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e468m17/CurveParameters.v b/src/Specific/montgomery64_2e468m17/CurveParameters.v
index df2734355..46f3af838 100644
--- a/src/Specific/montgomery64_2e468m17/CurveParameters.v
+++ b/src/Specific/montgomery64_2e468m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e480m2e240m1/CurveParameters.v b/src/Specific/montgomery64_2e480m2e240m1/CurveParameters.v
index 399ada91e..84f491bef 100644
--- a/src/Specific/montgomery64_2e480m2e240m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e480m2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e488m17/CurveParameters.v b/src/Specific/montgomery64_2e488m17/CurveParameters.v
index 88fe34402..686a23539 100644
--- a/src/Specific/montgomery64_2e488m17/CurveParameters.v
+++ b/src/Specific/montgomery64_2e488m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e489m21/CurveParameters.v b/src/Specific/montgomery64_2e489m21/CurveParameters.v
index 8a183cfe6..dcff12f2b 100644
--- a/src/Specific/montgomery64_2e489m21/CurveParameters.v
+++ b/src/Specific/montgomery64_2e489m21/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e495m31/CurveParameters.v b/src/Specific/montgomery64_2e495m31/CurveParameters.v
index 23089a738..168ddec41 100644
--- a/src/Specific/montgomery64_2e495m31/CurveParameters.v
+++ b/src/Specific/montgomery64_2e495m31/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e510m290x2e496m1/CurveParameters.v b/src/Specific/montgomery64_2e510m290x2e496m1/CurveParameters.v
index 70ce77a74..d8cf3d25f 100644
--- a/src/Specific/montgomery64_2e510m290x2e496m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e510m290x2e496m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e511m187/CurveParameters.v b/src/Specific/montgomery64_2e511m187/CurveParameters.v
index 69af68680..20f69fb93 100644
--- a/src/Specific/montgomery64_2e511m187/CurveParameters.v
+++ b/src/Specific/montgomery64_2e511m187/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e511m481/CurveParameters.v b/src/Specific/montgomery64_2e511m481/CurveParameters.v
index 355738361..37ba2f8dd 100644
--- a/src/Specific/montgomery64_2e511m481/CurveParameters.v
+++ b/src/Specific/montgomery64_2e511m481/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e512m491x2e496m1/CurveParameters.v b/src/Specific/montgomery64_2e512m491x2e496m1/CurveParameters.v
index 26ea5eb0f..accf6b9a7 100644
--- a/src/Specific/montgomery64_2e512m491x2e496m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e512m491x2e496m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e512m569/CurveParameters.v b/src/Specific/montgomery64_2e512m569/CurveParameters.v
index 55400d77c..0496d086b 100644
--- a/src/Specific/montgomery64_2e512m569/CurveParameters.v
+++ b/src/Specific/montgomery64_2e512m569/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/montgomery64_2e521m1/CurveParameters.v b/src/Specific/montgomery64_2e521m1/CurveParameters.v
index a95521e2e..171d1b5a0 100644
--- a/src/Specific/montgomery64_2e521m1/CurveParameters.v
+++ b/src/Specific/montgomery64_2e521m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := None;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := true;
     freeze := Some false;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e127m1/CurveParameters.v b/src/Specific/solinas32_2e127m1/CurveParameters.v
index b7fed3164..2071cfd04 100644
--- a/src/Specific/solinas32_2e127m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e127m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e129m25/CurveParameters.v b/src/Specific/solinas32_2e129m25/CurveParameters.v
index 3830b60ac..7031863e9 100644
--- a/src/Specific/solinas32_2e129m25/CurveParameters.v
+++ b/src/Specific/solinas32_2e129m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e130m5/CurveParameters.v b/src/Specific/solinas32_2e130m5/CurveParameters.v
index 03a00d55b..4c7d39418 100644
--- a/src/Specific/solinas32_2e130m5/CurveParameters.v
+++ b/src/Specific/solinas32_2e130m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e137m13/CurveParameters.v b/src/Specific/solinas32_2e137m13/CurveParameters.v
index e04bf7c43..11881a98e 100644
--- a/src/Specific/solinas32_2e137m13/CurveParameters.v
+++ b/src/Specific/solinas32_2e137m13/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e140m27/CurveParameters.v b/src/Specific/solinas32_2e140m27/CurveParameters.v
index 4b0a53147..57672aa0b 100644
--- a/src/Specific/solinas32_2e140m27/CurveParameters.v
+++ b/src/Specific/solinas32_2e140m27/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e141m9/CurveParameters.v b/src/Specific/solinas32_2e141m9/CurveParameters.v
index 228ad1c88..8c12f0251 100644
--- a/src/Specific/solinas32_2e141m9/CurveParameters.v
+++ b/src/Specific/solinas32_2e141m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e150m3/CurveParameters.v b/src/Specific/solinas32_2e150m3/CurveParameters.v
index 315907b0d..ca67a36cd 100644
--- a/src/Specific/solinas32_2e150m3/CurveParameters.v
+++ b/src/Specific/solinas32_2e150m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e150m5/CurveParameters.v b/src/Specific/solinas32_2e150m5/CurveParameters.v
index f1e2d4e21..4ee09cc7d 100644
--- a/src/Specific/solinas32_2e150m5/CurveParameters.v
+++ b/src/Specific/solinas32_2e150m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e152m17/CurveParameters.v b/src/Specific/solinas32_2e152m17/CurveParameters.v
index f81199d0f..22ea729fc 100644
--- a/src/Specific/solinas32_2e152m17/CurveParameters.v
+++ b/src/Specific/solinas32_2e152m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e158m15/CurveParameters.v b/src/Specific/solinas32_2e158m15/CurveParameters.v
index fb34a0130..726a23d43 100644
--- a/src/Specific/solinas32_2e158m15/CurveParameters.v
+++ b/src/Specific/solinas32_2e158m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e165m25/CurveParameters.v b/src/Specific/solinas32_2e165m25/CurveParameters.v
index 493acbfc6..2cd0d20c0 100644
--- a/src/Specific/solinas32_2e165m25/CurveParameters.v
+++ b/src/Specific/solinas32_2e165m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e166m5/CurveParameters.v b/src/Specific/solinas32_2e166m5/CurveParameters.v
index 584877a0d..785fab228 100644
--- a/src/Specific/solinas32_2e166m5/CurveParameters.v
+++ b/src/Specific/solinas32_2e166m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e171m19/CurveParameters.v b/src/Specific/solinas32_2e171m19/CurveParameters.v
index b2027b474..ea04a1f0b 100644
--- a/src/Specific/solinas32_2e171m19/CurveParameters.v
+++ b/src/Specific/solinas32_2e171m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e174m17/CurveParameters.v b/src/Specific/solinas32_2e174m17/CurveParameters.v
index 47f9092a1..a3763c3c8 100644
--- a/src/Specific/solinas32_2e174m17/CurveParameters.v
+++ b/src/Specific/solinas32_2e174m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e174m3/CurveParameters.v b/src/Specific/solinas32_2e174m3/CurveParameters.v
index 901a78cfb..a183ef6ba 100644
--- a/src/Specific/solinas32_2e174m3/CurveParameters.v
+++ b/src/Specific/solinas32_2e174m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e189m25/CurveParameters.v b/src/Specific/solinas32_2e189m25/CurveParameters.v
index b1b1fe437..f846046f4 100644
--- a/src/Specific/solinas32_2e189m25/CurveParameters.v
+++ b/src/Specific/solinas32_2e189m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e190m11/CurveParameters.v b/src/Specific/solinas32_2e190m11/CurveParameters.v
index 5b8cad554..b610a7925 100644
--- a/src/Specific/solinas32_2e190m11/CurveParameters.v
+++ b/src/Specific/solinas32_2e190m11/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e191m19/CurveParameters.v b/src/Specific/solinas32_2e191m19/CurveParameters.v
index fae39382e..d07863ecc 100644
--- a/src/Specific/solinas32_2e191m19/CurveParameters.v
+++ b/src/Specific/solinas32_2e191m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e192m2e64m1/CurveParameters.v b/src/Specific/solinas32_2e192m2e64m1/CurveParameters.v
index 81f5d6eb9..7f67556c1 100644
--- a/src/Specific/solinas32_2e192m2e64m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e192m2e64m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e194m33/CurveParameters.v b/src/Specific/solinas32_2e194m33/CurveParameters.v
index 648dae549..ac84fa183 100644
--- a/src/Specific/solinas32_2e194m33/CurveParameters.v
+++ b/src/Specific/solinas32_2e194m33/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e196m15/CurveParameters.v b/src/Specific/solinas32_2e196m15/CurveParameters.v
index c571253e5..f650aa6fe 100644
--- a/src/Specific/solinas32_2e196m15/CurveParameters.v
+++ b/src/Specific/solinas32_2e196m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e198m17/CurveParameters.v b/src/Specific/solinas32_2e198m17/CurveParameters.v
index d99687342..edf315311 100644
--- a/src/Specific/solinas32_2e198m17/CurveParameters.v
+++ b/src/Specific/solinas32_2e198m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e205m45x2e198m1/CurveParameters.v b/src/Specific/solinas32_2e205m45x2e198m1/CurveParameters.v
index 6efcefadb..0d9676ba1 100644
--- a/src/Specific/solinas32_2e205m45x2e198m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e205m45x2e198m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e206m5/CurveParameters.v b/src/Specific/solinas32_2e206m5/CurveParameters.v
index 9661f9597..11912b12b 100644
--- a/src/Specific/solinas32_2e206m5/CurveParameters.v
+++ b/src/Specific/solinas32_2e206m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e212m29/CurveParameters.v b/src/Specific/solinas32_2e212m29/CurveParameters.v
index 89447d3aa..608767c8b 100644
--- a/src/Specific/solinas32_2e212m29/CurveParameters.v
+++ b/src/Specific/solinas32_2e212m29/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e213m3/CurveParameters.v b/src/Specific/solinas32_2e213m3/CurveParameters.v
index 3b12b73f8..fb3ffa3b2 100644
--- a/src/Specific/solinas32_2e213m3/CurveParameters.v
+++ b/src/Specific/solinas32_2e213m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e216m2e108m1/CurveParameters.v b/src/Specific/solinas32_2e216m2e108m1/CurveParameters.v
index 5710a3c64..c780f984b 100644
--- a/src/Specific/solinas32_2e216m2e108m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e216m2e108m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e221m3/CurveParameters.v b/src/Specific/solinas32_2e221m3/CurveParameters.v
index 2b591da9c..44a491d2e 100644
--- a/src/Specific/solinas32_2e221m3/CurveParameters.v
+++ b/src/Specific/solinas32_2e221m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e222m117/CurveParameters.v b/src/Specific/solinas32_2e222m117/CurveParameters.v
index 0f31d178e..75c7e2c96 100644
--- a/src/Specific/solinas32_2e222m117/CurveParameters.v
+++ b/src/Specific/solinas32_2e222m117/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e224m2e96p1/CurveParameters.v b/src/Specific/solinas32_2e224m2e96p1/CurveParameters.v
index 7a7b807a5..97c22e1cd 100644
--- a/src/Specific/solinas32_2e224m2e96p1/CurveParameters.v
+++ b/src/Specific/solinas32_2e224m2e96p1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e226m5/CurveParameters.v b/src/Specific/solinas32_2e226m5/CurveParameters.v
index f1dc1994d..9aa558673 100644
--- a/src/Specific/solinas32_2e226m5/CurveParameters.v
+++ b/src/Specific/solinas32_2e226m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e230m27/CurveParameters.v b/src/Specific/solinas32_2e230m27/CurveParameters.v
index 3ff7db66b..dfc3c0964 100644
--- a/src/Specific/solinas32_2e230m27/CurveParameters.v
+++ b/src/Specific/solinas32_2e230m27/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e235m15/CurveParameters.v b/src/Specific/solinas32_2e235m15/CurveParameters.v
index 477375958..2c254584e 100644
--- a/src/Specific/solinas32_2e235m15/CurveParameters.v
+++ b/src/Specific/solinas32_2e235m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e243m9/CurveParameters.v b/src/Specific/solinas32_2e243m9/CurveParameters.v
index 885a220ea..0ced35491 100644
--- a/src/Specific/solinas32_2e243m9/CurveParameters.v
+++ b/src/Specific/solinas32_2e243m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e251m9/CurveParameters.v b/src/Specific/solinas32_2e251m9/CurveParameters.v
index f0d999a16..1cbf603c8 100644
--- a/src/Specific/solinas32_2e251m9/CurveParameters.v
+++ b/src/Specific/solinas32_2e251m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e254m127x2e240m1/CurveParameters.v b/src/Specific/solinas32_2e254m127x2e240m1/CurveParameters.v
index 3621b91c5..ac8cdc9d4 100644
--- a/src/Specific/solinas32_2e254m127x2e240m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e254m127x2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e255m19/CurveParameters.v b/src/Specific/solinas32_2e255m19/CurveParameters.v
index f36489ed8..64e2e84b7 100644
--- a/src/Specific/solinas32_2e255m19/CurveParameters.v
+++ b/src/Specific/solinas32_2e255m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e255m2e4m2e1m1/CurveParameters.v b/src/Specific/solinas32_2e255m2e4m2e1m1/CurveParameters.v
index 8d1a99a21..bdbf97b17 100644
--- a/src/Specific/solinas32_2e255m2e4m2e1m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e255m2e4m2e1m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e255m765/CurveParameters.v b/src/Specific/solinas32_2e255m765/CurveParameters.v
index 1d71fdff4..7e852b89d 100644
--- a/src/Specific/solinas32_2e255m765/CurveParameters.v
+++ b/src/Specific/solinas32_2e255m765/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e256m189/CurveParameters.v b/src/Specific/solinas32_2e256m189/CurveParameters.v
index d3fbb51d9..6d6c9c664 100644
--- a/src/Specific/solinas32_2e256m189/CurveParameters.v
+++ b/src/Specific/solinas32_2e256m189/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e256m2e224p2e192p2e96m1/CurveParameters.v b/src/Specific/solinas32_2e256m2e224p2e192p2e96m1/CurveParameters.v
index 87b4ba01c..ed060118e 100644
--- a/src/Specific/solinas32_2e256m2e224p2e192p2e96m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e256m2e224p2e192p2e96m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e256m2e32m977/CurveParameters.v b/src/Specific/solinas32_2e256m2e32m977/CurveParameters.v
index eb4797601..507c16669 100644
--- a/src/Specific/solinas32_2e256m2e32m977/CurveParameters.v
+++ b/src/Specific/solinas32_2e256m2e32m977/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e256m88x2e240m1/CurveParameters.v b/src/Specific/solinas32_2e256m88x2e240m1/CurveParameters.v
index dbb23c9f5..b86e7df67 100644
--- a/src/Specific/solinas32_2e256m88x2e240m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e256m88x2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e266m3/CurveParameters.v b/src/Specific/solinas32_2e266m3/CurveParameters.v
index 99e44e720..72da81c42 100644
--- a/src/Specific/solinas32_2e266m3/CurveParameters.v
+++ b/src/Specific/solinas32_2e266m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e285m9/CurveParameters.v b/src/Specific/solinas32_2e285m9/CurveParameters.v
index 571611a8c..e8fc65d20 100644
--- a/src/Specific/solinas32_2e285m9/CurveParameters.v
+++ b/src/Specific/solinas32_2e285m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e291m19/CurveParameters.v b/src/Specific/solinas32_2e291m19/CurveParameters.v
index 7f8506441..e05bfb74e 100644
--- a/src/Specific/solinas32_2e291m19/CurveParameters.v
+++ b/src/Specific/solinas32_2e291m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e321m9/CurveParameters.v b/src/Specific/solinas32_2e321m9/CurveParameters.v
index 969bc78b4..4aab4b64c 100644
--- a/src/Specific/solinas32_2e321m9/CurveParameters.v
+++ b/src/Specific/solinas32_2e321m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e322m2e161m1/CurveParameters.v b/src/Specific/solinas32_2e322m2e161m1/CurveParameters.v
index a95e50088..d6740403e 100644
--- a/src/Specific/solinas32_2e322m2e161m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e322m2e161m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e336m17/CurveParameters.v b/src/Specific/solinas32_2e336m17/CurveParameters.v
index 41635b9ec..15113ce93 100644
--- a/src/Specific/solinas32_2e336m17/CurveParameters.v
+++ b/src/Specific/solinas32_2e336m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e336m3/CurveParameters.v b/src/Specific/solinas32_2e336m3/CurveParameters.v
index 3da01232a..8bcb0ddbc 100644
--- a/src/Specific/solinas32_2e336m3/CurveParameters.v
+++ b/src/Specific/solinas32_2e336m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e338m15/CurveParameters.v b/src/Specific/solinas32_2e338m15/CurveParameters.v
index 21876e595..a76083880 100644
--- a/src/Specific/solinas32_2e338m15/CurveParameters.v
+++ b/src/Specific/solinas32_2e338m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e369m25/CurveParameters.v b/src/Specific/solinas32_2e369m25/CurveParameters.v
index eaf6e034a..bcbf236a9 100644
--- a/src/Specific/solinas32_2e369m25/CurveParameters.v
+++ b/src/Specific/solinas32_2e369m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e379m19/CurveParameters.v b/src/Specific/solinas32_2e379m19/CurveParameters.v
index f0c77132e..f58ddcf9b 100644
--- a/src/Specific/solinas32_2e379m19/CurveParameters.v
+++ b/src/Specific/solinas32_2e379m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e382m105/CurveParameters.v b/src/Specific/solinas32_2e382m105/CurveParameters.v
index 54e3b65bc..c7a1df85a 100644
--- a/src/Specific/solinas32_2e382m105/CurveParameters.v
+++ b/src/Specific/solinas32_2e382m105/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e384m2e128m2e96p2e32m1/CurveParameters.v b/src/Specific/solinas32_2e384m2e128m2e96p2e32m1/CurveParameters.v
index d58628a03..9b8dba361 100644
--- a/src/Specific/solinas32_2e384m2e128m2e96p2e32m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e384m2e128m2e96p2e32m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e384m317/CurveParameters.v b/src/Specific/solinas32_2e384m317/CurveParameters.v
index 3dda959a2..303f38aa6 100644
--- a/src/Specific/solinas32_2e384m317/CurveParameters.v
+++ b/src/Specific/solinas32_2e384m317/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e384m5x2e368m1/CurveParameters.v b/src/Specific/solinas32_2e384m5x2e368m1/CurveParameters.v
index bf1dfae0e..45616f877 100644
--- a/src/Specific/solinas32_2e384m5x2e368m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e384m5x2e368m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e384m79x2e376m1/CurveParameters.v b/src/Specific/solinas32_2e384m79x2e376m1/CurveParameters.v
index 91c9e295e..6f020d716 100644
--- a/src/Specific/solinas32_2e384m79x2e376m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e384m79x2e376m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e401m31/CurveParameters.v b/src/Specific/solinas32_2e401m31/CurveParameters.v
index 3f0b95dfb..9b085df66 100644
--- a/src/Specific/solinas32_2e401m31/CurveParameters.v
+++ b/src/Specific/solinas32_2e401m31/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e414m17/CurveParameters.v b/src/Specific/solinas32_2e414m17/CurveParameters.v
index 943a6dc12..e27103969 100644
--- a/src/Specific/solinas32_2e414m17/CurveParameters.v
+++ b/src/Specific/solinas32_2e414m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e416m2e208m1/CurveParameters.v b/src/Specific/solinas32_2e416m2e208m1/CurveParameters.v
index 225811e1b..327219e36 100644
--- a/src/Specific/solinas32_2e416m2e208m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e416m2e208m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e444m17/CurveParameters.v b/src/Specific/solinas32_2e444m17/CurveParameters.v
index dda8b0de0..0d71315d5 100644
--- a/src/Specific/solinas32_2e444m17/CurveParameters.v
+++ b/src/Specific/solinas32_2e444m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e448m2e224m1/CurveParameters.v b/src/Specific/solinas32_2e448m2e224m1/CurveParameters.v
index 54aacfbfe..7588e5dd1 100644
--- a/src/Specific/solinas32_2e448m2e224m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e448m2e224m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e450m2e225m1/CurveParameters.v b/src/Specific/solinas32_2e450m2e225m1/CurveParameters.v
index d7741bda7..052aeb36e 100644
--- a/src/Specific/solinas32_2e450m2e225m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e450m2e225m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e452m3/CurveParameters.v b/src/Specific/solinas32_2e452m3/CurveParameters.v
index 62460e879..c876bc5bb 100644
--- a/src/Specific/solinas32_2e452m3/CurveParameters.v
+++ b/src/Specific/solinas32_2e452m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e468m17/CurveParameters.v b/src/Specific/solinas32_2e468m17/CurveParameters.v
index 9a2f689cf..4bb88d487 100644
--- a/src/Specific/solinas32_2e468m17/CurveParameters.v
+++ b/src/Specific/solinas32_2e468m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e480m2e240m1/CurveParameters.v b/src/Specific/solinas32_2e480m2e240m1/CurveParameters.v
index f07253919..810a28856 100644
--- a/src/Specific/solinas32_2e480m2e240m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e480m2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e488m17/CurveParameters.v b/src/Specific/solinas32_2e488m17/CurveParameters.v
index 78967fede..888cb21c1 100644
--- a/src/Specific/solinas32_2e488m17/CurveParameters.v
+++ b/src/Specific/solinas32_2e488m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e489m21/CurveParameters.v b/src/Specific/solinas32_2e489m21/CurveParameters.v
index 03ee43b95..517a6dc09 100644
--- a/src/Specific/solinas32_2e489m21/CurveParameters.v
+++ b/src/Specific/solinas32_2e489m21/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e495m31/CurveParameters.v b/src/Specific/solinas32_2e495m31/CurveParameters.v
index f30322224..a92c8f408 100644
--- a/src/Specific/solinas32_2e495m31/CurveParameters.v
+++ b/src/Specific/solinas32_2e495m31/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e510m290x2e496m1/CurveParameters.v b/src/Specific/solinas32_2e510m290x2e496m1/CurveParameters.v
index 9160fda47..b18533e1f 100644
--- a/src/Specific/solinas32_2e510m290x2e496m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e510m290x2e496m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e511m187/CurveParameters.v b/src/Specific/solinas32_2e511m187/CurveParameters.v
index 1ccfc438e..257c04523 100644
--- a/src/Specific/solinas32_2e511m187/CurveParameters.v
+++ b/src/Specific/solinas32_2e511m187/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e511m481/CurveParameters.v b/src/Specific/solinas32_2e511m481/CurveParameters.v
index 10a07a04a..d7640365d 100644
--- a/src/Specific/solinas32_2e511m481/CurveParameters.v
+++ b/src/Specific/solinas32_2e511m481/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e512m491x2e496m1/CurveParameters.v b/src/Specific/solinas32_2e512m491x2e496m1/CurveParameters.v
index d0e7b78e1..a8f2f3ed5 100644
--- a/src/Specific/solinas32_2e512m491x2e496m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e512m491x2e496m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e512m569/CurveParameters.v b/src/Specific/solinas32_2e512m569/CurveParameters.v
index 4753c1271..e97a2dd47 100644
--- a/src/Specific/solinas32_2e512m569/CurveParameters.v
+++ b/src/Specific/solinas32_2e512m569/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas32_2e521m1/CurveParameters.v b/src/Specific/solinas32_2e521m1/CurveParameters.v
index 998d3b5a3..14fb480f7 100644
--- a/src/Specific/solinas32_2e521m1/CurveParameters.v
+++ b/src/Specific/solinas32_2e521m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e127m1/CurveParameters.v b/src/Specific/solinas64_2e127m1/CurveParameters.v
index b924f87ee..3cbb46ff2 100644
--- a/src/Specific/solinas64_2e127m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e127m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e129m25/CurveParameters.v b/src/Specific/solinas64_2e129m25/CurveParameters.v
index 96fd81053..df897a547 100644
--- a/src/Specific/solinas64_2e129m25/CurveParameters.v
+++ b/src/Specific/solinas64_2e129m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e130m5/CurveParameters.v b/src/Specific/solinas64_2e130m5/CurveParameters.v
index 7a5249950..16175f52a 100644
--- a/src/Specific/solinas64_2e130m5/CurveParameters.v
+++ b/src/Specific/solinas64_2e130m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e137m13/CurveParameters.v b/src/Specific/solinas64_2e137m13/CurveParameters.v
index 4f1115fad..e8e42dabb 100644
--- a/src/Specific/solinas64_2e137m13/CurveParameters.v
+++ b/src/Specific/solinas64_2e137m13/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e140m27/CurveParameters.v b/src/Specific/solinas64_2e140m27/CurveParameters.v
index 94213885b..8b2d58b07 100644
--- a/src/Specific/solinas64_2e140m27/CurveParameters.v
+++ b/src/Specific/solinas64_2e140m27/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e141m9/CurveParameters.v b/src/Specific/solinas64_2e141m9/CurveParameters.v
index d83903c89..0ad50a39e 100644
--- a/src/Specific/solinas64_2e141m9/CurveParameters.v
+++ b/src/Specific/solinas64_2e141m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e150m3/CurveParameters.v b/src/Specific/solinas64_2e150m3/CurveParameters.v
index bf35f1164..e451620f4 100644
--- a/src/Specific/solinas64_2e150m3/CurveParameters.v
+++ b/src/Specific/solinas64_2e150m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e150m5/CurveParameters.v b/src/Specific/solinas64_2e150m5/CurveParameters.v
index 718dbb762..598e97b48 100644
--- a/src/Specific/solinas64_2e150m5/CurveParameters.v
+++ b/src/Specific/solinas64_2e150m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e152m17/CurveParameters.v b/src/Specific/solinas64_2e152m17/CurveParameters.v
index 2d7cd9ea1..e17acd9de 100644
--- a/src/Specific/solinas64_2e152m17/CurveParameters.v
+++ b/src/Specific/solinas64_2e152m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e158m15/CurveParameters.v b/src/Specific/solinas64_2e158m15/CurveParameters.v
index 7016fa94e..87d0e02c0 100644
--- a/src/Specific/solinas64_2e158m15/CurveParameters.v
+++ b/src/Specific/solinas64_2e158m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e165m25/CurveParameters.v b/src/Specific/solinas64_2e165m25/CurveParameters.v
index 25d170524..bbdb16a2c 100644
--- a/src/Specific/solinas64_2e165m25/CurveParameters.v
+++ b/src/Specific/solinas64_2e165m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e166m5/CurveParameters.v b/src/Specific/solinas64_2e166m5/CurveParameters.v
index 7672318f0..ef48bf342 100644
--- a/src/Specific/solinas64_2e166m5/CurveParameters.v
+++ b/src/Specific/solinas64_2e166m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e171m19/CurveParameters.v b/src/Specific/solinas64_2e171m19/CurveParameters.v
index 9c8f78cbb..ff1df7e1c 100644
--- a/src/Specific/solinas64_2e171m19/CurveParameters.v
+++ b/src/Specific/solinas64_2e171m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e174m17/CurveParameters.v b/src/Specific/solinas64_2e174m17/CurveParameters.v
index cccbe28d9..69603408a 100644
--- a/src/Specific/solinas64_2e174m17/CurveParameters.v
+++ b/src/Specific/solinas64_2e174m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e174m3/CurveParameters.v b/src/Specific/solinas64_2e174m3/CurveParameters.v
index ef1b83ba0..f09389f59 100644
--- a/src/Specific/solinas64_2e174m3/CurveParameters.v
+++ b/src/Specific/solinas64_2e174m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e189m25/CurveParameters.v b/src/Specific/solinas64_2e189m25/CurveParameters.v
index d36fff1d8..a009d1f50 100644
--- a/src/Specific/solinas64_2e189m25/CurveParameters.v
+++ b/src/Specific/solinas64_2e189m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e190m11/CurveParameters.v b/src/Specific/solinas64_2e190m11/CurveParameters.v
index da8101a3f..75a2918dd 100644
--- a/src/Specific/solinas64_2e190m11/CurveParameters.v
+++ b/src/Specific/solinas64_2e190m11/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e191m19/CurveParameters.v b/src/Specific/solinas64_2e191m19/CurveParameters.v
index de1dfbf8b..514a5a09c 100644
--- a/src/Specific/solinas64_2e191m19/CurveParameters.v
+++ b/src/Specific/solinas64_2e191m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e192m2e64m1/CurveParameters.v b/src/Specific/solinas64_2e192m2e64m1/CurveParameters.v
index 0b605eea5..f44b5be97 100644
--- a/src/Specific/solinas64_2e192m2e64m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e192m2e64m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e194m33/CurveParameters.v b/src/Specific/solinas64_2e194m33/CurveParameters.v
index 145f8cfa3..905a67b54 100644
--- a/src/Specific/solinas64_2e194m33/CurveParameters.v
+++ b/src/Specific/solinas64_2e194m33/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e196m15/CurveParameters.v b/src/Specific/solinas64_2e196m15/CurveParameters.v
index 1d3245ba0..ebcf4a84e 100644
--- a/src/Specific/solinas64_2e196m15/CurveParameters.v
+++ b/src/Specific/solinas64_2e196m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e198m17/CurveParameters.v b/src/Specific/solinas64_2e198m17/CurveParameters.v
index ae38f6968..cb3a65318 100644
--- a/src/Specific/solinas64_2e198m17/CurveParameters.v
+++ b/src/Specific/solinas64_2e198m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e205m45x2e198m1/CurveParameters.v b/src/Specific/solinas64_2e205m45x2e198m1/CurveParameters.v
index fc06a06c9..2d6935360 100644
--- a/src/Specific/solinas64_2e205m45x2e198m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e205m45x2e198m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e206m5/CurveParameters.v b/src/Specific/solinas64_2e206m5/CurveParameters.v
index c722b983b..185e3afb6 100644
--- a/src/Specific/solinas64_2e206m5/CurveParameters.v
+++ b/src/Specific/solinas64_2e206m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e212m29/CurveParameters.v b/src/Specific/solinas64_2e212m29/CurveParameters.v
index 87ab43407..26435ae90 100644
--- a/src/Specific/solinas64_2e212m29/CurveParameters.v
+++ b/src/Specific/solinas64_2e212m29/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e213m3/CurveParameters.v b/src/Specific/solinas64_2e213m3/CurveParameters.v
index 8022eb3ed..7b8111f00 100644
--- a/src/Specific/solinas64_2e213m3/CurveParameters.v
+++ b/src/Specific/solinas64_2e213m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e216m2e108m1/CurveParameters.v b/src/Specific/solinas64_2e216m2e108m1/CurveParameters.v
index 9bd95fba4..e60d40411 100644
--- a/src/Specific/solinas64_2e216m2e108m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e216m2e108m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e221m3/CurveParameters.v b/src/Specific/solinas64_2e221m3/CurveParameters.v
index fa880e875..b6c3b8c1a 100644
--- a/src/Specific/solinas64_2e221m3/CurveParameters.v
+++ b/src/Specific/solinas64_2e221m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e222m117/CurveParameters.v b/src/Specific/solinas64_2e222m117/CurveParameters.v
index 52d07cc8e..2781a543c 100644
--- a/src/Specific/solinas64_2e222m117/CurveParameters.v
+++ b/src/Specific/solinas64_2e222m117/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e224m2e96p1/CurveParameters.v b/src/Specific/solinas64_2e224m2e96p1/CurveParameters.v
index 876e04190..32bf066b1 100644
--- a/src/Specific/solinas64_2e224m2e96p1/CurveParameters.v
+++ b/src/Specific/solinas64_2e224m2e96p1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e226m5/CurveParameters.v b/src/Specific/solinas64_2e226m5/CurveParameters.v
index 07474bfa5..b7d00c001 100644
--- a/src/Specific/solinas64_2e226m5/CurveParameters.v
+++ b/src/Specific/solinas64_2e226m5/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e230m27/CurveParameters.v b/src/Specific/solinas64_2e230m27/CurveParameters.v
index 881ad3371..c6ea3202b 100644
--- a/src/Specific/solinas64_2e230m27/CurveParameters.v
+++ b/src/Specific/solinas64_2e230m27/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e235m15/CurveParameters.v b/src/Specific/solinas64_2e235m15/CurveParameters.v
index 782c518d0..80a94df58 100644
--- a/src/Specific/solinas64_2e235m15/CurveParameters.v
+++ b/src/Specific/solinas64_2e235m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e243m9/CurveParameters.v b/src/Specific/solinas64_2e243m9/CurveParameters.v
index f82527cda..60427d462 100644
--- a/src/Specific/solinas64_2e243m9/CurveParameters.v
+++ b/src/Specific/solinas64_2e243m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e251m9/CurveParameters.v b/src/Specific/solinas64_2e251m9/CurveParameters.v
index 0a70c2d9c..5a6c7841a 100644
--- a/src/Specific/solinas64_2e251m9/CurveParameters.v
+++ b/src/Specific/solinas64_2e251m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e254m127x2e240m1/CurveParameters.v b/src/Specific/solinas64_2e254m127x2e240m1/CurveParameters.v
index c3d5cadb3..d6432aa60 100644
--- a/src/Specific/solinas64_2e254m127x2e240m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e254m127x2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e255m19/CurveParameters.v b/src/Specific/solinas64_2e255m19/CurveParameters.v
index 2247cf21c..652d9dce7 100644
--- a/src/Specific/solinas64_2e255m19/CurveParameters.v
+++ b/src/Specific/solinas64_2e255m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e255m2e4m2e1m1/CurveParameters.v b/src/Specific/solinas64_2e255m2e4m2e1m1/CurveParameters.v
index 9fc910069..97af18cea 100644
--- a/src/Specific/solinas64_2e255m2e4m2e1m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e255m2e4m2e1m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e255m765/CurveParameters.v b/src/Specific/solinas64_2e255m765/CurveParameters.v
index b539bfcba..39be5d174 100644
--- a/src/Specific/solinas64_2e255m765/CurveParameters.v
+++ b/src/Specific/solinas64_2e255m765/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e256m189/CurveParameters.v b/src/Specific/solinas64_2e256m189/CurveParameters.v
index 3faf572c1..86d4cd268 100644
--- a/src/Specific/solinas64_2e256m189/CurveParameters.v
+++ b/src/Specific/solinas64_2e256m189/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1/CurveParameters.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1/CurveParameters.v
index 8246add65..36bcac59d 100644
--- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e256m2e32m977/CurveParameters.v b/src/Specific/solinas64_2e256m2e32m977/CurveParameters.v
index a1fc58c39..435eb4061 100644
--- a/src/Specific/solinas64_2e256m2e32m977/CurveParameters.v
+++ b/src/Specific/solinas64_2e256m2e32m977/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e256m88x2e240m1/CurveParameters.v b/src/Specific/solinas64_2e256m88x2e240m1/CurveParameters.v
index 1679a5878..0667ab22e 100644
--- a/src/Specific/solinas64_2e256m88x2e240m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e256m88x2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e266m3/CurveParameters.v b/src/Specific/solinas64_2e266m3/CurveParameters.v
index c6a6d6f0f..1aa25a425 100644
--- a/src/Specific/solinas64_2e266m3/CurveParameters.v
+++ b/src/Specific/solinas64_2e266m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e285m9/CurveParameters.v b/src/Specific/solinas64_2e285m9/CurveParameters.v
index 983ba5c44..938d4c035 100644
--- a/src/Specific/solinas64_2e285m9/CurveParameters.v
+++ b/src/Specific/solinas64_2e285m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e291m19/CurveParameters.v b/src/Specific/solinas64_2e291m19/CurveParameters.v
index ce2892f3c..3f580fdc6 100644
--- a/src/Specific/solinas64_2e291m19/CurveParameters.v
+++ b/src/Specific/solinas64_2e291m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e321m9/CurveParameters.v b/src/Specific/solinas64_2e321m9/CurveParameters.v
index 237d94057..4b7c0edf8 100644
--- a/src/Specific/solinas64_2e321m9/CurveParameters.v
+++ b/src/Specific/solinas64_2e321m9/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e322m2e161m1/CurveParameters.v b/src/Specific/solinas64_2e322m2e161m1/CurveParameters.v
index 53426dc32..3df995a12 100644
--- a/src/Specific/solinas64_2e322m2e161m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e322m2e161m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e336m17/CurveParameters.v b/src/Specific/solinas64_2e336m17/CurveParameters.v
index bfc39f125..24cdbb10b 100644
--- a/src/Specific/solinas64_2e336m17/CurveParameters.v
+++ b/src/Specific/solinas64_2e336m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e336m3/CurveParameters.v b/src/Specific/solinas64_2e336m3/CurveParameters.v
index d96a4df65..a0361f045 100644
--- a/src/Specific/solinas64_2e336m3/CurveParameters.v
+++ b/src/Specific/solinas64_2e336m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e338m15/CurveParameters.v b/src/Specific/solinas64_2e338m15/CurveParameters.v
index 51da3f012..ddc66d0bc 100644
--- a/src/Specific/solinas64_2e338m15/CurveParameters.v
+++ b/src/Specific/solinas64_2e338m15/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e369m25/CurveParameters.v b/src/Specific/solinas64_2e369m25/CurveParameters.v
index e9bdceb4f..f44d54162 100644
--- a/src/Specific/solinas64_2e369m25/CurveParameters.v
+++ b/src/Specific/solinas64_2e369m25/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e379m19/CurveParameters.v b/src/Specific/solinas64_2e379m19/CurveParameters.v
index 328340177..b7b223fa9 100644
--- a/src/Specific/solinas64_2e379m19/CurveParameters.v
+++ b/src/Specific/solinas64_2e379m19/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e382m105/CurveParameters.v b/src/Specific/solinas64_2e382m105/CurveParameters.v
index 556c60ca5..be7f65910 100644
--- a/src/Specific/solinas64_2e382m105/CurveParameters.v
+++ b/src/Specific/solinas64_2e382m105/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e384m2e128m2e96p2e32m1/CurveParameters.v b/src/Specific/solinas64_2e384m2e128m2e96p2e32m1/CurveParameters.v
index ff2491005..d32f419fd 100644
--- a/src/Specific/solinas64_2e384m2e128m2e96p2e32m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e384m2e128m2e96p2e32m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e384m317/CurveParameters.v b/src/Specific/solinas64_2e384m317/CurveParameters.v
index 98c11d04c..5378ea206 100644
--- a/src/Specific/solinas64_2e384m317/CurveParameters.v
+++ b/src/Specific/solinas64_2e384m317/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e384m5x2e368m1/CurveParameters.v b/src/Specific/solinas64_2e384m5x2e368m1/CurveParameters.v
index 464bdd196..e3713eb11 100644
--- a/src/Specific/solinas64_2e384m5x2e368m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e384m5x2e368m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e384m79x2e376m1/CurveParameters.v b/src/Specific/solinas64_2e384m79x2e376m1/CurveParameters.v
index aa9062b2b..bb124cd64 100644
--- a/src/Specific/solinas64_2e384m79x2e376m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e384m79x2e376m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e401m31/CurveParameters.v b/src/Specific/solinas64_2e401m31/CurveParameters.v
index bd98620a8..0d6d08d4c 100644
--- a/src/Specific/solinas64_2e401m31/CurveParameters.v
+++ b/src/Specific/solinas64_2e401m31/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e413m21/CurveParameters.v b/src/Specific/solinas64_2e413m21/CurveParameters.v
index d383b4fa8..a438267f2 100644
--- a/src/Specific/solinas64_2e413m21/CurveParameters.v
+++ b/src/Specific/solinas64_2e413m21/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e414m17/CurveParameters.v b/src/Specific/solinas64_2e414m17/CurveParameters.v
index d06e02006..0567d0263 100644
--- a/src/Specific/solinas64_2e414m17/CurveParameters.v
+++ b/src/Specific/solinas64_2e414m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e416m2e208m1/CurveParameters.v b/src/Specific/solinas64_2e416m2e208m1/CurveParameters.v
index b7c68efb5..d8528c1df 100644
--- a/src/Specific/solinas64_2e416m2e208m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e416m2e208m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e444m17/CurveParameters.v b/src/Specific/solinas64_2e444m17/CurveParameters.v
index df67731b8..3b463bfb8 100644
--- a/src/Specific/solinas64_2e444m17/CurveParameters.v
+++ b/src/Specific/solinas64_2e444m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e448m2e224m1/CurveParameters.v b/src/Specific/solinas64_2e448m2e224m1/CurveParameters.v
index 1ef3be55f..4c48e54cc 100644
--- a/src/Specific/solinas64_2e448m2e224m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e448m2e224m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e450m2e225m1/CurveParameters.v b/src/Specific/solinas64_2e450m2e225m1/CurveParameters.v
index 079a6f996..e251b6d9f 100644
--- a/src/Specific/solinas64_2e450m2e225m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e450m2e225m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e452m3/CurveParameters.v b/src/Specific/solinas64_2e452m3/CurveParameters.v
index 1101199b0..e51728504 100644
--- a/src/Specific/solinas64_2e452m3/CurveParameters.v
+++ b/src/Specific/solinas64_2e452m3/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e468m17/CurveParameters.v b/src/Specific/solinas64_2e468m17/CurveParameters.v
index f2c5524a6..0ed707400 100644
--- a/src/Specific/solinas64_2e468m17/CurveParameters.v
+++ b/src/Specific/solinas64_2e468m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e480m2e240m1/CurveParameters.v b/src/Specific/solinas64_2e480m2e240m1/CurveParameters.v
index 20644d974..e4fd7f1e8 100644
--- a/src/Specific/solinas64_2e480m2e240m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e480m2e240m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := Some true;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e488m17/CurveParameters.v b/src/Specific/solinas64_2e488m17/CurveParameters.v
index 11dabfb7a..1bb8100c7 100644
--- a/src/Specific/solinas64_2e488m17/CurveParameters.v
+++ b/src/Specific/solinas64_2e488m17/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e489m21/CurveParameters.v b/src/Specific/solinas64_2e489m21/CurveParameters.v
index 3332babb3..31010d631 100644
--- a/src/Specific/solinas64_2e489m21/CurveParameters.v
+++ b/src/Specific/solinas64_2e489m21/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e495m31/CurveParameters.v b/src/Specific/solinas64_2e495m31/CurveParameters.v
index 19ff6e419..57b353b9f 100644
--- a/src/Specific/solinas64_2e495m31/CurveParameters.v
+++ b/src/Specific/solinas64_2e495m31/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e510m290x2e496m1/CurveParameters.v b/src/Specific/solinas64_2e510m290x2e496m1/CurveParameters.v
index b5322d6a5..551628047 100644
--- a/src/Specific/solinas64_2e510m290x2e496m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e510m290x2e496m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e511m187/CurveParameters.v b/src/Specific/solinas64_2e511m187/CurveParameters.v
index 95ed58cf9..edae92ba4 100644
--- a/src/Specific/solinas64_2e511m187/CurveParameters.v
+++ b/src/Specific/solinas64_2e511m187/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e511m481/CurveParameters.v b/src/Specific/solinas64_2e511m481/CurveParameters.v
index 3980e7c06..5bdb984cf 100644
--- a/src/Specific/solinas64_2e511m481/CurveParameters.v
+++ b/src/Specific/solinas64_2e511m481/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e512m491x2e496m1/CurveParameters.v b/src/Specific/solinas64_2e512m491x2e496m1/CurveParameters.v
index 3c85a70eb..eaf5cb704 100644
--- a/src/Specific/solinas64_2e512m491x2e496m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e512m491x2e496m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e512m569/CurveParameters.v b/src/Specific/solinas64_2e512m569/CurveParameters.v
index 47256506f..13d176bc4 100644
--- a/src/Specific/solinas64_2e512m569/CurveParameters.v
+++ b/src/Specific/solinas64_2e512m569/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
diff --git a/src/Specific/solinas64_2e521m1/CurveParameters.v b/src/Specific/solinas64_2e521m1/CurveParameters.v
index be045a15d..5d7dabf27 100644
--- a/src/Specific/solinas64_2e521m1/CurveParameters.v
+++ b/src/Specific/solinas64_2e521m1/CurveParameters.v
@@ -19,6 +19,7 @@ Definition curve : CurveParameters :=
     coef_div_modulus := Some 2%nat;
 
     goldilocks := None;
+    karatsuba := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;