Let a closure specification name the closure's captured variables - #208
Conversation
5b7d469 to
705dcfbCompare`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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BTDWVnDzef1Kx97mHWUsTU472d573 to
f69593eCompareThere was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit:f69593e6c7
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| let closure_def_id = self.tcx.local_parent(self.local_def_id); | ||
| let captures = self.tcx.closure_captures(closure_def_id); |
There was a problem hiding this comment.
When a capture-bearing FnMut closure is stored and then invoked, its MIR function receives the environment through &mut self, not as the tuple projected here. The new contract still substitutes projections directly from that parameter, so calls such as let mut f = closure!(captures(acc: &mut i32), ...); f() install a contract with an incompatible environment shape and can crash the analyzer or produce invalid verification conditions; reject this case until mutable closure environments are modeled consistently.
Useful? React with 👍 / 👎.
| let Some(idx) = captures | ||
| .iter() | ||
| .position(|capture| capture.var_ident.name == ident.name) |
There was a problem hiding this comment.
For precise captures such as a closure that reads both point.x and point.y, closure_captures can contain multiple entries with the same var_ident but different place projections. Searching only by name always selects the first field, so captures(point: Point) is bound to a field value rather than the captured variable and any clause using another field is translated from the wrong term. Detect projected captures or reconstruct the captured place instead of choosing the first same-named entry.
Useful? React with 👍 / 👎.
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Pull request overview
Adds closure specifications that can reference captured variables.
Changes:
- Introduces the
captures(...)clause. - Maps declared capture names to closure environment fields.
- Adds UI coverage for shared, mutable, and reordered captures.
Reviewed changes
Copilot reviewed 9 out of 9 changed files in this pull request and generated 6 comments.
Show a summary per file
| File | Description |
|---|---|
thrust-macros/src/closure.rs | Parses captures and generates environment parameters. |
src/analyze/annot.rs | Defines the closure-environment attribute path. |
src/analyze/annot_fn.rs | Binds capture names to environment projections. |
tests/ui/pass/closure_captures.rs | Tests shared capture success. |
tests/ui/fail/closure_captures.rs | Tests shared capture verification failure. |
tests/ui/pass/closure_captures_order.rs | Tests name-based capture ordering. |
tests/ui/fail/closure_captures_order.rs | Tests reordered capture verification failure. |
tests/ui/pass/closure_captures_mut.rs | Tests mutable capture success. |
tests/ui/fail/closure_captures_mut.rs | Tests mutable capture verification failure. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
| let Some(idx) = captures | ||
| .iter() | ||
| .position(|capture| capture.var_ident.name == ident.name) | ||
| else { |
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
| if self.is_closure_env_param(param) { | ||
| self.build_env_from_captures(chc::Term::var(param_idx), param.pat); | ||
| continue; |
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
4dbfcaa to
b3748d6Compareb3748d6 to
d9e96b2CompareCover 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.
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.
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`.
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.
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)`.
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]`.
Uh oh!
There was an error while loading. Please reload this page.
Summary
closure!clauses could only name the closure's arguments; its upvars sat in the companion formula functions as an unnameable dummy parameter. This adds acapturesclause, so a clause can talk about captured state:Only the captures a clause names need restating, and in any order.
This is the "environment exposure" follow-up left open by #189.
How it works
A closure's upvars are already a structured value —
replace_closure_modelmapsTyKind::Closuretomodel::Closure<tupled_upvars_ty>, which builds to the upvar tuple'srty, so a closure'sFunctionTypetakes it as the leading parameter and the inferred pvars already range over it. The clause side was all that was missing.thrust-macros/src/closure.rs—captures(..)becomes a tuple pattern in the companion's upvars parameter ((n, b,): (i32, bool,)), replacing the previous()dummy, marked#[thrust::closure_upvars]. The marker sits on the parameter rather than the function so it needs no index, which differs between the two companions (requiresleads with the upvars,ensuresleads withresult).src/analyze/annot_fn.rs— binds that pattern by name, matching each againsttcx.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.src/analyze/annot.rs— the new attribute path.No change to
FunctionType, subtyping, or the CHC encoding.Reading a capture out of the upvars
How a closure holds its upvars depends on its kind, so the projection does too:
Fn&(captures)upvars.box_current().proj(i)FnMut&mut (captures)Mut(upvars.mut_current().proj(i), upvars.mut_final().proj(i))FnOnce(captures)upvars.proj(i)For
FnMuttheMutis distributed inward, so each capture carries the value on entry and the value on exit. That means a capture is restated one&mutdeeper than the closure holds it:Naming something the closure does not capture — including a variable it captures only field by field, which a clause cannot name — reports
`n` is not captured by this closureagainst thecapturesentry.Tests
One passing/failing pair per closure kind, since the kind is what selects how a capture is read out:
closure_captures—Fn; the capture is named in bothrequiresandensures, covering both companion layouts. The failing side calls the closure with an argument the declared precondition rules out, so the capture is exercised at the call site and not only in the body.closure_captures_fn_once—FnOnce, capture taken by mutable borrow.closure_captures_fn_mut—FnMut, the two-level case above. 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.The full UI suite shows no regressions: the failing set is identical to the base tree's pre-existing solver-limitation failures (32), with 270 → 276 passing.
Rough edges
pre!/post!on aFnMutclosure panics.translate_closure_{pre,post}conditionpass the receiver's term as the upvars argument, and the receiver is modelled asClosure<F>— the bare upvar tuple, with noMut— while aFnMutclosure'sFunctionTypeexpects&mut (captures). This predates thecapturesclause: the same shape already fails onmainthrough plainpre!/post!, where the upvars' predicate variable is declared with theMutand applied without it. It is also orthogonal to capture mode — aFnMutclosure with a by-value capture hits it too. Lifting the receiver term to aMutforFnMutclosures looks like the fix, but belongs in its own change.