From b518fb3d3d4e6dbe9f448136c900c20b9b1df213 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Tue, 16 Apr 2024 13:02:32 +0200 Subject: [PATCH] Distribute `kelrond` with `kmultiversx` (#232) * Remove `kbuild` step * Remove `kwasm` * Move `kelrond` into Python package * Set Version: 0.1.32 * Set Version: 0.1.33 --------- Co-authored-by: devops --- Makefile | 2 +- generate-claims.sh | 8 +- kmultiversx/pyproject.toml | 11 +- .../src/kmultiversx/scripts/kelrond.py | 15 ++ .../src/kmultiversx/scripts/kelrond.sh | 10 +- kwasm | 156 ------------------ package/version | 2 +- 7 files changed, 29 insertions(+), 175 deletions(-) create mode 100644 kmultiversx/src/kmultiversx/scripts/kelrond.py rename kelrond => kmultiversx/src/kmultiversx/scripts/kelrond.sh (92%) mode change 100755 => 100644 delete mode 100755 kwasm diff --git a/Makefile b/Makefile index c5e3fb21..f080df95 100644 --- a/Makefile +++ b/Makefile @@ -87,7 +87,7 @@ test: test-simple mandos-test test-elrond-contracts test-custom-contracts # Unit Tests # ---------- -TEST := ./kelrond +TEST := $(POETRY) run -- kelrond CHECK := git --no-pager diff --no-index --ignore-all-space -R TEST_CONCRETE_BACKEND:= llvm diff --git a/generate-claims.sh b/generate-claims.sh index 12e6bd76..6fba3ad1 100755 --- a/generate-claims.sh +++ b/generate-claims.sh @@ -8,7 +8,7 @@ poetry -C kmultiversx install sc-meta all build --path deps/mx-sdk-rs/contracts/examples/adder --wasm-symbols --no-wasm-opt sc-meta all build --path tests/contracts/foundrylike --wasm-symbols --no-wasm-opt -K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --directory "tests/contracts/foundrylike" --gen-claims 2>&1 | tee kasmer.log +poetry -C kmultiversx run -- kasmer --directory "tests/contracts/foundrylike" --gen-claims 2>&1 | tee kasmer.log # Coindrip @@ -19,13 +19,13 @@ do done sc-meta all build --path deps/coindrip-protocol-sc --wasm-symbols --no-wasm-opt sc-meta all build --path tests/contracts/test_coindrip --wasm-symbols --no-wasm-opt -K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --directory "tests/contracts/test_coindrip" --gen-claims 2>&1 | tee kasmer.log +poetry -C kmultiversx run -- kasmer --directory "tests/contracts/test_coindrip" --gen-claims 2>&1 | tee kasmer.log # Crowdfunding sc-meta all build --path deps/mx-sdk-rs/contracts/examples/crowdfunding-esdt --wasm-symbols --no-wasm-opt sc-meta all build --path tests/contracts/test_crowdfunding-esdt --wasm-symbols --no-wasm-opt -K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --directory "tests/contracts/test_crowdfunding-esdt" --gen-claims 2>&1 | tee kasmer.log +poetry -C kmultiversx run -- kasmer --directory "tests/contracts/test_crowdfunding-esdt" --gen-claims 2>&1 | tee kasmer.log # Pair @@ -37,4 +37,4 @@ K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- ka sc-meta all build --path deps/mx-sdk-rs/contracts/examples/multisig --wasm-symbols --no-wasm-opt sc-meta all build --path tests/contracts/test_multisig --wasm-symbols --no-wasm-opt -K_OPTS="-Xmx8192m" kbuild kompile llvm-kasmer && poetry -C kmultiversx run -- kasmer --directory "tests/contracts/test_multisig" --gen-claims 2>&1 | tee kasmer.log +poetry -C kmultiversx run -- kasmer --directory "tests/contracts/test_multisig" --gen-claims 2>&1 | tee kasmer.log diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml index 4b6e3cfa..24c6048b 100644 --- a/kmultiversx/pyproject.toml +++ b/kmultiversx/pyproject.toml @@ -4,12 +4,17 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmultiversx" -version = "0.1.32" +version = "0.1.33" description = "Python tools for Elrond semantics" authors = [ "Runtime Verification, Inc. ", ] +[tool.poetry.scripts] +mandos = "kmultiversx.scenario:run_tests" +kasmer = "kmultiversx.kasmer:main" +kelrond = "kmultiversx.scripts.kelrond:main" + [tool.poetry.plugins.kdist] mx-semantics = "kmultiversx.kdist.plugin" @@ -54,7 +59,3 @@ skip-string-normalization = true [tool.mypy] disallow_untyped_defs = true - -[tool.poetry.scripts] -mandos = "kmultiversx.scenario:run_tests" -kasmer = "kmultiversx.kasmer:main" diff --git a/kmultiversx/src/kmultiversx/scripts/kelrond.py b/kmultiversx/src/kmultiversx/scripts/kelrond.py new file mode 100644 index 00000000..87a9f419 --- /dev/null +++ b/kmultiversx/src/kmultiversx/scripts/kelrond.py @@ -0,0 +1,15 @@ +import sys +from pathlib import Path + +from pyk.utils import run_process + +SCRIPT_FILE = Path(__file__).parent / 'kelrond.sh' + + +def main() -> None: + proc_res = run_process(['bash', str(SCRIPT_FILE)] + sys.argv[1:], pipe_stdout=False, check=False) + sys.exit(proc_res.returncode) + + +if __name__ == '__main__': + main() diff --git a/kelrond b/kmultiversx/src/kmultiversx/scripts/kelrond.sh old mode 100755 new mode 100644 similarity index 92% rename from kelrond rename to kmultiversx/src/kmultiversx/scripts/kelrond.sh index 2671a426..eeb44c9d --- a/kelrond +++ b/kmultiversx/src/kmultiversx/scripts/kelrond.sh @@ -1,18 +1,12 @@ -#!/usr/bin/env bash - set -euo pipefail shopt -s extglob notif() { echo "== $@" >&2 ; } fatal() { echo "[FATAL] $@" ; exit 1 ; } -kelrond_dir="${KELROND_DIR:-$(dirname $0)}" -build_dir="$kelrond_dir/.build" -kdist_dir="$(poetry -C kmultiversx run -- kdist which)" +kdist_dir="$(kdist which)" defn_dir="${KELROND_DEFN_DIR:-$kdist_dir}/mx-semantics" -kwasm_dir=$kelrond_dir/deps/wasm-semantics - export K_OPTS="${K_OPTS:--Xmx16G -Xss512m}" # Utilities @@ -24,7 +18,7 @@ preprocess() { tmp_dir="$(mktemp -d)" tmp_input="$tmp_dir/$(basename $run_file))" touch "$tmp_input" - poetry -C kmultiversx run kwasm-preprocess "$run_file" > "$tmp_input" + kwasm-preprocess "$run_file" > "$tmp_input" run_file="$tmp_input" } diff --git a/kwasm b/kwasm deleted file mode 100755 index 170a5506..00000000 --- a/kwasm +++ /dev/null @@ -1,156 +0,0 @@ -#!/usr/bin/env bash - -set -euo pipefail -shopt -s extglob - -notif() { echo "== $@" >&2 ; } -fatal() { echo "[FATAL] $@" ; exit 1 ; } - -kwasm_dir="${KWASM_DIR:-$(dirname $0)}" -build_dir="$kwasm_dir/.build" -defn_dir="${KWASM_DEFN_DIR:-$build_dir/defn}" -lib_dir="$build_dir/local/lib" -k_release_dir="${K_RELEASE:-$kwasm_dir/deps/k/k-distribution/target/release/k}" -if [[ ! -f "${k_release_dir}/bin/kompile" ]]; then - if which kompile &> /dev/null; then - k_release_dir="$(dirname $(which kompile))/.." - else - fatal "Cannot find K Installation!" - fi -fi - -export PATH="$k_release_dir/lib/native/linux:$k_release_dir/lib/native/linux64:$k_release_dir/bin/:$PATH" -export LD_LIBRARY_PATH="$k_release_dir/lib/native/linux64:$lib_dir:${LD_LIBRARY_PATH:-}" - -test_logs="$build_dir/logs" -mkdir -p "$test_logs" -test_log="$test_logs/tests.log" - -export K_OPTS="${K_OPTS:--Xmx16G}" - -# Utilities -# --------- - -preprocess() { - local this_script_dir tmp_dir tmp_input - this_script_dir="$(dirname $0)" - tmp_dir="$(mktemp -d)" - tmp_input="$tmp_dir/$(basename $run_file))" - touch "$tmp_input" - python "$this_script_dir/preprocessor.py" "$run_file" > "$tmp_input" - run_file="$tmp_input" -} - -# Runners -# ------- - -run_krun() { - preprocess - export K_OPTS="$K_OPTS -Xss500m" - krun --directory "$backend_dir" "$run_file" "$@" -} - -run_kast() { - local output_mode - - preprocess - output_mode="${1:-kast}" ; shift - kast --directory "$backend_dir" "$run_file" --output "$output_mode" "$@" -} - -run_prove() { - export K_OPTS=-Xmx8G - haskell_backend_command="$k_release_dir/bin/kore-exec" - if $repl; then - haskell_backend_command="$k_release_dir/bin/kore-repl --repl-script $kwasm_dir/kast.kscript" - fi - kprove --directory "$backend_dir" "$run_file" "$@" --haskell-backend-command "$haskell_backend_command" -} - -# Main -# ---- - -usage() { - echo " - usage: $0 run [--backend (llvm|haskell)] * - $0 kast [--backend (llvm|haskell)] * - $0 prove [--backend (haskell)] [--repl] * -m - - $0 [help|--help|version|--version] - - $0 run : Run a single WebAssembly program - $0 kast : Parse a single WebAssembly program and output it in supported format - $0 prove : Run a WebAssembly K proof - - $0 help : Display this help message. - $0 version : Display the KWasm, K, Kore, and Z3 versions in use. - - Note: is a path to a file containing a WebAssembly program. - is a K specification to be proved. - are any arguments you want to pass to K when executing/proving. - is the format for Kast to output the term in. - is the module to take as axioms for verification. -" -} - -usage_fatal() { - usage - fatal "$@" -} - -[[ ! -z ${1:-} ]] || usage_fatal "Must supply a command to run." -if [[ "$1" == '--help' ]] || [[ "$1" == 'help' ]]; then - usage - exit 0 -fi - -if [[ "$1" == 'version' ]] || [[ "$1" == '--version' ]]; then - notif "KWasm Version" - git rev-parse --short HEAD - notif "K Version" - kompile --version - notif "Kore Version" - kore-exec --version - notif "Z3 Version" - z3 --version - exit 0 -fi - -run_command="$1"; shift - -[[ ! -z ${1:-} ]] || usage_fatal "Must supply a file to work on." - -backend="llvm" -repl=false -[[ ! "$run_command" == 'prove' ]] || backend='haskell' -args=() -while [[ $# -gt 0 ]]; do - arg="$1" - case $arg in - --backend) args+=("$arg" "$2") ; backend="$2" ; shift 2 ;; - --repl) args+=("$arg") ; repl=true ; shift ;; - *) break ;; - esac -done - -! $repl || [[ "$backend" == "haskell" ]] || fatal "--repl option only available for Haskell backend." - -backend_dir="$defn_dir/$backend" - -# get the run file -[[ ! -z ${1:-} ]] || usage_fatal "Must supply a file to run on." -run_file="$1" ; shift -if [[ "$run_file" == '-' ]]; then - tmp_input="$(mktemp)" - trap "rm -rf $tmp_input" INT TERM EXIT - cat - > "$tmp_input" - run_file="$tmp_input" -fi -[[ -f "$run_file" ]] || fatal "File does not exist: $run_file" - -case "$run_command-$backend" in - run-@(llvm|haskell) ) run_krun "$@" ;; - kast-@(llvm|haskell) ) run_kast "$@" ;; - prove-@(haskell) ) run_prove "$@" ;; - *) usage_fatal "Unknown command on '$backend' backend: $run_command" ;; -esac diff --git a/package/version b/package/version index 28d00753..50140e35 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.32 +0.1.33