[v3risec]

Summary

This PR adds Kani contracts and verification harnesses for Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics.

The verification covers three areas:

1. Unsafe from_ptr methods: safety contracts and proof_for_contract harnesses for the required atomic types.
2. Unsafe atomic operation helpers: contracts and harnesses for the internal helpers used by the safe atomic abstractions.
3. Atomic intrinsics: Kani-facing const-generic wrappers covering the ordering combinations required by the challenge.

The PR also verifies valid-ordering behavior of safe atomic APIs and includes expected-panic harnesses for invalid orderings. Callback-taking methods use ordinary proof harnesses, as explained below.

No standard-library runtime function bodies are changed.

Challenge Coverage

Part 1: Unsafe from_ptr Methods

Safety contracts and contract proof harnesses cover:

• 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 express pointer alignment, readable and writable backing storage, and preservation of pointer identity in the returned atomic reference.

Proof targets refer to the underlying Atomic implementations so that Kani can resolve them after the public atomic types became aliases. The harness calls still exercise the public atomic APIs.

For integer atomics, the harnesses use symbolic byte storage and symbolic offsets. Contract preconditions retain valid, sufficiently aligned locations.

The bool harness also uses symbolic byte storage, avoiding the unsupported arbitrary-bool-array layout under initialization checking. Its preconditions retain valid bool representations, and assertions and cover checks confirm that both false and true remain reachable.

For AtomicPtr::from_ptr, the stored pointer value is an arbitrary address. The outer pointer containing that value points to valid storage. The required representative pointee sizes are covered by:

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

Part 2: Unsafe Atomic Operation Helpers

Contracts and proof harnesses cover the 14 helpers listed in Part 2:

• 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_umax
• atomic_umin

The contracts distinguish the local memory requirements of each operation:

• Loads require readable, initialized storage.
• Stores require writable storage.
• Read-modify-write operations require readable and writable storage.
• Mutation footprints are expressed with kani::modifies.
• Postconditions preserve the memory predicates needed for subsequent accesses.

Runtime ordering restrictions are encoded where applicable:

• Loads accept Relaxed, Acquire, or SeqCst.
• Stores accept Relaxed, Release, or SeqCst.
• Compare-exchange failure orderings accept Relaxed, Acquire, or SeqCst.

The load/store harnesses explicitly instantiate VOLATILE = false.

Harnesses cover the supported integer widths and, where applicable, pointer-sized integers and arbitrary pointer values. Target-specific cases are guarded by target_has_atomic or target_has_atomic_load_store.

Optional: Safe APIs and Ordering Validation

Ordering contracts are retained for safe load, store, and compare-exchange methods.

The callback-taking methods fetch_update, try_update, and update instead use ordinary #[kani::proof] harnesses. Their previous modifies(self) contracts excluded legal callback writes to captured state or other memory.

For these methods, the harnesses:

• Express the valid fetch-order restriction explicitly with kani::assume.
• Use symbolic initial values, replacement values, and orderings.
• Exercise callbacks that modify captured state.
• Check returned values and final atomic values.
• Cover both Some and None paths for fetch_update and try_update.

These proofs cover the callbacks constructed by the harnesses; they do not claim a general mutation contract for every possible FnMut.

Expected-panic harnesses also cover invalid orderings for load, store, compare-exchange, and update methods.

Part 3: Atomic Intrinsics

Kani-facing wrappers provide contract boundaries around the bodyless atomic intrinsic declarations. Their bodies call the corresponding intrinsics directly.

The harnesses instantiate all 91 ordering combinations listed by the challenge:

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
Signed max	5
Signed min	5
Unsigned max	5
Unsigned min	5
Total	91

Both compare-exchange families enumerate all 15 required success/failure ordering pairs.

The type matrices include supported integer widths, pointer-sized integers, and pointer forms where permitted by the intrinsic. Signed and unsigned extrema use their respective type families.

Load/store wrappers explicitly select non-volatile accesses.

Verification Strategy

Inputs and initial values are symbolic wherever possible. Pointer payloads may contain arbitrary addresses; the atomic operations manipulate those values without dereferencing their pointees.

Contract proofs assume the declared preconditions. Ordinary callback harnesses state their ordering assumptions explicitly.

