Challenge 26: Verify the safety of Rc and Weak in alloc::rc

[kasimte]

Towards #382. Solves Challenge 26: Verify reference-counted Cell implementation: safety contracts on all 12 required pub unsafe functions and Kani harnesses covering all 54 listed safe functions in alloc::rc. The suite lives in one mod verify: 101 harness macros expand to 1,293 harness functions, 205 of them proof_for_contract, plus 3 standalone harnesses. Every harness carries a kani::cover non-vacuity witness. Element types are primitives, slices, and small arrays (the challenge permits limiting generic T to primitives). Allocator coverage is Global, explicit and default. System lives in std and is not nameable from alloc's harnesses. All 1,293 harnesses pass via scripts/run-kani.sh.

Coverage: required unsafe functions (12/12)

Function	Verified via
Rc<MaybeUninit<T>, A>::assume_init	proof_for_contract (rc_check_assume_init, 13 types)
Rc<[MaybeUninit<T>], A>::assume_init	proof_for_contract (rc_check_assume_init_slice, 12 types)
Rc<T>::from_raw	proof_for_contract (rc_check_from_raw_{sized,unsized}, 18 instantiations)
Rc<T>::increment_strong_count	proof_for_contract (sized + unsized, 18)
Rc<T>::decrement_strong_count	proof_for_contract (sized + unsized, 18)
Rc<T, A>::from_raw_in	proof_for_contract (sized + unsized, 18)
Rc<T, A>::increment_strong_count_in	proof_for_contract (sized + unsized, 18)
Rc<T, A>::decrement_strong_count_in	proof_for_contract (sized + unsized, 18)
Rc<T, A>::get_mut_unchecked	proof_for_contract (sized + unsized, 18)
Rc<dyn Any, A>::downcast_unchecked	proof_for_contract (13 types + 5 Vec payloads)
Weak<T>::from_raw	proof_for_contract (sized + unsized, 18)
Weak<T, A>::from_raw_in	proof_for_contract (sized + unsized, 18)

Coverage: safe functions (54/54)

All 54 functions from the challenge's table, grouped by API area; each entry names its harness family.

• Constructors: new, new_uninit, new_zeroed, try_new, try_new_uninit, try_new_zeroed, new_uninit_in, new_zeroed_in, new_cyclic_in, try_new_in, try_new_uninit_in, try_new_zeroed_in, pin, pin_in (one rc_check_* family each; pin/pin_in include a !Unpin sentinel type).
• Slice constructors: new_uninit_slice, new_zeroed_slice, new_uninit_slice_in, new_zeroed_slice_in, into_array (one family each, symbolic lengths under layout-validity assumptions).
• Accessors and conversions: inner, into_inner_with_allocator, into_raw_with_allocator, as_ptr, get_mut (three-state), make_mut (three-state), downcast (success + failure), from_box_in, try_unwrap (three-state).
• From/FromIterator/TryFrom: From<&str>, From<Vec<T>>, From<Rc<str>>, ToRcSlice::to_rc_slice (both specializations), TryFrom<Rc<[T]>> for Rc<[T; N]> (both arms, one cover per arm).
• RcFromSlice: the T: Copy-era specialization (today's TrivialClone impl; rc_check_from_slice_copy, 13 types) and the T: Clone default (rc_check_from_slice_clone, via a manual-Clone wrapper — every primitive is TrivialClone, so no primitive can reach the default path).
• Ownership and drop glue: Drop for Rc (three-state), Clone for Rc, Default (13 types + Vec payloads), Default for Rc<str>.
• Weak: as_ptr (live + dangling), into_raw_with_allocator (live + dangling), upgrade (three-path), inner (both branches), Drop for Weak (three-path).
• RcInnerPtr: inc_strong, inc_weak (non-overflow harnesses + the two should_panic overflow harnesses).
• UniqueRc/UniqueRcUninit: into_rc, downgrade, Deref, DerefMut, Drop for UniqueRc (both branches), UniqueRcUninit::new, data_ptr, Drop for UniqueRcUninit.

Contracts

• Contracts use safety::{requires, ensures}. The four modifies clauses use cfg_attr(kani, kani::modifies(...)) — the safety crate exposes no modifies wrapper.
• All pointer-validity preconditions are pure provenance checks: rebuild the inner pointer from the data pointer, compare with ptr::addr_eq, check size and alignment via kani::mem::checked_size_of_raw/checked_align_of_raw, and require strong >= 1. No contract constructs or consumes an Rc internally.
• assume_init harness comments state exactly what is constrained (the harness-generated bytes, before set_len) and why the postcondition assertion is not circular.

Proof soundness

• One kani::cover witness per harness body (141 source lines), placed after the last assumption and before the operation under verification (in should_panic harnesses, before the panicking operation); every harness reports N of N cover properties satisfied.
• Branch-state harnesses assert the constructed state's documented outcome (Some/None, Ok/Err, strong/weak count relations, pointer identity, post-drop upgrade() behavior, make_mut's clone-on-write and weak-disassociation effects); constructor harnesses assert value preservation.
• The nondeterministic-input helpers carry their own covers, so every kani::assume in the suite has a reachability witness downstream of it; TryFrom additionally covers both match arms.
• Branch-state families (unique/shared/weak_present, success/failure, live/strong_zero/dangling) construct each behavior-relevant state explicitly.
• should_panic pairing: both reachable abort guards in the file (inc_strong/inc_weak refcount overflow) have #[kani::should_panic] harnesses. A sweep of the remaining assert!/panic!/unwrap sites found no other guard reachable under the documented preconditions: the Layout::array().unwrap() sites are unreachable under the harnesses' layout-validity assumptions, and the TrustedLen capacity overflow panic requires an iterator longer than usize::MAX.

Loop verification

from_iter_exact's element-writing loop is verified against the unmodified upstream for-loop by bounded unrolling (#[kani::unwind(5)], length-3 inputs, justified in-code). Unrolling is deliberate: a loop-contract formulation cannot carry the harnesses' element-value postconditions, because under invariant havoc no invariant relates an opaque impl Iterator's yielded prefix to the memory the harness asserts on. The file contains no cfg(kani) code substitutions: the code Kani verifies is the code that runs.

Bounds

The shared nondeterministic-vector helper bounds the symbolic length (sz <= 100). This is a CI tractability measure, not a safety precondition; sampled harnesses re-verified locally with the bound removed: clone_rc_vec_u8 22.4s, from_raw_vec_u8 40.5s, get_mut_vec_u8_shared_none 35.2s (all successful, covers satisfied). The assume_init_slice harnesses carry the same len <= 100 bound for CI-runner memory on wide element types: the unbounded form verifies on the Linux CI runners, but the widest variants exceed macOS runner memory. In-code comments carry the same statements. Fixed harness lengths (len 3, N = 100 in into_array) carry in-code justifications.

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

[feliperodri]

Thanks @kasimte, and apologies — this was also missed in the Challenge 26 round (created after our triage snapshot). Reviewed now.

This is excellent and essentially equal on verification merit to the solution we approved: 12/12 unsafe fns with genuine safety::{requires,ensures} + matching #[kani::proof_for_contract] (21 macro sites, sized + unsized/slice; real provenance/validity preconditions and checkable postconditions, satisfied by construction not assume) and ~54/54 safe abstractions (≥75%). Clean on T1/T2/T7, symbolic inputs, kani::cover non-vacuity witnesses, should_panic refcount-overflow twins.

Requesting changes for two reasons:

1. One runtime-code edit. Weak::drop is reformatted from upstream's one-liner (let inner = if let Some(inner) = self.inner() { inner } else { return };) to a 5-line block. Semantically identical, but per CLAUDE.md this repo must not change std runtime logic / must stay in upstream sync, and it will diverge from upstream rustfmt (risk of check_rustc.sh format mismatch). Please revert that line.
2. Prioritization: we reviewed both open Ch26 solutions and approved #582 (v3risec) — same 12/12 real proof_for_contract + ~54/54 coverage, but with no runtime-source edit and a leaner harness count (yours expands to ~1,293 harnesses = higher CI cost). We're keeping this as the strong alternative.

Minor: 5 loop-bearing safe fns use #[kani::unwind(5)] (bounded, len-3 inputs) — fine and challenge-permitted, but a weaker guarantee than an inductive proof. Superb work; revert the Weak::drop reflow and it's a clean equal to #582.