Move coef, coef_mod to gallina

Also pose mul_code, square_code

After    | File Name                                                | Before   || Change
-------------------------------------------------------------------------------------------
4m28.75s | Total                                                    | 4m31.79s || -0m03.03s
-------------------------------------------------------------------------------------------
1m57.67s | Specific/NISTP256/AMD64/femul                            | 2m00.16s || -0m02.48s
0m23.68s | Specific/NISTP256/AMD64/fesub                            | 0m23.69s || -0m00.01s
0m21.58s | Specific/NISTP256/AMD64/feadd                            | 0m21.76s || -0m00.18s
0m20.13s | Specific/X25519/C64/freeze                               | 0m19.99s || +0m00.14s
0m17.60s | Specific/NISTP256/AMD64/feopp                            | 0m17.82s || -0m00.21s
0m15.23s | Specific/NISTP256/AMD64/fenz                             | 0m15.24s || -0m00.00s
0m11.79s | Specific/X25519/C64/Synthesis                            | 0m11.98s || -0m00.19s
0m09.47s | Specific/NISTP256/AMD64/Synthesis                        | 0m09.57s || -0m00.09s
0m04.95s | Specific/X25519/C64/ladderstep                           | 0m04.96s || -0m00.00s
0m02.59s | Specific/NISTP256/AMD64/femulDisplay                     | 0m02.61s || -0m00.02s
0m02.33s | Specific/X25519/C64/femul                                | 0m02.26s || +0m00.07s
0m01.87s | Specific/NISTP256/AMD64/feaddDisplay                     | 0m01.88s || -0m00.00s
0m01.81s | Specific/NISTP256/AMD64/fesubDisplay                     | 0m01.80s || +0m00.01s
0m01.78s | Specific/X25519/C64/fesquare                             | 0m01.81s || -0m00.03s
0m01.66s | Specific/NISTP256/AMD64/feoppDisplay                     | 0m01.66s || +0m00.00s
0m01.48s | Specific/NISTP256/AMD64/fenzDisplay                      | 0m01.46s || +0m00.02s
0m01.46s | Specific/X25519/C64/freezeDisplay                        | 0m01.45s || +0m00.01s
0m01.07s | Specific/Framework/ArithmeticSynthesis/Defaults          | 0m01.14s || -0m00.06s
0m01.03s | Specific/Framework/ArithmeticSynthesis/Base              | 0m00.87s || +0m00.16s
0m00.99s | Specific/Framework/SynthesisFramework                    | 0m01.04s || -0m00.05s
0m00.80s | Specific/Framework/MontgomeryReificationTypesPackage     | 0m00.75s || +0m00.05s
0m00.77s | Specific/Framework/ReificationTypesPackage               | 0m00.76s || +0m00.01s
0m00.75s | Specific/Framework/ArithmeticSynthesis/Karatsuba         | 0m00.76s || -0m00.01s
0m00.74s | Specific/Framework/ArithmeticSynthesis/Freeze            | 0m00.75s || -0m00.01s
0m00.72s | Specific/Framework/ArithmeticSynthesis/FreezePackage     | 0m00.74s || -0m00.02s
0m00.72s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.77s || -0m00.05s
0m00.71s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage   | 0m00.68s || +0m00.02s
0m00.71s | Specific/Framework/ArithmeticSynthesis/BasePackage       | 0m00.71s || +0m00.00s
0m00.70s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.74s || -0m00.04s
0m00.69s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage  | 0m00.67s || +0m00.01s
0m00.69s | Specific/Framework/ArithmeticSynthesis/SquareFromMul     | 0m00.70s || -0m00.01s
0m00.32s | Specific/Framework/CurveParametersPackage                | 0m00.32s || +0m00.00s
0m00.27s | Specific/Framework/CurveParameters                       | 0m00.30s || -0m00.02s

4 files changed, 128 insertions, 66 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/Base.v b/src/Specific/Framework/ArithmeticSynthesis/Base.v
index 7c80b238d..81aff8dea 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Base.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Base.v
@@ -5,6 +5,7 @@ Require Import Crypto.Specific.Framework.CurveParameters.
 Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics.
 Require Import Crypto.Util.QUtil.
 Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.CacheTerm.
 
@@ -31,68 +32,21 @@ Section wt.
   Local Coercion Z.pos : positive >-> Z.
   Definition wt_gen (m : positive) (sz : nat) (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i).
 End wt.
