Contract calls

mx-semantics/main/accounts/code-tools.md

@@ -0,0 +1,17 @@
+```k
+
+module MX-ACCOUNTS-CODE-TOOLS
+    imports private COMMON-K-CELL
+    imports private MX-ACCOUNTS-ADDRESS-CONFIGURATION
+    imports private MX-ACCOUNTS-CODE-CONFIGURATION
+
+    rule
+        <k> newExecutionEnvironment(... contractAddress: Address:String)
+            => host.newEnvironment(Code)
+            ...
+        </k>
+        <mx-account-address> Address </mx-account-address>
+        <mx-account-code> Code:ContractCode </mx-account-code>
+endmodule
+
+```

mx-semantics/main/accounts/configuration.md

@@ -1,31 +1,48 @@
 ```k
 
 module MX-ACCOUNTS-CONFIGURATION
-    imports INT-SYNTAX
-    imports STRING-SYNTAX
+    imports MX-ACCOUNTS-ADDRESS-CONFIGURATION
+    imports MX-ACCOUNTS-CODE-CONFIGURATION
+    imports MX-ACCOUNTS-ESDT-CONFIGURATION
     imports MX-STORAGE-CONFIGURATION
 
     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-address/>
+                <mx-esdt-datas/>
                 <mx-account-storage/>
+                <mx-account-code/>
             </mx-account>
         </mx-accounts>
 
 endmodule
 
+module MX-ACCOUNTS-ADDRESS-CONFIGURATION
+    imports STRING-SYNTAX
+
+    configuration
+        // TODO: The address should be bytes.
+        <mx-account-address> "" </mx-account-address>
+endmodule
+
+module MX-ACCOUNTS-ESDT-CONFIGURATION
+    imports INT-SYNTAX
+    imports STRING-SYNTAX
+
+    configuration
+        <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>
+endmodule
+
 module MX-ACCOUNTS-STACK-CONFIGURATION
     imports LIST
 
@@ -45,4 +62,10 @@ module MX-STORAGE-CONFIGURATION
         </mx-account-storage>
 endmodule
 
+module MX-ACCOUNTS-CODE-CONFIGURATION
+    imports MX-COMMON-SYNTAX
+    configuration
+        <mx-account-code> .ContractCode </mx-account-code>
+endmodule
+
 ```

mx-semantics/main/accounts/esdt-hooks.md

@@ -1,8 +1,9 @@
 ```k
 
-module MX-ACCOUNTS-HOOKS
+module MX-ACCOUNTS-ESDT-HOOKS
     imports private COMMON-K-CELL
-    imports private MX-ACCOUNTS-CONFIGURATION
+    imports private MX-ACCOUNTS-ADDRESS-CONFIGURATION
+    imports private MX-ACCOUNTS-ESDT-CONFIGURATION
     imports private MX-COMMON-SYNTAX
 
     rule

mx-semantics/main/accounts/tools.md

@@ -4,10 +4,14 @@ module MX-ACCOUNTS-TOOLS
     imports private BOOL
     imports private COMMON-K-CELL
     imports private INT
+    imports private MX-ACCOUNTS-ADDRESS-CONFIGURATION
+    imports private MX-ACCOUNTS-ESDT-CONFIGURATION
+    // TODO: refactor so that MX-ACCOUNTS-CONFIGURATION is not needed here.
     imports private MX-ACCOUNTS-CONFIGURATION
+    // TODO: refactor so that MX-ACCOUNTS-STACK-CONFIGURATION is not needed here.
+    imports private MX-ACCOUNTS-STACK-CONFIGURATION
     imports private MX-COMMON-SYNTAX
     imports private STRING
-    imports private MX-ACCOUNTS-STACK-CONFIGURATION
 
     syntax MxInstructions ::= transferESDT
                                   ( source: String

mx-semantics/main/biguint/tools.md

@@ -0,0 +1,14 @@
+```k
+
+module MX-BIGUINT-TOOLS
+    imports private COMMON-K-CELL
+    imports private MX-BIGUINT-CONFIGURATION
+    imports private MX-COMMON-SYNTAX
+
+    rule
+        <k> clearBigInts => .K ... </k>
+        <bigIntHeap> _ => .Map </bigIntHeap>
+        <bigIntHeapNextId> _ => 0 </bigIntHeapNextId>
+endmodule
+
+```

mx-semantics/main/call-state/configuration.md

@@ -0,0 +1,25 @@
+```k
+requires "../biguint/configuration.md"
+requires "../calls/configuration.md"
+
+module MX-CALL-STATE-CONFIGURATION
+    imports MX-BIGUINT-CONFIGURATION
+    imports MX-CALL-CONFIGURATION
+    imports MX-CALL-RETV-CONFIGURATION
+
+    configuration
+        <mx-call-state>
+            <mx-call-data/>
+            <mx-return-values/>
+            <mx-biguint/>
+        </mx-call-state>
+endmodule
+
+module MX-CALL-STATE-STACK-CONFIGURATION
+    imports LIST
+
+    configuration
+        <mx-call-state-stack> .List </mx-call-state-stack>
+endmodule
+
+```

mx-semantics/main/call-state/tools.md

@@ -0,0 +1,39 @@
+```k
+
+module MX-CALL-STATE-TOOLS
+    imports private COMMON-K-CELL
+    imports private MX-CALL-STATE-CONFIGURATION
+    imports private MX-CALL-STATE-STACK-CONFIGURATION
+    imports private MX-COMMON-SYNTAX
+
+    rule
+        <k> pushCallState => host.pushCallState ... </k>
+        State:MxCallStateCell
+        <mx-call-state-stack>
+            (.List => ListItem(State))
+            ...
+        </mx-call-state-stack>
+
+    rule
+        <k> popCallState => host.popCallState ... </k>
+        (_:MxCallStateCell => State)
+        <mx-call-state-stack>
+            (ListItem(State:MxCallStateCell) => .List)
+            ...
+        </mx-call-state-stack>
+
+    rule
+        <k> resetCallState => host.resetCallState ... </k>
+        ( _:MxCallStateCell
+            =>  <mx-call-state>
+                    <mx-biguint>
+                        <bigIntHeap> .Map </bigIntHeap>
+                        ...
+                    </mx-biguint>
+                    ...
+                </mx-call-state>
+        )
+
+endmodule
+
+```

mx-semantics/main/calls/configuration.md

@@ -24,4 +24,11 @@ module MX-CALL-RESULT-CONFIGURATION
         <mx-call-result> .MxCallResult </mx-call-result>
 endmodule
 
+module MX-CALL-RETV-CONFIGURATION
+    imports MX-COMMON-SYNTAX
+
+    configuration
+        <mx-return-values> .MxValueList </mx-return-values>
+endmodule
+
 ```

