Pi-Squared-Inc · virgil-serbanuta · Sep 2, 2024 · Aug 28, 2024 · Aug 28, 2024 · Sep 2, 2024
diff --git a/Makefile b/Makefile
@@ -45,12 +45,18 @@ execution-test: $(EXECUTION_OUTPUTS)
 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)
+	# Workaround for https://github.com/runtimeverification/k/issues/4141
+	-rm -r $(RUST_PREPROCESSING_KOMPILED)
+	$$(which kompile) rust-semantics/targets/preprocessing/rust.md --emit-json -o $(RUST_PREPROCESSING_KOMPILED) --debug
 
 $(RUST_EXECUTION_TIMESTAMP): $(RUST_SEMANTICS_FILES)
-	$$(which kompile) rust-semantics/targets/execution/rust.md --emit-json -o $(RUST_EXECUTION_KOMPILED)
+	# Workaround for https://github.com/runtimeverification/k/issues/4141
+	-rm -r $(RUST_EXECUTION_KOMPILED)
+	$$(which kompile) rust-semantics/targets/execution/rust.md --emit-json -o $(RUST_EXECUTION_KOMPILED) --debug
 
 $(MX_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES)
+	# Workaround for https://github.com/runtimeverification/k/issues/4141
+	-rm -r $(MX_TESTING_KOMPILED)
 	$$(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)

diff --git a/mx-semantics/main/accounts/configuration.md b/mx-semantics/main/accounts/configuration.md
@@ -24,4 +24,11 @@ module MX-ACCOUNTS-CONFIGURATION
 
 endmodule
 
