fix(rt): resolve thunk(operandCopy) in projection traversal

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

@@ -1051,6 +1051,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 )
@@ -1852,6 +1858,9 @@ Zero-sized types can be decoded trivially into their respective representation.
   // zero-sized array
   rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoArrayType(_, _))
         => Range(.List) ... </k>
+  // zero-sized closure/function-like value (opaque fun type in SMIR metadata)
+  rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoFunType(_))
+        => Aggregate(variantIdx(0), .List) ... </k>
 ```
 
 Allocated constants of reference type with a single provenance map entry are decoded as references

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)
+}

kmir/src/tests/integration/data/prove-rs/iter-copied-take-next-thunk.rs

@@ -0,0 +1,19 @@
+#[derive(Copy, Clone)]
+struct Pubkey([u8; 32]);
+
+fn main() {
+    let _keep: fn(usize) -> u8 = repro;
+}
+
+#[no_mangle]
+pub fn repro(n: usize) -> u8 {
+    let keys = [Pubkey([1; 32]); 11];
+    let mut it = keys.iter().take(n).copied();
+
+    if 1 <= n && n <= 11 {
+        let first = it.next().unwrap();
+        first.0[0]
+    } else {
+        0
+    }
+}

kmir/src/tests/integration/data/prove-rs/iter-map-eq-copied-take-thunk-fail.rs

@@ -0,0 +1,21 @@
+const TAKE_N: usize = 3;
+
+fn main() {
+    let _keep: fn(&[AccountInfo<'_>; 5], [Pubkey; 11]) -> bool = repro;
+}
+
+#[no_mangle]
+pub fn repro(accounts: &[AccountInfo<'_>; 5], signers: [Pubkey; 11]) -> bool {
+    accounts[2..]
+        .iter()
+        .map(|signer| *signer.key)
+        .eq(signers.iter().take(TAKE_N).copied())
+}
+
+#[derive(Clone)]
+struct AccountInfo<'a> {
+    key: &'a Pubkey,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+struct Pubkey([u8; 32]);

kmir/src/tests/integration/test_integration.py

@@ -38,6 +38,24 @@
     'assume-cheatcode-conflict-fail': ['check_assume_conflict'],
     'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
     'test_offset_from-fail': ['testing'],
+    'closure-no-capture': ['repro'],
+    'iter-copied-take-next-thunk': ['repro'],
+    'iter-map-eq-copied-take-thunk-fail': ['repro'],
+}
+PROVE_RS_OPTS = {
+    # These are red reproducers: fail fast on the first thunk frontier to keep CI runtime bounded.
+    'iter-copied-take-next-thunk': {
+        'max_depth': 200,
+        'fail_fast': True,
+        'break_on_thunk': True,
+        'terminate_on_thunk': True,
+    },
+    'iter-map-eq-copied-take-thunk-fail': {
+        'max_depth': 200,
+        'fail_fast': True,
+        'break_on_thunk': True,
+        'terminate_on_thunk': True,
+    },
 }
 PROVE_RS_SHOW_SPECS = [
     'local-raw-fail',
@@ -89,6 +107,9 @@ def test_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> No
 
     for start_symbol in start_symbols:
         prove_rs_opts.start_symbol = start_symbol
+        if rs_file.stem in PROVE_RS_OPTS:
+            for opt, val in PROVE_RS_OPTS[rs_file.stem].items():
+                setattr(prove_rs_opts, opt, val)
         apr_proof = kmir.prove_rs(prove_rs_opts)
 
         if should_show: