PR 3/3: Crucible backend

ARCHITECTURE.md

@@ -103,7 +103,8 @@ five steps and never inspects anything backend-specific:
    depends on the other, so the prover's expensive AutoSetup/summary/invariant work overlaps
    with per-unit property inference. Property extraction fans out one agent per *unit* —
    `ecosystem.units(main)` — one per **component** of the main contract/program in both
-   ecosystems — bounded by a semaphore (`--max-concurrent`).
+   ecosystems ([docs/crucible.md](docs/crucible.md) §2) — bounded by a semaphore
+   (`--max-concurrent`).
 4. **Per-unit formalization** (parallel). For each unit's properties, the backend's
    `Formalizer.formalize()` is invoked. Results are cached by the backend's result type.
 5. **Report assembly** (shared, best-effort). The driver collects per-unit verdicts via a
@@ -257,8 +258,9 @@ the authoring agent. A callback protocol streams per-rule outcomes to the UI and
   Rust/Solana targets: a `SolanaApplication` analysis model, Solana-specific analysis/property
   prompts ([templates/solana/](composer/templates/solana/)), and per-component `units()` — one
   unit per `ProgramComponent`, the Solana analog of EVM's `ContractComponent`
-  ([docs/ecosystem-abstraction.md](docs/ecosystem-abstraction.md) §4). It plugs into the same
-  driver via the `SOLANA` ecosystem; the matching verification backend (Crucible) lands separately.
+  ([docs/crucible.md](docs/crucible.md) §2). It plugs into the same
+  driver via the `SOLANA` ecosystem; the matching verification backend is
+  [Crucible](docs/crucible.md).
 - **NatSpec** ([composer/spec/natspec/](composer/spec/natspec/)) — a *greenfield* workflow
   (its own asyncio orchestrator, not the generic driver) that goes from a design doc to Solidity
   interfaces, stub implementations, and CVL. A semaphore-serialized "semantic registry"

composer/crucible_launch.py

@@ -0,0 +1,22 @@
+"""Console entry points for the Crucible (Solana fuzzing) application.
+
+Crucible is now a *pure-Rust app* (``docs/rust-applications.md``): the ``crucible_app`` wheel + its
+descriptor define everything (the shared fixture, crate deliverable, workspace prep, sandbox
+grants, verdict summary), so these are the same two-line shims echoprover uses — no
+Crucible-specific Python package. ``import composer.bind`` runs first (inside
+``composer.rustapp.cli``) for the import-time DI / test-tape bootstrap.
+"""
+
+from composer.rustapp.cli import console_main, tui_main
+
+_MODULE = "crucible_app"
+
+
+def console_crucible() -> int:
+    """Run the Crucible application in console mode."""
+    return console_main(_MODULE)
+
+
+def tui_crucible() -> int:
+    """Run the Crucible application in the Textual TUI."""
+    return tui_main(_MODULE)

composer/layout.py

@@ -0,0 +1,22 @@
+"""Project-root directory names shared across backends.
+
+These two paths are the pair every surface agrees on: :data:`CERTORA_DIR` is
+what a user keeps, :data:`INTERNAL_DIR` is what a user ignores. They live here
+— not in :mod:`composer.spec.gen_types` — because :mod:`composer.sandbox` must
+import :data:`INTERNAL_DIR` without pulling pydantic. The 6.1 escape suite
+collects ``composer.sandbox`` in a guest that has only pytest and
+``annotated-types``.
+"""
+
+from pathlib import Path
+
+#: Deliverable layout under the project root (specs, confs, reports).
+CERTORA_DIR = Path("certora")
+
+#: Everything generated that is NOT a deliverable: diagnostics, scratch, and
+#: the build/fuzz outputs a run accumulates. A project that ignores this
+#: directory ignores all of it, and every source surface withholds it whole
+#: (``fs_forbidden_read``, ``RUST_FORBIDDEN_READ``). Spelled once because a
+#: subdirectory that grows without bound is only safe while it is *inside*
+#: the directory those rules name.
+INTERNAL_DIR = Path(".certora_internal")

composer/llm/anthropic.py

@@ -8,6 +8,7 @@
 from functools import cache
 
 import anthropic
+import httpx
 
 from composer.input.files import UploaderBase, ContentRenderer
 from composer.input.types import ModelConfiguration
@@ -225,8 +226,14 @@ def should_retry(self, exc: Exception) -> bool:
         and every 5xx, which covers 529 overloaded) plus connection-level
         failures (``APITimeoutError`` subclasses ``APIConnectionError``).
         400-class request errors are deterministic — an over-long prompt fails
