Rename Elrond to MultiversX

.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}

.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

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

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-*

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.

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";

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'

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  <mandos>
            <k>

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  <mandos>

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  <mandos>

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  <mandos>

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  <mandos>

kmxwasm/k-src/lemmas/proven-elrond-lemmas.md → 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

kmxwasm/k-src/lemmas/semantics/elrond-wasm-lemma-proofs.md → 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

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

kmxwasm/k-src/elrond-lemmas.md → 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

kmxwasm/k-src/elrond-wasm.md → 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

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

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

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
       <k>

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)

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)

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:

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)

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