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..9397ec71e 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 ( 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 ) ``` @@ -173,6 +178,13 @@ module KMIR-SPL-TOKEN 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(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 @@ -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> ListItem( // data: Rc> 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>, 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 + // 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(?SplIsNativeCOpt:Value) // Account.is_native: COption + // 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(?SplCloseAuthCOpt:Value) // Account.close_authority: COption + // Model COption as Some(pubkey); None is not represented here. + ListItem(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplCloseAuthKey:List)))))) ) ) ) @@ -338,9 +359,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(?SplMintFreezeAuthorityCOpt:Value) + // Model COption as Some(pubkey); None is not represented here. + ListItem(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintFreezeAuthorityKey:List)))))) ) ) ) @@ -391,10 +420,10 @@ module KMIR-SPL-TOKEN andBool #isSplPubkey(?SplMintOwnerKey) andBool 0 <=Int ?SplMintLamports andBool ?SplMintLamports > ListItem( // data: Rc> 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), @@ -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 #finishSPLRcDeref(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET) => #resolveSPLRcRef(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET) @@ -510,6 +546,31 @@ expose the wrapped payload directly. => #setLocalValue(DEST, SPLRefCell(PLACE, VAL)) ~> #continueAt(TARGET) ... + + // Cross-frame write helper for SPL ref cells + rule #writeThroughAbsPlace(AbsPlace(0, place(local(I), PROJS)), VAL) + => #forceSetPlaceValue(place(local(I), PROJS), VAL) + ... + + LOCALS + requires 0 <=Int I andBool I #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) + ... + + STACK + requires 0 #traverseProjection( DEST, SPLRefCell(PLACE, VAL), @@ -553,14 +614,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 ( AbsPlace ) rule #traverseProjection( DEST, SPLDataBorrow(PLACE, VAL), @@ -573,13 +634,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 ( AbsPlace ) rule #traverseProjection( DEST, SPLDataBorrowMut(PLACE, VAL), @@ -592,8 +653,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,7 +823,7 @@ expose the wrapped payload directly. syntax KItem ::= #mkSPLAccountPack ( Evaluation , Evaluation , Place ) [seqstrict(1,2)] rule #mkSPLAccountPack(ACCOUNT, SPLDataBorrowMut(PLACE, SPLDataBuffer(_)), DEST) - => #forceSetPlaceValue( + => #writeThroughAbsPlace( PLACE, SPLRefCell(PLACE, SPLDataBuffer(ACCOUNT)) ) 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..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,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::::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); @@ -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<'_>) {} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index a5b2f5cb3..e7d5b1df4 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -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 = [