Trait creusot_contracts::model::DeepModel

pub trait DeepModel {
    type DeepModelTy;

    // Required method
    fn deep_model(self) -> Self::DeepModelTy;
}

The deep model corresponds to the model used for specifying operations such as equality, hash function or ordering, which are computed deeply in a data structure. Typically, such a model recursively calls deep models of inner types.

Required Associated Types

type DeepModelTy

Required Methods

fn deep_model(self) -> Self::DeepModelTy

logic

Implementations on Foreign Types

impl DeepModel for bool

fn deep_model(self) -> Self::DeepModelTy

logic

self

type DeepModelTy = bool

impl DeepModel for i8

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for i16

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for i32

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for i64

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for i128

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for isize

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for u8

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for u16

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for u32

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for u64

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for u128

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for ()

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { () }

type DeepModelTy = ()

impl DeepModel for usize

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { self@ }

type DeepModelTy = Int

impl DeepModel for BigRational

fn deep_model(self) -> Self::DeepModelTy

logic

type DeepModelTy = Real

impl<A: DeepModel> DeepModel for (A,)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy,)

impl<A: DeepModel, B: DeepModel> DeepModel for (A, B)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy)

impl<A: DeepModel, B: DeepModel, C: DeepModel> DeepModel for (A, B, C)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy)

impl<A: DeepModel, B: DeepModel, C: DeepModel, D: DeepModel> DeepModel for (A, B, C, D)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy, <D as DeepModel>::DeepModelTy)

impl<A: DeepModel, B: DeepModel, C: DeepModel, D: DeepModel, E: DeepModel> DeepModel for (A, B, C, D, E)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy, <D as DeepModel>::DeepModelTy, <E as DeepModel>::DeepModelTy)

impl<A: DeepModel, B: DeepModel, C: DeepModel, D: DeepModel, E: DeepModel, F: DeepModel> DeepModel for (A, B, C, D, E, F)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy, <D as DeepModel>::DeepModelTy, <E as DeepModel>::DeepModelTy, <F as DeepModel>::DeepModelTy)

impl<A: DeepModel, B: DeepModel, C: DeepModel, D: DeepModel, E: DeepModel, F: DeepModel, G: DeepModel> DeepModel for (A, B, C, D, E, F, G)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy, <D as DeepModel>::DeepModelTy, <E as DeepModel>::DeepModelTy, <F as DeepModel>::DeepModelTy, <G as DeepModel>::DeepModelTy)

impl<A: DeepModel, B: DeepModel, C: DeepModel, D: DeepModel, E: DeepModel, F: DeepModel, G: DeepModel, H: DeepModel> DeepModel for (A, B, C, D, E, F, G, H)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy, <D as DeepModel>::DeepModelTy, <E as DeepModel>::DeepModelTy, <F as DeepModel>::DeepModelTy, <G as DeepModel>::DeepModelTy, <H as DeepModel>::DeepModelTy)

impl<A: DeepModel, B: DeepModel, C: DeepModel, D: DeepModel, E: DeepModel, F: DeepModel, G: DeepModel, H: DeepModel, I: DeepModel> DeepModel for (A, B, C, D, E, F, G, H, I)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy, <D as DeepModel>::DeepModelTy, <E as DeepModel>::DeepModelTy, <F as DeepModel>::DeepModelTy, <G as DeepModel>::DeepModelTy, <H as DeepModel>::DeepModelTy, <I as DeepModel>::DeepModelTy)

impl<A: DeepModel, B: DeepModel, C: DeepModel, D: DeepModel, E: DeepModel, F: DeepModel, G: DeepModel, H: DeepModel, I: DeepModel, J: DeepModel> DeepModel for (A, B, C, D, E, F, G, H, I, J)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy, <D as DeepModel>::DeepModelTy, <E as DeepModel>::DeepModelTy, <F as DeepModel>::DeepModelTy, <G as DeepModel>::DeepModelTy, <H as DeepModel>::DeepModelTy, <I as DeepModel>::DeepModelTy, <J as DeepModel>::DeepModelTy)

