Skip to content

fix(spl): adjustRef for SPL Token domain data #870

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

Open
Stevengre wants to merge 10 commits into
base: feature/p-token
Choose a base branch
from
Open

fix(spl): adjustRef for SPL Token domain data #870

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
5fd4b51
feat(spl): adjustRef for spl domain data
Stevengre Nov 27, 2025
d40541a
use some pubkey by default
Stevengre Nov 28, 2025
396877e
fix: kompile bugs caused by git rebase
Stevengre Nov 28, 2025
c8fca40
recover feature/p-token
Stevengre Nov 28, 2025
c9aeb57
delete useless simplification rule
Stevengre Nov 28, 2025
f07f3d3
simplify the test
Stevengre Dec 1, 2025
571cf15
no need strict
Stevengre Dec 1, 2025
2097ccf
introduce a new sort to describe abs place
Stevengre Dec 1, 2025
51eb312
stop recursive adjustRef
Stevengre Dec 1, 2025
807b1c0
recover integration test
Stevengre Dec 1, 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
147 changes: 104 additions & 43 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 @@ -89,10 +89,15 @@ module KMIR-SPL-TOKEN
## Helper syntax

```k
syntax Value ::= SPLRefCell ( Place , Value )
syntax AbsPlace ::= AbsPlace ( Int , Place )

syntax AbsPlace ::= #adjustAbsPlace ( AbsPlace , Int ) [function, total]
rule #adjustAbsPlace(AbsPlace(DEPTH, PLACE), OFFSET) => AbsPlace(DEPTH +Int OFFSET, PLACE)

syntax Value ::= SPLRefCell ( AbsPlace , Value ) // Place of the buffer, value in the cell
| SPLDataBuffer ( Value )
| SPLDataBorrow ( Place , Value )
| SPLDataBorrowMut ( Place , Value )
| SPLDataBorrow ( AbsPlace , Value ) // Place of the buffer, borrowed value
| SPLDataBorrowMut ( AbsPlace , Value )
| SPLPubkeyRef ( Value )
```

Expand Down Expand Up @@ -173,6 +178,13 @@ module KMIR-SPL-TOKEN
rule #isSPLRentGetFunc(_) => false [owise]
rule #isSPLRentGetFunc("Rent::get") => true // mock harness
rule #isSPLRentGetFunc("solana_sysvar::rent::<impl Sysvar for solana_rent::Rent>::get") => true

