From 6697bfccd3ff722cda5ec2f45ecf452009adba93 Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 10:18:36 +0900
Subject: [PATCH 01/15] add test

---
 crates/anodized/tests/trait_fn_patterns.rs | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 crates/anodized/tests/trait_fn_patterns.rs

diff --git a/crates/anodized/tests/trait_fn_patterns.rs b/crates/anodized/tests/trait_fn_patterns.rs
new file mode 100644
index 0000000..498012e
--- /dev/null
+++ b/crates/anodized/tests/trait_fn_patterns.rs
@@ -0,0 +1,22 @@
+use anodized::spec;
+
+#[spec]
+trait PatternArguments {
+    #[spec(requires: left <= right)]
+    fn func((left, right): (i32, i32)) {
+        let _ = (left, right);
+    }
+}
+
+struct Bounds {
+    lower: i32,
+    upper: i32,
+}
+
+#[spec]
+trait PatternArguments {
+    #[spec(requires: lower <= upper)]
+    fn func(Bounds { lower, upper }: Bounds) {
+        let _ = (lower, upper);
+    }
+}

From 3cfed138a72ac3a2999452ef99b8cf0d5e9074e2 Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 13:56:46 +0900
Subject: [PATCH 02/15] WIP

---
 crates/anodized-core/src/instrument/traits.rs | 144 +++++++++++++++---
 crates/anodized/tests/trait_fn_patterns.rs    |   6 +-
 2 files changed, 126 insertions(+), 24 deletions(-)

diff --git a/crates/anodized-core/src/instrument/traits.rs b/crates/anodized-core/src/instrument/traits.rs
index e064039..40006a0 100644
--- a/crates/anodized-core/src/instrument/traits.rs
+++ b/crates/anodized-core/src/instrument/traits.rs
@@ -2,10 +2,11 @@
 #[path = "traits_tests.rs"]
 mod traits_tests;
 
