Generate nondeterministic reference-count state for Rc/Arc Arbitrary

[rbeauchamp]

Description

kani::any::<Rc<T>>() / kani::any::<Arc<T>>() (and the AnyRc/AnyArc autoharness models) always produced a fresh allocation: strong_count == 1 and weak_count == 0 on every generated value. A function observing reference-count state could be verified for states a real caller can violate — e.g. assert_eq!(Arc::strong_count(&a), 1) passed even though let _y = a.clone(); f(a) trips it at runtime. This is an input-space under-approximation (false-negative hazard) affecting strong_count, weak_count, get_mut, try_unwrap, make_mut, etc.

Design

Every documented count-dependent behavior of Rc/Arc branches only on uniqueness: strong_count == 1, and for get_mut/try_unwrap additionally weak_count == 0. The behavioral equivalence classes of real reference-count states are therefore exactly four — strong ∈ {1, ≥2} × weak ∈ {0, ≥1} — and the generator now covers all four with one representative each (strong_count ∈ {1, 2}, weak_count ∈ {0, 1}) by nondeterministically leaking a clone() and/or a downgrade(). A leaked reference is observationally identical to one held by a caller for the duration of the function under verification. Generation stays loop-free, so it needs no unwinding bound, and the pointee remains fully nondeterministic.

Note: this intentionally makes previously-"verified" uniqueness assertions fail — that is the soundness fix taking effect, not a regression.

Context

Surfaced in #4752 (during review of #4698). The issue offered two directions — model nondeterministic refcount state, or document the limitation; this PR implements the former, and the equivalence-class argument means the {1, 2} × {0, 1} representatives are behaviorally complete for the documented API surface rather than a lossy bound.

Manual testing

• New tests/kani/RefCount/nondet_rc_arc.rs (12 harnesses): count validity (strong_count >= 1), reachability of shared/weak states (#[kani::should_panic] on the old always-unique assertions — each now fails on exactly the count assertion), both get_mut outcomes, get_mut succeeds under assume(unique && no weak), and extreme pointee values (kani::cover!(*rc == 255) SATISFIED) under sharing.
• Extended tests/script-based-pre/cargo_autoharness_smart_pointers/ with arc_count, which fails through the AnyArc model path on assertion failed: Arc::strong_count(&a) == 1 (verifying the models carry the same semantics); .expected updated.
• Regression sweep of existing Rc/Arc-touching suites (FunctionContracts/receiver_contracts, SizeAndAlignOfDst, UnsizedCoercion, AsyncAwait, Drop): 28/28 pass.

Resolves #4752

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