DNM: QED team WIP branch

src/expr/src/scalar/func.rs

@@ -1501,7 +1501,7 @@ fn mul_numeric<'a>(a: Datum<'a>, b: Datum<'a>) -> Result<Datum<'a>, EvalError> {
 fn mul_interval<'a>(a: Datum<'a>, b: Datum<'a>) -> Result<Datum<'a>, EvalError> {
     a.unwrap_interval()
         .checked_mul(b.unwrap_float64())
-        .ok_or_else(|| EvalError::IntervalOutOfRange(format!("{a} * {b}").into()))
+        .ok_or_else(|| unreachable!())
         .map(Datum::from)
 }
 
@@ -1701,7 +1701,7 @@ fn div_interval<'a>(a: Datum<'a>, b: Datum<'a>) -> Result<Datum<'a>, EvalError>
     } else {
         a.unwrap_interval()
             .checked_div(b)
-            .ok_or_else(|| EvalError::IntervalOutOfRange(format!("{a} / {b}").into()))
+            .ok_or_else(|| unreachable!())
             .map(Datum::from)
     }
 }
@@ -10030,3 +10030,150 @@ mod test {
         proptest_binary(BinaryFunc::Left, &arena, &str_datums, &i32_datums);
     }
 }
+
+mod kani_test {
+    use std::mem::ManuallyDrop;
+
+    use ordered_float::OrderedFloat;
+
+    use crate::func::binary::EagerBinaryFunc;
+
+    use super::*;
+
+    fn check_uniqueness<F>(func: F)
+    where
+        F: for<'a> EagerUnaryFunc<'a>,
+        for<'a> <F as EagerUnaryFunc<'a>>::Input: PartialEq + kani::Arbitrary,
+        for<'a> <F as EagerUnaryFunc<'a>>::Output: PartialEq,
+    {
+        let a1: F::Input = kani::any();
+        let a2: F::Input = kani::any();
+        kani::assume(a1 != a2);
+        let arena = ManuallyDrop::new(RowArena::new());
+
+        let r1 = func.call(a1).into_result(&*arena);
+        let r2 = func.call(a2).into_result(&*arena);
+
+        match (r1, r2) {
+            (Ok(r1), Ok(r2)) => {
+                assert_ne!(r1, r2);
+            }
+            a => {
+                std::mem::forget(a);
+            }
+        }
+        std::mem::forget(func);
+    }
+
+    fn check_monotone_binary_first_arg_float_float<F>(func: F)
+    where
+        F: for<'a> EagerBinaryFunc<'a, Input1 = Datum<'a>, Input2 = Datum<'a>>,
+    {
+        let a1 = OrderedFloat(kani::any::<f64>());
+        let a2 = OrderedFloat(kani::any::<f64>());
+        let a3 = OrderedFloat(kani::any::<f64>());
+        let b = OrderedFloat(kani::any::<f64>());
+        kani::assume(a1 <= a2);
+        kani::assume(a2 <= a3);
+        let arena = ManuallyDrop::new(RowArena::new());
+
+        let r1 = func.call(a1.into(), b.into(), &*arena).into_result(&*arena);
+        let r2 = func.call(a2.into(), b.into(), &*arena).into_result(&*arena);
+        let r3 = func.call(a3.into(), b.into(), &*arena).into_result(&*arena);
+
+        match (&r1, &r2, &r3) {
+            (Ok(Datum::Float64(r1)), Ok(Datum::Float64(r2)), Ok(Datum::Float64(r3))) => {
+                assert!((r1 <= r2 && r2 <= r3) || (r1 >= r2 && r2 >= r3));
+            }
+            _ => (),
+        }
+        std::mem::forget(func);
+        std::mem::forget((r1, r2, r3));
+    }
+
+    fn check_monotone_binary_first_arg_interval_float<F>(func: F)
+    where
+        F: for<'a> EagerBinaryFunc<'a, Input1 = Datum<'a>, Input2 = Datum<'a>>,
+    {
+        let a1 = kani::any::<Interval>();
+        let a2 = kani::any::<Interval>();
+        let a3 = kani::any::<Interval>();
+        let b = OrderedFloat(kani::any::<f64>());
+        kani::assume(a1 <= a2);
+        kani::assume(a2 <= a3);
+        let arena = ManuallyDrop::new(RowArena::new());
+
+        let r1 = func.call(a1.into(), b.into(), &*arena).into_result(&*arena);
+        let r2 = func.call(a2.into(), b.into(), &*arena).into_result(&*arena);
+        let r3 = func.call(a3.into(), b.into(), &*arena).into_result(&*arena);
+
+        match (&r1, &r2, &r3) {
+            (Ok(Datum::Interval(r1)), Ok(Datum::Interval(r2)), Ok(Datum::Interval(r3))) => {
+                assert!((r1 <= r2 && r2 <= r3) || (r1 >= r2 && r2 >= r3));
+            }
+            _ => (),
+        }
+        std::mem::forget(func);
+        std::mem::forget((r1, r2, r3));
+    }
+
+    #[kani::proof]
+    #[kani::unwind(5)]
+    fn negint64_preserves_uniqueness() {
+        check_uniqueness(NegInt64);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(5)]
+    fn negint16_preserves_uniqueness() {
+        check_uniqueness(NegInt16);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(5)]
+    fn negint32_preserves_uniqueness() {
+        check_uniqueness(NegInt32);
+    }
+
+    // FAILS
+    #[kani::proof]
+    #[kani::unwind(5)]
+    fn add_float64_is_monotone_in_first_arg() {
+        check_monotone_binary_first_arg_float_float(AddFloat64);
+    }
+
+    // FAILS
+    #[kani::proof]
+    #[kani::unwind(5)]
+    fn sub_float64_is_monotone_in_first_arg() {
+        check_monotone_binary_first_arg_float_float(SubFloat64);
+    }
+
+    // FAILS
+    #[kani::proof]
+    #[kani::unwind(5)]
+    fn mul_float64_is_monotone_in_first_arg() {
+        check_monotone_binary_first_arg_float_float(MulFloat64);
+    }
+
+    // FAILS
+    #[kani::proof]
+    #[kani::unwind(5)]
+    fn div_float64_is_monotone_in_first_arg() {
+        check_monotone_binary_first_arg_float_float(DivFloat64);
+    }
+
+    // FAILS
+    #[kani::proof]
+    #[kani::unwind(10)]
+    fn mul_interval_is_monotone_in_first_arg() {
+        check_monotone_binary_first_arg_interval_float(MulInterval);
+    }
+
+    // FAILS
+    #[kani::proof]
+    #[kani::unwind(5)]
+    fn div_interval_is_monotone_in_first_arg() {
+        check_monotone_binary_first_arg_interval_float(DivInterval);
+    }
+}

