Emit Model predicates for associated types referenced only in specs#134
Merged
Conversation
A projection like <Self::Item as Model>::Ty can appear only inside a spec/invariant body, which is not part of the method signature that model_where_predicates scanned. As a result no Self::Item: Model bound was emitted and the lowered predicate signatures failed to typecheck (E0277). Propagate associated type declarations through #[thrust_macros::context] (into_header_only now keeps associated type items) and attach the Model/PartialEq predicates for every associated type in scope of the outer impl/trait, deduplicating against the signature-scanned projections.
Pairs the trait_assoc_type_spec test by the fail/pass convention: the fail case has an unsatisfiable predicate (produces is always false) so the exists postcondition cannot be proven, while the pass case uses a satisfiable predicate (x == self.v).
After simplifying the closure to `|x|`, `Model` is no longer referenced, so the import triggered a machine-applicable unused_imports warning. ui_test switches into rustfix mode for any such warning and then fails trying to read a missing .fixed golden file.
Contributor
There was a problem hiding this comment.
Pull request overview
This PR fixes a typechecking gap in thrust-macros where Model/PartialEq bounds were not emitted for associated types referenced only inside spec/invariant bodies (not in method signatures), causing lowered predicate signatures to fail to typecheck.
Changes:
- Preserve associated
typeitems when embedding the outerimpl/traitheader via#[thrust::_outer_context(..)], and expose them viaassociated_type_idents(). - Extend
model_where_predicatesto emitT: Modeland<T as Model>::Ty: PartialEqbounds for all associated types declared by the outerimpl/trait, with deduplication. - Add UI pass/fail coverage for a trait whose
ensuresreferencesSelf::Itemonly inside the formula body.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
| thrust-macros/src/formula_fn_type_lowering.rs | Emits model predicates for outer associated types and deduplicates generated where-predicates. |
| thrust-macros/src/fn_outer_item.rs | Retains associated type items in header-only outer context and provides associated_type_idents(). |
| tests/ui/pass/trait_assoc_type_spec.rs | Adds a passing UI test ensuring associated types used only in specs get required bounds. |
| tests/ui/fail/trait_assoc_type_spec.rs | Adds a failing UI test validating the expected solver failure mode (Unsat). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: cd15db92d1
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
A GAT (`type Item<U>;`) requires generic arguments, so fabricating a bare `Self::Item: Model` bound from it is ill-formed (E0107) and rejects the macro expansion before verification. Only enumerate associated types without generic parameters; GATs are left as a TODO.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
model_where_predicatesonly scanned the method signature (sig.inputs/sig.output) for associated-type projections. A projection like<Self::Item as Model>::Tythat appears only inside a spec/invariant body (e.g. anensuresformula) was never seen, so noSelf::Item: Modelbound was emitted and the lowered predicate signatures failed to typecheck:Adding both
Self::Item: Modeland<Self::Item as Model>::Ty: PartialEq(exactly whatmodel_predicatesemits per type) clears it.Fix
Two steps:
Propagate associated item info through
#[thrust_macros::context].FnOuterItem::into_header_onlypreviously cleared all items, dropping thetype Item;declarations from the#[thrust::_outer_context(..)]header. It now retains associatedtypeitems, and a newassociated_type_idents()accessor reads them back.Attach
Model/PartialEqpredicates to every associated type in scope.model_where_predicatesnow enumerates the outerimpl/trait's associated types and emitsSelf::Item: thrust_models::Model+<Self::Item as thrust_models::Model>::Ty: PartialEqfor each — whether or not the projection appears in the signature. Results are deduplicated against the signature-scanned projections (same token-string dedup already used ininvariant.rs), and they flow correctly through the invariantSelf -> __ThrustSelfrewriting path.Tests
Adds a fail/pass test pair
trait_assoc_type_spec(a trait whoseensuresreferencesSelf::Itemonly inside the formula body):producesis unsatisfiable (false), soexists(|x| produces(*self, x))cannot be proven (Unsat).producesis satisfiable (x == self.v), so theexistsholds.Verified locally against the CI-pinned solvers (z3 4.13.0 + the COAR pcsat image): full
cargo test --test uiis green (238 passed), andcargo fmt/cargo clippy -D warningsare clean.https://claude.ai/code/session_01Juzob4ch5BFshNw9RqNtPi
Generated by Claude Code