Explicitly specify base

This allows it to be something other than log2(m)/sz.

After    | File Name                                                | Before   || Change
-------------------------------------------------------------------------------------------
8m20.82s | Total                                                    | 8m37.82s || -0m17.00s
-------------------------------------------------------------------------------------------
1m59.42s | Specific/NISTP256/AMD64/femul                            | 2m19.09s || -0m19.67s
3m28.66s | Specific/X25519/C64/ladderstep                           | 3m28.02s || +0m00.63s
0m24.97s | Specific/X25519/C64/femul                                | 0m24.60s || +0m00.36s
0m24.08s | Specific/NISTP256/AMD64/fesub                            | 0m23.48s || +0m00.59s
0m22.00s | Specific/NISTP256/AMD64/feadd                            | 0m21.34s || +0m00.66s
0m20.34s | Specific/X25519/C64/freeze                               | 0m19.76s || +0m00.57s
0m19.85s | Specific/X25519/C64/fesquare                             | 0m19.93s || -0m00.07s
0m18.04s | Specific/NISTP256/AMD64/feopp                            | 0m17.69s || +0m00.34s
0m15.10s | Specific/NISTP256/AMD64/fenz                             | 0m15.37s || -0m00.26s
0m08.31s | Specific/NISTP256/AMD64/Synthesis                        | 0m08.24s || +0m00.07s
0m05.96s | Specific/X25519/C64/Synthesis                            | 0m06.25s || -0m00.29s
0m02.10s | Specific/Framework/ArithmeticSynthesis/Defaults          | 0m02.14s || -0m00.04s
0m01.00s | Specific/Framework/SynthesisFramework                    | 0m01.03s || -0m00.03s
0m00.97s | Specific/Framework/ArithmeticSynthesis/Base              | 0m01.02s || -0m00.05s
0m00.89s | Specific/Framework/ArithmeticSynthesis/Freeze            | 0m00.84s || +0m00.05s
0m00.80s | Specific/Framework/ArithmeticSynthesis/Karatsuba         | 0m00.81s || -0m00.01s
0m00.79s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.80s || -0m00.01s
0m00.76s | Specific/Framework/MontgomeryReificationTypesPackage     | 0m00.75s || +0m00.01s
0m00.74s | Specific/Framework/ReificationTypesPackage               | 0m00.77s || -0m00.03s
0m00.74s | Specific/Framework/ArithmeticSynthesis/BasePackage       | 0m00.74s || +0m00.00s
0m00.73s | Specific/Framework/ArithmeticSynthesis/SquareFromMul     | 0m00.70s || +0m00.03s
0m00.72s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage   | 0m00.68s || +0m00.03s
0m00.70s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.72s || -0m00.02s
0m00.70s | Specific/Framework/ArithmeticSynthesis/FreezePackage     | 0m00.77s || -0m00.07s
0m00.69s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage  | 0m00.70s || -0m00.01s
0m00.42s | Specific/X25519/C64/CurveParameters                      | 0m00.38s || +0m00.03s
0m00.36s | Specific/Framework/CurveParameters                       | 0m00.32s || +0m00.03s
0m00.33s | Specific/Framework/RawCurveParameters                    | 0m00.29s || +0m00.04s
0m00.33s | Specific/Framework/CurveParametersPackage                | 0m00.30s || +0m00.03s
0m00.32s | Specific/NISTP256/AMD64/CurveParameters                  | 0m00.30s || +0m00.02s

1 files changed, 23 insertions, 12 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
index d5b4e567c..80e032fb8 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
@@ -5,7 +5,7 @@ Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Util.TagList.
 
 Module TAG.
-  Inductive tags := r | m | wt | sz2 | half_sz | half_sz_nonzero | s_nonzero | sz_le_log2_m | m_correct | m_enc | coef | coef_mod | sz_nonzero | wt_nonzero | wt_nonneg | wt_divides | wt_divides' | wt_divides_chains | wt_pos | wt_multiples | c_small | m_enc_bounded | m_correct_wt.
+  Inductive tags := r | m | wt | sz2 | half_sz | half_sz_nonzero | s_nonzero | sz_le_log2_m | base_pos | m_correct | m_enc | coef | coef_mod | sz_nonzero | wt_nonzero | wt_nonneg | wt_divides | wt_divides' | wt_divides_chains | wt_pos | wt_multiples | c_small | m_enc_bounded | m_correct_wt.
 End TAG.
 
 Ltac add_r pkg :=
