Remove automatic call to init function during contract deployment (#22)

* Remove automatic call to `init` function during `deployContract` * Adjust tests * Set Version: 0.1.17 * Set Version: 0.1.21 * fix wast tests deploy commands --------- Co-authored-by: devops <[email protected]>
runtimeverification · Aug 15, 2024 · d73500d · d73500d
1 parent 2ef6bf9
commit d73500d
Show file tree

Hide file tree

Showing 19 changed files with 21 additions and 60 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.20
+0.1.21
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "ksoroban"
-version = "0.1.20"
+version = "0.1.21"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/ksoroban/kast/syntax.py b/src/ksoroban/kast/syntax.py
@@ -40,9 +40,8 @@ def upload_wasm(name: bytes, contract: KInner) -> KInner:
     return KApply('uploadWasm', [token(name), contract])
 
 
-def deploy_contract(from_addr: bytes, address: bytes, wasm_hash: bytes, args: list[KInner] | None = None) -> KInner:
-    args = args if args is not None else []
-    return KApply('deployContract', [account_id(from_addr), contract_id(address), token(wasm_hash), list_of(args)])
+def deploy_contract(from_addr: bytes, address: bytes, wasm_hash: bytes) -> KInner:
+    return KApply('deployContract', [account_id(from_addr), contract_id(address), token(wasm_hash)])
 
 
 def call_tx(from_addr: KInner, to_addr: KInner, func: str, args: Iterable[KInner], result: KInner) -> KInner:

diff --git a/src/ksoroban/kdist/soroban-semantics/kasmer.md b/src/ksoroban/kdist/soroban-semantics/kasmer.md
@@ -20,7 +20,7 @@ module KASMER-SYNTAX-COMMON
     syntax Step ::= setExitCode(Int)                                                                     [symbol(setExitCode)]
                   | setAccount( address: AccountId, balance: Int)                                        [symbol(setAccount)]
                   | uploadWasm(Bytes, ModuleDecl)                                                        [symbol(uploadWasm)]
-                  | deployContract( from: Address, address: ContractId, wasmHash: Bytes, args: List )    [symbol(deployContract)]
+                  | deployContract( from: Address, address: ContractId, wasmHash: Bytes )                [symbol(deployContract)]
                   | callTx( from: Address, to: Address, func: WasmString, args: List, result: ScVal)     [symbol(callTx)]
 
 
@@ -104,7 +104,7 @@ module KASMER
 
  // -----------------------------------------------------------------------------------------------------------------------
     rule [deployContract-existing]:
-        <k> deployContract(_OWNER, ADDR, _WASM_HASH, _ARGS) => #hostTrap ... </k>
+        <k> deployContract(_OWNER, ADDR, _WASM_HASH) => #hostTrap ... </k>
         <contract>
            <contractId> ADDR </contractId>
            ...
@@ -114,12 +114,7 @@ module KASMER
     syntax HostCell
 
     rule [deployContract]:
-        <k> deployContract(OWNER, ADDR, WASM_HASH, ARGS)
-         => allocObjects(ARGS)
-         ~> callContractFromStack(OWNER, ADDR, #quoteUnparseWasmString("init"))
-         ~> #resetHost
-            ...
-        </k>
+        <k> deployContract(_OWNER, ADDR, WASM_HASH) => .K ... </k>
         ( .Bag =>
           <contract>
             <contractId> ADDR </contractId>

diff --git a/src/ksoroban/kdist/soroban-semantics/soroban.md b/src/ksoroban/kdist/soroban-semantics/soroban.md
@@ -129,25 +129,6 @@ module SOROBAN
         requires isListIndex(FUNCIDX, FUNCADDRS)
       [priority(60)]
 
-    rule [mkCall-no-init]:
-        <k> mkCall(_FROM, _TO, FUNCNAME:WasmStringToken, .List) => .K ... </k>
-        <callState>
-          <wasm>
-            <instrs> .K </instrs>
-            <moduleInst>
-              <modIdx> MODIDX </modIdx>
-              <exports> EXPORTS </exports>
-              ...
-            </moduleInst>
-            ...
-          </wasm>
-          <contractModIdx> MODIDX:Int </contractModIdx>
-          ...
-        </callState>
-        requires notBool (FUNCNAME in_keys(EXPORTS))
-         andBool #parseWasmString(FUNCNAME) ==K "\"init\""
-      [priority(60)]
-
     syntax InternalInstr ::= pushArgs(List)      [symbol(pushArgs)]
                            | pushArg(HostVal)    [symbol(pushArg)]
  // ---------------------------------------------------------------------

diff --git a/src/tests/integration/data/add_i32.wast b/src/tests/integration/data/add_i32.wast
@@ -77,8 +77,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"calculator"),
-  b"arith",
-  .List
+  b"arith"
 )
 
 callTx(

diff --git a/src/tests/integration/data/add_u128.wast b/src/tests/integration/data/add_u128.wast
@@ -192,8 +192,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"calculator"),
-  b"arith",
-  .List
+  b"arith"
 )
 
 callTx(

diff --git a/src/tests/integration/data/add_u32.wast b/src/tests/integration/data/add_u32.wast
@@ -71,8 +71,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"calculator"),
-  b"arith",
-  .List
+  b"arith"
 )
 
 callTx(

diff --git a/src/tests/integration/data/add_u64.wast b/src/tests/integration/data/add_u64.wast
@@ -140,8 +140,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"calculator"),
-  b"arith",
-  .List
+  b"arith"
 )
 
 callTx(

diff --git a/src/tests/integration/data/errors.wast b/src/tests/integration/data/errors.wast
@@ -122,8 +122,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"test-sc"),
-  b"test-wasm",
-  .List
+  b"test-wasm"
 )
 
 callTx(

diff --git a/src/tests/integration/data/extend_ttl.wast b/src/tests/integration/data/extend_ttl.wast
@@ -62,8 +62,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"test-sc"),
-  b"test-wasm",
-  .List
+  b"test-wasm"
 )
 
 callTx(

diff --git a/src/tests/integration/data/increment.wast b/src/tests/integration/data/increment.wast
@@ -127,8 +127,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"test-sc"),
-  b"test-wasm",
-  .List
+  b"test-wasm"
 )
 
 ;; assert_eq!(client.increment(&true), 1);

