Mx blockchain hooks

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
+
+```

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
+
+```

mx-semantics/main/biguint/hooks.md

@@ -1,11 +1,11 @@
 ```k
 
 module MX-BIGUINT-HOOKS
-    imports BOOL
-    imports COMMON-K-CELL
-    imports K-EQUAL-SYNTAX
-    imports MX-BIGUINT-CONFIGURATION
-    imports MX-COMMON-SYNTAX
+    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>

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
+
+```

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
+
+```

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
+
+```

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
+
+```

mx-semantics/main/configuration.md

@@ -1,13 +1,22 @@
 ```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
 

mx-semantics/main/mx-common.md

@@ -1,9 +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
 
 ```

mx-semantics/main/syntax.md

@@ -2,8 +2,10 @@
 
 module MX-COMMON-SYNTAX
     imports INT-SYNTAX
+    imports STRING-SYNTAX
 
-    syntax MxValue ::= mxIntValue(Int)
+    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 ")"

mx-semantics/test/execution.md

@@ -3,12 +3,17 @@
 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, ";"}
 
@@ -18,7 +23,10 @@ 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
 
@@ -79,4 +87,81 @@ module MX-BIGUINT-TEST
 
 endmodule
 
+module MX-CALL-TEST
+    imports private COMMON-K-CELL
+    imports private MX-CALL-CONFIGURATION
+    imports private MX-TEST-EXECUTION-PARSING-SYNTAX
+
+    rule
+        <k> setCaller(S:String) => .K ... </k>
+        <mx-caller> _ => S </mx-caller>
+endmodule
+
+module MX-ACCOUNTS-TEST
+    imports private COMMON-K-CELL
+    imports private MX-ACCOUNTS-CONFIGURATION
+    imports private MX-TEST-EXECUTION-PARSING-SYNTAX
+
+    rule
+        <k> addAccount(S:String) => .K ... </k>
+        <mx-accounts>
+            .Bag
+            =>  <mx-account>
+                    <mx-account-address> S </mx-account-address>
+                    <mx-esdt-datas> .Bag </mx-esdt-datas>
+                </mx-account>
+        </mx-accounts>
+
+    rule
+        <k> setBalance
+                (... account: Account:String
+                , token: TokenName:String
+                , nonce: Nonce:Int
+                , value: Value:Int
+                ) => .K
+            ...
+        </k>
+        <mx-account-address> Account </mx-account-address>
+        <mx-esdt-id>
+            <mx-esdt-id-name> TokenName </mx-esdt-id-name>
+            <mx-esdt-id-nonce> Nonce </mx-esdt-id-nonce>
+        </mx-esdt-id>
+        <mx-esdt-balance> _ => Value </mx-esdt-balance>
+        [priority(50)]
+
+    rule
+        <k> setBalance
+                (... account: Account:String
+                , token: TokenName:String
+                , nonce: Nonce:Int
+                , value: Value:Int
+                ) => .K
+            ...
+        </k>
+        <mx-account-address> Account </mx-account-address>
+        <mx-esdt-datas>
+            .Bag =>
+                <mx-esdt-data>
+                    <mx-esdt-id>
+                        <mx-esdt-id-name> TokenName </mx-esdt-id-name>
+                        <mx-esdt-id-nonce> Nonce </mx-esdt-id-nonce>
+                    </mx-esdt-id>
+                    <mx-esdt-balance> Value </mx-esdt-balance>
+                </mx-esdt-data>
+        </mx-esdt-datas>
+        [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
+        <k> setBlockTimestamp(T:Int) => .K ... </k>
+        <mx-current-block-timestamp> _ => T </mx-current-block-timestamp>
+
+endmodule
+
 ```

tests/mx/blockchain/get-block-timestamp.mx

@@ -0,0 +1,3 @@
+setBlockTimestamp(1234);
+call 0 MX#getBlockTimestamp;
+check_eq mxIntValue(1234)

tests/mx/blockchain/get-caller.mx

@@ -0,0 +1,3 @@
+setCaller("Owner");
+call 0 MX#getCaller;
+check_eq mxStringValue("Owner")

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)