PR 3/3: Crucible backend (capstone) by ericeil · Pull Request #98 · Certora/AutoProver

ericeil · 2026-07-23T18:43:16Z

PR 3 of 3 — Crucible backend (capstone)

Part of the stacked split of eric/crucible (see docs/pr-split-plan.md).
Stack: master → eric/ecosystem → eric/rust → eric/crucible-app.
Base: eric/rust (PR #97) — review PRs #96 and #97 first.

The tip of the stack — the Solana verification application, wiring PR 1 (ecosystem) +
PR 2 (rust framework) + the upstream command sandbox together.

What this adds

composer/crucible/* and rust/crucible-app (the Crucible wheel)
Crucible RAG: committed manifest rust/crucible-app/crucible_kb.rag.json + shared
composer/scripts/rag_import.py, composer/rag/{import_format,db}.py, composer/tools/crucible_rag.py
ReportBackend "crucible" + render labels + as_report_backend
Sandbox default → launcher for crucible (fail-closed; the launcher itself is upstream)
test_scenarios/solana_vault + the crucible test gates — the vault sample also makes PR 2's
test_solana_gate runnable from here
docs/application-abstraction.md — the five pieces of an analyzed application / Rust app
framework (moved here from the ecosystem PR, where it did not belong), plus the crucible-*
design docs

Finalizes the PR 2 cross-cutting intermediates

rust/Cargo.toml re-adds the crucible-app workspace member.
rustapp/adapter.py swaps the tag cast back to the validating as_report_backend, now that
report/schema.py closes ReportBackend to {prover, foundry, crucible}.
Carries the crucible-specific sandbox tweaks: sandbox/recipes.py per-run RUSTUP_HOME;
docker-compose.sandbox.yml un-gated run-confined-build.

Verification

cargo build (all 4 crates) ✓
crucible-layer modules import ✓

Notes

Draft: the real-LLM gates were not run here — test_crucible_gate,
test_crucible_setup_gate, test_crucible_formalize_gate, test_crucible_e2e_gate.
(setup/formalize were verified green earlier this cycle against a real crucible build.)

🤖 Generated with Claude Code

The Solana verification application, wiring PRs 1–2 and the upstream command sandbox together: the `crucible_app` wheel (`rust/crucible-app` — harness authoring, the in-loop judge, per-component units), the crucible RAG corpus as a committed manifest plus the shared importer, the `solana_vault` scenario and the crucible gates, and the container vertical (`Dockerfile.crucible`, the compose overlays, the entrypoint's setup-db). Rebased onto `eric/rust`, which now carries the framework layer these sit on. Everything in this commit is crucible-owned; the framework changes the Crucible work produced (the driver's `preflight` phase, the abstract component unit, the declarative descriptor slots, the RAG seam) live in PR 2, where the rest of that layer already was. Adopting PR 2's `uv sync`-builds-the-workspace mechanism: * `crucible_app` is back in the `apps` group and `[tool.uv.sources]`, so a bare `uv sync` compiles it — `dev` includes `apps`, and the container image (which sets `UV_NO_DEV=1`) still gets neither. * Its crate carries `[tool.uv] cache-keys` like the others, so editing the crate recompiles the wheel with no manual `maturin develop`. `templates/**/*.j2` and `askama.toml` are keys here and not on the other crates because askama compiles the templates *into* the binary — editing a `.j2` changes the wheel exactly as editing a `.rs` does. * `rust/Cargo.lock` is committed (no longer gitignored) and regenerated to include `crucible-app`; `uv.lock` likewise. PR 2 kept the code for building the program **under analysis**; it doesn't belong to a layer every Rust backend shares (a Rust backend need not build a crate to validate a program, depend on the analyzed crate, or use the sandbox at all), so it came back here and registers into two seams PR 2 declares in `composer/rustapp/toolchain.py` — both empty there, keyed by chain: * `WORKSPACE_TOOLCHAINS["solana"]` → `composer.spec.solana.build.prepare_workspace`, the toolchain half of a wheel's `workspace_prep` plan: `cargo fetch` each `warm_dirs` unconfined, `cargo-build-sbf` the program confined + offline, place its IDL. The host still writes the plan's `files` and reports the IDL path back as the `idl` context key; it no longer knows what a build is. The rest of `solana/build.py` (`build_program`, `warm_cargo_cache`, the `Anchor.toml` / `declare_id!` program-id resolution, the IDL address fill-in) returns with it. * `SOURCE_CRATES["solana"]` → `composer/spec/cargo.py`'s manifest walk, which fills `AuthorInput.program_crate`. `prepare_workspace` re-resolves the crate itself rather than reading that wire copy, whose empty strings can't say whether anything was resolved. Also back: the sandbox build grants a confined sBPF build needs (the private per-run `RUSTUP_HOME`, the `PATH` `cargo-build-sbf` install tree, `~/.gitconfig`, the pinned registry protocol, `CARGO_NET_OFFLINE=true`), the `RUST_FORBIDDEN_READ` exclusions for the scratch dirs *this* backend creates in the workdir, and the `"crucible"` report vocabulary (its outcome/group labels, its `ReportTerms`, and its member of the closed `ReportBackend` set). The null Solana backend stays on PR 2's `"none"` tag — an all-UNKNOWN report should not borrow a real verifier's words. `test_crucible_granularity.py` drops its two `isinstance(x, FeatureUnit)` asserts: PR 2 removed `@runtime_checkable` from that protocol, on the grounds that a structural isinstance compares attribute names rather than signatures and so could not hold the Main-is-not-a-Unit line anyway. The unit's member assertions stay (they are the real check) and the type checker holds the line, as it does for the peer test in `test_null_solana_backend.py`. Verified: `pytest -m "not expensive"` 493 passed, 2 skipped, 17 deselected; `pyright` 0 errors. docs/pr-split-plan.md records the boundary this re-split settled on. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The capstone shipped the backend but three of the seams it was supposed to close were left open, so `console-crucible` could not run at all: * `crucible-app` did not compile. `Verdict::with_outcome` takes an `Outcome` enum (the SDK moved off free strings so a typo can't reach a report row as an unexplained UNKNOWN), but three call sites still passed `&str`. The `all(...)` closure in `validate` now threads `Outcome` too, which is what made the string form load-bearing. * `console-crucible` / `tui-crucible` had no entry points. The placeholder comment said they land in PR3 together with `composer.crucible_launch` — the module landed, the scripts didn't. * The `crucible_kb` RAG corpus was registered in neither half, so `validate_rag_db` rejected the descriptor at `build_application` time. The tools module was already present; this adds the connection (`CRUCIBLE_DEFAULT_CONNECTION` in `KNOWLEDGE_BASES`) and the deferred-import factory in `rag_env._FACTORIES`. `test_rag_env` pinned "nothing is registered at all" as the branch's resting state. That's now a behaviour test over an explicitly emptied registry, plus a regression test that `crucible_kb` validates in both halves. Verified: 519 passed, pyright clean, and tests/test_crucible_sandbox_gate.py passes against the real cargo-build-sbf + crucible CLI under the confined launcher. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Triaging klend's two counterexamples took an hour and a harness rebuild, and both turned out to be harness defects rather than program bugs. Everything needed to reach that conclusion was already on disk and thrown away. Three changes, in increasing order of how much they prevent rather than merely report: * **The crash's reproducing sequence reaches the report.** `finding_detail` now reads the `crash_<id>.meta.json` Crucible writes next to the payload and appends the iteration and the per-action name/success/error-code. Best-effort by design: missing or unparsable metadata degrades to exactly the previous one-line detail, because a finding must still report. * **A BAD verdict is flagged when the metadata alone shows it is a harness bug.** `HarnessSuspicion` names the two decidable smells — `InitialState` (fired on iteration 0, so the post-setup fixture already violates the invariant) and `ViolatingActionFailed` (fired on an action that reverted, so the transition the property is scoped to never happened). Both of klend's findings are caught, with the specific reason and the fix. An enum, not a bool-plus-string, so each variant carries just the evidence that justifies it; a violation following a *successful* action is deliberately left unflagged, since a marker on every finding is worthless. The flag rides on the FIRST line of `detail`, because that is what the live console shows; the sequence follows on later lines for the report. `adapter.py` now emits only that first line, keeping the one-line-per-verdict view intact. * **Assertion messages must carry their operands.** The root cause of the unreadable "total supply exceeds deposit_limit" was our own cheat sheet: it requires a custom message (to prefix the property title), and a custom message makes `fuzz_assert*` use it VERBATIM — the macro's built-in `(left != right)` dump is discarded. The guidance now demands format args and shows the contrast, and judge Criterion 7 rejects both an operand-less message and the precondition-scope error that produced both false positives (including that an `Option`-returning read is not a guard against a zeroed account, which deserializes into a default struct). Verified against the real klend crash files: both are flagged with the correct reason and full sequence. The 11 new triage tests use those two `meta.json` bodies verbatim as regression cases. Deferred, per discussion: re-validating the accumulated harness at end of run (later components silently broke earlier ones on this run) and namespacing per-component helpers. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The klend run delivered a crate that compiled for NO feature: two components each emitted an ungated `impl Fixture { fn read_token_balance }`, and rustc's E0592 fires on a duplicate inherent method regardless of module. All 14 gated builds had passed, because each assembled only its own section — the union was an artifact no step ever compiled. Fix the class rather than the instance. Each section now goes into a module gated on its Cargo feature, with a generated `#[invariant_test]` entry delegating into it: #[cfg(feature = "c_x")] mod section_c_x { use super::*; /* authored: pub fn c_x + helpers */ } #[cfg(feature = "c_x")] #[invariant_test] fn c_x(fixture: &mut Fixture) { section_c_x::c_x(fixture) } The `#[cfg]` — not the module — is what isolates: a module gives inherent impls no namespace (verified), so the module is simply the single item the gate hangs on, which is what avoids gating authored source item-by-item. Since each `#[invariant_test]` expands its own `fn main()` + `#[global_allocator]`, exactly one feature is ever enabled, so same-named helpers in different sections can never coexist in a build. The entry has to be generated because the macro expands `main()` as a SIBLING of the fn it annotates, so it cannot come from inside the module; it only reads the signature, never the body, which is what makes a delegating wrapper work. We do not reimplement `main` — that is ~100 lines of libafl wiring we would then own. `compile`, `validate` and `finalize` all wrap identically, so a gated build is now the deliverable restricted to one section rather than a differently-shaped artifact. That equivalence is the property that was missing. Two normalizations on authored source, both anchored on the known fn name: strip any `#[invariant_test]` the model adds anyway (it would expand `main()` inside the module — a link error, not something the revise loop can act on), and make the fn `pub` (called from the root; private is E0603). The prompt asks for a bare `pub fn` and explains that helper names can no longer clash. `finalize`'s dedupe survives for the case it was written for — two targets on one authored body — and now declares only the features it emits an entry for, since a feature whose `main()` does not exist is a link error, not a usable target. Verified by regenerating klend's real 14 sections through the new wrapping: 14/14 features build, against 0/14 as delivered. Still open (#4's other half): a per-feature build gate at end of run, to catch whatever cross-section conflicts this does not prevent. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Rebased onto the `eric/rust` that now sits on master, so the plugin system (#89/#96) is underneath this branch for the first time. Three seams moved: * `_extract_all` takes a `PluginPhaseManager`. `test_crucible_granularity` drives that helper directly, so it now passes one — and gets it from a new `PluginManager.without_plugins`, rather than depending on the ambient entry points happening to be empty (they are today; installing any plugin would otherwise silently change what this test measures). The granularity claim is about the unit axis; the hooks themselves are `test_plugin_scope.py`'s. * `PropertyPrompts` carries a bound `render_initial` renderer, not an `initial` template — the fake ecosystem's namespace follows. * `llm_factory` is gone from `composer.workflow.services`: an unused import in the three crucible gate modules. `RUST_FORBIDDEN_READ` keeps this branch's scratch-dir exclusions — PR 2 pushed them out of the front half precisely because they belong to the backend that creates the dirs, and that backend is this one. Only the doc comment's cross-reference changes, since master's Foundry filter is now the `fs_forbidden_read` predicate. Verified: pyright 0 errors, 653 passed / 17 deselected. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Every expensive Crucible/Solana gate died at setup with AttributeError: 'str' object has no attribute 'uploader' composer/workflow/services.py:382: uploader = provider.uploader() `standard_connections` takes a `ProviderService` — it asks it for an uploader and builds the memory tool from it — but these five gates still passed the literal string "anthropic". Production call sites (`rustapp/entry.py`, `pipeline/cli.py`, `workflow/executor.py`) were already correct, so only the tests were stale. Each gate already built `get_provider_for(tiered=...)`, just *inside* the `async with` and ten lines too late to use. Hoist it above the context manager and pass `.provider_service`. Found by running the full-vertical gate; it now passes end to end (0:50:32, 2 components / 20 properties / all GOOD), which also exercises the feature-gated section modules on a live run — 2 gated modules, 2 generated `#[invariant_test]` entries, and `cargo build --features=<f>` green for each declared feature. Note the shape of this: the routine suite stayed green the whole time because the drift sat only behind `-m expensive`, so every gate that could catch a real regression was unrunnable. Same reason the delivered crate went unchecked. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…uilt New §17 in crucible-component-units.md, next to §13 stage 5 and §16 where the per-feature build claim already lived. Covers what klend exposed (a green 283-property run whose delivered crate compiled for no feature), why no gate was at fault — a gated build is single-component by construction, the union exists only after `finalize`, and nothing revalidated it — and how feature-gating each section removes the class rather than detecting it, including the three properties that make the generated entry point legitimate. Records the per-feature build gate as a future direction with the sketch, its measured cost (~6 s per feature warm, and the CARGO_HOME/target reuse it depends on), and the reasoning for declining it now: gating removes the only failure it has ever caught, and it cannot affect pass/fail, so a broken package would need report-and-continue — new schema plus a phase for a warning — for a speculative catch. Revisit only if a conflict recurs despite gating. Also notes why the same bug hid twice: the per-feature assertion exists, but in an expensive-marked test on a 2-component scenario, too small to ever collide. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…test 10790fb added a `without_plugins` classmethod to `composer/pipeline/plugins.py` for one caller: `test_crucible_granularity`, which drives `_extract_all` directly and now has to hand it a `PluginPhaseManager`. That put a branch-only edit in a master-owned module for a test's benefit, so this PR no longer touches `plugins.py` at all — it is byte-identical to master again. The test builds the empty manager itself, `PluginManager({}, run)`. That reaches into the dataclass's fields positionally, which is what the named constructor existed to avoid; the tradeoff is deliberate and contained to a test. If the manager's field layout changes on master this breaks at construction rather than at a named seam. The intent the classmethod encoded is unchanged and still holds: the granularity claim is about the unit axis, so the phase runs with no plugins by construction rather than by the ambient entry points happening to be empty. pyright 0 errors, test_crucible_granularity 7 passed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The format, the importer and the KNOWLEDGE_BASES registry moved down to eric/rust (nothing in them is corpus-specific), so this branch keeps only what adopting the mechanism costs: the committed manifest, composer/tools/crucible_rag.py, and one entry in each of the two registries. composer/scripts/rag_import.py, composer/rag/import_format.py and tests/test_rag_import.py are now byte-identical to PR 2's copies. rag-import-format.md is the one shared file with a delta either way, so it gets a cross-cutting row in the split plan: PR 2 describes the mechanism with an empty registry, and this branch fills in the adopted state — §4's registry holds crucible_kb, and §7 gains a "first adopter" subsection carrying the facts that only make sense here (the 126-section manifest, the Dockerfile/entrypoint setup-db wiring, the demo, and how to regenerate the JSON after a crucible docs update). pyright 0 errors; 653 passed, 1 skipped, 17 deselected. The skip is tests/test_rag_import.py: this venv has no spaCy, which the importer pulls in via text_processors — it runs on PR 2's env, where the ragbuild group is installed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Mechanical, one rename per compiler error, and every accessor the SDK now provides deletes one the wheel used to carry: * `ctx_str`/`ctx_u64` are gone — `input.setup`, `input.idl` and `input.args.get("fuzz_timeout")` are fields on the input. * `arg_program`/`arg_program_crate` are gone with them: `AppArgs` carries the program and its (already resolved) crate, so the precondition check no longer re-splits `path:Name` out of `main_contract`, and no longer has a "no project_root in args" branch — the field is typed. * `validate` receives the target with the rows it covers, so the `self.units(input).filter(...)` re-derivation and the local `all` closure give way to `target.all` / `target.verdicts`. * `finalize` reads a `FinalizeInput`; `delivered_sections` loops `outcomes.delivered()` instead of digging six JSON keys. * the descriptor declares its preflight and setup steps as phase roles, so the two phase key/label pairs it used to repeat are written once. The kind checks (`input.kind == "setup"`) become matches on `Authored`, which is what caught the one latent bug here: `units()` returned rows for a preflight input as well as a component. Nothing called it that way, so nothing was broken — but the check said "not setup" where it meant "component", and the variant makes that unrepresentable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

ericeil force-pushed the eric/rust branch from 0b7bb90 to a44644b Compare July 23, 2026 18:50

ericeil force-pushed the eric/crucible-app branch 2 times, most recently from bb347ed to f003b03 Compare July 23, 2026 19:46

ericeil force-pushed the eric/rust branch from a44644b to 4bbeb08 Compare July 23, 2026 19:46

ericeil force-pushed the eric/crucible-app branch 2 times, most recently from a707702 to d890343 Compare July 23, 2026 19:58

ericeil force-pushed the eric/rust branch from 7ea1a77 to 9a670d1 Compare July 23, 2026 20:15

ericeil force-pushed the eric/crucible-app branch from d890343 to a985a45 Compare July 23, 2026 20:15

ericeil force-pushed the eric/rust branch from 9a670d1 to a077199 Compare July 23, 2026 22:18

ericeil force-pushed the eric/crucible-app branch from a985a45 to c4f8b82 Compare July 23, 2026 22:23

ericeil force-pushed the eric/rust branch from a077199 to 4a1ecda Compare July 23, 2026 22:36

ericeil force-pushed the eric/crucible-app branch 2 times, most recently from 0712081 to 85b3424 Compare July 23, 2026 23:55

ericeil force-pushed the eric/rust branch from 4a1ecda to 75b0bec Compare July 23, 2026 23:55

ericeil force-pushed the eric/crucible-app branch from 85b3424 to f1381ae Compare July 24, 2026 00:02

ericeil force-pushed the eric/rust branch from 75b0bec to 0671f74 Compare July 24, 2026 00:02

ericeil force-pushed the eric/crucible-app branch from f1381ae to 18ba037 Compare July 24, 2026 00:08

ericeil force-pushed the eric/rust branch from 0671f74 to 5361ead Compare July 24, 2026 00:08

ericeil force-pushed the eric/rust branch from 5361ead to 37277ad Compare July 31, 2026 04:07

ericeil force-pushed the eric/crucible-app branch 3 times, most recently from e2249eb to e369524 Compare July 31, 2026 23:55

ericeil force-pushed the eric/rust branch from ee74e24 to 372504a Compare August 3, 2026 21:30

ericeil force-pushed the eric/crucible-app branch from e369524 to b4a6919 Compare August 3, 2026 21:30

ericeil force-pushed the eric/rust branch from 372504a to 65e2043 Compare August 4, 2026 18:35

ericeil force-pushed the eric/crucible-app branch 2 times, most recently from d91ad75 to 00f3faf Compare August 4, 2026 23:42

ericeil and others added 3 commits August 5, 2026 11:39

ericeil and others added 7 commits August 5, 2026 11:39

ericeil force-pushed the eric/crucible-app branch from 00f3faf to b6832eb Compare August 5, 2026 19:11

Navigation Menu

Uh oh!

PR 3/3: Crucible backend (capstone) - #98

PR 3/3: Crucible backend (capstone)#98
ericeil wants to merge 10 commits into
eric/rustfrom
eric/crucible-app

ericeil commented Jul 23, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

ericeil commented Jul 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR 3 of 3 — Crucible backend (capstone)

What this adds

Finalizes the PR 2 cross-cutting intermediates

Verification

Notes

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

ericeil commented Jul 23, 2026 •

edited

Loading