impl<A: DeepModel, B: DeepModel, C: DeepModel, D: DeepModel, E: DeepModel, F: DeepModel, G: DeepModel, H: DeepModel, I: DeepModel, J: DeepModel, K: DeepModel> DeepModel for (A, B, C, D, E, F, G, H, I, J, K)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy, <D as DeepModel>::DeepModelTy, <E as DeepModel>::DeepModelTy, <F as DeepModel>::DeepModelTy, <G as DeepModel>::DeepModelTy, <H as DeepModel>::DeepModelTy, <I as DeepModel>::DeepModelTy, <J as DeepModel>::DeepModelTy, <K as DeepModel>::DeepModelTy)

impl<A: DeepModel, B: DeepModel, C: DeepModel, D: DeepModel, E: DeepModel, F: DeepModel, G: DeepModel, H: DeepModel, I: DeepModel, J: DeepModel, K: DeepModel, L: DeepModel> DeepModel for (A, B, C, D, E, F, G, H, I, J, K, L)

fn deep_model(self) -> Self::DeepModelTy

logic

pearlite! { ($(self.$idx.deep_model(),)+) }

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy, <D as DeepModel>::DeepModelTy, <E as DeepModel>::DeepModelTy, <F as DeepModel>::DeepModelTy, <G as DeepModel>::DeepModelTy, <H as DeepModel>::DeepModelTy, <I as DeepModel>::DeepModelTy, <J as DeepModel>::DeepModelTy, <K as DeepModel>::DeepModelTy, <L as DeepModel>::DeepModelTy)

impl<T: DeepModel + ?Sized> DeepModel for &T

fn deep_model(self) -> Self::DeepModelTy

logic

(*self).deep_model()

type DeepModelTy = <T as DeepModel>::DeepModelTy

impl<T: DeepModel + ?Sized> DeepModel for &mut T

fn deep_model(self) -> Self::DeepModelTy

logic

(*self).deep_model()

type DeepModelTy = <T as DeepModel>::DeepModelTy

impl<T: DeepModel> DeepModel for [T]

fn deep_model(self) -> Self::DeepModelTy

logic

ensures

(&self)@.len() == result.len()

ensures

forall<i: Int> 0 <= i && i < result.len() ==> result[i] == (&self)[i].deep_model()

type DeepModelTy = Seq<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel, const N: usize> DeepModel for [T; N]

fn deep_model(self) -> Self::DeepModelTy

logic

ensures

self.view().len() == result.len()

ensures

forall<i: _> 0 <= i && i < result.len() ==> result[i] == self[i].deep_model()

type DeepModelTy = Seq<<T as DeepModel>::DeepModelTy>

impl<T: ?Sized> DeepModel for *const T

fn deep_model(self) -> Self::DeepModelTy

logic

ensures

result.addr == self.addr_logic()

type DeepModelTy = PtrDeepModel

impl<T: ?Sized> DeepModel for *mut T

fn deep_model(self) -> Self::DeepModelTy

logic

ensures

result.addr == self.addr_logic()

type DeepModelTy = PtrDeepModel

Implementors

impl DeepModel for Int

type DeepModelTy = Int

impl DeepModel for Duration

type DeepModelTy = Int

impl DeepModel for Instant

type DeepModelTy = Int

impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Box<T, A>

type DeepModelTy = Box<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel> DeepModel for Option<T>

type DeepModelTy = Option<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel> DeepModel for Reverse<T>

type DeepModelTy = Reverse<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel> DeepModel for Rc<T>

type DeepModelTy = <T as DeepModel>::DeepModelTy

impl<T: DeepModel> DeepModel for Arc<T>

type DeepModelTy = <T as DeepModel>::DeepModelTy

impl<T: DeepModel, A: Allocator> DeepModel for VecDeque<T, A>

type DeepModelTy = Seq<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel, A: Allocator> DeepModel for Vec<T, A>

type DeepModelTy = Seq<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel, E: DeepModel> DeepModel for Result<T, E>

type DeepModelTy = Result<<T as DeepModel>::DeepModelTy, <E as DeepModel>::DeepModelTy>