Switch arithmetic to cps for Z * Z under the hood

This is in preparation for writing a ~compiler for the arithmetic things
to expression trees.

I'm not sure what's up with femul in the table below; I ran it again and
got:
After:
src/Specific/NISTP256/AMD64/femul (real: 115.70, user: 115.25, sys: 0.44, mem: 3571448 ko)
Before:
src/Specific/NISTP256/AMD64/femul (real: 118.49, user: 117.99, sys: 0.43, mem: 3581612 ko)

After     | File Name                                                | Before    || Change
---------------------------------------------------------------------------------------------
17m02.82s | Total                                                    | 16m36.20s || +0m26.61s
---------------------------------------------------------------------------------------------
2m27.04s  | Specific/NISTP256/AMD64/femul                            | 2m04.60s  || +0m22.43s
1m38.55s  | Specific/X2448/Karatsuba/C64/femul                       | 1m41.44s  || -0m02.89s
0m12.46s  | Arithmetic/Saturated/AddSub                              | 0m09.77s  || +0m02.69s
3m22.38s  | Specific/X25519/C64/ladderstep                           | 3m23.49s  || -0m01.11s
0m54.40s  | Specific/X25519/C32/fesquare                             | 0m52.68s  || +0m01.71s
0m28.70s  | Arithmetic/Karatsuba                                     | 0m27.59s  || +0m01.10s
0m10.00s  | Arithmetic/Saturated/MontgomeryAPI                       | 0m08.95s  || +0m01.05s
0m08.15s  | Specific/X2448/Karatsuba/C64/Synthesis                   | 0m09.47s  || -0m01.32s
0m05.62s  | Arithmetic/Saturated/MulSplit                            | 0m04.28s  || +0m01.33s
1m29.44s  | Specific/X25519/C32/femul                                | 1m28.55s  || +0m00.89s
0m39.38s  | Specific/X25519/C32/freeze                               | 0m38.62s  || +0m00.76s
0m31.54s  | Specific/NISTP256/AMD128/femul                           | 0m31.60s  || -0m00.06s
0m24.80s  | Specific/X25519/C64/femul                                | 0m24.10s  || +0m00.69s
0m23.82s  | Specific/NISTP256/AMD64/fesub                            | 0m23.52s  || +0m00.30s
0m21.81s  | Specific/NISTP256/AMD64/feadd                            | 0m21.90s  || -0m00.08s
0m20.30s  | Specific/X25519/C64/freeze                               | 0m20.26s  || +0m00.03s
0m20.12s  | Specific/X25519/C32/Synthesis                            | 0m20.77s  || -0m00.64s
0m19.12s  | Specific/X25519/C64/fesquare                             | 0m19.02s  || +0m00.10s
0m17.28s  | Specific/NISTP256/AMD64/feopp                            | 0m17.68s  || -0m00.39s
0m15.99s  | Specific/NISTP256/AMD128/fesub                           | 0m16.03s  || -0m00.04s
0m15.88s  | Specific/NISTP256/AMD128/feadd                           | 0m16.56s  || -0m00.67s
0m15.03s  | Specific/NISTP256/AMD64/fenz                             | 0m15.00s  || +0m00.02s
0m14.18s  | Specific/NISTP256/AMD128/fenz                            | 0m14.12s  || +0m00.06s
0m13.46s  | Specific/NISTP256/AMD128/feopp                           | 0m12.88s  || +0m00.58s
0m12.15s  | Arithmetic/Core                                          | 0m12.03s  || +0m00.12s
0m07.82s  | Arithmetic/Saturated/Core                                | 0m07.05s  || +0m00.77s
0m07.13s  | Specific/NISTP256/AMD64/Synthesis                        | 0m08.05s  || -0m00.92s
0m05.48s  | Specific/X25519/C64/Synthesis                            | 0m05.68s  || -0m00.19s
0m04.02s  | Specific/Framework/ArithmeticSynthesis/Montgomery        | 0m03.89s  || +0m00.12s
0m03.52s  | Arithmetic/MontgomeryReduction/WordByWord/Proofs         | 0m03.34s  || +0m00.18s
0m03.32s  | Specific/NISTP256/AMD128/Synthesis                       | 0m03.46s  || -0m00.14s
0m02.30s  | Specific/Framework/ArithmeticSynthesis/Defaults          | 0m02.31s  || -0m00.01s
0m02.08s  | Arithmetic/Saturated/Freeze                              | 0m01.94s  || +0m00.14s
0m01.66s  | Specific/Framework/OutputType                            | 0m01.66s  || +0m00.00s
0m01.54s  | Arithmetic/CoreUnfolder                                  | 0m01.43s  || +0m00.11s
0m01.35s  | Specific/Framework/ArithmeticSynthesis/Karatsuba         | 0m01.28s  || +0m00.07s
0m01.13s  | Arithmetic/Saturated/CoreUnfolder                        | 0m01.16s  || -0m00.03s
0m01.06s  | Arithmetic/Saturated/WrappersUnfolder                    | 0m01.04s  || +0m00.02s
0m01.04s  | Arithmetic/Saturated/UniformWeight                       | 0m00.95s  || +0m00.09s
0m01.03s  | Specific/Framework/ArithmeticSynthesis/Base              | 0m01.14s  || -0m00.10s
0m01.02s  | Specific/Framework/SynthesisFramework                    | 0m01.04s  || -0m00.02s
0m00.97s  | Specific/Framework/ArithmeticSynthesis/HelperTactics     | 0m01.01s  || -0m00.04s
0m00.92s  | Specific/Framework/ReificationTypes                      | 0m00.90s  || +0m00.02s
0m00.92s  | Specific/Framework/ArithmeticSynthesis/Freeze            | 0m00.93s  || -0m00.01s
0m00.90s  | Arithmetic/Saturated/MulSplitUnfolder                    | 0m00.83s  || +0m00.07s
0m00.83s  | Specific/Framework/ReificationTypesPackage               | 0m00.79s  || +0m00.03s
0m00.83s  | Arithmetic/Saturated/FreezeUnfolder                      | 0m00.86s  || -0m00.03s
0m00.82s  | Specific/Framework/ArithmeticSynthesis/BasePackage       | 0m00.77s  || +0m00.04s
0m00.81s  | Specific/Framework/ArithmeticSynthesis/SquareFromMul     | 0m00.72s  || +0m00.09s
0m00.81s  | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.82s  || -0m00.00s
0m00.80s  | Specific/Framework/MontgomeryReificationTypesPackage     | 0m00.82s  || -0m00.01s
0m00.78s  | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.79s  || -0m00.01s
0m00.78s  | Arithmetic/Saturated/Wrappers                            | 0m00.78s  || +0m00.00s
0m00.76s  | Specific/Framework/ArithmeticSynthesis/FreezePackage     | 0m00.80s  || -0m00.04s
0m00.76s  | Specific/Framework/ArithmeticSynthesis/DefaultsPackage   | 0m00.75s  || +0m00.01s
0m00.75s  | Specific/Framework/MontgomeryReificationTypes            | 0m00.78s  || -0m00.03s
0m00.73s  | Specific/Framework/ArithmeticSynthesis/Ladderstep        | 0m00.77s  || -0m00.04s
0m00.73s  | Arithmetic/MontgomeryReduction/WordByWord/Definition     | 0m00.80s  || -0m00.07s
0m00.72s  | Arithmetic/Saturated/UniformWeightInstances              | 0m00.78s  || -0m00.06s
0m00.68s  | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage  | 0m00.76s  || -0m00.07s
0m00.43s  | Util/ZUtil/CPS                                           | 0m00.42s  || +0m00.01s

