creusot_std/std/

cmp.rs

use crate::{partial_ord_laws_impl, prelude::*};
use core::cmp::*;

#[cfg(creusot)]
pub use creusot_std_proc::PartialEq;

#[cfg(not(creusot))]
pub use core::cmp::PartialEq;

extern_spec! {
    mod core {
        mod cmp {
            trait PartialEq<Rhs: ?Sized + DeepModel<DeepModelTy = Self::DeepModelTy>>: DeepModel {
                #[ensures(result == (self.deep_model() == rhs.deep_model()))]
                fn eq(&self, rhs: &Rhs) -> bool;

                #[ensures(result == (self.deep_model() != rhs.deep_model()))]
                fn ne(&self, rhs: &Rhs) -> bool {
                    !(self == rhs)
                }
            }

            trait PartialOrd<Rhs: ?Sized + DeepModel<DeepModelTy = Self::DeepModelTy>>:
                DeepModel<DeepModelTy: PartialOrdLogic>
            {
                #[ensures(result == (*self).deep_model().partial_cmp_log((*rhs).deep_model()))]
                fn partial_cmp(&self, rhs: &Rhs) -> Option<Ordering>;

                #[ensures(result == (self.deep_model() < other.deep_model()))]
                fn lt(&self, other: &Rhs) -> bool {
                    match self.partial_cmp(other) {
                        Some(Ordering::Less) => true,
                        _ => false,
                    }
                }

                #[ensures(result == (self.deep_model() <= other.deep_model()))]
                fn le(&self, other: &Rhs) -> bool {
                    match self.partial_cmp(other) {
                        Some(Ordering::Less | Ordering::Equal) => true,
                        _ => false,
                    }
                }

                #[ensures(result == (self.deep_model() > other.deep_model()))]
                fn gt(&self, other: &Rhs) -> bool {
                    match self.partial_cmp(other) {
                        Some(Ordering::Greater) => true,
                        _ => false,
                    }
                }

                #[ensures(result == (self.deep_model() >= other.deep_model()))]
                fn ge(&self, other: &Rhs) -> bool {
                    match self.partial_cmp(other) {
                        Some(Ordering::Greater | Ordering::Equal) => true,
                        _ => false,
                    }
                }
            }

            trait Ord: DeepModel<DeepModelTy: OrdLogic> {
                #[ensures(result == (*self).deep_model().cmp_log((*rhs).deep_model()))]
                fn cmp(&self, rhs: &Self) -> Ordering;

                #[ensures(result.deep_model() >= self.deep_model())]
                #[ensures(result.deep_model() >= o.deep_model())]
                #[ensures(result == self || result == o)]
                #[ensures(self.deep_model() <= o.deep_model() ==> result == o)]
                #[ensures(o.deep_model() < self.deep_model() ==> result == self)]
                fn max(self, o: Self) -> Self where Self: Sized {
                    let _ = snapshot!(Self::DeepModelTy::lt_log_total);
                    if self <= o { o } else { self }
                }

                #[ensures(result.deep_model() <= self.deep_model())]
                #[ensures(result.deep_model() <= o.deep_model())]
                #[ensures(result == self || result == o)]
                #[ensures(self.deep_model() < o.deep_model() ==> result == self)]
                #[ensures(o.deep_model() <= self.deep_model() ==> result == o)]
                fn min(self, o: Self) -> Self where Self: Sized {
                    let _ = snapshot!(Self::DeepModelTy::lt_log_total);
                    if self < o { self } else { o }
                }

                #[requires(min.deep_model() <= max.deep_model())]
                #[ensures(result.deep_model() >= min.deep_model())]
                #[ensures(result.deep_model() <= max.deep_model())]
                #[ensures(result == self || result == min || result == max)]
                #[ensures(if self.deep_model() > max.deep_model() {
                    result == max
                } else if self.deep_model() < min.deep_model() {
                    result == min
                } else { result == self })]
                fn clamp(self, min: Self, max: Self) -> Self where Self: Sized {
                    let _ = snapshot!(Self::DeepModelTy::lt_log_total);
                    if self > max { max } else if self < min { min } else { self }
                }
            }

            #[ensures(result.deep_model() >= v1.deep_model())]
            #[ensures(result.deep_model() >= v2.deep_model())]
            #[ensures(result == v1 || result == v2)]
            #[ensures(v1.deep_model() <= v2.deep_model() ==> result == v2)]
            #[ensures(v2.deep_model() < v1.deep_model() ==> result == v1)]
            fn max<T: Ord + DeepModel<DeepModelTy: OrdLogic>>(v1: T, v2: T) -> T {
                <T as Ord>::max(v1, v2)
            }

            #[ensures(result.deep_model() <= v1.deep_model())]
            #[ensures(result.deep_model() <= v2.deep_model())]
            #[ensures(result == v1 || result == v2)]
            #[ensures(v1.deep_model() < v2.deep_model() ==> result == v1)]
            #[ensures(v2.deep_model() <= v1.deep_model() ==> result == v2)]
            fn min<T: Ord + DeepModel<DeepModelTy: OrdLogic>>(v1: T, v2: T) -> T {
                <T as Ord>::min(v1, v2)
            }
        }
    }
}

