diff --git a/.gitignore b/.gitignore
index ea8c4bf..2f7896d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-/target
+target/
diff --git a/Cargo.lock b/Cargo.lock
index acdb4d0..d262154 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -711,11 +711,21 @@ dependencies = [
  "process_control",
  "tempfile",
  "thiserror 2.0.18",
+ "thrust-macros",
  "tracing",
  "tracing-subscriber",
  "ui_test",
 ]
 
+[[package]]
+name = "thrust-macros"
+version = "0.1.0"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
 [[package]]
 name = "tracing"
 version = "0.1.44"
diff --git a/Cargo.toml b/Cargo.toml
index 2cc1907..72b9bd5 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,3 +1,7 @@
+[workspace]
+members = [".", "thrust-macros"]
+resolver = "2"
+
 [package]
 name = "thrust"
 version = "0.1.0"
@@ -18,6 +22,11 @@ name = "ui"
 harness = false
 
 [dependencies]
+# Workaround until thrust supports invocation via cargo: adding thrust-macros as
+# a dependency ensures cargo builds (and rebuilds) it alongside thrust. It is not
+# used as a proc-macro here; the dylib is loaded at runtime via --extern.
+thrust-macros = { path = "thrust-macros" }
+
 anyhow = "1.0.102"
 pretty = { version = "0.12.5", features = ["termcolor"] }
 tempfile = "3.27.0"
diff --git a/src/main.rs b/src/main.rs
index 391424e..1a26967 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -66,8 +66,36 @@ impl Callbacks for CompilerCalls {
     }
 }
 
+fn thrust_macros_path() -> Option<std::path::PathBuf> {
+    let exe = std::env::current_exe().ok()?;
+    let dir = exe.parent()?;
+    // When thrust-macros is a cargo dependency it lands in deps/ with a hash
+    // suffix (e.g. libthrust_macros-<hash>.so), so check both locations.
+    let search_dirs = [dir.to_path_buf(), dir.join("deps")];
+    for search_dir in &search_dirs {
+        for ext in ["so", "dylib", "dll"] {
+            // First try the exact name (e.g. when built standalone).
+            let candidate = search_dir.join(format!("libthrust_macros.{ext}"));
+            if candidate.exists() {
+                return Some(candidate);
+            }
+            // Then scan for libthrust_macros-<hash>.<ext>.
+            if let Ok(entries) = std::fs::read_dir(search_dir) {
+                for entry in entries.flatten() {
+                    let name = entry.file_name();
+                    let name = name.to_string_lossy();
+                    if name.starts_with("libthrust_macros-") && name.ends_with(ext) {
+                        return Some(entry.path());
+                    }
+                }
+            }
+        }
+    }
+    None
+}
+
 pub fn main() {
-    let args = std::env::args().collect::<Vec<_>>();
+    let mut args = std::env::args().collect::<Vec<_>>();
 
     use tracing_subscriber::{filter::EnvFilter, prelude::*};
     tracing_subscriber::registry()
@@ -80,6 +108,14 @@ pub fn main() {
         )
         .init();
 
+    if let Some(path) = thrust_macros_path() {
+        args.push("--extern".to_owned());
+        args.push(format!("thrust_macros={}", path.display()));
+        tracing::debug!("linking thrust_macros from {}", path.display());
+    } else {
+        tracing::warn!("could not locate thrust_macros library");
+    }
+
     let code =
         rustc_driver::catch_with_exit_code(|| RunCompiler::new(&args, &mut CompilerCalls {}).run());
     std::process::exit(code);
diff --git a/std.rs b/std.rs
index 6d6718c..fb0abcd 100644
--- a/std.rs
+++ b/std.rs
@@ -273,179 +273,232 @@ mod thrust_models {
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(result == <x>)]
-fn _extern_spec_box_new<T>(x: T) -> Box<T> where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == thrust_models::model::Box::new(x))]
+fn _extern_spec_box_new<T>(x: T) -> Box<T> where T: thrust_models::Model, T::Ty: PartialEq {
     Box::new(x)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(*x == ^y && *y == ^x)]
-fn _extern_spec_std_mem_swap<T>(x: &mut T, y: &mut T) where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == (x == y))]
+fn _extern_spec_box_partialeq_eq<T>(x: &Box<T>, y: &Box<T>) -> bool
+  where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
+{
+    <Box<T> as PartialEq>::eq(x, y)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(*x == !y && *y == !x)]
+fn _extern_spec_std_mem_swap<T>(x: &mut T, y: &mut T) where T: thrust_models::Model, T::Ty: PartialEq {
     std::mem::swap(x, y)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(^dest == src && result == *dest)]
-fn _extern_spec_std_mem_replace<T>(dest: &mut T, src: T) -> T where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(!dest == src && result == *dest)]
+fn _extern_spec_std_mem_replace<T>(dest: &mut T, src: T) -> T where T: thrust_models::Model, T::Ty: PartialEq {
     std::mem::replace(dest, src)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(opt != std::option::Option::<T0>::None())]
