Implement prank cheat code (#1446)

* add prank cheatcode

* remove #checkSinglePrank

* add docs

* check depth

* expected depth should be equal to prank depth plus one

* Update include/kframework/foundry.md

Co-authored-by: Everett Hildenbrandt <[email protected]>

* update foundry.k.check

* initialize singleCaller cell to false

Co-authored-by: Everett Hildenbrandt <[email protected]>

Author: anvacaru

include/kframework/foundry.md

@@ -581,6 +581,21 @@ Finally, the original sender of the transaction, `ACCTFROM` is changed to the ne
       [priority(40)]
 ```
 
+We define a new rule for the `#halt ~> #return _ _` production that will trigger the `#endPrank` rules if the prank was set only for a single call and if the current call depth is equal to the depth at which `prank` was invoked plus one.
+
+
+```{.k .bytes}
+    rule <k> (. => #endPrank) ~> #halt ~> #return _RETSTART _RETWIDTH ... </k>
+         <callDepth> CD </callDepth>
+         <prank>
+           <singleCall> true </singleCall>
+           <depth> PD </depth>
+           ...
+         </prank>
+      requires CD ==Int PD +Int 1
+      [priority(40)]
+```
+
 #### `startPrank` - Sets `msg.sender` and `tx.origin` for all subsequent calls until `stopPrank` is called.
 
 ```
@@ -594,14 +609,31 @@ The `#loadAccount` production is used to load accounts into the state if they ar
 
 ```{.k .bytes}
     rule [foundry.call.startPrank]:
-         <k> #call_foundry SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #setPrank #asWord(ARGS) .Account ... </k>
+         <k> #call_foundry SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #setPrank #asWord(ARGS) .Account false ... </k>
       requires SELECTOR ==Int selector ( "startPrank(address)" )
 
     rule [foundry.call.startPrankWithOrigin]:
-         <k> #call_foundry SELECTOR ARGS => #loadAccount  #asWord(#range(ARGS, 0, 32)) ~> #loadAccount #asWord(#range(ARGS, 32, 32)) ~> #setPrank #asWord(#range(ARGS, 0, 32)) #asWord(#range(ARGS, 32, 32)) ... </k>
+         <k> #call_foundry SELECTOR ARGS => #loadAccount #asWord(#range(ARGS, 0, 32)) ~> #loadAccount #asWord(#range(ARGS, 32, 32)) ~> #setPrank #asWord(#range(ARGS, 0, 32)) #asWord(#range(ARGS, 32, 32)) false ... </k>
       requires SELECTOR ==Int selector ( "startPrank(address,address)" )
 ```
 
+#### `prank` - Impersonate `msg.sender` and `tx.origin` for only for the next call.
+
+```
+function prank(address) external;
+function prank(address sender, address origin) external;
+```
+
+```{.k .bytes}
+    rule [foundry.call.prank]:
+         <k> #call_foundry SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #setPrank #asWord(ARGS) .Account true ... </k>
+      requires SELECTOR ==Int selector ( "prank(address)" )
+
+    rule [foundry.call.prankWithOrigin]:
+         <k> #call_foundry SELECTOR ARGS => #loadAccount #asWord(#range(ARGS, 0, 32)) ~> #loadAccount #asWord(#range(ARGS, 32, 32)) ~> #setPrank #asWord(#range(ARGS, 0, 32)) #asWord(#range(ARGS, 32, 32)) true ... </k>
+      requires SELECTOR ==Int selector ( "prank(address,address)" )
+```
+
 #### `stopPrank` - Stops impersonating `msg.sender` and `tx.origin`.
 
 ```
@@ -736,12 +768,12 @@ Utils
          </expected>
 ```
 
-- `#setPrank NEWCALLER NEWORIGIN` will set the `<prank/>` subconfiguration for the given accounts.
+- `#setPrank NEWCALLER NEWORIGIN SINGLEPRANK` will set the `<prank/>` subconfiguration for the given accounts.
 
 ```k
-    syntax KItem ::= "#setPrank" Int Account [klabel(foundry_setPrank)]
- // -------------------------------------------------------------------
-    rule <k> #setPrank NEWCALLER NEWORIGIN => . ... </k>
+    syntax KItem ::= "#setPrank" Int Account Bool [klabel(foundry_setPrank)]
+ // ------------------------------------------------------------------------
+    rule <k> #setPrank NEWCALLER NEWORIGIN SINGLEPRANK => . ... </k>
          <callDepth> CD </callDepth>
          <caller> CL </caller>
          <origin> OG </origin>
@@ -752,7 +784,7 @@ Utils
            <newOrigin> _ => NEWORIGIN </newOrigin>
            <active> false => true </active>
            <depth> _ => CD </depth>
-           <singleCall> _ => false </singleCall>
+           <singleCall> _ => SINGLEPRANK </singleCall>
          </prank>
 ```
 

kevm-pyk/src/kevm_pyk/solc_to_k.py

@@ -414,6 +414,7 @@ def _init_term(
                 KVariable('ACCOUNTS_INIT'),
             ]
         ),
