Pi-Squared-Inc · virgil-serbanuta · Sep 4, 2024 · Sep 2, 2024 · Sep 2, 2024 · Sep 2, 2024
diff --git a/mx-semantics/main/accounts/configuration.md b/mx-semantics/main/accounts/configuration.md
@@ -3,6 +3,7 @@
 module MX-ACCOUNTS-CONFIGURATION
     imports INT-SYNTAX
     imports STRING-SYNTAX
+    imports MX-STORAGE-CONFIGURATION
 
     configuration
         <mx-accounts>
@@ -19,6 +20,7 @@ module MX-ACCOUNTS-CONFIGURATION
                         <mx-esdt-balance> 0 </mx-esdt-balance>
                     </mx-esdt-data>
                 </mx-esdt-datas>
+                <mx-account-storage/>
             </mx-account>
         </mx-accounts>
 
@@ -31,4 +33,16 @@ module MX-ACCOUNTS-STACK-CONFIGURATION
         <mx-world-stack> .List </mx-world-stack>
 endmodule
 
+module MX-STORAGE-CONFIGURATION
+    imports MX-COMMON-SYNTAX
+
+    configuration
+        <mx-account-storage>
+            <mx-account-storage-item multiplicity="*" type="Map">
+                <mx-account-storage-key> "" </mx-account-storage-key>
+                <mx-account-storage-value> mxWrappedEmpty </mx-account-storage-value>
+            </mx-account-storage-item>
+        </mx-account-storage>
+endmodule
+
 ```
diff --git a/mx-semantics/main/accounts/hooks.md → mx-semantics/main/accounts/esdt-hooks.md b/mx-semantics/main/accounts/hooks.md → mx-semantics/main/accounts/esdt-hooks.md
diff --git a/mx-semantics/main/accounts/storage-hooks.md b/mx-semantics/main/accounts/storage-hooks.md
@@ -0,0 +1,15 @@
+```k
+
+module MX-STORAGE-HOOKS
+    imports MX-COMMON-SYNTAX
+    imports MX-STORAGE-TOOLS-SYNTAX
+
+    rule MX#storageLoad(mxStringValue(Key:String), Destination:MxValue )
+        => storageLoad(getCallee(), Key, Destination)
+
+    rule MX#storageStore(mxStringValue(Key:String), Value:MxWrappedValue)
+        => storageStore(getCallee(), Key, Value)
+
+endmodule
+
+```
diff --git a/mx-semantics/main/accounts/storage-tools.md b/mx-semantics/main/accounts/storage-tools.md
@@ -0,0 +1,68 @@
+```k
+
+module MX-STORAGE-TOOLS-SYNTAX
+    imports MX-COMMON-SYNTAX
+    imports STRING-SYNTAX
+
+    syntax MxInstructions ::= storageLoad(address: String, key: String, destination: MxValue)
+                            | storageStore(address: String, key: String, value: MxWrappedValue)
+endmodule
+
+module MX-STORAGE-TOOLS
+    imports private COMMON-K-CELL
+    imports private MX-ACCOUNTS-CONFIGURATION
+    imports private MX-COMMON-SYNTAX
+    imports private MX-STORAGE-TOOLS-SYNTAX
+    imports private STRING-SYNTAX
+
+    rule
+        <k>
+            storageLoad(... address: Address:String, key: Key:String, destination: Destination:MxValue)
+            => storeHostValue(Destination, Value)
+            ...
+        </k>
+        <mx-account-address> Address </mx-account-address>
+        <mx-account-storage-key> Key </mx-account-storage-key>
+        <mx-account-storage-value> Value </mx-account-storage-value>
+        [priority(50)]
+
+    rule
+        <k>
+            storageLoad(... address: Address:String, key: _Key:String, destination: Destination:MxValue)
+            => storeHostValue(Destination, mxWrappedEmpty)
+            ...
+        </k>
+        <mx-account-address> Address </mx-account-address>
+        [priority(100)]
+
+    rule
+        <k>
+            storageStore(... address: Address:String, key: Key:String, value: Value:MxWrappedValue)
+            => .K
+            ...
+        </k>
+        <mx-account-address> Address </mx-account-address>
+        <mx-account-storage-key> Key </mx-account-storage-key>
+        <mx-account-storage-value> _ => Value </mx-account-storage-value>
+        [priority(50)]
+
+    rule
+        <k>
+            storageStore(... address: Address:String, key: Key:String, value: Value:MxWrappedValue)
+            => .K
+            ...
+        </k>
+        <mx-account-address> Address </mx-account-address>
+        <mx-account-storage>
+            .Bag =>
+            <mx-account-storage-item>
+                <mx-account-storage-key> Key </mx-account-storage-key>
+                <mx-account-storage-value> Value </mx-account-storage-value>
+            </mx-account-storage-item>
+            ...
+        </mx-account-storage>
+        [priority(100)]
+
+endmodule
+
+```
diff --git a/mx-semantics/main/calls/tools.md b/mx-semantics/main/calls/tools.md
@@ -31,6 +31,7 @@ module MX-CALLS-TOOLS
     imports private K-EQUAL-SYNTAX
     imports private MX-CALL-RESULT-CONFIGURATION
     imports private MX-CALL-TOOLS-SYNTAX
+    imports private MX-COMMON-SYNTAX
     imports private STRING
 
     syntax MxInstructions ::= callContractAux
@@ -262,6 +263,9 @@ module MX-CALLS-TOOLS
     // TODO: Not implemented.
     rule asyncExecute => .K
 
+    rule [[getCallee() => Callee]]
+        <mx-callee> Callee:String </mx-callee>
+
 endmodule
 
-```
+```
diff --git a/mx-semantics/main/mx-common.md b/mx-semantics/main/mx-common.md
@@ -1,6 +1,8 @@
 ```k
 
