From e9045153370189a7280e962460c82ab65f48c317 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Mon, 9 Dec 2024 15:26:40 +0300 Subject: [PATCH 1/8] fix `prove_parser` help text: `Test => Prove` --- src/komet/komet.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/komet/komet.py b/src/komet/komet.py index f3a0fcc..6758368 100644 --- a/src/komet/komet.py +++ b/src/komet/komet.py @@ -175,7 +175,7 @@ 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 = command_parser.add_parser('prove', help='Prove the soroban contract in the current working directory') prove_parser.add_argument( 'prove_command', default='run', From 06b6c73cf4fad82c6dc6ae091acf3c080a52402a Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 11 Dec 2024 17:02:11 +0300 Subject: [PATCH 2/8] add `--id ` option --- src/komet/kasmer.py | 12 +++++++++--- src/komet/komet.py | 15 +++++++++------ 2 files changed, 18 insertions(+), 9 deletions(-) diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index 96934a1..1c74637 100644 --- a/src/komet/kasmer.py +++ b/src/komet/kasmer.py @@ -236,7 +236,7 @@ def make_steps(*args: KInner) -> KInner: return run_claim(name, claim, proof_dir, bug_report) - def deploy_and_run(self, contract_wasm: Path, child_wasms: tuple[Path, ...]) -> None: + def deploy_and_run(self, contract_wasm: Path, child_wasms: tuple[Path, ...], id: str | None) -> None: """Run all of the tests in a soroban test contract. Args: @@ -255,9 +255,15 @@ def deploy_and_run(self, contract_wasm: Path, child_wasms: tuple[Path, ...]) -> conf, subst = self.deploy_test(contract_kast, child_kasts, has_init) - test_bindings = [b for b in bindings if b.name.startswith('test_')] + test_bindings = [b for b in bindings if b.name.startswith('test_') and (id is None or b.name == id)] + + if id is None: + print(f'Discovered {len(test_bindings)} test functions:') + elif not test_bindings: + raise KeyError(f'Test function {id!r} not found.') + else: + print('Selected a single test function:') - print(f'Discovered {len(test_bindings)} test functions:') for binding in test_bindings: print(f' - {binding.name}') diff --git a/src/komet/komet.py b/src/komet/komet.py index 6758368..705ab5c 100644 --- a/src/komet/komet.py +++ b/src/komet/komet.py @@ -47,7 +47,7 @@ def main() -> None: _exec_kast(program=args.program, backend=args.backend, output=args.output) elif args.command == 'test': wasm = Path(args.wasm.name) if args.wasm is not None else None - _exec_test(wasm=wasm) + _exec_test(wasm=wasm, id=args.id) 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 @@ -77,7 +77,7 @@ def _exec_kast(*, program: Path, backend: Backend, output: KAstOutput | None) -> _exit_with_output(proc_res) -def _exec_test(*, wasm: Path | None) -> None: +def _exec_test(*, wasm: Path | None, id: str | None) -> None: """Run a soroban test contract given its compiled wasm file. This will get the bindings for the contract and run all of the test functions. @@ -96,7 +96,7 @@ def _exec_test(*, wasm: Path | None) -> None: child_wasms = _read_config_file(kasmer) wasm = kasmer.build_soroban_contract(Path.cwd()) - kasmer.deploy_and_run(wasm, child_wasms) + kasmer.deploy_and_run(wasm, child_wasms, id=id) sys.exit(0) @@ -173,7 +173,7 @@ def _argument_parser() -> ArgumentParser: kast_parser.add_argument('--output', metavar='FORMAT', type=KAstOutput, help='format to output the term in') 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') + _add_common_test_arguments(test_parser) prove_parser = command_parser.add_parser('prove', help='Prove the soroban contract in the current working directory') prove_parser.add_argument( @@ -183,10 +183,9 @@ def _argument_parser() -> ArgumentParser: 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('--bug-report', type=bug_report_arg, default=None, help='Bug report directory for proofs') - prove_parser.add_argument('--id', help='Name of the test function in the testing contract') + _add_common_test_arguments(prove_parser) return parser @@ -194,3 +193,7 @@ def _argument_parser() -> ArgumentParser: def _add_common_arguments(parser: ArgumentParser) -> None: parser.add_argument('program', metavar='PROGRAM', type=file_path, help='path to test file') parser.add_argument('--backend', metavar='BACKEND', type=Backend, default=Backend.LLVM, help='K backend to use') + +def _add_common_test_arguments(parser: ArgumentParser) -> None: + parser.add_argument('--id', help='Name of the test function in the testing contract') + parser.add_argument('--wasm', type=FileType('r'), help='Use a specific contract wasm file instead') From abcb341389fdff29def3e1ed00aad8a3914e02ea Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 11 Dec 2024 17:11:47 +0300 Subject: [PATCH 3/8] add `--max-examples` option --- src/komet/kasmer.py | 14 +++++++++----- src/komet/komet.py | 16 ++++++++++++---- 2 files changed, 21 insertions(+), 9 deletions(-) diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index 1c74637..8b73a4e 100644 --- a/src/komet/kasmer.py +++ b/src/komet/kasmer.py @@ -179,7 +179,7 @@ def call_init() -> tuple[KInner, ...]: return conf, subst - def run_test(self, conf: KInner, subst: dict[str, KInner], binding: ContractBinding) -> None: + def run_test(self, conf: KInner, subst: dict[str, KInner], binding: ContractBinding, max_examples: int) -> None: """Given a configuration with a deployed test contract, fuzz over the tests for the supplied binding. Raises: @@ -202,7 +202,9 @@ def make_steps(*args: KInner) -> Pattern: steps_strategy = binding.strategy.map(lambda args: make_steps(*args)) template_subst = {EVar('VarSTEPS', SortApp('SortSteps')): steps_strategy} - fuzz(self.definition.path, template_config_kore, template_subst, check_exit_code=True) + fuzz( + self.definition.path, template_config_kore, template_subst, check_exit_code=True, max_examples=max_examples + ) def run_prove( self, @@ -236,7 +238,9 @@ def make_steps(*args: KInner) -> KInner: return run_claim(name, claim, proof_dir, bug_report) - def deploy_and_run(self, contract_wasm: Path, child_wasms: tuple[Path, ...], id: str | None) -> None: + def deploy_and_run( + self, contract_wasm: Path, child_wasms: tuple[Path, ...], max_examples: int = 100, id: str | None = None + ) -> None: """Run all of the tests in a soroban test contract. Args: @@ -257,7 +261,7 @@ def deploy_and_run(self, contract_wasm: Path, child_wasms: tuple[Path, ...], id: test_bindings = [b for b in bindings if b.name.startswith('test_') and (id is None or b.name == id)] - if id is None: + if id is None: print(f'Discovered {len(test_bindings)} test functions:') elif not test_bindings: raise KeyError(f'Test function {id!r} not found.') @@ -269,7 +273,7 @@ def deploy_and_run(self, contract_wasm: Path, child_wasms: tuple[Path, ...], id: for binding in test_bindings: print(f'\n Running {binding.name}...') - self.run_test(conf, subst, binding) + self.run_test(conf, subst, binding, max_examples) print(' Test passed.') def deploy_and_prove( diff --git a/src/komet/komet.py b/src/komet/komet.py index 705ab5c..5d1ca0f 100644 --- a/src/komet/komet.py +++ b/src/komet/komet.py @@ -47,7 +47,9 @@ def main() -> None: _exec_kast(program=args.program, backend=args.backend, output=args.output) elif args.command == 'test': wasm = Path(args.wasm.name) if args.wasm is not None else None - _exec_test(wasm=wasm, id=args.id) + if args.max_examples < 1: + raise ValueError(f'--max-examples must be a positive integer (greater than 0), given {args.max_examples}') + _exec_test(wasm=wasm, max_examples=args.max_examples, id=args.id) 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 @@ -77,7 +79,7 @@ def _exec_kast(*, program: Path, backend: Backend, output: KAstOutput | None) -> _exit_with_output(proc_res) -def _exec_test(*, wasm: Path | None, id: str | None) -> None: +def _exec_test(*, wasm: Path | None, max_examples: int, id: str | None) -> None: """Run a soroban test contract given its compiled wasm file. This will get the bindings for the contract and run all of the test functions. @@ -96,7 +98,7 @@ def _exec_test(*, wasm: Path | None, id: str | None) -> None: child_wasms = _read_config_file(kasmer) wasm = kasmer.build_soroban_contract(Path.cwd()) - kasmer.deploy_and_run(wasm, child_wasms, id=id) + kasmer.deploy_and_run(wasm, child_wasms, max_examples, id) sys.exit(0) @@ -173,9 +175,14 @@ def _argument_parser() -> ArgumentParser: kast_parser.add_argument('--output', metavar='FORMAT', type=KAstOutput, help='format to output the term in') test_parser = command_parser.add_parser('test', help='Test the soroban contract in the current working directory') + test_parser.add_argument( + '--max-examples', type=int, default=100, help='Maximum number of inputs for fuzzing (default: 100)' + ) _add_common_test_arguments(test_parser) - prove_parser = command_parser.add_parser('prove', help='Prove the soroban contract in the current working directory') + prove_parser = command_parser.add_parser( + 'prove', help='Prove the soroban contract in the current working directory' + ) prove_parser.add_argument( 'prove_command', default='run', @@ -194,6 +201,7 @@ def _add_common_arguments(parser: ArgumentParser) -> None: parser.add_argument('program', metavar='PROGRAM', type=file_path, help='path to test file') parser.add_argument('--backend', metavar='BACKEND', type=Backend, default=Backend.LLVM, help='K backend to use') + def _add_common_test_arguments(parser: ArgumentParser) -> None: parser.add_argument('--id', help='Name of the test function in the testing contract') parser.add_argument('--wasm', type=FileType('r'), help='Use a specific contract wasm file instead') From f43b9f0b9e13e8774c557594d9ad65516fc86baa Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 11 Dec 2024 17:22:14 +0300 Subject: [PATCH 4/8] add `--directory` option --- src/komet/komet.py | 28 ++++++++++++++++++++++------ 1 file changed, 22 insertions(+), 6 deletions(-) diff --git a/src/komet/komet.py b/src/komet/komet.py index 5d1ca0f..fe0a1c4 100644 --- a/src/komet/komet.py +++ b/src/komet/komet.py @@ -49,11 +49,13 @@ def main() -> None: wasm = Path(args.wasm.name) if args.wasm is not None else None if args.max_examples < 1: raise ValueError(f'--max-examples must be a positive integer (greater than 0), given {args.max_examples}') - _exec_test(wasm=wasm, max_examples=args.max_examples, id=args.id) + _exec_test(dir_path=args.directory, wasm=wasm, max_examples=args.max_examples, id=args.id) 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, id=args.id, proof_dir=args.proof_dir, bug_report=args.bug_report) + _exec_prove_run( + dir_path=args.directory, wasm=wasm, id=args.id, proof_dir=args.proof_dir, bug_report=args.bug_report + ) if args.prove_command == 'view': assert args.proof_dir is not None _exec_prove_view(proof_dir=args.proof_dir, id=args.id) @@ -79,7 +81,7 @@ def _exec_kast(*, program: Path, backend: Backend, output: KAstOutput | None) -> _exit_with_output(proc_res) -def _exec_test(*, wasm: Path | None, max_examples: int, id: str | None) -> None: +def _exec_test(*, dir_path: Path | None, wasm: Path | None, max_examples: int, id: str | None) -> None: """Run a soroban test contract given its compiled wasm file. This will get the bindings for the contract and run all of the test functions. @@ -87,6 +89,7 @@ def _exec_test(*, wasm: Path | None, max_examples: int, id: str | None) -> None: Exits successfully when all the tests pass. """ + dir_path = Path.cwd() if dir_path is None else dir_path kasmer = Kasmer(concrete_definition) child_wasms: tuple[Path, ...] = () @@ -96,7 +99,7 @@ def _exec_test(*, wasm: Path | None, max_examples: int, id: str | None) -> None: # 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. child_wasms = _read_config_file(kasmer) - wasm = kasmer.build_soroban_contract(Path.cwd()) + wasm = kasmer.build_soroban_contract(dir_path) kasmer.deploy_and_run(wasm, child_wasms, max_examples, id) @@ -104,15 +107,21 @@ def _exec_test(*, wasm: Path | None, max_examples: int, id: str | None) -> None: def _exec_prove_run( - *, wasm: Path | None, id: str | None, proof_dir: Path | None, bug_report: BugReport | None = None + *, + dir_path: Path | None, + wasm: Path | None, + id: str | None, + proof_dir: Path | None, + bug_report: BugReport | None = None, ) -> None: + dir_path = Path.cwd() if dir_path is None else dir_path kasmer = Kasmer(symbolic_definition) child_wasms: tuple[Path, ...] = () if wasm is None: child_wasms = _read_config_file(kasmer) - wasm = kasmer.build_soroban_contract(Path.cwd()) + wasm = kasmer.build_soroban_contract(dir_path) kasmer.deploy_and_prove(wasm, child_wasms, id, proof_dir, bug_report) @@ -205,3 +214,10 @@ def _add_common_arguments(parser: ArgumentParser) -> None: def _add_common_test_arguments(parser: ArgumentParser) -> None: parser.add_argument('--id', help='Name of the test function in the testing contract') parser.add_argument('--wasm', type=FileType('r'), help='Use a specific contract wasm file instead') + parser.add_argument( + '--directory', + '-C', + type=ensure_dir_path, + default=None, + help='The working directory for the command (defaults to the current working directory).', + ) From f571a318272eb211311aa3c508cc639f6927c3c4 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 11 Dec 2024 14:21:16 +0000 Subject: [PATCH 5/8] Set Version: 0.1.46 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 6ee33ba..79e0dd8 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.45 +0.1.46 diff --git a/pyproject.toml b/pyproject.toml index e82e651..69d07f7 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.45" +version = "0.1.46" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From 1599fb2c4d25540aa5de8c62a6a18be4aa067549 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Tue, 17 Dec 2024 10:59:36 +0300 Subject: [PATCH 6/8] fix `--directory`: find `kasmer.json` in the specified dir. --- src/komet/komet.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/komet/komet.py b/src/komet/komet.py index fe0a1c4..46e3027 100644 --- a/src/komet/komet.py +++ b/src/komet/komet.py @@ -98,7 +98,7 @@ def _exec_test(*, dir_path: Path | None, wasm: Path | None, max_examples: int, i # 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. - child_wasms = _read_config_file(kasmer) + child_wasms = _read_config_file(kasmer, dir_path) wasm = kasmer.build_soroban_contract(dir_path) kasmer.deploy_and_run(wasm, child_wasms, max_examples, id) @@ -120,7 +120,7 @@ def _exec_prove_run( child_wasms: tuple[Path, ...] = () if wasm is None: - child_wasms = _read_config_file(kasmer) + child_wasms = _read_config_file(kasmer, dir_path) wasm = kasmer.build_soroban_contract(dir_path) kasmer.deploy_and_prove(wasm, child_wasms, id, proof_dir, bug_report) From ecb827a15659c12c4927f46d0b2d0f9dc6c498b0 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Thu, 19 Dec 2024 13:08:54 +0300 Subject: [PATCH 7/8] update docstrings --- src/komet/kasmer.py | 39 +++++++++++++++++++++++++++++++++++---- 1 file changed, 35 insertions(+), 4 deletions(-) diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index 8b73a4e..e6e7e00 100644 --- a/src/komet/kasmer.py +++ b/src/komet/kasmer.py @@ -136,10 +136,18 @@ def kast_from_wasm(self, wasm: Path) -> 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. + """Takes a wasm soroban contract and its dependencies as kast terms and deploys them in a fresh configuration. + + Args: + contract: The test contract to deploy, represented as a kast term. + child_contracts: A tuple of child contracts required by the test contract. + init: Whether to initialize the contract by calling its 'init' function after deployment. Returns: A configuration with the contract deployed. + + Raises: + AssertionError if the deployment fails """ def wasm_hash(i: int) -> bytes: @@ -182,8 +190,15 @@ def call_init() -> tuple[KInner, ...]: def run_test(self, conf: KInner, subst: dict[str, KInner], binding: ContractBinding, max_examples: int) -> None: """Given a configuration with a deployed test contract, fuzz over the tests for the supplied binding. + Args: + conf: The template configuration. + subst: A substitution mapping such that 'Subst(subst).apply(conf)' gives the initial configuration with the + deployed contract. + binding: The contract binding that specifies the test name and parameters. + max_examples: The maximum number of fuzzing test cases to generate and execute. + Raises: - CalledProcessError if the test fails + AssertionError if the test fails """ from_acct = account_id(b'test-account') @@ -214,6 +229,16 @@ def run_prove( proof_dir: Path | None = None, bug_report: BugReport | None = None, ) -> APRProof: + """Given a configuration with a deployed test contract, prove the test case defined by the supplied binding. + + Args: + conf: The template configuration with configuration variables. + subst: A substitution mapping such that `Subst(subst).apply(conf)` produces the initial configuration with + the deployed contract. + binding: The contract binding specifying the test name and parameters. + proof_dir: An optional directory to save the generated proof. + bug_report: An optional object to log and collect details about the proof for debugging purposes. + """ from_acct = account_id(b'test-account') to_acct = contract_id(b'test-contract') name = binding.name @@ -245,9 +270,12 @@ def deploy_and_run( Args: contract_wasm: The path to the compiled wasm contract. + child_wasms: A tuple of paths to the compiled wasm contracts required as dependencies by the test contract. + max_examples: The maximum number of test inputs to generate for fuzzing. + id: The specific test function name to run. If None, all tests are executed. Raises: - CalledProcessError if any of the tests fail + AssertionError if any of the tests fail """ print(f'Processing contract: {contract_wasm.stem}') @@ -288,7 +316,10 @@ def deploy_and_prove( Args: contract_wasm: The path to the compiled wasm contract. - proof_dir: The optional location to save the proof. + child_wasms: A tuple of paths to the compiled wasm contracts required as dependencies by the test contract. + id: The specific test function name to run. If None, all tests are executed. + proof_dir: An optional location to save the proof. + bug_report: An optional BugReport object to log and collect details about the proof for debugging. Raises: KSorobanError if a proof fails From 2488d4210f370dd6688fce26969d5ee4d4b64bfa Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 19 Dec 2024 10:09:31 +0000 Subject: [PATCH 8/8] Set Version: 0.1.47 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 79e0dd8..9506d14 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.46 +0.1.47 diff --git a/pyproject.toml b/pyproject.toml index 69d07f7..c727f91 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.46" +version = "0.1.47" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ",