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

creusot_std/cell/
permcell.rs
