Improved digest and proof version handling (#2064)

* Consolidate proof digests from index.json and digest, use IDs/version for setUp methods

* Set Version: 1.0.289

* Store IDs as ints not strings

* Set Version: 1.0.290

* Simplify functions, rename IDs to versions

* Always update digest

* Read warning when contract out of date, write digest file with formatting

* Fix --id argument not updated

* Set Version: 1.0.291

* Update kevm-pyk/src/kevm_pyk/cli.py

Co-authored-by: Everett Hildenbrandt <[email protected]>

* Set Version: 1.0.292

* Set Version: 1.0.292

* Use colon instead of comma as separator for test

* Fix formatting

* Fix <code> cell being taken from setUp proof

* Set Version: 1.0.294

* Set Version: 1.0.296

* Update kevm-pyk/src/kontrol/foundry.py

Co-authored-by: Palina Tolmach <[email protected]>

* Set Version: 1.0.297

* Simplify free_proof_version

* Delete package/debian/changelog

* Set Version: 1.0.298

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.297"
+version = "1.0.298"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.297'
+VERSION: Final = '1.0.298'

kevm-pyk/src/kevm_pyk/cli.py

@@ -167,7 +167,7 @@ def foundry_args(self) -> ArgumentParser:
     def foundry_test_args(self) -> ArgumentParser:
         args = ArgumentParser(add_help=False)
         args.add_argument('test', type=str, help='Test to run')
-        args.add_argument('--id', type=str, default=None, required=False, help='ID of the test')
+        args.add_argument('--version', type=int, default=None, required=False, help='Version of the test to use')
         return args
 
     @cached_property

kevm-pyk/src/kontrolx/__main__.py

@@ -1,9 +1,7 @@
 from __future__ import annotations
 
-import argparse
 import json
 import logging
-import re
 import sys
 from argparse import ArgumentParser
 from typing import TYPE_CHECKING
@@ -145,7 +143,7 @@ def exec_foundry_prove(
     max_depth: int = 1000,
     max_iterations: int | None = None,
     reinit: bool = False,
-    tests: Iterable[tuple[str, str | None]] = (),
+    tests: Iterable[tuple[str, int | None]] = (),
     exclude_tests: Iterable[str] = (),
     workers: int = 1,
     simplify_init: bool = True,
@@ -218,7 +216,7 @@ def exec_foundry_prove(
 def exec_foundry_show(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     nodes: Iterable[NodeIdLike] = (),
     node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (),
     to_module: bool = False,
@@ -234,7 +232,7 @@ def exec_foundry_show(
     output = foundry_show(
         foundry_root=foundry_root,
         test=test,
-        id=id,
+        version=version,
         nodes=nodes,
         node_deltas=node_deltas,
         to_module=to_module,
@@ -249,18 +247,18 @@ def exec_foundry_show(
     print(output)
 
 
-def exec_foundry_to_dot(foundry_root: Path, test: str, id: str | None, **kwargs: Any) -> None:
-    foundry_to_dot(foundry_root=foundry_root, test=test, id=id)
+def exec_foundry_to_dot(foundry_root: Path, test: str, version: int | None, **kwargs: Any) -> None:
+    foundry_to_dot(foundry_root=foundry_root, test=test, version=version)
 
 
 def exec_foundry_list(foundry_root: Path, **kwargs: Any) -> None:
     stats = foundry_list(foundry_root=foundry_root)
     print('\n'.join(stats))
 
 
-def exec_foundry_view_kcfg(foundry_root: Path, test: str, id: str | None, **kwargs: Any) -> None:
+def exec_foundry_view_kcfg(foundry_root: Path, test: str, version: int | None, **kwargs: Any) -> None:
     foundry = Foundry(foundry_root)
-    test_id = foundry.get_test_id(test, id)
+    test_id = foundry.get_test_id(test, version)
     contract_name, _ = test_id.split('.')
     proof = foundry.get_apr_proof(test_id)
 
@@ -275,14 +273,16 @@ def _custom_view(elem: KCFGElem) -> Iterable[str]:
     viewer.run()
 
 
-def exec_foundry_remove_node(foundry_root: Path, test: str, node: NodeIdLike, id: str | None, **kwargs: Any) -> None:
-    foundry_remove_node(foundry_root=foundry_root, test=test, id=id, node=node)
+def exec_foundry_remove_node(
+    foundry_root: Path, test: str, node: NodeIdLike, version: int | None, **kwargs: Any
+) -> None:
+    foundry_remove_node(foundry_root=foundry_root, test=test, version=version, node=node)
 
 
 def exec_foundry_simplify_node(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     node: NodeIdLike,
     replace: bool = False,
     minimize: bool = True,
@@ -301,7 +301,7 @@ def exec_foundry_simplify_node(
     pretty_term = foundry_simplify_node(
         foundry_root=foundry_root,
         test=test,
-        id=id,
+        version=version,
         node=node,
         replace=replace,
         minimize=minimize,
@@ -317,7 +317,7 @@ def exec_foundry_simplify_node(
 def exec_foundry_step_node(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     node: NodeIdLike,
     repeat: int = 1,
     depth: int = 1,
@@ -335,7 +335,7 @@ def exec_foundry_step_node(
     foundry_step_node(
         foundry_root=foundry_root,
         test=test,
-        id=id,
+        version=version,
         node=node,
         repeat=repeat,
         depth=depth,
@@ -349,17 +349,17 @@ def exec_foundry_step_node(
 def exec_foundry_merge_nodes(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     nodes: Iterable[NodeIdLike],
     **kwargs: Any,
 ) -> None:
-    foundry_merge_nodes(foundry_root=foundry_root, node_ids=nodes, test=test, id=id)
+    foundry_merge_nodes(foundry_root=foundry_root, node_ids=nodes, test=test, version=version)
 
 
 def exec_foundry_section_edge(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     edge: tuple[str, str],
     sections: int = 2,
     replace: bool = False,
@@ -377,7 +377,7 @@ def exec_foundry_section_edge(
     foundry_section_edge(
         foundry_root=foundry_root,
         test=test,
-        id=id,
+        version=version,
         edge=edge,
         sections=sections,
         replace=replace,
@@ -391,7 +391,7 @@ def exec_foundry_section_edge(
 def exec_foundry_get_model(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     nodes: Iterable[NodeIdLike] = (),
     pending: bool = False,
     failing: bool = False,
@@ -400,7 +400,7 @@ def exec_foundry_get_model(
     output = foundry_get_model(
         foundry_root=foundry_root,
         test=test,
-        id=id,
+        version=version,
         nodes=nodes,
         pending=pending,
         failing=failing,
@@ -436,15 +436,12 @@ def parse(s: str) -> list[T]:
     solc_to_k_args.add_argument('contract_file', type=file_path, help='Path to contract file.')
     solc_to_k_args.add_argument('contract_name', type=str, help='Name of contract to generate K helpers for.')
 
-    def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
-        pattern = r'^([^,]+)(?:,\s*(\S+))?$'
-        match = re.match(pattern, value)
-
-        if match:
-            groups = match.groups()
-            return groups[0], groups[1] if groups[1] is not None else None
+    def _parse_test_version_tuple(value: str) -> tuple[str, int | None]:
+        if ':' in value:
+            test, version = value.split(':')
+            return (test, int(version))
         else:
-            raise argparse.ArgumentTypeError("Invalid tuple format. Expected 'test, id' or 'test'")
+            return (value, None)
 
     foundry_kompile = command_parser.add_parser(
         'foundry-kompile',
@@ -489,15 +486,15 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
     )
     foundry_prove_args.add_argument(
         '--test',
-        type=_parse_test_id_tuple,
+        type=_parse_test_version_tuple,
         dest='tests',
         default=[],
         action='append',
         help='Limit to only listed tests, ContractName.TestName',
     )
     foundry_prove_args.add_argument(
         '--exclude-test',
-        type=_parse_test_id_tuple,
+        type=_parse_test_version_tuple,
         dest='exclude_tests',
         default=[],
         action='append',