Use div_cps and modulo_cps in more places

After     | File Name                                                | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------
10m04.41s | Total                                                    | 10m03.68s || +0m00.73s | +0.12%
--------------------------------------------------------------------------------------------------------
3m04.06s  | Specific/X25519/C64/ladderstep                           | 3m04.00s  || +0m00.06s | +0.03%
1m48.23s  | Specific/NISTP256/AMD64/femul                            | 1m48.30s  || -0m00.07s | -0.06%
0m38.59s  | Arithmetic/Karatsuba                                     | 0m38.51s  || +0m00.08s | +0.20%
0m22.50s  | Specific/X25519/C64/femul                                | 0m23.15s  || -0m00.64s | -2.80%
0m21.79s  | Specific/NISTP256/AMD64/fesub                            | 0m21.76s  || +0m00.02s | +0.13%
0m19.78s  | Specific/NISTP256/AMD64/feadd                            | 0m19.94s  || -0m00.16s | -0.80%
0m18.57s  | Specific/X25519/C64/freeze                               | 0m18.57s  || +0m00.00s | +0.00%
0m17.96s  | Specific/X25519/C64/fesquare                             | 0m18.36s  || -0m00.39s | -2.17%
0m16.54s  | Specific/NISTP256/AMD64/feopp                            | 0m16.18s  || +0m00.35s | +2.22%
0m14.58s  | Specific/X25519/C64/fecarry                              | 0m14.76s  || -0m00.17s | -1.21%
0m13.80s  | Specific/NISTP256/AMD64/fenz                             | 0m13.84s  || -0m00.03s | -0.28%
0m13.34s  | Specific/X25519/C64/fesub                                | 0m13.57s  || -0m00.23s | -1.69%
0m12.72s  | Arithmetic/Saturated/AddSub                              | 0m12.74s  || -0m00.01s | -0.15%
0m12.19s  | Specific/X25519/C64/feadd                                | 0m12.48s  || -0m00.29s | -2.32%
0m10.57s  | Arithmetic/Saturated/MontgomeryAPI                       | 0m10.36s  || +0m00.21s | +2.02%
0m10.17s  | Arithmetic/Saturated/Core                                | 0m09.92s  || +0m00.25s | +2.52%
0m06.47s  | Specific/NISTP256/AMD64/Synthesis                        | 0m06.65s  || -0m00.18s | -2.70%
0m06.02s  | Arithmetic/Saturated/MulSplit                            | 0m05.87s  || +0m00.14s | +2.55%
0m05.27s  | Specific/X25519/C64/Synthesis                            | 0m05.45s  || -0m00.18s | -3.30%
0m03.70s  | Arithmetic/MontgomeryReduction/WordByWord/Proofs         | 0m03.65s  || +0m00.05s | +1.36%
0m03.66s  | Specific/Framework/ArithmeticSynthesis/Montgomery        | 0m03.70s  || -0m00.04s | -1.08%
0m02.93s  | Specific/Framework/ArithmeticSynthesis/Defaults          | 0m02.60s  || +0m00.33s | +12.69%
0m02.42s  | Arithmetic/Saturated/Freeze                              | 0m02.45s  || -0m00.03s | -1.22%
0m01.57s  | Arithmetic/CoreUnfolder                                  | 0m01.52s  || +0m00.05s | +3.28%
0m01.44s  | Specific/Framework/ArithmeticSynthesis/HelperTactics     | 0m01.11s  || +0m00.32s | +29.72%
0m01.29s  | Specific/Framework/ArithmeticSynthesis/Karatsuba         | 0m01.21s  || +0m00.08s | +6.61%
0m01.19s  | Specific/Framework/ArithmeticSynthesis/Base              | 0m01.00s  || +0m00.18s | +18.99%
0m01.04s  | Arithmetic/Saturated/CoreUnfolder                        | 0m01.13s  || -0m00.08s | -7.96%
0m01.00s  | Arithmetic/Saturated/UniformWeight                       | 0m00.95s  || +0m00.05s | +5.26%
0m00.92s  | Arithmetic/Saturated/WrappersUnfolder                    | 0m00.96s  || -0m00.03s | -4.16%
0m00.89s  | Specific/Framework/SynthesisFramework                    | 0m01.00s  || -0m00.10s | -10.99%
0m00.87s  | Specific/Framework/ReificationTypes                      | 0m01.00s  || -0m00.13s | -13.00%
0m00.84s  | Specific/Framework/MontgomeryReificationTypesPackage     | 0m00.82s  || +0m00.02s | +2.43%
0m00.81s  | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.72s  || +0m00.09s | +12.50%
0m00.80s  | Specific/Framework/ArithmeticSynthesis/Freeze            | 0m00.86s  || -0m00.05s | -6.97%
0m00.78s  | Arithmetic/MontgomeryReduction/WordByWord/Definition     | 0m00.76s  || +0m00.02s | +2.63%
0m00.77s  | Specific/Framework/MontgomeryReificationTypes            | 0m00.80s  || -0m00.03s | -3.75%
0m00.76s  | Arithmetic/Saturated/MulSplitUnfolder                    | 0m00.80s  || -0m00.04s | -5.00%
0m00.76s  | Specific/Framework/ArithmeticSynthesis/DefaultsPackage   | 0m00.70s  || +0m00.06s | +8.57%
0m00.75s  | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage  | 0m00.64s  || +0m00.10s | +17.18%
0m00.75s  | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.71s  || +0m00.04s | +5.63%
0m00.74s  | Arithmetic/Saturated/Wrappers                            | 0m00.78s  || -0m00.04s | -5.12%
0m00.73s  | Arithmetic/Saturated/FreezeUnfolder                      | 0m00.77s  || -0m00.04s | -5.19%
0m00.72s  | Specific/Framework/ArithmeticSynthesis/SquareFromMul     | 0m00.72s  || +0m00.00s | +0.00%
0m00.72s  | Specific/Framework/ReificationTypesPackage               | 0m00.84s  || -0m00.12s | -14.28%
0m00.71s  | Specific/Framework/ArithmeticSynthesis/FreezePackage     | 0m00.69s  || +0m00.02s | +2.89%
0m00.70s  | Specific/Framework/ArithmeticSynthesis/Ladderstep        | 0m00.67s  || +0m00.02s | +4.47%
0m00.69s  | Specific/Framework/ArithmeticSynthesis/BasePackage       | 0m01.03s  || -0m00.34s | -33.00%
0m00.66s  | Arithmetic/Saturated/UniformWeightInstances              | 0m00.67s  || -0m00.01s | -1.49%
0m15.65s  | Arithmetic/Core                                          | 0m14.01s  || +0m01.64s | +11.70%

1 files changed, 57 insertions, 24 deletions

diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index 929aa2260..a33bd394d 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -438,23 +438,32 @@ Module B.
     Qed. Hint Rewrite eval_negate_snd : push_basesystem_eval.
 
     Section Carries.
-      Context {modulo div:Z->Z->Z}.
+      Context {modulo_cps div_cps:forall {R},Z->Z->(Z->R)->R}.
+      Let modulo x y := modulo_cps _ x y id.
+      Let div x y := div_cps _ x y id.
+      Context {modulo_cps_id : forall R x y f, modulo_cps R x y f = f (modulo x y)}
+              {div_cps_id : forall R x y f, div_cps R x y f = f (div x y)}.
       Context {div_mod : forall a b:Z, b <> 0 ->
                                        a = b * (div a b) + modulo a b}.
+      Hint Rewrite modulo_cps_id div_cps_id : uncps.
 
       Definition carryterm_cps (w fw:Z) (t:limb) {T} (f:list limb->T) :=
         if dec (fst t = w)
         then dlet t2 := snd t in
-             dlet d2 := div t2 fw in
-             dlet m2 := modulo t2 fw in
-             f ((w*fw, d2) :: (w, m2) :: @nil limb)
+             div_cps _ t2 fw (fun d2 =>
+             modulo_cps _ t2 fw (fun m2 =>
+             dlet d2 := d2 in
+             dlet m2 := m2 in
+             f ((w*fw, d2) :: (w, m2) :: @nil limb)))
         else f [t].
 
       Definition carryterm w fw t := carryterm_cps w fw t id.
       Lemma carryterm_cps_id w fw t {T} f :
         @carryterm_cps w fw t T f
         = f (@carryterm w fw t).
