Skip to content

Commit ae678d6

Browse files
tothtamas28tothtamas28
authored
Add concrete interpretation for symbolic cheatcodes (#785)
1 parent 050e42f commit ae678d6

File tree

1 file changed

+199
-37
lines changed
  • kmir/src/kmir/kdist/mir-semantics/symbolic

1 file changed

+199
-37
lines changed

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

Lines changed: 199 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -387,7 +387,7 @@ An `AccountInfo` reference is passed to the function.
387387
rule #functionName(IntrinsicFunction(symbol(NAME))) => NAME
388388
```
389389

390-
```{.k .symbolic}
390+
```k
391391
// special rule to intercept the cheat code function calls and replace them by #mkPToken<thing>
392392
rule [cheatcode-is-account]:
393393
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(PLACE) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
@@ -415,7 +415,7 @@ An `AccountInfo` reference is passed to the function.
415415
syntax KItem ::= #mkPTokenAccount ( Place )
416416
| #mkPTokenMint ( Place )
417417
| #mkPTokenRent ( Place )
418-
// | #mkPTokenMultisig ( Place )
418+
// | #mkPTokenMultisig ( Place )
419419
420420
// place assumed to be a ref to an AccountInfo, having 1 field holding a pointer to an account
421421
// dereference, then read and dereference pointer in field 1 to read the account data
@@ -424,47 +424,60 @@ An `AccountInfo` reference is passed to the function.
424424
rule
425425
<k> #mkPTokenAccount(place(LOCAL, PROJS))
426426
=> #setLocalValue(
427-
place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), ?HACK) projectionElemDeref .ProjectionElems)),
428-
#addAccount(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), ?HACK) projectionElemDeref .ProjectionElems)))))
427+
place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)),
428+
#addAccount(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)))))
429429
...
430430
</k>
431431
432432
rule
433433
<k> #mkPTokenMint(place(LOCAL, PROJS))
434434
=> #setLocalValue(
435-
place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), ?HACK) projectionElemDeref .ProjectionElems)),
436-
#addMint(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), ?HACK) projectionElemDeref .ProjectionElems)))))
435+
place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)),
436+
#addMint(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)))))
437437
...
438438
</k>
439439
440440
rule
441441
<k> #mkPTokenRent(place(LOCAL, PROJS))
442442
=> #setLocalValue(
443-
place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), ?HACK) projectionElemDeref .ProjectionElems)),
444-
#addRent(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), ?HACK) projectionElemDeref .ProjectionElems)))))
443+
place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)),
444+
#addRent(operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems)))))
445445
...
446446
</k>
447+
```
448+
449+
```k
450+
syntax Ty ::= #hack() [function, total, symbol(#hack)]
451+
rule #hack() => ty(0)
452+
```
447453

454+
```k
448455
syntax Evaluation ::= #addAccount ( Evaluation ) [seqstrict()]
449456
| #addMint ( Evaluation ) [seqstrict()]
450457
| #addRent ( Evaluation ) [seqstrict()]
451-
// | #addMultisig ( Evaluation ) [seqstrict()]
458+
// | #addMultisig ( Evaluation ) [seqstrict()]
459+
```
452460

461+
#### `#addAccount`
462+
463+
```{.k .symbolic}
453464
// NB these rewrites also ensure the data_len field in PAcc is set correctly for the given data
454465
rule #addAccount(Aggregate(variantIdx(0), _:List ListItem(Integer(DATA_LEN, 64, false))) #as P_ACC)
455466
=> PAccountAccount(
456-
#toPAcc(P_ACC),
457-
IAcc(Key(?MINT),
458-
Key(?OWNER),
459-
Amount(?AMOUNT),
460-
Flag(?DELEGATEFLAG), Key(?DELEGATE),
461-
U8(?STATE),
462-
Flag(?NATIVEFLAG),
463-
Amount(?NATIVE_AMOUNT),
464-
Amount(?DELEG_AMOUNT),
465-
Flag(?CLOSEFLAG), Key(?CLOSE_AUTH)
466-
)
467-
)
467+
#toPAcc(P_ACC),
468+
IAcc(Key(?MINT),
469+
Key(?OWNER),
470+
Amount(?AMOUNT),
471+
Flag(?DELEGATEFLAG),
472+
Key(?DELEGATE),
473+
U8(?STATE),
474+
Flag(?NATIVEFLAG),
475+
Amount(?NATIVE_AMOUNT),
476+
Amount(?DELEG_AMOUNT),
477+
Flag(?CLOSEFLAG),
478+
Key(?CLOSE_AUTH)
479+
)
480+
)
468481
ensures 0 <=Int ?STATE andBool ?STATE <Int 256
469482
andBool 0 <=Int ?DELEGATEFLAG andBool ?DELEGATEFLAG <=Int 1 // not allowed any other values
470483
andBool 0 <=Int ?NATIVEFLAG andBool ?NATIVEFLAG <=Int 1 // not allowed any other values
@@ -477,17 +490,43 @@ An `AccountInfo` reference is passed to the function.
477490
andBool 0 <=Int ?NATIVE_AMOUNT andBool ?NATIVE_AMOUNT <Int 1 <<Int 64
478491
andBool 0 <=Int ?DELEG_AMOUNT andBool ?DELEG_AMOUNT <Int 1 <<Int 64
479492
andBool DATA_LEN ==Int 165 // size_of(Account), see pinocchio_token_interface::state::Transmutable instance
493+
```
480494

495+
```{.k .concrete}
496+
rule #addAccount(Aggregate(variantIdx(0), _:List ListItem(Integer(DATA_LEN, 64, false))) #as P_ACC)
497+
=> PAccountAccount(
498+
#toPAcc(P_ACC),
499+
IAcc(#randKey(), // mint
500+
#randKey(), // owner
501+
#randAmount(), // amount
502+
Flag(#randU1()), // delegateflag, only 0 or 1 allowed
503+
#randKey(), // delegate
504+
U8(#randU8()), // state
505+
Flag(#randU1()), // nativeflag, only 0 or 1 allowed
506+
#randAmount(), // native_amount
507+
#randAmount(), // deleg_amount
508+
Flag(#randU1()), // closeflag, only 0 or 1 allowed
509+
#randKey() // close_auth
510+
)
511+
)
512+
requires DATA_LEN ==Int 165 // size_of(Account), see pinocchio_token_interface::state::Transmutable instance
513+
```
514+
515+
#### `#addMint`
516+
517+
```{.k .symbolic}
481518
rule #addMint(Aggregate(variantIdx(0), _:List ListItem(Integer(DATA_LEN, 64, false))) #as P_ACC)
482519
=> PAccountMint(
483-
#toPAcc(P_ACC),
484-
IMint(Flag(?MINT_AUTH_FLAG), Key(?MINT_AUTH_KEY),
485-
Amount(?SUPPLY),
486-
U8(?DECIMALS),
487-
U8(?INITIALISED),
488-
Flag(?FREEZE_AUTH_FLAG), Key(?FREEZE_AUTH_KEY)
489-
)
490-
)
520+
#toPAcc(P_ACC),
521+
IMint(Flag(?MINT_AUTH_FLAG),
522+
Key(?MINT_AUTH_KEY),
523+
Amount(?SUPPLY),
524+
U8(?DECIMALS),
525+
U8(?INITIALISED),
526+
Flag(?FREEZE_AUTH_FLAG),
527+
Key(?FREEZE_AUTH_KEY)
528+
)
529+
)
491530
ensures 0 <=Int ?DECIMALS andBool ?DECIMALS <Int 256
492531
andBool 0 <=Int ?INITIALISED andBool ?INITIALISED <=Int 1 // not allowed any other values
493532
andBool 0 <=Int ?MINT_AUTH_FLAG andBool ?MINT_AUTH_FLAG <=Int 1 // not allowed any other values
@@ -496,17 +535,54 @@ An `AccountInfo` reference is passed to the function.
496535
andBool size(?FREEZE_AUTH_KEY) ==Int 32 andBool allBytes(?FREEZE_AUTH_KEY)
497536
andBool 0 <=Int ?SUPPLY andBool ?SUPPLY <Int 1 <<Int 64
498537
andBool DATA_LEN ==Int 82 // size_of(Mint), see pinocchio_token_interface::state::Transmutable instance
538+
```
499539

540+
```{.k .concrete}
541+
rule #addMint(Aggregate(variantIdx(0), _:List ListItem(Integer(DATA_LEN, 64, false))) #as P_ACC)
542+
=> PAccountMint(
543+
#toPAcc(P_ACC),
544+
IMint(Flag(#randU1()), // mint_auth_flag, only 0 or 1 allowed
545+
#randKey(), // mint_auth_key
546+
#randAmount(), // supply
547+
U8(#randU8()), // decimals
548+
U8(#randU1()), // initialized, only 0 or 1 allowed
549+
Flag(#randU1()), // freeze_auth_flag, only 0 or 1 allowed
550+
#randKey() // freeze_auth_key
551+
)
552+
)
553+
requires DATA_LEN ==Int 82 // size_of(Mint), see pinocchio_token_interface::state::Transmutable instance
554+
```
555+
556+
#### `#addRent`
557+
558+
```{.k .symbolic}
500559
rule #addRent(Aggregate(variantIdx(0), _:List ListItem(Integer(DATA_LEN, 64, false))) #as P_ACC)
501560
=> PAccountRent(
502-
#toPAcc(P_ACC),
503-
PRent(U64(?LMP_PER_BYTEYEAR), F64(?_EXEMPT_THRESHOLD), U8(?BURN_PCT))
504-
)
561+
#toPAcc(P_ACC),
562+
PRent(
563+
U64(?LMP_PER_BYTEYEAR),
564+
F64(?_EXEMPT_THRESHOLD),
565+
U8(?BURN_PCT)
566+
)
567+
)
505568
ensures 0 <=Int ?LMP_PER_BYTEYEAR andBool ?LMP_PER_BYTEYEAR <Int 1 <<Int 64
506569
andBool 0 <=Int ?BURN_PCT andBool ?BURN_PCT <Int 256
507570
andBool DATA_LEN ==Int 17 // size_of(Rent), see pinocchio::sysvars::rent::Rent::LEN
508571
```
509572

573+
```{.k .concrete}
574+
rule #addRent(Aggregate(variantIdx(0), _:List ListItem(Integer(DATA_LEN, 64, false))) #as P_ACC)
575+
=> PAccountRent(
576+
#toPAcc(P_ACC),
577+
PRent(
578+
U64(#randU64()), // lmp_per_byteyear
579+
F64(#randExemptThreshold()), // exempt_threshold
580+
U8(#randU8()) // burn_pct
581+
)
582+
)
583+
requires DATA_LEN ==Int 17 // size_of(Rent), see pinocchio::sysvars::rent::Rent::LEN
584+
```
585+
510586
### Establishing Access to the Second Component of a `PAccount`-sorted Value
511587

512588
Access to the data structure that follow a pinocchio account is usually via characteristic sequences of statements:
@@ -536,11 +612,11 @@ The `PAccByteRef` carries a stack offset, so it must be adjusted on reads.
536612
rule #adjustRef(PAccByteRef(HEIGHT, PLACE, MUT, LEN), OFFSET) => PAccByteRef(HEIGHT +Int OFFSET, PLACE, MUT, LEN)
537613
```
538614

539-
```{.k .symbolic}
615+
```k
540616
// intercept calls to `borrow_data_unchecked` and write `PAccountRef` to destination
541617
rule [cheatcode-borrow-data]:
542618
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
543-
=> #mkPAccByteRef(DEST, operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), ?_HACK) .ProjectionElems))), mutabilityNot)
619+
=> #mkPAccByteRef(DEST, operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) .ProjectionElems))), mutabilityNot)
544620
~> #execBlockIdx(TARGET)
545621
...
546622
</k>
@@ -550,7 +626,7 @@ The `PAccByteRef` carries a stack offset, so it must be adjusted on reads.
550626
// intercept calls to `borrow_mut_data_unchecked` and write `PAccountRef` to destination
551627
rule [cheatcode-borrow-mut-data]:
552628
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
553-
=> #mkPAccByteRef(DEST, operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), ?_HACK) .ProjectionElems))), mutabilityMut)
629+
=> #mkPAccByteRef(DEST, operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) .ProjectionElems))), mutabilityMut)
554630
~> #execBlockIdx(TARGET)
555631
...
556632
</k>
@@ -610,7 +686,7 @@ While the `PAccByteRef` is generic, the `load_*` functions are specific to the c
610686
A (small) complication is that the reference is returned within a `Result` enum.
611687
NB Both `load_unchecked` and `load_mut_unchecked` are intercepted in the same way, mutability information is already held in the `PAccountByteRef`.
612688

613-
```{.k .symbolic}
689+
```k
614690
// intercept calls to `load_unchecked` and `load_mut_unchecked`
615691
rule [cheatcode-mk-iface-account-ref]:
616692
<k> #execTerminator(terminator(terminatorKindCall(FUNC, OPERAND .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
@@ -687,7 +763,15 @@ Only the system Rent will be stored as a value directly. The `SysRent` wrapper i
687763
=> #setLocalValue(
688764
DEST,
689765
Aggregate(variantIdx(0), // returns a Result type
690-
ListItem(SysRent(PRent(U64(?SYS_LMP_PER_BYTEYEAR), F64(?_SYS_EXEMPT_THRESHOLD), U8(?SYS_BURN_PCT))))
766+
ListItem(
767+
SysRent(
768+
PRent(
769+
U64(?SYS_LMP_PER_BYTEYEAR),
770+
F64(?_SYS_EXEMPT_THRESHOLD),
771+
U8(?SYS_BURN_PCT)
772+
)
773+
)
774+
)
691775
)
692776
)
693777
~> #execBlockIdx(TARGET)
@@ -699,6 +783,30 @@ Only the system Rent will be stored as a value directly. The `SysRent` wrapper i
699783
[priority(30), preserves-definedness]
700784
```
701785

786+
```{.k .concrete}
787+
rule [cheatcode-get-sys-prent]:
788+
<k> #execTerminator(terminator(terminatorKindCall(FUNC, .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
789+
=> #setLocalValue(
790+
DEST,
791+
Aggregate(variantIdx(0), // returns a Result type
792+
ListItem(
793+
SysRent(
794+
PRent(
795+
U64(#randU64()), // sys_lmp_per_byteyear
796+
F64(#randExemptThreshold()), // sys_exempt_threshold
797+
U8(#randU8()) // sys_burn_pct
798+
)
799+
)
800+
)
801+
)
802+
)
803+
~> #execBlockIdx(TARGET)
804+
...
805+
</k>
806+
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "<sysvars::rent::Rent as sysvars::Sysvar>::get"
807+
[priority(30)]
808+
```
809+
702810
### Access to the `Rent` struct
703811

704812
When accessing the `SysRent`, the data structure is transformed to a normal `Aggregate` struct on the fly
@@ -773,6 +881,60 @@ NB The projection rule must have higher priority than the one which auto-project
773881
[preserves-definedness] // by construction, VAL has the right shape from introducing the context
774882
```
775883

884+
## Helpers for fuzzing
885+
886+
```{.k .concrete}
887+
syntax Int ::= #randU1() [function, total, impure, symbol(randU1) ]
888+
| #randU8() [function, total, impure, symbol(randU8) ]
889+
| #randU32() [function, total, impure, symbol(randU32)]
890+
| #randU64() [function, total, impure, symbol(randU64)]
891+
892+
rule #randU1() => randInt(2)
893+
rule #randU8() => randInt(256)
894+
rule #randU32() => randInt(4294967296)
895+
rule #randU64() => randInt(18446744073709551616)
896+
897+
syntax Float ::= #randExemptThreshold() [function, total, impure, symbol(randExemptThreshold)]
898+
rule #randExemptThreshold() => Int2Float(#randU32(), 52, 11)
899+
900+
syntax Amount ::= #randAmount() [function, total, impure, symbol(randAmount)]
901+
rule #randAmount() => Amount(#randU64())
902+
903+
syntax Key ::= #randKey() [function, total, impure, symbol(randKey)]
904+
rule #randKey() => Key(ListItem(Integer(#randU8(), 8, false))
905+
ListItem(Integer(#randU8(), 8, false))
906+
ListItem(Integer(#randU8(), 8, false))
907+
ListItem(Integer(#randU8(), 8, false))
908+
ListItem(Integer(#randU8(), 8, false))
909+
ListItem(Integer(#randU8(), 8, false))
910+
ListItem(Integer(#randU8(), 8, false))
911+
ListItem(Integer(#randU8(), 8, false))
912+
ListItem(Integer(#randU8(), 8, false))
913+
ListItem(Integer(#randU8(), 8, false))
914+
ListItem(Integer(#randU8(), 8, false))
915+
ListItem(Integer(#randU8(), 8, false))
916+
ListItem(Integer(#randU8(), 8, false))
917+
ListItem(Integer(#randU8(), 8, false))
918+
ListItem(Integer(#randU8(), 8, false))
919+
ListItem(Integer(#randU8(), 8, false))
920+
ListItem(Integer(#randU8(), 8, false))
921+
ListItem(Integer(#randU8(), 8, false))
922+
ListItem(Integer(#randU8(), 8, false))
923+
ListItem(Integer(#randU8(), 8, false))
924+
ListItem(Integer(#randU8(), 8, false))
925+
ListItem(Integer(#randU8(), 8, false))
926+
ListItem(Integer(#randU8(), 8, false))
927+
ListItem(Integer(#randU8(), 8, false))
928+
ListItem(Integer(#randU8(), 8, false))
929+
ListItem(Integer(#randU8(), 8, false))
930+
ListItem(Integer(#randU8(), 8, false))
931+
ListItem(Integer(#randU8(), 8, false))
932+
ListItem(Integer(#randU8(), 8, false))
933+
ListItem(Integer(#randU8(), 8, false))
934+
ListItem(Integer(#randU8(), 8, false))
935+
ListItem(Integer(#randU8(), 8, false)))
936+
```
937+
776938
```k
777939
endmodule
778940
```

0 commit comments

Comments
 (0)