Integration tests for symbolic constructor

package/version

@@ -1 +1 @@
-0.1.282
+0.1.283

pyproject.toml

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

src/tests/integration/conftest.py

@@ -76,12 +76,14 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo
                             str(TEST_DATA_DIR / 'lemmas.k'),
                             str(TEST_DATA_DIR / 'cse-lemmas.k'),
                             str(TEST_DATA_DIR / 'pausability-lemmas.k'),
+                            str(TEST_DATA_DIR / 'symbolic-bytes-lemmas.k'),
                         ],
                         'imports': [
                             'LoopsTest:SUM-TO-N-INVARIANT',
                             'ArithmeticCallTest:CSE-LEMMAS',
                             'CSETest:CSE-LEMMAS',
                             'PortalTest:PAUSABILITY-LEMMAS',
+                            'ImmutableVarsTest:SYMBOLIC-BYTES-LEMMAS',
                         ],
                     }
                 ),

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

@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+import "forge-std/Test.sol";
+import "kontrol-cheatcodes/KontrolCheats.sol";
+
+contract ImmutableVarsContract {
+    uint256 public immutable y;
+
+    constructor(uint256 _y) {
+        y = _y;
+    }
+}
+
+contract ImmutableVarsTest is Test {
+    function test_run_deployment(uint256 x) public returns (bool) {
+        ImmutableVarsContract c = new ImmutableVarsContract(x);
+        assert(c.y() == 85);
+    }
+}

src/tests/integration/test-data/symbolic-bytes-lemmas.k

@@ -0,0 +1,25 @@
+requires "evm.md"
+requires "foundry.md"
+
+module SYMBOLIC-BYTES-LEMMAS
+    imports BOOL
+    imports FOUNDRY
+    imports INFINITE-GAS
+    imports INT-SYMBOLIC
+
+    // Byte indexing in terms of #asWord
+    rule BA [ X ] => #asWord ( #range (BA, X, 1) )
+      requires X <=Int lengthBytes(BA)
+      [simplification(40)]
+
+    rule [bytes-concat-lookup-left]:
+        (A:Bytes +Bytes B:Bytes) [I] => A [I]
+      requires 0 <=Int I andBool I <Int lengthBytes(A)
+      [simplification, preserves-definedness]
+
+    rule [bytes-concat-lookup-right]:
+        (A:Bytes +Bytes B:Bytes) [I] => B [I -Int lengthBytes(A)]
+      requires lengthBytes(A) <=Int I
+      [simplification, preserves-definedness]
+
+endmodule