managedDeployFromSourceContract

runtimeverification · Aug 7, 2023 · db42449 · db42449
1 parent 3fc73fb
commit db42449
Show file tree

Hide file tree

Showing 7 changed files with 165 additions and 22 deletions.
diff --git a/Makefile b/Makefile
@@ -47,7 +47,7 @@ else
 endif
 K_BIN := $(K_RELEASE)/bin
 K_LIB := $(K_RELEASE)/lib/kframework
-export K_OPTS ?= -Xmx20G -Xss512m
+export K_OPTS ?= -Xmx24G -Xss512m
 export K_RELEASE
 
 PYTHONPATH := $(K_LIB):$(KWASM_BINARY_PARSER):$(PYTHONPATH)

diff --git a/elrond-config.md b/elrond-config.md
@@ -717,5 +717,64 @@ Initialize the call state and invoke the endpoint function:
       requires notBool( FUNCNAME in_keys(EXPORTS) )
       [priority(60)]
 
+```
+
+## Deploying Contract
+
+```k
+    syntax InternalCmd ::= deployContract(Bytes, Bytes, Code, Int, ListBytes, Int, Int, Bytes) [klabel(deployContractAux)]
+                         | deployContract(Bytes,        Code, Int, ListBytes, Int, Int, Bytes) [klabel(deployContract)]
+ // ----------------------------------------------------------------------------------------------------------------------
+    rule [deployContract]:
+        <commands> deployContract(FROM, MODULE, VAL, ARGS, GAS, GASPRICE, HASH)
+                => deployContract(FROM, genNewAddress(FROM, NONCE), MODULE, VAL, ARGS, GAS, GASPRICE, HASH)
+                   ...
+        </commands>
+        <account>
+           <address> FROM </address>
+           <nonce> NONCE </nonce>
+           ...
+        </account>
+      [priority(60)]
+   
+
+    syntax Bytes ::= genNewAddress(Bytes, Int)    [function, total]
+ // ------------------------------------------------------------
+ // default address generation rule
+ // TODO implement the address generation formula from the Go implementation
+    rule genNewAddress(FROM, NONCE) => FROM +Bytes Int2Bytes(NONCE, BE, Signed)   [owise]
+
+    rule [deployContractAux]:
+        <commands> deployContract(FROM, NEWADDR, MODULE, VAL, ARGS, GAS, GASPRICE, HASH) 
+                => createAccount(NEWADDR)
+                ~> setAccountOwner(NEWADDR, FROM)
+                ~> setAccountCode(NEWADDR, MODULE)
+                ~> callContract(NEWADDR, "init", mkVmInputDeploy(FROM, VAL, ARGS, GAS, GASPRICE, HASH))
+                   ...
+        </commands>
+        <account>
+           <address> FROM </address>
+           <nonce> NONCE => NONCE +Int 1 </nonce>
+           <balance> BALANCE => BALANCE -Int GAS *Int GASPRICE </balance>
+           ...
+        </account>
+      [priority(60)]
+
+
+    syntax VmInputCell ::= mkVmInputDeploy(Bytes, Int, ListBytes, Int, Int, Bytes)    [function, total]
+ // -----------------------------------------------------------------------------------
+    rule mkVmInputDeploy(FROM, VALUE, ARGS, GASLIMIT, GASPRICE, HASH)
+      => <vmInput>
+            <caller> FROM </caller>
+            <callArgs> ARGS </callArgs>
+            <callValue> VALUE </callValue>
+            <esdtTransfers> .List </esdtTransfers>
+            // gas
+            <gasProvided> GASLIMIT </gasProvided>
+            <gasPrice> GASPRICE </gasPrice>
+            // hash
+            <originalTxHash> HASH </originalTxHash>
+          </vmInput>
+
 endmodule
 ```
diff --git a/mandos.md b/mandos.md
@@ -427,34 +427,18 @@ TODO make sure that none of the state changes are persisted -- [Doc](https://doc
     rule [deployTxAux]:
         <k> deployTxAux(FROM, VALUE, MODULE, ARGS, GASLIMIT, GASPRICE, HASH) => #wait ... </k>
         <commands> . 
-                => createAccount(NEWADDR)
-                ~> setAccountOwner(NEWADDR, FROM)
-                ~> setAccountCode(NEWADDR, MODULE)
-                ~> callContract(NEWADDR, "init", mkVmInputDeploy(FROM, VALUE, ARGS, GASLIMIT, GASPRICE, HASH))
+                => deployContract(FROM, MODULE, VALUE, ARGS, GASLIMIT, GASPRICE, HASH) 
         </commands>
+      [priority(60)]
+
+    rule [[ genNewAddress(FROM, NONCE) => NEWADDR ]]
         <account>
            <address> FROM </address>
-           <nonce> NONCE => NONCE +Int 1 </nonce>
-           <balance> BALANCE => BALANCE -Int GASLIMIT *Int GASPRICE </balance>
+           <nonce> NONCE</nonce>
            ...
         </account>
         <newAddresses> ... tuple(FROM, NONCE) |-> NEWADDR:Bytes ... </newAddresses>
-      [priority(60)]
 
-    syntax VmInputCell ::= mkVmInputDeploy(Bytes, Int, ListBytes, Int, Int, Bytes)    [function, total]
- // -----------------------------------------------------------------------------------
-    rule mkVmInputDeploy(FROM, VALUE, ARGS, GASLIMIT, GASPRICE, HASH)
-      => <vmInput>
-            <caller> FROM </caller>
-            <callArgs> ARGS </callArgs>
-            <callValue> VALUE </callValue>
-            <esdtTransfers> .List </esdtTransfers>
-            // gas
-            <gasProvided> GASLIMIT </gasProvided>
-            <gasPrice> GASPRICE </gasPrice>
-            // hash
-            <originalTxHash> HASH </originalTxHash>
-          </vmInput>
 ```
 
 ### Step type: transfer

