From 1b798923df64ddd160fbd4c8de28a270e3c50393 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 9 Dec 2025 15:42:35 +0800 Subject: [PATCH 1/7] fix(spl): refactor the spl-token cheatcode_is* --- .../kdist/mir-semantics/symbolic/spl-token.md | 576 ++++-------------- .../data/rs/spl_token_domain_data.rs | 1 - 2 files changed, 105 insertions(+), 472 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 9c8ccb78d..b86a0a19f 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -95,6 +95,14 @@ module KMIR-SPL-TOKEN | SPLDataBorrow ( Place , Value ) | SPLDataBorrowMut ( Place , Value ) | SPLPubkeyRef ( Value ) + + syntax Place ::= placeOf ( Operand ) [function] + rule placeOf(operandCopy(P)) => P + rule placeOf(operandMove(P)) => P + + syntax Operand ::= #appendProjsOp ( Operand , ProjectionElems ) [function] + rule #appendProjsOp(operandCopy(place(L, PROJS)), EXTRA) => operandCopy(place(L, appendP(PROJS, EXTRA))) + rule #appendProjsOp(operandMove(place(L, PROJS)), EXTRA) => operandMove(place(L, appendP(PROJS, EXTRA))) ``` ## Helper predicates @@ -324,67 +332,38 @@ module KMIR-SPL-TOKEN ``` ## Cheatcode handling + ```{.k .symbolic} rule [cheatcode-is-spl-account]: #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) - => #setLocalValue( - place(LOCAL, appendP(PROJS, projectionElemDeref .ProjectionElems)), - Aggregate(variantIdx(0), - 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) - ), - Integer(?SplLamports:Int, 64, false) - ) - ) // lamports: Rc> - ListItem( // data: Rc> - SPLRefCell( - place( - LOCAL, - appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems) - ), - 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 - // Model COption as - // Some(pubkey); None is not represented here. - ListItem(Aggregate(variantIdx(1), - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplDelegateKey:List)))))) - ListItem(Aggregate(variantIdx(?SplAccountState:Int), .List)) // Account.state: AccountState (repr u8) - // Allow COption with a symbolic variant (0=None, 1=Some(amount)). - ListItem(Aggregate(variantIdx(?SplIsNativeLamportsVariant:Int), - ListItem(Integer(?SplIsNativeLamports:Int, 64, false)))) - ListItem(Integer(?SplDelegatedAmount:Int, 64, false)) // Account.delegated_amount: u64 - // Model COption as - // Some(pubkey); None is not represented here. - ListItem(Aggregate(variantIdx(1), - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplCloseAuthKey:List)))))) - ) - ) - ) - ) - ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplOwnerKey:List))))) // owner: &'a Pubkey - ListItem(Integer(?SplRentEpoch:Int, 64, false)) // rent_epoch: u64 - ListItem(BoolVal(?_SplIsSigner:Bool)) // is_signer: bool - ListItem(BoolVal(?_SplIsWritable:Bool)) // is_writable: bool - ListItem(BoolVal(?_SplExecutable:Bool)) // executable: bool - ) + => #forceSetPlaceValue( + place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(1), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), + SPLDataBuffer( + 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(Aggregate(variantIdx(1), // delegate COption + ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplDelegateKey:List)))))) + ListItem(Aggregate(variantIdx(?SplAccountState:Int), .List)) // Account.state: AccountState + ListItem(Aggregate(variantIdx(?SplIsNativeLamportsVariant:Int), // is_native COption + ListItem(Integer(?SplIsNativeLamports:Int, 64, false)))) + ListItem(Integer(?SplDelegatedAmount:Int, 64, false)) // Account.delegated_amount: u64 + ListItem(Aggregate(variantIdx(1), // close_authority COption + ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplCloseAuthKey:List)))))) + ) + ) ) - ~> #execBlockIdx(TARGET) + ~> #forceSetPlaceValue( + place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), + #initBorrow(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems))), 165) + ) + ~> #execBlockIdx(TARGET) ... requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "spl_token::entrypoint::cheatcode_is_spl_account" - orBool #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "cheatcode_is_spl_account" - ensures #isSplPubkey(?SplAccountKey) - andBool #isSplPubkey(?SplOwnerKey) - andBool 0 <=Int ?SplLamports andBool ?SplLamports #initBorrow(Aggregate ( variantIdx ( 0 ) , + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , false )))))) + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , false )))))) + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , true )))))) + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Reference ( OFFSET , PLACE , MUT , metadata ( dynamicSize ( _ ) , 0 , dynamicSize ( _ )))))))) + ), N) + => Aggregate ( variantIdx ( 0 ) , + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , false )))))) + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , false )))))) + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , true )))))) + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Reference ( OFFSET , PLACE , MUT , metadata ( dynamicSize ( N ) , 0 , dynamicSize ( N )))))))) + ) ... + + + rule #traverseProjection(DEST, SPLDataBuffer(VAL), .ProjectionElems, CTXTS) ~> #derefTruncate(dynamicSize (_), PROJS) + => #traverseProjection(DEST, SPLDataBuffer(VAL), PROJS, CTXTS) ... + + rule [cheatcode-is-spl-mint]: #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) - => #setLocalValue( - place(LOCAL, appendP(PROJS, projectionElemDeref .ProjectionElems)), - Aggregate(variantIdx(0), - 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) - ), - Integer(?SplMintLamports:Int, 64, false) - ) - ) - ListItem( - SPLRefCell( - place( - LOCAL, - appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems) - ), - SPLDataBuffer( - Aggregate(variantIdx(0), - // optional key. The model always carries a payload key (never to be read if None) - ListItem(Aggregate(variantIdx(?SplMintHasAuthKey), - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintAuthorityKey:List)))))) - ListItem(Integer(?SplMintSupply:Int, 64, false)) - ListItem(Integer(?SplMintDecimals:Int, 8, false)) - ListItem(BoolVal(?_SplMintInitialised)) - // optional key. The model always carries a payload key (never to be read if None) - ListItem(Aggregate(variantIdx(?SplMintHasFreezeKey), - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintFreezeAuthorityKey:List)))))) - ) - ) - ) - ) - ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplMintOwnerKey:List))))) // owner: &'a Pubkey - ListItem(Integer(?SplMintRentEpoch:Int, 64, false)) - ListItem(BoolVal(?_SplMintIsSigner:Bool)) - ListItem(BoolVal(?_SplMintIsWritable:Bool)) - ListItem(BoolVal(?_SplMintExecutable:Bool)) - ) + => #forceSetPlaceValue( + place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(1), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), + SPLDataBuffer( + Aggregate(variantIdx(0), + // optional key. The model always carries a payload key (never to be read if None) + ListItem(Aggregate(variantIdx(?SplMintHasAuthKey:Int), // mint_authority COption + ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintAuthorityKey:List)))))) + ListItem(Integer(?SplMintSupply:Int, 64, false)) // supply: u64 + ListItem(Integer(?SplMintDecimals:Int, 8, false)) // decimals: u8 + ListItem(BoolVal(?_SplMintInitialised:Bool)) // is_initialized: bool + // optional key. The model always carries a payload key (never to be read if None) + ListItem(Aggregate(variantIdx(?SplMintHasFreezeKey:Int), // freeze_authority COption + ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintFreezeAuthorityKey:List)))))) + ) + ) ) - ~> #execBlockIdx(TARGET) + ~> #forceSetPlaceValue( + place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), + #initBorrow(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems))), 82) + ) + ~> #execBlockIdx(TARGET) ... requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "spl_token::entrypoint::cheatcode_is_spl_mint" orBool #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "cheatcode_is_spl_mint" - ensures #isSplPubkey(?SplMintAccountKey) - andBool #isSplPubkey(?SplMintOwnerKey) - andBool 0 <=Int ?SplMintHasAuthKey andBool ?SplMintHasAuthKey <=Int 1 + ensures 0 <=Int ?SplMintHasAuthKey andBool ?SplMintHasAuthKey <=Int 1 andBool #isSplPubkey(?SplMintAuthorityKey) andBool 0 <=Int ?SplMintHasFreezeKey andBool ?SplMintHasFreezeKey <=Int 1 andBool #isSplPubkey(?SplMintFreezeAuthorityKey) - andBool 0 <=Int ?SplMintLamports andBool ?SplMintLamports #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) - => #setLocalValue( - place(LOCAL, appendP(PROJS, projectionElemDeref .ProjectionElems)), - Aggregate(variantIdx(0), - 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) - ), - Integer(?SplRentLamports:Int, 64, false) - ) - ) // lamports: Rc> - ListItem( // data: Rc> - SPLRefCell( - place( - LOCAL, - appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems) - ), - SPLDataBuffer( - Aggregate(variantIdx(0), - ListItem(Integer(?SplRentLamportsPerByteYear:Int, 64, false)) - ListItem(Float(2.0, 64)) - ListItem(Integer(?SplRentBurnPercent:Int, 8, false)) - ) - ) - ) - ) - ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplRentOwnerKey:List))))) // owner: &'a Pubkey - ListItem(Integer(?SplRentRentEpoch:Int, 64, false)) // rent_epoch: u64 - ListItem(BoolVal(false)) // is_signer: bool - ListItem(BoolVal(false)) // is_writable: bool - ListItem(BoolVal(false)) // executable: bool - ) + => #forceSetPlaceValue( + place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(1), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), + SPLDataBuffer( + Aggregate(variantIdx(0), + ListItem(Integer(?SplRentLamportsPerByteYear:Int, 64, false)) // lamports_per_byte_year: u64 + ListItem(Float(2.0, 64)) // exemption_threshold: f64 + ListItem(Integer(?SplRentBurnPercent:Int, 8, false)) // burn_percent: u8 + ) + ) ) - ~> #execBlockIdx(TARGET) + ~> #forceSetPlaceValue( + place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), + #initBorrow(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems))), 17) + ) + ~> #execBlockIdx(TARGET) ... requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "spl_token::entrypoint::cheatcode_is_spl_rent" orBool #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "cheatcode_is_spl_rent" - ensures #isSplPubkey(?SplRentAccountKey) - andBool #isSplPubkey(?SplRentOwnerKey) - andBool 0 <=Int ?SplRentLamports andBool ?SplRentLamports >` - -We shortcut the MIR field access that ` as Deref>::deref` performs and -expose the wrapped payload directly. - -```k - rule [spl-rc-deref]: - #execTerminator(terminator(terminatorKindCall(FUNC, OP:Operand .Operands, DEST, TARGET, _UNWIND), _SPAN)) - => #finishSPLRcDeref(OP, DEST, TARGET) - ... - - requires #isSPLRcRefCellDerefFunc(#functionName(lookupFunction(#tyOfCall(FUNC)))) - [priority(30), preserves-definedness] - - syntax KItem ::= #finishSPLRcDeref ( Evaluation , Place , MaybeBasicBlockIdx ) [seqstrict(1)] - | #resolveSPLRcRef ( Value , Place , MaybeBasicBlockIdx ) - | #finishResolvedSPLRc ( Place , MaybeBasicBlockIdx ) - - rule #finishSPLRcDeref(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET) - => #resolveSPLRcRef(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET) - ... - - - rule #resolveSPLRcRef(Reference(0, place(local(I), PROJS), _, _), DEST, TARGET) - => #traverseProjection( - toLocal(I), - getValue(LOCALS, I), - PROJS, - .Contexts - ) - ~> #readProjection(false) - ~> #finishResolvedSPLRc(DEST, TARGET) - ... - - LOCALS - requires 0 <=Int I - andBool I #resolveSPLRcRef(Reference(OFFSET, place(local(I), PROJS), _, _), DEST, TARGET) - => #traverseProjection( - toStack(OFFSET, local(I)), - #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(I), OFFSET), - PROJS, - .Contexts - ) - ~> #readProjection(false) - ~> #finishResolvedSPLRc(DEST, TARGET) - ... - - STACK - requires 0 SPLRefCell(PLACE, VAL) ~> #finishResolvedSPLRc(DEST, TARGET) - => #setLocalValue(DEST, SPLRefCell(PLACE, VAL)) ~> #continueAt(TARGET) - ... - -``` - -## Pubkey references - -```k - syntax Context ::= "CtxSPLPubkeyRef" - - rule #traverseProjection( - DEST, - SPLPubkeyRef(VAL), - projectionElemDeref PROJS, - CTXTS - ) - => #traverseProjection( - DEST, - VAL, - PROJS, - CtxSPLPubkeyRef CTXTS - ) - ... - - [priority(30)] - rule #buildUpdate(VAL, CtxSPLPubkeyRef CTXS) => #buildUpdate(SPLPubkeyRef(VAL), CTXS) - rule #projectionsFor(CtxSPLPubkeyRef CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS) -``` - -## Borrowed buffer projections - -```k - // Step 1 - syntax Context ::= CtxSPLRefCell ( Place ) - rule #traverseProjection( - DEST, - SPLRefCell(PLACE, VAL), - projectionElemDeref PROJS, - CTXTS - ) - => #traverseProjection( - DEST, - VAL, - 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 ) - rule #traverseProjection( - DEST, - SPLDataBorrow(PLACE, VAL), - projectionElemDeref PROJS, - CTXTS - ) - => #traverseProjection( - DEST, - VAL, - 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 ) - rule #traverseProjection( - DEST, - SPLDataBorrowMut(PLACE, VAL), - projectionElemDeref PROJS, - CTXTS - ) - => #traverseProjection( - DEST, - VAL, - 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) - - // Step 3 - syntax Context ::= "CtxSPLDataBuffer" - rule #traverseProjection( - DEST, - SPLDataBuffer(VALUE), - projectionElemDeref PROJS, - CTXTS - ) - => #traverseProjection( - DEST, - VALUE, - PROJS, - CtxSPLDataBuffer CTXTS - ) - ... - - [priority(30)] - rule #buildUpdate(VAL, CtxSPLDataBuffer CTXS) => #buildUpdate(SPLDataBuffer(VAL), CTXS) - rule #projectionsFor(CtxSPLDataBuffer CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS) -``` - ## RefCell::<&mut [u8]> helpers ```k rule [spl-borrow-data]: #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) - => #mkSPLBorrowData( - DEST, - operandCopy(place(LOCAL, PROJS)), - place(LOCAL, PROJS), - #isSPLBorrowMutFunc(#functionName(lookupFunction(#tyOfCall(FUNC)))) - ) + => #setSPLBorrowData(DEST, operandCopy(place(LOCAL, PROJS))) ~> #execBlockIdx(TARGET) ... requires #isSPLBorrowFunc(#functionName(lookupFunction(#tyOfCall(FUNC)))) [priority(30), preserves-definedness] - syntax KItem ::= #mkSPLBorrowData ( Place , Evaluation , Place , Bool ) [seqstrict(2)] - - rule #mkSPLBorrowData(DEST, SPLRefCell(PLACE, BUF), _SRC, false) - => #setLocalValue(DEST, SPLRefCell(PLACE, SPLDataBorrow(PLACE, BUF))) - ... - - - rule #mkSPLBorrowData(DEST, SPLRefCell(PLACE, BUF), _SRC, true) - => #setLocalValue(DEST, SPLRefCell(PLACE, SPLDataBorrowMut(PLACE, BUF))) - ... - -``` - -## `Ref`/`RefMut` deref shortcuts - -```k - rule [spl-ref-deref]: - #execTerminator(terminator(terminatorKindCall(FUNC, ARG_OP:Operand .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) - => #mkSPLRefDeref(DEST, ARG_OP) - ~> #execBlockIdx(TARGET) - ... - - requires #isSPLRefDerefFunc(#functionName(lookupFunction(#tyOfCall(FUNC)))) - [priority(30), preserves-definedness] - - syntax KItem ::= #mkSPLRefDeref ( Place , Evaluation ) [seqstrict(2)] - - rule #mkSPLRefDeref(DEST, Reference(0, place(local(I), .ProjectionElems), _, _)) - => #mkSPLRefDeref(DEST, getValue(LOCALS, I)) - ... - - LOCALS - requires 0 <=Int I - andBool I #mkSPLRefDeref(DEST, Reference(OFFSET, place(local(I), .ProjectionElems), _, _)) - => #mkSPLRefDeref( - DEST, - #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(I), OFFSET) - ) - ... - - STACK - requires 0 #mkSPLRefDeref(DEST, SPLDataBorrow(_, _) #as BORROW) - => #setLocalValue(DEST, BORROW) - ... + syntax KItem ::= #setSPLBorrowData ( Place , Evaluation ) [seqstrict(2)] + rule #setSPLBorrowData(DEST, Reference(OFFSET, place(LOCAL, PROJS), MUT, META)) + => #setLocalValue(DEST, Aggregate(variantIdx(0), + ListItem(Aggregate(variantIdx(0), ListItem(PtrLocal(OFFSET, place(LOCAL, appendP(PROJS, projectionElemField(fieldIdx(1), #hack()) projectionElemField(fieldIdx(0), #hack()) .ProjectionElems)), MUT, META)))) + ListItem(Aggregate(variantIdx(0), ListItem(Reference(OFFSET, place (LOCAL, appendP(PROJS, projectionElemField(fieldIdx(0), #hack()) .ProjectionElems)), MUT, META)))))) ... - - rule #mkSPLRefDeref(DEST, SPLDataBorrowMut(_, _) #as BORROW) - => #setLocalValue(DEST, BORROW) - ... - - - rule [spl-ref-deref-owise]: - #mkSPLRefDeref(DEST, VAL) - => #setLocalValue(DEST, VAL) - ... - - [owise] ``` ## Account::unpack_from_slice / Account::pack_into_slice ```k rule [spl-account-unpack]: #execTerminator(terminator(terminatorKindCall(FUNC, OP:Operand .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) - => #mkSPLAccountUnpack(DEST, OP) + => #splUnpack(DEST, #withDeref(OP)) ~> #execBlockIdx(TARGET) ... requires #isSPLUnpackFunc(#functionName(lookupFunction(#tyOfCall(FUNC)))) [priority(30), preserves-definedness] - syntax KItem ::= #mkSPLAccountUnpack ( Place , Evaluation ) [seqstrict(2)] - - rule #mkSPLAccountUnpack(DEST, Reference(0, place(local(I), projectionElemDeref .ProjectionElems), _, _)) - => #mkSPLAccountUnpack(DEST, getValue(LOCALS, I)) - ... - - LOCALS - requires 0 <=Int I - andBool I #mkSPLAccountUnpack(DEST, Reference(OFFSET, place(local(I), projectionElemDeref .ProjectionElems), _, _)) - => #mkSPLAccountUnpack( - DEST, - #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(I), OFFSET) - ) - ... - - STACK - requires 0 #mkSPLAccountUnpack(DEST, SPLDataBorrow(_, SPLDataBuffer(ACCOUNT))) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(ACCOUNT))) - ... - - - rule #mkSPLAccountUnpack(DEST, SPLDataBorrowMut(_, SPLDataBuffer(ACCOUNT))) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(ACCOUNT))) - ... + syntax KItem ::= #splUnpack ( Place , Evaluation ) [seqstrict(2)] + rule #splUnpack(DEST, SPLDataBuffer(VAL)) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(VAL))) ... -``` -```k rule [spl-account-pack]: - #execTerminator(terminator(terminatorKindCall(FUNC, SRC_OP:Operand BUF_OP:Operand .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) - => #mkSPLAccountPack(SRC_OP, BUF_OP) - ~> #execBlockIdx(TARGET) - ... + #execTerminator(terminator(terminatorKindCall(FUNC, SRC:Operand DST:Operand .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) + => #splPack(SRC, #withDeref(DST)) ~> #execBlockIdx(TARGET) ... requires #isSPLPackFunc(#functionName(lookupFunction(#tyOfCall(FUNC)))) [priority(30), preserves-definedness] - syntax KItem ::= #mkSPLAccountPack ( Evaluation , Evaluation ) [seqstrict(1,2)] - - rule #mkSPLAccountPack(ACCOUNT, SPLDataBorrowMut(PLACE, SPLDataBuffer(_))) - => #forceSetPlaceValue( - PLACE, - SPLRefCell(PLACE, SPLDataBuffer(ACCOUNT)) - ) - ... - + syntax KItem ::= #splPack ( Evaluation , Evaluation ) [seqstrict(1)] + rule #splPack(VAL, DEST) => #setLocalValue(placeOf(DEST), SPLDataBuffer(VAL)) ... ``` ```{.k .symbolic} - // Rent::from_account_info + // Rent::from_account_info - navigate to data buffer using projection path from cheatcode rule [spl-rent-from-account-info]: - #execTerminator(terminator(terminatorKindCall(FUNC, OP .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) - => #mkSPLRentFromAccountInfo(DEST, OP) + #execTerminator(terminator(terminatorKindCall(FUNC, OP:Operand .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) + => #splUnpack(DEST, #appendProjsOp(OP, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(1), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)) ~> #execBlockIdx(TARGET) ... requires #isSPLRentFromAccountInfoFunc(#functionName(lookupFunction(#tyOfCall(FUNC)))) [priority(30), preserves-definedness] - - syntax KItem ::= #mkSPLRentFromAccountInfo ( Place , Evaluation ) [seqstrict(2)] - - - // Accept references without an explicit deref projection (e.g., borrowed AccountInfo locals on the stack) - rule #mkSPLRentFromAccountInfo(DEST, Reference(0, place(local(I), .ProjectionElems), _, _)) - => #mkSPLRentFromAccountInfo(DEST, getValue(LOCALS, I)) - ... - - LOCALS - requires 0 <=Int I - andBool I #mkSPLRentFromAccountInfo(DEST, Reference(OFFSET, place(local(I), .ProjectionElems), _, _)) - => #mkSPLRentFromAccountInfo( - DEST, - #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(I), OFFSET) - ) - ... - - STACK - requires 0 #mkSPLRentFromAccountInfo( - DEST, - Aggregate(variantIdx(0), - ListItem(_KEY) - ListItem(_LAMPORTS_CELL) - ListItem(SPLRefCell(_, SPLDataBuffer(RENT_DATA))) - _REST:List - ) - ) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(RENT_DATA))) - ... - ``` ```{.k .symbolic} diff --git a/kmir/src/tests/integration/data/rs/spl_token_domain_data.rs b/kmir/src/tests/integration/data/rs/spl_token_domain_data.rs index 5cbe0f734..adc4433b5 100644 --- a/kmir/src/tests/integration/data/rs/spl_token_domain_data.rs +++ b/kmir/src/tests/integration/data/rs/spl_token_domain_data.rs @@ -171,7 +171,6 @@ fn test_spl_mint_domain_data(mint: &AccountInfo<'_>) { assert_eq!(mint.data_len(), Mint::LEN); let mut mint_state = get_mint(mint); - assert!(!mint_state.is_initialized); mint_state.is_initialized = true; mint_state.supply = 42; mint_state.decimals = 9; From 194456b23ec794c69ec56b7776c8a8ec6b2cfa53 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 10 Dec 2025 10:16:51 +0800 Subject: [PATCH 2/7] chore: clean up the dead code --- .../kdist/mir-semantics/symbolic/spl-token.md | 183 +++--------------- 1 file changed, 31 insertions(+), 152 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 b86a0a19f..675cae120 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -6,23 +6,26 @@ requires "../rt/configuration.md" ``` We mirror the Solana `AccountInfo` layout so that MIR code can traverse the -fields exactly as it would against the real SPL runtime. The account data -contains the real SPL `Account` struct layout described in `info.md` -(`mint`, `owner`, `amount`, `COption`, `AccountState`, `COption`, -`delegated_amount`, `COption`). No Pinocchio-specific payloads are -embedded. +fields exactly as it would against the real SPL runtime. -## Data Access Overview +## Data Layout + +The account data uses `SPLDataBuffer` wrapper containing the actual struct: +- **Account** (165 bytes): `mint`, `owner`, `amount`, `delegate`, `state`, `is_native`, `delegated_amount`, `close_authority` +- **Mint** (82 bytes): `mint_authority`, `supply`, `decimals`, `is_initialized`, `freeze_authority` +- **Rent** (17 bytes): `lamports_per_byte_year`, `exemption_threshold`, `burn_percent` + +## Cheatcode Flow ``` -cheatcode_is_spl_account(acc) -Account::unpack_from_slice(&acc.data.borrow()) -Account::pack_into_slice(&a, &mut acc.data.borrow_mut()) - -> #isSPLRcRefCellDerefFunc (rule [spl-rc-deref]) - -> #isSPLBorrowFunc (rule [spl-borrow-data]) - -> #isSPLRefDerefFunc (rule [spl-ref-deref]) - -> Borrowed buffer projections - -> #isSPLUnpackFunc / #isSPLPackFunc (rule [spl-account-unpack]) +cheatcode_is_spl_account(acc) -> sets SPLDataBuffer at data field, initializes borrow metadata +cheatcode_is_spl_mint(acc) -> sets SPLDataBuffer at data field, initializes borrow metadata +cheatcode_is_spl_rent(acc) -> sets SPLDataBuffer at data field, initializes borrow metadata + +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::get() -> returns cached or new symbolic Rent value ``` @@ -90,11 +93,7 @@ module KMIR-SPL-TOKEN ## Helper syntax ```k - syntax Value ::= SPLRefCell ( Place , Value ) - | SPLDataBuffer ( Value ) - | SPLDataBorrow ( Place , Value ) - | SPLDataBorrowMut ( Place , Value ) - | SPLPubkeyRef ( Value ) + syntax Value ::= SPLDataBuffer ( Value ) syntax Place ::= placeOf ( Operand ) [function] rule placeOf(operandCopy(P)) => P @@ -111,29 +110,11 @@ module KMIR-SPL-TOKEN syntax Bool ::= #isSplPubkey ( List ) [function, total] rule #isSplPubkey(KEY) => size(KEY) ==Int 32 andBool allBytes(KEY) - syntax Bool ::= #isSplCOptionPubkey ( Value ) [function, total] - rule #isSplCOptionPubkey(Aggregate(variantIdx(0), .List)) => true - rule #isSplCOptionPubkey(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Range(KEY)))))) - => #isSplPubkey(KEY) - rule #isSplCOptionPubkey(_) => false [owise] - - syntax Bool ::= #isSplCOptionU64 ( Value ) [function, total] - rule #isSplCOptionU64(Aggregate(variantIdx(0), .List)) => true - rule #isSplCOptionU64(Aggregate(variantIdx(1), ListItem(Integer(AMT, 64, false)) REST)) - => 0 <=Int AMT andBool AMT false [owise] - // AccountState in SPL semantics is carried as an enum variantIdx(0..2); accept legacy u8 too. syntax Bool ::= #isSplAccountStateVal ( Value ) [function, total] rule #isSplAccountStateVal(Aggregate(variantIdx(N), .List)) => 0 <=Int N andBool N <=Int 2 rule #isSplAccountStateVal(_) => false [owise] - syntax Bool ::= #isSPLRcRefCellDerefFunc ( String ) [function, total] - rule #isSPLRcRefCellDerefFunc("> as std::ops::Deref>::deref") => true - rule #isSPLRcRefCellDerefFunc("> as std::ops::Deref>::deref") => true - rule #isSPLRcRefCellDerefFunc(_) => false [owise] - syntax Bool ::= #isSPLBorrowFunc ( String ) [function, total] rule #isSPLBorrowFunc("std::cell::RefCell::<&mut [u8]>::borrow") => true rule #isSPLBorrowFunc("std::cell::RefCell::<&mut [u8]>::borrow_mut") => true @@ -141,18 +122,6 @@ module KMIR-SPL-TOKEN rule #isSPLBorrowFunc("std::cell::RefCell::<&mut u64>::borrow_mut") => true rule #isSPLBorrowFunc(_) => false [owise] - syntax Bool ::= #isSPLBorrowMutFunc ( String ) [function, total] - rule #isSPLBorrowMutFunc("std::cell::RefCell::<&mut [u8]>::borrow_mut") => true - rule #isSPLBorrowMutFunc("std::cell::RefCell::<&mut u64>::borrow_mut") => true - rule #isSPLBorrowMutFunc(_) => false [owise] - - syntax Bool ::= #isSPLRefDerefFunc ( String ) [function, total] - rule #isSPLRefDerefFunc(" as std::ops::Deref>::deref") => true - rule #isSPLRefDerefFunc(" as std::ops::DerefMut>::deref_mut") => true - rule #isSPLRefDerefFunc(" as std::ops::Deref>::deref") => true - rule #isSPLRefDerefFunc(" as std::ops::DerefMut>::deref_mut") => true - rule #isSPLRefDerefFunc(_) => false [owise] - syntax Bool ::= #isSPLUnpackFunc ( String ) [function, total] rule #isSPLUnpackFunc(_) => false [owise] // spl-token account @@ -186,7 +155,7 @@ module KMIR-SPL-TOKEN ## Slice metadata for SPL account buffers ```k - // Account data (&mut [u8]) length hints (Account::LEN) + // Account data buffer length (Account::LEN = 165) rule #maybeDynamicSize( dynamicSize(_), SPLDataBuffer( @@ -206,45 +175,7 @@ module KMIR-SPL-TOKEN requires #isSplAccountStateVal(STATE) [priority(30)] - rule #maybeDynamicSize( - dynamicSize(_), - SPLDataBorrow(_, SPLDataBuffer( - Aggregate(variantIdx(0), - ListItem(Aggregate(variantIdx(0), ListItem(Range(_)))) - ListItem(Aggregate(variantIdx(0), ListItem(Range(_)))) - ListItem(Integer(_, 64, false)) - ListItem(_DELEG) - ListItem(STATE) - ListItem(_IS_NATIVE) - ListItem(Integer(_, 64, false)) - ListItem(_CLOSE) - ) - )) - ) - => dynamicSize(165) - requires #isSplAccountStateVal(STATE) - [priority(30)] - - rule #maybeDynamicSize( - dynamicSize(_), - SPLDataBorrowMut(_, SPLDataBuffer( - Aggregate(variantIdx(0), - ListItem(Aggregate(variantIdx(0), ListItem(Range(_)))) - ListItem(Aggregate(variantIdx(0), ListItem(Range(_)))) - ListItem(Integer(_, 64, false)) - ListItem(_DELEG) - ListItem(STATE) - ListItem(_IS_NATIVE) - ListItem(Integer(_, 64, false)) - ListItem(_CLOSE) - ) - )) - ) - => dynamicSize(165) - requires #isSplAccountStateVal(STATE) - [priority(30)] - - // Mint data (&mut [u8]) length hints (Mint::LEN) + // Mint data buffer length (Mint::LEN = 82) rule #maybeDynamicSize( dynamicSize(_), SPLDataBuffer( @@ -260,37 +191,7 @@ module KMIR-SPL-TOKEN => dynamicSize(82) [priority(30)] - rule #maybeDynamicSize( - dynamicSize(_), - SPLDataBorrow(_, SPLDataBuffer( - Aggregate(variantIdx(0), - ListItem(_AUTH) - ListItem(Integer(_, 64, false)) - ListItem(Integer(_, 8, false)) - ListItem(BoolVal(_)) - ListItem(_FREEZE) - ) - )) - ) - => dynamicSize(82) - [priority(30)] - - rule #maybeDynamicSize( - dynamicSize(_), - SPLDataBorrowMut(_, SPLDataBuffer( - Aggregate(variantIdx(0), - ListItem(_AUTH) - ListItem(Integer(_, 64, false)) - ListItem(Integer(_, 8, false)) - ListItem(BoolVal(_)) - ListItem(_FREEZE) - ) - )) - ) - => dynamicSize(82) - [priority(30)] - - // Rent data (&mut [u8]) length hints (Rent::LEN) + // Rent data buffer length (Rent::LEN = 17) rule #maybeDynamicSize( dynamicSize(_), SPLDataBuffer( @@ -303,32 +204,6 @@ module KMIR-SPL-TOKEN ) => dynamicSize(17) [priority(30)] - - rule #maybeDynamicSize( - dynamicSize(_), - SPLDataBorrow(_, SPLDataBuffer( - Aggregate(variantIdx(0), - ListItem(Integer(_, 64, false)) - ListItem(Float(2.0, 64)) - ListItem(Integer(_, 8, false)) - ) - )) - ) - => dynamicSize(17) - [priority(30)] - - rule #maybeDynamicSize( - dynamicSize(_), - SPLDataBorrowMut(_, SPLDataBuffer( - Aggregate(variantIdx(0), - ListItem(Integer(_, 64, false)) - ListItem(Float(2.0, 64)) - ListItem(Integer(_, 8, false)) - ) - )) - ) - => dynamicSize(17) - [priority(30)] ``` ## Cheatcode handling @@ -454,9 +329,10 @@ module KMIR-SPL-TOKEN [priority(30), preserves-definedness] ``` -## RefCell::<&mut [u8]> helpers +## RefCell borrow helpers ```k + // RefCell::<&mut [u8]>::borrow / borrow_mut - returns Ref/RefMut wrapper with pointer to data rule [spl-borrow-data]: #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) => #setSPLBorrowData(DEST, operandCopy(place(LOCAL, PROJS))) @@ -474,8 +350,10 @@ module KMIR-SPL-TOKEN ``` -## Account::unpack_from_slice / Account::pack_into_slice +## Pack / Unpack operations + ```k + // Account/Mint::unpack_from_slice - extracts struct from SPLDataBuffer rule [spl-account-unpack]: #execTerminator(terminator(terminatorKindCall(FUNC, OP:Operand .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) => #splUnpack(DEST, #withDeref(OP)) @@ -490,6 +368,7 @@ module KMIR-SPL-TOKEN => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(VAL))) ... + // Account/Mint::pack_into_slice - writes struct into SPLDataBuffer rule [spl-account-pack]: #execTerminator(terminator(terminatorKindCall(FUNC, SRC:Operand DST:Operand .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) => #splPack(SRC, #withDeref(DST)) ~> #execBlockIdx(TARGET) ... @@ -501,8 +380,10 @@ module KMIR-SPL-TOKEN rule #splPack(VAL, DEST) => #setLocalValue(placeOf(DEST), SPLDataBuffer(VAL)) ... ``` +## Rent sysvar handling + ```{.k .symbolic} - // Rent::from_account_info - navigate to data buffer using projection path from cheatcode + // Rent::from_account_info - navigates to data buffer using projection path rule [spl-rent-from-account-info]: #execTerminator(terminator(terminatorKindCall(FUNC, OP:Operand .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) => #splUnpack(DEST, #appendProjsOp(OP, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(1), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)) @@ -511,10 +392,8 @@ module KMIR-SPL-TOKEN requires #isSPLRentFromAccountInfoFunc(#functionName(lookupFunction(#tyOfCall(FUNC)))) [priority(30), preserves-definedness] -``` -```{.k .symbolic} - // Rent::get (stable value, stored once in outermost frame like p-token SysRent) + // Rent::get - returns stable value, cached in outermost frame rule [spl-rent-get]: #execTerminator(terminator(terminatorKindCall(FUNC, .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) => #writeSPLSysRent(DEST) From a69fab2b777edba81005913c4b86e7b0ed614af5 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 10 Dec 2025 10:32:59 +0800 Subject: [PATCH 3/7] docs: provide information for the structure of the data --- .../kdist/mir-semantics/symbolic/spl-token.md | 93 ++++++++++++++++--- 1 file changed, 79 insertions(+), 14 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 675cae120..42f54d4b6 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -208,11 +208,76 @@ module KMIR-SPL-TOKEN ## Cheatcode handling +The cheatcode functions receive an `&AccountInfo` argument. To access the underlying +data buffer, we navigate through the following Solana AccountInfo structure: + +``` +AccountInfo (arg is &AccountInfo, so first deref) +├── field 0: key: &Pubkey +├── field 1: lamports: Rc> +├── field 2: data: Rc> <- we want this +│ └── Rc +│ └── field 0: RcInner +│ └── field 0: Cell (strong count) +│ └── field 1: Cell (weak count) +│ └── field 2: T = RefCell<&mut [u8]> +│ └── field 0: Cell +│ └── field 1: UnsafeCell<&mut [u8]> +│ └── field 0: &mut [u8] <- the actual data buffer (deref to get [u8]) +├── field 3: owner: &Pubkey +├── ... +``` + +**Projection path to data buffer** (DATA_BUFFER_PROJS): +``` +Deref -> AccountInfo (deref &AccountInfo) +Field(2) -> .data (Rc>) +Field(0) -> RcInner (RcInner>) +Field(0) -> first field (due to repr, actual RefCell is here) +Deref -> RefCell content (deref the pointer inside Rc) +Field(2) -> RefCell.value (UnsafeCell<&mut [u8]>) +Field(1) -> UnsafeCell.value (the &mut [u8] reference) +Field(0) -> inner value +Deref -> [u8] (the actual byte slice) +``` + +**Projection path to RefCell** (REFCELL_PROJS) - used for initializing borrow metadata: +``` +Deref -> AccountInfo +Field(2) -> .data +Field(0) -> RcInner +Field(0) -> RefCell location +Deref -> RefCell content +``` + ```{.k .symbolic} + // Projection path constants for navigating AccountInfo structure + // Path to the actual data buffer: AccountInfo -> data -> Rc -> RcInner -> RefCell -> UnsafeCell -> &mut [u8] -> [u8] + syntax ProjectionElems ::= "DATA_BUFFER_PROJS" [alias] + rule DATA_BUFFER_PROJS => projectionElemDeref // deref &AccountInfo + projectionElemField(fieldIdx(2), #hack()) // .data (Rc>) + projectionElemField(fieldIdx(0), #hack()) // RcInner + projectionElemField(fieldIdx(0), #hack()) // first field (RefCell location) + projectionElemDeref // deref Rc pointer + projectionElemField(fieldIdx(2), #hack()) // RefCell.value (UnsafeCell) + projectionElemField(fieldIdx(1), #hack()) // UnsafeCell.value + projectionElemField(fieldIdx(0), #hack()) // inner + projectionElemDeref // deref to [u8] + .ProjectionElems + + // Path to RefCell for borrow metadata: AccountInfo -> data -> Rc -> RcInner -> RefCell + syntax ProjectionElems ::= "REFCELL_PROJS" [alias] + rule REFCELL_PROJS => projectionElemDeref // deref &AccountInfo + projectionElemField(fieldIdx(2), #hack()) // .data + projectionElemField(fieldIdx(0), #hack()) // RcInner + projectionElemField(fieldIdx(0), #hack()) // RefCell location + projectionElemDeref // deref Rc pointer + .ProjectionElems + rule [cheatcode-is-spl-account]: #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) => #forceSetPlaceValue( - place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(1), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), + place(LOCAL, appendP(PROJS, DATA_BUFFER_PROJS)), // navigate to [u8] data buffer SPLDataBuffer( Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintKey:List)))) // Account.mint: Pubkey @@ -230,9 +295,9 @@ module KMIR-SPL-TOKEN ) ) ~> #forceSetPlaceValue( - place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), - #initBorrow(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems))), 165) - ) + place(LOCAL, appendP(PROJS, REFCELL_PROJS)), // navigate to RefCell for borrow init + #initBorrow(operandCopy(place(LOCAL, appendP(PROJS, REFCELL_PROJS))), 165) + ) ~> #execBlockIdx(TARGET) ... @@ -271,7 +336,7 @@ module KMIR-SPL-TOKEN rule [cheatcode-is-spl-mint]: #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) => #forceSetPlaceValue( - place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(1), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), + place(LOCAL, appendP(PROJS, DATA_BUFFER_PROJS)), // navigate to [u8] data buffer SPLDataBuffer( Aggregate(variantIdx(0), // optional key. The model always carries a payload key (never to be read if None) @@ -287,9 +352,9 @@ module KMIR-SPL-TOKEN ) ) ~> #forceSetPlaceValue( - place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), - #initBorrow(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems))), 82) - ) + place(LOCAL, appendP(PROJS, REFCELL_PROJS)), // navigate to RefCell for borrow init + #initBorrow(operandCopy(place(LOCAL, appendP(PROJS, REFCELL_PROJS))), 82) + ) ~> #execBlockIdx(TARGET) ... @@ -306,7 +371,7 @@ module KMIR-SPL-TOKEN rule [cheatcode-is-spl-rent]: #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) => #forceSetPlaceValue( - place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(1), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), + place(LOCAL, appendP(PROJS, DATA_BUFFER_PROJS)), // navigate to [u8] data buffer SPLDataBuffer( Aggregate(variantIdx(0), ListItem(Integer(?SplRentLamportsPerByteYear:Int, 64, false)) // lamports_per_byte_year: u64 @@ -316,9 +381,9 @@ module KMIR-SPL-TOKEN ) ) ~> #forceSetPlaceValue( - place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)), - #initBorrow(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems))), 17) - ) + place(LOCAL, appendP(PROJS, REFCELL_PROJS)), // navigate to RefCell for borrow init + #initBorrow(operandCopy(place(LOCAL, appendP(PROJS, REFCELL_PROJS))), 17) + ) ~> #execBlockIdx(TARGET) ... @@ -383,10 +448,10 @@ module KMIR-SPL-TOKEN ## Rent sysvar handling ```{.k .symbolic} - // Rent::from_account_info - navigates to data buffer using projection path + // Rent::from_account_info - navigates to data buffer using DATA_BUFFER_PROJS rule [spl-rent-from-account-info]: #execTerminator(terminator(terminatorKindCall(FUNC, OP:Operand .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) - => #splUnpack(DEST, #appendProjsOp(OP, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref projectionElemField(fieldIdx(2), #hack()) projectionElemField(fieldIdx(1), #hack()) projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)) + => #splUnpack(DEST, #appendProjsOp(OP, DATA_BUFFER_PROJS)) ~> #execBlockIdx(TARGET) ... From ac4f36b444a55b899190376ae180881cdae15418 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 10 Dec 2025 10:48:14 +0800 Subject: [PATCH 4/7] allow None for COption values --- kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md | 8 +++++--- 1 file changed, 5 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 42f54d4b6..9018da2d4 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -283,13 +283,13 @@ Deref -> RefCell content 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(1), // delegate COption + ListItem(Aggregate(variantIdx(?SplHasDelegateKey:Int), // delegate COption ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplDelegateKey:List)))))) ListItem(Aggregate(variantIdx(?SplAccountState:Int), .List)) // Account.state: AccountState ListItem(Aggregate(variantIdx(?SplIsNativeLamportsVariant:Int), // is_native COption ListItem(Integer(?SplIsNativeLamports:Int, 64, false)))) ListItem(Integer(?SplDelegatedAmount:Int, 64, false)) // Account.delegated_amount: u64 - ListItem(Aggregate(variantIdx(1), // close_authority COption + ListItem(Aggregate(variantIdx(?SplHasCloseAuthKey:Int), // close_authority COption ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplCloseAuthKey:List)))))) ) ) @@ -305,13 +305,15 @@ Deref -> RefCell content orBool #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "cheatcode_is_spl_account" ensures #isSplPubkey(?SplMintKey) andBool #isSplPubkey(?SplTokenOwnerKey) + andBool 0 <=Int ?SplHasDelegateKey andBool ?SplHasDelegateKey <=Int 1 andBool #isSplPubkey(?SplDelegateKey) - andBool #isSplPubkey(?SplCloseAuthKey) andBool 0 <=Int ?SplAmount andBool ?SplAmount Date: Wed, 10 Dec 2025 10:49:52 +0800 Subject: [PATCH 5/7] add comments for #initBorrow --- .../kdist/mir-semantics/symbolic/spl-token.md | 33 +++++++++++++++---- 1 file changed, 26 insertions(+), 7 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 9018da2d4..c97074335 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -250,6 +250,17 @@ Field(0) -> RefCell location Deref -> RefCell content ``` +**RefCell<&mut [u8]> structure** - used by `#initBorrow` to set correct buffer size: +``` +RefCell<&mut [u8]> +├── field 0: Cell (BorrowFlag - borrow state counter) +├── field 1: Cell (borrow count for runtime checking) +├── field 2: UnsafeCell<&mut [u8]> +│ └── field 0: &mut [u8] (the actual reference) +│ └── metadata: dynamicSize(N) (buffer length: Account=165, Mint=82, Rent=17) +``` +The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynamicSize. + ```{.k .symbolic} // Projection path constants for navigating AccountInfo structure // Path to the actual data buffer: AccountInfo -> data -> Rc -> RcInner -> RefCell -> UnsafeCell -> &mut [u8] -> [u8] @@ -316,18 +327,26 @@ Deref -> RefCell content andBool #isSplPubkey(?SplCloseAuthKey) [priority(30), preserves-definedness] + // #initBorrow(RefCell, N) - Initialize RefCell borrow metadata with correct buffer size + // RefCell<&mut [u8]> layout: + // field 0: BorrowFlag (Cell) - borrow state counter + // field 1: borrow count (for runtime borrow checking) + // field 2: UnsafeCell<&mut [u8]> containing the actual reference with metadata + // This rule: + // 1. Resets borrow counters to 0 (no active borrows) + // 2. Sets the dynamicSize in metadata to N (the known buffer length: 165/82/17) syntax Evaluation ::= #initBorrow(Evaluation, Int) [seqstrict(1)] rule #initBorrow(Aggregate ( variantIdx ( 0 ) , - ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , false )))))) - ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , false )))))) - ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , true )))))) - ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Reference ( OFFSET , PLACE , MUT , metadata ( dynamicSize ( _ ) , 0 , dynamicSize ( _ )))))))) + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , false )))))) // borrow flag + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , false )))))) // borrow count + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , true )))))) // inner wrapper + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Reference ( OFFSET , PLACE , MUT , metadata ( dynamicSize ( _ ) , 0 , dynamicSize ( _ )))))))) // &mut [u8] reference ), N) => Aggregate ( variantIdx ( 0 ) , - ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , false )))))) - ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , false )))))) + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , false )))))) // reset borrow flag to 0 + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , false )))))) // reset borrow count to 0 ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , true )))))) - ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Reference ( OFFSET , PLACE , MUT , metadata ( dynamicSize ( N ) , 0 , dynamicSize ( N )))))))) + ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Reference ( OFFSET , PLACE , MUT , metadata ( dynamicSize ( N ) , 0 , dynamicSize ( N )))))))) // set size to N ) ... From acdd9e2ffd0d7a045c79bed7508e89acdc8e7827 Mon Sep 17 00:00:00 2001 From: JianHong Zhao Date: Wed, 10 Dec 2025 11:07:28 +0800 Subject: [PATCH 6/7] Update kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md Co-authored-by: Jost Berthold --- 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 c97074335..194cc5cb0 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -232,8 +232,8 @@ AccountInfo (arg is &AccountInfo, so first deref) ``` Deref -> AccountInfo (deref &AccountInfo) Field(2) -> .data (Rc>) -Field(0) -> RcInner (RcInner>) -Field(0) -> first field (due to repr, actual RefCell is here) +Field(0) -> RcInner (NonNull>>) +Field(0) -> actual pointer (*RcInner>) Deref -> RefCell content (deref the pointer inside Rc) Field(2) -> RefCell.value (UnsafeCell<&mut [u8]>) Field(1) -> UnsafeCell.value (the &mut [u8] reference) From e381b09c3bee17f512d455cb584e81b4455a6429 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 10 Dec 2025 13:56:09 +0800 Subject: [PATCH 7/7] align with real spl-token program --- .../kdist/mir-semantics/symbolic/spl-token.md | 14 ++++------ .../data/rs/spl_token_domain_data.rs | 28 +++++++++---------- 2 files changed, 20 insertions(+), 22 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 c97074335..591e154c2 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -95,13 +95,10 @@ module KMIR-SPL-TOKEN ```k syntax Value ::= SPLDataBuffer ( Value ) - syntax Place ::= placeOf ( Operand ) [function] - rule placeOf(operandCopy(P)) => P - rule placeOf(operandMove(P)) => P - - syntax Operand ::= #appendProjsOp ( Operand , ProjectionElems ) [function] + syntax Operand ::= #appendProjsOp ( Operand , ProjectionElems ) [function, total] rule #appendProjsOp(operandCopy(place(L, PROJS)), EXTRA) => operandCopy(place(L, appendP(PROJS, EXTRA))) rule #appendProjsOp(operandMove(place(L, PROJS)), EXTRA) => operandMove(place(L, appendP(PROJS, EXTRA))) + rule #appendProjsOp(OP, _) => OP [owise] ``` ## Helper predicates @@ -457,13 +454,14 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami // Account/Mint::pack_into_slice - writes struct into SPLDataBuffer rule [spl-account-pack]: #execTerminator(terminator(terminatorKindCall(FUNC, SRC:Operand DST:Operand .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN)) - => #splPack(SRC, #withDeref(DST)) ~> #execBlockIdx(TARGET) ... + => #splPack(#withDeref(SRC), #withDeref(DST)) ~> #execBlockIdx(TARGET) ... requires #isSPLPackFunc(#functionName(lookupFunction(#tyOfCall(FUNC)))) [priority(30), preserves-definedness] - syntax KItem ::= #splPack ( Evaluation , Evaluation ) [seqstrict(1)] - rule #splPack(VAL, DEST) => #setLocalValue(placeOf(DEST), SPLDataBuffer(VAL)) ... + syntax KItem ::= #splPack ( Evaluation , Operand ) [seqstrict(1)] + rule #splPack(VAL, operandCopy(DEST)) => #setLocalValue(DEST, SPLDataBuffer(VAL)) ... + rule #splPack(VAL, operandMove(DEST)) => #setLocalValue(DEST, SPLDataBuffer(VAL)) ... ``` ## Rent sysvar handling diff --git a/kmir/src/tests/integration/data/rs/spl_token_domain_data.rs b/kmir/src/tests/integration/data/rs/spl_token_domain_data.rs index adc4433b5..2520ea036 100644 --- a/kmir/src/tests/integration/data/rs/spl_token_domain_data.rs +++ b/kmir/src/tests/integration/data/rs/spl_token_domain_data.rs @@ -38,18 +38,18 @@ fn main() { ); let mut mint_data = [0u8; Mint::LEN]; - Mint::pack(Mint::default(), &mut mint_data).unwrap(); + Mint::pack(&Mint::default(), &mut mint_data).unwrap(); let mut mint_lamports = 0; let mint = AccountInfo::from_data(&mut mint_data[..], &MINT_KEY, &TOKEN_PROGRAM_ID, &mut mint_lamports); let mut multisig_data = [0u8; Multisig::LEN]; - Multisig::pack(Multisig::default(), &mut multisig_data).unwrap(); + Multisig::pack(&Multisig::default(), &mut multisig_data).unwrap(); let mut multisig_lamports = 0; let multisig = AccountInfo::from_data(&mut multisig_data[..], &MULTISIG_KEY, &TOKEN_PROGRAM_ID, &mut multisig_lamports); let mut rent_data = [0u8; Rent::LEN]; - Rent::pack(Rent::default(), &mut rent_data).unwrap(); + Rent::pack(&Rent::default(), &mut rent_data).unwrap(); let mut rent_lamports = RENT_LAMPORTS; let rent = AccountInfo::new( &SYSVAR_RENT_ID, @@ -87,7 +87,7 @@ impl<'a> AccountInfo<'a> { owner: &'a Pubkey, lamports: &'a mut u64, ) -> Self { - Account::pack(account, data).unwrap(); + Account::pack(&account, data).unwrap(); Self::from_data(data, key, owner, lamports) } @@ -154,7 +154,7 @@ fn test_spl_account_domain_data(acc: &AccountInfo<'_>) { account.state = AccountState::Initialized; account.delegated_amount = 789; account.close_authority = COption::Some(ACCOUNT_CLOSE_AUTHORITY); - Account::pack(account, &mut acc.data.borrow_mut()).unwrap(); + Account::pack(&account, &mut acc.data.borrow_mut()).unwrap(); let unpacked_account = get_account(acc); assert!(unpacked_account.is_native()); assert_eq!(unpacked_account.mint, MINT_KEY); @@ -176,7 +176,7 @@ fn test_spl_mint_domain_data(mint: &AccountInfo<'_>) { mint_state.decimals = 9; mint_state.mint_authority = COption::Some(MINT_AUTHORITY); mint_state.freeze_authority = COption::Some(FREEZE_AUTHORITY); - Mint::pack(mint_state, &mut mint.data.borrow_mut()).unwrap(); + Mint::pack(&mint_state, &mut mint.data.borrow_mut()).unwrap(); let unpacked_mint = get_mint(mint); assert!(unpacked_mint.is_initialized); assert_eq!(unpacked_mint.supply, 42); @@ -196,7 +196,7 @@ fn test_spl_multisig_domain_data(multisig: &AccountInfo<'_>) { multisig_state.signers[0] = MULTISIG_SIGNER_A; multisig_state.signers[1] = MULTISIG_SIGNER_B; multisig_state.signers[2] = MULTISIG_SIGNER_C; - Multisig::pack(multisig_state, &mut multisig.data.borrow_mut()).unwrap(); + Multisig::pack(&multisig_state, &mut multisig.data.borrow_mut()).unwrap(); let unpacked_multisig = get_multisig(multisig); assert!(unpacked_multisig.is_initialized); assert_eq!(unpacked_multisig.m, 2); @@ -351,7 +351,7 @@ impl Account { Self::unpack_from_slice(data) } - fn pack_into_slice(self, dst: &mut [u8]) { + fn pack_into_slice(&self, dst: &mut [u8]) { dst[0..32].copy_from_slice(self.mint.as_ref()); dst[32..64].copy_from_slice(self.owner.as_ref()); dst[64..72].copy_from_slice(&self.amount.to_le_bytes()); @@ -362,7 +362,7 @@ impl Account { encode_coption_key(&self.close_authority, &mut dst[129..165]); } - fn pack(account: Account, dst: &mut [u8]) -> Result<(), ProgramError> { + fn pack(account: &Account, dst: &mut [u8]) -> Result<(), ProgramError> { if dst.len() < Self::LEN { return Err(ProgramError::InvalidAccountData); } @@ -421,7 +421,7 @@ impl Mint { Self::unpack_from_slice(data) } - fn pack_into_slice(self, dst: &mut [u8]) { + fn pack_into_slice(&self, dst: &mut [u8]) { encode_coption_key(&self.mint_authority, &mut dst[0..36]); dst[36..44].copy_from_slice(&self.supply.to_le_bytes()); dst[44] = self.decimals; @@ -429,7 +429,7 @@ impl Mint { encode_coption_key(&self.freeze_authority, &mut dst[46..82]); } - fn pack(mint: Mint, dst: &mut [u8]) -> Result<(), ProgramError> { + fn pack(mint: &Mint, dst: &mut [u8]) -> Result<(), ProgramError> { if dst.len() < Self::LEN { return Err(ProgramError::InvalidAccountData); } @@ -491,7 +491,7 @@ impl Multisig { Self::unpack_from_slice(data) } - fn pack_into_slice(self, dst: &mut [u8]) { + fn pack_into_slice(&self, dst: &mut [u8]) { dst[0] = self.m; dst[1] = self.n; dst[2] = self.is_initialized as u8; @@ -501,7 +501,7 @@ impl Multisig { } } - fn pack(multisig: Multisig, dst: &mut [u8]) -> Result<(), ProgramError> { + fn pack(multisig: &Multisig, dst: &mut [u8]) -> Result<(), ProgramError> { if dst.len() < Self::LEN { return Err(ProgramError::InvalidAccountData); } @@ -564,7 +564,7 @@ impl Rent { }) } - fn pack(rent: Rent, dst: &mut [u8]) -> Result<(), ProgramError> { + fn pack(rent: &Rent, dst: &mut [u8]) -> Result<(), ProgramError> { if dst.len() < Self::LEN { return Err(ProgramError::InvalidAccountData); }