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