Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393#![allow(deprecated)]#![allow(unused_imports)]
use core::cell::UnsafeCell;use core::marker;use core::{mem, mem::MaybeUninit};
use super::invariant::*;use super::iset::*;use super::modes::*;use super::pervasive::*;use super::prelude::*;pub use super::raw_ptr::MemContents;use super::*;
pub mod invcell;pub mod pcell;pub mod pcell_maybe_uninit;
// note that almost everything in this module is now deprecated and will be deleted
verus! {
broadcast use {super::imap::group_imap_lemmas, super::iset::group_iset_lemmas};
/// **Now deprecated** See [`pcell::PCell`] or [`pcell_maybe_uninit::PCell`] instead////// `PCell<V>` (which stands for "permissioned call") is the primitive Verus `Cell` type.////// Technically, it is a wrapper around/// `core::cell::UnsafeCell<core::mem::MaybeUninit<V>>`, and thus has the same runtime/// properties: there are no runtime checks (as there would be for Rust's traditional/// [`core::cell::RefCell`](https://doc.rust-lang.org/core/cell/struct.RefCell.html))./// Its data may be uninitialized.////// Furthermore (and unlike both/// [`core::cell::Cell`](https://doc.rust-lang.org/core/cell/struct.Cell.html) and/// [`core::cell::RefCell`](https://doc.rust-lang.org/core/cell/struct.RefCell.html)),/// a `PCell<V>` may be `Sync` (depending on `V`)./// Thanks to verification, Verus ensures that access to the cell is data-race-free.////// `PCell` uses a _ghost permission token_ similar to [`simple_pptr::PPtr`] -- see the [`simple_pptr::PPtr`]/// documentation for the basics./// For `PCell`, the associated type of the permission token is [`cell::PointsTo`].////// ### Differences from `PPtr`.////// The key difference is that, whereas [`simple_pptr::PPtr`] represents a fixed address in memory,/// a `PCell` has _no_ fixed address because a `PCell` might be moved./// As such, the [`pcell.id()`](PCell::id) does not correspond to a memory address; rather,/// it is a unique identifier that is fixed for a given cell, even when it is moved.////// The arbitrary ID given by [`pcell.id()`](PCell::id) is of type [`CellId`]./// Despite the fact that it is, in some ways, "like a pointer", note that/// `CellId` does not support any meangingful arithmetic,/// has no concept of a "null ID",/// and has no runtime representation.////// Also note that the `PCell` might be dropped before the `PointsTo` token is dropped,/// although in that case it will no longer be possible to use the `PointsTo` in `exec` code/// to extract data from the cell.#[cfg_attr(not(verus_verify_core), deprecated = "use `vstd::cell::pcell::PCell` or `vstd::cell::pcell_maybe_uninit::PCell` instead")]#[verifier::external_body]#[verifier::accept_recursive_types(V)]pub struct PCell<V> { ucell: UnsafeCell<MaybeUninit<V>>,}
/// `PCell` is _always_ safe to `Send` or `Sync`. Rather, it is the [`PointsTo`] object where `Send` and `Sync` matter./// (It doesn't matter if you move the bytes to another thread if you can't access them.)#[verifier::external]unsafe impl<T> Sync for PCell<T> {
}
#[verifier::external]unsafe impl<T> Send for PCell<T> {
}
/// Permission object associated with a [`PCell<V>`].////// See the documentation of [`PCell<V>`] for more information.// PointsTo<V>, on the other hand, needs to inherit both Send and Sync from the V,// which it does by default in the given definition.// (Note: this depends on the current behavior that #[verifier::spec] fields are still counted for marker traits)#[verifier::external_body]#[verifier::reject_recursive_types_in_ground_variants(V)]pub tracked struct PointsTo<V> { phantom: marker::PhantomData<V>, no_copy: NoCopy,}
pub ghost struct PointsToData<V> { pub pcell: CellId, pub mem_contents: MemContents<V>,}
#[doc(hidden)]#[macro_export]macro_rules! pcell_points_internal { [$pcell:expr => $val:expr] => { $crate::vstd::cell::PointsToData { pcell: $pcell, mem_contents: $val, } };}
#[macro_export]macro_rules! pcell_points { [$($tail:tt)*] => { $crate::vstd::prelude::verus_proof_macro_exprs!( $crate::vstd::cell::pcell_points_internal!($($tail)*) ) }}
pub use pcell_points_internal;pub use pcell_points;
#[verifier::external_body]pub struct CellId { id: int,}
impl<V> PointsTo<V> { /// The [`CellId`] of the [`PCell`] this permission is associated with. pub uninterp spec fn id(&self) -> CellId;
/// The contents of the cell, either unitialized or initialized to some `V`. pub uninterp spec fn mem_contents(&self) -> MemContents<V>;
pub open spec fn view(self) -> PointsToData<V> { PointsToData { pcell: self.id(), mem_contents: self.mem_contents() } }
/// Is this cell initialized? #[verifier::inline] pub open spec fn is_init(&self) -> bool { self.mem_contents().is_init() }
/// Is this cell uninitialized? #[verifier::inline] pub open spec fn is_uninit(&self) -> bool { self.mem_contents().is_uninit() }
/// Value of the cell (if initialized) #[verifier::inline] pub open spec fn value(&self) -> V recommends self.is_init(), { self.mem_contents().value() }}
#[cfg_attr(not(verus_verify_core), deprecated = "use `vstd::cell::pcell::PCell` or `vstd::cell::pcell_maybe_uninit::PCell` instead")]impl<V> PCell<V> { /// A unique ID for the cell. pub uninterp spec fn id(&self) -> CellId;
/// Return an empty ("uninitialized") cell. #[inline(always)] #[verifier::external_body] pub const fn empty() -> (pt: (PCell<V>, Tracked<PointsTo<V>>)) ensures pt.1@@ == pcell_points![ pt.0.id() => MemContents::Uninit ], { let p = PCell { ucell: UnsafeCell::new(MaybeUninit::uninit()) }; (p, Tracked::assume_new()) }
#[inline(always)] #[verifier::external_body] pub const fn new(v: V) -> (pt: (PCell<V>, Tracked<PointsTo<V>>)) ensures pt.1@@ == pcell_points! [ pt.0.id() => MemContents::Init(v) ], { let p = PCell { ucell: UnsafeCell::new(MaybeUninit::new(v)) }; (p, Tracked::assume_new()) }
#[inline(always)] #[verifier::external_body] pub fn put(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, v: V) requires old(perm)@ == pcell_points![ self.id() => MemContents::Uninit ], ensures final(perm)@ == pcell_points![ self.id() => MemContents::Init(v) ], opens_invariants none no_unwind { unsafe { *(self.ucell.get()) = MaybeUninit::new(v); } }
#[inline(always)] #[verifier::external_body] pub fn take(&self, Tracked(perm): Tracked<&mut PointsTo<V>>) -> (v: V) requires self.id() == old(perm)@.pcell, old(perm).is_init(), ensures final(perm).id() == old(perm)@.pcell, final(perm).mem_contents() == MemContents::Uninit, v == old(perm).value(), opens_invariants none no_unwind { unsafe { let mut m = MaybeUninit::uninit(); mem::swap(&mut m, &mut *self.ucell.get()); m.assume_init() } }
#[inline(always)] #[verifier::external_body] pub fn replace(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> (out_v: V) requires self.id() == old(perm)@.pcell, old(perm).is_init(), ensures final(perm).id() == old(perm)@.pcell, final(perm).mem_contents() == MemContents::Init(in_v), out_v == old(perm).value(), opens_invariants none no_unwind { unsafe { let mut m = MaybeUninit::new(in_v); mem::swap(&mut m, &mut *self.ucell.get()); m.assume_init() } }
// The reason for the the lifetime parameter 'a is // that `self` actually contains the data in its interior, so it needs // to outlive the returned borrow. #[inline(always)] #[verifier::external_body] pub fn borrow<'a>(&'a self, Tracked(perm): Tracked<&'a PointsTo<V>>) -> (v: &'a V) requires self.id() == perm@.pcell, perm.is_init(), ensures *v == perm.value(), opens_invariants none no_unwind { unsafe { (*self.ucell.get()).assume_init_ref() } }
////////////////////////////////// // Untrusted functions below here #[inline(always)] pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>) -> (v: V) requires self.id() == perm@.pcell, perm.is_init(), ensures v == perm.value(), opens_invariants none no_unwind { let tracked mut perm = perm; self.take(Tracked(&mut perm)) }
#[doc(hidden)] #[inline(always)] #[verifier::external_body] pub fn borrow_mut<'a>(&'a self, Tracked(perm): Tracked<&'a mut PointsTo<V>>) -> (v: &'a mut V) requires self.id() == perm@.pcell, perm.is_init(), ensures *v == old(perm).value(), final(perm).id() == old(perm).id(), final(perm).is_init(), final(perm).value() == *final(v), opens_invariants none no_unwind { unsafe { (*self.ucell.get()).assume_init_mut() } }}
#[cfg_attr(not(verus_verify_core), deprecated = "use `vstd::cell::pcell::PCell` or `vstd::cell::pcell_maybe_uninit::PCell` instead")]impl<V: Copy> PCell<V> { #[inline(always)] pub fn write(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) requires self.id() == old(perm)@.pcell, old(perm).is_init(), ensures final(perm).id() == old(perm)@.pcell, final(perm).mem_contents() == MemContents::Init(in_v), opens_invariants none no_unwind { let _out = self.replace(Tracked(&mut *perm), in_v); }}
struct InvCellPred {}
impl<T> InvariantPredicate<(ISet<T>, PCell<T>), PointsTo<T>> for InvCellPred { closed spec fn inv(k: (ISet<T>, PCell<T>), perm: PointsTo<T>) -> bool { let (possible_values, pcell) = k; { &&& perm.is_init() &&& possible_values.contains(perm.value()) &&& pcell.id() == perm@.pcell } }}
/// **Now deprecated** See [`invcell::InvCell`] instead#[cfg_attr(not(verus_verify_core), deprecated = "use `vstd::cell::invcell::InvCell` instead")]#[verifier::reject_recursive_types(T)]pub struct InvCell<T> { possible_values: Ghost<ISet<T>>, pcell: PCell<T>, perm_inv: Tracked<LocalInvariant<(ISet<T>, PCell<T>), PointsTo<T>, InvCellPred>>,}
#[cfg_attr(not(verus_verify_core), deprecated = "use `vstd::cell::invcell::InvCell` instead")]impl<T> InvCell<T> { #[verifier::type_invariant] closed spec fn wf(&self) -> bool { &&& self.perm_inv@.constant() == (self.possible_values@, self.pcell) }
pub closed spec fn inv(&self, val: T) -> bool { &&& self.possible_values@.contains(val) }
pub fn new(val: T, Ghost(f): Ghost<spec_fn(T) -> bool>) -> (cell: Self) requires f(val), ensures forall|v| f(v) <==> cell.inv(v), { let (pcell, Tracked(perm)) = PCell::new(val); let ghost possible_values = ISet::new(f); let tracked perm_inv = LocalInvariant::new((possible_values, pcell), perm, 0); InvCell { possible_values: Ghost(possible_values), pcell, perm_inv: Tracked(perm_inv) } }}
#[cfg_attr(not(verus_verify_core), deprecated = "use `vstd::cell::invcell::InvCell` instead")]impl<T> InvCell<T> { pub fn replace(&self, val: T) -> (old_val: T) requires self.inv(val), ensures self.inv(old_val), { proof { use_type_invariant(self); } let r; open_local_invariant!(self.perm_inv.borrow() => perm => { r = self.pcell.replace(Tracked(&mut perm), val); }); r }}
#[cfg_attr(not(verus_verify_core), deprecated = "use `vstd::cell::invcell::InvCell` instead")]impl<T: Copy> InvCell<T> { pub fn get(&self) -> (val: T) ensures self.inv(val), { proof { use_type_invariant(self); } let r; open_local_invariant!(self.perm_inv.borrow() => perm => { r = *self.pcell.borrow(Tracked(&perm)); }); r }}
} // verus!