+module MX-ACCOUNTS-STACK-CONFIGURATION
+    imports LIST
+
+    configuration
+        <mx-world-stack> .List </mx-world-stack>
+endmodule
+
 ```
diff --git a/mx-semantics/main/accounts/hooks.md b/mx-semantics/main/accounts/hooks.md
@@ -10,7 +10,7 @@ module MX-ACCOUNTS-HOOKS
                 ( mxStringValue(Owner:String)
                 , mxStringValue(TokenId:String)
                 , mxIntValue(Nonce:Int)
-                , .MxHookArgs
+                , .MxValueList
                 ) => MX#bigIntNew(mxIntValue(Balance)) ... </k>
         <mx-account-address> Owner </mx-account-address>
         <mx-esdt-id>
@@ -23,9 +23,9 @@ module MX-ACCOUNTS-HOOKS
     rule
         <k> MX#bigIntGetESDTExternalBalance
                 ( mxStringValue(Owner:String)
-                , mxStringValue(TokenId:String)
-                , mxIntValue(Nonce:Int)
-                , .MxHookArgs
+                , mxStringValue(_TokenId:String)
+                , mxIntValue(_Nonce:Int)
+                , .MxValueList
                 ) => MX#bigIntNew(mxIntValue(0)) ... </k>
         <mx-account-address> Owner </mx-account-address>
         [priority(100)]

diff --git a/mx-semantics/main/accounts/tools.md b/mx-semantics/main/accounts/tools.md
@@ -0,0 +1,152 @@
+```k
+
+module MX-ACCOUNTS-TOOLS
+    imports private BOOL
+    imports private COMMON-K-CELL
+    imports private INT
+    imports private MX-ACCOUNTS-CONFIGURATION
+    imports private MX-COMMON-SYNTAX
+    imports private STRING
+    imports private MX-ACCOUNTS-STACK-CONFIGURATION
+
+    syntax MxInstructions ::= transferESDT
+                                  ( source: String
+                                  , destination: String
+                                  , token: String
+                                  , nonce: Int
+                                  , value: Int
+                                  )
+                            | checkAccountExists(address: String)
+                            | checkESDTBalance(account: String, token: String, value: Int)
+                            | addToESDTBalance(account: String, token: String, delta: Int, allowNew: Bool)
+
+ // ------------------------------------------------------
+
+    rule transferESDTs(... transfers: .MxEsdtTransferList) => .K
+    rule (.K => transferESDT
+                (... source: Source, destination: Destination
+                , token: TokenName, nonce: Nonce, value: Value
+                )
+        ) ~> transferESDTs
+            (... source: Source:String
+            , destination: Destination:String
+            , transfers:
+                ( mxTransferValue
+                    (... token: TokenName:String
+                    , nonce: Nonce:Int
+                    , value: Value:Int
+                    )
+                , Ts:MxEsdtTransferList
+                ) => Ts
+            )
+
+    rule transferESDT
+            (... source: Source:String, destination: Destination:String
+            , token: TokenName:String, nonce: 0, value: Value:Int
+            )
+      => checkAccountExists(Source)
+      ~> checkAccountExists(Destination)
+      ~> checkESDTBalance(Source, TokenName, Value)
+      ~> addToESDTBalance(Source, TokenName, 0 -Int Value, false)
+      ~> addToESDTBalance(Destination, TokenName, Value, true)
+
+ // ------------------------------------------------------
+
+    rule [checkAccountExists-pass]:
+        <k> checkAccountExists(Address:String) => .K ... </k>
+        <mx-account-address> Address </mx-account-address>
+      [priority(50)]
+
+    rule [checkAccountExists-fail]:
+        <k> checkAccountExists(Address:String)
+            => #exception(ExecutionFailed, "account not found: " +String Address)
+            ...
+        </k>
+      [priority(100)]
+
+
+ // ------------------------------------------------------
+    rule [checkESDTBalance]:
+        <k> checkESDTBalance(Account:String, TokenName:String, 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> 0 </mx-esdt-id-nonce>
+        </mx-esdt-id>
+        <mx-esdt-balance> OriginalFrom:Int </mx-esdt-balance>
+        requires Value <=Int OriginalFrom
+        [priority(50)]
+
+    // VALUE > ORIGFROM or TOKEN does not exist
+    rule [checkESDTBalance-oof-instrs-empty]:
+        <k> checkESDTBalance(_, _, _) => #exception(OutOfFunds, "") ... </k>
+        [priority(100)]
+
+  // ------------------------------------------------------
+    rule [addToESDTBalance]:
+        <k>
+            addToESDTBalance
+                (... account: Account:String
+                , token: TokenName:String
+                , delta: Delta:Int
+                , allowNew: _:Bool
+                )
+            => .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> 0 </mx-esdt-id-nonce>
+        </mx-esdt-id>
+        <mx-esdt-balance> OriginalFrom:Int => OriginalFrom +Int Delta </mx-esdt-balance>
+        [priority(50)]
+
+    rule [addToESDTBalance-new-esdtData]:
+        <k>
+            addToESDTBalance
+                (... account: Account:String
+                , token: TokenName:String
+                , delta: Delta:Int
+                , allowNew: true
+                )
+            => .K
+            ...
+        </k>
+        <mx-account-address> Account </mx-account-address>
+        ( .Bag =>
+            <mx-esdt-data>
+                <mx-esdt-id>
+                    <mx-esdt-id-name> TokenName </mx-esdt-id-name>
+                    <mx-esdt-id-nonce> 0 </mx-esdt-id-nonce>
+                </mx-esdt-id>
+                <mx-esdt-balance> Delta </mx-esdt-balance>
+            </mx-esdt-data>
+        )
+        [priority(100), preserves-definedness]
+
+    rule [addToESDTBalance-new-err-instrs-empty]:
+        addToESDTBalance(... account: _:String, token: _:String, delta: _:Int, allowNew: false)
+        => #exception(ExecutionFailed, "new ESDT data on sender")
+        [priority(100), preserves-definedness]
+
+  // ------------------------------------------------------
+    rule [pushWorldState]:
+         <k> pushWorldState => .K ... </k>
+         <mx-world-stack> (.List => ListItem(ACCTDATA)) ... </mx-world-stack>
+         <mx-accounts> ACCTDATA </mx-accounts>
+    rule [dropWorldState]:
+         <k> dropWorldState => .K ... </k>
+         <mx-world-stack> (ListItem(_) => .List) ... </mx-world-stack>
+
+  // ------------------------------------------------------
+    rule transferFunds(... from: From:String, to: To:String, amount: 0)
+        => checkAccountExists(From)
+        ~> checkAccountExists(To)
+
+endmodule
+
+```
diff --git a/mx-semantics/main/blocks/hooks.md b/mx-semantics/main/blocks/hooks.md
@@ -6,7 +6,7 @@ module MX-BLOCKS-HOOKS
     imports private MX-COMMON-SYNTAX
 
     rule
-        <k> MX#getBlockTimestamp ( .MxHookArgs ) => mxIntValue(T) ... </k>
+        <k> MX#getBlockTimestamp ( .MxValueList ) => 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
@@ -1,12 +1,27 @@
 ```k
 
 module MX-CALL-CONFIGURATION
-    imports STRING
+    imports INT-SYNTAX
+    imports MX-COMMON-SYNTAX
+    imports STRING-SYNTAX
 
     configuration
         <mx-call-data>
+            <mx-callee> "" </mx-callee>
             <mx-caller> "" </mx-caller>
+            <mx-call-args> .MxValueList </mx-call-args>
+            <mx-egld-value> 0 </mx-egld-value>
+            <mx-esdt-transfers> .MxEsdtTransferList </mx-esdt-transfers>
+            <mx-gas-provided> 0 </mx-gas-provided>
+            <mx-gas-price> 0 </mx-gas-price>
         </mx-call-data>
 endmodule
 
+module MX-CALL-RESULT-CONFIGURATION
+    imports MX-COMMON-SYNTAX
+
+    configuration
+        <mx-call-result> .MxCallResult </mx-call-result>
+endmodule
+
 ```
diff --git a/mx-semantics/main/calls/hooks.md b/mx-semantics/main/calls/hooks.md
@@ -2,13 +2,65 @@
 
 module MX-CALLS-HOOKS
     imports private COMMON-K-CELL
+    imports private INT
     imports private MX-CALL-CONFIGURATION
+    imports private MX-CALL-TOOLS-SYNTAX
     imports private MX-COMMON-SYNTAX
+    imports private STRING
 
     rule
-        <k> MX#getCaller ( .MxHookArgs ) => mxStringValue(Caller) ... </k>
+        <k> MX#getCaller ( .MxValueList ) => mxStringValue(Caller) ... </k>
         <mx-caller> Caller:String </mx-caller>
 
+    rule
+        <k>
+            MX#managedMultiTransferESDTNFTExecute
+                ( mxStringValue(Destination:String)
+                , mxTransfersValue(Transfers:MxEsdtTransferList)
+                , mxIntValue(_Gas:Int)
+                , mxStringValue("")  // Function name
+                , mxListValue(.MxValueList)  // Other arguments
+                )
+            => (transferESDTs(Callee, Destination, Transfers) ~> mxIntValue(0))
+            ...
+        </k>
+        <mx-callee> Callee:String </mx-callee>
+
+    rule
+        MX#managedMultiTransferESDTNFTExecute
+            ( mxStringValue(Destination:String)
+            , mxTransfersValue(Transfers:MxEsdtTransferList)
+            , mxIntValue(GasLimit:Int)
+            , mxStringValue(FunctionName:String)
+            , mxListValue(Args:MxValueList)
+            )
+        => executeOnDestContext(Destination, 0, Transfers, GasLimit, FunctionName, Args)
+        requires 0 <Int lengthString(FunctionName)
+
+    rule [executeOnDestContext]:
+        <k> executeOnDestContext
+                (... destination: Destination:String
+                , egldValue: Value:Int
+                , esdtTransfers: Esdt:MxEsdtTransferList
+                , gasLimit: GasLimit:Int
+                , function: Func:String
+                , args: Args:MxValueList
+                )
+            => callContract
+                    ( Func
+                    , prepareIndirectContractCallInput
+                        (... caller: Callee
+                        , callee: Destination
+                        , egldValue: Value
+                        , esdtTransfers: Esdt
+                        , gasLimit: GasLimit
+                        , args:Args
+                        )
+                    )
+                ~> finishExecuteOnDestContext
+            ...
+        </k>
+        <mx-callee> Callee </mx-callee>
 endmodule
 
 ```