Support Rust syntax in thrust::predicate bodies

[coord-e]

Summary

#[thrust::predicate] bodies can now be written as ordinary Rust boolean expressions instead of raw SMT-LIB2 string literals, reusing the existing formula_fn translation pipeline (AnnotFnTranslator).

// before — raw SMT2
#[thrust_macros::predicate]
fn is_double(self, doubled: Self) -> bool {
    "(= (* (tuple_proj<Int>.0 self_) 2) (tuple_proj<Int>.0 doubled))"; true
}

// after — Rust syntax
#[thrust_macros::predicate]
fn is_double(self, doubled: Self) -> bool {
    self.x * 2 == doubled.x
}

Raw SMT2 string bodies still work unchanged (backward compatible).

How it works

A predicate written with #[thrust_macros::predicate] whose body is a Rust expression is expanded with an additional #[thrust::formula_fn] attribute, which is the single discriminator:

• present ⇒ the body is interpreted by AnnotFnTranslator through the existing formula_fns cache (formula_fn_with_args), exactly like requires/ensures/invariant. The resulting chc::Formula is emitted as the predicate's SMT define-fun.
• absent ⇒ the legacy raw-SMT2 string path (unchanged).

The macro picks which by inspecting the body (string-literal statement ⇒ raw; otherwise Rust). Borrow-check skipping is free, since mir_borrowck_skip_formula_fn already keys on the formula_fn attribute. Predicate call sites are still resolved as named UserDefinedPred atoms.

Changes

• chc.rs — UserDefinedPredDef body becomes a UserDefinedPredBody { Raw, Formula } enum; add push_pred_define_formula. New TermSortEnv trait (var_sort/term_sort), implemented for Clause and IndexVec<TermVarIdx, Sort>.
• chc/smtlib2.rs — the Term/Atom/Formula/Body Display wrappers now hold &dyn TermSortEnv instead of &Clause. A Formula predicate body is rendered by passing the sig's sorts as an IndexVec — no synthetic/fake Clause is fabricated.
• chc/format_context.rs — uses the TermSortEnv trait (moved Clause::term_sort onto it).
• chc/unbox.rs — unbox Formula predicate bodies.
• analyze/crate_.rs — register predicate items also marked formula_fn.
• analyze/local_def.rs — define_as_predicate branches on the formula_fn attribute; pulls the formula from formula_fn_with_args, naming params v{i}.
• thrust-macros/src/spec.rs — expand_predicate: detect raw-vs-Rust body; for Rust bodies add #[thrust::formula_fn], rewrite self→self_, add allow-attrs.
• tests — scalar (annot_preds), trait (annot_preds_trait), and multi-field (annot_preds_trait_multi) predicate tests (pass + fail) converted to Rust syntax.

Dependency

Named struct-field access (self.x) in the trait/multi-field predicates relies on #118 (merged), which taught the formula translator to resolve named ADT fields.

Notes

• Rebased onto the latest main (single feature commit).
• Verification (local, z3 4.13.0 + docker pcsat): the full ui suite passes except iterators/fixed_filter_loop_none.rs, which returns solver unknown on z3 4.13.0. That failure is pre-existing and unrelated — it reproduces identically on main at the rebase base with the same z3, and main pins z3 to 4.15.4 (ci: pin Z3 to 4.15.4, the latest version without mut_recursive timeout #149) precisely to avoid such solver-version issues. CI runs 4.15.4.
• Inspected the generated SMT2: self.x * 2 == doubled.x lowers to exactly (= (* (tuple_proj<Int>.0 v0) 2) (tuple_proj<Int>.0 v1)) — identical to the previous raw form.

https://claude.ai/code/session_01WdLyxyy4ieAxrexj83X5MX

[coord-e]

全体の設計は妥当だと思います。formula_fn 属性による判別、v{i} パラメータ名と TermVarIdx の対応（FunctionParamIdx → TermVarIdx がインデックス一致、AnnotFnTranslator::build_env_from_params も sig.inputs() と同順で列挙）、TermSortEnv リファクタの Clause ケースでの挙動保存、unbox の新バリアント対応、既存の生 SMT2 述語が is_raw_smt2_body で従来どおり raw 判定される点、いずれも確認しました。cargo check --all-targets は通ります（手元にソルバがないため ui テストは未実行）。

バグ2件とコメントの陳腐化1件をインラインで指摘しています。

---

Generated by Claude Code

[coord-e]

mk_args(&[]) discards the predicate's generic args. For a Rust-bodied predicate declared in a trait default body or inside a generic impl, formula_fn_with_args reaches EarlyBinder::instantiate with an empty arg list and ICEs with "type parameter out of range".

Every other formula_fn_with_args call site (analyze.rs:760/782/859, local_def.rs:837) threads through real generic_args. crate_::placeholder_generic_args (crate_.rs:193) exists for exactly this case — it is currently private, so it would need to be reachable from here.

---

Generated by Claude Code

[coord-e]

define-funs are emitted in push order, i.e. source order. A Rust predicate body that calls another predicate declared later in the file therefore emits a define-fun referring to a symbol the solver has not seen yet, and the query is rejected.

This is newly reachable with this PR: AnnotFnTranslator (annot_fn.rs:841-873) now translates predicate calls appearing inside formulas, so a predicate body can reference another predicate. Raw SMT-LIB bodies never produced such a reference, which is why push order was fine until now.

---

Generated by Claude Code

[coord-e]

The heading comment on expand_predicate (L19-21) is now stale — it states that predicate bodies are consumed as raw SMT-LIB string literals and "are not routed through formula!", which the formula_fn branch added below directly contradicts.

---

Generated by Claude Code