Successful-call harnesses include kani::cover checks to demonstrate reachability. The optional-update harnesses additionally check reachability of both update and no-update branches.

Proof generation follows the target's atomic capabilities rather than assuming every width is available on every platform.

Verification Results

CI passes for commit 4bb26f7, including:

• All eight Kani verification partitions across Ubuntu and macOS.
• Rust Tests.
• The other enabled PR checks.

Kani CI results

Additional local validation with -Z uninit-checks passed for:

• Nine callback harnesses covering fetch_update, try_update, and update across bool, i32, and pointer atomics.
• Two expected-panic harnesses checking invalid orderings.

These runs used the unmodified Kani version pinned by this repository. The CI configuration for this commit does not enable -Z uninit-checks; the initialization-checking results above were obtained locally.

Scope and Limitations

Initialization Checking and the Upstream Store Model

While investigating initialization checking, I found a Kani bug affecting atomic stores to initially uninitialized storage:

• Issue: -Z uninit-checks rejects valid atomic stores to uninitialized memory kani#5114
• Proposed fix: Fix atomic store reads and initialization tracking kani#5115

The existing model generates an unnecessary read of the old destination value for a store. Its initialization instrumentation also checks the old contents without recording the destination as initialized.

The proposed fix makes stores write-only while preserving exchange behavior, updates initialization tracking, and adds regression tests.

No Kani patch is included in this Challenge 7 PR or used for its reported verification results. The existing store harnesses use initialized storage; the initially-uninitialized case remains affected by the upstream issue. The store contract has not been strengthened to require prior initialization as a workaround.

Data Races

The harnesses are single-threaded and do not model concurrent thread interleavings. This PR does not claim to discharge the Challenge 7 data-race obligation.

The discussion of this requirement remains tracked in #733.

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.

[feliperodri]

Approving — leading solution for Challenge 7

