vstd/
cell.rs

1#![allow(deprecated)]
2#![allow(unused_imports)]
3
4use core::cell::UnsafeCell;
5use core::marker;
6use core::{mem, mem::MaybeUninit};
7
8use super::invariant::*;
9use super::modes::*;
10use super::pervasive::*;
11use super::prelude::*;
12pub use super::raw_ptr::MemContents;
13use super::set::*;
14use super::*;
15
16verus! {
17
18broadcast use {super::map::group_map_axioms, super::set::group_set_axioms};
19// TODO implement: borrow_mut; figure out Drop, see if we can avoid leaking?
20
21/// `PCell<V>` (which stands for "permissioned call") is the primitive Verus `Cell` type.
22///
23/// Technically, it is a wrapper around
24/// `core::cell::UnsafeCell<core::mem::MaybeUninit<V>>`, and thus has the same runtime
25/// properties: there are no runtime checks (as there would be for Rust's traditional
26/// [`core::cell::RefCell`](https://doc.rust-lang.org/core/cell/struct.RefCell.html)).
27/// Its data may be uninitialized.
28///
29/// Furthermore (and unlike both
30/// [`core::cell::Cell`](https://doc.rust-lang.org/core/cell/struct.Cell.html) and
31/// [`core::cell::RefCell`](https://doc.rust-lang.org/core/cell/struct.RefCell.html)),
32/// a `PCell<V>` may be `Sync` (depending on `V`).
33/// Thanks to verification, Verus ensures that access to the cell is data-race-free.
34///
35/// `PCell` uses a _ghost permission token_ similar to [`simple_pptr::PPtr`] -- see the [`simple_pptr::PPtr`]
36/// documentation for the basics.
37/// For `PCell`, the associated type of the permission token is [`cell::PointsTo`].
38///
39/// ### Differences from `PPtr`.
40///
41/// The key difference is that, whereas [`simple_pptr::PPtr`] represents a fixed address in memory,
42/// a `PCell` has _no_ fixed address because a `PCell` might be moved.
43/// As such, the [`pcell.id()`](PCell::id) does not correspond to a memory address; rather,
44/// it is a unique identifier that is fixed for a given cell, even when it is moved.
45///
46/// The arbitrary ID given by [`pcell.id()`](PCell::id) is of type [`CellId`].
47/// Despite the fact that it is, in some ways, "like a pointer", note that
48/// `CellId` does not support any meangingful arithmetic,
49/// has no concept of a "null ID",
50/// and has no runtime representation.
51///
52/// Also note that the `PCell` might be dropped before the `PointsTo` token is dropped,
53/// although in that case it will no longer be possible to use the `PointsTo` in `exec` code
54/// to extract data from the cell.
55///
56/// ### Example (TODO)
57#[verifier::external_body]
58#[verifier::accept_recursive_types(V)]
59pub struct PCell<V> {
60    ucell: UnsafeCell<MaybeUninit<V>>,
61}
62
63/// `PCell` is _always_ safe to `Send` or `Sync`. Rather, it is the [`PointsTo`] object where `Send` and `Sync` matter.
64/// (It doesn't matter if you move the bytes to another thread if you can't access them.)
65#[verifier::external]
66unsafe impl<T> Sync for PCell<T> {
67
68}
69
70#[verifier::external]
71unsafe impl<T> Send for PCell<T> {
72
73}
74
75/// Permission object associated with a [`PCell<V>`].
76///
77/// See the documentation of [`PCell<V>`] for more information.
78// PointsTo<V>, on the other hand, needs to inherit both Send and Sync from the V,
79// which it does by default in the given definition.
80// (Note: this depends on the current behavior that #[verifier::spec] fields are still counted for marker traits)
81#[verifier::external_body]
82#[verifier::reject_recursive_types_in_ground_variants(V)]
83pub tracked struct PointsTo<V> {
84    phantom: marker::PhantomData<V>,
85    no_copy: NoCopy,
86}
87
88pub ghost struct PointsToData<V> {
89    pub pcell: CellId,
90    pub mem_contents: MemContents<V>,
91}
92
93#[doc(hidden)]
94#[macro_export]
95macro_rules! pcell_points_internal {
96    [$pcell:expr => $val:expr] => {
97        $crate::vstd::cell::PointsToData {
98            pcell: $pcell,
99            mem_contents: $val,
100        }
101    };
102}
103
104#[macro_export]
105macro_rules! pcell_points {
106    [$($tail:tt)*] => {
107        $crate::vstd::prelude::verus_proof_macro_exprs!(
108            $crate::vstd::cell::pcell_points_internal!($($tail)*)
109        )
110    }
111}
112
113pub use pcell_points_internal;
114pub use pcell_points;
115
116#[verifier::external_body]
117pub struct CellId {
118    id: int,
119}
120
121impl<V> PointsTo<V> {
122    /// The [`CellId`] of the [`PCell`] this permission is associated with.
123    pub uninterp spec fn id(&self) -> CellId;
124
125    /// The contents of the cell, either unitialized or initialized to some `V`.
126    pub uninterp spec fn mem_contents(&self) -> MemContents<V>;
127
128    pub open spec fn view(self) -> PointsToData<V> {
129        PointsToData { pcell: self.id(), mem_contents: self.mem_contents() }
130    }
131
132    /// Is this cell initialized?
133    #[verifier::inline]
134    pub open spec fn is_init(&self) -> bool {
135        self.mem_contents().is_init()
136    }
137
138    /// Is this cell uninitialized?
139    #[verifier::inline]
140    pub open spec fn is_uninit(&self) -> bool {
141        self.mem_contents().is_uninit()
142    }
143
144    /// Value of the cell (if initialized)
145    #[verifier::inline]
146    pub open spec fn value(&self) -> V
147        recommends
148            self.is_init(),
149    {
150        self.mem_contents().value()
151    }
152}
153
154impl<V> PCell<V> {
155    /// A unique ID for the cell.
156    pub uninterp spec fn id(&self) -> CellId;
157
158    /// Return an empty ("uninitialized") cell.
159    #[inline(always)]
160    #[verifier::external_body]
161    pub const fn empty() -> (pt: (PCell<V>, Tracked<PointsTo<V>>))
162        ensures
163            pt.1@@ === pcell_points![ pt.0.id() => MemContents::Uninit ],
164    {
165        let p = PCell { ucell: UnsafeCell::new(MaybeUninit::uninit()) };
166        (p, Tracked::assume_new())
167    }
168
169    #[inline(always)]
170    #[verifier::external_body]
171    pub const fn new(v: V) -> (pt: (PCell<V>, Tracked<PointsTo<V>>))
172        ensures
173            pt.1@@ === pcell_points! [ pt.0.id() => MemContents::Init(v) ],
174    {
175        let p = PCell { ucell: UnsafeCell::new(MaybeUninit::new(v)) };
176        (p, Tracked::assume_new())
177    }
178
179    #[inline(always)]
180    #[verifier::external_body]
181    pub fn put(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, v: V)
182        requires
183            old(perm)@ === pcell_points![ self.id() => MemContents::Uninit ],
184        ensures
185            perm@ === pcell_points![ self.id() => MemContents::Init(v) ],
186        opens_invariants none
187        no_unwind
188    {
189        unsafe {
190            *(self.ucell.get()) = MaybeUninit::new(v);
191        }
192    }
193
194    #[inline(always)]
195    #[verifier::external_body]
196    pub fn take(&self, Tracked(perm): Tracked<&mut PointsTo<V>>) -> (v: V)
197        requires
198            self.id() === old(perm)@.pcell,
199            old(perm).is_init(),
200        ensures
201            perm.id() === old(perm)@.pcell,
202            perm.mem_contents() === MemContents::Uninit,
203            v === old(perm).value(),
204        opens_invariants none
205        no_unwind
206    {
207        unsafe {
208            let mut m = MaybeUninit::uninit();
209            mem::swap(&mut m, &mut *self.ucell.get());
210            m.assume_init()
211        }
212    }
213
214    #[inline(always)]
215    #[verifier::external_body]
216    pub fn replace(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> (out_v: V)
217        requires
218            self.id() === old(perm)@.pcell,
219            old(perm).is_init(),
220        ensures
221            perm.id() === old(perm)@.pcell,
222            perm.mem_contents() === MemContents::Init(in_v),
223            out_v === old(perm).value(),
224        opens_invariants none
225        no_unwind
226    {
227        unsafe {
228            let mut m = MaybeUninit::new(in_v);
229            mem::swap(&mut m, &mut *self.ucell.get());
230            m.assume_init()
231        }
232    }
233
234    // The reason for the the lifetime parameter 'a is
235    // that `self` actually contains the data in its interior, so it needs
236    // to outlive the returned borrow.
237    #[inline(always)]
238    #[verifier::external_body]
239    pub fn borrow<'a>(&'a self, Tracked(perm): Tracked<&'a PointsTo<V>>) -> (v: &'a V)
240        requires
241            self.id() === perm@.pcell,
242            perm.is_init(),
243        ensures
244            *v === perm.value(),
245        opens_invariants none
246        no_unwind
247    {
248        unsafe { (*self.ucell.get()).assume_init_ref() }
249    }
250
251    //////////////////////////////////
252    // Untrusted functions below here
253    #[inline(always)]
254    pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>) -> (v: V)
255        requires
256            self.id() === perm@.pcell,
257            perm.is_init(),
258        ensures
259            v === perm.value(),
260        opens_invariants none
261        no_unwind
262    {
263        let tracked mut perm = perm;
264        self.take(Tracked(&mut perm))
265    }
266    // TODO this should replace the external_body implementation of `new` above;
267    // however it requires unstable features: const_mut_refs and const_refs_to_cell
268    //#[inline(always)]
269    //pub const fn new(v: V) -> (pt: (PCell<V>, Tracked<PointsTo<V>>))
270    //    ensures (pt.1@@ === PointsToData{ pcell: pt.0.id(), value: MemContents::Init(v) }),
271    //{
272    //    let (p, Tracked(mut t)) = Self::empty();
273    //    p.put(Tracked(&mut t), v);
274    //    (p, Tracked(t))
275    //}
276
277}
278
279impl<V: Copy> PCell<V> {
280    #[inline(always)]
281    #[verifier::external_body]
282    pub fn write(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V)
283        requires
284            self.id() === old(perm)@.pcell,
285            old(perm).is_init(),
286        ensures
287            perm.id() === old(perm)@.pcell,
288            perm.mem_contents() === MemContents::Init(in_v),
289        opens_invariants none
290        no_unwind
291    {
292        let _out = self.replace(Tracked(&mut *perm), in_v);
293    }
294}
295
296struct InvCellPred {}
297
298impl<T> InvariantPredicate<(Set<T>, PCell<T>), PointsTo<T>> for InvCellPred {
299    closed spec fn inv(k: (Set<T>, PCell<T>), perm: PointsTo<T>) -> bool {
300        let (possible_values, pcell) = k;
301        {
302            &&& perm.is_init()
303            &&& possible_values.contains(perm.value())
304            &&& pcell.id() === perm@.pcell
305        }
306    }
307}
308
309#[verifier::reject_recursive_types(T)]
310pub struct InvCell<T> {
311    possible_values: Ghost<Set<T>>,
312    pcell: PCell<T>,
313    perm_inv: Tracked<LocalInvariant<(Set<T>, PCell<T>), PointsTo<T>, InvCellPred>>,
314}
315
316impl<T> InvCell<T> {
317    #[verifier::type_invariant]
318    closed spec fn wf(&self) -> bool {
319        &&& self.perm_inv@.constant() === (self.possible_values@, self.pcell)
320    }
321
322    pub closed spec fn inv(&self, val: T) -> bool {
323        &&& self.possible_values@.contains(val)
324    }
325
326    pub fn new(val: T, Ghost(f): Ghost<spec_fn(T) -> bool>) -> (cell: Self)
327        requires
328            f(val),
329        ensures
330            forall|v| f(v) <==> cell.inv(v),
331    {
332        let (pcell, Tracked(perm)) = PCell::new(val);
333        let ghost possible_values = Set::new(f);
334        let tracked perm_inv = LocalInvariant::new((possible_values, pcell), perm, 0);
335        InvCell { possible_values: Ghost(possible_values), pcell, perm_inv: Tracked(perm_inv) }
336    }
337}
338
339impl<T> InvCell<T> {
340    pub fn replace(&self, val: T) -> (old_val: T)
341        requires
342            self.inv(val),
343        ensures
344            self.inv(old_val),
345    {
346        proof {
347            use_type_invariant(self);
348        }
349        let r;
350        open_local_invariant!(self.perm_inv.borrow() => perm => {
351            r = self.pcell.replace(Tracked(&mut perm), val);
352        });
353        r
354    }
355}
356
357impl<T: Copy> InvCell<T> {
358    pub fn get(&self) -> (val: T)
359        ensures
360            self.inv(val),
361    {
362        proof {
363            use_type_invariant(self);
364        }
365        let r;
366        open_local_invariant!(self.perm_inv.borrow() => perm => {
367            r = *self.pcell.borrow(Tracked(&perm));
368        });
369        r
370    }
371}
372
373} // verus!
vstd/cell.rs

vstd/
cell.rs
