fix bv ord ops

flux-rs · Jan 6, 2025 · aae509c · aae509c
1 parent 50e349d
commit aae509c
Show file tree

Hide file tree

Showing 2 changed files with 44 additions and 1 deletion.
diff --git 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
@@ -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)
+}