1 files changed, 6 insertions, 6 deletions

diff --git a/src/Util/ZUtil/CPS.v b/src/Util/ZUtil/CPS.v
index 754f6cf56..3c0007c88 100644
--- a/src/Util/ZUtil/CPS.v
+++ b/src/Util/ZUtil/CPS.v
@@ -35,38 +35,38 @@ Module Z.
                  | break_innermost_match_step ].
 
   Definition get_carry_cps {T} (bitwidth : Z) (v : Z) (f : Z * Z -> T) : T
-    := let '(v, c) := Z.get_carry bitwidth v in f (v, c).
+    := f (Z.get_carry bitwidth v).
   Definition get_carry_cps_correct {T} bitwidth v f
     : @get_carry_cps T bitwidth v f = f (Z.get_carry bitwidth v)
     := eq_refl.
   Hint Rewrite @get_carry_cps_correct : uncps.
   Definition add_with_get_carry_cps {T} (bitwidth : Z) (c : Z) (x y : Z) (f : Z * Z -> T) : T
-    := let '(v, c) := Z.add_with_get_carry bitwidth c x y in f (v, c).
+    := f (Z.add_with_get_carry bitwidth c x y).
   Definition add_with_get_carry_cps_correct {T} bitwidth c x y f
     : @add_with_get_carry_cps T bitwidth c x y f = f (Z.add_with_get_carry bitwidth c x y)
     := eq_refl.
   Hint Rewrite @add_with_get_carry_cps_correct : uncps.
   Definition add_get_carry_cps {T} (bitwidth : Z) (x y : Z) (f : Z * Z -> T) : T
-    := let '(v, c) := Z.add_get_carry bitwidth x y in f (v, c).
+    := f (Z.add_get_carry bitwidth x y).
   Definition add_get_carry_cps_correct {T} bitwidth x y f
     : @add_get_carry_cps T bitwidth x y f = f (Z.add_get_carry bitwidth x y)
     := eq_refl.
   Hint Rewrite @add_get_carry_cps_correct : uncps.
 
   Definition get_borrow_cps {T} (bitwidth : Z) (v : Z) (f : Z * Z -> T)
-    := let '(v, c) := Z.get_borrow bitwidth v in f (v, c).
+    := f (Z.get_borrow bitwidth v).
   Definition get_borrow_cps_correct {T} bitwidth v f
     : @get_borrow_cps T bitwidth v f = f (Z.get_borrow bitwidth v)
     := eq_refl.
   Hint Rewrite @get_borrow_cps_correct : uncps.
   Definition sub_with_get_borrow_cps {T} (bitwidth : Z) (c : Z) (x y : Z) (f : Z * Z -> T) : T
-    := let '(v, c) := Z.sub_with_get_borrow bitwidth c x y in f (v, c).
+    := f (Z.sub_with_get_borrow bitwidth c x y).
   Definition sub_with_get_borrow_cps_correct {T} (bitwidth : Z) (c : Z) (x y : Z) (f : Z * Z -> T)
     : @sub_with_get_borrow_cps T bitwidth c x y f = f (Z.sub_with_get_borrow bitwidth c x y)
     := eq_refl.
   Hint Rewrite @sub_with_get_borrow_cps_correct : uncps.
   Definition sub_get_borrow_cps {T} (bitwidth : Z) (x y : Z) (f : Z * Z -> T) : T
-    := let '(v, c) := Z.sub_get_borrow bitwidth x y in f (v, c).
+    := f (Z.sub_get_borrow bitwidth x y).
   Definition sub_get_borrow_cps_correct {T} (bitwidth : Z) (x y : Z) (f : Z * Z -> T)
     : @sub_get_borrow_cps T bitwidth x y f = f (Z.sub_get_borrow bitwidth x y)
     := eq_refl.