Experimental: update cheatcode preconditions in CSE

deps/k_release

@@ -1 +1 @@
-7.1.286
+7.1.286

src/kontrol/prove.py

@@ -966,6 +966,7 @@ def _init_cterm(
         'CALLER_CELL': KVariable('CALLER_ID', sort=KSort('Int')),
         'LOCALMEM_CELL': bytesToken(b''),
         'ACTIVE_CELL': FALSE,
+        'DEPTH_CELL': intToken(0),
         'MEMORYUSED_CELL': intToken(0),
         'WORDSTACK_CELL': KApply('.WordStack_EVM-TYPES_WordStack'),
         'PC_CELL': intToken(0),
@@ -975,6 +976,7 @@ def _init_cterm(
         'ISREVERTEXPECTED_CELL': FALSE,
         'ISOPCODEEXPECTED_CELL': FALSE,
         'RECORDEVENT_CELL': FALSE,
+        'EXPECTEDDEPTH_CELL': intToken(0),
         'ISEVENTEXPECTED_CELL': FALSE,
         'ISCALLWHITELISTACTIVE_CELL': FALSE,
         'ISSTORAGEWHITELISTACTIVE_CELL': FALSE,
@@ -984,7 +986,7 @@ def _init_cterm(
         'MOCKFUNCTIONS_CELL': KApply('.MockFunctionCellMap'),
     }
 
-    storage_constraints: list[KApply] = []
+    cse_constraints: list[KApply] = []
 
     if config_type == ConfigType.TEST_CONFIG or active_simbolik:
         init_account_list = (
@@ -1026,7 +1028,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
             )
 
@@ -1041,6 +1043,50 @@ def _init_cterm(
         if not isinstance(method, Contract.Constructor) and not (method.view or method.pure):
             init_subst['STATIC_CELL'] = FALSE
 
+        # TODO:
+        # andBool notBool (ACTIVE_CELL orBool PRAKNDEPTH_CELL >=Int CALLDEPTH_CELL)
+        # andBool notBool (EXPECTED_REVERT_CELL orBool REVERTDEPTH_CELL >=Int CALLDEPTH_CELL)
+
+        # Assume we're not in an active prank context
+        inactive_prank_constraint = mlEqualsTrue(
+            notBool(
+                KApply(
+                    '_orBool_',
+                    [
+                        KVariable('ACTIVE_CELL', sort=KSort('Bool')),
+                        KApply(
+                            '_>=Int_',
+                            [
+                                KVariable('DEPTH_CELL', sort=KSort('Int')),
+                                KVariable('CALLDEPTH_CELL', sort=KSort('Int')),
+                            ],
+                        ),
+                    ],
+                )
+            )
+        )
+        inactive_expect_revert_constraint = mlEqualsTrue(
+            notBool(
+                KApply(
+                    '_orBool_',
+                    [
+                        KVariable('ISREVERTEXPECTED_CELL', sort=KSort('Bool')),
+                        KApply(
+                            '_>=Int_',
+                            [
+                                KVariable('EXPECTEDDEPTH_CELL', sort=KSort('Int')),
+                                KVariable('CALLDEPTH_CELL', sort=KSort('Int')),
+                            ],
+                        ),
+                    ],
+                )
+            )
+        )
+        cse_constraints += [
+            inactive_prank_constraint,
+            inactive_expect_revert_constraint,
+        ]
+
     if calldata is not None:
         init_subst['CALLDATA_CELL'] = calldata
 
@@ -1065,7 +1111,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 = []

src/tests/integration/test-data/foundry-dependency-all

@@ -2,6 +2,8 @@ AddConst.applyOp(uint256)
 ArithmeticCallTest.test_double_add(uint256,uint256)
 ArithmeticCallTest.test_double_add_double_sub(uint256,uint256)
 ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256)
+ArithmeticCallTest.test_double_add_sub_external_revert(uint256,uint256,uint256)
+ArithmeticCallTest.test_double_add_sub_external_prank(uint256,uint256,uint256)
 ArithmeticContract.add(uint256,uint256)
 ArithmeticContract.add_sub_external(uint256,uint256,uint256)
 CallableStorageContract.str()

src/tests/integration/test-data/foundry/test/ArithmeticCall.t.sol

@@ -30,4 +30,22 @@ contract ArithmeticCallTest is Test {
         a = arith.add_sub_external(a, y, z);
         assert(a > x);
     }
+
+    function test_double_add_sub_external_revert(uint x, uint y, uint z) external {
+        vm.assume(x == type(uint256).max);
+        vm.assume(y > 0);
+
+        // the call should revert due to overflow in `add`
+        vm.expectRevert(); 
+        uint a = arith.add_sub_external(x, y, z);
+        assert(a > x);
+    }
+
+    function test_double_add_sub_external_prank(uint x, uint y, uint z) external {
+        address prankCaller = address(0xBEEF);
+
+        vm.prank(prankCaller);
+        uint a = arith.add_sub_external(x, y, z);
+        assert(a > x);
+    }
 }

src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected

@@ -126,6 +126,9 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                    <callGas>
                      0
                    </callGas>
+                   <callDepth>
+                     CALLDEPTH_CELL:Int
+                   </callDepth>
                    <codeAddr>
                      C_ADDCONST_ID:Int
                    </codeAddr>
@@ -182,6 +185,24 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
              true
            </stackChecks>
            <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <depth>
+                 0
+               </depth>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               <expectedDepth>
+                 0
+               </expectedDepth>
+               ...
+             </expectedRevert>
              <expectedOpcode>
                <isOpcodeExpected>
                  false
@@ -211,7 +232,9 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
              ...
            </cheatcodes>
          </foundry>
-      requires ( 0 <=Int KV0_x:Int
+      requires ( ( notBool _ACTIVE_CELL:Bool )
+       andBool ( ( notBool _ISREVERTEXPECTED_CELL:Bool )
+       andBool ( 0 <=Int KV0_x:Int
        andBool ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
        andBool ( 0 <=Int C_ADDCONST_ID:Int
@@ -221,6 +244,8 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
        andBool ( NUMBER_CELL:Int <Int pow32
        andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
        andBool ( TIMESTAMP_CELL:Int <Int 34359738368
+       andBool ( _DEPTH_CELL:Int <Int CALLDEPTH_CELL:Int
+       andBool ( _EXPECTEDDEPTH_CELL:Int <Int CALLDEPTH_CELL:Int
        andBool ( C_ADDCONST_NONCE:Int <Int maxUInt64
        andBool ( CALLER_ID:Int =/=Int #address ( FoundryCheat )
        andBool ( ORIGIN_ID:Int =/=Int #address ( FoundryCheat )
@@ -243,7 +268,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
           orBool ( 10 <Int C_ADDCONST_ID:Int
                  ))
        andBool ( KV0_x:Int <=Int ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) )
-               ))))))))))))))))))))))))
+               ))))))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-8-TO-6)]
 
     rule [BASIC-BLOCK-9-TO-7]: <foundry>
