Function axiom_nonnull_addr_nonzero 

pub broadcast proof fn axiom_nonnull_addr_nonzero<T: PointeeSized>(p: NonNull<T>)

ensures

(#[trigger] spec_nonnull_as_ptr(p))@.addr != 0,

The wrapped pointer “must always be non-null, even if the pointer is never dereferenced” (Reference).