CSE: assume cheatcodes' expected calldepth is less than the current one

Author: palinatolmach

src/kontrol/kdist/cheatcodes.md

@@ -581,21 +581,25 @@ WThe `#checkRevert` will be used to compare the status code of the execution and
          <callDepth> CD </callDepth>
          <wordStack> _ : _ : _ : _ : _ : RETSTART : RETWIDTH : _WS </wordStack>
          <expectedRevert>
-           <isRevertExpected> true </isRevertExpected>
-           <expectedDepth> CD </expectedDepth>
+           <isRevertExpected> ISREVERTEXPECTED_CELL </isRevertExpected>
+           <expectedDepth> EXPECTEDDEPTH_CELL </expectedDepth>
            ...
          </expectedRevert>
+         requires ISREVERTEXPECTED_CELL
+          andBool EXPECTEDDEPTH_CELL==Int CD
       [priority(32)]
 
     rule [foundry.set.expectrevert.2]:
          <k> #next [ _OP:CallSixOp ] ~> (.K => #checkRevert ~> #updateRevertOutput RETSTART RETWIDTH) ~> #execute ... </k>
          <callDepth> CD </callDepth>
          <wordStack> _ : _ : _ : _ : RETSTART : RETWIDTH : _WS </wordStack>
          <expectedRevert>
-           <isRevertExpected> true </isRevertExpected>
-           <expectedDepth> CD </expectedDepth>
+           <isRevertExpected> ISREVERTEXPECTED_CELL </isRevertExpected>
+           <expectedDepth> EXPECTEDDEPTH_CELL </expectedDepth>
            ...
          </expectedRevert>
+         requires ISREVERTEXPECTED_CELL
+          andBool EXPECTEDDEPTH_CELL==Int CD
       [priority(32)]
 
     rule [foundry.set.expectrevert.3]:
@@ -763,14 +767,16 @@ The last point is required in order to prevent overwriting the caller for subcal
          <wordStack> _ : ACCTTO : _WS </wordStack>
          <id> ACCT </id>
          <prank>
-           <active> true </active>
+           <active> ACTIVE_CELL </active>
            <newCaller> NCL </newCaller>
-           <depth> CD </depth>
+           <depth> ACTIVECALLDEPTH_CELL </depth>
            ...
          </prank>
       requires ACCT =/=K NCL
        andBool ACCTTO =/=K #address(FoundryCheat)
        andBool (OP ==K CALL orBool OP ==K CALLCODE orBool OP ==K STATICCALL orBool OP ==K CREATE orBool OP ==K CREATE2)
+       andBool ACTIVE_CELL
+       andBool ACTIVECALLDEPTH_CELL ==Int CD
       [priority(34)]
 ```
 

src/kontrol/prove.py

@@ -950,7 +950,7 @@ def _init_cterm(
         'TRACEDATA_CELL': KApply('.List'),
     }
 
-    storage_constraints: list[KApply] = []
+    cse_constraints: list[KApply] = []
 
     if config_type == ConfigType.TEST_CONFIG or active_simbolik:
         init_account_list = (
@@ -991,7 +991,7 @@ def _init_cterm(
             accounts.append(Foundry.symbolic_account(contract_account_name, contract_code))
         else:
             # Symbolic accounts of all relevant contracts
-            accounts, storage_constraints = _create_cse_accounts(
+            accounts, cse_constraints = _create_cse_accounts(
                 foundry, storage_fields, contract_account_name, contract_code
             )
 
@@ -1006,6 +1006,23 @@ def _init_cterm(
         if not isinstance(method, Contract.Constructor) and not (method.view or method.pure):
             init_subst['STATIC_CELL'] = FALSE
 
+        # Summarization applies to external calls, at least one level deeper than the test call where an `expectRevert` or `prank` is expected
+        expectrevert_depth_constraint = mlEqualsTrue(
+            KApply(
+                '_>Int_',
+                [KVariable('CALLDEPTH_CELL', sort=KSort('Int')), KVariable('EXPECTEDDEPTH_CELL', sort=KSort('Int'))],
+            )
+        )
+        prank_depth_constraint = mlEqualsTrue(
+            KApply(
+                '_>Int_', [KVariable('CALLDEPTH_CELL', sort=KSort('Int')), KVariable('DEPTH_CELL', sort=KSort('Int'))]
+            )
+        )
+        cse_constraints += [
+            expectrevert_depth_constraint,
+            prank_depth_constraint,
+        ]
+
     if calldata is not None:
         init_subst['CALLDATA_CELL'] = calldata
 
@@ -1030,7 +1047,7 @@ def _init_cterm(
     if preconditions is not None:
         for precondition in preconditions:
             init_cterm = init_cterm.add_constraint(mlEqualsTrue(precondition))
-    for constraint in storage_constraints:
+    for constraint in cse_constraints:
         init_cterm = init_cterm.add_constraint(constraint)
 
     non_cheatcode_contract_ids = []