Thanks @v3risec. Reviewed both open Challenge 7 solutions with our vacuity tooling and local Kani (pinned 0.67.0 / CBMC 6.8.0). This is complete and sound, and directly fixes the failure mode of the other solution (#578, whose contracts were decorative). Prioritizing it.

Coverage:

• Part 1: 12/12 from_ptr with real #[requires] (align + valid-for-read + valid-for-write) / #[ensures(ptr::eq)] and matching #[kani::proof_for_contract] — including AtomicI128/U128 (the exact gap that sank #578; the harnesses exist in source and compile on targets with 128-bit atomic support). AtomicPtr covered over pointee sizes 0/1/2/3/4 as the doc requires.
• Part 2: all 14 unsafe atomic ops (store/load/swap/add/sub/compare_exchange(_weak)/and/nand/or/xor/max/umax/umin + atomic_min) with requires + kani::modifies + ensures + proof_for_contract across every width + isize/usize + *mut u8, plus ordering #[requires] on the safe methods and 6 #[kani::should_panic] illegal-ordering proofs.
• Part 3: intrinsic wrappers (const-generic intrinsics can't carry contracts directly — kani#3345) with proof_for_contract enumerating orderings/type matrix.

Soundness (all clean):

• T1: no cfg body swaps — fn bodies unchanged, only attributes + use added.
• T2: n/a (no loops/invariants).
• T7: every contract has an explicit proof_for_contract; .github/workflows/kani.yml has no atomic autoharness entries, so — unlike #578 — the contracts are genuinely checked, not decorative.
• Not assume-the-conclusion; genuinely symbolic (kani::any() values, any_ordering() families covering all legal variants, arbitrary pointer addresses).
• No runtime std logic changed.

Local Kani (CBMC 6.8.0): 3/3 runnable-sample harnesses VERIFICATION SUCCESSFUL — harness_atomic_add_i32 (proof_for_contract), harness_safe_compare_exchange_panics_on_release (should_panic), harness_atomic_bool_from_ptr (proof_for_contract). harness_atomic_i128_from_ptr didn't register locally because 128-bit atomics are cfg-gated off on x86_64 — a target limitation, not an omission (the harness is present in source).

Note for the record: T-generic data-race / mixed-size overlapping-access UB is explicitly out of scope (Kani single-threaded model — consistent with the challenge, which points to concurrency being separate). Complete, sound, and the decisive improvement over #578.

[v3risec]

@feliperodri Thanks for the thorough review and approval! I really appreciate the detailed validation.

[v3risec]

I added an explicit #[kani::unwind(2)] bound to the proof harnesses for Atomic*::update. update is implemented as a retry loop around compare_exchange_weak. Without an explicit unwind bound, Kani/CBMC does not infer a finite bound for this loop and keeps unwinding it during symbolic execution, which caused these harnesses to run indefinitely.

The explicit bound does not change the implementation being verified; it only controls loop unwinding in the proof harness. This is sound for these harnesses because Kani keeps unwinding assertions enabled: if two unwindings were insufficient to cover a feasible execution under the current model, the corresponding unwinding assertion would fail instead of silently truncating the proof.

With #[kani::unwind(2)], the unwinding assertions for the update loops pass, and all 14 update harnesses verify successfully.

This bound should be understood as a bound for these single-threaded verification harnesses under Kani's current atomic model, rather than as a general semantic bound on Atomic::update. In particular, Rust permits compare_exchange_weak to fail spuriously.

[feliperodri]

@v3risec, a consistency note after re-reviewing #587 (Ch27, Arc).

Challenge 7's UB list requires the absence of data races, and this PR states that its harnesses are single-threaded and don't discharge that obligation. #587 is in the same position for Ch27. Both are approved as sound proofs toward their challenges, but neither solves its challenge on its own. Separately, CI doesn't pass -Z uninit-checks, so "reading from uninitialized memory" isn't checked automatically either.

You can address these in follow-up PRs. Whether solutions must cover data races, which Kani can't check, is being discussed in #733.

[feliperodri]

@v3risec, changing my review to request changes so this isn't merged as a solution to Challenge 7.

Challenge 7's UB list requires the absence of data races, and this PR states that its harnesses are single-threaded and don't discharge that obligation. Kani can't check data races, so this is a gap in the tool rather than in the proofs. #733 asks the committee how solutions should be judged on it. Until that's decided, a PR that leaves out a listed UB item doesn't complete the challenge.

The proofs themselves remain sound and useful. Separately, this has merge conflicts with main after the recent subtree syncs; could you rebase it?

[v3risec]

Thanks! I'm working on rebasing the PR.

[v3risec]

@feliperodri I have synchronized this branch with current main and updated the verification code for the atomic API changes.

CI passed for commit 4bb26f7, including all eight Kani verification partitions across Ubuntu and macOS, and Rust Tests.

The changes are:

• Updated the load/store proof targets, helper calls, and intrinsic wrappers to explicitly specify VOLATILE = false, resolving the const-generic compilation errors introduced by the upstream API changes. These proofs cover ordinary atomic accesses; the new volatile paths remain outside this PR's verification scope.
• Updated contract proof targets to refer to the underlying Atomic<T> implementations, which Kani can resolve after the public atomic types became aliases. Also corrected the target configuration for the pointer update harness.
• Changed the bool from_ptr harness to use symbolic byte storage, avoiding the unsupported arbitrary-bool-array layout under initialization checking. The contract preconditions retain valid bool representations, with assertions and cover checks confirming that both false and true are reachable.
• Replaced the contracts on fetch_update, try_update, and update with ordinary proof harnesses. Their previous modifies(self) specification excluded legal callback writes to captured state. The harnesses now express the ordering preconditions explicitly with kani::assume, exercise callbacks that modify captured state, and check returned values and final atomic values. The optional-update harnesses cover both Some and None.
• Fixed import formatting and added comments explaining the callback verification approach and its scope.

Regarding your note about -Z uninit-checks, I have now run all 338 Challenge 7 harnesses available on x86_64-unknown-linux-gnu with initialization checking enabled, using the unmodified Kani version pinned by this repository:

• 14 from_ptr harnesses.
• 135 unsafe-helper harnesses.
• 91 atomic-intrinsic harnesses.
• 98 safe-API harnesses, including 14 expected-panic harnesses.

All 338 passed, and all 374 cover properties were satisfied. The 128-bit cases were not registered on this target because of its atomic capability configuration. The CI configuration does not enable -Z uninit-checks, so the initialization-checking results above are additional local validation alongside the passing CI results.

No standard-library runtime function bodies were changed, and no Kani modifications were used for these verification results.

The verification remains single-threaded and does not discharge the data-race obligation discussed in #733.