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).

5 files changed, 33 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;