Let a closure specification name the closure's captured variables

[coord-e]

Summary

closure! clauses could only name the closure's arguments; its environment sat in the companion formula functions as an unnameable dummy parameter. This adds a captures clause, so a clause can talk about captured state:

let n = 5;
let f = thrust_macros::closure!(
    captures(n: i32),
    ensures(result == x + n),
    |x: i32| -> i32 { x + n },
);

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

The environment already carries the captures as a structured value — replace_closure_model maps TyKind::Closure to model::Closure<tupled_upvars_ty>, which builds to the upvar tuple's rty, so a closure's FunctionType takes 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 environment parameter ((n, b,): (i32, bool,)), replacing the previous () dummy, marked #[thrust::closure_env].
• src/analyze/annot_fn.rs — binds that pattern by name rather than by position, matching each against tcx.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; with positional binding two captures of the same type would swap silently.
• src/analyze/annot.rs — the new attribute path.

No change to FunctionType, subtyping, or the CHC encoding.

How a capture is restated

A capture is restated with the type it has where the closure is written, with one exception:

Capture	Restated as	In a clause
by value (move, or Copy used by value)	n: i32	n
shared borrow	n: i32 — read through	n
mutable borrow	acc: &mut i32	*acc on entry, !acc on exit

Shared borrows are read through so that adding or removing move does not change how a clause is written. A mutable borrow is left as the Mut it is, because a clause has to say which of the two values it means; that is the existing Mut vocabulary, not new surface.

Errors

Each reports against the offending captures entry:

Case	Message
name the closure does not capture	`m` is not captured by this closure
restated with a type of a different sort	`n` is captured as `i32`
capture taken field by field (RFC 2229)	`p` is captured field by field, which a closure specification cannot name
closure called through &mut	this closure is called through `&mut`, so a specification cannot name its captures yet

That last one is a pre-existing analyzer limitation rather than a limitation of this feature: when a closure is called through &mut self its environment becomes &mut Tuple<..>, and the pvar for it is declared with one sort and applied with another (A2_Mut<Tuple<Mut<Int>>> vs A1_Tuple<Mut<Int>>). That shape already fails on main through plain pre!/post!, with no closure! involved, and it is orthogonal to capture mode — a FnMut closure with a by-value capture hits it too. Reporting it keeps closure! from turning it into a panic.

Tests

Passing/failing pairs following the repo convention:

• closure_captures — a shared-borrow capture named in ensures.
• closure_captures_order — the closure captures b before n because its body uses b first, while captures lists n first. The env is (own bool, own int) and the installed postcondition resolves to ν = ($1 + $0.1), i.e. index 1 for n; positional binding would have taken $0.0 and picked up the bool. This is the regression test for name resolution.
• closure_captures_mut — a mutable-borrow capture, relating *acc to !acc.

All three capture modes are covered. The full UI suite shows no regressions: the failing set is identical to the base tree's pre-existing solver-limitation failures (32), with 268 → 276 passing.

Out of scope

• Precise (field-level) capture — edition 2021 can capture s.a rather than s; naming that would need place paths, not just identifiers. Reported as an error.
• Closures called through &mut — blocked on the pre-existing environment-sort inconsistency described above, not on anything in this change.