From 4ab656f7a1354d901293202003678343c50026c7 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 5 Nov 2024 09:17:02 -0600
Subject: [PATCH] tests: add a test that get_impl_paths and recursive-checking
 handles weird Send/Sync impls correctly

---
 source/rust_verify_test/tests/traits.rs | 96 +++++++++++++++++++++++++
 1 file changed, 96 insertions(+)

diff --git a/source/rust_verify_test/tests/traits.rs b/source/rust_verify_test/tests/traits.rs
index 2c44a0595..fc8625401 100644
--- a/source/rust_verify_test/tests/traits.rs
+++ b/source/rust_verify_test/tests/traits.rs
@@ -4225,3 +4225,99 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_vir_error_msg(err, "found a cyclic self-reference in a definition")
 }
+
+test_verify_one_file! {
+    #[test] test_recursion_through_sync_impl_is_checked verus_code! {
+        trait Tr {
+            proof fn tr_g() {
+            }
+        }
+
+        struct X<T, S> {
+            rc: std::rc::Rc<u64>,
+            t: T,
+            s: S,
+        }
+
+        #[verifier::external]
+        unsafe impl<T: Sync + Tr, S: Sync> Sync for X<T, S> {
+        }
+
+
+        trait Sr {
+            proof fn f() { }
+        }
+
+        struct Y<R> {
+            r: R,
+        }
+
+        impl<W: Sync> Sr for Y<W> {
+            proof fn f() { }
+        }
+
+
+        struct A1 { }
+
+        struct B1 { }
+
+        impl Tr for A1 {
+            proof fn tr_g() {
+                test();
+            }
+        }
+
+
+        proof fn test() {
+            let r = Y::<X<A1, B1>>::f();
+        }
+    } => Err(err) => assert_vir_error_msg(err, "found a cyclic self-reference in a definition")
+}
+
+test_verify_one_file! {
+    #[test] test_recursion_through_send_impl_is_checked verus_code! {
+        trait Tr {
+            proof fn tr_g() {
+            }
+        }
+
+        struct X<T, S> {
+            rc: std::rc::Rc<u64>,
+            t: T,
+            s: S,
+        }
+
+        #[verifier::external]
+        unsafe impl<T: Send + Tr, S: Send> Send for X<T, S> {
+        }
+
+
+        trait Sr {
+            proof fn f() { }
+        }
+
+        struct Y<R> {
+            r: R,
+        }
+
+        impl<W: Send> Sr for Y<W> {
+            proof fn f() { }
+        }
+
+
+        struct A1 { }
+
+        struct B1 { }
+
+        impl Tr for A1 {
+            proof fn tr_g() {
+                test();
+            }
+        }
+
+
+        proof fn test() {
+            let r = Y::<X<A1, B1>>::f();
+        }
+    } => Err(err) => assert_vir_error_msg(err, "found a cyclic self-reference in a definition")
+}