-#[thrust::ensures(std::option::Option::<T0>::Some(result) == opt)]
-fn _extern_spec_option_unwrap<T>(opt: Option<T>) -> T where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == (x == y))]
+fn _extern_spec_option_partialeq_eq<T>(x: &Option<T>, y: &Option<T>) -> bool
+  where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
+{
+    <Option<T> as PartialEq>::eq(x, y)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(opt != None)]
+#[thrust_macros::ensures(Some(result) == opt)]
+fn _extern_spec_option_unwrap<T>(opt: Option<T>) -> T where T: thrust_models::Model, T::Ty: PartialEq {
     Option::unwrap(opt)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
-    (*opt == std::option::Option::<T0>::None() && result == true)
-    || (*opt != std::option::Option::<T0>::None() && result == false)
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*opt == None && result == true)
+    || (*opt != None && result == false)
 )]
-fn _extern_spec_option_is_none<T>(opt: &Option<T>) -> bool where T: thrust_models::Model {
+fn _extern_spec_option_is_none<T>(opt: &Option<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
     Option::is_none(opt)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
-    (*opt == std::option::Option::<T0>::None() && result == false)
-    || (*opt != std::option::Option::<T0>::None() && result == true)
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*opt == None && result == false)
+    || (*opt != None && result == true)
 )]
-fn _extern_spec_option_is_some<T>(opt: &Option<T>) -> bool where T: thrust_models::Model {
+fn _extern_spec_option_is_some<T>(opt: &Option<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
     Option::is_some(opt)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
-    (opt != std::option::Option::<T0>::None() && std::option::Option::<T0>::Some(result) == opt)
-    || (opt == std::option::Option::<T0>::None() && result == default)
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (opt != None && Some(result) == opt)
+    || (opt == None && result == default)
 )]
-fn _extern_spec_option_unwrap_or<T>(opt: Option<T>, default: T) -> T where T: thrust_models::Model {
+fn _extern_spec_option_unwrap_or<T>(opt: Option<T>, default: T) -> T where T: thrust_models::Model, T::Ty: PartialEq {
     Option::unwrap_or(opt, default)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
-    (exists x:T0. opt == std::option::Option::<T0>::Some(x) && result == std::result::Result::<T0, T1>::Ok(x))
-    || (opt == std::option::Option::<T0>::None() && result == std::result::Result::<T0, T1>::Err(err))
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (thrust_models::exists(|x| opt == Some(x) && result == Ok(x)))
+    || (opt == None && result == Err(err))
 )]
-fn _extern_spec_option_ok_or<T, E>(opt: Option<T>, err: E) -> Result<T, E> where T: thrust_models::Model, E: thrust_models::Model {
+fn _extern_spec_option_ok_or<T, E>(opt: Option<T>, err: E) -> Result<T, E>
+    where T: thrust_models::Model, T::Ty: PartialEq,
+          E: thrust_models::Model, E::Ty: PartialEq,
+{
     Option::ok_or(opt, err)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(^opt == std::option::Option::<T0>::None() && result == *opt)]
-fn _extern_spec_option_take<T>(opt: &mut Option<T>) -> Option<T> where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(!opt == None && result == *opt)]
+fn _extern_spec_option_take<T>(opt: &mut Option<T>) -> Option<T> where T: thrust_models::Model, T::Ty: PartialEq {
     Option::take(opt)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(^opt == std::option::Option::<T0>::Some(src) && result == *opt)]
-fn _extern_spec_option_replace<T>(opt: &mut Option<T>, src: T) -> Option<T> where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(!opt == Some(src) && result == *opt)]
+fn _extern_spec_option_replace<T>(opt: &mut Option<T>, src: T) -> Option<T>
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
     Option::replace(opt, src)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
-    (exists x:T0. opt == <std::option::Option::<T0>::Some(x)> && result == std::option::Option::<&T0>::Some(<x>))
-    || (opt == <std::option::Option::<T0>::None()> && result == std::option::Option::<&T0>::None())
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    thrust_models::exists(|x| opt == &Some(x) && result == Some(&x))
+    || (opt == &None && result == None)
 )]
