Skip to content

Commit ec9efc8

Browse files
jbertholdjberthold
authored
feat(spl): support cheatcode for spl-token's Rent (#867)
- solve runtimeverification/solana-token#110
2 parents 4d8344e + 983ea7d commit ec9efc8

2 files changed

Lines changed: 167 additions & 1 deletion

File tree

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

Lines changed: 166 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -156,6 +156,17 @@ 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+
// Rent sysvar calls (includes mock harness direct calls to Rent::from_account_info / Rent::get)
161+
syntax Bool ::= #isSPLRentFromAccountInfoFunc ( String ) [function, total]
162+
rule #isSPLRentFromAccountInfoFunc(_) => false [owise]
163+
rule #isSPLRentFromAccountInfoFunc("Rent::from_account_info") => true // mock harness
164+
rule #isSPLRentFromAccountInfoFunc("solana_sysvar::<solana_rent::Rent as solana_sysvar::Sysvar>::from_account_info") => true
165+
166+
syntax Bool ::= #isSPLRentGetFunc ( String ) [function, total]
167+
rule #isSPLRentGetFunc(_) => false [owise]
168+
rule #isSPLRentGetFunc("Rent::get") => true // mock harness
169+
rule #isSPLRentGetFunc("solana_sysvar::rent::<impl Sysvar for solana_rent::Rent>::get") => true
159170
```
160171

161172

@@ -275,6 +286,56 @@ module KMIR-SPL-TOKEN
275286
andBool 0 <=Int ?SplMintDecimals andBool ?SplMintDecimals <Int 256
276287
andBool #isSplCOptionPubkey(?SplMintFreezeAuthorityCOpt)
277288
[priority(30), preserves-definedness]
289+
290+
rule [cheatcode-is-spl-rent]:
291+
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
292+
=> #setLocalValue(
293+
place(LOCAL, appendP(PROJS, projectionElemDeref .ProjectionElems)),
294+
Aggregate(variantIdx(0),
295+
ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplRentAccountKey:List))))) // pub key: &'a Pubkey
296+
ListItem(
297+
SPLRefCell(
298+
place(
299+
LOCAL,
300+
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(1), #hack()) .ProjectionElems)
301+
),
302+
Integer(?SplRentLamports:Int, 64, false)
303+
)
304+
) // lamports: Rc<RefCell<&'a mut u64>>
305+
ListItem( // data: Rc<RefCell<&'a mut [u8]>>
306+
SPLRefCell(
307+
place(
308+
LOCAL,
309+
appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(2), #hack()) .ProjectionElems)
310+
),
311+
SPLDataBuffer(
312+
Aggregate(variantIdx(0),
313+
ListItem(Integer(?SplRentLamportsPerByteYear:Int, 64, false))
314+
ListItem(Float(2.0, 64))
315+
ListItem(Integer(?SplRentBurnPercent:Int, 8, false))
316+
)
317+
)
318+
)
319+
)
320+
ListItem(SPLPubkeyRef(Aggregate(variantIdx(0), ListItem(Range(?SplRentOwnerKey:List))))) // owner: &'a Pubkey
321+
ListItem(Integer(?SplRentRentEpoch:Int, 64, false)) // rent_epoch: u64
322+
ListItem(BoolVal(false)) // is_signer: bool
323+
ListItem(BoolVal(false)) // is_writable: bool
324+
ListItem(BoolVal(false)) // executable: bool
325+
)
326+
)
327+
~> #execBlockIdx(TARGET)
328+
...
329+
</k>
330+
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "spl_token::entrypoint::cheatcode_is_spl_rent"
331+
orBool #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "cheatcode_is_spl_rent"
332+
ensures #isSplPubkey(?SplRentAccountKey)
333+
andBool #isSplPubkey(?SplRentOwnerKey)
334+
andBool 0 <=Int ?SplRentLamports andBool ?SplRentLamports <Int 18446744073709551616
335+
andBool 0 <=Int ?SplRentRentEpoch andBool ?SplRentRentEpoch <Int 18446744073709551616
336+
andBool 0 <=Int ?SplRentLamportsPerByteYear andBool ?SplRentLamportsPerByteYear <Int (1 <<Int 32)
337+
andBool 0 <=Int ?SplRentBurnPercent andBool ?SplRentBurnPercent <=Int 100
338+
[priority(30), preserves-definedness]
278339
```
279340