-      Proof using Type. cbv [carryterm_cps carryterm Let_In]; prove_id. Qed.
+      Proof using div_cps_id modulo_cps_id.
+        cbv [carryterm_cps carryterm Let_In]; prove_id.
+      Qed.
       Hint Opaque carryterm : uncps.
       Hint Rewrite carryterm_cps_id : uncps.
 
@@ -473,7 +482,9 @@ Module B.
       Definition carry w fw p := carry_cps w fw p id.
       Lemma carry_cps_id w fw p {T} f:
         @carry_cps w fw p T f = f (carry w fw p).
-      Proof using Type. cbv [carry_cps carry]; prove_id. Qed.
+      Proof using div_cps_id modulo_cps_id.
+        cbv [carry_cps carry]; prove_id.
+      Qed.
       Hint Opaque carry : uncps.
       Hint Rewrite carry_cps_id : uncps.
 
@@ -484,12 +495,19 @@ Module B.
     End Carries.
 
   End Associational.
+
+  Ltac div_mod_cps_t :=
+    intros; autorewrite with uncps push_id; try reflexivity.
+
   Hint Rewrite
-      @Associational.carry_cps_id
-      @Associational.carryterm_cps_id
       @Associational.reduce_cps_id
       @Associational.split_cps_id
       @Associational.mul_cps_id : uncps.
+  Hint Rewrite
+       @Associational.carry_cps_id
+       @Associational.carryterm_cps_id
+       using div_mod_cps_t : uncps.
+
 
   Module Positional.
     Section Positional.
@@ -644,14 +662,20 @@ Module B.
         : push_basesystem_eval.
 
       Section Carries.
