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

creusot_std/cell/
permcell.rs
