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, and reachability witnesses after all proof_for_contract calls, so contract preconditions are exercised by explicit kani::cover checks
• 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: 57 / 58 (98.3%)

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

Covered safe functions (57/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 and conversion

• 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
• ArcFromSlice<T: Clone>::from_slice
• TryFrom<Arc<[T],A:Allocator>>::try_from
• ToArcSlice<T, I>::to_arc_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 (1/58)

• Default<str>::default

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: 57/58 safe functions are in the stable passing set (98.3%), 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!

[v3risec]

Update Challenge 27 Arc/Weak verification coverage in several areas.

It adds harnesses for ArcFromSlice<T: Clone>::from_slice, ToArcSlice<T, I>::to_arc_slice, and TryFrom<Arc<[T], A>> for Arc<[T; N], A>. The new harnesses cover representative concrete types, both success and error paths where applicable, and check allocation identity, slice/array lengths, and strong/weak ownership invariants. The ArcFromSlice<T: Clone> path uses a non-trivial Clone wrapper so that the default clone-per-element implementation is exercised, while the iterator-based harnesses use bounded sources and explicit unwind limits to keep the verification tractable.

Reachability witnesses were also added after all proof_for_contract calls, covering the unsafe Arc/Weak operations and their sized, slice, allocator, and trait-object variants.

This change also addresses verify-rust-std#673. The repository is still pinned to a Kani version affected by kani#4537, which is fixed upstream by kani#4542, but Kani cannot be updated as part of this change. Therefore, the expected assertions for the affected ownership-sensitive branches are kept explicitly in the harness comments and temporarily disabled:

• Arc::try_unwrap with another strong owner;
• Arc::make_mut clone-on-write with another strong owner;
• Arc::get_mut with an outstanding weak owner.

These branches are not currently reliable under the pinned Kani model. The assertions should be re-enabled once the repository adopts a Kani version containing the upstream fix.

[feliperodri]

Approving — leading solution for Challenge 27

Thanks @v3risec. After reviewing both open Challenge 27 (Arc/Weak) solutions with our vacuity tooling and local Kani (pinned 0.67.0 / CBMC 6.8.0), this is complete and sound. Prioritizing it.

Coverage against Ch27 criteria:

• A: 12/12 unsafe pub fns. Each has real #[requires]/#[ensures] (not trivially true) with a matching #[kani::proof_for_contract] at the exact fn path — assume_init (both sized+slice), from_raw / from_raw_in, increment_strong_count(_in), decrement_strong_count(_in), get_mut_unchecked, Arc<dyn Any+Send+Sync,A>::downcast_unchecked, Weak::from_raw(_in). Contracts include checked_align_of_raw/checked_size_of_raw, can_dereference, byte-sub round-trip, strong.load(Relaxed) >= 1, is_dangling-sentinel disjuncts, and modifies frames.
• B: 57/58 safe abstractions ≥ 75% (98.3%). Primitive-mono over the full integer/bool/unit/[u8;4] matrix; Global allocator only (challenge-allowed). Only missing: Default<str>::default.

Soundness (all clean):

• T1: no cfg body swaps — bodies of the 12 unsafe fns are unmodified; only outer attributes added.
• T2: no invariant(true), no loop_invariant(true).
• T7: every contracted fn has its matching proof_for_contract at the correct instantiation; .github/workflows/kani.yml unchanged (no autoharness dependency).
• Not assume-the-conclusion — kani::assume uses are limited to layout well-formedness, slice-length CI budget, and caller-side can_dereference(initialized) obligations. None assume the fn's own postcondition.
• Inputs symbolic (kani::any::<T>()); slice length capped at 100 (documented CI budget, "can be removed for local verification").
• kani::unwind(6) only on two Cloned<slice::Iter> harnesses over a fixed [T;4] source — appropriate.
• No runtime std logic changes.

Local Kani sample (CBMC 6.8.0): 2/2 so far VERIFICATION SUCCESSFUL — harness_arc_assume_init_i8 (proof_for_contract), harness_arc_downcast_unchecked_i8 (proof_for_contract). Two more (harness_arc_increment_strong_count_i8, harness_arc_clone_i8) still running; will update if any fail. All static evidence supports approval.

Minor notes for the record (non-blocking):

1. Weak::from_raw/from_raw_in sentinel-is_dangling(ptr)==true branch coverage: harnesses always downgrade a live Arc before into_raw, so the dangling-path leg of the disjunctive precondition isn't exercised even though the contract admits it.
2. downcast_unchecked contract is precondition-only (no ensures) — weak but faithful to the fn's docs.
3. Data-race obligation (challenge line 64) explicitly out of scope: "single-threaded, no concurrent thread interleavings." Challenge 27 sidesteps this by pointing to Challenge 7; noted for the record.

Solid, complete, sound. Bounded + primitive-mono is challenge-allowed.

[feliperodri]

@HuStmpHrrr @rajath-mk @rafaelsamenezes could you review this proposed solution?

[HuStmpHrrr]

subsumed by the condition below?

[v3risec]

Fixed. I refactored the overlapping requirements into the shared arc_raw_valid(ptr) predicate, which captures the raw layout validity, dereferenceable strong-count field, and strong >= 1. The separate redundant pointer requirements are no longer needed.

[HuStmpHrrr]

same refactror as challenge 26?

[v3risec]

Fixed. I updated this to follow the same refactoring pattern as Challenge 26, adapted to Arc's atomic reference counts. The repeated checks are now shared through the arc_raw_* and weak_raw_* helpers.

[v3risec]

@feliperodri @HuStmpHrrr Thanks for the detailed review. I went through the comments and updated the contracts and harnesses accordingly.

• Weak::from_raw / Weak::from_raw_in sentinel coverage: added dedicated contract harnesses using Weak::new / Weak::new_in to exercise the is_dangling(ptr) == true branch. The harnesses check that the sentinel representation is preserved and that inner() remains None.

• downcast_unchecked contract: added an ensures clause requiring the resulting typed Arc pointer to be dereferenceable.

• Data-race scope: this remains explicitly limited to single-threaded Kani verification, with no concurrent interleavings or liveness claims. The Weak::upgrade harnesses were adjusted accordingly to avoid the unbounded weak-CAS retry behavior while preserving the behavior relevant to these single-threaded proofs.

• Harness setup cleanup: several harnesses that previously used Arc::downgrade only to construct a particular Weak state now construct that state directly by reserving the corresponding weak count, or use new_cyclic_in where appropriate. This keeps those harnesses focused on the function under verification instead of depending on Arc::downgrade as part of their setup.

• Raw-pointer contract refactor: the repeated Arc/Weak raw-pointer validity checks were factored into shared helpers, following the same structure as Challenge 26 and removing redundant preconditions.

I reran the updated harnesses locally, and the verification passes.