Challenge 7: Verify safety of Atomic types and Atomic Intrinsics with Kani

[v3risec]

Summary

This PR adds a Kani-based solution for Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics.

The verification is organized around the three parts of the challenge:

1. Unsafe from_ptr methods — add safety contracts and proof_for_contract harnesses for the atomic from_ptr APIs.
2. Unsafe atomic operation helpers — add contracts for the internal unsafe helpers used by the safe atomic abstractions, together with proof harnesses over the supported atomic type families.
3. Atomic intrinsics — verify the complete set of ordering-specific atomic intrinsic operations required by the challenge through Kani-facing const-generic wrappers.

The PR also covers the challenge's optional ordering-validation requirement by adding contracts to safe atomic APIs whose documented ordering restrictions otherwise result in panics.

No atomic runtime implementation is replaced. The changes consist of safety contracts, Kani proof harnesses, verification helpers, and the safety contract dependency.

Challenge Coverage

Part 1: Unsafe from_ptr Methods

This PR adds safety contracts to:

• AtomicBool::from_ptr
• AtomicPtr::from_ptr
• AtomicI8::from_ptr
• AtomicU8::from_ptr
• AtomicI16::from_ptr
• AtomicU16::from_ptr
• AtomicI32::from_ptr
• AtomicU32::from_ptr
• AtomicI64::from_ptr
• AtomicU64::from_ptr
• AtomicI128::from_ptr
• AtomicU128::from_ptr

The contracts encode the safety obligations of the raw pointer used to construct the atomic reference, including:

• sufficient alignment for the corresponding atomic type;
• readable / initialized backing storage;
• writable backing storage for the lifetime of the returned atomic reference;
• preservation of the expected pointer identity in the returned reference.

Each contract is exercised with #[kani::proof_for_contract].

For the integer atomic types, the harnesses construct symbolic values in raw backing storage and select a valid aligned location from that storage before invoking from_ptr.

For AtomicPtr<T>::from_ptr, the stored pointer value itself remains arbitrary. Only the outer pointer containing that value is required to point to valid storage, matching the distinction made by the Challenge 7 specification.

The required representative pointee sizes for AtomicPtr<T> are covered with:

Pointee type	Size property
()	0 bytes
u8	1 byte
u16	2 bytes
u32	4 bytes
[u8; 3]	non-power-of-two size

This directly covers the Challenge 7 requirement for pointee sizes 0, 1, 2, 4, and at least one non-power-of-two size.

Part 2: Unsafe Atomic Operation Helpers

Safety contracts are added to the internal unsafe helpers used to implement atomic operations, including:

• atomic_store
• atomic_load
• atomic_swap
• atomic_add
• atomic_sub
• atomic_compare_exchange
• atomic_compare_exchange_weak
• atomic_and
• atomic_nand
• atomic_or
• atomic_xor
• atomic_max
• atomic_min
• atomic_umax
• atomic_umin

The contracts describe the local memory obligations of each operation.

For example:

• a load requires readable initialized storage;
• a store requires writable storage;
• read-modify-write operations require both readable and writable storage;
• mutation footprints are described with kani::modifies;
• postconditions preserve the memory predicates needed for subsequent accesses.

Ordering restrictions are also encoded where the internal helper accepts a runtime Ordering:

• loads accept Relaxed, Acquire, or SeqCst;
• stores accept Relaxed, Release, or SeqCst;
• compare-exchange failure orderings are restricted to Relaxed, Acquire, or SeqCst.

The proof harnesses instantiate these helpers over the atomic integer widths available on the target and, where applicable, pointer-sized integers and arbitrary pointer values. Platform-specific cases are guarded by the corresponding target_has_atomic / target_has_atomic_load_store configuration.

This keeps the verification aligned with the atomic capabilities exposed by each compilation target instead of assuming that every width is universally available.

Optional: Safe-API Ordering Contracts

Challenge 7 lists contracts preventing invalid atomic orderings as optional because an invalid ordering causes a panic rather than undefined behavior.

This PR includes that additional layer.

Ordering contracts are added to safe atomic APIs such as load, store, compare-exchange operations, and update-style APIs so their documented restrictions are explicit in the verification interface.

In particular:

• load excludes Release and AcqRel;
• store excludes Acquire and AcqRel;
• compare-exchange failure ordering excludes Release and AcqRel;
• update/fetch-style failure orderings use the same load-order restriction.