// Adjust references when moving across stack frames
rule #adjustRef(SPLRefCell(ABS_PLACE, VAL), OFFSET) => SPLRefCell(#adjustAbsPlace(ABS_PLACE, OFFSET), VAL)
rule #adjustRef(SPLDataBorrow(ABS_PLACE, VAL), OFFSET) => SPLDataBorrow(#adjustAbsPlace(ABS_PLACE, OFFSET), VAL)
rule #adjustRef(SPLDataBorrowMut(ABS_PLACE, VAL), OFFSET) => SPLDataBorrowMut(#adjustAbsPlace(ABS_PLACE, OFFSET), VAL)
rule #adjustRef(SPLDataBuffer(VAL), OFFSET) => SPLDataBuffer(#adjustRef(VAL, OFFSET))
rule #adjustRef(SPLPubkeyRef(VAL), OFFSET) => SPLPubkeyRef(#adjustRef(VAL, OFFSET))
```

## Slice metadata for SPL account buffers
Expand Down Expand Up @@ -290,29 +302,38 @@ module KMIR-SPL-TOKEN
ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplAccountKey:List))))) // pub key: &'a Pubkey
ListItem(
SPLRefCell(
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems)
AbsPlace(
0,
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems)
)
),
Integer(?SplLamports:Int, 64, false)
)
) // lamports: Rc<RefCell<&'a mut u64>>
ListItem( // data: Rc<RefCell<&'a mut [u8]>>
SPLRefCell(
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems)
AbsPlace(
0,
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems)
)
),
SPLDataBuffer( // data: Rc<RefCell<&'a mut [u8]>>, Aggregate is for &account.data
Aggregate(variantIdx(0),
ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintKey:List)))) // Account.mint: Pubkey
ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplTokenOwnerKey:List)))) // Account.owner: Pubkey
ListItem(Integer(?SplAmount:Int, 64, false)) // Account.amount: u64
ListItem(?SplDelegateCOpt:Value) // Account.delegate: COption<Pubkey>
// Model COption<Pubkey> as Some(pubkey); None is not represented here.
ListItem(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplDelegateKey:List))))))
ListItem(Integer(?SplAccountState:Int, 8, false)) // Account.state: AccountState (repr u8)
ListItem(?SplIsNativeCOpt:Value) // Account.is_native: COption<u64>
// Model COption<u64> as Some(amount); None is not represented here.
ListItem(Aggregate(variantIdx(1), ListItem(Integer(?SplIsNativeLamports:Int, 64, false))))
ListItem(Integer(?SplDelegatedAmount:Int, 64, false)) // Account.delegated_amount: u64
ListItem(?SplCloseAuthCOpt:Value) // Account.close_authority: COption<Pubkey>
// Model COption<Pubkey> as Some(pubkey); None is not represented here.
ListItem(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplCloseAuthKey:List))))))
)
)
)
Expand All @@ -338,9 +359,9 @@ module KMIR-SPL-TOKEN
andBool 0 <=Int ?SplAmount andBool ?SplAmount <Int (1 <<Int 64)
andBool 0 <=Int ?SplAccountState andBool ?SplAccountState <Int 256
andBool 0 <=Int ?SplDelegatedAmount andBool ?SplDelegatedAmount <Int (1 <<Int 64)
andBool #isSplCOptionPubkey(?SplDelegateCOpt)
andBool #isSplCOptionPubkey(?SplCloseAuthCOpt)
andBool #isSplCOptionU64(?SplIsNativeCOpt)
andBool #isSplPubkey(?SplDelegateKey)
andBool #isSplPubkey(?SplCloseAuthKey)
andBool 0 <=Int ?SplIsNativeLamports andBool ?SplIsNativeLamports <Int (1 <<Int 64)
[priority(30), preserves-definedness]

rule [cheatcode-is-spl-mint]:
Expand All @@ -351,26 +372,34 @@ module KMIR-SPL-TOKEN
ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplMintAccountKey:List))))) // pub key: &'a Pubkey
ListItem(
SPLRefCell(
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems)
AbsPlace(
0,
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems)
)
),
Integer(?SplMintLamports:Int, 64, false)
)
)
ListItem(
SPLRefCell(
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems)
AbsPlace(
0,
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems)
)
),
SPLDataBuffer(
Aggregate(variantIdx(0),
ListItem(?SplMintAuthorityCOpt:Value)
// Model COption<Pubkey> as Some(pubkey); None is not represented here.
ListItem(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintAuthorityKey:List))))))
ListItem(Integer(?SplMintSupply:Int, 64, false))
ListItem(Integer(?SplMintDecimals:Int, 8, false))
ListItem(BoolVal(false))
ListItem(?SplMintFreezeAuthorityCOpt:Value)
// Model COption<Pubkey> as Some(pubkey); None is not represented here.
ListItem(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintFreezeAuthorityKey:List))))))
)
)
)
Expand All @@ -391,10 +420,10 @@ module KMIR-SPL-TOKEN
andBool #isSplPubkey(?SplMintOwnerKey)
andBool 0 <=Int ?SplMintLamports andBool ?SplMintLamports <Int 18446744073709551616
andBool 0 <=Int ?SplMintRentEpoch andBool ?SplMintRentEpoch <Int 18446744073709551616
andBool #isSplCOptionPubkey(?SplMintAuthorityCOpt)
andBool #isSplPubkey(?SplMintAuthorityKey)
andBool 0 <=Int ?SplMintSupply andBool ?SplMintSupply <Int (1 <<Int 64)
andBool 0 <=Int ?SplMintDecimals andBool ?SplMintDecimals <Int 256
andBool #isSplCOptionPubkey(?SplMintFreezeAuthorityCOpt)
andBool #isSplPubkey(?SplMintFreezeAuthorityKey)
[priority(30), preserves-definedness]

rule [cheatcode-is-spl-rent]:
Expand All @@ -405,18 +434,24 @@ module KMIR-SPL-TOKEN
ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplRentAccountKey:List))))) // pub key: &'a Pubkey
ListItem(
SPLRefCell(
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems)
AbsPlace(
0,
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems)
)
),
Integer(?SplRentLamports:Int, 64, false)
)
) // lamports: Rc<RefCell<&'a mut u64>>
ListItem( // data: Rc<RefCell<&'a mut [u8]>>
SPLRefCell(
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems)
AbsPlace(
0,
place(
LOCAL,
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems)
)
),
SPLDataBuffer(
Aggregate(variantIdx(0),
Expand Down Expand Up @@ -463,8 +498,9 @@ expose the wrapped payload directly.
[priority(30), preserves-definedness]

syntax KItem ::= #finishSPLRcDeref ( Evaluation , Place , MaybeBasicBlockIdx ) [seqstrict(1)]
| #resolveSPLRcRef ( Value , Place , MaybeBasicBlockIdx )
| #finishResolvedSPLRc ( Place , MaybeBasicBlockIdx )
| #resolveSPLRcRef ( Value , Place , MaybeBasicBlockIdx )
| #finishResolvedSPLRc ( Place , MaybeBasicBlockIdx )
| #writeThroughAbsPlace ( AbsPlace , Value )

rule <k> #finishSPLRcDeref(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET)
=> #resolveSPLRcRef(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET)
Expand Down Expand Up @@ -510,6 +546,31 @@ expose the wrapped payload directly.
=> #setLocalValue(DEST, SPLRefCell(PLACE, VAL)) ~> #continueAt(TARGET)
...
</k>

// Cross-frame write helper for SPL ref cells
rule <k> #writeThroughAbsPlace(AbsPlace(0, place(local(I), PROJS)), VAL)
=> #forceSetPlaceValue(place(local(I), PROJS), VAL)
...
</k>
<locals> LOCALS </locals>
requires 0 <=Int I andBool I <Int size(LOCALS)
andBool isTypedLocal(LOCALS[I])

rule <k> #writeThroughAbsPlace(AbsPlace(OFFSET, place(local(I), PROJS)), VAL)
=> #traverseProjection(
toStack(OFFSET, local(I)),
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(I), OFFSET),
PROJS,
.Contexts
)
~> #writeProjection(VAL)
...
</k>
<stack> STACK </stack>
requires 0 <Int OFFSET
andBool OFFSET <=Int size(STACK)
andBool isStackFrame(STACK[OFFSET -Int 1])
andBool 0 <=Int I
```

