Added integration test for simbolik

package/version

@@ -1 +1 @@
-0.1.210
+0.1.211

pyproject.toml

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

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

@@ -205,6 +205,7 @@ SetUpTest.testSetUpCalled()
 SetUpTest.testSetUpCalledSymbolic(uint256)
 SignTest.testSign()
 SignTest.testSign_symbolic(uint256)
+SimbolikCode.getNumber()
 SnapshotTest.testSnapshot()
 StartPrankTestMsgSender.test_startprank_msgsender_setup()
 StartPrankTestOrigin.test_startprank_origin_setup()

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

@@ -0,0 +1,16 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+// For Simbolik contracts must be deployed to a concrete address and they must
+// have concrete runtime bytecode. The purpose of this is test is to ensure
+// that the initial konfiguration contains the appropiate <account> and
+// <code>-cells.
+contract SimbolikCode {
+
+    uint256 number = 42;
+
+    function getNumber() external view returns (uint256) {
+        return number;
+    }
+
+}

src/tests/integration/test_simbolik_prove.py

@@ -0,0 +1,59 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+from pyk.kast.inner import KApply, KSort, KToken
+from pyk.utils import single
+
+from kontrol.options import ProveOptions, RPCOptions
+from kontrol.prove import foundry_prove
+
+from .test_foundry_prove import assert_pass
+
+if TYPE_CHECKING:
+
+    from pyk.kore.rpc import KoreServer
+    from pyk.utils import BugReport
+
+    from kontrol.foundry import Foundry
+
+
+def test_simbolik_prove(
+    foundry: Foundry,
+    bug_report: BugReport | None,
+    server: KoreServer,
+) -> None:
+    test_id = 'SimbolikCode.getNumber()'
+
+    prove_options = ProveOptions(
+        bug_report=bug_report,
+        active_symbolik=True,
+    )
+
+    # When
+    prove_res = foundry_prove(
+        foundry,
+        tests=[(test_id, None)],
+        prove_options=prove_options,
+        rpc_options=RPCOptions(port=server.port, smt_timeout=500),
+    )
+
+    # Then
+    proof = single(prove_res)
+    assert_pass(test_id, proof)
+
+    # All accounts must have a concrete address and code cell
+    init_node = proof.kcfg.node(proof.init)
+
+    accounts = init_node.cterm.cells.get('ACCOUNTS_CELL', None)
+    assert isinstance(accounts, KApply)
+    assert 0 < len(accounts.args)
+
+    empty = foundry.kevm.definition.empty_config(KSort('AccountCell'))
+    for account in accounts.args:
+        subst = empty.match(account)
+        assert subst is not None
+        acct_id = subst.get('ACCTID_CELL', None)
+        assert isinstance(acct_id, KToken)
+        code = subst.get('CODE_CELL', None)
+        assert isinstance(code, KToken)