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

vstd/
cell.rs
