From c48996eafc149d3726293a4e01acdc10e7a15f40 Mon Sep 17 00:00:00 2001
From: Vivien Rindisbacher <56514534+vrindisbacher@users.noreply.github.com>
Date: Wed, 18 Dec 2024 12:52:13 -0800
Subject: [PATCH] Add bit vec ord ops (#952)

* Add bit vec ord ops

* Add tests for each bv ord
---
 crates/flux-middle/src/lib.rs     | 32 +++++++++++
 tests/tests/pos/surface/bv_ord.rs | 89 +++++++++++++++++++++++++++++++
 2 files changed, 121 insertions(+)
 create mode 100644 tests/tests/pos/surface/bv_ord.rs

diff --git a/crates/flux-middle/src/lib.rs b/crates/flux-middle/src/lib.rs
index 42e6c68512..5232c90718 100644
--- a/crates/flux-middle/src/lib.rs
+++ b/crates/flux-middle/src/lib.rs
@@ -274,6 +274,38 @@ pub static THEORY_FUNCS: LazyLock<UnordMap<Symbol, TheoryFunc>> = LazyLock::new(
                 rty::FuncSort::new(vec![BitVec(bv_param0)], BitVec(bv_param0)),
             ),
         },
+        TheoryFunc {
+            name: Symbol::intern("bv_ule"),
+            fixpoint_name: Symbol::intern("bvule"),
+            sort: rty::PolyFuncSort::new(
+                List::singleton(SortParamKind::BvSize),
+                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], Bool),
+            ),
+        },
+        TheoryFunc {
+            name: Symbol::intern("bv_uge"),
+            fixpoint_name: Symbol::intern("bvuge"),
+            sort: rty::PolyFuncSort::new(
+                List::singleton(SortParamKind::BvSize),
+                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], Bool),
+            ),
+        },
+        TheoryFunc {
+            name: Symbol::intern("bv_ugt"),
+            fixpoint_name: Symbol::intern("bvugt"),
+            sort: rty::PolyFuncSort::new(
+                List::singleton(SortParamKind::BvSize),
+                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], Bool),
+            ),
+        },
+        TheoryFunc {
+            name: Symbol::intern("bv_ult"),
+            fixpoint_name: Symbol::intern("bvugt"),
+            sort: rty::PolyFuncSort::new(
+                List::singleton(SortParamKind::BvSize),
+                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], Bool),
+            ),
+        },
         // Set operations
         TheoryFunc {
             name: Symbol::intern("set_empty"),
diff --git a/tests/tests/pos/surface/bv_ord.rs b/tests/tests/pos/surface/bv_ord.rs
new file mode 100644
index 0000000000..efb8dc7276
--- /dev/null
+++ b/tests/tests/pos/surface/bv_ord.rs
@@ -0,0 +1,89 @@
+#[flux::opaque]
+#[flux::refined_by(x: bitvec<32>)]
+pub struct BV32(u32);
+
+impl BV32 {
+    #[flux::trusted]
+    #[flux::sig(fn (u32[@x]) -> BV32[bv_int_to_bv32(x)])]
+    pub fn new(x: u32) -> Self {
+        BV32(x)
+    }
+}
+
+impl PartialEq for BV32 {
+    #[flux::trusted]
+    #[flux::sig(fn (&BV32[@val1], &BV32[@val2]) -> bool[val1 == val2])]
+    fn eq(&self, other: &Self) -> bool {
+        self.0 == other.0
+    }
+
+    #[flux::trusted]
+    #[flux::sig(fn (&BV32[@val1], &BV32[@val2]) -> bool[val1 != val2])]
+    fn ne(&self, other: &Self) -> bool {
+        self.0 != other.0
+    }
+}
+
+impl PartialOrd for BV32 {
+    #[flux::trusted]
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
+        self.0.partial_cmp(&other.0)
+    }
+
+    #[flux::trusted]
+    #[flux::sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_ule(x, y)])]
+    fn le(&self, other: &Self) -> bool {
+        self.0 <= other.0
+    }
+
+    #[flux::trusted]
+    #[flux::sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_ult(x, y)])]
+    fn lt(&self, other: &Self) -> bool {
+        self.0 < other.0
+    }
+
+    #[flux::trusted]
+    #[flux::sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_uge(x, y)])]
+    fn ge(&self, other: &Self) -> bool {
+        self.0 >= other.0
+    }
+
+    #[flux::trusted]
+    #[flux::sig(fn (&BV32[@x], &BV32[@y]) -> bool[bv_ugt(x, y)])]
+    fn gt(&self, other: &Self) -> bool {
+        self.0 > other.0
+    }
+}
+
+#[flux::sig(fn (BV32[@x]) -> bool[bv_ule(x, x)])]
+pub fn trivial_le(x: BV32) -> bool {
+    x <= x
+}
+
+#[flux::sig(fn (BV32[@x]) -> bool[bv_ult(x, x)])]
+pub fn trivial_lt(x: BV32) -> bool {
+    x < x
+}
+
+#[flux::sig(fn (BV32[@x]) -> bool[bv_uge(x, x)])]
+pub fn trivial_ge(x: BV32) -> bool {
+    x <= x
+}
+
+#[flux::sig(fn (BV32[@x]) -> bool[bv_ugt(x, x)])]
+pub fn trivial_gt(x: BV32) -> bool {
+    x < x
+}
+
+#[flux::sig(fn (BV32[@x], BV32[@y]) -> bool[
+    bv_ule(x, bv_int_to_bv32(10))
+    && 
+    bv_uge(y, bv_int_to_bv32(20))
+    &&
+    bv_ult(x, bv_int_to_bv32(11))
+    &&
+    bv_ugt(y, bv_int_to_bv32(21))
+])]
+pub fn real_example(x: BV32, y: BV32) -> bool {
+    x <= BV32::new(10) && y >= BV32::new(20) && x < BV32::new(11) && y > BV32::new(21)
+}