Skip to content

Commit a88e6be

Browse files
StevengreStevengre
committed
feat(spl): adjustRef for spl domain data
1 parent 4d8344e commit a88e6be

File tree

3 files changed

+123
-38
lines changed

3 files changed

+123
-38
lines changed

‎kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md‎

Lines changed: 96 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -89,10 +89,10 @@ module KMIR-SPL-TOKEN
8989
## Helper syntax
9090

9191
```k
92-
syntax Value ::= SPLRefCell ( Place , Value )
92+
syntax Value ::= SPLRefCell ( Value , Value ) // Reference to the buffer, value in the cell
9393
| SPLDataBuffer ( Value )
94-
| SPLDataBorrow ( Place , Value )
95-
| SPLDataBorrowMut ( Place , Value )
94+
| SPLDataBorrow ( Value , Value ) // Reference to the buffer, borrowed value
95+
| SPLDataBorrowMut ( Value , Value )
9696
| SPLPubkeyRef ( Value )
9797
```
9898

@@ -156,6 +156,18 @@ module KMIR-SPL-TOKEN
156156
rule #isSPLPackFunc("solana_program_pack::<spl_token_interface::state::Mint as solana_program_pack::Pack>::pack") => true
157157
// mock mint
158158
rule #isSPLPackFunc("Mint::pack") => true
159+
160+
// Adjust references when moving across stack frames
161+
rule #adjustRef(SPLRefCell(PLACE, VAL), OFFSET) => SPLRefCell(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET))
162+
rule #adjustRef(SPLDataBorrow(PLACE, VAL), OFFSET) => SPLDataBorrow(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET))
163+
rule #adjustRef(SPLDataBorrowMut(PLACE, VAL), OFFSET) => SPLDataBorrowMut(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET))
164+
rule #adjustRef(SPLDataBuffer(VAL), OFFSET) => SPLDataBuffer(#adjustRef(VAL, OFFSET))
165+
rule #adjustRef(SPLPubkeyRef(VAL), OFFSET) => SPLPubkeyRef(#adjustRef(VAL, OFFSET))
166+
// COption values are pure data; adjusting references is a no-op
167+
rule #adjustRef(VAL, _) => VAL
168+
requires #isSplCOptionPubkey(VAL) orBool #isSplCOptionU64(VAL)
169+
[simplification]
170+
159171
```
160172

161173

@@ -169,29 +181,39 @@ module KMIR-SPL-TOKEN
169181
ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplAccountKey:List))))) // pub key: &'a Pubkey
170182
ListItem(
171183
SPLRefCell(
172-
place(
173-
LOCAL,
174-
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems)
184+
Reference(
185+
0,
186+
place(
187+
LOCAL,
188+
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems)
189+
),
190+
mutabilityNot,
191+
metadata(noMetadataSize, 0, noMetadataSize)
175192
),
176193
Integer(?SplLamports:Int, 64, false)
177194
)
178195
) // lamports: Rc<RefCell<&'a mut u64>>
179196
ListItem( // data: Rc<RefCell<&'a mut [u8]>>
180197
SPLRefCell(
181-
place(
182-
LOCAL,
183-
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems)
198+
Reference(
199+
0,
200+
place(
201+
LOCAL,
202+
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems)
203+
),
204+
mutabilityNot,
205+
metadata(noMetadataSize, 0, noMetadataSize)
184206
),
185207
SPLDataBuffer( // data: Rc<RefCell<&'a mut [u8]>>, Aggregate is for &account.data
186208
Aggregate(variantIdx(0),
187209
ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintKey:List)))) // Account.mint: Pubkey
188210
ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplTokenOwnerKey:List)))) // Account.owner: Pubkey
189211
ListItem(Integer(?SplAmount:Int, 64, false)) // Account.amount: u64
190-
ListItem(?SplDelegateCOpt:Value) // Account.delegate: COption<Pubkey>
212+
ListItem(Aggregate(variantIdx(0), .List)) // COption<Pubkey> default None
191213
ListItem(Integer(?SplAccountState:Int, 8, false)) // Account.state: AccountState (repr u8)
192-
ListItem(?SplIsNativeCOpt:Value) // Account.is_native: COption<u64>
214+
ListItem(Aggregate(variantIdx(0), .List)) // COption<u64> default None
193215
ListItem(Integer(?SplDelegatedAmount:Int, 64, false)) // Account.delegated_amount: u64
194-
ListItem(?SplCloseAuthCOpt:Value) // Account.close_authority: COption<Pubkey>
216+
ListItem(Aggregate(variantIdx(0), .List)) // COption<Pubkey> default None
195217
)
196218
)
197219
)
@@ -217,9 +239,9 @@ module KMIR-SPL-TOKEN
217239
andBool 0 <=Int ?SplAmount andBool ?SplAmount <Int (1 <<Int 64)
218240
andBool 0 <=Int ?SplAccountState andBool ?SplAccountState <Int 256
219241
andBool 0 <=Int ?SplDelegatedAmount andBool ?SplDelegatedAmount <Int (1 <<Int 64)
220-
andBool #isSplCOptionPubkey(?SplDelegateCOpt)
221-
andBool #isSplCOptionPubkey(?SplCloseAuthCOpt)
222-
andBool #isSplCOptionU64(?SplIsNativeCOpt)
242+
andBool #isSplCOptionPubkey(Aggregate(variantIdx(0), .List))
243+
andBool #isSplCOptionPubkey(Aggregate(variantIdx(0), .List))
244+
andBool #isSplCOptionU64(Aggregate(variantIdx(0), .List))
223245
[priority(30), preserves-definedness]
224246
225247
rule [cheatcode-is-spl-mint]:
@@ -230,26 +252,36 @@ module KMIR-SPL-TOKEN
230252
ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplMintAccountKey:List))))) // pub key: &'a Pubkey
231253
ListItem(
232254
SPLRefCell(
233-
place(
234-
LOCAL,
235-
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems)
255+
Reference(
256+
0,
257+
place(
258+
LOCAL,
259+
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems)
260+
),
261+
mutabilityNot,
262+
metadata(noMetadataSize, 0, noMetadataSize)
236263
),
237264
Integer(?SplMintLamports:Int, 64, false)
238265
)
239266
)
240267
ListItem(
241268
SPLRefCell(
242-
place(
243-
LOCAL,
244-
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems)
269+
Reference(
270+
0,
271+
place(
272+
LOCAL,
273+
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems)
274+
),
275+
mutabilityNot,
276+
metadata(noMetadataSize, 0, noMetadataSize)
245277
),
246278
SPLDataBuffer(
247279
Aggregate(variantIdx(0),
248-
ListItem(?SplMintAuthorityCOpt:Value)
280+
ListItem(Aggregate(variantIdx(0), .List))
249281
ListItem(Integer(?SplMintSupply:Int, 64, false))
250282
ListItem(Integer(?SplMintDecimals:Int, 8, false))
251283
ListItem(BoolVal(false))
252-
ListItem(?SplMintFreezeAuthorityCOpt:Value)
284+
ListItem(Aggregate(variantIdx(0), .List))
253285
)
254286
)
255287
)
@@ -270,10 +302,10 @@ module KMIR-SPL-TOKEN
270302
andBool #isSplPubkey(?SplMintOwnerKey)
271303
andBool 0 <=Int ?SplMintLamports andBool ?SplMintLamports <Int 18446744073709551616
272304
andBool 0 <=Int ?SplMintRentEpoch andBool ?SplMintRentEpoch <Int 18446744073709551616
273-
andBool #isSplCOptionPubkey(?SplMintAuthorityCOpt)
305+
andBool #isSplCOptionPubkey(Aggregate(variantIdx(0), .List))
274306
andBool 0 <=Int ?SplMintSupply andBool ?SplMintSupply <Int (1 <<Int 64)
275307
andBool 0 <=Int ?SplMintDecimals andBool ?SplMintDecimals <Int 256
276-
andBool #isSplCOptionPubkey(?SplMintFreezeAuthorityCOpt)
308+
andBool #isSplCOptionPubkey(Aggregate(variantIdx(0), .List))
277309
[priority(30), preserves-definedness]
278310
```
279311

