From 8525b7be92414929649db156008c8047d33dda92 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 29 Jul 2026 10:20:43 +0000
Subject: [PATCH] Implement Arbitrary for Rc<T> and Arc<T>

Box<T> has an Arbitrary implementation, but Rc<T> and Arc<T> did not, so
functions taking reference-counted arguments could not be verified against
nondeterministic inputs (and were skipped by 'kani autoharness' with
'Missing Arbitrary implementation'). Add the analogous implementations.

Unlike slice or container arguments, these need no bound: a smart pointer
to T covers exactly the values of T, so the generated values retain Kani's
usual full-coverage guarantee.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 library/kani/src/arbitrary.rs  | 18 ++++++++++++++++++
 tests/kani/Arbitrary/rc_arc.rs | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+)
 create mode 100644 tests/kani/Arbitrary/rc_arc.rs

diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs
index f16f06165d29..0b3fb5084091 100644
--- a/library/kani/src/arbitrary.rs
+++ b/library/kani/src/arbitrary.rs
@@ -15,6 +15,24 @@ where
     }
 }
 
+impl<T> Arbitrary for std::rc::Rc<T>
+where
+    T: Arbitrary,
+{
+    fn any() -> Self {
+        std::rc::Rc::new(T::any())
+    }
+}
+
+impl<T> Arbitrary for std::sync::Arc<T>
+where
+    T: Arbitrary,
+{
+    fn any() -> Self {
+        std::sync::Arc::new(T::any())
+    }
+}
+
 impl Arbitrary for std::time::Duration {
     fn any() -> Self {
         const NANOS_PER_SEC: u32 = 1_000_000_000;
diff --git a/tests/kani/Arbitrary/rc_arc.rs b/tests/kani/Arbitrary/rc_arc.rs
new file mode 100644
index 000000000000..8dee0066ee52
--- /dev/null
+++ b/tests/kani/Arbitrary/rc_arc.rs
@@ -0,0 +1,33 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that Rc<T> and Arc<T> implement Arbitrary (like Box<T>), producing an
+// unconstrained value of the pointee type behind shared-ownership indirection.
+
+use std::rc::Rc;
+use std::sync::Arc;
+
+#[derive(kani::Arbitrary)]
+struct Point {
+    x: u8,
+    y: u8,
+}
+
+#[kani::proof]
+fn check_rc() {
+    let p: Rc<Point> = kani::any();
+    kani::cover!(p.x == 255 && p.y == 0, "extreme values are generated");
+}
+
+#[kani::proof]
+fn check_arc() {
+    let v: Arc<i32> = kani::any();
+    kani::cover!(*v == i32::MIN, "extreme values are generated");
+    kani::cover!(*v == 42, "specific values are generated");
+}
+
+#[kani::proof]
+fn check_nested() {
+    let v: Rc<Arc<u8>> = kani::any();
+    kani::cover!(**v == 7, "nested smart pointers are generated");
+}