Use a better strategy in Rows.sat_reduce

We now preserve the invariant that weights are in the image of the weight function, insofar as we can, which allows a more fine-tuned analysis of values. After | File Name | Before || Change | % Change --------------------------------------------------------------------------------------------------------------------- 79m58.21s | Total | 19m03.93s || +60m54.27s | +319.44% --------------------------------------------------------------------------------------------------------------------- 66m49.59s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m10.66s || +60m38.93s | +981.74% 4m39.21s | Experiments/NewPipeline/Toplevel1.vo | 4m35.82s || +0m03.38s | +1.22% 1m34.88s | Experiments/NewPipeline/Toplevel2.vo | 1m32.56s || +0m02.31s | +2.50% 0m42.21s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m40.89s || +0m01.32s | +3.22% 0m41.78s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m39.80s || +0m01.98s | +4.97% 0m41.27s | p521_32.c | 0m40.10s || +0m01.17s | +2.91% 0m25.58s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m24.41s || +0m01.16s | +4.79% 1m18.15s | Experiments/NewPipeline/Arithmetic.vo | 1m17.89s || +0m00.26s | +0.33% 0m34.15s | p521_64.c | 0m33.58s || +0m00.57s | +1.69% 0m26.61s | p384_32.c | 0m26.50s || +0m00.10s | +0.41% 0m22.60s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m22.20s || +0m00.40s | +1.80% 0m18.67s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m17.70s || +0m00.97s | +5.48% 0m14.94s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m14.26s || +0m00.67s | +4.76% 0m09.34s | p384_64.c | 0m09.02s || +0m00.32s | +3.54% 0m09.29s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.04s || +0m00.25s | +2.76% 0m06.29s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.98s || +0m00.30s | +5.18% 0m05.94s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.74s || +0m00.20s | +3.48% 0m04.64s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.48s || +0m00.15s | +3.57% 0m04.59s | secp256k1_32.c | 0m04.60s || -0m00.00s | -0.21% 0m04.51s | p256_32.c | 0m04.49s || +0m00.01s | +0.44% 0m04.50s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.46s || +0m00.04s | +0.89% 0m03.64s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.49s || +0m00.14s | +4.29% 0m02.55s | p224_32.c | 0m02.52s || +0m00.02s | +1.19% 0m02.32s | curve25519_32.c | 0m02.41s || -0m00.09s | -3.73% 0m01.82s | p256_64.c | 0m01.81s || +0m00.01s | +0.55% 0m01.74s | p224_64.c | 0m01.86s || -0m00.12s | -6.45% 0m01.68s | secp256k1_64.c | 0m01.77s || -0m00.09s | -5.08% 0m01.64s | curve25519_64.c | 0m01.97s || -0m00.33s | -16.75% 0m01.50s | Experiments/NewPipeline/CLI.vo | 0m01.46s || +0m00.04s | +2.73% 0m01.35s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.28s || +0m00.07s | +5.46% 0m01.23s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.18s || +0m00.05s | +4.23%
mit-plv · Nov 2, 2018 · 4c3405e · 4c3405e
1 parent 29b2e54
commit 4c3405e
Showing 1 changed file with 43 additions and 11 deletions.
diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v
@@ -2114,13 +2114,33 @@ Module Rows.
         let pq_a := Associational.sat_mul base p_a q_a in
         flatten m (from_associational m pq_a).
 
+      (* if [s] is not exactly equal to a weight, we must adjust it to
+         be a weight, so that rather than dividing by s and
+         multiplying by c, we divide by w and multiply by c*(w/s).
+         See
+         https://github.com/mit-plv/fiat-crypto/issues/326#issuecomment-404135131
+         for a bit more discussion *)
+      Definition adjust_s fuel s : Z * bool :=
+        fold_right
+          (fun w_i res
+           => let '(v, found_adjustment) := res in
+              let res := (v, found_adjustment) in
+              if found_adjustment:bool
+              then res
+              else if w_i mod s =? 0
+                   then (w_i, true)
+                   else res)
+          (s, false)
+          (map weight (seq 0 fuel)).
+
       (* TODO : move sat_reduce and repeat_sat_reduce to Saturated.Associational *)
-      Definition sat_reduce base s c (p : list (Z * Z)) :=
-        let lo_hi := Associational.split s p in
-        fst lo_hi ++ (Associational.sat_mul_const base c (snd lo_hi)).
+      Definition sat_reduce base s c n (p : list (Z * Z)) :=
+        let '(s', _) := adjust_s (S (S n)) s in
+        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 q) p (seq 0 n).
+        fold_right (fun _ q => sat_reduce base s c n 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
@@ -2202,23 +2222,35 @@ Module Rows.
         length (fst (mul base n m p q)) = m.
       Proof using wprops. solver; cbn [fst snd]; distr_length. Qed.
 
-      Lemma eval_sat_reduce base s c p :
+      Lemma adjust_s_invariant fuel s (s_nz:s<>0) :
+        fst (adjust_s fuel s) mod s = 0
+        /\ fst (adjust_s fuel s) <> 0.
+      Proof.
+        cbv [adjust_s]; rewrite fold_right_map; generalize (seq 0 fuel); intro ls; induction ls as [|l ls IHls];
+          cbn.
+        { rewrite Z.mod_same by assumption; auto. }
+        { break_match; cbn in *; auto. }
+      Qed.
+
+      Lemma eval_sat_reduce base s c n p :
         base <> 0 -> s - Associational.eval c <> 0 -> s <> 0 ->
-        Associational.eval (sat_reduce base s c p) mod (s - Associational.eval c)
+        Associational.eval (sat_reduce base s c n p) mod (s - Associational.eval c)
         = Associational.eval p mod (s - Associational.eval c).
-      Proof using Type.
+      Proof using wprops.
         intros; cbv [sat_reduce].
-        autorewrite with push_eval.
-        rewrite <-Associational.reduction_rule by omega.
-        autorewrite with push_eval; reflexivity.
+        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 push_eval; trivial.
       Qed.
       Hint Rewrite eval_sat_reduce using auto : push_eval.
 
       Lemma eval_repeat_sat_reduce base s c p n :
         base <> 0 -> s - Associational.eval c <> 0 -> s <> 0 ->
         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 Type.
+      Proof using wprops.
         intros; cbv [repeat_sat_reduce].
         apply fold_right_invariant; intros; autorewrite with push_eval; auto.
       Qed.