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, so the dual attribute doesn't change call-site behavior.

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. main is merged into this branch, so that support is included here.

Verification

• 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.
• Full ui suite: 230 passed (z3 4.13.0 + docker pcsat for the relevant tests).

https://claude.ai/code/session_01WdLyxyy4ieAxrexj83X5MX