From 077527d93984f24263d54dc10f84612eb58a3500 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 8 Jun 2026 17:03:57 +0000
Subject: [PATCH 1/4] Support Rust syntax in thrust::predicate bodies

Predicate bodies can now be written as ordinary Rust boolean expressions
instead of raw SMT-LIB2 string literals, reusing the formula_fn translation
pipeline (AnnotFnTranslator).

A predicate whose body is a Rust expression is emitted by the
thrust_macros::predicate proc macro with an additional #[thrust::formula_fn]
attribute; that attribute is the discriminator. When present, the body is
translated through the existing formula_fns cache and the resulting
chc::Formula is emitted as the predicate's SMT define-fun. Raw SMT2 string
bodies continue to work unchanged.

- chc: UserDefinedPredDef gains a UserDefinedPredBody { Raw, Formula } enum
  plus push_pred_define_formula; smtlib2 renders a Formula body via a
  synthetic Clause; unbox unboxes Formula bodies.
- analyze: register predicate items marked formula_fn; define_as_predicate
  pulls the translated formula from formula_fn_with_args and names params
  v{i} to match TermVarIdx rendering.
- annot_fn: ExprKind::Field resolves named ADT fields (e.g. self.x) to tuple
  projection indices, enabling struct predicates in trait impls.
- macro: detect raw-vs-Rust body, rewrite self->self_, add allow attrs.
- tests: paired pass/fail ui tests for free-function and trait predicates.

https://claude.ai/code/session_01WdLyxyy4ieAxrexj83X5MX
---
 src/analyze/annot_fn.rs                       | 21 +++++--
 src/analyze/crate_.rs                         | 12 +++-
 src/analyze/local_def.rs                      | 40 +++++++++++--
 src/chc.rs                                    | 33 ++++++++++-
 src/chc/smtlib2.rs                            | 28 ++++++++-
 src/chc/unbox.rs                              |  6 ++
 tests/ui/fail/annot_preds_rust_syntax.rs      | 19 ++++++
 .../ui/fail/annot_preds_trait_rust_syntax.rs  | 45 ++++++++++++++
 tests/ui/pass/annot_preds_rust_syntax.rs      | 19 ++++++
 .../ui/pass/annot_preds_trait_rust_syntax.rs  | 45 ++++++++++++++
 thrust-macros/src/spec.rs                     | 58 ++++++++++++++++---
 11 files changed, 300 insertions(+), 26 deletions(-)
 create mode 100644 tests/ui/fail/annot_preds_rust_syntax.rs
 create mode 100644 tests/ui/fail/annot_preds_trait_rust_syntax.rs
 create mode 100644 tests/ui/pass/annot_preds_rust_syntax.rs
 create mode 100644 tests/ui/pass/annot_preds_trait_rust_syntax.rs

diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs
index 9e418169..10e65112 100644
--- a/src/analyze/annot_fn.rs
+++ b/src/analyze/annot_fn.rs
@@ -529,11 +529,22 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                 FormulaOrTerm::Term(chc::Term::tuple(terms))
             }
             ExprKind::Field(expr, field) => {
-                let index = field
-                    .name
-                    .as_str()
-                    .parse::<usize>()
-                    .expect("tuple field index must be a non-negative integer");
+                // Tuples use numeric field names (`.0`); structs (represented as
+                // tuples in the logic) use named fields resolved to their position.
+                let index = match field.name.as_str().parse::<usize>() {
+                    Ok(index) => index,
+                    Err(_) => {
+                        let adt = self
+                            .expr_ty(expr)
+                            .ty_adt_def()
+                            .expect("named field access on a non-ADT type");
+                        adt.non_enum_variant()
+                            .fields
+                            .iter()
+                            .position(|f| f.name == field.name)
+                            .expect("unknown named field in formula")
+                    }
+                };
                 let term = self.to_term(expr);
                 FormulaOrTerm::Term(term.tuple_proj(index))
             }
diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs
index 74198f18..16016814 100644
--- a/src/analyze/crate_.rs
+++ b/src/analyze/crate_.rs
@@ -89,7 +89,17 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         }
 
         if analyzer.is_annotated_as_predicate() {
-            analyzer.analyze_predicate_definition();
+            // A predicate whose body is a Rust expression is also marked
+            // `formula_fn`; register it first so `analyze_predicate_definition`
+            // can pull the translated formula via `formula_fn_with_args`.
+            let is_formula_fn = analyzer.is_annotated_as_formula_fn();
+            drop(analyzer);
+            if is_formula_fn {
+                self.ctx.register_formula_fn(local_def_id);
+            }
+            self.ctx
+                .local_def_analyzer(local_def_id)
+                .analyze_predicate_definition();
             self.skip_analysis.insert(local_def_id);
             return;
         }
diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs
index 83559a11..bc93e861 100644
--- a/src/analyze/local_def.rs
+++ b/src/analyze/local_def.rs
@@ -136,6 +136,40 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     }
 
     fn define_as_predicate(&self, pred: chc::UserDefinedPred) {
+        let sig = self.ctx.fn_sig(self.local_def_id.to_def_id());
+        let arg_sorts = sig
+            .inputs()
+            .iter()
+            .map(|input_ty| self.type_builder.build(*input_ty).to_sort());
+
+        // A predicate marked `formula_fn` carries a Rust-expression body that has
+        // been translated into a `chc::Formula`; otherwise the body is a raw
+        // SMT-LIB2 string literal.
+        if self.is_annotated_as_formula_fn() {
+            // Name the parameters `v{i}` to match how `chc::TermVarIdx` renders the
+            // formula's variables (see `chc::UserDefinedPredBody::Formula`).
+            let arg_name_and_sorts = arg_sorts
+                .enumerate()
+                .map(|(i, sort)| (format!("v{i}"), sort))
+                .collect::<Vec<_>>();
+
+            let formula_fn = self
+                .ctx
+                .formula_fn_with_args(self.local_def_id, self.tcx.mk_args(&[]))
+                .expect("predicate formula function is not registered");
+            let formula = formula_fn
+                .formula()
+                .clone()
+                .map_var(|idx| chc::TermVarIdx::from(idx.index()));
+
+            self.ctx.system.borrow_mut().push_pred_define_formula(
+                pred,
+                chc::UserDefinedPredSig::from(arg_name_and_sorts),
+                formula,
+            );
+            return;
+        }
+
         // function's body
         use rustc_hir::{Block, Expr, ExprKind};
 
@@ -164,12 +198,6 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                     .to_string()
             });
 
