style fix

Author: coord-e

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<Int-Int>.1 self_) (tuple_proj<Int-Int>.1 dist))
-            (= (tuple_proj<Int-Int>.0 self_) item)
-            (= (+ (tuple_proj<Int-Int>.0 self_) 1) (tuple_proj<Int-Int>.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);
 }

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<Int-Int>.1 self_) (tuple_proj<Int-Int>.1 dist))
-            (= (tuple_proj<Int-Int>.0 self_) item)
-            (= (+ (tuple_proj<Int-Int>.0 self_) 1) (tuple_proj<Int-Int>.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);
 }

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<WherePredicate> {
-        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));