-Ltac pose_wt m sz wt :=
-  let v := (eval cbv [wt_gen] in (wt_gen m sz)) in
-  cache_term v wt.
-
-Ltac pose_sz2 sz sz2 :=
-  let v := (eval vm_compute in ((sz * 2) - 1)%nat) in
-  cache_term v sz2.
 
-Ltac pose_half_sz sz half_sz :=
-  let v := (eval compute in (sz / 2)%nat) in
-  cache_term v half_sz.
+Section gen.
+  Context (m : positive)
+          (sz : nat)
+          (coef_div_modulus : nat).
 
-Ltac pose_half_sz_nonzero half_sz half_sz_nonzero :=
-  cache_proof_with_type_by
-    (half_sz <> 0%nat)
-    ltac:(cbv; congruence)
-           half_sz_nonzero.
-
-Ltac pose_s_nonzero s s_nonzero :=
-  cache_proof_with_type_by
-    (s <> 0)
-    ltac:(vm_decide_no_check)
-           s_nonzero.
+  Local Notation wt := (wt_gen m sz).
 
-Ltac pose_sz_le_log2_m sz m sz_le_log2_m :=
-  cache_proof_with_type_by
-    (Z.of_nat sz <= Z.log2_up (Z.pos m))
-    ltac:(vm_decide_no_check)
-           sz_le_log2_m.
+  Definition sz2' := ((sz * 2) - 1)%nat.
 
-Ltac pose_m_correct m s c m_correct :=
-  cache_proof_with_type_by
-    (Z.pos m = s - Associational.eval c)
-    ltac:(vm_decide_no_check)
-           m_correct.
+  Definition half_sz' := (sz / 2)%nat.
 
-Ltac pose_m_enc sz s c wt m_enc :=
-  let v := (eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c))) in
-  let v := (eval compute in v) in (* compute away the type arguments *)
-  cache_term v m_enc.
-Ltac pose_coef sz wt m_enc coef_div_modulus coef := (* subtraction coefficient *)
-  let v := (eval vm_compute in
-               ((fix addm (acc: Z^sz) (ctr : nat) : Z^sz :=
-                   match ctr with
-                   | O => acc
-                   | S n => addm (Positional.add_cps wt acc m_enc id) n
-                   end) (Positional.zeros sz) coef_div_modulus)) in
-  cache_term v coef.
+  Definition m_enc'
+    := Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (Z.pos m).
 
-Ltac pose_coef_mod sz wt m coef coef_mod :=
-  cache_term_with_type_by
-    (mod_eq m (Positional.eval (n:=sz) wt coef) 0)
-    ltac:(exact eq_refl)
-           coef_mod.
-Ltac pose_sz_nonzero sz sz_nonzero :=
-  cache_proof_with_type_by
-    (sz <> 0%nat)
-    ltac:(vm_decide_no_check)
-           sz_nonzero.
-Section wt_gen.
-  Context (m : positive) (sz : nat).
-  Local Notation wt := (wt_gen m sz).
   Local Ltac Q_cbv :=
     cbv [wt_gen Qround.Qceiling QArith_base.Qmult QArith_base.Qdiv QArith_base.inject_Z QArith_base.Qden QArith_base.Qnum QArith_base.Qopp Qround.Qfloor QArith_base.Qinv QArith_base.Qle Z.of_nat].
   Lemma wt_gen0_1 : wt 0 = 1.
@@ -169,8 +123,95 @@ Section wt_gen.
         constructor; eauto using wt_gen_divides_chain.
     Qed.
   End divides.
-End wt_gen.
 
