Merge branch 'master' into _update-deps/runtimeverification/wasm-sema…

…ntics

Makefile

@@ -276,11 +276,13 @@ TEST_MANDOS := $(POETRY_RUN) mandos --definition-dir $(llvm_dir)/mandos-kompiled
 #
 # > error: package `clap_derive v4.4.0` cannot be built because it requires rustc 1.70.0 or newer,
 # > while the currently active rustc version is 1.69.0-nightly
-# 
-# To avoid this, we enforce minimal version resolution before building the contract
+# > Either upgrade to rustc 1.70.0 or newer, or use
+# > cargo update -p [email protected] --precise ver
+#
+# Use a precise clap version.
 mxpy-build/%:
 	if [ ! -f "$*/Cargo.lock" ]; then \
-	    cargo generate-lockfile --manifest-path $*/Cargo.toml -Z minimal-versions ; \
+	    cargo update --manifest-path $*/Cargo.toml -p clap --precise 4.1.0 ; \
 	fi
 
 	mxpy contract build "$*" --wasm-symbols --no-wasm-opt

kmultiversx/src/kmultiversx/foundry.py

@@ -13,13 +13,13 @@
 from pyk.cli.utils import dir_path
 from pyk.cterm import CTerm, build_claim
 from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst
+from pyk.kast.manip import split_config_from
 from pyk.ktool.krun import KRun
 from pyk.prelude.collections import list_of, map_of, set_of
 from pyk.prelude.kint import leInt
 from pyk.prelude.ml import mlEqualsTrue
 from pyk.prelude.utils import token
 from pyk.utils import ensure_dir_path
-from pykwasm import wasm2kast
 from pykwasm.kwasm_ast import KInt
 
 from kmultiversx.scenario import (
@@ -29,14 +29,15 @@
     ListBytes,
     get_steps_sc_call,
     mandos_argument_to_kbytes,
-    split_config_from,
     wrapBytes,
 )
+from kmultiversx.utils import kast_to_json_str, krun_config, load_wasm
 
 if TYPE_CHECKING:
     from hypothesis.strategies import SearchStrategy
     from pyk.cterm import KClaim
     from pyk.kast.inner import KInner
+    from pyk.ktool.krun import KPrint
 
 INPUT_FILE_NAME = 'foundry.json'
 TEST_PREFIX = 'test_'
@@ -55,11 +56,6 @@ def load_input_json(test_dir: str) -> dict:
         raise FileNotFoundError(f'{INPUT_FILE_NAME!r} not found in "{test_dir!r}"') from None
 
 
-def load_wasm(filename: str) -> KInner:
-    with open(filename, 'rb') as f:
-        return wasm2kast.wasm2kast(f, filename)
-
-
 def find_test_wasm_path(test_dir: str) -> str:
     test_wasm_path = glob.glob(test_dir + '/output/*.wasm')
     # TODO this loads the first wasm file in the directory. what if there are multiple wasm files?
