From 154e4a98fdbd75d1e6ef7bddba8dd4e62ad9e5cd Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 13 Aug 2026 15:12:23 +0000 Subject: [PATCH 1/4] Match the receiver of pre!/post! to the closure's function type A closure's pre- and postcondition are over its upvars as its body receives them, so a closure that mutates them takes them behind a `Mut` while one that only reads them takes the upvars themselves. `pre!(f(..))`/`post!(f(..), r)` applied them to whatever shape the specification names the closure by: a closure value gave the bare upvars, and a `&mut` to a closure gave a `Mut` where the upvars themselves are expected. Either mismatch emitted a predicate variable at a sort other than its declaration, which the solver rejects before producing a verdict. Adapt the receiver term to the first parameter of the closure's function type: a closure value stands for upvars the call leaves as they are, and a `&mut` to a closure contributes the upvars it holds on entry. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_0192XpBfrsKiGya1e3t3Cj84 --- src/analyze/annot_fn.rs | 36 +++++++++++++++++-- tests/ui/fail/closure_mut_capture_pre_post.rs | 19 ++++++++++ tests/ui/fail/closure_ref_mut_pre_post.rs | 16 +++++++++ tests/ui/pass/closure_captures_fn_once.rs | 3 +- tests/ui/pass/closure_mut_capture_pre_post.rs | 20 +++++++++++ tests/ui/pass/closure_ref_mut_pre_post.rs | 17 +++++++++ 6 files changed, 107 insertions(+), 4 deletions(-) create mode 100644 tests/ui/fail/closure_mut_capture_pre_post.rs create mode 100644 tests/ui/fail/closure_ref_mut_pre_post.rs create mode 100644 tests/ui/pass/closure_mut_capture_pre_post.rs create mode 100644 tests/ui/pass/closure_ref_mut_pre_post.rs diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 1eea3402..7c3311ee 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -416,6 +416,38 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { } } + /// Whether the receiver denotes the mutable-reference model of a closure (`&mut F` in the + /// specified signature) rather than the closure itself. + fn is_mut_receiver(&self, ty: mir_ty::Ty<'tcx>) -> bool { + matches!( + ty.kind(), + mir_ty::TyKind::Adt(adt, _) if Some(adt.did()) == self.def_ids.mut_model() + ) + } + + /// The receiver term to supply as the closure's environment, which is the first parameter of + /// its contract. + /// + /// A closure that mutates its environment receives it behind a `Mut` holding the environment + /// on entry and on exit, while a specification names the closure either by value or through a + /// `&mut`, so the two shapes need not agree. A closure value stands for an environment that + /// the call leaves as it is, and a `&mut` to a closure contributes the environment it holds on + /// entry. + fn closure_receiver_term( + &self, + receiver: &'tcx rustc_hir::Expr<'tcx>, + fn_ty: &rty::FunctionType, + ) -> chc::Term { + let env_ty = &fn_ty.params[rty::FunctionParamIdx::from(0usize)].ty; + let receiver_is_mut = self.is_mut_receiver(self.expr_ty(receiver)); + let term = self.to_term(receiver); + match (env_ty.is_mut(), receiver_is_mut) { + (true, false) => chc::Term::mut_(term.clone(), term), + (false, true) => term.mut_current(), + _ => term, + } + } + /// Resolves the [`rty::FunctionType`] of the closure contract referred to by the receiver. /// /// The receiver type is instantiated to the actual closure type in the formula function; its @@ -467,7 +499,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { "closure precondition arity mismatch: closure takes {} argument(s)", fn_ty.params.len() - 1 ); - let param_args: Vec<_> = std::iter::once(self.to_term(receiver)) + let param_args: Vec<_> = std::iter::once(self.closure_receiver_term(receiver, &fn_ty)) .chain(logical_args) .collect(); FormulaOrTerm::Formula(fn_ty.precondition_formula(¶m_args)) @@ -497,7 +529,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { "closure postcondition arity mismatch: closure takes {} argument(s)", fn_ty.params.len() - 1 ); - let param_args: Vec<_> = std::iter::once(self.to_term(receiver)) + let param_args: Vec<_> = std::iter::once(self.closure_receiver_term(receiver, &fn_ty)) .chain(logical_args) .collect(); let result = self.to_term(result); diff --git a/tests/ui/fail/closure_mut_capture_pre_post.rs b/tests/ui/fail/closure_mut_capture_pre_post.rs new file mode 100644 index 00000000..4db0b583 --- /dev/null +++ b/tests/ui/fail/closure_mut_capture_pre_post.rs @@ -0,0 +1,19 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +#[thrust_macros::requires(thrust_macros::pre!(f()))] +#[thrust_macros::ensures(thrust_macros::post!(f(), result))] +fn call i64>(mut f: F) -> i64 { + f() +} + +fn main() { + let mut cnt: i64 = 0; + let f = || -> i64 { + cnt += 1; + cnt + }; + let r = call(f); + // `f` increments `cnt` once, so `r == 1` + assert!(r == 2); +} diff --git a/tests/ui/fail/closure_ref_mut_pre_post.rs b/tests/ui/fail/closure_ref_mut_pre_post.rs new file mode 100644 index 00000000..e409ee6a --- /dev/null +++ b/tests/ui/fail/closure_ref_mut_pre_post.rs @@ -0,0 +1,16 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +#[thrust_macros::requires(thrust_macros::pre!(f()))] +#[thrust_macros::ensures(thrust_macros::post!(f(), result))] +fn call i64>(f: &mut F) -> i64 { + f() +} + +fn main() { + let k: i64 = 1; + let mut f = || -> i64 { k }; + let r = call(&mut f); + // `f` returns `k`, which is 1 + assert!(r == 2); +} diff --git a/tests/ui/pass/closure_captures_fn_once.rs b/tests/ui/pass/closure_captures_fn_once.rs index a9115dbe..49d919a2 100644 --- a/tests/ui/pass/closure_captures_fn_once.rs +++ b/tests/ui/pass/closure_captures_fn_once.rs @@ -2,8 +2,7 @@ //@compile-flags: -C debug-assertions=off // Passed straight to `apply` to keep the closure `FnOnce`: binding it to a `let` first -// makes it `FnMut`, and `pre!`/`post!` hand a `FnMut` closure upvars stripped of their -// `Mut`. +// makes it `FnMut`, whose contract holds the captures behind another `Mut`. #[thrust_macros::requires(thrust_macros::pre!(f(x)))] #[thrust_macros::ensures(thrust_macros::post!(f(x), result))] fn apply i32>(x: i32, f: F) -> i32 { diff --git a/tests/ui/pass/closure_mut_capture_pre_post.rs b/tests/ui/pass/closure_mut_capture_pre_post.rs new file mode 100644 index 00000000..8f78b296 --- /dev/null +++ b/tests/ui/pass/closure_mut_capture_pre_post.rs @@ -0,0 +1,20 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +// A closure that mutates a capture receives its environment behind a `Mut`, while the +// higher-order function names the closure by value in `pre!`/`post!`. +#[thrust_macros::requires(thrust_macros::pre!(f()))] +#[thrust_macros::ensures(thrust_macros::post!(f(), result))] +fn call i64>(mut f: F) -> i64 { + f() +} + +fn main() { + let mut cnt: i64 = 0; + let f = || -> i64 { + cnt += 1; + cnt + }; + let r = call(f); + assert!(r == 1); +} diff --git a/tests/ui/pass/closure_ref_mut_pre_post.rs b/tests/ui/pass/closure_ref_mut_pre_post.rs new file mode 100644 index 00000000..96e81f36 --- /dev/null +++ b/tests/ui/pass/closure_ref_mut_pre_post.rs @@ -0,0 +1,17 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +// The higher-order function names the closure through a `&mut` in `pre!`/`post!`, while a +// closure that only reads its captures receives its environment as it is. +#[thrust_macros::requires(thrust_macros::pre!(f()))] +#[thrust_macros::ensures(thrust_macros::post!(f(), result))] +fn call i64>(f: &mut F) -> i64 { + f() +} + +fn main() { + let k: i64 = 1; + let mut f = || -> i64 { k }; + let r = call(&mut f); + assert!(r == 1); +} From 7ba313a343d8598fd4e416f152454bdf12f614b0 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 13 Aug 2026 16:57:25 +0000 Subject: [PATCH 2/4] Test the by-value closure receiver built with Mut::new Naming the closure by value in `post!` leaves its environment as the call found it, so it cannot carry the environment from one call to the next. Building the receiver with `Mut::new` names that environment, which works for a closure held by value as much as for one held behind a `&mut`. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_0192XpBfrsKiGya1e3t3Cj84 --- .../fail/closure_receiver_mut_model_byval.rs | 28 +++++++++++++++++ .../pass/closure_receiver_mut_model_byval.rs | 30 +++++++++++++++++++ 2 files changed, 58 insertions(+) create mode 100644 tests/ui/fail/closure_receiver_mut_model_byval.rs create mode 100644 tests/ui/pass/closure_receiver_mut_model_byval.rs diff --git a/tests/ui/fail/closure_receiver_mut_model_byval.rs b/tests/ui/fail/closure_receiver_mut_model_byval.rs new file mode 100644 index 00000000..fd78c749 --- /dev/null +++ b/tests/ui/fail/closure_receiver_mut_model_byval.rs @@ -0,0 +1,28 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +use thrust_models::{ + exists, + model::{Int, Mut}, +}; + +#[thrust_macros::ensures(exists(|g, h, i: Int| + thrust_macros::post!(Mut::new(f, g)(), i) + && thrust_macros::post!(Mut::new(g, h)(), result) +))] +fn call_twice i64>(mut f: F) -> i64 { + f(); + f() +} + +fn main() { + let mut cnt: i64 = 0; + let f = move || -> i64 { + cnt += 1; + cnt + }; + let r = call_twice(f); + // `f` increments `cnt` on each of the two calls, so `r == 2` + assert!(r == 3); +} diff --git a/tests/ui/pass/closure_receiver_mut_model_byval.rs b/tests/ui/pass/closure_receiver_mut_model_byval.rs new file mode 100644 index 00000000..69b5d159 --- /dev/null +++ b/tests/ui/pass/closure_receiver_mut_model_byval.rs @@ -0,0 +1,30 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +use thrust_models::{ + exists, + model::{Int, Mut}, +}; + +// Naming the closure by value leaves its environment as the call found it, which cannot +// carry the environment from one call to the next. `Mut::new` builds the receiver instead, +// naming the environment between the two calls. +#[thrust_macros::ensures(exists(|g, h, i: Int| + thrust_macros::post!(Mut::new(f, g)(), i) + && thrust_macros::post!(Mut::new(g, h)(), result) +))] +fn call_twice i64>(mut f: F) -> i64 { + f(); + f() +} + +fn main() { + let mut cnt: i64 = 0; + let f = move || -> i64 { + cnt += 1; + cnt + }; + let r = call_twice(f); + assert!(r == 2); +} From 4122e6175ce985d0e607d61ff5b4e94a4128e894 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 14 Aug 2026 02:48:45 +0000 Subject: [PATCH 3/4] Say upvars and function type `upvars` is what the rest of the codebase calls the values a closure carries, from `tupled_upvars_ty` down to the existing closure tests, and it does not collide with the translator's own variable environment. The closure's pre- and postcondition live in its `rty::FunctionType`, which names the same thing the surrounding code already reaches for. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_0192XpBfrsKiGya1e3t3Cj84 --- src/analyze/annot_fn.rs | 17 ++++++++--------- tests/ui/pass/closure_captures_fn_once.rs | 2 +- tests/ui/pass/closure_mut_capture_pre_post.rs | 2 +- .../ui/pass/closure_receiver_mut_model_byval.rs | 6 +++--- tests/ui/pass/closure_ref_mut_pre_post.rs | 2 +- 5 files changed, 14 insertions(+), 15 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 7c3311ee..c46d528b 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -425,23 +425,22 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { ) } - /// The receiver term to supply as the closure's environment, which is the first parameter of - /// its contract. + /// The receiver term to supply as the closure's upvars, which are the first parameter of its + /// [`rty::FunctionType`]. /// - /// A closure that mutates its environment receives it behind a `Mut` holding the environment - /// on entry and on exit, while a specification names the closure either by value or through a - /// `&mut`, so the two shapes need not agree. A closure value stands for an environment that - /// the call leaves as it is, and a `&mut` to a closure contributes the environment it holds on - /// entry. + /// A closure that mutates its upvars receives them behind a `Mut` holding the upvars on entry + /// and on exit, while a specification names the closure either by value or through a `&mut`, + /// so the two shapes need not agree. A closure value stands for upvars that the call leaves + /// as they are, and a `&mut` to a closure contributes the upvars it holds on entry. fn closure_receiver_term( &self, receiver: &'tcx rustc_hir::Expr<'tcx>, fn_ty: &rty::FunctionType, ) -> chc::Term { - let env_ty = &fn_ty.params[rty::FunctionParamIdx::from(0usize)].ty; + let upvars_ty = &fn_ty.params[rty::FunctionParamIdx::from(0usize)].ty; let receiver_is_mut = self.is_mut_receiver(self.expr_ty(receiver)); let term = self.to_term(receiver); - match (env_ty.is_mut(), receiver_is_mut) { + match (upvars_ty.is_mut(), receiver_is_mut) { (true, false) => chc::Term::mut_(term.clone(), term), (false, true) => term.mut_current(), _ => term, diff --git a/tests/ui/pass/closure_captures_fn_once.rs b/tests/ui/pass/closure_captures_fn_once.rs index 49d919a2..bac7d0ec 100644 --- a/tests/ui/pass/closure_captures_fn_once.rs +++ b/tests/ui/pass/closure_captures_fn_once.rs @@ -2,7 +2,7 @@ //@compile-flags: -C debug-assertions=off // Passed straight to `apply` to keep the closure `FnOnce`: binding it to a `let` first -// makes it `FnMut`, whose contract holds the captures behind another `Mut`. +// makes it `FnMut`, which holds its upvars behind another `Mut`. #[thrust_macros::requires(thrust_macros::pre!(f(x)))] #[thrust_macros::ensures(thrust_macros::post!(f(x), result))] fn apply i32>(x: i32, f: F) -> i32 { diff --git a/tests/ui/pass/closure_mut_capture_pre_post.rs b/tests/ui/pass/closure_mut_capture_pre_post.rs index 8f78b296..890c02ba 100644 --- a/tests/ui/pass/closure_mut_capture_pre_post.rs +++ b/tests/ui/pass/closure_mut_capture_pre_post.rs @@ -1,7 +1,7 @@ //@check-pass //@compile-flags: -C debug-assertions=off -// A closure that mutates a capture receives its environment behind a `Mut`, while the +// A closure that mutates a capture receives its upvars behind a `Mut`, while the // higher-order function names the closure by value in `pre!`/`post!`. #[thrust_macros::requires(thrust_macros::pre!(f()))] #[thrust_macros::ensures(thrust_macros::post!(f(), result))] diff --git a/tests/ui/pass/closure_receiver_mut_model_byval.rs b/tests/ui/pass/closure_receiver_mut_model_byval.rs index 69b5d159..1c242719 100644 --- a/tests/ui/pass/closure_receiver_mut_model_byval.rs +++ b/tests/ui/pass/closure_receiver_mut_model_byval.rs @@ -7,9 +7,9 @@ use thrust_models::{ model::{Int, Mut}, }; -// Naming the closure by value leaves its environment as the call found it, which cannot -// carry the environment from one call to the next. `Mut::new` builds the receiver instead, -// naming the environment between the two calls. +// Naming the closure by value leaves its upvars as the call found them, which cannot carry +// the upvars from one call to the next. `Mut::new` builds the receiver instead, naming the +// upvars between the two calls. #[thrust_macros::ensures(exists(|g, h, i: Int| thrust_macros::post!(Mut::new(f, g)(), i) && thrust_macros::post!(Mut::new(g, h)(), result) diff --git a/tests/ui/pass/closure_ref_mut_pre_post.rs b/tests/ui/pass/closure_ref_mut_pre_post.rs index 96e81f36..c61a17cc 100644 --- a/tests/ui/pass/closure_ref_mut_pre_post.rs +++ b/tests/ui/pass/closure_ref_mut_pre_post.rs @@ -2,7 +2,7 @@ //@compile-flags: -C debug-assertions=off // The higher-order function names the closure through a `&mut` in `pre!`/`post!`, while a -// closure that only reads its captures receives its environment as it is. +// closure that only reads its captures receives its upvars as they are. #[thrust_macros::requires(thrust_macros::pre!(f()))] #[thrust_macros::ensures(thrust_macros::post!(f(), result))] fn call i64>(f: &mut F) -> i64 { From f6f3192e7025da2fed4e3d74393b0d76161512dd Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 14 Aug 2026 07:50:50 +0000 Subject: [PATCH 4/4] Bridge the rust-call receiver in the three cases it differs Comparing whether each side is a `Mut` conflates the question with what the answer is for: the specification names the closure by what it holds, the body takes it as its rust-call receiver, and the difference is closed by the same three steps `RustCallVisitor` performs on the argument of a call. A closure value is borrowed as `&{closure}` or as `&mut {closure}`, and a `&mut {closure}` is reborrowed as `&{closure}`. Nothing is done otherwise: a receiver that already carries a `Mut` for a body that takes one keeps it, and with it the upvars the call leaves behind, which the previous shape spent on a `Mut` rebuilt from the entry upvars alone. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_0192XpBfrsKiGya1e3t3Cj84 --- src/analyze/annot_fn.rs | 42 ++++++++++++++++++++++------------------- 1 file changed, 23 insertions(+), 19 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index c46d528b..f7eb1534 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -416,33 +416,37 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { } } - /// Whether the receiver denotes the mutable-reference model of a closure (`&mut F` in the - /// specified signature) rather than the closure itself. - fn is_mut_receiver(&self, ty: mir_ty::Ty<'tcx>) -> bool { - matches!( - ty.kind(), - mir_ty::TyKind::Adt(adt, _) if Some(adt.did()) == self.def_ids.mut_model() - ) - } - - /// The receiver term to supply as the closure's upvars, which are the first parameter of its - /// [`rty::FunctionType`]. + /// The receiver term as the closure's own body takes it. /// - /// A closure that mutates its upvars receives them behind a `Mut` holding the upvars on entry - /// and on exit, while a specification names the closure either by value or through a `&mut`, - /// so the two shapes need not agree. A closure value stands for upvars that the call leaves - /// as they are, and a `&mut` to a closure contributes the upvars it holds on entry. + /// That body takes the upvars by `&`, by `&mut`, or by value, following the kind inferred + /// for the closure, while `pre!`/`post!` reach the closure through the parameter the + /// annotated function declares. A call bridges the two by borrowing the closure into the + /// receiver the body takes; the same borrow is taken here on the term. fn closure_receiver_term( &self, receiver: &'tcx rustc_hir::Expr<'tcx>, fn_ty: &rty::FunctionType, ) -> chc::Term { + let held_as = match self.expr_ty(receiver).kind() { + mir_ty::TyKind::Adt(adt, _) if Some(adt.did()) == self.def_ids.mut_model() => { + Some(rty::RefKind::Mut) + } + mir_ty::TyKind::Ref(_, _, mir_ty::Mutability::Not) => Some(rty::RefKind::Immut), + _ => None, + }; let upvars_ty = &fn_ty.params[rty::FunctionParamIdx::from(0usize)].ty; - let receiver_is_mut = self.is_mut_receiver(self.expr_ty(receiver)); + let received_as = match upvars_ty.as_pointer().map(|ty| ty.kind) { + Some(rty::PointerKind::Ref(kind)) => Some(kind), + _ => None, + }; + let term = self.to_term(receiver); - match (upvars_ty.is_mut(), receiver_is_mut) { - (true, false) => chc::Term::mut_(term.clone(), term), - (false, true) => term.mut_current(), + match (held_as, received_as) { + (None, Some(rty::RefKind::Immut)) => chc::Term::box_(term), + (None, Some(rty::RefKind::Mut)) => chc::Term::mut_(term.clone(), term), + (Some(rty::RefKind::Mut), Some(rty::RefKind::Immut)) => { + chc::Term::box_(term.mut_current()) + } _ => term, } }