Challenge 27: Verify Arc/Weak safety in alloc::sync with Kani

[v3risec]

Summary

This PR adds Kani-based verification artifacts for Arc/Weak safety in library/alloc/src/sync.rs for Challenge 27.

The change introduces:

• safety contracts for all required unsafe Arc/Weak functions listed in the challenge
• tool-agnostic #[requires] / #[ensures] contracts provided by the safety crate, while retaining Kani-specific modifies clauses as frame conditions
• proof harness modules under #[cfg(kani)] for those unsafe functions and a broad safe-function subset
• atomic-aware contracts and harnesses that check pointer layout/alignment/allocation consistency and key strong/weak refcount invariants
• shared helper-based construction for nondeterministic unsized slice inputs, so Arc<[T]> / Weak<[T]> paths can be exercised in a reusable way

No non-verification runtime behavior is changed in normal builds.

Verification Coverage Report

Unsafe functions (required by Challenge 27)

Coverage: 12 / 12 (100%)

Verified set includes:

• Arc<mem::MaybeUninit<T>,A>::assume_init
• Arc<[mem::MaybeUninit<T>],A>::assume_init
• Arc<T:?Sized>::from_raw
• Arc<T:?Sized>::increment_strong_count
• Arc<T:?Sized>::decrement_strong_count
• Arc<T:?Sized,A:Allocator>::from_raw_in
• Arc<T:?Sized,A:Allocator>::increment_strong_count_in
• Arc<T:?Sized,A:Allocator>::decrement_strong_count_in
• Arc<T:?Sized,A:Allocator>::get_mut_unchecked
• Arc<dyn Any+Send+Sync,A:Allocator>::downcast_unchecked
• Weak<T:?Sized>::from_raw
• Weak<T:?Sized,A:Allocator>::from_raw_in

Safe functions (Challenge 27 list)

Stable passing coverage: 54 / 58 (93.1%)

This exceeds the challenge threshold (>= 75%).

Covered safe functions (54/58), grouped by API category:

Allocation

• Arc<T>::new
• Arc<T>::new_uninit
• Arc<T>::new_zeroed
• Arc<T>::pin
• Arc<T>::try_pin
• Arc<T>::try_new
• Arc<T>::try_new_uninit
• Arc<T>::try_new_zeroed
• Arc<T,A:Allocator>::new_in
• Arc<T,A:Allocator>::new_uninit_in
• Arc<T,A:Allocator>::new_zeroed_in
• Arc<T,A:Allocator>::new_cyclic_in
• Arc<T,A:Allocator>::pin_in
• Arc<T,A:Allocator>::try_pin_in
• Arc<T,A:Allocator>::try_new_in
• Arc<T,A:Allocator>::try_new_uninit_in
• Arc<T,A:Allocator>::try_new_zeroed_in
• Arc<T,A:Allocator>::try_unwrap
• Arc<T,A:Allocator>::into_inner
• Arc<T:?Sized,A:Allocator>::into_inner_with_allocator

Slice

• Arc<[T]>::new_uninit_slice
• Arc<[T]>::new_zeroed_slice
• Arc<[T]>::into_array
• Arc<[T],A:Allocator>::new_uninit_slice_in
• Arc<[T],A:Allocator>::new_zeroed_slice_in
• ArcFromSlice<T: Copy>::from_slice

Conversion and pointer

• Arc<T:?Sized,A:Allocator>::into_raw_with_allocator
• Arc<T:?Sized,A:Allocator>::as_ptr
• Arc<T:?Sized,A:Allocator>::inner
• Arc<T:?Sized,A:Allocator>::from_box_in
• Clone<T:?Sized, A:Allocator>::clone for Arc
• Arc<T:?Sized+CloneToUninit, A:Allocator+Clone>::make_mut
• Arc<T:?Sized, A:Allocator>::get_mut
• Drop<T:?Sized, A:Allocator>::drop for Arc
• Arc<dyn Any+Send+Sync,A:Allocator>::downcast

Weak and trait-related operations

• Weak<T:?Sized,A:Allocator>::as_ptr
• Weak<T:?Sized,A:Allocator>::into_raw_with_allocator
• Weak<T:?Sized,A:Allocator>::upgrade
• Weak<T:?Sized,A:Allocator>::inner
• Drop<T:?Sized, A:Allocator>::drop for Weak

Default and conversions

