Add allowCalls cheatcode (#926)

* Draft for the `allowCalls` implementation * Make `AllowedCallCellMap` empty in init cterm * `allowedCallsList` refactoring, add `allowedAllCalls` * Add new rule, K cell pattern * Add list simplifications * Adjust and add tests for `allowCalls` * Add tests for `allowCalls` to end-to-end tests * Update expected output in `end-to-end` tests * Remove fixed `kontrol-cheatcodes` version * Removed a TODO comment * `cheatcodes.md` cleanup * Remove `ADDRESSLIST_CELL` * `AllowChangesTest` cleanup * Another output update * Update expected output * Update CSE expected output * Update `trace` tests output * Use `auxiliary_lemmas` in end-to-end tests * Output update for `RandomVarTest` * Enable `auxiliary_lemmas` in `build` instead of `prove` * Change `testFailAllowCalls_ifNotWhitelisted` signature * Remove `expectRevert` from failing test * Apply review suggestion Co-authored-by: Andrei Văcaru <[email protected]> * Another output update for `RandomVarTest` * Reduce `end-to-end` parallel processes to 6 * update expected output * Apply `CallToAddress` review suggestion Co-authored-by: Andrei Văcaru <[email protected]> * Use `.Bytes` to represent all calls being allowed * Another output update for `RandomVarTest.test_custom_names` * Experiment: add `--force-sequential` to end-to-end tests * Reduce num processes in the update-output job to 4 * Update `RandomVarTest.test_custom_names` * update expected output * see full diff in ci * show diff in ci * update expected output * Change Solidity version in `AllowChangesTest` * Add `end-to-end` tests to the output update workflow * Update Solidity versions in `allow` tests * Bring back source maps for tests with expected output * Address review comments --------- Co-authored-by: Andrei Văcaru <[email protected]>
runtimeverification · Jan 28, 2025 · 895036a · 895036a
1 parent 9de9378
commit 895036a
Show file tree

Hide file tree

Showing 61 changed files with 951 additions and 843 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -149,7 +149,7 @@ jobs:
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry'
       - name: 'Run end-to-end tests'
         run: |
-          TEST_ARGS='--numprocesses=8 -vv -k "test_kontrol_end_to_end"'
+          TEST_ARGS='--numprocesses=6 -vv --force-sequential -k "test_kontrol_end_to_end"'
           docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}"
       - name: 'Tear down Docker'
         if: always()

diff --git a/.github/workflows/update-expected-output.yml b/.github/workflows/update-expected-output.yml
@@ -28,9 +28,10 @@ jobs:
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry'
       - name: 'Run integration tests'
         run: |
-          TEST_ARGS="--maxfail=1000 --numprocesses=6 --update-expected-output --force-sequential -vv"
+          TEST_ARGS="--maxfail=1000 --numprocesses=4 --update-expected-output --force-sequential -vv"
           docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end)\"' || true"
           docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_cse or test_foundry_minimize_proof\"' || true"
+          docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_end_to_end\"' || true"
       - name: 'Copy updated files to host'
         run: |
           docker cp kontrol-ci-integration-${GITHUB_SHA}:/home/github-user/workspace/src/tests/integration/test-data/show ./src/tests/integration/test-data/

diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md
@@ -76,8 +76,8 @@ module FOUNDRY-CHEAT-CODES
         </expectEmit>
         <whitelist>
           <isCallWhitelistActive> false </isCallWhitelistActive>
+          <allowedCallsList> .List </allowedCallsList>
           <isStorageWhitelistActive> false </isStorageWhitelistActive>
-          <addressList> .List </addressList>
           <storageSlotList> .List </storageSlotList>
         </whitelist>
         <mockCalls>
@@ -946,7 +946,8 @@ A `StorageSlot` pair is formed from an address and a storage index.
 
 ```k
     syntax StorageSlot ::= "{" Int "|" Int "}"
- // ------------------------------------------
+    syntax CallToAddress ::= "{" Int "|" Bytes "}"
+ // ----------------------------------------------
 ```
 
 We define two new status codes:
@@ -965,15 +966,14 @@ If the address is not in the whitelist `WLIST` then `KEVM` goes into an error st
 
 ```k
     rule [foundry.catchNonWhitelistedCalls]:
-         <k> (#call _ ACCTTO _ _ _ _ false
-          ~> #popCallStack
-          ~> #popWorldState) => #end KONTROL_WHITELISTCALL ... </k>
+         <k> (#call _ ACCTTO _ _ _ CALLDATA false
+          ~> #return _ _) => #end KONTROL_WHITELISTCALL ... </k>
          <whitelist>
            <isCallWhitelistActive> true </isCallWhitelistActive>
-           <addressList> WLIST </addressList>
+           <allowedCallsList> WLIST </allowedCallsList>
            ...
          </whitelist>
-      requires notBool ACCTTO in WLIST
+      requires notBool ({ACCTTO|CALLDATA} in WLIST orBool {ACCTTO|.Bytes} in WLIST)
       [priority(40)]
 ```
 
