implement vec_new for test_get_core_state

src/ksoroban/kdist/soroban-semantics/host/vector.md

@@ -10,8 +10,23 @@ module HOST-VECTOR
     imports WASM-OPERATIONS
     imports HOST-INTEGER
     imports SWITCH-SYNTAX
+```
 
-    // vec_unpack_to_linear_memory
+## vec_new
+
+```k
+    rule [hostfun-vec-new]:
+        <instrs> hostCall ( "v" , "_" , [ .ValTypes ] -> [ i64  .ValTypes ] )
+              => allocObject(ScVec(.List))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <locals> .Map </locals>
+```
+
+## vec_unpack_to_linear_memory
+
+```k
     rule [hostfun-vec-unpack-to-linear-memory]:
         <instrs> hostCall ( "v" , "h" , [ i64  i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
               => loadObject(HostVal(LEN))
@@ -61,8 +76,7 @@ module HOST-VECTOR
         <hostStack> U32(VALS_POS) : U32(LEN) : S => S </hostStack>
 
     rule [vecNewFromLinearMemoryAux]:
-        <instrs> vecNewFromLinearMemoryAux => #waitCommands ... </instrs>
-        <k> (.K => allocObject(ScVec(Bytes2Vals(BS)))) ... </k>
+        <instrs> vecNewFromLinearMemoryAux => allocObject(ScVec(Bytes2Vals(BS))) ... </instrs>
         <hostStack> BS : S => S </hostStack>
 
 

src/tests/integration/data/vec.wast

@@ -0,0 +1,28 @@
+
+setExitCode(1)
+
+uploadWasm( b"test-wasm",
+(module
+  (import "v" "_" (func $vec_new (result i64)))
+  (func $create_vec (result i64)
+    call $vec_new)
+  (export "create_vec" (func $create_vec)))
+)
+
+setAccount(Account(b"test-account"), 9876543210)
+
+deployContract(
+  Account(b"test-account"),
+  Contract(b"test-sc"),
+  b"test-wasm"
+)
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "create_vec",
+  .List,
+  ScVec(.List)
+)
+
+setExitCode(0)