From 86074df5220ec7940e5764b937c7dfd7e21d5f20 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 10 Mar 2026 14:35:49 +0800 Subject: [PATCH 1/8] test(integration): add spl-multisig iter-eq copied next repro --- ...ig-iter-eq-copied-next-fail.repro.expected | 15 +++++++ .../spl-multisig-iter-eq-copied-next-fail.rs | 44 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 2 + 3 files changed, 61 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/spl-multisig-iter-eq-copied-next-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected new file mode 100644 index 000000000..645835cf8 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (1837 steps) +└─ 3 (stuck, leaf) + #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandM + span: 149 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/spl-multisig-iter-eq-copied-next-fail.rs b/kmir/src/tests/integration/data/prove-rs/spl-multisig-iter-eq-copied-next-fail.rs new file mode 100644 index 000000000..f50b540f3 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/spl-multisig-iter-eq-copied-next-fail.rs @@ -0,0 +1,44 @@ +const MAX_SIGNERS: usize = 3; + +fn main() { + let _keep: fn() -> bool = repro; +} + +fn account_key(signer: &AccountInfo<'_>) -> Pubkey { + *signer.key +} + +#[inline(never)] +#[no_mangle] +pub fn repro() -> bool { + let k0 = Pubkey([1; 32]); + let k1 = Pubkey([2; 32]); + let k2 = Pubkey([3; 32]); + let n = 2usize; + let accounts = [ + AccountInfo { key: &k0 }, + AccountInfo { key: &k1 }, + AccountInfo { key: &k2 }, + ]; + let multisig = Multisig { + signers: [k1, k2, k0], + }; + + accounts[1..] + .iter() + .map(account_key) + .eq(multisig.signers.iter().take(n).copied()) +} + +#[derive(Clone)] +struct AccountInfo<'a> { + key: &'a Pubkey, +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +struct Pubkey([u8; 32]); + +#[derive(Clone, Debug)] +struct Multisig { + signers: [Pubkey; MAX_SIGNERS], +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 945002873..36cd122fa 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -39,6 +39,7 @@ 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], 'test_offset_from-fail': ['testing'], 'iter-eq-copied-take-dereftruncate': ['repro'], + 'spl-multisig-iter-eq-copied-next-fail': ['repro'], } PROVE_RS_SHOW_SPECS = [ 'local-raw-fail', @@ -64,6 +65,7 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', + 'spl-multisig-iter-eq-copied-next-fail', ] From f04e1656d159ea0ccd87cea14e73f09c5e688acf Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 10 Mar 2026 14:41:33 +0800 Subject: [PATCH 2/8] fix(call): match projected operandMove callees --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 2 +- .../show/spl-multisig-iter-eq-copied-next-fail.repro.expected | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index ea3d2e418..df6b5a082 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -315,7 +315,7 @@ where the returned result should go. ... - rule #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), .ProjectionElems)), ARGS, DEST, TARGET, UNWIND), SPAN)) + rule #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), _PROJS)), ARGS, DEST, TARGET, UNWIND), SPAN)) => #execTerminatorCall(tyOfLocal(getLocal(LOCALS, I)), lookupFunction(tyOfLocal(getLocal(LOCALS, I))), ARGS, DEST, TARGET, UNWIND, SPAN) ... diff --git a/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected index 645835cf8..d16aaf84f 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected @@ -3,9 +3,9 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (1837 steps) +│ (1839 steps) └─ 3 (stuck, leaf) - #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandM + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , span: 149 From ceb4a2a0874c83d85a46b559c3beedc60940e59c Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 10 Mar 2026 15:55:41 +0800 Subject: [PATCH 3/8] fix(call): compute projected callee types through to EndProgram --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 13 +++++++++++-- ...ltisig-iter-eq-copied-next-fail.repro.expected | 15 ++++++++------- kmir/src/tests/integration/test_integration.py | 6 ++++++ 3 files changed, 25 insertions(+), 9 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index df6b5a082..6026990db 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -315,12 +315,21 @@ where the returned result should go. ... - rule #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), _PROJS)), ARGS, DEST, TARGET, UNWIND), SPAN)) - => #execTerminatorCall(tyOfLocal(getLocal(LOCALS, I)), lookupFunction(tyOfLocal(getLocal(LOCALS, I))), ARGS, DEST, TARGET, UNWIND, SPAN) + rule #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), PROJS)), ARGS, DEST, TARGET, UNWIND), SPAN)) + => #execTerminatorCall(#callOperandTy(I, PROJS, LOCALS), lookupFunction(#callOperandTy(I, PROJS, LOCALS)), ARGS, DEST, TARGET, UNWIND, SPAN) ... LOCALS + syntax Ty ::= #callOperandTy(Int, ProjectionElems, List) [function, total] + | #callOperandTyAux(MaybeTy, Ty) [function, total] + + rule #callOperandTy(I, PROJS, LOCALS) + => #callOperandTyAux(getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS), tyOfLocal(getLocal(LOCALS, I))) + + rule #callOperandTyAux(TY:Ty, _FALLBACK) => TY + rule #callOperandTyAux(_, FALLBACK) => FALLBACK [owise] + // Intrinsic function call - execute directly without state switching rule [termCallIntrinsic]: #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND, SPAN) ~> _ diff --git a/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected index d16aaf84f..463b6a3f7 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected @@ -3,13 +3,14 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (1839 steps) -└─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , - span: 149 - - -┌─ 2 (root, leaf, target, terminal) +│ (5648 steps) +├─ 3 (terminal) │ #EndProgram ~> .K +│ +┊ 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 36cd122fa..b4a4e3f28 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -68,6 +68,10 @@ 'spl-multisig-iter-eq-copied-next-fail', ] +PROVE_RS_SHOULD_FAIL_OVERRIDES = { + 'spl-multisig-iter-eq-copied-next-fail': False, +} + @pytest.mark.parametrize( 'rs_file', @@ -76,6 +80,8 @@ ) def test_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: should_fail = rs_file.stem.endswith('fail') + if rs_file.stem in PROVE_RS_SHOULD_FAIL_OVERRIDES: + should_fail = PROVE_RS_SHOULD_FAIL_OVERRIDES[rs_file.stem] should_show = rs_file.stem in PROVE_RS_SHOW_SPECS is_smir = rs_file.suffix == '.json' From 30fe5498e92df9bdbf482af57bb614b9d46b010a Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 10 Mar 2026 17:20:45 +0800 Subject: [PATCH 4/8] fix(call): tighten projected callee type guard --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 6026990db..be826825b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -316,19 +316,17 @@ where the returned result should go. rule #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), PROJS)), ARGS, DEST, TARGET, UNWIND), SPAN)) - => #execTerminatorCall(#callOperandTy(I, PROJS, LOCALS), lookupFunction(#callOperandTy(I, PROJS, LOCALS)), ARGS, DEST, TARGET, UNWIND, SPAN) + => #execTerminatorCall(#projectedCallTy(I, PROJS, LOCALS), lookupFunction(#projectedCallTy(I, PROJS, LOCALS)), ARGS, DEST, TARGET, UNWIND, SPAN) ... LOCALS + requires isTy(getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS)) - syntax Ty ::= #callOperandTy(Int, ProjectionElems, List) [function, total] - | #callOperandTyAux(MaybeTy, Ty) [function, total] + syntax Ty ::= #projectedCallTy(Int, ProjectionElems, List) [function] - rule #callOperandTy(I, PROJS, LOCALS) - => #callOperandTyAux(getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS), tyOfLocal(getLocal(LOCALS, I))) - - rule #callOperandTyAux(TY:Ty, _FALLBACK) => TY - rule #callOperandTyAux(_, FALLBACK) => FALLBACK [owise] + rule #projectedCallTy(I, PROJS, LOCALS) + => {getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS)}:>Ty + requires isTy(getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS)) // Intrinsic function call - execute directly without state switching rule [termCallIntrinsic]: From 8989be986cef378982a84fe2a76bced755798bb5 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 10 Mar 2026 17:34:24 +0800 Subject: [PATCH 5/8] test(integration): rename passing spl-multisig repro --- ...tisig-iter-eq-copied-next-fail.repro.expected | 16 ---------------- ...il.rs => spl-multisig-iter-eq-copied-next.rs} | 0 kmir/src/tests/integration/test_integration.py | 9 +-------- 3 files changed, 1 insertion(+), 24 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected rename kmir/src/tests/integration/data/prove-rs/{spl-multisig-iter-eq-copied-next-fail.rs => spl-multisig-iter-eq-copied-next.rs} (100%) diff --git a/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected deleted file mode 100644 index 463b6a3f7..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected +++ /dev/null @@ -1,16 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (5648 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/data/prove-rs/spl-multisig-iter-eq-copied-next-fail.rs b/kmir/src/tests/integration/data/prove-rs/spl-multisig-iter-eq-copied-next.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/spl-multisig-iter-eq-copied-next-fail.rs rename to kmir/src/tests/integration/data/prove-rs/spl-multisig-iter-eq-copied-next.rs diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index b4a4e3f28..7e9b8cb0f 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -39,7 +39,7 @@ 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], 'test_offset_from-fail': ['testing'], 'iter-eq-copied-take-dereftruncate': ['repro'], - 'spl-multisig-iter-eq-copied-next-fail': ['repro'], + 'spl-multisig-iter-eq-copied-next': ['repro'], } PROVE_RS_SHOW_SPECS = [ 'local-raw-fail', @@ -65,13 +65,8 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', - 'spl-multisig-iter-eq-copied-next-fail', ] -PROVE_RS_SHOULD_FAIL_OVERRIDES = { - 'spl-multisig-iter-eq-copied-next-fail': False, -} - @pytest.mark.parametrize( 'rs_file', @@ -80,8 +75,6 @@ ) def test_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: should_fail = rs_file.stem.endswith('fail') - if rs_file.stem in PROVE_RS_SHOULD_FAIL_OVERRIDES: - should_fail = PROVE_RS_SHOULD_FAIL_OVERRIDES[rs_file.stem] should_show = rs_file.stem in PROVE_RS_SHOW_SPECS is_smir = rs_file.suffix == '.json' From f023dae0383f742541318c401657420cfd35f815 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 11 Mar 2026 09:13:23 +0800 Subject: [PATCH 6/8] fix(call): make projected call type helper total --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index be826825b..d9ec36515 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -320,13 +320,21 @@ where the returned result should go. ... LOCALS - requires isTy(getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS)) + requires 0 <=Int I andBool I TypedLocal), PROJS)) + [preserves-definedness] // valid local indexing checked, projected call target must resolve to a Ty - syntax Ty ::= #projectedCallTy(Int, ProjectionElems, List) [function] + syntax Ty ::= #projectedCallTy(Int, ProjectionElems, List) [function, total] rule #projectedCallTy(I, PROJS, LOCALS) - => {getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS)}:>Ty - requires isTy(getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS)) + => {getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)}:>Ty + requires 0 <=Int I andBool I TypedLocal), PROJS)) + [preserves-definedness] + + rule #projectedCallTy(_, _, _) => ty(-1) [owise] // Intrinsic function call - execute directly without state switching rule [termCallIntrinsic]: From 70031ffa84e45339cac75f5c450b6157a54af07a Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 11 Mar 2026 21:16:10 +0800 Subject: [PATCH 7/8] fix(call): use TyUnknown for projected call fallback --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index d9ec36515..b55c35527 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -320,21 +320,18 @@ where the returned result should go. ... LOCALS - requires 0 <=Int I andBool I TypedLocal), PROJS)) + requires #projectedCallTy(I, PROJS, LOCALS) =/=K TyUnknown [preserves-definedness] // valid local indexing checked, projected call target must resolve to a Ty syntax Ty ::= #projectedCallTy(Int, ProjectionElems, List) [function, total] rule #projectedCallTy(I, PROJS, LOCALS) - => {getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)}:>Ty + => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) requires 0 <=Int I andBool I TypedLocal), PROJS)) [preserves-definedness] - rule #projectedCallTy(_, _, _) => ty(-1) [owise] + rule #projectedCallTy(_, _, _) => TyUnknown [owise] // Intrinsic function call - execute directly without state switching rule [termCallIntrinsic]: From b4702ecbad69886e7d6ff052d6f6b9d950c40638 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 11 Mar 2026 21:35:50 +0800 Subject: [PATCH 8/8] fix(call): make projected call helper a MaybeTy --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index b55c35527..82c28b3f0 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -316,14 +316,14 @@ where the returned result should go. rule #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), PROJS)), ARGS, DEST, TARGET, UNWIND), SPAN)) - => #execTerminatorCall(#projectedCallTy(I, PROJS, LOCALS), lookupFunction(#projectedCallTy(I, PROJS, LOCALS)), ARGS, DEST, TARGET, UNWIND, SPAN) + => #execTerminatorCall({#projectedCallTy(I, PROJS, LOCALS)}:>Ty, lookupFunction({#projectedCallTy(I, PROJS, LOCALS)}:>Ty), ARGS, DEST, TARGET, UNWIND, SPAN) ... LOCALS - requires #projectedCallTy(I, PROJS, LOCALS) =/=K TyUnknown + requires isTy(#projectedCallTy(I, PROJS, LOCALS)) [preserves-definedness] // valid local indexing checked, projected call target must resolve to a Ty - syntax Ty ::= #projectedCallTy(Int, ProjectionElems, List) [function, total] + syntax MaybeTy ::= #projectedCallTy(Int, ProjectionElems, List) [function, total] rule #projectedCallTy(I, PROJS, LOCALS) => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)