From 07ca661557d86b96d1ee0a9b9013d0834158571f Mon Sep 17 00:00:00 2001
From: Jason Gross <jasongross9@gmail.com>
Date: Mon, 18 Jul 2016 19:09:46 +0200
Subject: Move some definitions to Pow2Base (#24)

* Move some definitions to Pow2Base

These definitions don't depend on PseudoMersenneBaseParams, only on
limb_widths, and we'll want them for BarrettReduction / P256.

* Fix for Coq 8.4
---
 src/Util/ZUtil.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src/Util/ZUtil.v')

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 2bcbabaac..a64515427 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -51,6 +51,13 @@ Create HintDb zstrip_div.
 Module Z.
   Definition pow2_mod n i := (n & (Z.ones i)).
 
+  Lemma pow2_mod_spec : forall a b, (0 <= b) -> Z.pow2_mod a b = a mod (2 ^ b).
+  Proof.
+    intros.
+    unfold Z.pow2_mod.
+    rewrite Z.land_ones; auto.
+  Qed.
+
   Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
   Proof. intros; omega. Qed.
 
-- 
cgit v1.2.3