Arbitrary/autoharness: nondeterministic Rc<T>/Arc<T> values always have strong_count == 1 #4752

Summary

Kani's Arbitrary implementations for Rc<T> and Arc<T> (added in #4697) construct a fresh allocation:

impl<T: Arbitrary> Arbitrary for std::sync::Arc<T> {
    fn any() -> Self { std::sync::Arc::new(T::any()) }
}

so every nondeterministic Rc/Arc value observably has strong_count == 1 and weak_count == 0. This is also what the autoharness smart-pointer models (any_rc/any_arc, #4698) produce, since they call kani::any::<T>() inside a fresh Rc::new/Arc::new.

Why this matters

A function that observes reference-count state can be "proved" for a state a real caller can violate. For example:

fn f(a: std::sync::Arc<u32>) {
    assert_eq!(std::sync::Arc::strong_count(&a), 1); // "verified", but a caller may pass a clone
}

An autoharness (or a manual harness using kani::any::<Arc<u32>>()) only ever sees strong_count == 1, so this passes — even though let x = Arc::new(0); let _y = x.clone(); f(x); would trip the assertion at runtime. The same applies to Arc::weak_count, Arc::get_mut, Arc::try_unwrap, Rc::make_mut, etc.

Scope / notes

• This is a property of the Arbitrary impls themselves, not specific to autoharness: it affects any harness that uses kani::any::<Arc<T>>()/kani::any::<Rc<T>>().
• It pre-dates the autoharness smart-pointer support (Autoharness: support smart pointers of compiler-derivable pointees #4698); that PR extends the existing Arbitrary semantics to compiler-derivable pointees but does not change refcount behavior.
• Box<T> is unaffected: it is uniquely owned and has no observable aliasing/refcount state, so Box<T> genuinely covers exactly the values of T.

Possible directions

1. Model a nondeterministic reference-count state (e.g. leak additional clones/weak refs so strong_count/weak_count are nondeterministic), and report such values as bounded where a finite bound is used.
2. Document the limitation explicitly for Rc/Arc Arbitrary.

Surfaced during review of #4698 (Copilot).