Challenge 26: verify Rc/Weak safety in alloc::rc with Kani

[v3risec]

Summary

This PR adds Kani-based verification artifacts for Rc/Weak safety in library/alloc/src/rc.rs for Challenge 26.

The change introduces:

• proof harness modules under #[cfg(kani)] for 12 required unsafe functions and a broad safe-function subset
• contracts/harnesses that check pointer layout/alignment/allocation consistency and key reference-count invariants
• shared helper-based construction for nondeterministic unsized slice inputs, so Rc<[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 26)

Coverage: 12 / 12 (100%)

Verified set includes:

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

Safe functions (Challenge 26 list)

Coverage: 51 / 54 (94.4%)

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

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

Allocation

• Rc<T>::new
• Rc<T>::new_uninit
• Rc<T>::new_zeroed
• Rc<T>::try_new
• Rc<T>::try_new_uninit
• Rc<T>::try_new_zeroed
• Rc<T>::pin
• Rc<T,A:Allocator>::new_uninit_in
• Rc<T,A:Allocator>::new_zeroed_in
• Rc<T,A:Allocator>::new_cyclic_in
• Rc<T,A:Allocator>::try_new_in
• Rc<T,A:Allocator>::try_new_uninit_in
• Rc<T,A:Allocator>::try_new_zeroed_in
• Rc<T,A:Allocator>::pin_in

Slice

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

Conversion and pointer

• Rc<T:?Sized, A:Allocator>::inner
• Rc<T:?Sized, A:Allocator>::into_inner_with_allocator
• Rc<T,A:Allocator>::try_unwrap
• Rc<T:?Sized,A:Allocator>::into_raw_with_allocator
• Rc<T:?Sized,A:Allocator>::as_ptr
• Rc<T:?Sized,A:Allocator>::get_mut
• Rc<T:?Sized+CloneToUninit, A:Allocator+Clone>::make_mut
• Rc<T:?Sized,A:Allocator>::from_box_in
• Rc<dyn Any,A:Allocator>::downcast

Trait implementations (Rc)

• Clone<T: ?Sized, A:Allocator>::clone for Rc
• Drop<T: ?Sized, A:Allocator>::drop for Rc
• Default<T:Default>::default
• Default<str>::default
• From<&str>::from
• From<Vec<T,A:Allocator>>::from
• From<Rc<str>>::from

Weak and traits

• 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

UniqueRc and traits

• UniqueRc<T:?Sized,A:Allocator>::into_rc
• UniqueRc<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 UniqueRc
• UniqueRcUninit<T:?Sized, A:Allocator>::new
• UniqueRcUninit<T:?Sized, A:Allocator>::data_ptr
• Drop<T:?Sized, A:Allocator>::drop for UniqueRcUninit

Refcount internals

• RcInnerPtr::inc_strong
• RcInnerPtr::inc_weak

Not yet listed as standalone harness targets (3/54):

• RcFromSlice<T: Clone>::from_slice
• ToRcSlice<T, I>::to_rc_slice
• TryFrom<Rc<[T],A:Allocator>>::try_from

Three Criteria Met (Challenge 26)

• Required unsafe functions covered: All 12/12 required unsafe functions in Challenge 26 are annotated with contracts and verified.
• Safe-function threshold met: 51/54 safe functions are covered (94.4%), which exceeds the Challenge 26 requirement of at least 75%.
• Challenge scope allowances respected: Generic T is instantiated with allowed representative concrete types, 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. Contract for unsafe functions

• Attach requires preconditions for pointer validity, alignment soundness, same-allocation checks, and refcount well-formedness.
• Attach postconditions where appropriate (ensures) and mutation footprints (kani::modifies) for refcount-changing operations.

2. Harness-backed behavioral checks

• Use #[kani::proof_for_contract(...)] harnesses for all required unsafe functions, and regular #[kani::proof] harnesses for the covered safe functions.

3. Helper-based unsized generalization

• Introduce shared helper functions for nondeterministic vector/slice setup and reuse them across harnesses that target ?Sized slice-based functions.
• Use the helpers to exercise unsized slice cases through Rc<[T]>/Weak<[T]> constructions without duplicating per-harness setup logic.

4. Challenge alignment

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

Scope assumptions (per challenge allowance)

• Harnesses instantiate representative concrete types, including signed/unsigned widths (i8..i128, u8..u128), bool, (), arrays, vectors, slices, str, and trait objects (dyn Any).
• Allocator coverage is limited to Global (both explicit Rc<_, Global> / Weak<_, Global> and default Rc/Weak aliases).

Verification

All harnesses in this PR pass locally with Kani 0.65.

