creusot_std/
invariant.rs

1//! Type invariants
2//!
3//! See [`Invariant`].
4
5mod guarded;
6mod subset;
7
8pub use self::{
9    guarded::{Guarded, GuardedBorrow},
10    subset::{InhabitedInvariant, Subset},
11};
12
13use crate::prelude::*;
14
15/// A user-defined _type invariant_.
16///
17/// Type invariants are additional pre- and postconditions added to each program functions.
18///
19/// Not to be confused with [loop invariants][crate::macros::invariant] or
20/// [resource invariants][crate::ghost::invariant].
21///
22/// # Example
23///
24/// ```rust
25/// # use creusot_std::prelude::*;
26/// struct SumTo10 {
27///     a: i32,
28///     b: i32,
29/// }
30/// // The type invariant constrains the set of valid `SumTo10`s to
31/// // only allow values where the sum of both fields is equal to 10.
32/// impl Invariant for SumTo10 {
33///     #[logic(open)]
34///     fn invariant(self) -> bool {
35///         pearlite! {
36///             self.a@ + self.b@ == 10
37///         }
38///     }
39/// }
40///
41/// // #[requires(inv(x))]     // generated by Creusot
42/// // #[ensures(inv(result))] // generated by Creusot
43/// fn invariant_holds(mut x: SumTo10) -> SumTo10 {
44///     assert!(x.a + x.b == 10); // We are given the invariant when entering the function
45///     x.a = 5; // we can break it locally!
46///     x.b = 5; // but it must be restored eventually
47///     x
48/// }
49/// ```
50///
51/// # Structural invariants
52///
53/// A type automatically inherits the invariants of its fields.
54///
55/// Examples:
56/// - `x: (T, U)` -> `inv(x.0) && inv(x.1)`
57/// - `x: &T` -> `inv(*x)`
58/// - `x: Vec<T>` -> `forall<i> 0 <= i && i < x@.len() ==> inv(x@[i])`
59///
60/// This does not prevent the type to additionnaly implement the `Invariant` trait.
61///
62/// ## Mutable borrows
63///
64/// For mutable borrows, the invariant is the conjunction of the invariants of the current
65/// and final values: `x: &mut T` -> `inv(*x) && inv(^x)`.
66///
67/// # Logical functions
68///
69/// Invariant pre- and postconditions are not added to logical functions:
70/// ```
71/// # use creusot_std::prelude::*;
72/// # struct SumTo10 { a: i32, b: i32 }
73/// # impl Invariant for SumTo10 {
74/// # #[logic(open)] fn invariant(self) -> bool { pearlite!{self.a@ + self.b@ == 10} }
75/// # }
76/// #[logic]
77/// #[ensures(x.a@ + x.b@ == 10)]
78/// fn not_provable(x: SumTo10) {}
79/// ```
80pub trait Invariant {
81    #[logic(prophetic)]
82    #[intrinsic("invariant")]
83    fn invariant(self) -> bool;
84}
85
86impl<T: ?Sized> Invariant for &T {
87    #[logic(open, prophetic, inline)]
88    #[creusot::trusted_trivial_if_param_trivial]
89    fn invariant(self) -> bool {
90        inv(*self)
91    }
92}
93
94impl<T: ?Sized> Invariant for &mut T {
95    #[logic(open, prophetic, inline)]
96    #[creusot::trusted_trivial_if_param_trivial]
97    fn invariant(self) -> bool {
98        pearlite! { inv(*self) && inv(^self) }
99    }
100}
101
102/// Whether the invariant of a value holds
103///
104/// This function is functionnaly equivalent to [`Invariant::invariant`], except that it
105/// can be called on any type (even if it does not implement [`Invariant`]).
106#[logic(prophetic, inline, open)]
107#[intrinsic("inv")]
108pub fn inv<T: ?Sized>(_: T) -> bool {
109    dead
110}
111
112#[cfg(not(creusot))]
113pub fn inv<T: ?Sized>(_: &T) -> bool {
114    panic!()
115}
creusot_std/invariant.rs

creusot_std/
invariant.rs
