From 8a844940ac9a62f76f00883037c87dd208a9626d Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 30 Jul 2024 15:34:46 -0500 Subject: [PATCH 01/19] Add haskell backend target --- src/ksoroban/kdist/plugin.py | 11 +++++++++++ 1 file changed, 11 insertions(+) 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], From 2015b73c3d5521ac15fe50ea6d433b0cb35907ec Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 30 Jul 2024 17:10:25 -0500 Subject: [PATCH 02/19] Rename --- src/ksoroban/kasmer.py | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/src/ksoroban/kasmer.py b/src/ksoroban/kasmer.py index 84985bf..23ee82b 100644 --- a/src/ksoroban/kasmer.py +++ b/src/ksoroban/kasmer.py @@ -45,10 +45,10 @@ class Kasmer: """Reads soroban contracts, and runs tests for them.""" - definition_info: SorobanDefinitionInfo + definition: SorobanDefinitionInfo - def __init__(self, definition_info: SorobanDefinitionInfo) -> None: - self.definition_info = definition_info + def __init__(self, definition: SorobanDefinitionInfo) -> None: + self.definition = definition def _which(self, cmd: str) -> Path: path_str = shutil.which(cmd) @@ -140,9 +140,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 = self.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(self.definition.kdefinition, kore_result) conf, subst = split_config_from(kast_result) @@ -162,18 +162,16 @@ 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 deploy_and_run(self, contract_wasm: Path) -> None: """Run all of the tests in a soroban test contract. From 8a4edc171caf0f4122c3eadc2f367ff20f5def4c Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 30 Jul 2024 17:24:42 -0500 Subject: [PATCH 03/19] Add module level SorobanDefinitionInfo instances --- src/ksoroban/ksoroban.py | 6 ++---- src/ksoroban/utils.py | 5 +++++ 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/ksoroban/ksoroban.py b/src/ksoroban/ksoroban.py index 1e6b5cb..046ed60 100644 --- a/src/ksoroban/ksoroban.py +++ b/src/ksoroban/ksoroban.py @@ -15,7 +15,7 @@ from pykwasm.scripts.preprocessor import preprocess from .kasmer import Kasmer -from .utils import SorobanDefinitionInfo +from .utils import llvm_definition if TYPE_CHECKING: from collections.abc import Iterator @@ -68,9 +68,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(llvm_definition) if wasm is None: # We build the contract here, specifying where it's saved so we know where to find it. diff --git a/src/ksoroban/utils.py b/src/ksoroban/utils.py index 8126a43..e66df0e 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 @@ -55,3 +56,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) + + +llvm_definition = SorobanDefinitionInfo(kdist.get('soroban-semantics.llvm')) +haskell_definition = SorobanDefinitionInfo(kdist.get('soroban-semantics.haskell')) From a431e0c4775de49d0b64ad1336696e3af32cbeb5 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 30 Jul 2024 17:26:17 -0500 Subject: [PATCH 04/19] Rename --- src/ksoroban/kasmer.py | 6 +++--- src/ksoroban/utils.py | 6 +++--- src/tests/integration/test_integration.py | 8 ++++---- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/ksoroban/kasmer.py b/src/ksoroban/kasmer.py index 23ee82b..188932f 100644 --- a/src/ksoroban/kasmer.py +++ b/src/ksoroban/kasmer.py @@ -39,15 +39,15 @@ from pyk.kast.inner import KInner from pyk.kore.syntax import Pattern - from .utils import SorobanDefinitionInfo + from .utils import SorobanDefinition class Kasmer: """Reads soroban contracts, and runs tests for them.""" - definition: SorobanDefinitionInfo + definition: SorobanDefinition - def __init__(self, definition: SorobanDefinitionInfo) -> None: + def __init__(self, definition: SorobanDefinition) -> None: self.definition = definition def _which(self, cmd: str) -> Path: diff --git a/src/ksoroban/utils.py b/src/ksoroban/utils.py index e66df0e..341ad68 100644 --- a/src/ksoroban/utils.py +++ b/src/ksoroban/utils.py @@ -21,7 +21,7 @@ class KSorobanError(RuntimeError): ... -class SorobanDefinitionInfo: +class SorobanDefinition: """Anything related to the Soroban K definition goes here.""" definition_info: DefinitionInfo @@ -58,5 +58,5 @@ def krun_with_kast(self, pgm: KInner, sort: KSort | None = None, **kwargs: Any) return self.krun.run_process(kore_term, **kwargs) -llvm_definition = SorobanDefinitionInfo(kdist.get('soroban-semantics.llvm')) -haskell_definition = SorobanDefinitionInfo(kdist.get('soroban-semantics.haskell')) +llvm_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm')) +haskell_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..d6e61a5 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 SorobanDefinition TEST_DATA = (Path(__file__).parent / 'data').resolve(strict=True) TEST_FILES = TEST_DATA.glob('*.wast') @@ -18,12 +18,12 @@ @pytest.fixture -def soroban_definition() -> SorobanDefinitionInfo: - return SorobanDefinitionInfo(DEFINITION_DIR) +def soroban_definition() -> SorobanDefinition: + return SorobanDefinition(DEFINITION_DIR) @pytest.fixture -def kasmer(soroban_definition: SorobanDefinitionInfo) -> Kasmer: +def kasmer(soroban_definition: SorobanDefinition) -> Kasmer: return Kasmer(soroban_definition) From e1e9a5b88df8f3f3b8db9c7c8a552d2e9d8230d8 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 30 Jul 2024 17:27:11 -0500 Subject: [PATCH 05/19] Make Kasmer.deploy_test unconditionally use the llvm definition --- src/ksoroban/kasmer.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/ksoroban/kasmer.py b/src/ksoroban/kasmer.py index 188932f..5215dc4 100644 --- a/src/ksoroban/kasmer.py +++ b/src/ksoroban/kasmer.py @@ -31,6 +31,7 @@ upload_wasm, ) from .scval import SCType +from .utils import llvm_definition if TYPE_CHECKING: from typing import Any @@ -121,7 +122,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 +142,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.krun_with_kast(steps, sort=KSort('Steps'), output=KRunOutput.KORE) + proc_res = llvm_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.kdefinition, kore_result) + kast_result = kore_to_kast(llvm_definition.kdefinition, kore_result) conf, subst = split_config_from(kast_result) From 8d495da1d9ebfc666af59ff90849f26b46ed5d8b Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 2 Aug 2024 17:09:37 -0500 Subject: [PATCH 06/19] Draft of 'ksoroban prove' --- src/ksoroban/kasmer.py | 51 +++++++++++++++++++++++++++++++++++-- src/ksoroban/kast/syntax.py | 4 ++- src/ksoroban/ksoroban.py | 21 ++++++++++++++- src/ksoroban/proof.py | 40 +++++++++++++++++++++++++++++ src/ksoroban/scval.py | 32 +++++++++++++++++++++++ src/ksoroban/utils.py | 5 ++++ 6 files changed, 149 insertions(+), 4 deletions(-) create mode 100644 src/ksoroban/proof.py diff --git a/src/ksoroban/kasmer.py b/src/ksoroban/kasmer.py index 5215dc4..12464d8 100644 --- a/src/ksoroban/kasmer.py +++ b/src/ksoroban/kasmer.py @@ -9,17 +9,22 @@ 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 from pyk.kore.parser import KoreParser from pyk.kore.syntax import EVar, SortApp from pyk.ktool.kfuzz import fuzz +from pyk.ktool.kompile import KompileBackend from pyk.ktool.krun import KRunOutput +from pyk.prelude.ml import mlEqualsTrue +from pyk.prelude.utils import token from pyk.utils import run_process from pykwasm.wasm2kast import wasm2kast from .kast.syntax import ( + STEPS_TERMINATOR, account_id, call_tx, contract_id, @@ -30,6 +35,7 @@ steps_of, upload_wasm, ) +from .proof import run_claim from .scval import SCType from .utils import llvm_definition @@ -175,7 +181,35 @@ def make_steps(*args: KInner) -> Pattern: fuzz(self.definition.path, template_config_kore, template_subst, check_exit_code=True) - def deploy_and_run(self, contract_wasm: Path) -> None: + def run_prove( + self, conf: KInner, subst: dict[str, KInner], binding: ContractBinding, proof_dir: Path | None = None + ) -> None: + 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(binding.name, lhs, rhs) + + proof = run_claim(binding.name, claim, proof_dir) + print(proof.summary) + + def deploy_and_run(self, contract_wasm: Path, proof_dir: Path | None = None) -> None: """Run all of the tests in a soroban test contract. Args: @@ -192,7 +226,11 @@ def deploy_and_run(self, contract_wasm: Path) -> None: for binding in bindings: if not binding.name.startswith('test_'): continue - self.run_test(conf, subst, binding) + backend = self.definition.backend + if backend == KompileBackend.LLVM: + self.run_test(conf, subst, binding) + elif backend == KompileBackend.HASKELL: + self.run_prove(conf, subst, binding, proof_dir) @dataclass(frozen=True) @@ -206,3 +244,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/ksoroban.py b/src/ksoroban/ksoroban.py index 046ed60..22b978f 100644 --- a/src/ksoroban/ksoroban.py +++ b/src/ksoroban/ksoroban.py @@ -12,10 +12,11 @@ from pyk.kdist import kdist from pyk.ktool.kprint import KAstOutput, _kast from pyk.ktool.krun import _krun +from pyk.utils import ensure_dir_path from pykwasm.scripts.preprocessor import preprocess from .kasmer import Kasmer -from .utils import llvm_definition +from .utils import haskell_definition, llvm_definition if TYPE_CHECKING: from collections.abc import Iterator @@ -38,6 +39,9 @@ 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': + wasm = Path(args.wasm.name) if args.wasm is not None else None + _exec_prove(wasm=wasm, proof_dir=args.proof_dir) raise AssertionError() @@ -81,6 +85,17 @@ def _exec_test(*, wasm: Path | None) -> None: sys.exit(0) +def _exec_prove(*, wasm: Path | None, proof_dir: Path | None) -> None: + kasmer = Kasmer(haskell_definition) + + if wasm is None: + wasm = kasmer.build_soroban_contract(Path.cwd()) + + kasmer.deploy_and_run(wasm, proof_dir) + + sys.exit(0) + + @contextmanager def _preprocessed(program: Path) -> Iterator[Path]: program_text = program.read_text() @@ -112,6 +127,10 @@ 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') + test_parser = command_parser.add_parser('prove', 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') + test_parser.add_argument('--proof-dir', type=ensure_dir_path, default=None, help='Output directory for proofs') + return parser diff --git a/src/ksoroban/proof.py b/src/ksoroban/proof.py new file mode 100644 index 0000000..5b97c4b --- /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 haskell_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=haskell_definition.kdefinition, definition_dir=haskell_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(haskell_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 341ad68..dbda4a2 100644 --- a/src/ksoroban/utils.py +++ b/src/ksoroban/utils.py @@ -16,6 +16,7 @@ from pyk.kast.inner import KInner, KSort from pyk.kast.outer import KDefinition + from pyk.ktool.kompile import KompileBackend class KSorobanError(RuntimeError): ... @@ -33,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') From c255f394cb238d21f156143fd795be4213caea1b Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 5 Aug 2024 23:19:12 +0000 Subject: [PATCH 07/19] Set Version: 0.1.16 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index c34958a..e8e277f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.15 +0.1.16 diff --git a/pyproject.toml b/pyproject.toml index 725b4db..7f440c8 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "ksoroban" -version = "0.1.15" +version = "0.1.16" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From 9d050b76cabe527ea2b0506e974ecb6dac38e92e Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 6 Aug 2024 16:56:39 -0500 Subject: [PATCH 08/19] Lemmas --- .../kdist/soroban-semantics/kasmer.md | 4 +++- .../soroban-semantics/ksoroban-lemmas.md | 21 +++++++++++++++++++ 2 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md diff --git a/src/ksoroban/kdist/soroban-semantics/kasmer.md b/src/ksoroban/kdist/soroban-semantics/kasmer.md index 059db27..cf29ec7 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 @@ -154,4 +156,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..a195881 --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md @@ -0,0 +1,21 @@ +```k +requires "wasm-semantics/kwasm-lemmas.md" +requires "data.md" + +module KSOROBAN-LEMMAS [symbolic] + imports KWASM-LEMMAS + imports HOST-OBJECT-LEMMAS +endmodule +``` + +```k +module HOST-OBJECT-LEMMAS [symbolic] + imports HOST-OBJECT + + rule (_I < T &Int 255 [simplification] + + rule X |Int 0 => X [simplification] + + rule (_X < 0 requires S >=Int 8 [simplification] +endmodule +``` From d347d1dc95ed8d9b65100220ac6bf97af153a36b Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 6 Aug 2024 19:17:11 -0500 Subject: [PATCH 09/19] prove view command --- src/ksoroban/ksoroban.py | 33 +++++++++++++++++++++++++++------ 1 file changed, 27 insertions(+), 6 deletions(-) diff --git a/src/ksoroban/ksoroban.py b/src/ksoroban/ksoroban.py index 22b978f..7b9e2df 100644 --- a/src/ksoroban/ksoroban.py +++ b/src/ksoroban/ksoroban.py @@ -12,6 +12,8 @@ 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 @@ -40,8 +42,12 @@ def main() -> None: wasm = Path(args.wasm.name) if args.wasm is not None else None _exec_test(wasm=wasm) elif args.command == 'prove': - wasm = Path(args.wasm.name) if args.wasm is not None else None - _exec_prove(wasm=wasm, proof_dir=args.proof_dir) + 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() @@ -85,7 +91,7 @@ def _exec_test(*, wasm: Path | None) -> None: sys.exit(0) -def _exec_prove(*, wasm: Path | None, proof_dir: Path | None) -> None: +def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None) -> None: kasmer = Kasmer(haskell_definition) if wasm is None: @@ -96,6 +102,13 @@ def _exec_prove(*, wasm: Path | None, proof_dir: Path | None) -> None: sys.exit(0) +def _exec_prove_view(*, proof_dir: Path, id: str) -> None: + proof = APRProof.read_proof_data(proof_dir, id) + viewer = APRProofViewer(proof, haskell_definition.krun) + viewer.run() + sys.exit(0) + + @contextmanager def _preprocessed(program: Path) -> Iterator[Path]: program_text = program.read_text() @@ -127,9 +140,17 @@ 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') - test_parser = command_parser.add_parser('prove', 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') - test_parser.add_argument('--proof-dir', type=ensure_dir_path, default=None, help='Output directory for proofs') + 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 From 7b96ae19257e21d8e5b1076c0b3fe2a0f24aa5e3 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Wed, 7 Aug 2024 16:30:21 -0500 Subject: [PATCH 10/19] More lemmas. test_adder now passes! --- .../soroban-semantics/ksoroban-lemmas.md | 36 +++++++++++++++---- 1 file changed, 30 insertions(+), 6 deletions(-) diff --git a/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md b/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md index a195881..695d39b 100644 --- a/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md +++ b/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md @@ -4,18 +4,42 @@ requires "data.md" module KSOROBAN-LEMMAS [symbolic] imports KWASM-LEMMAS + imports INT-BITWISE-LEMMAS imports HOST-OBJECT-LEMMAS endmodule -``` -```k +module INT-BITWISE-LEMMAS [symbolic] + + 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 fullMask(M) requires isPowerOf2(M) [simplification, concrete(M)] + +endmodule + module HOST-OBJECT-LEMMAS [symbolic] imports HOST-OBJECT + imports INT-BITWISE-LEMMAS - rule (_I < T &Int 255 [simplification] - - rule X |Int 0 => X [simplification] + rule (_I < T &Int MASK + requires isFullMask(MASK) andBool SHIFT >=Int log2Int(MASK +Int 1) + [simplification, concrete(SHIFT, MASK)] - rule (_X < 0 requires S >=Int 8 [simplification] endmodule ``` From 4ed0e9487f73e13391e68901a9ae94e9c27db35e Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Wed, 7 Aug 2024 16:42:44 -0500 Subject: [PATCH 11/19] Rename --- src/ksoroban/kasmer.py | 6 +++--- src/ksoroban/ksoroban.py | 8 ++++---- src/ksoroban/proof.py | 6 +++--- src/ksoroban/utils.py | 4 ++-- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/ksoroban/kasmer.py b/src/ksoroban/kasmer.py index 12464d8..688e82e 100644 --- a/src/ksoroban/kasmer.py +++ b/src/ksoroban/kasmer.py @@ -37,7 +37,7 @@ ) from .proof import run_claim from .scval import SCType -from .utils import llvm_definition +from .utils import concrete_definition if TYPE_CHECKING: from typing import Any @@ -148,9 +148,9 @@ def deploy_test(contract: KInner) -> tuple[KInner, dict[str, KInner]]: ) # Run the steps and grab the resulting config as a starting place to call transactions - proc_res = llvm_definition.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(llvm_definition.kdefinition, kore_result) + kast_result = kore_to_kast(concrete_definition.kdefinition, kore_result) conf, subst = split_config_from(kast_result) diff --git a/src/ksoroban/ksoroban.py b/src/ksoroban/ksoroban.py index 7b9e2df..8495daa 100644 --- a/src/ksoroban/ksoroban.py +++ b/src/ksoroban/ksoroban.py @@ -18,7 +18,7 @@ from pykwasm.scripts.preprocessor import preprocess from .kasmer import Kasmer -from .utils import haskell_definition, llvm_definition +from .utils import concrete_definition, symbolic_definition if TYPE_CHECKING: from collections.abc import Iterator @@ -78,7 +78,7 @@ def _exec_test(*, wasm: Path | None) -> None: Exits successfully when all the tests pass. """ - kasmer = Kasmer(llvm_definition) + 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. @@ -92,7 +92,7 @@ def _exec_test(*, wasm: Path | None) -> None: def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None) -> None: - kasmer = Kasmer(haskell_definition) + kasmer = Kasmer(symbolic_definition) if wasm is None: wasm = kasmer.build_soroban_contract(Path.cwd()) @@ -104,7 +104,7 @@ def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None) -> None: def _exec_prove_view(*, proof_dir: Path, id: str) -> None: proof = APRProof.read_proof_data(proof_dir, id) - viewer = APRProofViewer(proof, haskell_definition.krun) + viewer = APRProofViewer(proof, symbolic_definition.krun) viewer.run() sys.exit(0) diff --git a/src/ksoroban/proof.py b/src/ksoroban/proof.py index 5b97c4b..f7300c2 100644 --- a/src/ksoroban/proof.py +++ b/src/ksoroban/proof.py @@ -8,7 +8,7 @@ from pyk.kcfg.semantics import DefaultSemantics from pyk.proof import APRProof, APRProver -from .utils import haskell_definition +from .utils import symbolic_definition if TYPE_CHECKING: from collections.abc import Iterator @@ -19,7 +19,7 @@ @contextmanager def _explore_context() -> Iterator[KCFGExplore]: - with cterm_symbolic(definition=haskell_definition.kdefinition, definition_dir=haskell_definition.path) as cts: + with cterm_symbolic(definition=symbolic_definition.kdefinition, definition_dir=symbolic_definition.path) as cts: yield KCFGExplore(cts) @@ -30,7 +30,7 @@ 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(haskell_definition.kdefinition, claim=claim, logs={}, proof_dir=proof_dir) + proof = APRProof.from_claim(symbolic_definition.kdefinition, claim=claim, logs={}, proof_dir=proof_dir) with _explore_context() as kcfg_explore: prover = APRProver(kcfg_explore) diff --git a/src/ksoroban/utils.py b/src/ksoroban/utils.py index dbda4a2..a990b1f 100644 --- a/src/ksoroban/utils.py +++ b/src/ksoroban/utils.py @@ -63,5 +63,5 @@ def krun_with_kast(self, pgm: KInner, sort: KSort | None = None, **kwargs: Any) return self.krun.run_process(kore_term, **kwargs) -llvm_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm')) -haskell_definition = SorobanDefinition(kdist.get('soroban-semantics.haskell')) +concrete_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm')) +symbolic_definition = SorobanDefinition(kdist.get('soroban-semantics.haskell')) From 373de1801dce01452337564b5454f4dc503f8b62 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 7 Aug 2024 21:52:28 +0000 Subject: [PATCH 12/19] Set Version: 0.1.17 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index e8e277f..04c5555 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.16 +0.1.17 diff --git a/pyproject.toml b/pyproject.toml index 7f440c8..9333926 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "ksoroban" -version = "0.1.16" +version = "0.1.17" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From 1364dd6c382988594c37bbc9a1e39829d0644ff2 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Wed, 7 Aug 2024 19:38:20 -0500 Subject: [PATCH 13/19] Fix the lemmas. I scuffed them somehow when doing some reformatting before a commit. --- src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md b/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md index 695d39b..7d5f9b5 100644 --- a/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md +++ b/src/ksoroban/kdist/soroban-semantics/ksoroban-lemmas.md @@ -9,6 +9,8 @@ module KSOROBAN-LEMMAS [symbolic] 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] @@ -29,7 +31,7 @@ module INT-BITWISE-LEMMAS [symbolic] rule fullMask(I:Int) => (1 < 0 requires I <=Int 0 - rule I modInt M => I &Int fullMask(M) requires isPowerOf2(M) [simplification, concrete(M)] + rule I modInt M => I &Int (M -Int 1) requires isPowerOf2(M) [simplification, concrete(M)] endmodule From 28e074171d66c757ca5ad36409cfb16a62c1a940 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 8 Aug 2024 12:12:50 -0500 Subject: [PATCH 14/19] Makefile: Build every soroban-semantics target --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From c7966e87e958ff986ee81e163d4fe3859d4cffbd Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 9 Aug 2024 14:39:33 -0500 Subject: [PATCH 15/19] Adjust how prove/fuzz gets selected --- src/ksoroban/kasmer.py | 42 ++++++++++++++++++++++++++++------------ src/ksoroban/ksoroban.py | 2 +- 2 files changed, 31 insertions(+), 13 deletions(-) diff --git a/src/ksoroban/kasmer.py b/src/ksoroban/kasmer.py index 688e82e..79342fa 100644 --- a/src/ksoroban/kasmer.py +++ b/src/ksoroban/kasmer.py @@ -16,10 +16,10 @@ from pyk.kore.parser import KoreParser from pyk.kore.syntax import EVar, SortApp from pyk.ktool.kfuzz import fuzz -from pyk.ktool.kompile import KompileBackend 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 @@ -37,7 +37,7 @@ ) from .proof import run_claim from .scval import SCType -from .utils import concrete_definition +from .utils import KSorobanError, concrete_definition if TYPE_CHECKING: from typing import Any @@ -45,6 +45,7 @@ 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 SorobanDefinition @@ -183,7 +184,7 @@ def make_steps(*args: KInner) -> Pattern: def run_prove( self, conf: KInner, subst: dict[str, KInner], binding: ContractBinding, proof_dir: Path | None = None - ) -> None: + ) -> APRProof: from_acct = account_id(b'test-account') to_acct = contract_id(b'test-contract') name = binding.name @@ -204,12 +205,11 @@ def make_steps(*args: KInner) -> KInner: del rhs_subst['LOGGING_CELL'] rhs = CTerm(Subst(rhs_subst).apply(conf)) - claim, _ = cterm_build_claim(binding.name, lhs, rhs) + claim, _ = cterm_build_claim(name, lhs, rhs) - proof = run_claim(binding.name, claim, proof_dir) - print(proof.summary) + return run_claim(name, claim, proof_dir) - def deploy_and_run(self, contract_wasm: Path, proof_dir: Path | None = None) -> None: + def deploy_and_run(self, contract_wasm: Path) -> None: """Run all of the tests in a soroban test contract. Args: @@ -226,11 +226,29 @@ def deploy_and_run(self, contract_wasm: Path, proof_dir: Path | None = None) -> for binding in bindings: if not binding.name.startswith('test_'): continue - backend = self.definition.backend - if backend == KompileBackend.LLVM: - self.run_test(conf, subst, binding) - elif backend == KompileBackend.HASKELL: - self.run_prove(conf, subst, binding, proof_dir) + 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) diff --git a/src/ksoroban/ksoroban.py b/src/ksoroban/ksoroban.py index 8495daa..fedd157 100644 --- a/src/ksoroban/ksoroban.py +++ b/src/ksoroban/ksoroban.py @@ -97,7 +97,7 @@ def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None) -> None: if wasm is None: wasm = kasmer.build_soroban_contract(Path.cwd()) - kasmer.deploy_and_run(wasm, proof_dir) + kasmer.deploy_and_prove(wasm, proof_dir) sys.exit(0) From b7868f83d1092291badbc630f9f28524a37e8d2e Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 9 Aug 2024 14:47:19 -0500 Subject: [PATCH 16/19] Add the adder proof to the tests --- src/tests/integration/test_integration.py | 32 ++++++++++++++--------- 1 file changed, 20 insertions(+), 12 deletions(-) diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py index d6e61a5..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 SorobanDefinition +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() -> SorobanDefinition: - return SorobanDefinition(DEFINITION_DIR) +def concrete_kasmer() -> Kasmer: + return Kasmer(concrete_definition) @pytest.fixture -def kasmer(soroban_definition: SorobanDefinition) -> 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) From fdf2a55300b7cc8e94de2ed1fae707f64d5a3ce2 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 9 Aug 2024 19:47:43 +0000 Subject: [PATCH 17/19] Set Version: 0.1.18 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 04c5555..f8bc4c6 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.17 +0.1.18 diff --git a/pyproject.toml b/pyproject.toml index 9333926..b212017 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "ksoroban" -version = "0.1.17" +version = "0.1.18" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From 1ad6d805699e35c4f18b0173f66e26a6423e2ade Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 9 Aug 2024 20:00:31 +0000 Subject: [PATCH 18/19] Set Version: 0.1.18 --- package/version | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/package/version b/package/version index 44905e7..f8bc4c6 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.18 \ No newline at end of file +0.1.18 From 090f6fc4698b8f1a42b7e77c5d91f31fa4728869 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 13 Aug 2024 09:05:33 +0000 Subject: [PATCH 19/19] Set Version: 0.1.20 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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. ",