Implement kasmerx verify

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. <[email protected]>",

kmxwasm/src/kmxwasm/kasmerx/__main__.py

@@ -6,16 +6,20 @@
 from pathlib import Path
 from typing import TYPE_CHECKING
 
+import pyk
 from pyk.utils import check_dir_path
 
 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
     from typing import Final
 
+    from pyk.utils import BugReport
+
 
 logger: Final = logging.getLogger(__name__)
 
@@ -35,6 +39,16 @@ class BuildOpts(KasmerxOpts): ...
 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:
     import sys
 
@@ -50,6 +64,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 +85,19 @@ def _kasmerx_fuzz(opts: FuzzOpts) -> None:
     kasmerx_fuzz(project)
 
 
+def _kasmerx_verify(opts: VerifyOpts) -> None:
+    project = load_project(opts.project_dir)
+    kasmerx_verify(
+        project=project,
+        test=opts.test,
+        step=opts.step,
+        iterations=opts.iterations,
+        restart=opts.restart,
+        booster=opts.booster,
+        bug_report=opts.bug_report,
+    )
+
+
 # ----------------------
 # Command line arguments
 # ----------------------
@@ -82,6 +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,
+            step=ns.step,
+            iterations=ns.iterations,
+            restart=ns.restart,
+            booster=ns.booster,
+            bug_report=ns.bug_report,
+        ),
     }[ns.command]
 
 
@@ -94,6 +132,36 @@ 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')
+    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
 
 

kmxwasm/src/kmxwasm/kasmerx/verify.py

@@ -0,0 +1,47 @@
+from __future__ import annotations
+
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+from pyk.utils import BugReport
+
+from ..property import RunClaim
+
+if TYPE_CHECKING:
+    from .utils import KasmerxProject
+
+
+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=restart,
+        booster=booster,
+        remove=[],
+        run_node_id=None,
+        depth=step,
+        iterations=iterations,
+        kcfg_path=Path(f'.property/{test}'),
+        bug_report=bug_report,
+    )
+    action.run()

package/version

@@ -1 +1 @@
-0.1.41
+0.1.42