Pi-Squared-Inc · ACassimiro · Aug 30, 2024 · Aug 28, 2024 · Aug 29, 2024
diff --git a/Makefile b/Makefile
@@ -1,49 +1,60 @@
-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)
 
 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
@@ -0,0 +1,27 @@
+```k
+
+module MX-ACCOUNTS-CONFIGURATION
+    imports INT-SYNTAX
+    imports STRING-SYNTAX
+
+    configuration
+        <mx-accounts>
+            <mx-account multiplicity="*" type="Map">
+                // TODO: The address should be bytes.
+                <mx-account-address> "" </mx-account-address>
+                <mx-esdt-datas>
+                    <mx-esdt-data multiplicity="*" type="Map">
+                        // TODO: The esdt-id should be bytes.
+                        <mx-esdt-id>
+                            <mx-esdt-id-name> "" </mx-esdt-id-name>
+                            <mx-esdt-id-nonce> 0 </mx-esdt-id-nonce>
+                        </mx-esdt-id>
+                        <mx-esdt-balance> 0 </mx-esdt-balance>
+                    </mx-esdt-data>
+                </mx-esdt-datas>
+            </mx-account>
+        </mx-accounts>
+
+endmodule
+
+```
diff --git a/mx-semantics/main/accounts/hooks.md 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
+        <k> MX#bigIntGetESDTExternalBalance
+                ( mxStringValue(Owner:String)
+                , mxStringValue(TokenId:String)
+                , mxIntValue(Nonce:Int)
+                , .MxHookArgs
+                ) => MX#bigIntNew(mxIntValue(Balance)) ... </k>
+        <mx-account-address> Owner </mx-account-address>
+        <mx-esdt-id>
+            <mx-esdt-id-name> TokenId </mx-esdt-id-name>
+            <mx-esdt-id-nonce> Nonce </mx-esdt-id-nonce>
+        </mx-esdt-id>
+        <mx-esdt-balance> Balance:Int </mx-esdt-balance>
+        [priority(50)]
+
+    rule
+        <k> MX#bigIntGetESDTExternalBalance
+                ( mxStringValue(Owner:String)
+                , mxStringValue(TokenId:String)
+                , mxIntValue(Nonce:Int)
+                , .MxHookArgs
+                ) => MX#bigIntNew(mxIntValue(0)) ... </k>
+        <mx-account-address> Owner </mx-account-address>
+        [priority(100)]
+
+endmodule
+
+```
diff --git a/mx-semantics/main/biguint/configuration.md b/mx-semantics/main/biguint/configuration.md
@@ -0,0 +1,14 @@
+```k
+
+module MX-BIGUINT-CONFIGURATION
+    imports INT
+    imports MAP
+
+    configuration
+        <mx-biguint>
+            <bigIntHeap> .Map </bigIntHeap>
+            <bigIntHeapNextId> 0 </bigIntHeapNextId>
+        </mx-biguint>
+endmodule
+
+```
diff --git a/mx-semantics/main/biguint/hooks.md 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
+        <k> MX#bigIntNew(mxIntValue(Value:Int)) => mxIntValue(NextId) ... </k>
+        <bigIntHeap> Ints:Map => Ints[NextId <- Value] </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+
+    rule
+        <k> MX#bigIntAdd(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue(NextId)
+            ...
+        </k>
+        <bigIntHeap>
+            Ints:Map
+            => Ints [ NextId
+                    <-  {Ints[Id1] orDefault 0}:>Int
+                        +Int {Ints[Id2] orDefault 0}:>Int
+                    ]
+        </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+        requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+            andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+    rule
+        <k> MX#bigIntSub(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue(NextId)
+            ...
+        </k>
+        <bigIntHeap>
+            Ints:Map
+            => Ints [ NextId
+                    <-  {Ints[Id1] orDefault 0}:>Int
+                        -Int {Ints[Id2] orDefault 0}:>Int
+                    ]
+        </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+        requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+            andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+    rule
+        <k> MX#bigIntMul(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue(NextId)
+            ...
+        </k>
+        <bigIntHeap>
+            Ints:Map
+            => Ints [ NextId
+                    <-  {Ints[Id1] orDefault 0}:>Int
+                        *Int {Ints[Id2] orDefault 0}:>Int
+                    ]
+        </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+        requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+            andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+    rule
+        <k> MX#bigIntDiv(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue(NextId)
+            ...
+        </k>
+        <bigIntHeap>
+            Ints:Map
+            => Ints [ NextId
+                    <-  {Ints[Id1] orDefault 0}:>Int
+                        /Int {Ints[Id2] orDefault 0}:>Int
+                    ]
+        </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+        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
+        <k> MX#bigIntCmp(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue
+                ( #cmpInt
+                  ( {Ints[Id1] orDefault 0}:>Int
+                  , {Ints[Id2] orDefault 0}:>Int
+                  )
+                )
+            ...
+        </k>
+        <bigIntHeap> Ints:Map </bigIntHeap>
+        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  <Int I2
+    rule #cmpInt(I1, I2) =>  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
@@ -0,0 +1,15 @@
+```k
+
+module MX-BLOCKS-CONFIGURATION
+    imports INT-SYNTAX
+
+    configuration
+        <mx-blocks>
+            <mx-current-block>
+                <mx-current-block-timestamp> 0 </mx-current-block-timestamp>
+            </mx-current-block>
+        </mx-blocks>
+
+endmodule
+
+```
diff --git a/mx-semantics/main/blocks/hooks.md 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
+        <k> MX#getBlockTimestamp ( .MxHookArgs ) => mxIntValue(T) ... </k>
+        <mx-current-block-timestamp> T </mx-current-block-timestamp>
+
+endmodule
+
+```
diff --git a/mx-semantics/main/calls/configuration.md b/mx-semantics/main/calls/configuration.md
@@ -0,0 +1,12 @@
+```k
+
+module MX-CALL-CONFIGURATION
+    imports STRING
+
+    configuration
+        <mx-call-data>
+            <mx-caller> "" </mx-caller>
+        </mx-call-data>
+endmodule
+
+```
diff --git a/mx-semantics/main/calls/hooks.md 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
+        <k> MX#getCaller ( .MxHookArgs ) => mxStringValue(Caller) ... </k>
+        <mx-caller> Caller:String </mx-caller>
+
+endmodule
+
+```
diff --git a/mx-semantics/main/configuration.md 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
+        <mx-common>
+            <mx-call-data/>
+            <mx-biguint/>
+            <mx-blocks/>
+            <mx-accounts/>
+        </mx-common>
+endmodule
+
+```
diff --git a/mx-semantics/main/mx-common.md 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
+
+```
diff --git a/mx-semantics/main/syntax.md 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
+
+```