@@ -292,8 +324,9 @@ expose the wrapped payload directly.
292324
[priority(30), preserves-definedness]
293325
294326
syntax KItem ::= #finishSPLRcDeref ( Evaluation , Place , MaybeBasicBlockIdx ) [seqstrict(1)]
295-
| #resolveSPLRcRef ( Value , Place , MaybeBasicBlockIdx )
296-
| #finishResolvedSPLRc ( Place , MaybeBasicBlockIdx )
327+
| #resolveSPLRcRef ( Value , Place , MaybeBasicBlockIdx )
328+
| #finishResolvedSPLRc ( Place , MaybeBasicBlockIdx )
329+
| #writeThroughRef ( Value , Value ) [seqstrict(2)]
297330
298331
rule <k> #finishSPLRcDeref(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET)
299332
=> #resolveSPLRcRef(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET)
@@ -339,6 +372,31 @@ expose the wrapped payload directly.
339372
=> #setLocalValue(DEST, SPLRefCell(PLACE, VAL)) ~> #continueAt(TARGET)
340373
...
341374
</k>
375+
376+
// Cross-frame write helper for SPL ref cells
377+
rule <k> #writeThroughRef(Reference(0, place(local(I), PROJS), _, _), VAL)
378+
=> #forceSetPlaceValue(place(local(I), PROJS), VAL)
379+
...
380+
</k>
381+
<locals> LOCALS </locals>
382+
requires 0 <=Int I andBool I <Int size(LOCALS)
383+
andBool isTypedLocal(LOCALS[I])
384+
385+
rule <k> #writeThroughRef(Reference(OFFSET, place(local(I), PROJS), _, _), VAL)
386+
=> #traverseProjection(
387+
toStack(OFFSET, local(I)),
388+
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(I), OFFSET),
389+
PROJS,
390+
.Contexts
391+
)
392+
~> #writeProjection(VAL)
393+
...
394+
</k>
395+
<stack> STACK </stack>
396+
requires 0 <Int OFFSET
397+
andBool OFFSET <=Int size(STACK)
398+
andBool isStackFrame(STACK[OFFSET -Int 1])
399+
andBool 0 <=Int I
342400
```
343401

344402
## Pubkey references
@@ -369,7 +427,7 @@ expose the wrapped payload directly.
369427

370428
```k
371429
// Step 1
372-
syntax Context ::= CtxSPLRefCell ( Place )
430+
syntax Context ::= CtxSPLRefCell ( Value )
373431
rule <k> #traverseProjection(
374432
DEST,
375433
SPLRefCell(PLACE, VAL),
@@ -382,14 +440,14 @@ expose the wrapped payload directly.
382440
PROJS,
383441
CtxSPLRefCell(PLACE) CTXTS
384442
)
385-
...
386-
</k>
443+
...
444+
</k>
387445
[priority(30)]
388446
rule #buildUpdate(VAL, CtxSPLRefCell(PLACE) CTXS) => #buildUpdate(SPLRefCell(PLACE, VAL), CTXS)
389447
rule #projectionsFor(CtxSPLRefCell(_) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS)
390448
391449
// Step 2
392-
syntax Context ::= CtxSPLDataBorrow ( Place )
450+
syntax Context ::= CtxSPLDataBorrow ( Value )
393451
rule <k> #traverseProjection(
394452
DEST,
395453
SPLDataBorrow(PLACE, VAL),
@@ -402,13 +460,13 @@ expose the wrapped payload directly.
402460
PROJS,
403461
CtxSPLDataBorrow(PLACE) CTXTS
404462
)
405-
...
406-
</k>
463+
...
464+
</k>
407465
[priority(30)]
408466
rule #buildUpdate(VAL, CtxSPLDataBorrow(PLACE) CTXS) => #buildUpdate(SPLDataBorrow(PLACE, SPLDataBuffer(VAL)), CTXS)
409467
rule #projectionsFor(CtxSPLDataBorrow(_) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS)
410468
411-
syntax Context ::= CtxSPLDataBorrowMut ( Place )
469+
syntax Context ::= CtxSPLDataBorrowMut ( Value )
412470
rule <k> #traverseProjection(
413471
DEST,
414472
SPLDataBorrowMut(PLACE, VAL),
@@ -421,8 +479,8 @@ expose the wrapped payload directly.
421479
PROJS,
422480
CtxSPLDataBorrowMut(PLACE) CTXTS
423481
)
424-
...
425-
</k>
482+
...
483+
</k>
426484
[priority(30)]
427485
rule #buildUpdate(VAL, CtxSPLDataBorrowMut(PLACE) CTXS) => #buildUpdate(SPLDataBorrowMut(PLACE, SPLDataBuffer(VAL)), CTXS)
428486
rule #projectionsFor(CtxSPLDataBorrowMut(_) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS)
@@ -591,13 +649,14 @@ expose the wrapped payload directly.
591649
syntax KItem ::= #mkSPLAccountPack ( Evaluation , Evaluation , Place ) [seqstrict(1,2)]
592650
593651
rule <k> #mkSPLAccountPack(ACCOUNT, SPLDataBorrowMut(PLACE, SPLDataBuffer(_)), DEST)
594-
=> #forceSetPlaceValue(
652+
=> #writeThroughRef(
595653
PLACE,
596654
SPLRefCell(PLACE, SPLDataBuffer(ACCOUNT))
597655
)
598656
~> #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List))))
599657
...
600658
</k>
659+
requires isRef(PLACE)
601660
```
602661

603662
```k

