Propagate Self trait bound into invariant_context formula fns#131
Conversation
A loop invariant inside a trait default method is rewritten into a free `formula_fn` in which `Self` is replaced by a synthetic generic (`__ThrustSelf`) instantiated with the real `Self` via turbofish. The rewrite previously only touched the formula function's parameters, and the synthetic generic carried no bound beyond `Model`. As a result an invariant that named a trait associated type (`Self::Item`) or called a trait predicate (`Self::step`) failed to compile (E0220 / E0599 — or E0401, since `Self` was left untouched in the body and where clause). Fix `expand_invariant` to: - rewrite `Self` to the synthetic generic in the body and the propagated where-clause predicates too (not just the parameters), and rewrite the leading segment of qualified paths like `Self::Item` / `Self::step`; - mirror the host's implicit `Self: Trait` bound onto the synthetic generic so the trait's associated types and predicates stay resolvable; - drop where-predicates that the rewrite duplicates against the synthetic generic's own `Model` bounds. Add paired pass/fail UI tests exercising a `Self`-typed loop invariant in a trait default method. https://claude.ai/code/session_01YDgGqc9Prd1Vqjy2p2Ns8H
coord-e
force-pushed
the
claude/epic-pasteur-7buhri
branch
from
7cd1949 to
addc3c6
Compare
![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: addc3c614f
ℹ️ 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".
| rewriter.visit_where_predicate_mut(pred); | ||
| } | ||
| def_params.push(quote!(#synth)); | ||
| def_wheres.extend(type_lowering.model_where_predicates_for(&synth)); |
There was a problem hiding this comment.
When an invariant closure parameter itself uses an associated type, e.g. |item: Self::Item| in a trait default method, the rewrite above turns it into __ThrustSelf::Item and lower_params will emit <__ThrustSelf::Item as thrust_models::Model>::Ty. This block only adds Model bounds for __ThrustSelf, not for any rewritten projections, so such invariants still fail to compile unless the trait separately constrains every associated type as Model; the macro needs to propagate projection bounds for the rewritten closure parameter types as well.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Pull request overview
This PR fixes #[thrust_macros::invariant_context] expansion for loop invariants inside trait default methods by correctly propagating Self usage into the generated #[thrust::formula_fn] context, ensuring associated types and trait predicates remain resolvable after lowering.
Changes:
- Rewrite
Self→__ThrustSelfnot only in invariant formula parameters, but also in the formula body and propagated where-predicates. - Enhance
SelfRewriterto rewrite the leadingSelfsegment in qualified paths (e.g.,Self::Item,Self::step). - Add UI tests covering
Self-typed loop invariants in trait default methods (pass + expected Unsat fail).
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| thrust-macros/src/invariant.rs | Expands Self rewriting to body/where-preds, updates SelfRewriter, and mirrors the enclosing trait bound onto __ThrustSelf. |
| tests/ui/pass/loop_invariant_trait_self.rs | New passing UI test for trait default method invariant referring to Self-trait predicate. |
| tests/ui/fail/loop_invariant_trait_self.rs | New failing UI test expecting Unsat for an intentionally too-strong invariant in the same scenario. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| if let Some(FnOuterItem::ItemTrait(item_trait)) = | ||
| context.and_then(|context| context.outer.as_ref()) | ||
| { | ||
| let trait_ident = &item_trait.ident; | ||
| let (_, ty_generics, _) = item_trait.generics.split_for_impl(); | ||
| def_wheres.push(syn::parse_quote!(#synth: #trait_ident #ty_generics)); | ||
| } |
follow-up of #99
Problem
A loop invariant inside a trait default method can refer to
Self, the trait's associated types (Self::Item) and its predicates (Self::step).#[thrust_macros::invariant_context]rewrites such aninvariant!into_invariant_with_context!, which lowers it to a free#[thrust::formula_fn]whereSelfis replaced by a synthetic generic__ThrustSelf(instantiated with the realSelfvia turbofish, legal in expression position).The rewrite was incomplete:
SelfRewriteronly visited the formula function's parameters, leavingSelfuntouched in the body and in the propagated where-clause predicates.Self, not the leading segment ofSelf::Item/Self::step.__ThrustSelfcarried no bound beyondModel— in particular not the host's implicitSelf: Footrait bound.So an invariant naming a trait associated type or predicate failed to compile.
Fix
In
expand_invariant:Self→__ThrustSelfin the body and the propagated where-clause predicates too, not just the parameters.SelfRewriternow rewrites the leading segment of any path, covering both bareSelfand qualifiedSelf::Item/Self::step.Self: Traitbound onto the synthetic generic, so the trait's associated types and predicates stay resolvable.Modelbounds.Tests
Paired UI tests exercising a
Self-typed loop invariant in a trait default method (associated type + predicate):tests/ui/pass/loop_invariant_trait_self.rs— verifies (//@check-pass).tests/ui/fail/loop_invariant_trait_self.rs— too-strong invariant, fails withUnsat.Both fail to compile without the fix (
E0401), confirming they cover the bug.Verification
Ran the full suite locally with the pinned CI toolchain (Z3 4.13.0 + the pinned COAR/PCSat image via Docker):
cargo test— 234 passed (was 232; +2 new tests), no regressions.cargo fmt --all -- --check— clean.cargo clippy --all-targets -- -D warnings— clean.https://claude.ai/code/session_01YDgGqc9Prd1Vqjy2p2Ns8H
Generated by Claude Code