-requires "accounts/hooks.md"
+requires "accounts/esdt-hooks.md"
+requires "accounts/storage-hooks.md"
+requires "accounts/storage-tools.md"
 requires "accounts/tools.md"
 requires "biguint/hooks.md"
 requires "blocks/hooks.md"
@@ -15,6 +17,8 @@ module MX-COMMON
     imports private MX-BLOCKS-HOOKS
     imports private MX-CALLS-HOOKS
     imports private MX-CALLS-TOOLS
+    imports private MX-STORAGE-HOOKS
+    imports private MX-STORAGE-TOOLS
     imports private MX-TOOLS
 endmodule
 

diff --git a/mx-semantics/main/syntax.md b/mx-semantics/main/syntax.md
@@ -14,6 +14,9 @@ module MX-COMMON-SYNTAX
                       | MxEsdtTransfer
                       | mxTransfersValue(MxEsdtTransferList)
                       | mxUnitValue()
+                      | MxWrappedValue
+    syntax MxWrappedValue ::= "mxWrappedEmpty"
+
     syntax MxHookName ::= r"MX#[a-zA-Z][a-zA-Z0-9]*"  [token]
     syntax MxValueList ::= List{MxValue, ","}
     syntax HookCall ::= MxHookName "(" MxValueList ")"
@@ -40,6 +43,7 @@ module MX-COMMON-SYNTAX
                             | processBuiltinFunction(BuiltinFunction, String, String, MxCallDataCell)
                               [symbol(processBuiltinFunction)]
                             | checkBool(Bool, String)    [symbol(checkBool)]
+                            | storeHostValue(destination: MxValue, value: MxValue)
 
     syntax MxCallResult ::= ".MxCallResult"
                           | mxCallResult
@@ -62,6 +66,8 @@ module MX-COMMON-SYNTAX
                            | "ExecutionFailed"          [symbol(ExecutionFailed)]
                            | "UpgradeFailed"            [symbol(UpgradeFailed)]
                            | "SimulateFailed"           [symbol(SimulateFailed)]
