fix(rt): closure aggregate + #setTupleArgs fallback (#952)

## Summary

Add three semantics fixes needed by the closure-call path, plus a
regression test:

- Add `aggregateKindClosure` reduction:
- `ARGS:List ~> #mkAggregate(aggregateKindClosure(...)) =>
Aggregate(variantIdx(0), ARGS)`
- Add `#setTupleArgs(IDX, VAL:Value) [owise]` fallback for unwrapped
single-value arguments
- Add typed-closure callee setup rule `setupCalleeClosure3` (with
`isFunType` predicate)
- Add `closure-no-capture.rs` regression test

## Context

Stable MIR represents closure construction via
[`Rvalue::Aggregate(AggregateKind::Closure(...))`](https://github.com/rust-lang/rust/blob/a2545fd6fc66b4323f555223a860c451885d1d2b/compiler/stable_mir/src/mir/body.rs#L633).
The K semantics had rules for tuple/ADT aggregates, but no rule for
`aggregateKindClosure`.

For closure calls, argument placement goes through `#setTupleArgs`.
Existing rules only handled tuple/list-shaped payloads.

Also, once closure type metadata is present, closure env locals can be
typed as `Ref<FunType(...)>`. Before this PR, closure setup rules only
matched `VoidType`-based closure typing paths, so the typed closure path
needed an explicit setup rule.

### Red vs Green for `aggregateKindClosure`

**RED:**
```
ListItem(...) ~> #mkAggregate(aggregateKindClosure(...))
```
No matching rule, execution is stuck.

**GREEN:**
`aggregateKindClosure` reduces to `Aggregate(variantIdx(0), ARGS)`, so
closure aggregate construction proceeds.

### Red vs Green for `#setTupleArgs [owise]`

After closure aggregate reduction is added, execution advances to the
next blocker:

**RED (next blocker):**
```
#setTupleArgs(2, Integer(41,8,false))
```
No existing `#setTupleArgs` rule matches this plain `Value` shape.

**GREEN:**
The fallback
```
#setTupleArgs(IDX, VAL:Value) => #setLocalValue(..., #incrementRef(VAL)) [owise]
```
handles the unwrapped single-value case and allows argument setup to
continue.

### Red vs Green for `setupCalleeClosure3`

With typed closure metadata, closure env can appear as
`Ref<FunType(...)>`. Existing closure setup rules were guarded for
`VoidType` closure typing paths, so typed closure setup could miss those
rules.

**RED:**
Typed closure env path does not satisfy the existing `VoidType` guard
shape for closure setup, so closure-call setup does not reliably take
the typed closure path.

**GREEN:**
`setupCalleeClosure3` adds the typed path explicitly:
- guard uses `isFunType(#lookupMaybeTy(pointeeTy(...)))`
- still performs the same tuple-arg unpacking via `#setTupleArgs(2,
getValue(LOCALS, TUPLE))`

This keeps closure-call argument placement consistent when closure env
typing is known.

## Proof evidence

**Without fix (RED):** `closure-no-capture.rs` gets stuck on closure
aggregate, and after adding only the closure aggregate rule it gets
stuck at `#setTupleArgs(2, Integer(41,8,false))`.

**With fix (GREEN):**
```
test_prove_rs[closure-no-capture] PASSED
```

## Test plan

- [x] `test_prove_rs[closure-no-capture]`
- [x] `make test-integration` regression

Author: Stevengre

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -606,6 +606,11 @@ Therefore a heuristics is used here:
   // unpack tuple and set arguments individually
   rule <k> #setTupleArgs(IDX, Aggregate(variantIdx(0), ARGS)) => #setTupleArgs(IDX, ARGS) ... </k>
 
+  rule <k> #setTupleArgs(IDX, VAL:Value)
+        => #setTupleArgs(IDX, ListItem(VAL))
+        ...
+       </k> [owise]
+
   rule <k> #setTupleArgs(_, .List ) => .K ... </k>
 
   rule <k> #setTupleArgs(IDX, ListItem(VAL) REST:List)

kmir/src/kmir/kdist/mir-semantics/rt/data.md

@@ -1051,6 +1051,12 @@ Literal arrays are also built using this RValue.
         ...
        </k>
 
+  rule <k> ARGS:List ~> #mkAggregate(aggregateKindClosure(_DEF, _TY_ARGS))
+        =>
+            Aggregate(variantIdx(0), ARGS)
+        ...
+       </k>
+
 
   // #readOperands accumulates a list of `TypedLocal` values from operands
   syntax KItem ::= #readOperands ( Operands )

kmir/src/tests/integration/data/prove-rs/closure-staged.rs

@@ -0,0 +1,11 @@
+fn apply<F: FnOnce(u8) -> u8>(f: F, v: u8) -> u8 {
+    f(v)
+}
+
+fn main() {
+    let delta: u8 = 1u8;
+    let _captured = |x: u8| x + delta;
+
+    let f = |x: u8| x + 1u8;
+    assert_eq!(apply(f, 41u8), 42u8);
+}