diff --git a/Makefile b/Makefile index 95115add..e508a8f9 100644 --- a/Makefile +++ b/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 clap_builder@4.4.2 --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 diff --git a/kmultiversx/src/kmultiversx/foundry.py b/kmultiversx/src/kmultiversx/foundry.py index ce9081a4..c61fd2fd 100644 --- a/kmultiversx/src/kmultiversx/foundry.py +++ b/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) diff --git a/kmultiversx/src/kmultiversx/scenario.py b/kmultiversx/src/kmultiversx/scenario.py index cb72d2fa..1d7a26f5 100755 --- a/kmultiversx/src/kmultiversx/scenario.py +++ b/kmultiversx/src/kmultiversx/scenario.py @@ -7,7 +7,7 @@ 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 @@ -15,14 +15,9 @@ 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) diff --git a/kmultiversx/src/kmultiversx/utils.py b/kmultiversx/src/kmultiversx/utils.py new file mode 100644 index 00000000..4f1f4b70 --- /dev/null +++ b/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)