Change thrust-macros expansion for extern_spec_fn functions

When the annotated function already has #[thrust::extern_spec_fn],
inject requires_path/ensures_path into the original function body
instead of generating a separate _thrust_extern_spec_ wrapper.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: coord-e

thrust-macros/src/lib.rs

@@ -58,7 +58,19 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
             .map_or(true, |s| s.ident != "requires")
     });
 
-    transform(func, req_expr, ens_expr).unwrap_or_else(|e| e.to_compile_error().into())
+    let is_extern_spec = func.attrs.iter().any(|a| {
+        a.path()
+            .segments
+            .last()
+            .map_or(false, |s| s.ident == "extern_spec_fn")
+    });
+
+    if is_extern_spec {
+        transform_extern_spec(func, req_expr, ens_expr)
+            .unwrap_or_else(|e| e.to_compile_error().into())
+    } else {
+        transform(func, req_expr, ens_expr).unwrap_or_else(|e| e.to_compile_error().into())
+    }
 }
 
 /// Pass-through no-op. When `#[ensures]` is consumed by `#[requires]`, this is never
@@ -69,6 +81,61 @@ pub fn ensures(_attr: TokenStream, item: TokenStream) -> TokenStream {
     item
 }
 
+fn transform_extern_spec(
+    mut func: ItemFn,
+    req_expr: TokenStream2,
+    ens_expr: TokenStream2,
+) -> syn::Result<TokenStream> {
+    let name = &func.sig.ident;
+    let requires_name = format_ident!("_thrust_requires_{}", name);
+    let ensures_name = format_ident!("_thrust_ensures_{}", name);
+
+    let generics = &func.sig.generics;
+
+    let def_generics = generic_params_tokens(generics);
+    let turbofish = generic_turbofish(generics);
+    let model_preds = model_where_predicates(generics);
+    let extended_where = extended_where_clause(generics, &model_preds);
+
+    // Parameters with types replaced by <T as thrust_models::Model>::Ty
+    let model_ty_params = fn_params_with_model_ty(&func.sig.inputs);
+
+    // Return type for ensures helper (wrapped in ::Ty)
+    let ret_model_ty: Type = match &func.sig.output {
+        ReturnType::Default => syn::parse_quote!(<() as thrust_models::Model>::Ty),
+        ReturnType::Type(_, ty) => syn::parse_quote!(<#ty as thrust_models::Model>::Ty),
+    };
+
+    // Prepend requires_path/ensures_path statements to the original block
+    let orig_stmts = func.block.stmts.clone();
+    func.block = syn::parse_quote!({
+        #[thrust::requires_path]
+        #requires_name #turbofish;
+        #[thrust::ensures_path]
+        #ensures_name #turbofish;
+        #(#orig_stmts)*
+    });
+
+    let output = quote! {
+        #[allow(unused_variables)]
+        #[thrust::formula_fn]
+        fn #requires_name #def_generics(#model_ty_params) -> bool #extended_where {
+            #req_expr
+        }
+
+        #[allow(unused_variables)]
+        #[thrust::formula_fn]
+        fn #ensures_name #def_generics(result: #ret_model_ty, #model_ty_params) -> bool #extended_where {
+            #ens_expr
+        }
+
+        #[allow(path_statements)]
+        #func
+    };
+
+    Ok(output.into())
+}
+
 fn transform(
     func: ItemFn,
     req_expr: TokenStream2,