diff --git a/tests/multisig.test b/tests/multisig.test
@@ -1,3 +1,9 @@
 deps/mx-sdk-rs/contracts/examples/multisig/scenarios/changeBoard.scen.json
 deps/mx-sdk-rs/contracts/examples/multisig/scenarios/changeQuorum.scen.json
 deps/mx-sdk-rs/contracts/examples/multisig/scenarios/changeQuorum_tooBig.scen.json
+deps/mx-sdk-rs/contracts/examples/multisig/scenarios/deploy_duplicate_bm.scen.json
+deps/mx-sdk-rs/contracts/examples/multisig/scenarios/deployAdder_err.scen.json 
+deps/mx-sdk-rs/contracts/examples/multisig/scenarios/deployAdder_then_call.scen.json 
+deps/mx-sdk-rs/contracts/examples/multisig/scenarios/deployFactorial.scen.json 
+deps/mx-sdk-rs/contracts/examples/multisig/scenarios/deployOtherMultisig.scen.json
+deps/mx-sdk-rs/contracts/examples/multisig/scenarios/remove_everyone.scen.json
diff --git a/tests/simple/bad-bounds.wast b/tests/simple/bad-bounds.wast
@@ -147,6 +147,7 @@ callTx(
   , ListItem(Int2Bytes(1, BE, Signed)) ListItem(Int2Bytes(123, BE, Unsigned))
   , 0
   , 0
+  , b""
 )
 
 checkExpectStatus(OK)
@@ -162,6 +163,7 @@ callTx(
   , ListItem(Int2Bytes(1, BE, Signed))
   , 0
   , 0
+  , b""
 )
 
 checkExpectStatus(ExecutionFailed)
@@ -177,6 +179,7 @@ callTx(
   , ListItem(Int2Bytes(-1, BE, Signed)) ListItem(Int2Bytes(123, BE, Unsigned))
   , 0
   , 0
+  , b""
 )
 
 checkExpectStatus(ExecutionFailed)
@@ -193,6 +196,7 @@ callTx(
     ListItem(Int2Bytes(maxUInt64 +Int 5, BE, Unsigned))
   , 0
   , 0
+  , b""
 )
 
 checkExpectStatus(UserError)

diff --git a/vmhooks/baseOps.md b/vmhooks/baseOps.md
@@ -310,6 +310,10 @@ module BASEOPS
     rule <instrs> #signalError => #throwExceptionBs(UserError, DATA) ... </instrs>
          <bytesStack> DATA : STACK => STACK </bytesStack>
 
+   // extern long long getGasLeft(void *context);
+    rule [getGasLeft]:
+        <instrs> hostCall("env", "getGasLeft", [ .ValTypes ] -> [ i64 .ValTypes ]) => i64.const maxSInt64 ... </instrs>
+
     // extern long long getBlockTimestamp(void *context);
     rule <instrs> hostCall("env", "getBlockTimestamp", [ .ValTypes ] -> [ i64 .ValTypes ]) => i64.const TIMESTAMP ... </instrs>
          <curBlockTimestamp> TIMESTAMP </curBlockTimestamp>

