diff --git a/Makefile b/Makefile
index 69f7ec5..20e642f 100644
--- a/Makefile
+++ b/Makefile
@@ -1,34 +1,40 @@
-SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
+RUST_SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
RUST_PREPROCESSING_KOMPILED ::= .build/rust-preprocessing-kompiled
RUST_PREPROCESSING_TIMESTAMP ::= $(RUST_PREPROCESSING_KOMPILED)/timestamp
RUST_EXECUTION_KOMPILED ::= .build/rust-execution-kompiled
RUST_EXECUTION_TIMESTAMP ::= $(RUST_EXECUTION_KOMPILED)/timestamp
-SYNTAX_INPUT_DIR ::= tests/syntax
-SYNTAX_OUTPUT_DIR ::= .build/syntax-output
+RUST_SYNTAX_INPUT_DIR ::= tests/syntax
+RUST_SYNTAX_OUTPUT_DIR ::= .build/syntax-output
PREPROCESSING_INPUT_DIR ::= tests/preprocessing
PREPROCESSING_OUTPUT_DIR ::= .build/preprocessing-output
EXECUTION_INPUT_DIR ::= tests/execution
EXECUTION_OUTPUT_DIR ::= .build/execution-output
-SYNTAX_INPUTS ::= $(wildcard $(SYNTAX_INPUT_DIR)/*.rs)
-SYNTAX_OUTPUTS ::= $(patsubst $(SYNTAX_INPUT_DIR)/%.rs,$(SYNTAX_OUTPUT_DIR)/%.rs-parsed,$(SYNTAX_INPUTS))
+SYNTAX_INPUTS ::= $(wildcard $(RUST_SYNTAX_INPUT_DIR)/*.rs)
+SYNTAX_OUTPUTS ::= $(patsubst $(RUST_SYNTAX_INPUT_DIR)/%.rs,$(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed,$(SYNTAX_INPUTS))
PREPROCESSING_INPUTS ::= $(wildcard $(PREPROCESSING_INPUT_DIR)/*.rs)
PREPROCESSING_OUTPUTS ::= $(patsubst $(PREPROCESSING_INPUT_DIR)/%,$(PREPROCESSING_OUTPUT_DIR)/%.preprocessed.kore,$(PREPROCESSING_INPUTS))
-PREPROCESSING_STATUSES ::= $(patsubst %.preprocessed.kore,%.status,$(PREPROCESSING_OUTPUTS))
EXECUTION_INPUTS ::= $(wildcard $(EXECUTION_INPUT_DIR)/*.*.run)
EXECUTION_OUTPUTS ::= $(patsubst $(EXECUTION_INPUT_DIR)/%,$(EXECUTION_OUTPUT_DIR)/%.executed.kore,$(EXECUTION_INPUTS))
-EXECUTION_STATUSES ::= $(patsubst %.executed.kore,%.status,$(EXECUTION_OUTPUTS))
-.PHONY: clean build test syntax-test preprocessing-test execution-test
+MX_SEMANTICS_FILES ::= $(shell find mx-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
+MX_TESTING_KOMPILED ::= .build/mx-testing-kompiled
+MX_TESTING_TIMESTAMP ::= $(MX_TESTING_KOMPILED)/timestamp
+MX_TESTING_INPUT_DIR ::= tests/mx
+MX_TESTING_OUTPUT_DIR ::= .build/mx/output
+MX_TESTING_INPUTS ::= $(wildcard $(MX_TESTING_INPUT_DIR)/**/*.mx)
+MX_TESTING_OUTPUTS ::= $(patsubst $(MX_TESTING_INPUT_DIR)/%,$(MX_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_TESTING_INPUTS))
+
+.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test
clean:
rm -r .build
-build: $(RUST_PREPROCESSING_TIMESTAMP) $(RUST_EXECUTION_TIMESTAMP)
+build: $(RUST_PREPROCESSING_TIMESTAMP) $(RUST_EXECUTION_TIMESTAMP) $(MX_TESTING_TIMESTAMP)
-test: syntax-test preprocessing-test execution-test
+test: syntax-test preprocessing-test execution-test mx-test
syntax-test: $(SYNTAX_OUTPUTS)
@@ -36,14 +42,19 @@ preprocessing-test: $(PREPROCESSING_OUTPUTS)
execution-test: $(EXECUTION_OUTPUTS)
-$(RUST_PREPROCESSING_TIMESTAMP): $(SEMANTICS_FILES)
+mx-test: $(MX_TESTING_OUTPUTS)
+
+$(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
$$(which kompile) rust-semantics/targets/preprocessing/rust.md --emit-json -o $(RUST_PREPROCESSING_KOMPILED)
-$(RUST_EXECUTION_TIMESTAMP): $(SEMANTICS_FILES)
+$(RUST_EXECUTION_TIMESTAMP): $(RUST_SEMANTICS_FILES)
$$(which kompile) rust-semantics/targets/execution/rust.md --emit-json -o $(RUST_EXECUTION_KOMPILED)
-$(SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
- mkdir -p $(SYNTAX_OUTPUT_DIR)
+$(MX_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES)
+ $$(which kompile) mx-semantics/targets/testing/mx.md -o $(MX_TESTING_KOMPILED) --debug
+
+$(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(RUST_SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
+ mkdir -p $(RUST_SYNTAX_OUTPUT_DIR)
kast --definition $(RUST_PREPROCESSING_KOMPILED) $< --sort Crate > $@.tmp && mv -f $@.tmp $@
$(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
@@ -70,3 +81,13 @@ $(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: $(EXECUTION_INPUT_DIR)/%.run $(RUST
-pTEST=$(CURDIR)/parse-test.sh
cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
mv -f $@.tmp $@
+
+$(MX_TESTING_OUTPUT_DIR)/%.mx.executed.kore: $(MX_TESTING_INPUT_DIR)/%.mx $(MX_TESTING_TIMESTAMP)
+ mkdir -p $(dir $@)
+ krun \
+ $< \
+ --definition $(MX_TESTING_KOMPILED) \
+ --output kore \
+ --output-file $@.tmp
+ cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+ mv -f $@.tmp $@
diff --git a/mx-semantics/main/accounts/configuration.md b/mx-semantics/main/accounts/configuration.md
new file mode 100644
index 0000000..992f016
--- /dev/null
+++ b/mx-semantics/main/accounts/configuration.md
@@ -0,0 +1,27 @@
+```k
+
+module MX-ACCOUNTS-CONFIGURATION
+ imports INT-SYNTAX
+ imports STRING-SYNTAX
+
+ configuration
+
+
+ // TODO: The address should be bytes.
+ ""
+
+
+ // TODO: The esdt-id should be bytes.
+
+ ""
+ 0
+
+ 0
+
+
+
+
+
+endmodule
+
+```
diff --git a/mx-semantics/main/accounts/hooks.md b/mx-semantics/main/accounts/hooks.md
new file mode 100644
index 0000000..bd9440e
--- /dev/null
+++ b/mx-semantics/main/accounts/hooks.md
@@ -0,0 +1,35 @@
+```k
+
+module MX-ACCOUNTS-HOOKS
+ imports private COMMON-K-CELL
+ imports private MX-ACCOUNTS-CONFIGURATION
+ imports private MX-COMMON-SYNTAX
+
+ rule
+ MX#bigIntGetESDTExternalBalance
+ ( mxStringValue(Owner:String)
+ , mxStringValue(TokenId:String)
+ , mxIntValue(Nonce:Int)
+ , .MxHookArgs
+ ) => MX#bigIntNew(mxIntValue(Balance)) ...
+ Owner
+
+ TokenId
+ Nonce
+
+ Balance:Int
+ [priority(50)]
+
+ rule
+ MX#bigIntGetESDTExternalBalance
+ ( mxStringValue(Owner:String)
+ , mxStringValue(TokenId:String)
+ , mxIntValue(Nonce:Int)
+ , .MxHookArgs
+ ) => MX#bigIntNew(mxIntValue(0)) ...
+ Owner
+ [priority(100)]
+
+endmodule
+
+```
\ No newline at end of file
diff --git a/mx-semantics/main/biguint/configuration.md b/mx-semantics/main/biguint/configuration.md
new file mode 100644
index 0000000..9468de1
--- /dev/null
+++ b/mx-semantics/main/biguint/configuration.md
@@ -0,0 +1,14 @@
+```k
+
+module MX-BIGUINT-CONFIGURATION
+ imports INT
+ imports MAP
+
+ configuration
+
+ .Map
+ 0
+
+endmodule
+
+```
\ No newline at end of file
diff --git a/mx-semantics/main/biguint/hooks.md b/mx-semantics/main/biguint/hooks.md
new file mode 100644
index 0000000..c7ba438
--- /dev/null
+++ b/mx-semantics/main/biguint/hooks.md
@@ -0,0 +1,101 @@
+```k
+
+module MX-BIGUINT-HOOKS
+ imports private BOOL
+ imports private COMMON-K-CELL
+ imports private K-EQUAL-SYNTAX
+ imports private MX-BIGUINT-CONFIGURATION
+ imports private MX-COMMON-SYNTAX
+
+ rule
+ MX#bigIntNew(mxIntValue(Value:Int)) => mxIntValue(NextId) ...
+ Ints:Map => Ints[NextId <- Value]
+ NextId => NextId +Int 1
+
+ rule
+ MX#bigIntAdd(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+ => mxIntValue(NextId)
+ ...
+
+
+ Ints:Map
+ => Ints [ NextId
+ <- {Ints[Id1] orDefault 0}:>Int
+ +Int {Ints[Id2] orDefault 0}:>Int
+ ]
+
+ NextId => NextId +Int 1
+ requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+ andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+ rule
+ MX#bigIntSub(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+ => mxIntValue(NextId)
+ ...
+
+
+ Ints:Map
+ => Ints [ NextId
+ <- {Ints[Id1] orDefault 0}:>Int
+ -Int {Ints[Id2] orDefault 0}:>Int
+ ]
+
+ NextId => NextId +Int 1
+ requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+ andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+ rule
+ MX#bigIntMul(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+ => mxIntValue(NextId)
+ ...
+
+
+ Ints:Map
+ => Ints [ NextId
+ <- {Ints[Id1] orDefault 0}:>Int
+ *Int {Ints[Id2] orDefault 0}:>Int
+ ]
+
+ NextId => NextId +Int 1
+ requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+ andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+ rule
+ MX#bigIntDiv(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+ => mxIntValue(NextId)
+ ...
+
+
+ Ints:Map
+ => Ints [ NextId
+ <- {Ints[Id1] orDefault 0}:>Int
+ /Int {Ints[Id2] orDefault 0}:>Int
+ ]
+
+ NextId => NextId +Int 1
+ requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+ andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+ andBool Ints[Id2] orDefault 0 =/=K 0
+
+ rule
+ MX#bigIntCmp(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+ => mxIntValue
+ ( #cmpInt
+ ( {Ints[Id1] orDefault 0}:>Int
+ , {Ints[Id2] orDefault 0}:>Int
+ )
+ )
+ ...
+
+ Ints:Map
+ requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+ andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+ syntax Int ::= #cmpInt ( Int , Int ) [function, total, symbol(cmpInt), smtlib(cmpInt)]
+ rule #cmpInt(I1, I2) => -1 requires I1 1 requires I1 >Int I2
+ rule #cmpInt(I1, I2) => 0 requires I1 ==Int I2
+
+endmodule
+
+```
diff --git a/mx-semantics/main/blocks/configuration.md b/mx-semantics/main/blocks/configuration.md
new file mode 100644
index 0000000..e41e471
--- /dev/null
+++ b/mx-semantics/main/blocks/configuration.md
@@ -0,0 +1,15 @@
+```k
+
+module MX-BLOCKS-CONFIGURATION
+ imports INT-SYNTAX
+
+ configuration
+
+
+ 0
+
+
+
+endmodule
+
+```
diff --git a/mx-semantics/main/blocks/hooks.md b/mx-semantics/main/blocks/hooks.md
new file mode 100644
index 0000000..22c0362
--- /dev/null
+++ b/mx-semantics/main/blocks/hooks.md
@@ -0,0 +1,14 @@
+```k
+
+module MX-BLOCKS-HOOKS
+ imports private COMMON-K-CELL
+ imports private MX-BLOCKS-CONFIGURATION
+ imports private MX-COMMON-SYNTAX
+
+ rule
+ MX#getBlockTimestamp ( .MxHookArgs ) => mxIntValue(T) ...
+ T
+
+endmodule
+
+```
diff --git a/mx-semantics/main/calls/configuration.md b/mx-semantics/main/calls/configuration.md
new file mode 100644
index 0000000..c509fd8
--- /dev/null
+++ b/mx-semantics/main/calls/configuration.md
@@ -0,0 +1,12 @@
+```k
+
+module MX-CALL-CONFIGURATION
+ imports STRING
+
+ configuration
+
+ ""
+
+endmodule
+
+```
\ No newline at end of file
diff --git a/mx-semantics/main/calls/hooks.md b/mx-semantics/main/calls/hooks.md
new file mode 100644
index 0000000..c4076e0
--- /dev/null
+++ b/mx-semantics/main/calls/hooks.md
@@ -0,0 +1,14 @@
+```k
+
+module MX-CALLS-HOOKS
+ imports private COMMON-K-CELL
+ imports private MX-CALL-CONFIGURATION
+ imports private MX-COMMON-SYNTAX
+
+ rule
+ MX#getCaller ( .MxHookArgs ) => mxStringValue(Caller) ...
+ Caller:String
+
+endmodule
+
+```
\ No newline at end of file
diff --git a/mx-semantics/main/configuration.md b/mx-semantics/main/configuration.md
new file mode 100644
index 0000000..c6f0195
--- /dev/null
+++ b/mx-semantics/main/configuration.md
@@ -0,0 +1,23 @@
+```k
+
+requires "accounts/configuration.md"
+requires "biguint/configuration.md"
+requires "blocks/configuration.md"
+requires "calls/configuration.md"
+
+module MX-COMMON-CONFIGURATION
+ imports MX-ACCOUNTS-CONFIGURATION
+ imports MX-BIGUINT-CONFIGURATION
+ imports MX-BLOCKS-CONFIGURATION
+ imports MX-CALL-CONFIGURATION
+
+ configuration
+
+
+
+
+
+
+endmodule
+
+```
\ No newline at end of file
diff --git a/mx-semantics/main/mx-common.md b/mx-semantics/main/mx-common.md
new file mode 100644
index 0000000..27bb479
--- /dev/null
+++ b/mx-semantics/main/mx-common.md
@@ -0,0 +1,15 @@
+```k
+
+requires "accounts/hooks.md"
+requires "biguint/hooks.md"
+requires "blocks/hooks.md"
+requires "calls/hooks.md"
+
+module MX-COMMON
+ imports private MX-ACCOUNTS-HOOKS
+ imports private MX-BIGUINT-HOOKS
+ imports private MX-BLOCKS-HOOKS
+ imports private MX-CALLS-HOOKS
+endmodule
+
+```
\ No newline at end of file
diff --git a/mx-semantics/main/syntax.md b/mx-semantics/main/syntax.md
new file mode 100644
index 0000000..66b1315
--- /dev/null
+++ b/mx-semantics/main/syntax.md
@@ -0,0 +1,14 @@
+```k
+
+module MX-COMMON-SYNTAX
+ imports INT-SYNTAX
+ imports STRING-SYNTAX
+
+ syntax MxValue ::= mxIntValue(Int)
+ | mxStringValue(String)
+ syntax MxHookName ::= r"MX#[a-zA-Z][a-zA-Z0-9]*" [token]
+ syntax MxHookArgs ::= List{MxValue, ","}
+ syntax HookCall ::= MxHookName "(" MxHookArgs ")"
+endmodule
+
+```
diff --git a/mx-semantics/targets/testing/configuration.md b/mx-semantics/targets/testing/configuration.md
new file mode 100644
index 0000000..3f6e4b5
--- /dev/null
+++ b/mx-semantics/targets/testing/configuration.md
@@ -0,0 +1,26 @@
+```k
+
+requires "../../test/configuration.md"
+requires "../../main/configuration.md"
+
+module COMMON-K-CELL
+ imports private MX-TEST-EXECUTION-PARSING-SYNTAX
+
+ configuration
+ $PGM:MxTest
+endmodule
+
+module MX-CONFIGURATION
+ imports COMMON-K-CELL
+ imports MX-COMMON-CONFIGURATION
+ imports MX-TEST-CONFIGURATION
+
+ configuration
+
+
+
+
+
+endmodule
+
+```
diff --git a/mx-semantics/targets/testing/mx.md b/mx-semantics/targets/testing/mx.md
new file mode 100644
index 0000000..febdec7
--- /dev/null
+++ b/mx-semantics/targets/testing/mx.md
@@ -0,0 +1,19 @@
+```k
+
+requires "configuration.md"
+requires "../../main/mx-common.md"
+requires "../../main/syntax.md"
+requires "../../test/execution.md"
+
+module MX-SYNTAX
+ imports MX-COMMON-SYNTAX
+ imports MX-TEST-EXECUTION-PARSING-SYNTAX
+endmodule
+
+module MX
+ imports private MX-COMMON
+ imports private MX-CONFIGURATION
+ imports private MX-TEST-EXECUTION
+endmodule
+
+```
\ No newline at end of file
diff --git a/mx-semantics/test/configuration.md b/mx-semantics/test/configuration.md
new file mode 100644
index 0000000..033a43e
--- /dev/null
+++ b/mx-semantics/test/configuration.md
@@ -0,0 +1,13 @@
+```k
+
+module MX-TEST-CONFIGURATION
+ imports MX-TEST-EXECUTION-PARSING-SYNTAX
+
+ configuration
+
+ .MxValueStack
+
+
+endmodule
+
+```
diff --git a/mx-semantics/test/execution.md b/mx-semantics/test/execution.md
new file mode 100644
index 0000000..cef680c
--- /dev/null
+++ b/mx-semantics/test/execution.md
@@ -0,0 +1,167 @@
+```k
+
+module MX-TEST-EXECUTION-PARSING-SYNTAX
+ imports INT-SYNTAX
+ imports MX-COMMON-SYNTAX
+ imports STRING-SYNTAX
+
+ syntax TestInstruction ::= "push" MxValue
+ | "call" argcount:Int MxHookName
+ | "get_big_int"
+ | getBigint(Int)
+ | "check_eq" MxValue
+ | setCaller(String)
+ | addAccount(String)
+ | setBalance(account:String, token:String, nonce:Int, value:Int)
+ | setBlockTimestamp(Int)
+
+ syntax MxTest ::= NeList{TestInstruction, ";"}
+
+ syntax MxValueStack ::= List{MxValue, ","}
+endmodule
+
+module MX-TEST-EXECUTION
+ imports private COMMON-K-CELL
+ imports private INT
+ imports private MX-ACCOUNTS-TEST
+ imports private MX-BIGUINT-TEST
+ imports private MX-BLOCKS-TEST
+ imports private MX-CALL-TEST
+ imports private MX-TEST-CONFIGURATION
+ imports private MX-TEST-EXECUTION-PARSING-SYNTAX
+
+ rule I:TestInstruction ; Is:MxTest => I ~> Is
+ rule .MxTest => .K
+
+ rule
+ push V:MxValue => .K ...
+ L:MxValueStack => V , L
+
+ rule
+ call N:Int Hook:MxHookName => Hook(takeArgs(N, L)) ...
+ L:MxValueStack => drop(N, L)
+
+ rule
+ V:MxValue => .K ...
+ L:MxValueStack => V , L
+
+ rule
+ get_big_int => testGetBigInt(IntId) ...
+ mxIntValue(IntId) , L:MxValueStack => L
+
+ rule
+ check_eq V => .K ...
+ V , L:MxValueStack => L
+
+ syntax MxHookArgs ::= takeArgs(Int, MxValueStack) [function, total]
+ rule takeArgs(N:Int, _:MxValueStack) => .MxHookArgs
+ requires N <=Int 0
+ rule takeArgs(N:Int, (V:MxValue , Vs:MxValueStack)) => V , takeArgs(N -Int 1, Vs)
+ requires 0 Vs
+ requires N <=Int 0
+ rule drop(N:Int, (_V:MxValue , Vs:MxValueStack)) => drop(N -Int 1, Vs)
+ requires 0 testGetBigInt(IntId:Int)
+ => mxIntValue({Ints[IntId] orDefault 0}:>Int)
+ ...
+
+ Ints:Map
+ NextId => NextId +Int 1
+ requires IntId in_keys(Ints) andBool isInt(Ints[IntId] orDefault 0)
+
+endmodule
+
+module MX-CALL-TEST
+ imports private COMMON-K-CELL
+ imports private MX-CALL-CONFIGURATION
+ imports private MX-TEST-EXECUTION-PARSING-SYNTAX
+
+ rule
+ setCaller(S:String) => .K ...
+ _ => S
+endmodule
+
+module MX-ACCOUNTS-TEST
+ imports private COMMON-K-CELL
+ imports private MX-ACCOUNTS-CONFIGURATION
+ imports private MX-TEST-EXECUTION-PARSING-SYNTAX
+
+ rule
+ addAccount(S:String) => .K ...
+
+ .Bag
+ =>
+ S
+ .Bag
+
+
+
+ rule
+ setBalance
+ (... account: Account:String
+ , token: TokenName:String
+ , nonce: Nonce:Int
+ , value: Value:Int
+ ) => .K
+ ...
+
+ Account
+
+ TokenName
+ Nonce
+
+ _ => Value
+ [priority(50)]
+
+ rule
+ setBalance
+ (... account: Account:String
+ , token: TokenName:String
+ , nonce: Nonce:Int
+ , value: Value:Int
+ ) => .K
+ ...
+
+ Account
+
+ .Bag =>
+
+
+ TokenName
+ Nonce
+
+ Value
+
+
+ [priority(100)]
+
+endmodule
+
+module MX-BLOCKS-TEST
+ imports private COMMON-K-CELL
+ imports private MX-BLOCKS-CONFIGURATION
+ imports private MX-TEST-EXECUTION-PARSING-SYNTAX
+
+ rule
+ setBlockTimestamp(T:Int) => .K ...
+ _ => T
+
+endmodule
+
+```
diff --git a/rust-semantics/targets/execution/configuration.md b/rust-semantics/targets/execution/configuration.md
index e5f0d55..c035ed0 100644
--- a/rust-semantics/targets/execution/configuration.md
+++ b/rust-semantics/targets/execution/configuration.md
@@ -3,7 +3,7 @@
module COMMON-K-CELL
imports private RUST-EXECUTION-TEST-PARSING-SYNTAX
imports private RUST-PREPROCESSING-SYNTAX
-
+
configuration
crateParser($PGM:Crate) ~> $TEST:ExecutionTest
endmodule
diff --git a/tests/mx/biguint/add.mx b/tests/mx/biguint/add.mx
new file mode 100644
index 0000000..548c1ba
--- /dev/null
+++ b/tests/mx/biguint/add.mx
@@ -0,0 +1,7 @@
+push mxIntValue(10);
+call 1 MX#bigIntNew;
+push mxIntValue(20);
+call 1 MX#bigIntNew;
+call 2 MX#bigIntAdd;
+get_big_int;
+check_eq mxIntValue(30)
diff --git a/tests/mx/biguint/div.mx b/tests/mx/biguint/div.mx
new file mode 100644
index 0000000..50c61eb
--- /dev/null
+++ b/tests/mx/biguint/div.mx
@@ -0,0 +1,7 @@
+push mxIntValue(40);
+call 1 MX#bigIntNew;
+push mxIntValue(500);
+call 1 MX#bigIntNew;
+call 2 MX#bigIntDiv;
+get_big_int;
+check_eq mxIntValue(12)
diff --git a/tests/mx/biguint/eq.mx b/tests/mx/biguint/eq.mx
new file mode 100644
index 0000000..c811ec1
--- /dev/null
+++ b/tests/mx/biguint/eq.mx
@@ -0,0 +1,6 @@
+push mxIntValue(20);
+call 1 MX#bigIntNew;
+push mxIntValue(20);
+call 1 MX#bigIntNew;
+call 2 MX#bigIntCmp;
+check_eq mxIntValue(0)
diff --git a/tests/mx/biguint/gt.mx b/tests/mx/biguint/gt.mx
new file mode 100644
index 0000000..a18aff7
--- /dev/null
+++ b/tests/mx/biguint/gt.mx
@@ -0,0 +1,6 @@
+push mxIntValue(10);
+call 1 MX#bigIntNew;
+push mxIntValue(20);
+call 1 MX#bigIntNew;
+call 2 MX#bigIntCmp;
+check_eq mxIntValue(1)
diff --git a/tests/mx/biguint/lt.mx b/tests/mx/biguint/lt.mx
new file mode 100644
index 0000000..ca2859b
--- /dev/null
+++ b/tests/mx/biguint/lt.mx
@@ -0,0 +1,6 @@
+push mxIntValue(20);
+call 1 MX#bigIntNew;
+push mxIntValue(10);
+call 1 MX#bigIntNew;
+call 2 MX#bigIntCmp;
+check_eq mxIntValue(-1)
diff --git a/tests/mx/biguint/mul.mx b/tests/mx/biguint/mul.mx
new file mode 100644
index 0000000..f65ece6
--- /dev/null
+++ b/tests/mx/biguint/mul.mx
@@ -0,0 +1,7 @@
+push mxIntValue(40);
+call 1 MX#bigIntNew;
+push mxIntValue(50);
+call 1 MX#bigIntNew;
+call 2 MX#bigIntMul;
+get_big_int;
+check_eq mxIntValue(2000)
diff --git a/tests/mx/biguint/new.mx b/tests/mx/biguint/new.mx
new file mode 100644
index 0000000..76ad5a4
--- /dev/null
+++ b/tests/mx/biguint/new.mx
@@ -0,0 +1,4 @@
+push mxIntValue(10);
+call 1 MX#bigIntNew;
+get_big_int;
+check_eq mxIntValue(10)
diff --git a/tests/mx/biguint/sub.mx b/tests/mx/biguint/sub.mx
new file mode 100644
index 0000000..3365431
--- /dev/null
+++ b/tests/mx/biguint/sub.mx
@@ -0,0 +1,7 @@
+push mxIntValue(40);
+call 1 MX#bigIntNew;
+push mxIntValue(50);
+call 1 MX#bigIntNew;
+call 2 MX#bigIntSub;
+get_big_int;
+check_eq mxIntValue(10)
diff --git a/tests/mx/blockchain/get-block-timestamp.mx b/tests/mx/blockchain/get-block-timestamp.mx
new file mode 100644
index 0000000..fc9a5c7
--- /dev/null
+++ b/tests/mx/blockchain/get-block-timestamp.mx
@@ -0,0 +1,3 @@
+setBlockTimestamp(1234);
+call 0 MX#getBlockTimestamp;
+check_eq mxIntValue(1234)
diff --git a/tests/mx/blockchain/get-caller.mx b/tests/mx/blockchain/get-caller.mx
new file mode 100644
index 0000000..99fa7ae
--- /dev/null
+++ b/tests/mx/blockchain/get-caller.mx
@@ -0,0 +1,3 @@
+setCaller("Owner");
+call 0 MX#getCaller;
+check_eq mxStringValue("Owner")
diff --git a/tests/mx/blockchain/get-sc-balance.mx b/tests/mx/blockchain/get-sc-balance.mx
new file mode 100644
index 0000000..8b03c0c
--- /dev/null
+++ b/tests/mx/blockchain/get-sc-balance.mx
@@ -0,0 +1,17 @@
+addAccount("Owner");
+
+push mxIntValue(0);
+push mxStringValue("MyToken");
+push mxStringValue("Owner");
+call 3 MX#bigIntGetESDTExternalBalance;
+get_big_int;
+check_eq mxIntValue(0);
+
+setBalance("Owner", "MyToken", 0, 1234);
+
+push mxIntValue(0);
+push mxStringValue("MyToken");
+push mxStringValue("Owner");
+call 3 MX#bigIntGetESDTExternalBalance;
+get_big_int;
+check_eq mxIntValue(1234)