## Pubkey references
Expand Down Expand Up @@ -540,7 +601,7 @@ expose the wrapped payload directly.

```k
// Step 1
syntax Context ::= CtxSPLRefCell ( Place )
syntax Context ::= CtxSPLRefCell ( AbsPlace )
rule <k> #traverseProjection(
DEST,
SPLRefCell(PLACE, VAL),
Expand All @@ -553,14 +614,14 @@ expose the wrapped payload directly.
PROJS,
CtxSPLRefCell(PLACE) CTXTS
)
...
</k>
...
</k>
[priority(30)]
rule #buildUpdate(VAL, CtxSPLRefCell(PLACE) CTXS) => #buildUpdate(SPLRefCell(PLACE, VAL), CTXS)
rule #projectionsFor(CtxSPLRefCell(_) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS)

// Step 2
syntax Context ::= CtxSPLDataBorrow ( Place )
syntax Context ::= CtxSPLDataBorrow ( AbsPlace )
rule <k> #traverseProjection(
DEST,
SPLDataBorrow(PLACE, VAL),
Expand All @@ -573,13 +634,13 @@ expose the wrapped payload directly.
PROJS,
CtxSPLDataBorrow(PLACE) CTXTS
)
...
</k>
...
</k>
[priority(30)]
rule #buildUpdate(VAL, CtxSPLDataBorrow(PLACE) CTXS) => #buildUpdate(SPLDataBorrow(PLACE, SPLDataBuffer(VAL)), CTXS)
rule #projectionsFor(CtxSPLDataBorrow(_) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS)

syntax Context ::= CtxSPLDataBorrowMut ( Place )
syntax Context ::= CtxSPLDataBorrowMut ( AbsPlace )
rule <k> #traverseProjection(
DEST,
SPLDataBorrowMut(PLACE, VAL),
Expand All @@ -592,8 +653,8 @@ expose the wrapped payload directly.
PROJS,
CtxSPLDataBorrowMut(PLACE) CTXTS
)
...
</k>
...
</k>
[priority(30)]
rule #buildUpdate(VAL, CtxSPLDataBorrowMut(PLACE) CTXS) => #buildUpdate(SPLDataBorrowMut(PLACE, SPLDataBuffer(VAL)), CTXS)
rule #projectionsFor(CtxSPLDataBorrowMut(_) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS)
Expand Down Expand Up @@ -762,7 +823,7 @@ expose the wrapped payload directly.
syntax KItem ::= #mkSPLAccountPack ( Evaluation , Evaluation , Place ) [seqstrict(1,2)]

rule <k> #mkSPLAccountPack(ACCOUNT, SPLDataBorrowMut(PLACE, SPLDataBuffer(_)), DEST)
=> #forceSetPlaceValue(
=> #writeThroughAbsPlace(
PLACE,
SPLRefCell(PLACE, SPLDataBuffer(ACCOUNT))
)
Expand Down
16 changes: 16 additions & 0 deletions kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -133,12 +133,24 @@ fn test_spltoken_domain_data(
multisig: &AccountInfo<'_>,
rent: &AccountInfo<'_>,
) {
test_spl_account_is_native_branches(acc);
test_spl_account_domain_data(acc);
test_spl_mint_domain_data(mint);
test_spl_multisig_domain_data(multisig);
test_spl_rent_domain_data(rent);
}

fn test_spl_account_is_native_branches(acc: &AccountInfo<'_>) {
// Keep is_native symbolic, hit pack through an extra call frame, and exercise COption::<u64>::is_some
cheatcode_is_spl_account(acc);

let account = get_account(acc);
let mut borrow = acc.data.borrow_mut();
pack_account_inner(&mut borrow, &account);

let _ = account.is_native();
}

fn test_spl_account_domain_data(acc: &AccountInfo<'_>) {
cheatcode_is_spl_account(acc);

Expand Down Expand Up @@ -242,6 +254,10 @@ fn get_multisig(acc: &AccountInfo<'_>) -> Multisig {
Multisig::unpack_unchecked(&acc.data.borrow()).unwrap()
}

fn pack_account_inner(buf: &mut [u8], account: &Account) {
Account::pack(account.clone(), buf).unwrap();
}

#[inline(never)]
fn cheatcode_is_spl_account(_: &AccountInfo<'_>) {}

Expand Down
1 change: 1 addition & 0 deletions kmir/src/tests/integration/test_integration.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@
'test_spl_mint_domain_data',
'test_spl_rent_domain_data',
'test_spl_account_lamports_read_then_write',
'test_spl_account_is_native_branch',
],
}
PROVE_RS_SHOW_SPECS = [
Expand Down
Loading