From 026fedaaf0486fccfce11b81c15980532dab9959 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 9 Aug 2026 02:13:34 +0000 Subject: [PATCH 1/9] Let a closure specification name the closure's captured variables MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `closure!` clauses could only name the closure's arguments; its environment sat in the companion formula functions as an unnameable dummy parameter. Add a `captures` clause that restates the captured variables a clause wants to name: let f = thrust_macros::closure!( captures(n: i32), ensures(result == x + n), |x: i32| -> i32 { x + n }, ); The environment already carries the captures as a structured value — a closure's `FunctionType` takes the tupled upvars as its leading parameter — so the clause side is all that was missing. `captures` becomes a tuple pattern in the companion's environment parameter, marked `#[thrust::closure_env]`. Rather than binding the pattern positionally, the plugin matches each name against `closure_captures`: a closure captures in the order its body first uses each variable, which is not the order a clause would naturally list them in, and two captures of the same type would otherwise swap silently. Only the captures a clause names need restating, in any order. A capture is restated with the type it has where the closure is written, except that a mutable borrow is named as the `&mut` it is, so a clause can say both what the capture was on entry (`*acc`) and what it becomes (`!acc`). A shared borrow is read through instead, so adding or removing `move` does not change how a clause names the variable. Naming something the closure does not capture, restating a capture with a type of a different sort, and a capture taken field by field each report an error against the `captures` entry. Naming captures of a closure called through `&mut` reports an error too: that environment is a `Mut`, a shape the analyzer does not yet represent consistently between a closure's definition and its call sites. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01BTDWVnDzef1Kx97mHWUsTU --- src/analyze/annot.rs | 4 + src/analyze/annot_fn.rs | 116 ++++++++++++++++++++++++ tests/ui/fail/closure_captures.rs | 20 ++++ tests/ui/fail/closure_captures_mut.rs | 22 +++++ tests/ui/fail/closure_captures_order.rs | 22 +++++ tests/ui/pass/closure_captures.rs | 21 +++++ tests/ui/pass/closure_captures_mut.rs | 26 ++++++ tests/ui/pass/closure_captures_order.rs | 23 +++++ thrust-macros/src/closure.rs | 86 +++++++++++++----- 9 files changed, 319 insertions(+), 21 deletions(-) create mode 100644 tests/ui/fail/closure_captures.rs create mode 100644 tests/ui/fail/closure_captures_mut.rs create mode 100644 tests/ui/fail/closure_captures_order.rs create mode 100644 tests/ui/pass/closure_captures.rs create mode 100644 tests/ui/pass/closure_captures_mut.rs create mode 100644 tests/ui/pass/closure_captures_order.rs diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 869b9bf9..c6b7a288 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -46,6 +46,10 @@ pub fn refinement_path_path() -> [Symbol; 2] { [Symbol::intern("thrust"), Symbol::intern("refinement_path")] } +pub fn closure_env_path() -> [Symbol; 2] { + [Symbol::intern("thrust"), Symbol::intern("closure_env")] +} + pub fn model_ty_path() -> [Symbol; 3] { [ Symbol::intern("thrust"), diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 9aba2f3c..d81de20f 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -211,6 +211,10 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { fn build_env_from_params(&mut self) { for (idx, param) in self.body.params.iter().enumerate() { let param_idx = rty::FunctionParamIdx::from(idx); + if self.is_closure_env_param(param) { + self.build_env_from_captures(chc::Term::var(param_idx), param.pat); + continue; + } let mir_ty = self.pat_ty(param.pat); // `at_entry()` yields the `Inner` of a `FnParam`; classify by it so // a singleton wrapped argument collapses like any other singleton below. @@ -227,6 +231,118 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { } } + /// Whether the parameter stands in for the closure environment, as marked by + /// `#[thrust::closure_env]` on a `closure!` specification. + fn is_closure_env_param(&self, param: &rustc_hir::Param<'tcx>) -> bool { + let attr_path = analyze::annot::closure_env_path(); + self.tcx + .hir_attrs(param.hir_id) + .iter() + .any(|attr| attr.path_matches(&attr_path)) + } + + /// Binds the names of a closure specification's environment pattern to the + /// closure's captured variables. + /// + /// The pattern lists the captures a clause names, in the order it wrote them, + /// while the environment holds every capture in the order rustc chose. The two + /// are therefore matched up by name. + fn build_env_from_captures( + &mut self, + env: chc::Term, + pat: &'tcx rustc_hir::Pat<'tcx>, + ) { + let rustc_hir::PatKind::Tuple(subpats, _) = pat.kind else { + panic!( + "closure environment is expected to be a tuple pattern: {:?}", + pat + ); + }; + let closure_def_id = self.tcx.local_parent(self.local_def_id); + let captures = self.tcx.closure_captures(closure_def_id); + let closure_ty = self.tcx.type_of(closure_def_id).instantiate_identity(); + let mir_ty::TyKind::Closure(_, closure_args) = closure_ty.kind() else { + panic!("closure specification is expected to sit inside a closure"); + }; + let upvar_tys = closure_args.as_closure().upvar_tys(); + // A closure called through `&mut self` receives its environment behind a `Mut`, + // a shape the analyzer does not yet represent consistently across a closure's + // definition and its call sites. + let env_ty = self.analyzer.fn_sig(closure_def_id.to_def_id()).inputs()[0]; + if !subpats.is_empty() + && matches!( + env_ty.kind(), + mir_ty::TyKind::Ref(_, _, mir_ty::Mutability::Mut) + ) + { + self.tcx.dcx().span_fatal( + pat.span, + "this closure is called through `&mut`, so a specification cannot name its captures yet", + ); + } + for subpat in subpats { + let rustc_hir::PatKind::Binding(_, hir_id, ident, None) = subpat.kind else { + panic!("closure capture is expected to be a binding: {:?}", subpat); + }; + let Some(idx) = captures + .iter() + .position(|capture| capture.var_ident.name == ident.name) + else { + self.tcx.dcx().span_fatal( + subpat.span, + format!("`{}` is not captured by this closure", ident), + ); + }; + let term = self.capture_term( + env.clone().tuple_proj(idx), + captures[idx], + upvar_tys[idx], + subpat, + ); + self.env.insert(hir_id, term); + } + } + + /// The value a capture name stands for, reporting against `subpat` when the + /// restated type does not describe what the closure captured. + /// + /// A shared borrow is read through, so that adding or removing `move` does not + /// change how a clause names the variable. A mutable borrow is left as the `Mut` + /// it is, since a clause has to say whether it means the value on entry or the + /// one on exit. + fn capture_term( + &self, + term: chc::Term, + capture: &mir_ty::CapturedPlace<'tcx>, + upvar_ty: mir_ty::Ty<'tcx>, + subpat: &'tcx rustc_hir::Pat<'tcx>, + ) -> chc::Term { + if !capture.place.projections.is_empty() { + self.tcx.dcx().span_fatal( + subpat.span, + format!( + "`{}` is captured field by field, which a closure specification cannot name", + capture.var_ident + ), + ); + } + let (named_ty, term) = match upvar_ty.kind() { + mir_ty::TyKind::Ref(_, referent_ty, mir_ty::Mutability::Not) => { + (*referent_ty, term.box_current()) + } + _ => (upvar_ty, term), + }; + if self.type_builder.build(self.pat_ty(subpat)).to_sort() + != self.type_builder.build(named_ty).to_sort() + { + self.tcx.dcx().span_fatal( + subpat.span, + format!("`{}` is captured as `{}`", capture.var_ident, named_ty), + ); + } + term + } + fn singleton_term_for_ty( ty: &rty::Type, ) -> Option> { diff --git a/tests/ui/fail/closure_captures.rs b/tests/ui/fail/closure_captures.rs new file mode 100644 index 00000000..d18c2d69 --- /dev/null +++ b/tests/ui/fail/closure_captures.rs @@ -0,0 +1,20 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +// The declared postcondition carries the captured `n`, which is 5, so `r` is 8. +#[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 { + f(x) +} + +fn main() { + let n = 5; + let f = thrust_macros::closure!( + captures(n: i32), + ensures(result == x + n), + |x: i32| -> i32 { x + n }, + ); + let r = apply(3, f); + assert!(r == 9); +} diff --git a/tests/ui/fail/closure_captures_mut.rs b/tests/ui/fail/closure_captures_mut.rs new file mode 100644 index 00000000..046e867e --- /dev/null +++ b/tests/ui/fail/closure_captures_mut.rs @@ -0,0 +1,22 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +// The declared postcondition pins `result` to `x + 1`, which is 4. +#[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 { + f(x) +} + +fn main() { + let mut acc = 0; + let r = apply( + 3, + thrust_macros::closure!( + captures(acc: &mut i32), + ensures(result == x + 1 && !acc == *acc + 1), + |x: i32| -> i32 { acc += 1; x + acc }, + ), + ); + assert!(r == 5); +} diff --git a/tests/ui/fail/closure_captures_order.rs b/tests/ui/fail/closure_captures_order.rs new file mode 100644 index 00000000..6670bdf2 --- /dev/null +++ b/tests/ui/fail/closure_captures_order.rs @@ -0,0 +1,22 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +// `captures` lists `n` first while the closure captures `b` first; `n` still carries +// its own value, 5, so `r` is 8. +#[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 { + f(x) +} + +fn main() { + let n = 5; + let b = true; + let f = thrust_macros::closure!( + captures(n: i32, b: bool), + ensures(result == x + n), + move |x: i32| -> i32 { if b { x + n } else { x } }, + ); + let r = apply(3, f); + assert!(r == 9); +} diff --git a/tests/ui/pass/closure_captures.rs b/tests/ui/pass/closure_captures.rs new file mode 100644 index 00000000..51708fcf --- /dev/null +++ b/tests/ui/pass/closure_captures.rs @@ -0,0 +1,21 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +// A closure specification naming a captured variable. `n` is captured by reference, +// which the specification reads through: the clause names the variable, not the borrow. +#[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 { + f(x) +} + +fn main() { + let n = 5; + let f = thrust_macros::closure!( + captures(n: i32), + ensures(result == x + n), + |x: i32| -> i32 { x + n }, + ); + let r = apply(3, f); + assert!(r == 8); +} diff --git a/tests/ui/pass/closure_captures_mut.rs b/tests/ui/pass/closure_captures_mut.rs new file mode 100644 index 00000000..0d658305 --- /dev/null +++ b/tests/ui/pass/closure_captures_mut.rs @@ -0,0 +1,26 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +// A capture taken by mutable borrow is named as the `&mut` it is, so that the clause +// can say both what it was on entry (`*acc`) and what it becomes (`!acc`). +// +// The closure is passed straight to `apply`: binding it to a `let` first would have it +// called through `&mut`, which a specification cannot name its captures through yet. +#[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 { + f(x) +} + +fn main() { + let mut acc = 0; + let r = apply( + 3, + thrust_macros::closure!( + captures(acc: &mut i32), + ensures(result == x + 1 && !acc == *acc + 1), + |x: i32| -> i32 { acc += 1; x + acc }, + ), + ); + assert!(r == 4); +} diff --git a/tests/ui/pass/closure_captures_order.rs b/tests/ui/pass/closure_captures_order.rs new file mode 100644 index 00000000..8c234815 --- /dev/null +++ b/tests/ui/pass/closure_captures_order.rs @@ -0,0 +1,23 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +// The closure captures `b` before `n`, since that is the order its body first uses +// them, while `captures` lists `n` first. Matching the two up by name is what makes +// `n` resolve to the second captured value rather than the first. +#[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 { + f(x) +} + +fn main() { + let n = 5; + let b = true; + let f = thrust_macros::closure!( + captures(n: i32, b: bool), + ensures(result == x + n), + move |x: i32| -> i32 { if b { x + n } else { x } }, + ); + let r = apply(3, f); + assert!(r == 8); +} diff --git a/thrust-macros/src/closure.rs b/thrust-macros/src/closure.rs index 9c154544..8a6217ea 100644 --- a/thrust-macros/src/closure.rs +++ b/thrust-macros/src/closure.rs @@ -3,9 +3,10 @@ //! //! ```ignore //! let f = thrust_macros::closure!( +//! captures(n: i32), //! requires(x > 0), -//! ensures(result > x), -//! |x: i32| -> i32 { x + 1 }, +//! ensures(result > x + n), +//! |x: i32| -> i32 { x + n + 1 }, //! ); //! ``` //! @@ -16,6 +17,10 @@ //! `spec.rs`). Each clause is optional (an omitted one leaves that side inferred) //! and may be repeated, in which case its predicates are conjoined. //! +//! `captures` restates the captured variables a clause wants to name, with the types +//! they have outside the closure. Only the ones a clause names need restating, and in +//! any order: the plugin matches them against the closure's real captures by name. +//! //! A clause sees no threaded generic or `Self` context, so a closure in a generic //! context cannot refer to generic- or `Self`-typed values. @@ -31,11 +36,13 @@ use syn::{ use crate::FormulaFnTypeLowering; mod kw { + syn::custom_keyword!(captures); syn::custom_keyword!(requires); syn::custom_keyword!(ensures); } struct ClosureSpec { + captures: Vec, requires: Vec, ensures: Vec, closure: syn::ExprClosure, @@ -43,22 +50,30 @@ struct ClosureSpec { impl Parse for ClosureSpec { fn parse(input: ParseStream) -> syn::Result { + let mut captures = Vec::new(); let mut requires = Vec::new(); let mut ensures = Vec::new(); loop { - let clause = if input.peek(kw::requires) { - input.parse::()?; - &mut requires - } else if input.peek(kw::ensures) { - input.parse::()?; - &mut ensures + if input.peek(kw::captures) { + input.parse::()?; + let content; + parenthesized!(content in input); + captures.extend(content.parse_terminated(FnArg::parse, syn::Token![,])?); } else { - break; - }; - let content; - parenthesized!(content in input); - clause.push(content.parse()?); + let clause = if input.peek(kw::requires) { + input.parse::()?; + &mut requires + } else if input.peek(kw::ensures) { + input.parse::()?; + &mut ensures + } else { + break; + }; + let content; + parenthesized!(content in input); + clause.push(content.parse()?); + } input.parse::>()?; } @@ -66,6 +81,7 @@ impl Parse for ClosureSpec { input.parse::>()?; Ok(Self { + captures, requires, ensures, closure, @@ -86,15 +102,14 @@ pub fn expand(input: TokenStream) -> TokenStream { fn expand_closure(spec: ClosureSpec) -> syn::Result { let ClosureSpec { + captures, requires, ensures, mut closure, } = spec; - // A closure's parameters are `[env, arg1, .., argN]`, the environment being the - // closure value itself. A clause names only the arguments, so the companions take - // a dummy parameter in the environment's place to keep the positions aligned. - let mut fn_params: Vec = vec![syn::parse_quote!(_thrust_closure_env: ())]; + let env = env_param(&captures)?; + let mut arg_params: Vec = Vec::new(); for param in &closure.inputs { let syn::Pat::Type(pt) = param else { return Err(syn::Error::new_spanned( @@ -104,7 +119,7 @@ fn expand_closure(spec: ClosureSpec) -> syn::Result { }; let pat = &pt.pat; let ty = &pt.ty; - fn_params.push(syn::parse_quote!(#pat: #ty)); + arg_params.push(syn::parse_quote!(#pat: #ty)); } if !ensures.is_empty() && matches!(closure.output, syn::ReturnType::Default) { @@ -118,14 +133,21 @@ fn expand_closure(spec: ClosureSpec) -> syn::Result { // clause has none of its own. let spec_sig: syn::Signature = syn::parse_quote!(fn closure_spec()); let type_lowering = FormulaFnTypeLowering::new(&spec_sig); - let model_params = type_lowering.lower_params(&fn_params); + // A closure's parameters are `[env, arg1, .., argN]`, the environment holding its + // captures. The companions take the environment in that same leading position, so + // their parameters line up with the closure's. + let env_model = type_lowering.lower_params([&env]); + let arg_models = type_lowering.lower_params(&arg_params); let mut prelude: Vec = Vec::new(); if let Some(body) = conjoin(requires) { prelude.push(quote! { #[allow(unused_variables, non_snake_case)] #[thrust::formula_fn] - fn _thrust_closure_requires(#model_params) -> bool { + fn _thrust_closure_requires( + #[thrust::closure_env] #env_model, + #arg_models + ) -> bool { #body } @@ -138,7 +160,11 @@ fn expand_closure(spec: ClosureSpec) -> syn::Result { prelude.push(quote! { #[allow(unused_variables, non_snake_case)] #[thrust::formula_fn] - fn _thrust_closure_ensures(result: #ret_model, #model_params) -> bool { + fn _thrust_closure_ensures( + result: #ret_model, + #[thrust::closure_env] #env_model, + #arg_models + ) -> bool { #body } @@ -164,6 +190,24 @@ fn expand_closure(spec: ClosureSpec) -> syn::Result { Ok(closure) } +/// The companion parameter holding the closure environment: a tuple of the captures a +/// clause names, which the plugin matches up with the real environment by name. +fn env_param(captures: &[FnArg]) -> syn::Result { + let mut names = Vec::new(); + let mut tys = Vec::new(); + for capture in captures { + let FnArg::Typed(capture) = capture else { + return Err(syn::Error::new_spanned( + capture, + "closure! captures are written as `name: Type`", + )); + }; + names.push(&capture.pat); + tys.push(&capture.ty); + } + Ok(syn::parse_quote!((#(#names,)*): (#(#tys,)*))) +} + fn conjoin(preds: Vec) -> Option { preds .into_iter() From d0b21132d5c3a972ca48544aae6b8c6c815ae61b Mon Sep 17 00:00:00 2001 From: coord_e Date: Thu, 13 Aug 2026 20:54:02 +0900 Subject: [PATCH 2/9] style fix --- src/analyze/annot_fn.rs | 70 ++---------------------------------- thrust-macros/src/closure.rs | 4 +-- 2 files changed, 4 insertions(+), 70 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index d81de20f..b905ed55 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -249,7 +249,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { /// are therefore matched up by name. fn build_env_from_captures( &mut self, - env: chc::Term, + upvars_term: chc::Term, pat: &'tcx rustc_hir::Pat<'tcx>, ) { let rustc_hir::PatKind::Tuple(subpats, _) = pat.kind else { @@ -260,26 +260,6 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { }; let closure_def_id = self.tcx.local_parent(self.local_def_id); let captures = self.tcx.closure_captures(closure_def_id); - let closure_ty = self.tcx.type_of(closure_def_id).instantiate_identity(); - let mir_ty::TyKind::Closure(_, closure_args) = closure_ty.kind() else { - panic!("closure specification is expected to sit inside a closure"); - }; - let upvar_tys = closure_args.as_closure().upvar_tys(); - // A closure called through `&mut self` receives its environment behind a `Mut`, - // a shape the analyzer does not yet represent consistently across a closure's - // definition and its call sites. - let env_ty = self.analyzer.fn_sig(closure_def_id.to_def_id()).inputs()[0]; - if !subpats.is_empty() - && matches!( - env_ty.kind(), - mir_ty::TyKind::Ref(_, _, mir_ty::Mutability::Mut) - ) - { - self.tcx.dcx().span_fatal( - pat.span, - "this closure is called through `&mut`, so a specification cannot name its captures yet", - ); - } for subpat in subpats { let rustc_hir::PatKind::Binding(_, hir_id, ident, None) = subpat.kind else { panic!("closure capture is expected to be a binding: {:?}", subpat); @@ -293,54 +273,8 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { format!("`{}` is not captured by this closure", ident), ); }; - let term = self.capture_term( - env.clone().tuple_proj(idx), - captures[idx], - upvar_tys[idx], - subpat, - ); - self.env.insert(hir_id, term); - } - } - - /// The value a capture name stands for, reporting against `subpat` when the - /// restated type does not describe what the closure captured. - /// - /// A shared borrow is read through, so that adding or removing `move` does not - /// change how a clause names the variable. A mutable borrow is left as the `Mut` - /// it is, since a clause has to say whether it means the value on entry or the - /// one on exit. - fn capture_term( - &self, - term: chc::Term, - capture: &mir_ty::CapturedPlace<'tcx>, - upvar_ty: mir_ty::Ty<'tcx>, - subpat: &'tcx rustc_hir::Pat<'tcx>, - ) -> chc::Term { - if !capture.place.projections.is_empty() { - self.tcx.dcx().span_fatal( - subpat.span, - format!( - "`{}` is captured field by field, which a closure specification cannot name", - capture.var_ident - ), - ); - } - let (named_ty, term) = match upvar_ty.kind() { - mir_ty::TyKind::Ref(_, referent_ty, mir_ty::Mutability::Not) => { - (*referent_ty, term.box_current()) - } - _ => (upvar_ty, term), - }; - if self.type_builder.build(self.pat_ty(subpat)).to_sort() - != self.type_builder.build(named_ty).to_sort() - { - self.tcx.dcx().span_fatal( - subpat.span, - format!("`{}` is captured as `{}`", capture.var_ident, named_ty), - ); + self.env.insert(hir_id, upvars_term.clone().tuple_proj(idx)); } - term } fn singleton_term_for_ty( diff --git a/thrust-macros/src/closure.rs b/thrust-macros/src/closure.rs index 8a6217ea..a2bc5793 100644 --- a/thrust-macros/src/closure.rs +++ b/thrust-macros/src/closure.rs @@ -18,8 +18,8 @@ //! and may be repeated, in which case its predicates are conjoined. //! //! `captures` restates the captured variables a clause wants to name, with the types -//! they have outside the closure. Only the ones a clause names need restating, and in -//! any order: the plugin matches them against the closure's real captures by name. +//! they are captured by the closure. Only the ones a clause names need restating, and +//! in any order: the plugin matches them against the closure's real captures by name. //! //! A clause sees no threaded generic or `Self` context, so a closure in a generic //! context cannot refer to generic- or `Self`-typed values. From d9e96b2a9ff6564be457c37800e50029ca142c8a Mon Sep 17 00:00:00 2001 From: coord_e Date: Thu, 13 Aug 2026 22:46:26 +0900 Subject: [PATCH 3/9] fixup! Let a closure specification name the closure's captured variables --- src/analyze/annot_fn.rs | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index b905ed55..e086b7b9 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -260,20 +260,35 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { }; let closure_def_id = self.tcx.local_parent(self.local_def_id); let captures = self.tcx.closure_captures(closure_def_id); + let closure_ty = self.tcx.type_of(closure_def_id).instantiate_identity(); + let mir_ty::TyKind::Closure(_, closure_args) = closure_ty.kind() else { + panic!("closure specification is expected to sit inside a closure"); + }; + let mut upvar_terms = Vec::new(); + for i in 0..captures.len() { + let upvar_term = match closure_args.as_closure().kind() { + mir_ty::ClosureKind::Fn => upvars_term.clone().box_current().tuple_proj(i), + mir_ty::ClosureKind::FnMut => chc::Term::mut_( + upvars_term.clone().mut_current().tuple_proj(i), + upvars_term.clone().mut_final().tuple_proj(i), + ), + mir_ty::ClosureKind::FnOnce => upvars_term.clone().tuple_proj(i), + }; + upvar_terms.push(upvar_term); + } for subpat in subpats { let rustc_hir::PatKind::Binding(_, hir_id, ident, None) = subpat.kind else { panic!("closure capture is expected to be a binding: {:?}", subpat); }; - let Some(idx) = captures - .iter() - .position(|capture| capture.var_ident.name == ident.name) - else { + let Some(idx) = captures.iter().position(|capture| { + capture.var_ident.name == ident.name && capture.place.projections.is_empty() + }) else { self.tcx.dcx().span_fatal( subpat.span, format!("`{}` is not captured by this closure", ident), ); }; - self.env.insert(hir_id, upvars_term.clone().tuple_proj(idx)); + self.env.insert(hir_id, upvar_terms[idx].clone()); } } From 78564775f334f97513ef6cc48ce13942f88c8416 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 13 Aug 2026 14:12:23 +0000 Subject: [PATCH 4/9] fixup! Let a closure specification name the closure's captured variables Cover a capture named in `requires`, where the environment leads the companion's parameters instead of following `result`. The failing side calls the closure with an argument the declared precondition rules out, so the pair exercises the capture reaching the call site rather than only the closure body. --- tests/ui/fail/closure_captures_requires.rs | 22 ++++++++++++++++++++++ tests/ui/pass/closure_captures_requires.rs | 22 ++++++++++++++++++++++ 2 files changed, 44 insertions(+) create mode 100644 tests/ui/fail/closure_captures_requires.rs create mode 100644 tests/ui/pass/closure_captures_requires.rs diff --git a/tests/ui/fail/closure_captures_requires.rs b/tests/ui/fail/closure_captures_requires.rs new file mode 100644 index 00000000..45a8bb2f --- /dev/null +++ b/tests/ui/fail/closure_captures_requires.rs @@ -0,0 +1,22 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +// The declared precondition is `x > n`, and the captured `n` is 5, so calling the +// closure with 3 must fail verification. +#[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 { + f(x) +} + +fn main() { + let n = 5; + let f = thrust_macros::closure!( + captures(n: i32), + requires(x > n), + ensures(result == x + n), + |x: i32| -> i32 { x + n }, + ); + let r = apply(3, f); + assert!(r == 8); +} diff --git a/tests/ui/pass/closure_captures_requires.rs b/tests/ui/pass/closure_captures_requires.rs new file mode 100644 index 00000000..f86b1ba1 --- /dev/null +++ b/tests/ui/pass/closure_captures_requires.rs @@ -0,0 +1,22 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +// A capture named in `requires`, where the environment leads the companion's +// parameters instead of following `result` as it does for `ensures`. +#[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 { + f(x) +} + +fn main() { + let n = 5; + let f = thrust_macros::closure!( + captures(n: i32), + requires(x > n), + ensures(result == x + n), + |x: i32| -> i32 { x + n }, + ); + let r = apply(7, f); + assert!(r == 12); +} From ac0884ac2aa220409eaaaf798193c4462987b385 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 13 Aug 2026 14:16:59 +0000 Subject: [PATCH 5/9] fixup! Let a closure specification name the closure's captured variables Cover a `FnMut` closure, whose environment is a `Mut` that the capture terms distribute over. Calling it directly rather than through `pre!`/`post!` keeps the environment intact: those translate the receiver as the closure value, which carries no `Mut`, so the specification would be handed the wrong shape. The body has to prove the declared relation between the capture's entry and exit values, so the pair pins the distribution rather than only its sorts. --- tests/ui/fail/closure_captures_fn_mut.rs | 17 +++++++++++++++++ tests/ui/pass/closure_captures_fn_mut.rs | 23 +++++++++++++++++++++++ 2 files changed, 40 insertions(+) create mode 100644 tests/ui/fail/closure_captures_fn_mut.rs create mode 100644 tests/ui/pass/closure_captures_fn_mut.rs diff --git a/tests/ui/fail/closure_captures_fn_mut.rs b/tests/ui/fail/closure_captures_fn_mut.rs new file mode 100644 index 00000000..cc6b3c16 --- /dev/null +++ b/tests/ui/fail/closure_captures_fn_mut.rs @@ -0,0 +1,17 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +// The captured `acc` counts up from 0, so the first call returns 4. +fn main() { + let mut acc = 0; + let mut f = thrust_macros::closure!( + captures(acc: &mut i32), + ensures(result == x + 1 && !acc == *acc + 1), + move |x: i32| -> i32 { + acc += 1; + x + acc + }, + ); + let r = f(3); + assert!(r == 5); +} diff --git a/tests/ui/pass/closure_captures_fn_mut.rs b/tests/ui/pass/closure_captures_fn_mut.rs new file mode 100644 index 00000000..f8394d73 --- /dev/null +++ b/tests/ui/pass/closure_captures_fn_mut.rs @@ -0,0 +1,23 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +// A `FnMut` closure receives its environment as a `Mut`, so every capture carries both +// the value on entry (`*acc`) and the value on exit (`!acc`), and is restated one `&mut` +// deeper than what it is captured as. The body has to prove the relation between the +// two, which is what pins the environment down. +// +// The closure is called directly: reaching it through `pre!`/`post!` instead would hand +// the specification an environment without that `Mut`. +fn main() { + let mut acc = 0; + let mut f = thrust_macros::closure!( + captures(acc: &mut i32), + ensures(result == x + 1 && !acc == *acc + 1), + move |x: i32| -> i32 { + acc += 1; + x + acc + }, + ); + let r = f(3); + assert!(r == 4); +} From aa638ebc9ea54e55bfb8c3887936d1d0979fcabf Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 13 Aug 2026 14:20:44 +0000 Subject: [PATCH 6/9] fixup! Let a closure specification name the closure's captured variables Cover a `FnMut` closure capturing by mutable borrow, where the capture carries two `Mut` levels: the environment's, holding the slot on entry and on exit, and the borrow's, whose current value is the one a counter holds. Relating the two ends of the call therefore reads `*(!acc) == *(*acc) + 1`. --- tests/ui/fail/closure_captures_fn_mut_ref.rs | 17 +++++++++++++++++ tests/ui/pass/closure_captures_fn_mut_ref.rs | 20 ++++++++++++++++++++ 2 files changed, 37 insertions(+) create mode 100644 tests/ui/fail/closure_captures_fn_mut_ref.rs create mode 100644 tests/ui/pass/closure_captures_fn_mut_ref.rs diff --git a/tests/ui/fail/closure_captures_fn_mut_ref.rs b/tests/ui/fail/closure_captures_fn_mut_ref.rs new file mode 100644 index 00000000..776bd27d --- /dev/null +++ b/tests/ui/fail/closure_captures_fn_mut_ref.rs @@ -0,0 +1,17 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +// The captured `acc` counts up from 0, so the first call returns 4. +fn main() { + let mut acc = 0; + let mut f = thrust_macros::closure!( + captures(acc: &mut &mut i32), + ensures(result == x + 1 && *(!acc) == *(*acc) + 1), + |x: i32| -> i32 { + acc += 1; + x + acc + }, + ); + let r = f(3); + assert!(r == 5); +} diff --git a/tests/ui/pass/closure_captures_fn_mut_ref.rs b/tests/ui/pass/closure_captures_fn_mut_ref.rs new file mode 100644 index 00000000..b8871483 --- /dev/null +++ b/tests/ui/pass/closure_captures_fn_mut_ref.rs @@ -0,0 +1,20 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +// A `FnMut` closure that captures by mutable borrow carries two `Mut` levels: the outer +// one is the environment's, holding the slot on entry (`*acc`) and on exit (`!acc`), +// and the inner one is the borrow's, whose current value is what the counter holds. So +// counting up by one across the call reads `*(!acc) == *(*acc) + 1`. +fn main() { + let mut acc = 0; + let mut f = thrust_macros::closure!( + captures(acc: &mut &mut i32), + ensures(result == x + 1 && *(!acc) == *(*acc) + 1), + |x: i32| -> i32 { + acc += 1; + x + acc + }, + ); + let r = f(3); + assert!(r == 4); +} From 6f725dd97fc23db17ca845b4b9cffd8bf09294aa Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 13 Aug 2026 14:26:35 +0000 Subject: [PATCH 7/9] fixup! Let a closure specification name the closure's captured variables Keep one pair per closure kind, since that is what selects how a capture is read out of the environment, and name each pair after the kind it covers. The `Fn` pair takes over naming a capture in `requires` as well as in `ensures`, covering both companion layouts; the `FnMut` pair keeps the mutable-borrow capture, which is the richer of the two that were there. --- tests/ui/fail/closure_captures.rs | 6 +++-- tests/ui/fail/closure_captures_fn_mut.rs | 6 ++--- tests/ui/fail/closure_captures_fn_mut_ref.rs | 17 -------------- ...res_mut.rs => closure_captures_fn_once.rs} | 0 tests/ui/fail/closure_captures_order.rs | 22 ------------------ tests/ui/fail/closure_captures_requires.rs | 22 ------------------ tests/ui/pass/closure_captures.rs | 9 ++++---- tests/ui/pass/closure_captures_fn_mut.rs | 17 ++++++-------- tests/ui/pass/closure_captures_fn_mut_ref.rs | 20 ---------------- ...res_mut.rs => closure_captures_fn_once.rs} | 5 ++-- tests/ui/pass/closure_captures_order.rs | 23 ------------------- tests/ui/pass/closure_captures_requires.rs | 22 ------------------ 12 files changed, 22 insertions(+), 147 deletions(-) delete mode 100644 tests/ui/fail/closure_captures_fn_mut_ref.rs rename tests/ui/fail/{closure_captures_mut.rs => closure_captures_fn_once.rs} (100%) delete mode 100644 tests/ui/fail/closure_captures_order.rs delete mode 100644 tests/ui/fail/closure_captures_requires.rs delete mode 100644 tests/ui/pass/closure_captures_fn_mut_ref.rs rename tests/ui/pass/{closure_captures_mut.rs => closure_captures_fn_once.rs} (74%) delete mode 100644 tests/ui/pass/closure_captures_order.rs delete mode 100644 tests/ui/pass/closure_captures_requires.rs diff --git a/tests/ui/fail/closure_captures.rs b/tests/ui/fail/closure_captures.rs index d18c2d69..45a8bb2f 100644 --- a/tests/ui/fail/closure_captures.rs +++ b/tests/ui/fail/closure_captures.rs @@ -1,7 +1,8 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -// The declared postcondition carries the captured `n`, which is 5, so `r` is 8. +// The declared precondition is `x > n`, and the captured `n` is 5, so calling the +// closure with 3 must fail verification. #[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 { @@ -12,9 +13,10 @@ fn main() { let n = 5; let f = thrust_macros::closure!( captures(n: i32), + requires(x > n), ensures(result == x + n), |x: i32| -> i32 { x + n }, ); let r = apply(3, f); - assert!(r == 9); + assert!(r == 8); } diff --git a/tests/ui/fail/closure_captures_fn_mut.rs b/tests/ui/fail/closure_captures_fn_mut.rs index cc6b3c16..776bd27d 100644 --- a/tests/ui/fail/closure_captures_fn_mut.rs +++ b/tests/ui/fail/closure_captures_fn_mut.rs @@ -5,9 +5,9 @@ fn main() { let mut acc = 0; let mut f = thrust_macros::closure!( - captures(acc: &mut i32), - ensures(result == x + 1 && !acc == *acc + 1), - move |x: i32| -> i32 { + captures(acc: &mut &mut i32), + ensures(result == x + 1 && *(!acc) == *(*acc) + 1), + |x: i32| -> i32 { acc += 1; x + acc }, diff --git a/tests/ui/fail/closure_captures_fn_mut_ref.rs b/tests/ui/fail/closure_captures_fn_mut_ref.rs deleted file mode 100644 index 776bd27d..00000000 --- a/tests/ui/fail/closure_captures_fn_mut_ref.rs +++ /dev/null @@ -1,17 +0,0 @@ -//@error-in-other-file: Unsat -//@compile-flags: -C debug-assertions=off - -// The captured `acc` counts up from 0, so the first call returns 4. -fn main() { - let mut acc = 0; - let mut f = thrust_macros::closure!( - captures(acc: &mut &mut i32), - ensures(result == x + 1 && *(!acc) == *(*acc) + 1), - |x: i32| -> i32 { - acc += 1; - x + acc - }, - ); - let r = f(3); - assert!(r == 5); -} diff --git a/tests/ui/fail/closure_captures_mut.rs b/tests/ui/fail/closure_captures_fn_once.rs similarity index 100% rename from tests/ui/fail/closure_captures_mut.rs rename to tests/ui/fail/closure_captures_fn_once.rs diff --git a/tests/ui/fail/closure_captures_order.rs b/tests/ui/fail/closure_captures_order.rs deleted file mode 100644 index 6670bdf2..00000000 --- a/tests/ui/fail/closure_captures_order.rs +++ /dev/null @@ -1,22 +0,0 @@ -//@error-in-other-file: Unsat -//@compile-flags: -C debug-assertions=off - -// `captures` lists `n` first while the closure captures `b` first; `n` still carries -// its own value, 5, so `r` is 8. -#[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 { - f(x) -} - -fn main() { - let n = 5; - let b = true; - let f = thrust_macros::closure!( - captures(n: i32, b: bool), - ensures(result == x + n), - move |x: i32| -> i32 { if b { x + n } else { x } }, - ); - let r = apply(3, f); - assert!(r == 9); -} diff --git a/tests/ui/fail/closure_captures_requires.rs b/tests/ui/fail/closure_captures_requires.rs deleted file mode 100644 index 45a8bb2f..00000000 --- a/tests/ui/fail/closure_captures_requires.rs +++ /dev/null @@ -1,22 +0,0 @@ -//@error-in-other-file: Unsat -//@compile-flags: -C debug-assertions=off - -// The declared precondition is `x > n`, and the captured `n` is 5, so calling the -// closure with 3 must fail verification. -#[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 { - f(x) -} - -fn main() { - let n = 5; - let f = thrust_macros::closure!( - captures(n: i32), - requires(x > n), - ensures(result == x + n), - |x: i32| -> i32 { x + n }, - ); - let r = apply(3, f); - assert!(r == 8); -} diff --git a/tests/ui/pass/closure_captures.rs b/tests/ui/pass/closure_captures.rs index 51708fcf..f2e46f81 100644 --- a/tests/ui/pass/closure_captures.rs +++ b/tests/ui/pass/closure_captures.rs @@ -1,8 +1,8 @@ //@check-pass //@compile-flags: -C debug-assertions=off -// A closure specification naming a captured variable. `n` is captured by reference, -// which the specification reads through: the clause names the variable, not the borrow. +// A capture named in both clauses, so the environment is read from both companion +// layouts: `requires` takes it first, `ensures` takes it after `result`. #[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 { @@ -13,9 +13,10 @@ fn main() { let n = 5; let f = thrust_macros::closure!( captures(n: i32), + requires(x > n), ensures(result == x + n), |x: i32| -> i32 { x + n }, ); - let r = apply(3, f); - assert!(r == 8); + let r = apply(7, f); + assert!(r == 12); } diff --git a/tests/ui/pass/closure_captures_fn_mut.rs b/tests/ui/pass/closure_captures_fn_mut.rs index f8394d73..b8871483 100644 --- a/tests/ui/pass/closure_captures_fn_mut.rs +++ b/tests/ui/pass/closure_captures_fn_mut.rs @@ -1,19 +1,16 @@ //@check-pass //@compile-flags: -C debug-assertions=off -// A `FnMut` closure receives its environment as a `Mut`, so every capture carries both -// the value on entry (`*acc`) and the value on exit (`!acc`), and is restated one `&mut` -// deeper than what it is captured as. The body has to prove the relation between the -// two, which is what pins the environment down. -// -// The closure is called directly: reaching it through `pre!`/`post!` instead would hand -// the specification an environment without that `Mut`. +// A `FnMut` closure that captures by mutable borrow carries two `Mut` levels: the outer +// one is the environment's, holding the slot on entry (`*acc`) and on exit (`!acc`), +// and the inner one is the borrow's, whose current value is what the counter holds. So +// counting up by one across the call reads `*(!acc) == *(*acc) + 1`. fn main() { let mut acc = 0; let mut f = thrust_macros::closure!( - captures(acc: &mut i32), - ensures(result == x + 1 && !acc == *acc + 1), - move |x: i32| -> i32 { + captures(acc: &mut &mut i32), + ensures(result == x + 1 && *(!acc) == *(*acc) + 1), + |x: i32| -> i32 { acc += 1; x + acc }, diff --git a/tests/ui/pass/closure_captures_fn_mut_ref.rs b/tests/ui/pass/closure_captures_fn_mut_ref.rs deleted file mode 100644 index b8871483..00000000 --- a/tests/ui/pass/closure_captures_fn_mut_ref.rs +++ /dev/null @@ -1,20 +0,0 @@ -//@check-pass -//@compile-flags: -C debug-assertions=off - -// A `FnMut` closure that captures by mutable borrow carries two `Mut` levels: the outer -// one is the environment's, holding the slot on entry (`*acc`) and on exit (`!acc`), -// and the inner one is the borrow's, whose current value is what the counter holds. So -// counting up by one across the call reads `*(!acc) == *(*acc) + 1`. -fn main() { - let mut acc = 0; - let mut f = thrust_macros::closure!( - captures(acc: &mut &mut i32), - ensures(result == x + 1 && *(!acc) == *(*acc) + 1), - |x: i32| -> i32 { - acc += 1; - x + acc - }, - ); - let r = f(3); - assert!(r == 4); -} diff --git a/tests/ui/pass/closure_captures_mut.rs b/tests/ui/pass/closure_captures_fn_once.rs similarity index 74% rename from tests/ui/pass/closure_captures_mut.rs rename to tests/ui/pass/closure_captures_fn_once.rs index 0d658305..6f42beba 100644 --- a/tests/ui/pass/closure_captures_mut.rs +++ b/tests/ui/pass/closure_captures_fn_once.rs @@ -4,8 +4,9 @@ // A capture taken by mutable borrow is named as the `&mut` it is, so that the clause // can say both what it was on entry (`*acc`) and what it becomes (`!acc`). // -// The closure is passed straight to `apply`: binding it to a `let` first would have it -// called through `&mut`, which a specification cannot name its captures through yet. +// The closure is passed straight to `apply`, which keeps it `FnOnce` and its +// environment a plain tuple. A `FnMut` closure reached through `pre!`/`post!` instead +// would be handed an environment without the `Mut` those translate away. #[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_captures_order.rs b/tests/ui/pass/closure_captures_order.rs deleted file mode 100644 index 8c234815..00000000 --- a/tests/ui/pass/closure_captures_order.rs +++ /dev/null @@ -1,23 +0,0 @@ -//@check-pass -//@compile-flags: -C debug-assertions=off - -// The closure captures `b` before `n`, since that is the order its body first uses -// them, while `captures` lists `n` first. Matching the two up by name is what makes -// `n` resolve to the second captured value rather than the first. -#[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 { - f(x) -} - -fn main() { - let n = 5; - let b = true; - let f = thrust_macros::closure!( - captures(n: i32, b: bool), - ensures(result == x + n), - move |x: i32| -> i32 { if b { x + n } else { x } }, - ); - let r = apply(3, f); - assert!(r == 8); -} diff --git a/tests/ui/pass/closure_captures_requires.rs b/tests/ui/pass/closure_captures_requires.rs deleted file mode 100644 index f86b1ba1..00000000 --- a/tests/ui/pass/closure_captures_requires.rs +++ /dev/null @@ -1,22 +0,0 @@ -//@check-pass -//@compile-flags: -C debug-assertions=off - -// A capture named in `requires`, where the environment leads the companion's -// parameters instead of following `result` as it does for `ensures`. -#[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 { - f(x) -} - -fn main() { - let n = 5; - let f = thrust_macros::closure!( - captures(n: i32), - requires(x > n), - ensures(result == x + n), - |x: i32| -> i32 { x + n }, - ); - let r = apply(7, f); - assert!(r == 12); -} From 4d6e98e2a8e1cb5c77d5eb7f6fa2c23450245d9d Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 13 Aug 2026 14:29:33 +0000 Subject: [PATCH 8/9] fixup! Let a closure specification name the closure's captured variables Drop the test comments that restate the case, keeping only the two that say something the case does not: why the `FnOnce` closure is passed inline, and why the `FnMut` capture is spelled `*(!acc)` rather than `!(*acc)`. --- tests/ui/fail/closure_captures.rs | 2 -- tests/ui/fail/closure_captures_fn_mut.rs | 1 - tests/ui/fail/closure_captures_fn_once.rs | 1 - tests/ui/pass/closure_captures.rs | 2 -- tests/ui/pass/closure_captures_fn_mut.rs | 7 +++---- tests/ui/pass/closure_captures_fn_once.rs | 9 +++------ 6 files changed, 6 insertions(+), 16 deletions(-) diff --git a/tests/ui/fail/closure_captures.rs b/tests/ui/fail/closure_captures.rs index 45a8bb2f..0da513e9 100644 --- a/tests/ui/fail/closure_captures.rs +++ b/tests/ui/fail/closure_captures.rs @@ -1,8 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -// The declared precondition is `x > n`, and the captured `n` is 5, so calling the -// closure with 3 must fail verification. #[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/fail/closure_captures_fn_mut.rs b/tests/ui/fail/closure_captures_fn_mut.rs index 776bd27d..91aaae16 100644 --- a/tests/ui/fail/closure_captures_fn_mut.rs +++ b/tests/ui/fail/closure_captures_fn_mut.rs @@ -1,7 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -// The captured `acc` counts up from 0, so the first call returns 4. fn main() { let mut acc = 0; let mut f = thrust_macros::closure!( diff --git a/tests/ui/fail/closure_captures_fn_once.rs b/tests/ui/fail/closure_captures_fn_once.rs index 046e867e..bd2efe00 100644 --- a/tests/ui/fail/closure_captures_fn_once.rs +++ b/tests/ui/fail/closure_captures_fn_once.rs @@ -1,7 +1,6 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off -// The declared postcondition pins `result` to `x + 1`, which is 4. #[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_captures.rs b/tests/ui/pass/closure_captures.rs index f2e46f81..560f80da 100644 --- a/tests/ui/pass/closure_captures.rs +++ b/tests/ui/pass/closure_captures.rs @@ -1,8 +1,6 @@ //@check-pass //@compile-flags: -C debug-assertions=off -// A capture named in both clauses, so the environment is read from both companion -// layouts: `requires` takes it first, `ensures` takes it after `result`. #[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_captures_fn_mut.rs b/tests/ui/pass/closure_captures_fn_mut.rs index b8871483..5465eab9 100644 --- a/tests/ui/pass/closure_captures_fn_mut.rs +++ b/tests/ui/pass/closure_captures_fn_mut.rs @@ -1,10 +1,9 @@ //@check-pass //@compile-flags: -C debug-assertions=off -// A `FnMut` closure that captures by mutable borrow carries two `Mut` levels: the outer -// one is the environment's, holding the slot on entry (`*acc`) and on exit (`!acc`), -// and the inner one is the borrow's, whose current value is what the counter holds. So -// counting up by one across the call reads `*(!acc) == *(*acc) + 1`. +// A `FnMut` environment is itself a `Mut`, so a mutable-borrow capture has two levels: +// the outer holds the slot on entry (`*acc`) and on exit (`!acc`), the inner is the +// borrow, whose current value is the counter. Hence `*(!acc)`, not `!(*acc)`. fn main() { let mut acc = 0; let mut f = thrust_macros::closure!( diff --git a/tests/ui/pass/closure_captures_fn_once.rs b/tests/ui/pass/closure_captures_fn_once.rs index 6f42beba..4cd88c76 100644 --- a/tests/ui/pass/closure_captures_fn_once.rs +++ b/tests/ui/pass/closure_captures_fn_once.rs @@ -1,12 +1,9 @@ //@check-pass //@compile-flags: -C debug-assertions=off -// A capture taken by mutable borrow is named as the `&mut` it is, so that the clause -// can say both what it was on entry (`*acc`) and what it becomes (`!acc`). -// -// The closure is passed straight to `apply`, which keeps it `FnOnce` and its -// environment a plain tuple. A `FnMut` closure reached through `pre!`/`post!` instead -// would be handed an environment without the `Mut` those translate away. +// 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 an environment stripped +// of its `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 { From 62d0de787087105d2fe5304e7a07baf5f7fb54d0 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 13 Aug 2026 14:51:16 +0000 Subject: [PATCH 9/9] fixup! Let a closure specification name the closure's captured variables Call the captured state a closure's upvars throughout, the word the surrounding code already uses (`tupled_upvars_ty`, `upvar_tys`), rather than its environment. The marker attribute becomes `#[thrust::closure_upvars]`. --- src/analyze/annot.rs | 4 +-- src/analyze/annot_fn.rs | 30 +++++++++++------------ tests/ui/pass/closure_captures_fn_mut.rs | 7 +++--- tests/ui/pass/closure_captures_fn_once.rs | 4 +-- thrust-macros/src/closure.rs | 20 +++++++-------- 5 files changed, 33 insertions(+), 32 deletions(-) diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index c6b7a288..a4df8ae0 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -46,8 +46,8 @@ pub fn refinement_path_path() -> [Symbol; 2] { [Symbol::intern("thrust"), Symbol::intern("refinement_path")] } -pub fn closure_env_path() -> [Symbol; 2] { - [Symbol::intern("thrust"), Symbol::intern("closure_env")] +pub fn closure_upvars_path() -> [Symbol; 2] { + [Symbol::intern("thrust"), Symbol::intern("closure_upvars")] } pub fn model_ty_path() -> [Symbol; 3] { diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index e086b7b9..1eea3402 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -211,7 +211,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { fn build_env_from_params(&mut self) { for (idx, param) in self.body.params.iter().enumerate() { let param_idx = rty::FunctionParamIdx::from(idx); - if self.is_closure_env_param(param) { + if self.is_closure_upvars_param(param) { self.build_env_from_captures(chc::Term::var(param_idx), param.pat); continue; } @@ -231,22 +231,22 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { } } - /// Whether the parameter stands in for the closure environment, as marked by - /// `#[thrust::closure_env]` on a `closure!` specification. - fn is_closure_env_param(&self, param: &rustc_hir::Param<'tcx>) -> bool { - let attr_path = analyze::annot::closure_env_path(); + /// Whether the parameter holds the closure's upvars, as marked by + /// `#[thrust::closure_upvars]` on a `closure!` specification. + fn is_closure_upvars_param(&self, param: &rustc_hir::Param<'tcx>) -> bool { + let attr_path = analyze::annot::closure_upvars_path(); self.tcx .hir_attrs(param.hir_id) .iter() .any(|attr| attr.path_matches(&attr_path)) } - /// Binds the names of a closure specification's environment pattern to the - /// closure's captured variables. + /// Binds the names of a closure specification's upvars pattern to the closure's + /// captured variables. /// /// The pattern lists the captures a clause names, in the order it wrote them, - /// while the environment holds every capture in the order rustc chose. The two - /// are therefore matched up by name. + /// while the upvars hold every capture in the order rustc chose. The two are + /// therefore matched up by name. fn build_env_from_captures( &mut self, upvars_term: chc::Term, @@ -254,7 +254,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { ) { let rustc_hir::PatKind::Tuple(subpats, _) = pat.kind else { panic!( - "closure environment is expected to be a tuple pattern: {:?}", + "closure upvars are expected to be a tuple pattern: {:?}", pat ); }; @@ -443,7 +443,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { } /// The values of a closure's parameters: the closure's first (RustCall) parameter is its - /// environment, which is the closure value itself, followed by the logical arguments. + /// upvars, which are the closure value itself, followed by the logical arguments. fn translate_closure_precondition( &self, receiver: &'tcx rustc_hir::Expr<'tcx>, @@ -459,8 +459,8 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { ) }); let logical_args = self.closure_spec_args(args); - // `fn_ty` is a closure (RustCall ABI), so its parameters are `[env, args..]`, where the - // environment is the closure value itself. + // `fn_ty` is a closure (RustCall ABI), so its parameters are `[upvars, args..]`, where + // the upvars are the closure value itself. assert_eq!( logical_args.len(), fn_ty.params.len() - 1, @@ -489,8 +489,8 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { ) }); let logical_args = self.closure_spec_args(args); - // `fn_ty` is a closure (RustCall ABI), so its parameters are `[env, args..]`, where the - // environment is the closure value itself. + // `fn_ty` is a closure (RustCall ABI), so its parameters are `[upvars, args..]`, where + // the upvars are the closure value itself. assert_eq!( logical_args.len(), fn_ty.params.len() - 1, diff --git a/tests/ui/pass/closure_captures_fn_mut.rs b/tests/ui/pass/closure_captures_fn_mut.rs index 5465eab9..d5023dbe 100644 --- a/tests/ui/pass/closure_captures_fn_mut.rs +++ b/tests/ui/pass/closure_captures_fn_mut.rs @@ -1,9 +1,10 @@ //@check-pass //@compile-flags: -C debug-assertions=off -// A `FnMut` environment is itself a `Mut`, so a mutable-borrow capture has two levels: -// the outer holds the slot on entry (`*acc`) and on exit (`!acc`), the inner is the -// borrow, whose current value is the counter. Hence `*(!acc)`, not `!(*acc)`. +// A `FnMut` closure holds its upvars behind a `Mut`, so a mutable-borrow capture has +// two levels: the outer holds the slot on entry (`*acc`) and on exit (`!acc`), the +// inner is the borrow, whose current value is the counter. Hence `*(!acc)`, not +// `!(*acc)`. fn main() { let mut acc = 0; let mut f = thrust_macros::closure!( diff --git a/tests/ui/pass/closure_captures_fn_once.rs b/tests/ui/pass/closure_captures_fn_once.rs index 4cd88c76..a9115dbe 100644 --- a/tests/ui/pass/closure_captures_fn_once.rs +++ b/tests/ui/pass/closure_captures_fn_once.rs @@ -2,8 +2,8 @@ //@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 an environment stripped -// of its `Mut`. +// makes it `FnMut`, and `pre!`/`post!` hand a `FnMut` closure upvars stripped of their +// `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/thrust-macros/src/closure.rs b/thrust-macros/src/closure.rs index a2bc5793..33845a9f 100644 --- a/thrust-macros/src/closure.rs +++ b/thrust-macros/src/closure.rs @@ -108,7 +108,7 @@ fn expand_closure(spec: ClosureSpec) -> syn::Result { mut closure, } = spec; - let env = env_param(&captures)?; + let upvars = upvars_param(&captures)?; let mut arg_params: Vec = Vec::new(); for param in &closure.inputs { let syn::Pat::Type(pt) = param else { @@ -133,10 +133,10 @@ fn expand_closure(spec: ClosureSpec) -> syn::Result { // clause has none of its own. let spec_sig: syn::Signature = syn::parse_quote!(fn closure_spec()); let type_lowering = FormulaFnTypeLowering::new(&spec_sig); - // A closure's parameters are `[env, arg1, .., argN]`, the environment holding its - // captures. The companions take the environment in that same leading position, so - // their parameters line up with the closure's. - let env_model = type_lowering.lower_params([&env]); + // A closure's parameters are `[upvars, arg1, .., argN]`. The companions take the + // upvars in that same leading position, so their parameters line up with the + // closure's. + let upvars_model = type_lowering.lower_params([&upvars]); let arg_models = type_lowering.lower_params(&arg_params); let mut prelude: Vec = Vec::new(); @@ -145,7 +145,7 @@ fn expand_closure(spec: ClosureSpec) -> syn::Result { #[allow(unused_variables, non_snake_case)] #[thrust::formula_fn] fn _thrust_closure_requires( - #[thrust::closure_env] #env_model, + #[thrust::closure_upvars] #upvars_model, #arg_models ) -> bool { #body @@ -162,7 +162,7 @@ fn expand_closure(spec: ClosureSpec) -> syn::Result { #[thrust::formula_fn] fn _thrust_closure_ensures( result: #ret_model, - #[thrust::closure_env] #env_model, + #[thrust::closure_upvars] #upvars_model, #arg_models ) -> bool { #body @@ -190,9 +190,9 @@ fn expand_closure(spec: ClosureSpec) -> syn::Result { Ok(closure) } -/// The companion parameter holding the closure environment: a tuple of the captures a -/// clause names, which the plugin matches up with the real environment by name. -fn env_param(captures: &[FnArg]) -> syn::Result { +/// The companion parameter holding the closure's upvars: a tuple of the captures a +/// clause names, which the plugin matches up with the real upvars by name. +fn upvars_param(captures: &[FnArg]) -> syn::Result { let mut names = Vec::new(); let mut tys = Vec::new(); for capture in captures {