creusot_std/std/ptr/
nonnull.rs

1use super::PointerExt;
2use crate::prelude::*;
3use core::ptr::NonNull;
4
5impl<T: ?Sized> View for NonNull<T> {
6    type ViewTy = *mut T;
7    #[logic(opaque)]
8    fn view(self) -> *mut T {
9        dead
10    }
11}
12
13/// Additional lemmas for [`NonNull`].
14pub trait NonNullExt {
15    #[logic]
16    fn view_inj(n1: Self, n2: Self);
17}
18
19impl<T: ?Sized> NonNullExt for NonNull<T> {
20    /// Asserts that the `NonNull` is only defined by the contained pointer.
21    #[logic]
22    #[trusted]
23    #[ensures(n1@ == n2@ ==> n1 == n2)]
24    fn view_inj(n1: Self, n2: Self) {}
25}
26
27impl<T: ?Sized> DeepModel for NonNull<T> {
28    type DeepModelTy = <*mut T as DeepModel>::DeepModelTy;
29    #[logic(open, inline)]
30    fn deep_model(self) -> Self::DeepModelTy {
31        self.view().deep_model()
32    }
33}
34
35impl<T: ?Sized> PointerExt<T> for NonNull<T> {
36    #[logic(open, inline)]
37    fn addr_logic(self) -> usize {
38        self.view().addr_logic()
39    }
40
41    #[logic(open, inline)]
42    fn is_aligned_logic(self) -> bool {
43        self.view().is_aligned_logic()
44    }
45}
46
47impl<T: ?Sized> Invariant for NonNull<T> {
48    #[logic(open)]
49    fn invariant(self) -> bool {
50        !self.is_null_logic()
51    }
52}
53
54extern_spec! {
55    impl<T> NonNull<T> {
56        #[ensures(result.is_aligned_logic())]
57        const fn dangling() -> NonNull<T>;
58    }
59
60    impl<T> NonNull<T>
61        where T: ?Sized
62    {
63        #[requires(!ptr.is_null_logic())]
64        #[ensures(result@ == ptr)]
65        const unsafe fn new_unchecked(ptr: *mut T) -> NonNull<T>;
66
67        #[ensures(match result {
68            None => ptr.is_null_logic(),
69            Some(res) => res@ == ptr,
70        })]
71        const fn new(ptr: *mut T) -> Option<NonNull<T>>;
72
73        #[ensures(result.is_aligned_logic())]
74        const fn from_ref(r: &T) -> NonNull<T>;
75
76        #[ensures(result.is_aligned_logic())]
77        const fn from_mut(r: &mut T) -> NonNull<T>;
78
79        #[ensures(result == self@)]
80        const fn as_ptr(self) -> *mut T;
81
82        #[ensures(result@ == self@ as *mut U)]
83        const fn cast<U>(self) -> NonNull<U>;
84    }
85
86    impl<T> Clone for NonNull<T>
87        where T: ?Sized
88    {
89        #[ensures(result == *self)]
90        fn clone(&self) -> Self {
91            *self
92        }
93    }
94}
creusot_std/std/ptr/nonnull.rs

creusot_std/std/ptr/
nonnull.rs
