creusot_std/cell/
permcell.rs

1//! Shared mutation with a ghost token
2//!
3//! This allows a form of interior mutability, using [ghost](mod@crate::ghost) code to keep
4//! track of the logical value.
5
6use crate::{
7    ghost::{NotObjective, Perm, perm::PermTarget},
8    prelude::*,
9};
10use core::{cell::UnsafeCell, marker::PhantomData};
11
12/// Cell with ghost permissions
13///
14/// When writing/reading the cell, you need to explicitly pass a [`Perm`] object.
15///
16/// # Safety
17///
18/// When using Creusot to verify the code, all methods should be safe to call. Indeed,
19/// Creusot ensures that every operation on the inner value uses the right [`Perm`] object
20/// created by [`PermCell::new`], ensuring safety in a manner similar to
21/// [ghost_cell](https://docs.rs/ghost-cell/latest/ghost_cell/).
22#[trusted(positive(T))]
23#[opaque]
24#[repr(transparent)]
25pub struct PermCell<T: ?Sized>(UnsafeCell<T>);
26
27impl<T: ?Sized> PermTarget for PermCell<T> {
28    type Value<'a>
29        = &'a T
30    where
31        Self: 'a;
32    type PermPayload = (NotObjective, PhantomData<T>);
33}
34
35#[trusted]
36unsafe impl<T: ?Sized> Send for PermCell<T> {}
37#[trusted]
38unsafe impl<T: ?Sized> Sync for PermCell<T> {}
39
40impl<T: ?Sized> Invariant for Perm<PermCell<T>> {
41    #[logic(open, prophetic, inline)]
42    #[creusot::trusted_trivial_if_param_trivial]
43    fn invariant(self) -> bool {
44        pearlite! { inv(self.val()) }
45    }
46}
47
48impl<T: ?Sized> PermCell<T> {
49    /// Creates a new `PermCell` containing the given value.
50    #[trusted]
51    #[check(terminates)]
52    #[ensures(result.0 == *result.1.ward())]
53    #[ensures(*result.1.val() == value)]
54    pub fn new(value: T) -> (Self, Ghost<Perm<PermCell<T>>>)
55    where
56        T: Sized,
57    {
58        let this = Self(UnsafeCell::new(value));
59        let perm = Ghost::conjure();
60        (this, perm)
61    }
62
63    /// Sets the contained value.
64    ///
65    /// # Safety
66    ///
67    /// You must ensure that no other borrows to the inner value of `self` exists when calling
68    /// this function.
69    ///
70    /// Creusot will check that all calls to this function are indeed safe: see the
71    /// [type documentation](PermCell#safety).
72    #[trusted]
73    #[check(terminates)]
74    #[requires(self == perm.ward())]
75    #[ensures(val == *(^perm).val())]
76    #[ensures(resolve(*perm.val()))]
77    #[ensures(self == (^perm).ward())]
78    pub unsafe fn set(&self, perm: Ghost<&mut Perm<PermCell<T>>>, val: T)
79    where
80        T: Sized,
81    {
82        let _ = perm;
83        unsafe {
84            *self.0.get() = val;
85        }
86    }
87
88    /// Replaces the contained value with `val`, and returns the old contained value.
89    ///
90    /// # Safety
91    ///
92    /// You must ensure that no other borrows to the inner value of `self` exists when calling
93    /// this function.
94    ///
95    /// Creusot will check that all calls to this function are indeed safe: see the
96    /// [type documentation](PermCell#safety).
97    #[trusted]
98    #[check(terminates)]
99    #[requires(self == perm.ward())]
100    #[ensures(val == *(^perm).val())]
101    #[ensures(result == *perm.val())]
102    #[ensures(self == (^perm).ward())]
103    pub unsafe fn replace(&self, perm: Ghost<&mut Perm<PermCell<T>>>, val: T) -> T
104    where
105        T: Sized,
106    {
107        let _ = perm;
108        unsafe { core::ptr::replace(self.0.get(), val) }
109    }
110
111    /// Unwraps the value, consuming the cell.
112    #[trusted]
113    #[check(terminates)]
114    #[requires(self == *perm.ward())]
115    #[ensures(result == *perm.val())]
116    pub fn into_inner(self, perm: Ghost<Perm<PermCell<T>>>) -> T
117    where
118        T: Sized,
119    {
120        let _ = perm;
121        self.0.into_inner()
122    }
123
124    /// Immutably borrows the wrapped value.
125    ///
126    /// The permission also acts as a guard, preventing writes to the underlying value
127    /// while it is borrowed.
128    ///
129    /// # Safety
130    ///
131    /// You must ensure that no mutable borrow to the inner value of `self` exists when calling
132    /// this function.
133    ///
134    /// Creusot will check that all calls to this function are indeed safe: see the
135    /// [type documentation](PermCell#safety).
136    #[trusted]
137    #[check(terminates)]
138    #[requires(self == perm.ward())]
139    #[ensures(*result == *perm.val())]
140    pub unsafe fn borrow<'a>(&'a self, perm: Ghost<&'a Perm<PermCell<T>>>) -> &'a T {
141        let _ = perm;
142        unsafe { &*self.0.get() }
143    }
144
145    /// Mutably borrows the wrapped value.
146    ///
147    /// The permission also acts as a guard, preventing accesses to the underlying value
148    /// while it is borrowed.
149    ///
150    /// # Safety
151    ///
152    /// You must ensure that no other borrows to the inner value of `self` exists when calling
153    /// this function.
154    ///
155    /// Creusot will check that all calls to this function are indeed safe: see the
156    /// [type documentation](PermCell#safety).
157    #[trusted]
158    #[check(terminates)]
159    #[requires(self == perm.ward())]
160    #[ensures(self == (^perm).ward())]
161    #[ensures(*result == *perm.val())]
162    #[ensures(^result == *(^perm).val())]
163    pub unsafe fn borrow_mut<'a>(&'a self, perm: Ghost<&'a mut Perm<PermCell<T>>>) -> &'a mut T {
164        let _ = perm;
165        unsafe { &mut *self.0.get() }
166    }
167
168    /// Returns a copy of the contained value.
169    ///
170    /// # Safety
171    ///
172    /// You must ensure that no mutable borrow to the inner value of `self` exists when calling
173    /// this function.
174    ///
175    /// Creusot will check that all calls to this function are indeed safe: see the
176    /// [type documentation](PermCell#safety).
177    #[trusted]
178    #[check(terminates)]
179    #[requires(self == perm.ward())]
180    #[ensures(result == *perm.val())]
181    pub unsafe fn get(&self, perm: Ghost<&Perm<PermCell<T>>>) -> T
182    where
183        T: Copy + Sized,
184    {
185        let _ = perm;
186        unsafe { *self.0.get() }
187    }
188
189    /// Returns a raw pointer to the underlying data in this cell.
190    #[trusted]
191    #[ensures(true)]
192    pub fn as_ptr(&self) -> *mut T {
193        self.0.get()
194    }
195
196    /// Returns a `&PermCell<T>` from a `&mut T`
197    #[trusted]
198    #[check(terminates)]
199    #[ensures(result.0 == result.1.ward())]
200    #[ensures(^t == *(^result.1).val())]
201    #[ensures(*t == *result.1.val())]
202    pub fn from_mut(t: &mut T) -> (&PermCell<T>, Ghost<&mut Perm<PermCell<T>>>) {
203        // SAFETY: `PermCell` is layout-compatible with `Cell` and `T` because it is `repr(transparent)`.
204        // SAFETY: `&mut` ensures unique access
205        let cell: &PermCell<T> = unsafe { &*(t as *mut T as *const Self) };
206        let perm = Ghost::conjure();
207        (cell, perm)
208    }
209
210    /// Takes the value of the cell, leaving `Default::default()` in its place.
211    ///
212    /// # Safety
213    ///
214    /// You must ensure that no other borrows to the inner value of `self` exists when calling
215    /// this function.
216    ///
217    /// Creusot will check that all calls to this function are indeed safe: see the
218    /// [type documentation](PermCell#safety).
219    #[requires(self == perm.ward())]
220    #[ensures(self == (^perm).ward())]
221    #[ensures(result == *perm.val())]
222    #[ensures(T::default.postcondition((), *(^perm).val()))]
223    pub unsafe fn take(&self, perm: Ghost<&mut Perm<PermCell<T>>>) -> T
224    where
225        T: Default,
226    {
227        unsafe { self.replace(perm, T::default()) }
228    }
229}
creusot_std/cell/permcell.rs

creusot_std/cell/
permcell.rs
