Unfold Z.mul_split_at_bitwidth for reification

Also reimplement it with a shift and a mask

5 files changed, 26 insertions, 4 deletions

diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
index 3c3ac61b2..72bbfb03a 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
@@ -9,6 +9,7 @@ Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.ZUtil.Stabilization.
+Require Import Crypto.Util.ZUtil.MulSplit.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.FixedWordSizesEquality.
@@ -348,8 +349,10 @@ Proof.
     [ apply is_bounded_by_truncation_bounds..
     | split; ibbio_do_cbv;
       [ eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v mod _)) (v:=ZToInterp _);
+        [ .. | cbn -[Z.mul_split_at_bitwidth]; rewrite Z.mul_split_at_bitwidth_mod ];
         ibbio_prefin_by_apply
       | eapply is_bounded_by_compose with (T1:=TZ) (f_v := fun v => ZToInterp (v / _))   (v:=ZToInterp _);
+        [ .. | cbn -[Z.mul_split_at_bitwidth]; rewrite Z.mul_split_at_bitwidth_div ];
         ibbio_prefin_by_apply ]
     | apply is_bounded_by_truncation_bounds
     | split; ibbio_do_cbv;
diff --git a/src/Specific/MontgomeryP256.v b/src/Specific/MontgomeryP256.v
index cda758108..09e93ef81 100644
--- a/src/Specific/MontgomeryP256.v
+++ b/src/Specific/MontgomeryP256.v
@@ -22,6 +22,10 @@ Proof.
   eapply (lift2_sig (fun A B c => c = (redc (r:=r)(R_numlimbs:=4) p256 A B 1)
                            )); eexists.
   cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth runtime_add runtime_mul Let_In].
+  (* TODO: is there a better way to do this?  Maybe make runtime_mul_split_at_bitwidth? *)
+  cbv [Definitions.Z.mul_split_at_bitwidth].
+  change Z.mul with runtime_mul; change Z.shiftr with runtime_shr; change Z.land with runtime_and.
+  cbv -[Definitions.Z.add_get_carry runtime_add runtime_mul runtime_and runtime_shr Let_In]. (* unfold Z.ones *)
   (*
   cbv [
       r wt sz p256
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index fb7d0133a..01e125e00 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -26,7 +26,6 @@ Require Export Crypto.Util.ZUtil.Sgn.
 Require Export Crypto.Util.ZUtil.Tactics.
 Require Export Crypto.Util.ZUtil.Testbit.
 Require Export Crypto.Util.ZUtil.ZSimplify.
-Require Export Crypto.Util.ZUtil.Z2Nat.
 Import Nat.
 Local Open Scope Z.
 
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index fb7754a7a..f6892be13 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -1,6 +1,7 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.ZUtil.Notations.
+Require Import Crypto.Util.LetIn.
 Local Open Scope Z_scope.
 
 Module Z.
@@ -36,7 +37,15 @@ Module Z.
        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).
+    := dlet xy := x * y in
+        (match bitwidth with
+         | Z.pos _ | Z0 => xy &' Z.ones bitwidth
+         | Z.neg _ => xy mod 2^bitwidth
+         end,
+         match bitwidth with
+         | Z.pos _ | Z0 => xy >> bitwidth
+         | Z.neg _ => xy / 2^bitwidth
+         end).
   Definition mul_split (s x y : Z) : Z * Z
     := if s =? 2^Z.log2 s
        then mul_split_at_bitwidth (Z.log2 s) x y
diff --git a/src/Util/ZUtil/MulSplit.v b/src/Util/ZUtil/MulSplit.v
index 2f6805446..1cc6b7af0 100644
--- a/src/Util/ZUtil/MulSplit.v
+++ b/src/Util/ZUtil/MulSplit.v
@@ -1,4 +1,5 @@
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
 Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.Tactics.BreakMatch.
@@ -6,9 +7,15 @@ Local Open Scope Z_scope.
 
 Module Z.
   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.
+  Proof.
+    unfold Z.mul_split_at_bitwidth, LetIn.Let_In; break_innermost_match; Z.ltb_to_lt; try reflexivity;
+      apply Z.land_ones; lia.
+  Qed.
   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.
+  Proof.
+    unfold Z.mul_split_at_bitwidth, LetIn.Let_In; break_innermost_match; Z.ltb_to_lt; try reflexivity;
+      apply Z.shiftr_div_pow2; lia.
+  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;