• Default<T:Default>::default
• Default<core::ffi::CStr>::default
• Default<[T]>::default
• From<&str>::from
• From<Vec<T,A:Allocator+Clone>>::from
• From<Arc<str>>::from

UniqueArc / UniqueArcUninit and traits

• UniqueArcUninit<T:?Sized, A:Allocator>::new
• UniqueArcUninit<T:?Sized, A:Allocator>::data_ptr
• Drop<T:?Sized, A:Allocator>::drop for UniqueArcUninit
• UniqueArc<T:?Sized,A:Allocator>::into_arc
• UniqueArc<T:?Sized,A:Allocator+Clone>::downgrade
• Deref<T:?Sized,A:Allocator>::deref
• DerefMut<T:?Sized,A:Allocator>::deref_mut
• Drop<T:?Sized, A:Allocator>::drop for UniqueArc

Not yet listed as standalone harness targets (4/58)

• Default<str>::default
• ArcFromSlice<T: Clone>::from_slice
• TryFrom<Arc<[T],A:Allocator>>::try_from
• ToArcSlice<T, I>::to_arc_slice

Current Criteria Met

• Required unsafe functions covered: all 12/12 required unsafe functions in Challenge 27 have contracts and proof harnesses. They are verified directly using #[kani::proof_for_contract].
• Safe-function threshold met: 54/58 safe functions are in the stable passing set (93.1%), exceeding the challenge threshold of at least 75%.
• Challenge scope allowances respected: generic T is instantiated with representative concrete types allowed by the challenge, and allocator-focused proofs are limited to standard-library allocator scope (Global).

Approach

The verification strategy combines contracts for unsafe entry points with executable proof harnesses:

1. Contracts for unsafe functions

• Use the tool-agnostic safety::{requires, ensures} attributes for preconditions and postconditions on all 12 required unsafe functions.
• Specify pointer validity, alignment, same-allocation, initialization, and reference-count requirements as appropriate for each function.
• Retain Kani-specific modifies clauses as frame conditions, since the safety crate currently provides requires and ensures but not a corresponding modifies attribute.

2. Harness-backed behavioral checks

• Add dedicated #[kani::proof] / #[kani::proof_for_contract] modules for required unsafe functions and safe-function coverage targets.
• Cover ownership-state-sensitive APIs by constructing representative states such as unique ownership, shared strong ownership, and externally held weak references.

3. Helper-based unsized generalization

• Introduce shared helper functions for nondeterministic vector/slice construction and reuse them across Arc<[T]> / Weak<[T]> harnesses.
• Use those helpers to exercise ?Sized slice cases without duplicating setup logic across harnesses.

4. Challenge alignment

• Keep all verification code under cfg(kani) so normal std behavior is unchanged.
• Target the Challenge 27 success criteria directly: full required unsafe coverage and safe coverage above the required threshold.

Scope assumptions (per challenge allowance)

• Harnesses instantiate representative concrete types including signed/unsigned widths (i8..i128, u8..u128), bool, (), arrays, vectors, slices, str, CStr, and trait objects (dyn Any, dyn Any + Send + Sync where required by the API).
• Allocator coverage is limited to Global.

Data-race scope

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

Within this scope, the proofs check memory safety for the explored executions, including pointer validity and provenance-related conditions, layout and allocation consistency, and strong/weak reference-count invariants. Atomic loads and updates are exercised as part of those sequential executions, but their behavior under concurrent interleavings, synchronization, and memory-ordering interactions remains outside the scope of these proofs.

Verification

All passing harnesses listed in this report pass locally with the current Kani setup used for this repository.

Resolves #383

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

[Copilot]

Copilot wasn't able to review any files in this pull request.

[v3risec]

I would like to report on the two CI failures from this PR.

For Kani / Verify std library using autoharness (macos-latest) (pull_request), the check reported two failing harnesses:

• sync::verify_2459::harness_arc_make_mut_vec_u32_shared
• slice::ascii::verify::check_is_ascii

Both failures were reported as CBMC timed out.

Of these two, slice::ascii::verify::check_is_ascii was not introduced by this PR; it is a pre-existing harness in the repository.

For sync::verify_2459::harness_arc_make_mut_vec_u32_shared, I was able to verify it successfully in my local environment, and I did not reproduce the CBMC timed out behavior there.

