Extend external_derive to cover proc-macro-generated impls

Proc-macro crates such as serde do not emit #[automatically_derived] on
the impls they generate. As a result, #[verifier::external_derive] had no
effect on serde-derived Serialize/Deserialize impls (issues #1575, #1577,
#1956): the gate in get_attributes_for_automatic_derive returned None
immediately for any impl lacking that attribute.

The fix checks span.from_expansion() as a secondary signal. When an impl
is macro-expanded but not #[automatically_derived], and the self type has
#[verifier::external_derive] (with AllExternal or a matching trait name),
the impl is now marked external. If the type has no external_derive
annotation at all, macro-expanded impls fall through to the normal
classification path unchanged, preserving existing behavior.

Tests added in rust_verify_test/tests/std.rs simulate proc-macro derives
with macro_rules! (which produces macro-expanded impls without
#[automatically_derived]) and verify that external_derive AllExternal and
SomeExternal(TraitName) both suppress verification of the generated impl.

Author: hz2

source/rust_verify/src/external.rs

@@ -645,6 +645,11 @@ impl<'a> GeneralItem<'a> {
 /// the *type* has the verus_macro attribute.
 ///
 /// Different traits are handled on a case-by-case basis; see automatic_derive.rs
+///
+/// Proc-macro crates (e.g., serde) do not emit `#[automatically_derived]`, so
+/// their impls would normally be invisible to this function. As a second path,
+/// we also handle macro-expanded impls where the struct has an explicit
+/// `#[verifier::external_derive]` annotation naming the trait.
 fn get_attributes_for_automatic_derive<'tcx>(
     ctxt: &ContextX<'tcx>,
     general_item: &GeneralItem<'tcx>,
@@ -660,7 +665,11 @@ fn get_attributes_for_automatic_derive<'tcx>(
         )));
     };
 
-    if !crate::automatic_derive::is_automatically_derived(attrs) {
+    let is_auto_derived = crate::automatic_derive::is_automatically_derived(attrs);
+    // proc-macro derives do not emit #[automatically_derived]; check span origin instead
+    let is_macro_expanded = !is_auto_derived && span.from_expansion();
+
+    if !is_auto_derived && !is_macro_expanded {
         return None;
     }
 
@@ -676,7 +685,9 @@ fn get_attributes_for_automatic_derive<'tcx>(
                         path.res.def_id()
                     }
                     _ => {
-                        warn_unknown();
+                        if is_auto_derived {
+                            warn_unknown();
+                        }
                         return None;
                     }
                 };
@@ -686,11 +697,25 @@ fn get_attributes_for_automatic_derive<'tcx>(
                     let mut type_eattrs = match ctxt.get_external_attrs(type_attrs) {
                         Ok(eattrs) => eattrs,
                         Err(_) => {
-                            warn_unknown();
+                            if is_auto_derived {
+                                warn_unknown();
+                            }
                             return None;
                         }
                     };
 
+                    // for proc-macro-derived impls, only proceed if the type explicitly
+                    // requests external treatment via external_derive; otherwise fall through
+                    // to None so the impl is handled by the normal classification logic
+                    if is_macro_expanded
+                        && matches!(
+                            &type_eattrs.external_auto_derives,
+                            crate::attributes::AutoDerivesAttr::Regular
+                        )
+                    {
+                        return None;
+                    }
+
                     if match &type_eattrs.external_auto_derives {
                         crate::attributes::AutoDerivesAttr::Regular => false,
                         crate::attributes::AutoDerivesAttr::AllExternal => true,
@@ -718,6 +743,12 @@ fn get_attributes_for_automatic_derive<'tcx>(
                         return Some(type_eattrs);
                     }
 
+                    // for proc-macro impls that have external_derive but the trait name did not
+                    // match any listed name, fall through to normal classification
+                    if is_macro_expanded {
+                        return None;
+                    }
+
                     if opts_in_to_verus(&type_eattrs) {
                         let trait_def_id = impll.of_trait.unwrap().trait_ref.path.res.def_id();
                         let rust_item = get_rust_item(ctxt.tcx, trait_def_id);
@@ -734,17 +765,23 @@ fn get_attributes_for_automatic_derive<'tcx>(
                         None
                     }
                 } else {
-                    warn_unknown();
+                    if is_auto_derived {
+                        warn_unknown();
+                    }
                     None
                 }
             }
             _ => {
-                warn_unknown();
+                if is_auto_derived {
+                    warn_unknown();
+                }
                 None
             }
         },
         _ => {
-            warn_unknown();
+            if is_auto_derived {
+                warn_unknown();
+            }
             None
         }
     }

source/rust_verify_test/tests/std.rs

@@ -603,6 +603,65 @@ test_verify_one_file_with_options! {
     } => Err(err) => assert_vir_error_msg(err, "cannot use function `test_crate::X::clone` which is ignored")
 }
 
+// Proc-macro crates (e.g., serde) do not emit #[automatically_derived], so
+// their impls have span.from_expansion() == true but no automatically_derived attr.
+// We simulate this with a macro_rules! that produces an impl without that attribute.
+test_verify_one_file_with_options! {
+    #[test] external_derive_proc_macro_all ["--no-external-by-default"] => verus_code! {
+        macro_rules! fake_serialize {
+            ($t:ty) => {
+                impl FakeSerialize for $t {
+                    fn serialize(&self) -> u64 { 0 }
+                }
+            }
+        }
+
+        trait FakeSerialize {
+            fn serialize(&self) -> u64;
+        }
+
+        #[verifier::external_derive]
+        struct X {
+            u: u64,
+        }
+
+        fake_serialize!(X);
+
+        fn test(x: X) {
+            // calling serialize on X should work since the impl is marked external
+            let _ = x.serialize();
+        }
+    } => Ok(())
+}
+
+test_verify_one_file_with_options! {
+    #[test] external_derive_proc_macro_named ["--no-external-by-default"] => verus_code! {
+        macro_rules! fake_serialize {
+            ($t:ty) => {
+                impl FakeSerialize for $t {
+                    fn serialize(&self) -> u64 { 0 }
+                }
+            }
+        }
+
+        trait FakeSerialize {
+            fn serialize(&self) -> u64;
+        }
+
+        // only FakeSerialize is listed -- the macro-expanded impl should be ignored
+        #[verifier::external_derive(FakeSerialize)]
+        struct X {
+            u: u64,
+        }
+
+        fake_serialize!(X);
+
+        fn test(x: X) {
+            let _ = x.serialize();
+        }
+    } => Ok(())
+}
+
 test_verify_one_file! {
     #[test] vec_index_nounwind verus_code! {
         use vstd::*;