-        Context {modulo div : Z->Z->Z}.
+        Context {modulo_cps div_cps:forall {R},Z->Z->(Z->R)->R}.
+        Let modulo x y := modulo_cps _ x y id.
+        Let div x y := div_cps _ x y id.
+        Context {modulo_cps_id : forall R x y f, modulo_cps R x y f = f (modulo x y)}
+                {div_cps_id : forall R x y f, div_cps R x y f = f (div x y)}.
         Context {div_mod : forall a b:Z, b <> 0 ->
-                                       a = b * (div a b) + modulo a b}.
+                                         a = b * (div a b) + modulo a b}.
+        Hint Rewrite modulo_cps_id div_cps_id : uncps.
+
         Definition carry_cps {n m} (index:nat) (p:tuple Z n)
                    {T} (f:tuple Z m->T) :=
           to_associational_cps p
             (fun P =>  @Associational.carry_cps
-                         modulo div
+                         modulo_cps div_cps
                          (weight index)
                          (weight (S index) / weight index)
                          P T
@@ -690,7 +714,9 @@ Module B.
       Definition chained_carries {n} p idxs := @chained_carries_cps n p idxs _ id.
       Lemma chained_carries_id {n} p idxs : forall {T} f,
           @chained_carries_cps n p idxs T f = f (chained_carries p idxs).
-      Proof using Type. cbv [chained_carries_cps chained_carries]; prove_id. Qed.
+      Proof using modulo_cps_id div_cps_id.
+        cbv [chained_carries_cps chained_carries]; prove_id.
+      Qed.
       Hint Opaque chained_carries : uncps.
       Hint Rewrite @chained_carries_id : uncps.
 
@@ -738,10 +764,10 @@ Module B.
             (fun P => Associational.reduce_cps s c P
                (fun R => from_associational_cps n R f)).
 
-        Definition carry_reduce_cps {n div modulo}
+        Definition carry_reduce_cps {n div_cps modulo_cps}
                    (s:Z) (c:list limb) (p : tuple Z n)
                    {T} (f: tuple Z n ->T) :=
-          carry_cps (div:=div) (modulo:=modulo) (n:=n) (m:=S n) (pred n) p
+          carry_cps (div_cps:=div_cps) (modulo_cps:=modulo_cps) (n:=n) (m:=S n) (pred n) p
             (fun r => reduce_cps (m:=S n) (n:=n) s c r f).
 
         Definition negate_snd_cps {n} (p : tuple Z n)
@@ -820,18 +846,23 @@ Module B.
       Section F.
         Context {sz:nat} {sz_nonzero : sz<>0%nat} {m :positive}.
         Context (weight_divides : forall i : nat, weight (S i) / weight i <> 0).
-        Context {modulo div:Z->Z->Z}
-                {div_mod : forall a b:Z, b <> 0 ->
+        Context {modulo_cps div_cps:forall {R},Z->Z->(Z->R)->R}.
+        Let modulo x y := modulo_cps _ x y id.
+        Let div x y := div_cps _ x y id.
+        Context {modulo_cps_id : forall R x y f, modulo_cps R x y f = f (modulo x y)}
+                {div_cps_id : forall R x y f, div_cps R x y f = f (div x y)}.
+        Context {div_mod : forall a b:Z, b <> 0 ->
                                          a = b * (div a b) + modulo a b}.
+        Hint Rewrite modulo_cps_id div_cps_id : uncps.
 
         Definition Fencode (x : F m) : tuple Z sz :=
-          encode (div:=div) (modulo:=modulo) (F.to_Z x).
+          encode (div_cps:=div_cps) (modulo_cps:=modulo_cps) (F.to_Z x).
 
         Definition Fdecode (x : tuple Z sz) : F m := F.of_Z m (eval x).
 
         Lemma Fdecode_Fencode_id x : Fdecode (Fencode x) = x.
-        Proof using div_mod sz_nonzero weight_0 weight_divides weight_nonzero.
-          cbv [Fdecode Fencode]; rewrite @eval_encode by auto.
+        Proof using div_mod sz_nonzero weight_0 weight_divides weight_nonzero div_cps_id modulo_cps_id.
+          cbv [Fdecode Fencode]; rewrite @eval_encode by eauto.
           apply F.of_Z_to_Z.
         Qed.
 
@@ -935,21 +966,23 @@ Module B.
       Positional.opp_cps
   .
   Hint Rewrite
-      @Associational.carry_cps_id
-      @Associational.carryterm_cps_id
       @Associational.reduce_cps_id
       @Associational.split_cps_id
       @Associational.mul_cps_id
-      @Positional.carry_cps_id
       @Positional.from_associational_cps_id
       @Positional.place_cps_id
       @Positional.add_to_nth_cps_id
       @Positional.to_associational_cps_id
-      @Positional.chained_carries_id
       @Positional.sub_id
       @Positional.select_id
     : uncps.
   Hint Rewrite
+       @Associational.carry_cps_id
+       @Associational.carryterm_cps_id
+       @Positional.carry_cps_id
+       @Positional.chained_carries_id
+       using div_mod_cps_t : uncps.
+  Hint Rewrite
        @Associational.eval_mul
        @Positional.eval_single
        @Positional.eval_unit
@@ -966,7 +999,7 @@ Module B.
        @Positional.eval_chained_carries
        @Positional.eval_sub
        @Positional.eval_select
-    using (assumption || vm_decide) : push_basesystem_eval.
+       using (assumption || (div_mod_cps_t; auto) || vm_decide) : push_basesystem_eval.
 End B.
 
 (* Modulo and div that do shifts if possible, otherwise normal mod/div *)