Challenge 11: Safety of Methods for Numeric Primitive Types

  • Status: Open
  • Tracking Issue: #59
  • Start date: 2024-08-20
  • End date: 2024-12-10

Goal

Verify the safety of public unsafe methods for floats and integers in core::num.

To find the documentation for these methods, navigate first to the core::num documentation, then click on the appropriate primitive type in the left-side menu bar. For example, for i8::unchecked_add, click on i8.

Success Criteria

Part 1: Unsafe Integer Methods

Prove the absence of arithmetic overflow/underflow and undefined behavior in the following methods for each of the listed integer types, given that their safety preconditions are satisfied:

MethodInteger Types
unchecked_addi8, i16, i32, i64, i128, u8, u16, u32, u64, u128
unchecked_subi8, i16, i32, i64, i128, u8, u16, u32, u64, u128
unchecked_muli8, i16, i32, i64, i128, u8, u16, u32, u64, u128
unchecked_shli8, i16, i32, i64, i128, u8, u16, u32, u64, u128
unchecked_shri8, i16, i32, i64, i128, u8, u16, u32, u64, u128
unchecked_negi8, i16, i32, i64, i128

Part 2: Safe API Verification

Now, verify some of the safe APIs that leverage the unsafe integer methods from Part 1. Verify the absence of arithmetic overflow/underflow and undefined behavior of the following methods for each of the listed integer types:

MethodInteger Types
wrapping_shli8, i16, i32, i64, i128, u8, u16, u32, u64, u128
wrapping_shri8, i16, i32, i64, i128, u8, u16, u32, u64, u128
widening_mulu8, u16, u32, u64
carrying_mulu8, u16, u32, u64

Part 3: Float to Integer Conversion

Verify the absence of arithmetic overflow/underflow and undefined behavior in to_int_unchecked for f16, f32, f64, and f128.

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:

  • Invoking undefined behavior via compiler intrinsics.
  • Reading from uninitialized memory.
  • Mutating immutable bytes.
  • 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.