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.

2 files changed, 19 insertions, 3 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.
diff --git a/src/Util/ZUtil/MulSplit.v b/src/Util/ZUtil/MulSplit.v
index e0448fe69..2f6805446 100644
--- a/src/Util/ZUtil/MulSplit.v
+++ b/src/Util/ZUtil/MulSplit.v
@@ -1,10 +1,22 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.Tactics.BreakMatch.
 Local Open Scope Z_scope.
 
 Module Z.
-  Lemma mul_split_mod s x y : fst (Z.mul_split s x y)  = (x * y) mod s.
+  Lemma mul_split_at_bitwidth_mod bw x y : fst (Z.mul_split_at_bitwidth bw x y)  = (x * y) mod 2^bw.
   Proof. reflexivity. Qed.
-  Lemma mul_split_div s x y : snd (Z.mul_split s x y)  = (x * y) / s.
+  Lemma mul_split_at_bitwidth_div bw x y : snd (Z.mul_split_at_bitwidth bw x y)  = (x * y) / 2^bw.
   Proof. reflexivity. Qed.
+  Lemma mul_split_mod s x y : fst (Z.mul_split s x y)  = (x * y) mod s.
+  Proof.
+    unfold Z.mul_split; break_match; Z.ltb_to_lt;
+      [ rewrite mul_split_at_bitwidth_mod; congruence | reflexivity ].
+  Qed.
+  Lemma mul_split_div s x y : snd (Z.mul_split s x y)  = (x * y) / s.
+  Proof.
+    unfold Z.mul_split; break_match; Z.ltb_to_lt;
+      [ rewrite mul_split_at_bitwidth_div; congruence | reflexivity ].
+  Qed.
 End Z.