Add param/ret/sig refinement-type annotations via thrust_macros by coord-e · Pull Request #98 · coord-e/thrust

coord-e · 2026-05-26T15:38:58Z

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

Introduce `thrust_macros::param`, `thrust_macros::ret`, and `thrust_macros::sig` attribute macros that lower refinement types (e.g. `{ v: i32 | v > 0 }`) into `#[thrust::formula_fn]`s, giving refinement formulas the same rustc-typechecked treatment as requires/ensures. Each refinement is placed via a new "type position" — a path addressing into the function type (parameter index or return slot, then generic-argument indices for enum args and Box pointees) — emitted as a `#[thrust::refine(..)]` path statement and installed into the parameter or return RefinedType template. Migrate the existing `thrust::sig` tests to `thrust_macros::sig`.

Replace the bare `Vec<usize>` type position with `rty::TypePosition` (a `TypePositionRoot` of `Param(idx)` / `Return`, plus a projection of nested type-argument indices). The `#[thrust::refine(..)]` attribute now uses the `result` keyword to select the return instead of the parameter count, which was unintuitive. Adds `Display` (`$1`, `result.0`).

Replace the previous TypePositionRoot + projection: Vec<usize> split with a flat Vec<TypePositionStep>, where each step is one of: - Param(FunctionParamIdx): navigate into a function type's parameter - Return: navigate into a function type's return slot - TypeArg(usize): navigate into a generic type's type argument This makes the path representation uniform across all type levels, enabling future support for refinements on positions inside higher-order function types (e.g. [$0, result] for the return type of a function-typed first parameter). The attribute encoding changes accordingly: - result (ident) => Return - integer i => Param(i) - bracket group [i] => TypeArg(i) The macro-side RefineRoot+projection split is similarly replaced with a flat Vec<RefineStep> in the Refinement struct, and scan_type now threads the full steps Vec through recursive calls. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

Align the macro-emitted attribute with the existing requires_path / ensures_path convention: the _path suffix conveys that the attribute's target is a path to a formula_fn. The symbol-path helper follows suit (refine_path -> refinement_path_path). https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

Move the param/ret/sig expansion logic and its token-scanning helpers out of the crate root into a dedicated refine module, leaving only the thin proc-macro entry points in lib.rs. Shrinks lib.rs from ~1232 to ~813 lines. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