-fn _extern_spec_option_as_ref<T>(opt: &Option<T>) -> Option<&T> where T: thrust_models::Model {
+fn _extern_spec_option_as_ref<T>(opt: &Option<T>) -> Option<&T> where T: thrust_models::Model, T::Ty: PartialEq {
     Option::as_ref(opt)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
-    (exists x1:T0, x2:T0.
-      *opt == std::option::Option::<T0>::Some(x1) &&
-      ^opt == std::option::Option::<T0>::Some(x2) &&
-      result == std::option::Option::<&mut T0>::Some(<x1, x2>)
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    thrust_models::exists(|x1, x2|
+      *opt == Some(x1) &&
+      !opt == Some(x2) &&
+      result == Some(thrust_models::model::Mut::new(x1, x2))
     )
     || (
-      *opt == std::option::Option::<T0>::None() &&
-      ^opt == std::option::Option::<T0>::None() &&
-      result == std::option::Option::<&mut T0>::None()
+      *opt == None &&
+      !opt == None &&
+      result == None
     )
 )]
-fn _extern_spec_option_as_mut<T>(opt: &mut Option<T>) -> Option<&mut T> where T: thrust_models::Model {
+fn _extern_spec_option_as_mut<T>(opt: &mut Option<T>) -> Option<&mut T>
+  where T: thrust_models::Model, T::Ty: PartialEq
+{
     Option::as_mut(opt)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(exists x:T0. res == std::result::Result::<T0, T1>::Ok(x))]
-#[thrust::ensures(std::result::Result::<T0, T1>::Ok(result) == res)]
-fn _extern_spec_result_unwrap<T, E: std::fmt::Debug>(res: Result<T, E>) -> T where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == (x == y))]
+fn _extern_spec_result_partialeq_eq<T, E>(x: &Result<T, E>, y: &Result<T, E>) -> bool
+  where T: thrust_models::Model + PartialEq, T::Ty: PartialEq,
+        E: thrust_models::Model + PartialEq, E::Ty: PartialEq,
+{
+    <Result<T, E> as PartialEq>::eq(x, y)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(thrust_models::exists(|x| res == Ok(x)))]
+#[thrust_macros::ensures(Ok(result) == res)]
+fn _extern_spec_result_unwrap<T, E: std::fmt::Debug>(res: Result<T, E>) -> T
+  where T: thrust_models::Model, T::Ty: PartialEq,
+        E: thrust_models::Model, E::Ty: PartialEq,
+{
     Result::unwrap(res)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(exists x:T1. res == std::result::Result::<T0, T1>::Err(x))]
-#[thrust::ensures(std::result::Result::<T0, T1>::Err(result) == res)]
-fn _extern_spec_result_unwrap_err<T: std::fmt::Debug, E>(res: Result<T, E>) -> E where T: thrust_models::Model, E: thrust_models::Model {
+#[thrust_macros::requires(thrust_models::exists(|x| res == Err(x)))]
+#[thrust_macros::ensures(Err(result) == res)]
+fn _extern_spec_result_unwrap_err<T: std::fmt::Debug, E>(res: Result<T, E>) -> E
+  where T: thrust_models::Model, T::Ty: PartialEq,
+        E: thrust_models::Model, E::Ty: PartialEq,
+{
     Result::unwrap_err(res)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
-    (exists x:T0. res == std::result::Result::<T0, T1>::Ok(x) && result == std::option::Option::<T0>::Some(x))
-    || (exists x:T1. res == std::result::Result::<T0, T1>::Err(x) && result == std::option::Option::<T0>::None())
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    thrust_models::exists(|x| res == Ok(x) && result == Some(x))
+    || thrust_models::exists(|x| res == Err(x) && result == None)
 )]
-fn _extern_spec_result_ok<T, E>(res: Result<T, E>) -> Option<T> where T: thrust_models::Model, E: thrust_models::Model {
+fn _extern_spec_result_ok<T, E>(res: Result<T, E>) -> Option<T>
+  where T: thrust_models::Model, T::Ty: PartialEq,
+        E: thrust_models::Model, E::Ty: PartialEq,
+{
     Result::ok(res)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
-    (exists x:T0. res == std::result::Result::<T0, T1>::Ok(x) && result == std::option::Option::<T1>::None())
-    || (exists x:T1. res == std::result::Result::<T0, T1>::Err(x) && result == std::option::Option::<T1>::Some(x))
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    thrust_models::exists(|x| res == Ok(x) && result == None)
+    || thrust_models::exists(|x| res == Err(x) && result == Some(x))
 )]
-fn _extern_spec_result_err<T, E>(res: Result<T, E>) -> Option<E> where T: thrust_models::Model, E: thrust_models::Model {
+fn _extern_spec_result_err<T, E>(res: Result<T, E>) -> Option<E>
+  where T: thrust_models::Model, T::Ty: PartialEq,
+        E: thrust_models::Model, E::Ty: PartialEq,
+{
     Result::err(res)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
-    (exists x:T0. *res == std::result::Result::<T0, T1>::Ok(x) && result == true)
-    || (exists x:T1. *res == std::result::Result::<T0, T1>::Err(x) && result == false)
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    thrust_models::exists(|x| *res == Ok(x) && result == true)
+    || thrust_models::exists(|x| *res == Err(x) && result == false)
 )]
-fn _extern_spec_result_is_ok<T, E>(res: &Result<T, E>) -> bool where T: thrust_models::Model, E: thrust_models::Model {
+fn _extern_spec_result_is_ok<T, E>(res: &Result<T, E>) -> bool
+  where T: thrust_models::Model, T::Ty: PartialEq,
+        E: thrust_models::Model, E::Ty: PartialEq,
+{
     Result::is_ok(res)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
-    (exists x:T0. *res == std::result::Result::<T0, T1>::Ok(x) && result == false)
-    || (exists x:T1. *res == std::result::Result::<T0, T1>::Err(x) && result == true)
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    thrust_models::exists(|x| *res == Ok(x) && result == false)
+    || thrust_models::exists(|x| *res == Err(x) && result == true)
 )]
-fn _extern_spec_result_is_err<T, E>(res: &Result<T, E>) -> bool where T: thrust_models::Model, E: thrust_models::Model {
+fn _extern_spec_result_is_err<T, E>(res: &Result<T, E>) -> bool
+  where T: thrust_models::Model, T::Ty: PartialEq,
+        E: thrust_models::Model, E::Ty: PartialEq,
+{
     Result::is_err(res)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)] // TODO: require x != i32::MIN
