Shallow model

You can implement the @ operator for your type. To do that, you just implement the creusot_contracts::ShallowModel trait specifying the associated type ShallowModelTy.

For example, the following gives a spooky data type MyPair<T, U> a nice pair model.

#![allow(unused)]
fn main() {
struct MyPair<T, U>(T, U);

impl<T, U> ShallowModel for MyPair<T, U> {
    type ShallowModelTy = (T, U);

    #[logic]
    #[open]
    fn shallow_model(self) -> Self::ShallowModelTy {
        (self.0, self.1)
    }
}

#[ensures(result@ == (a, b))]
fn my_pair<T, U>(a: T, b: U) -> MyPair<T, U> {
    MyPair(a, b)
}
}