vstd/std_specs/
nonzero.rs

1use super::super::prelude::*;
2use super::cmp::{
3    OrdSpec, OrdSpecImpl, PartialEqSpec, PartialEqSpecImpl, PartialOrdSpec, PartialOrdSpecImpl,
4};
5use super::convert::FromSpecImpl;
6use super::ops::{BitOrSpec, BitOrSpecImpl};
7use core::cmp::Ordering;
8use core::num::{NonZero, ZeroablePrimitive};
9use core::ops::BitOr;
10
11verus! {
12
13#[verifier::external_trait_specification]
14#[verifier::external_trait_extension(ZeroablePrimitiveSpec via ZeroablePrimitiveSpecImpl)]
15pub trait ExZeroablePrimitive: Sized + Copy {
16    type ExternalTraitSpecificationFor: ZeroablePrimitive;
17
18    spec fn is_zero(self) -> bool;
19}
20
21macro_rules! impl_zeroable_primitive_spec_impl {
22    ($($t:ty),*) => {
23        $(
24            verus! {
25                impl ZeroablePrimitiveSpecImpl for $t {
26                    open spec fn is_zero(self) -> bool {
27                        self == 0
28                    }
29                }
30            }
31        )*
32    };
33}
34
35// The implementators of `ZeroablePrimitive` coincide with `Integer`.
36impl_zeroable_primitive_spec_impl!(char, u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize);
37
38#[verifier::external_type_specification]
39#[verifier::external_body]
40#[verifier::reject_recursive_types(T)]
41pub struct ExNonZero<T: ZeroablePrimitive>(NonZero<T>);
42
43impl<T: ZeroablePrimitive> View for NonZero<T> {
44    type V = T;
45
46    uninterp spec fn view(&self) -> Self::V;
47}
48
49// Need this to define `BitOrSpecImpl`
50pub uninterp spec fn nonzero_from_primitive<T: ZeroablePrimitive>(n: T) -> NonZero<T>;
51
52pub broadcast axiom fn axiom_nonzero_from_primitive_view_eq<T: ZeroablePrimitive>(n: T)
53    requires
54        !n.is_zero(),
55    ensures
56        #[trigger] nonzero_from_primitive(n)@ == n,
57;
58
59pub broadcast axiom fn axiom_view_nonzero_from_primitive_eq<T: ZeroablePrimitive>(n: NonZero<T>)
60    ensures
61        #[trigger] nonzero_from_primitive(n@) == n,
62;
63
64pub broadcast axiom fn axiom_nonzero_is_not_zero<T: ZeroablePrimitive>(n: NonZero<T>)
65    ensures
66        !(#[trigger] n@).is_zero(),
67;
68
69pub assume_specification<T: ZeroablePrimitive>[ NonZero::<T>::new ](n: T) -> (ret: Option<
70    NonZero<T>,
71>)
72    ensures
73        match ret {
74            Some(nz) => nz@ == n && !n.is_zero(),
75            None => n.is_zero(),
76        },
77    opens_invariants none
78    no_unwind
79;
80
81pub assume_specification<T: ZeroablePrimitive>[ NonZero::<T>::new_unchecked ](n: T) -> (ret:
82    NonZero<T>)
83    requires
84        !n.is_zero(),
85    ensures
86        ret@ == n,
87    opens_invariants none
88    no_unwind
89;
90
91#[verifier::inline]
92pub open spec fn nonzero_spec_get<T: ZeroablePrimitive>(n: NonZero<T>) -> T {
93    n@
94}
95
96#[verifier::when_used_as_spec(nonzero_spec_get)]
97pub assume_specification<T: ZeroablePrimitive>[ NonZero::<T>::get ](n: NonZero<T>) -> T
98    returns
99        n@,
100    opens_invariants none
101    no_unwind
102;
103
104impl<T: ZeroablePrimitive + PartialEqSpec> PartialEqSpecImpl for NonZero<T> {
105    open spec fn obeys_eq_spec() -> bool {
106        true
107    }
108
109    open spec fn eq_spec(&self, other: &Self) -> bool {
110        self.get().eq_spec(&other.get())
111    }
112}
113
114// Ord is not implemented because of the [`Destruct`](https://doc.rust-lang.org/std/marker/trait.Destruct.html) trait bound.
115impl<T: ZeroablePrimitive + PartialOrdSpec> PartialOrdSpecImpl for NonZero<T> {
116    open spec fn obeys_partial_cmp_spec() -> bool {
117        true
118    }
119
120    open spec fn partial_cmp_spec(&self, other: &Self) -> Option<Ordering> {
121        self.get().partial_cmp_spec(&other.get())
122    }
123}
124
125impl<T: ZeroablePrimitive + BitOrSpec<Output = T>> BitOrSpecImpl<T> for NonZero<T> {
126    open spec fn obeys_bitor_spec() -> bool {
127        true
128    }
129
130    open spec fn bitor_req(self, rhs: T) -> bool {
131        self.get().bitor_req(rhs)
132    }
133
134    open spec fn bitor_spec(self, rhs: T) -> Self::Output {
135        nonzero_from_primitive(self.get().bitor_spec(rhs))
136    }
137}
138
139impl<T: ZeroablePrimitive + BitOrSpec<Output = T>> BitOrSpecImpl<NonZero<T>> for NonZero<T> {
140    open spec fn obeys_bitor_spec() -> bool {
141        true
142    }
143
144    open spec fn bitor_req(self, rhs: NonZero<T>) -> bool {
145        self.get().bitor_req(rhs.get())
146    }
147
148    open spec fn bitor_spec(self, rhs: NonZero<T>) -> Self::Output {
149        nonzero_from_primitive(self.get().bitor_spec(rhs.get()))
150    }
151}
152
153impl<T: ZeroablePrimitive> FromSpecImpl<NonZero<T>> for T {
154    open spec fn obeys_from_spec() -> bool {
155        true
156    }
157
158    open spec fn from_spec(nz: NonZero<T>) -> Self {
159        nz.get()
160    }
161}
162
163pub assume_specification<T: ZeroablePrimitive>[ <NonZero<T> as Clone>::clone ](
164    nz: &NonZero<T>,
165) -> NonZero<T>
166    returns
167        nz,
168;
169
170pub broadcast group group_nonzero_axioms {
171    axiom_nonzero_from_primitive_view_eq,
172    axiom_view_nonzero_from_primitive_eq,
173    axiom_nonzero_is_not_zero,
174}
175
176} // verus!
vstd/std_specs/nonzero.rs

vstd/std_specs/
nonzero.rs
