From 5fd4b514b87b77bdb542519f71f8b06591b22967 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 27 Nov 2025 13:11:49 +0800 Subject: [PATCH 01/10] feat(spl): adjustRef for spl domain data --- .../kdist/mir-semantics/symbolic/spl-token.md | 140 ++++++++++++------ .../data/prove-rs/spl_token_domain_data.rs | 21 +++ .../src/tests/integration/test_integration.py | 4 +- 3 files changed, 117 insertions(+), 48 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 eb5c7c54a..e84feafda 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -89,10 +89,10 @@ module KMIR-SPL-TOKEN ## Helper syntax ```k - syntax Value ::= SPLRefCell ( Place , Value ) + syntax Value ::= SPLRefCell ( Value , Value ) // Reference to the buffer, value in the cell | SPLDataBuffer ( Value ) - | SPLDataBorrow ( Place , Value ) - | SPLDataBorrowMut ( Place , Value ) + | SPLDataBorrow ( Value , Value ) // Reference to the buffer, borrowed value + | SPLDataBorrowMut ( Value , Value ) | SPLPubkeyRef ( Value ) ``` @@ -163,16 +163,17 @@ module KMIR-SPL-TOKEN // mock mint rule #isSPLPackFunc("Mint::pack") => 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 + // Adjust references when moving across stack frames + rule #adjustRef(SPLRefCell(PLACE, VAL), OFFSET) => SPLRefCell(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) + rule #adjustRef(SPLDataBorrow(PLACE, VAL), OFFSET) => SPLDataBorrow(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) + rule #adjustRef(SPLDataBorrowMut(PLACE, VAL), OFFSET) => SPLDataBorrowMut(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) + rule #adjustRef(SPLDataBuffer(VAL), OFFSET) => SPLDataBuffer(#adjustRef(VAL, OFFSET)) + rule #adjustRef(SPLPubkeyRef(VAL), OFFSET) => SPLPubkeyRef(#adjustRef(VAL, OFFSET)) + // COption values are pure data; adjusting references is a no-op + rule #adjustRef(VAL, _) => VAL + requires #isSplCOptionPubkey(VAL) orBool #isSplCOptionU64(VAL) + [simplification] - syntax Bool ::= #isSPLRentGetFunc ( String ) [function, total] - rule #isSPLRentGetFunc(_) => false [owise] - rule #isSPLRentGetFunc("Rent::get") => true // mock harness - rule #isSPLRentGetFunc("solana_sysvar::rent::::get") => true ``` ## Slice metadata for SPL account buffers @@ -290,29 +291,39 @@ 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) + Reference( + 0, + place( + LOCAL, + appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems) + ), + mutabilityNot, + metadata(noMetadataSize, 0, noMetadataSize) ), Integer(?SplLamports:Int, 64, false) ) ) // lamports: Rc> ListItem( // data: Rc> SPLRefCell( - place( - LOCAL, - appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems) + Reference( + 0, + place( + LOCAL, + appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems) + ), + mutabilityNot, + metadata(noMetadataSize, 0, noMetadataSize) ), SPLDataBuffer( // data: Rc>, 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 + ListItem(Aggregate(variantIdx(0), .List)) // COption default None ListItem(Integer(?SplAccountState:Int, 8, false)) // Account.state: AccountState (repr u8) - ListItem(?SplIsNativeCOpt:Value) // Account.is_native: COption + ListItem(Aggregate(variantIdx(0), .List)) // COption default None ListItem(Integer(?SplDelegatedAmount:Int, 64, false)) // Account.delegated_amount: u64 - ListItem(?SplCloseAuthCOpt:Value) // Account.close_authority: COption + ListItem(Aggregate(variantIdx(0), .List)) // COption default None ) ) ) @@ -338,9 +349,9 @@ module KMIR-SPL-TOKEN andBool 0 <=Int ?SplAmount andBool ?SplAmount #finishSPLRcDeref(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET) => #resolveSPLRcRef(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET) @@ -510,6 +532,31 @@ expose the wrapped payload directly. => #setLocalValue(DEST, SPLRefCell(PLACE, VAL)) ~> #continueAt(TARGET) ... + + // Cross-frame write helper for SPL ref cells + rule #writeThroughRef(Reference(0, place(local(I), PROJS), _, _), VAL) + => #forceSetPlaceValue(place(local(I), PROJS), VAL) + ... + + LOCALS + requires 0 <=Int I andBool I #writeThroughRef(Reference(OFFSET, place(local(I), PROJS), _, _), VAL) + => #traverseProjection( + toStack(OFFSET, local(I)), + #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(I), OFFSET), + PROJS, + .Contexts + ) + ~> #writeProjection(VAL) + ... + + STACK + requires 0 #traverseProjection( DEST, SPLRefCell(PLACE, VAL), @@ -553,14 +600,14 @@ expose the wrapped payload directly. PROJS, CtxSPLRefCell(PLACE) CTXTS ) - ... - + ... + [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 ( Value ) rule #traverseProjection( DEST, SPLDataBorrow(PLACE, VAL), @@ -573,13 +620,13 @@ expose the wrapped payload directly. PROJS, CtxSPLDataBorrow(PLACE) CTXTS ) - ... - + ... + [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 ( Value ) rule #traverseProjection( DEST, SPLDataBorrowMut(PLACE, VAL), @@ -592,8 +639,8 @@ expose the wrapped payload directly. PROJS, CtxSPLDataBorrowMut(PLACE) CTXTS ) - ... - + ... + [priority(30)] rule #buildUpdate(VAL, CtxSPLDataBorrowMut(PLACE) CTXS) => #buildUpdate(SPLDataBorrowMut(PLACE, SPLDataBuffer(VAL)), CTXS) rule #projectionsFor(CtxSPLDataBorrowMut(_) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS) @@ -762,13 +809,14 @@ expose the wrapped payload directly. syntax KItem ::= #mkSPLAccountPack ( Evaluation , Evaluation , Place ) [seqstrict(1,2)] rule #mkSPLAccountPack(ACCOUNT, SPLDataBorrowMut(PLACE, SPLDataBuffer(_)), DEST) - => #forceSetPlaceValue( + => #writeThroughRef( PLACE, SPLRefCell(PLACE, SPLDataBuffer(ACCOUNT)) ) ~> #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ... + requires isRef(PLACE) ``` ```{.k .symbolic} diff --git a/kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs b/kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs index 773548d0a..60d7cb49d 100644 --- a/kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs +++ b/kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs @@ -133,12 +133,33 @@ fn test_spltoken_domain_data( multisig: &AccountInfo<'_>, rent: &AccountInfo<'_>, ) { + test_spl_account_pack_is_native_branch(acc); + test_spl_account_is_native_branch(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_pack_is_native_branch(acc: &AccountInfo<'_>) { + // Keep is_native symbolic and pack through an extra call frame to mirror process_burn’s cross-frame writeback + cheatcode_is_spl_account(acc); + let account = get_account(acc); + let mut borrow = acc.data.borrow_mut(); + pack_account_inner(&mut borrow, &account); +} + +fn pack_account_inner(buf: &mut [u8], account: &Account) { + Account::pack(account.clone(), buf).unwrap(); +} + +fn test_spl_account_is_native_branch(acc: &AccountInfo<'_>) { + // Keep is_native symbolic and exercise COption::::is_some to reproduce the ndbranch + cheatcode_is_spl_account(acc); + let account = get_account(acc); + let _ = account.is_native(); +} + fn test_spl_account_domain_data(acc: &AccountInfo<'_>) { cheatcode_is_spl_account(acc); diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index a5b2f5cb3..b217538f4 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -38,10 +38,10 @@ 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], 'spl_token_domain_data': [ + 'test_spl_account_pack_is_native_branch', + 'test_spl_account_is_native_branch', 'test_spl_account_domain_data', 'test_spl_mint_domain_data', - 'test_spl_rent_domain_data', - 'test_spl_account_lamports_read_then_write', ], } PROVE_RS_SHOW_SPECS = [ From d40541a373ceebe2b2f5049bd3d2423fc6c60445 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 28 Nov 2025 09:51:17 +0800 Subject: [PATCH 02/10] use some pubkey by default --- .../kdist/mir-semantics/symbolic/spl-token.md | 25 +++++++++++-------- 1 file changed, 15 insertions(+), 10 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 e84feafda..bae52fb86 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -319,11 +319,14 @@ module KMIR-SPL-TOKEN 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(Aggregate(variantIdx(0), .List)) // COption default None + // Model COption 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(Aggregate(variantIdx(0), .List)) // COption default None + // Model COption 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(Aggregate(variantIdx(0), .List)) // COption default None + // Model COption as Some(pubkey); None is not represented here. + ListItem(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplCloseAuthKey:List)))))) ) ) ) @@ -349,9 +352,9 @@ module KMIR-SPL-TOKEN andBool 0 <=Int ?SplAmount andBool ?SplAmount 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(Aggregate(variantIdx(0), .List)) + // Model COption as Some(pubkey); None is not represented here. + ListItem(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintFreezeAuthorityKey:List)))))) ) ) ) @@ -412,10 +417,10 @@ module KMIR-SPL-TOKEN andBool #isSplPubkey(?SplMintOwnerKey) andBool 0 <=Int ?SplMintLamports andBool ?SplMintLamports Date: Fri, 28 Nov 2025 11:46:17 +0800 Subject: [PATCH 03/10] fix: kompile bugs caused by git rebase --- .../kdist/mir-semantics/symbolic/spl-token.md | 30 +++++++++++++++---- 1 file changed, 24 insertions(+), 6 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 bae52fb86..4e13a0d48 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -163,6 +163,14 @@ module KMIR-SPL-TOKEN // mock mint rule #isSPLPackFunc("Mint::pack") => true + syntax Bool ::= #isSPLRentFromAccountInfoFunc ( String ) [function, total] + rule #isSPLRentFromAccountInfoFunc(NAME) => findString(NAME, "Rent::from_account_info", 0) =/=Int -1 + rule #isSPLRentFromAccountInfoFunc(_) => false [owise] + + syntax Bool ::= #isSPLRentGetFunc ( String ) [function, total] + rule #isSPLRentGetFunc(NAME) => findString(NAME, "Rent::get", 0) =/=Int -1 + rule #isSPLRentGetFunc(_) => false [owise] + // Adjust references when moving across stack frames rule #adjustRef(SPLRefCell(PLACE, VAL), OFFSET) => SPLRefCell(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) rule #adjustRef(SPLDataBorrow(PLACE, VAL), OFFSET) => SPLDataBorrow(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) @@ -431,18 +439,28 @@ 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) + Reference( + 0, + place( + LOCAL, + appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems) + ), + mutabilityNot, + metadata(noMetadataSize, 0, noMetadataSize) ), Integer(?SplRentLamports:Int, 64, false) ) ) // lamports: Rc> ListItem( // data: Rc> SPLRefCell( - place( - LOCAL, - appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems) + Reference( + 0, + place( + LOCAL, + appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems) + ), + mutabilityNot, + metadata(noMetadataSize, 0, noMetadataSize) ), SPLDataBuffer( Aggregate(variantIdx(0), From c8fca402f0c3abd02cad1c17076f5bf3c9da7afc Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 28 Nov 2025 11:55:46 +0800 Subject: [PATCH 04/10] recover feature/p-token --- kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md | 7 +++++-- 1 file changed, 5 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 4e13a0d48..74b9a166f 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -163,13 +163,16 @@ module KMIR-SPL-TOKEN // mock mint rule #isSPLPackFunc("Mint::pack") => true + // Rent sysvar calls (includes mock harness direct calls to Rent::from_account_info / Rent::get) syntax Bool ::= #isSPLRentFromAccountInfoFunc ( String ) [function, total] - rule #isSPLRentFromAccountInfoFunc(NAME) => findString(NAME, "Rent::from_account_info", 0) =/=Int -1 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(NAME) => findString(NAME, "Rent::get", 0) =/=Int -1 rule #isSPLRentGetFunc(_) => false [owise] + rule #isSPLRentGetFunc("Rent::get") => true // mock harness + rule #isSPLRentGetFunc("solana_sysvar::rent::::get") => true // Adjust references when moving across stack frames rule #adjustRef(SPLRefCell(PLACE, VAL), OFFSET) => SPLRefCell(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) From c9aeb57b7e6251147d59c67ce4c9814c85dbafb4 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 28 Nov 2025 12:14:36 +0800 Subject: [PATCH 05/10] delete useless simplification rule --- kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md | 5 ----- 1 file changed, 5 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 74b9a166f..0a224ab74 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -180,11 +180,6 @@ module KMIR-SPL-TOKEN rule #adjustRef(SPLDataBorrowMut(PLACE, VAL), OFFSET) => SPLDataBorrowMut(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) rule #adjustRef(SPLDataBuffer(VAL), OFFSET) => SPLDataBuffer(#adjustRef(VAL, OFFSET)) rule #adjustRef(SPLPubkeyRef(VAL), OFFSET) => SPLPubkeyRef(#adjustRef(VAL, OFFSET)) - // COption values are pure data; adjusting references is a no-op - rule #adjustRef(VAL, _) => VAL - requires #isSplCOptionPubkey(VAL) orBool #isSplCOptionU64(VAL) - [simplification] - ``` ## Slice metadata for SPL account buffers From f07f3d3bba409056ba38a9c11c15758ea90783f4 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 1 Dec 2025 18:31:58 +0800 Subject: [PATCH 06/10] simplify the test --- .../data/prove-rs/spl_token_domain_data.rs | 21 +++++++------------ .../src/tests/integration/test_integration.py | 1 - 2 files changed, 8 insertions(+), 14 deletions(-) diff --git a/kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs b/kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs index 60d7cb49d..abe53c34e 100644 --- a/kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs +++ b/kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs @@ -133,30 +133,21 @@ fn test_spltoken_domain_data( multisig: &AccountInfo<'_>, rent: &AccountInfo<'_>, ) { - test_spl_account_pack_is_native_branch(acc); - test_spl_account_is_native_branch(acc); + 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_pack_is_native_branch(acc: &AccountInfo<'_>) { - // Keep is_native symbolic and pack through an extra call frame to mirror process_burn’s cross-frame writeback +fn test_spl_account_is_native_branches(acc: &AccountInfo<'_>) { + // Keep is_native symbolic, hit pack through an extra call frame, and exercise COption::::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); -} - -fn pack_account_inner(buf: &mut [u8], account: &Account) { - Account::pack(account.clone(), buf).unwrap(); -} -fn test_spl_account_is_native_branch(acc: &AccountInfo<'_>) { - // Keep is_native symbolic and exercise COption::::is_some to reproduce the ndbranch - cheatcode_is_spl_account(acc); - let account = get_account(acc); let _ = account.is_native(); } @@ -263,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<'_>) {} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index b217538f4..03494e75d 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -38,7 +38,6 @@ 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], 'spl_token_domain_data': [ - 'test_spl_account_pack_is_native_branch', 'test_spl_account_is_native_branch', 'test_spl_account_domain_data', 'test_spl_mint_domain_data', From 571cf15e0b2bb761bae87d3c32aeed62fd02e1e2 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 1 Dec 2025 19:22:14 +0800 Subject: [PATCH 07/10] no need strict --- kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 0a224ab74..e384d7d35 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -507,7 +507,7 @@ expose the wrapped payload directly. syntax KItem ::= #finishSPLRcDeref ( Evaluation , Place , MaybeBasicBlockIdx ) [seqstrict(1)] | #resolveSPLRcRef ( Value , Place , MaybeBasicBlockIdx ) | #finishResolvedSPLRc ( Place , MaybeBasicBlockIdx ) - | #writeThroughRef ( Value , Value ) [seqstrict(2)] + | #writeThroughRef ( Value , Value ) rule #finishSPLRcDeref(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET) => #resolveSPLRcRef(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET) From 2097ccfc304fd119243f2d1710637a4e1c812ab2 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 1 Dec 2025 20:40:07 +0800 Subject: [PATCH 08/10] introduce a new sort to describe abs place --- .../kdist/mir-semantics/symbolic/spl-token.md | 68 ++++++++----------- 1 file changed, 30 insertions(+), 38 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 e384d7d35..20444b8aa 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -89,10 +89,15 @@ module KMIR-SPL-TOKEN ## Helper syntax ```k - syntax Value ::= SPLRefCell ( Value , Value ) // Reference to the buffer, value in the cell + 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 ( Value , Value ) // Reference to the buffer, borrowed value - | SPLDataBorrowMut ( Value , Value ) + | SPLDataBorrow ( AbsPlace , Value ) // Place of the buffer, borrowed value + | SPLDataBorrowMut ( AbsPlace , Value ) | SPLPubkeyRef ( Value ) ``` @@ -175,9 +180,9 @@ module KMIR-SPL-TOKEN rule #isSPLRentGetFunc("solana_sysvar::rent::::get") => true // Adjust references when moving across stack frames - rule #adjustRef(SPLRefCell(PLACE, VAL), OFFSET) => SPLRefCell(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) - rule #adjustRef(SPLDataBorrow(PLACE, VAL), OFFSET) => SPLDataBorrow(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) - rule #adjustRef(SPLDataBorrowMut(PLACE, VAL), OFFSET) => SPLDataBorrowMut(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) + rule #adjustRef(SPLRefCell(PLACE, VAL), OFFSET) => SPLRefCell(#adjustAbsPlace(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) + rule #adjustRef(SPLDataBorrow(PLACE, VAL), OFFSET) => SPLDataBorrow(#adjustAbsPlace(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) + rule #adjustRef(SPLDataBorrowMut(PLACE, VAL), OFFSET) => SPLDataBorrowMut(#adjustAbsPlace(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) rule #adjustRef(SPLDataBuffer(VAL), OFFSET) => SPLDataBuffer(#adjustRef(VAL, OFFSET)) rule #adjustRef(SPLPubkeyRef(VAL), OFFSET) => SPLPubkeyRef(#adjustRef(VAL, OFFSET)) ``` @@ -297,28 +302,24 @@ module KMIR-SPL-TOKEN ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplAccountKey:List))))) // pub key: &'a Pubkey ListItem( SPLRefCell( - Reference( + AbsPlace( 0, place( LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems) - ), - mutabilityNot, - metadata(noMetadataSize, 0, noMetadataSize) + ) ), Integer(?SplLamports:Int, 64, false) ) ) // lamports: Rc> ListItem( // data: Rc> SPLRefCell( - Reference( + AbsPlace( 0, place( LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems) - ), - mutabilityNot, - metadata(noMetadataSize, 0, noMetadataSize) + ) ), SPLDataBuffer( // data: Rc>, Aggregate is for &account.data Aggregate(variantIdx(0), @@ -371,28 +372,24 @@ module KMIR-SPL-TOKEN ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplMintAccountKey:List))))) // pub key: &'a Pubkey ListItem( SPLRefCell( - Reference( + AbsPlace( 0, place( LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems) - ), - mutabilityNot, - metadata(noMetadataSize, 0, noMetadataSize) + ) ), Integer(?SplMintLamports:Int, 64, false) ) ) ListItem( SPLRefCell( - Reference( + AbsPlace( 0, place( LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems) - ), - mutabilityNot, - metadata(noMetadataSize, 0, noMetadataSize) + ) ), SPLDataBuffer( Aggregate(variantIdx(0), @@ -437,28 +434,24 @@ module KMIR-SPL-TOKEN ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplRentAccountKey:List))))) // pub key: &'a Pubkey ListItem( SPLRefCell( - Reference( + AbsPlace( 0, place( LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems) - ), - mutabilityNot, - metadata(noMetadataSize, 0, noMetadataSize) + ) ), Integer(?SplRentLamports:Int, 64, false) ) ) // lamports: Rc> ListItem( // data: Rc> SPLRefCell( - Reference( + AbsPlace( 0, place( LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems) - ), - mutabilityNot, - metadata(noMetadataSize, 0, noMetadataSize) + ) ), SPLDataBuffer( Aggregate(variantIdx(0), @@ -507,7 +500,7 @@ expose the wrapped payload directly. syntax KItem ::= #finishSPLRcDeref ( Evaluation , Place , MaybeBasicBlockIdx ) [seqstrict(1)] | #resolveSPLRcRef ( Value , Place , MaybeBasicBlockIdx ) | #finishResolvedSPLRc ( Place , MaybeBasicBlockIdx ) - | #writeThroughRef ( Value , Value ) + | #writeThroughAbsPlace ( AbsPlace , Value ) rule #finishSPLRcDeref(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET) => #resolveSPLRcRef(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET) @@ -555,7 +548,7 @@ expose the wrapped payload directly. // Cross-frame write helper for SPL ref cells - rule #writeThroughRef(Reference(0, place(local(I), PROJS), _, _), VAL) + rule #writeThroughAbsPlace(AbsPlace(0, place(local(I), PROJS)), VAL) => #forceSetPlaceValue(place(local(I), PROJS), VAL) ... @@ -563,7 +556,7 @@ expose the wrapped payload directly. requires 0 <=Int I andBool I #writeThroughRef(Reference(OFFSET, place(local(I), PROJS), _, _), VAL) + rule #writeThroughAbsPlace(AbsPlace(OFFSET, place(local(I), PROJS)), VAL) => #traverseProjection( toStack(OFFSET, local(I)), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(I), OFFSET), @@ -608,7 +601,7 @@ expose the wrapped payload directly. ```k // Step 1 - syntax Context ::= CtxSPLRefCell ( Value ) + syntax Context ::= CtxSPLRefCell ( AbsPlace ) rule #traverseProjection( DEST, SPLRefCell(PLACE, VAL), @@ -628,7 +621,7 @@ expose the wrapped payload directly. rule #projectionsFor(CtxSPLRefCell(_) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS) // Step 2 - syntax Context ::= CtxSPLDataBorrow ( Value ) + syntax Context ::= CtxSPLDataBorrow ( AbsPlace ) rule #traverseProjection( DEST, SPLDataBorrow(PLACE, VAL), @@ -647,7 +640,7 @@ expose the wrapped payload directly. rule #buildUpdate(VAL, CtxSPLDataBorrow(PLACE) CTXS) => #buildUpdate(SPLDataBorrow(PLACE, SPLDataBuffer(VAL)), CTXS) rule #projectionsFor(CtxSPLDataBorrow(_) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS) - syntax Context ::= CtxSPLDataBorrowMut ( Value ) + syntax Context ::= CtxSPLDataBorrowMut ( AbsPlace ) rule #traverseProjection( DEST, SPLDataBorrowMut(PLACE, VAL), @@ -830,14 +823,13 @@ expose the wrapped payload directly. syntax KItem ::= #mkSPLAccountPack ( Evaluation , Evaluation , Place ) [seqstrict(1,2)] rule #mkSPLAccountPack(ACCOUNT, SPLDataBorrowMut(PLACE, SPLDataBuffer(_)), DEST) - => #writeThroughRef( + => #writeThroughAbsPlace( PLACE, SPLRefCell(PLACE, SPLDataBuffer(ACCOUNT)) ) ~> #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ... - requires isRef(PLACE) ``` ```{.k .symbolic} From 51eb312d975033c4fa39f47de8644eed04ef9d08 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 1 Dec 2025 21:03:00 +0800 Subject: [PATCH 09/10] stop recursive adjustRef --- kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md | 6 +++--- 1 file changed, 3 insertions(+), 3 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 20444b8aa..9397ec71e 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -180,9 +180,9 @@ module KMIR-SPL-TOKEN rule #isSPLRentGetFunc("solana_sysvar::rent::::get") => true // Adjust references when moving across stack frames - rule #adjustRef(SPLRefCell(PLACE, VAL), OFFSET) => SPLRefCell(#adjustAbsPlace(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) - rule #adjustRef(SPLDataBorrow(PLACE, VAL), OFFSET) => SPLDataBorrow(#adjustAbsPlace(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) - rule #adjustRef(SPLDataBorrowMut(PLACE, VAL), OFFSET) => SPLDataBorrowMut(#adjustAbsPlace(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) + 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)) ``` From 807b1c0f56235a80551e761aeb3d653c4639181e Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 1 Dec 2025 21:04:23 +0800 Subject: [PATCH 10/10] recover integration test --- kmir/src/tests/integration/test_integration.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 03494e75d..e7d5b1df4 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -38,9 +38,11 @@ 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], 'spl_token_domain_data': [ - 'test_spl_account_is_native_branch', 'test_spl_account_domain_data', '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 = [