diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-07-18 19:09:46 +0200 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-07-18 19:09:46 +0200 |
| commit | 07ca661557d86b96d1ee0a9b9013d0834158571f (patch) | |
| tree | 78980ce7dbbf836f1d109159332600370ed224e6 /src/Util/ZUtil.v | |
| parent | 0fd535b57b93bada6cc00c2e372f2f94d2768567 (diff) | |
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
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 7 |
1 files changed, 7 insertions, 0 deletions
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. |