-        identically on every attempt — and are deliberately excluded."""
-        if isinstance(exc, anthropic.APIConnectionError):
+        identically on every attempt — and are deliberately excluded.
+
+        ``httpx.TimeoutException`` is here because we stream: the SDK's own retries and its
+        exception wrapping both cover the *request*, and once it has handed the response stream to
+        the caller a stall surfaces raw from the transport, as ``httpx.ReadTimeout``. It means the
+        same thing as an ``APITimeoutError`` — the provider went quiet — and nothing has been
+        produced that a retry would duplicate."""
+        if isinstance(exc, (anthropic.APIConnectionError, httpx.TimeoutException)):
             return True
         if isinstance(exc, anthropic.APIStatusError):
             return exc.status_code in (408, 409, 429) or exc.status_code >= 500
@@ -293,7 +300,16 @@ def builder_for(
         return ChatAnthropic(
             model_name=self.model_name,
             max_tokens_to_sample=opts.tokens,
-            timeout=None,
+            # An explicit None DISABLES the SDK's timeouts (None != not-given), so a
+            # socket that dies silently mid-stream hangs the session forever. A float
+            # is a per-phase httpx timeout — for a streamed response, the max silence
+            # between chunks, not a cap on the whole turn.
+            timeout=300.0,
+            # Stream every request: a long authoring turn (Opus + thinking on a large
+            # prompt) can exceed the SDK's 600s non-streaming ceiling, and a silent
+            # 10-minute wait is long enough for NAT/idle killers to drop the socket
+            # (surfaces as APIConnectionError mid-run). Streaming keeps bytes flowing.
+            streaming=True,
             max_retries=8,
             stop=None,
             betas=betas,

composer/pipeline/core.py

@@ -56,7 +56,8 @@
 from composer.llm.types import CacheLevel
 from composer.input.files import Document
 from composer.spec.source.report.build import build_report
-from composer.spec.source.report.collect import ReportComponentInput, Verdict, EvidenceFetcher, Formalized
+from composer.spec.source.report.collect import Formalized, ReportComponentInput, Verdict
+from composer.spec.source.report.findings import FindingsPolicy
 from composer.spec.source.report.schema import (
     AutoProverReport, RuleName, ReportBackend, SourceEditRecord, VerificationArtifactRecord,
 )
@@ -204,10 +205,16 @@ async def fetch_verdicts(self, formalized: Formalized[FormT]) -> dict[RuleName,
         Never called for gave-up or budget-curtailed components."""
         ...
 
-    def findings_evidence(self) -> EvidenceFetcher | None:
-        """The per-rule evidence source for findings synthesis, or None if this backend produces no
-        findings. Returning None is how a backend opts out — the report then builds no findings for
-        it, with no backend-specific branching in the report layer. Default: None."""
+    def findings_policy(
+        self, outcomes: list[ComponentOutcome[FormT, U]]
+    ) -> FindingsPolicy | None:
+        """How this backend writes its violated rules up as findings, or None if it produces none.
+
+        Returning None is how a backend opts out — the report then builds no findings for it, with
+        no backend-specific branching in the report layer. Default: None.
+
+        Takes ``outcomes`` because a backend whose evidence is in its own results has nowhere else
+        to read it from; one whose evidence is a run-scoped store ignores them."""
         return None
 
     async def finalize(self, outcomes: list[ComponentOutcome[FormT, U]], run: PipelineRun) -> None:
@@ -695,18 +702,17 @@ async def _run(batch: _Batch[U]) -> ComponentOutcome[FormT, U]:
         for o in outcomes
         for pa in o.artifacts
     ]
-    findings_evidence = formalizer.findings_evidence()
+    findings = formalizer.findings_policy(outcomes)
     try:
         async def _report() -> AutoProverReport:
             return await build_report(
                 contract_name=source.contract_name, backend=formalizer.backend_tag,
                 components=inputs, llm=run.env.llm_lite(), fetch_verdicts=formalizer.fetch_verdicts,
                 source_edits=await formalizer.source_edits(outcomes, run),
                 verification_artifacts=artifact_records,
-                # Findings only when the backend supplies evidence — skip the heavy model otherwise.
-                findings_llm=run.env.llm_heavy() if findings_evidence else None,
-                fetch_evidence=findings_evidence,
-
+                # Findings only when the backend declared a policy — skip the heavy model otherwise.
+                findings_llm=run.env.llm_heavy() if findings else None,
+                findings=findings,
             )
         report = await run.runner(
             job=_report,

composer/pipeline/ecosystem.py

@@ -14,10 +14,12 @@
 Solana model + prompts and reuses the shared ``RUST`` language facet. See ``docs/ecosystem-abstraction.md``.
 """
 
+import re
 from dataclasses import dataclass
 from pathlib import PurePath
 from typing import Any, Callable, Collection, Literal, Mapping, TypedDict
 
+from composer.spec.gen_types import INTERNAL_DIR
 from composer.spec.context import SourceCode
 from composer.spec.code_explorer import CodeExplorerPromptParams
 from composer.spec.gen_types import TypedTemplate
@@ -250,13 +252,33 @@ def _evm_analysis_extra_input(source: SourceCode) -> list[str | dict]:
 #: Cargo/Anchor project layout: hide build output, VCS, lockfiles, and the JS side; keep the
 #: crate sources and `tests/`. A pattern suffices here — unlike the Foundry-shaped
 #: ``fs_forbidden_read``, nothing needs carving back out of an excluded directory.
-RUST_FORBIDDEN_READ = r"(^target/.*)|(^\.git.*)|(^node_modules/.*)|(.*\.lock$)"
-# NOTE: the confined-build scratch dirs (``.sandbox_cargo`` / ``.sandbox_rustup`` /
-# ``.sandbox_tmp`` and nested ``target/``) also have to be excluded — a build fills them with
-# hundreds of MB the source tools' file-listing would pull into the model's context — but that
-# extension lives with the *backend* that runs confined Rust builds inside the workdir. Nothing in
-# the front half, and nothing in the Rust application framework itself, creates them: a Rust
-# backend need not build a crate to validate the program, nor use the sandbox at all.
+#:
+#: The second group covers the hundreds of MB of build/scratch **this backend** generates inside the
+#: workdir mid-run (nothing in the front half or the Rust framework creates them), which the source
+#: tools' file-listing would otherwise pull into LLM context and blow the model's window:
+#:   • ``INTERNAL_DIR`` — the whole of it, which is what that directory is *for*: the sandbox's
+#:     per-run scratch (a private ``CARGO_HOME`` holding the entire cargo registry, ~19.5k files /
+#:     ~520 MB; a private ``RUSTUP_HOME`` whose ``toolchains`` symlinks the shared rustup home, so a
+#:     naive listing enumerates the whole Rust toolchain), the run's logs, and a backend's own
+#:     accumulating outputs. Named as a whole rather than subdirectory-by-subdirectory because the
+#:     next thing to grow without bound is the one nobody remembered to add: a klend run put 48k
+#:     files into a fuzzer corpus/crashes pair sitting outside this rule and lost 7 of 15 components
+#:     to prompts of 1.6–4.7M tokens against a 1M limit. This matches ``fs_forbidden_read``, which
+#:     has always withheld the directory whole for Solidity.
+#:   • nested ``target/``      — cargo build output below the root (e.g. the generated harness
+#:     crate's own ``target``, ~4k files, ~900 MB); the top-level ``^target/`` misses it.
+#: These are never source, so they are never readable by the source tools (belt-and-suspenders with
+#: each run's own cleanup: a re-run or cached CI workspace can leave them behind).
+RUST_FORBIDDEN_READ = "|".join(
+    (
+        r"(^target/.*)",
+        r"(^\.git.*)",
+        r"(^node_modules/.*)",
+        r"(.*\.lock$)",
+        rf"(^{re.escape(INTERNAL_DIR.as_posix())}/.*)",
+        r"(.*/target/.*)",
+    )
+)
 
 RUST = Language(
     name="rust",

composer/rag/db.py

@@ -49,14 +49,17 @@
 DEFAULT_CONNECTION: str = f"postgresql://rag_user:rag_password@{_RAG_HOST}:{_RAG_PORT}/rag_db"
 SANITY_DEFAULT_CONNECTION: str = f"postgresql://extended_rag_user:rag_password@{_RAG_HOST}:{_RAG_PORT}/rag_db"
 FOUNDRY_DEFAULT_CONNECTION: str = f"postgresql://foundry_rag_user:rag_password@{_RAG_HOST}:{_RAG_PORT}/rag_db"
+CRUCIBLE_DEFAULT_CONNECTION: str = f"postgresql://crucible_rag_user:rag_password@{_RAG_HOST}:{_RAG_PORT}/rag_db"
 
 # Logical knowledge-base tag -> default DB connection, for corpora ingested by the generic importer
 # (`composer.scripts.rag_import`). The tag is the one the manifest carries (== a wheel's
-# `rag_db_default`), so the import target and the runtime search tools resolve by one name —
-# `composer.tools.rag_env` requires both halves before a tag is usable. Empty until the first such
-# corpus lands with the application that declares it; the CVL/Foundry builders use the constants
-# above instead.
-KNOWLEDGE_BASES: dict[str, str] = {}
+# `rag_db_default`), so the import target and the runtime search tools resolve by one name — see
+# `composer.tools.rag_env`, which requires both halves before a tag is usable. The CVL/Foundry
+# builders keep using their constants above.
+KNOWLEDGE_BASES: dict[str, str] = {
+    # Crucible harness-authoring docs; manifest at `rust/crucible-app/crucible_kb.rag.json`.
+    "crucible_kb": CRUCIBLE_DEFAULT_CONNECTION,
+}
 
 
 type _RagHeader = str | None