Refactor proof setup (#63)

* Make `method_to_apr_proof` public

* Move calls

* Extract method `get_contract_and_method`

* Extract function `collect_tests`

* Extract function `collect_setup_methods`

* Update digest directly

* Rename variables

* Move statement

* Simplify log messages

* Change `_run_cfg_group` to work with `FoundryTest`

* Change `method_to_apr_proof` to work with `FoundryTest`

* Extract nested function `run_prover`

* Extract function `method_to_initialized_cfg`

* Pull setup digest computation

* Eliminate else branch

* Extract function `_setup_cterm`

* Pull `setUp()` final state loading

* Eliminate parameter `save_directory`

* Remove parameter `exclude_tests`

* Fix number of `pytest` workers on CI

* Set Version: 0.1.16

---------

Co-authored-by: devops <devops@runtimeverification.com>

.github/workflows/test-pr.yml

@@ -82,9 +82,9 @@ jobs:
             docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` plugin foundry'
       - name: 'Run profiling'
         run: |
-          PROF_ARGS=
-          [ ${{ matrix.backend }} == 'booster' ] && PROF_ARGS=--use-booster
-          docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} make profile PROF_ARGS=${PROF_ARGS}
+          PROF_ARGS=--numprocesses=8
+          [ ${{ matrix.backend }} == 'booster' ] && PROF_ARGS+=' --use-booster'
+          docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} make profile PROF_ARGS="${PROF_ARGS}"
       - name: 'Tear down Docker'
         if: always()
         run: |
@@ -114,9 +114,9 @@ jobs:
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` plugin haskell foundry'
       - name: 'Run integration tests'
         run: |
-          TEST_ARGS=
-          [ ${{ matrix.backend }} == 'booster' ] && TEST_ARGS=--use-booster
-          docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS=${TEST_ARGS}
+          TEST_ARGS=--numprocesses=8
+          [ ${{ matrix.backend }} == 'booster' ] && TEST_ARGS+=' --use-booster'
+          docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}"
       - name: 'Tear down Docker'
         if: always()
         run: |

package/version

@@ -1 +1 @@
-0.1.15
+0.1.16

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.15"
+version = "0.1.16"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/kontrol/__main__.py

@@ -144,7 +144,6 @@ def exec_prove(
     max_iterations: int | None = None,
     reinit: bool = False,
     tests: Iterable[tuple[str, int | None]] = (),
-    exclude_tests: Iterable[str] = (),
     workers: int = 1,
     simplify_init: bool = True,
     break_every_step: bool = False,
@@ -181,7 +180,6 @@ def exec_prove(
         max_iterations=max_iterations,
         reinit=reinit,
         tests=tests,
-        exclude_tests=exclude_tests,
         workers=workers,
         simplify_init=simplify_init,
         break_every_step=break_every_step,
@@ -495,14 +493,6 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]:
         action='append',
         help='Limit to only listed tests, ContractName.TestName',
     )
-    prove_args.add_argument(
-        '--exclude-test',
-        type=_parse_test_version_tuple,
-        dest='exclude_tests',
-        default=[],
-        action='append',
-        help='Skip listed tests, ContractName.TestName',
-    )
     prove_args.add_argument(
         '--reinit',
         dest='reinit',

src/kontrol/foundry.py

@@ -250,21 +250,20 @@ def _escape_brackets(regs: list[str]) -> list[str]:
         regs = [reg.replace('(', '\\(') for reg in regs]
         return [reg.replace(')', '\\)') for reg in regs]
 
-    def matching_tests(self, tests: list[str], exclude_tests: list[str]) -> list[str]:
+    def matching_tests(self, tests: list[str]) -> list[str]:
         all_tests = self.all_tests
         all_non_tests = self.all_non_tests
         matched_tests = set()
         unfound_tests: list[str] = []
         tests = self._escape_brackets(tests)
-        exclude_tests = self._escape_brackets(exclude_tests)
         for t in tests:
             if not any(re.search(t, test) for test in (all_tests + all_non_tests)):
                 unfound_tests.append(t)
         for test in all_tests:
-            if any(re.search(t, test) for t in tests) and not any(re.search(t, test) for t in exclude_tests):
+            if any(re.search(t, test) for t in tests):
                 matched_tests.add(test)
         for test in all_non_tests:
-            if any(re.search(t, test) for t in tests) and not any(re.search(t, test) for t in exclude_tests):
+            if any(re.search(t, test) for t in tests):
                 matched_tests.add(test)
         if unfound_tests:
             raise ValueError(f'Test identifiers not found: {set(unfound_tests)}')
@@ -273,7 +272,7 @@ def matching_tests(self, tests: list[str], exclude_tests: list[str]) -> list[str
         return list(matched_tests)
 
     def matching_sig(self, test: str) -> str:
-        test_sigs = self.matching_tests([test], [])
+        test_sigs = self.matching_tests([test])
         if len(test_sigs) != 1:
             raise ValueError(f'Found {test_sigs} matching tests, must specify one')
         return test_sigs[0]
@@ -387,10 +386,15 @@ def get_optional_proof(self, test_id: str) -> Proof | None:
             return Proof.read_proof_data(self.proofs_dir, test_id)
         return None
 
-    def get_method(self, test: str) -> Contract.Method:
+    def get_contract_and_method(self, test: str) -> tuple[Contract, Contract.Method]:
         contract_name, method_name = test.split('.')
         contract = self.contracts[contract_name]
-        return contract.method_by_sig[method_name]
+        method = contract.method_by_sig[method_name]
+        return contract, method
+
+    def get_method(self, test: str) -> Contract.Method:
+        _, method = self.get_contract_and_method(test)
+        return method
 
     def resolve_proof_version(
         self,