diff --git a/vmhooks/managedei.md b/vmhooks/managedei.md
@@ -125,5 +125,91 @@ module MANAGEDEI
         <locals> 0 |-> <i32> BUF_IDX </locals>
         <originalTxHash> HASH </originalTxHash>
 
+ // extern int32_t managedDeployFromSourceContract(void*, long long gas, int32_t valHandle, int32_t addrHandle, int32_t codeMetaHandle, int32_t argsHandle, int32_t resAddrHandle, int32_t resHandle);
+    rule [managedDeployFromSourceContract]:
+        <instrs> hostCall("env", "managedDeployFromSourceContract",
+                          [i64 i32 i32 i32 i32 i32 i32 .ValTypes] -> [i32 .ValTypes ] )
+              => #deployFromSourceContractAux(
+                    getBuffer(ADDR_IDX), 
+                    getBigInt(VAL_IDX),
+                    readManagedVecOfManagedBuffers(ARGS_IDX), 
+                    GAS
+                  )
+              ~> #setBuffer(RES_ADDR_IDX, genNewAddress(CALLEE, NONCE))
+              ~> #setReturnDataIfExists(size(OUT), RES_IDX)
+              ~> i32.const 0
+                 ...
+        </instrs>
+        <locals>
+          0 |-> <i64> GAS
+          1 |-> <i32> VAL_IDX
+          2 |-> <i32> ADDR_IDX
+          3 |-> <i32> _ // TODO use code metadata handle
+          4 |-> <i32> ARGS_IDX
+          5 |-> <i32> RES_ADDR_IDX
+          6 |-> <i32> RES_IDX
+        </locals>
+        <out> OUT </out>
+        <callee> CALLEE </callee>
+        <account>
+           <address> CALLEE </address>
+           <nonce> NONCE </nonce>
+           ...
+        </account>
+
+    syntax InternalInstr ::= #setReturnDataIfExists(Int, Int) // oldLen, resHandle
+ // -----------------------------------------------------------
+    rule [setReturnDataIfExists]:
+        <instrs> #setReturnDataIfExists(OldLen, DestHandle)
+              => #setBuffer(DestHandle, .Bytes) ... // TODO implement WriteManagedVecOfManagedBuffers
+        </instrs>
+        <out> OUTPUT </out>
+      requires size(OUTPUT) >Int OldLen
+
+    rule [setReturnDataIfExists-nil]:
+        <instrs> #setReturnDataIfExists(OldLen, DestHandle)
+              => #setBuffer(DestHandle, .Bytes) ...
+        </instrs>
+        <out> OUTPUT </out>
+      requires size(OUTPUT) <=Int OldLen
+    
+    syntax InternalInstr ::= #deployFromSourceContractAux(BytesResult, IntResult, ListBytesResult, Int)
+                           | #deployFromSourceContract(Bytes, Int, ListBytes, Int)
+ // --------------------------------------------------------------------------------------------------
+    rule [deployFromSourceContractAux]:
+        <instrs> #deployFromSourceContractAux(SRC_ADDR:Bytes, VAL:Int, ARGS:ListBytes, GAS:Int)
+              => #deployFromSourceContract(SRC_ADDR, VAL, ARGS, GAS) ...
+        </instrs>
+
+    rule [deployFromSourceContractAux-err]:
+        <instrs> #deployFromSourceContractAux(_,_,_,_)
+              => #throwException(ExecutionFailed, "managedDeployFromSourceContract: argument parsing failed") ...
+        </instrs>
+      [owise]
+
+    rule [deployFromSourceContract]:
+        <instrs> #deployFromSourceContract(SRC_ADDR, VAL, ARGS, GAS)
+              => #finishExecuteOnDestContext  // wait for the 'init' function
+              ~> drop
+                 ...
+        </instrs>
+        <commands> (. => deployContract(FROM, CODE, VAL, ARGS, GAS, GASPRICE, HASH)) ... </commands>
+        <account>
+          <address> SRC_ADDR </address>
+          <code> CODE:ModuleDecl </code>
+          ...
+        </account>
+        <callee> FROM </callee>
+        <gasPrice> GASPRICE </gasPrice>
+        <originalTxHash> HASH </originalTxHash>
+
+    rule [deployFromSourceContract-notfound]:
+        <instrs> #deployFromSourceContract(SRC_ADDR, _, _, _)
+              => #throwExceptionBs(ExecutionFailed, b"source contract not found: " +Bytes SRC_ADDR) ...
+        </instrs>
+      [owise]
+        
+        
+
 endmodule
 ```