‎kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -127,12 +127,33 @@ fn test_spltoken_domain_data(
127127
multisig: &AccountInfo<'_>,
128128
rent: &AccountInfo<'_>,
129129
) {
130+
test_spl_account_pack_is_native_branch(acc);
131+
test_spl_account_is_native_branch(acc);
130132
test_spl_account_domain_data(acc);
131133
test_spl_mint_domain_data(mint);
132134
test_spl_multisig_domain_data(multisig);
133135
test_spl_rent_domain_data(rent);
134136
}
135137

138+
fn test_spl_account_pack_is_native_branch(acc: &AccountInfo<'_>) {
139+
// Keep is_native symbolic and pack through an extra call frame to mirror process_burn’s cross-frame writeback
140+
cheatcode_is_spl_account(acc);
141+
let account = get_account(acc);
142+
let mut borrow = acc.data.borrow_mut();
143+
pack_account_inner(&mut borrow, &account);
144+
}
145+
146+
fn pack_account_inner(buf: &mut [u8], account: &Account) {
147+
Account::pack(account.clone(), buf).unwrap();
148+
}
149+
150+
fn test_spl_account_is_native_branch(acc: &AccountInfo<'_>) {
151+
// Keep is_native symbolic and exercise COption::<u64>::is_some to reproduce the ndbranch
152+
cheatcode_is_spl_account(acc);
153+
let account = get_account(acc);
154+
let _ = account.is_native();
155+
}
156+
136157
fn test_spl_account_domain_data(acc: &AccountInfo<'_>) {
137158
cheatcode_is_spl_account(acc);
138159

‎kmir/src/tests/integration/test_integration.py‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,12 @@
3737
'assume-cheatcode': ['check_assume'],
3838
'assume-cheatcode-conflict-fail': ['check_assume_conflict'],
3939
'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
40-
'spl_token_domain_data': ['test_spl_account_domain_data', 'test_spl_mint_domain_data'],
40+
'spl_token_domain_data': [
41+
'test_spl_account_pack_is_native_branch',
42+
'test_spl_account_is_native_branch',
43+
'test_spl_account_domain_data',
44+
'test_spl_mint_domain_data',
45+
],
4146
}
4247
PROVE_RS_SHOW_SPECS = [
4348
'local-raw-fail',

0 commit comments

Comments
 (0)