diff --git a/src/tests/integration/data/increment_panic.wast b/src/tests/integration/data/increment_panic.wast
@@ -182,8 +182,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"test-sc"),
-  b"test-wasm",
-  .List
+  b"test-wasm"
 )
 
 callTx(

diff --git a/src/tests/integration/data/ledger_sequence_get_set.wast b/src/tests/integration/data/ledger_sequence_get_set.wast
@@ -74,8 +74,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"test-sc"),
-  b"test-wasm",
-  .List
+  b"test-wasm"
 )
 
 callTx(

diff --git a/src/tests/integration/data/struct_storage.wast b/src/tests/integration/data/struct_storage.wast
@@ -409,8 +409,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"test-ctr"),
-  b"test-wasm",
-  .List
+  b"test-wasm"
 )
 
 callTx(

diff --git a/src/tests/integration/data/structs.wast b/src/tests/integration/data/structs.wast
@@ -394,8 +394,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"test-ctr"),
-  b"test-wasm",
-  .List
+  b"test-wasm"
 )
 
 callTx(

diff --git a/src/tests/integration/data/symbol_small.wast b/src/tests/integration/data/symbol_small.wast
@@ -32,8 +32,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"test-sc"),
-  b"test-wasm",
-  .List
+  b"test-wasm"
 )
 
 callTx(

diff --git a/src/tests/integration/data/symbols.wast b/src/tests/integration/data/symbols.wast
@@ -152,8 +152,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"test-sc"),
-  b"test-wasm",
-  .List
+  b"test-wasm"
 )
 
 callTx(

diff --git a/src/tests/integration/data/tuple_to_vec.wast b/src/tests/integration/data/tuple_to_vec.wast
@@ -211,8 +211,7 @@ setAccount(Account(b"test-account"), 9876543210)
 deployContract(
   Account(b"test-account"),
   Contract(b"test-ctr"),
-  b"test-wasm",
-  .List
+  b"test-wasm"
 )
 
 callTx(