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. ", diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index 96934a1..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: @@ -179,11 +187,18 @@ 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. + 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') @@ -202,7 +217,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, @@ -212,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 @@ -236,14 +263,19 @@ 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, ...], max_examples: int = 100, id: str | None = None + ) -> None: """Run all of the tests in a soroban test contract. 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}') @@ -255,15 +287,21 @@ 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}') 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( @@ -278,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 diff --git a/src/komet/komet.py b/src/komet/komet.py index f3a0fcc..46e3027 100644 --- a/src/komet/komet.py +++ b/src/komet/komet.py @@ -47,11 +47,15 @@ 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) + if args.max_examples < 1: + raise ValueError(f'--max-examples must be a positive integer (greater than 0), given {args.max_examples}') + _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) @@ -77,7 +81,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(*, 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. @@ -85,6 +89,7 @@ def _exec_test(*, wasm: Path | 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, ...] = () @@ -93,24 +98,30 @@ def _exec_test(*, wasm: Path | None) -> None: # 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) - wasm = kasmer.build_soroban_contract(Path.cwd()) + child_wasms = _read_config_file(kasmer, dir_path) + wasm = kasmer.build_soroban_contract(dir_path) - kasmer.deploy_and_run(wasm, child_wasms) + kasmer.deploy_and_run(wasm, child_wasms, max_examples, id) sys.exit(0) 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()) + 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) @@ -173,9 +184,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('--wasm', type=FileType('r'), help='Test a specific contract wasm file instead') + 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='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', @@ -183,10 +199,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 +209,15 @@ 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') + parser.add_argument( + '--directory', + '-C', + type=ensure_dir_path, + default=None, + help='The working directory for the command (defaults to the current working directory).', + )