@@ -22,10 +22,9 @@ Ltac add_m pkg :=
   Tag.update pkg TAG.m m.
 
 Ltac add_wt pkg :=
-  let m := Tag.get pkg TAG.m in
-  let sz := Tag.get pkg TAG.sz in
+  let base := Tag.get pkg TAG.base in
   let wt := fresh "wt" in
-  let wt := pose_wt m sz wt in
+  let wt := pose_wt base wt in
   Tag.update pkg TAG.wt wt.
 
 Ltac add_sz2 pkg :=
@@ -59,6 +58,12 @@ Ltac add_sz_le_log2_m pkg :=
   let sz_le_log2_m := pose_sz_le_log2_m sz m sz_le_log2_m in
   Tag.update pkg TAG.sz_le_log2_m sz_le_log2_m.
 
+Ltac add_base_pos pkg :=
+  let base := Tag.get pkg TAG.base in
+  let base_pos := fresh "base_pos" in
+  let base_pos := pose_base_pos base base_pos in
+  Tag.update pkg TAG.base_pos base_pos.
+
 Ltac add_m_correct pkg :=
   let m := Tag.get pkg TAG.m in
   let s := Tag.get pkg TAG.s in
@@ -68,29 +73,32 @@ Ltac add_m_correct pkg :=
   Tag.update pkg TAG.m_correct m_correct.
 
 Ltac add_m_enc pkg :=
-  let sz := Tag.get pkg TAG.sz in
+  let base := Tag.get pkg TAG.base in
   let m := Tag.get pkg TAG.m in
+  let sz := Tag.get pkg TAG.sz in
   let m_enc := fresh "m_enc" in
-  let m_enc := pose_m_enc sz m m_enc in
+  let m_enc := pose_m_enc base m sz m_enc in
   Tag.update pkg TAG.m_enc m_enc.
 
 Ltac add_coef pkg :=
-  let sz := Tag.get pkg TAG.sz in
+  let base := Tag.get pkg TAG.base in
   let m := Tag.get pkg TAG.m in
+  let sz := Tag.get pkg TAG.sz in
   let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in
   let coef := fresh "coef" in
-  let coef := pose_coef sz m coef_div_modulus coef in
+  let coef := pose_coef base m sz coef_div_modulus coef in
   Tag.update pkg TAG.coef coef.
 
 Ltac add_coef_mod pkg :=
-  let sz := Tag.get pkg TAG.sz in
   let wt := Tag.get pkg TAG.wt in
-  let m := Tag.get pkg TAG.m in
   let coef := Tag.get pkg TAG.coef in
+  let base := Tag.get pkg TAG.base in
+  let m := Tag.get pkg TAG.m in
+  let sz := Tag.get pkg TAG.sz in
   let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in
-  let sz_le_log2_m := Tag.get pkg TAG.sz_le_log2_m in
+  let base_pos := Tag.get pkg TAG.base_pos in
   let coef_mod := fresh "coef_mod" in
-  let coef_mod := pose_coef_mod sz wt m coef coef_div_modulus sz_le_log2_m coef_mod in
+  let coef_mod := pose_coef_mod wt coef base m sz coef_div_modulus base_pos coef_mod in
   Tag.update pkg TAG.coef_mod coef_mod.
 
 Ltac add_sz_nonzero pkg :=
@@ -177,6 +185,7 @@ Ltac add_Base_package pkg :=
   let pkg := add_half_sz_nonzero pkg in
   let pkg := add_s_nonzero pkg in
   let pkg := add_sz_le_log2_m pkg in
+  let pkg := add_base_pos pkg in
   let pkg := add_m_correct pkg in
   let pkg := add_m_enc pkg in
   let pkg := add_coef pkg in
@@ -214,6 +223,8 @@ Module MakeBasePackage (PKG : PrePackage).
   Notation s_nonzero := (ltac:(let v := get_s_nonzero () in exact v)) (only parsing).
   Ltac get_sz_le_log2_m _ := get TAG.sz_le_log2_m.
   Notation sz_le_log2_m := (ltac:(let v := get_sz_le_log2_m () in exact v)) (only parsing).
+  Ltac get_base_pos _ := get TAG.base_pos.
+  Notation base_pos := (ltac:(let v := get_base_pos () in exact v)) (only parsing).
   Ltac get_m_correct _ := get TAG.m_correct.
   Notation m_correct := (ltac:(let v := get_m_correct () in exact v)) (only parsing).
   Ltac get_m_enc _ := get TAG.m_enc.