Extending CSE support

.gitignore

@@ -1,3 +1,4 @@
+.DS_Store
 /dist/
 __pycache__/
 .coverage

package/version

@@ -1 +1 @@
-0.1.204
+0.1.205

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]>",

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'

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) )

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)

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

@@ -0,0 +1,2 @@
+CSETest.test_add_const(uint256,uint256)
+CSETest.test_identity(uint256,uint256)

src/tests/integration/test-data/foundry-init-code-skip

@@ -0,0 +1 @@
+ConstructorTest.run_constructor()

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);
+      }
+    }
+}

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);
+}

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)));
+    }
+}

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;
+    }
+}

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);
+    }
+}

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
+
+
+

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
+
+
+