// Make equality and comparisons on integers pure operations.
macro_rules! impl_cmp_int {
    ($($t:ty)*) => {
$(

extern_spec! {
    impl PartialEq<$t> for $t {
        #[check(ghost)]
        #[ensures(result == (self.deep_model() == rhs.deep_model()))]
        fn eq(&self, rhs: &$t) -> bool;

        #[check(ghost)]
        #[ensures(result == (self.deep_model() != rhs.deep_model()))]
        fn ne(&self, rhs: &$t) -> bool;
    }

    impl PartialOrd<$t> for $t
    {
        #[check(ghost)]
        #[ensures(result == (*self).deep_model().partial_cmp_log((*rhs).deep_model()))]
        fn partial_cmp(&self, rhs: &$t) -> Option<Ordering>;

        #[check(ghost)]
        #[ensures(result == (self.deep_model() < other.deep_model()))]
        fn lt(&self, other: &$t) -> bool {
            match self.partial_cmp(other) {
                Some(Ordering::Less) => true,
                _ => false,
            }
        }

        #[check(ghost)]
        #[ensures(result == (self.deep_model() <= other.deep_model()))]
        fn le(&self, other: &$t) -> bool {
            match self.partial_cmp(other) {
                Some(Ordering::Less | Ordering::Equal) => true,
                _ => false,
            }
        }

        #[check(ghost)]
        #[ensures(result == (self.deep_model() > other.deep_model()))]
        fn gt(&self, other: &$t) -> bool {
            match self.partial_cmp(other) {
                Some(Ordering::Greater) => true,
                _ => false,
            }
        }

        #[check(ghost)]
        #[ensures(result == (self.deep_model() >= other.deep_model()))]
        fn ge(&self, other: &$t) -> bool {
            match self.partial_cmp(other) {
                Some(Ordering::Greater | Ordering::Equal) => true,
                _ => false,
            }
        }
    }

    impl Ord for $t
    {
        #[check(ghost)]
        #[ensures(result == (*self).deep_model().cmp_log((*rhs).deep_model()))]
        fn cmp(&self, rhs: &Self) -> Ordering;

        // TODO: cannot write a `#[check(ghost)]` extern specs for the rest of the
        // items, because they have a default implementation, which means we
        // cannot differentiate an extern spec for `Ord::max` from a one for
        // `<$t as Ord>::max`.

        // #[check(ghost)]
        // #[ensures(result.deep_model() >= self.deep_model())]
        // #[ensures(result.deep_model() >= o.deep_model())]
        // #[ensures(result == self || result == o)]
        // #[ensures(self.deep_model() <= o.deep_model() ==> result == o)]
        // #[ensures(o.deep_model() < self.deep_model() ==> result == self)]
        // fn max(self, o: Self) -> Self;

        // #[check(ghost)]
        // #[ensures(result.deep_model() <= self.deep_model())]
        // #[ensures(result.deep_model() <= o.deep_model())]
        // #[ensures(result == self || result == o)]
        // #[ensures(self.deep_model() < o.deep_model() ==> result == self)]
        // #[ensures(o.deep_model() <= self.deep_model() ==> result == o)]
        // fn min(self, o: Self) -> Self;

        // #[check(ghost)]
        // #[requires(min.deep_model() <= max.deep_model())]
        // #[ensures(result.deep_model() >= min.deep_model())]
        // #[ensures(result.deep_model() <= max.deep_model())]
        // #[ensures(result == self || result == min || result == max)]
        // #[ensures(if self.deep_model() > max.deep_model() {
        //     result == max
        // } else if self.deep_model() < min.deep_model() {
        //     result == min
        // } else { result == self })]
        // fn clamp(self, min: Self, max: Self) -> Self;
    }
}

)* };

}

impl_cmp_int!(i8 i16 i32 i64 i128 isize u8 u16 u32 u64 u128 usize);

impl<T: DeepModel> DeepModel for Reverse<T> {
    type DeepModelTy = Reverse<T::DeepModelTy>;

    #[logic(open, inline)]
    fn deep_model(self) -> Self::DeepModelTy {
        pearlite! { Reverse(self.0.deep_model()) }
    }
}

impl<T: PartialOrdLogic> PartialOrdLogic for Reverse<T> {
    #[logic(open, inline)]
    fn lt_log(self, o: Self) -> bool {
        o.0 < self.0
    }

    #[logic(open, inline)]
    fn le_log(self, o: Self) -> bool {
        o.0 <= self.0
    }

    partial_ord_laws_impl! {}
}