creusot_contracts/
invariant.rs

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

creusot_contracts/
invariant.rs
