Extending CSE support (#355)

* test for CSE function calls * Set Version: 0.1.152 * Set Version: 0.1.153 * further examples, tests, and lemmas * Set Version: 0.1.155 * Update dependency: deps/kevm_release (#364) * deps/kevm_release: Set Version 1.0.452 * Set Version: 0.1.155 * Sync Poetry files: kevm-pyk version 1.0.452 * flake.{nix,lock}: update Nix derivations * Sync Poetry files: kevm-pyk version 1.0.452 * Sync Poetry files: kevm-pyk version 1.0.452 * Sync Poetry files: kevm-pyk version 1.0.452 * Sync Poetry files: kevm-pyk version 1.0.452 * Sync Poetry files: kevm-pyk version 1.0.452 * Sync Poetry files: kevm-pyk version 1.0.452 --------- Co-authored-by: devops <[email protected]> * Set Version: 0.1.156 * Set Version: 0.1.158 * Set Version: 0.1.167 * refactoring, removing unneeded files * Set Version: 0.1.169 * Add `kontrol refute-node` and `kontrol unrefute-node` commands (#381) * Implement kontrol refute-node command * Implement kontrol unrefute-node command * Filter proof versions to exclude subproofs * Factor out foundry_refute_node and foundry_unrefute_node * Add test for foundry_refute_node * Add expected output for node refutation test * Set Version: 0.1.165 * Set Version: 0.1.169 --------- Co-authored-by: Lucas MT <[email protected]> Co-authored-by: devops <[email protected]> * Update dependency: deps/kevm_release (#392) * deps/kevm_release: Set Version 1.0.462 * Set Version: 0.1.169 * Sync Poetry files: kevm-pyk version 1.0.462 * flake.{nix,lock}: update Nix derivations * Set Version: 0.1.170 * flake.{nix,lock}: update Nix derivations * deps/kevm_release: Set Version 1.0.463 * Sync Poetry files: kevm-pyk version 1.0.463 * flake.{nix,lock}: update Nix derivations * Updated expected output --------- Co-authored-by: devops <[email protected]> Co-authored-by: Palina Tolmach <[email protected]> * Set Version: 0.1.171 * Set Version: 0.1.172 * path correction * redesigning CSE tests * slightly more general WETH contract * minor spacing consistencies * generalising test harness * Set Version: 0.1.174 * additional proof options for dependency tests * AddConst test * initialisation of accessedStorage * formatting * test correction * adding expected files, WETH9 contract * correction * removing accessStorage manipulation, adding full WETH9 * adding nocse kcfgs and updating cse ones * correction * Set Version: 0.1.175 * addresses not equal to cheatcode address * Set Version: 0.1.177 * deps/kevm_release: Set Version 1.0.465 * Sync Poetry files: kevm-pyk version 1.0.465 * flake.{nix,lock}: update Nix derivations * deps/kevm_release: Set Version 1.0.466 * Sync Poetry files: kevm-pyk version 1.0.466 * deps/k_release: sync release file version 6.3.17 * flake.{nix,lock}: update Nix derivations * kontrol/{solc_to_k,prove,foundry}: updates from upstream * src/tests/unit: update expected output * additional lemmas for discharging infeasible branches * Set Version: 0.1.178 * caller in accounts * :integration/test_kontrol_cse.py: init * updating expected outputs * Set Version: 0.1.180 * Generate xml report (#377) * generating a simple xml report * report with time for each test case * xml report generated from results of kontrol prove command * formatted failure text * Added flag to generate the report only if the --xml-test_report is provided * execution time in kontrol side * Set proof execution time * report with <error> tag for tests that end with exceptions * report is generated in function foundry_to_xml * Set Version: 0.1.162 * Formatting * Added file attribute to testcase * Set Version: 0.1.163 * Set Version: 0.1.164 * Printing exception trace in the report * Added CI test for the xml report feature * Fixed CI test * Add setup exectuion time to the testsuites * Fixed testsuites total execution time * Added one more assertion to CI test * Added property with kontrol version to xml report * Set Version: 0.1.165 * Set Version: 0.1.165 * undo changes to profiling test * Formatting * Fixed print failure info in xml report * Set Version: 0.1.179 * Set Version: 0.1.180 * Addressed PR comments --------- Co-authored-by: devops <[email protected]> Co-authored-by: Palina Tolmach <[email protected]> * Refactor get_test_id to fetch latest version (#406) * foundry.py: refactor get_test_id to fetch latest version * Set Version: 0.1.179 * add docstrings and unit test * test_foundry_list.py: revert changes * Set Version: 0.1.180 * foundry-list.expected: revert changes * test_get_test_id.py: add new unit tests * foundry.py: refactor get_test_id * test_get_test_id.py: update fixture and add new test case * test_get_test_id.py: refactor using monkeypatch * Set Version: 0.1.181 --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]> * Remove upper bound from pytest version (#408) * Remove upper bound from pytest version * Set Version: 0.1.180 * Set Version: 0.1.181 * Set Version: 0.1.182 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]> Co-authored-by: rv-jenkins <[email protected]> * Update dependency: deps/kevm_release (#410) * deps/kevm_release: Set Version 1.0.478 * Set Version: 0.1.180 * Sync Poetry files: kevm-pyk version 1.0.478 * flake.{nix,lock}: update Nix derivations * Set Version: 0.1.181 * deps/kevm_release: Set Version 1.0.479 * Sync Poetry files: kevm-pyk version 1.0.479 * flake.{nix,lock}: update Nix derivations * Set Version: 0.1.182 * deps/kevm_release: Set Version 1.0.480 * Sync Poetry files: kevm-pyk version 1.0.480 * flake.{nix,lock}: update Nix derivations * Set Version: 0.1.183 * deps/kevm_release: Set Version 1.0.481 * Sync Poetry files: kevm-pyk version 1.0.481 * flake.{nix,lock}: update Nix derivations * Update expected output (w/o `test_foundry_xml_report`) * deps/kevm_release: Set Version 1.0.482 * Sync Poetry files: kevm-pyk version 1.0.482 * deps/k_release: sync release file version 6.3.25 * flake.{nix,lock}: update Nix derivations * Reinit proofs in `test_foundry_xml_report` * Updated expected output w/new exec time format, `terminal` node label --------- Co-authored-by: devops <[email protected]> Co-authored-by: Palina Tolmach <[email protected]> * Set Version: 0.1.184 * simplifying lemams and adding them to CI * Set Version: 0.1.185 * test_kontrol_cse.py: move dependency test from test_foundry_prove * Set Version: 0.1.188 * test_kontrol_cse.py: refactor test harness * Set Version: 0.1.192 * Update dependency: deps/kevm_release (#419) * deps/kevm_release: Set Version 1.0.485 * Set Version: 0.1.188 * Sync Poetry files: kevm-pyk version 1.0.485 * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: devops <[email protected]> * skipping tests * correction * correction: caller in accounts * Set Version: 0.1.193 * Set Version: 0.1.194 * removing cbor and hash disabling * updating expected output * manual correction of expected output * adding appropriate expected outputs * attempting to manually fix expected output * Set Version: 0.1.195 * adding a CSE CI runner, removing no-cse executions * removing no-cse.expected files * updating expected outputs * Set Version: 0.1.197 * Set Version: 0.1.197 * name correction for CI job * Update src/tests/integration/test-data/foundry-dependency-all Co-authored-by: Andrei Văcaru <[email protected]> * Update src/tests/integration/test-data/foundry-dependency-skip Co-authored-by: Andrei Văcaru <[email protected]> * removing unused code * bringing back execution without CSE for testing purposes * Set Version: 0.1.200 * adding expected output for no-cse tests * Set Version: 0.1.202 * Set Version: 0.1.204 * updating expected outputs, correcting non-cse executions * removing no-cse and updating expected outputs * Updating the running of proofs * Set Version: 0.1.205 * adding a skipped test in init tests due to a run-constructor error --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]> Co-authored-by: lucasmt <[email protected]> Co-authored-by: Lucas MT <[email protected]> Co-authored-by: Palina Tolmach <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> Co-authored-by: Andrei <[email protected]> Co-authored-by: Lisandra <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]> Co-authored-by: Tamás Tóth <[email protected]>
runtimeverification · Mar 15, 2024 · 8c41d6f · 8c41d6f
1 parent 3af182c
commit 8c41d6f
Show file tree

Hide file tree

Showing 30 changed files with 3,225 additions and 5,199 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,4 @@
+.DS_Store
 /dist/
 __pycache__/
 .coverage

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.204
+0.1.205
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.204"
+version = "0.1.205"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.204'
+VERSION: Final = '0.1.205'
diff --git a/src/tests/integration/test-data/cse-lemmas.k b/src/tests/integration/test-data/cse-lemmas.k
@@ -9,6 +9,22 @@ module CSE-LEMMAS
     imports MAP-SYMBOLIC
     imports SET-SYMBOLIC
 
+    // xor in terms of -Int
+    rule X xorInt maxUInt256 => maxUInt256 -Int X
+      requires #rangeUInt ( 256 , X )
+      [simplification]
+
+    // for-loop chop
+    rule chop ( ( X:Int +Int Y:Int ) ) ==Int 0 => X ==Int pow256 -Int (Y modInt pow256)
+      requires #rangeUInt(256, X) andBool 0 <=Int Y
+      [simplification, concrete(Y)]
+
+    // Set equality needed for discharging `#Not ( #Exists ( ... )` on `<accessedAccounts>` unification
+    rule { S1:Set #Equals S2:Set |Set SetItem ( X ) } =>
+         { X in S1 } #And
+         ( { S2 #Equals S1 } #Or { S2 #Equals S1 -Set SetItem ( X ) } )
+         [simplification]
+
     // Non-equality of byte arrays
     rule { B1:Bytes #Equals B2:Bytes } => #Bottom
       requires notBool ( lengthBytes(B1) ==Int lengthBytes(B2) )

diff --git a/src/tests/integration/test-data/foundry-dependency-all b/src/tests/integration/test-data/foundry-dependency-all
@@ -1,3 +1,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)
+CSETest.test_add_const(uint256,uint256)
+CSETest.test_identity(uint256,uint256)
+Identity.applyOp(uint256)
+Identity.identity(uint256)
diff --git a/src/tests/integration/test-data/foundry-dependency-skip b/src/tests/integration/test-data/foundry-dependency-skip
@@ -0,0 +1,2 @@
+CSETest.test_add_const(uint256,uint256)
+CSETest.test_identity(uint256,uint256)
diff --git a/src/tests/integration/test-data/foundry-init-code-skip b/src/tests/integration/test-data/foundry-init-code-skip
@@ -0,0 +1 @@
+ConstructorTest.run_constructor()
diff --git a/src/tests/integration/test-data/foundry/src/cse/Binary.sol b/src/tests/integration/test-data/foundry/src/cse/Binary.sol
@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+import { UIntBinaryOp } from "./OperatorInterfaces.sol";
+import { Identity } from "./Unary.sol";
+
+// CSE challenge: storage variable of a contract type
+// CSE challenge: cross-contract external function call
+contract Add is UIntBinaryOp {
+    Identity id;
+
+    function applyOp(uint256 x, uint256 y) external view returns (uint256 result) {
+      return id.applyOp(x) + id.applyOp(y);
+    }
+
+}
+
+// CSE challenge: storage variable of a contract type
+// CSE challenge: cross-contract external function call
+contract Sub is UIntBinaryOp {
+    Identity id;
+
+    function applyOp(uint256 x, uint256 y) external view returns (uint256 result) {
+      return id.applyOp(x) - id.applyOp(y);
+    }
+}
+
+// CSE challenge: storage variable of a contract type
+// CSE challenge: cross-contract external function call
+// CSE challenge: bounded reasoning
+contract Multiply is UIntBinaryOp {
+    Add adder;
+
+    function applyOp(uint256 x, uint256 y) external view returns (uint256 result) {
+      for (result = 0; y > 0; y--) {
+        result = adder.applyOp(result, x);
+      }
+    }
+}
diff --git a/src/tests/integration/test-data/foundry/src/cse/OperatorInterfaces.sol b/src/tests/integration/test-data/foundry/src/cse/OperatorInterfaces.sol
@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+interface UIntUnaryOp {
+  function applyOp(uint256 x) external view returns (uint256);
+}
+
+interface UIntBinaryOp {
+  function applyOp(uint256 x, uint256 y) external view returns (uint256 result);
+}
diff --git a/src/tests/integration/test-data/foundry/src/cse/Unary.sol b/src/tests/integration/test-data/foundry/src/cse/Unary.sol
@@ -0,0 +1,42 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+import { UIntUnaryOp } from "./OperatorInterfaces.sol";
+
+// CSE challenge: external function call
+contract Identity is UIntUnaryOp {
+
+    function identity(uint256 x) external pure returns (uint256) {
+        return x;
+    }
+
+    function applyOp(uint256 x) external view returns (uint256) {
+        return this.identity(x);
+    }
+}
+
+// CSE challenge: storage variable of a basic type
+contract AddConst is UIntUnaryOp {
+    uint256 c;
+
+    function setConst(uint256 x) external {
+        c = x;
+    }
+
+    function applyOp(uint256 x) external view returns (uint256) {
+        return x + c;
+    }
+}
+
+// CSE challenge: storage variable of an interface type
+//                this is higher-order and not possible in general
+//                one way of handling this is instantiating the `UIntUnaryOp`
+//                interface with specific contracts that implement it
+// CSE challenge: cross-contract external function call
+contract Iterate is UIntUnaryOp {
+    UIntUnaryOp f;
+
+    function applyOp(uint256 x) external view returns (uint256) {
+        return f.applyOp((f.applyOp(x)));
+    }
+}
diff --git a/src/tests/integration/test-data/foundry/src/cse/WETH9.sol b/src/tests/integration/test-data/foundry/src/cse/WETH9.sol
@@ -0,0 +1,66 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+// CSE challenge: initialised contract variables
+// CSE challenge: global variables
+// CSE challenge: mappings in storage
+
+contract WETH9 {
+    string public name = "Wrapped Ether";
+    string public symbol = "WETH";
+    uint8 public decimals = 18;
+
+    event Approval(address indexed src, address indexed guy, uint256 wad);
+    event Transfer(address indexed src, address indexed dst, uint256 wad);
+    event Deposit(address indexed dst, uint256 wad);
+    event Withdrawal(address indexed src, uint256 wad);
+
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    fallback() external payable {
+        deposit();
+    }
+
+    function deposit() public payable {
+        balanceOf[msg.sender] += msg.value;
+        emit Deposit(msg.sender, msg.value);
+    }
+
+    function withdraw(uint256 wad) public {
+        require(balanceOf[msg.sender] >= wad);
+        balanceOf[msg.sender] -= wad;
+        payable(msg.sender).transfer(wad);
+        emit Withdrawal(msg.sender, wad);
+    }
+
+    function totalSupply() public view returns (uint256) {
+        return address(this).balance;
+    }
+
+    function approve(address guy, uint256 wad) public returns (bool) {
+        allowance[msg.sender][guy] = wad;
+        emit Approval(msg.sender, guy, wad);
+        return true;
+    }
+
+    function transfer(address dst, uint256 wad) public returns (bool) {
+        return transferFrom(msg.sender, dst, wad);
+    }
+
+    function transferFrom(address src, address dst, uint256 wad) public returns (bool) {
+        require(balanceOf[src] >= wad);
+
+        if (src != msg.sender && allowance[src][msg.sender] != type(uint256).max) {
+            require(allowance[src][msg.sender] >= wad);
+            allowance[src][msg.sender] -= wad;
+        }
+
+        balanceOf[src] -= wad;
+        balanceOf[dst] += wad;
+
+        emit Transfer(src, dst, wad);
+
+        return true;
+    }
+}
diff --git a/src/tests/integration/test-data/foundry/test/CSE.t.sol b/src/tests/integration/test-data/foundry/test/CSE.t.sol
@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+import "forge-std/Test.sol";
+
+import "src/cse/Unary.sol";
+import "src/cse/Binary.sol";
+import "src/cse/WETH9.sol";
+
+contract CSETest is Test {
+    Identity i;
+    AddConst c;
+    Multiply m;
+
+    function setUp() external {
+        i = new Identity();
+        c = new AddConst();
+        m = new Multiply();
+    }
+
+    // CSE challenge: External function call
+    function test_identity(uint256 x, uint256 y) external view {
+        vm.assume(x < 2 ** 64 && y < 2 ** 64);
+        uint256 z = i.applyOp(x) + i.applyOp(y) + i.applyOp(y);
+        assert(z == x + 2 * y);
+    }
+
+    function test_add_const(uint256 x, uint256 y) external {
+        vm.assume(x < 2 ** 64 && y < 2 ** 64);
+        c.setConst(x);
+        uint256 z = c.applyOp(y);
+        assert(z == x + y);
+    }
+}
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
@@ -0,0 +1,63 @@
+
+┌─ 1 (root, init)
+│   k: #execute ~> CONTINUATION:K
+│   pc: 0
+│   callDepth: CALLDEPTH_CELL:Int
+│   statusCode: STATUSCODE:StatusCode
+│
+│  (324 steps)
+├─ 3 (split)
+│   k: JUMPI 180 bool2Word ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTR ...
+│   pc: 158
+│   callDepth: CALLDEPTH_CELL:Int
+│   statusCode: STATUSCODE:StatusCode
+┃
+┃ (branch)
+┣━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+┃  │
+┃  ├─ 4
+┃  │   k: JUMPI 180 bool2Word ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTR ...
+┃  │   pc: 158
+┃  │   callDepth: CALLDEPTH_CELL:Int
+┃  │   statusCode: STATUSCODE:StatusCode
+┃  │
+┃  │  (122 steps)
+┃  ├─ 6 (terminal)
+┃  │   k: #halt ~> CONTINUATION:K
+┃  │   pc: 87
+┃  │   callDepth: CALLDEPTH_CELL:Int
+┃  │   statusCode: EVMC_SUCCESS
+┃  │
+┃  ┊  constraint: OMITTED CONSTRAINT
+┃  ┊  subst: OMITTED SUBST
+┃  └─ 2 (leaf, target, terminal)
+┃      k: #halt ~> CONTINUATION:K
+┃      pc: PC_CELL_5d410f2a:Int
+┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
+┃      statusCode: STATUSCODE_FINAL:StatusCode
+┃
+┗━━┓ constraint: ( notBool VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) )
+   │
+   ├─ 5
+   │   k: JUMPI 180 bool2Word ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTR ...
+   │   pc: 158
+   │   callDepth: CALLDEPTH_CELL:Int
+   │   statusCode: STATUSCODE:StatusCode
+   │
+   │  (47 steps)
+   ├─ 7 (terminal)
+   │   k: #halt ~> CONTINUATION:K
+   │   pc: 179
+   │   callDepth: CALLDEPTH_CELL:Int
+   │   statusCode: EVMC_REVERT
+   │
+   ┊  constraint: OMITTED CONSTRAINT
+   ┊  subst: OMITTED SUBST
+   └─ 2 (leaf, target, terminal)
+       k: #halt ~> CONTINUATION:K
+       pc: PC_CELL_5d410f2a:Int
+       callDepth: CALLDEPTH_CELL_5d410f2a:Int
+       statusCode: STATUSCODE_FINAL:StatusCode
+
+
+
diff --git a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).no-cse.expected b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).no-cse.expected
@@ -0,0 +1,63 @@
+
+┌─ 1 (root, init)
+│   k: #execute ~> CONTINUATION:K
+│   pc: 0
+│   callDepth: CALLDEPTH_CELL:Int
+│   statusCode: STATUSCODE:StatusCode
+│
+│  (324 steps)
+├─ 3 (split)
+│   k: JUMPI 180 bool2Word ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTR ...
+│   pc: 158
+│   callDepth: CALLDEPTH_CELL:Int
+│   statusCode: STATUSCODE:StatusCode
+┃
+┃ (branch)
+┣━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+┃  │
+┃  ├─ 4
+┃  │   k: JUMPI 180 bool2Word ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTR ...
+┃  │   pc: 158
+┃  │   callDepth: CALLDEPTH_CELL:Int
+┃  │   statusCode: STATUSCODE:StatusCode
+┃  │
+┃  │  (122 steps)
+┃  ├─ 6 (terminal)
+┃  │   k: #halt ~> CONTINUATION:K
+┃  │   pc: 87
+┃  │   callDepth: CALLDEPTH_CELL:Int
+┃  │   statusCode: EVMC_SUCCESS
+┃  │
+┃  ┊  constraint: OMITTED CONSTRAINT
+┃  ┊  subst: OMITTED SUBST
+┃  └─ 2 (leaf, target, terminal)
+┃      k: #halt ~> CONTINUATION:K
+┃      pc: PC_CELL_5d410f2a:Int
+┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
+┃      statusCode: STATUSCODE_FINAL:StatusCode
+┃
+┗━━┓ constraint: ( notBool VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) )
+   │
+   ├─ 5
+   │   k: JUMPI 180 bool2Word ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTR ...
+   │   pc: 158
+   │   callDepth: CALLDEPTH_CELL:Int
+   │   statusCode: STATUSCODE:StatusCode
+   │
+   │  (47 steps)
+   ├─ 7 (terminal)
+   │   k: #halt ~> CONTINUATION:K
+   │   pc: 179
+   │   callDepth: CALLDEPTH_CELL:Int
+   │   statusCode: EVMC_REVERT
+   │
+   ┊  constraint: OMITTED CONSTRAINT
+   ┊  subst: OMITTED SUBST
+   └─ 2 (leaf, target, terminal)
+       k: #halt ~> CONTINUATION:K
+       pc: PC_CELL_5d410f2a:Int
+       callDepth: CALLDEPTH_CELL_5d410f2a:Int
+       statusCode: STATUSCODE_FINAL:StatusCode
+
+
+
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		CSETest.test_add_const(uint256,uint256)
		CSETest.test_identity(uint256,uint256)