creusot_contracts/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
6#[cfg(creusot)]
7use crate::resolve::structural_resolve;
8use crate::{logic::Id, prelude::*};
9use std::{cell::UnsafeCell, marker::PhantomData};
10
11/// Cell with ghost permissions
12///
13/// When writing/reading the cell, you need to explicitly pass a [`PermCellOwn`] object.
14///
15/// # Safety
16///
17/// When using Creusot to verify the code, all methods should be safe to call. Indeed,
18/// Creusot ensures that every operation on the inner value uses the right [`PermCellOwn`] object
19/// created by [`PermCell::new`], ensuring safety in a manner similar to [ghost_cell](https://docs.rs/ghost-cell/latest/ghost_cell/).
20#[repr(transparent)]
21#[opaque]
22pub struct PermCell<T: ?Sized>(UnsafeCell<T>);
23
24/// Token that represents the ownership of a [`PermCell`] object.
25///
26/// A `PermCellOwn` only exists in the ghost world, and it must be used in conjunction with
27/// [`PermCell`] in order to read or write the value.
28#[opaque]
29pub struct PermCellOwn<T: ?Sized>(PhantomData<T>);
30
31impl<T> View for PermCellOwn<T> {
32    type ViewTy = T;
33
34    #[logic(open, inline)]
35    fn view(self) -> Self::ViewTy {
36        *self.val()
37    }
38}
39
40impl<T: ?Sized> Resolve for PermCellOwn<T> {
41    #[logic(open, prophetic, inline)]
42    #[creusot::trusted_trivial_if_param_trivial]
43    fn resolve(self) -> bool {
44        resolve(self.val())
45    }
46
47    #[trusted]
48    #[logic(prophetic)]
49    #[requires(inv(self))]
50    #[requires(structural_resolve(self))]
51    #[ensures(self.resolve())]
52    fn resolve_coherence(self) {}
53}
54
55impl<T: Sized> Invariant for PermCellOwn<T> {
56    #[logic(open, prophetic, inline)]
57    #[creusot::trusted_trivial_if_param_trivial]
58    fn invariant(self) -> bool {
59        pearlite! { inv(self.val()) }
60    }
61}
62
63impl<T: ?Sized> PermCellOwn<T> {
64    /// Returns the logical identity of the cell.
65    ///
66    /// To use a [`PermCell`], this and [`PermCell::id`] must agree.
67    #[logic(opaque)]
68    pub fn id(self) -> Id {
69        dead
70    }
71
72    /// Get the logical value.
73    #[logic(opaque)]
74    pub fn val<'a>(self) -> &'a T {
75        dead
76    }
77
78    #[check(ghost)]
79    #[ensures(*result == self.id())]
80    pub fn id_ghost(&self) -> Ghost<Id> {
81        snapshot!(self.id()).into_ghost()
82    }
83
84    /// If one owns two `PermCellOwn`s in ghost code, then they have different ids.
85    #[trusted]
86    #[check(ghost)]
87    #[ensures(own1.id() != own2.id())]
88    #[ensures(*own1 == ^own1)]
89    #[allow(unused_variables)]
90    pub fn disjoint_lemma(own1: &mut PermCellOwn<T>, own2: &PermCellOwn<T>) {}
91}
92
93impl<T> PermCell<T> {
94    /// Creates a new `PermCell` containing the given value.
95    #[trusted]
96    #[check(terminates)]
97    #[ensures(result.0.id() == result.1.id())]
98    #[ensures((*result.1)@ == value)]
99    pub fn new(value: T) -> (Self, Ghost<PermCellOwn<T>>) {
100        let this = Self(UnsafeCell::new(value));
101        let perm = Ghost::conjure();
102        (this, perm)
103    }
104
105    /// Sets the contained value.
106    ///
107    /// # Safety
108    ///
109    /// You must ensure that no other borrows to the inner value of `self` exists when calling
110    /// this function.
111    ///
112    /// Creusot will check that all calls to this function are indeed safe: see the
113    /// [type documentation](PermCell#safety).
114    #[trusted]
115    #[check(terminates)]
116    #[requires(self.id() == perm.id())]
117    #[ensures(val == (^perm)@)]
118    #[ensures(resolve(perm@))]
119    #[ensures(self.id() == (^perm).id())]
120    pub unsafe fn set(&self, perm: Ghost<&mut PermCellOwn<T>>, val: T) {
121        let _ = perm;
122        unsafe {
123            *self.0.get() = val;
124        }
125    }
126
127    /// Replaces the contained value with `val`, and returns the old contained value.
128    ///
129    /// # Safety
130    ///
131    /// You must ensure that no other borrows 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.id() == perm.id())]
139    #[ensures(val == (^perm)@)]
140    #[ensures(result == perm@)]
141    #[ensures(self.id() == (^perm).id())]
142    pub unsafe fn replace(&self, perm: Ghost<&mut PermCellOwn<T>>, val: T) -> T {
143        let _ = perm;
144        unsafe { std::ptr::replace(self.0.get(), val) }
145    }
146
147    /// Unwraps the value, consuming the cell.
148    #[trusted]
149    #[check(terminates)]
150    #[requires(self.id() == perm.id())]
151    #[ensures(result == perm@)]
152    pub fn into_inner(self, perm: Ghost<PermCellOwn<T>>) -> T {
153        let _ = perm;
154        self.0.into_inner()
155    }
156
157    /// Immutably borrows the wrapped value.
158    ///
159    /// The permission also acts as a guard, preventing writes to the underlying value
160    /// while it is borrowed.
161    ///
162    /// # Safety
163    ///
164    /// You must ensure that no mutable borrow to the inner value of `self` exists when calling
165    /// this function.
166    ///
167    /// Creusot will check that all calls to this function are indeed safe: see the
168    /// [type documentation](PermCell#safety).
169    #[trusted]
170    #[check(terminates)]
171    #[requires(self.id() == perm.id())]
172    #[ensures(*result == perm@)]
173    pub unsafe fn borrow<'a>(&'a self, perm: Ghost<&'a PermCellOwn<T>>) -> &'a T {
174        let _ = perm;
175        unsafe { &*self.0.get() }
176    }
177
178    /// Mutably borrows the wrapped value.
179    ///
180    /// The permission also acts as a guard, preventing accesses to the underlying value
181    /// while it is borrowed.
182    ///
183    /// # Safety
184    ///
185    /// You must ensure that no other borrows to the inner value of `self` exists when calling
186    /// this function.
187    ///
188    /// Creusot will check that all calls to this function are indeed safe: see the
189    /// [type documentation](PermCell#safety).
190    #[trusted]
191    #[check(terminates)]
192    #[requires(self.id() == perm.id())]
193    #[ensures(self.id() == (^perm).id())]
194    #[ensures(*result == perm@)]
195    #[ensures(^result == (^perm)@)]
196    pub unsafe fn borrow_mut<'a>(&'a self, perm: Ghost<&'a mut PermCellOwn<T>>) -> &'a mut T {
197        let _ = perm;
198        unsafe { &mut *self.0.get() }
199    }
200}
201
202impl<T: Copy> PermCell<T> {
203    /// Returns a copy of the contained value.
204    ///
205    /// # Safety
206    ///
207    /// You must ensure that no mutable borrow to the inner value of `self` exists when calling
208    /// this function.
209    ///
210    /// Creusot will check that all calls to this function are indeed safe: see the
211    /// [type documentation](PermCell#safety).
212    #[trusted]
213    #[check(terminates)]
214    #[requires(self.id() == perm.id())]
215    #[ensures(result == (**perm)@)]
216    pub unsafe fn get(&self, perm: Ghost<&PermCellOwn<T>>) -> T {
217        let _ = perm;
218        unsafe { *self.0.get() }
219    }
220}
221
222impl<T> PermCell<T> {
223    /// Returns the logical identity of the cell.
224    ///
225    /// This is used to guarantee that a [`PermCellOwn`] is always used with the right [`PermCell`].
226    #[logic(opaque)]
227    pub fn id(self) -> Id {
228        dead
229    }
230
231    #[check(ghost)]
232    #[ensures(*result == self.id())]
233    pub fn id_ghost(&self) -> Ghost<Id> {
234        snapshot!(self.id()).into_ghost()
235    }
236
237    /// Returns a raw pointer to the underlying data in this cell.
238    #[trusted]
239    #[ensures(true)]
240    pub fn as_ptr(&self) -> *mut T {
241        self.0.get()
242    }
243
244    /// Returns a `&PermCell<T>` from a `&mut T`
245    #[trusted]
246    #[check(terminates)]
247    #[ensures(result.0.id() == result.1.id())]
248    #[ensures(^t == (^result.1)@)]
249    #[ensures(*t == result.1@)]
250    pub fn from_mut(t: &mut T) -> (&PermCell<T>, Ghost<&mut PermCellOwn<T>>) {
251        // SAFETY: `PermCell` is layout-compatible with `Cell` and `T` because it is `repr(transparent)`.
252        // SAFETY: `&mut` ensures unique access
253        let cell: &PermCell<T> = unsafe { &*(t as *mut T as *const Self) };
254        let perm = Ghost::conjure();
255        (cell, perm)
256    }
257}
258
259impl<T: Default> PermCell<T> {
260    /// Takes the value of the cell, leaving `Default::default()` in its place.
261    ///
262    /// # Safety
263    ///
264    /// You must ensure that no other borrows to the inner value of `self` exists when calling
265    /// this function.
266    ///
267    /// Creusot will check that all calls to this function are indeed safe: see the
268    /// [type documentation](PermCell#safety).
269    #[requires(self.id() == perm.id())]
270    #[ensures(self.id() == (^perm).id())]
271    #[ensures(result == perm@)]
272    #[ensures(T::default.postcondition((), (^perm)@))]
273    pub unsafe fn take(&self, perm: Ghost<&mut PermCellOwn<T>>) -> T {
274        unsafe { self.replace(perm, T::default()) }
275    }
276}
creusot_contracts/cell/permcell.rs

creusot_contracts/cell/
permcell.rs