@@ -1003,9 +1003,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]:
-         <k> #cheatcode_call SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #addAddressToWhitelist #asWord(ARGS) ... </k>
-         requires SELECTOR ==Int selector ( "allowCallsToAddress(address)" )
+    rule [foundry.allowAllCallsToAddress]:
+         <k> #cheatcode_call SELECTOR ARGS
+          => #loadAccount #asWord(ARGS)
+          ~> #setAllowedCall #asWord(ARGS) .Bytes  ... </k>
+         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]:
+         <k> #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)))
+         ...
+         </k>
+         requires SELECTOR ==Int selector ( "allowCalls(address,bytes)" )
 ```
 
 #### `allowChangesToStorage` - Add an account address and a storage slot to a whitelist.
@@ -1608,19 +1631,6 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
     rule #checkTopics(ListItem(CHECK) CHECKS, ListItem(V1) L1, ListItem(V2) L2) => #checkTopic(CHECK, V1, V2) andBool #checkTopics(CHECKS, L1, L2) requires size(L1) ==Int size(L2)
 ```
 
-- `#addAddressToWhitelist` enables the whitelist restriction for calls and adds an address to the whitelist.
-
-```k
-    syntax KItem ::= "#addAddressToWhitelist" Int [symbol(foundry_addAddressToWhitelist)]
- // -------------------------------------------------------------------------------------
-    rule <k> #addAddressToWhitelist ACCT => .K ... </k>
-        <whitelist>
-          <isCallWhitelistActive> _ => true </isCallWhitelistActive>
-          <addressList> WLIST => WLIST ListItem(ACCT) </addressList>
-          ...
-        </whitelist>
-```
-
 - `#addStorageSlotToWhitelist` enables the whitelist restriction for storage chagnes and adds a `StorageSlot` item to the whitelist.
 
 ```k
@@ -1652,6 +1662,19 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
     rule <k> #etchAccountIfEmpty _ => .K ... </k> [owise]
 ```
 