Platform-specific CI tractability note

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.

Resolves #382

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

[feliperodri]

You should use macros to reduce code duplication. It'll also make review easier.

[Copilot]

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

[Copilot]

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

[Copilot]

Pull request overview

Copilot reviewed 1 out of 3 changed files in this pull request and generated 5 comments.

[v3risec]

Thanks for the thoughtful review. We have addressed all 5 comments and pushed 3 follow-up commits with the requested changes. The PR should now be ready for another round of CI and review. Could you please re-run the CI checks when possible?

[v3risec]

Hi, I would like to report what appears to be a CI resource / environment issue rather than a reproducible proof failure.
In my latest commit f6716a99a6b05a4f298cc83f62aff10ab8c3fad3, I observed two CBMC out-of-memory failures in CI:

1. In Kani / Verify std library (partition 1) (pull_request),
   rc::verify_3051::harness_from_vec_i32 failed with:
   CBMC appears to have run out of memory.

2. In Kani / Verify std library using autoharness (macos-latest) (pull_request),
   rc::verify_1650::harness_rc_from_raw_in_vec_u64 failed with:
   CBMC appears to have run out of memory.

What I want to emphasize is that both of these harnesses verify successfully in my local environment, and I do not see any CBMC appears to have run out of memory failure locally.

They also succeeded in the earlier commit e189a7d8a8b06cee7eb6a33c32ea024639702ebe. The harness definitions themselves were unchanged between the two commits, although shared helper code used by them did change (ptr::write_bytes added), so I cannot claim the proof inputs were fully identical across revisions. Still, the local-vs-CI discrepancy suggests that these proofs may be close to the CI resource boundary.

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-based system
• Kernel: Linux 6.11.0-26-generic
• Kani: repo-pinned version from tool_config/kani-version.toml, commit 415ca503aea80fd4c4c4819ad4770b744f1bc3a1
• CBMC: 6.8.0 (cbmc-6.8.0)
• Rust: rustc 1.92.0-nightly (b6f0945e4 2025-10-08)
• Host: x86_64-unknown-linux-gnu
• LLVM: 21.1.2

So these do not appear to be stable. Given that these harnesses pass locally without any CBMC out-of-memory issue, 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 resource issue:

The recent changes add a macOS-only bound to the nondeterministic slice/vector length used by the shared Rc<[T]> / Weak<[T]> helper code. This was added because some of these harnesses were hitting CBMC resource limits in GitHub Actions, while the same harnesses verified successfully in my local Ubuntu environment.

The bound is guarded by #[cfg(target_os = "macos")], so it only applies to the macOS CI configuration. Ubuntu/Linux verification keeps the original unbounded path with respect to this additional platform-specific assumption.

The intent is to keep the macOS CI jobs within their time/memory budget, not to change normal std behavior or the Linux verification setup.

[feliperodri]

Challenge 26 (Rc/Weak) — verification-soundness review

This is genuine, substantial verification work: 112 #[kani::proof] + 20 #[kani::proof_for_contract] (the macros expand these across ~13 primitive/slice instantiations each, yielding the full 132/24 harness counts). Both success criteria are met and the work is sound. I'm landing on COMMENT for a few non-blocking issues a maintainer should weigh before merge.

Soundness checklist — all clear

