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')