Factor out a common computation to fix n² behavior

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
79m19.27s | Total                                                                | 79m40.48s || -0m21.20s | -0.44%
--------------------------------------------------------------------------------------------------------------------
66m25.35s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo                | 66m13.56s || +0m11.78s | +0.29%
4m37.48s  | Experiments/NewPipeline/Toplevel1.vo                                 | 4m46.12s  || -0m08.63s | -3.01%
1m31.62s  | Experiments/NewPipeline/Toplevel2.vo                                 | 1m36.13s  || -0m04.50s | -4.69%
0m38.77s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m41.51s  || -0m02.73s | -6.60%
0m09.03s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m11.08s  || -0m02.05s | -18.50%
1m18.56s  | Experiments/NewPipeline/Arithmetic.vo                                | 1m20.43s  || -0m01.87s | -2.32%
0m41.04s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m42.15s  || -0m01.10s | -2.63%
0m39.96s  | p521_32.c                                                            | 0m41.66s  || -0m01.69s | -4.08%
0m33.17s  | p521_64.c                                                            | 0m34.21s  || -0m01.03s | -3.04%
0m24.54s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m25.88s  || -0m01.33s | -5.17%
0m17.82s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m19.33s  || -0m01.50s | -7.81%
0m06.01s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m07.38s  || -0m01.37s | -18.56%
0m05.85s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m07.55s  || -0m01.70s | -22.51%
0m26.58s  | p384_32.c                                                            | 0m26.63s  || -0m00.05s | -0.18%
0m22.45s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m23.09s  || -0m00.64s | -2.77%
0m14.58s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m15.11s  || -0m00.52s | -3.50%
0m09.01s  | p384_64.c                                                            | 0m09.32s  || -0m00.31s | -3.32%
0m04.65s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m05.37s  || -0m00.71s | -13.40%
0m04.59s  | secp256k1_32.c                                                       | 0m04.52s  || +0m00.07s | +1.54%
0m04.47s  | p256_32.c                                                            | 0m04.53s  || -0m00.06s | -1.32%
0m04.32s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m04.84s  || -0m00.51s | -10.74%
0m03.70s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m04.16s  || -0m00.46s | -11.05%
0m02.52s  | p224_32.c                                                            | 0m02.63s  || -0m00.10s | -4.18%
0m02.42s  | curve25519_32.c                                                      | 0m02.34s  || +0m00.08s | +3.41%
0m01.86s  | p224_64.c                                                            | 0m01.76s  || +0m00.10s | +5.68%
0m01.72s  | p256_64.c                                                            | 0m01.72s  || +0m00.00s | +0.00%
0m01.65s  | secp256k1_64.c                                                       | 0m01.71s  || -0m00.06s | -3.50%
0m01.59s  | curve25519_64.c                                                      | 0m01.57s  || +0m00.02s | +1.27%
0m01.51s  | Experiments/NewPipeline/CLI.vo                                       | 0m01.50s  || +0m00.01s | +0.66%
0m01.27s  | Experiments/NewPipeline/StandaloneOCamlMain.vo                       | 0m01.30s  || -0m00.03s | -2.30%
0m01.18s  | Experiments/NewPipeline/StandaloneHaskellMain.vo                     | 0m01.39s  || -0m00.20s | -15.10%

1 files changed, 12 insertions, 9 deletions

diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v
index 59c13e8c5..05bd2e83f 100644
--- a/src/Experiments/NewPipeline/Arithmetic.v
+++ b/src/Experiments/NewPipeline/Arithmetic.v
@@ -15,6 +15,7 @@ Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Import Crypto.Util.Tactics.RunTacticAsConstr.
 Require Import Crypto.Util.Tactics.Head.
+Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.OptionList.
 Require Import Crypto.Util.Prod.
@@ -2134,13 +2135,13 @@ Module Rows.
           (map weight (seq 0 fuel)).
 
       (* TODO : move sat_reduce and repeat_sat_reduce to Saturated.Associational *)
-      Definition sat_reduce base s c n (p : list (Z * Z)) :=
-        let '(s', _) := adjust_s (S (S n)) s in
+      Definition sat_reduce base s s' c (p : list (Z * Z)) :=
         let lo_hi := Associational.split s' p in
         fst lo_hi ++ (Associational.sat_mul_const base [(1, s'/s)] (Associational.sat_mul_const base c (snd lo_hi))).
 
       Definition repeat_sat_reduce base s c (p : list (Z * Z)) n :=
-        fold_right (fun _ q => sat_reduce base s c n q) p (seq 0 n).
+        let '(s', _) := adjust_s (S (S n)) s in
+        fold_right (fun _ q => sat_reduce base s s' c q) p (seq 0 n).
 
       Definition mulmod base s c n nreductions (p q : list Z) :=
         let p_a := Positional.to_associational weight n p in
@@ -2232,16 +2233,17 @@ Module Rows.
         { break_match; cbn in *; auto. }
       Qed.
 
-      Lemma eval_sat_reduce base s c n p :
+      Lemma eval_sat_reduce base s s' c p :
         base <> 0 -> s - Associational.eval c <> 0 -> s <> 0 ->
-        Associational.eval (sat_reduce base s c n p) mod (s - Associational.eval c)
+        s' mod s = 0 -> s' <> 0 ->
+        Associational.eval (sat_reduce base s s' c p) mod (s - Associational.eval c)
         = Associational.eval p mod (s - Associational.eval c).
       Proof using wprops.
         intros; cbv [sat_reduce].
-        lazymatch goal with |- context[adjust_s ?fuel ?s] => destruct (adjust_s_invariant fuel s ltac:(assumption)) as [Hmod ?] end.
         eta_expand; autorewrite with push_eval zsimplify_const; cbn [fst snd].
         rewrite !Z.mul_assoc, <- (Z.mul_comm (Associational.eval c)), <- !Z.mul_assoc, <-Associational.reduction_rule by auto.
-        autorewrite with zsimplify_const; rewrite !Z.mul_assoc, Z.mul_div_eq_full, Hmod by auto.
+        autorewrite with zsimplify_const; rewrite !Z.mul_assoc, Z.mul_div_eq_full by auto.
+        rewrite_hyp !*.
         autorewrite with zsimplify_const push_eval; trivial.
       Qed.
       Hint Rewrite eval_sat_reduce using auto : push_eval.
@@ -2251,8 +2253,9 @@ Module Rows.
         Associational.eval (repeat_sat_reduce base s c p n) mod (s - Associational.eval c)
         = Associational.eval p mod (s - Associational.eval c).
       Proof using wprops.
-        intros; cbv [repeat_sat_reduce].
-        apply fold_right_invariant; intros; autorewrite with push_eval; auto.
+        intros; cbv [repeat_sat_reduce]; eta_expand.
+        apply fold_right_invariant; intros; autorewrite with push_eval; auto;
+          apply adjust_s_invariant; assumption.
       Qed.
       Hint Rewrite eval_repeat_sat_reduce using auto : push_eval.