From cf41472b28ed9e004302fc4b6d0ed788b1e9394f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Tue, 28 May 2024 07:57:26 +0000 Subject: [PATCH 1/3] Add CLI skeleton --- kmxwasm/src/kmxwasm/kasmerx/__main__.py | 17 +++++++++++++++++ kmxwasm/src/kmxwasm/kasmerx/verify.py | 25 +++++++++++++++++++++++++ 2 files changed, 42 insertions(+) create mode 100644 kmxwasm/src/kmxwasm/kasmerx/verify.py diff --git a/kmxwasm/src/kmxwasm/kasmerx/__main__.py b/kmxwasm/src/kmxwasm/kasmerx/__main__.py index 1eb54a36..61180431 100644 --- a/kmxwasm/src/kmxwasm/kasmerx/__main__.py +++ b/kmxwasm/src/kmxwasm/kasmerx/__main__.py @@ -11,6 +11,7 @@ from .build import kasmerx_build from .fuzz import kasmerx_fuzz from .utils import load_project +from .verify import kasmerx_verify if TYPE_CHECKING: from collections.abc import Sequence @@ -35,6 +36,11 @@ class BuildOpts(KasmerxOpts): ... class FuzzOpts(KasmerxOpts): ... +@dataclass +class VerifyOpts(KasmerxOpts): + test: str + + def main() -> None: import sys @@ -50,6 +56,8 @@ def kasmerx(args: Sequence[str]) -> None: return _kasmerx_build(opts) case FuzzOpts(): return _kasmerx_fuzz(opts) + case VerifyOpts(): + return _kasmerx_verify(opts) case _: raise AssertionError() @@ -69,6 +77,11 @@ def _kasmerx_fuzz(opts: FuzzOpts) -> None: kasmerx_fuzz(project) +def _kasmerx_verify(opts: VerifyOpts) -> None: + project = load_project(opts.project_dir) + kasmerx_verify(project, opts.test) + + # ---------------------- # Command line arguments # ---------------------- @@ -82,6 +95,7 @@ def _parse_args(args: Sequence[str]) -> KasmerxOpts: return { 'build': BuildOpts(project_dir=project_dir), 'fuzz': FuzzOpts(project_dir=project_dir), + 'verify': VerifyOpts(project_dir=project_dir, test=ns.test), }[ns.command] @@ -94,6 +108,9 @@ def _arg_parser() -> ArgumentParser: command_parser.add_parser('build', help='build main and test contracts, and generate claims') command_parser.add_parser('fuzz', help='fuzz test contract') + verify_parser = command_parser.add_parser('verify', help='verify test contract') + verify_parser.add_argument('test', metavar='TEST', help='name of test function') + return parser diff --git a/kmxwasm/src/kmxwasm/kasmerx/verify.py b/kmxwasm/src/kmxwasm/kasmerx/verify.py new file mode 100644 index 00000000..8b28b38a --- /dev/null +++ b/kmxwasm/src/kmxwasm/kasmerx/verify.py @@ -0,0 +1,25 @@ +from pathlib import Path + +from ..property import RunClaim +from .utils import KasmerxProject + + +def kasmerx_verify(project: KasmerxProject, test: str) -> None: + claim_file = project.test_dir / f'generated_claims/{test}-spec.json' + + if not claim_file.exists(): + raise ValueError(f'Claim file does not exist: {claim_file}') + + action = RunClaim( + claim_path=claim_file, + is_k=False, + restart=False, + booster=True, + remove=[], + run_node_id=None, + depth=10000, + iterations=10000, + kcfg_path=Path(f'.property/{test}'), + bug_report=None, + ) + action.run() From dd657d14817801a7b6fd1c217d06bb9147ced688 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Tue, 28 May 2024 11:42:57 +0000 Subject: [PATCH 2/3] Add further command line options --- kmxwasm/src/kmxwasm/kasmerx/__main__.py | 55 ++++++++++++++++++++++++- kmxwasm/src/kmxwasm/kasmerx/verify.py | 36 ++++++++++++---- 2 files changed, 82 insertions(+), 9 deletions(-) diff --git a/kmxwasm/src/kmxwasm/kasmerx/__main__.py b/kmxwasm/src/kmxwasm/kasmerx/__main__.py index 61180431..c6475446 100644 --- a/kmxwasm/src/kmxwasm/kasmerx/__main__.py +++ b/kmxwasm/src/kmxwasm/kasmerx/__main__.py @@ -6,6 +6,7 @@ from pathlib import Path from typing import TYPE_CHECKING +import pyk from pyk.utils import check_dir_path from .build import kasmerx_build @@ -17,6 +18,8 @@ from collections.abc import Sequence from typing import Final + from pyk.utils import BugReport + logger: Final = logging.getLogger(__name__) @@ -39,6 +42,11 @@ class FuzzOpts(KasmerxOpts): ... @dataclass class VerifyOpts(KasmerxOpts): test: str + step: int | None + iterations: int | None + restart: bool | None + booster: bool | None + bug_report: BugReport | None def main() -> None: @@ -79,7 +87,15 @@ def _kasmerx_fuzz(opts: FuzzOpts) -> None: def _kasmerx_verify(opts: VerifyOpts) -> None: project = load_project(opts.project_dir) - kasmerx_verify(project, opts.test) + kasmerx_verify( + project=project, + test=opts.test, + step=opts.step, + iterations=opts.iterations, + restart=opts.restart, + booster=opts.booster, + bug_report=opts.bug_report, + ) # ---------------------- @@ -95,7 +111,15 @@ def _parse_args(args: Sequence[str]) -> KasmerxOpts: return { 'build': BuildOpts(project_dir=project_dir), 'fuzz': FuzzOpts(project_dir=project_dir), - 'verify': VerifyOpts(project_dir=project_dir, test=ns.test), + 'verify': VerifyOpts( + project_dir=project_dir, + test=ns.test, + step=ns.step, + iterations=ns.iterations, + restart=ns.restart, + booster=ns.booster, + bug_report=ns.bug_report, + ), }[ns.command] @@ -110,6 +134,33 @@ def _arg_parser() -> ArgumentParser: verify_parser = command_parser.add_parser('verify', help='verify test contract') verify_parser.add_argument('test', metavar='TEST', help='name of test function') + verify_parser.add_argument( + '--restart', + action='store_true', + default=None, + help='restart the backend with the results of the previous run', + ) + verify_parser.add_argument( + '--step', + type=int, + help='number of steps to run at a time', + ) + verify_parser.add_argument( + '--iterations', + type=int, + help='number of batches of --step steps to run', + ) + verify_parser.add_argument( + '--booster', + action='store_true', + default=None, + help='use the booster backend', + ) + verify_parser.add_argument( + '--bug-report', + type=pyk.cli.args.bug_report_arg, + help='generate bug report with given name', + ) return parser diff --git a/kmxwasm/src/kmxwasm/kasmerx/verify.py b/kmxwasm/src/kmxwasm/kasmerx/verify.py index 8b28b38a..635e2583 100644 --- a/kmxwasm/src/kmxwasm/kasmerx/verify.py +++ b/kmxwasm/src/kmxwasm/kasmerx/verify.py @@ -1,25 +1,47 @@ +from __future__ import annotations + from pathlib import Path +from typing import TYPE_CHECKING + +from pyk.utils import BugReport from ..property import RunClaim -from .utils import KasmerxProject +if TYPE_CHECKING: + from .utils import KasmerxProject -def kasmerx_verify(project: KasmerxProject, test: str) -> None: + +def kasmerx_verify( + project: KasmerxProject, + test: str, + *, + step: int | None = None, + iterations: int | None = None, + restart: bool | None = None, + booster: bool | None = None, + bug_report: BugReport | None = None, +) -> None: claim_file = project.test_dir / f'generated_claims/{test}-spec.json' if not claim_file.exists(): raise ValueError(f'Claim file does not exist: {claim_file}') + # Default values + step = 10000 if step is None else step + iterations = 10000 if iterations is None else iterations + restart = bool(restart) + booster = bool(booster) + action = RunClaim( claim_path=claim_file, is_k=False, - restart=False, - booster=True, + restart=restart, + booster=booster, remove=[], run_node_id=None, - depth=10000, - iterations=10000, + depth=step, + iterations=iterations, kcfg_path=Path(f'.property/{test}'), - bug_report=None, + bug_report=bug_report, ) action.run() From 3ce303d7dd58805883ea30b028e11bed808da405 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 28 May 2024 12:22:17 +0000 Subject: [PATCH 3/3] Set Version: 0.1.42 --- kmxwasm/pyproject.toml | 2 +- package/version | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kmxwasm/pyproject.toml b/kmxwasm/pyproject.toml index 158bf7ab..bd2a1d96 100644 --- a/kmxwasm/pyproject.toml +++ b/kmxwasm/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmxwasm" -version = "0.1.41" +version = "0.1.42" description = "Symbolic execution for the MultiversX blockchain with the Wasm semantics, using pyk." authors = [ "Runtime Verification, Inc. ", diff --git a/package/version b/package/version index 37f868fb..4a3e97d0 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.41 +0.1.42