fix(rt): closure aggregate + #setTupleArgs fallback

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

@@ -512,13 +512,51 @@ Therefore a heuristics is used here:
      andBool lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType
     [priority(45), preserves-definedness]
 
+  // Closure-call setup for typed closure environments.
+  // When the closure pointee type is known (`typeInfoFunType`), we still need to unpack
+  // the second tuple argument into `_2 .. _n` locals.
+  rule [setupCalleeClosure3]: <k> #setUpCalleeData(
+              monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))),
+                operandMove(place(local(CLOSURE:Int), .ProjectionElems))
+                operandMove(place(local(TUPLE), .ProjectionElems))
+                .Operands,
+                _SPAN
+              )
+         =>
+           #setLocalValue(place(local(1), .ProjectionElems), #incrementRef(getValue(LOCALS, CLOSURE)))
+           ~> #setTupleArgs(2, getValue(LOCALS, TUPLE))
+           ~> #execBlock(FIRST)
+          // arguments are tuple components, stored as _2 .. _n
+         ...
+       </k>
+       <currentFrame>
+         <currentBody> _ => toKList(BLOCKS) </currentBody>
+         <locals> LOCALS => #reserveFor(NEWLOCALS) </locals>
+         <stack>
+              (ListItem(CALLERFRAME => #updateStackLocal(#updateStackLocal(CALLERFRAME, TUPLE, Moved), CLOSURE, Moved)))
+              _:List
+          </stack>
+         ...
+       </currentFrame>
+    requires 0 <=Int CLOSURE andBool CLOSURE <Int size(LOCALS)
+     andBool 0 <=Int TUPLE andBool TUPLE <Int size(LOCALS)
+     andBool isTypedValue(LOCALS[TUPLE])
+     andBool isTupleType(lookupTy(tyOfLocal({LOCALS[TUPLE]}:>TypedLocal)))
+     andBool isTypedValue(LOCALS[CLOSURE])
+     andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
+     andBool isFunType(#lookupMaybeTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))))
+    [priority(46), preserves-definedness]
+
   syntax Bool ::= isTupleType ( TypeInfo ) [function, total]
                 | isRefType ( TypeInfo ) [function, total]
+                | isFunType ( TypeInfo ) [function, total]
   // -------------------------------------------------------
   rule isTupleType(typeInfoTupleType(_, _)) => true
   rule isTupleType(    _                  ) => false [owise]
   rule isRefType(typeInfoRefType(_)) => true
   rule isRefType(    _             ) => false [owise]
+  rule isFunType(typeInfoFunType(_)) => true
+  rule isFunType(    _             ) => false [owise]
 
   syntax KItem ::= #setTupleArgs ( Int , Value )
                  | #setTupleArgs ( Int , List )
@@ -532,6 +570,12 @@ Therefore a heuristics is used here:
         => #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(VAL)) ~> #setTupleArgs(IDX +Int 1, REST)
         ...
        </k>
+
+  // Fallback for closure-call paths where the argument is not wrapped as a tuple.
+  rule <k> #setTupleArgs(IDX, VAL:Value)
+        => #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(VAL))
+        ...
+       </k> [owise]
 ```
 
 

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

@@ -1049,6 +1049,12 @@ Literal arrays are also built using this RValue.
         ...
        </k>
 
+  rule <k> ARGS:List ~> #mkAggregate(aggregateKindClosure(_CLOSUREDEF, _GENERICARGS))
+        =>
+            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-no-capture.rs

@@ -0,0 +1,12 @@
+fn apply<F: FnOnce(u8) -> u8>(f: F, v: u8) -> u8 {
+    f(v)
+}
+
+fn main() {
+    let _ = repro();
+}
+
+fn repro() -> u8 {
+    let f = |x: u8| x + 1;
+    apply(f, 41u8)
+}