Skip to content

Commit 39ce2a6

Browse files
StevengreStevengre
committed
update spl/p-token.md to use #execTerminatorCall
1 parent 56a84c6 commit 39ce2a6

File tree

2 files changed

+66
-90
lines changed

2 files changed

+66
-90
lines changed

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

Lines changed: 36 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -467,32 +467,28 @@ An `AccountInfo` reference is passed to the function.
467467
```k
468468
// special rule to intercept the cheat code function calls and replace them by #mkPToken<thing>
469469
rule [cheatcode-is-account]:
470-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(PLACE) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
471-
=> #mkPTokenAccount(PLACE) ~> #execBlockIdx(TARGET)
472-
...
470+
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
471+
=> #mkPTokenAccount(PLACE) ~> #continueAt(TARGET)
473472
</k>
474-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio_token_program::entrypoint::cheatcode_is_account"
473+
requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::cheatcode_is_account"
475474
[priority(30), preserves-definedness]
476475
rule [cheatcode-is-mint]:
477-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(PLACE) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
478-
=> #mkPTokenMint(PLACE) ~> #execBlockIdx(TARGET)
479-
...
476+
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
477+
=> #mkPTokenMint(PLACE) ~> #continueAt(TARGET)
480478
</k>
481-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio_token_program::entrypoint::cheatcode_is_mint"
479+
requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::cheatcode_is_mint"
482480
[priority(30), preserves-definedness]
483481
rule [cheatcode-is-multisig]:
484-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(PLACE) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
485-
=> #mkPTokenMultisig(PLACE) ~> #execBlockIdx(TARGET)
486-
...
482+
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
483+
=> #mkPTokenMultisig(PLACE) ~> #continueAt(TARGET)
487484
</k>
488-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio_token_program::entrypoint::cheatcode_is_multisig"
485+
requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::cheatcode_is_multisig"
489486
[priority(30), preserves-definedness]
490487
rule [cheatcode-is-rent]:
491-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(PLACE) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
492-
=> #mkPTokenRent(PLACE) ~> #execBlockIdx(TARGET)
493-
...
488+
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
489+
=> #mkPTokenRent(PLACE) ~> #continueAt(TARGET)
494490
</k>
495-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio_token_program::entrypoint::cheatcode_is_rent"
491+
requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::cheatcode_is_rent"
496492
[priority(30), preserves-definedness]
497493
498494
// cheat codes and rules to create a special PTokenAccount flavour
@@ -737,22 +733,20 @@ The `PAccByteRef` carries a stack offset, so it must be adjusted on reads.
737733
```k
738734
// intercept calls to `borrow_data_unchecked` and write `PAccountRef` to destination
739735
rule [cheatcode-borrow-data]:
740-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
736+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, TARGET, _UNWIND) ~> _CONT
741737
=> #mkPAccByteRef(DEST, operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) .ProjectionElems))), mutabilityNot)
742-
~> #execBlockIdx(TARGET)
743-
...
738+
~> #continueAt(TARGET)
744739
</k>
745-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio::account_info::AccountInfo::borrow_data_unchecked"
740+
requires #functionName(FUNC) ==String "pinocchio::account_info::AccountInfo::borrow_data_unchecked"
746741
[priority(30), preserves-definedness]
747742
748743
// intercept calls to `borrow_mut_data_unchecked` and write `PAccountRef` to destination
749744
rule [cheatcode-borrow-mut-data]:
750-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
745+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, TARGET, _UNWIND) ~> _CONT
751746
=> #mkPAccByteRef(DEST, operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) .ProjectionElems))), mutabilityMut)
752-
~> #execBlockIdx(TARGET)
753-
...
747+
~> #continueAt(TARGET)
754748
</k>
755-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio::account_info::AccountInfo::borrow_mut_data_unchecked"
749+
requires #functionName(FUNC) ==String "pinocchio::account_info::AccountInfo::borrow_mut_data_unchecked"
756750
[priority(30), preserves-definedness]
757751
758752
syntax KItem ::= #mkPAccByteRef( Place , Evaluation , Mutability ) [seqstrict(2)]
@@ -816,51 +810,47 @@ NB Both `load_unchecked` and `load_mut_unchecked` are intercepted in the same wa
816810
```k
817811
// intercept calls to `load_unchecked` and `load_mut_unchecked`
818812
rule [cheatcode-mk-iface-account-ref]:
819-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, OPERAND .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
813+
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND) ~> _CONT
820814
=> #mkPAccountRef(DEST, OPERAND, PAccountIAcc, true)
821-
~> #execBlockIdx(TARGET)
822-
...
815+
~> #continueAt(TARGET)
823816
</k>
824817
requires (
825-
#functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio_token_interface::state::load_unchecked::<pinocchio_token_interface::state::account::Account>"
818+
#functionName(FUNC) ==String "pinocchio_token_interface::state::load_unchecked::<pinocchio_token_interface::state::account::Account>"
826819
orBool
827-
#functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio_token_interface::state::load_mut_unchecked::<pinocchio_token_interface::state::account::Account>"
820+
#functionName(FUNC) ==String "pinocchio_token_interface::state::load_mut_unchecked::<pinocchio_token_interface::state::account::Account>"
828821
)
829822
[priority(30), preserves-definedness]
830823
831824
rule [cheatcode-mk-imint-ref]:
832-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, OPERAND .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
825+
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND) ~> _CONT
833826
=> #mkPAccountRef(DEST, OPERAND, PAccountIMint, true)
834-
~> #execBlockIdx(TARGET)
835-
...
827+
~> #continueAt(TARGET)
836828
</k>
837829
requires (
838-
#functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio_token_interface::state::load_unchecked::<pinocchio_token_interface::state::mint::Mint>"
830+
#functionName(FUNC) ==String "pinocchio_token_interface::state::load_unchecked::<pinocchio_token_interface::state::mint::Mint>"
839831
orBool
840-
#functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio_token_interface::state::load_mut_unchecked::<pinocchio_token_interface::state::mint::Mint>"
832+
#functionName(FUNC) ==String "pinocchio_token_interface::state::load_mut_unchecked::<pinocchio_token_interface::state::mint::Mint>"
841833
)
842834
[priority(30), preserves-definedness]
843835
844836
rule [cheatcode-mk-imulti-ref]:
845-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, OPERAND .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
837+
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND) ~> _CONT
846838
=> #mkPAccountRef(DEST, OPERAND, PAccountIMulti, true)
847-
~> #execBlockIdx(TARGET)
848-
...
839+
~> #continueAt(TARGET)
849840
</k>
850841
requires (
851-
#functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio_token_interface::state::load_unchecked::<pinocchio_token_interface::state::multisig::Multisig>"
842+
#functionName(FUNC) ==String "pinocchio_token_interface::state::load_unchecked::<pinocchio_token_interface::state::multisig::Multisig>"
852843
orBool
853-
#functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio_token_interface::state::load_mut_unchecked::<pinocchio_token_interface::state::multisig::Multisig>"
844+
#functionName(FUNC) ==String "pinocchio_token_interface::state::load_mut_unchecked::<pinocchio_token_interface::state::multisig::Multisig>"
854845
)
855846
[priority(30), preserves-definedness]
856847
857848
rule [cheatcode-mk-prent-ref]:
858-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, OPERAND .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
849+
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND) ~> _CONT
859850
=> #mkPAccountRef(DEST, OPERAND, PAccountPRent, false)
860-
~> #execBlockIdx(TARGET)
861-
...
851+
~> #continueAt(TARGET)
862852
</k>
863-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "pinocchio::sysvars::rent::Rent::from_bytes_unchecked"
853+
requires #functionName(FUNC) ==String "pinocchio::sysvars::rent::Rent::from_bytes_unchecked"
864854
[priority(30), preserves-definedness]
865855
866856
// expect the Evaluation to return a `PAccByteRef` referring to a `PAccount<Thing>` (not checked)
@@ -902,12 +892,11 @@ Therefore, the value gets created in a dedicated place on first access.
902892

903893
```k
904894
rule [cheatcode-get-sys-prent]:
905-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
895+
<k> #execTerminatorCall(_, FUNC, .Operands, DEST, TARGET, _UNWIND) ~> _CONT
906896
=> #writeSysRent(DEST)
907-
~> #execBlockIdx(TARGET)
908-
...
897+
~> #continueAt(TARGET)
909898
</k>
910-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "<sysvars::rent::Rent as sysvars::Sysvar>::get"
899+
requires #functionName(FUNC) ==String "<sysvars::rent::Rent as sysvars::Sysvar>::get"
911900
[priority(30), preserves-definedness]
912901
913902
syntax KItem ::= #writeSysRent ( Place )

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

