creusot_std/
invariant.rs

1//! Type invariants
2//!
3//! See [`Invariant`].
4
5use crate::prelude::*;
6#[cfg(creusot)]
7use crate::resolve::structural_resolve;
8use core::ops::{Deref, DerefMut};
9
10/// A user-defined _type invariant_.
11///
12/// Type invariants are additional pre- and postconditions added to each program functions.
13///
14/// Not to be confused with [loop invariants][crate::macros::invariant] or
15/// [resource invariants][crate::ghost::invariant].
16///
17/// # Example
18///
19/// ```rust
20/// # use creusot_std::prelude::*;
21/// struct SumTo10 {
22///     a: i32,
23///     b: i32,
24/// }
25/// // The type invariant constrains the set of valid `SumTo10`s to
26/// // only allow values where the sum of both fields is equal to 10.
27/// impl Invariant for SumTo10 {
28///     #[logic(open)]
29///     fn invariant(self) -> bool {
30///         pearlite! {
31///             self.a@ + self.b@ == 10
32///         }
33///     }
34/// }
35///
36/// // #[requires(inv(x))]     // generated by Creusot
37/// // #[ensures(inv(result))] // generated by Creusot
38/// fn invariant_holds(mut x: SumTo10) -> SumTo10 {
39///     assert!(x.a + x.b == 10); // We are given the invariant when entering the function
40///     x.a = 5; // we can break it locally!
41///     x.b = 5; // but it must be restored eventually
42///     x
43/// }
44/// ```
45///
46/// # Structural invariants
47///
48/// A type automatically inherits the invariants of its fields.
49///
50/// Examples:
51/// - `x: (T, U)` -> `inv(x.0) && inv(x.1)`
52/// - `x: &T` -> `inv(*x)`
53/// - `x: Vec<T>` -> `forall<i> 0 <= i && i < x@.len() ==> inv(x@[i])`
54///
55/// This does not prevent the type to additionnaly implement the `Invariant` trait.
56///
57/// ## Mutable borrows
58///
59/// For mutable borrows, the invariant is the conjunction of the invariants of the current
60/// and final values: `x: &mut T` -> `inv(*x) && inv(^x)`.
61///
62/// # Logical functions
63///
64/// Invariant pre- and postconditions are not added to logical functions:
65/// ```
66/// # use creusot_std::prelude::*;
67/// # struct SumTo10 { a: i32, b: i32 }
68/// # impl Invariant for SumTo10 {
69/// # #[logic(open)] fn invariant(self) -> bool { pearlite!{self.a@ + self.b@ == 10} }
70/// # }
71/// #[logic]
72/// #[ensures(x.a@ + x.b@ == 10)]
73/// fn not_provable(x: SumTo10) {}
74/// ```
75pub trait Invariant {
76    #[logic(prophetic)]
77    #[intrinsic("invariant")]
78    fn invariant(self) -> bool;
79}
80
81impl<T: ?Sized> Invariant for &T {
82    #[logic(open, prophetic, inline)]
83    #[creusot::trusted_trivial_if_param_trivial]
84    fn invariant(self) -> bool {
85        inv(*self)
86    }
87}
88
89impl<T: ?Sized> Invariant for &mut T {
90    #[logic(open, prophetic, inline)]
91    #[creusot::trusted_trivial_if_param_trivial]
92    fn invariant(self) -> bool {
93        pearlite! { inv(*self) && inv(^self) }
94    }
95}
96
97/// Whether the invariant of a value holds
98///
99/// This function is functionnaly equivalent to [`Invariant::invariant`], except that it
100/// can be called on any type (even if it does not implement [`Invariant`]).
101#[logic(prophetic, inline, open)]
102#[intrinsic("inv")]
103pub fn inv<T: ?Sized>(_: T) -> bool {
104    dead
105}
106
107#[cfg(not(creusot))]
108pub fn inv<T: ?Sized>(_: &T) -> bool {
109    panic!()
110}
111
112/// A type implements `InhabitedInvariants` when its type invariant is inhabited.
113/// This is needed to define subset types.
114pub trait InhabitedInvariant: Invariant {
115    #[logic]
116    #[ensures(result.invariant())]
117    fn inhabits() -> Self;
118}
119
120/// A _subset_ type.
121///
122/// This the same as `T`, with one exception: the invariant for `T` will also
123/// be verified in logic.
124///
125/// # Example
126///
127/// ```
128/// # use creusot_std::{invariant::{InhabitedInvariant, Subset}, prelude::*};
129/// struct Pair(i32);
130/// impl Invariant for Pair {
131///     #[logic] fn invariant(self) -> bool { self.0 % 2 == 0 }
132/// }
133/// impl InhabitedInvariant for Pair {
134///     #[logic]
135///     #[ensures(result.invariant())]
136///     fn inhabits() -> Self { Self(0i32) }
137/// }
138///
139/// #[logic]
140/// fn pair_in_logic(x: Subset<Pair>) {
141///     proof_assert!(x.0 % 2 == 0);
142/// }
143/// ```
144#[repr(transparent)]
145#[opaque]
146pub struct Subset<T: InhabitedInvariant>(T);
147
148impl<T: InhabitedInvariant + DeepModel> DeepModel for Subset<T> {
149    type DeepModelTy = T::DeepModelTy;
150
151    #[logic(inline)]
152    fn deep_model(self) -> T::DeepModelTy {
153        pearlite! { self.inner().deep_model() }
154    }
155}
156
157impl<T: InhabitedInvariant> Subset<T> {
158    #[trusted]
159    #[logic(opaque)]
160    #[ensures(result.invariant())]
161    pub fn inner(self) -> T {
162        dead
163    }
164
165    /// Create a new element of `Subset<T>` in logic.
166    ///
167    /// As per the [documentation of Subset](Subset), the returned value will
168    /// satisfy `T`'s type invariant.
169    #[trusted]
170    #[logic(opaque)]
171    #[requires(x.invariant())]
172    #[ensures(result.inner() == x)]
173    pub fn new_logic(x: T) -> Self {
174        let _ = x;
175        dead
176    }
177
178    /// Characterize that `Subset<T>` indeed contains a `T` (and only a `T`).
179    ///
180    /// # Example
181    ///
182    /// ```
183    /// # use creusot_std::{invariant::Subset, prelude::*};
184    /// #[requires(x == y.inner())]
185    /// fn foo<T: InhabitedInvariant>(x: T, y: Subset<T>) {
186    ///     let x = Subset::new(x);
187    ///     let _ = snapshot!(Subset::<T>::inner_inj);
188    ///     proof_assert!(x == y);
189    /// }
190    /// ```
191    #[trusted]
192    #[logic(opaque)]
193    #[requires(self.inner() == other.inner())]
194    #[ensures(self == other)]
195    pub fn inner_inj(self, other: Self) {}
196
197    /// Create a new element of `Subset<T>`.
198    ///
199    /// # Example
200    ///
201    /// ```
202    /// # use creusot_std::{invariant::{InhabitedInvariant, Subset}, prelude::*};
203    /// // Use the `Pair` type defined in `Subset`'s documentation
204    /// # struct Pair(i32);
205    /// # impl Invariant for Pair {
206    /// #     #[logic] fn invariant(self) -> bool { self.0 % 2 == 0 } }
207    /// # impl InhabitedInvariant for Pair {
208    /// #     #[logic] #[ensures(result.invariant())]
209    /// #     fn inhabits() -> Self { Self(0i32) } }
210    ///
211    /// let p = Subset::new(Pair(0));
212    /// proof_assert!(p.inner().0 == 0i32);
213    /// ```
214    #[check(ghost)]
215    #[trusted]
216    #[ensures(result == Self::new_logic(x))]
217    pub fn new(x: T) -> Self {
218        Subset(x)
219    }
220
221    /// Unwrap the `Subset` to get the inner value.
222    ///
223    /// # Example
224    ///
225    /// ```
226    /// # use creusot_std::{invariant::{InhabitedInvariant, Subset}, prelude::*};
227    /// // Use the `Pair` type defined in `Subset`'s documentation
228    /// # struct Pair(i32);
229    /// # impl Invariant for Pair {
230    /// #     #[logic] fn invariant(self) -> bool { self.0 % 2 == 0 } }
231    /// # impl InhabitedInvariant for Pair {
232    /// #     #[logic] #[ensures(result.invariant())]
233    /// #     fn inhabits() -> Self { Self(0i32) } }
234    ///
235    /// fn changes_pair(p: &mut Subset<Pair>) { /* ... */ }
236    ///
237    /// let mut p = Subset::new(Pair(0));
238    /// changes_pair(&mut p);
239    /// let inner = p.into_inner();
240    /// proof_assert!(inner.0 % 2 == 0);
241    /// ```
242    #[check(ghost)]
243    #[trusted]
244    #[ensures(result == self.inner())]
245    pub fn into_inner(self) -> T {
246        self.0
247    }
248}
249
250impl<T: InhabitedInvariant> Deref for Subset<T> {
251    type Target = T;
252
253    #[check(ghost)]
254    #[trusted]
255    #[ensures(*result == self.inner())]
256    fn deref(&self) -> &Self::Target {
257        &self.0
258    }
259}
260
261impl<T: InhabitedInvariant> DerefMut for Subset<T> {
262    #[check(ghost)]
263    #[trusted]
264    #[ensures(*result == self.inner())]
265    #[ensures(^result == (^self).inner())]
266    fn deref_mut(&mut self) -> &mut Self::Target {
267        &mut self.0
268    }
269}
270
271impl<T: InhabitedInvariant + Clone> Clone for Subset<T> {
272    #[ensures(T::clone.postcondition((&(self.inner()),), result.inner()))]
273    fn clone(&self) -> Self {
274        snapshot! { Self::inner_inj };
275        Self::new(self.deref().clone())
276    }
277}
278
279impl<T: InhabitedInvariant + Copy> Copy for Subset<T> {}
280
281impl<T: InhabitedInvariant> Resolve for Subset<T> {
282    #[logic(open, prophetic, inline)]
283    fn resolve(self) -> bool {
284        pearlite! { resolve(self.inner()) }
285    }
286
287    #[trusted]
288    #[logic(prophetic)]
289    #[requires(structural_resolve(self))]
290    #[ensures(self.resolve())]
291    fn resolve_coherence(self) {}
292}
293
294impl<T: InhabitedInvariant + DeepModel + PartialEq> PartialEq for Subset<T> {
295    #[trusted]
296    #[ensures(result == (self.deep_model() == rhs.deep_model()))]
297    fn eq(&self, rhs: &Self) -> bool {
298        self.0 == rhs.0
299    }
300}
301
302impl<T: InhabitedInvariant + DeepModel + Eq> Eq for Subset<T> {}
creusot_std/invariant.rs

creusot_std/
invariant.rs
