Add mul_split_at_bitwidth, define things in terms of that

This will make it easier on the reflective machinery, because it won't
have to carry around such large constants.

1 files changed, 5 insertions, 1 deletions

diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index ff15dc83c..fb7754a7a 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -35,6 +35,10 @@ Module Z.
        then add_get_carry (Z.log2 bound) x y
        else ((x + y) mod bound, (x + y) / bound).
 
+  Definition mul_split_at_bitwidth (bitwidth : Z) (x y : Z) : Z * Z
+    := ((x * y) mod 2^bitwidth, (x * y) / 2^bitwidth).
   Definition mul_split (s x y : Z) : Z * Z
-    := ((x * y) mod s, (x * y) / s).
+    := if s =? 2^Z.log2 s
+       then mul_split_at_bitwidth (Z.log2 s) x y
+       else ((x * y) mod s, (x * y) / s).
 End Z.