diff --git a/package/version b/package/version index 0321d8e76..d28e773d1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.210 +0.1.211 diff --git a/pyproject.toml b/pyproject.toml index 88d7b56ea..da60e34ec 100644 --- a/pyproject.toml +++ b/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. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 1cb35e4a4..bbeb63dd1 100644 --- a/src/kontrol/__init__.py +++ b/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' diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all index 3c7ff6f55..74b70d5c6 100644 --- a/src/tests/integration/test-data/foundry-prove-all +++ b/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() diff --git a/src/tests/integration/test-data/foundry/test/SimbolikCodeTest.t.sol b/src/tests/integration/test-data/foundry/test/SimbolikCodeTest.t.sol new file mode 100644 index 000000000..d643d9edd --- /dev/null +++ b/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 and +// -cells. +contract SimbolikCode { + + uint256 number = 42; + + function getNumber() external view returns (uint256) { + return number; + } + +} diff --git a/src/tests/integration/test_simbolik_prove.py b/src/tests/integration/test_simbolik_prove.py new file mode 100644 index 000000000..425692123 --- /dev/null +++ b/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)