mx-semantics/main/calls/hooks.md

@@ -36,6 +36,21 @@ module MX-CALLS-HOOKS
             )
         => executeOnDestContext(Destination, 0, Transfers, GasLimit, FunctionName, Args)
         requires 0 <Int lengthString(FunctionName)
+
+    rule MX#managedExecuteOnDestContext
+            ( mxStringValue(Destination:String)
+            , mxIntValue(EgldValue:Int)
+            , mxTransfersValue(Transfers:MxEsdtTransferList)
+            , mxIntValue(GasLimit:Int)
+            , mxStringValue(FunctionName:String)
+            , mxListValue(Args:MxValueList)
+            )
+        => executeOnDestContext
+            ( Destination, EgldValue, Transfers
+            , GasLimit, FunctionName, Args
+            )
+
+    rule MX#finish ( V:MxValue ) => returnCallData(V)
 endmodule
 
 ```

mx-semantics/main/calls/tools.md

@@ -26,10 +26,12 @@ module MX-CALL-TOOLS-SYNTAX
 endmodule
 
 module MX-CALLS-TOOLS
+    imports private BOOL
     imports private COMMON-K-CELL
     imports private INT
     imports private K-EQUAL-SYNTAX
     imports private MX-CALL-RESULT-CONFIGURATION
+    imports private MX-CALL-RETV-CONFIGURATION
     imports private MX-CALL-TOOLS-SYNTAX
     imports private MX-COMMON-SYNTAX
     imports private STRING
@@ -47,6 +49,7 @@ module MX-CALLS-TOOLS
                             | "endCall"  [symbol(endCall)]
                             | "asyncExecute"  [symbol(asyncExecute)]
                             | "setVMOutput"  [symbol(setVMOutput)]
+                            | mkCall(function: String, callData: MxCallDataCell)
 
   // -----------------------------------------------------------------------------------
     rule prepareIndirectContractCallInput
@@ -95,6 +98,13 @@ module MX-CALLS-TOOLS
         </k>
         <mx-call-result> _ => .MxCallResult </mx-call-result>
 
+    rule [callContractAux]:
+        callContractAux(_FROM, TO, FUNCNAME, VMINPUT)
+        => newExecutionEnvironment(TO)
+            ~> mkCall(FUNCNAME, VMINPUT)
+      requires notBool(isBuiltin(FUNCNAME))
+          andBool "callBack" =/=K FUNCNAME
+
     rule [callContractAux-builtin]:
         callContractAux
             (... caller: From:String
@@ -168,9 +178,64 @@ module MX-CALLS-TOOLS
         => .K
         requires getCallFunc(FUNC, Args) ==K ""
 
+    rule [determineIsSCCallAfter-call]:
+        determineIsSCCallAfter
+            ( Sender:String, Destination:String, Func:BuiltinFunction
+            ,   <mx-call-data>
+                    <mx-call-args> Args:MxValueList </mx-call-args>
+                    <mx-gas-provided> Gas:Int </mx-gas-provided>
+                    <mx-gas-price> GasPrice:Int </mx-gas-price>
+                    ...
+                </mx-call-data>
+            )
+        => newExecutionEnvironment(Destination)
+            ~> mkCall
+                ( getCallFunc(Func, Args)
+                , mkCallDataEsdtExec(Sender, Destination, Func, Args, Gas, GasPrice)
+                )
+      requires getCallFunc(Func, Args) =/=K ""
+
+
+    syntax MxCallDataCell ::= mkCallDataEsdtExec
+        (caller: String, callee: String
+        , transferFunction: BuiltinFunction
+        , args: MxValueList, gas: Int, gasPrice: Int)
+        [function, total]
+  // -----------------------------------------------------------------------------------
+    rule mkCallDataEsdtExec
+            (... caller: Caller:String
+            , callee: Callee:String
+            , transferFunction: Function:BuiltinFunction
+            , args: Args:MxValueList
+            , gas: Gas:Int, gasPrice: GasPrice:Int
+            )
+        =>  <mx-call-data>
+                <mx-callee> Callee </mx-callee>
+                <mx-caller> Caller </mx-caller>
+                <mx-call-args> getCallArgs(Function, Args) </mx-call-args>
+                <mx-egld-value> 0 </mx-egld-value>
+                <mx-esdt-transfers> parseESDTTransfers(Function, Args) </mx-esdt-transfers>
+                <mx-gas-provided> Gas </mx-gas-provided>
+                <mx-gas-price> GasPrice </mx-gas-price>
+            </mx-call-data>
+
+    syntax MxValueList ::= getCallArgs(BuiltinFunction, MxValueList)  [function, total]
+  // -------------------------------------------------------------------------------
+    rule getCallArgs(#ESDTTransfer, Args:MxValueList)
+        => drop(3, Args) // drop token, amount, func
+    rule getCallArgs(_, _) => .MxValueList  [owise]
+
+    syntax MxValueList ::= drop(Int, MxValueList)  [function, total]
+  // -------------------------------------------------------------------------------
+    rule drop(N:Int, Vs:MxValueList) => Vs
+        requires N <=Int 0
+    rule drop(N:Int, (_V:MxValue ,  Vs:MxValueList)) => drop(N -Int 1, Vs)
+        requires 0 <Int N
+
+
     syntax String ::= getCallFunc(BuiltinFunction, MxValueList)  [function, total]
   // --------------------------------------------------------------------------
-    rule getCallFunc(#ESDTTransfer,    ARGS) => getArgString(ARGS, 2) // token&amount&func&...
+    rule getCallFunc(#ESDTTransfer,    Args) => getArgString(Args, 2) // token&amount&func&...
     // rule getCallFunc(#ESDTNFTTransfer, ARGS) => getArgString(ARGS, 4) // token&nonce&amount&dest&func&...
     // rule getCallFunc(#MultiESDTNFTTransfer, ARGS)
     //     => getArg(ARGS, MultiESDTNFTTransfer.num(ARGS) *Int 3 +Int 2)
@@ -214,8 +279,9 @@ module MX-CALLS-TOOLS
   // ------------------------------------------------------
     rule [finishExecuteOnDestContext-ok]:
         <k> finishExecuteOnDestContext => mxIntValue(0) ... </k>
-        <mx-call-result> mxCallResult(... returnCode: OK) => .MxCallResult </mx-call-result>
- 
+        <mx-call-result> mxCallResult(... returnCode: OK, out: Value:MxValue) => .MxCallResult </mx-call-result>
+        <mx-return-values> .MxValueList => Value , .MxValueList </mx-return-values>
+
     rule [finishExecuteOnDestContext-exception]:
         <k> finishExecuteOnDestContext => resolveErrorFromOutput(EC, MSG) ... </k>
         <mx-call-result> mxCallResult(... returnCode: EC:ExceptionCode, returnMessage: MSG) => .MxCallResult </mx-call-result>
@@ -250,7 +316,7 @@ module MX-CALLS-TOOLS
             ~> popCallState
             ~> dropWorldState
 
-    rule [setVMOutput]:
+    rule [setVMOutput-no-retv]:
         <k> setVMOutput => .K ... </k>
         <mx-call-result>
             _ => mxCallResult
@@ -259,6 +325,34 @@ module MX-CALLS-TOOLS
                     , out: mxUnitValue()
                     )
         </mx-call-result>
+        <mx-return-values> .MxValueList </mx-return-values>
+
+    rule [setVMOutput-with-retv]:
+        <k> setVMOutput => .K ... </k>
+        <mx-call-result>
+            _ => mxCallResult
+                    (... returnCode: OK
+                    , returnMessage: ""
+                    , out: ReturnValue
+                    )
+        </mx-call-result>
+        <mx-return-values> ReturnValue:MxValue , .MxValueList => .MxValueList </mx-return-values>
+
+
+    rule
+        <k>
+            mkCall
+                (... function: FunctionName:String
+                , callData: CallData:MxCallDataCell
+                )
+            => clearBigInts ~> host.mkCall(FunctionName)
+            ...
+        </k>
+        (_:MxCallDataCell => CallData)
+
+    rule
+        <k> returnCallData(V:MxValue) => .K ... </k>
+        <mx-return-values> .MxValueList => V , .MxValueList </mx-return-values>
 
     // TODO: Not implemented.
     rule asyncExecute => .K