diff options
-rw-r--r-- | _CoqProject | 2 | ||||
-rw-r--r-- | src/Util/ZUtil/CC.v | 32 | ||||
-rw-r--r-- | src/Util/ZUtil/Definitions.v | 13 | ||||
-rw-r--r-- | src/Util/ZUtil/Rshi.v | 20 |
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 |