Encode function parameters as $i (matching FunctionParamIdx's Display) and type arguments as bare integers, instead of bare integers for params and bracketed [i] for type args. Reads more naturally and keeps the attribute syntax consistent with how parameters are displayed elsewhere. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

- Rename FunctionTemplateTypeBuilder::refine to install_refinement_at, matching the RefinedType method it delegates to. - Rename extract_refine_paths / extract_refine_annots to extract_refinement_paths / extract_refinement_annots, and clarify the related panic messages, to reduce the overloaded use of "refine". - Make TypePosition's Display match the refinement_path(..) surface syntax (comma-separated steps) instead of dot-separated. - Replace the macro's build_refine_jobs (and its complex tuple return type) with annotated_type_exprs returning PositionedTypeExpr, and introduce NamedType / SigAnnotation structs so parse_sig_attr no longer needs an allow(clippy::type_complexity). Rename RefineStep to PositionStep, RefineKind to AnnotationKind, and expand_refine to expand for clarity. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

- Replace the undefined phrase "refine position" in parser diagnostics with "type position". - Drop the non-empty invariant from TypePosition: an empty path is a valid notion (it addresses the type itself); a path is only non-empty when applied to a function type. TypePosition::new now takes the full step vector, and that non-emptiness is checked where it matters (the function-type builder). - Rename the macro module file thrust-macros/src/refine.rs to rty.rs and use TypePositionStep there, mirroring the plugin's rty module instead of naming the same concept differently. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

extract_refinement_annots was using FormulaFn::to_ensure_annot to build the refinement, which is a misleading name for that call site (a refinement_path is not an ensures annotation). Introduce a properly-named FormulaFn::to_refinement that returns a rty::Refinement<FunctionParamIdx> directly, removing the awkward AnnotFormula unwrap-or-panic on what was always the Formula variant. The shared var mapping (param 0 -> Value, rest -> Free) lives in a private helper used by both to_ensure_annot and to_refinement. Also rename FunctionTemplateTypeBuilder::install_refinement_at to refinement_at to match the builder's existing param_refinement / ret_refinement convention. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

Add pass/fail pairs for both the param and sig macro forms, using a generic Pair<T> enum monomorphized to Pair<i32> in the signature and a refinement annotation that supplies the element type explicitly as Pair<{ v: i32 | v > 0 }>. Exercises the TypeArg navigation step into enum type arguments. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

… conventions - Centralize per-variant explanations on rty::TypePositionStep itself and reduce the duplicated copies in TypePosition, install_refinement_at, the macro's TypePositionStep, and parse_type_position to thin pointers back to the canonical source. - Fix "Box type position must be [0]" assert message left over from the earlier bracket-encoded syntax. - Drop FormulaFn::formula_with_value_binder. The 0->Value, i>0->Free(i-1) mapping is justified by the layout each macro generates (ensures puts the result at index 0; the refinement-type macros put the binder at index 0), not by a shared abstraction. Inline the mapping into to_ensure_annot and to_refinement, with each method's doc stating which macro's layout it relies on. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

The previous wording claimed "parameters 1..n are the enclosing function's parameters in order", but that framing only fits direct parameter/return refinement; a refinement_path can also be installed at, say, an ADT type-argument position. Describe parameters 1..n as "the formula's free variables" without overspecifying their meaning. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

Replace rty::expand + AnnotationKind dispatch with three separate proc-macro implementations (expand_param, expand_ret, expand_sig). Each parses its own attribute form (which differs fundamentally) and collects refinements via a kind-specific collector (collect_param_refinements / collect_ret_refinements / collect_sig_refinements). The only shared step is the final output assembly, extracted as expand_with_refinements with a clear concrete contract. Drop the ad-hoc aggregates that just named tuples: PositionedTypeExpr, NamedType, SigAnnotation, and AnnotationKind. The parsers now use plain tuples destructured at the call site (parse_name_typed_binding -> (name, ty_tokens), parse_refinement -> (binder, binder_ty, formula)) with names introduced at the point they have local meaning. Also rename codegen helpers to describe what they produce: refine_fn_name -> formula_fn_name, refine_formula_fn -> build_formula_fn, refine_path_stmt -> build_refinement_path_stmt. Document Refinement's fields so binder_ty / formula are no longer opaquely "tokens". https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

- RefinedType models the `{ binder : ty | formula }` syntax fragment. - RefinedTypeAnnotation is a RefinedType paired with its position in the function signature (where it applies). Rename collect_*_refinements to collect_*_annotations and expand_with_refinements to expand_with_annotations so the function names line up with the type they handle. Update parse_refinement to parse_refined_type, returning a RefinedType directly. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

Reframe the type-expression walker so its name and signature tell you what it does: it takes type-expression tokens and returns the refined-type annotations they contain, with positions relative to the input. No mutable accumulator, no implicit root-step parameter. Callers add the root step via a small anchor_at helper that prepends a TypePositionStep to every annotation's position; nested recursion inside parse_refined_type_annotations uses the same helper to attribute TypeArg steps for each generic argument. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

Drop emit_error and inline its two-line body at each call site, and shorten the module-level doc, the type and function doc comments, and the inline comments in parse_refined_type_annotations. Also remove the section-banner separator comments. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

Copilot

Pull request overview

Introduces thrust_macros::param, thrust_macros::ret, and thrust_macros::sig attribute macros to express refinement types in type positions and lower them into the existing typechecked #[thrust::formula_fn] pipeline by emitting #[thrust::refinement_path(..)] path statements that the analyzer collects and installs into RefinedType templates.

Changes:

Add proc-macro support for parsing refinement-type syntax in type positions and generating corresponding formula_fns plus refinement_path statements.
Extend the analyzer to collect #[thrust::refinement_path(..)] statements, translate referenced formula functions into rty::Refinement, and install them into parameter/return refined types via a type-position navigator.
Add/migrate UI tests to cover param/ret/sig success and failure cases, including migration of the annot_box_term test to thrust_macros::sig.

Reviewed changes

Copilot reviewed 18 out of 18 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
thrust-macros/src/rty.rs	Implements `param`/`ret`/`sig` expansion and token scanning for refinement types and type-position paths.
thrust-macros/src/lib.rs	Exposes the new proc-macro attributes (`param`, `ret`, `sig`) and wires in the new module.
src/analyze/annot.rs	Adds parsing for `#[thrust::refinement_path(..)]` type-position tokens into `rty::TypePosition`.
src/analyze/annot_fn.rs	Adds `FormulaFn::to_refinement` to translate macro-generated formula fns into `rty::Refinement`.
src/analyze.rs	Collects `refinement_path` statements from function bodies and resolves them into positioned refinements.
src/analyze/local_def.rs	Plumbs extracted positioned refinements into function template construction.
src/rty.rs	Introduces `TypePosition`/`TypePositionStep` and adds `RefinedType::install_refinement_at` navigator.
src/refine/template.rs	Adds `FunctionTemplateTypeBuilder::refinement_at` for installing refinements at a type position.
tests/ui/pass/refine_sig.rs	New passing UI test for `thrust_macros::sig` on a simple function.
tests/ui/pass/refine_sig_generic_adt.rs	New passing UI test for `sig` refining a generic ADT’s type argument.
tests/ui/pass/refine_param_simple.rs	New passing UI test for `param` + `ret` interaction.
tests/ui/pass/refine_param_generic_adt.rs	New passing UI test for `param` refining a generic ADT argument.
tests/ui/pass/annot_box_term.rs	Migrates existing `sig` box-term test to `thrust_macros::sig`.
tests/ui/fail/refine_sig.rs	New failing UI test ensuring `sig` refinements are enforced (`Unsat`).
tests/ui/fail/refine_sig_generic_adt.rs	New failing UI test for `sig` with generic ADT refinement mismatch.
tests/ui/fail/refine_param_simple.rs	New failing UI test for `param`/`ret` mismatch (`Unsat`).
tests/ui/fail/refine_param_generic_adt.rs	New failing UI test for generic ADT param refinement mismatch (`Unsat`).
tests/ui/fail/annot_box_term.rs	Migrates existing failing `sig` box-term test to `thrust_macros::sig`.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

coord-e · 2026-06-02T17:01:49Z

+    // A nominal type `Name<arg0, ..>`: each arg sits one `TypeArg(i)` deeper.
+    if let TokenTree2::Ident(_) = &tokens[0] {
+        if let Some(TokenTree2::Punct(p)) = tokens.get(1) {
+            if p.as_char() == '<' {
+                let mut out = Vec::new();
+                let mut type_idx = 0;
+                for arg in split_angle_args(&tokens[2..]) {
+                    if is_lifetime(&arg) {
+                        continue;
+                    }
+                    out.extend(anchor_at(
+                        parse_refined_type_annotations(&arg)?,
+                        TypePositionStep::TypeArg(type_idx),
+                    ));
+                    type_idx += 1;
+                }
+                return Ok(out);
+            }
+        }
+    }


Fixed in d65014e. parse_refined_type_annotations now walks through path::to::Name segments before looking for <, and treats a leading & (with optional lifetime / mut) as a TypeArg(0) step into the pointee — so std::vec::Vec<{..}>, crate::Pair<{..}>, and &Vec<{..}> all get their nested refinements discovered.

Added a refine_param_path_qualified pass/fail pair (crate::Pair<{ v: i32 | v > 0 }>) that exercises this; without the fix, the pass test fails verification because the refinement is silently missed.

Generated by Claude Code

Good point — you're right that we don't need to validate the prefix is a path here. The only thing that matters is whether the tokens contain a < whose args might host refinements; whatever comes before is just opaque skin. Simplified in 1f35265 to a single "find the first top-level <" — this covers paths, plain idents, dyn/impl prefixes, etc. without enumerating them.

Generated by Claude Code

coord-e · 2026-06-02T17:02:03Z

+        fn #name #def_generics(
+            #binder: <#binder_ty as thrust_models::Model>::Ty,
+            #model_params


Fixed in d65014e. The parser now stores binder_ty with every nested refinement brace replaced by the brace's own binder type — strip_refinement_braces does this recursively, so Pair<{ v: i32 | v > 0 }> ends up stored as Pair<i32>, valid in <#binder_ty as thrust_models::Model>::Ty. The nested refinement isn't lost: it's still discovered by parse_refined_type_annotations and emitted as its own annotation at the appropriate position.

Added a refine_param_nested_binder pass/fail pair using { q: Pair<{ v: i32 | v > 0 }> | true }; without the fix the file doesn't compile at all.

Generated by Claude Code

Agreed — the separate strip_refinement_braces was a second traversal of the same tokens. Folded into parse_refined_type_annotations in 1f35265: it now returns (annotations, stripped_tokens), where the stripped form is rebuilt as it descends (the brace case yields its binder type as the stripped form; the reference/generic cases reassemble around their recursively-stripped children). strip_refinement_braces is gone.

Generated by Claude Code

… from binder type Address two reviewer findings in parse_refined_type_annotations: - It previously only recognized refined generics when the token stream started with `Ident <` directly, silently missing common spellings like `std::vec::Vec<{..}>`, `crate::Pair<{..}>`, and `&Vec<{..}>`. Walk through path segments to the final ident, and treat a leading `&` (with optional lifetime and `mut`) as a TypeArg(0) step into the pointee. - build_formula_fn used the binder type's tokens verbatim in a Rust type position (`<#binder_ty as Model>::Ty`), which is ill-formed when the binder type itself contains nested refinement braces such as `Pair<{ v: i32 | v > 0 }>`. The parser now stores binder_ty with every nested refinement brace replaced by the brace's binder type, yielding a valid Rust type at emission while still recording the nested annotations (at their own positions) separately. Inline the now-redundant parse_refined_type helper into the brace arm of parse_refined_type_annotations. Add pass/fail tests for each fix: - refine_param_path_qualified: `crate::Pair<{ v: i32 | v > 0 }>`. - refine_param_nested_binder: `{ q: Pair<{ v: i32 | v > 0 }> | true }`. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

Address two follow-ups on the review-fix commit: - The path-walking loop was over-careful: at this layer the only thing that matters is whether tokens contain a `<` whose args might host refinements; the prefix is opaque. Replace the loop with a single search for the first top-level `<`, which covers paths (`crate::Pair<..>`), unqualified names (`Vec<..>`), and `dyn` / `impl` prefixes without enumerating them. - The separate strip_refinement_braces was a second recursion over the same tokens. Fold it into parse_refined_type_annotations so each call returns the annotations it found together with the type expression rewritten as plain Rust (every refinement brace replaced by its binder type). Drop strip_refinement_braces. https://claude.ai/code/session_01Km9xwaVaGQjnAy1iHsPewa

claude added 16 commits June 2, 2026 16:19

coord-e force-pushed the claude/eager-lovelace-8wLLI branch from 1972402 to d115126 Compare June 2, 2026 16:21

coord-e marked this pull request as ready for review June 2, 2026 16:22

coord-e requested a review from Copilot June 2, 2026 16:22

Copilot started reviewing on behalf of coord-e June 2, 2026 16:22 View session

Copilot AI reviewed Jun 2, 2026

View reviewed changes

claude added 2 commits June 2, 2026 16:38

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

Add param/ret/sig refinement-type annotations via thrust_macros#98
coord-e wants to merge 18 commits into
mainfrom
claude/eager-lovelace-8wLLI

coord-e commented May 26, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

coord-e Jun 2, 2026

Uh oh!

coord-e Jun 3, 2026

Uh oh!

coord-e Jun 2, 2026

Uh oh!

coord-e Jun 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

coord-e commented May 26, 2026

Summary

Design

Changes

Verification

Known limitation (pre-existing, not introduced here)

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

Test plan

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

coord-e Jun 2, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Jun 3, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Jun 2, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Jun 3, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants