From 554ee331d63b8eaad7da9bb6cf8146264fc68c89 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 23 Mar 2026 12:31:11 +0000 Subject: [PATCH 1/3] test(rt): expose closure zero-sized decode thunk via terminate-on-thunk MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rename closure-staged.rs → closure-staged-fail.rs and enable terminate-on-thunk for this test. Without a #decodeConstant rule for typeInfoFunType, the non-capturing closure passed as a constant operand cannot be decoded and falls through to a thunk: Node 3: #decodeConstant(constantKindZeroSized, ty(33), typeInfoFunType("...")) Node 4: thunk(#decodeConstant(...)) ← proof terminates here Also adds PROVE_TERMINATE_ON_THUNK list to test_integration.py for per-test thunk termination control. Co-Authored-By: Claude Opus 4.6 (1M context) --- ...osure-staged.rs => closure-staged-fail.rs} | 0 .../show/closure-staged-fail.main.expected | 20 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 7 ++++++- 3 files changed, 26 insertions(+), 1 deletion(-) rename kmir/src/tests/integration/data/prove-rs/{closure-staged.rs => closure-staged-fail.rs} (100%) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/closure-staged-fail.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/closure-staged.rs b/kmir/src/tests/integration/data/prove-rs/closure-staged-fail.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/closure-staged.rs rename to kmir/src/tests/integration/data/prove-rs/closure-staged-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure-staged-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure-staged-fail.main.expected new file mode 100644 index 000000000..6e5a105ea --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/closure-staged-fail.main.expected @@ -0,0 +1,20 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (44 steps) +├─ 3 +│ #decodeConstant ( constantKindZeroSized , ty ( 33 ) , typeInfoFunType ( "{closur +│ span: 98 +│ +│ (1 step) +└─ 4 (leaf, terminal) + thunk ( #decodeConstant ( constantKindZeroSized , ty ( 33 ) , typeInfoFunType ( + span: 98 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index a0486027b..2db39c422 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -41,7 +41,11 @@ 'iter-eq-copied-take-dereftruncate': ['repro'], 'spl-multisig-iter-eq-copied-next': ['repro'], } +PROVE_TERMINATE_ON_THUNK = [ + 'closure-staged-fail', +] PROVE_SHOW_SPECS = [ + 'closure-staged-fail', 'local-raw-fail', 'interior-mut-fail', 'interior-mut3-fail', @@ -84,7 +88,8 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: if update_expected_output and not should_show: pytest.skip() - prove_opts = ProveOpts(rs_file, smir=is_smir) + should_terminate_on_thunk = rs_file.stem in PROVE_TERMINATE_ON_THUNK + prove_opts = ProveOpts(rs_file, smir=is_smir, terminate_on_thunk=should_terminate_on_thunk) printer = PrettyPrinter(kmir.definition) cterm_show = CTermShow(printer.print) From ea760c0baa1f5eecd4bf5a63aa32a437d21b176c Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 23 Mar 2026 12:34:12 +0000 Subject: [PATCH 2/3] fix(rt): decode zero-sized function types and recognize them as ZSTs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two fixes for zero-sized function item types (closures without captures): 1. types.md: Add #zeroSizedType(typeInfoFunType(_)) => true Function items are inherently zero-sized (#elemSize already returns 0), but #zeroSizedType did not recognize them. This prevented rvalueRef from materializing uninitialized zero-sized closure locals. 2. data.md: Add #decodeConstant rule for typeInfoFunType Zero-sized function constants decode to Aggregate(variantIdx(0), .List), matching the existing treatment of zero-sized structs and tuples. RED → GREEN for closure-staged (with terminate-on-thunk): Before: 44 steps → thunk(#decodeConstant(constantKindZeroSized, _, typeInfoFunType(_))) — proof terminated on thunk After: 266 steps → #EndProgram — proof passes, no thunks Renames closure-staged-fail.rs back to closure-staged.rs. Co-Authored-By: Claude Opus 4.6 (1M context) --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 3 +++ kmir/src/kmir/kdist/mir-semantics/rt/types.md | 5 +++-- ...osure-staged-fail.rs => closure-staged.rs} | 0 .../show/closure-staged-fail.main.expected | 20 ------------------- .../show/closure-staged.main.expected | 17 ++++++++++++++++ .../src/tests/integration/test_integration.py | 4 ++-- 6 files changed, 25 insertions(+), 24 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{closure-staged-fail.rs => closure-staged.rs} (100%) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/closure-staged-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index df6203ea4..5839521b4 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1921,6 +1921,9 @@ Zero-sized types can be decoded trivially into their respective representation. // zero-sized array rule #decodeConstant(constantKindZeroSized, _TY, typeInfoArrayType(_, _)) => Range(.List) ... + // zero-sized function item (e.g., closures without captures) + rule #decodeConstant(constantKindZeroSized, _TY, typeInfoFunType(_)) + => Aggregate(variantIdx(0), .List) ... ``` Allocated constants of reference type with a single provenance map entry are decoded as references diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md index 3998cb3eb..26b4f20a4 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md @@ -320,8 +320,9 @@ Slices, `str`s and dynamic types require it, and any `Ty` that `is_sized` does rule #zeroSizedType(typeInfoTupleType(.Tys, _)) => true rule #zeroSizedType(typeInfoStructType(_, _, .Tys, _)) => true rule #zeroSizedType(typeInfoVoidType) => true - // FIXME: Only unit tuples, empty structs, and void are recognized here; other - // zero-sized types (e.g. single-variant enums, function or closure items, + rule #zeroSizedType(typeInfoFunType(_)) => true + // FIXME: Only unit tuples, empty structs, void, and function items are + // recognized here; other zero-sized types (e.g. single-variant enums, // newtype wrappers around ZSTs) still fall through because we do not consult // the layout metadata yet. Update once we rely on machineSize(0). rule #zeroSizedType(_) => false [owise] diff --git a/kmir/src/tests/integration/data/prove-rs/closure-staged-fail.rs b/kmir/src/tests/integration/data/prove-rs/closure-staged.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/closure-staged-fail.rs rename to kmir/src/tests/integration/data/prove-rs/closure-staged.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure-staged-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure-staged-fail.main.expected deleted file mode 100644 index 6e5a105ea..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/closure-staged-fail.main.expected +++ /dev/null @@ -1,20 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (44 steps) -├─ 3 -│ #decodeConstant ( constantKindZeroSized , ty ( 33 ) , typeInfoFunType ( "{closur -│ span: 98 -│ -│ (1 step) -└─ 4 (leaf, terminal) - thunk ( #decodeConstant ( constantKindZeroSized , ty ( 33 ) , typeInfoFunType ( - span: 98 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected new file mode 100644 index 000000000..0d681857f --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected @@ -0,0 +1,17 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (266 steps) +├─ 3 (terminal) +│ #EndProgram ~> .K +│ function: main +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + #EndProgram ~> .K + + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 2db39c422..43d9f0b26 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -42,10 +42,10 @@ 'spl-multisig-iter-eq-copied-next': ['repro'], } PROVE_TERMINATE_ON_THUNK = [ - 'closure-staged-fail', + 'closure-staged', ] PROVE_SHOW_SPECS = [ - 'closure-staged-fail', + 'closure-staged', 'local-raw-fail', 'interior-mut-fail', 'interior-mut3-fail', From 3aa012d2528408fb833da0952b9a3cdc2ce83b3c Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 26 Mar 2026 03:01:39 +0000 Subject: [PATCH 3/3] chore(test): remove closure-staged expected output MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The expected output was only needed to show the RED → GREEN transition in the commit history. Now that the fix is in place, closure-staged passes as a normal prove test without needing show output. Co-Authored-By: Claude Opus 4.6 (1M context) --- .../prove-rs/show/closure-staged.main.expected | 17 ----------------- kmir/src/tests/integration/test_integration.py | 1 - 2 files changed, 18 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected deleted file mode 100644 index 0d681857f..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (266 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ function: main -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 43d9f0b26..ea4be38e0 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -45,7 +45,6 @@ 'closure-staged', ] PROVE_SHOW_SPECS = [ - 'closure-staged', 'local-raw-fail', 'interior-mut-fail', 'interior-mut3-fail',