From 354c996a2dc5cfff4f4821ac58f121f44ab7e7f0 Mon Sep 17 00:00:00 2001
From: Nico Lehmann <nico.lehmannm@gmail.com>
Date: Sun, 5 Jan 2025 11:23:04 -0300
Subject: [PATCH] Upstream Bv32

---
 lib/flux-rs/src/bitvec.rs | 159 ++++++++++++++++++++++++++++++++++++++
 lib/flux-rs/src/lib.rs    |   2 +
 2 files changed, 161 insertions(+)
 create mode 100644 lib/flux-rs/src/bitvec.rs

diff --git a/lib/flux-rs/src/bitvec.rs b/lib/flux-rs/src/bitvec.rs
new file mode 100644
index 0000000000..b94135cdfc
--- /dev/null
+++ b/lib/flux-rs/src/bitvec.rs
@@ -0,0 +1,159 @@
+use std::ops::{Add, BitAnd, BitOr, Not, Rem, Shl, Shr, Sub};
+
+use flux_attrs::*;
+
+#[derive(Debug, Clone, Copy, Hash)]
+#[opaque]
+#[refined_by(x: bitvec<32>)]
+pub struct BV32(u32);
+
+#[trusted]
+impl PartialOrd for BV32 {
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
+        self.0.partial_cmp(&other.0)
+    }
+
+    #[sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_ule(x, y)])]
+    fn le(&self, other: &Self) -> bool {
+        self.0 <= other.0
+    }
+
+    #[sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_ult(x, y)])]
+    fn lt(&self, other: &Self) -> bool {
+        self.0 < other.0
+    }
+
+    #[sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_uge(x, y)])]
+    fn ge(&self, other: &Self) -> bool {
+        self.0 >= other.0
+    }
+
+    #[sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_ugt(x, y)])]
+    fn gt(&self, other: &Self) -> bool {
+        self.0 > other.0
+    }
+}
+
+#[trusted]
+impl BV32 {
+    #[sig(fn (BV32[@x], BV32[@y]) -> BV32[bv_add(x, y)])]
+    pub fn wrapping_add(self, other: BV32) -> BV32 {
+        BV32(self.0.wrapping_add(other.0))
+    }
+
+    #[sig(fn (u32[@val]) -> BV32[bv_int_to_bv32(val)])]
+    pub const fn new(value: u32) -> BV32 {
+        BV32(value)
+    }
+}
+
+impl From<u32> for BV32 {
+    #[trusted]
+    #[sig(fn (u32[@val]) -> BV32[bv_int_to_bv32(val)])]
+    fn from(value: u32) -> BV32 {
+        BV32(value)
+    }
+}
+
+impl Into<u32> for BV32 {
+    #[trusted]
+    #[sig(fn (BV32[@val]) -> u32[bv_bv32_to_int(val)])]
+    fn into(self) -> u32 {
+        self.0
+    }
+}
+
+impl Not for BV32 {
+    type Output = BV32;
+
+    #[trusted]
+    #[sig(fn (BV32[@x]) -> BV32[bv_not(x)])]
+    fn not(self) -> BV32 {
+        BV32(!self.0)
+    }
+}
+
+impl BitAnd for BV32 {
+    type Output = BV32;
+
+    #[trusted]
+    #[sig(fn (BV32[@x], BV32[@y]) -> BV32[bv_and(x, y)])]
+    fn bitand(self, rhs: Self) -> BV32 {
+        BV32(self.0 & rhs.0)
+    }
+}
+
+impl BitOr for BV32 {
+    type Output = BV32;
+
+    #[trusted]
+    #[sig(fn (BV32[@x], BV32[@y]) -> BV32[bv_or(x, y)])]
+    fn bitor(self, rhs: Self) -> BV32 {
+        BV32(self.0 | rhs.0)
+    }
+}
+
+impl Shl for BV32 {
+    type Output = BV32;
+
+    #[trusted]
+    #[sig(fn (BV32[@x], BV32[@y]) -> BV32[bv_shl(x, y)])]
+    fn shl(self, rhs: Self) -> BV32 {
+        BV32(self.0 << rhs.0)
+    }
+}
+
+impl Shr for BV32 {
+    type Output = BV32;
+
+    #[trusted]
+    #[sig(fn (BV32[@x], BV32[@y]) -> BV32[bv_lshr(x, y)])]
+    fn shr(self, rhs: Self) -> BV32 {
+        BV32(self.0 >> rhs.0)
+    }
+}
+
+impl Add for BV32 {
+    type Output = BV32;
+
+    #[trusted]
+    #[sig(fn (BV32[@val1], BV32[@val2]) -> BV32[bv_add(val1, val2)])]
+    fn add(self, rhs: Self) -> BV32 {
+        BV32(self.0 + rhs.0)
+    }
+}
+
+impl Sub for BV32 {
+    type Output = BV32;
+
+    #[trusted]
+    #[sig(fn (BV32[@val1], BV32[@val2]) -> BV32[bv_sub(val1, val2)])]
+    fn sub(self, rhs: Self) -> BV32 {
+        BV32(self.0.wrapping_add(!rhs.0))
+    }
+}
+
+impl Rem for BV32 {
+    type Output = BV32;
+
+    #[trusted]
+    #[sig(fn (BV32[@val1], BV32[@val2]) -> BV32[bv_urem(val1, val2)])]
+    fn rem(self, rhs: Self) -> BV32 {
+        BV32(self.0 & rhs.0)
+    }
+}
+
+#[trusted]
+impl PartialEq for BV32 {
+    #[sig(fn (&BV32[@val1], &BV32[@val2]) -> bool[val1 == val2])]
+    fn eq(&self, other: &Self) -> bool {
+        self.0 == other.0
+    }
+
+    #[sig(fn (&BV32[@val1], &BV32[@val2]) -> bool[val1 != val2])]
+    fn ne(&self, other: &Self) -> bool {
+        self.0 != other.0
+    }
+}
+
+impl Eq for BV32 {}
diff --git a/lib/flux-rs/src/lib.rs b/lib/flux-rs/src/lib.rs
index a9b572e1e5..a157b2c3f2 100644
--- a/lib/flux-rs/src/lib.rs
+++ b/lib/flux-rs/src/lib.rs
@@ -1,3 +1,5 @@
+pub mod bitvec;
+
 pub use flux_attrs::*;
 
 #[sig(fn(bool[true]) )]