Forcing sequential proof advancement in CI (#2608)

* forcing sequential proof advancement in CI

* moving logic to python code

* named parameters

* ensuring claim data is updated sequentially and before we hit the process pool map

* removing parallelism

* removing data races from digest updates

* stronger locks

* two runners and 45-minute timeout

kevm-pyk/src/kevm_pyk/__main__.py

@@ -14,6 +14,7 @@
 from pathlib import Path
 from typing import TYPE_CHECKING
 
+from filelock import SoftFileLock
 from pathos.pools import ProcessPool  # type: ignore
 from pyk.cli.pyk import parse_toml_args
 from pyk.cterm import CTermSymbolic
@@ -171,28 +172,29 @@ def digest(self) -> str:
         return hash_str(f'{claim_hash}{deps_digest}')
 
     def up_to_date(self, digest_file: Path | None) -> bool:
-        if not isinstance(digest_file, Path) or not digest_file.exists():
-            return False
-        digest_dict = json.loads(digest_file.read_text())
-        if 'claims' not in digest_dict:
-            digest_dict['claims'] = {}
-            digest_file.write_text(json.dumps(digest_dict, indent=4))
-        if self.claim.label not in digest_dict['claims']:
-            return False
-        return digest_dict['claims'][self.claim.label] == self.digest
+        with SoftFileLock(f'{digest_file}.lock'):
+            if not isinstance(digest_file, Path) or not digest_file.exists():
+                return False
+            digest_dict = json.loads(digest_file.read_text())
+            if 'claims' not in digest_dict:
+                return False
+            if self.claim.label not in digest_dict['claims']:
+                return False
+            return digest_dict['claims'][self.claim.label] == self.digest
 
     def update_digest(self, digest_file: Path | None) -> None:
         if digest_file is None:
             return
         digest_dict = {}
-        if digest_file.exists():
-            digest_dict = json.loads(digest_file.read_text())
-        if 'claims' not in digest_dict:
-            digest_dict['claims'] = {}
-        digest_dict['claims'][self.claim.label] = self.digest
-        digest_file.write_text(json.dumps(digest_dict, indent=4))
+        with SoftFileLock(f'{digest_file}.lock'):
+            if digest_file.exists():
+                digest_dict = json.loads(digest_file.read_text())
+            if 'claims' not in digest_dict:
+                digest_dict['claims'] = {}
+            digest_dict['claims'][self.claim.label] = self.digest
+            digest_file.write_text(json.dumps(digest_dict, indent=4))
 
-        _LOGGER.info(f'Updated claim {self.claim.label} in digest file: {digest_file}')
+            _LOGGER.info(f'Updated claim {self.claim.label} in digest file: {digest_file}')
 
 
 def init_claim_jobs(spec_module_name: str, claims: list[KClaim]) -> frozenset[KClaimJob]:

kevm-pyk/src/tests/integration/test_prove.py

@@ -329,7 +329,6 @@ def test_prove_rules(
     tmp_path: Path,
     caplog: LogCaptureFixture,
     no_use_booster: bool,
-    force_sequential: bool,
     use_booster_dev: bool,
     bug_report: BugReport | None,
     spec_name: str | None,
@@ -340,8 +339,8 @@ def test_prove_rules(
         tmp_path,
         caplog,
         no_use_booster,
-        force_sequential,
-        use_booster_dev,
+        force_sequential=True,
+        use_booster_dev=use_booster_dev,
         bug_report=bug_report,
         spec_name=spec_name,
     )
@@ -358,7 +357,6 @@ def test_prove_functional(
     tmp_path: Path,
     caplog: LogCaptureFixture,
     no_use_booster: bool,
-    force_sequential: bool,
     use_booster_dev: bool,
     bug_report: BugReport | None,
     spec_name: str | None,
@@ -369,8 +367,8 @@ def test_prove_functional(
         tmp_path,
         caplog,
         no_use_booster,
-        force_sequential,
-        use_booster_dev,
+        force_sequential=True,
+        use_booster_dev=use_booster_dev,
         bug_report=bug_report,
         spec_name=spec_name,
         workers=8,
@@ -381,7 +379,6 @@ def test_prove_dss(
     kompiled_target_for: Callable[[Path], Path],
     tmp_path: Path,
     caplog: LogCaptureFixture,
-    force_sequential: bool,
     bug_report: BugReport | None,
 ) -> None:
     for spec_file in [REPO_ROOT / 'tests/specs/mcd/vat-spec.k', REPO_ROOT / 'tests/specs/mcd-structured/vat-spec.k']:
@@ -390,9 +387,9 @@ def test_prove_dss(
             kompiled_target_for,
             tmp_path,
             caplog,
-            False,
-            force_sequential,
-            False,
+            no_use_booster=False,
+            force_sequential=True,
+            use_booster_dev=False,
             bug_report=bug_report,
             spec_name=None,
             workers=8,