+  Definition coef'
+    := (fix addm (acc: Z^sz) (ctr : nat) : Z^sz :=
+          match ctr with
+          | O => acc
+          | S n => addm (Positional.add_cps wt acc m_enc' id) n
+          end) (Positional.zeros sz) coef_div_modulus.
+
+  Lemma coef_mod'
+        (sz_le_log2_m : Z.of_nat sz <= Z.log2_up (Z.pos m))
+    : mod_eq m (Positional.eval (n:=sz) wt coef') 0.
+  Proof.
+    cbv [coef' m_enc'].
+    remember (Positional.zeros sz) as v eqn:Hv.
+    assert (Hv' : mod_eq m (Positional.eval wt v) 0)
+      by (subst v; autorewrite with push_basesystem_eval; reflexivity);
+      clear Hv.
+    revert dependent v.
+    induction coef_div_modulus as [|n IHn]; clear coef_div_modulus;
+      intros; [ assumption | ].
+    rewrite IHn; [ reflexivity | ].
+    pose proof wt_gen0_1.
+    pose proof wt_gen_nonzero.
+    pose proof div_mod.
+    pose proof wt_gen_divides'.
+    destruct (Nat.eq_dec sz 0).
+    { subst; reflexivity. }
+    { repeat autounfold; autorewrite with uncps push_id push_basesystem_eval.
+      rewrite Positional.eval_encode by auto.
+      cbv [mod_eq] in *.
+      push_Zmod; rewrite Hv'; pull_Zmod.
+      reflexivity. }
+  Qed.
+End gen.
+
+Ltac pose_wt m sz wt :=
+  let v := (eval cbv [wt_gen] in (wt_gen m sz)) in
+  cache_term v wt.
+
+Ltac pose_sz2 sz sz2 :=
+  let v := (eval vm_compute in (sz2' sz)) in
+  cache_term v sz2.
+
+Ltac pose_half_sz sz half_sz :=
+  let v := (eval compute in (half_sz' sz)) in
+  cache_term v half_sz.
+
+Ltac pose_half_sz_nonzero half_sz half_sz_nonzero :=
+  cache_proof_with_type_by
+    (half_sz <> 0%nat)
+    ltac:(cbv; congruence)
+           half_sz_nonzero.
+
+Ltac pose_s_nonzero s s_nonzero :=
+  cache_proof_with_type_by
+    (s <> 0)
+    ltac:(vm_decide_no_check)
+           s_nonzero.
+
+Ltac pose_sz_le_log2_m sz m sz_le_log2_m :=
+  cache_proof_with_type_by
+    (Z.of_nat sz <= Z.log2_up (Z.pos m))
+    ltac:(vm_decide_no_check)
+           sz_le_log2_m.
+
+Ltac pose_m_correct m s c m_correct :=
+  cache_proof_with_type_by
+    (Z.pos m = s - Associational.eval c)
+    ltac:(vm_decide_no_check)
+           m_correct.
+
+Ltac pose_m_enc sz m m_enc :=
+  let v := (eval vm_compute in (m_enc' m sz)) in
+  let v := (eval compute in v) in (* compute away the type arguments *)
+  cache_term v m_enc.
+Ltac pose_coef sz m coef_div_modulus coef := (* subtraction coefficient *)
+  let v := (eval vm_compute in (coef' m sz coef_div_modulus)) in
+  cache_term v coef.
+
+Ltac pose_coef_mod sz wt m coef coef_div_modulus sz_le_log2_m coef_mod :=
+  cache_proof_with_type_by
+    (mod_eq m (Positional.eval (n:=sz) wt coef) 0)
+    ltac:(vm_cast_no_check (coef_mod' m sz coef_div_modulus sz_le_log2_m))
+           coef_mod.
+Ltac pose_sz_nonzero sz sz_nonzero :=
+  cache_proof_with_type_by
+    (sz <> 0%nat)
+    ltac:(vm_decide_no_check)
+           sz_nonzero.
 
 Ltac pose_wt_nonzero wt wt_nonzero :=
   cache_proof_with_type_by
diff --git a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
index 791762975..ea53542a1 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
@@ -69,20 +69,17 @@ Ltac add_m_correct pkg :=
 
 Ltac add_m_enc pkg :=
   let sz := Tag.get pkg TAG.sz in
-  let s := Tag.get pkg TAG.s in
-  let c := Tag.get pkg TAG.c in
-  let wt := Tag.get pkg TAG.wt in
+  let m := Tag.get pkg TAG.m in
   let m_enc := fresh "m_enc" in
-  let m_enc := pose_m_enc sz s c wt m_enc in
+  let m_enc := pose_m_enc sz m m_enc in
   Tag.update pkg TAG.m_enc m_enc.
 
 Ltac add_coef pkg :=
   let sz := Tag.get pkg TAG.sz in
-  let wt := Tag.get pkg TAG.wt in
-  let m_enc := Tag.get pkg TAG.m_enc in
+  let m := Tag.get pkg TAG.m in
   let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in
   let coef := fresh "coef" in
-  let coef := pose_coef sz wt m_enc coef_div_modulus coef in
+  let coef := pose_coef sz m coef_div_modulus coef in
   Tag.update pkg TAG.coef coef.
 
 Ltac add_coef_mod pkg :=
@@ -90,8 +87,10 @@ Ltac add_coef_mod pkg :=
   let wt := Tag.get pkg TAG.wt in
   let m := Tag.get pkg TAG.m in
   let coef := Tag.get pkg TAG.coef in
+  let coef_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 coef_mod := fresh "coef_mod" in
-  let coef_mod := pose_coef_mod sz wt m coef coef_mod in
+  let coef_mod := pose_coef_mod sz wt m coef coef_div_modulus sz_le_log2_m coef_mod in
   Tag.update pkg TAG.coef_mod coef_mod.
 
 Ltac add_sz_nonzero pkg :=
diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v
index 89884fec6..472349180 100644
--- a/src/Specific/Framework/CurveParameters.v
+++ b/src/Specific/Framework/CurveParameters.v
@@ -11,7 +11,7 @@ Local Set Primitive Projections.
 Module Export Notations := RawCurveParameters.Notations.
 
 Module TAG. (* namespacing *)
-  Inductive tags := CP | sz | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel.
+  Inductive tags := CP | sz | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel | mul_code | square_code.
 End TAG.
 
 Module Export CurveParameters.
@@ -220,6 +220,10 @@ Module Export CurveParameters.
     internal_pose_of_CP CP CurveParameters.upper_bound_of_exponent upper_bound_of_exponent.
   Ltac pose_modinv_fuel CP modinv_fuel :=
     internal_pose_of_CP CP CurveParameters.modinv_fuel modinv_fuel.
+  Ltac pose_mul_code CP mul_code :=
+    internal_pose_of_CP CP CurveParameters.mul_code mul_code.
+  Ltac pose_square_code CP square_code :=
+    internal_pose_of_CP CP CurveParameters.square_code square_code.
 
   (* Everything below this line autogenerated by remake_packages.py *)
   Ltac add_sz pkg :=
@@ -300,6 +304,18 @@ Module Export CurveParameters.
     let modinv_fuel := pose_modinv_fuel CP modinv_fuel in
     Tag.update pkg TAG.modinv_fuel modinv_fuel.
 
+  Ltac add_mul_code pkg :=
+    let CP := Tag.get pkg TAG.CP in
+    let mul_code := fresh "mul_code" in
+    let mul_code := pose_mul_code CP mul_code in
+    Tag.update pkg TAG.mul_code mul_code.
+
+  Ltac add_square_code pkg :=
+    let CP := Tag.get pkg TAG.CP in
+    let square_code := fresh "square_code" in
+    let square_code := pose_square_code CP square_code in
+    Tag.update pkg TAG.square_code square_code.
+
   Ltac add_CurveParameters_package pkg :=
     let pkg := add_sz pkg in
     let pkg := add_bitwidth pkg in
@@ -314,5 +330,7 @@ Module Export CurveParameters.
     let pkg := add_freeze_allowable_bit_widths pkg in
     let pkg := add_upper_bound_of_exponent pkg in
     let pkg := add_modinv_fuel pkg in
+    let pkg := add_mul_code pkg in
+    let pkg := add_square_code pkg in
     Tag.strip_local pkg.
 End CurveParameters.
diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v
index 10b72f2ba..75ef1f7e7 100644
--- a/src/Specific/Framework/CurveParametersPackage.v
+++ b/src/Specific/Framework/CurveParametersPackage.v
@@ -49,4 +49,8 @@ Module MakeCurveParametersPackage (PKG : PrePackage).
   Notation upper_bound_of_exponent := (ltac:(let v := get_upper_bound_of_exponent () in exact v)) (only parsing).
   Ltac get_modinv_fuel _ := get TAG.modinv_fuel.
   Notation modinv_fuel := (ltac:(let v := get_modinv_fuel () in exact v)) (only parsing).
+  Ltac get_mul_code _ := get TAG.mul_code.
+  Notation mul_code := (ltac:(let v := get_mul_code () in exact v)) (only parsing).
+  Ltac get_square_code _ := get TAG.square_code.
+  Notation square_code := (ltac:(let v := get_square_code () in exact v)) (only parsing).
 End MakeCurveParametersPackage.