External calls in CSE executions

[PetarMax]

When it comes to handling external function calls, the current CSE initial state is too general, leading to infeasible branches and even proof crashes. PR #355 introduces a simple contract whose only purpose is to test the handling of external calls:

contract IdentityContract {

    function identity(uint256 x) external pure returns (uint256) {
        return x;
    }

    function identity_wrapper(uint256 x) external returns (uint256) {
        return this.identity_wrapper(x);
    }
}

Executing identity_wrapper in CSE mode results in the following problems:

1. An infeasible branch on ID_CELL:Int #Equals 645326474426547203313410069153905908525362434349, since the address of the contract analysed cannot be the address of the Foundry cheatcodes. This can be fixed by having the disequality in the intiial CSE state.
2. An infeasible branch on true #Equals BAL:Int <Int 0, where BAL is an account balance. This can be fixed by having balances and other account parameters be within the appropriate bounds in the initial CSE state. This also means that the <accounts> cell should not be fully symbolic, but should expose the accounts that we know have to be present (e.g., the contract being executed).
3. A (presumably) infeasible branch on the contract analysed being precompiled. This can be fixed by having the disequality in the initial CSE state.
4. an infinite branching on #checkBalanceUnderflow caused by incompleteness of the associated rules, as brought up in this KEVM issue, which leads to a crash.

The associated kcfg and the bug report which includes all of the requests are attached below.

identity_wrapper.txt
id-wrapper-crash.tar.gz

[PetarMax]

We now have support for basic external function calls as part of #355. Problem 1 was resolved by adding the condition explicitly. The remaining problems disappeared with the addition of the contract being executed to <accounts>, as the add_invariant function of KEVM adds the appropriate constraints.

As an example, from the src/tests/integration/test-data/foundry folder of Kontrol, executing:

kontrol build --require src/cse/lemmas.k --module-import CSETest:CSE-LEMMAS --verbose --regen --rekompile               
kontrol prove --match-test 'Identity.identity'
kontrol prove --verbose --match-test 'Identity.applyOp' --include-summary 'Identity.identity' 

results in expected KCFGs and branchings. Specifically, the KCFG of Identity.identity is

┌─ 1 (root, init)
│   k: #execute ~> CONTINUATION:K
│   pc: 0
│   callDepth: CALLDEPTH_CELL:Int
│   statusCode: STATUSCODE:StatusCode
│   src: src/cse/ExternalFunctionCall.sol:8:18
│
│  (331 steps)
├─ 3 (terminal)
│   k: #halt ~> CONTINUATION:K
│   pc: 87
│   callDepth: CALLDEPTH_CELL:Int
│   statusCode: EVMC_SUCCESS
│   src: src/cse/ExternalFunctionCall.sol:15:16
│
┊  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

the KCFG for Identity.applyOp without CSE is

