creusot_std/invariant/
guarded.rs

1use crate::{logic::Mapping, prelude::*};
2
3/// Guards that can be used in [`Guarded`].
4pub trait Guard<T> {
5    /// Property that must be satisfied by the end of `Guarded`.
6    ///
7    /// `initial` is the initial guarded value remembered by `Guarded`,
8    /// `current` is the current guarded value (the `inner` field of `Guarded`).
9    #[logic(prophetic)]
10    fn guards(self, initial: T, current: T) -> bool;
11}
12
13/// Guard predicate under mutable references.
14///
15/// Notably, `G: GuardRef<T>` implies `G: Guard<&mut T>`
16/// and `G: Guard<FullBorrow<T>>`.
17pub trait GuardRef<T> {
18    #[logic(prophetic)]
19    fn guards_ref(self, x: T) -> bool;
20}
21
22impl<'a, G: GuardRef<T>, T> Guard<&'a mut T> for G {
23    #[logic(open, prophetic, inline)]
24    fn guards(self, initial: &'a mut T, current: &'a mut T) -> bool {
25        pearlite! { self.guards_ref(*current) && ^initial == ^current }
26    }
27}
28
29/// `Guarded` is a wrapper around an object of type `T`, which makes sure that a
30/// guard (a predicate on `T`) is satisfied when the guarded object disappears.
31/// It works by making the guard part of the type invariant of `Guarded`,
32/// and uses some internal Creusot machinery to ensure that the guard
33/// never changes during the lifetime of the `Guarded` object.
34///
35/// As such, the guard can be broken locally, but it must be restored before the
36/// `Guarded` object is dropped, passed as a parameter, returned or when a
37/// borrow of the `Guarded` is resolved.
38///
39/// The guard is represented by a value `guard: G` whose type implements the trait
40/// [`Guard<T>`]. The relation [`guard.guards(inner, initial)`][Guard::guards]
41/// is the property that must be satisfied when the guarded object disappears,
42/// where `inner` is the current value of the guarded object, and `initial` is
43/// its initial value when the `Guarded` object is created. The initial value is
44/// used to guarantee that the guarded object is not replaced with another (it
45/// may be mutated, but not replaced with another) using e.g., [`std::mem::swap`].
46///
47/// `Guarded` is typically used with a `T` mutable borrow. In this case,
48/// `Guard<&mut T>` guarantees that the prophecies never change, and the
49/// guard typically guarantees that the final value of the borrow satisfies
50/// some property. Other uses include types that behave like mutable borrows,
51/// such as `FullBorrow`.
52///
53/// # Example
54///
55/// ```
56/// use creusot_std::prelude::*;
57/// use creusot_std::invariant::Guarded;
58///
59/// #[ensures(^b == 0i32)]
60/// fn breaks_inv(b: &mut i32) { *b = 0; }
61///
62/// let mut x = 1;
63/// let guarded = Guarded::new_m(&mut x, snapshot!(|x: i32| x == 1i32));
64/// // break the guard...
65/// breaks_inv(&mut *guarded.inner);
66/// // but restore it before we are done
67/// *guarded.inner = 1;
68/// ```
69#[repr(transparent)]
70#[intrinsic("guarded")]
71pub struct Guarded<T, G: Guard<T>> {
72    /// Payload of this `Guarded` value.
73    pub inner: T,
74    _guard: Snapshot<G>,
75    _initial: Snapshot<T>,
76}
77
78impl<T, G: Guard<T>> Invariant for Guarded<T, G> {
79    #[logic(open, prophetic, inline)]
80    fn invariant(self) -> bool {
81        pearlite! { (*self._guard).guards(*self._initial, self.inner) }
82    }
83}
84
85impl<T, G: Guard<T>> Guarded<T, G> {
86    #[logic(open, inline)]
87    pub fn guard(self) -> G {
88        pearlite! { *self._guard }
89    }
90}
91
92impl<'a, T, G: GuardRef<T>> Guarded<&'a mut T, G> {
93    /// Create a new guarded borrow.
94    ///
95    /// The borrow contained in the result is guaranteed to satisfy the
96    /// [`guard`](Guard::guard) at the end of its lifetime. Thus, we get the
97    /// guard for its prophecy.
98    ///
99    /// Note that the type of the second argument may not be inferred during
100    /// compilation with rustc if it is directly constructed using
101    /// the `snapshot!` macro. You may want to spell out the first type
102    /// argument of `Guarded`, or use `Guarded::new_m` if the guard is a `Mapping`.
103    #[trusted]
104    #[requires(guard.guards_ref(*borrow))]
105    #[ensures(result.inner == borrow)]
106    #[ensures(result.guard() == *guard)]
107    #[ensures(guard.guards_ref(^borrow))]
108    #[check(ghost)]
109    pub fn new(borrow: &'a mut T, guard: Snapshot<G>) -> Self {
110        Self { inner: borrow, _guard: guard, _initial: snapshot!(borrow) }
111    }
112}
113
114impl<'a, T> Guarded<&'a mut T, Mapping<T, bool>> {
115    /// Variant of [`Guarded::new`] specialized with `Mapping` as the guard.
116    #[requires(guard.guards_ref(*borrow))]
117    #[ensures(result.inner == borrow)]
118    #[ensures(result.guard() == *guard)]
119    #[ensures(guard.guards_ref(^borrow))]
120    #[check(ghost)]
121    pub fn new_m(borrow: &'a mut T, guard: Snapshot<Mapping<T, bool>>) -> Self {
122        Self::new(borrow, guard)
123    }
124}
125
126impl<'a, T> Guarded<&'a mut Option<T>, IsSome> {
127    #[trusted]
128    #[check(ghost)]
129    #[ensures(*result.inner == Some(**borrow))]
130    #[ensures(^result.inner == Some(^borrow))]
131    pub fn some(borrow: Ghost<&'a mut T>) -> Ghost<Self> {
132        let _ = borrow;
133        Ghost::conjure()
134    }
135}
136
137impl<T> GuardRef<T> for Mapping<T, bool> {
138    #[logic(open, inline)]
139    fn guards_ref(self, x: T) -> bool {
140        pearlite! { self[x] }
141    }
142}
143
144/// Guard an `Option` that must remain `Some`.
145pub struct IsSome;
146
147impl<T> GuardRef<Option<T>> for IsSome {
148    #[logic(open, inline)]
149    fn guards_ref(self, x: Option<T>) -> bool {
150        pearlite! { x != None }
151    }
152}
creusot_std/invariant/guarded.rs

creusot_std/invariant/
guarded.rs
