UI/UX improvements (#53)

* fix `prove_parser` help text: `Test => Prove`

* add `--id <function_name>` option

* add `--max-examples` option

* add `--directory` option

* Set Version: 0.1.46

* fix `--directory`: find `kasmer.json` in the specified dir.

* update docstrings

* Set Version: 0.1.47

---------

Co-authored-by: devops <[email protected]>

package/version

@@ -1 +1 @@
-0.1.46
+0.1.47

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. <[email protected]>",

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

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,14 +81,15 @@ 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.
     The test functions are expected to be named with a prefix of 'test_' and return a boolean value.
 
     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,24 +184,40 @@ 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',
         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('--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
 
 
 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).',
+    )