@@ -126,14 +122,8 @@ def deploy_test(krun: KRun, test_wasm: KInner, contract_wasms: dict[bytes, KInne
     return sym_conf, subst
 
 
-def run_config(krun: KRun, conf: KInner) -> KInner:
-    conf_kore = krun.kast_to_kore(conf, sort=KSort('GeneratedTopCell'))
-    res_conf_kore = krun.run_kore_term(conf_kore)
-    return krun.kore_to_kast(res_conf_kore)
-
-
 def run_config_and_check_empty(krun: KRun, conf: KInner) -> tuple[KInner, KInner, dict[str, KInner]]:
-    final_conf = run_config(krun, conf)
+    final_conf = krun_config(krun, conf)
     sym_conf, subst = split_config_from(final_conf)
     k_cell = subst['K_CELL']
     if not isinstance(k_cell, KSequence) or k_cell.arity != 0:
@@ -164,7 +154,7 @@ def run_test(krun: KRun, sym_conf: KInner, init_subst: dict[str, KInner], endpoi
     conf_with_steps = Subst(subst)(sym_conf)
 
     try:
-        run_config(krun, conf_with_steps)
+        krun_config(krun, conf_with_steps)
     except RuntimeError as rte:
         if rte.args[0].startswith('Command krun exited with code 1'):
             raise RuntimeError(f'Test failed for input input: {args}') from None
@@ -254,23 +244,27 @@ def run_concrete(
 
 
 def generate_claims(
-    krun: KRun,
+    kprint: KPrint,
     test_endpoints: Mapping[str, tuple[str, ...]],
     sym_conf: KInner,
     init_subst: dict[str, KInner],
     output_dir: Path,
+    pretty_print: bool = False,
 ) -> None:
     output_dir = ensure_dir_path(output_dir)
 
     for endpoint, arg_types in test_endpoints.items():
         claim = generate_claim(endpoint, arg_types, sym_conf, init_subst)
 
-        output_file = output_dir / f'{endpoint}-spec.k'
-
-        txt = krun.pretty_print(claim)  # TODO wrap this in a spec module with imports
+        if pretty_print:
+            txt = kprint.pretty_print(claim)
+            ext = 'k'
+        else:
+            txt = kast_to_json_str(claim)
+            ext = 'json'
 
-        with open(output_file, 'w') as f:
-            f.write(txt)
+        output_file = output_dir / f'{endpoint}-spec.{ext}'
+        output_file.write_text(txt)
 
 
 def generate_claim(
@@ -440,18 +434,26 @@ def main() -> None:
         type=dir_path,
         help='Path to Foundry LLVM definition to use.',
     )
-    parser.add_argument('-d', '--directory', required=True, help='path to the test contract')
+    parser.add_argument('-d', '--directory', required=True, help='Path to the test contract.')
     parser.add_argument(
         '--gen-claims',
         dest='gen_claims',
         action='store_true',
-        help='generate claims for symbolic testing',
+        help='Generate claims for symbolic testing.',
     )
     parser.add_argument(
         '--output-dir',
         dest='output_dir',
         required=False,
-        help='directory to store generated claims',
+        help='Directory to store generated claims.',
+    )
+    parser.add_argument(
+        '-p',
+        '--pretty',
+        dest='pretty',
+        default=False,
+        action='store_true',
+        help='Pretty print claims. Default output format is JSON.',
     )
     args = parser.parse_args()
 
@@ -484,6 +486,7 @@ def main() -> None:
             output_dir = Path('generated_claims')
 
         print('Generating claims:', output_dir)
-        generate_claims(krun, test_endpoints, sym_conf, init_subst, output_dir)
+        generate_claims(krun, test_endpoints, sym_conf, init_subst, output_dir, args.pretty)
+
     else:
         run_concrete(krun, test_endpoints, sym_conf, init_subst)

kmultiversx/src/kmultiversx/scenario.py

@@ -7,22 +7,17 @@
 import subprocess
 import sys
 import tempfile
-from typing import Iterable, Optional, TypeVar
+from typing import Iterable, Optional
 
 from Cryptodome.Hash import keccak
 from pyk.cli.utils import dir_path
 from pyk.kast.inner import KApply, KInner, KSequence, KSort, KToken, Subst
 from pyk.kast.manip import split_config_from
 from pyk.ktool.krun import KRun
 from pyk.prelude.collections import set_of
-from pykwasm import wasm2kast
 from pykwasm.kwasm_ast import KBytes, KInt, KString
 
-T = TypeVar('T')
-
-
-def flatten(l: list[list[T]]) -> list[T]:
-    return [item for sublist in l for item in sublist]
+from kmultiversx.utils import flatten, kast_to_json_str, krun_config, load_wasm
 
 
 def wrapBytes(bs: KToken) -> KInner:  # noqa: N802
@@ -74,10 +69,6 @@ def ListBytes(items: Iterable[KInner]) -> KInner:  # noqa: N802
     return KList(items, empty='.ListBytes', list_item='ListBytesItem', concat='_ListBytes_')
 
 
-def config_to_kast_term(config: KInner) -> dict:
-    return {'format': 'KAST', 'version': 2, 'term': config.to_dict()}
-
-
 ###############################
 
 addr_prefix = 'address:'
@@ -487,19 +478,12 @@ def register(with_name: str) -> KInner:
 
 def file_to_module_decl(filename: str, output_dir: str) -> KInner:
     if filename[-5:] == '.wasm':
-        return wasm_file_to_module_decl(filename)
+        return load_wasm(filename)
     if filename[-5:] == '.wast' or filename[-4:] == '.wat':
         return wat_file_to_module_decl(filename, output_dir)
     raise ValueError(f'Filetype not yet supported: {filename}')
 
 
-def wasm_file_to_module_decl(filename: str) -> KInner:
-    # Check that file exists.
-    with open(filename, 'rb') as f:
-        module = wasm2kast.wasm2kast(f, filename)
-        return module
-
-
 def wat_file_to_module_decl(filename: str, output_dir: str) -> KInner:
     if not os.path.exists(filename):
         raise Exception(f'file {filename} does not exist')
@@ -515,7 +499,7 @@ def wat_file_to_module_decl(filename: str, output_dir: str) -> KInner:
         print('stderr:')
         print(e.stderr)
         raise e
-    return wasm_file_to_module_decl(new_wasm_filename)
+    return load_wasm(new_wasm_filename)
 
 
 def get_external_file_path(test_file: str, rel_path_to_new_file: str) -> str:
@@ -697,7 +681,7 @@ def run_test_file(
         if cmd_args.log_level != 'none':
             log_intermediate_state(krun, '%s_%d_%s.pre' % (test_name, i, step_name), init_config, output_dir)
 
-        new_config = krun_config(krun, init_config=init_config)
+        new_config = krun_config(krun, conf=init_config)
         final_config = new_config
 
         if cmd_args.log_level != 'none':
@@ -715,18 +699,12 @@ def run_test_file(
     return final_config
 
 
-def krun_config(krun: KRun, init_config: KInner) -> KInner:
-    kore_config = krun.kast_to_kore(init_config, sort=KSort('GeneratedTopCell'))
-    kore_config = krun.run_kore_term(kore_config)
-    return krun.kore_to_kast(kore_config)
-
-
 # ... Setup Elrond Wasm
 
 
 def log_intermediate_state(krun: KRun, name: str, config: KInner, output_dir: str) -> None:
     with open('%s/%s' % (output_dir, name), 'w') as f:
-        f.write(json.dumps(config_to_kast_term(config)))
+        f.write(kast_to_json_str(config))
     with open('%s/%s.pretty.k' % (output_dir, name), 'w') as f:
         pretty = krun.pretty_print(config)
         f.write(pretty)
@@ -771,7 +749,7 @@ def run_tests() -> None:
 
         initial_name = '0000_initial_config'
         with open('%s/%s' % (tmpdir, initial_name), 'w') as f:
-            f.write(json.dumps(config_to_kast_term(template_wasm_config)))
+            f.write(kast_to_json_str(template_wasm_config))
 
         run_test_file(krun, template_wasm_config, test, tmpdir, args)
 

kmultiversx/src/kmultiversx/utils.py

@@ -0,0 +1,37 @@
+from __future__ import annotations
+
+import json
+from typing import TYPE_CHECKING, TypeVar
+
+from pyk.kast.inner import KSort
+from pykwasm import wasm2kast
+
+if TYPE_CHECKING:
+    from pyk.kast.inner import KInner
+    from pyk.kast.kast import KAst
+    from pyk.ktool.krun import KRun
+
+    T = TypeVar('T')
+
+
+def kast_to_json(config: KAst) -> dict:
+    return {'format': 'KAST', 'version': config.version(), 'term': config.to_dict()}
+
+
+def kast_to_json_str(config: KAst) -> str:
+    return json.dumps(kast_to_json(config), sort_keys=True)
+
+
+def flatten(l: list[list[T]]) -> list[T]:
+    return [item for sublist in l for item in sublist]
+
+
+def load_wasm(filename: str) -> KInner:
+    with open(filename, 'rb') as f:
+        return wasm2kast.wasm2kast(f, filename)
+
+
+def krun_config(krun: KRun, conf: KInner) -> KInner:
+    conf_kore = krun.kast_to_kore(conf, sort=KSort('GeneratedTopCell'))
+    res_conf_kore = krun.run_kore_term(conf_kore, pipe_stderr=False)
+    return krun.kore_to_kast(res_conf_kore)