Merging latest master into feature/p-token#981
Merged
Stevengre merged 7 commits intofeature/p-tokenfrom Mar 10, 2026
Merged
Conversation
Collaborator
dkcumming
commented
Mar 9, 2026
dkcumming
commented
- fix(kompile): map linked NormalSym functions to monoItemFn(noBody) 953
- fix(rt): generalize direct-tag enum decoding to any variant count and discriminant 955
- fix(rt): closure aggregate + #setTupleArgs fallback 952
- fix(rt): bug fix for castKindPtrToPtr 974
- fix(rt): repair closure callee setup for iter-eq repro 957
) ## Summary - Generate `MonoItemKind::MonoItemFn(symbol(...), defId(...), noBody)` for linked `NormalSym` entries that are present in `function_symbols` but missing from `items`. - Keep function resolution on concrete linked symbols instead of falling back to `"** UNKNOWN FUNCTION **"` for bodyless linked functions. - Refresh affected integration/show fixtures and normalize panic symbol hash suffixes in fixture comparison to keep snapshot output stable. - Preserve readable `kmir show --statistics --leaves` annotations for `noBody` callees (`>> function`, `>> call span`, `>> message`) even after replacing `"** UNKNOWN FUNCTION **"` with concrete symbols. ## Context In multi-crate SMIR, linked external functions can exist in `function_symbols` but not in local `items` (no local body). Before this change, that gap could leave `lookupFunction(Ty)` without a generated `monoItemFn` equation. ### Red vs Green **RED (actual stuck shape in show fixtures):** ```k #setUpCalleeData( monoItemFn(... name: symbol("** UNKNOWN FUNCTION **"), id: defId(38), body: noBody), ... ) ``` This is the unresolved-function path. **GREEN (after fix):** ```k #setUpCalleeData( monoItemFn(... name: symbol("_ZN4core9panicking5panic17h<hash>E"), id: defId(38), body: noBody), ... ) ``` The same path now resolves to a concrete linked symbol instead of `"** UNKNOWN FUNCTION **"`. --------- Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
… discriminant (#955) ## Summary Replace the specialized \`#decodeOptionTag01\` rule (which only handled exactly 2 variants with discriminants 0/1 and the Option-like 0+1 field pattern) with a general \`#decodeEnumDirect\` decoder that handles: - Any number of variants (not just two) - Any discriminant values (not just 0 and 1) - Any unsigned integer tag width (u8, u16, etc.) - Any number of fields per variant New K helper functions (all total with `owise` fallbacks): - `#decodeEnumDirectFields`: given variant index, decode its fields using per-variant offsets - `#decodeEnumDirectTag`: read tag bytes as unsigned little-endian integer - `#nthTys`: index into per-variant field type lists - `#nthVariantOffsets`: extract field offsets from nth variant layout ## Context Before this change, direct-tag enum decoding was specialized to `discriminants: 0, 1` and single-byte tag checks (modeled after `Option`). Any enum with different discriminant values or more than two variants would produce `UnableToDecode`. ## Changes - `kmir/src/kmir/kdist/mir-semantics/rt/decoding.md`: replace `#decodeOptionTag01` with general `#decodeEnumDirect` rules - `kmir/src/tests/integration/data/prove-rs/enum-direct-tag-decode.rs`: add Rust test covering repr(u8) 0/1, repr(u8) 2/5, repr(u16) 0/256, and 3-variant enums - `kmir/src/tests/integration/test_integration.py`: register the new prove-rs test ## Testing - `make build` ✅ - `uv --directory kmir run pytest kmir/src/tests/integration/test_integration.py -k 'enum-direct-tag-decode' -vv` ✅ --------- Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>
## 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(...))`](https://github.com/rust-lang/rust/blob/a2545fd6fc66b4323f555223a860c451885d1d2b/compiler/stable_mir/src/mir/body.rs#L633). 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 - [x] `test_prove_rs[closure-no-capture]` - [x] `make test-integration` regression
This PR addresses an issue that was first identified in solana-token's `test_validate_owner_multisig.rs` proof. `iter_next_3.rs` is a minimized test that reproduces the issue. ### Problem When executing Rust's slice iterator (`core::slice::Iter`), the `Iter::new` function creates two pointers: a start pointer and an end pointer. The `next` method compares these pointers for equality to determine whether iteration is complete. During `Iter::new`, the end pointer undergoes a `PtrToPtr` cast (e.g., from `*const [u8; 32]` to `*mut [u8; 32]`) that changes its initially correct metadata to one that causes the issue. - Initially correct metadata: `metadata(staticSize(32), 3, dynamicSize(3))` - Resulting metadata: `metadata(staticSize(32), 3, staticSize(32))` - Applied `convertMetadata` rule: https://github.com/runtimeverification/mir-semantics/blob/8b331c654d225b13b410970599e559e95947edc5/kmir/src/kmir/kdist/mir-semantics/rt/data.md?plain=1#L1508 This rule sets the origin to `staticSize(32)` (matched with `ORIGIN_SIZE`), discarding the previous correct `dynamicSize(3)`. The start pointer does not undergo this additional cast, and maintains its metadata: `metadata(staticSize(32), 3, dynamicSize(3))`. This causes the two pointers to end up with different metadata: `metadata(staticSize(32), 3, dynamicSize(3))` vs `metadata(staticSize(32), 3, staticSize(32))`. When `Iter::next` compares the pointers for equality at the end of iteration, the comparison evaluates to `false` instead of `true`, causing the proof to take the wrong branch (not-at-the-end) and eventually get stuck on an out-of-bounds access. ### Solution We add a `#cast` rule for `castKindPtrToPtr`, with higher priority, that matches when the source and target pointer types have identical pointee types. This rule preserves the source pointer metadata. This works because when the pointee types are identical, the pointer representation does not need to change. The only reason such a cast exists in MIR is a mutability change, which does not affect the pointer's runtime representation or metadata. When the pointee types are not identical, the rule does not match, and we fallback to the existing rule and handle the cast as before. For casts where both the pointee type and mutability differ (e.g., `*const T1` to `*mut T2`: `T1=/=T2`), I am not sure how MIR is generated for these, but either case is handled correctly: - If it is a single cast, the pointee types differ, so the new rule does not match and the fallback rule handles it as before. Mutability is not involved in type projections or equality checks, so it does not interfere. - If it is two separate casts (one for mutability, one for the pointee type), the new rule matches the mutability cast and the fallback rule handles the pointee type cast. ### Why mutability information was not added It would be possible to thread mutability information through the semantics (from the smir.json, which now includes mutability on `PtrType` and `RefType`, PR [here](runtimeverification/stable-mir-json#127)) and add an explicit check that the cast is indeed a mutability-only change. I chose not to include it, with the following reasoning. The new mutability information would only be used to confirm that the source and target pointer types differ in mutability in the new `#cast` rule. Any other place where the new mutability information would be threaded through would be `_`. At the same time, if the source and target pointer types have identical pointee types, the only possible difference that would have led to a cast is a difference in mutability. Propagating the mutability in the semantics for this check alone seems to add overhead for no benefit, especially considering that mutability is not checked/enforced anywhere else. So, it seems sufficient to just rely on the fact that because the pointee type is the same, we do not need to change the metadata of the pointer, so we simply do not. Mutability does not affect that.
## Summary - adds `iter-eq-copied-take-dereftruncate` as a regression - fixes `setupCalleeClosure2` by initializing callee `_1` with the closure env before tuple unpacking - removes temporary show tracking after the repro reaches `#EndProgram` ## Why This Fix - Red commit frontier: after `1947` steps the new repro stopped at: - `#traverseProjection(toLocal(1), thunk(operandCopy(place(... local: local(1) ...))))` - Root cause: `setupCalleeClosure2` reserved `NEWLOCALS` and unpacked the tuple argument into `_2..`, but never wrote the closure receiver/env into `_1`. The std closure body later dereferenced `local(1)`, so execution walked a bad projection path instead of the closure env. - Fix: write `#incrementRef(getValue(LOCALS, CLOSURE))` into `local(1)` before `#setTupleArgs(2, ...)`. - Effect: the same repro moves from the stuck `1947`-step leaf to `#EndProgram` after `5601` steps. The cleanup commit then deletes only the temporary show artifact.
Stevengre
approved these changes
Mar 10, 2026
Stevengre
reviewed
Mar 10, 2026
| └─ 3 (stuck, leaf) | ||
| ListItem ( thunk ( #decodeConstant ( constantKindZeroSized , ty ( 89 ) , typeInf | ||
| span: 274 | ||
| #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandM |
Contributor
There was a problem hiding this comment.
This is not expected. I'm investigating, but we can merge it first.
dkcumming
added a commit
to runtimeverification/solana-token
that referenced
this pull request
Mar 10, 2026
- 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)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.