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 all 12 required unsafe functions and all 54 listed safe functions;
• contracts for unsafe pointer and reference-count operations;
• semantic result assertions for safe functions, followed by kani::cover properties to demonstrate that the checked paths are reachable;
• 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: 54 / 54 (100%)

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

Covered safe functions (54/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
• RcFromSlice<T: Clone>::from_slice
• ToRcSlice<T, I>::to_rc_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
• TryFrom<Rc<[T],A:Allocator>>::try_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

Note

• Verify the default RcFromSlice<T: Clone>::from_slice implementation with a manually implemented non-trivial Clone type, ensuring that the harness does not dispatch to the TrivialClone specialization.
• Verify ToRcSlice<T, I>::to_rc_slice through the FromIterator and exact-size TrustedLen path.
• Both harnesses execute the real Rc::from_iter_exact implementation and its original element-writing loop. The target implementation is not replaced with a cfg(kani)-specific loop.
• These two harnesses use symbolic inputs bounded to at most four elements and unwind the real loop. This is a verification tractability bound: current Kani loop contracts cannot soundly and tractably summarize the iterator's private pointer state, pointer provenance, and yielded values.

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: 54/54 safe functions are covered (100%), 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.
• Check safe functions' results including ownership changes, reference counts, pointer identity, slice length, and initialized payload.
• Place kani::cover properties after the corresponding assertions to show that the verified paths are not vacuous.

3. Helper-based unbounded input generalization

• Introduce shared helper functions for nondeterministic and unbounded 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.

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.

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.

[v3risec]

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

[v3risec]

Strengthen the Challenge 26 Kani safe functions' harnesses for Rc and related Weak, UniqueRc, and UniqueRcUninit paths.

The safe functions' harnesses now:

• add semantic result assertions with matching kani::cover properties;
• check strong and weak reference-count invariants across construction, cloning, conversion, raw-pointer roundtrips, and destruction;
• cover live, expired, and dangling weak-pointer states;
• exercise relevant ownership transitions, including unique, shared, and weak-present states;

[v3risec]

Added standalone verification coverage for the two previously uncovered safe functions:

• RcFromSlice<T: Clone>::from_slice
• ToRcSlice<T, I>::to_rc_slice

The RcFromSlice harness uses a type with a manual, non-trivial Clone implementation, which forces dispatch through the default clone-per-element implementation rather than the TrivialClone specialization.

The ToRcSlice harness exercises the exact-size TrustedLen path through FromIterator. Both harnesses call the real Rc::from_iter_exact implementation and unwind its original element-writing loop.

These two harnesses use nondeterministic inputs bounded to at most four elements with #[kani::unwind(6)]. The bound is needed because current Kani loop contracts cannot soundly and tractably summarize the iterator's private pointer state, pointer provenance, and yielded values.

With these additions, the PR now provides standalone coverage for all 54/54 safe functions listed in Challenge 26.

[feliperodri]

Approving — leading solution for Challenge 26

Thanks @v3risec. After reviewing both open Challenge 26 (Rc/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 Ch26 criteria:

• A: 12/12 unsafe pub fns with real #[requires]/#[ensures]/kani::modifies contracts backed by matching #[kani::proof_for_contract] harnesses, monomorphized across primitive T (i8..i128, u8..u128, bool, unit, [u8;4]) and unsized [T] as challenge-allowed.
• B: ~54/54 safe abstractions with unsafe (~100%, ≥ 75%). Complete coverage across new(_uninit/_zeroed/in), try*, pin/pin_in, into_array, get_mut/make_mut (with 3-state coverage), downcast (Ok+Err), from_box_in, RcFromSlice / ToRcSlice, Drop/Clone/Default, all From/TryFrom variants, Weak::{as_ptr,into_raw_with_allocator,upgrade,inner} (multi-path), inc_strong/inc_weak (+ should_panic overflow), UniqueRc + UniqueRcUninit.

Soundness (all clean):

• T1: no cfg body swaps — grep for cfg(not(kani)) in the diff returns 0 hits; harnesses run the real bodies.
• T2: no trivial invariants, no loop_invariant(true).
• T7: all 12 unsafe fns have explicit proof_for_contract; .github/workflows/kani.yml autoharness allowlist unchanged — no silent autoharness dependency.
• Not assume-the-conclusion — the only kani::assume(can_dereference(...)) is Vec::set_len's own precondition inside a helper, not the fn under proof.
• Inputs symbolic (kani::any::<T>()); slice length bounded ≤100 (documented CI-tractability budget); iterator loops unwind(6) for 4-element input (documented Kani loop-contract limitation).
• No runtime std logic changed.

Local Kani sample (CBMC 6.8.0): 4/4 VERIFICATION SUCCESSFUL — harness_rc_assume_init_i8 (proof_for_contract), harness_rc_downcast_unchecked_i8 (proof_for_contract), harness_inc_strong_overflow_should_panic, harness_rc_default_str.

Minor weaknesses to note for the record (non-blocking):

1. verifier_nondet_vec uses ptr::write_bytes(..., kani::any::<u8>(), size_of::<T>() * sz) — one symbolic byte pattern replicated across all elements, so a run over Rc<[u32]> only covers [0x00000000; n], [0x01010101; n], … Symbolic but coverage-limited for multi-byte T.
2. Rc::from_raw, Rc::increment_strong_count, and Weak::from_raw (non-_in variants) read (*ptr).get() inside unsafe without an explicit kani::mem::can_dereference in the requires, unlike the _in variants which do. Harmless for the roundtrip harnesses (pointers are always valid), but the exported contract is weaker than the _in variant for arbitrary callers — consider adding can_dereference to match.
3. Rc::get_mut_unchecked contract only requires can_write(value); the documented safety property (no other Rc/Weak may reference the inner value) is not encoded — the harness proves UB-freedom of the body but under-specifies the caller obligation.
4. Roundtrip-narrowed inputs (from_raw/increment/decrement use ptr obtained via into_raw) narrow the input universe vs a fully symbolic pointer meeting the precondition.

These are contract-strength refinements, not soundness bugs; they can be addressed in a followup. Challenge 26 explicitly permits bounded + primitive-mono.

[feliperodri]

@lucasccordeiro @rajath-mk @patricklam @HuStmpHrrr could you review this propose solution for challenge 26?

[HuStmpHrrr]

checking now

[v3risec]

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

The main changes are:

• Strengthened the strong-count contracts so increment_strong_count records the pre-state and specifies the +1 transition, while decrement_strong_count specifies the -1 transition.
• Refactored the repeated raw-pointer/layout/refcount checks into shared Kani-only helpers.
• Unified the raw-pointer validity checks used by the non-_in and _in variants, including explicit dereferenceability checks for the reference-count storage.
• Clarified that the dangling case accepted by Weak::from_raw{,_in} is the exact usize::MAX sentinel used by Weak::new[_in], not an arbitrary dangling pointer.
• Made the Weak raw-pointer contracts sentinel-safe and added dedicated proof_for_contract harnesses for the sentinel paths of both Weak::from_raw and Weak::from_raw_in.
• Changed verifier_nondet_vec so each byte is independently symbolic instead of repeating one symbolic byte across the whole buffer.
• Documented the remaining modeling limitation of Rc::get_mut_unchecked: can_write captures writable storage, but the temporal aliasing/active-borrow/exact-inner-type obligation from the API safety documentation is not fully expressible by this contract.
• I kept the raw-pointer contract harnesses based on structurally valid pointers rather than arbitrary pointer bits. Evaluating the raw-layout predicates itself performs provenance-sensitive pointer reconstruction, so starting from an arbitrary address and attempting to filter it afterward would not be a sound replacement.

I also noticed that the Kani CI jobs are currently failing while setting up Kani/CBMC, before reaching the verification itself. The failure comes from Homebrew rejecting the diffblue/cbmc tap as untrusted:

Refusing to load formula diffblue/cbmc/... from untrusted tap diffblue/cbmc.
Error: Cannot tap diffblue/cbmc: invalid syntax in tap!

Is this a known CI/infrastructure issue at the moment, or is there anything I should change on my side?

I'm happy to make any further changes or refinements if needed. Thanks again for the review!

[HuStmpHrrr]

apologies for the delay