-#[thrust::ensures(result >= 0 && (result == x || result == -x))]
+#[thrust_macros::requires(true)] // TODO: require x != i32::MIN
+#[thrust_macros::ensures(result >= 0 && (result == x || result == -x))]
 fn _extern_spec_i32_abs(x: i32) -> i32 {
     i32::abs(x)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
     (x >= y && result == (x - y))
     || (x < y && result == (y - x))
 )]
@@ -454,109 +507,113 @@ fn _extern_spec_i32_abs_diff(x: i32, y: i32) -> u32 {
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))]
 fn _extern_spec_i32_signum(x: i32) -> i32 {
     i32::signum(x)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures((x < 0 && result == false) || (x >= 0 && result == true))]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures((x < 0 && result == false) || (x >= 0 && result == true))]
 fn _extern_spec_i32_is_positive(x: i32) -> bool {
     i32::is_positive(x)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures((x <= 0 && result == true) || (x > 0 && result == false))]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures((x <= 0 && result == true) || (x > 0 && result == false))]
 fn _extern_spec_i32_is_negative(x: i32) -> bool {
     i32::is_negative(x)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(*result.1 == 0)]
-fn _extern_spec_vec_new<T>() -> Vec<T> where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result.1 == 0)]
+fn _extern_spec_vec_new<T>() -> Vec<T> where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::<T>::new()
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(^vec == ((*(*vec).0).store(*(*vec).1, elem), *(*vec).1 + 1))]
-fn _extern_spec_vec_push<T>(vec: &mut Vec<T>, elem: T) where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(!vec == thrust_models::model::Vec((*vec).0.store((*vec).1, elem), (*vec).1 + 1))]
+fn _extern_spec_vec_push<T>(vec: &mut Vec<T>, elem: T)
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
     Vec::push(vec, elem)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(result == *(*vec).1)]
-fn _extern_spec_vec_len<T>(vec: &Vec<T>) -> usize where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == vec.1)]
+fn _extern_spec_vec_len<T>(vec: &Vec<T>) -> usize where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::len(vec)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(index < *(*vec).1)]
-#[thrust::ensures(*result == (*(*vec).0).select(index))]
-fn _extern_spec_vec_index<T>(vec: &Vec<T>, index: usize) -> &T where T: thrust_models::Model {
+#[thrust_macros::requires(index < vec.1)]
+#[thrust_macros::ensures(*result == vec.0[index])]
+fn _extern_spec_vec_index<T>(vec: &Vec<T>, index: usize) -> &T where T: thrust_models::Model, T::Ty: PartialEq {
     <Vec<T> as std::ops::Index<usize>>::index(vec, index)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(index < *(*vec).1)]
-#[thrust::ensures(
-    *result == (*(*vec).0).select(index) &&
-    ^result == (*(^vec).0).select(index) &&
-    ^vec == (<(*(*vec).0).store(index, ^result)>, (*vec).1)
+#[thrust_macros::requires(index < (*vec).1)]
+#[thrust_macros::ensures(
+    *result == (*vec).0[index] &&
+    !result == (!vec).0[index] &&
+    !vec == thrust_models::model::Vec((*vec).0.store(index, !result), (*vec).1)
 )]
-fn _extern_spec_vec_index_mut<T>(vec: &mut Vec<T>, index: usize) -> &mut T where T: thrust_models::Model {
+fn _extern_spec_vec_index_mut<T>(vec: &mut Vec<T>, index: usize) -> &mut T
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
     <Vec<T> as std::ops::IndexMut<usize>>::index_mut(vec, index)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(*(^vec).1 == 0)]
-fn _extern_spec_vec_clear<T>(vec: &mut Vec<T>) where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures((!vec).1 == 0)]
+fn _extern_spec_vec_clear<T>(vec: &mut Vec<T>) where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::clear(vec)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
-    (^vec).0 == (*vec).0 && (
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (!vec).0 == (*vec).0 && (
         (
-            *(*vec).1 > 0 &&
-            *(^vec).1 == *(*vec).1 - 1 &&
-            result == std::option::Option::<T0>::Some((*(*vec).0).select(*(*vec).1 - 1))
+            (*vec).1 > 0 &&
+            (!vec).1 == (*vec).1 - 1 &&
+            result == Some((*vec).0[(*vec).1 - 1])
         ) || (
-            *(*vec).1 == 0 &&
-            *(^vec).1 == 0 &&
-            result == std::option::Option::<T0>::None()
+            (*vec).1 == 0 &&
+            (!vec).1 == 0 &&
+            result == None
         )
     )
 )]
