Add param/ret/sig refinement-type annotations via thrust_macros

[coord-e]

Summary

Adds thrust_macros::param, thrust_macros::ret, and thrust_macros::sig attribute macros that express refinement types (e.g. List<{ v: i32 | v > 0 }>) and lower them to the same rustc-typechecked #[thrust::formula_fn] machinery already used by requires/ensures. This gives refinement-type formulas full name resolution, model-type checking, user-defined predicates, etc. — instead of the limited hand-written DSL in src/annot.rs.

This is a step toward #70 (dropping the old annotation parser): it implements thrust::param / thrust::ret (plus sig) on top of the typechecked formula mechanism. See "Follow-up: removing the old parser" below.

Design

A refinement is placed via a type position — a path of indices that addresses into the function type uniformly:

• first index selects a parameter (by index) or the return slot (== parameter count);
• subsequent indices descend into generic arguments (enum type-args, Box pointee).

Each macro emits, per refinement, a sibling #[thrust::formula_fn] and injects a #[thrust::refine(i, j, …)] path statement into the body. The plugin collects these, translates each formula to a Refinement, and installs it into the parameter/return RefinedType template via a new RefinedType::install_refinement_at navigator.

• param(name: ty) — root [param_index(name)]
• ret(ty) — root [param_count]
• sig(fn(n0: t0, …) -> ret) — one job per arg + the return; the direct counterpart of the legacy thrust::sig

All three share one token scanner and lower to the same #[thrust::refine(..)] attribute + navigator (no param/ret special-casing in the plugin).

Changes

• thrust-macros/src/lib.rs: param/ret/sig proc macros + shallow type-expression scanner.
• src/analyze/annot.rs: refine_path() + integer-position parser.
• src/analyze.rs: collect #[thrust::refine(..)] statements and resolve them to positioned refinements (reusing FormulaFn::to_ensure_annot).
• src/rty.rs: RefinedType::install_refinement_at navigator (Function params/ret, enum args, Box pointee).
• src/refine/template.rs: FunctionTemplateTypeBuilder::refine entry.
• src/analyze/local_def.rs: wiring.
• Migrated the existing thrust::sig tests (annot_box_term) to thrust_macros::sig, plus new refine_param_simple / refine_sig pass+fail tests.

The legacy parse_rty path is left intact and untouched.

Verification

• Full suite green: 192 UI tests (188 baseline + 4 new) + doc tests, against Z3 4.13.0 + the COAR pcsat image (matching CI).
• cargo fmt --all -- --check and cargo clippy -- -D warnings clean.

Known limitation (pre-existing, not introduced here)

While building the type at any depth is correct, thrust's verifier reliably enforces only top-level (depth-0) parameter/return refinements today. Enum/datatype nested args are enforced soundly, but Box (own-pointer) pointee refinements in return position are not — filed as #97. The committed tests therefore stick to depth-0 cases plus the whole-box sig migration.

Follow-up: removing the old parser (#70)

After this change, nothing in the repo (src, tests, examples, injected std.rs prelude) uses the legacy thrust::param/thrust::ret/thrust::sig or raw thrust::requires(..)/thrust::ensures(..) forms — all use thrust_macros::*. The AnnotParser (parse_rty/parse_formula) is reachable only from its own code paths and can be removed in a follow-up (retaining AnnotFormula, which the formula_fn path still uses). Left out of this PR to keep it focused.

Test plan

• cargo test (full UI + doc tests) passes with Z3 + COAR image
• cargo fmt --all -- --check
• cargo clippy -- -D warnings
• param/ret/sig pass+fail tests behave correctly (refinement enforced)
• annot_box_term migration: pass stays pass, fail stays Unsat

Refs #70.

https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

---

Generated by Claude Code