src/ore/Cargo.toml

@@ -125,7 +125,7 @@ async = [
     "dep:tracing",
 ]
 bytes = ["dep:bytes", "compact_bytes", "smallvec", "smallvec/const_generics", "region", "tracing"]
-network = ["async", "dep:bytes", "smallvec", "tonic", "dep:tracing"]
+network = ["async", "dep:bytes", "smallvec", "tonic", "dep:tracing", "tokio/fs"]
 panic = ["sentry-panic"]
 process = ["libc"]
 region = ["dep:lgalloc", "dep:bytemuck"]

src/repr/src/adt/interval.rs

@@ -28,7 +28,7 @@ include!(concat!(env!("OUT_DIR"), "/mz_repr.adt.interval.rs"));
 /// An interval of time meant to express SQL intervals.
 ///
 /// Obtained by parsing an `INTERVAL '<value>' <unit> [TO <precision>]`.
-#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Hash, Deserialize)]
+#[derive(Debug, Clone, Copy, Serialize, Hash, Deserialize, kani::Arbitrary)]
 pub struct Interval {
     /// A possibly negative number of months for field types like `YEAR`
     pub months: i32,
@@ -43,6 +43,26 @@ pub struct Interval {
     pub micros: i64,
 }
 
+impl PartialEq for Interval {
+    fn eq(&self, other: &Self) -> bool {
+        self.as_microseconds() == other.as_microseconds()
+    }
+}
+
+impl Eq for Interval {}
+
+impl PartialOrd for Interval {
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
+        Some(self.cmp(other))
+    }
+}
+
+impl Ord for Interval {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.as_microseconds().cmp(&other.as_microseconds())
+    }
+}
+
 impl Default for Interval {
     fn default() -> Self {
         Self {
@@ -221,8 +241,8 @@ impl Interval {
 
         if micros.is_nan()
             || micros.is_infinite()
-            || Numeric::from(micros) < Numeric::from(i64::MIN)
-            || Numeric::from(micros) > Numeric::from(i64::MAX)
+            || micros < i64::MIN as f64
+            || micros > i64::MAX as f64
         {
             return None;
         }