-fn _extern_spec_vec_pop<T>(vec: &mut Vec<T>) -> Option<T> where T: thrust_models::Model {
+fn _extern_spec_vec_pop<T>(vec: &mut Vec<T>) -> Option<T> where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::pop(vec)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(result == (*(*vec).1 == 0))]
-fn _extern_spec_vec_is_empty<T>(vec: &Vec<T>) -> bool where T: thrust_models::Model {
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == ((*vec).1 == 0))]
+fn _extern_spec_vec_is_empty<T>(vec: &Vec<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::is_empty(vec)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust::requires(true)]
-#[thrust::ensures(
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
     (
-        *(*vec).1 > len &&
-        ^vec == (<(*vec).0>, <len>)
+        (*vec).1 > len &&
+        !vec == thrust_models::model::Vec((*vec).0, len)
     ) || (
-        *(*vec).1 <= len &&
-        ^vec == *vec
+        (*vec).1 <= len &&
+        !vec == *vec
     )
 )]
-fn _extern_spec_vec_truncate<T>(vec: &mut Vec<T>, len: usize) where T: thrust_models::Model {
+fn _extern_spec_vec_truncate<T>(vec: &mut Vec<T>, len: usize) where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::truncate(vec, len)
 }
diff --git a/tests/ui/fail/annot_enum_simple.rs b/tests/ui/fail/annot_enum_simple.rs
index b0f9077..f97225a 100644
--- a/tests/ui/fail/annot_enum_simple.rs
+++ b/tests/ui/fail/annot_enum_simple.rs
@@ -1,12 +1,17 @@
 //@error-in-other-file: Unsat
 
+#[derive(PartialEq)]
 pub enum X {
     A(i64),
     B(bool),
 }
 
