Skip to content

Commit 8db489b

Browse files
jbertholdStevengre
jberthold
and
Stevengre
authored
SPL cheat code tweaks (#878)
includes one `#Ceil` rule that should be back-ported to `master` --------- Co-authored-by: Stevengre <zhaojianhong96@gmail.com>
1 parent e6e8c72 commit 8db489b

2 files changed

Lines changed: 80 additions & 46 deletions

File tree

‎kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,17 @@ Definedness of the list and list elements is also guaranteed.
7979
For symbolic enum values, the variant index remains unevaluated but the original (symbolic) discriminant can be restored:
8080

8181
```k
82+
syntax Int ::= size(Discriminants) [function, total]
83+
rule size(.Discriminants) => 0
84+
rule size(discriminant(_) REST) => 1 +Int size(REST)
85+
86+
rule #Ceil(#lookupDiscrAux(DISCRS:Discriminants, I:Int))
87+
=> #Ceil(DISCRS)
88+
#And #Ceil(I)
89+
#And {true #Equals 0 <=Int I}
90+
#And {true #Equals I <Int size(DISCRS)}
91+
[simplification]
92+
8293
rule #lookupDiscriminant(typeInfoEnumType(_, _, _, _, _), #findVariantIdxAux(DISCR, DISCRS, _IDX)) => DISCR
8394
requires isOneOf(DISCR, DISCRS)
8495
[simplification, preserves-definedness, symbolic(DISCR)]

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

Lines changed: 69 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,11 @@ module KMIR-SPL-TOKEN
115115
requires REST ==K .List
116116
rule #isSplCOptionU64(_) => false [owise]
117117
118+
// AccountState in SPL semantics is carried as an enum variantIdx(0..2); accept legacy u8 too.
119+
syntax Bool ::= #isSplAccountStateVal ( Value ) [function, total]
120+
rule #isSplAccountStateVal(Aggregate(variantIdx(N), .List)) => 0 <=Int N andBool N <=Int 2
121+
rule #isSplAccountStateVal(_) => false [owise]
122+
118123
syntax Bool ::= #isSPLRcRefCellDerefFunc ( String ) [function, total]
119124
rule #isSPLRcRefCellDerefFunc("<std::rc::Rc<std::cell::RefCell<&mut [u8]>> as std::ops::Deref>::deref") => true
120125
rule #isSPLRcRefCellDerefFunc("<std::rc::Rc<std::cell::RefCell<&mut u64>> as std::ops::Deref>::deref") => true
@@ -182,55 +187,58 @@ module KMIR-SPL-TOKEN
182187
rule #maybeDynamicSize(
183188
dynamicSize(_),
184189
SPLDataBuffer(
185-
Aggregate(variantIdx(0),
186-
ListItem(Aggregate(variantIdx(0), ListItem(Range(_)))) // mint
187-
ListItem(Aggregate(variantIdx(0), ListItem(Range(_)))) // owner
188-
ListItem(Integer(_, 64, false)) // amount
189-
ListItem(_DELEG) // delegate COption
190-
ListItem(Integer(_, 8, false)) // state
191-
ListItem(_IS_NATIVE) // is_native COption
192-
ListItem(Integer(_, 64, false)) // delegated_amount
193-
ListItem(_CLOSE) // close_authority COption
194-
)
190+
Aggregate(variantIdx(0),
191+
ListItem(Aggregate(variantIdx(0), ListItem(Range(_)))) // mint
192+
ListItem(Aggregate(variantIdx(0), ListItem(Range(_)))) // owner
193+
ListItem(Integer(_, 64, false)) // amount
194+
ListItem(_DELEG) // delegate COption
195+
ListItem(STATE) // state
196+
ListItem(_IS_NATIVE) // is_native COption
197+
ListItem(Integer(_, 64, false)) // delegated_amount
198+
ListItem(_CLOSE) // close_authority COption
195199
)
196200
)
201+
)
197202
=> dynamicSize(165)
203+
requires #isSplAccountStateVal(STATE)
198204
[priority(30)]
199205
200206
rule #maybeDynamicSize(
201207
dynamicSize(_),
202208
SPLDataBorrow(_, SPLDataBuffer(
203-
Aggregate(variantIdx(0),
204-
ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
205-
ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
206-
ListItem(Integer(_, 64, false))
207-
ListItem(_DELEG)
208-
ListItem(Integer(_, 8, false))
209-
ListItem(_IS_NATIVE)
210-
ListItem(Integer(_, 64, false))
211-
ListItem(_CLOSE)
212-
)
213-
))
214-
)
209+
Aggregate(variantIdx(0),
210+
ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
211+
ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
212+
ListItem(Integer(_, 64, false))
213+
ListItem(_DELEG)
214+
ListItem(STATE)
215+
ListItem(_IS_NATIVE)
216+
ListItem(Integer(_, 64, false))
217+
ListItem(_CLOSE)
218+
)
219+
))
220+
)
215221
=> dynamicSize(165)
222+
requires #isSplAccountStateVal(STATE)
216223
[priority(30)]
217224
218225
rule #maybeDynamicSize(
219226
dynamicSize(_),
220227
SPLDataBorrowMut(_, SPLDataBuffer(
221-
Aggregate(variantIdx(0),
222-
ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
223-
ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
224-
ListItem(Integer(_, 64, false))
225-
ListItem(_DELEG)
226-
ListItem(Integer(_, 8, false))
227-
ListItem(_IS_NATIVE)
228-
ListItem(Integer(_, 64, false))
229-
ListItem(_CLOSE)
230-
)
231-
))
232-
)
228+
Aggregate(variantIdx(0),
229+
ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
230+
ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
231+
ListItem(Integer(_, 64, false))
232+
ListItem(_DELEG)
233+
ListItem(STATE)
234+
ListItem(_IS_NATIVE)
235+
ListItem(Integer(_, 64, false))
236+
ListItem(_CLOSE)
237+
)
238+
))
239+
)
233240
=> dynamicSize(165)
241+
requires #isSplAccountStateVal(STATE)
234242
[priority(30)]
235243
236244
// Mint data (&mut [u8]) length hints (Mint::LEN)
@@ -348,11 +356,19 @@ module KMIR-SPL-TOKEN
348356
ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintKey:List)))) // Account.mint: Pubkey
349357
ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplTokenOwnerKey:List)))) // Account.owner: Pubkey
350358
ListItem(Integer(?SplAmount:Int, 64, false)) // Account.amount: u64
351-
ListItem(?SplDelegateCOpt:Value) // Account.delegate: COption<Pubkey>
352-
ListItem(Integer(?SplAccountState:Int, 8, false)) // Account.state: AccountState (repr u8)
353-
ListItem(?SplIsNativeCOpt:Value) // Account.is_native: COption<u64>
359+
// Model COption<Pubkey> as
360+
// Some(pubkey); None is not represented here.
361+
ListItem(Aggregate(variantIdx(1),
362+
ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplDelegateKey:List))))))
363+
ListItem(Aggregate(variantIdx(?SplAccountState:Int), .List)) // Account.state: AccountState (repr u8)
364+
// Allow COption<u64> with a symbolic variant (0=None, 1=Some(amount)).
365+
ListItem(Aggregate(variantIdx(?SplIsNativeLamportsVariant:Int),
366+
ListItem(Integer(?SplIsNativeLamports:Int, 64, false))))
354367
ListItem(Integer(?SplDelegatedAmount:Int, 64, false)) // Account.delegated_amount: u64
355-
ListItem(?SplCloseAuthCOpt:Value) // Account.close_authority: COption<Pubkey>
368+
// Model COption<Pubkey> as
369+
// Some(pubkey); None is not represented here.
370+
ListItem(Aggregate(variantIdx(1),
371+
ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplCloseAuthKey:List))))))
356372
)
357373
)
358374
)
@@ -375,12 +391,13 @@ module KMIR-SPL-TOKEN
375391
andBool 0 <=Int ?SplRentEpoch andBool ?SplRentEpoch <Int 18446744073709551616
376392
andBool #isSplPubkey(?SplMintKey)
377393
andBool #isSplPubkey(?SplTokenOwnerKey)
394+
andBool #isSplPubkey(?SplDelegateKey)
395+
andBool #isSplPubkey(?SplCloseAuthKey)
378396
andBool 0 <=Int ?SplAmount andBool ?SplAmount <Int (1 <<Int 64)
379-
andBool 0 <=Int ?SplAccountState andBool ?SplAccountState <Int 256
397+
andBool 0 <=Int ?SplAccountState andBool ?SplAccountState <=Int 2
380398
andBool 0 <=Int ?SplDelegatedAmount andBool ?SplDelegatedAmount <Int (1 <<Int 64)
381-
andBool #isSplCOptionPubkey(?SplDelegateCOpt)
382-
andBool #isSplCOptionPubkey(?SplCloseAuthCOpt)
383-
andBool #isSplCOptionU64(?SplIsNativeCOpt)
399+
andBool 0 <=Int ?SplIsNativeLamportsVariant andBool ?SplIsNativeLamportsVariant <=Int 1
400+
andBool 0 <=Int ?SplIsNativeLamports andBool ?SplIsNativeLamports <Int (1 <<Int 64)
384401
[priority(30), preserves-definedness]
385402
386403
rule [cheatcode-is-spl-mint]:
@@ -406,11 +423,17 @@ module KMIR-SPL-TOKEN
406423
),
407424
SPLDataBuffer(
408425
Aggregate(variantIdx(0),
409-
ListItem(?SplMintAuthorityCOpt:Value)
426+
// Model COption<Pubkey> as
427+
// Some(pubkey); None is not represented here.
428+
ListItem(Aggregate(variantIdx(1),
429+
ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintAuthorityKey:List))))))
410430
ListItem(Integer(?SplMintSupply:Int, 64, false))
411431
ListItem(Integer(?SplMintDecimals:Int, 8, false))
412432
ListItem(BoolVal(false))
413-
ListItem(?SplMintFreezeAuthorityCOpt:Value)
433+
// Model COption<Pubkey> as
434+
// Some(pubkey); None is not represented here.
435+
ListItem(Aggregate(variantIdx(1),
436+
ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintFreezeAuthorityKey:List))))))
414437
)
415438
)
416439
)
@@ -429,12 +452,12 @@ module KMIR-SPL-TOKEN
429452
orBool #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "cheatcode_is_spl_mint"
430453
ensures #isSplPubkey(?SplMintAccountKey)
431454
andBool #isSplPubkey(?SplMintOwnerKey)
455+
andBool #isSplPubkey(?SplMintAuthorityKey)
456+
andBool #isSplPubkey(?SplMintFreezeAuthorityKey)
432457
andBool 0 <=Int ?SplMintLamports andBool ?SplMintLamports <Int 18446744073709551616
433458
andBool 0 <=Int ?SplMintRentEpoch andBool ?SplMintRentEpoch <Int 18446744073709551616
434-
andBool #isSplCOptionPubkey(?SplMintAuthorityCOpt)
435459
andBool 0 <=Int ?SplMintSupply andBool ?SplMintSupply <Int (1 <<Int 64)
436460
andBool 0 <=Int ?SplMintDecimals andBool ?SplMintDecimals <Int 256
437-
andBool #isSplCOptionPubkey(?SplMintFreezeAuthorityCOpt)
438461
[priority(30), preserves-definedness]
439462
440463
rule [cheatcode-is-spl-rent]:

0 commit comments

Comments
 (0)