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

creusot_std/cell/
permcell.rs