-        let sig = self.ctx.fn_sig(self.local_def_id.to_def_id());
-        let arg_sorts = sig
-            .inputs()
-            .iter()
-            .map(|input_ty| self.type_builder.build(*input_ty).to_sort());
-
         let arg_name_and_sorts = arg_names.into_iter().zip(arg_sorts).collect::<Vec<_>>();
 
         self.ctx.system.borrow_mut().push_pred_define(
diff --git a/src/chc.rs b/src/chc.rs
index 58166391..8f8de32d 100644
--- a/src/chc.rs
+++ b/src/chc.rs
@@ -1768,11 +1768,22 @@ pub struct PredVarDef {
 
 pub type UserDefinedPredSig = Vec<(String, Sort)>;
 
+/// The body of a user-defined predicate.
+///
+/// A predicate can be defined either by a raw SMT-LIB2 string (inserted into the
+/// generated `define-fun` verbatim) or by a [`Formula`] translated from a Rust
+/// expression via the `formula_fn` infrastructure.
+#[derive(Debug, Clone)]
+pub enum UserDefinedPredBody {
+    Raw(String),
+    Formula(Formula<TermVarIdx>),
+}
+
 #[derive(Debug, Clone)]
 pub struct UserDefinedPredDef {
     symbol: UserDefinedPred,
     sig: UserDefinedPredSig,
-    body: String,
+    body: UserDefinedPredBody,
 }
 
 /// A CHC system.
@@ -1800,8 +1811,24 @@ impl System {
         sig: UserDefinedPredSig,
         body: String,
     ) {
-        self.user_defined_pred_defs
-            .push(UserDefinedPredDef { symbol, sig, body })
+        self.user_defined_pred_defs.push(UserDefinedPredDef {
+            symbol,
+            sig,
+            body: UserDefinedPredBody::Raw(body),
+        })
+    }
+
+    pub fn push_pred_define_formula(
+        &mut self,
+        symbol: UserDefinedPred,
+        sig: UserDefinedPredSig,
+        formula: Formula<TermVarIdx>,
+    ) {
+        self.user_defined_pred_defs.push(UserDefinedPredDef {
+            symbol,
+            sig,
+            body: UserDefinedPredBody::Formula(formula),
+        })
     }
 
     pub fn push_clause(&mut self, clause: Clause) -> Option<ClauseId> {
diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs
index e8886ed6..5103b35c 100644
--- a/src/chc/smtlib2.rs
+++ b/src/chc/smtlib2.rs
@@ -577,10 +577,32 @@ impl<'ctx, 'a> std::fmt::Display for UserDefinedPredDef<'ctx, 'a> {
         );
         write!(
             f,
-            "(define-fun {name} {params} Bool {body})",
+            "(define-fun {name} {params} Bool ",
             name = self.inner.symbol,
-            body = &self.inner.body,
-        )
+        )?;
+        match &self.inner.body {
+            chc::UserDefinedPredBody::Raw(body) => write!(f, "{body}")?,
+            chc::UserDefinedPredBody::Formula(formula) => {
+                // Term display needs a `Clause` to resolve sorts (for box/mut/tuple
+                // constructors); build a synthetic one whose `vars` are the
+                // predicate's parameter sorts in order. The formula's `Var(v{i})`
+                // and the `(v{i} Sort)` parameter list above both render via
+                // `TermVarIdx`, so they line up by index.
+                let clause = chc::Clause {
+                    vars: self
+                        .inner
+                        .sig
+                        .iter()
+                        .map(|(_, sort)| sort.clone())
+                        .collect(),
+                    head: chc::Atom::top(),
+                    body: chc::Body::default(),
+                    debug_info: chc::DebugInfo::default(),
+                };
+                write!(f, "{}", Formula::new(self.ctx, &clause, formula))?;
+            }
+        }
+        write!(f, ")")
     }
 }
 
diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs
index b3b24d52..f95889be 100644
--- a/src/chc/unbox.rs
+++ b/src/chc/unbox.rs
@@ -159,6 +159,12 @@ fn unbox_user_defined_pred_def(user_defined_pred_def: UserDefinedPredDef) -> Use
         .into_iter()
         .map(|(name, sort)| (name, unbox_sort(sort)))
         .collect();
+    let body = match body {
+        UserDefinedPredBody::Raw(s) => UserDefinedPredBody::Raw(s),
+        UserDefinedPredBody::Formula(formula) => {
+            UserDefinedPredBody::Formula(unbox_formula(formula))
+        }
+    };
     UserDefinedPredDef { symbol, sig, body }
 }
 
