fix(rt): closure aggregate + #setTupleArgs fallback by Stevengre · Pull Request #952 · runtimeverification/mir-semantics

Stevengre · 2026-02-28T02:20:39Z

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(...)). 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

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

dkcumming

Just commenting for now sorry, I need to look closer tomorrow. But just mentioning that the link you sent was from current rust MIR (fine in this case) but for clarity the AggregateKind we are representing is this Stable MIR one. Also I think the assert would be good in the test to see that the data is correctly manipulated

dkcumming

Hesitant to approve without knowing if the change to data.md is mistakenly included or what it relates to. Happy to approve otherwise

dkcumming · 2026-03-05T04:11:04Z

+fn repro() -> u8 {
+    let f = |x: u8| x + 1;
+    apply(f, 41u8)
+}


Great example. If you would be open to it in the future it would be nice to use git rebase -i to have the inclusion of the test as the first commit with the expected output failing clearly, then the inclusion of the fix in a following commit, then the update of the test from failing to to passing. It isn't a bit deal but it makes it nice to see the commit history as a story solving the problem. I think #919 is a good example of this.

dkcumming · 2026-03-05T04:12:48Z

+     andBool isTypedValue(LOCALS[CLOSURE])
+     andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
+     andBool isFunType(#lookupMaybeTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))))
+    [priority(46), preserves-definedness]


Seems like we are getting some interesting priorities 40, 45 ,46. Maybe not part of this PR but we could do a write up above the rules that explains in relation to the Rust source code and Stable MIR the how the precedence the rules apply

dkcumming · 2026-03-05T04:13:55Z

+  // 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(


Not sure if there is a way to refactor the 3 rules since they seem very similar. Not worth thinking about right now as this unblocks these closures but we should do some clean up at some point

dkcumming · 2026-03-05T04:42:20Z

+  rule <k> ARGS:List ~> #mkAggregate(aggregateKindClosure(_CLOSUREDEF, _GENERICARGS))
+        =>
+            Aggregate(variantIdx(0), ARGS)
+        ...
+       </k>
+


Is this necessary? It seems unrelated to the test you provided. I removed it and the test passed.

daniel@daniel-MS-7E06 mir-semantics$ git diff diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index b47c6fe9..89982d1f 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1051,13 +1051,6 @@ 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 ) | #readOperandsAux( List , Operands ) daniel@daniel-MS-7E06 mir-semantics$ make test-integration TEST_ARGS='-k closure-no-capture' //-snip- kmir/src/tests/integration/test_integration.py::test_prove_rs[closure-no-capture] [gw3] [100%] PASSED kmir/src/tests/integration/test_integration.py::test_prove_rs[closure-no-capture] ================================= slowest durations =================================== 39.33s call src/tests/integration/test_integration.py::test_prove_rs[closure-no-capture] (2 durations < 0.005s hidden. Use -vv to show these durations.) ================================== 1 passed in 40.09s ================================== daniel@daniel-MS-7E06 mir-semantics$

Stevengre · 2026-03-06T03:38:04Z

@dkcumming I refactored the commit history to show each change's meaning. And it shows that there is no need for closure3. (Interesting) But the changes in data.md is indeed needed.

dkcumming

LGTM

