diff --git a/package/version b/package/version index 0e24a92..7ac4e5e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.12 +0.1.13 diff --git a/pyproject.toml b/pyproject.toml index 03d0aa8..4773f4a 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "ksoroban" -version = "0.1.12" +version = "0.1.13" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/ksoroban/kasmer.py b/src/ksoroban/kasmer.py index 57115f4..84985bf 100644 --- a/src/ksoroban/kasmer.py +++ b/src/ksoroban/kasmer.py @@ -8,32 +8,36 @@ from tempfile import mkdtemp from typing import TYPE_CHECKING -from pyk.kast.inner import KSort +from hypothesis import strategies +from pyk.kast.inner import KSort, KVariable from pyk.kast.manip import Subst, split_config_from from pyk.konvert import kast_to_kore, kore_to_kast from pyk.kore.parser import KoreParser +from pyk.kore.syntax import EVar, SortApp +from pyk.ktool.kfuzz import fuzz from pyk.ktool.krun import KRunOutput from pyk.utils import run_process from pykwasm.wasm2kast import wasm2kast from .kast.syntax import ( - SC_VOID, account_id, call_tx, contract_id, deploy_contract, sc_bool, - sc_u32, set_account, set_exit_code, steps_of, upload_wasm, ) +from .scval import SCType if TYPE_CHECKING: from typing import Any + from hypothesis.strategies import SearchStrategy from pyk.kast.inner import KInner + from pyk.kore.syntax import Pattern from .utils import SorobanDefinitionInfo @@ -70,16 +74,15 @@ def contract_bindings(self, wasm_contract: Path) -> list[ContractBinding]: bindings_list = json.loads(proc_res.stdout) bindings = [] for binding_dict in bindings_list: - # TODO: Properly read and store the type information in the bindings (ie. type parameters for vecs, tuples, etc.) if binding_dict['type'] != 'function': continue name = binding_dict['name'] inputs = [] for input_dict in binding_dict['inputs']: - inputs.append(input_dict['value']['type']) + inputs.append(SCType.from_dict(input_dict['value'])) outputs = [] for output_dict in binding_dict['outputs']: - outputs.append(output_dict['type']) + outputs.append(SCType.from_dict(output_dict)) bindings.append(ContractBinding(name, tuple(inputs), tuple(outputs))) return bindings @@ -146,33 +149,31 @@ def deploy_test(self, contract: KInner) -> tuple[KInner, dict[str, KInner]]: return conf, subst def run_test(self, conf: KInner, subst: dict[str, KInner], binding: ContractBinding) -> None: - """Given a configuration with a deployed test contract, run the tests for the supplied binding. + """Given a configuration with a deployed test contract, fuzz over the tests for the supplied binding. Raises: CalledProcessError if the test fails """ - def getarg(arg: str) -> KInner: - # TODO: Implement actual argument generation. - # That's every possible ScVal in Soroban. - # Concrete values for fuzzing/variables for proving. - if arg == 'u32': - return sc_u32(10) - return SC_VOID - from_acct = account_id(b'test-account') to_acct = contract_id(b'test-contract') name = binding.name - args = [getarg(arg) for arg in binding.inputs] result = sc_bool(True) - steps = steps_of([set_exit_code(1), call_tx(from_acct, to_acct, name, args, result), set_exit_code(0)]) + def make_steps(*args: KInner) -> Pattern: + steps_kast = steps_of([set_exit_code(1), call_tx(from_acct, to_acct, name, args, result), set_exit_code(0)]) + return kast_to_kore(self.definition_info.kdefinition, steps_kast, KSort('Steps')) + + subst['PROGRAM_CELL'] = KVariable('STEPS') + template_config = Subst(subst).apply(conf) + template_config_kore = kast_to_kore( + self.definition_info.kdefinition, template_config, KSort('GeneratedTopCell') + ) - subst['PROGRAM_CELL'] = steps - test_config = Subst(subst).apply(conf) - test_config_kore = kast_to_kore(self.definition_info.kdefinition, test_config, KSort('GeneratedTopCell')) + steps_strategy = binding.strategy.map(lambda args: make_steps(*args)) + template_subst = {EVar('VarSTEPS', SortApp('SortSteps')): steps_strategy} - self.definition_info.krun.run_pattern(test_config_kore, check=True) + fuzz(self.definition_info.path, template_config_kore, template_subst, check_exit_code=True) def deploy_and_run(self, contract_wasm: Path) -> None: """Run all of the tests in a soroban test contract. @@ -199,5 +200,9 @@ class ContractBinding: """Represents one of the function bindings for a soroban contract.""" name: str - inputs: tuple[str, ...] - outputs: tuple[str, ...] + inputs: tuple[SCType, ...] + outputs: tuple[SCType, ...] + + @cached_property + def strategy(self) -> SearchStrategy[tuple[KInner, ...]]: + return strategies.tuples(*(arg.strategy().map(lambda x: x.to_kast()) for arg in self.inputs)) diff --git a/src/ksoroban/kast/syntax.py b/src/ksoroban/kast/syntax.py index b244991..f156f67 100644 --- a/src/ksoroban/kast/syntax.py +++ b/src/ksoroban/kast/syntax.py @@ -3,10 +3,8 @@ from typing import TYPE_CHECKING from pyk.kast.inner import KApply, KSort, KToken, build_cons -from pyk.prelude.bytes import bytesToken -from pyk.prelude.collections import list_of -from pyk.prelude.kbool import boolToken -from pyk.prelude.kint import intToken +from pyk.prelude.collections import list_of, map_of +from pyk.prelude.utils import token from pykwasm.kwasm_ast import wasm_string if TYPE_CHECKING: @@ -21,31 +19,31 @@ def steps_of(steps: Iterable[KInner]) -> KInner: def account_id(acct_id: bytes) -> KApply: - return KApply('AccountId', [bytesToken(acct_id)]) + return KApply('AccountId', [token(acct_id)]) def contract_id(contract_id: bytes) -> KApply: - return KApply('ContractId', [bytesToken(contract_id)]) + return KApply('ContractId', [token(contract_id)]) def set_exit_code(i: int) -> KInner: - return KApply('setExitCode', [intToken(i)]) + return KApply('setExitCode', [token(i)]) def set_account(acct: bytes, i: int) -> KInner: - return KApply('setAccount', [account_id(acct), intToken(i)]) + return KApply('setAccount', [account_id(acct), token(i)]) def upload_wasm(name: bytes, contract: KInner) -> KInner: - return KApply('uploadWasm', [bytesToken(name), contract]) + 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), bytesToken(wasm_hash), list_of(args)]) + return KApply('deployContract', [account_id(from_addr), contract_id(address), token(wasm_hash), list_of(args)]) -def call_tx(from_addr: KInner, to_addr: KInner, func: str, args: list[KInner], result: KInner) -> KInner: +def call_tx(from_addr: KInner, to_addr: KInner, func: str, args: Iterable[KInner], result: KInner) -> KInner: return KApply('callTx', [from_addr, to_addr, wasm_string(func), list_of(args), result]) @@ -53,11 +51,51 @@ def call_tx(from_addr: KInner, to_addr: KInner, func: str, args: list[KInner], r def sc_bool(b: bool) -> KInner: - return KApply('SCVal:Bool', [boolToken(b)]) + return KApply('SCVal:Bool', [token(b)]) def sc_u32(i: int) -> KInner: - return KApply('SCVal:U32', [intToken(i)]) + return KApply('SCVal:U32', [token(i)]) + + +def sc_u64(i: int) -> KInner: + return KApply('SCVal:U64', [token(i)]) + + +def sc_u128(i: int) -> KInner: + return KApply('SCVal:U128', [token(i)]) + + +def sc_u256(i: int) -> KInner: + return KApply('SCVal:U256', [token(i)]) + + +def sc_i32(i: int) -> KInner: + return KApply('SCVal:I32', [token(i)]) + + +def sc_i64(i: int) -> KInner: + return KApply('SCVal:I64', [token(i)]) + + +def sc_i128(i: int) -> KInner: + return KApply('SCVal:I128', [token(i)]) + + +def sc_i256(i: int) -> KInner: + return KApply('SCVal:I256', [token(i)]) + + +def sc_symbol(s: str) -> KInner: + return KApply('SCVal:Symbol', [token(s)]) + + +def sc_vec(l: Iterable[KInner]) -> KInner: + return KApply('SCVal:Vec', list_of(l)) + + +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')) diff --git a/src/ksoroban/scval.py b/src/ksoroban/scval.py new file mode 100644 index 0000000..deda98b --- /dev/null +++ b/src/ksoroban/scval.py @@ -0,0 +1,320 @@ +from __future__ import annotations + +from abc import ABC, abstractmethod +from dataclasses import dataclass +from typing import TYPE_CHECKING + +from hypothesis import strategies + +from .kast.syntax import ( + sc_bool, + sc_i32, + sc_i64, + sc_i128, + sc_i256, + sc_map, + sc_symbol, + sc_u32, + sc_u64, + sc_u128, + sc_u256, + sc_vec, +) +from .utils import KSorobanError + +if TYPE_CHECKING: + from typing import Any, Final, TypeVar + + from hypothesis.strategies import SearchStrategy + from pyk.kast.inner import KInner + + SCT = TypeVar('SCT', bound='SCType') + +# SCVals + + +@dataclass(frozen=True) +class SCValue(ABC): + @abstractmethod + def to_kast(self) -> KInner: ... + + +@dataclass(frozen=True) +class SCBool(SCValue): + val: bool + + def to_kast(self) -> KInner: + return sc_bool(self.val) + + +@dataclass(frozen=True) +class SCIntegral(SCValue): + val: int + + +@dataclass(frozen=True) +class SCI32(SCIntegral): + def to_kast(self) -> KInner: + return sc_i32(self.val) + + +@dataclass(frozen=True) +class SCI64(SCIntegral): + def to_kast(self) -> KInner: + return sc_i64(self.val) + + +@dataclass(frozen=True) +class SCI128(SCIntegral): + def to_kast(self) -> KInner: + return sc_i128(self.val) + + +@dataclass(frozen=True) +class SCI256(SCIntegral): + def to_kast(self) -> KInner: + return sc_i256(self.val) + + +@dataclass(frozen=True) +class SCU32(SCIntegral): + def to_kast(self) -> KInner: + return sc_u32(self.val) + + +@dataclass(frozen=True) +class SCU64(SCIntegral): + def to_kast(self) -> KInner: + return sc_u64(self.val) + + +@dataclass(frozen=True) +class SCU128(SCIntegral): + def to_kast(self) -> KInner: + return sc_u128(self.val) + + +@dataclass(frozen=True) +class SCU256(SCIntegral): + def to_kast(self) -> KInner: + return sc_u256(self.val) + + +@dataclass(frozen=True) +class SCSymbol(SCValue): + val: str + + def to_kast(self) -> KInner: + return sc_symbol(self.val) + + +@dataclass(frozen=True) +class SCVec(SCValue): + val: tuple[SCValue] + + def to_kast(self) -> KInner: + return sc_vec(v.to_kast() for v in self.val) + + +@dataclass(frozen=True) +class SCMap(SCValue): + val: dict[SCValue, SCValue] + + def to_kast(self) -> KInner: + return sc_map(((k.to_kast(), v.to_kast()) for k, v in self.val.items())) + + +# SCTypes + +_NAME_TO_CLASSNAME: Final = { + 'bool': 'SCBoolType', + 'i32': 'SCI32Type', + 'i64': 'SCI64Type', + 'i128': 'SCI128Type', + 'i256': 'SCI256Type', + 'u32': 'SCU32Type', + 'u64': 'SCU64Type', + 'u128': 'SCU128Type', + 'u256': 'SCU256Type', + 'symbol': 'SCSymbolType', + 'vec': 'SCVecType', + 'map': 'SCMapType', +} + + +@dataclass +class SCType(ABC): + @staticmethod + def from_dict(d: dict[str, Any]) -> SCType: + type_name = d['type'] + try: + cls_name = _NAME_TO_CLASSNAME[type_name] + except KeyError: + raise KSorobanError(f'Unsupported SC value type: {type_name!r}') from None + cls = globals()[cls_name] + return cls._from_dict(d) + + @classmethod + @abstractmethod + def _from_dict(cls: type[SCT], d: dict[str, Any]) -> SCT: ... + + @abstractmethod + def strategy(self) -> SearchStrategy: ... + + +@dataclass +class SCMonomorphicType(SCType): + @classmethod + def _from_dict(cls: type[SCT], d: dict[str, Any]) -> SCT: + return cls() + + +@dataclass +class SCBoolType(SCMonomorphicType): + def strategy(self) -> SearchStrategy: + return strategies.booleans().map(SCBool) + + +@dataclass +class SCIntegralType(SCMonomorphicType): + @staticmethod + @abstractmethod + def _range() -> tuple[int, int]: ... + + @staticmethod + @abstractmethod + def _val_class() -> type[SCIntegral]: ... + + def strategy(self) -> SearchStrategy: + min, max = self._range() + return strategies.integers(min_value=min, max_value=max).map(self._val_class()) + + +@dataclass +class SCI32Type(SCIntegralType): + @staticmethod + def _range() -> tuple[int, int]: + return -(2**31), (2**31) - 1 + + @staticmethod + def _val_class() -> type[SCI32]: + return SCI32 + + +@dataclass +class SCI64Type(SCIntegralType): + @staticmethod + def _range() -> tuple[int, int]: + return -(2**63), (2**63) - 1 + + @staticmethod + def _val_class() -> type[SCI64]: + return SCI64 + + +@dataclass +class SCI128Type(SCIntegralType): + @staticmethod + def _range() -> tuple[int, int]: + return -(2**127), (2**127) - 1 + + @staticmethod + def _val_class() -> type[SCI128]: + return SCI128 + + +@dataclass +class SCI256Type(SCIntegralType): + @staticmethod + def _range() -> tuple[int, int]: + return -(2**255), (2**255) - 1 + + @staticmethod + def _val_class() -> type[SCI256]: + return SCI256 + + +@dataclass +class SCU32Type(SCIntegralType): + @staticmethod + def _range() -> tuple[int, int]: + return 0, (2**32) - 1 + + @staticmethod + def _val_class() -> type[SCU32]: + return SCU32 + + +@dataclass +class SCU64Type(SCIntegralType): + @staticmethod + def _range() -> tuple[int, int]: + return 0, (2**64) - 1 + + @staticmethod + def _val_class() -> type[SCU64]: + return SCU64 + + +@dataclass +class SCU128Type(SCIntegralType): + @staticmethod + def _range() -> tuple[int, int]: + return 0, (2**128) - 1 + + @staticmethod + def _val_class() -> type[SCU128]: + return SCU128 + + +@dataclass +class SCU256Type(SCIntegralType): + @staticmethod + def _range() -> tuple[int, int]: + return 0, (2**256) - 1 + + @staticmethod + def _val_class() -> type[SCU256]: + return SCU256 + + +@dataclass +class SCSymbolType(SCMonomorphicType): + def strategy(self) -> SearchStrategy: + return strategies.text( + alphabet='_0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ', max_size=32 + ).map(SCSymbol) + + +@dataclass +class SCVecType(SCType): + element: SCType + + def __init__(self, element: SCType) -> None: + self.element = element + + @classmethod + def _from_dict(cls: type[SCVecType], d: dict[str, Any]) -> SCVecType: + return SCVecType(SCType.from_dict(d['element'])) + + def strategy(self) -> SearchStrategy: + return strategies.lists(elements=self.element.strategy()).map(tuple).map(SCVec) + + +@dataclass +class SCMapType(SCType): + key: SCType + value: SCType + + def __init__(self, key: SCType, value: SCType) -> None: + self.key = key + self.value = value + + @classmethod + def _from_dict(cls: type[SCMapType], d: dict[str, Any]) -> SCMapType: + key = SCType.from_dict(d['key']) + value = SCType.from_dict(d['value']) + return SCMapType(key, value) + + def strategy(self) -> SearchStrategy: + return strategies.dictionaries(keys=self.key.strategy(), values=self.value.strategy()).map(SCMap) diff --git a/src/ksoroban/utils.py b/src/ksoroban/utils.py index 9183ef2..8126a43 100644 --- a/src/ksoroban/utils.py +++ b/src/ksoroban/utils.py @@ -17,6 +17,9 @@ from pyk.kast.outer import KDefinition +class KSorobanError(RuntimeError): ... + + class SorobanDefinitionInfo: """Anything related to the Soroban K definition goes here.""" diff --git a/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs index 1961aa9..45cf218 100644 --- a/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs +++ b/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs @@ -6,13 +6,13 @@ pub struct AdderContract; #[contractimpl] impl AdderContract { - pub fn add(env: Env, first: u32, second: u32) -> u32 { - first + second + pub fn add(env: Env, first: u32, second: u32) -> u64 { + first as u64 + second as u64 } pub fn test_add(env: Env, num: u32) -> bool { let sum = Self::add(env, num, 5); - sum == num + 5 + sum == num as u64 + 5 } } diff --git a/src/tests/integration/data/soroban/contracts/test_adder_fail/Cargo.toml b/src/tests/integration/data/soroban/contracts/test_adder_fail/Cargo.toml new file mode 100644 index 0000000..63f0667 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_adder_fail/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "test_adder_fail" +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"] } diff --git a/src/tests/integration/data/soroban/contracts/test_adder_fail/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_adder_fail/src/lib.rs new file mode 100644 index 0000000..2acd2c6 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_adder_fail/src/lib.rs @@ -0,0 +1,17 @@ +#![no_std] +use soroban_sdk::{contract, contractimpl, Env}; + +#[contract] +pub struct AdderContract; + +#[contractimpl] +impl AdderContract { + pub fn add(env: Env, first: u32, second: u32) -> u32 { + first + second + } + + pub fn test_add_fail(env: Env, num: u32) -> bool { + let sum = Self::add(env, num, 4294967295); + sum == num + 4294967295 // overflow! + } +} diff --git a/src/tests/integration/data/soroban/contracts/valtypes/Cargo.toml b/src/tests/integration/data/soroban/contracts/valtypes/Cargo.toml new file mode 100644 index 0000000..b9979b6 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/valtypes/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "valtypes" +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"] } diff --git a/src/tests/integration/data/soroban/contracts/valtypes/src/lib.rs b/src/tests/integration/data/soroban/contracts/valtypes/src/lib.rs new file mode 100644 index 0000000..2658ab3 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/valtypes/src/lib.rs @@ -0,0 +1,25 @@ +#![no_std] +use soroban_sdk::{contract, contractimpl, Env, I256, Map, Symbol, U256, Vec}; +#[contract] +pub struct TypesContract; + +#[contractimpl] +impl TypesContract { + pub fn bool_type(_env: Env, b: bool) -> bool { b } + + pub fn signed_types(_env: Env, _i_32: i32, _i_64: i64, _i_128: i128, _i_256: I256) {} + + pub fn unsigned_types(_env: Env, _u_32: u32, _u_64: u64, _u_128: u128, _u_256: U256) {} + + pub fn symbol_type(_env: Env, symbol: Symbol) -> Symbol { symbol } + + pub fn vec_type(_env: Env, vec: Vec) -> Vec { vec } + + pub fn nested_vec_type(_env: Env, nested_vec: Vec>) -> Vec> { nested_vec } + + pub fn map_type(_env: Env, map: Map) -> Map { map } + + pub fn nested_map_type(_env: Env, map: Map>) -> Map> { map } + + pub fn deeply_nested_type(_env: Env, nested: Vec>>>) -> Vec>>> { nested } +} diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py index 03b3ac9..70dc65e 100644 --- a/src/tests/integration/test_integration.py +++ b/src/tests/integration/test_integration.py @@ -1,4 +1,5 @@ from pathlib import Path +from subprocess import CalledProcessError import pytest from pyk.kdist import kdist @@ -11,7 +12,7 @@ TEST_FILES = TEST_DATA.glob('*.wast') SOROBAN_CONTRACTS_DIR = TEST_DATA / 'soroban' / 'contracts' -SOROBAN_CONTRACTS = SOROBAN_CONTRACTS_DIR.glob('*') +SOROBAN_TEST_CONTRACTS = SOROBAN_CONTRACTS_DIR.glob('test_*') DEFINITION_DIR = kdist.get('soroban-semantics.llvm') @@ -31,10 +32,24 @@ def test_run(program: Path, tmp_path: Path) -> None: _krun(input_file=program, definition_dir=DEFINITION_DIR, check=True) -@pytest.mark.parametrize('contract_path', SOROBAN_CONTRACTS, ids=lambda p: str(p.stem)) +@pytest.mark.parametrize('contract_path', SOROBAN_TEST_CONTRACTS, ids=lambda p: str(p.stem)) def test_ksoroban(contract_path: Path, tmp_path: Path, kasmer: Kasmer) -> None: # Given contract_wasm = kasmer.build_soroban_contract(contract_path, tmp_path) # Then - kasmer.deploy_and_run(contract_wasm) + if contract_path.stem.endswith('_fail'): + with pytest.raises(CalledProcessError): + kasmer.deploy_and_run(contract_wasm) + else: + kasmer.deploy_and_run(contract_wasm) + + +def test_bindings(tmp_path: Path, kasmer: Kasmer) -> None: + # Given + contract_path = SOROBAN_CONTRACTS_DIR / 'valtypes' + contract_wasm = kasmer.build_soroban_contract(contract_path, tmp_path) + + # Then + # Just run this and make sure it doesn't throw an error + kasmer.contract_bindings(contract_wasm)