Contract calls (#74)

* Contract calls * Review fix: Rename module --------- Co-authored-by: ACassimiro <cassimiroaellison@gmail.com>
Pi-Squared-Inc · Sep 4, 2024 · 2c3287d · 2c3287d
1 parent 04a092e
commit 2c3287d
Show file tree

Hide file tree

Showing 19 changed files with 433 additions and 38 deletions.
diff --git a/mx-semantics/main/accounts/code-tools.md b/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
+
+```
diff --git a/mx-semantics/main/accounts/configuration.md b/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
+
 ```
diff --git a/mx-semantics/main/accounts/esdt-hooks.md b/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

diff --git a/mx-semantics/main/accounts/tools.md b/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

diff --git a/mx-semantics/main/biguint/tools.md b/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
+
+```
diff --git a/mx-semantics/main/call-state/configuration.md b/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-RETURN-VALUE-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
+
+```
diff --git a/mx-semantics/main/call-state/tools.md b/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
+
+```
diff --git a/mx-semantics/main/calls/configuration.md b/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-RETURN-VALUE-CONFIGURATION
+    imports MX-COMMON-SYNTAX
+
+    configuration
+        <mx-return-values> .MxValueList </mx-return-values>
+endmodule
+
 ```
diff --git a/mx-semantics/main/calls/hooks.md b/mx-semantics/main/calls/hooks.md
@@ -34,8 +34,33 @@ module MX-CALLS-HOOKS
             , mxStringValue(FunctionName:String)
             , mxListValue(Args:MxValueList)
             )
-        => executeOnDestContext(Destination, 0, Transfers, GasLimit, FunctionName, Args)
+        => executeOnDestContext
+            (... destination: Destination
+            , egldValue: 0
+            , esdtTransfers: Transfers
+            , gasLimit: GasLimit
+            , function: FunctionName
+            , args: 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: Destination
+            , egldValue: EgldValue
+            , esdtTransfers: Transfers
+            , gasLimit: GasLimit
+            , function: FunctionName
+            , args: Args
+            )
+
+    rule MX#finish ( V:MxValue ) => returnCallData(V)
 endmodule
 
 ```