Challenge 12: Safety of NonZero

• Status: Open
• Tracking Issue: #71
• Start date: 2024/08/23
• End date: 2025/04/10
• Reward: 10000 USD

Goal

Verify the safety of NonZero in core::num.

Assumptions

new and get leverage transmute_unchecked, so verifying the safety of these methods would require verifying that transmutations are safe. This task is out of scope for this challenge (instead, it's work for Challenge 1). For this challenge, for a transmutation from type T to type U, it suffices to write and verify a contract that T and U have the same size.

You may assume that each NonZeroInner type upholds the safety conditions of the ZeroablePrimitive trait. Specifically, you need not verify that the integer primitives which implement ZeroablePrimitive are valid when 0, or that transmutations to the Option type are sound.

Success Criteria

Part 1: new and new_unchecked

Verify the safety and correctness of NonZero::new and NonZero::new_unchecked.

Specifically, write and verify contracts specifying the following:

1. The preconditions specified by the SAFETY comments are upheld.
2. For an input n:
   a. A NonZero object is created if and only if the input was nonzero.
   b. The value of the NonZeroInner object equals n.

Part 2: Other Uses of unsafe

Verify the safety of the following functions and methods (all located within core::num::nonzero):

List of UBs

In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following undefined behaviors ref:

• Invoking undefined behavior via compiler intrinsics.
• Reading from uninitialized memory.
• Producing an invalid value.

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.