From 2ef6bf939151ceddbcde04fa13e8d095b2daa20e Mon Sep 17 00:00:00 2001 From: gtrepta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 13 Aug 2024 04:41:17 -0500 Subject: [PATCH] Add `ksoroban prove` command (#20) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add haskell backend target * Rename * Add module level SorobanDefinitionInfo instances * Rename * Make Kasmer.deploy_test unconditionally use the llvm definition * Draft of 'ksoroban prove' * Set Version: 0.1.16 * Lemmas * prove view command * More lemmas. test_adder now passes! * Rename * Set Version: 0.1.17 * Fix the lemmas. I scuffed them somehow when doing some reformatting before a commit. * Makefile: Build every soroban-semantics target * Adjust how prove/fuzz gets selected * Add the adder proof to the tests * Set Version: 0.1.18 * Set Version: 0.1.18 * Set Version: 0.1.20 --------- Co-authored-by: devops Co-authored-by: Burak Bilge Yalçınkaya --- Makefile | 2 +- package/version | 2 +- pyproject.toml | 2 +- src/ksoroban/kasmer.py | 89 ++++++++++++++++--- src/ksoroban/kast/syntax.py | 4 +- src/ksoroban/kdist/plugin.py | 11 +++ .../kdist/soroban-semantics/kasmer.md | 4 +- .../soroban-semantics/ksoroban-lemmas.md | 47 ++++++++++ src/ksoroban/ksoroban.py | 46 +++++++++- src/ksoroban/proof.py | 40 +++++++++ src/ksoroban/scval.py | 32 +++++++ src/ksoroban/utils.py | 12 ++- src/tests/integration/test_integration.py | 32 ++++--- 13 files changed, 289 insertions(+), 34 deletions(-) create mode 100644 src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md create mode 100644 src/ksoroban/proof.py diff --git a/Makefile b/Makefile index 7f5ed8d..d8915b5 100644 --- a/Makefile +++ b/Makefile @@ -23,7 +23,7 @@ poetry-install: # Semantics kdist-build: poetry-install - $(POETRY) run kdist -v build soroban-semantics.llvm + $(POETRY) run kdist -v build -j2 soroban-semantics.* kdist-clean: poetry-install $(POETRY) run kdist clean diff --git a/package/version b/package/version index d8a023e..baa9837 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.19 +0.1.20 diff --git a/pyproject.toml b/pyproject.toml index 4628faa..b09704b 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "ksoroban" -version = "0.1.19" +version = "0.1.20" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/ksoroban/kasmer.py b/src/ksoroban/kasmer.py index 84985bf..79342fa 100644 --- a/src/ksoroban/kasmer.py +++ b/src/ksoroban/kasmer.py @@ -9,6 +9,7 @@ from typing import TYPE_CHECKING from hypothesis import strategies +from pyk.cterm import CTerm, cterm_build_claim 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 @@ -16,10 +17,14 @@ from pyk.kore.syntax import EVar, SortApp from pyk.ktool.kfuzz import fuzz from pyk.ktool.krun import KRunOutput +from pyk.prelude.ml import mlEqualsTrue +from pyk.prelude.utils import token +from pyk.proof import ProofStatus from pyk.utils import run_process from pykwasm.wasm2kast import wasm2kast from .kast.syntax import ( + STEPS_TERMINATOR, account_id, call_tx, contract_id, @@ -30,7 +35,9 @@ steps_of, upload_wasm, ) +from .proof import run_claim from .scval import SCType +from .utils import KSorobanError, concrete_definition if TYPE_CHECKING: from typing import Any @@ -38,17 +45,18 @@ from hypothesis.strategies import SearchStrategy from pyk.kast.inner import KInner from pyk.kore.syntax import Pattern + from pyk.proof import APRProof - from .utils import SorobanDefinitionInfo + from .utils import SorobanDefinition class Kasmer: """Reads soroban contracts, and runs tests for them.""" - definition_info: SorobanDefinitionInfo + definition: SorobanDefinition - def __init__(self, definition_info: SorobanDefinitionInfo) -> None: - self.definition_info = definition_info + def __init__(self, definition: SorobanDefinition) -> None: + self.definition = definition def _which(self, cmd: str) -> Path: path_str = shutil.which(cmd) @@ -121,7 +129,8 @@ def kast_from_wasm(self, wasm: Path) -> KInner: """Get a kast term from a wasm program.""" return wasm2kast(open(wasm, 'rb')) - def deploy_test(self, contract: KInner) -> tuple[KInner, dict[str, KInner]]: + @staticmethod + def deploy_test(contract: KInner) -> tuple[KInner, dict[str, KInner]]: """Takes a wasm soroban contract as a kast term and deploys it in a fresh configuration. Returns: @@ -140,9 +149,9 @@ def deploy_test(self, contract: KInner) -> tuple[KInner, dict[str, KInner]]: ) # Run the steps and grab the resulting config as a starting place to call transactions - proc_res = self.definition_info.krun_with_kast(steps, sort=KSort('Steps'), output=KRunOutput.KORE) + proc_res = concrete_definition.krun_with_kast(steps, sort=KSort('Steps'), output=KRunOutput.KORE) kore_result = KoreParser(proc_res.stdout).pattern() - kast_result = kore_to_kast(self.definition_info.kdefinition, kore_result) + kast_result = kore_to_kast(concrete_definition.kdefinition, kore_result) conf, subst = split_config_from(kast_result) @@ -162,18 +171,43 @@ def run_test(self, conf: KInner, subst: dict[str, KInner], binding: ContractBind 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')) + return kast_to_kore(self.definition.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') - ) + template_config_kore = kast_to_kore(self.definition.kdefinition, template_config, KSort('GeneratedTopCell')) steps_strategy = binding.strategy.map(lambda args: make_steps(*args)) template_subst = {EVar('VarSTEPS', SortApp('SortSteps')): steps_strategy} - fuzz(self.definition_info.path, template_config_kore, template_subst, check_exit_code=True) + fuzz(self.definition.path, template_config_kore, template_subst, check_exit_code=True) + + def run_prove( + self, conf: KInner, subst: dict[str, KInner], binding: ContractBinding, proof_dir: Path | None = None + ) -> APRProof: + from_acct = account_id(b'test-account') + to_acct = contract_id(b'test-contract') + name = binding.name + result = sc_bool(True) + + def make_steps(*args: KInner) -> KInner: + return steps_of([set_exit_code(1), call_tx(from_acct, to_acct, name, args, result), set_exit_code(0)]) + + vars, ctrs = binding.symbolic_args() + + lhs_subst = subst.copy() + lhs_subst['PROGRAM_CELL'] = make_steps(*vars) + lhs = CTerm(Subst(lhs_subst).apply(conf), [mlEqualsTrue(c) for c in ctrs]) + + rhs_subst = subst.copy() + rhs_subst['PROGRAM_CELL'] = STEPS_TERMINATOR + rhs_subst['EXITCODE_CELL'] = token(0) + del rhs_subst['LOGGING_CELL'] + rhs = CTerm(Subst(rhs_subst).apply(conf)) + + claim, _ = cterm_build_claim(name, lhs, rhs) + + return run_claim(name, claim, proof_dir) def deploy_and_run(self, contract_wasm: Path) -> None: """Run all of the tests in a soroban test contract. @@ -194,6 +228,28 @@ def deploy_and_run(self, contract_wasm: Path) -> None: continue self.run_test(conf, subst, binding) + def deploy_and_prove(self, contract_wasm: Path, proof_dir: Path | None = None) -> None: + """Prove all of the tests in a soroban test contract. + + Args: + contract_wasm: The path to the compiled wasm contract. + proof_dir: The optional location to save the proof. + + Raises: + KSorobanError if a proof fails + """ + contract_kast = self.kast_from_wasm(contract_wasm) + conf, subst = self.deploy_test(contract_kast) + + bindings = self.contract_bindings(contract_wasm) + + for binding in bindings: + if not binding.name.startswith('test_'): + continue + proof = self.run_prove(conf, subst, binding, proof_dir) + if proof.status == ProofStatus.FAILED: + raise KSorobanError(proof.summary) + @dataclass(frozen=True) class ContractBinding: @@ -206,3 +262,12 @@ class ContractBinding: @cached_property def strategy(self) -> SearchStrategy[tuple[KInner, ...]]: return strategies.tuples(*(arg.strategy().map(lambda x: x.to_kast()) for arg in self.inputs)) + + def symbolic_args(self) -> tuple[tuple[KInner, ...], tuple[KInner, ...]]: + args: tuple[KInner, ...] = () + constraints: tuple[KInner, ...] = () + for i, arg in enumerate(self.inputs): + v, c = arg.as_var(f'ARG_{i}') + args += (v,) + constraints += c + return args, constraints diff --git a/src/ksoroban/kast/syntax.py b/src/ksoroban/kast/syntax.py index f156f67..4c6b400 100644 --- a/src/ksoroban/kast/syntax.py +++ b/src/ksoroban/kast/syntax.py @@ -13,9 +13,11 @@ from pyk.kast.inner import KInner +STEPS_TERMINATOR = KApply('.List{"kasmerSteps"}') + def steps_of(steps: Iterable[KInner]) -> KInner: - return build_cons(KApply('.List{"kasmerSteps"}'), 'kasmerSteps', steps) + return build_cons(STEPS_TERMINATOR, 'kasmerSteps', steps) def account_id(acct_id: bytes) -> KApply: diff --git a/src/ksoroban/kdist/plugin.py b/src/ksoroban/kdist/plugin.py index 0e68f3f..30952f4 100644 --- a/src/ksoroban/kdist/plugin.py +++ b/src/ksoroban/kdist/plugin.py @@ -48,6 +48,17 @@ def deps(self) -> tuple[str]: 'source': SourceTarget(), 'llvm': KompileTarget( lambda src_dir: { + 'backend': 'llvm', + 'main_file': src_dir / 'soroban-semantics/kasmer.md', + 'syntax_module': 'KASMER-SYNTAX', + 'include_dirs': [src_dir], + 'md_selector': 'k', + 'warnings_to_errors': True, + }, + ), + 'haskell': KompileTarget( + lambda src_dir: { + 'backend': 'haskell', 'main_file': src_dir / 'soroban-semantics/kasmer.md', 'syntax_module': 'KASMER-SYNTAX', 'include_dirs': [src_dir], diff --git a/src/ksoroban/kdist/soroban-semantics/kasmer.md b/src/ksoroban/kdist/soroban-semantics/kasmer.md index b8692e5..a0fb2cb 100644 --- a/src/ksoroban/kdist/soroban-semantics/kasmer.md +++ b/src/ksoroban/kdist/soroban-semantics/kasmer.md @@ -2,6 +2,7 @@ ```k requires "soroban.md" requires "cheatcodes.md" +requires "ksoroban-lemmas.md" module KASMER-SYNTAX imports WASM-TEXT-SYNTAX @@ -33,6 +34,7 @@ module KASMER imports SOROBAN imports CHEATCODES imports KASMER-SYNTAX-COMMON + imports KSOROBAN-LEMMAS configuration @@ -158,4 +160,4 @@ module KASMER (_:HostCell => .HostStack ... ) endmodule -``` \ No newline at end of file +``` diff --git a/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md b/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md new file mode 100644 index 0000000..7d5f9b5 --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md @@ -0,0 +1,47 @@ +```k +requires "wasm-semantics/kwasm-lemmas.md" +requires "data.md" + +module KSOROBAN-LEMMAS [symbolic] + imports KWASM-LEMMAS + imports INT-BITWISE-LEMMAS + imports HOST-OBJECT-LEMMAS +endmodule + +module INT-BITWISE-LEMMAS [symbolic] + imports INT + imports BOOL + + rule C |Int S => S |Int C [simplification, concrete(C), symbolic(S)] + rule X |Int 0 => X [simplification] + + rule A &Int B => B &Int A [simplification, concrete(A), symbolic(B)] + rule (A &Int B) &Int C => A &Int (B &Int C) [simplification, concrete(B, C)] + rule A &Int (B &Int C) => (A &Int B) &Int C [simplification, symbolic(A, B)] + + syntax Bool ::= isPowerOf2(Int) [function, total] + rule isPowerOf2(I:Int) => I ==Int 1 < false requires I <=Int 0 + + syntax Bool ::= isFullMask(Int) [function, total] + rule isFullMask(I:Int) => I ==Int fullMask(log2Int(I) +Int 1) requires 0 false requires I <=Int 0 + + syntax Int ::= fullMask(Int) [function, total] + rule fullMask(I:Int) => (1 < 0 requires I <=Int 0 + + rule I modInt M => I &Int (M -Int 1) requires isPowerOf2(M) [simplification, concrete(M)] + +endmodule + +module HOST-OBJECT-LEMMAS [symbolic] + imports HOST-OBJECT + imports INT-BITWISE-LEMMAS + + rule (_I < T &Int MASK + requires isFullMask(MASK) andBool SHIFT >=Int log2Int(MASK +Int 1) + [simplification, concrete(SHIFT, MASK)] + +endmodule +``` diff --git a/src/ksoroban/ksoroban.py b/src/ksoroban/ksoroban.py index 1e6b5cb..fedd157 100644 --- a/src/ksoroban/ksoroban.py +++ b/src/ksoroban/ksoroban.py @@ -12,10 +12,13 @@ from pyk.kdist import kdist from pyk.ktool.kprint import KAstOutput, _kast 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 pykwasm.scripts.preprocessor import preprocess from .kasmer import Kasmer -from .utils import SorobanDefinitionInfo +from .utils import concrete_definition, symbolic_definition if TYPE_CHECKING: from collections.abc import Iterator @@ -38,6 +41,13 @@ def main() -> None: elif args.command == 'test': wasm = Path(args.wasm.name) if args.wasm is not None else None _exec_test(wasm=wasm) + elif args.command == 'prove': + if args.prove_command is None or args.prove_command == 'run': + wasm = Path(args.wasm.name) if args.wasm is not None else None + _exec_prove_run(wasm=wasm, proof_dir=args.proof_dir) + if args.prove_command == 'view': + assert args.proof_dir is not None + _exec_prove_view(proof_dir=args.proof_dir, id=args.id) raise AssertionError() @@ -68,9 +78,7 @@ def _exec_test(*, wasm: Path | None) -> None: Exits successfully when all the tests pass. """ - definition_dir = kdist.get('soroban-semantics.llvm') - definition_info = SorobanDefinitionInfo(definition_dir) - kasmer = Kasmer(definition_info) + kasmer = Kasmer(concrete_definition) if wasm is None: # We build the contract here, specifying where it's saved so we know where to find it. @@ -83,6 +91,24 @@ def _exec_test(*, wasm: Path | None) -> None: sys.exit(0) +def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None) -> None: + kasmer = Kasmer(symbolic_definition) + + if wasm is None: + wasm = kasmer.build_soroban_contract(Path.cwd()) + + kasmer.deploy_and_prove(wasm, proof_dir) + + sys.exit(0) + + +def _exec_prove_view(*, proof_dir: Path, id: str) -> None: + proof = APRProof.read_proof_data(proof_dir, id) + viewer = APRProofViewer(proof, symbolic_definition.krun) + viewer.run() + sys.exit(0) + + @contextmanager def _preprocessed(program: Path) -> Iterator[Path]: program_text = program.read_text() @@ -114,6 +140,18 @@ def _argument_parser() -> ArgumentParser: test_parser = command_parser.add_parser('test', help='Test the soroban contract in the current working directory') test_parser.add_argument('--wasm', type=FileType('r'), help='Test a specific contract wasm file instead') + prove_parser = command_parser.add_parser('prove', help='Test the soroban contract in the current working directory') + prove_parser.add_argument( + 'prove_command', + default='run', + choices=('run', 'view'), + metavar='COMMAND', + help='Proof command to run. One of (%(choices)s)', + ) + prove_parser.add_argument('--wasm', type=FileType('r'), help='Prove a specific contract wasm file instead') + prove_parser.add_argument('--proof-dir', type=ensure_dir_path, default=None, help='Output directory for proofs') + prove_parser.add_argument('--id', help='Name of the test function in the testing contract') + return parser diff --git a/src/ksoroban/proof.py b/src/ksoroban/proof.py new file mode 100644 index 0000000..f7300c2 --- /dev/null +++ b/src/ksoroban/proof.py @@ -0,0 +1,40 @@ +from __future__ import annotations + +from contextlib import contextmanager +from typing import TYPE_CHECKING + +from pyk.cterm import cterm_symbolic +from pyk.kcfg import KCFGExplore +from pyk.kcfg.semantics import DefaultSemantics +from pyk.proof import APRProof, APRProver + +from .utils import symbolic_definition + +if TYPE_CHECKING: + from collections.abc import Iterator + from pathlib import Path + + from pyk.kast.outer import KClaim + + +@contextmanager +def _explore_context() -> Iterator[KCFGExplore]: + with cterm_symbolic(definition=symbolic_definition.kdefinition, definition_dir=symbolic_definition.path) as cts: + yield KCFGExplore(cts) + + +class SorobanSemantics(DefaultSemantics): ... + + +def run_claim(id: str, claim: KClaim, proof_dir: Path | None = None) -> APRProof: + if proof_dir is not None and APRProof.proof_data_exists(id, proof_dir): + proof = APRProof.read_proof_data(proof_dir, id) + else: + proof = APRProof.from_claim(symbolic_definition.kdefinition, claim=claim, logs={}, proof_dir=proof_dir) + + with _explore_context() as kcfg_explore: + prover = APRProver(kcfg_explore) + prover.advance_proof(proof) + + proof.write_proof_data() + return proof diff --git a/src/ksoroban/scval.py b/src/ksoroban/scval.py index deda98b..62b7592 100644 --- a/src/ksoroban/scval.py +++ b/src/ksoroban/scval.py @@ -5,6 +5,9 @@ from typing import TYPE_CHECKING from hypothesis import strategies +from pyk.kast.inner import KApply, KSort, KVariable +from pyk.prelude.kint import leInt +from pyk.prelude.utils import token from .kast.syntax import ( sc_bool, @@ -161,6 +164,10 @@ def _from_dict(cls: type[SCT], d: dict[str, Any]) -> SCT: ... @abstractmethod def strategy(self) -> SearchStrategy: ... + @classmethod + @abstractmethod + def as_var(cls, name: str) -> tuple[KInner, tuple[KInner, ...]]: ... + @dataclass class SCMonomorphicType(SCType): @@ -174,6 +181,10 @@ class SCBoolType(SCMonomorphicType): def strategy(self) -> SearchStrategy: return strategies.booleans().map(SCBool) + @classmethod + def as_var(cls, name: str) -> tuple[KInner, tuple[KInner, ...]]: + return KApply('SCVal:Bool', [KVariable(name, KSort('Bool'))]), () + @dataclass class SCIntegralType(SCMonomorphicType): @@ -189,6 +200,15 @@ def strategy(self) -> SearchStrategy: min, max = self._range() return strategies.integers(min_value=min, max_value=max).map(self._val_class()) + @classmethod + def as_var(cls, name: str) -> tuple[KInner, tuple[KInner, ...]]: + var = KVariable(name, KSort('Int')) + label = f'SCVal:{cls.__name__[2:-4]}' + k = KApply(label, [var]) + min, max = cls._range() + constraints = (leInt(token(min), var), leInt(var, token(max))) + return k, constraints + @dataclass class SCI32Type(SCIntegralType): @@ -285,6 +305,10 @@ def strategy(self) -> SearchStrategy: alphabet='_0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ', max_size=32 ).map(SCSymbol) + @classmethod + def as_var(cls, name: str) -> tuple[KInner, tuple[KInner, ...]]: + return KApply('SCVal:Symbol', [KVariable(name, KSort('String'))]), () + @dataclass class SCVecType(SCType): @@ -300,6 +324,10 @@ def _from_dict(cls: type[SCVecType], d: dict[str, Any]) -> SCVecType: def strategy(self) -> SearchStrategy: return strategies.lists(elements=self.element.strategy()).map(tuple).map(SCVec) + @classmethod + def as_var(cls, name: str) -> tuple[KInner, tuple[KInner, ...]]: + return KApply('SCVal:Vec', [KVariable(name, KSort('List'))]), () + @dataclass class SCMapType(SCType): @@ -318,3 +346,7 @@ def _from_dict(cls: type[SCMapType], d: dict[str, Any]) -> SCMapType: def strategy(self) -> SearchStrategy: return strategies.dictionaries(keys=self.key.strategy(), values=self.value.strategy()).map(SCMap) + + @classmethod + def as_var(cls, name: str) -> tuple[KInner, tuple[KInner, ...]]: + return KApply('SCVal:Map', [KVariable(name, KSort('Map'))]), () diff --git a/src/ksoroban/utils.py b/src/ksoroban/utils.py index 8126a43..a990b1f 100644 --- a/src/ksoroban/utils.py +++ b/src/ksoroban/utils.py @@ -4,6 +4,7 @@ from typing import TYPE_CHECKING from pyk.kast.outer import read_kast_definition +from pyk.kdist import kdist from pyk.konvert import kast_to_kore from pyk.ktool.kompile import DefinitionInfo from pyk.ktool.krun import KRun @@ -15,12 +16,13 @@ from pyk.kast.inner import KInner, KSort from pyk.kast.outer import KDefinition + from pyk.ktool.kompile import KompileBackend class KSorobanError(RuntimeError): ... -class SorobanDefinitionInfo: +class SorobanDefinition: """Anything related to the Soroban K definition goes here.""" definition_info: DefinitionInfo @@ -32,6 +34,10 @@ def __init__(self, path: Path) -> None: def path(self) -> Path: return self.definition_info.path + @cached_property + def backend(self) -> KompileBackend: + return self.definition_info.backend + @cached_property def kdefinition(self) -> KDefinition: return read_kast_definition(self.path / 'compiled.json') @@ -55,3 +61,7 @@ def krun_with_kast(self, pgm: KInner, sort: KSort | None = None, **kwargs: Any) """ kore_term = kast_to_kore(self.kdefinition, pgm, sort=sort) return self.krun.run_process(kore_term, **kwargs) + + +concrete_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm')) +symbolic_definition = SorobanDefinition(kdist.get('soroban-semantics.haskell')) diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py index 70dc65e..ad5425a 100644 --- a/src/tests/integration/test_integration.py +++ b/src/tests/integration/test_integration.py @@ -6,7 +6,7 @@ from pyk.ktool.krun import _krun from ksoroban.kasmer import Kasmer -from ksoroban.utils import SorobanDefinitionInfo +from ksoroban.utils import concrete_definition, symbolic_definition TEST_DATA = (Path(__file__).parent / 'data').resolve(strict=True) TEST_FILES = TEST_DATA.glob('*.wast') @@ -18,13 +18,13 @@ @pytest.fixture -def soroban_definition() -> SorobanDefinitionInfo: - return SorobanDefinitionInfo(DEFINITION_DIR) +def concrete_kasmer() -> Kasmer: + return Kasmer(concrete_definition) @pytest.fixture -def kasmer(soroban_definition: SorobanDefinitionInfo) -> Kasmer: - return Kasmer(soroban_definition) +def symbolic_kasmer() -> Kasmer: + return Kasmer(symbolic_definition) @pytest.mark.parametrize('program', TEST_FILES, ids=str) @@ -33,23 +33,31 @@ def test_run(program: Path, tmp_path: Path) -> None: @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: +def test_ksoroban(contract_path: Path, tmp_path: Path, concrete_kasmer: Kasmer) -> None: # Given - contract_wasm = kasmer.build_soroban_contract(contract_path, tmp_path) + contract_wasm = concrete_kasmer.build_soroban_contract(contract_path, tmp_path) # Then if contract_path.stem.endswith('_fail'): with pytest.raises(CalledProcessError): - kasmer.deploy_and_run(contract_wasm) + concrete_kasmer.deploy_and_run(contract_wasm) else: - kasmer.deploy_and_run(contract_wasm) + concrete_kasmer.deploy_and_run(contract_wasm) -def test_bindings(tmp_path: Path, kasmer: Kasmer) -> None: +def test_prove_adder(tmp_path: Path, symbolic_kasmer: Kasmer) -> None: + # Given + contract_wasm = symbolic_kasmer.build_soroban_contract(SOROBAN_CONTRACTS_DIR / 'test_adder', tmp_path) + + # Then + symbolic_kasmer.deploy_and_prove(contract_wasm, tmp_path) + + +def test_bindings(tmp_path: Path, concrete_kasmer: Kasmer) -> None: # Given contract_path = SOROBAN_CONTRACTS_DIR / 'valtypes' - contract_wasm = kasmer.build_soroban_contract(contract_path, tmp_path) + contract_wasm = concrete_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) + concrete_kasmer.contract_bindings(contract_wasm)