Module nonzero 

Specifications for core::num::NonZero<usize> using a wrapper type NonZeroUsize.

Why wrappers instead of assume_specification

core::num::NonZero::<T>::{new, get} are generic over T: ZeroablePrimitive, where ZeroablePrimitive is a sealed external trait (its Sealed super-trait is private to core). That combination makes both standard escape hatches unusable:

• assume_specification requires a byte-for-byte signature match with the original generic function, so it cannot be specialized.
• #[verifier::external_trait_specification] for ZeroablePrimitive fails because the proxy trait cannot reproduce the private Sealed super-trait bound.

Either path forces Verus into --no-lifetime, which is infectious across crate boundaries (any downstream --importer would also need it).

Instead, we wrap the std NonZero<usize> in our own #[verifier::external_body] newtype and expose new/get as external_body exec functions whose Verus signatures only mention the wrapper. The std NonZero<usize> therefore never appears in any spec or wrapper signature, which lets verification run with full lifetime checking enabled.

Structs

NonZeroUsize

Functions

group_nonzero_axioms