From 633fe8b2285a566194304e5b7af3267a852a10bc Mon Sep 17 00:00:00 2001 From: Raoul Schaffranek Date: Mon, 4 Mar 2024 15:02:20 +0100 Subject: [PATCH 1/5] Added integration test for simbolik. --- .../integration/test-data/foundry-prove-all | 1 + .../foundry/test/SimbolikCodeTest.t.sol | 16 +++++ src/tests/integration/test_simbolik_prove.py | 58 +++++++++++++++++++ 3 files changed, 75 insertions(+) create mode 100644 src/tests/integration/test-data/foundry/test/SimbolikCodeTest.t.sol create mode 100644 src/tests/integration/test_simbolik_prove.py diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all index 11dbd2000..bda4dc949 100644 --- a/src/tests/integration/test-data/foundry-prove-all +++ b/src/tests/integration/test-data/foundry-prove-all @@ -200,6 +200,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..e1b930491 --- /dev/null +++ b/src/tests/integration/test_simbolik_prove.py @@ -0,0 +1,58 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +from pyk.kast.inner import KSort, KToken +from pyk.utils import single + +from kontrol.foundry import Foundry +from kontrol.options import ProveOptions, RPCOptions +from kontrol.prove import foundry_prove + +from .test_foundry_prove import assert_pass, foundry, server # noqa: F403 + +if TYPE_CHECKING: + + from pyk.kore.rpc import KoreServer + from pyk.utils import BugReport + + +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 accounts is not None + 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) From bd1776978884ebaa0830e830adf99944a1297279 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 4 Mar 2024 14:04:58 +0000 Subject: [PATCH 2/5] Set Version: 0.1.179 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index e5c7f62e4..f4fdeb66b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.178 +0.1.179 diff --git a/pyproject.toml b/pyproject.toml index 63b20088e..94a3ae1f4 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.178" +version = "0.1.179" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 9ffb713bc..ea7dbbf01 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.178' +VERSION: Final = '0.1.179' From c0be72435eaa6af9e8ffc99a6f4e597b3d6d5e40 Mon Sep 17 00:00:00 2001 From: Raoul Schaffranek Date: Mon, 4 Mar 2024 16:02:41 +0100 Subject: [PATCH 3/5] Fix coding style. --- src/tests/integration/test_simbolik_prove.py | 23 ++++++++++---------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/tests/integration/test_simbolik_prove.py b/src/tests/integration/test_simbolik_prove.py index e1b930491..986ab2178 100644 --- a/src/tests/integration/test_simbolik_prove.py +++ b/src/tests/integration/test_simbolik_prove.py @@ -2,27 +2,28 @@ from typing import TYPE_CHECKING -from pyk.kast.inner import KSort, KToken +from pyk.kast.inner import KApply, KSort, KToken from pyk.utils import single -from kontrol.foundry import Foundry from kontrol.options import ProveOptions, RPCOptions from kontrol.prove import foundry_prove -from .test_foundry_prove import assert_pass, foundry, server # noqa: F403 +from .test_foundry_prove import assert_pass, foundry, server # noqa: F401 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, + foundry: Foundry, # noqa: F811 bug_report: BugReport | None, - server: KoreServer, + server: KoreServer, # noqa: F811 ) -> None: - test_id = "SimbolikCode.getNumber()" + test_id = 'SimbolikCode.getNumber()' prove_options = ProveOptions( bug_report=bug_report, @@ -44,15 +45,15 @@ def test_simbolik_prove( # 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 accounts is not None + 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")) + 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) + acct_id = subst.get('ACCTID_CELL', None) assert isinstance(acct_id, KToken) - code = subst.get("CODE_CELL", None) + code = subst.get('CODE_CELL', None) assert isinstance(code, KToken) From b09b27f2bb724392f61d11a7f9bbc8161fb6c890 Mon Sep 17 00:00:00 2001 From: devops Date: Sun, 17 Mar 2024 11:21:45 +0000 Subject: [PATCH 4/5] Set Version: 0.1.211 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) 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' From 6fa840ed6949de0595cb5cfa5698ad2e8abb131f Mon Sep 17 00:00:00 2001 From: Raoul Schaffranek Date: Mon, 18 Mar 2024 13:14:41 +0100 Subject: [PATCH 5/5] Fix code QA issues. --- src/tests/integration/test_simbolik_prove.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tests/integration/test_simbolik_prove.py b/src/tests/integration/test_simbolik_prove.py index 986ab2178..425692123 100644 --- a/src/tests/integration/test_simbolik_prove.py +++ b/src/tests/integration/test_simbolik_prove.py @@ -8,7 +8,7 @@ from kontrol.options import ProveOptions, RPCOptions from kontrol.prove import foundry_prove -from .test_foundry_prove import assert_pass, foundry, server # noqa: F401 +from .test_foundry_prove import assert_pass if TYPE_CHECKING: @@ -19,9 +19,9 @@ def test_simbolik_prove( - foundry: Foundry, # noqa: F811 + foundry: Foundry, bug_report: BugReport | None, - server: KoreServer, # noqa: F811 + server: KoreServer, ) -> None: test_id = 'SimbolikCode.getNumber()'