Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into release
Browse files Browse the repository at this point in the history
  • Loading branch information
rv-jenkins committed Sep 14, 2024
2 parents 0b1823e + 86451cb commit 53feda1
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion src/kontrol/kdist/cheatcodes.md
Original file line number Diff line number Diff line change
Expand Up @@ -328,15 +328,17 @@ This rule then takes from the function call data the account using `#asWord(#ran

```
function symbolicStorage(address) external;
function setArbitraryStorage(address) external;
```

`cheatcode.call.symbolicStorage` will match when the `symbolicStorage` cheat code function is called.
`cheatcode.call.symbolicStorage` will match when either of the `symbolicStorage` or `setArbitraryStorage` cheat code functions are called.
This rule then takes the address using `#asWord(#range(ARGS, 0, 32))` and makes its storage completely symbolic.

```k
rule [cheatcode.call.symbolicStorage]:
<k> #cheatcode_call SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #setSymbolicStorage #asWord(ARGS) ... </k>
requires SELECTOR ==Int selector ( "symbolicStorage(address)" )
orBool SELECTOR ==Int selector ( "setArbitraryStorage(address)")
```

#### `copyStorage` - Copies the storage of one account into another.
Expand Down Expand Up @@ -1585,6 +1587,7 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
rule ( selector ( "expectEmit(bool,bool,bool,bool,address)" ) => 2176505587 )
rule ( selector ( "sign(uint256,bytes32)" ) => 3812747940 )
rule ( selector ( "symbolicStorage(address)" ) => 769677742 )
rule ( selector ( "setArbitraryStorage(address)" ) => 3781367863 )
rule ( selector ( "freshUInt(uint8)" ) => 625253732 )
rule ( selector ( "freshBool()" ) => 2935720297 )
rule ( selector ( "freshBytes(uint256)" ) => 1389402351 )
Expand Down

0 comments on commit 53feda1

Please sign in to comment.