vstd_extra/external/
nonzero.rs

1//! Specifications for `core::num::NonZero<usize>` using a wrapper type `NonZeroUsize`.
2//!
3//! ## Why wrappers instead of `assume_specification`
4//!
5//! `core::num::NonZero::<T>::{new, get}` are generic over
6//! `T: ZeroablePrimitive`, where `ZeroablePrimitive` is a sealed external
7//! trait (its `Sealed` super-trait is private to `core`). That combination
8//! makes both standard escape hatches unusable:
9//!   * `assume_specification` requires a *byte-for-byte* signature match with
10//!     the original generic function, so it cannot be specialized.
11//!   * `#[verifier::external_trait_specification]` for `ZeroablePrimitive`
12//!     fails because the proxy trait cannot reproduce the private `Sealed`
13//!     super-trait bound.
14//!
15//! Either path forces Verus into `--no-lifetime`, which is infectious across
16//! crate boundaries (any downstream `--import`er would also need it).
17//!
18//! Instead, we wrap the std `NonZero<usize>` in our own
19//! `#[verifier::external_body]` newtype and expose `new`/`get` as
20//! `external_body` exec functions whose Verus signatures only mention the
21//! wrapper. The std `NonZero<usize>` therefore never appears in any spec or
22//! wrapper signature, which lets verification run with full lifetime checking
23//! enabled.
24use core::cmp::Ordering;
25use core::ops::BitOr;
26use vstd::prelude::*;
27use vstd::std_specs::cmp::*;
28use vstd::std_specs::ops::BitOrSpecImpl;
29
30verus! {
31
32#[verifier::external_body]
33#[derive(PartialEq, Eq, PartialOrd, Ord, Hash)]
34pub struct NonZeroUsize {
35    pub inner: core::num::NonZero<usize>,
36}
37
38impl View for NonZeroUsize {
39    type V = usize;
40
41    uninterp spec fn view(&self) -> Self::V;
42}
43
44impl NonZeroUsize {
45    pub uninterp spec fn nonzero_usize_from_usize(n: usize) -> Self;
46
47    pub broadcast axiom fn axiom_nonzero_usize_from_usize_view_eq(n: usize)
48        requires
49            n != 0,
50        ensures
51            (#[trigger] Self::nonzero_usize_from_usize(n)).view() == n,
52    ;
53
54    pub broadcast axiom fn axiom_view_nonzero_usize_from_usize_eq(self)
55        ensures
56            Self::nonzero_usize_from_usize(#[trigger] self.view()) == self,
57    ;
58
59    #[verifier::external_body]
60    pub const fn new(n: usize) -> (ret: Option<Self>)
61        ensures
62            match ret {
63                Some(nz) => nz.view() == n,
64                None => n == 0,
65            },
66    {
67        if let Some(inner) = core::num::NonZeroUsize::new(n) {
68            Some(NonZeroUsize { inner })
69        } else {
70            None
71        }
72    }
73
74    #[verifier::external_body]
75    #[verifier::when_used_as_spec(nonzero_usize_from_usize)]
76    pub const unsafe fn new_unchecked(n: usize) -> (ret: Self)
77        ensures
78            ret.view() == n,
79            ret == Self::nonzero_usize_from_usize(n),
80    {
81        NonZeroUsize { inner: core::num::NonZeroUsize::new_unchecked(n) }
82    }
83
84    #[verifier::external_body]
85    pub const fn get(&self) -> (ret: usize)
86        ensures
87            ret == self.view(),
88    {
89        self.inner.get()
90    }
91
92    broadcast axiom fn lemma_nonzero_neq_zero(self)
93        ensures
94            #[trigger] self.view() != 0,
95    ;
96}
97
98impl Clone for NonZeroUsize {
99    #[verifier::external_body]
100    fn clone(&self) -> (ret: Self)
101        ensures
102            ret.view() == self.view(),
103    {
104        NonZeroUsize { inner: self.inner }
105    }
106}
107
108impl Copy for NonZeroUsize {
109
110}
111
112impl PartialEqSpecImpl for NonZeroUsize {
113    open spec fn obeys_eq_spec() -> bool {
114        true
115    }
116
117    open spec fn eq_spec(&self, other: &Self) -> bool {
118        self.view() == other.view()
119    }
120}
121
122impl PartialOrdSpecImpl for NonZeroUsize {
123    open spec fn obeys_partial_cmp_spec() -> bool {
124        true
125    }
126
127    open spec fn partial_cmp_spec(&self, other: &Self) -> Option<Ordering> {
128        if self.view() < other.view() {
129            Some(Ordering::Less)
130        } else if self.view() > other.view() {
131            Some(Ordering::Greater)
132        } else {
133            Some(Ordering::Equal)
134        }
135    }
136}
137
138impl OrdSpecImpl for NonZeroUsize {
139    open spec fn obeys_cmp_spec() -> bool {
140        true
141    }
142
143    open spec fn cmp_spec(&self, other: &Self) -> Ordering {
144        vstd::std_specs::cmp::PartialOrdSpec::partial_cmp_spec(self, other)->0
145    }
146}
147
148pub broadcast group group_nonzero_axioms {
149    NonZeroUsize::lemma_nonzero_neq_zero,
150    NonZeroUsize::axiom_nonzero_usize_from_usize_view_eq,
151    NonZeroUsize::axiom_view_nonzero_usize_from_usize_eq,
152}
153
154impl BitOrSpecImpl<usize> for NonZeroUsize {
155    open spec fn obeys_bitor_spec() -> bool {
156        true
157    }
158
159    open spec fn bitor_req(self, rhs: usize) -> bool {
160        true
161    }
162
163    open spec fn bitor_spec(self, rhs: usize) -> Self {
164        Self::nonzero_usize_from_usize(self.view() | rhs)
165    }
166}
167
168impl BitOr<usize> for NonZeroUsize {
169    type Output = Self;
170
171    fn bitor(self, rhs: usize) -> (ret: Self::Output)
172        ensures
173            ret.view() == self.view() | rhs,
174    {
175        unsafe { Self::new_unchecked(self.get() | rhs) }
176    }
177}
178
179} // verus!
vstd_extra/external/nonzero.rs

vstd_extra/external/
nonzero.rs