280341
## Accessing `Rc<RefCell<_>>`
@@ -600,6 +661,111 @@ expose the wrapped payload directly.
600661
</k>
601662
```
602663

664+
```{.k .symbolic}
665+
// Rent::from_account_info
666+
rule [spl-rent-from-account-info]:
667+
<k> #execTerminator(terminator(terminatorKindCall(FUNC, OP .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
668+
=> #mkSPLRentFromAccountInfo(DEST, OP)
669+
~> #execBlockIdx(TARGET)
670+
...
671+
</k>
672+
requires #isSPLRentFromAccountInfoFunc(#functionName(lookupFunction(#tyOfCall(FUNC))))
673+
[priority(30), preserves-definedness]
674+
675+
syntax KItem ::= #mkSPLRentFromAccountInfo ( Place , Evaluation ) [seqstrict(2)]
676+
677+
678+
// Accept references without an explicit deref projection (e.g., borrowed AccountInfo locals on the stack)
679+
rule <k> #mkSPLRentFromAccountInfo(DEST, Reference(0, place(local(I), .ProjectionElems), _, _))
680+
=> #mkSPLRentFromAccountInfo(DEST, getValue(LOCALS, I))
681+
...
682+
</k>
683+
<locals> LOCALS </locals>
684+
requires 0 <=Int I
685+
andBool I <Int size(LOCALS)
686+
andBool isTypedValue(LOCALS[I])
687+
688+
rule <k> #mkSPLRentFromAccountInfo(DEST, Reference(OFFSET, place(local(I), .ProjectionElems), _, _))
689+
=> #mkSPLRentFromAccountInfo(
690+
DEST,
691+
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(I), OFFSET)
692+
)
693+
...
694+
</k>
695+
<stack> STACK </stack>
696+
requires 0 <Int OFFSET
697+
andBool OFFSET <=Int size(STACK)
698+
andBool isStackFrame(STACK[OFFSET -Int 1])
699+
andBool 0 <=Int I
700+
701+
rule <k> #mkSPLRentFromAccountInfo(
702+
DEST,
703+
Aggregate(variantIdx(0),
704+
ListItem(_KEY)
705+
ListItem(_LAMPORTS_CELL)
706+
ListItem(SPLRefCell(_, SPLDataBuffer(RENT_DATA)))
707+
_REST:List
708+
)
709+
)
710+
=> #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(RENT_DATA)))
711+
...
712+
</k>
713+
```
714+
715+
```{.k .symbolic}
716+
// Rent::get (stable value, stored once in outermost frame like p-token SysRent)
717+
rule [spl-rent-get]:
718+
<k> #execTerminator(terminator(terminatorKindCall(FUNC, .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
719+
=> #writeSPLSysRent(DEST)
720+
~> #execBlockIdx(TARGET)
721+
...
722+
</k>
723+
requires #isSPLRentGetFunc(#functionName(lookupFunction(#tyOfCall(FUNC))))
724+
[priority(30), preserves-definedness]
725+
726+
syntax KItem ::= #writeSPLSysRent ( Place )
727+
728+
// reuse existing Rent value if already initialised in outermost frame
729+
rule <k> #writeSPLSysRent(DEST) => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(RENTVAL))) ... </k>
730+
<stack>
731+
STACK:List
732+
ListItem(StackFrame(_, _, _, _, ListItem(typedValue(RENTVAL, _, _)) _REST))
733+
</stack>
734+
requires 0 <Int size(STACK)
735+
[preserves-definedness]
736+
737+
rule <k> #writeSPLSysRent(DEST) => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(RENTVAL))) ... </k>
738+
<stack>
739+
ListItem(StackFrame(_, _, _, _, ListItem(typedValue(RENTVAL, _, _)) _REST))
740+
</stack>
741+
[preserves-definedness]
742+
743+
// first access: create SysRent in outermost frame's return slot (local 0)
744+
rule [mk-spl-sys-rent]:
745+
<k> #writeSPLSysRent(_DEST) ~> _CONT </k>
746+
<stack>
747+
_:List
748+
ListItem(StackFrame(_, _, _, _,
749+
ListItem(newLocal(_, _) =>
750+
typedValue(
751+
Aggregate(variantIdx(0),
752+
ListItem(Integer(?SplSysRentLamportsPerByteYear:Int, 64, false))
753+
ListItem(Float(2.0, 64))
754+
ListItem(Integer(?SplSysRentBurnPercent:Int, 8, false))
755+
),
756+
ty(0),
757+
mutabilityNot
758+
)
759+
) _:List
760+
))
761+
</stack>
762+
ensures 0 <=Int ?SplSysRentLamportsPerByteYear
763+
andBool ?SplSysRentLamportsPerByteYear <Int (1 <<Int 32)
764+
andBool 0 <=Int ?SplSysRentBurnPercent
765+
andBool ?SplSysRentBurnPercent <=Int 100
766+
[preserves-definedness]
767+
```
768+
603769
```k
604770
endmodule
605771
```

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@
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': ['test_spl_account_domain_data', 'test_spl_mint_domain_data', 'test_spl_rent_domain_data'],
4141
}
4242
PROVE_RS_SHOW_SPECS = [
4343
'local-raw-fail',

0 commit comments

Comments
 (0)