Add new assembly-mimicking operations rshi, cc_m, and cc_l

4 files changed, 67 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 4e5f33519..faecc2fbf 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6567,6 +6567,7 @@ src/Util/ZRange/CornersMonotoneBounds.v
 src/Util/ZRange/Operations.v
 src/Util/ZUtil/AddGetCarry.v
 src/Util/ZUtil/AddModulo.v
+src/Util/ZUtil/CC.v
 src/Util/ZUtil/CPS.v
 src/Util/ZUtil/Definitions.v
 src/Util/ZUtil/Div.v
@@ -6582,6 +6583,7 @@ src/Util/ZUtil/Notations.v
 src/Util/ZUtil/Peano.v
 src/Util/ZUtil/Pow2Mod.v
 src/Util/ZUtil/Quot.v
+src/Util/ZUtil/Rshi.v
 src/Util/ZUtil/Sgn.v
 src/Util/ZUtil/Stabilization.v
 src/Util/ZUtil/Tactics.v
diff --git a/src/Util/ZUtil/CC.v b/src/Util/ZUtil/CC.v
new file mode 100644
index 000000000..fb2fb1b93
--- /dev/null
+++ b/src/Util/ZUtil/CC.v
@@ -0,0 +1,32 @@
+Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Hints.PullPush.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Local Open Scope Z_scope.
+
+Module Z.
+  Hint Rewrite Z.log2_pow2 Z.pow_1_r using solve [auto using Z.log2_nonneg with zarith] : push_Zpow.
+
+  Lemma cc_m_eq : forall s x, 2 < s -> Z.cc_m s x = x / (s / 2).
+  Proof.
+    intros; cbv [Z.cc_m].
+    assert (1 <= Z.log2 s) by (rewrite <-Z.log2_2; auto using Z.log2_le_mono with lia).
+    break_match; [ | reflexivity ].
+    match goal with H : _ = s |- _ => rewrite <-H end.
+    autorewrite with Zshift_to_pow push_Zpow.
+    reflexivity.
+  Qed.
+
+  Lemma cc_m_small : forall s x, 2 < s -> s mod 2 = 0 -> 0 <= x < s -> 0 <= Z.cc_m s x < 2.
+  Proof.
+    intros. rewrite cc_m_eq by auto.
+    repeat match goal with
+           | _ => split
+           | _ => apply Z.div_lt_upper_bound
+           | _ => solve [Z.zero_bounds]
+           end.
+    Z.div_mod_to_quot_rem; lia.
+  Qed.
+End Z.
\ No newline at end of file
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index 66fc7f558..2c87a9497 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -13,6 +13,19 @@ Module Z.
   Definition add_modulo x y modulus :=
     if (modulus <=? x + y) then (x + y) - modulus else (x + y).
 
+  (* most significant bit *)
+  Definition cc_m s x := if dec (2 ^ (Z.log2 s) = s) then x >> (Z.log2 s - 1) else x / (s / 2).
+
+  (* least significant bit *)
+  Definition cc_l x := Z.land x (Z.ones 1).
+
+  (* two-register right shift *)
+  Definition rshi s hi lo n :=
+       let k := Z.log2 s in
+       if dec (2 ^ k = s)
+       then ((lo + (hi << k)) >> n) &' (Z.ones k)
+       else ((lo + hi * s) >> n) mod s.
+
   Definition get_carry (bitwidth : Z) (v : Z) : Z * Z
     := (v mod 2^bitwidth, v / 2^bitwidth).
   Definition add_with_carry (c : Z) (x y : Z) : Z
diff --git a/src/Util/ZUtil/Rshi.v b/src/Util/ZUtil/Rshi.v
new file mode 100644
index 000000000..9a1d8a20b
--- /dev/null
+++ b/src/Util/ZUtil/Rshi.v
@@ -0,0 +1,20 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Hints.PullPush.
+Local Open Scope Z_scope.
+
+Module Z.
+     Lemma rshi_correct : forall s a b n, 0 <= n -> s <> 0 ->
+         Z.rshi s a b n = ((b + a * s) / 2 ^ n) mod s.
+     Proof.
+       cbv [Z.rshi]; intros. pose proof (Z.log2_nonneg s).
+       break_match;
+         repeat match goal with
+              | H : _ = s |- _ => rewrite H
+              | _ => rewrite Z.land_ones by auto with zarith
+              | _ => progress autorewrite with Zshift_to_pow push_Zpow
+              | _ => reflexivity
+              end.
+     Qed.
+End Z.
\ No newline at end of file