Merge branch 'master' into fix/vector-rel-handles

deps/kwasm_release

@@ -1 +1 @@
-0.1.104
+0.1.105

flake.nix

@@ -2,7 +2,7 @@
   description = "komet - K tooling for the Soroban platform";
 
   inputs = {
-    wasm-semantics.url = "github:runtimeverification/wasm-semantics/v0.1.102";
+    wasm-semantics.url = "github:runtimeverification/wasm-semantics/v0.1.105";
     k-framework.follows = "wasm-semantics/k-framework";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";

package/version

@@ -1 +1 @@
-0.1.32
+0.1.33

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "komet"
-version = "0.1.32"
+version = "0.1.33"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -18,7 +18,7 @@ soroban-semantics = "komet.kdist.plugin"
 
 [tool.poetry.dependencies]
 python = "^3.10"
-pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.104", subdirectory = "pykwasm" }
+pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.105", subdirectory = "pykwasm" }
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

src/komet/kasmer.py

@@ -48,6 +48,7 @@
     from pyk.kast.inner import KInner
     from pyk.kore.syntax import Pattern
     from pyk.proof import APRProof
+    from pyk.utils import BugReport
 
     from .utils import SorobanDefinition
 
@@ -204,7 +205,12 @@ def make_steps(*args: KInner) -> Pattern:
         fuzz(self.definition.path, template_config_kore, template_subst, check_exit_code=True)
 
     def run_prove(
-        self, conf: KInner, subst: dict[str, KInner], binding: ContractBinding, proof_dir: Path | None = None
+        self,
+        conf: KInner,
+        subst: dict[str, KInner],
+        binding: ContractBinding,
+        proof_dir: Path | None = None,
+        bug_report: BugReport | None = None,
     ) -> APRProof:
         from_acct = account_id(b'test-account')
         to_acct = contract_id(b'test-contract')
@@ -228,7 +234,7 @@ def make_steps(*args: KInner) -> KInner:
 
         claim, _ = cterm_build_claim(name, lhs, rhs)
 
-        return run_claim(name, claim, proof_dir)
+        return run_claim(name, claim, proof_dir, bug_report)
 
     def deploy_and_run(self, contract_wasm: Path, child_wasms: tuple[Path, ...]) -> None:
         """Run all of the tests in a soroban test contract.
@@ -261,7 +267,11 @@ def deploy_and_run(self, contract_wasm: Path, child_wasms: tuple[Path, ...]) ->
             print('    Test passed.')
 
     def deploy_and_prove(
-        self, contract_wasm: Path, child_wasms: tuple[Path, ...], proof_dir: Path | None = None
+        self,
+        contract_wasm: Path,
+        child_wasms: tuple[Path, ...],
+        proof_dir: Path | None = None,
+        bug_report: BugReport | None = None,
     ) -> None:
         """Prove all of the tests in a soroban test contract.
 
@@ -283,7 +293,7 @@ def deploy_and_prove(
         for binding in bindings:
             if not binding.name.startswith('test_'):
                 continue
-            proof = self.run_prove(conf, subst, binding, proof_dir)
+            proof = self.run_prove(conf, subst, binding, proof_dir, bug_report)
             if proof.status == ProofStatus.FAILED:
                 raise KSorobanError(proof.summary)
 

src/komet/komet.py

@@ -9,6 +9,7 @@
 from tempfile import NamedTemporaryFile
 from typing import TYPE_CHECKING
 
+from pyk.cli.args import bug_report_arg
 from pyk.cli.utils import file_path
 from pyk.kdist import kdist
 from pyk.ktool.kprint import KAstOutput, _kast
@@ -25,6 +26,8 @@
     from collections.abc import Iterator
     from subprocess import CompletedProcess
 
+    from pyk.utils import BugReport
+
 
 sys.setrecursionlimit(4000)
 
@@ -48,7 +51,7 @@ def main() -> None:
     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, proof_dir=args.proof_dir)
+            _exec_prove_run(wasm=wasm, 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)
@@ -98,7 +101,7 @@ def _exec_test(*, wasm: Path | None) -> None:
     sys.exit(0)
 
 
-def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None) -> None:
+def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None, bug_report: BugReport | None = None) -> None:
     kasmer = Kasmer(symbolic_definition)
 
     child_wasms: tuple[Path, ...] = ()
@@ -107,7 +110,7 @@ def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None) -> None:
         wasm = kasmer.build_soroban_contract(Path.cwd())
         child_wasms = _read_config_file()
 
-    kasmer.deploy_and_prove(wasm, child_wasms, proof_dir)
+    kasmer.deploy_and_prove(wasm, child_wasms, proof_dir, bug_report)
 
     sys.exit(0)
 
@@ -172,6 +175,7 @@ def _argument_parser() -> ArgumentParser:
     )
     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')
 
     return parser

src/komet/proof.py

@@ -15,24 +15,30 @@
     from pathlib import Path
 
     from pyk.kast.outer import KClaim
+    from pyk.utils import BugReport
 
 
 @contextmanager
-def _explore_context() -> Iterator[KCFGExplore]:
-    with cterm_symbolic(definition=symbolic_definition.kdefinition, definition_dir=symbolic_definition.path) as cts:
+def _explore_context(id: str, bug_report: BugReport | None) -> Iterator[KCFGExplore]:
+    with cterm_symbolic(
+        definition=symbolic_definition.kdefinition,
+        definition_dir=symbolic_definition.path,
+        id=id if bug_report else None,
+        bug_report=bug_report,
+    ) as cts:
         yield KCFGExplore(cts)
 
 
 class SorobanSemantics(DefaultSemantics): ...
 
 
-def run_claim(id: str, claim: KClaim, proof_dir: Path | None = None) -> APRProof:
+def run_claim(id: str, claim: KClaim, proof_dir: Path | None = None, bug_report: BugReport | 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(symbolic_definition.kdefinition, claim=claim, logs={}, proof_dir=proof_dir)
 
-    with _explore_context() as kcfg_explore:
+    with _explore_context(id, bug_report) as kcfg_explore:
         prover = APRProver(kcfg_explore)
         prover.advance_proof(proof)