creusot_std/invariant/
subset.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use crate::resolve::structural_resolve;
4use core::ops::{Deref, DerefMut};
5
6/// A type implements `InhabitedInvariant` when its type invariant is inhabited.
7/// This is needed to define subset types.
8pub trait InhabitedInvariant: Invariant + Sized {
9    #[logic]
10    #[ensures(result.invariant())]
11    fn inhabits() -> Self;
12}
13
14/// A _subset_ type.
15///
16/// This the same as `T`, with one exception: the invariant for `T` will also
17/// be verified in logic.
18///
19/// # Example
20///
21/// ```
22/// # use creusot_std::{invariant::{InhabitedInvariant, Subset}, prelude::*};
23/// struct Pair(i32);
24/// impl Invariant for Pair {
25///     #[logic] fn invariant(self) -> bool { self.0 % 2 == 0 }
26/// }
27/// impl InhabitedInvariant for Pair {
28///     #[logic]
29///     #[ensures(result.invariant())]
30///     fn inhabits() -> Self { Self(0i32) }
31/// }
32///
33/// #[logic]
34/// fn pair_in_logic(x: Subset<Pair>) {
35///     proof_assert!(x.0 % 2 == 0);
36/// }
37/// ```
38#[repr(transparent)]
39#[opaque]
40pub struct Subset<T: InhabitedInvariant>(T);
41
42impl<T: InhabitedInvariant + DeepModel> DeepModel for Subset<T> {
43    type DeepModelTy = T::DeepModelTy;
44
45    #[logic(inline)]
46    fn deep_model(self) -> T::DeepModelTy {
47        pearlite! { self.inner().deep_model() }
48    }
49}
50
51impl<T: InhabitedInvariant> Subset<T> {
52    #[trusted]
53    #[logic(opaque)]
54    #[ensures(result.invariant())]
55    pub fn inner(self) -> T {
56        dead
57    }
58
59    /// Create a new element of `Subset<T>` in logic.
60    ///
61    /// As per the [documentation of Subset](Subset), the returned value will
62    /// satisfy `T`'s type invariant.
63    #[trusted]
64    #[logic(opaque)]
65    #[requires(x.invariant())]
66    #[ensures(result.inner() == x)]
67    pub fn new_logic(x: T) -> Self {
68        let _ = x;
69        dead
70    }
71
72    /// Characterize that `Subset<T>` indeed contains a `T` (and only a `T`).
73    ///
74    /// # Example
75    ///
76    /// ```
77    /// # use creusot_std::{invariant::Subset, prelude::*};
78    /// #[requires(x == y.inner())]
79    /// fn foo<T: InhabitedInvariant>(x: T, y: Subset<T>) {
80    ///     let x = Subset::new(x);
81    ///     let _ = snapshot!(Subset::<T>::inner_inj);
82    ///     proof_assert!(x == y);
83    /// }
84    /// ```
85    #[trusted]
86    #[logic(opaque)]
87    #[requires(self.inner() == other.inner())]
88    #[ensures(self == other)]
89    pub fn inner_inj(self, other: Self) {}
90
91    /// Create a new element of `Subset<T>`.
92    ///
93    /// # Example
94    ///
95    /// ```
96    /// # use creusot_std::{invariant::{InhabitedInvariant, Subset}, prelude::*};
97    /// // Use the `Pair` type defined in `Subset`'s documentation
98    /// # struct Pair(i32);
99    /// # impl Invariant for Pair {
100    /// #     #[logic] fn invariant(self) -> bool { self.0 % 2 == 0 } }
101    /// # impl InhabitedInvariant for Pair {
102    /// #     #[logic] #[ensures(result.invariant())]
103    /// #     fn inhabits() -> Self { Self(0i32) } }
104    ///
105    /// let p = Subset::new(Pair(0));
106    /// proof_assert!(p.inner().0 == 0i32);
107    /// ```
108    #[check(ghost)]
109    #[trusted]
110    #[ensures(result == Self::new_logic(x))]
111    pub fn new(x: T) -> Self {
112        Subset(x)
113    }
114
115    /// Unwrap the `Subset` to get the inner value.
116    ///
117    /// # Example
118    ///
119    /// ```
120    /// # use creusot_std::{invariant::{InhabitedInvariant, Subset}, prelude::*};
121    /// // Use the `Pair` type defined in `Subset`'s documentation
122    /// # struct Pair(i32);
123    /// # impl Invariant for Pair {
124    /// #     #[logic] fn invariant(self) -> bool { self.0 % 2 == 0 } }
125    /// # impl InhabitedInvariant for Pair {
126    /// #     #[logic] #[ensures(result.invariant())]
127    /// #     fn inhabits() -> Self { Self(0i32) } }
128    ///
129    /// fn changes_pair(p: &mut Subset<Pair>) { /* ... */ }
130    ///
131    /// let mut p = Subset::new(Pair(0));
132    /// changes_pair(&mut p);
133    /// let inner = p.into_inner();
134    /// proof_assert!(inner.0 % 2 == 0);
135    /// ```
136    #[check(ghost)]
137    #[trusted]
138    #[ensures(result == self.inner())]
139    pub fn into_inner(self) -> T {
140        self.0
141    }
142}
143
144impl<T: InhabitedInvariant> Deref for Subset<T> {
145    type Target = T;
146
147    #[check(ghost)]
148    #[trusted]
149    #[ensures(*result == self.inner())]
150    fn deref(&self) -> &Self::Target {
151        &self.0
152    }
153}
154
155impl<T: InhabitedInvariant> DerefMut for Subset<T> {
156    #[check(ghost)]
157    #[trusted]
158    #[ensures(*result == self.inner())]
159    #[ensures(^result == (^self).inner())]
160    fn deref_mut(&mut self) -> &mut Self::Target {
161        &mut self.0
162    }
163}
164
165impl<T: InhabitedInvariant + Clone> Clone for Subset<T> {
166    #[ensures(T::clone.postcondition((&(self.inner()),), result.inner()))]
167    fn clone(&self) -> Self {
168        snapshot! { Self::inner_inj };
169        Self::new(self.deref().clone())
170    }
171}
172
173impl<T: InhabitedInvariant + Copy> Copy for Subset<T> {}
174
175impl<T: InhabitedInvariant> Resolve for Subset<T> {
176    #[logic(open, prophetic, inline)]
177    fn resolve(self) -> bool {
178        pearlite! { resolve(self.inner()) }
179    }
180
181    #[trusted]
182    #[logic(prophetic)]
183    #[requires(structural_resolve(self))]
184    #[ensures(self.resolve())]
185    fn resolve_coherence(self) {}
186}
187
188impl<T: InhabitedInvariant + DeepModel + PartialEq> PartialEq for Subset<T> {
189    #[trusted]
190    #[ensures(result == (self.deep_model() == rhs.deep_model()))]
191    fn eq(&self, rhs: &Self) -> bool {
192        self.0 == rhs.0
193    }
194}
195
196impl<T: InhabitedInvariant + DeepModel + Eq> Eq for Subset<T> {}
creusot_std/invariant/subset.rs

creusot_std/invariant/
subset.rs
