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

creusot_std/cell/
permcell.rs
