From 1865775859f80d8e8924699afb4672cda0059698 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 14:40:37 +0000 Subject: [PATCH 1/2] Lower closure type params nested inside FnParam and other paths `thrust_models::FnParam` in a loop invariant could not refer to a closure-typed function parameter: the macro rewrote a bare `F` to `Closure` but never descended into the generic arguments of composite path types, so `FnParam` was left as-is and `f.at_entry()` produced `::Ty` instead of the expected `Closure`, causing a type mismatch. `lower_closure_type_params_in_ty` now recurses into a path type's generic arguments (and qualified self), so `FnParam` becomes `FnParam>` and `f.at_entry()` recovers the modeled closure. A closure with no captures models to a null (singleton) sort. Ordinary singleton-sorted parameters are already collapsed to their canonical value in `build_env_from_params` so they are never referenced by a variable in a formula, but `FnParam` wrappers were excluded from that handling because the wrapper type does not `build` to a meaningful type. As a result a singleton closure passed via `FnParam` kept a param-variable reference, which later ICE'd during clause building. Classify the wrapped parameter by its `Inner` sort instead, so a singleton closure collapses to its canonical value like any other singleton, keeping singleton value vars out of refinements. Adds a pass/fail test pair: `last_apply` proves a postcondition from an invariant that relates the accumulator to the entry closure's postcondition via `post!(f.at_entry())` (a capturing closure), and `unchanged` covers the null-sort closure-identity case. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Y4wjjU3RJ1Nrp82Vrci7Qn --- src/analyze/annot_fn.rs | 20 ++++++-- .../fail/loop_invariant_fn_param_closure.rs | 50 +++++++++++++++++++ .../pass/loop_invariant_fn_param_closure.rs | 50 +++++++++++++++++++ thrust-macros/src/formula_fn_type_lowering.rs | 18 +++++++ 4 files changed, 133 insertions(+), 5 deletions(-) create mode 100644 tests/ui/fail/loop_invariant_fn_param_closure.rs create mode 100644 tests/ui/pass/loop_invariant_fn_param_closure.rs diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index aa733308..b6abfb43 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -213,8 +213,11 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { for (idx, param) in self.body.params.iter().enumerate() { let param_idx = rty::FunctionParamIdx::from(idx); let mir_ty = self.pat_ty(param.pat); - let ty = self.type_builder.build(mir_ty); - let term = if !self.is_fn_param_wrapper_ty(mir_ty) && ty.to_sort().is_singleton() { + // `at_entry()` yields the `Inner` of a `FnParam`; classify by it so + // a singleton wrapped argument collapses like any other singleton below. + let repr_ty = self.fn_param_wrapper_inner_ty(mir_ty).unwrap_or(mir_ty); + let ty = self.type_builder.build(repr_ty); + let term = if ty.to_sort().is_singleton() { // the analyzer don't expect params with singleton sorts to be used in formula... // FIXME: fix the analyzer side to uniformly accept all params Self::singleton_term_for_ty(&ty).unwrap() @@ -259,9 +262,16 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { } } - fn is_fn_param_wrapper_ty(&self, ty: mir_ty::Ty<'tcx>) -> bool { - ty.ty_adt_def() - .is_some_and(|def| Some(def.did()) == self.def_ids.fn_param_wrapper()) + /// The `Inner` of a `thrust_models::FnParam` wrapper type, if `ty` is one. + fn fn_param_wrapper_inner_ty(&self, ty: mir_ty::Ty<'tcx>) -> Option> { + match ty.kind() { + mir_ty::TyKind::Adt(def, args) + if Some(def.did()) == self.def_ids.fn_param_wrapper() => + { + Some(args.type_at(0)) + } + _ => None, + } } fn build_env_from_pat( diff --git a/tests/ui/fail/loop_invariant_fn_param_closure.rs b/tests/ui/fail/loop_invariant_fn_param_closure.rs new file mode 100644 index 00000000..c808b111 --- /dev/null +++ b/tests/ui/fail/loop_invariant_fn_param_closure.rs @@ -0,0 +1,50 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +// A loop invariant refers to a closure parameter via `FnParam`, whose +// `f.at_entry()` yields `Closure`. Here the invariant relates `acc` to the +// entry closure's postcondition, from which the postcondition below is proven. +#[thrust_macros::ensures((n > 0) ==> thrust_macros::post!(f(n - 1), result))] +#[thrust_macros::invariant_context] +fn last_apply(f: F, n: i64) -> i64 +where + F: Fn(i64) -> i64, +{ + let mut acc = 0_i64; + let mut i = 0_i64; + while i < n { + thrust_macros::invariant!( + |i: i64, acc: i64, f: thrust_models::FnParam| + (i > 0) ==> thrust_macros::post!(f.at_entry()(i - 1), acc) + ); + acc = f(i); + i += 1; + } + acc +} + +// A capture-free closure is null (singleton) sorted; comparing its identity +// must collapse to a canonical value rather than ICE during clause building. +#[thrust_macros::invariant_context] +fn unchanged(mut f: F) +where + F: FnMut(i64) -> i64, +{ + let _ = &mut f; + let mut i = 0_i64; + while i < 10 { + thrust_macros::invariant!( + |i: i64, f: thrust_models::FnParam| + f.at_entry() == f.at_entry() && i <= 10 + ); + i += 1; + } + assert!(i == 11); // Unsat: the loop exits with i == 10 +} + +fn main() { + let c = 7_i64; + let _ = last_apply(|x| x + c, 10); + + unchanged(|x| x + 1); +} diff --git a/tests/ui/pass/loop_invariant_fn_param_closure.rs b/tests/ui/pass/loop_invariant_fn_param_closure.rs new file mode 100644 index 00000000..79d3928f --- /dev/null +++ b/tests/ui/pass/loop_invariant_fn_param_closure.rs @@ -0,0 +1,50 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +// A loop invariant refers to a closure parameter via `FnParam`, whose +// `f.at_entry()` yields `Closure`. Here the invariant relates `acc` to the +// entry closure's postcondition, from which the postcondition below is proven. +#[thrust_macros::ensures((n > 0) ==> thrust_macros::post!(f(n - 1), result))] +#[thrust_macros::invariant_context] +fn last_apply(f: F, n: i64) -> i64 +where + F: Fn(i64) -> i64, +{ + let mut acc = 0_i64; + let mut i = 0_i64; + while i < n { + thrust_macros::invariant!( + |i: i64, acc: i64, f: thrust_models::FnParam| + (i > 0) ==> thrust_macros::post!(f.at_entry()(i - 1), acc) + ); + acc = f(i); + i += 1; + } + acc +} + +// A capture-free closure is null (singleton) sorted; comparing its identity +// must collapse to a canonical value rather than ICE during clause building. +#[thrust_macros::invariant_context] +fn unchanged(mut f: F) +where + F: FnMut(i64) -> i64, +{ + let _ = &mut f; + let mut i = 0_i64; + while i < 10 { + thrust_macros::invariant!( + |i: i64, f: thrust_models::FnParam| + f.at_entry() == f.at_entry() && i <= 10 + ); + i += 1; + } + assert!(i == 10); +} + +fn main() { + let c = 7_i64; + let _ = last_apply(|x| x + c, 10); + + unchanged(|x| x + 1); +} diff --git a/thrust-macros/src/formula_fn_type_lowering.rs b/thrust-macros/src/formula_fn_type_lowering.rs index 1111ba7e..944f5a8b 100644 --- a/thrust-macros/src/formula_fn_type_lowering.rs +++ b/thrust-macros/src/formula_fn_type_lowering.rs @@ -192,6 +192,24 @@ impl<'a> FormulaFnTypeLowering<'a> { .collect(); syn::Type::Tuple(tt) } + // Rewrite closure type params nested in generic arguments (or a qualified + // self), e.g. `FnParam` -> `FnParam>`. + syn::Type::Path(tp) => { + let mut tp = tp.clone(); + if let Some(qself) = &mut tp.qself { + qself.ty = Box::new(self.lower_closure_type_params_in_ty(&qself.ty)); + } + for segment in &mut tp.path.segments { + if let syn::PathArguments::AngleBracketed(args) = &mut segment.arguments { + for arg in &mut args.args { + if let syn::GenericArgument::Type(elem) = arg { + *elem = self.lower_closure_type_params_in_ty(elem); + } + } + } + } + syn::Type::Path(tp) + } // TODO: support more types including ADT _ => ty.clone(), } From 04547f1b5790e72770d9c5190311cd0c03a6d7ac Mon Sep 17 00:00:00 2001 From: coord_e Date: Sun, 5 Jul 2026 01:19:57 +0900 Subject: [PATCH 2/2] fixup! Lower closure type params nested inside FnParam and other paths --- thrust-macros/src/formula_fn_type_lowering.rs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/thrust-macros/src/formula_fn_type_lowering.rs b/thrust-macros/src/formula_fn_type_lowering.rs index 944f5a8b..faac646b 100644 --- a/thrust-macros/src/formula_fn_type_lowering.rs +++ b/thrust-macros/src/formula_fn_type_lowering.rs @@ -192,13 +192,8 @@ impl<'a> FormulaFnTypeLowering<'a> { .collect(); syn::Type::Tuple(tt) } - // Rewrite closure type params nested in generic arguments (or a qualified - // self), e.g. `FnParam` -> `FnParam>`. syn::Type::Path(tp) => { let mut tp = tp.clone(); - if let Some(qself) = &mut tp.qself { - qself.ty = Box::new(self.lower_closure_type_params_in_ty(&qself.ty)); - } for segment in &mut tp.path.segments { if let syn::PathArguments::AngleBracketed(args) = &mut segment.arguments { for arg in &mut args.args {