vstd_extra/external/
nonnull.rs

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

vstd_extra/external/
nonnull.rs