-#[thrust::requires(x == X::A(1))]
-#[thrust::ensures(true)]
+impl thrust_models::Model for X {
+    type Ty = X;
+}
+
+#[thrust_macros::requires(x == X::A(1))]
+#[thrust_macros::ensures(true)]
 fn test(x: X) {
     if let X::A(i) = x {
         assert!(i == 2);
diff --git a/tests/ui/fail/annot_exists.rs b/tests/ui/fail/annot_exists.rs
index 2558b59..496cfae 100644
--- a/tests/ui/fail/annot_exists.rs
+++ b/tests/ui/fail/annot_exists.rs
@@ -2,12 +2,14 @@
 //@compile-flags: -C debug-assertions=off
 //@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
 
+use thrust_models::exists;
+
 #[thrust::trusted]
 #[thrust::callable]
 fn rand() -> i32 { unimplemented!() }
 
-#[thrust::requires(true)]
-#[thrust::ensures(exists x:int. result == 2 * x)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(exists(|x: i32| result == 2 * x))]
 fn f() -> i32 {
     let x = rand();
     x + x + x
diff --git a/tests/ui/fail/annot_mut_term.rs b/tests/ui/fail/annot_mut_term.rs
index f1037dd..c7035b1 100644
--- a/tests/ui/fail/annot_mut_term.rs
+++ b/tests/ui/fail/annot_mut_term.rs
@@ -1,7 +1,9 @@
 //@error-in-other-file: Unsat
 
-#[thrust::requires(true)]
-#[thrust::ensures(x == <*x, y>)]
+use thrust_models::model::Mut;
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(x == Mut::new(*x, y))]
 fn f(x: &mut i64, y: i64) {
     *x = y;
 }
diff --git a/tests/ui/fail/tuple_annot.rs b/tests/ui/fail/tuple_annot.rs
index 9e5c4e1..f283236 100644
--- a/tests/ui/fail/tuple_annot.rs
+++ b/tests/ui/fail/tuple_annot.rs
@@ -1,8 +1,8 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(true)]
-#[thrust::ensures(^x == ((*x).1, (*x).1))]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(!x == ((*x).1, (*x).1))]
 fn swap_tuple(x: &mut (i32, i32)) {
     let v = *x;
     *x = (v.1, v.0);
diff --git a/tests/ui/pass/annot_enum_simple.rs b/tests/ui/pass/annot_enum_simple.rs
index 70eed4c..9ed6184 100644
--- a/tests/ui/pass/annot_enum_simple.rs
+++ b/tests/ui/pass/annot_enum_simple.rs
@@ -1,12 +1,17 @@
 //@check-pass
 
+#[derive(PartialEq)]
 pub enum X {
     A(i64),
     B(bool),
 }
 
-#[thrust::requires(x == X::A(1))]
-#[thrust::ensures(true)]
+impl thrust_models::Model for X {
+    type Ty = X;
+}
+
+#[thrust_macros::requires(x == X::A(1))]
+#[thrust_macros::ensures(true)]
 fn test(x: X) {
     if let X::A(i) = x {
         assert!(i == 1);
diff --git a/tests/ui/pass/annot_exists.rs b/tests/ui/pass/annot_exists.rs
index 1496c7f..3ab0003 100644
--- a/tests/ui/pass/annot_exists.rs
+++ b/tests/ui/pass/annot_exists.rs
@@ -2,12 +2,14 @@
 //@compile-flags: -C debug-assertions=off
 //@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
 
+use thrust_models::exists;
+
 #[thrust::trusted]
 #[thrust::callable]
 fn rand() -> i32 { unimplemented!() }
 
-#[thrust::requires(true)]
-#[thrust::ensures(exists x:int. result == 2 * x)]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(exists(|x: i32| result == 2 * x))]
 fn f() -> i32 {
     let x = rand();
     x + x
diff --git a/tests/ui/pass/annot_mut_term.rs b/tests/ui/pass/annot_mut_term.rs
index 172a1df..60aa17c 100644
--- a/tests/ui/pass/annot_mut_term.rs
+++ b/tests/ui/pass/annot_mut_term.rs
@@ -1,7 +1,9 @@
 //@check-pass
 
-#[thrust::requires(true)]
-#[thrust::ensures(x == <*x, y>)]
+use thrust_models::model::Mut;
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(x == Mut::new(*x, y))]
 fn f(x: &mut i64, y: i64) {
     *x = y;
 }
diff --git a/tests/ui/pass/tuple_annot.rs b/tests/ui/pass/tuple_annot.rs
index 530706f..4ab7274 100644
--- a/tests/ui/pass/tuple_annot.rs
+++ b/tests/ui/pass/tuple_annot.rs
@@ -1,8 +1,8 @@
 //@check-pass
 //@compile-flags: -C debug-assertions=off
 
-#[thrust::requires(true)]
-#[thrust::ensures(^x == ((*x).1, (*x).0))]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(!x == ((*x).1, (*x).0))]
 fn swap_tuple(x: &mut (i32, i32)) {
     let v = *x;
     *x = (v.1, v.0);
diff --git a/thrust-macros/Cargo.lock b/thrust-macros/Cargo.lock
new file mode 100644
index 0000000..b4a86db
--- /dev/null
+++ b/thrust-macros/Cargo.lock
@@ -0,0 +1,47 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.79"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e835ff2298f5721608eb1a980ecaee1aef2c132bf95ecc026a11b7bf3c01c02e"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.36"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.55"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "002a1b3dbf967edfafc32655d0f377ab0bb7b994aa1d32c8cc7e9b8bf3ebb8f0"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "thrust-macros"
+version = "0.1.0"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
diff --git a/thrust-macros/Cargo.toml b/thrust-macros/Cargo.toml
new file mode 100644
index 0000000..4858a70
--- /dev/null
+++ b/thrust-macros/Cargo.toml
@@ -0,0 +1,13 @@
+[package]
+name = "thrust-macros"
+version = "0.1.0"
+authors = ["coord_e <me@coord-e.com>"]
+edition = "2021"
+
+[lib]
+proc-macro = true
+
+[dependencies]
+proc-macro2 = "1"
+quote = "1"
+syn = { version = "2", features = ["full"] }
diff --git a/thrust-macros/src/lib.rs b/thrust-macros/src/lib.rs
new file mode 100644
index 0000000..e114453
--- /dev/null
+++ b/thrust-macros/src/lib.rs
@@ -0,0 +1,388 @@
+use proc_macro::TokenStream;
+use proc_macro2::TokenStream as TokenStream2;
+use quote::{format_ident, quote, ToTokens};
+use syn::{
+    parse_macro_input, punctuated::Punctuated, FnArg, GenericParam, Generics, ItemFn, Pat,
+    ReturnType, Type, TypeParamBound, WherePredicate,
+};
+
+#[proc_macro_attribute]
+pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let expr = TokenStream2::from(attr);
+    let mut func = parse_macro_input!(item as ItemFn);
+
+    let (req_expr, ens_expr) = match extract_requires_ensures(&mut func) {
+        Ok((req, ens)) => (req, ens),
+        Err(e) => return e.to_compile_error().into(),
+    };
+    func.attrs.push(syn::parse_quote!(
+        #[::thrust_macros::_requires_ensures(#req_expr && #expr, #ens_expr)]
+    ));
+
+    func.into_token_stream().into()
+}
+
+#[proc_macro_attribute]
+pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let expr = TokenStream2::from(attr);
+    let mut func = parse_macro_input!(item as ItemFn);
+
+    let (req_expr, ens_expr) = match extract_requires_ensures(&mut func) {
+        Ok((req, ens)) => (req, ens),
+        Err(e) => return e.to_compile_error().into(),
+    };
+    func.attrs.push(syn::parse_quote!(
+        #[::thrust_macros::_requires_ensures(#req_expr, #ens_expr && #expr)]
+    ));
+
+    func.into_token_stream().into()
+}
+
+fn extract_requires_ensures(func: &mut ItemFn) -> syn::Result<(syn::Expr, syn::Expr)> {
+    let mut result = None;
+
+    let requires_ensures_path: syn::Path = syn::parse_quote!(::thrust_macros::_requires_ensures);
+
+    for attr in &func.attrs {
+        if attr.path() == &requires_ensures_path {
+            if result.is_some() {
+                return Err(syn::Error::new_spanned(
+                    attr,
+                    "multiple _requires_ensures attributes found; expected at most one",
+                ));
+            }
+
+            let parser = Punctuated::<syn::Expr, syn::Token![,]>::parse_separated_nonempty;
+            let mut exprs = attr.parse_args_with(parser)?;
+            if exprs.len() != 2 {
+                return Err(syn::Error::new_spanned(
+                    attr,
+                    "expected exactly two comma-separated expressions in _requires_ensures attribute",
+                ));
+            }
+            let ens_expr = exprs.pop().unwrap().into_value();
+            let req_expr = exprs.pop().unwrap().into_value();
+            result = Some((req_expr, ens_expr));
+        }
+    }
+
+    func.attrs
+        .retain(|attr| attr.path() != &requires_ensures_path);
+
+    if let Some((req_expr, ens_expr)) = result {
+        Ok((req_expr, ens_expr))
+    } else {
+        Ok((syn::parse_quote!(true), syn::parse_quote!(true)))
+    }
+}
+
+#[proc_macro_attribute]
+pub fn _requires_ensures(attr: TokenStream, item: TokenStream) -> TokenStream {
+    use syn::parse::Parser as _;
+    let parser = Punctuated::<syn::Expr, syn::Token![,]>::parse_separated_nonempty;
+    let mut exprs = match parser.parse(attr.clone()) {
+        Ok(exprs) => exprs,
+        Err(e) => return e.to_compile_error().into(),
+    };
+    if exprs.len() != 2 {
+        return syn::Error::new_spanned(
+            TokenStream2::from(attr),
+            "expected exactly two comma-separated expressions in _requires_ensures attribute",
+        )
+        .to_compile_error()
+        .into();
+    }
+
+    let ens_expr = exprs.pop().unwrap().into_value();
+    let req_expr = exprs.pop().unwrap().into_value();
+
+    let func = parse_macro_input!(item as ItemFn);
+    ExpandedTokens::new(func, req_expr, ens_expr)
+        .into_token_stream()
+        .into()
+}
+
+struct ExpandedTokens {
+    func: ItemFn,
+
+    requires_name: syn::Ident,
+    ensures_name: syn::Ident,
+    req_expr: syn::Expr,
+    ens_expr: syn::Expr,
+
+    def_generics: TokenStream2,
+    turbofish: TokenStream2,
+    extended_where: TokenStream2,
+
+    model_ty_params: TokenStream2,
+    ret_model_ty: Type,
+}
+
+impl quote::ToTokens for ExpandedTokens {
+    fn to_tokens(&self, tokens: &mut TokenStream2) {
+        if self.is_extern_spec_fn() {
+            self.expand_extern_spec_fn().to_tokens(tokens);
+        } else {
+            self.expand().to_tokens(tokens);
+        }
+    }
+}
+
+impl ExpandedTokens {
+    pub fn new(func: ItemFn, req_expr: syn::Expr, ens_expr: syn::Expr) -> Self {
+        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);
+
+        let model_ty_params = fn_params_with_model_ty(&func.sig.inputs);
+        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),
+        };
+
+        Self {
+            func,
+            req_expr,
+            ens_expr,
+            requires_name,
+            ensures_name,
+            def_generics,
+            turbofish,
+            extended_where,
+            model_ty_params,
+            ret_model_ty,
+        }
+    }
+
+    fn is_extern_spec_fn(&self) -> bool {
+        let extern_spec_fn_path: syn::Path = syn::parse_quote!(thrust::extern_spec_fn);
+        self.func
+            .attrs
+            .iter()
+            .any(|a| a.path() == &extern_spec_fn_path)
+    }
+
+    fn requires_fn(&self) -> TokenStream2 {
+        let requires_name = &self.requires_name;
+        let def_generics = &self.def_generics;
+        let model_ty_params = &self.model_ty_params;
+        let extended_where = &self.extended_where;
+        let req_expr = &self.req_expr;
+
+        quote! {
+            #[allow(unused_variables)]
+            #[allow(non_snake_case)]
+            #[thrust::formula_fn]
+            fn #requires_name #def_generics(#model_ty_params) -> bool #extended_where {
+                #req_expr
+            }
+        }
+    }
+
+    fn ensures_fn(&self) -> TokenStream2 {
+        let ensures_name = &self.ensures_name;
+        let def_generics = &self.def_generics;
+        let model_ty_params = &self.model_ty_params;
+        let extended_where = &self.extended_where;
+        let ret_model_ty = &self.ret_model_ty;
+        let ens_expr = &self.ens_expr;
+
+        quote! {
+            #[allow(unused_variables)]
+            #[allow(non_snake_case)]
+            #[thrust::formula_fn]
+            fn #ensures_name #def_generics(result: #ret_model_ty, #model_ty_params) -> bool #extended_where {
+                #ens_expr
+            }
+        }
+    }
+
+    fn expand(&self) -> TokenStream2 {
+        let mut func = self.func.clone();
+        let trusted_path: syn::Path = syn::parse_quote!(thrust::trusted);
+        for attr in &mut func.attrs {
+            if attr.path() == &trusted_path {
+                *attr = syn::parse_quote!(#[thrust::ignored]);
+            }
+        }
+
+        let requires_fn = self.requires_fn();
+        let ensures_fn = self.ensures_fn();
+
+        let extern_spec_name = format_ident!("_thrust_extern_spec_{}", self.func.sig.ident);
+        let def_generics = &self.def_generics;
+        let orig_inputs = &self.func.sig.inputs;
+        let orig_output = &self.func.sig.output;
+        let extended_where = &self.extended_where;
+
+        let requires_name = &self.requires_name;
+        let ensures_name = &self.ensures_name;
+        let turbofish = &self.turbofish;
+
+        let name = &self.func.sig.ident;
+        let call_args = fn_arg_idents(&self.func.sig.inputs);
+
+        quote! {
+            #func
+
+            #requires_fn
+            #ensures_fn
+
+            #[thrust::extern_spec_fn]
+            #[allow(path_statements)]
+            fn #extern_spec_name #def_generics(#orig_inputs) #orig_output #extended_where {
+                #[thrust::requires_path]
+                #requires_name #turbofish;
+
+                #[thrust::ensures_path]
+                #ensures_name #turbofish;
+
+                #name #turbofish(#call_args)
+            }
+        }
+    }
+
+    fn expand_extern_spec_fn(&self) -> TokenStream2 {
+        let requires_name = &self.requires_name;
+        let ensures_name = &self.ensures_name;
+        let turbofish = &self.turbofish;
+
+        let mut func = self.func.clone();
+        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 requires_fn = self.requires_fn();
+        let ensures_fn = self.ensures_fn();
+
+        quote! {
+            #requires_fn
+            #ensures_fn
+
+            #[allow(path_statements)]
+            #func
+        }
+    }
+}
+
+/// Returns `<T: Bound, U, 'a>` — the generic param list for function definitions,
+/// without a where clause.
+fn generic_params_tokens(generics: &Generics) -> TokenStream2 {
+    if generics.params.is_empty() {
+        return quote!();
+    }
+    let params = &generics.params;
+    quote!(<#params>)
+}
+
+/// Returns `::<T, U, 'a>` for turbofish use, or nothing if no generic params.
+fn generic_turbofish(generics: &Generics) -> TokenStream2 {
+    if generics.params.is_empty() {
+        return quote!();
+    }
+    let args: Vec<TokenStream2> = generics
+        .params
+        .iter()
+        .map(|p| match p {
+            GenericParam::Type(tp) => tp.ident.to_token_stream(),
+            GenericParam::Lifetime(lp) => lp.lifetime.to_token_stream(),
+            GenericParam::Const(cp) => cp.ident.to_token_stream(),
+        })
+        .collect();
+    quote!(::<#(#args),*>)
+}
+
+/// Returns `T: thrust_models::Model` predicates for every type param that does not
+/// already carry an `Fn`, `FnOnce`, or `FnMut` bound.
+fn model_where_predicates(generics: &Generics) -> Vec<WherePredicate> {
+    generics
+        .params
+        .iter()
+        .flat_map(|p| {
+            let GenericParam::Type(tp) = p else {
+                return vec![];
+            };
+            let has_fn_bound = tp.bounds.iter().any(|b| {
+                let TypeParamBound::Trait(tb) = b else {
+                    return false;
+                };
+                tb.path.segments.last().map_or(false, |s| {
+                    matches!(s.ident.to_string().as_str(), "Fn" | "FnOnce" | "FnMut")
+                })
+            });
+            if has_fn_bound {
+                return vec![];
+            }
+            let ident = &tp.ident;
+            vec![
+                syn::parse_quote!(#ident: thrust_models::Model),
+                syn::parse_quote!(<#ident as thrust_models::Model>::Ty: PartialEq),
+            ]
+        })
+        .collect()
+}
+
+/// Builds `where <original predicates>, <model predicates>`.
+/// Returns an empty token stream when both sets are empty.
+fn extended_where_clause(generics: &Generics, model_preds: &[WherePredicate]) -> TokenStream2 {
+    let existing: Vec<&WherePredicate> = generics
+        .where_clause
+        .as_ref()
+        .map(|wc| wc.predicates.iter().collect())
+        .unwrap_or_default();
+
+    if existing.is_empty() && model_preds.is_empty() {
+        return quote!();
+    }
+
+    quote! { where #(#existing,)* #(#model_preds),* }
+}
+
+/// Maps each typed function parameter `x: T` to `x: <T as thrust_models::Model>::Ty`.
+/// Receiver (`self`) parameters are skipped.
+fn fn_params_with_model_ty(
+    inputs: &syn::punctuated::Punctuated<FnArg, syn::token::Comma>,
+) -> TokenStream2 {
+    let params: Vec<TokenStream2> = inputs
+        .iter()
+        .filter_map(|arg| {
+            let FnArg::Typed(pt) = arg else { return None };
+            let pat = &pt.pat;
+            let ty = &pt.ty;
+            let model_ty: Type = syn::parse_quote!(<#ty as thrust_models::Model>::Ty);
+            Some(quote!(#pat: #model_ty))
+        })
+        .collect();
+    quote!(#(#params),*)
+}
+
+/// Extracts argument identifiers from function parameters for use in a call expression.
+fn fn_arg_idents(inputs: &syn::punctuated::Punctuated<FnArg, syn::token::Comma>) -> TokenStream2 {
+    let args: Vec<TokenStream2> = inputs
+        .iter()
+        .filter_map(|arg| match arg {
+            FnArg::Typed(pt) => {
+                if let Pat::Ident(pi) = &*pt.pat {
+                    Some(pi.ident.to_token_stream())
+                } else {
+                    None
+                }
+            }
+            FnArg::Receiver(_) => Some(quote!(self)),
+        })
+        .collect();
+    quote!(#(#args),*)
+}