Skip to content

Commit

Permalink
Storage hooks (#71)
Browse files Browse the repository at this point in the history
* Storage hooks

* Read existing storage

* set storage hooks
  • Loading branch information
virgil-serbanuta authored Sep 4, 2024
1 parent b86e46d commit 8dd30e7
Show file tree
Hide file tree
Showing 12 changed files with 208 additions and 2 deletions.
14 changes: 14 additions & 0 deletions mx-semantics/main/accounts/configuration.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
module MX-ACCOUNTS-CONFIGURATION
imports INT-SYNTAX
imports STRING-SYNTAX
imports MX-STORAGE-CONFIGURATION
configuration
<mx-accounts>
Expand All @@ -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>
Expand All @@ -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
```
File renamed without changes.
15 changes: 15 additions & 0 deletions mx-semantics/main/accounts/storage-hooks.md
Original file line number Diff line number Diff line change
@@ -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
```
68 changes: 68 additions & 0 deletions mx-semantics/main/accounts/storage-tools.md
Original file line number Diff line number Diff line change
@@ -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
```
6 changes: 5 additions & 1 deletion mx-semantics/main/calls/tools.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -262,6 +263,9 @@ module MX-CALLS-TOOLS
// TODO: Not implemented.
rule asyncExecute => .K
rule [[getCallee() => Callee]]
<mx-callee> Callee:String </mx-callee>
endmodule
```
```
6 changes: 5 additions & 1 deletion mx-semantics/main/mx-common.md
Original file line number Diff line number Diff line change
@@ -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"
Expand All @@ -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
Expand Down
6 changes: 6 additions & 0 deletions mx-semantics/main/syntax.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 ")"
Expand All @@ -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
Expand All @@ -62,6 +66,8 @@ module MX-COMMON-SYNTAX
| "ExecutionFailed" [symbol(ExecutionFailed)]
| "UpgradeFailed" [symbol(UpgradeFailed)]
| "SimulateFailed" [symbol(SimulateFailed)]
syntax String ::= getCallee() [function, total]
endmodule
```
49 changes: 49 additions & 0 deletions mx-semantics/test/execution.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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>
Expand Down Expand Up @@ -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
Expand All @@ -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>
Expand Down Expand Up @@ -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
Expand Down
9 changes: 9 additions & 0 deletions tests/mx/storage/get-empty-storage.mx
Original file line number Diff line number Diff line change
@@ -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
10 changes: 10 additions & 0 deletions tests/mx/storage/get-existing-storage.mx
Original file line number Diff line number Diff line change
@@ -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"))
13 changes: 13 additions & 0 deletions tests/mx/storage/set-empty-storage.mx
Original file line number Diff line number Diff line change
@@ -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"))
14 changes: 14 additions & 0 deletions tests/mx/storage/set-existing-storage.mx
Original file line number Diff line number Diff line change
@@ -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"))

0 comments on commit 8dd30e7

Please sign in to comment.