Add Z.bneg, Z.lneg

1 files changed, 12 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index 373c71763..82b065394 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -76,4 +76,16 @@ Module Z.
     := if s =? 2^Z.log2 s
        then mul_split_at_bitwidth (Z.log2 s) x y
        else ((x * y) mod s, (x * y) / s).
+
+  (** Boolean negation *)
+  Definition bneg (v : Z) : Z
+    := if dec (v = 0) then 1 else 0.
+
+  (** Logical negation, modulo a bitwidth *)
+  Definition lneg (bitwidth : Z) (v : Z) : Z
+    := (-v) mod 2^bitwidth.
+  Definition lneg_full (s : Z) (v : Z) : Z
+    := if s =? 2^Z.log2 s
+       then lneg (Z.log2 s) v
+       else (-v) mod s.
 End Z.