Extending CSE support

package/version

@@ -1 +1 @@
-0.1.173
+0.1.174

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.173"
+version = "0.1.174"
 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.173'
+VERSION: Final = '0.1.174'

src/kontrol/foundry.py

@@ -336,6 +336,14 @@ def loc_FOUNDRY_FAILED() -> KApply:  # noqa: N802
             )
         )
 
+    @staticmethod
+    def symbolic_contract_prefix() -> str:
+        return 'CONTRACT'
+
+    @staticmethod
+    def symbolic_contract_id() -> str:
+        return Foundry.symbolic_contract_prefix() + '_ID'
+
     @staticmethod
     def address_TEST_CONTRACT() -> KToken:  # noqa: N802
         return intToken(0x7FA9385BE102AC3EAC297483DD6233D62B3E1496)
@@ -357,6 +365,17 @@ def account_CHEATCODE_ADDRESS(store_var: KInner) -> KApply:  # noqa: N802
             intToken(0),
         )
 
+    @staticmethod
+    def symbolic_account(prefix: str, program: KInner, storage: KInner | None = None) -> KApply:
+        return KEVM.account_cell(
+            KVariable(prefix + '_ID', sort=KSort('Int')),
+            KVariable(prefix + '_BAL', sort=KSort('Int')),
+            program,
+            storage if storage is not None else KVariable(prefix + '_STORAGE', sort=KSort('Map')),
+            KVariable(prefix + '_ORIGSTORAGE', sort=KSort('Map')),
+            KVariable(prefix + '_NONCE', sort=KSort('Int')),
+        )
+
     @staticmethod
     def help_info() -> list[str]:
         res_lines: list[str] = []

src/kontrol/prove.py

@@ -16,7 +16,7 @@
 from pyk.prelude.k import GENERATED_TOP_CELL
 from pyk.prelude.kbool import FALSE, TRUE, notBool
 from pyk.prelude.kint import intToken
-from pyk.prelude.ml import mlEqualsTrue
+from pyk.prelude.ml import mlEqualsFalse, mlEqualsTrue
 from pyk.prelude.string import stringToken
 from pyk.proof.proof import Proof
 from pyk.proof.reachability import APRProof
@@ -572,6 +572,7 @@ def _init_cterm(
         'STATUSCODE_CELL': KVariable('STATUSCODE'),
         'PROGRAM_CELL': program,
         'JUMPDESTS_CELL': KEVM.compute_valid_jumpdests(program),
+        'ID_CELL': KVariable(Foundry.symbolic_contract_id(), sort=KSort('Int')),
         'ORIGIN_CELL': KVariable('ORIGIN_ID', sort=KSort('Int')),
         'CALLER_CELL': KVariable('CALLER_ID', sort=KSort('Int')),
         'LOCALMEM_CELL': bytesToken(b''),
@@ -609,6 +610,17 @@ def _init_cterm(
             'ACCOUNTS_CELL': KEVM.accounts(init_account_list),
         }
         init_subst.update(init_subst_test)
+    else:
+        # Symbolic accounts of all relevant contracts
+        # Status: Currently, only the executing contract
+        # TODO: Add all other accounts belonging to relevant contracts
+        accounts: list[KInner] = [
+            Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), program),
+            KVariable('ACCOUNTS_REST', sort=KSort('AccountCellMap')),
+        ]
+
+        init_subst_accounts = {'ACCOUNTS_CELL': KEVM.accounts(accounts)}
+        init_subst.update(init_subst_accounts)
 
     if calldata is not None:
         init_subst['CALLDATA_CELL'] = calldata
@@ -623,6 +635,14 @@ def _init_cterm(
 
     init_term = Subst(init_subst)(empty_config)
     init_cterm = CTerm.from_kast(init_term)
+    # The address of the executing contract is always guaranteed not to be the address of the cheatcode contract
+    init_cterm = init_cterm.add_constraint(
+        mlEqualsFalse(
+            KApply(
+                '_==Int_', [KVariable(Foundry.symbolic_contract_id(), sort=KSort('Int')), Foundry.address_CHEATCODE()]
+            )
+        )
+    )
     init_cterm = KEVM.add_invariant(init_cterm)
 
     return init_cterm

src/tests/integration/test-data/foundry/foundry.toml

@@ -4,4 +4,8 @@ out = 'out'
 test = 'test'
 extra_output = ['storageLayout', 'abi', 'evm.methodIdentifiers', 'evm.deployedBytecode.object', 'devdoc']
 rpc_endpoints = { optimism = "https://optimism.alchemyapi.io/v2/...", mainnet = "${RPC_MAINNET}" }
+
+bytecode_hash = "none"
+cbor_metadata = false
+
 ast = true

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/src/cse/lemmas.k

@@ -0,0 +1,33 @@
+requires "evm.md"
+requires "foundry.md"
+
+module CSE-LEMMAS
+    imports BOOL
+    imports FOUNDRY
+    imports INFINITE-GAS
+    imports INT-SYMBOLIC
+    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]
+
+endmodule
+
+module CSE-LEMMAS-SPEC
+    imports CSE-LEMMAS
+
+endmodule

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