┌─ 1 (root, init)
│   k: #execute ~> CONTINUATION:K
│   pc: 0
│   callDepth: CALLDEPTH_CELL:Int
│   statusCode: STATUSCODE:StatusCode
│   src: src/cse/ExternalFunctionCall.sol:8:18
│
│  (367 steps)
├─ 3 (split)
│   k: #checkDepthExceeded ~> #checkNonceExceeded CONTRACT_ID:Int ~> #call CONTRACT_ID: ...
│   pc: 148
│   callDepth: CALLDEPTH_CELL:Int
│   statusCode: STATUSCODE:StatusCode
│   src: src/cse/ExternalFunctionCall.sol:14:17
┃
┃ (branch)
┣━━┓ constraint: { true #Equals CALLDEPTH_CELL:Int <Int 1024 }
┃  │
┃  ├─ 4
┃  │   k: #checkDepthExceeded ~> #checkNonceExceeded CONTRACT_ID:Int ~> #call CONTRACT_ID: ...
┃  │   pc: 148
┃  │   callDepth: CALLDEPTH_CELL:Int
┃  │   statusCode: STATUSCODE:StatusCode
┃  │   src: src/cse/ExternalFunctionCall.sol:14:17
┃  │
┃  │  (348 steps)
┃  ├─ 6
┃  │   k: #halt ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃  │   pc: 87
┃  │   callDepth: ( CALLDEPTH_CELL:Int +Int 1 )
┃  │   statusCode: EVMC_SUCCESS
┃  │   src: src/cse/ExternalFunctionCall.sol:15:16
┃  │
┃  │  (328 steps)
┃  ├─ 8 (terminal)
┃  │   k: #halt ~> CONTINUATION:K
┃  │   pc: 87
┃  │   callDepth: CALLDEPTH_CELL:Int
┃  │   statusCode: EVMC_SUCCESS
┃  │   src: src/cse/ExternalFunctionCall.sol:15:16
┃  │
┃  ┊  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: { true #Equals 1024 <=Int CALLDEPTH_CELL:Int }
   │
   ├─ 5
   │   k: #checkDepthExceeded ~> #checkNonceExceeded CONTRACT_ID:Int ~> #call CONTRACT_ID: ...
   │   pc: 148
   │   callDepth: CALLDEPTH_CELL:Int
   │   statusCode: STATUSCODE:StatusCode
   │   src: src/cse/ExternalFunctionCall.sol:14:17
   │
   │  (77 steps)
   ├─ 7 (terminal)
   │   k: #halt ~> CONTINUATION:K
   │   pc: 163
   │   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

and the KCFG for Identity.applyOp with CSE is

┌─ 1 (root, init)
│   k: #execute ~> CONTINUATION:K
│   pc: 0
│   callDepth: CALLDEPTH_CELL:Int
│   statusCode: STATUSCODE:StatusCode
│   src: src/cse/ExternalFunctionCall.sol:8:18
│
│  (367 steps)
├─ 3 (split)
│   k: #checkDepthExceeded ~> #checkNonceExceeded CONTRACT_ID:Int ~> #call CONTRACT_ID: ...
│   pc: 148
│   callDepth: CALLDEPTH_CELL:Int
│   statusCode: STATUSCODE:StatusCode
│   src: src/cse/ExternalFunctionCall.sol:14:17
┃
┃ (branch)
┣━━┓ constraint: { true #Equals CALLDEPTH_CELL:Int <Int 1024 }
┃  │
┃  ├─ 4
┃  │   k: #checkDepthExceeded ~> #checkNonceExceeded CONTRACT_ID:Int ~> #call CONTRACT_ID: ...
┃  │   pc: 148
┃  │   callDepth: CALLDEPTH_CELL:Int
┃  │   statusCode: STATUSCODE:StatusCode
┃  │   src: src/cse/ExternalFunctionCall.sol:14:17
┃  │
┃  │  (346 steps)
┃  ├─ 6 (terminal)
┃  │   k: #halt ~> CONTINUATION:K
┃  │   pc: 87
┃  │   callDepth: CALLDEPTH_CELL:Int
┃  │   statusCode: EVMC_SUCCESS
┃  │   src: src/cse/ExternalFunctionCall.sol:15:16
┃  │
┃  ┊  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: { true #Equals 1024 <=Int CALLDEPTH_CELL:Int }
   │
   ├─ 5
   │   k: #checkDepthExceeded ~> #checkNonceExceeded CONTRACT_ID:Int ~> #call CONTRACT_ID: ...
   │   pc: 148
   │   callDepth: CALLDEPTH_CELL:Int
   │   statusCode: STATUSCODE:StatusCode
   │   src: src/cse/ExternalFunctionCall.sol:14:17
   │
   │  (77 steps)
   ├─ 7 (terminal)
   │   k: #halt ~> CONTINUATION:K
   │   pc: 163
   │   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

and we can see that how the specification of Identity.identity is applied (the edges 4--6--8 become a single edge 4--6, saving 330 steps.

The branching on the call depth that is still present is expected.