aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-04-02 17:51:17 -0400
committerGravatar Jason Gross <jgross@mit.edu>2019-04-02 17:51:17 -0400
commitef3ce824f87fd11eed78a13a884579499a8ffc53 (patch)
treea6af1f34cffc7dedee718e263f6e5d2751eaf28c /src/Util
parentbacfa270c0c492ef8518d360d87e46cee292474f (diff)
Add Z.combine_at_bitwidth
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/ZUtil/Combine.v34
-rw-r--r--src/Util/ZUtil/Definitions.v3
2 files changed, 37 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Combine.v b/src/Util/ZUtil/Combine.v
new file mode 100644
index 000000000..3ac4179c5
--- /dev/null
+++ b/src/Util/ZUtil/Combine.v
@@ -0,0 +1,34 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Notations.
+Local Open Scope Z_scope.
+
+Module Z.
+ Lemma combine_at_bitwidth_correct bitwidth lo hi
+ : Z.combine_at_bitwidth bitwidth lo hi = lo + (hi << bitwidth).
+ Proof. reflexivity. Qed.
+
+ Lemma combine_at_bitwidth_Proper bitwidth
+ : Proper (Z.le ==> Z.le ==> Z.le) (Z.combine_at_bitwidth bitwidth).
+ Proof.
+ cbv [Proper respectful]; intros; rewrite !combine_at_bitwidth_correct.
+ destruct bitwidth as [|bitwidth|bitwidth];
+ [ | assert (0 <= 2^Z.pos bitwidth) by (apply Z.pow_nonneg; lia).. ];
+ rewrite ?Z.shiftl_mul_pow2, ?Z.shiftl_div_pow2, ?Z.pow_0_r by lia; cbn [Z.opp]; try nia;
+ Z.div_mod_to_quot_rem; nia.
+ Qed.
+ Hint Resolve combine_at_bitwidth_Proper : zarith.
+
+ Lemma combine_at_bitwidth_Proper1 bitwidth x
+ : Proper (Z.le ==> Z.le) (Z.combine_at_bitwidth bitwidth x).
+ Proof. repeat intro; eapply combine_at_bitwidth_Proper; (eassumption + reflexivity). Qed.
+ Hint Resolve combine_at_bitwidth_Proper1 : zarith.
+
+ Lemma combine_at_bitwidth_Proper2 bitwidth x
+ : Proper (Z.le ==> Z.le) (fun y => Z.combine_at_bitwidth bitwidth y x).
+ Proof. repeat intro; eapply combine_at_bitwidth_Proper; (eassumption + reflexivity). Qed.
+ Hint Resolve combine_at_bitwidth_Proper2 : zarith.
+End Z.
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index 8fe5772f5..a5ac1a95b 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -85,6 +85,9 @@ Module Z.
then mul_split_at_bitwidth (Z.log2 s) x y
else ((x * y) mod s, (x * y) / s).
+ Definition combine_at_bitwidth (bitwidth lo hi : Z) : Z
+ := lo + (hi << bitwidth).
+
(** if positive, round up to 2^k-1 (0b11111....); if negative, round down to -2^k (0b...111000000...) *)
Definition round_lor_land_bound (x : Z) : Z
:= if (0 <=? x)%Z