Multi-spec buffers: parallel, per-precision CVL verification

certora_autosetup/cache/content_cache.py

@@ -15,6 +15,19 @@
 from certora_autosetup.utils.constants import DIR_CERTORA_INTERNAL, DIR_CONTENT_CACHE
 
 
+def hash_text(text: str) -> str:
+    """SHA-256 of a string's UTF-8 bytes (first 16 hex chars) — the in-memory analog of
+    :meth:`ContentCache._hash_file`, for content that isn't on disk (e.g. an in-state spec buffer)."""
+    return hashlib.sha256(text.encode()).hexdigest()[:16]
+
+
+def hash_content_parts(parts: list[str]) -> str:
+    """Combine already-hashed content parts (e.g. ``"name:<hash>"`` and ``"extra:<flag>"`` strings)
+    into one 32-char cache key. The final step shared by :meth:`ContentCache.compute_cache_key` and
+    any in-memory content digest."""
+    return hashlib.sha256("\n".join(parts).encode()).hexdigest()[:32]
+
+
 class ContentCache:
     """Content-hash-based cache for arbitrary data keyed by file contents.
 
@@ -72,8 +85,7 @@ def compute_cache_key(
             for part in extra_key_parts:
                 parts.append(f"extra:{part}")
 
-        combined = "\n".join(parts)
-        return hashlib.sha256(combined.encode()).hexdigest()[:32]
+        return hash_content_parts(parts)
 
     def get(self, cache_key: str) -> dict[str, Any] | None:
         """Retrieve cached data for the given key.

composer/authoring/tools.py

@@ -259,7 +259,7 @@ def _verify_attempts(state: GatedGiveUpState) -> int:
         for msg in state.get("messages", [])
         if isinstance(msg, AIMessage)
         for call in msg.tool_calls
-        if call["name"] == "verify_spec"
+        if call["name"] == "submit_buffer"
     )
 
 

composer/prover/callbacks.py

@@ -1,5 +1,5 @@
 """Stream-event prover callbacks shared by the codegen prover tool and the
-source-pipeline ``verify_spec`` tool.
+source-pipeline buffer prover jobs.
 
 ``ProverEventCallbacks`` translates the ``ProverCallbacks`` lifecycle into the
 custom stream events the UI renders, keyed by tool_call_id. Both prover entry

composer/prover/cloud.py

@@ -7,6 +7,7 @@
 
 import asyncio
 import logging
+import shutil
 import tempfile
 from contextlib import asynccontextmanager
 from dataclasses import dataclass
@@ -159,6 +160,42 @@ def _results_api() -> ProverOutputAPI:
     return ProverOutputAPI(enable_cache=False)
 
 
+#: A fetch failure here is a *transport* fault, not a bad job: by the time we download documents
+#: the job has already polled ``SUCCEEDED``. Re-fetching the same completed job is cheap; re-running
+#: the whole proof (what the caller does if this context raises) throws away a finished — often
+#: hours-long — verification. So retry the fetch itself a few times with exponential backoff before
+#: giving up. POU retries at the individual-request level; this covers a whole-fetch failure that
+#: outlives those (e.g. a mid-transfer reset that exhausts the request-level retries on one file).
+_FETCH_MAX_ATTEMPTS = 3
+_FETCH_BACKOFF_BASE_S = 2.0
+
+
+async def _fetch_results(job_id: str, dest: Path) -> None:
+    """Download a completed job's sources + tree view into ``dest``, retrying a transient failure.
+
+    Each attempt starts from an empty ``dest`` so a partially-written archive from a failed attempt
+    cannot leave a truncated file behind. Never re-runs the job — only re-reads it.
+    """
+    for attempt in range(1, _FETCH_MAX_ATTEMPTS + 1):
+        try:
+            await asyncio.to_thread(
+                _results_api().fetch_sources_and_treeview_files, job_id, dest
+            )
+            return
+        except Exception as exc:
+            if attempt == _FETCH_MAX_ATTEMPTS:
+                raise
+            backoff = _FETCH_BACKOFF_BASE_S * 2 ** (attempt - 1)
+            logger.warning(
+                "Fetching results for completed job %s failed (attempt %d/%d): %s. "
+                "Re-fetching the finished job in %.0fs (not re-proving).",
+                job_id[:8], attempt, _FETCH_MAX_ATTEMPTS, exc, backoff,
+            )
+            for child in dest.iterdir():
+                shutil.rmtree(child) if child.is_dir() else child.unlink()
+            await asyncio.sleep(backoff)
+
+
 @asynccontextmanager
 async def cloud_results(
     run_result_link: str,
@@ -202,7 +239,5 @@ async def on_status(status: str) -> None:
         # tens of gigabytes on real jobs and used to exhaust the disk; across the
         # jobs measured here these two subtrees are ~3% of the archive. POU writes
         # them in the same layout the archive had, so the parse is unchanged.
-        await asyncio.to_thread(
-            _results_api().fetch_sources_and_treeview_files, cloud_job.job_id, dest
-        )
+        await _fetch_results(cloud_job.job_id, dest)
         yield (dest, runtime_ms)

composer/scripts/budget_math.py

@@ -347,7 +347,7 @@ def headroom_note(cap: float) -> str:
         "groups/`prover_links` exclude curtailed",
         "- rendered HTML (`autoprove-report-render`) shows the budget appendix",
         "- thread trail (`ap-trail export` + this script): the `<system-alert>` wrap-up "
-        "appears in the author transcript; no `verify_spec`/`feedback_tool` calls after it",
+        "appears in the author transcript; no `submit_buffer`/`feedback_tool` calls after it",
         "- `components_to_prover_runs.json` lacks curtailed entries",
         "",
         "## Caveats",

composer/spec/cvl_generation.py

@@ -269,16 +269,24 @@ async def _get_feedback(
     def _version_history(self) -> Sequence[str]:
         return ()
 
+def cvl_guidance_tools() -> list[BaseTool]:
+    """The dependency-free CVL *guidance* tools — no spec-writing tools. Used by the buffer-authoring
+    agent, which writes CVL through the buffer tools (put_buffer / edit_buffer) rather than put_cvl."""
+    return [
+        ERC20TokenGuidance.as_tool("erc20_guidance"),
+        UnresolvedCallGuidance.as_tool("unresolved_call_guidance"),
+    ]
+
+
 def static_tools() -> list[BaseTool]:
-    """The dependency-free CVL authoring tools. The property-management suite
-    (feedback / skip tools) is NOT here — it carries runtime deps; see
+    """The dependency-free CVL authoring tools — the single-``curr_spec`` writing tools plus guidance.
+    The property-management suite (feedback / skip tools) is NOT here — it carries runtime deps; see
     :func:`skip_tools` and :class:`FeedbackToolBase`."""
     return [
         put_cvl, put_cvl_raw,
         get_cvl(CVLGenerationState),
         edit_cvl(CVLGenerationState),
-        ERC20TokenGuidance.as_tool("erc20_guidance"),
-        UnresolvedCallGuidance.as_tool("unresolved_call_guidance"),
+        *cvl_guidance_tools(),
     ]
 
 

composer/spec/source/artifacts.py

@@ -100,7 +100,7 @@ def _write_conf(
         self, spec: SpecIdentity, base_config: dict | None, spec_path: Path,
     ) -> None:
         """The prover conf for the run: the generation's final ``state["config"]`` plus
-        the fixed run overlay (shared with the live ``verify_spec`` run). No-op if no
+        the fixed run overlay (shared with the live prover run). No-op if no
         base config."""
         if base_config is None:
             _log.warning("no base config for %s; skipping conf dump", spec.stem)