Challenge 27: Verify safety of Arc functions

[Samuelsills]

Summary

Add Kani proof harnesses for Arc functions specified in Challenge #27:

Unsafe (12/12 — all required):

• assume_init (single + slice), from_raw, from_raw_in, increment_strong_count, increment_strong_count_in, decrement_strong_count, decrement_strong_count_in, get_mut_unchecked, downcast_unchecked, Weak::from_raw, Weak::from_raw_in

Safe (35/42 — 83%, exceeds 75% threshold):

• Allocation, conversion, cloning, downcasting, Weak pointer operations, trait implementations

All harnesses verified locally with Kani.

Resolves #383

[Samuelsills]

Verification Coverage Report

Unsafe Functions (12/12 — 100% ✅)

assume_init (single), assume_init (slice), from_raw, from_raw_in, increment_strong_count, increment_strong_count_in, decrement_strong_count, decrement_strong_count_in, get_mut_unchecked, downcast_unchecked, Weak::from_raw, Weak::from_raw_in

Safe Functions with Unsafe Code (35/42 — 83%, exceeds 75% threshold ✅)

Allocation, conversion, cloning, downcasting, Weak pointer operations, trait implementations.

Total: 47 harnesses (12 unsafe + 35 safe)

UBs Checked

• ✅ Accessing dangling or misaligned pointers
• ✅ Invoking UB via compiler intrinsics
• ✅ Mutating immutable bytes
• ✅ Producing an invalid value

Note on Data Races

In single-threaded Kani verification, data races cannot occur (no concurrent threads). Pointer validity, alignment, and initialization are verified for all operations.

Verification Approach

• Tool: Kani Rust Verifier
• Generic T limited to primitive types (i32) per spec allowance
• Allocators limited to Global per spec allowance

[Copilot]

Pull request overview

Adds Kani verification harnesses to alloc::sync (Arc/Weak) as part of Challenge #27 / tracking issue #383, aiming to model-check the safety contracts of selected APIs (including all required unsafe ones).

Changes:

• Introduces a #[cfg(kani)] verification module in library/alloc/src/sync.rs.
• Adds Kani proof harnesses covering 12 required unsafe Arc/Weak functions plus a broad set of safe Arc/Weak operations.

[Copilot]

Arc::increment_strong_count’s safety contract requires that the pointer comes from Arc::into_raw. This harness uses Arc::as_ptr(&a) instead, which means the proof is not exercising the API under its documented preconditions (and could be unsound under strict provenance assumptions). Consider obtaining ptr via Arc::into_raw(...) (and then balancing the extra strong count via Arc::from_raw/Arc::decrement_strong_count as in the docs).

Suggested change

	let ptr = Arc::as_ptr(&a);
	unsafe {
	Arc::increment_strong_count(ptr);
	}
	let a2 = unsafe { Arc::from_raw(ptr) };
	assert!(*a2 == 42);
	}
	#[kani::proof]
	fn verify_increment_strong_count_in() {
	let a = Arc::new_in(42i32, Global);
	let ptr = Arc::as_ptr(&a);
	unsafe {
	Arc::increment_strong_count_in(ptr, Global);
	}
	let a2 = unsafe { Arc::from_raw_in(ptr, Global) };
	let ptr = Arc::into_raw(a);
	unsafe {
	Arc::increment_strong_count(ptr);
	}
	let a1 = unsafe { Arc::from_raw(ptr) };
	let a2 = unsafe { Arc::from_raw(ptr) };
	assert!(*a1 == 42);
	assert!(*a2 == 42);
	}
	#[kani::proof]
	fn verify_increment_strong_count_in() {
	let a = Arc::new_in(42i32, Global);
	let (ptr, alloc) = Arc::into_raw_with_allocator(a);
	unsafe {
	Arc::increment_strong_count_in(ptr, alloc);
	}
	let a1 = unsafe { Arc::from_raw_in(ptr, alloc) };
	let a2 = unsafe { Arc::from_raw_in(ptr, alloc) };
	assert!(*a1 == 42);

[Copilot]

Arc::increment_strong_count_in requires the pointer be obtained from Arc::into_raw/Arc::into_raw_with_allocator for the same A. Using Arc::as_ptr(&a) here means the harness is not respecting the documented safety preconditions, weakening/invalidating the proof. Please switch to Arc::into_raw_with_allocator (or Arc::into_raw for Global) and ensure the strong-count balance is handled as intended by the API.

Suggested change

	let ptr = Arc::as_ptr(&a);
	unsafe {
	Arc::increment_strong_count(ptr);
	}
	let a2 = unsafe { Arc::from_raw(ptr) };
	assert!(*a2 == 42);
	}
	#[kani::proof]
	fn verify_increment_strong_count_in() {
	let a = Arc::new_in(42i32, Global);
	let ptr = Arc::as_ptr(&a);
	unsafe {
	Arc::increment_strong_count_in(ptr, Global);
	}
	let a2 = unsafe { Arc::from_raw_in(ptr, Global) };
	assert!(*a2 == 42);
	let ptr = Arc::into_raw(a);
	unsafe {
	Arc::increment_strong_count(ptr);
	}
	let a1 = unsafe { Arc::from_raw(ptr) };
	let a2 = unsafe { Arc::from_raw(ptr) };
	assert!(*a1 == 42 && *a2 == 42);
	}
	#[kani::proof]
	fn verify_increment_strong_count_in() {
	let a = Arc::new_in(42i32, Global);
	let (ptr, alloc) = Arc::into_raw_with_allocator(a);
	unsafe {
	Arc::increment_strong_count_in(ptr, alloc);
	}
	let a1 = unsafe { Arc::from_raw_in(ptr, alloc) };
	let a2 = unsafe { Arc::from_raw_in(ptr, alloc) };
	assert!(*a1 == 42 && *a2 == 42);

[Copilot]

Arc::decrement_strong_count’s safety contract requires that ptr was obtained through Arc::into_raw. This harness derives ptr via Arc::as_ptr(&a2) and then forgets the Arc, which doesn’t match the API’s specified preconditions and may undermine the proof. Prefer let ptr = Arc::into_raw(a2); (no forget needed) and then call decrement_strong_count(ptr).

[Copilot]

Arc::decrement_strong_count_in requires ptr to originate from Arc::into_raw_with_allocator for the same allocator passed in. This harness uses Arc::as_ptr + forget, which doesn’t satisfy the documented preconditions and can make the proof misleading. Please obtain ptr with Arc::into_raw_with_allocator(a2) (or Arc::into_raw_in-equivalent pattern) and then call decrement_strong_count_in with the returned allocator.