diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md
index c7c4ffcc9..f7137c421 100644
--- a/src/kontrol/kdist/cheatcodes.md
+++ b/src/kontrol/kdist/cheatcodes.md
@@ -76,8 +76,8 @@ module FOUNDRY-CHEAT-CODES
false
+ .List
false
- .List
.List
@@ -946,6 +946,7 @@ A `StorageSlot` pair is formed from an address and a storage index.
```k
syntax StorageSlot ::= "{" Int "|" Int "}"
+ syntax CallToAddress ::= "{" Int "|" Bytes "}"
// ------------------------------------------
```
@@ -965,15 +966,17 @@ If the address is not in the whitelist `WLIST` then `KEVM` goes into an error st
```k
rule [foundry.catchNonWhitelistedCalls]:
- (#call _ ACCTTO _ _ _ _ false
+ #call _ ACCTTO _ _ _ CALLDATA false
+ /*
~> #popCallStack
- ~> #popWorldState) => #end KONTROL_WHITELISTCALL ...
+ ~> #popWorldState)
+ */ => #end KONTROL_WHITELISTCALL ...
true
- WLIST
+ WLIST
...
- requires notBool ACCTTO in WLIST
+ requires notBool ({ACCTTO|CALLDATA} in WLIST orBool {ACCTTO|b"*"} in WLIST)
[priority(40)]
```
@@ -1003,9 +1006,32 @@ function allowCallsToAddress(address) external;
Adds an account address to the whitelist. The execution of the modified KEVM will stop when a call has been made to an address which is not in the whitelist.
```k
- rule [foundry.allowCallsToAddress]:
- #cheatcode_call SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #addAddressToWhitelist #asWord(ARGS) ...
- requires SELECTOR ==Int selector ( "allowCallsToAddress(address)" )
+ rule [foundry.allowAllCallsToAddress]:
+ #cheatcode_call SELECTOR ARGS
+ => #loadAccount #asWord(ARGS)
+ ~> #setAllowedAllCalls #asWord(ARGS) ...
+ requires SELECTOR ==Int selector("allowCallsToAddress(address)")
+```
+
+#### `allowCalls` - Add an account address and calldata prefix to a whitelist.
+
+```
+function allowCalls(address, bytes calldata data) external;
+```
+
+Adds an account address and calldata prefix to the whitelist. The execution of the modified KEVM will stop when a call has been made to an address and/or with calldata which are not in the whitelist.
+
+```k
+ rule [foundry.allowCalls]:
+ #cheatcode_call SELECTOR ARGS
+ => #loadAccount #asWord(#range(ARGS, 0, 32))
+ ~> #etchAccountIfEmpty #asWord(#range(ARGS, 0, 32))
+ ~> #setAllowedCall
+ #asWord(#range(ARGS, 0, 32))
+ #range(ARGS, #asWord(#range(ARGS, 32, 32)) +Int 32, #asWord(#range(ARGS, #asWord(#range(ARGS, 32, 32)), 32)))
+ ...
+
+ requires SELECTOR ==Int selector ( "allowCalls(address,bytes)" )
```
#### `allowChangesToStorage` - Add an account address and a storage slot to a whitelist.
@@ -1591,14 +1617,14 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
- `#addAddressToWhitelist` enables the whitelist restriction for calls and adds an address to the whitelist.
```k
- syntax KItem ::= "#addAddressToWhitelist" Int [symbol(foundry_addAddressToWhitelist)]
+ // syntax KItem ::= "#addAddressToWhitelist" Int [symbol(foundry_addAddressToWhitelist)]
// -------------------------------------------------------------------------------------
- rule #addAddressToWhitelist ACCT => .K ...
-
- _ => true
- WLIST => WLIST ListItem(ACCT)
- ...
-
+ // rule #addAddressToWhitelist ACCT => .K ...
+ //
+ // _ => true
+ // WLIST => WLIST ListItem(ACCT)
+ // ...
+ //
```
- `#addStorageSlotToWhitelist` enables the whitelist restriction for storage chagnes and adds a `StorageSlot` item to the whitelist.
@@ -1632,6 +1658,27 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
rule #etchAccountIfEmpty _ => .K ... [owise]
```
+- `#setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA` and `setAllowedAllCalls ALLOWEDACCOUNT` will update the `` list with the given account and calldata.
+
+```k
+ syntax KItem ::= "#setAllowedCall" Account Bytes [symbol(foundry_setAllowedCall)]
+ syntax KItem ::= "#setAllowedAllCalls" Account [symbol(foundry_setAllowedAllCalls)]
+ // ---------------------------------------------------------------------------------
+ rule #setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA => .K ...
+
+ _ => true
+ ALLOWEDCALLS => ALLOWEDCALLS ListItem({ALLOWEDACCOUNT|ALLOWEDCALLDATA})
+ ...
+
+
+ rule #setAllowedAllCalls ALLOWEDACCOUNT => .K ...
+
+ _ => true
+ ALLOWEDCALLS => ALLOWEDCALLS ListItem({ALLOWEDACCOUNT|b"*"})
+ ...
+
+```
+
- `#setMockCall MOCKADDRESS MOCKCALLDATA MOCKRETURN` will update the `` mapping for the given account.
```k
@@ -1745,6 +1792,7 @@ Selectors for **implemented** cheat code functions.
rule ( selector ( "prank(address)" ) => 3395723175 )
rule ( selector ( "prank(address,address)" ) => 1206193358 )
rule ( selector ( "allowCallsToAddress(address)" ) => 1850795572 )
+ rule ( selector ( "allowCalls(address,bytes)" ) => 1808051021 )
rule ( selector ( "allowChangesToStorage(address,uint256)" ) => 4207417100 )
rule ( selector ( "infiniteGas()" ) => 3986649939 )
rule ( selector ( "setGas(uint256)" ) => 3713137314 )
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index a9169b5a1..f95707bf6 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -1040,6 +1040,7 @@ def _init_cterm(
'ISSTORAGEWHITELISTACTIVE_CELL': FALSE,
'ADDRESSLIST_CELL': list_empty(),
'STORAGESLOTLIST_CELL': list_empty(),
+ 'ALLOWEDCALLSLIST_CELL': list_empty(),
'MOCKCALLS_CELL': KApply('.MockCallCellMap'),
'MOCKFUNCTIONS_CELL': KApply('.MockFunctionCellMap'),
'ACTIVETRACING_CELL': TRUE if trace_options.active_tracing else FALSE,