vstd_extra/external/
nonnull.rs

1use core::marker::PointeeSized;
2use core::ptr::NonNull;
3use vstd::prelude::*;
4use vstd::raw_ptr::*;
5
6verus! {
7
8#[verifier::external_type_specification]
9#[verifier::reject_recursive_types(T)]
10#[verifier::external_body]
11pub struct ExNonNull<T: PointeeSized>(NonNull<T>);
12
13// The model for NonNull<T> is *mut T, so we can reuse the existing pointer specs.
14// See https://doc.rust-lang.org/stable/std/ptr/struct.NonNull.html.
15pub uninterp spec fn ptr_mut_from_nonull<T: PointeeSized>(ptr: NonNull<T>) -> *mut T;
16
17// This is the type invariant, the address (represented by the View of *mut T)) is not zero.
18pub broadcast axiom fn axiom_nonull_is_nonnull<T: PointeeSized>(ptr: NonNull<T>)
19    ensures
20        (#[trigger] ptr_mut_from_nonull(ptr))@.addr != 0,
21;
22
23// Inverse function:
24// Constructing NonNull<T> from the *mut T model.
25pub uninterp spec fn nonnull_from_ptr_mut<T: PointeeSized>(ptr: *mut T) -> NonNull<T>;
26
27pub broadcast axiom fn axiom_ptr_mut_from_nonull_eq<T: PointeeSized>(ptr: NonNull<T>)
28    ensures
29        nonnull_from_ptr_mut(#[trigger] ptr_mut_from_nonull(ptr)) == ptr,
30;
31
32pub broadcast axiom fn axiom_nonull_from_ptr_mut_eq<T: PointeeSized>(ptr: *mut T)
33    requires
34        ptr@.addr != 0,
35    ensures
36        ptr_mut_from_nonull(#[trigger] nonnull_from_ptr_mut(ptr)) == ptr,
37;
38
39pub assume_specification<T: PointeeSized>[ NonNull::new_unchecked ](ptr: *mut T) -> NonNull<T>
40    requires
41        ptr@.addr != 0,
42    returns
43        nonnull_from_ptr_mut(ptr),
44;
45
46pub assume_specification<T: PointeeSized>[ NonNull::as_ptr ](_0: NonNull<T>) -> (ret: *mut T)
47    ensures
48        ret@.addr != 0,
49    returns
50        ptr_mut_from_nonull(_0),
51;
52
53// Specification for NonNull::dangling(), uninterptred because the ptr only has to satisfy the alignment requirement.
54// See https://doc.rust-lang.org/stable/std/ptr/struct.NonNull.html#method.dangling.
55pub uninterp spec fn nonnull_dangling_spec<T>() -> NonNull<T>;
56
57pub assume_specification<T>[ NonNull::dangling ]() -> (ret: NonNull<T>)
58    ensures
59        ptr_mut_from_nonull(ret)@.addr as nat % align_of::<T>() as nat == 0,
60    returns
61        nonnull_dangling_spec::<T>(),
62;
63
64pub broadcast group group_nonnull {
65    axiom_nonull_is_nonnull,
66    axiom_ptr_mut_from_nonull_eq,
67    axiom_nonull_from_ptr_mut_eq,
68}
69
70} // verus!
vstd_extra/external/nonnull.rs

vstd_extra/external/
nonnull.rs
