CSE: Include symbolic contracts corresponding to contract fields into accounts

package/version

@@ -1 +1 @@
-0.1.310
+0.1.311

pyproject.toml

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

src/tests/integration/test-data/cse-lemmas.k

@@ -31,7 +31,7 @@ module CSE-LEMMAS
       [simplification]
 
     // Function selector does not match
-    rule { B:Bytes #Equals B1:Bytes +Bytes B2:Bytes } => #Bottom
+    rule { B:Bytes #Equals B1:Bytes +Bytes _:Bytes } => #Bottom
       requires #range(B, 0, 4) =/=K #range (B1, 0, 4)
       [simplification(60), concrete(B, B1)]
 
@@ -40,6 +40,20 @@ module CSE-LEMMAS
       requires 4 <=Int lengthBytes(B) andBool #range(B, 0, 4) ==K B1
       [simplification(60), concrete(B, B1)]
 
+    // Bitwise inequalities
+    rule [bitwise-and-maxUInt-lt-l]:
+      A <Int X &Int Y => false
+      requires 0 <=Int X andBool 0 <=Int Y
+       andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+       andBool X +Int 1 <=Int A
+       [concrete(X), simplification, preserves-definedness]
+
+    rule [bitwise-and-maxUInt-le-r]:
+      X &Int Y <=Int A => true
+      requires 0 <=Int X andBool 0 <=Int Y
+       andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+       andBool X +Int 1 <=Int A
+       [concrete(X), simplification, preserves-definedness]
 
 endmodule
 

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

@@ -7,6 +7,7 @@ ArithmeticContract.add_sub_external(uint256,uint256,uint256)
 CSETest.test_add_const(uint256,uint256)
 CSETest.test_identity(uint256,uint256)
 ConstructorTest.test_contract_call()
+ContractFieldTest.testEscrowToken()
 Identity.applyOp(uint256)
 Identity.identity(uint256)
 ImportedContract.set(uint256)

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

@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+import {Test} from "forge-std/Test.sol";
+
+contract TToken {
+    uint128 private totalSupply;
+
+    constructor(uint128 _totalSupply) {
+        totalSupply = _totalSupply;
+    }
+
+    function getTotalSupply() public returns (uint256) {
+      return 32 + uint256(totalSupply);
+    }
+}
+
+contract TEscrow {
+    TToken token;
+
+    constructor(address _token) {
+        token = TToken(_token);
+    }
+
+    function getTokenTotalSupply() public returns (uint256) {
+        return token.getTotalSupply() + 13;
+    }
+}
+
+contract ContractFieldTest is Test {
+    TToken token;
+    TEscrow escrow;
+
+    function setUp() public {
+        token = new TToken(12300);
+        escrow = new TEscrow(address(token));
+    }
+
+    /* Calling `getTokenTotalSupply` will summarize `totalSupply` and
+       include `TestToken token` into the list of accounts in `getTokenTotalSupply`'s summary
+    */
+    function testEscrowToken() public {
+        assert(escrow.getTokenTotalSupply() == 12345);
+    }
+}

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

@@ -6,7 +6,7 @@
 │   statusCode: STATUSCODE:StatusCode
 ┃
 ┃ (branch)
-┣━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) )
+┣━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
 ┃  │
 ┃  ├─ 8
 ┃  │   k: #execute ~> CONTINUATION:K
@@ -29,7 +29,7 @@
 ┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
 ┃
-┗━━┓ constraint: ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) <Int VV0_x_114b9705:Int
+┗━━┓ constraint: ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) <Int VV0_x_114b9705:Int
    │
    ├─ 9
    │   k: #execute ~> CONTINUATION:K
@@ -76,7 +76,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
              <ethereum>
                <evm>
                  <output>
-                   ( _OUTPUT_CELL => #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) ) )
+                   ( _OUTPUT_CELL => #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) )
                  </output>
                  <statusCode>
                    ( _STATUSCODE => EVMC_SUCCESS )
@@ -98,7 +98,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                      ( .WordStack => ( selector ( "applyOp(uint256)" ) : .WordStack ) )
                    </wordStack>
                    <localMem>
-                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) ) )
+                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) )
                    </localMem>
                    <memoryUsed>
                      0
@@ -138,7 +138,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -247,7 +247,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) )
+       andBool ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
                ))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-8-TO-6)]
 
@@ -288,7 +288,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( .WordStack => ( 0 : ( VV0_x_114b9705:Int : ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) : ( 118 : ( 0 : ( VV0_x_114b9705:Int : ( 70 : ( selector ( "applyOp(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) )
+                     ( .WordStack => ( 0 : ( VV0_x_114b9705:Int : ( #lookup ( CONTRACT_STORAGE:Map , 0 ) : ( 118 : ( 0 : ( VV0_x_114b9705:Int : ( 70 : ( selector ( "applyOp(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
                      ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
@@ -331,7 +331,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -440,7 +440,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) <Int VV0_x_114b9705:Int
+       andBool ( ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) <Int VV0_x_114b9705:Int
                ))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-9-TO-7)]