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%

4 files changed, 74 insertions, 38 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 *)
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Base.v b/src/Specific/Framework/ArithmeticSynthesis/Base.v
index a3ed3dfef..490ff35c7 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Base.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Base.v
@@ -49,7 +49,7 @@ Section gen.
   Definition half_sz' := (sz / 2)%nat.
 
   Definition m_enc'
-    := Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (Z.pos m).
+    := Positional.encode (modulo_cps:=@modulo_cps) (div_cps:=@div_cps) (n:=sz) wt (Z.pos m).
 
   Lemma sz2'_nonzero
         (sz_nonzero : sz <> 0%nat)
@@ -152,7 +152,7 @@ Section gen.
     destruct (Nat.eq_dec sz 0).
     { subst; reflexivity. }
     { repeat autounfold; autorewrite with uncps push_id push_basesystem_eval.
-      rewrite Positional.eval_encode by auto.
+      rewrite Positional.eval_encode by (intros; autorewrite with uncps; unfold id; auto).
       cbv [mod_eq] in *.
       push_Zmod; rewrite Hv'; pull_Zmod.
       reflexivity. }
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v
index 023d0821d..75360a92d 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v
@@ -28,7 +28,7 @@ Local Ltac solve_constant_local_sig :=
   idtac;
   lazymatch goal with
   | [ |- { c : Z^?sz | Positional.Fdecode (m:=?M) ?wt c = ?v } ]
-    => (exists (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt (F.to_Z (m:=M) v)));
+    => (exists (Positional.encode (n:=sz) (modulo_cps:=@modulo_cps) (div_cps:=@div_cps) wt (F.to_Z (m:=M) v)));
        lazymatch goal with
        | [ sz_nonzero : sz <> 0%nat, base_pos : (1 <= _)%Q |- _ ]
          => clear -base_pos sz_nonzero
@@ -37,7 +37,8 @@ Local Ltac solve_constant_local_sig :=
   abstract (
       setoid_rewrite Positional.Fdecode_Fencode_id;
       [ reflexivity
-      | auto using wt_gen0_1, wt_gen_nonzero, wt_gen_divides', div_mod.. ]
+      | auto using wt_gen0_1, wt_gen_nonzero, wt_gen_divides', div_mod;
+        intros; autorewrite with uncps push_id; auto using div_mod.. ]
     ).
 
 Section gen.
@@ -118,8 +119,7 @@ Section gen.
         unfold chained_carries'.
         rewrite IHcarry_chains by auto.
         repeat autounfold; autorewrite with uncps push_id push_basesystem_eval.
-        rewrite Positional.eval_carry by auto.
-        rewrite Positional.eval_chained_carries by auto; reflexivity. } }
+        reflexivity. } }
   Defined.
 
   Definition constant_sig' v
@@ -264,6 +264,7 @@ Section gen.
       | [ |- context[@proj1_sig ?A ?P ?x] ]
         => pattern (@proj1_sig A P x);
              exact (@proj2_sig A P x)
+      | _ => eauto using @Core.modulo_id, @Core.div_id with nocore
       end.
   Defined.
 
@@ -403,6 +404,8 @@ Ltac pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_si
        (Positional.Fdecode_Fencode_id
           (sz_nonzero := sz_nonzero)
           (div_mod := div_mod)
+          (modulo_cps_id:=@Core.modulo_id)
+          (div_cps_id:=@Core.div_id)
           wt eq_refl wt_nonzero wt_divides')
        (Positional.eq_Feq_iff wt)
        (proj2_sig add_sig)
diff --git a/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v b/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
index e777fe23e..0b8c649a0 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
@@ -77,11 +77,11 @@ Section chained_carries_cps'.
        | nil => f a
        | carry_chain :: nil
          => Positional.chained_carries_cps
-              (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain f
+              (n:=sz) (div_cps:=@div_cps) (modulo_cps:=@modulo_cps) wt a carry_chain f
        | carry_chain :: carry_chains
          => Positional.chained_carries_cps
-              (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain
-              (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r
+              (n:=sz) (div_cps:=@div_cps) (modulo_cps:=@modulo_cps) wt a carry_chain
+              (fun r => Positional.carry_reduce_cps (n:=sz) (div_cps:=@div_cps) (modulo_cps:=@modulo_cps) wt s c r
               (fun r' => chained_carries_cps' r' carry_chains f))
        end.
   Fixpoint chained_carries_cps' (a : Tuple.tuple Z sz) (carry_chains : list (list nat))
@@ -93,11 +93,11 @@ Section chained_carries_cps'.
     : chained_carries_cps' a (carry_chain :: carry_chains) f
       = match length carry_chains with
         | O => Positional.chained_carries_cps
-                 (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain f
+                 (n:=sz) (div_cps:=@div_cps) (modulo_cps:=@modulo_cps) wt a carry_chain f
         | S _
           => Positional.chained_carries_cps
-               (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain
-               (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r
+               (n:=sz) (div_cps:=@div_cps) (modulo_cps:=@modulo_cps) wt a carry_chain
+               (fun r => Positional.carry_reduce_cps (n:=sz) (div_cps:=@div_cps) (modulo_cps:=@modulo_cps) wt s c r
                (fun r' => chained_carries_cps' r' carry_chains f))
         end.
   Proof.
@@ -114,7 +114,7 @@ Section chained_carries_cps'.
     destruct carry_chains as [|carry_chain carry_chains]; [ reflexivity | ].
     cbv [chained_carries'].
     revert a carry_chain; induction carry_chains as [|? carry_chains IHcarry_chains]; intros.
-    { simpl; repeat autounfold; autorewrite with uncps; reflexivity. }
+    { simpl; repeat autounfold; autorewrite with uncps. reflexivity. }
     { rewrite !step_chained_carries_cps'.
       simpl @length; cbv iota beta.
       repeat autounfold; autorewrite with uncps.
@@ -179,6 +179,6 @@ Ltac solve_constant_sig :=
   lazymatch goal with
   | [ |- { c : Z^?sz | Positional.Fdecode (m:=?M) ?wt c = ?v } ]
     => let t := (eval vm_compute in
-                    (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt (F.to_Z (m:=M) v))) in
+                    (Positional.encode (n:=sz) (modulo_cps:=@modulo_cps) (div_cps:=@div_cps) wt (F.to_Z (m:=M) v))) in
        (exists t; vm_decide)
   end.