1. cfg-swap vacuity — BENIGN. The only #[cfg(not(kani))] (library/alloc/src/rc.rs, diff line 434) rewrites the from_slice for (i,item) in iter.enumerate() loop into an equivalent while let Some(item) = iter.next() under #[cfg(kani)], purely to attach #[kani::loop_invariant(i == guard.n_elems)] and loop_modifies. Runtime path keeps the upstream body; the Kani body performs identical ptr::write + n_elems bookkeeping. This is the accepted for→while rewrite pattern, not a fatal body swap. The other cfg(not(...)) are no_global_oom_handling (upstream) and target_os="macos" harness disables (resource limits) — benign.
2. No assume-the-conclusion. proof_for_contract harnesses construct a valid Rc/Weak from kani::any() and derive the raw pointer via into_raw/into_raw_with_allocator, so the precondition holds by construction rather than by assuming the conclusion.
3. No trivial invariants. Only loop_invariant(i == guard.n_elems) — meaningful. No invariant(true), requires(true), or assume(false).
4. Contract-liveness (T7) — real & faithful. All 10 proof_for_contract-verified unsafe fns target contracts newly added in this diff. Contracts encode provenance/refcount preconditions with the correct predicates: from_raw/from_raw_in (diff ~1333, ~1630) require ptr::addr_eq to the rebuilt inner pointer, kani::mem::checked_size_of_raw/checked_align_of_raw match, and strong >= 1; get_mut_unchecked (~1955) requires can_write and ensures result aliases the value; downcast_unchecked (~2204) requires (*self).is::<T>() (exactly the documented precondition); Weak::from_raw{,_in} (~3317/~3534) correctly special-case the is_dangling sentinel plus weak > 0 and same_allocation. These are faithful, not decorative, not over-constrained.
5. Symbolic, not concrete. Values are kani::any(); pointers are symbolic in Kani's model. Slice lengths are symbolic within a bound.
6. Bounded vs unbounded. Slice harnesses bound length (kani::assume(len <= 1024) / sz <= 1024 in verifier_nondet_vec). Acceptable for tractability; challenge permits primitive types only.
7. Success criteria — MET. (a) All 12 required unsafe fns have contracts: 10 verified via proof_for_contract; the two assume_init variants carry contracts (requires can_dereference, ensures strong_count >= 1) verified via #[kani::proof] with an explicit postcondition assertion — justified by both the Kani 0.65 MaybeUninit-impl path-resolution limitation and the challenge's own note that "showing something is initialized … may be impossible to express." (b) Safe-fn coverage spans essentially the entire ~53-entry list (new/new_uninit/new_zeroed/try_* families, pin/pin_in, into_array, get_mut, make_mut, downcast, from_box_in, From impls, Drop/Clone/Default, UniqueRc/UniqueRcUninit, Weak::{as_ptr,upgrade,inner,into_raw_with_allocator}, RcInnerPtr::inc_*), well above 75%. Branch-split harnesses (unique/shared/weak-present; success/failure; live/strong_zero/dangling) show real thought.

This is clearly superior to the competing #574 (zero contracts, concrete-only inputs).

Non-blocking issues to address

• Convention: uses raw kani:: attributes, not the tool-agnostic safety crate. All contracts are #[cfg_attr(kani, kani::requires(...))] / kani::ensures / kani::modifies with use core::kani. Per CLAUDE.md / library/contracts/safety, contracts are supposed to use use safety::{requires, ensures} so they are tool-agnostic and plausibly upstreamable. As written these contracts are Kani-only and diverge from every other merged challenge. Recommend porting to the safety attributes. (Note the Cargo.lock churn adding safety/proc-macro-error to core/alloc deps — reconcile with the branch's existing safety integration.)
• assume_init contracts are present but not proof_for_contract-enforced. The harnesses (verify_1198/verify_1239) run the real body on constructed-valid inputs and manually assert the postcondition, which is sound. But the code comment's claim that "the requires clause is still checked as an assertion at the call site" is imprecise — a contract on a normally-called (non-stubbed, non-target) function is inert in Kani; the requires is satisfied here only because the input is constructed valid, not independently checked. Reword the comment to avoid over-claiming.
• Roundtrip inside a requires clause. The increment_strong_count/increment_strong_count_in preconditions (diff ~1408, ~1760) build Rc::from_raw(ptr) and call into_raw inside the requires to compare addresses. It nets out refcount-neutral and evidently passes CI, but embedding construct/consume logic in a precondition is fragile; consider simplifying to the pure provenance/addr_eq checks used by the other contracts.

Net: sound, faithful, meets both criteria. The above are quality/convention items, not soundness defects.

[v3risec]

@feliperodri Thanks for the detailed review. I’ve addressed the three non-blocking points:

• Migrated all 13 requires and 6 ensures contracts in alloc::rc to the tool-agnostic safety::{requires, ensures} attributes. The four kani::modifies attributes remain Kani-specific frame conditions because the safety crate does not currently provide an equivalent modifies attribute.
• Reworked the comments for both assume_init harness groups. They now state explicitly that a regular #[kani::proof] executes the real function body but does not activate the callee’s requires or ensures contract.
• Explicitly mirrored the expressible assume_init contract conditions in the harnesses:
  • both scalar and slice harnesses assert kani::mem::can_dereference(Rc::as_ptr(&uninit)) before the call;
  • the scalar harness asserts Rc::strong_count(&init) >= 1 afterward;
  • the slice harness retains the stronger strong_count == 1 assertion;
  • the existing value, allocation-address, and slice-length assertions remain in place.
• Clarified that the initialization obligation is established constructively: scalar values are initialized with MaybeUninit::write, while slice backing storage is initialized before assume_init is called.
• Removed the Rc::from_raw/into_raw roundtrips from the affected requires clauses. The contracts now use only the direct pointer/address, dynamic size/alignment, and strong >= 1 checks, while retaining their existing frame conditions.

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