+
+    syntax String ::= getCallee()  [function, total]
 endmodule
 
 ```
diff --git a/mx-semantics/test/execution.md b/mx-semantics/test/execution.md
@@ -9,17 +9,22 @@ module MX-TEST-EXECUTION-PARSING-SYNTAX
                               | "push" MxValue
                               | "call" argcount:Int MxHookName
                               | "get_big_int"
+                              | "push_store_data"
                               | getBigint(Int)
                               | "check_eq" MxValue
                               | setCallee(String)
                               | setCaller(String)
+                              | setCallee(String)
                               | addAccount(String)
                               | setBalance(account:String, token:String, nonce:Int, value:Int)
+                              | setStorage(account:String, key:String, value:MxValue)
                               | setBlockTimestamp(Int)
 
     syntax MxTest ::= NeList{TestInstruction, ";"}
 
     syntax MxValueStack ::= List{MxValue, ","}
+
+    syntax MxWrappedValue ::= wrappedMx(MxValue)
 endmodule
 
 module MX-TEST-EXECUTION
@@ -51,6 +56,14 @@ module MX-TEST-EXECUTION
         <k> get_big_int => testGetBigInt(IntId) ... </k>
         <mx-test-stack> mxIntValue(IntId) , L:MxValueStack => L </mx-test-stack>
 
+    rule
+        <k> storeHostValue (... destination: Destination:MxValue, value: Value:MxValue)
+                ~> push_store_data ; Is
+            => Is
+            ...
+        </k>
+        <mx-test-stack> L:MxValueStack => Destination, Value, L </mx-test-stack>
+
     rule
         <k> check_eq V => .K ... </k>
         <mx-test-stack> V , L:MxValueStack => L </mx-test-stack>
@@ -101,6 +114,10 @@ module MX-CALL-TEST
     rule
         <k> setCaller(S:String) => .K ... </k>
         <mx-caller> _ => S </mx-caller>
+
+    rule
+        <k> setCallee(S:String) => .K ... </k>
+        <mx-callee> _ => S </mx-callee>
 endmodule
 
 module MX-ACCOUNTS-TEST
@@ -119,6 +136,7 @@ module MX-ACCOUNTS-TEST
             =>  <mx-account>
                     <mx-account-address> S </mx-account-address>
                     <mx-esdt-datas> .Bag </mx-esdt-datas>
+                    <mx-account-storage> .Bag </mx-account-storage>
                 </mx-account>
             ...
         </mx-accounts>
@@ -166,6 +184,37 @@ module MX-ACCOUNTS-TEST
     rule (.K => error) ~> setBalance(...)
         [priority(200)]
 
+    rule
+        <k> setStorage
+                (... account: Account:String
+                , key: Key:String
+                , value: Value:MxValue
+                ) => .K
+            ...
+        </k>
+        <mx-account-address> Account </mx-account-address>
+        <mx-account-storage-key> Key </mx-account-storage-key>
+        <mx-account-storage-value> _ => Value </mx-account-storage-value>
+        [priority(50)]
+
+    rule
+        <k> setStorage
+                (... account: Account:String
+                , key: Key:String
+                , value: Value:MxValue
+                ) => .K
+            ...
+        </k>
+        <mx-account-address> Account </mx-account-address>
+        <mx-account-storage>
+            .Bag =>
+            <mx-account-storage-item>
+                <mx-account-storage-key> Key </mx-account-storage-key>
+                <mx-account-storage-value> wrappedMx(Value) </mx-account-storage-value>
+            </mx-account-storage-item>
+        </mx-account-storage>
+        [priority(100)]
+
 endmodule
 
 module MX-BLOCKS-TEST

diff --git a/tests/mx/storage/get-empty-storage.mx b/tests/mx/storage/get-empty-storage.mx
@@ -0,0 +1,9 @@
+addAccount("Owner");
+setCallee("Owner");
+
+push mxIntValue(12);
+push mxStringValue("MyKey");
+call 2 MX#storageLoad;
+push_store_data;
+check_eq mxIntValue(12);
+check_eq mxWrappedEmpty
diff --git a/tests/mx/storage/get-existing-storage.mx b/tests/mx/storage/get-existing-storage.mx
@@ -0,0 +1,10 @@
+addAccount("Owner");
+setCallee("Owner");
+setStorage("Owner", "MyKey", mxStringValue("Hello"));
+
+push mxIntValue(12);
+push mxStringValue("MyKey");
+call 2 MX#storageLoad;
+push_store_data;
+check_eq mxIntValue(12);
+check_eq wrappedMx(mxStringValue("Hello"))
diff --git a/tests/mx/storage/set-empty-storage.mx b/tests/mx/storage/set-empty-storage.mx
@@ -0,0 +1,13 @@
+addAccount("Owner");
+setCallee("Owner");
+
+push wrappedMx(mxStringValue("Hello"));
+push mxStringValue("MyKey");
+call 2 MX#storageStore;
+
+push mxIntValue(12);
+push mxStringValue("MyKey");
+call 2 MX#storageLoad;
+push_store_data;
+check_eq mxIntValue(12);
+check_eq wrappedMx(mxStringValue("Hello"))
diff --git a/tests/mx/storage/set-existing-storage.mx b/tests/mx/storage/set-existing-storage.mx
@@ -0,0 +1,14 @@
+addAccount("Owner");
+setCallee("Owner");
+setStorage("Owner", "MyKey", mxStringValue("Hello"));
+
+push wrappedMx(mxStringValue("World"));
+push mxStringValue("MyKey");
+call 2 MX#storageStore;
+
+push mxIntValue(12);
+push mxStringValue("MyKey");
+call 2 MX#storageLoad;
+push_store_data;
+check_eq mxIntValue(12);
+check_eq wrappedMx(mxStringValue("World"))