+- `#setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA` and `setAllowedAllCalls ALLOWEDACCOUNT` will update the `<allowedCallsList>` list with the given account and calldata.
+
+```k
+    syntax KItem ::= "#setAllowedCall" Account Bytes [symbol(foundry_setAllowedCall)]
+ // -----------------------------------------------------------------------------------
+    rule <k> #setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA => .K ... </k>
+         <whitelist>
+            <isCallWhitelistActive> _ => true </isCallWhitelistActive>
+            <allowedCallsList> ALLOWEDCALLS => ALLOWEDCALLS ListItem({ALLOWEDACCOUNT|ALLOWEDCALLDATA}) </allowedCallsList>
+            ...
+         </whitelist>
+```
+
 - `#setMockCall MOCKADDRESS MOCKCALLDATA MOCKRETURN` will update the `<mockcalls>` mapping for the given account.
 
 ```k
@@ -1765,6 +1788,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/kdist/kontrol_lemmas.md b/src/kontrol/kdist/kontrol_lemmas.md
@@ -188,5 +188,18 @@ module KONTROL-AUX-LEMMAS
       requires 0 <Int X andBool 0 <=Int Z andBool ( Z +Int 1) modInt X ==Int 0
       [simplification, concrete(X, Z), preserves-definedness]
 
+    //
+    // List simplifications for `allowCalls`
+    //
+
+    // List membership check simplification for lists with a single element
+    rule KI:KItem in ListItem(KI:KItem) => true [simplification]
+    rule KI:KItem in ListItem(KJ:KItem) => KI ==K KJ [simplification]
+
+    // Recursive list membership check for lists with multiple elements
+    rule KI:KItem in (ListItem(KI) Rest) => true [simplification]
+    rule KI:KItem in (ListItem(KJ) Rest) => KI in Rest [simplification]
+    rule KI:KItem in .List => false [simplification]
+
 endmodule
 ```
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
@@ -1038,8 +1038,8 @@ def _init_cterm(
         'ISEVENTEXPECTED_CELL': FALSE,
         'ISCALLWHITELISTACTIVE_CELL': FALSE,
         '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,
@@ -1425,7 +1425,7 @@ def _final_term(
         'ISEVENTEXPECTED_CELL': KVariable('ISEVENTEXPECTED_FINAL'),
         'ISCALLWHITELISTACTIVE_CELL': KVariable('ISCALLWHITELISTACTIVE_FINAL'),
         'ISSTORAGEWHITELISTACTIVE_CELL': KVariable('ISSTORAGEWHITELISTACTIVE_FINAL'),
-        'ADDRESSLIST_CELL': KVariable('ADDRESSLIST_FINAL'),
+        'ALLOWEDCALLSLIST_CELL': KVariable('ALLOWEDCALLSLIST_FINAL'),
         'STORAGESLOTLIST_CELL': KVariable('STORAGESLOTLIST_FINAL'),
     }
 

diff --git a/src/tests/integration/test-data/end-to-end-prove-all b/src/tests/integration/test-data/end-to-end-prove-all
@@ -1,3 +1,5 @@
+AllowChangesTest.testAllowCalls(uint256)
+AllowChangesTest.testFailAllowCalls_ifNotWhitelisted(uint256)
 CounterTest.test_Increment()
 ForgetBranchTest.test_forgetBranch(uint256)
 RandomVarTest.test_custom_names()

diff --git a/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol b/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol
@@ -42,13 +42,11 @@ contract AllowChangesTest is Test, KontrolCheats {
 	}
 	function testFailAllowCallsToAddress() public {
 		kevm.allowCallsToAddress(address(canChange));
-		kevm.allowChangesToStorage(address(canChange), 0);
 
 		cannotChange.changeSlot0(10245);
 	}
 
 	function testFailAllowChangesToStorage() public {
-		kevm.allowCallsToAddress(address(canChange));
 		kevm.allowChangesToStorage(address(canChange), 0);
 
 		canChange.changeSlot1(23452);

diff --git a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected
@@ -258,12 +258,12 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0
                <isCallWhitelistActive>
                  false
                </isCallWhitelistActive>
+               <allowedCallsList>
+                 .List
+               </allowedCallsList>
                <isStorageWhitelistActive>
                  false
                </isStorageWhitelistActive>
-               <addressList>
-                 .List
-               </addressList>
                <storageSlotList>
                  .List
                </storageSlotList>

diff --git a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
@@ -189,12 +189,12 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                <isCallWhitelistActive>
                  false
                </isCallWhitelistActive>
+               <allowedCallsList>
+                 .List
+               </allowedCallsList>
                <isStorageWhitelistActive>
                  false
                </isStorageWhitelistActive>
-               <addressList>
-                 .List
-               </addressList>
                <storageSlotList>
                  .List
                </storageSlotList>
@@ -368,12 +368,12 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                <isCallWhitelistActive>
                  false
                </isCallWhitelistActive>
+               <allowedCallsList>
+                 .List
+               </allowedCallsList>
                <isStorageWhitelistActive>
                  false
                </isStorageWhitelistActive>
-               <addressList>
-                 .List
-               </addressList>
                <storageSlotList>
                  .List
                </storageSlotList>

diff --git a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected
@@ -218,12 +218,12 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0
                <isCallWhitelistActive>
                  false
                </isCallWhitelistActive>
+               <allowedCallsList>
+                 .List
+               </allowedCallsList>
                <isStorageWhitelistActive>
                  false
                </isStorageWhitelistActive>
-               <addressList>
-                 .List
-               </addressList>
                <storageSlotList>
                  .List
                </storageSlotList>

diff --git a/...tegration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected b/...tegration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected
@@ -450,12 +450,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                <isCallWhitelistActive>
                  false
                </isCallWhitelistActive>
+               <allowedCallsList>
+                 .List
+               </allowedCallsList>
                <isStorageWhitelistActive>
                  false
                </isStorageWhitelistActive>
-               <addressList>
-                 .List
-               </addressList>
                <storageSlotList>
                  .List
                </storageSlotList>
@@ -859,12 +859,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                <isCallWhitelistActive>
                  false
                </isCallWhitelistActive>
+               <allowedCallsList>
+                 .List
+               </allowedCallsList>
                <isStorageWhitelistActive>
                  false
                </isStorageWhitelistActive>
-               <addressList>
-                 .List
-               </addressList>
                <storageSlotList>
                  .List
                </storageSlotList>
@@ -1250,12 +1250,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                <isCallWhitelistActive>
                  false
                </isCallWhitelistActive>
+               <allowedCallsList>
+                 .List
+               </allowedCallsList>
                <isStorageWhitelistActive>
                  false
                </isStorageWhitelistActive>
-               <addressList>
-                 .List
-               </addressList>
                <storageSlotList>
                  .List
                </storageSlotList>
@@ -1643,12 +1643,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                <isCallWhitelistActive>
                  false
                </isCallWhitelistActive>
+               <allowedCallsList>
+                 .List
+               </allowedCallsList>
                <isStorageWhitelistActive>
                  false
                </isStorageWhitelistActive>
-               <addressList>
-                 .List
-               </addressList>
                <storageSlotList>
                  .List
                </storageSlotList>
@@ -2037,12 +2037,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                <isCallWhitelistActive>
                  false
                </isCallWhitelistActive>
+               <allowedCallsList>
+                 .List
+               </allowedCallsList>
                <isStorageWhitelistActive>
                  false
                </isStorageWhitelistActive>
-               <addressList>
-                 .List
-               </addressList>
                <storageSlotList>
                  .List
                </storageSlotList>