vstd_extra/external/
nonnull.rs

1use super::nonzero::NonZeroUsize;
2use core::marker::PointeeSized;
3use core::ptr::NonNull;
4use vstd::prelude::*;
5use vstd::raw_ptr::*;
6use vstd::std_specs::cmp::*;
7
8verus! {
9
10#[verifier::external_type_specification]
11#[verifier::reject_recursive_types(T)]
12#[verifier::external_body]
13pub struct ExNonNull<T: PointeeSized>(NonNull<T>);
14
15pub trait NonNullAdditionalFns<T: PointeeSized> {
16    // The model for NonNull<T> is *mut T, so that we can reuse the existing pointer infrastructure.
17    // See https://doc.rust-lang.org/stable/std/ptr/struct.NonNull.html.
18    spec fn view_ptr_mut(self) -> *mut T;
19
20    /// Specification for `NonNull::cast`.
21    spec fn cast_spec<U>(self) -> NonNull<U>;
22
23    /// Specification for `NonNull::dangling()`.
24    spec fn dangling_spec() -> NonNull<T>;
25
26    /// Type invariant: the address of the pointer is non-null.
27    broadcast proof fn lemma_addr_is_nonnull(self)
28        ensures
29            !(#[trigger] self.view_ptr_mut()).is_null(),
30    ;
31
32    spec fn addr_spec(self) -> NonZeroUsize;
33
34    broadcast proof fn lemma_addr_view_eq_view_ptr_mut(self)
35        ensures
36            (#[trigger] self.addr_spec()).view() == self.view_ptr_mut().addr(),
37    ;
38
39    /// A wrapper of `NonNull::addr` in `std`, here we use our own `NonZeroUsize`
40    fn addr_v(self) -> NonZeroUsize
41        returns
42            self.addr_spec(),
43    ;
44}
45
46impl<T: PointeeSized> NonNullAdditionalFns<T> for NonNull<T> {
47    uninterp spec fn view_ptr_mut(self) -> *mut T;
48
49    uninterp spec fn cast_spec<U>(self) -> NonNull<U>;
50
51    uninterp spec fn dangling_spec() -> NonNull<T>;
52
53    axiom fn lemma_addr_is_nonnull(self);
54
55    open spec fn addr_spec(self) -> NonZeroUsize {
56        NonZeroUsize::nonzero_usize_from_usize(self.view_ptr_mut()@.addr)
57    }
58
59    axiom fn lemma_addr_view_eq_view_ptr_mut(self);
60
61    #[verifier::external_body]
62    #[verifier::when_used_as_spec(nonnull_addr_spec_wrapper)]
63    fn addr_v(self) -> NonZeroUsize {
64        unimplemented!()
65    }
66}
67
68#[verifier::inline]
69pub open spec fn nonnull_addr_spec_wrapper<T: PointeeSized>(ptr: NonNull<T>) -> NonZeroUsize {
70    ptr.addr_spec()
71}
72
73#[verifier::inline]
74pub open spec fn nonnull_view_ptr_mut_wrapper<T: PointeeSized>(ptr: NonNull<T>) -> *mut T {
75    ptr.view_ptr_mut()
76}
77
78#[verifier::inline]
79pub open spec fn nonnull_cast_spec_wrapper<T: PointeeSized, U>(ptr: NonNull<T>) -> NonNull<U> {
80    ptr.cast_spec::<U>()
81}
82
83/// An uninterpreted specification that constructs a `NonNull<T>` from a raw pointer.
84pub uninterp spec fn nonnull_from_ptr_mut_spec<T: PointeeSized>(ptr: *mut T) -> NonNull<T>;
85
86#[verifier::inline]
87pub open spec fn nonnull_new_spec<T: PointeeSized>(ptr: *mut T) -> Option<NonNull<T>> {
88    if ptr.is_null() {
89        None
90    } else {
91        Some(nonnull_from_ptr_mut_spec(ptr))
92    }
93}
94
95/// The view of a `NonNull<T>` constructed from `*mut T` should be exactly that `*mut T`.
96pub broadcast axiom fn axiom_nonnull_from_ptr_mut_spec_eq<T: PointeeSized>(ptr: *mut T)
97    requires
98        !ptr.is_null(),
99    ensures
100        (#[trigger] nonnull_from_ptr_mut_spec(ptr)).view_ptr_mut() == ptr,
101;
102
103/// The `NonNull` constructed from the view of a `NonNull<T>` should be exactly that `NonNull<T>`.
104/// Implies that `a.view_ptr_mut() == b.view_ptr_mut() ==> a == b`.
105pub broadcast axiom fn axiom_view_ptr_mut_eq<T: PointeeSized>(a: NonNull<T>)
106    ensures
107        nonnull_from_ptr_mut_spec(#[trigger] a.view_ptr_mut()) == a,
108;
109
110/// The semantic of casting a `NonNull<T>` should be the same as casting the underlying raw pointer
111/// (including the address, metadata, and provenance).
112pub broadcast axiom fn axiom_cast_spec_eq<T: PointeeSized, U>(ptr: NonNull<T>)
113    ensures
114        (#[trigger] ptr.cast_spec::<U>()).view_ptr_mut() == ptr.view_ptr_mut() as *mut U,
115;
116
117#[verifier::when_used_as_spec(nonnull_from_ptr_mut_spec)]
118pub assume_specification<T: PointeeSized>[ NonNull::new_unchecked ](ptr: *mut T) -> (ret: NonNull<
119    T,
120>)
121    requires
122        !ptr.is_null(),
123    ensures
124        ret.view_ptr_mut() == ptr,
125    returns
126        nonnull_from_ptr_mut_spec(ptr),
127;
128
129#[verifier::when_used_as_spec(nonnull_new_spec)]
130pub assume_specification<T: PointeeSized>[ core::ptr::NonNull::<T>::new ](ptr: *mut T) -> (ret:
131    core::option::Option<core::ptr::NonNull<T>>)
132    ensures
133        ret matches Some(nn) ==> nn.view_ptr_mut() == ptr,
134    returns
135        nonnull_new_spec(ptr),
136;
137
138#[verifier::when_used_as_spec(nonnull_view_ptr_mut_wrapper)]
139pub assume_specification<T: PointeeSized>[ NonNull::as_ptr ](ptr: NonNull<T>) -> (ret: *mut T)
140    ensures
141        !ret.is_null(),
142        ptr.view_ptr_mut() == ret,
143;
144
145#[verifier::when_used_as_spec(nonnull_cast_spec_wrapper)]
146pub assume_specification<T: PointeeSized, U>[ NonNull::<T>::cast::<U> ](ptr: NonNull<T>) -> (ret:
147    NonNull<U>)
148    ensures
149        ret.view_ptr_mut() == ptr.view_ptr_mut() as *mut U,
150    returns
151        ptr.cast_spec::<U>(),
152;
153
154// Specification for NonNull::dangling(), uninterpreted because the ptr only has to satisfy the alignment requirement.
155// See https://doc.rust-lang.org/stable/std/ptr/struct.NonNull.html#method.dangling.
156pub uninterp spec fn nonnull_dangling_spec<T>() -> NonNull<T>;
157
158#[verifier::when_used_as_spec(nonnull_dangling_spec)]
159pub assume_specification<T>[ NonNull::dangling ]() -> (ret: NonNull<T>)
160    ensures
161        ret.view_ptr_mut()@.addr as nat % align_of::<T>() as nat == 0,
162        ret.view_ptr_mut()@.provenance == Provenance::null(),
163    returns
164        nonnull_dangling_spec::<T>(),
165;
166
167#[verifier::inline]
168pub open spec fn nonnull_with_addr_spec_wrapper<T: PointeeSized>(
169    ptr: NonNull<T>,
170    addr: NonZeroUsize,
171) -> NonNull<T> {
172    ptr.with_addr_spec(addr)
173}
174
175// To prevent circular dependency
176pub trait NonNullAdditionalFnsMore<T>: NonNullAdditionalFns<T> where T: PointeeSized {
177    spec fn with_addr_spec(self, addr: NonZeroUsize) -> NonNull<T>;
178
179    proof fn lemma_with_addr_properties(self, addr: NonZeroUsize)
180        ensures
181            self.with_addr_spec(addr).view_ptr_mut()@.metadata == self.view_ptr_mut()@.metadata,
182            self.with_addr_spec(addr).view_ptr_mut()@.provenance == self.view_ptr_mut()@.provenance,
183            self.with_addr_spec(addr).view_ptr_mut()@.addr == addr.view(),
184    ;
185
186    fn with_addr_v(self, addr: NonZeroUsize) -> (ret: NonNull<T>)
187        returns
188            self.with_addr_spec(addr),
189    ;
190
191    /// A wrapper of `NonNull::map_addr` in `std`, here we use our own `NonZeroUsize`
192    fn map_addr_v<F: FnOnce(NonZeroUsize) -> NonZeroUsize>(self, f: F) -> (ret: NonNull<T>)
193        requires
194            f.requires((self.addr_spec(),)),
195        ensures
196            ret.view_ptr_mut()@.metadata == self.view_ptr_mut()@.metadata,
197            ret.view_ptr_mut()@.provenance == self.view_ptr_mut()@.provenance,
198            f.ensures((self.addr_spec(),), ret.addr_spec()),
199    ;
200}
201
202impl<T: PointeeSized> NonNullAdditionalFnsMore<T> for NonNull<T> {
203    #[verifier::external_body]
204    fn map_addr_v<F: FnOnce(NonZeroUsize) -> NonZeroUsize>(self, f: F) -> (ret: NonNull<T>) {
205        unimplemented!()
206    }
207
208    uninterp spec fn with_addr_spec(self, addr: NonZeroUsize) -> NonNull<T>;
209
210    axiom fn lemma_with_addr_properties(self, addr: NonZeroUsize);
211
212    #[verifier::external_body]
213    #[verifier::when_used_as_spec(nonnull_with_addr_spec_wrapper)]
214    fn with_addr_v(self, addr: NonZeroUsize) -> (ret: NonNull<T>) {
215        unimplemented!()
216    }
217}
218
219pub broadcast group group_nonull_axioms {
220    axiom_nonnull_from_ptr_mut_spec_eq,
221    axiom_cast_spec_eq,
222    axiom_view_ptr_mut_eq,
223    NonNullAdditionalFns::lemma_addr_view_eq_view_ptr_mut,
224    NonNullAdditionalFns::lemma_addr_is_nonnull,
225}
226
227} // verus!
vstd_extra/external/nonnull.rs

vstd_extra/external/
nonnull.rs
