FxDAO test (#23)

* Add simple FxDAO test

* fix typo in `sixBitStringTable`

* update test_fxdao

* add `SCBytes` constructor

* add child contracts and init function support

* update tests

* Set Version: 0.1.23

* add `test_get_core_state`

* implement `vec_new` for test_get_core_state

* partially implement `obj_cmp` for `test_get_core_state`

* Set Version: 0.1.26

* fix: rename variable missed during merge

---------

Co-authored-by: devops <[email protected]>

package/version

@@ -1 +1 @@
-0.1.25
+0.1.26

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "komet"
-version = "0.1.25"
+version = "0.1.26"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/komet/kasmer.py

@@ -24,12 +24,14 @@
 from pykwasm.wasm2kast import wasm2kast
 
 from .kast.syntax import (
+    SC_VOID,
     STEPS_TERMINATOR,
     account_id,
     call_tx,
     contract_id,
     deploy_contract,
     sc_bool,
+    sc_bytes,
     set_account,
     set_exit_code,
     steps_of,
@@ -130,20 +132,37 @@ def kast_from_wasm(self, wasm: Path) -> KInner:
         return wasm2kast(open(wasm, 'rb'))
 
     @staticmethod
-    def deploy_test(contract: KInner) -> tuple[KInner, dict[str, KInner]]:
+    def deploy_test(
+        contract: KInner, child_contracts: tuple[KInner, ...], init: bool
+    ) -> tuple[KInner, dict[str, KInner]]:
         """Takes a wasm soroban contract as a kast term and deploys it in a fresh configuration.
 
         Returns:
             A configuration with the contract deployed.
         """
 
+        def wasm_hash(i: int) -> bytes:
+            return str(i).rjust(32, '_').encode()
+
+        def call_init() -> tuple[KInner, ...]:
+            hashes = tuple(wasm_hash(i) for i in range(len(child_contracts)))
+            upload_wasms = tuple(upload_wasm(h, c) for h, c in zip(hashes, child_contracts, strict=False))
+
+            from_addr = account_id(b'test-account')
+            to_addr = contract_id(b'test-contract')
+            args = [sc_bytes(h) for h in hashes]
+            init_tx = call_tx(from_addr, to_addr, 'init', args, SC_VOID)
+
+            return upload_wasms + (init_tx,)
+
         # Set up the steps that will deploy the contract
         steps = steps_of(
             [
                 set_exit_code(1),
                 upload_wasm(b'test', contract),
                 set_account(b'test-account', 9876543210),
                 deploy_contract(b'test-account', b'test-contract', b'test'),
+                *(call_init() if init else ()),
                 set_exit_code(0),
             ]
         )
@@ -209,7 +228,7 @@ def make_steps(*args: KInner) -> KInner:
 
         return run_claim(name, claim, proof_dir)
 
-    def deploy_and_run(self, contract_wasm: Path) -> None:
+    def deploy_and_run(self, contract_wasm: Path, child_wasms: tuple[Path, ...]) -> None:
         """Run all of the tests in a soroban test contract.
 
         Args:
@@ -220,21 +239,28 @@ def deploy_and_run(self, contract_wasm: Path) -> None:
         """
         print(f'Processing contract: {contract_wasm.stem}')
 
+        bindings = self.contract_bindings(contract_wasm)
+        has_init = 'init' in (b.name for b in bindings)
+
         contract_kast = self.kast_from_wasm(contract_wasm)
-        conf, subst = self.deploy_test(contract_kast)
+        child_kasts = tuple(self.kast_from_wasm(c) for c in child_wasms)
 
-        bindings = [b for b in self.contract_bindings(contract_wasm) if b.name.startswith('test_')]
+        conf, subst = self.deploy_test(contract_kast, child_kasts, has_init)
 
-        print(f'Discovered {len(bindings)} test functions:')
-        for binding in bindings:
+        test_bindings = [b for b in bindings if b.name.startswith('test_')]
+
+        print(f'Discovered {len(test_bindings)} test functions:')
+        for binding in test_bindings:
             print(f'    - {binding.name}')
 
-        for binding in bindings:
+        for binding in test_bindings:
             print(f'\n  Running {binding.name}...')
             self.run_test(conf, subst, binding)
             print('    Test passed.')
 
-    def deploy_and_prove(self, contract_wasm: Path, proof_dir: Path | None = None) -> None:
+    def deploy_and_prove(
+        self, contract_wasm: Path, child_wasms: tuple[Path, ...], proof_dir: Path | None = None
+    ) -> None:
         """Prove all of the tests in a soroban test contract.
 
         Args:
@@ -244,10 +270,13 @@ def deploy_and_prove(self, contract_wasm: Path, proof_dir: Path | None = None) -
         Raises:
             KSorobanError if a proof fails
         """
+        bindings = self.contract_bindings(contract_wasm)
+        has_init = 'init' in (b.name for b in bindings)
+
         contract_kast = self.kast_from_wasm(contract_wasm)
-        conf, subst = self.deploy_test(contract_kast)
+        child_kasts = tuple(self.kast_from_wasm(c) for c in child_wasms)
 
-        bindings = self.contract_bindings(contract_wasm)
+        conf, subst = self.deploy_test(contract_kast, child_kasts, has_init)
 
         for binding in bindings:
             if not binding.name.startswith('test_'):

src/komet/kast/syntax.py

@@ -2,7 +2,7 @@
 
 from typing import TYPE_CHECKING
 
-from pyk.kast.inner import KApply, KSort, KToken, build_cons
+from pyk.kast.inner import KApply, build_cons
 from pyk.prelude.collections import list_of, map_of
 from pyk.prelude.utils import token
 from pykwasm.kwasm_ast import wasm_string
@@ -91,6 +91,10 @@ def sc_symbol(s: str) -> KInner:
     return KApply('SCVal:Symbol', [token(s)])
 
 
+def sc_bytes(b: bytes) -> KInner:
+    return KApply('SCVal:Bytes', [token(b)])
+
+
 def sc_vec(l: Iterable[KInner]) -> KInner:
     return KApply('SCVal:Vec', list_of(l))
 
@@ -99,4 +103,4 @@ def sc_map(m: dict[KInner, KInner] | Iterable[tuple[KInner, KInner]]) -> KInner:
     return KApply('SCVal:Map', map_of(m))
 
 
-SC_VOID: Final = KToken('Void', KSort('ScVal'))
+SC_VOID: Final = KApply('SCVal:Void', ())

src/komet/kdist/soroban-semantics/data.md

@@ -266,7 +266,7 @@ module HOST-OBJECT
 
     syntax String ::= "sixBitStringTable" [macro]
  // -------------------------------------------------------------------------------------------
-    rule sixBitStringTable => "_0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefgyahijklmnopqrstuvwxyz"
+    rule sixBitStringTable => "_0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"
 
     syntax String ::= decode6bitChar(Int)   [function, total, symbol(decode6bitChar)]
  // ---------------------------------------------------------------------------------

src/komet/kdist/soroban-semantics/host/context.md

@@ -7,6 +7,46 @@ module HOST-CONTEXT
     imports HOST-INTEGER
 ```
 
+## obj_cmp
+
+```k
+    rule [hostfun-obj-cmp]:
+        <instrs> hostCall ( "x" , "0" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObjectFull(HostVal(OBJ_B))
+              ~> loadObjectFull(HostVal(OBJ_A))
+              ~> objCmp
+                 ...
+        </instrs>
+        <locals>
+            0 |-> <i64> OBJ_A
+            1 |-> <i64> OBJ_B
+        </locals>
+
+    // TODO This only works for addresses. Implement it properly for other cases.
+    // https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#comparison
+    syntax InternalInstr ::= "objCmp"   [symbol(objCmp)]
+ // ----------------------------------------------------
+    rule [objCmp-equal]:
+        <instrs> objCmp => i64.const compareAddress(A, B) ... </instrs>
+        <hostStack> ScAddress(A) : ScAddress(B) : S => S </hostStack>
+
+    syntax Int ::= compareAddress(Address, Address)    [function, total, symbol(compareAddress)]
+ // -------------------------------------------------------------------------------------
+    rule compareAddress(Account(_),  Contract(_)) => -1
+    rule compareAddress(Contract(_), Account(_))  => 1
+    rule compareAddress(Contract(A), Contract(B)) => compareBytes(A, B)
+    rule compareAddress(Account(A),  Account(B))  => compareBytes(A, B)
+
+    syntax Int ::= compareBytes(Bytes, Bytes)       [function, total, symbol(compareBytes)]
+                 | compareString(String, String)    [function, total, symbol(compareString)]
+ // -------------------------------------------------------------------------------------
+    rule compareBytes(A, B) => compareString(Bytes2String(A), Bytes2String(B))
+    rule compareString(A, B) => -1 requires A  <String B
+    rule compareString(A, B) =>  0 requires A ==String B
+    rule compareString(A, B) =>  1 requires A  >String B
+
+```
+
 ## get_ledger_sequence
 
 Return the current ledger sequence number as `U32`.

src/komet/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/komet/komet.py

@@ -1,5 +1,6 @@
 from __future__ import annotations
 
+import json
 import sys
 from argparse import ArgumentParser, FileType
 from contextlib import contextmanager
@@ -14,7 +15,7 @@
 from pyk.ktool.krun import _krun
 from pyk.proof.reachability import APRProof
 from pyk.proof.tui import APRProofViewer
-from pyk.utils import ensure_dir_path
+from pyk.utils import abs_or_rel_to, ensure_dir_path
 from pykwasm.scripts.preprocessor import preprocess
 
 from .kasmer import Kasmer
@@ -25,6 +26,9 @@
     from subprocess import CompletedProcess
 
 
+sys.setrecursionlimit(4000)
+
+
 class Backend(Enum):
     LLVM = 'llvm'
     HASKELL = 'haskell'
@@ -80,28 +84,46 @@ def _exec_test(*, wasm: Path | None) -> None:
     """
     kasmer = Kasmer(concrete_definition)
 
+    child_wasms: tuple[Path, ...] = ()
+
     if wasm is None:
         # We build the contract here, specifying where it's saved so we know where to find it.
         # Knowing where the compiled contract is saved by default when building it would eliminate
         # the need for this step, but at the moment I don't know how to retrieve that information.
         wasm = kasmer.build_soroban_contract(Path.cwd())
+        child_wasms = _read_config_file()
 
-    kasmer.deploy_and_run(wasm)
+    kasmer.deploy_and_run(wasm, child_wasms)
 
     sys.exit(0)
 
 
 def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None) -> None:
     kasmer = Kasmer(symbolic_definition)
 
+    child_wasms: tuple[Path, ...] = ()
+
     if wasm is None:
         wasm = kasmer.build_soroban_contract(Path.cwd())
+        child_wasms = _read_config_file()
 
-    kasmer.deploy_and_prove(wasm, proof_dir)
+    kasmer.deploy_and_prove(wasm, child_wasms, proof_dir)
 
     sys.exit(0)
 
 
+def _read_config_file(dir_path: Path | None = None) -> tuple[Path, ...]:
+    dir_path = Path.cwd() if dir_path is None else dir_path
+    config_path = dir_path / 'kasmer.json'
+
+    if config_path.is_file():
+        with open(config_path) as f:
+            config = json.load(f)
+            return tuple(abs_or_rel_to(Path(c), dir_path) for c in config['contracts'])
+
+    return ()
+
+
 def _exec_prove_view(*, proof_dir: Path, id: str) -> None:
     proof = APRProof.read_proof_data(proof_dir, id)
     viewer = APRProofViewer(proof, symbolic_definition.krun)

src/komet/scval.py

@@ -11,6 +11,7 @@
 
 from .kast.syntax import (
     sc_bool,
+    sc_bytes,
     sc_i32,
     sc_i64,
     sc_i128,
@@ -111,6 +112,14 @@ def to_kast(self) -> KInner:
         return sc_symbol(self.val)
 
 
+@dataclass(frozen=True)
+class SCBytes(SCValue):
+    val: bytes
+
+    def to_kast(self) -> KInner:
+        return sc_bytes(self.val)
+
+
 @dataclass(frozen=True)
 class SCVec(SCValue):
     val: tuple[SCValue]
@@ -140,6 +149,7 @@ def to_kast(self) -> KInner:
     'u128': 'SCU128Type',
     'u256': 'SCU256Type',
     'symbol': 'SCSymbolType',
+    'bytes': 'SCBytesType',
     'vec': 'SCVecType',
     'map': 'SCMapType',
 }
@@ -310,6 +320,16 @@ def as_var(cls, name: str) -> tuple[KInner, tuple[KInner, ...]]:
         return KApply('SCVal:Symbol', [KVariable(name, KSort('String'))]), ()
 
 
+@dataclass
+class SCBytesType(SCMonomorphicType):
+    def strategy(self) -> SearchStrategy:
+        return strategies.binary().map(SCBytes)
+
+    @classmethod
+    def as_var(cls, name: str) -> tuple[KInner, tuple[KInner, ...]]:
+        return KApply('SCVal:Bytes', [KVariable(name, KSort('Bytes'))]), ()
+
+
 @dataclass
 class SCVecType(SCType):
     element: SCType

src/tests/integration/data/soroban/contracts/test_fxdao/Cargo.toml

@@ -0,0 +1,15 @@
+[package]
+name = "test_fxdao"
+version = "0.0.0"
+edition = "2021"
+publish = false
+
+[lib]
+crate-type = ["cdylib"]
+doctest = false
+
+[dependencies]
+soroban-sdk = { workspace = true }
+
+[dev-dependencies]
+soroban-sdk = { workspace = true, features = ["testutils"] }