For the other failing check, Kani / Kani List (pull_request), the CI error message appears to indicate an infrastructure issue. From the message, it looks like the CI worker may have run into a disk-space / log-writing problem, which caused the command to terminate.

For reference, my local verification environment is:

• CPU: 2 x Intel(R) Xeon(R) Gold 6230R CPU @ 2.10GHz
• Cores / threads: 52 physical cores / 104 logical CPUs
• Memory: 125 GiB RAM
• OS: Ubuntu 24.04.1 LTS
• Kernel: Linux 6.11.0-26-generic
• Kani: 0.65.0, repo-pinned commit 415ca503aea80fd4c4c4819ad4770b744f1bc3a1
• CBMC: 6.8.0 (cbmc-6.8.0)
• Rust: rustc 1.92.0-nightly (b6f0945 2025-10-08)
• Host: x86_64-unknown-linux-gnu
• LLVM: 21.1.2

Based on the current evidence, my impression is that these failures are more likely related to CI environment instability or resource constraints than to a semantic issue in the harnesses introduced by this PR. Would it make sense to investigate whether the CI runners are hitting memory limits, and if so, whether the memory budget or other CI resource constraints for these Kani jobs should be adjusted?

[v3risec]

Update on the CI timeout:

The previous failure in sync::verify_2459::harness_arc_make_mut_vec_u32_shared
appears to be due to the resource limits of the macOS CI runner rather than a
semantic issue in the harness. I was able to verify the harness locally on my
Ubuntu environment without reproducing the CBMC timed out failure.

To keep the macOS CI job within its time/memory budget, the latest commit adds a
macOS-only bound on the nondeterministic slice/vector length used by the shared
Arc slice helpers:

• on macOS: len / sz is additionally bounded to <= 1024
• on Ubuntu/Linux: the harness remains unchanged and is still not given this
  additional platform-specific bound

This is intended as a CI-resource guard for macOS only. The general capacity and
layout assumptions are still checked as before, and the unbounded Ubuntu path is
preserved to keep the broader verification coverage.

[feliperodri]

Challenge 27 (Arc/Weak) — Kani verification review of PR #587

This is a substantial, genuinely sound effort — vastly stronger than the competing #575 (which was rejected for zero contracts + concrete inputs). #587 uses symbolic inputs throughout (kani::any, verifier_nondet_vec), exercises every behavior-relevant branch explicitly, and adds real pointer-provenance + refcount preconditions. However, two criterion-linked issues block approval.

What's correct (credited)

• No fatal vacuity. No cfg(kani) body-swaps. The only source changes are additive #[cfg_attr(kani, kani::requires/ensures/modifies(...))] attributes plus the #[cfg(kani)] mod verify block. No kani::assume(false), no assume-the-conclusion.
• All 12 required unsafe functions have harnesses. 10 are verified via #[kani::proof_for_contract]: from_raw, increment_strong_count, decrement_strong_count, from_raw_in, increment_strong_count_in, decrement_strong_count_in, get_mut_unchecked, downcast_unchecked, Weak::from_raw, Weak::from_raw_in.
• Contracts are faithful (not decorative or over-constrained). library/alloc/src/sync.rs diff lines 233–245 (from_raw), 277–302 (decrement_strong_count), 310–327 (from_raw_in) encode the documented safety preconditions: ptr reconstructs to &raw const (*inner).data (ptr == rebuilt_ptr), checked_size_of_raw/checked_align_of_raw match, and strong.load(Relaxed) >= 1. The Weak::from_raw/from_raw_in contracts (diff lines 434–530) correctly branch on the is_dangling(ptr) sentinel and preserve the weak count. Preconditions are satisfiable and non-vacuous because harnesses build valid Arcs via into_raw/into_raw_with_allocator round-trips (e.g. diff lines 692–710, 843–861).
• Symbolic, not concrete. Values are kani::any; the decrement_* harnesses clone() first to keep strong >= 1; try_unwrap (diff 1824–1850) covers unique/shared/weak-present states; drop, downcast, Weak::upgrade/inner/drop all cover dangling-vs-live and multi-owner states.
• Safe-function coverage well above the 75% bar. ~56 of the ~58 listed safe functions have harnesses (missing at most TryFrom<Arc<[T]>>::try_from and ToArcSlice::to_arc_slice).
• Bounded appropriately per the challenge: primitive types + Global allocator only, as explicitly permitted; macOS len <= 1024 guards are for CI performance.