+        'SINGLECALL_CELL': FALSE,
         'EXPECTEDREVERT_CELL': FALSE,
     }
 

tests/foundry/foundry.k.check.expected

@@ -2433,6 +2433,8 @@ module PLAINPRANKTEST-BIN-RUNTIME
 
     syntax PlainPrankTestMethod ::= "testFail_startPrank_existingAlready" "(" ")" [symbol(), klabel(method_PlainPrankTest_testFail_startPrank_existingAlready)]
 
+    syntax PlainPrankTestMethod ::= "test_prank_zeroAddress_true" "(" ")" [symbol(), klabel(method_PlainPrankTest_test_prank_zeroAddress_true)]
+    
     syntax PlainPrankTestMethod ::= "test_startPrankWithOrigin_true" "(" ")" [symbol(), klabel(method_PlainPrankTest_test_startPrankWithOrigin_true)]
 
     syntax PlainPrankTestMethod ::= "test_startPrank_true" "(" ")" [symbol(), klabel(method_PlainPrankTest_test_startPrank_true)]
@@ -2455,6 +2457,9 @@ module PLAINPRANKTEST-BIN-RUNTIME
     rule  ( PlainPrankTest . testFail_startPrank_existingAlready ( ) => #abiCallData ( "testFail_startPrank_existingAlready" , .TypedArgs ) )
 
 
+    rule  ( PlainPrankTest . test_prank_zeroAddress_true ( ) => #abiCallData ( "test_prank_zeroAddress_true" , .TypedArgs ) )
+      
+    
     rule  ( PlainPrankTest . test_startPrankWithOrigin_true ( ) => #abiCallData ( "test_startPrankWithOrigin_true" , .TypedArgs ) )
 
 
@@ -2482,6 +2487,9 @@ module PLAINPRANKTEST-BIN-RUNTIME
     rule  ( selector ( "testFail_startPrank_existingAlready" ) => 2262269573 )
 
 
+    rule  ( selector ( "test_prank_zeroAddress_true" ) => 3793950116 )
+      
+    
     rule  ( selector ( "test_startPrankWithOrigin_true" ) => 1559633499 )
 
 

tests/foundry/test/PlainPrankTest.t.sol

@@ -13,8 +13,8 @@ contract AdditionalToken {
     }
 
     function incrementCount() public {
-        require(msg.sender != owner);
-        count = count + 1;
+        if(msg.sender != owner)
+            count = count + 1;
     }
 }
 
@@ -56,4 +56,11 @@ contract PlainPrankTest is Test {
         vm.stopPrank();
     }
 
+    function test_prank_zeroAddress_true() public {
+        AdditionalToken token = new AdditionalToken();
+        vm.prank(address(0));
+        token.incrementCount();
+        token.incrementCount();
+        assert(token.count() == 1);
+    }
 }