creusot_std/

peano.rs

//! Peano integers
//!
//! Peano integers are a specialized kind of integers, that allow to increase the integer
//! without checking for overflows.
//!
//! See <https://inria.hal.science/hal-01162661v1> for reference.
//!
//! # Usage in data structures
//!
//! They are useful when specifying a data structure where
//! - checking for overflows of the length is hard (and may leak to the users of the library),
//! - overflows are practically impossible because the length only grows by one at a time.
//!
//! In this case, you could use a [`PeanoInt`] to store the length.
//!
//! # Why not always use them ?
//!
//! Well, simply because you cannot add two peano integers together, at least not
//! efficiently. If you need to do usual arithmetic operations, you should use a normal
//! integer.
//!
//! # Ghost code
//!
//! You cannot increase a peano integer in [`ghost`] code, as it may
//! overflow the backing integer. Since ghost code is not executed, the time argument is
//! not applicable.

use crate::prelude::{Clone, Default, *};
use core::cmp::Ordering;

/// A peano integer wrapping a 64-bits integer.
///
/// See the [module](crate::peano) explanation.
#[derive(Default, Clone, Copy, Eq)]
#[non_exhaustive]
#[repr(transparent)]
pub struct PeanoInt(pub u64);

impl DeepModel for PeanoInt {
    type DeepModelTy = u64;
    #[logic(open, inline)]
    fn deep_model(self) -> u64 {
        self.0
    }
}

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

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

    #[logic]
    #[ensures(!(self < self))]
    fn irreflexive(self) {}

    #[logic]
    #[requires(x < y)]
    #[requires(y < z)]
    #[ensures(x < z)]
    fn transitive(x: Self, y: Self, z: Self) {}

    #[logic]
    #[ensures((self <= other) == (self < other || self == other))]
    fn le_lt_log(self, other: Self) {}
}

impl OrdLogic for PeanoInt {
    #[logic]
    #[ensures(self < other || self == other || other < self)]
    fn lt_log_total(self, other: Self) {}
}

impl View for PeanoInt {
    type ViewTy = u64;
    #[logic(open, inline)]
    fn view(self) -> u64 {
        self.0
    }
}

impl PartialOrd for PeanoInt {
    #[check(ghost)]
    #[ensures(result == Some((*self).cmp_log(*other)))]
    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
        Some(self.cmp(other))
    }

    // FIXME: those implementations are only here to specify that they are `ghost`.
    // We should have a mechanism to say 'These functions are ghost if `partial_cpm` is ghost'.

    #[check(ghost)]
    #[ensures(result == (self@ < other@))]
    fn lt(&self, other: &Self) -> bool {
        matches!(self.partial_cmp(other), Some(Ordering::Less))
    }
    #[check(ghost)]
    #[ensures(result == (self@ <= other@))]
    fn le(&self, other: &Self) -> bool {
        matches!(self.partial_cmp(other), Some(Ordering::Less | Ordering::Equal))
    }
    #[check(ghost)]
    #[ensures(result == (self@ > other@))]
    fn gt(&self, other: &Self) -> bool {
        matches!(self.partial_cmp(other), Some(Ordering::Greater))
    }
    #[check(ghost)]
    #[ensures(result == (self@ >= other@))]
    fn ge(&self, other: &Self) -> bool {
        matches!(self.partial_cmp(other), Some(Ordering::Greater | Ordering::Equal))
    }
}
impl Ord for PeanoInt {
    #[check(ghost)]
    #[ensures(result == (*self).cmp_log(*other))]
    fn cmp(&self, other: &Self) -> Ordering {
        self.0.cmp(&other.0)
    }
}
impl PartialEq for PeanoInt {
    #[check(ghost)]
    #[ensures(result == (*self == *other))]
    fn eq(&self, other: &Self) -> bool {
        self.0 == other.0
    }
}

impl PeanoInt {
    /// Create a new peano integer with value `0`.
    #[check(ghost)]
    #[ensures(result.0 == 0u64)]
    pub fn new() -> Self {
        Self(0)
    }

    /// Increase the integer by one.
    ///
    /// This method guarantees that increments cannot get optimized together, e.g. that
    /// ```rust
    /// # use creusot_std::peano::PeanoInt;
    /// let mut x = PeanoInt::new();
    /// for _ in 0..1_000_000 {
    ///     x.incr();
    /// }
    /// ```
    /// Does not get optimized down to a single addition.
    ///
    /// Since the backing integer is 64 bits long, no program could ever actually reach
    /// the point where the integer overflows.
    #[trusted]
    #[check(terminates)]
    #[ensures(result.0@ == self.0@ + 1)]
    pub fn incr(self) -> Self {
        // Use volatile read, to avoid optimizing successive increments.
        // SAFETY: using `read_volatile` on a reference of a `Copy` object is always safe.
        let x = unsafe { core::ptr::read_volatile(&self.0) };
        Self(x + 1)
    }

    /// Get the underlying integer.
    #[check(ghost)]
    #[ensures(result == self.0)]
    pub fn to_u64(self) -> u64 {
        self.0
    }

    /// Get the underlying integer.
    #[check(ghost)]
    #[trusted]
    #[ensures(result@ == self.0@)]
    pub fn to_i64(self) -> i64 {
        self.0 as i64
    }

    /// Get the underlying integer.
    #[check(ghost)]
    #[ensures(result@ == self.0@)]
    pub fn to_u128(self) -> u128 {
        self.0 as u128
    }

    /// Get the underlying integer.
    #[check(ghost)]
    #[ensures(result@ == self.0@)]
    pub fn to_i128(self) -> i128 {
        self.0 as i128
    }
}

impl From<PeanoInt> for u64 {
    #[check(ghost)]
    #[ensures(result == val.0)]
    fn from(val: PeanoInt) -> Self {
        val.to_u64()
    }
}

impl From<PeanoInt> for i64 {
    #[check(ghost)]
    #[ensures(result@ == val.0@)]
    fn from(val: PeanoInt) -> Self {
        val.to_i64()
    }
}

impl From<PeanoInt> for u128 {
    #[check(ghost)]
    #[ensures(result@ == val.0@)]
    fn from(val: PeanoInt) -> Self {
        val.to_u128()
    }
}

impl From<PeanoInt> for i128 {
    #[check(ghost)]
    #[ensures(result@ == val.0@)]
    fn from(val: PeanoInt) -> Self {
        val.to_i128()
    }
}