-use quote::quote;
+use quote::{ToTokens, quote};
 use syn::{
-    Attribute, Block, FnArg, ImplItem, ImplItemFn, Pat, ReturnType, TraitItem, TraitItemFn,
-    Visibility, parse_quote,
+    Attribute, Block, Expr, ExprCall, ExprStruct, ExprTuple, FnArg, ImplItem, ImplItemFn, Pat,
+    PatConst, PatIdent, PatLit, PatMacro, PatParen, PatPath, PatRange, PatStruct, PatTuple,
+    PatTupleStruct, ReturnType, TraitItem, TraitItemFn, Visibility, parse_quote,
 };
 
 use crate::{
@@ -366,29 +367,130 @@ Instead, ensure that both the trait and the impl fn have a `#[spec]` annotation.
 fn build_call_args(
     inputs: &syn::punctuated::Punctuated<FnArg, syn::Token![,]>,
 ) -> syn::Result<Vec<proc_macro2::TokenStream>> {
-    let mut args = Vec::new();
-    for input in inputs.iter() {
-        match input {
-            FnArg::Receiver(_) => {
-                args.push(quote! { self });
+    let mut args = vec![];
+    for input in inputs {
+        let tokens = match input {
+            FnArg::Receiver(receiver) => receiver.self_token.to_token_stream(),
+            FnArg::Typed(pat_type) => {
+                let expr = sanitize_pat_for_expr(&pat_type.pat)?;
+                expr.to_token_stream()
             }
-            FnArg::Typed(pat) => match pat.pat.as_ref() {
-                Pat::Ident(pat_ident) => {
-                    let ident = &pat_ident.ident;
-                    args.push(quote! { #ident });
-                }
-                _ => {
-                    return Err(syn::Error::new_spanned(
-                        &pat.pat,
-                        "unsupported pattern in trait method arguments",
-                    ));
-                }
-            },
-        }
+        };
+        args.push(tokens);
     }
     Ok(args)
 }
 
+/// Sanitize the pattern so that it may be used as an expression to reconstruct what it matched.
+fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
+    match pat {
+        Pat::Const(pat_const) => Ok(Pat::Const(PatConst {
+            attrs: vec![],
+            const_token: pat_const.const_token,
+            block: pat_const.block.clone(),
+        })),
+        Pat::Ident(pat_ident) if pat_ident.by_ref.is_none() => {
+            let None = pat_ident.by_ref else {
+                return Err(syn::Error::new_spanned(
+                    &pat_ident.by_ref,
+                    "not allowed here due to `#[spec]`",
+                ));
+            };
+            Ok(Pat::Ident(PatIdent {
+                attrs: vec![],
+                by_ref: None,
+                mutability: None,
+                ident: pat_ident.ident.clone(),
+                subpat: None,
+            }))
+        }
+        Pat::Lit(pat_lit) => Ok(Pat::Lit(PatLit {
+            attrs: vec![],
+            lit: pat_lit.lit.clone(),
+        })),
+        Pat::Path(pat_path) => Ok(Pat::Path(PatPath {
+            attrs: vec![],
+            qself: pat_path.qself.clone(),
+            path: pat_path.path.clone(),
+        })),
+        Pat::Range(pat_range) => Ok(Pat::Range(PatRange {
+            attrs: vec![],
+            start: pat_range.start.clone(),
+            limits: pat_range.limits,
+            end: pat_range.end.clone(),
+        })),
+        Pat::Paren(pat_paren) => Ok(Pat::Paren(PatParen {
+            attrs: vec![],
+            paren_token: pat_paren.paren_token,
+            pat: sanitize_pat_for_expr(&pat_paren.pat)?.into(),
+        })),
+        Pat::Reference(pat_reference) => sanitize_pat_for_expr(&pat_reference.pat),
+        Pat::Type(pat_type) => sanitize_pat_for_expr(&pat_type.pat),
+        Pat::Struct(pat_struct) => {
+            let None = pat_struct.rest else {
+                return Err(syn::Error::new_spanned(
+                    &pat_struct.rest,
+                    "not allowed here due to `#[spec]`",
+                ));
+            };
+            let mut fields = syn::punctuated::Punctuated::<syn::FieldPat, syn::token::Comma>::new();
+            for field_pat in &pat_struct.fields {
+                let field_value = syn::FieldPat {
+                    attrs: vec![],
+                    member: field_pat.member.clone(),
+                    colon_token: field_pat.colon_token,
+                    pat: sanitize_pat_for_expr(&field_pat.pat)?.into(),
+                };
+                fields.push(field_value);
+            }
+            Ok(Pat::Struct(PatStruct {
+                attrs: vec![],
+                qself: pat_struct.qself.clone(),
+                path: pat_struct.path.clone(),
+                brace_token: pat_struct.brace_token,
+                fields,
+                rest: None,
+            }))
+        }
+        Pat::Tuple(pat_tuple) => {
+            let mut elems = syn::punctuated::Punctuated::<syn::Pat, syn::token::Comma>::new();
+            for elem_pat in &pat_tuple.elems {
+                let elem_value = sanitize_pat_for_expr(&elem_pat)?;
+                elems.push(elem_value);
+            }
+            Ok(Pat::Tuple(PatTuple {
+                attrs: vec![],
+                paren_token: pat_tuple.paren_token,
+                elems,
+            }))
+        }
+        Pat::TupleStruct(pat_tuple_struct) => {
+            let mut elems = syn::punctuated::Punctuated::<syn::Pat, syn::token::Comma>::new();
+            for elem_pat in &pat_tuple_struct.elems {
+                let elem_value = sanitize_pat_for_expr(&elem_pat)?;
+                elems.push(elem_value);
+            }
+            Ok(Pat::TupleStruct(PatTupleStruct {
+                attrs: vec![],
+                qself: pat_tuple_struct.qself.clone(),
+                path: pat_tuple_struct.path.clone(),
+                paren_token: pat_tuple_struct.paren_token,
+                elems,
+            }))
+        }
+        Pat::Macro(pat_macro) => Err(syn::Error::new_spanned(
+            &pat_macro,
+            "not allowed here due to `#[spec]`",
+        )),
+        Pat::Or(pat_or) => todo!(),
+        Pat::Rest(pat_rest) => todo!(),
+        Pat::Slice(pat_slice) => todo!(),
+        Pat::Verbatim(token_stream) => todo!(),
+        Pat::Wild(pat_wild) => todo!(),
+        _ => todo!(),
+    }
+}
+
 /// Prefix an identifier with `__anodized_`, preserving the original span.
 /// Used when generating mangled method names in trait and impl expansion.
 fn mangle_ident(original_ident: &syn::Ident) -> syn::Ident {
diff --git a/crates/anodized/tests/trait_fn_patterns.rs b/crates/anodized/tests/trait_fn_patterns.rs
index 498012e..b90470f 100644
--- a/crates/anodized/tests/trait_fn_patterns.rs
+++ b/crates/anodized/tests/trait_fn_patterns.rs
@@ -1,9 +1,9 @@
 use anodized::spec;
 
 #[spec]
-trait PatternArguments {
+trait TraitA {
     #[spec(requires: left <= right)]
-    fn func((left, right): (i32, i32)) {
+    fn func(input @ (left, right): (i32, i32)) {
         let _ = (left, right);
     }
 }
@@ -14,7 +14,7 @@ struct Bounds {
 }
 
 #[spec]
-trait PatternArguments {
+trait TraitB {
     #[spec(requires: lower <= upper)]
     fn func(Bounds { lower, upper }: Bounds) {
         let _ = (lower, upper);

From 8589727ad48a29d7dc4b1f63cc2bf1d3ab27df08 Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 14:21:01 +0900
Subject: [PATCH 03/15] improve tests

---
 crates/anodized-core/src/instrument/traits.rs | 40 ++++++++++++++-----
 crates/anodized/tests/trait_fn_patterns.rs    |  4 +-
 2 files changed, 33 insertions(+), 11 deletions(-)

diff --git a/crates/anodized-core/src/instrument/traits.rs b/crates/anodized-core/src/instrument/traits.rs
index 40006a0..8e58066 100644
--- a/crates/anodized-core/src/instrument/traits.rs
+++ b/crates/anodized-core/src/instrument/traits.rs
@@ -2,11 +2,11 @@
 #[path = "traits_tests.rs"]
 mod traits_tests;
 
-use quote::{ToTokens, quote};
+use quote::ToTokens;
 use syn::{
-    Attribute, Block, Expr, ExprCall, ExprStruct, ExprTuple, FnArg, ImplItem, ImplItemFn, Pat,
-    PatConst, PatIdent, PatLit, PatMacro, PatParen, PatPath, PatRange, PatStruct, PatTuple,
-    PatTupleStruct, ReturnType, TraitItem, TraitItemFn, Visibility, parse_quote,
+    Attribute, Block, FnArg, ImplItem, ImplItemFn, Pat, PatConst, PatIdent, PatLit, PatParen,
+    PatPath, PatRange, PatSlice, PatStruct, PatTuple, PatTupleStruct, ReturnType, TraitItem,
+    TraitItemFn, Visibility, parse_quote,
 };
 
 use crate::{
@@ -381,7 +381,7 @@ fn build_call_args(
     Ok(args)
 }
 
-/// Sanitize the pattern so that it may be used as an expression to reconstruct what it matched.
+/// Sanitize a pattern to be valid as an expression that reconstructs the matched value.
 fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
     match pat {
         Pat::Const(pat_const) => Ok(Pat::Const(PatConst {
@@ -478,15 +478,35 @@ fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
                 elems,
             }))
         }
+        Pat::Slice(pat_slice) => {
+            let mut elems = syn::punctuated::Punctuated::<syn::Pat, syn::token::Comma>::new();
+            for elem_pat in &pat_slice.elems {
+                let elem_value = sanitize_pat_for_expr(&elem_pat)?;
+                elems.push(elem_value);
+            }
+            Ok(Pat::Slice(PatSlice {
+                attrs: vec![],
+                bracket_token: pat_slice.bracket_token,
+                elems,
+            }))
+        }
+        Pat::Verbatim(token_stream) => Ok(Pat::Verbatim(token_stream.clone())),
         Pat::Macro(pat_macro) => Err(syn::Error::new_spanned(
             &pat_macro,
             "not allowed here due to `#[spec]`",
         )),
-        Pat::Or(pat_or) => todo!(),
-        Pat::Rest(pat_rest) => todo!(),
-        Pat::Slice(pat_slice) => todo!(),
-        Pat::Verbatim(token_stream) => todo!(),
-        Pat::Wild(pat_wild) => todo!(),
+        Pat::Or(pat_or) => Err(syn::Error::new_spanned(
+            &pat_or,
+            "or-pattern not allowed here due to `#[spec]`",
+        )),
+        Pat::Rest(pat_rest) => Err(syn::Error::new_spanned(
+            &pat_rest,
+            "not allowed here due to `#[spec]`",
+        )),
+        Pat::Wild(pat_wild) => Err(syn::Error::new_spanned(
+            &pat_wild,
+            "not allowed here due to `#[spec]`",
+        )),
         _ => todo!(),
     }
 }
diff --git a/crates/anodized/tests/trait_fn_patterns.rs b/crates/anodized/tests/trait_fn_patterns.rs
index b90470f..ba228b2 100644
--- a/crates/anodized/tests/trait_fn_patterns.rs
+++ b/crates/anodized/tests/trait_fn_patterns.rs
@@ -1,3 +1,5 @@
+#![allow(unused)]
+
 use anodized::spec;
 
 #[spec]
@@ -8,7 +10,7 @@ trait TraitA {
     }
 }
 
-struct Bounds {
+pub struct Bounds {
     lower: i32,
     upper: i32,
 }

From 96c6f2c8c0915de9225c2fa2e9b0197c35cea249 Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 14:24:44 +0900
Subject: [PATCH 04/15] clean up

---
 crates/anodized-core/src/instrument/traits.rs | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/crates/anodized-core/src/instrument/traits.rs b/crates/anodized-core/src/instrument/traits.rs
index 8e58066..5b290ab 100644
--- a/crates/anodized-core/src/instrument/traits.rs
+++ b/crates/anodized-core/src/instrument/traits.rs
@@ -2,7 +2,6 @@
 #[path = "traits_tests.rs"]
 mod traits_tests;
 
-use quote::ToTokens;
 use syn::{
     Attribute, Block, FnArg, ImplItem, ImplItemFn, Pat, PatConst, PatIdent, PatLit, PatParen,
     PatPath, PatRange, PatSlice, PatStruct, PatTuple, PatTupleStruct, ReturnType, TraitItem,
@@ -353,7 +352,7 @@ Instead, ensure that both the trait and the impl fn have a `#[spec]` annotation.
 /// Build argument tokens for calling the mangled trait method from the wrapper.
 ///
 /// Purpose: the wrapper method needs to forward its arguments to the mangled
-/// implementation, so this extracts a usable token for each input.
+/// implementation, so this constructs a usable expression for each input.
 ///
 /// Examples (inputs -> output tokens):
 /// - `fn f(&self, x: i32)` -> `self, x`
@@ -366,17 +365,17 @@ Instead, ensure that both the trait and the impl fn have a `#[spec]` annotation.
 /// part of the public API.
 fn build_call_args(
     inputs: &syn::punctuated::Punctuated<FnArg, syn::Token![,]>,
-) -> syn::Result<Vec<proc_macro2::TokenStream>> {
+) -> syn::Result<Vec<syn::Expr>> {
     let mut args = vec![];
     for input in inputs {
-        let tokens = match input {
-            FnArg::Receiver(receiver) => receiver.self_token.to_token_stream(),
+        let expr = match input {
+            FnArg::Receiver(_) => parse_quote!(self),
             FnArg::Typed(pat_type) => {
-                let expr = sanitize_pat_for_expr(&pat_type.pat)?;
-                expr.to_token_stream()
+                let pat = sanitize_pat_for_expr(&pat_type.pat)?;
+                parse_quote!(#pat)
             }
         };
-        args.push(tokens);
+        args.push(expr);
     }
     Ok(args)
 }

From 657e899a9f6f85ddd3b3a1d151c44f1308f35e08 Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 14:28:29 +0900
Subject: [PATCH 05/15] extend doc comment

---
 crates/anodized-core/src/instrument/traits.rs | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/crates/anodized-core/src/instrument/traits.rs b/crates/anodized-core/src/instrument/traits.rs
index 5b290ab..c140681 100644
--- a/crates/anodized-core/src/instrument/traits.rs
+++ b/crates/anodized-core/src/instrument/traits.rs
@@ -354,9 +354,11 @@ Instead, ensure that both the trait and the impl fn have a `#[spec]` annotation.
 /// Purpose: the wrapper method needs to forward its arguments to the mangled
 /// implementation, so this constructs a usable expression for each input.
 ///
-/// Examples (inputs -> output tokens):
-/// - `fn f(&self, x: i32)` -> `self, x`
-/// - `fn f(self, a: u8, b: u8)` -> `self, a, b`
+/// Examples (inputs -> output expressions):
+/// - `fn f(&self, x: i32)` -> `self`, `x`
+/// - `fn f(self, a: u8, b: u8)` -> `self`, `a`, `b`
+/// - `fn f(input @ (left, right): (i32, i32))` -> `input`
+/// - `fn f(Bounds { lower, upper }: Bounds)` -> `Bounds { lower, upper }`
 ///
 /// The caller is responsible for ensuring these tokens are used in a call
 /// expression like `Self::__anodized_f(#(#args),*)`.

From 58ad636165594ff5146697f9c8eb150bfef22a10 Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 14:30:06 +0900
Subject: [PATCH 06/15] nit

---
 crates/anodized-core/src/instrument/traits.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crates/anodized-core/src/instrument/traits.rs b/crates/anodized-core/src/instrument/traits.rs
index c140681..dcdd37b 100644
--- a/crates/anodized-core/src/instrument/traits.rs
+++ b/crates/anodized-core/src/instrument/traits.rs
@@ -354,7 +354,7 @@ Instead, ensure that both the trait and the impl fn have a `#[spec]` annotation.
 /// Purpose: the wrapper method needs to forward its arguments to the mangled
 /// implementation, so this constructs a usable expression for each input.
 ///
-/// Examples (inputs -> output expressions):
+/// Examples (inputs -> argument expressions):
 /// - `fn f(&self, x: i32)` -> `self`, `x`
 /// - `fn f(self, a: u8, b: u8)` -> `self`, `a`, `b`
 /// - `fn f(input @ (left, right): (i32, i32))` -> `input`

From d922194ec492eb585dca4c8a149bb0dcddf1bc7e Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 14:31:36 +0900
Subject: [PATCH 07/15] last todo

---
 crates/anodized-core/src/instrument/traits.rs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/crates/anodized-core/src/instrument/traits.rs b/crates/anodized-core/src/instrument/traits.rs
index dcdd37b..d8f7509 100644
--- a/crates/anodized-core/src/instrument/traits.rs
+++ b/crates/anodized-core/src/instrument/traits.rs
@@ -508,7 +508,10 @@ fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
             &pat_wild,
             "not allowed here due to `#[spec]`",
         )),
-        _ => todo!(),
+        _ => Err(syn::Error::new_spanned(
+            &pat,
+            "not allowed here due to `#[spec]`",
+        )),
     }
 }
 

From 8ab1144f79d5836c241b7554d612bd3eb7b3813b Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 14:34:58 +0900
Subject: [PATCH 08/15] rearrange

---
 crates/anodized-core/src/instrument/traits.rs | 28 +++++++++----------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/crates/anodized-core/src/instrument/traits.rs b/crates/anodized-core/src/instrument/traits.rs
index d8f7509..2e734eb 100644
--- a/crates/anodized-core/src/instrument/traits.rs
+++ b/crates/anodized-core/src/instrument/traits.rs
@@ -382,6 +382,20 @@ fn build_call_args(
     Ok(args)
 }
 
+/// Prefix an identifier with `__anodized_`, preserving the original span.
+/// Used when generating mangled method names in trait and impl expansion.
+fn mangle_ident(original_ident: &syn::Ident) -> syn::Ident {
+    syn::Ident::new(
+        &format!("__anodized_{original_ident}"),
+        original_ident.span(),
+    )
+}
+
+/// Checks to see if any `#[inline]` (with or without arg) exists in the function's attribs.
+fn has_inline_attr(attrs: &[syn::Attribute]) -> bool {
+    attrs.iter().any(|attr| attr.path().is_ident("inline"))
+}
+
 /// Sanitize a pattern to be valid as an expression that reconstructs the matched value.
 fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
     match pat {
@@ -514,17 +528,3 @@ fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
         )),
     }
 }
-
-/// Prefix an identifier with `__anodized_`, preserving the original span.
-/// Used when generating mangled method names in trait and impl expansion.
-fn mangle_ident(original_ident: &syn::Ident) -> syn::Ident {
-    syn::Ident::new(
-        &format!("__anodized_{original_ident}"),
-        original_ident.span(),
-    )
-}
-
-/// Checks to see if any `#[inline]` (with or without arg) exists in the function's attribs.
-fn has_inline_attr(attrs: &[syn::Attribute]) -> bool {
-    attrs.iter().any(|attr| attr.path().is_ident("inline"))
-}

From 963c2683230dae59b04ad1ca8853b5da13f8b51a Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 14:36:09 +0900
Subject: [PATCH 09/15] rename

---
 crates/anodized-core/src/instrument/traits.rs | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/crates/anodized-core/src/instrument/traits.rs b/crates/anodized-core/src/instrument/traits.rs
index 2e734eb..ddda400 100644
--- a/crates/anodized-core/src/instrument/traits.rs
+++ b/crates/anodized-core/src/instrument/traits.rs
@@ -373,7 +373,7 @@ fn build_call_args(
         let expr = match input {
             FnArg::Receiver(_) => parse_quote!(self),
             FnArg::Typed(pat_type) => {
-                let pat = sanitize_pat_for_expr(&pat_type.pat)?;
+                let pat = sanitize_pat_as_expr(&pat_type.pat)?;
                 parse_quote!(#pat)
             }
         };
@@ -397,7 +397,7 @@ fn has_inline_attr(attrs: &[syn::Attribute]) -> bool {
 }
 
 /// Sanitize a pattern to be valid as an expression that reconstructs the matched value.
-fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
+fn sanitize_pat_as_expr(pat: &Pat) -> syn::Result<Pat> {
     match pat {
         Pat::Const(pat_const) => Ok(Pat::Const(PatConst {
             attrs: vec![],
@@ -437,10 +437,10 @@ fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
         Pat::Paren(pat_paren) => Ok(Pat::Paren(PatParen {
             attrs: vec![],
             paren_token: pat_paren.paren_token,
-            pat: sanitize_pat_for_expr(&pat_paren.pat)?.into(),
+            pat: sanitize_pat_as_expr(&pat_paren.pat)?.into(),
         })),
-        Pat::Reference(pat_reference) => sanitize_pat_for_expr(&pat_reference.pat),
-        Pat::Type(pat_type) => sanitize_pat_for_expr(&pat_type.pat),
+        Pat::Reference(pat_reference) => sanitize_pat_as_expr(&pat_reference.pat),
+        Pat::Type(pat_type) => sanitize_pat_as_expr(&pat_type.pat),
         Pat::Struct(pat_struct) => {
             let None = pat_struct.rest else {
                 return Err(syn::Error::new_spanned(
@@ -454,7 +454,7 @@ fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
                     attrs: vec![],
                     member: field_pat.member.clone(),
                     colon_token: field_pat.colon_token,
-                    pat: sanitize_pat_for_expr(&field_pat.pat)?.into(),
+                    pat: sanitize_pat_as_expr(&field_pat.pat)?.into(),
                 };
                 fields.push(field_value);
             }
@@ -470,7 +470,7 @@ fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
         Pat::Tuple(pat_tuple) => {
             let mut elems = syn::punctuated::Punctuated::<syn::Pat, syn::token::Comma>::new();
             for elem_pat in &pat_tuple.elems {
-                let elem_value = sanitize_pat_for_expr(&elem_pat)?;
+                let elem_value = sanitize_pat_as_expr(&elem_pat)?;
                 elems.push(elem_value);
             }
             Ok(Pat::Tuple(PatTuple {
@@ -482,7 +482,7 @@ fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
         Pat::TupleStruct(pat_tuple_struct) => {
             let mut elems = syn::punctuated::Punctuated::<syn::Pat, syn::token::Comma>::new();
             for elem_pat in &pat_tuple_struct.elems {
-                let elem_value = sanitize_pat_for_expr(&elem_pat)?;
+                let elem_value = sanitize_pat_as_expr(&elem_pat)?;
                 elems.push(elem_value);
             }
             Ok(Pat::TupleStruct(PatTupleStruct {
@@ -496,7 +496,7 @@ fn sanitize_pat_for_expr(pat: &Pat) -> syn::Result<Pat> {
         Pat::Slice(pat_slice) => {
             let mut elems = syn::punctuated::Punctuated::<syn::Pat, syn::token::Comma>::new();
             for elem_pat in &pat_slice.elems {
-                let elem_value = sanitize_pat_for_expr(&elem_pat)?;
+                let elem_value = sanitize_pat_as_expr(&elem_pat)?;
                 elems.push(elem_value);
             }
             Ok(Pat::Slice(PatSlice {

From e0aa20dcb0b51891b06450f1a6e07ce98d224481 Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 15:11:59 +0900
Subject: [PATCH 10/15] clippy

---
 crates/anodized-core/src/instrument/traits.rs | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/crates/anodized-core/src/instrument/traits.rs b/crates/anodized-core/src/instrument/traits.rs
index ddda400..2ab1bd3 100644
--- a/crates/anodized-core/src/instrument/traits.rs
+++ b/crates/anodized-core/src/instrument/traits.rs
@@ -407,7 +407,7 @@ fn sanitize_pat_as_expr(pat: &Pat) -> syn::Result<Pat> {
         Pat::Ident(pat_ident) if pat_ident.by_ref.is_none() => {
             let None = pat_ident.by_ref else {
                 return Err(syn::Error::new_spanned(
-                    &pat_ident.by_ref,
+                    pat_ident.by_ref,
                     "not allowed here due to `#[spec]`",
                 ));
             };
@@ -470,7 +470,7 @@ fn sanitize_pat_as_expr(pat: &Pat) -> syn::Result<Pat> {
         Pat::Tuple(pat_tuple) => {
             let mut elems = syn::punctuated::Punctuated::<syn::Pat, syn::token::Comma>::new();
             for elem_pat in &pat_tuple.elems {
-                let elem_value = sanitize_pat_as_expr(&elem_pat)?;
+                let elem_value = sanitize_pat_as_expr(elem_pat)?;
                 elems.push(elem_value);
             }
             Ok(Pat::Tuple(PatTuple {
@@ -482,7 +482,7 @@ fn sanitize_pat_as_expr(pat: &Pat) -> syn::Result<Pat> {
         Pat::TupleStruct(pat_tuple_struct) => {
             let mut elems = syn::punctuated::Punctuated::<syn::Pat, syn::token::Comma>::new();
             for elem_pat in &pat_tuple_struct.elems {
-                let elem_value = sanitize_pat_as_expr(&elem_pat)?;
+                let elem_value = sanitize_pat_as_expr(elem_pat)?;
                 elems.push(elem_value);
             }
             Ok(Pat::TupleStruct(PatTupleStruct {
@@ -496,7 +496,7 @@ fn sanitize_pat_as_expr(pat: &Pat) -> syn::Result<Pat> {
         Pat::Slice(pat_slice) => {
             let mut elems = syn::punctuated::Punctuated::<syn::Pat, syn::token::Comma>::new();
             for elem_pat in &pat_slice.elems {
-                let elem_value = sanitize_pat_as_expr(&elem_pat)?;
+                let elem_value = sanitize_pat_as_expr(elem_pat)?;
                 elems.push(elem_value);
             }
             Ok(Pat::Slice(PatSlice {
@@ -507,23 +507,23 @@ fn sanitize_pat_as_expr(pat: &Pat) -> syn::Result<Pat> {
         }
         Pat::Verbatim(token_stream) => Ok(Pat::Verbatim(token_stream.clone())),
         Pat::Macro(pat_macro) => Err(syn::Error::new_spanned(
-            &pat_macro,
+            pat_macro,
             "not allowed here due to `#[spec]`",
         )),
         Pat::Or(pat_or) => Err(syn::Error::new_spanned(
-            &pat_or,
+            pat_or,
             "or-pattern not allowed here due to `#[spec]`",
         )),
         Pat::Rest(pat_rest) => Err(syn::Error::new_spanned(
-            &pat_rest,
+            pat_rest,
             "not allowed here due to `#[spec]`",
         )),
         Pat::Wild(pat_wild) => Err(syn::Error::new_spanned(
-            &pat_wild,
+            pat_wild,
             "not allowed here due to `#[spec]`",
         )),
         _ => Err(syn::Error::new_spanned(
-            &pat,
+            pat,
             "not allowed here due to `#[spec]`",
         )),
     }

From d3e11bcc98aba28561fc93b3915dbf18619f2c6e Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 15:39:44 +0900
Subject: [PATCH 11/15] improve tests

---
 crates/anodized/tests/trait_fn_patterns.rs | 64 ++++++++++++++++++----
 1 file changed, 54 insertions(+), 10 deletions(-)

diff --git a/crates/anodized/tests/trait_fn_patterns.rs b/crates/anodized/tests/trait_fn_patterns.rs
index ba228b2..aacda9b 100644
--- a/crates/anodized/tests/trait_fn_patterns.rs
+++ b/crates/anodized/tests/trait_fn_patterns.rs
@@ -3,22 +3,66 @@
 use anodized::spec;
 
 #[spec]
-trait TraitA {
-    #[spec(requires: left <= right)]
-    fn func(input @ (left, right): (i32, i32)) {
-        let _ = (left, right);
+trait Trait {
+    #[spec(requires: left < right)]
+    fn func_1(input @ (left, right): (i32, i32)) {
+        unimplemented!()
+    }
+
+    #[spec(requires: lower < upper)]
+    fn func_2(Bounds { lower, upper }: Bounds) {
+        unimplemented!()
+    }
+
+    #[spec(
+        requires: [
+            lower < upper,
+            i >= i,
+            i < upper,
+        ],
+    )]
+    fn func_3((i, Bounds { lower, upper }): (i32, Bounds)) {
+        unimplemented!()
     }
 }
 
-pub struct Bounds {
+struct Bounds {
     lower: i32,
     upper: i32,
 }
 
+struct Type;
+
 #[spec]
-trait TraitB {
-    #[spec(requires: lower <= upper)]
-    fn func(Bounds { lower, upper }: Bounds) {
-        let _ = (lower, upper);
-    }
+impl Trait for Type {
+    fn func_1(_: (i32, i32)) {}
+    fn func_2(_: Bounds) {}
+    fn func_3(_: (i32, Bounds)) {}
+}
+
+#[cfg(all(anodized_print, anodized_panic))]
+#[test]
+#[should_panic(expected = r#"precondition failed:
+    left < right"#)]
+fn test_1() {
+    let _ = Type::func_1((42, 1));
+}
+
+#[cfg(all(anodized_print, anodized_panic))]
+#[test]
+#[should_panic(expected = r#"precondition failed:
+    lower < upper"#)]
+fn test_2() {
+    let _ = Type::func_2(Bounds {
+        lower: 42,
+        upper: 1,
+    });
+}
+
+#[cfg(all(anodized_print, anodized_panic))]
+#[test]
+#[should_panic(expected = r#"precondition failed:
+    i < upper"#)]
+fn test_3() {
+    let _ = Type::func_3((42, Bounds { lower: 1, upper: 5 }));
 }

From 2977839e03eba28e03ad1c58faf7a8bb9f9dfc85 Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 15:41:35 +0900
Subject: [PATCH 12/15] nit

---
 crates/anodized/tests/trait_fn_patterns.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crates/anodized/tests/trait_fn_patterns.rs b/crates/anodized/tests/trait_fn_patterns.rs
index aacda9b..3203901 100644
--- a/crates/anodized/tests/trait_fn_patterns.rs
+++ b/crates/anodized/tests/trait_fn_patterns.rs
@@ -17,7 +17,7 @@ trait Trait {
     #[spec(
         requires: [
             lower < upper,
-            i >= i,
+            i >= lower,
             i < upper,
         ],
     )]

From 0dbeda742427850d0af5155f7a5052d360c302dc Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 15:42:46 +0900
Subject: [PATCH 13/15] improve doc comment

---
 crates/anodized-core/src/instrument/traits.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/crates/anodized-core/src/instrument/traits.rs b/crates/anodized-core/src/instrument/traits.rs
index 2ab1bd3..34ed7ee 100644
--- a/crates/anodized-core/src/instrument/traits.rs
+++ b/crates/anodized-core/src/instrument/traits.rs
@@ -360,8 +360,8 @@ Instead, ensure that both the trait and the impl fn have a `#[spec]` annotation.
 /// - `fn f(input @ (left, right): (i32, i32))` -> `input`
 /// - `fn f(Bounds { lower, upper }: Bounds)` -> `Bounds { lower, upper }`
 ///
-/// The caller is responsible for ensuring these tokens are used in a call
-/// expression like `Self::__anodized_f(#(#args),*)`.
+/// The caller is responsible for ensuring these expressions are used in a call
+/// like `Self::__anodized_f(#(#args),*)`.
 ///
 /// Callers: only `instrument_trait` in this module should use this; it is not
 /// part of the public API.

From 3256bfc6be4fc868af1edacfa9870dc2bdc54053 Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 15:47:34 +0900
Subject: [PATCH 14/15] improve tests

---
 crates/anodized/tests/trait_fn_patterns.rs | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/crates/anodized/tests/trait_fn_patterns.rs b/crates/anodized/tests/trait_fn_patterns.rs
index 3203901..119dd02 100644
--- a/crates/anodized/tests/trait_fn_patterns.rs
+++ b/crates/anodized/tests/trait_fn_patterns.rs
@@ -15,13 +15,13 @@ trait Trait {
     }
 
     #[spec(
-        requires: [
-            lower < upper,
-            i >= lower,
-            i < upper,
+        requires: lower < upper,
+        ensures: [
+            *output >= lower,
+            *output < upper,
         ],
     )]
-    fn func_3((i, Bounds { lower, upper }): (i32, Bounds)) {
+    fn func_3((i, Bounds { lower, upper }): (i32, Bounds)) -> i32 {
         unimplemented!()
     }
 }
@@ -37,7 +37,9 @@ struct Type;
 impl Trait for Type {
     fn func_1(_: (i32, i32)) {}
     fn func_2(_: Bounds) {}
-    fn func_3(_: (i32, Bounds)) {}
+    fn func_3((i, _): (i32, Bounds)) -> i32 {
+        i
+    }
 }
 
 #[cfg(all(anodized_print, anodized_panic))]
@@ -61,8 +63,8 @@ fn test_2() {
 
 #[cfg(all(anodized_print, anodized_panic))]
 #[test]
-#[should_panic(expected = r#"precondition failed:
-    i < upper"#)]
+#[should_panic(expected = r#"postcondition failed:
+    | output | * output < upper"#)]
 fn test_3() {
     let _ = Type::func_3((42, Bounds { lower: 1, upper: 5 }));
 }

From 978ae7992a5dec5882bd3aee5e2a782bdc39f0fb Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 21 Jul 2026 16:01:15 +0900
Subject: [PATCH 15/15] refine test

---
 crates/anodized/tests/trait_fn_patterns.rs | 25 ++++++++++++----------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/crates/anodized/tests/trait_fn_patterns.rs b/crates/anodized/tests/trait_fn_patterns.rs
index 119dd02..d32a415 100644
--- a/crates/anodized/tests/trait_fn_patterns.rs
+++ b/crates/anodized/tests/trait_fn_patterns.rs
@@ -3,41 +3,44 @@
 use anodized::spec;
 
 #[spec]
-trait Trait {
+trait Trait<T: Ord + Copy> {
     #[spec(requires: left < right)]
     fn func_1(input @ (left, right): (i32, i32)) {
         unimplemented!()
     }
 
     #[spec(requires: lower < upper)]
-    fn func_2(Bounds { lower, upper }: Bounds) {
+    fn func_2(Bounds { lower, upper }: Bounds<T>) {
         unimplemented!()
     }
 
     #[spec(
         requires: lower < upper,
+        // NOTE: `T: Copy` is needed for this to work at the moment.
         ensures: [
             *output >= lower,
             *output < upper,
         ],
     )]
-    fn func_3((i, Bounds { lower, upper }): (i32, Bounds)) -> i32 {
+    fn func_3((input, Bounds { lower, upper }): (T, Bounds<T>)) -> T {
         unimplemented!()
     }
 }
 
-struct Bounds {
-    lower: i32,
-    upper: i32,
+struct Bounds<T> {
+    lower: T,
+    upper: T,
 }
 
-struct Type;
+struct Type<T> {
+    _phantom: std::marker::PhantomData<T>,
+}
 
 #[spec]
-impl Trait for Type {
+impl<T: Ord + Copy> Trait<T> for Type<T> {
     fn func_1(_: (i32, i32)) {}
-    fn func_2(_: Bounds) {}
-    fn func_3((i, _): (i32, Bounds)) -> i32 {
+    fn func_2(_: Bounds<T>) {}
+    fn func_3((i, _): (T, Bounds<T>)) -> T {
         i
     }
 }
@@ -47,7 +50,7 @@ impl Trait for Type {
 #[should_panic(expected = r#"precondition failed:
     left < right"#)]
 fn test_1() {
-    let _ = Type::func_1((42, 1));
+    let _ = Type::<i32>::func_1((42, 1));
 }
 
 #[cfg(all(anodized_print, anodized_panic))]