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.

[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

[feliperodri]

Updated — Criterion 3 below has been tightened after auditing the per-check report rather than relying on Kani's defaults. See the note at the end: the final verdict is pending a committee discussion on the "mutating immutable bytes" criterion.

Criteria 1 and 2 are met. Local Kani (pinned 152c6a8c, nightly-2026-02-05, worktree at PR head 7814a58a) confirms it.

Criterion 1 — all 12 listed pub unsafe fn contracted and verified ✅

Evidence	Result
Contract attributes in library/alloc/src/rc.rs	12 #[requires]-annotated fns at lines 1291, 1436, 1515, 1576, 1622, 1777, 1890, 1945, 2065, 2293, 3399, 3581 — a 1:1 match with the table (checked by reading each signature, not by name)
kani list (local)	Reports exactly those 12 as the contracted functions in alloc::rc, backed by 207 #[kani::proof_for_contract] harnesses
Local verification, one harness per required fn	12/12 SUCCESSFUL, and each reports 1 of 1 cover properties satisfied → not vacuous
Liveness mutation: increment_strong_count's ensures checked_add(1)→(2)	Harness FAILED → the postcondition is genuinely evaluated

Criterion 2 — ≥75% of the 54 safe fns ✅ (well clear of threshold)

Evidence	Result
Per-function grep across the harness block	All 54 are actually called; 1127 plain #[kani::proof] rc harnesses
Local run of 105 harnesses = one per harness family, covering every one of the 12 + 54 functions	105/105 SUCCESSFUL
Effective count after discounting limitations (below)	46/54 = 85%, still ≥ 75%

Two limitations discount 8 functions: RcFromSlice<T: Clone>::from_slice and ToRcSlice::to_rc_slice are bounded to 4 elements via #[kani::unwind(6)] (disclosed in the PR); the six try_new* functions verify only the success path — their Err cover comes back UNREACHABLE because Kani cannot fail an allocation.

Criterion 3 — general rules ✅ / List of UBs ⚠️

General rules ✅

Evidence	Result
Diff vs merge-base 82ab358	rc.rs is +5518 / −0 (pure addition); alloc/src/lib.rs +1 cfg_attr(kani, …) gate; Cargo.lock trailing newline. No std runtime logic touched
Vacuity scan	Zero #[cfg(not(kani))], zero kani::stub → no body-swap or stub vacuity. Only 7 kani::assume calls, all benign (layout validity, sz < 100, can_dereference)
PR CI	All 4 Verify std library partitions, autoharness, goto-transcoder, upstream_test pass. The two red checks (Kani List, Kani Metrics) are exit 143 "runner has received a shutdown signal" — infra, not verification

List of UBs — audited per bullet

My earlier version of this comment asserted "pointer/alignment/overflow/invalid value enabled and passing" as a property of Kani's defaults. That overclaimed on one bullet, so here is the actual per-check tally from the 105-harness run (39,147 SUCCESS / 344 UNREACHABLE / 270 SATISFIED covers / 2 FAILURE — both FAILUREs are the intended intrinsic::abort inside the two #[kani::should_panic] overflow harnesses, so those harnesses pass):

UB bullet	Checks covering it	Verdict
Accessing a dangling or misaligned place	11,423 pointer_dereference; 799 "dereference failure: pointer invalid"; 799 "misaligned pointer to reference cast"	✅ Directly evidenced
UB via compiler intrinsics	332 arithmetic_overflow; "Offset in bytes overflows isize"; "Offset result and original pointer must point to the same allocation"; "`dst` must be properly aligned"; "failed to compute `size_of_val`/`align_of_val`"	✅ Directly evidenced
Producing an invalid value	Only where raw bytes become typed values — the misaligned pointer to reference cast class and can_dereference on nondet input (the PR's verifier_nondet_vec assumes it explicitly). No blanket validity check	⚠️ Partial
Mutating immutable bytes	None — Kani emits no check of this kind	❌ Not checked

Boundary of what these proofs establish: the run also contains 360 unsupported_construct checks — Kani's marker for a construct it cannot model, which fails if reached. All are SUCCESS (i.e. unreachable), but 68 read "Kani does not support reasoning about pointer to unallocated memory".

Verdict pending

Nothing above is a defect in this PR. But "mutating immutable bytes" is not checkable by Kani at all, which means no solution to any challenge in this repo has ever satisfied that bullet — it is an unstated repo-wide assumption rather than something #582 specifically misses.

I would rather resolve that at the policy level than silently accept it here, so I am holding the final verdict until the committee discusses whether to relax, reword, or formally carve out the "mutating immutable bytes" criterion (and, relatedly, how much of "producing an invalid value" we require). @v3risec — this is on us, not on your submission; please carry on with the four review items in the following comment.

[feliperodri]

Thank you, @v3risec, for this outstanding contribution — the rigor here is exactly the standard we want for these proofs. Placing a kani::cover after each assertion so reachability is demonstrated rather than assumed, and deliberately routing RcFromSlice<T: Clone>::from_slice through a non-TrivialClone type so the harness cannot silently fall through to the specialization, are the kind of details that make a solution trustworthy. Congratulations on completing Challenge 26! 🎉

Before we merge, four small items — none of them affect the verification result:

1. Drop the six unsatisfiable try_new* covers. The covers worded "try_new* allocation failure is reachable" (on try_new, try_new_uninit, try_new_zeroed, try_new_in, try_new_uninit_in, try_new_zeroed_in) come back UNREACHABLE, because Kani does not model allocation failure. They read as evidence that the fallible path is exercised when it is not. Please remove them, or replace them with a comment noting the Err branch is out of reach for Kani today.

2. Restore the trailing newline in library/Cargo.lock. The diff currently ends the file with \ No newline at end of file for no reason; it is the only non-additive change in the PR.

3. Please comment on the asymmetry in rc_raw_valid. It omits both the kani::mem::same_allocation(ptr, inner) check and the weak-count check that its sibling weak_raw_layout_valid / weak_raw_count_valid perform. Being more permissive, it is not unsound for these proofs — but the asymmetry looks unintended rather than deliberate. Either add the missing conjuncts or add a comment explaining why Rc::from_raw needs less than Weak::from_raw.

4. Mark the challenge resolved in the book and README, following docs: mark NonZero challenge as resolved #663 as the model:

   • README.md:53 — change the Challenge 26 row's status from Open to [Resolved](https://github.com/model-checking/verify-rust-std/pull/582) and fill the last column with [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/alloc/src/rc.rs).
   • doc/src/challenges/0026-rc.md — set **Status:** Resolved, add **Winning Solution:** [#582](https://github.com/model-checking/verify-rust-std/pull/582), and add a **Contributors** line.

One caveat we are tracking separately rather than asking you to fix: get_mut_unchecked's precondition is only can_write(value), so the documented aliasing requirement is not encoded. You already flag this in a source comment and it is not expressible in Kani today — filed as #693 for visibility.

[v3risec]

@feliperodri Thank you very much for the careful review and for the encouraging feedback on the verification work. I really appreciate both the detailed suggestions and the recognition. I’ve addressed all four merge-preparation items in a667d783:

1. Removed the unreachable allocation-failure kani::cover checks from the try_new* harnesses. The Err arms are retained with comments documenting that Kani does not currently model allocation failure, so those paths are intentionally not covered.

2. Restored the trailing newline in library/Cargo.lock. The unrelated lockfile diff is now gone from the PR.

3. Resolved the rc_raw_valid asymmetry by strengthening the Rc-side validation:

   • rc_raw_layout_valid now checks kani::mem::same_allocation between the payload pointer and the reconstructed RcInner;

   • rc_raw_valid now checks the implicit weak-count invariant through weak_raw_count_valid, with a comment documenting why this invariant holds for live strong references.

4. Marked Challenge 26 as resolved:

   • updated the README entry with the resolved PR and Kani proof link;

   • updated doc/src/challenges/0026-rc.md with the resolved status, winning solution Challenge 26: verify Rc/Weak safety in alloc::rc with Kani #582, and contributor credits for v3risec (Mingzhi Gao and Minghua Wang).

The get_mut_unchecked contract is unchanged, as discussed, since its aliasing limitation is tracked separately in #693.