creusot_std/invariant/
guarded.rs

1use crate::{logic::Mapping, prelude::*};
2use core::ops::Deref;
3
4/// A borrow _guarded_ by an invariant.
5///
6/// This is used to define [`GuardedBorrow`].
7/// This can also be used to define the equivalent of `GuardedBorrow` with
8/// smart pointers, like [`RefMut`](core::cell::RefMut).
9#[repr(transparent)]
10#[logically_visible]
11pub struct Guarded<T> {
12    /// Borrow contained in this guard.
13    ///
14    /// The `T` type parameter is meant to be a mutable borrow type (like
15    /// `&mut T`, or [`RefMut<T>`](core::cell::RefMut)).
16    pub borrow: T,
17    _guard: Snapshot<Mapping<T, bool>>,
18}
19
20impl<T> Guarded<T> {
21    /// The [`guard`](Guard::guard) associated with this borrow.
22    ///
23    /// The type invariant of the `Guarded` ensures that the current value
24    /// of [`borrow`](Self::borrow) satisfies this guard.
25    #[logic(open, inline)]
26    pub fn guard(self) -> Mapping<T, bool> {
27        *self._guard
28    }
29}
30
31impl<'a, T: ?Sized> Invariant for GuardedBorrow<'a, T> {
32    #[logic(open, prophetic)]
33    fn invariant(self) -> bool {
34        pearlite! { self.guard()[self.borrow] }
35    }
36}
37
38impl<T> Deref for Guarded<T> {
39    type Target = T;
40    #[ensures(*result == self.borrow)]
41    #[check(ghost)]
42    fn deref(&self) -> &Self::Target {
43        &self.borrow
44    }
45}
46
47// Forbid destructuring of `Guarded`
48impl<T> Drop for Guarded<T> {
49    fn drop(&mut self) {}
50}
51
52/// A mutable borrow, that asserts an invariant called the **guard**.
53///
54/// The guard can be broken locally, by accessing the
55/// [`borrow`](Guarded::borrow) directly. However, it must be restored by the
56/// end of the `GuardedBorrow`'s lifetime.
57///
58/// # Example
59///
60/// ```
61/// use creusot_std::prelude::*;
62/// use creusot_std::invariant::GuardedBorrow;
63///
64/// #[ensures(^b == 0i32)]
65/// fn breaks_inv(b: &mut i32) { *b = 0; }
66///
67/// let mut x = 1;
68/// let guarded = GuardedBorrow::new(&mut x, snapshot!(|x: i32| x == 1i32));
69/// // break the guard...
70/// breaks_inv(&mut *guarded.borrow);
71/// // but restore it before we are done
72/// *guarded.borrow = 1;
73/// ```
74pub type GuardedBorrow<'a, T> = Guarded<&'a mut T>;
75
76impl<'a, T: ?Sized> GuardedBorrow<'a, T> {
77    /// Create a new guarded borrow.
78    ///
79    /// The borrow contained in the result is guaranteed to satisfy the
80    /// [`guard`](Guard::guard) at the end of its lifetime.
81    ///
82    /// Note that the `borrow` field cannot have its final value changed,
83    /// ensuring that it will not get swapped for another borrow.
84    #[trusted]
85    #[ensures(result.borrow == borrow)]
86    #[ensures(forall<bor: &mut T> result.guard()[bor] == (guard[*bor] && ^bor == ^borrow))]
87    #[ensures(guard[^borrow])]
88    #[check(ghost)]
89    pub fn new(borrow: &'a mut T, #[allow(unused)] guard: Snapshot<Mapping<T, bool>>) -> Self {
90        Self { borrow, _guard: snapshot!(|_: &mut T| false /* placeholder */) }
91    }
92
93    /// Get a shared borrow out of this guarded borrow.
94    ///
95    /// It is not possible to break the guard anymore, since the returned borrow
96    /// is immutable.
97    #[trusted]
98    #[ensures(*result == *self.borrow)]
99    #[ensures(*self.borrow == ^self.borrow)]
100    #[check(ghost)]
101    pub fn into_shared(self) -> &'a T {
102        let ptr = self.borrow as *mut T;
103        core::mem::forget(self);
104        // SAFETY: we are bypassing the destructor of `self`, but it is ok since
105        // it does nothing anyways.
106        unsafe { &*ptr }
107    }
108}
creusot_std/invariant/guarded.rs

creusot_std/invariant/
guarded.rs
