Open i509VCB opened 2 years ago
This is a fun one, I'm pretty sure we discussed it. Because we only add 1, assuming 1ns per increment, it would take 213503.982335 years for it to wrap. So it wouldn't satisfy a theorem prover, but in this case I think it's reasonable to accept the safety justification.
Good catch, and I do think that the justification (stated well by raph) could at least be included in the doc comment.
Per the documentation of AtomicU64::fetch_add
This means that the following function will return zero if fetch_add is called U64::MAX times which violates the safety requirements for
NonZeroU64::new_unchecked
.