vstd_extra/
auxiliary.rs

1use vstd::atomic::PermissionU64;
2use vstd::cell::pcell::{PCell, PointsTo};
3use vstd::prelude::*;
4
5verus! {
6
7// Produces an arbitrary PointsTo permission for type T, this is sound because one can not use
8// such a permission to access memory.
9#[verifier(external_body)]
10pub proof fn arbitrary_cell_pointsto<T>() -> (tracked res: vstd::cell::pcell::PointsTo<T>) {
11    unimplemented!();
12}
13
14/// Extensional equality for `PermissionU64`: two permissions with the same
15/// `id()` and `value()` are equal. This is sound because `PermissionU64`'s
16/// view is determined entirely by `(patomic, value)`, and the tracked struct
17/// is a newtype wrapper around its view.
18pub axiom fn axiom_permission_u64_ext_eq(p1: PermissionU64, p2: PermissionU64)
19    requires
20        p1.id() == p2.id(),
21        p1.value() == p2.value(),
22    ensures
23        p1 == p2,
24;
25
26/// A Verus version of `unsafe { &mut *cell.get() }` for `UnsafeCell<T>`.
27/// FIXME: Waiting for official support from Verus.
28#[verifier::external_body]
29pub exec fn pcell_borrow_mut<'a, T>(cell: &'a PCell<T>, perm: &'a mut Tracked<PointsTo<T>>) -> (res:
30    &'a mut T)
31    requires
32        cell.id() == perm.id(),
33    ensures
34        *final(res) == *final(perm).value(),
35        final(perm).id() == old(perm).id(),
36    no_unwind
37{
38    // SAFETY: the caller must ensure that `perm` is a valid permission for `cell`.
39    unimplemented!();
40}
41
42} // verus!
vstd_extra/auxiliary.rs

vstd_extra/
auxiliary.rs