- fix(kompile): map linked NormalSym functions to monoItemFn(noBody) [953](#953) - fix(rt): generalize direct-tag enum decoding to any variant count and discriminant [955](#955) - fix(rt): closure aggregate + #setTupleArgs fallback [952](#952) - fix(rt): bug fix for castKindPtrToPtr [974](#974) - fix(rt): repair closure callee setup for iter-eq repro [957](#957)

- fix(rt): handle fun-type closure env refs in callee setup [956](runtimeverification/mir-semantics#956) - fix(decode): accept signed enum tag scalars in _extract_tag [954](runtimeverification/mir-semantics#954) - Added check for FunType in setupCalleeClosure [969](runtimeverification/mir-semantics#969) - Merge in latest master [973](runtimeverification/mir-semantics#973) - fix(kompile): map linked NormalSym functions to monoItemFn(noBody) [953](runtimeverification/mir-semantics#953) - fix(rt): generalize direct-tag enum decoding to any variant count and discriminant [955](runtimeverification/mir-semantics#955) - fix(spl-token): encode multisig signers as pubkey aggregates [958](runtimeverification/mir-semantics#958) - fix(rt): closure aggregate + #setTupleArgs fallback [952](runtimeverification/mir-semantics#952) - fix(rt): bug fix for castKindPtrToPtr [974](runtimeverification/mir-semantics#974) - fix(rt): repair closure callee setup for iter-eq repro [957](runtimeverification/mir-semantics#957) - Change the number of signers from 11 to 3 [982](runtimeverification/mir-semantics#982) - Merging latest master into feature/p-token [981](runtimeverification/mir-semantics#981)

Stevengre marked this pull request as ready for review March 2, 2026 13:04

Stevengre requested a review from dkcumming March 2, 2026 13:04

Stevengre self-assigned this Mar 2, 2026

Stevengre requested a review from mariaKt March 2, 2026 13:09

dkcumming reviewed Mar 2, 2026

View reviewed changes

Comment thread kmir/src/tests/integration/data/prove-rs/closure-no-capture.rs Outdated

Stevengre requested review from dkcumming and palinatolmach March 3, 2026 02:15

dkcumming reviewed Mar 5, 2026

View reviewed changes

Stevengre force-pushed the jh/fix-closure-aggregate-tuple-arg branch 3 times, most recently from 4e83d3b to 085024d Compare March 6, 2026 03:20

Stevengre requested a review from dkcumming March 6, 2026 03:35

Stevengre added 5 commits March 6, 2026 12:42

test(prove-rs): add closure staged red case with show snapshot

410a531

fix(rt): reduce aggregateKindClosure in mkAggregate

f7fc5bb

fix(rt): add initial value fallback for setTupleArgs

0acd839

fix(rt): finalize value fallback for setTupleArgs

491659c

test(integration): remove temporary closure show artifacts

a167b02

Stevengre force-pushed the jh/fix-closure-aggregate-tuple-arg branch from 085024d to a167b02 Compare March 6, 2026 05:03

dkcumming approved these changes Mar 6, 2026

View reviewed changes

Stevengre merged commit 022dafb into master Mar 6, 2026
7 checks passed

Stevengre deleted the jh/fix-closure-aggregate-tuple-arg branch March 6, 2026 06:06

Stevengre mentioned this pull request Mar 9, 2026

fix(rt): repair closure callee setup for iter-eq repro #957

Merged

dkcumming mentioned this pull request Mar 9, 2026

Merging latest master into feature/p-token #981

Merged

dkcumming mentioned this pull request Mar 10, 2026

Updated mir-semantics with lastest feature/p-token runtimeverification/solana-token#174

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

fix(rt): closure aggregate + #setTupleArgs fallback#952
Stevengre merged 5 commits intomasterfrom
jh/fix-closure-aggregate-tuple-arg

Stevengre commented Feb 28, 2026 •

edited

Loading

Uh oh!

dkcumming left a comment

Uh oh!

Uh oh!

dkcumming left a comment

Uh oh!

dkcumming Mar 5, 2026

Uh oh!

dkcumming Mar 5, 2026

Uh oh!

dkcumming Mar 5, 2026

Uh oh!

dkcumming Mar 5, 2026

Uh oh!

Stevengre commented Mar 6, 2026

Uh oh!

dkcumming left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

Stevengre commented Feb 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Context

Red vs Green for aggregateKindClosure

Red vs Green for #setTupleArgs [owise]

Red vs Green for setupCalleeClosure3

Proof evidence

Test plan

Uh oh!

dkcumming left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

dkcumming left a comment

Choose a reason for hiding this comment

Uh oh!

dkcumming Mar 5, 2026

Choose a reason for hiding this comment

Uh oh!

dkcumming Mar 5, 2026

Choose a reason for hiding this comment

Uh oh!

dkcumming Mar 5, 2026

Choose a reason for hiding this comment

Uh oh!

dkcumming Mar 5, 2026

Choose a reason for hiding this comment

Uh oh!

Stevengre commented Mar 6, 2026

Uh oh!

dkcumming left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Stevengre commented Feb 28, 2026 •

edited

Loading

Red vs Green for `aggregateKindClosure`

Red vs Green for `#setTupleArgs [owise]`

Red vs Green for `setupCalleeClosure3`