Lines changed: 30 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -283,7 +283,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
283283
.ProjectionElems
284284
285285
rule [cheatcode-is-spl-account]:
286-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
286+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
287287
=> #forceSetPlaceValue(
288288
place(LOCAL, appendP(PROJS, DATA_BUFFER_PROJS)), // navigate to [u8] data buffer
289289
SPLDataBuffer(
@@ -306,11 +306,10 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
306306
place(LOCAL, appendP(PROJS, REFCELL_PROJS)), // navigate to RefCell for borrow init
307307
#initBorrow(operandCopy(place(LOCAL, appendP(PROJS, REFCELL_PROJS))), 165)
308308
)
309-
~> #execBlockIdx(TARGET)
310-
...
309+
~> #continueAt(TARGET)
311310
</k>
312-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "spl_token::entrypoint::cheatcode_is_spl_account"
313-
orBool #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "cheatcode_is_spl_account"
311+
requires #functionName(FUNC) ==String "spl_token::entrypoint::cheatcode_is_spl_account"
312+
orBool #functionName(FUNC) ==String "cheatcode_is_spl_account"
314313
ensures #isSplPubkey(?SplMintKey)
315314
andBool #isSplPubkey(?SplTokenOwnerKey)
316315
andBool 0 <=Int ?SplHasDelegateKey andBool ?SplHasDelegateKey <=Int 1
@@ -355,7 +354,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
355354
</k>
356355
357356
rule [cheatcode-is-spl-mint]:
358-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
357+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
359358
=> #forceSetPlaceValue(
360359
place(LOCAL, appendP(PROJS, DATA_BUFFER_PROJS)), // navigate to [u8] data buffer
361360
SPLDataBuffer(
@@ -376,11 +375,10 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
376375
place(LOCAL, appendP(PROJS, REFCELL_PROJS)), // navigate to RefCell for borrow init
377376
#initBorrow(operandCopy(place(LOCAL, appendP(PROJS, REFCELL_PROJS))), 82)
378377
)
379-
~> #execBlockIdx(TARGET)
380-
...
378+
~> #continueAt(TARGET)
381379
</k>
382-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "spl_token::entrypoint::cheatcode_is_spl_mint"
383-
orBool #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "cheatcode_is_spl_mint"
380+
requires #functionName(FUNC) ==String "spl_token::entrypoint::cheatcode_is_spl_mint"
381+
orBool #functionName(FUNC) ==String "cheatcode_is_spl_mint"
384382
ensures 0 <=Int ?SplMintHasAuthKey andBool ?SplMintHasAuthKey <=Int 1
385383
andBool (0 ==Int #lookupDiscrAux(discriminant(0) discriminant(1) .Discriminants, ?SplMintHasAuthKey) orBool 1 ==Int #lookupDiscrAux(discriminant(0) discriminant(1) .Discriminants, ?SplMintHasAuthKey))
386384
andBool #isSplPubkey(?SplMintAuthorityKey)
@@ -392,7 +390,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
392390
[priority(30), preserves-definedness]
393391
394392
rule [cheatcode-is-spl-rent]:
395-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
393+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
396394
=> #forceSetPlaceValue(
397395
place(LOCAL, appendP(PROJS, DATA_BUFFER_PROJS)), // navigate to [u8] data buffer
398396
SPLDataBuffer(
@@ -407,11 +405,10 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
407405
place(LOCAL, appendP(PROJS, REFCELL_PROJS)), // navigate to RefCell for borrow init
408406
#initBorrow(operandCopy(place(LOCAL, appendP(PROJS, REFCELL_PROJS))), 17)
409407
)
410-
~> #execBlockIdx(TARGET)
411-
...
408+
~> #continueAt(TARGET)
412409
</k>
413-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "spl_token::entrypoint::cheatcode_is_spl_rent"
414-
orBool #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "cheatcode_is_spl_rent"
410+
requires #functionName(FUNC) ==String "spl_token::entrypoint::cheatcode_is_spl_rent"
411+
orBool #functionName(FUNC) ==String "cheatcode_is_spl_rent"
415412
ensures 0 <=Int ?SplRentLamportsPerByteYear andBool ?SplRentLamportsPerByteYear <Int (1 <<Int 32)
416413
andBool 0 <=Int ?SplRentBurnPercent andBool ?SplRentBurnPercent <=Int 100
417414
[priority(30), preserves-definedness]
@@ -422,12 +419,11 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
422419
```k
423420
// RefCell::<&mut [u8]>::borrow / borrow_mut - returns Ref/RefMut wrapper with pointer to data
424421
rule [spl-borrow-data]:
425-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
422+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, TARGET, _UNWIND) ~> _CONT
426423
=> #setSPLBorrowData(DEST, operandCopy(place(LOCAL, PROJS)))
427-
~> #execBlockIdx(TARGET)
428-
...
424+
~> #continueAt(TARGET)
429425
</k>
430-
requires #isSPLBorrowFunc(#functionName(lookupFunction(#tyOfCall(FUNC))))
426+
requires #isSPLBorrowFunc(#functionName(FUNC))
431427
[priority(30), preserves-definedness]
432428
433429
syntax KItem ::= #setSPLBorrowData ( Place , Evaluation ) [seqstrict(2)]
@@ -443,12 +439,11 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
443439
```k
444440
// Account/Mint::unpack_from_slice - extracts struct from SPLDataBuffer
445441
rule [spl-account-unpack]:
446-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, OP:Operand .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
442+
<k> #execTerminatorCall(_, FUNC, OP:Operand .Operands, DEST, TARGET, _UNWIND) ~> _CONT
447443
=> #splUnpack(DEST, #withDeref(OP))
448-
~> #execBlockIdx(TARGET)
449-
...
444+
~> #continueAt(TARGET)
450445
</k>
451-
requires #isSPLUnpackFunc(#functionName(lookupFunction(#tyOfCall(FUNC))))
446+
requires #isSPLUnpackFunc(#functionName(FUNC))
452447
[priority(30), preserves-definedness]
453448
454449
syntax KItem ::= #splUnpack ( Place , Evaluation ) [seqstrict(2)]
@@ -458,10 +453,10 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
458453
459454
// Account/Mint::pack_into_slice - writes struct into SPLDataBuffer
460455
rule [spl-account-pack]:
461-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, SRC:Operand DST:Operand .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
462-
=> #splPack(#withDeref(SRC), #withDeref(DST)) ~> #execBlockIdx(TARGET) ...
456+
<k> #execTerminatorCall(_, FUNC, SRC:Operand DST:Operand .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
457+
=> #splPack(#withDeref(SRC), #withDeref(DST)) ~> #continueAt(TARGET)
463458
</k>
464-
requires #isSPLPackFunc(#functionName(lookupFunction(#tyOfCall(FUNC))))
459+
requires #isSPLPackFunc(#functionName(FUNC))
465460
[priority(30), preserves-definedness]
466461
467462
syntax KItem ::= #splPack ( Evaluation , Operand ) [seqstrict(1)]
@@ -474,22 +469,20 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
474469
```{.k .symbolic}
475470
// Rent::from_account_info - navigates to data buffer using DATA_BUFFER_PROJS
476471
rule [spl-rent-from-account-info]:
477-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, OP:Operand .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
472+
<k> #execTerminatorCall(_, FUNC, OP:Operand .Operands, DEST, TARGET, _UNWIND) ~> _CONT
478473
=> #splUnpack(DEST, #appendProjsOp(OP, DATA_BUFFER_PROJS))
479-
~> #execBlockIdx(TARGET)
480-
...
474+
~> #continueAt(TARGET)
481475
</k>
482-
requires #isSPLRentFromAccountInfoFunc(#functionName(lookupFunction(#tyOfCall(FUNC))))
476+
requires #isSPLRentFromAccountInfoFunc(#functionName(FUNC))
483477
[priority(30), preserves-definedness]
484478
485479
// Rent::get - returns stable value, cached in outermost frame
486480
rule [spl-rent-get]:
487-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
481+
<k> #execTerminatorCall(_, FUNC, .Operands, DEST, TARGET, _UNWIND) ~> _CONT
488482
=> #writeSPLSysRent(DEST)
489-
~> #execBlockIdx(TARGET)
490-
...
483+
~> #continueAt(TARGET)
491484
</k>
492-
requires #isSPLRentGetFunc(#functionName(lookupFunction(#tyOfCall(FUNC))))
485+
requires #isSPLRentGetFunc(#functionName(FUNC))
493486
[priority(30), preserves-definedness]
494487
495488
syntax KItem ::= #writeSPLSysRent ( Place )
@@ -538,17 +531,11 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
538531
## Pubkey comparison shortcut
539532
```k
540533
rule [spl-cmp-pubkeys]:
541-
<k> #execTerminator(
542-
terminator(
543-
terminatorKindCall(FUNC, ARG1:Operand ARG2:Operand .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND),
544-
_SPAN
545-
)
546-
)
534+
<k> #execTerminatorCall(_, FUNC, ARG1:Operand ARG2:Operand .Operands, DEST, TARGET, _UNWIND) ~> _CONT
547535
=> #execSPLCmpPubkeys( DEST, #withDeref(ARG1), #withDeref(ARG2))
548-
~> #execBlockIdx(TARGET)
549-
...
536+
~> #continueAt(TARGET)
550537
</k>
551-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "spl_token::processor::Processor::cmp_pubkeys"
538+
requires #functionName(FUNC) ==String "spl_token::processor::Processor::cmp_pubkeys"
552539
[priority(30), preserves-definedness]
553540
554541
syntax KItem ::= #execSPLCmpPubkeys( Place , Evaluation , Evaluation ) [seqstrict(2,3)]

0 commit comments

Comments
 (0)