Blocking issues

1. Contracts bypass the mandated tool-agnostic safety crate. Every contract is written as #[cfg_attr(kani, kani::requires(...))] (e.g. sync.rs diff lines 191–204, 253–269, 335–363). The repo convention — used by every merged solution — is use safety::{requires, ensures}; then bare #[requires(...)]/#[ensures(...)] (see library/core/src/ptr/non_null.rs:1,175,244). grep finds zero other cfg_attr(kani, kani::requires) on main. The Kani-only form defeats the repo's tool-agnostic contract design, won't be seen by the runtime backend or future tools, and is why the triage counted "0 added contracts." These should be ported to the safety crate attributes before merge.

2. The two required assume_init contracts are not actually verified as contracts. Arc::<MaybeUninit<T>,A>::assume_init (diff 191–205) and Arc::<[MaybeUninit<T>],A>::assume_init (diff 212–226) carry requires/ensures, but their harnesses use #[kani::proof], not #[kani::proof_for_contract] (diff 615–623, 652–672). The code comment "the requires clause is still checked at the call site" (diff 604, 643) is incorrect — a plain kani::proof does not enforce a callee's requires/ensures; the attributes are inert there. The functions' absence of UB is genuinely verified (the real body runs under Kani and the harness asserts strong_count == 1 / data equality), so this is not a soundness hole — but the success criterion "the contracts have been verified" is not literally met for these two, and the misleading comment should be corrected. If the proof_for_contract path-resolution limitation is real for Kani 0.65, note it explicitly and, ideally, add manual assert!s mirroring the contract clauses.

Non-blocking

• Data-race / atomic obligation not addressed. Kani is single-threaded, so the challenge's data-race obligation is out of scope for these proofs. This is acknowledged in the challenge text as a shared difficulty with Challenge 7; fine to scope out, but the PR should state it explicitly rather than leave it implicit.
• Spurious edits to std source: blank lines inserted between #[cfg(...sanitize...)] and the acquire! macro (sync.rs diff lines 175, 183). Harmless (whitespace doesn't break attribute association) but unnecessary noise in the verification target; please drop them.
• Consider adding the two missing safe-fn harnesses (TryFrom<Arc<[T]>>::try_from, ToArcSlice::to_arc_slice) for completeness.

Direction

Convert all contracts to the safety crate attributes (issue 1); either verify the two assume_init contracts via proof_for_contract or, if blocked by tooling, add explicit assertions mirroring the clauses and fix the inaccurate comment (issue 2); revert the stray blank-line edits; and note the data-race scoping. Once the contract mechanism matches repo convention and the assume_init contracts are actually exercised, this is on track for approval.

[v3risec]

@feliperodri Thanks for the detailed review. I’ve addressed the two blocking issues and the related cleanup:

• Migrated the contracts for all 12 required unsafe functions to the tool-agnostic safety attributes by importing safety::{requires, ensures} and replacing all 15 kani::requires and 8 kani::ensures usages with bare #[requires] and #[ensures].
• Kept the four kani::modifies attributes as Kani-specific frame conditions, since the safety crate currently provides requires and ensures but not modifies.
• Updated both assume_init harnesses to use #[kani::proof_for_contract(...)] with explicit generic implementation target paths. This resolves the previous Kani target-resolution issue for the MaybeUninit-based Arc implementations.
• Strengthened the two assume_init contracts so that their preconditions check the storage as the initialized type (T or [T]). Their postconditions check that the returned Arc preserves the original data pointer and produces a dereferenceable initialized result.
• Removed the redundant manual can_dereference and strong_count assertions from the assume_init harnesses. The scalar harness retains a concrete value-preservation check; the contract itself now checks the generic safety properties.
• Removed the two stray blank lines before the acquire! macro.

The shared nondeterministic vector helper now bounds the symbolic length to <= 100 for CI resource stability. This is only a verification-time tractability bound for shared CI runners; it is not a safety condition or a function-behavior assumption. The bound can be removed for local verification to restore the intended unbounded input space.

The data-race obligation remains explicitly out of scope for these single-threaded Kani proofs.

Please let me know if there are any other changes you would like me to make.

[v3risec]

@feliperodri All CI checks are green now, and I’ve addressed the blocking and non-blocking issues. This should be ready for another look. Thanks!