Dedicated proof harnesses exercise the safe abstractions with valid symbolic orderings across AtomicBool, integer atomics, pointer-sized atomics, and AtomicPtr where applicable.

The verification module also contains explicit panic-oriented cases for invalid compare-exchange/update failure orderings, documenting the distinction between the safe contract domain and the underlying panic behavior.

Part 3: Atomic Intrinsics

The Challenge 7 intrinsic list contains ordering-specific compiler intrinsics for:

• store;
• load;
• exchange;
• add;
• subtract;
• compare exchange;
• weak compare exchange;
• and;
• nand;
• or;
• xor;
• signed max;
• signed min;
• unsigned max;
• unsigned min.

A direct contract cannot currently be attached to the bodyless rustc_intrinsic declarations in a way usable by Kani's function-contract machinery.

To work around that limitation without changing the intrinsic implementation, this PR introduces small Kani-facing const-generic wrappers around the atomic intrinsics.

The wrappers carry the same local memory obligations as the operations they represent:

• store wrappers require writable storage;
• load wrappers require readable initialized storage;
• read-modify-write wrappers require both readable and writable storage and declare their mutation footprint;
• compare-exchange wrappers similarly require a readable/writable destination.

The wrappers exist solely as verification targets; the underlying atomic intrinsic remains the operation being executed.

Ordering coverage

The proof harnesses instantiate every ordering required by the Challenge 7 intrinsic table:

Operation family	Ordering combinations
Store	3
Load	3
Exchange	5
Add	5
Sub	5
Compare exchange	15
Weak compare exchange	15
And	5
Nand	5
Or	5
Xor	5
Max	5
Min	5
Umax	5
Umin	5
Total	91

For compare exchange and weak compare exchange, all 15 legal success/failure pairs listed by the challenge are instantiated independently rather than replacing them with a single representative ordering.

Each intrinsic proof also contains a reachability witness after the call, preventing an unsatisfiable contract domain from making the proof silently vacuous.

Type coverage

The intrinsic harness macros instantiate the operation families according to the target's supported atomic widths.

Depending on the operation, this includes:

• i8 / u8
• i16 / u16
• i32 / u32
• i64 / u64
• i128 / u128
• isize / usize
• pointer values where the intrinsic supports the pointer form

Signed extrema and unsigned extrema are intentionally instantiated over their respective signed and unsigned type families.

Verification Strategy

Memory predicates

The contracts use the repository/Kani memory predicates to express the pointer-side UB obligations required by the challenge.

In particular, the contracts distinguish between:

• memory that may be safely read;
• memory that may be safely written;
• alignment appropriate for the accessed type;
• initialized storage needed by atomic loads and read-modify-write operations.

This is important for atomics because an arbitrary numeric or pointer value is valid input, while the memory location through which the atomic access occurs still has strict validity, initialization, and alignment requirements.

Symbolic values

The operation operands and initial atomic values are symbolic wherever possible.

For AtomicPtr, pointer payloads are constructed from arbitrary addresses rather than restricting them to dereferenceable pointers. Atomic pointer operations manipulate the pointer value; they do not dereference the pointee.

Platform-specific atomic support

Proof generation follows Rust's target configuration using:

• target_has_atomic_load_store
• target_has_atomic

This ensures that the proof suite does not instantiate an atomic width on targets where that atomic operation is unavailable.

Non-vacuity

The proof harnesses use kani::cover after the verified call so that the expected call path is demonstrated to be reachable.

This provides an explicit check against accidentally proving a contract only because its preconditions are impossible to satisfy.

Scope and Limitations

Intrinsic contracts use wrappers

Kani currently cannot attach usable function contracts directly to the bodyless rustc_intrinsic declarations targeted by this challenge.

The const-generic wrappers in core::intrinsics::verify therefore serve as the Kani contract boundary.

They do not replace or reimplement the atomic operation: their bodies immediately call the corresponding intrinsic.

Generic types

The intrinsic declarations themselves are generic, but Kani ultimately verifies concrete monomorphizations.

The harness macros therefore instantiate the integer, pointer-sized, signed, unsigned, and pointer cases permitted by each intrinsic and by the target configuration.

For AtomicPtr::from_ptr, the specific representative pointee sizes are exactly the coverage permitted by Challenge 7.

Data Races

The current Kani harnesses are single-threaded and do not model concurrent thread interleavings. Consequently, this PR does not claim to discharge the Challenge 7 data-race obligation or prove the absence of races.

Verification

All added Challenge 7 harnesses pass locally with Kani.

Resolves #83

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.