From 5169471c8a8acdc8050f2a0a98cf8ea04e3ae1e1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 16:38:59 +0000 Subject: [PATCH 1/2] Propagate Self trait bound into invariant_context formula fns MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- tests/ui/fail/loop_invariant_trait_self.rs | 67 +++++++++++++++++++++ tests/ui/pass/loop_invariant_trait_self.rs | 68 ++++++++++++++++++++++ thrust-macros/src/invariant.rs | 47 ++++++++++++--- 3 files changed, 175 insertions(+), 7 deletions(-) create mode 100644 tests/ui/fail/loop_invariant_trait_self.rs create mode 100644 tests/ui/pass/loop_invariant_trait_self.rs diff --git a/tests/ui/fail/loop_invariant_trait_self.rs b/tests/ui/fail/loop_invariant_trait_self.rs new file mode 100644 index 00000000..8e71f8cd --- /dev/null +++ b/tests/ui/fail/loop_invariant_trait_self.rs @@ -0,0 +1,67 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 + +// Same shape as the `pass` counterpart, but the invariant asserts the predicate +// `Self::step(c, it, c)` outright. `step` relates a state to its *successor* +// (`dist.start == self.start + 1`), so it can never hold with `dist == c`: the +// invariant is not inductive and verification fails with `Unsat`. + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] +#[thrust::trusted] +fn rand() -> i64 { + unimplemented!() +} + +#[thrust_macros::context] +trait Foo { + type Item; + + #[thrust_macros::predicate] + fn step(self, item: Self::Item, dist: Self) -> bool; + + #[thrust_macros::invariant_context] + fn run(self, item: Self::Item) + where + Self: Sized, + { + let c = self; + let it = item; + while rand() == 0 { + thrust_macros::invariant!(|c: Self, it: Self::Item| Self::step(c, it, c)); + } + let _last = c; + let _last_item = it; + } +} + +#[derive(PartialEq)] +struct Range { + start: i64, + end: i64, +} + +impl thrust_models::Model for Range { + type Ty = Range; +} + +#[thrust_macros::context] +impl Foo for Range { + type Item = i64; + + #[thrust_macros::predicate] + fn step(self, item: Self::Item, dist: Self) -> bool { + // self.end == dist.end && self.start == item && self.start + 1 == dist.start + "(and + (= (tuple_proj.1 self_) (tuple_proj.1 dist)) + (= (tuple_proj.0 self_) item) + (= (+ (tuple_proj.0 self_) 1) (tuple_proj.0 dist)) + )"; + true + } +} + +fn main() { + Range { start: 0, end: 5 }.run(0); +} diff --git a/tests/ui/pass/loop_invariant_trait_self.rs b/tests/ui/pass/loop_invariant_trait_self.rs new file mode 100644 index 00000000..9024162b --- /dev/null +++ b/tests/ui/pass/loop_invariant_trait_self.rs @@ -0,0 +1,68 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 + +// A loop invariant in a *trait default method* may refer to `Self`, the trait's +// associated types (`Self::Item`) and its predicates (`Self::step`). The +// invariant is rewritten into a free `formula_fn` in which `Self` becomes a +// synthetic generic, so that generic must inherit the host `Self: Foo` bound for +// the associated type / predicate to remain resolvable. + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] +#[thrust::trusted] +fn rand() -> i64 { + unimplemented!() +} + +#[thrust_macros::context] +trait Foo { + type Item; + + #[thrust_macros::predicate] + fn step(self, item: Self::Item, dist: Self) -> bool; + + #[thrust_macros::invariant_context] + fn run(self, item: Self::Item) + where + Self: Sized, + { + let c = self; + let it = item; + while rand() == 0 { + thrust_macros::invariant!(|c: Self, it: Self::Item| Self::step(c, it, c) || true); + } + let _last = c; + let _last_item = it; + } +} + +#[derive(PartialEq)] +struct Range { + start: i64, + end: i64, +} + +impl thrust_models::Model for Range { + type Ty = Range; +} + +#[thrust_macros::context] +impl Foo for Range { + type Item = i64; + + #[thrust_macros::predicate] + fn step(self, item: Self::Item, dist: Self) -> bool { + // self.end == dist.end && self.start == item && self.start + 1 == dist.start + "(and + (= (tuple_proj.1 self_) (tuple_proj.1 dist)) + (= (tuple_proj.0 self_) item) + (= (+ (tuple_proj.0 self_) 1) (tuple_proj.0 dist)) + )"; + true + } +} + +fn main() { + Range { start: 0, end: 5 }.run(0); +} diff --git a/thrust-macros/src/invariant.rs b/thrust-macros/src/invariant.rs index a400da85..9505a351 100644 --- a/thrust-macros/src/invariant.rs +++ b/thrust-macros/src/invariant.rs @@ -117,6 +117,19 @@ impl Context { FormulaFnTypeLowering::new(&self.sig) } } + + /// When the host is a trait, the bound `synth: Trait<..>` mirroring the + /// implicit `Self: Trait` bound of a trait method, so the synthetic + /// stand-in for `Self` can still name the trait's associated types and call + /// its predicates. + fn self_trait_bound(&self, synth: &syn::Ident) -> Option { + let FnOuterItem::ItemTrait(item_trait) = self.outer.as_ref()? else { + return None; + }; + let trait_ident = &item_trait.ident; + let (_, ty_generics, _) = item_trait.generics.split_for_impl(); + Some(syn::parse_quote!(#synth: #trait_ident #ty_generics)) + } } /// Expands a predicate closure into a `#[thrust::formula_fn]` plus a marker @@ -165,20 +178,40 @@ fn expand_invariant( def_wheres.extend(type_lowering.model_where_predicates()); - // `Self` in a method context: rewrite it to a synthetic generic, then pass - // the real `Self` via turbofish (legal in expression position). + let mut body = closure.body.clone(); + + // `Self` in a method context: rewrite it to a synthetic generic everywhere + // it reaches the formula function — parameters, body, and the propagated + // where-clause predicates — then pass the real `Self` via turbofish (legal + // in expression position). if crate::tokens_contain_ident(&closure.to_token_stream(), "Self") { let synth: syn::Ident = format_ident!("__ThrustSelf"); + let mut rewriter = SelfRewriter { synth: &synth }; for param in &mut fn_params { - SelfRewriter { synth: &synth }.visit_fn_arg_mut(param); + rewriter.visit_fn_arg_mut(param); + } + rewriter.visit_expr_mut(&mut body); + for pred in &mut def_wheres { + rewriter.visit_where_predicate_mut(pred); } def_params.push(quote!(#synth)); def_wheres.extend(type_lowering.model_where_predicates_for(&synth)); + // Mirror the host's implicit `Self: Trait` bound onto the synthetic + // generic so trait associated types (`Self::Item`) and predicates + // (`Self::step`) remain resolvable on it. + if let Some(bound) = context.and_then(|context| context.self_trait_bound(&synth)) { + def_wheres.push(bound); + } turbofish_args.push(quote!(Self)); + + // Rewriting `Self` to the synthetic generic can yield predicates that + // duplicate the synthetic generic's own `Model` bounds; drop the dups. + let mut seen = std::collections::HashSet::new(); + def_wheres.retain(|pred| seen.insert(pred.to_token_stream().to_string())); } let model_ty_params = type_lowering.lower_params(&fn_params); - let body = &closure.body; + let body = &body; let id = COUNTER.fetch_add(1, Ordering::Relaxed); let name = format_ident!("_thrust_invariant_{}", id); @@ -218,9 +251,9 @@ struct SelfRewriter<'a> { impl VisitMut for SelfRewriter<'_> { fn visit_path_mut(&mut self, path: &mut syn::Path) { syn::visit_mut::visit_path_mut(self, path); - if path.leading_colon.is_none() - && path.segments.len() == 1 - && path.segments[0].ident == "Self" + // Rewrite the leading `Self` of any path, covering both the bare type + // `Self` and qualified paths such as `Self::Item` / `Self::step`. + if path.leading_colon.is_none() && path.segments.first().is_some_and(|s| s.ident == "Self") { path.segments[0].ident = self.synth.clone(); } From addc3c614ff596d3cd7fa4bb153bdc01276eb055 Mon Sep 17 00:00:00 2001 From: coord_e Date: Tue, 16 Jun 2026 22:17:56 +0900 Subject: [PATCH 2/2] style fix --- tests/ui/fail/loop_invariant_trait_self.rs | 62 ++++++++++----------- tests/ui/pass/loop_invariant_trait_self.rs | 63 ++++++++++------------ thrust-macros/src/invariant.rs | 23 +++----- 3 files changed, 62 insertions(+), 86 deletions(-) diff --git a/tests/ui/fail/loop_invariant_trait_self.rs b/tests/ui/fail/loop_invariant_trait_self.rs index 8e71f8cd..914a9214 100644 --- a/tests/ui/fail/loop_invariant_trait_self.rs +++ b/tests/ui/fail/loop_invariant_trait_self.rs @@ -2,11 +2,6 @@ //@compile-flags: -C debug-assertions=off //@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 -// Same shape as the `pass` counterpart, but the invariant asserts the predicate -// `Self::step(c, it, c)` outright. `step` relates a state to its *successor* -// (`dist.start == self.start + 1`), so it can never hold with `dist == c`: the -// invariant is not inductive and verification fails with `Unsat`. - #[thrust_macros::requires(true)] #[thrust_macros::ensures(true)] #[thrust::trusted] @@ -15,53 +10,50 @@ fn rand() -> i64 { } #[thrust_macros::context] -trait Foo { - type Item; - +trait Gauge { #[thrust_macros::predicate] - fn step(self, item: Self::Item, dist: Self) -> bool; + fn invariant(x: i32) -> bool; + + fn update(&mut self) -> i32; #[thrust_macros::invariant_context] - fn run(self, item: Self::Item) - where - Self: Sized, - { - let c = self; - let it = item; + fn run(&mut self) -> i32 { + let mut state = 0; while rand() == 0 { - thrust_macros::invariant!(|c: Self, it: Self::Item| Self::step(c, it, c)); + state = self.update(); + thrust_macros::invariant!(|state: i32| Self::invariant(state)); } - let _last = c; - let _last_item = it; + state } } #[derive(PartialEq)] -struct Range { - start: i64, - end: i64, +struct Counter { + value: i32, } -impl thrust_models::Model for Range { - type Ty = Range; +impl thrust_models::Model for Counter { + type Ty = Counter; } #[thrust_macros::context] -impl Foo for Range { - type Item = i64; - +impl Gauge for Counter { #[thrust_macros::predicate] - fn step(self, item: Self::Item, dist: Self) -> bool { - // self.end == dist.end && self.start == item && self.start + 1 == dist.start - "(and - (= (tuple_proj.1 self_) (tuple_proj.1 dist)) - (= (tuple_proj.0 self_) item) - (= (+ (tuple_proj.0 self_) 1) (tuple_proj.0 dist)) - )"; - true + fn invariant(x: i32) -> bool { + "(>= x 0)"; true + } + + fn update(&mut self) -> i32 { + if self.value < 0 { + self.value *= -1; + } else { + self.value -= 1; + } + self.value } } fn main() { - Range { start: 0, end: 5 }.run(0); + let mut c = Counter { value: 0 }; + assert!(c.run() >= 0); } diff --git a/tests/ui/pass/loop_invariant_trait_self.rs b/tests/ui/pass/loop_invariant_trait_self.rs index 9024162b..5047710b 100644 --- a/tests/ui/pass/loop_invariant_trait_self.rs +++ b/tests/ui/pass/loop_invariant_trait_self.rs @@ -2,12 +2,6 @@ //@compile-flags: -C debug-assertions=off //@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60 -// A loop invariant in a *trait default method* may refer to `Self`, the trait's -// associated types (`Self::Item`) and its predicates (`Self::step`). The -// invariant is rewritten into a free `formula_fn` in which `Self` becomes a -// synthetic generic, so that generic must inherit the host `Self: Foo` bound for -// the associated type / predicate to remain resolvable. - #[thrust_macros::requires(true)] #[thrust_macros::ensures(true)] #[thrust::trusted] @@ -16,53 +10,50 @@ fn rand() -> i64 { } #[thrust_macros::context] -trait Foo { - type Item; - +trait Gauge { #[thrust_macros::predicate] - fn step(self, item: Self::Item, dist: Self) -> bool; + fn invariant(x: i32) -> bool; + + fn update(&mut self) -> i32; #[thrust_macros::invariant_context] - fn run(self, item: Self::Item) - where - Self: Sized, - { - let c = self; - let it = item; + fn run(&mut self) -> i32 { + let mut state = 0; while rand() == 0 { - thrust_macros::invariant!(|c: Self, it: Self::Item| Self::step(c, it, c) || true); + state = self.update(); + thrust_macros::invariant!(|state: i32| Self::invariant(state)); } - let _last = c; - let _last_item = it; + state } } #[derive(PartialEq)] -struct Range { - start: i64, - end: i64, +struct Counter { + value: i32, } -impl thrust_models::Model for Range { - type Ty = Range; +impl thrust_models::Model for Counter { + type Ty = Counter; } #[thrust_macros::context] -impl Foo for Range { - type Item = i64; - +impl Gauge for Counter { #[thrust_macros::predicate] - fn step(self, item: Self::Item, dist: Self) -> bool { - // self.end == dist.end && self.start == item && self.start + 1 == dist.start - "(and - (= (tuple_proj.1 self_) (tuple_proj.1 dist)) - (= (tuple_proj.0 self_) item) - (= (+ (tuple_proj.0 self_) 1) (tuple_proj.0 dist)) - )"; - true + fn invariant(x: i32) -> bool { + "(>= x 0)"; true + } + + fn update(&mut self) -> i32 { + if self.value < 0 { + self.value *= -1; + } else { + self.value += 1; + } + self.value } } fn main() { - Range { start: 0, end: 5 }.run(0); + let mut c = Counter { value: 0 }; + assert!(c.run() >= 0); } diff --git a/thrust-macros/src/invariant.rs b/thrust-macros/src/invariant.rs index 9505a351..24caf754 100644 --- a/thrust-macros/src/invariant.rs +++ b/thrust-macros/src/invariant.rs @@ -117,19 +117,6 @@ impl Context { FormulaFnTypeLowering::new(&self.sig) } } - - /// When the host is a trait, the bound `synth: Trait<..>` mirroring the - /// implicit `Self: Trait` bound of a trait method, so the synthetic - /// stand-in for `Self` can still name the trait's associated types and call - /// its predicates. - fn self_trait_bound(&self, synth: &syn::Ident) -> Option { - let FnOuterItem::ItemTrait(item_trait) = self.outer.as_ref()? else { - return None; - }; - let trait_ident = &item_trait.ident; - let (_, ty_generics, _) = item_trait.generics.split_for_impl(); - Some(syn::parse_quote!(#synth: #trait_ident #ty_generics)) - } } /// Expands a predicate closure into a `#[thrust::formula_fn]` plus a marker @@ -186,6 +173,8 @@ fn expand_invariant( // in expression position). if crate::tokens_contain_ident(&closure.to_token_stream(), "Self") { let synth: syn::Ident = format_ident!("__ThrustSelf"); + def_wheres.push(syn::parse_quote!(#synth: ?Sized)); + let mut rewriter = SelfRewriter { synth: &synth }; for param in &mut fn_params { rewriter.visit_fn_arg_mut(param); @@ -199,8 +188,12 @@ fn expand_invariant( // Mirror the host's implicit `Self: Trait` bound onto the synthetic // generic so trait associated types (`Self::Item`) and predicates // (`Self::step`) remain resolvable on it. - if let Some(bound) = context.and_then(|context| context.self_trait_bound(&synth)) { - def_wheres.push(bound); + 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)); } turbofish_args.push(quote!(Self));