Skip to content

fix(spl): update the unpack cheatcode for rent #902

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Stevengre merged 2 commits into from
Dec 19, 2025
Merged

fix(spl): update the unpack cheatcode for rent #902

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1870343
fix(spl): update the unpack cheatcode for rent
Stevengre Dec 18, 2025
185453f
docs(spl): update comments to use bincode::deserialize for Rent unpack
Stevengre Dec 19, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 5 additions & 17 deletions kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ cheatcode_is_spl_rent(acc) -> sets SPLDataBuffer at data field, initializes

Account::unpack_from_slice(buf) -> #splUnpack extracts value from SPLDataBuffer
Account::pack_into_slice(v,buf) -> #splPack writes value into SPLDataBuffer
Rent::from_account_info(acc) -> navigates to data buffer using projection path
bincode::deserialize(buf) -> #splUnpack extracts Rent from SPLDataBuffer
Rent::get() -> returns cached or new symbolic Rent value
```

Expand Down Expand Up @@ -127,6 +127,9 @@ module KMIR-SPL-TOKEN
// spl-token mint
rule #isSPLUnpackFunc("<state::Mint as solana_program_pack::Pack>::unpack_from_slice") => true
rule #isSPLUnpackFunc("Mint::unpack_from_slice") => true
// spl-token rent
rule #isSPLUnpackFunc("bincode::deserialize::<'_, solana_rent::Rent>") => true
rule #isSPLUnpackFunc("Rent::unpack") => true

syntax Bool ::= #isSPLPackFunc ( String ) [function, total]
rule #isSPLPackFunc(_) => false [owise]
Expand All @@ -137,12 +140,6 @@ module KMIR-SPL-TOKEN
rule #isSPLPackFunc("<state::Mint as solana_program_pack::Pack>::pack_into_slice") => true
rule #isSPLPackFunc("Mint::pack_into_slice") => true

// Rent sysvar calls (includes mock harness direct calls to Rent::from_account_info / Rent::get)
syntax Bool ::= #isSPLRentFromAccountInfoFunc ( String ) [function, total]
rule #isSPLRentFromAccountInfoFunc(_) => false [owise]
rule #isSPLRentFromAccountInfoFunc("Rent::from_account_info") => true // mock harness
rule #isSPLRentFromAccountInfoFunc("solana_sysvar::<solana_rent::Rent as solana_sysvar::Sysvar>::from_account_info") => true

syntax Bool ::= #isSPLRentGetFunc ( String ) [function, total]
rule #isSPLRentGetFunc(_) => false [owise]
rule #isSPLRentGetFunc("Rent::get") => true // mock harness
Expand Down Expand Up @@ -437,7 +434,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
## Pack / Unpack operations

```k
// Account/Mint::unpack_from_slice - extracts struct from SPLDataBuffer
// Account/Mint::unpack_from_slice, bincode::deserialize (for Rent) - extracts struct from SPLDataBuffer
rule [spl-account-unpack]:
<k> #execTerminatorCall(_, FUNC, OP:Operand .Operands, DEST, TARGET, _UNWIND) ~> _CONT
=> #splUnpack(DEST, #withDeref(OP))
Expand Down Expand Up @@ -467,15 +464,6 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
## Rent sysvar handling

```{.k .symbolic}
// Rent::from_account_info - navigates to data buffer using DATA_BUFFER_PROJS
rule [spl-rent-from-account-info]:
<k> #execTerminatorCall(_, FUNC, OP:Operand .Operands, DEST, TARGET, _UNWIND) ~> _CONT
=> #splUnpack(DEST, #appendProjsOp(OP, DATA_BUFFER_PROJS))
~> #continueAt(TARGET)
</k>
requires #isSPLRentFromAccountInfoFunc(#functionName(FUNC))
[priority(30), preserves-definedness]

// Rent::get - returns stable value, cached in outermost frame
rule [spl-rent-get]:
<k> #execTerminatorCall(_, FUNC, .Operands, DEST, TARGET, _UNWIND) ~> _CONT
Expand Down