creusot_contracts/
model.rs

1//! Logical models of types: [`View`] and [`DeepModel`]
2use crate::prelude::*;
3
4/// The view of a type is its logical model as typically used to specify a data
5/// structure. It is typically "shallow", and does not involve the model of
6/// other types contained by the datastructure.
7/// This kind of model is mostly useful for notation purposes,
8/// because this trait is linked to the `@` notation of pearlite.
9#[diagnostic::on_unimplemented(
10    message = "Cannot take the view of `{Self}`",
11    label = "no implementation for `{Self}@`"
12)]
13pub trait View {
14    type ViewTy;
15    #[logic]
16    #[intrinsic("view")]
17    fn view(self) -> Self::ViewTy;
18}
19
20pub use crate::base_macros::DeepModel;
21
22/// The deep model corresponds to the model used for specifying
23/// operations such as equality, hash function or ordering, which are
24/// computed deeply in a data structure.
25/// Typically, such a model recursively calls deep models of inner types.
26pub trait DeepModel {
27    type DeepModelTy;
28    #[logic]
29    fn deep_model(self) -> Self::DeepModelTy;
30}
31
32impl<T: DeepModel + ?Sized> DeepModel for &T {
33    type DeepModelTy = T::DeepModelTy;
34    #[logic(open, inline)]
35    fn deep_model(self) -> Self::DeepModelTy {
36        (*self).deep_model()
37    }
38}
39
40impl<T: DeepModel + ?Sized> DeepModel for &mut T {
41    type DeepModelTy = T::DeepModelTy;
42    #[logic(open, inline)]
43    fn deep_model(self) -> Self::DeepModelTy {
44        (*self).deep_model()
45    }
46}
47
48impl DeepModel for bool {
49    type DeepModelTy = bool;
50
51    #[logic(open, inline)]
52    fn deep_model(self) -> Self::DeepModelTy {
53        self
54    }
55}
56
57impl DeepModel for Int {
58    type DeepModelTy = Int;
59
60    #[logic(open, inline)]
61    fn deep_model(self) -> Self::DeepModelTy {
62        self
63    }
64}
65
66impl View for String {
67    type ViewTy = Seq<char>;
68
69    #[logic(opaque)]
70    fn view(self) -> Self::ViewTy {
71        dead
72    }
73}
74
75impl DeepModel for std::cmp::Ordering {
76    type DeepModelTy = std::cmp::Ordering;
77
78    #[logic(open, inline)]
79    fn deep_model(self) -> Self::DeepModelTy {
80        self
81    }
82}
creusot_contracts/model.rs

creusot_contracts/
model.rs
