Make adder work with the full Elrond semantics (#6)

.gitignore

@@ -5,6 +5,9 @@
 
 .build
 .kprove-*
+.kore-repl-history
+.sessionCommands
+tmp
 
 # User-specific files
 *.rsuser

.gitmodules

@@ -1,3 +1,3 @@
-[submodule "kmxwasm/k-src/wasm-semantics"]
-	path = kmxwasm/k-src/wasm-semantics
-	url = https://github.com/runtimeverification/wasm-semantics
+[submodule "kmxwasm/k-src/elrond-semantics"]
+	path = kmxwasm/k-src/elrond-semantics
+	url = https://github.com/runtimeverification/elrond-semantics

deps/pyk_release

@@ -1 +1 @@
-v0.1.209
+v0.1.366

kmxwasm/Makefile

@@ -82,12 +82,16 @@ black: poetry-install
 check-black: poetry-install
 	$(POETRY_RUN) black --check src
 
-kbuild-%:
+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
+
+kbuild-%: k-src/elrond-semantics/deps/wasm-semantics/blockchain-k-plugin/krypto.md
 	echo && kompile \
 			--backend $* \
 			--md-selector k \
 			--emit-json \
-			-I k-src/wasm-semantics \
+			-I k-src/elrond-semantics \
+			-I k-src/elrond-semantics/deps/wasm-semantics \
 			-I k-src/summaries \
 			--directory ../.build/defn/haskell \
 			--main-module ELROND-WASM \

kmxwasm/README.md

@@ -48,6 +48,13 @@ Setup:
 ```bash
 cd kmxwasm
 poetry install
+
+git submodule update --init
+cd k-src/elrond-semantics/
+git submodule update --init
+# The following is not needed for the actual semantics, but for initializing
+# some dependencies of the wasm-semantics submodule.
+make kbuild-haskell
 ```
 
 Running, this is an example for the multisig contract:

kmxwasm/k-src/ceils-syntax.k

@@ -0,0 +1,45 @@
+module CEILS-SYNTAX
+    imports BOOL
+    imports BYTES
+    imports INT
+    imports WASM-DATA
+
+    syntax Bool ::= definedSubstrBytes(Bytes, startIndex: Int, endIndex: Int)  [function, total]
+    syntax Bool ::= definedReplaceAtBytes(dest: Bytes, index: Int, src: Bytes)  [function, total]
+    syntax Bool ::= definedPadRightBytes(Bytes, length: Int, value: Int)  [function, total]
+    syntax Bool ::= definedModInt(Int, Int)  [function, total]
+    syntax Bool ::= definedShlInt(Int, Int)  [function, total]
+    syntax Bool ::= definedShrInt(Int, Int)  [function, total]
+    syntax Bool ::= definedProjectBytes(KItem)  [function, total]
+    syntax Bool ::= definedProjectInt(KItem)  [function, total]
+    syntax Bool ::= definedMapLookup(Map, KItem)  [function, total]
+
+    syntax Bool ::= definedGetInts(Ints, Int)  [function, total]
+    syntax Bool ::= definedGetElemSegment(ElemSegment, Int)  [function, total]
+
+    // ---------------------------------------
+
+    syntax Bytes ::= substrBytesTotal(Bytes, startIndex: Int, endIndex: Int)
+        [function, total, klabel(substrBytesTotal), symbol, no-evaluators]
+    syntax Bytes ::= replaceAtBytesTotal(dest: Bytes, index: Int, src: Bytes)
+        [function, total, klabel(replaceAtBytesTotal), symbol, no-evaluators]
+    syntax Bytes ::= padRightBytesTotal(Bytes, length: Int, value: Int)
+        [function, total, klabel(padRightBytesTotal), symbol, no-evaluators]
+    syntax Int ::= Int "modIntTotal" Int
+        [function, total, klabel(modIntTotal), symbol, no-evaluators, smtlib(modIntTotal)]
+    syntax Int ::= Int "<<IntTotal" Int
+        [function, total, klabel(shlIntTotal), symbol, no-evaluators]
+    syntax Int ::= Int ">>IntTotal" Int
+        [function, total, klabel(shrIntTotal), symbol, no-evaluators]
+    syntax Bytes ::= projectBytesTotal(KItem)
+        [function, total, klabel(projectBytesTotal), symbol, no-evaluators]
+    syntax Int ::= projectIntTotal(KItem)
+        [function, total, klabel(projectIntTotal), symbol, no-evaluators]
+
+
+    syntax Int ::= #getIntsTotal(Ints, Int)
+        [function, total, klabel(#getIntsTotal), symbol, no-evaluators/*, smtlib(poundGetInts)*/]
+    syntax Index ::= #getElemSegmentTotal(ElemSegment, Int)
+        [function, total, klabel(#getElemSegmentTotal), symbol, no-evaluators]
+
+endmodule