@@ -294,6 +319,9 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                    <callGas>
                      0
                    </callGas>
+                   <callDepth>
+                     CALLDEPTH_CELL:Int
+                   </callDepth>
                    <codeAddr>
                      C_ADDCONST_ID:Int
                    </codeAddr>
@@ -350,6 +378,24 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
              true
            </stackChecks>
            <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <depth>
+                 0
+               </depth>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               <expectedDepth>
+                 0
+               </expectedDepth>
+               ...
+             </expectedRevert>
              <expectedOpcode>
                <isOpcodeExpected>
                  false
@@ -379,7 +425,9 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
              ...
            </cheatcodes>
          </foundry>
-      requires ( 0 <=Int KV0_x:Int
+      requires ( ( notBool _ACTIVE_CELL:Bool )
+       andBool ( ( notBool _ISREVERTEXPECTED_CELL:Bool )
+       andBool ( 0 <=Int KV0_x:Int
        andBool ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
        andBool ( 0 <=Int C_ADDCONST_ID:Int
@@ -389,6 +437,8 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
        andBool ( NUMBER_CELL:Int <Int pow32
        andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
        andBool ( TIMESTAMP_CELL:Int <Int 34359738368
+       andBool ( _DEPTH_CELL:Int <Int CALLDEPTH_CELL:Int
+       andBool ( _EXPECTEDDEPTH_CELL:Int <Int CALLDEPTH_CELL:Int
        andBool ( C_ADDCONST_NONCE:Int <Int maxUInt64
        andBool ( CALLER_ID:Int =/=Int #address ( FoundryCheat )
        andBool ( ORIGIN_ID:Int =/=Int #address ( FoundryCheat )
@@ -411,7 +461,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
           orBool ( 10 <Int C_ADDCONST_ID:Int
                  ))
        andBool ( ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) <Int KV0_x:Int
-               ))))))))))))))))))))))))
+               ))))))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-9-TO-7)]
 
 endmodule