diff --git a/tests/ui/fail/annot_preds_rust_syntax.rs b/tests/ui/fail/annot_preds_rust_syntax.rs
new file mode 100644
index 00000000..646a4a97
--- /dev/null
+++ b/tests/ui/fail/annot_preds_rust_syntax.rs
@@ -0,0 +1,19 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -Adead_code -C debug-assertions=off
+
+// Predicate body written in Rust syntax instead of raw SMT-LIB2.
+#[thrust_macros::predicate]
+fn is_double(x: i64, doubled_x: i64) -> bool {
+    x * 2 == doubled_x
+}
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(is_double(x, result))]
+fn double(x: i64) -> i64 {
+    x + x + x
+}
+
+fn main() {
+    let a = 3;
+    assert!(double(a) == 9);
+}
diff --git a/tests/ui/fail/annot_preds_trait_rust_syntax.rs b/tests/ui/fail/annot_preds_trait_rust_syntax.rs
new file mode 100644
index 00000000..eeae01a3
--- /dev/null
+++ b/tests/ui/fail/annot_preds_trait_rust_syntax.rs
@@ -0,0 +1,45 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -Adead_code -C debug-assertions=off
+
+// A is represented as Tuple<Int> in SMT-LIB2 format.
+#[derive(PartialEq)]
+struct A {
+    x: i64,
+}
+
+impl thrust_models::Model for A {
+    type Ty = Self;
+}
+
+#[thrust_macros::context]
+trait Double {
+    // Support annotations in trait definitions
+    #[thrust_macros::predicate]
+    fn is_double(self, doubled: Self) -> bool;
+
+    // This annotations are applied to all implementors of the `Double` trait.
+    #[thrust_macros::requires(true)]
+    #[thrust_macros::ensures(Self::is_double(*self, !self))]
+    fn double(&mut self);
+}
+
+#[thrust_macros::context]
+impl Double for A {
+    // self.x * 3 (this isn't actually doubled!) does not comply with the trait.
+    #[thrust_macros::predicate]
+    fn is_double(self, doubled: Self) -> bool {
+        self.x * 3 == doubled.x
+    }
+
+    // Check if this method complies with annotations in
+    // trait definition.
+    fn double(&mut self) {
+        self.x += self.x;
+    }
+}
+
+fn main() {
+    let mut a = A { x: 3 };
+    a.double();
+    assert!(a.x == 6);
+}
diff --git a/tests/ui/pass/annot_preds_rust_syntax.rs b/tests/ui/pass/annot_preds_rust_syntax.rs
new file mode 100644
index 00000000..cd89d74e
--- /dev/null
+++ b/tests/ui/pass/annot_preds_rust_syntax.rs
@@ -0,0 +1,19 @@
+//@check-pass
+//@compile-flags: -Adead_code -C debug-assertions=off
+
+// Predicate body written in Rust syntax instead of raw SMT-LIB2.
+#[thrust_macros::predicate]
+fn is_double(x: i64, doubled_x: i64) -> bool {
+    x * 2 == doubled_x
+}
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(is_double(x, result))]
+fn double(x: i64) -> i64 {
+    x + x
+}
+
+fn main() {
+    let a = 3;
+    assert!(double(a) == 6);
+}
diff --git a/tests/ui/pass/annot_preds_trait_rust_syntax.rs b/tests/ui/pass/annot_preds_trait_rust_syntax.rs
new file mode 100644
index 00000000..0b915ea5
--- /dev/null
+++ b/tests/ui/pass/annot_preds_trait_rust_syntax.rs
@@ -0,0 +1,45 @@
+//@check-pass
+//@compile-flags: -Adead_code -C debug-assertions=off
+
+// A is represented as Tuple<Int> in SMT-LIB2 format.
+#[derive(PartialEq)]
+struct A {
+    x: i64,
+}
+
+impl thrust_models::Model for A {
+    type Ty = Self;
+}
+
+#[thrust_macros::context]
+trait Double {
+    // Support annotations in trait definitions
+    #[thrust_macros::predicate]
+    fn is_double(self, doubled: Self) -> bool;
+
+    // This annotations are applied to all implementors of the `Double` trait.
+    #[thrust_macros::requires(true)]
+    #[thrust_macros::ensures(Self::is_double(*self, !self))]
+    fn double(&mut self);
+}
+
+#[thrust_macros::context]
+impl Double for A {
+    // Write concrete definitions for predicates in `impl` blocks, in Rust syntax.
+    #[thrust_macros::predicate]
+    fn is_double(self, doubled: Self) -> bool {
+        self.x * 2 == doubled.x
+    }
+
+    // Check if this method complies with annotations in
+    // trait definition.
+    fn double(&mut self) {
+        self.x += self.x;
+    }
+}
+
+fn main() {
+    let mut a = A { x: 3 };
+    a.double();
+    assert!(a.x == 6);
+}
diff --git a/thrust-macros/src/spec.rs b/thrust-macros/src/spec.rs
index 943087de..e8cc7e6d 100644
--- a/thrust-macros/src/spec.rs
+++ b/thrust-macros/src/spec.rs
@@ -38,18 +38,55 @@ pub fn expand_predicate(item: TokenStream) -> TokenStream {
     let model_preds = type_lowering.model_where_predicates();
     let extended_where = extended_where_clause(&func, &model_preds);
 
+    // A predicate body written as a Rust expression is translated through the
+    // `formula_fn` pipeline; a raw SMT-LIB2 string-literal body is not.
+    let is_rust_body = func.block().is_some_and(|block| !is_raw_smt2_body(block));
+    let formula_fn_attr = if is_rust_body {
+        quote! {
+            #[thrust::formula_fn]
+            #[allow(unused_variables)]
+            #[allow(non_snake_case)]
+        }
+    } else {
+        quote!()
+    };
+
     let sig = quote! {
         #[allow(dead_code)]
+        #formula_fn_attr
         #[thrust::predicate]
         fn #name #def_generics(#model_ty_params) -> #model_ret #extended_where
     };
     if let Some(block) = func.block() {
+        let mut block = block.clone();
+        // The receiver `self` is lowered to a named `self_` parameter, so rewrite
+        // references in the (Rust) body to match.
+        if is_rust_body {
+            rewrite_self_in_block(&mut block);
+        }
         quote! { #sig #block }.into()
     } else {
         quote! { #sig; }.into()
     }
 }
 
+/// Whether a predicate body is a raw SMT-LIB2 definition, i.e. it contains a
+/// string-literal statement such as `"(= ..)"; true`.
+fn is_raw_smt2_body(block: &syn::Block) -> bool {
+    block.stmts.iter().any(|stmt| {
+        matches!(
+            stmt,
+            syn::Stmt::Expr(
+                syn::Expr::Lit(syn::ExprLit {
+                    lit: syn::Lit::Str(_),
+                    ..
+                }),
+                _,
+            )
+        )
+    })
+}
+
 pub fn expand_requires(attr: TokenStream, item: TokenStream) -> TokenStream {
     let expr = TokenStream2::from(attr);
     let mut func = parse_macro_input!(item as FnItemWithSignature);
@@ -480,19 +517,24 @@ fn mentions_self(sig: &syn::Signature) -> bool {
     visitor.mentions_self
 }
 
-fn rewrite_self_in_expr(expr: &mut syn::Expr) {
-    struct Visitor;
+struct RewriteSelf;
 
-    impl syn::visit_mut::VisitMut for Visitor {
-        fn visit_ident_mut(&mut self, ident: &mut syn::Ident) {
-            if ident == "self" {
-                *ident = format_ident!("self_");
-            }
+impl syn::visit_mut::VisitMut for RewriteSelf {
+    fn visit_ident_mut(&mut self, ident: &mut syn::Ident) {
+        if ident == "self" {
+            *ident = format_ident!("self_");
         }
     }
+}
+
+fn rewrite_self_in_expr(expr: &mut syn::Expr) {
+    use syn::visit_mut::VisitMut as _;
+    RewriteSelf.visit_expr_mut(expr);
+}
 
+fn rewrite_self_in_block(block: &mut syn::Block) {
     use syn::visit_mut::VisitMut as _;
-    Visitor.visit_expr_mut(expr);
+    RewriteSelf.visit_block_mut(block);
 }
 
 /// Returns `<T: Bound, U, 'a>` — the generic param list for function definitions,

From 3bddcdc7d20a4853ac5d89b56b37d7fa89db72c1 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 9 Jun 2026 14:48:00 +0000
Subject: [PATCH 2/4] Convert raw-SMT2 predicate tests to Rust syntax

Rewrite the existing predicate ui tests (annot_preds, annot_preds_trait,
annot_preds_trait_multi; pass and fail) to use the new Rust-expression
predicate bodies instead of raw SMT-LIB2 string literals, and drop the
now-redundant *_rust_syntax duplicate tests added earlier.

https://claude.ai/code/session_01WdLyxyy4ieAxrexj83X5MX
---
 tests/ui/fail/annot_preds.rs                  |  9 ++--
 tests/ui/fail/annot_preds_rust_syntax.rs      | 19 --------
 tests/ui/fail/annot_preds_trait.rs            |  9 +---
 tests/ui/fail/annot_preds_trait_multi.rs      | 19 ++------
 .../ui/fail/annot_preds_trait_rust_syntax.rs  | 45 -------------------
 tests/ui/pass/annot_preds.rs                  |  9 ++--
 tests/ui/pass/annot_preds_rust_syntax.rs      | 19 --------
 tests/ui/pass/annot_preds_trait.rs            |  9 +---
 tests/ui/pass/annot_preds_trait_multi.rs      | 18 +-------
 .../ui/pass/annot_preds_trait_rust_syntax.rs  | 45 -------------------
 10 files changed, 15 insertions(+), 186 deletions(-)
 delete mode 100644 tests/ui/fail/annot_preds_rust_syntax.rs
 delete mode 100644 tests/ui/fail/annot_preds_trait_rust_syntax.rs
 delete mode 100644 tests/ui/pass/annot_preds_rust_syntax.rs
 delete mode 100644 tests/ui/pass/annot_preds_trait_rust_syntax.rs

diff --git a/tests/ui/fail/annot_preds.rs b/tests/ui/fail/annot_preds.rs
index 725e23ba..3a0db5fa 100644
--- a/tests/ui/fail/annot_preds.rs
+++ b/tests/ui/fail/annot_preds.rs
@@ -1,12 +1,9 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -Adead_code -C debug-assertions=off
 
-#[thrust::predicate]
-fn is_double(x: thrust_models::model::Int, doubled_x: thrust_models::model::Int) -> bool {
-    "(=
-        (* x 2)
-        doubled_x
-    )"; true
+#[thrust_macros::predicate]
+fn is_double(x: i64, doubled_x: i64) -> bool {
+    x * 2 == doubled_x
 }
 
 #[thrust_macros::requires(true)]
diff --git a/tests/ui/fail/annot_preds_rust_syntax.rs b/tests/ui/fail/annot_preds_rust_syntax.rs
deleted file mode 100644
index 646a4a97..00000000
--- a/tests/ui/fail/annot_preds_rust_syntax.rs
+++ /dev/null
@@ -1,19 +0,0 @@
-//@error-in-other-file: Unsat
-//@compile-flags: -Adead_code -C debug-assertions=off
-
-// Predicate body written in Rust syntax instead of raw SMT-LIB2.
-#[thrust_macros::predicate]
-fn is_double(x: i64, doubled_x: i64) -> bool {
-    x * 2 == doubled_x
-}
-
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(is_double(x, result))]
-fn double(x: i64) -> i64 {
-    x + x + x
-}
-
-fn main() {
-    let a = 3;
-    assert!(double(a) == 9);
-}
diff --git a/tests/ui/fail/annot_preds_trait.rs b/tests/ui/fail/annot_preds_trait.rs
index d6e9a28f..eeae01a3 100644
--- a/tests/ui/fail/annot_preds_trait.rs
+++ b/tests/ui/fail/annot_preds_trait.rs
@@ -25,15 +25,10 @@ trait Double {
 
 #[thrust_macros::context]
 impl Double for A {
-    // Write concrete definitions for predicates in `impl` blocks
+    // self.x * 3 (this isn't actually doubled!) does not comply with the trait.
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // (tuple_proj<Int>.0 self) is equivalent to self.x
-        // self.x * 3 == doubled.x (this isn't actually doubled!) is written as following:
-        "(=
-            (* (tuple_proj<Int>.0 self_) 3)
-            (tuple_proj<Int>.0 doubled)
-        )"; true // This definition does not comply with annotations in trait!
+        self.x * 3 == doubled.x
     }
 
     // Check if this method complies with annotations in
diff --git a/tests/ui/fail/annot_preds_trait_multi.rs b/tests/ui/fail/annot_preds_trait_multi.rs
index b1156e50..1ffa1003 100644
--- a/tests/ui/fail/annot_preds_trait_multi.rs
+++ b/tests/ui/fail/annot_preds_trait_multi.rs
@@ -26,11 +26,7 @@ impl thrust_models::Model for A {
 impl Double for A {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 2 == doubled.x
-        "(=
-            (* (tuple_proj<Int>.0 self_) 2)
-            (tuple_proj<Int>.0 doubled)
-        )"; true
+        self.x * 2 == doubled.x
     }
 
     fn double(&mut self) {
@@ -50,19 +46,10 @@ impl thrust_models::Model for B {
 
 #[thrust_macros::context]
 impl Double for B {
+    // self.x * 3 (this isn't actually doubled!) does not comply with the trait.
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 3 == doubled.x && self.y * 2 == doubled.y (this isn't actually doubled!)
-        "(and
-            (=
-                (* (tuple_proj<Int-Int>.0 self_) 3)
-                (tuple_proj<Int-Int>.0 doubled)
-            )
-            (=
-                (* (tuple_proj<Int-Int>.1 self_) 2)
-                (tuple_proj<Int-Int>.1 doubled)
-            )
-        )"; true // This definition does not comply with annotations in trait!
+        self.x * 3 == doubled.x && self.y * 2 == doubled.y
     }
 
     fn double(&mut self) {
diff --git a/tests/ui/fail/annot_preds_trait_rust_syntax.rs b/tests/ui/fail/annot_preds_trait_rust_syntax.rs
deleted file mode 100644
index eeae01a3..00000000
--- a/tests/ui/fail/annot_preds_trait_rust_syntax.rs
+++ /dev/null
@@ -1,45 +0,0 @@
-//@error-in-other-file: Unsat
-//@compile-flags: -Adead_code -C debug-assertions=off
-
-// A is represented as Tuple<Int> in SMT-LIB2 format.
-#[derive(PartialEq)]
-struct A {
-    x: i64,
-}
-
-impl thrust_models::Model for A {
-    type Ty = Self;
-}
-
-#[thrust_macros::context]
-trait Double {
-    // Support annotations in trait definitions
-    #[thrust_macros::predicate]
-    fn is_double(self, doubled: Self) -> bool;
-
-    // This annotations are applied to all implementors of the `Double` trait.
-    #[thrust_macros::requires(true)]
-    #[thrust_macros::ensures(Self::is_double(*self, !self))]
-    fn double(&mut self);
-}
-
-#[thrust_macros::context]
-impl Double for A {
-    // self.x * 3 (this isn't actually doubled!) does not comply with the trait.
-    #[thrust_macros::predicate]
-    fn is_double(self, doubled: Self) -> bool {
-        self.x * 3 == doubled.x
-    }
-
-    // Check if this method complies with annotations in
-    // trait definition.
-    fn double(&mut self) {
-        self.x += self.x;
-    }
-}
-
-fn main() {
-    let mut a = A { x: 3 };
-    a.double();
-    assert!(a.x == 6);
-}
diff --git a/tests/ui/pass/annot_preds.rs b/tests/ui/pass/annot_preds.rs
index 516cb6ff..98b0e7d7 100644
--- a/tests/ui/pass/annot_preds.rs
+++ b/tests/ui/pass/annot_preds.rs
@@ -1,12 +1,9 @@
 //@check-pass
 //@compile-flags: -Adead_code -C debug-assertions=off
 
-#[thrust::predicate]
-fn is_double(x: thrust_models::model::Int, doubled_x: thrust_models::model::Int) -> bool {
-    "(=
-        (* x 2)
-        doubled_x
-    )"; true
+#[thrust_macros::predicate]
+fn is_double(x: i64, doubled_x: i64) -> bool {
+    x * 2 == doubled_x
 }
 
 #[thrust_macros::requires(true)]
diff --git a/tests/ui/pass/annot_preds_rust_syntax.rs b/tests/ui/pass/annot_preds_rust_syntax.rs
deleted file mode 100644
index cd89d74e..00000000
--- a/tests/ui/pass/annot_preds_rust_syntax.rs
+++ /dev/null
@@ -1,19 +0,0 @@
-//@check-pass
-//@compile-flags: -Adead_code -C debug-assertions=off
-
-// Predicate body written in Rust syntax instead of raw SMT-LIB2.
-#[thrust_macros::predicate]
-fn is_double(x: i64, doubled_x: i64) -> bool {
-    x * 2 == doubled_x
-}
-
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(is_double(x, result))]
-fn double(x: i64) -> i64 {
-    x + x
-}
-
-fn main() {
-    let a = 3;
-    assert!(double(a) == 6);
-}
diff --git a/tests/ui/pass/annot_preds_trait.rs b/tests/ui/pass/annot_preds_trait.rs
index 45f26ab6..0b915ea5 100644
--- a/tests/ui/pass/annot_preds_trait.rs
+++ b/tests/ui/pass/annot_preds_trait.rs
@@ -25,15 +25,10 @@ trait Double {
 
 #[thrust_macros::context]
 impl Double for A {
-    // Write concrete definitions for predicates in `impl` blocks
+    // Write concrete definitions for predicates in `impl` blocks, in Rust syntax.
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // (tuple_proj<Int>.0 self) is equivalent to self.x
-        // self.x * 2 == doubled.x is written as following:
-        "(=
-            (* (tuple_proj<Int>.0 self_) 2)
-            (tuple_proj<Int>.0 doubled)
-        )"; true
+        self.x * 2 == doubled.x
     }
 
     // Check if this method complies with annotations in
diff --git a/tests/ui/pass/annot_preds_trait_multi.rs b/tests/ui/pass/annot_preds_trait_multi.rs
index 326e5f01..dd8d9308 100644
--- a/tests/ui/pass/annot_preds_trait_multi.rs
+++ b/tests/ui/pass/annot_preds_trait_multi.rs
@@ -26,11 +26,7 @@ impl thrust_models::Model for A {
 impl Double for A {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 2 == doubled.x
-        "(=
-            (* (tuple_proj<Int>.0 self_) 2)
-            (tuple_proj<Int>.0 doubled)
-        )"; true
+        self.x * 2 == doubled.x
     }
 
     fn double(&mut self) {
@@ -52,17 +48,7 @@ impl thrust_models::Model for B {
 impl Double for B {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 2 == doubled.x && self.y * 2 == doubled.y
-        "(and
-            (=
-                (* (tuple_proj<Int-Int>.0 self_) 2)
-                (tuple_proj<Int-Int>.0 doubled)
-            )
-            (=
-                (* (tuple_proj<Int-Int>.1 self_) 2)
-                (tuple_proj<Int-Int>.1 doubled)
-            )
-        )"; true
+        self.x * 2 == doubled.x && self.y * 2 == doubled.y
     }
 
     fn double(&mut self) {
diff --git a/tests/ui/pass/annot_preds_trait_rust_syntax.rs b/tests/ui/pass/annot_preds_trait_rust_syntax.rs
deleted file mode 100644
index 0b915ea5..00000000
--- a/tests/ui/pass/annot_preds_trait_rust_syntax.rs
+++ /dev/null
@@ -1,45 +0,0 @@
-//@check-pass
-//@compile-flags: -Adead_code -C debug-assertions=off
-
-// A is represented as Tuple<Int> in SMT-LIB2 format.
-#[derive(PartialEq)]
-struct A {
-    x: i64,
-}
-
-impl thrust_models::Model for A {
-    type Ty = Self;
-}
-
-#[thrust_macros::context]
-trait Double {
-    // Support annotations in trait definitions
-    #[thrust_macros::predicate]
-    fn is_double(self, doubled: Self) -> bool;
-
-    // This annotations are applied to all implementors of the `Double` trait.
-    #[thrust_macros::requires(true)]
-    #[thrust_macros::ensures(Self::is_double(*self, !self))]
-    fn double(&mut self);
-}
-
-#[thrust_macros::context]
-impl Double for A {
-    // Write concrete definitions for predicates in `impl` blocks, in Rust syntax.
-    #[thrust_macros::predicate]
-    fn is_double(self, doubled: Self) -> bool {
-        self.x * 2 == doubled.x
-    }
-
-    // Check if this method complies with annotations in
-    // trait definition.
-    fn double(&mut self) {
-        self.x += self.x;
-    }
-}
-
-fn main() {
-    let mut a = A { x: 3 };
-    a.double();
-    assert!(a.x == 6);
-}

From 107baaedf86c9a3226c1f855f359081962a3ae8c Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Thu, 11 Jun 2026 01:50:43 +0000
Subject: [PATCH 3/4] Render predicate formulas via TermSortEnv; drop field
 dependency

Replace the synthetic `Clause` used to render a predicate's translated
formula with a `TermSortEnv` trait: anything that can resolve a term-level
variable's sort (a `Clause` via its `vars`, or a bare `IndexVec<TermVarIdx,
Sort>` for a define-fun signature) can drive term rendering. The smtlib2
Display wrappers now hold `&dyn TermSortEnv` instead of `&Clause`, so no
fake clause is fabricated.

Also revert the named-struct-field translator change and the trait
predicate test conversions: that field resolution is now a separate PR
(#118). The trait predicate tests stay on raw SMT2 here and can move to
Rust syntax once the field PR lands; the scalar free-function predicate
test exercises the Rust-syntax path.

https://claude.ai/code/session_01WdLyxyy4ieAxrexj83X5MX
---
 src/analyze/annot_fn.rs                  |  21 +---
 src/chc.rs                               |  25 ++++-
 src/chc/format_context.rs                |   2 +-
 src/chc/smtlib2.rs                       | 135 ++++++++++++-----------
 tests/ui/fail/annot_preds_trait.rs       |   9 +-
 tests/ui/fail/annot_preds_trait_multi.rs |  19 +++-
 tests/ui/pass/annot_preds_trait.rs       |   9 +-
 tests/ui/pass/annot_preds_trait_multi.rs |  18 ++-
 8 files changed, 149 insertions(+), 89 deletions(-)

diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs
index 10e65112..9e418169 100644
--- a/src/analyze/annot_fn.rs
+++ b/src/analyze/annot_fn.rs
@@ -529,22 +529,11 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                 FormulaOrTerm::Term(chc::Term::tuple(terms))
             }
             ExprKind::Field(expr, field) => {
-                // Tuples use numeric field names (`.0`); structs (represented as
-                // tuples in the logic) use named fields resolved to their position.
-                let index = match field.name.as_str().parse::<usize>() {
-                    Ok(index) => index,
-                    Err(_) => {
-                        let adt = self
-                            .expr_ty(expr)
-                            .ty_adt_def()
-                            .expect("named field access on a non-ADT type");
-                        adt.non_enum_variant()
-                            .fields
-                            .iter()
-                            .position(|f| f.name == field.name)
-                            .expect("unknown named field in formula")
-                    }
-                };
+                let index = field
+                    .name
+                    .as_str()
+                    .parse::<usize>()
+                    .expect("tuple field index must be a non-negative integer");
                 let term = self.to_term(expr);
                 FormulaOrTerm::Term(term.tuple_proj(index))
             }
diff --git a/src/chc.rs b/src/chc.rs
index 8f8de32d..5ceaf2ac 100644
--- a/src/chc.rs
+++ b/src/chc.rs
@@ -1706,9 +1706,32 @@ impl Clause {
     pub fn is_nop(&self) -> bool {
         self.head.is_top() || self.body.is_bottom()
     }
+}
+
+/// Resolves the sort of term-level variables.
+///
+/// Rendering a [`Term`] to SMT-LIB2 needs the sort of each variable, because
+/// box/mut/tuple constructors and selectors are sort-indexed. Anything that can
+/// provide variable sorts (a [`Clause`] via its `vars`, or a bare list of sorts
+/// for a `define-fun` signature) can drive term rendering through this trait,
+/// so callers need not fabricate a [`Clause`].
+pub trait TermSortEnv {
+    fn var_sort(&self, var: TermVarIdx) -> Sort;
 
     fn term_sort(&self, term: &Term<TermVarIdx>) -> Sort {
-        term.sort(|v| self.vars[*v].clone())
+        term.sort(|v| self.var_sort(*v))
+    }
+}
+
+impl TermSortEnv for Clause {
+    fn var_sort(&self, var: TermVarIdx) -> Sort {
+        self.vars[var].clone()
+    }
+}
+
+impl TermSortEnv for IndexVec<TermVarIdx, Sort> {
+    fn var_sort(&self, var: TermVarIdx) -> Sort {
+        self[var].clone()
     }
 }
 
diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs
index 94548274..4ca1ba72 100644
--- a/src/chc/format_context.rs
+++ b/src/chc/format_context.rs
@@ -7,7 +7,7 @@
 
 use std::collections::BTreeSet;
 
-use crate::chc::{self, hoice::HoiceDatatypeRenamer};
+use crate::chc::{self, hoice::HoiceDatatypeRenamer, TermSortEnv as _};
 
 /// A context for formatting a CHC system.
 ///
diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs
index 5103b35c..1d86fc53 100644
--- a/src/chc/smtlib2.rs
+++ b/src/chc/smtlib2.rs
@@ -89,11 +89,11 @@ impl<T> List<T> {
 }
 
 /// A wrapper around a [`chc::Term`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
-#[derive(Debug, Clone)]
+#[derive(Clone)]
 struct Term<'ctx, 'a> {
     ctx: &'ctx FormatContext,
-    // we need clause to select box/mut selector/constructor based on sort
-    clause: &'a chc::Clause,
+    // we need variable sorts to select box/mut selector/constructor
+    sorts: &'a dyn chc::TermSortEnv,
     inner: &'a chc::Term,
 }
 
@@ -106,49 +106,49 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> {
             chc::Term::Bool(b) => write!(f, "{}", b),
             chc::Term::String(s) => write!(f, "\"{}\"", s.escape_default()),
             chc::Term::Box(t) => {
-                let s = self.clause.term_sort(t);
+                let s = self.sorts.term_sort(t);
                 write!(
                     f,
                     "({} {})",
                     self.ctx.box_ctor(&s),
-                    Term::new(self.ctx, self.clause, t)
+                    Term::new(self.ctx, self.sorts, t)
                 )
             }
             chc::Term::Mut(t1, t2) => {
-                let s = self.clause.term_sort(t1);
+                let s = self.sorts.term_sort(t1);
                 write!(
                     f,
                     "({} {} {})",
                     self.ctx.mut_ctor(&s),
-                    Term::new(self.ctx, self.clause, t1),
-                    Term::new(self.ctx, self.clause, t2)
+                    Term::new(self.ctx, self.sorts, t1),
+                    Term::new(self.ctx, self.sorts, t2)
                 )
             }
             chc::Term::BoxCurrent(t) => {
-                let s = self.clause.term_sort(t).deref();
+                let s = self.sorts.term_sort(t).deref();
                 write!(
                     f,
                     "({} {})",
                     self.ctx.box_current(&s),
-                    Term::new(self.ctx, self.clause, t)
+                    Term::new(self.ctx, self.sorts, t)
                 )
             }
             chc::Term::MutCurrent(t) => {
-                let s = self.clause.term_sort(t).deref();
+                let s = self.sorts.term_sort(t).deref();
                 write!(
                     f,
                     "({} {})",
                     self.ctx.mut_current(&s),
-                    Term::new(self.ctx, self.clause, t)
+                    Term::new(self.ctx, self.sorts, t)
                 )
             }
             chc::Term::MutFinal(t) => {
-                let s = self.clause.term_sort(t).deref();
+                let s = self.sorts.term_sort(t).deref();
                 write!(
                     f,
                     "({} {})",
                     self.ctx.mut_final(&s),
-                    Term::new(self.ctx, self.clause, t)
+                    Term::new(self.ctx, self.sorts, t)
                 )
             }
             chc::Term::App(fn_, args) => {
@@ -156,11 +156,11 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> {
                     f,
                     "({} {})",
                     fn_,
-                    List::open(args.iter().map(|t| Term::new(self.ctx, self.clause, t)))
+                    List::open(args.iter().map(|t| Term::new(self.ctx, self.sorts, t)))
                 )
             }
             chc::Term::Tuple(ts) => {
-                let ss: Vec<_> = ts.iter().map(|t| self.clause.term_sort(t)).collect();
+                let ss: Vec<_> = ts.iter().map(|t| self.sorts.term_sort(t)).collect();
                 if ss.is_empty() {
                     write!(f, "{}", self.ctx.tuple_ctor(&ss),)
                 } else {
@@ -168,17 +168,17 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> {
                         f,
                         "({} {})",
                         self.ctx.tuple_ctor(&ss),
-                        List::open(ts.iter().map(|t| Term::new(self.ctx, self.clause, t)))
+                        List::open(ts.iter().map(|t| Term::new(self.ctx, self.sorts, t)))
                     )
                 }
             }
             chc::Term::TupleProj(t, i) => {
-                let s = self.clause.term_sort(t);
+                let s = self.sorts.term_sort(t);
                 write!(
                     f,
                     "({} {})",
                     self.ctx.tuple_proj(s.as_tuple().unwrap(), *i),
-                    Term::new(self.ctx, self.clause, t)
+                    Term::new(self.ctx, self.sorts, t)
                 )
             }
             chc::Term::DatatypeCtor(sort, sym, args) => {
@@ -189,17 +189,17 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> {
                         f,
                         "({} {})",
                         self.ctx.datatype_ctor(sort, sym),
-                        List::open(args.iter().map(|t| Term::new(self.ctx, self.clause, t)))
+                        List::open(args.iter().map(|t| Term::new(self.ctx, self.sorts, t)))
                     )
                 }
             }
             chc::Term::DatatypeDiscr(_s, t) => {
-                let s = self.clause.term_sort(t).into_datatype().unwrap();
+                let s = self.sorts.term_sort(t).into_datatype().unwrap();
                 write!(
                     f,
                     "({} {})",
                     self.ctx.datatype_discr(&s),
-                    Term::new(self.ctx, self.clause, t)
+                    Term::new(self.ctx, self.sorts, t)
                 )
             }
             chc::Term::FormulaExistentialVar(_, name) => write!(f, "{}", name),
@@ -208,23 +208,27 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> {
 }
 
 impl<'ctx, 'a> Term<'ctx, 'a> {
-    pub fn new(ctx: &'ctx FormatContext, clause: &'a chc::Clause, inner: &'a chc::Term) -> Self {
-        Self { ctx, clause, inner }
+    pub fn new(
+        ctx: &'ctx FormatContext,
+        sorts: &'a dyn chc::TermSortEnv,
+        inner: &'a chc::Term,
+    ) -> Self {
+        Self { ctx, sorts, inner }
     }
 }
 
 /// A wrapper around a [`chc::Atom`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
-#[derive(Debug, Clone)]
+#[derive(Clone)]
 pub struct Atom<'ctx, 'a> {
     ctx: &'ctx FormatContext,
-    clause: &'a chc::Clause,
+    sorts: &'a dyn chc::TermSortEnv,
     inner: &'a chc::Atom,
 }
 
 impl<'ctx, 'a> std::fmt::Display for Atom<'ctx, 'a> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         if let Some(guard) = &self.inner.guard {
-            let guard = Formula::new(self.ctx, self.clause, guard);
+            let guard = Formula::new(self.ctx, self.sorts, guard);
             write!(f, "(=> {} ", guard)?;
         }
         if self.inner.pred.is_negative() {
@@ -241,7 +245,7 @@ impl<'ctx, 'a> std::fmt::Display for Atom<'ctx, 'a> {
                 self.inner
                     .args
                     .iter()
-                    .map(|t| Term::new(self.ctx, self.clause, t)),
+                    .map(|t| Term::new(self.ctx, self.sorts, t)),
             );
             write!(f, "({} {})", pred, args)?;
         }
@@ -256,16 +260,20 @@ impl<'ctx, 'a> std::fmt::Display for Atom<'ctx, 'a> {
 }
 
 impl<'ctx, 'a> Atom<'ctx, 'a> {
-    pub fn new(ctx: &'ctx FormatContext, clause: &'a chc::Clause, inner: &'a chc::Atom) -> Self {
-        Self { ctx, clause, inner }
+    pub fn new(
+        ctx: &'ctx FormatContext,
+        sorts: &'a dyn chc::TermSortEnv,
+        inner: &'a chc::Atom,
+    ) -> Self {
+        Self { ctx, sorts, inner }
     }
 }
 
 /// A wrapper around a [`chc::Formula`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
-#[derive(Debug, Clone)]
+#[derive(Clone)]
 pub struct Formula<'ctx, 'a> {
     ctx: &'ctx FormatContext,
-    clause: &'a chc::Clause,
+    sorts: &'a dyn chc::TermSortEnv,
     inner: &'a chc::Formula,
 }
 
@@ -273,19 +281,19 @@ impl<'ctx, 'a> std::fmt::Display for Formula<'ctx, 'a> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self.inner {
             chc::Formula::Atom(atom) => {
-                let atom = Atom::new(self.ctx, self.clause, atom);
+                let atom = Atom::new(self.ctx, self.sorts, atom);
                 write!(f, "{}", atom)
             }
             chc::Formula::Not(fo) => {
-                let fo = Formula::new(self.ctx, self.clause, fo);
+                let fo = Formula::new(self.ctx, self.sorts, fo);
                 write!(f, "(not {})", fo)
             }
             chc::Formula::And(fs) => {
-                let fs = List::open(fs.iter().map(|fo| Formula::new(self.ctx, self.clause, fo)));
+                let fs = List::open(fs.iter().map(|fo| Formula::new(self.ctx, self.sorts, fo)));
                 write!(f, "(and {})", fs)
             }
             chc::Formula::Or(fs) => {
-                let fs = List::open(fs.iter().map(|fo| Formula::new(self.ctx, self.clause, fo)));
+                let fs = List::open(fs.iter().map(|fo| Formula::new(self.ctx, self.sorts, fo)));
                 write!(f, "(or {})", fs)
             }
             chc::Formula::Exists(vars, fo) => {
@@ -293,7 +301,7 @@ impl<'ctx, 'a> std::fmt::Display for Formula<'ctx, 'a> {
                     List::closed(vars.iter().map(|(v, s)| {
                         List::closed([v.to_string(), self.ctx.fmt_sort(s).to_string()])
                     }));
-                let fo = Formula::new(self.ctx, self.clause, fo);
+                let fo = Formula::new(self.ctx, self.sorts, fo);
                 write!(f, "(exists {vars} {fo})")
             }
         }
@@ -301,16 +309,20 @@ impl<'ctx, 'a> std::fmt::Display for Formula<'ctx, 'a> {
 }
 
 impl<'ctx, 'a> Formula<'ctx, 'a> {
-    pub fn new(ctx: &'ctx FormatContext, clause: &'a chc::Clause, inner: &'a chc::Formula) -> Self {
-        Self { ctx, clause, inner }
+    pub fn new(
+        ctx: &'ctx FormatContext,
+        sorts: &'a dyn chc::TermSortEnv,
+        inner: &'a chc::Formula,
+    ) -> Self {
+        Self { ctx, sorts, inner }
     }
 }
 
 /// A wrapper around a [`chc::Body`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
-#[derive(Debug, Clone)]
+#[derive(Clone)]
 pub struct Body<'ctx, 'a> {
     ctx: &'ctx FormatContext,
-    clause: &'a chc::Clause,
+    sorts: &'a dyn chc::TermSortEnv,
     inner: &'a chc::Body,
 }
 
@@ -320,16 +332,20 @@ impl<'ctx, 'a> std::fmt::Display for Body<'ctx, 'a> {
             self.inner
                 .atoms
                 .iter()
-                .map(|a| Atom::new(self.ctx, self.clause, a)),
+                .map(|a| Atom::new(self.ctx, self.sorts, a)),
         );
-        let formula = Formula::new(self.ctx, self.clause, &self.inner.formula);
+        let formula = Formula::new(self.ctx, self.sorts, &self.inner.formula);
         write!(f, "(and {atoms} {formula})")
     }
 }
 
 impl<'ctx, 'a> Body<'ctx, 'a> {
-    pub fn new(ctx: &'ctx FormatContext, clause: &'a chc::Clause, inner: &'a chc::Body) -> Self {
-        Self { ctx, clause, inner }
+    pub fn new(
+        ctx: &'ctx FormatContext,
+        sorts: &'a dyn chc::TermSortEnv,
+        inner: &'a chc::Body,
+    ) -> Self {
+        Self { ctx, sorts, inner }
     }
 }
 
@@ -583,23 +599,18 @@ impl<'ctx, 'a> std::fmt::Display for UserDefinedPredDef<'ctx, 'a> {
         match &self.inner.body {
             chc::UserDefinedPredBody::Raw(body) => write!(f, "{body}")?,
             chc::UserDefinedPredBody::Formula(formula) => {
-                // Term display needs a `Clause` to resolve sorts (for box/mut/tuple
-                // constructors); build a synthetic one whose `vars` are the
-                // predicate's parameter sorts in order. The formula's `Var(v{i})`
-                // and the `(v{i} Sort)` parameter list above both render via
-                // `TermVarIdx`, so they line up by index.
-                let clause = chc::Clause {
-                    vars: self
-                        .inner
-                        .sig
-                        .iter()
-                        .map(|(_, sort)| sort.clone())
-                        .collect(),
-                    head: chc::Atom::top(),
-                    body: chc::Body::default(),
-                    debug_info: chc::DebugInfo::default(),
-                };
-                write!(f, "{}", Formula::new(self.ctx, &clause, formula))?;
+                // Term display resolves variable sorts (for box/mut/tuple
+                // constructors) through a `TermSortEnv`: here, the predicate's
+                // parameter sorts in order. The formula's `Var(v{i})` and the
+                // `(v{i} Sort)` parameter list above both render via `TermVarIdx`,
+                // so they line up by index.
+                let sorts: rustc_index::IndexVec<chc::TermVarIdx, chc::Sort> = self
+                    .inner
+                    .sig
+                    .iter()
+                    .map(|(_, sort)| sort.clone())
+                    .collect();
+                write!(f, "{}", Formula::new(self.ctx, &sorts, formula))?;
             }
         }
         write!(f, ")")
diff --git a/tests/ui/fail/annot_preds_trait.rs b/tests/ui/fail/annot_preds_trait.rs
index eeae01a3..d6e9a28f 100644
--- a/tests/ui/fail/annot_preds_trait.rs
+++ b/tests/ui/fail/annot_preds_trait.rs
@@ -25,10 +25,15 @@ trait Double {
 
 #[thrust_macros::context]
 impl Double for A {
-    // self.x * 3 (this isn't actually doubled!) does not comply with the trait.
+    // Write concrete definitions for predicates in `impl` blocks
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        self.x * 3 == doubled.x
+        // (tuple_proj<Int>.0 self) is equivalent to self.x
+        // self.x * 3 == doubled.x (this isn't actually doubled!) is written as following:
+        "(=
+            (* (tuple_proj<Int>.0 self_) 3)
+            (tuple_proj<Int>.0 doubled)
+        )"; true // This definition does not comply with annotations in trait!
     }
 
     // Check if this method complies with annotations in
diff --git a/tests/ui/fail/annot_preds_trait_multi.rs b/tests/ui/fail/annot_preds_trait_multi.rs
index 1ffa1003..b1156e50 100644
--- a/tests/ui/fail/annot_preds_trait_multi.rs
+++ b/tests/ui/fail/annot_preds_trait_multi.rs
@@ -26,7 +26,11 @@ impl thrust_models::Model for A {
 impl Double for A {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        self.x * 2 == doubled.x
+        // self.x * 2 == doubled.x
+        "(=
+            (* (tuple_proj<Int>.0 self_) 2)
+            (tuple_proj<Int>.0 doubled)
+        )"; true
     }
 
     fn double(&mut self) {
@@ -46,10 +50,19 @@ impl thrust_models::Model for B {
 
 #[thrust_macros::context]
 impl Double for B {
-    // self.x * 3 (this isn't actually doubled!) does not comply with the trait.
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        self.x * 3 == doubled.x && self.y * 2 == doubled.y
+        // self.x * 3 == doubled.x && self.y * 2 == doubled.y (this isn't actually doubled!)
+        "(and
+            (=
+                (* (tuple_proj<Int-Int>.0 self_) 3)
+                (tuple_proj<Int-Int>.0 doubled)
+            )
+            (=
+                (* (tuple_proj<Int-Int>.1 self_) 2)
+                (tuple_proj<Int-Int>.1 doubled)
+            )
+        )"; true // This definition does not comply with annotations in trait!
     }
 
     fn double(&mut self) {
diff --git a/tests/ui/pass/annot_preds_trait.rs b/tests/ui/pass/annot_preds_trait.rs
index 0b915ea5..45f26ab6 100644
--- a/tests/ui/pass/annot_preds_trait.rs
+++ b/tests/ui/pass/annot_preds_trait.rs
@@ -25,10 +25,15 @@ trait Double {
 
 #[thrust_macros::context]
 impl Double for A {
-    // Write concrete definitions for predicates in `impl` blocks, in Rust syntax.
+    // Write concrete definitions for predicates in `impl` blocks
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        self.x * 2 == doubled.x
+        // (tuple_proj<Int>.0 self) is equivalent to self.x
+        // self.x * 2 == doubled.x is written as following:
+        "(=
+            (* (tuple_proj<Int>.0 self_) 2)
+            (tuple_proj<Int>.0 doubled)
+        )"; true
     }
 
     // Check if this method complies with annotations in
diff --git a/tests/ui/pass/annot_preds_trait_multi.rs b/tests/ui/pass/annot_preds_trait_multi.rs
index dd8d9308..326e5f01 100644
--- a/tests/ui/pass/annot_preds_trait_multi.rs
+++ b/tests/ui/pass/annot_preds_trait_multi.rs
@@ -26,7 +26,11 @@ impl thrust_models::Model for A {
 impl Double for A {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        self.x * 2 == doubled.x
+        // self.x * 2 == doubled.x
+        "(=
+            (* (tuple_proj<Int>.0 self_) 2)
+            (tuple_proj<Int>.0 doubled)
+        )"; true
     }
 
     fn double(&mut self) {
@@ -48,7 +52,17 @@ impl thrust_models::Model for B {
 impl Double for B {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        self.x * 2 == doubled.x && self.y * 2 == doubled.y
+        // self.x * 2 == doubled.x && self.y * 2 == doubled.y
+        "(and
+            (=
+                (* (tuple_proj<Int-Int>.0 self_) 2)
+                (tuple_proj<Int-Int>.0 doubled)
+            )
+            (=
+                (* (tuple_proj<Int-Int>.1 self_) 2)
+                (tuple_proj<Int-Int>.1 doubled)
+            )
+        )"; true
     }
 
     fn double(&mut self) {

From 9c96cde73c59cf80f11869af0caf41d67ea36604 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Fri, 12 Jun 2026 16:07:15 +0000
Subject: [PATCH 4/4] Convert trait predicate tests to Rust syntax

Now that named struct-field resolution is on main (#118), flip the trait
predicate tests (annot_preds_trait, annot_preds_trait_multi; pass and fail)
from raw SMT-LIB2 bodies to Rust-expression bodies using `self.x`.

https://claude.ai/code/session_01WdLyxyy4ieAxrexj83X5MX
---
 tests/ui/fail/annot_preds_trait.rs       |  9 ++-------
 tests/ui/fail/annot_preds_trait_multi.rs | 19 +++----------------
 tests/ui/pass/annot_preds_trait.rs       |  9 ++-------
 tests/ui/pass/annot_preds_trait_multi.rs | 18 ++----------------
 4 files changed, 9 insertions(+), 46 deletions(-)

diff --git a/tests/ui/fail/annot_preds_trait.rs b/tests/ui/fail/annot_preds_trait.rs
index d6e9a28f..eeae01a3 100644
--- a/tests/ui/fail/annot_preds_trait.rs
+++ b/tests/ui/fail/annot_preds_trait.rs
@@ -25,15 +25,10 @@ trait Double {
 
 #[thrust_macros::context]
 impl Double for A {
-    // Write concrete definitions for predicates in `impl` blocks
+    // self.x * 3 (this isn't actually doubled!) does not comply with the trait.
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // (tuple_proj<Int>.0 self) is equivalent to self.x
-        // self.x * 3 == doubled.x (this isn't actually doubled!) is written as following:
-        "(=
-            (* (tuple_proj<Int>.0 self_) 3)
-            (tuple_proj<Int>.0 doubled)
-        )"; true // This definition does not comply with annotations in trait!
+        self.x * 3 == doubled.x
     }
 
     // Check if this method complies with annotations in
diff --git a/tests/ui/fail/annot_preds_trait_multi.rs b/tests/ui/fail/annot_preds_trait_multi.rs
index b1156e50..1ffa1003 100644
--- a/tests/ui/fail/annot_preds_trait_multi.rs
+++ b/tests/ui/fail/annot_preds_trait_multi.rs
@@ -26,11 +26,7 @@ impl thrust_models::Model for A {
 impl Double for A {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 2 == doubled.x
-        "(=
-            (* (tuple_proj<Int>.0 self_) 2)
-            (tuple_proj<Int>.0 doubled)
-        )"; true
+        self.x * 2 == doubled.x
     }
 
     fn double(&mut self) {
@@ -50,19 +46,10 @@ impl thrust_models::Model for B {
 
 #[thrust_macros::context]
 impl Double for B {
+    // self.x * 3 (this isn't actually doubled!) does not comply with the trait.
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 3 == doubled.x && self.y * 2 == doubled.y (this isn't actually doubled!)
-        "(and
-            (=
-                (* (tuple_proj<Int-Int>.0 self_) 3)
-                (tuple_proj<Int-Int>.0 doubled)
-            )
-            (=
-                (* (tuple_proj<Int-Int>.1 self_) 2)
-                (tuple_proj<Int-Int>.1 doubled)
-            )
-        )"; true // This definition does not comply with annotations in trait!
+        self.x * 3 == doubled.x && self.y * 2 == doubled.y
     }
 
     fn double(&mut self) {
diff --git a/tests/ui/pass/annot_preds_trait.rs b/tests/ui/pass/annot_preds_trait.rs
index 45f26ab6..0b915ea5 100644
--- a/tests/ui/pass/annot_preds_trait.rs
+++ b/tests/ui/pass/annot_preds_trait.rs
@@ -25,15 +25,10 @@ trait Double {
 
 #[thrust_macros::context]
 impl Double for A {
-    // Write concrete definitions for predicates in `impl` blocks
+    // Write concrete definitions for predicates in `impl` blocks, in Rust syntax.
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // (tuple_proj<Int>.0 self) is equivalent to self.x
-        // self.x * 2 == doubled.x is written as following:
-        "(=
-            (* (tuple_proj<Int>.0 self_) 2)
-            (tuple_proj<Int>.0 doubled)
-        )"; true
+        self.x * 2 == doubled.x
     }
 
     // Check if this method complies with annotations in
diff --git a/tests/ui/pass/annot_preds_trait_multi.rs b/tests/ui/pass/annot_preds_trait_multi.rs
index 326e5f01..dd8d9308 100644
--- a/tests/ui/pass/annot_preds_trait_multi.rs
+++ b/tests/ui/pass/annot_preds_trait_multi.rs
@@ -26,11 +26,7 @@ impl thrust_models::Model for A {
 impl Double for A {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 2 == doubled.x
-        "(=
-            (* (tuple_proj<Int>.0 self_) 2)
-            (tuple_proj<Int>.0 doubled)
-        )"; true
+        self.x * 2 == doubled.x
     }
 
     fn double(&mut self) {
@@ -52,17 +48,7 @@ impl thrust_models::Model for B {
 impl Double for B {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 2 == doubled.x && self.y * 2 == doubled.y
-        "(and
-            (=
-                (* (tuple_proj<Int-Int>.0 self_) 2)
-                (tuple_proj<Int-Int>.0 doubled)
-            )
-            (=
-                (* (tuple_proj<Int-Int>.1 self_) 2)
-                (tuple_proj<Int-Int>.1 doubled)
-            )
-        )"; true
+        self.x * 2 == doubled.x && self.y * 2 == doubled.y
     }
 
     fn double(&mut self) {