From 561bc64d063b20160b405cbef7003d1b7fba4088 Mon Sep 17 00:00:00 2001
From: Vivien Rindisbacher <56514534+vrindisbacher@users.noreply.github.com>
Date: Mon, 6 Jan 2025 11:56:29 -0800
Subject: [PATCH] fix bv ord ops (#967)

---
 crates/flux-middle/src/lib.rs     |  2 +-
 tests/tests/pos/surface/bv_ord.rs | 43 +++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+), 1 deletion(-)

diff --git a/crates/flux-middle/src/lib.rs b/crates/flux-middle/src/lib.rs
index 5232c90718..2cad2d34f8 100644
--- a/crates/flux-middle/src/lib.rs
+++ b/crates/flux-middle/src/lib.rs
@@ -300,7 +300,7 @@ pub static THEORY_FUNCS: LazyLock<UnordMap<Symbol, TheoryFunc>> = LazyLock::new(
         },
         TheoryFunc {
             name: Symbol::intern("bv_ult"),
-            fixpoint_name: Symbol::intern("bvugt"),
+            fixpoint_name: Symbol::intern("bvult"),
             sort: rty::PolyFuncSort::new(
                 List::singleton(SortParamKind::BvSize),
                 rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], Bool),
diff --git a/tests/tests/pos/surface/bv_ord.rs b/tests/tests/pos/surface/bv_ord.rs
index efb8dc7276..1eebf53d87 100644
--- a/tests/tests/pos/surface/bv_ord.rs
+++ b/tests/tests/pos/surface/bv_ord.rs
@@ -1,3 +1,5 @@
+use std::ops::{Add, Sub};
+
 #[flux::opaque]
 #[flux::refined_by(x: bitvec<32>)]
 pub struct BV32(u32);
@@ -10,6 +12,26 @@ impl BV32 {
     }
 }
 
+impl Add for BV32 {
+    type Output = BV32;
+
+    #[flux_rs::trusted]
+    #[flux_rs::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;
+
+    #[flux_rs::trusted]
+    #[flux_rs::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 PartialEq for BV32 {
     #[flux::trusted]
     #[flux::sig(fn (&BV32[@val1], &BV32[@val2]) -> bool[val1 == val2])]
@@ -87,3 +109,24 @@ pub fn trivial_gt(x: BV32) -> bool {
 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)
 }
+
+
+#[flux_rs::sig(fn (BV32[@x], BV32[@y]) -> bool[true] requires bv_ult(x, y) && bv_ugt(x, bv_int_to_bv32(0x20)) && bv_ult(y, bv_int_to_bv32(0xFF)))]
+fn lt_imp(x: BV32, y: BV32) -> bool {
+    x - BV32::new(0x20) < y + BV32::new(0x20)
+}
+
+#[flux_rs::sig(fn (BV32[@x], BV32[@y]) -> bool[true] requires bv_ule(x, y) && bv_uge(x, bv_int_to_bv32(0x20)) && bv_ule(y, bv_int_to_bv32(0xFF)))]
+fn le_imp(x: BV32, y: BV32) -> bool {
+    x - BV32::new(0x20) <= y + BV32::new(0x20)
+}
+
+#[flux_rs::sig(fn (BV32[@x], BV32[@y]) -> bool[true] requires bv_ugt(x, y) && bv_ugt(y, bv_int_to_bv32(0x20)) && bv_ult(x, bv_int_to_bv32(0xFF)))]
+fn gt_imp(x: BV32, y: BV32) -> bool {
+    x + BV32::new(0x20) > y - BV32::new(0x20)
+}
+
+#[flux_rs::sig(fn (BV32[@x], BV32[@y]) -> bool[true] requires bv_uge(x, y) && bv_uge(y, bv_int_to_bv32(0x20)) && bv_ule(x, bv_int_to_bv32(0xFF)))]
+fn ge_imp(x: BV32, y: BV32) -> bool {
+    x + BV32::new(0x20) >= y - BV32::new(0x20)
+}