From 6d13a0eaf7abd0d3f06b9e9f95d08bdfa5dd84a3 Mon Sep 17 00:00:00 2001 From: Virgil Date: Mon, 16 Oct 2023 20:34:13 +0300 Subject: [PATCH] Rename Elrond to MultiversX --- .github/workflows/test.yml | 16 ++++++------- .gitmodules | 6 ++--- README.md | 4 ++-- kmxwasm/Makefile | 14 +++++------ kmxwasm/README.md | 2 +- kmxwasm/flake.nix | 2 +- kmxwasm/k-src/kbuild.toml | 10 ++++---- kmxwasm/k-src/lemmas/proofs/helper-lemmas.md | 2 +- kmxwasm/k-src/lemmas/proofs/list-size.k | 2 +- .../k-src/lemmas/proofs/max-inequalities.k | 2 +- kmxwasm/k-src/lemmas/proofs/mod-int-total.k | 2 +- kmxwasm/k-src/lemmas/proofs/pound-bool.k | 2 +- ...n-elrond-lemmas.md => proven-mx-lemmas.md} | 2 +- ...emma-proofs.md => mx-wasm-lemma-proofs.md} | 10 ++++---- .../semantics/private-specification-lemmas.md | 2 +- .../k-src/{elrond-lemmas.md => mx-lemmas.md} | 2 +- .../k-src/{elrond-semantics => mx-semantics} | 0 kmxwasm/k-src/{elrond-wasm.md => mx-wasm.md} | 18 +++++++------- kmxwasm/k-src/proof-extensions.md | 2 +- kmxwasm/pyproject.toml | 2 +- kmxwasm/samples/sum-to-n/sum-to-n-spec.k | 2 +- kmxwasm/src/kmxwasm/ast/{elrond.py => mx.py} | 0 kmxwasm/src/kmxwasm/execution.py | 5 +--- kmxwasm/src/kmxwasm/lazy_explorer.py | 24 +++++++++---------- kmxwasm/src/kmxwasm/lemmas/generate.py | 4 ++-- kmxwasm/src/kmxwasm/lemmas/lemmas.py | 6 ++--- kmxwasm/src/kmxwasm/proofs.py | 4 ++-- .../kmxwasm/property_testing/implication.py | 2 +- .../src/kmxwasm/property_testing/running.py | 2 +- .../property_testing/wasm_krun_initializer.py | 2 +- kmxwasm/src/tests/integration/test_claims.py | 2 +- kmxwasm/status.md | 4 ++-- 32 files changed, 78 insertions(+), 81 deletions(-) rename kmxwasm/k-src/lemmas/{proven-elrond-lemmas.md => proven-mx-lemmas.md} (99%) rename kmxwasm/k-src/lemmas/semantics/{elrond-wasm-lemma-proofs.md => mx-wasm-lemma-proofs.md} (83%) rename kmxwasm/k-src/{elrond-lemmas.md => mx-lemmas.md} (99%) rename kmxwasm/k-src/{elrond-semantics => mx-semantics} (100%) rename kmxwasm/k-src/{elrond-wasm.md => mx-wasm.md} (62%) rename kmxwasm/src/kmxwasm/ast/{elrond.py => mx.py} (100%) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index bfe2569f..c7831481 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -19,19 +19,19 @@ jobs: - name: 'Set up Docker' uses: ./.github/actions/with-docker with: - container-name: elrond-wasm-ci-${{ github.sha }} + container-name: mx-wasm-ci-${{ github.sha }} - name: 'Install dependencies' - run: docker exec --user user elrond-wasm-ci-${GITHUB_SHA} poetry -C kmxwasm install + run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} poetry -C kmxwasm install - name: 'Check code quality' - run: docker exec --user user elrond-wasm-ci-${GITHUB_SHA} make -C kmxwasm check + run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make -C kmxwasm check - name: 'Run unit tests' - run: docker exec --user user elrond-wasm-ci-${GITHUB_SHA} make -C kmxwasm test-unit + run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make -C kmxwasm test-unit # - name: 'Build LLVM semantics' - # run: docker exec --user user elrond-wasm-ci-${GITHUB_SHA} make -C kmxwasm kbuild-llvm + # run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make -C kmxwasm kbuild-llvm - name: 'Build Haskell semantics' - run: docker exec --user user elrond-wasm-ci-${GITHUB_SHA} make -C kmxwasm kbuild-haskell + run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make -C kmxwasm kbuild-haskell - name: 'Run integration tests' - run: docker exec --user user elrond-wasm-ci-${GITHUB_SHA} make -C kmxwasm test-integration + run: docker exec --user user mx-wasm-ci-${GITHUB_SHA} make -C kmxwasm test-integration - name: 'Tear down Docker' if: always() - run: docker stop --time 0 elrond-wasm-ci-${GITHUB_SHA} + run: docker stop --time 0 mx-wasm-ci-${GITHUB_SHA} diff --git a/.gitmodules b/.gitmodules index 92fdadc1..d47ba093 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,3 @@ -[submodule "kmxwasm/k-src/elrond-semantics"] - path = kmxwasm/k-src/elrond-semantics - url = https://github.com/runtimeverification/elrond-semantics +[submodule "kmxwasm/k-src/mx-semantics"] + path = kmxwasm/k-src/mx-semantics + url = https://github.com/runtimeverification/mx-semantics diff --git a/README.md b/README.md index a3cb810a..dfd8188b 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,2 @@ -# elrond-wasm -Wasm semantics for the Elrond/MultiversX blockchain network +# mx-wasm +Symbolic execution backend for the MultiversX blockchain network diff --git a/kmxwasm/Makefile b/kmxwasm/Makefile index 53fd2cd3..f8938247 100644 --- a/kmxwasm/Makefile +++ b/kmxwasm/Makefile @@ -82,19 +82,19 @@ black: poetry-install check-black: poetry-install $(POETRY_RUN) black --check src -k-src/elrond-semantics/deps/wasm-semantics/blockchain-k-plugin/krypto.md: - make -C k-src/elrond-semantics deps/wasm-semantics/blockchain-k-plugin/krypto.md +k-src/mx-semantics/deps/wasm-semantics/blockchain-k-plugin/krypto.md: + make -C k-src/mx-semantics deps/wasm-semantics/blockchain-k-plugin/krypto.md -kbuild-%: k-src/elrond-semantics/deps/wasm-semantics/blockchain-k-plugin/krypto.md +kbuild-%: k-src/mx-semantics/deps/wasm-semantics/blockchain-k-plugin/krypto.md echo && kompile \ --backend $* \ --md-selector k \ --emit-json \ -I k-src \ - -I k-src/elrond-semantics/deps \ + -I k-src/mx-semantics/deps \ --directory ../.build/defn/haskell \ - --main-module ELROND-WASM \ - --syntax-module ELROND-WASM-SYNTAX \ - k-src/elrond-wasm.md + --main-module MX-WASM \ + --syntax-module MX-WASM-SYNTAX \ + k-src/mx-wasm.md .PHONY: kbuild-* diff --git a/kmxwasm/README.md b/kmxwasm/README.md index c0aa586a..66843785 100644 --- a/kmxwasm/README.md +++ b/kmxwasm/README.md @@ -50,7 +50,7 @@ cd kmxwasm poetry install git submodule update --init -cd k-src/elrond-semantics/ +cd k-src/mx-semantics/ git submodule update --init # The following is not needed for the actual semantics, but for initializing # some dependencies of the wasm-semantics submodule. diff --git a/kmxwasm/flake.nix b/kmxwasm/flake.nix index cedfbcba..7ad379bf 100644 --- a/kmxwasm/flake.nix +++ b/kmxwasm/flake.nix @@ -1,5 +1,5 @@ { - description = "kmxwasm - Symbolic execution for the Elrond blockchain with the Wasm semantics, using pyk."; + description = "kmxwasm - Symbolic execution for the MulitversX blockchain with the Wasm semantics, using pyk."; inputs = { nixpkgs.url = "nixpkgs/nixos-22.05"; flake-utils.url = "github:numtide/flake-utils"; diff --git a/kmxwasm/k-src/kbuild.toml b/kmxwasm/k-src/kbuild.toml index 4c2de8d3..553a5a3e 100644 --- a/kmxwasm/k-src/kbuild.toml +++ b/kmxwasm/k-src/kbuild.toml @@ -4,21 +4,21 @@ version = "0.1.0" source = "." [dependencies] -elrond-semantics={ path = "elrond-semantics" } +elrond-semantics={ path = "mx-semantics" } [targets.llvm] -main-file = 'elrond-wasm.md' +main-file = 'mx-wasm.md' backend='llvm' [targets.haskell] -main-file = 'elrond-wasm.md' +main-file = 'mx-wasm.md' backend='haskell' [targets.lemma-proofs] -main-file = 'lemmas/semantics/elrond-wasm-lemma-proofs.md' +main-file = 'lemmas/semantics/mx-wasm-lemma-proofs.md' backend='haskell' [targets.llvm-library] llvm-kompile-type='c' -main-file = 'elrond-wasm.md' +main-file = 'mx-wasm.md' backend='llvm' diff --git a/kmxwasm/k-src/lemmas/proofs/helper-lemmas.md b/kmxwasm/k-src/lemmas/proofs/helper-lemmas.md index befaf6bb..51777044 100644 --- a/kmxwasm/k-src/lemmas/proofs/helper-lemmas.md +++ b/kmxwasm/k-src/lemmas/proofs/helper-lemmas.md @@ -1,6 +1,6 @@ ```k module HELPER-LEMMAS - imports private ELROND-WASM-LEMMA-PROOFS + imports private MX-WASM-LEMMA-PROOFS claim diff --git a/kmxwasm/k-src/lemmas/proofs/list-size.k b/kmxwasm/k-src/lemmas/proofs/list-size.k index db38aa38..b2eb45fe 100644 --- a/kmxwasm/k-src/lemmas/proofs/list-size.k +++ b/kmxwasm/k-src/lemmas/proofs/list-size.k @@ -1,7 +1,7 @@ requires "helper-lemmas.md" module LIST-SIZE - imports private ELROND-WASM-LEMMA-PROOFS + imports private MX-WASM-LEMMA-PROOFS imports private HELPER-LEMMAS claim diff --git a/kmxwasm/k-src/lemmas/proofs/max-inequalities.k b/kmxwasm/k-src/lemmas/proofs/max-inequalities.k index 8f86bbbd..1ed9eb9d 100644 --- a/kmxwasm/k-src/lemmas/proofs/max-inequalities.k +++ b/kmxwasm/k-src/lemmas/proofs/max-inequalities.k @@ -1,7 +1,7 @@ requires "helper-lemmas.md" module MAX-INEQUALITIES - imports private ELROND-WASM-LEMMA-PROOFS + imports private MX-WASM-LEMMA-PROOFS imports private HELPER-LEMMAS claim diff --git a/kmxwasm/k-src/lemmas/proofs/mod-int-total.k b/kmxwasm/k-src/lemmas/proofs/mod-int-total.k index e611dd3e..f79ff2a7 100644 --- a/kmxwasm/k-src/lemmas/proofs/mod-int-total.k +++ b/kmxwasm/k-src/lemmas/proofs/mod-int-total.k @@ -1,7 +1,7 @@ requires "helper-lemmas.md" module MOD-INT-TOTAL - imports private ELROND-WASM-LEMMA-PROOFS + imports private MX-WASM-LEMMA-PROOFS imports private HELPER-LEMMAS claim diff --git a/kmxwasm/k-src/lemmas/proofs/pound-bool.k b/kmxwasm/k-src/lemmas/proofs/pound-bool.k index 67676aac..bdd2b2fa 100644 --- a/kmxwasm/k-src/lemmas/proofs/pound-bool.k +++ b/kmxwasm/k-src/lemmas/proofs/pound-bool.k @@ -1,7 +1,7 @@ requires "helper-lemmas.md" module POUND-BOOL - imports private ELROND-WASM-LEMMA-PROOFS + imports private MX-WASM-LEMMA-PROOFS imports private HELPER-LEMMAS claim diff --git a/kmxwasm/k-src/lemmas/proven-elrond-lemmas.md b/kmxwasm/k-src/lemmas/proven-mx-lemmas.md similarity index 99% rename from kmxwasm/k-src/lemmas/proven-elrond-lemmas.md rename to kmxwasm/k-src/lemmas/proven-mx-lemmas.md index 4f707ce4..e2dbb77b 100644 --- a/kmxwasm/k-src/lemmas/proven-elrond-lemmas.md +++ b/kmxwasm/k-src/lemmas/proven-mx-lemmas.md @@ -1,5 +1,5 @@ ```k -module PROVEN-ELROND-LEMMAS +module PROVEN-MX-LEMMAS imports private BOOL imports private CEILS imports private ELROND diff --git a/kmxwasm/k-src/lemmas/semantics/elrond-wasm-lemma-proofs.md b/kmxwasm/k-src/lemmas/semantics/mx-wasm-lemma-proofs.md similarity index 83% rename from kmxwasm/k-src/lemmas/semantics/elrond-wasm-lemma-proofs.md rename to kmxwasm/k-src/lemmas/semantics/mx-wasm-lemma-proofs.md index 577a649d..76766d56 100644 --- a/kmxwasm/k-src/lemmas/semantics/elrond-wasm-lemma-proofs.md +++ b/kmxwasm/k-src/lemmas/semantics/mx-wasm-lemma-proofs.md @@ -1,18 +1,18 @@ ```k -requires "../../elrond-wasm.md" +requires "../../mx-wasm.md" requires "destructors.md" requires "private-specification-lemmas.md" requires "user-operations.md" -module ELROND-WASM-LEMMA-PROOFS-SYNTAX - imports ELROND-WASM-SYNTAX +module MX-WASM-LEMMA-PROOFS-SYNTAX + imports MX-WASM-SYNTAX endmodule -module ELROND-WASM-LEMMA-PROOFS +module MX-WASM-LEMMA-PROOFS imports BOOL imports DESTRUCTORS - imports ELROND-WASM-NO-LOCAL-LEMMAS + imports MX-WASM-NO-LOCAL-LEMMAS imports INT imports LIST imports PRIVATE-SPECIFICATION-LEMMAS diff --git a/kmxwasm/k-src/lemmas/semantics/private-specification-lemmas.md b/kmxwasm/k-src/lemmas/semantics/private-specification-lemmas.md index 5fe0a9fa..0e4d8158 100644 --- a/kmxwasm/k-src/lemmas/semantics/private-specification-lemmas.md +++ b/kmxwasm/k-src/lemmas/semantics/private-specification-lemmas.md @@ -1,6 +1,6 @@ ```k module PRIVATE-SPECIFICATION-LEMMAS - imports ELROND-WASM-NO-LOCAL-LEMMAS + imports MX-WASM-NO-LOCAL-LEMMAS // Y > 0 rule X /IntTotal Y => 0 diff --git a/kmxwasm/k-src/elrond-lemmas.md b/kmxwasm/k-src/mx-lemmas.md similarity index 99% rename from kmxwasm/k-src/elrond-lemmas.md rename to kmxwasm/k-src/mx-lemmas.md index 22cfc090..f936801b 100644 --- a/kmxwasm/k-src/elrond-lemmas.md +++ b/kmxwasm/k-src/mx-lemmas.md @@ -1,7 +1,7 @@ ```k require "ceils.k" -module ELROND-LEMMAS [symbolic] +module MX-LEMMAS [symbolic] imports private CEILS imports private ELROND imports private INT-KORE diff --git a/kmxwasm/k-src/elrond-semantics b/kmxwasm/k-src/mx-semantics similarity index 100% rename from kmxwasm/k-src/elrond-semantics rename to kmxwasm/k-src/mx-semantics diff --git a/kmxwasm/k-src/elrond-wasm.md b/kmxwasm/k-src/mx-wasm.md similarity index 62% rename from kmxwasm/k-src/elrond-wasm.md rename to kmxwasm/k-src/mx-wasm.md index ef6c0a84..41248c31 100644 --- a/kmxwasm/k-src/elrond-wasm.md +++ b/kmxwasm/k-src/mx-wasm.md @@ -1,23 +1,23 @@ ```k -require "elrond-lemmas.md" -require "elrond-semantics/foundry.md" -require "lemmas/proven-elrond-lemmas.md" +require "mx-lemmas.md" +require "mx-semantics/foundry.md" +require "lemmas/proven-mx-lemmas.md" require "proof-extensions.md" require "specification-lemmas.md" require "wasm-semantics/kwasm-lemmas.md" -module ELROND-WASM-SYNTAX +module MX-WASM-SYNTAX imports WASM-TEXT-SYNTAX imports FOUNDRY-SYNTAX endmodule -module ELROND-WASM - imports ELROND-LEMMAS - imports ELROND-WASM-NO-LOCAL-LEMMAS - imports PROVEN-ELROND-LEMMAS +module MX-WASM + imports MX-LEMMAS + imports MX-WASM-NO-LOCAL-LEMMAS + imports PROVEN-MX-LEMMAS endmodule -module ELROND-WASM-NO-LOCAL-LEMMAS +module MX-WASM-NO-LOCAL-LEMMAS imports CEILS imports FOUNDRY imports INT-KORE diff --git a/kmxwasm/k-src/proof-extensions.md b/kmxwasm/k-src/proof-extensions.md index cc71b34c..a562246c 100644 --- a/kmxwasm/k-src/proof-extensions.md +++ b/kmxwasm/k-src/proof-extensions.md @@ -1,5 +1,5 @@ ```k -require "elrond-semantics/elrond.md" +require "mx-semantics/elrond.md" module PROOF-EXTENSIONS imports ELROND diff --git a/kmxwasm/pyproject.toml b/kmxwasm/pyproject.toml index 29bbbf64..a82c1f54 100644 --- a/kmxwasm/pyproject.toml +++ b/kmxwasm/pyproject.toml @@ -5,7 +5,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmxwasm" version = "0.1.0" -description = "Symbolic execution for the Elrond blockchain with the Wasm semantics, using pyk." +description = "Symbolic execution for the MultiversX blockchain with the Wasm semantics, using pyk." authors = [ "Runtime Verification, Inc. ", ] diff --git a/kmxwasm/samples/sum-to-n/sum-to-n-spec.k b/kmxwasm/samples/sum-to-n/sum-to-n-spec.k index 9d6105b3..1bf3ab4b 100644 --- a/kmxwasm/samples/sum-to-n/sum-to-n-spec.k +++ b/kmxwasm/samples/sum-to-n/sum-to-n-spec.k @@ -1,5 +1,5 @@ module SUM-TO-N-SPEC - imports ELROND-WASM + imports MX-WASM claim diff --git a/kmxwasm/src/kmxwasm/ast/elrond.py b/kmxwasm/src/kmxwasm/ast/mx.py similarity index 100% rename from kmxwasm/src/kmxwasm/ast/elrond.py rename to kmxwasm/src/kmxwasm/ast/mx.py diff --git a/kmxwasm/src/kmxwasm/execution.py b/kmxwasm/src/kmxwasm/execution.py index e547e41e..404fc027 100644 --- a/kmxwasm/src/kmxwasm/execution.py +++ b/kmxwasm/src/kmxwasm/execution.py @@ -28,7 +28,7 @@ class Loop(Decision): @dataclass(frozen=True) -class UnimplementedElrondFunction(Decision): +class UnimplementedMxFunction(Decision): function_id: int function_name: str @@ -136,9 +136,6 @@ def __handle_call(self, call: KApply) -> Decision: def __function_name(self, id: int) -> str: return self.__functions.addr_to_function(str(id)).name() - def __is_elrond_function(self, id: int) -> bool: - return self.__functions.addr_to_function(str(id)).is_builtin() - def get_instrs_child(term: KInner) -> KInner: wasm = get_wasm_cell(term) diff --git a/kmxwasm/src/kmxwasm/lazy_explorer.py b/kmxwasm/src/kmxwasm/lazy_explorer.py index ca68cb8e..b4552eb6 100644 --- a/kmxwasm/src/kmxwasm/lazy_explorer.py +++ b/kmxwasm/src/kmxwasm/lazy_explorer.py @@ -74,7 +74,7 @@ def __make_summary_module(self) -> Module: krule_to_kore(self.printer().definition, self.printer().kompiled_kore, r) for r in self.__rules.summarize_rules() ] - sentences: list[Sentence] = [Import(module_name='ELROND-WASM', attrs=())] + sentences: list[Sentence] = [Import(module_name='MX-WASM', attrs=())] return Module(name=GENERATED_MODULE_NAME, sentences=sentences + axioms) def __write_semantics(self) -> None: @@ -85,16 +85,16 @@ def __write_semantics(self) -> None: ] identifiers_module = KFlatModule('IDENTIFIERS', sentences=identifier_sentences) - ims = [KImport('ELROND-WASM-CONFIGURATION'), KImport('IDENTIFIERS')] + ims = [KImport('MX-WASM-CONFIGURATION'), KImport('IDENTIFIERS')] reqs = [ KRequire('backend-fixes.md'), - KRequire('elrond-lemmas.md'), - KRequire('elrond-wasm-configuration.md'), + KRequire('mx-lemmas.md'), + KRequire('mx-wasm-configuration.md'), KRequire('proof-extensions.md'), ] - ims.append(KImport('ELROND-LEMMAS')) - ims.append(KImport('ELROND-WASM-CONFIGURATION')) + ims.append(KImport('MX-LEMMAS')) + ims.append(KImport('MX-WASM-CONFIGURATION')) ims.append(KImport('PROOF-EXTENSIONS')) ims.append(KImport('SUMMARY-MACROS')) summaries_module = KFlatModule('SUMMARIES', sentences=self.__rules.summarize_rules(), imports=ims) @@ -111,16 +111,16 @@ def kompile_semantics(k_dir: Path, definition_dir: Path) -> None: print(f'Kompile to {definition_dir}', flush=True) _ = subprocess.run(['rm', '-r', definition_dir]) - elrond_dir = k_dir / 'elrond-semantics' - wasm_dir = elrond_dir / 'deps' / 'wasm-semantics' + mx_dir = k_dir / 'mx-semantics' + wasm_dir = mx_dir / 'deps' / 'wasm-semantics' _ = kompile( - k_dir / 'elrond-wasm.md', + k_dir / 'mx-wasm.md', output_dir=definition_dir, backend=KompileBackend.HASKELL, - main_module='ELROND-WASM', - syntax_module='ELROND-WASM-SYNTAX', - include_dirs=[k_dir, elrond_dir, wasm_dir], + main_module='MX-WASM', + syntax_module='MX-WASM-SYNTAX', + include_dirs=[k_dir, mx_dir, wasm_dir], md_selector='k', ) print('Kompile done.', flush=True) diff --git a/kmxwasm/src/kmxwasm/lemmas/generate.py b/kmxwasm/src/kmxwasm/lemmas/generate.py index 80da1355..37b8a6ee 100755 --- a/kmxwasm/src/kmxwasm/lemmas/generate.py +++ b/kmxwasm/src/kmxwasm/lemmas/generate.py @@ -46,7 +46,7 @@ PROOFS_DIR = LEMMAS_DIR / 'proofs' HELPER_LEMMAS_FILE = PROOFS_DIR / 'helper-lemmas.md' -LEMMAS_FILE = LEMMAS_DIR / 'proven-elrond-lemmas.md' +LEMMAS_FILE = LEMMAS_DIR / 'proven-mx-lemmas.md' B = var('B', BOOL) L = var('L', LIST) @@ -252,7 +252,7 @@ def main(args: list[str]) -> None: # tools.printer # return - LEMMAS_FILE.write_text('```k\nmodule PROVEN-ELROND-LEMMAS\nendmodule\n```\n') + LEMMAS_FILE.write_text('```k\nmodule PROVEN-MX-LEMMAS\nendmodule\n```\n') HELPER_LEMMAS_FILE.write_text('```k\nmodule HELPER-LEMMAS\nendmodule\n```\n') with kbuild_semantics(KBUILD_DIR, config_file=KBUILD_ML_PATH, target=LEMMA_PROOFS, booster=False) as tools: diff --git a/kmxwasm/src/kmxwasm/lemmas/lemmas.py b/kmxwasm/src/kmxwasm/lemmas/lemmas.py index 0a4beda3..fe7ff90d 100644 --- a/kmxwasm/src/kmxwasm/lemmas/lemmas.py +++ b/kmxwasm/src/kmxwasm/lemmas/lemmas.py @@ -87,7 +87,7 @@ def make_claim_module(self) -> KFlatModule: proof = proofOperationList(self.proof) claims = [l.make_claim(proof) for l in self.lemmas] imports = [ - KImport(name='ELROND-WASM-LEMMA-PROOFS', public=False), + KImport(name='MX-WASM-LEMMA-PROOFS', public=False), KImport(name=HELPER_MODULE, public=False), ] return KFlatModule(name=self.name.upper(), sentences=claims, imports=imports) @@ -112,7 +112,7 @@ def make_proven_lemmas_module(lemma_proofs: list[LemmaProof], kast_defn: KDefini KImport(name='INT', public=False), KImport(name='LIST', public=False), ] - return KFlatModule(name='PROVEN-ELROND-LEMMAS', sentences=rules, imports=imports) + return KFlatModule(name='PROVEN-MX-LEMMAS', sentences=rules, imports=imports) @dataclass(frozen=True) @@ -134,6 +134,6 @@ def make_claim(self) -> KClaim: def make_helper_lemmas_module(lemmas: list[HelperLemma]) -> KFlatModule: claims = [l.make_claim() for l in lemmas] imports = [ - KImport(name='ELROND-WASM-LEMMA-PROOFS', public=False), + KImport(name='MX-WASM-LEMMA-PROOFS', public=False), ] return KFlatModule(name=HELPER_MODULE, sentences=claims, imports=imports) diff --git a/kmxwasm/src/kmxwasm/proofs.py b/kmxwasm/src/kmxwasm/proofs.py index d2e7f2d3..c42ee8ea 100644 --- a/kmxwasm/src/kmxwasm/proofs.py +++ b/kmxwasm/src/kmxwasm/proofs.py @@ -53,7 +53,7 @@ K_DIR = ROOT / 'kmxwasm' / 'k-src' BUILD_DIR = ROOT / '.build' DEFINITION_PARENT = BUILD_DIR / 'defn/haskell' -DEFINITION_NAME = 'elrond-wasm-kompiled' +DEFINITION_NAME = 'mx-wasm-kompiled' DATA_DIR = BUILD_DIR / 'data' JSON_DIR = DATA_DIR / 'json' DEBUG_DIR = BUILD_DIR / 'debug' @@ -462,7 +462,7 @@ def execute_function( if isinstance(decision, execution.Finish): rhs_ids.append(node_id) print([node_id], 'finished', flush=True) - elif isinstance(decision, execution.UnimplementedElrondFunction): + elif isinstance(decision, execution.UnimplementedMxFunction): raise ValueError(repr(decision)) elif isinstance(decision, execution.UnsummarizedFunction): return decision diff --git a/kmxwasm/src/kmxwasm/property_testing/implication.py b/kmxwasm/src/kmxwasm/property_testing/implication.py index 7bfd3c06..9d81f48b 100644 --- a/kmxwasm/src/kmxwasm/property_testing/implication.py +++ b/kmxwasm/src/kmxwasm/property_testing/implication.py @@ -1,6 +1,6 @@ from pyk.kast.inner import KApply, KInner, KSequence -from ..ast.elrond import commands_cell_contents, instrs_cell_contents, k_cell_contents +from ..ast.mx import commands_cell_contents, instrs_cell_contents, k_cell_contents def quick_ksequence_implication_check(antecedent: KSequence, consequent: KSequence) -> bool: diff --git a/kmxwasm/src/kmxwasm/property_testing/running.py b/kmxwasm/src/kmxwasm/property_testing/running.py index e5199f54..312e53d9 100644 --- a/kmxwasm/src/kmxwasm/property_testing/running.py +++ b/kmxwasm/src/kmxwasm/property_testing/running.py @@ -8,7 +8,7 @@ from pyk.kore.rpc import LogEntry from pyk.prelude.collections import LIST -from ..ast.elrond import ( +from ..ast.mx import ( CALL_STACK_PATH, cfg_changes_call_stack, command_is_new_wasm_instance, diff --git a/kmxwasm/src/kmxwasm/property_testing/wasm_krun_initializer.py b/kmxwasm/src/kmxwasm/property_testing/wasm_krun_initializer.py index e17f7f9f..c0633fa1 100644 --- a/kmxwasm/src/kmxwasm/property_testing/wasm_krun_initializer.py +++ b/kmxwasm/src/kmxwasm/property_testing/wasm_krun_initializer.py @@ -4,7 +4,7 @@ from pyk.prelude.collections import list_of, map_empty from pyk.prelude.utils import token -from ..ast.elrond import ( +from ..ast.mx import ( accountCellMap, commands_cell_contents, get_contract_mod_idx_cell, diff --git a/kmxwasm/src/tests/integration/test_claims.py b/kmxwasm/src/tests/integration/test_claims.py index c85ffe5c..be9c3380 100644 --- a/kmxwasm/src/tests/integration/test_claims.py +++ b/kmxwasm/src/tests/integration/test_claims.py @@ -10,7 +10,7 @@ from pyk.prelude.kint import intToken from pytest import TempPathFactory -from kmxwasm.ast.elrond import accountCellMap, bytesStack, listBytes, mapIntToBytes +from kmxwasm.ast.mx import accountCellMap, bytesStack, listBytes, mapIntToBytes from kmxwasm.ast.wasm import ( funcDefCellMap, globalInstCellMap, diff --git a/kmxwasm/status.md b/kmxwasm/status.md index 31aeb396..ef94a579 100644 --- a/kmxwasm/status.md +++ b/kmxwasm/status.md @@ -1,4 +1,4 @@ -# Wasm + Elrond function summarization +# Wasm + MultiversX function summarization This project started as an attempt to prove that a simple sum-to-n contract does what its name says. It turned out into a summarizer, so we should probably @@ -74,7 +74,7 @@ and are not exported in the json format). * Not implemented: * some builtins * Parallelism - * Real Elrond semantics + * Real MultiversX semantics * Branch merging * Loop invariants + summarization * Recursion invariants + summarization