From 18703439b3ebd80c9e735a89eb34041ca1f5307f Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 18 Dec 2025 21:51:47 +0800 Subject: [PATCH 1/2] fix(spl): update the unpack cheatcode for rent --- .../kdist/mir-semantics/symbolic/spl-token.md | 20 ++++--------------- 1 file changed, 4 insertions(+), 16 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md index 37bf39b84..b2130cf78 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -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 +Rent::unpack(buf) -> #splUnpack extracts Rent from SPLDataBuffer Rent::get() -> returns cached or new symbolic Rent value ``` @@ -127,6 +127,9 @@ module KMIR-SPL-TOKEN // spl-token mint rule #isSPLUnpackFunc("::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] @@ -137,12 +140,6 @@ module KMIR-SPL-TOKEN rule #isSPLPackFunc("::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::::from_account_info") => true - syntax Bool ::= #isSPLRentGetFunc ( String ) [function, total] rule #isSPLRentGetFunc(_) => false [owise] rule #isSPLRentGetFunc("Rent::get") => true // mock harness @@ -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]: - #execTerminatorCall(_, FUNC, OP:Operand .Operands, DEST, TARGET, _UNWIND) ~> _CONT - => #splUnpack(DEST, #appendProjsOp(OP, DATA_BUFFER_PROJS)) - ~> #continueAt(TARGET) - - requires #isSPLRentFromAccountInfoFunc(#functionName(FUNC)) - [priority(30), preserves-definedness] - // Rent::get - returns stable value, cached in outermost frame rule [spl-rent-get]: #execTerminatorCall(_, FUNC, .Operands, DEST, TARGET, _UNWIND) ~> _CONT From 185453fe09fcdcee1c173eac39302fdda419729d Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 19 Dec 2025 13:16:12 +0800 Subject: [PATCH 2/2] docs(spl): update comments to use bincode::deserialize for Rent unpack Update documentation and code comments to accurately reflect that Rent deserialization uses bincode::deserialize rather than Rent::unpack. --- kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md index b2130cf78..8f7b3505c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -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::unpack(buf) -> #splUnpack extracts Rent from SPLDataBuffer +bincode::deserialize(buf) -> #splUnpack extracts Rent from SPLDataBuffer Rent::get() -> returns cached or new symbolic Rent value ``` @@ -434,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]: #execTerminatorCall(_, FUNC, OP:Operand .Operands, DEST, TARGET, _UNWIND) ~> _CONT => #splUnpack(DEST, #withDeref(OP))