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

Two defects in the same function, both found by the 2026-08-07 rerun. The initial-state smell keyed on `iteration == 0`, read as "before the fuzzer changed anything". But Crucible's `iteration` is the fuzzer's GLOBAL test-case counter — which input this was, not how much ran within it — and `modes.rs` resets it to 0 outright when replaying a saved crash. The rerun produced the disproof: `crash_752c6358904f0e14`, iteration 0, one action that RAN, invariant violated after it. A genuine finding the old rule would have stamped SUSPECT HARNESS BUG, which is the same inversion the negative-action fix just removed from the other branch. Key on the sequence instead: no action succeeded — an empty one, or one whose every step failed — means nothing moved the chain off the post-setup state. That is the condition `iteration == 0` was standing in for, and it is strictly better: klend's `crash_ad707f0d6fef8cca`, the case that motivated the smell, had one FAILED action, so it stays correctly diagnosed while a first-iteration finding no longer trips. Second, the rendered sequence hid the only field that could explain itself. `success` is the ACTION's own `-> bool`; `error_code` is the TRANSACTION's result. For a negative action they diverge by design — it returns `true` for making the attempt while the instruction is expected to be rejected. That divergence was read as an upstream inconsistency and suppressed, so the rerun printed 1. reinitialize -> OK 2. reinitialize -> OK 3. init_without_signer -> OK beside a GOOD verdict for the property saying re-init must fail: the report contradicting itself, with the distinction that IS the finding erased. Rejected attempts now render `-> OK (tx rejected: <code>)` and one that went through stays bare. Regression cases are the real metadata from both runs. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The preflight emitted `src/probe.rs` (a section), `src/gate_root.rs` (a root just for the gates) and a manifest; the setup gate rebuilt the same three; and `crate_root` then assembled `src/main.rs` separately. The deliverable carried both roots, and `gate_root.rs` was a byte-identical prefix of `main.rs` — 413 of its 426 lines duplicated on the e2e run. Now each step writes the crate it is actually gating: - Preflight builds a crate of exactly one file, `src/preflight.rs`: the skeleton fixture and a gated `#[invariant_test]` entry with its body inline. Nothing to delegate to, so no section file, and nothing analyzed yet, so no other target. - Setup builds `src/main.rs` itself. It is the first callout holding both halves the real root needs, now that `Authored::Setup` carries the unit set — the host already had it in `begin` and simply wasn't passing it. Declaring the components before their section files exist costs that build nothing: a `#[cfg]`-disabled `mod` is stripped before rustc resolves its file. - `crate_root` renders the same files from the same two inputs. It cannot go away: the host serves a cached setup spec without calling `compile`, so on that path nothing else puts the crate on disk. Same renderer, so the second write is byte-identical rather than a second assembly to keep in step. `units` is deliberately outside `_setup_identity`: it decides scaffolding, not content, so a changed slug must not discard a still-correct fixture. `gate_root.rs` is gone. `src/main.rs` is written before it is known to compile, which it was not before — a setup that exhausts its revise budget now leaves a non-compiling root at the deliverable's path. Accepted deliberately: a failed setup produces no harness either way, and the last attempt is a more useful artifact than an absent file. Also renames the wheel's own build target from `probe` to `preflight`, and hoists `section_entry.j2`'s explanation of the `#[cfg]`/`#[invariant_test]` mechanism into `root_layout.j2`, emitted once per root instead of once per target — it describes the layout, not any one entry. Each component now costs 10 lines of scaffolding instead of 27. Validated end to end: the vault e2e gate passes, and klend (15 components, 411 properties, IDL path) builds a 4,705-line root declaring 15 absent modules. Its `main.rs` came back byte-identical across three separate cache-hit `crate_root` writes on runs where the setup gate never executed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Three components died on `InvalidUpdateError: At key 'curr_spec'` across two klend runs — 74 properties, no spec and no verdicts for any of them. It fires when the model emits two spec-writing tool calls in one turn: every write replaces the whole buffer, tool calls in a turn are one graph step, and `curr_spec` is the one field in `AuthoringExtra` without a reducer. Its two siblings have one precisely because they take several writes per step. Writes up the mechanism, why a last-write-wins reducer would be worse than the crash (both edits are computed from the same pre-step text, so keeping one silently discards the other), and the fix: refuse every write after the first in a turn, through the refusal path `apply_spec_update` already has, so the model re-issues them one at a time and nothing is lost. Shared, not Crucible's: Foundry, Crucible and CVL all extend `AuthoringExtra` and none redeclares the field, so the fix belongs at `apply_spec_update` — the one place every write in the repo funnels through. Only Crucible has been observed failing this way; the doc is explicit that this is an inference about exposure rather than evidence about the others. Not implemented here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

A run used to scatter its generated directories across the project root: `fuzz/<program>/` (the deliverable crate), `.sandbox_cargo/`, `.sandbox_rustup/` and `.sandbox_tmp/` (the command sandbox's per-run scratch) — four top-level dirs a user has to learn about and ignore, next to the `certora/` and `.certora_internal/` that already mean exactly "generated deliverable" and "generated diagnostic". Both halves now land where they belong. **The harness crate → `certora/crucible/fuzz/<program>/`.** Crucible's CLI defaults to `./fuzz/<program>/` but takes a global `-C/--harness-dir`, so the crate sits beside the reports and metadata the same run renders. `HARNESS_ROOT` is the one place the layout is spelled; `HarnessSpec::dir`/`path` replaced the ten `format!("fuzz/{program}/…")` sites, and both `crucible run` invocations pass `-C`. **`crucible run` chdirs into the crate, so its own relative paths are depth-sensitive.** Two of them: the path dep on the program's crate (ours, and now derived from `to_project_root`) and the `.so` the fixture loads — which was a literal in the *prompt*, copied into every authored fixture. The crate root now declares `const PROGRAM_SO` and the cheat sheet asks for that name, so the author never counts `../`. Same division as `SECTION_FN`: the model writes a constant and the wheel owns what varies. A wrong path here would have compiled fine and failed at `setup()`, which is the failure mode this removes rather than re-anchors. **The crate ships a `.gitignore`.** `find_fuzz_binary` pins `target/<profile>/invariant_test`, so `CARGO_TARGET_DIR` cannot be redirected: ~900 MB of build output plus the per-test `crashes/` land inside a directory users are now meant to commit. The fuzzer's `./corpus` and `./output` resolve against the *project* root instead (crucible passes the process cwd to `resolve_path`), which is also why `crash_meta_paths` needed only its second entry moved. **The sandbox scratch → `.certora_internal/sandbox/{cargo,rustup,tmp}`.** Same argument, reached from the other side: it is per-run, non-source and enormous, so it belongs under the directory every project already ignores and the source tools already withhold. `RUST_FORBIDDEN_READ` now excludes one prefix instead of three. Two things this breaks. A cached setup spec or a recorded tape from before this carries the old `.so` literal at the old depth. And `-C` is recent in crucible (`f7a1c38`); an older installed CLI fails with a clap error rather than anything diagnostic, which `validate_preconditions` does not yet detect — it checks that the binary exists, not that it takes the flag. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`lib.rs` had grown to 3230 lines holding everything the wheel does: the descriptor, the name derivation, the crate rendering, every prompt, the crash triage, and three test modules covering all of it. The SDK next door is already organized the way this wants to be — one module per part of the seam, addressed through the module that owns it — so this follows that shape. `app.rs` is the seam and nothing else: the `Backend` impl, each callout a few lines over the module that owns its material (`declaration`, `toolchain`, `layout`, `harness`, `section`, `prompts`, `facts`, `templates`, `build_log`, `triage`). `lib.rs` is now the map: crate docs, the module list, `export_app!`. The code moved verbatim, with three exceptions worth naming: a duplicated three-line doc comment above `api_facts` is now single; `validate_preconditions`, `descriptor`, `author_prompt` and `judge_instruction` are one-line delegations to the module that holds what they used to spell inline. **The descriptor's module is `declaration`, not `descriptor`.** `export_app!` emits one crate-root `#[pyfunction]` per callout, so a module named after one of them collides with the generated item — `mod descriptor` failed to compile on exactly that, and the same trap is waiting for `compile`, `validate`, `finalize` and the rest. There is a comment at the macro invocation saying so. Modules are private and items `pub(crate)`: the crate's only public surface is the PyO3 module, so nothing is re-exported and the crate docs name the modules in backticks rather than intra-doc links (a public doc linking a private item is a rustdoc warning). Tests moved with the code they test. The three blocks (`template_parity`, `section_isolation`, `crash_triage`) are redistributed into each module's own `#[cfg(test)] mod tests` — the SDK's convention — with the fixtures more than one of them needs hoisted into `testkit`. Same 59 tests, nothing dropped, added or weakened; `at()` takes the program it was implicitly carrying. Four doc pointers named `lib.rs` for something that moved (`ProgramTypes`, `attribute_finding`, `api_facts`, the declared event kinds) and now name the file that holds it. The line-anchored ones in `crucible-component-units.md` §8.1 and `crucible-unit-granularity.md` are left alone: they record what the code was before a planned change, so repointing them at today's files would misreport history. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The relocation under `certora/` moved the harness crate to a path that is no longer crucible's default, so `-C` started carrying a directory the CLI had not seen before — and `-C` is the one path it takes without resolving. Every other path `fuzz_run` accepts goes through its `resolve_path(&cwd, …)`; the harness dir goes straight into `resolve_fuzz_dir`, which returns it as given. Relative in, relative out. That relative dir is then used twice: `find_fuzz_binary` joins it to get `<dir>/target/release/invariant_test`, and the same dir becomes the spawned child's cwd. On Unix the chdir precedes the exec, so the equally-relative binary path resolves a *second* time, against the crate — `<dir>/<dir>/target/release/ invariant_test`. `find_fuzz_binary`'s own `exists()` check passes, because it runs before the chdir in the parent's frame; the spawn then fails with a bare `No such file or directory`, *after* a successful build. Preflight died 120s in on a crate that had compiled cleanly 51s earlier, with a message naming neither the path it wanted nor the one it had. Invisible until now: without `-C` the base is `current_dir()`, so `fuzz_dir` was always absolute and could not be re-resolved. `dir_arg` joins the workdir the host already materialized the crate in, so what reaches `-C` is absolute at both call sites — the dry-run gate in `compile` and the fuzz run in `validate`. `dir` keeps its own meaning, the crate-relative prefix every rendered file is spelled from, and says which of the two to hand the CLI. Fixing it here rather than upstream is not a workaround for the CLI's asymmetry: an absolute `-C` is unambiguous whatever the callee does with it, and the wheel knows the absolute location already. The CLI resolving `-C` like its siblings would still be worth doing for the next caller. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The 6.1 escape suite runs in a deliberately bare env — `uv run --no-project` with pytest, the repo on `PYTHONPATH`, no project build — on the premise its header states outright: the suite imports stdlib plus `composer.sandbox.*`, and `composer.sandbox.*` is stdlib. That premise expired at `bd582dd`, which gave `config.py` a `from annotated_types import Ge` to carry the `Ge(0)` bound on `BackendSpec.timeout_s`. Everywhere else that name resolves as a pydantic transitive; in the guest nothing pulls pydantic, so collection died on `ModuleNotFoundError` before a single kernel assertion ran. Adding the dep rather than dropping the import: the bound is read, not decorative. `test_wire_roundtrip.py` pulls `Ge`/`Le` off each mirrored field to generate values inside the *Rust* domain, so `timeout_s` is exercised as the `u64` it mirrors instead of as a Python int. Removing `Ge(0)` would leave that generator drawing negatives against a field whose deserializer refuses them — the drift check quietly weakened to make a provisioning script simpler. `annotated_types` is three files with no dependencies of its own, and it remains the only non-stdlib import anywhere under `composer/sandbox/`, so the env stays as light as the header claims. The header now says which dep and why, because the next import to arrive will land the same way and the comment is what decides whether anyone notices. Verified both directions locally, isolated: without the flag, the CI traceback reproduces at collection; with it, two tests collect. The assertions themselves are Landlock/seccomp-mediated and only mean anything on the guest's 6.1 kernel. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Two independent paths let a documented finding report as a clean row, both found in the klend run of 2026-08-10: its Oracle-Driven Refresh commentary records two counterexamples, and report.html shows one. `expect_check_failure` was session state that stopped at the publish gate. `SessionResult` carried it and `RustFormalResult` dropped it, so a check the author declared broken reported as whatever its campaign happened to observe — which for three of klend's four declared findings was "No counterexample". The declaration and the wheel's verdict now meet on `RustFormalResult`, whose `reported_verdicts()` both the report and the console rollup read. A declared check reports BAD either way; the detail separates a run that reproduced the finding (its counterexample) from one that did not (`NOT REPRODUCED`, since that claim rests on the author's reading alone). And the campaign stopped at its first crash, so the other 25 checks sharing that target were stamped GOOD after eleven test cases. That was `--mode explore` quietly implying `--stop-on-crash`, not anything about fuzzing: without it the fuzzer records each novel crash, prints a `[FUZZ_FINDING]` line and keeps going. The wheel spells the mode's settings out and omits the flag, `findings` parses every marker line rather than the first, and `Target` gains an `Exploration` so the partial run an author iterates against may still stop early — it never stamps, and the checks it abandons now say UNKNOWN rather than claiming to hold. Wire change, so the wheel needs a rebuild: uv sync --group test --group ci --group ragbuild --group apps \ --extra cpu --extra certora-cli Crucible dedups crashes by action-variant sequence, so two properties refuted along the same sequence of action types still yield one finding. GOOD from a full campaign means "explored to budget and not refuted" — a real claim, and still not proof. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Four reporting gaps the klend run of 2026-08-10 exposed, all of them inside the wheel or the Rust adapter — the shared report's renderer, template and schema are untouched. **Every verdict carries its campaign.** A GOOD from a ten-minute campaign is a real claim and one from a twelve-second campaign is nearly none, and a report row shows only its check, its outcome and its message. klend's 375 green rows said nothing about the runs behind them, and `duration_seconds` was null on all 376. `campaign.rs` ends every verdict with the component it came from and what the campaign spent against what it was allowed, reading the count off Crucible's own `Final stats:` line and degrading to the wall clock when there isn't one. Nothing shared had to change: `render.py` passes `message` through whatever the outcome, and the template renders it. The note goes last, and the component name first within it. A BAD verdict's first line is the only one the live console shows, so accounting must never displace a counterexample; and the report's groups are synthesized across components, so nothing else on a row says whose commentary explains it. **FINDINGS.md.** `finalize` is the hook for run-level artifacts, and by then the host holds every component's verdicts, declarations, skips and commentary at once. It now writes what failed and why, what each component declined beside what it checked, and a link to every commentary — the answer to "what did this run find", which a 433 KB property-keyed report with no anchors and one failing row in section 15 of 62 is the wrong shape for. **A source-confirmed defect is a finding, not a gap.** klend filed two bugs whose reasons open "KNOWN VULNERABILITY" and "The bug is real (confirmed in source: …)" through `record_skip`, so they rendered under "Formalization gaps" beside 31 real ones. The author prompt now routes those to `expect_check_failure` with a `// FINDING:` comment naming the source evidence, which the previous commit renders as a finding resting on the author's reading. The judge moves with it: a fn that asserts nothing is Criterion 1 on its face, so without this the judge would reject the exact handling the author was told to use — it is now told to judge the evidence instead, and to reject a suspicion or a property some action sequence could actually have observed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

33 of klend's 411 proposed properties were declined as unformalizable, and every one of them was decided when the property was *worded* — one phase before anything tried to check it. Four shapes account for all 33, and `backend_guidance.j2` is the only prose that reaches extraction, which runs before the fixture exists. The premise it was missing: a property becomes a predicate over accounts, evaluated between actions, with no pre-state and no knowledge of which instruction just ran. From that: - a per-call delta ("after switching groups the obligation is stale") is not checkable, but the standing relation it protects usually is — the same run formalized `obligation_fresh_implies_all_reserves_fresh`, which is that claim's observable content. 10 of the 33. - a rejection or liveness claim needs the exact attempt named, because the fixture is built FROM these properties: name it and it gets an action that makes the attempt and records the outcome, leave it at "must fail" and it gets an action whose bool is discarded. 9 of the 33, and klend's own reasons say so nearly verbatim. - constrain what the program writes, not what the harness writes. Asserting bounds on oracle bytes the harness wrote, or that an overflow cannot happen when the harness's own `1 + v % 1_000_000` is what prevents it, holds under every implementation including a broken one. 8 of the 33. - name the account fields that decide it; a bonus rate computed and stored nowhere leaves nothing to read. 5 of the 33. Plus two facts better known than worked around: a panic and a returned `Err` are indistinguishable after rollback, and a value a transaction perturbs and restores is invisible to a between-actions observer. This does not ask for fewer properties. A declined property with a precise reason is a good outcome; the win would be properties moving into the checked list, not off the proposal list. docs/crucible-uncheckable-properties.md records the baseline to measure a rerun against — and that this is prompt prose against an LLM phase, so it is unverified until one runs. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

A GOOD row said what the campaign spent but nothing about what it reached, and those are different claims. Measuring the klend run of 2026-08-10 found 26 of klend's 63 instruction handlers never entered and only 44 of the harness's 92 actions ever succeeding — so most of that report's 375 green rows sat over code the suite never executed. Nothing on a row could have shown that. Crucible already prints all of it. Edge and branch tracking runs to steer the fuzzer, so `[FUZZ_PULSE]` carries edges, branches and `discovered: N/M actions` on every campaign whether or not coverage was asked for; the run captured that stdout and dropped it. The note now carries it. That line is also where the execution count comes from. `reported_iterations` reads `[STATEFUL] Final stats:`, which only a stateful run prints — this backend never passes `--stateful`, so no klend campaign ever emitted one and every note degraded to bare wall clock. It stays as the fallback. LCOV comes from the campaign rather than a second pass: `--coverage` costs ~2% throughput (380.5 vs 389.8 exec/s over equal 180s budgets) because only the per-PC hit map is added to tracking that already runs. Crucible ignores `--lcov-out` for a live campaign and writes into the harness dir, which every component shares, so each file is moved out under its component's name before the next campaign can overwrite it — and moved on both arms of the run, since a campaign killed after its periodic flush would otherwise leave one behind to be published as the next component's coverage. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`crucible-idl-gen` wraps its account push in `if let Some(..)`, so a `None` optional is dropped from the instruction's account list. Anchor transmits an absent optional as the program's own id occupying a slot — its own derive emits `AccountMeta::new_readonly(crate::ID, false)` — so the program receives fewer accounts than it declares and rejects the instruction before running: 3005 `AccountNotEnoughKeys`, or 3007 `AccountOwnedByWrongProgram` when the optional is not last and the following account is read in its place. Nothing surfaces it. The action's transaction fails, the action returns `false`, the fuzzer treats that as a dead end, and the properties over that code hold vacuously. klend's 2026-08-10 fixture has 57 such sites. `refreshReserve` (4 of 6 accounts optional) is queued as a prefix by ten actions, so the entire core lending flow — deposit, borrow, repay, withdraw, liquidate — never executed once, and 26 of klend's 63 handlers sat at zero coverage. Writing the program id for just that helper's three `None`s took a 180s campaign from 6.1% to 7.4% of edges, 10.7% to 13.0% of branches, 44 to 46 of 92 actions ever succeeding, and 728 to 1775 violations found. Measured both ways — metas built by hand, and `Some(self.program_id)` through the generated struct — with the same result, so the one-token form is what the cheat sheet asks for. A gate rather than only a note in the prompt: that fixture's author already knew the convention, since one action hand-pushes the program id three times and works, and still wrote `None` in the shared helper beside it. The compile callout rejects it ahead of the build, because a build cannot see it — this compiles, links and dry-runs clean. Scoped to the IDL path. Crate mode uses anchor's derive, which is correct. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The Crucible e2e covered one Solana program, `solana_vault`, pinned to `anchor-lang = "1.0.1"` — the harness stack's own Anchor. So it takes the crate path, links Anchor's own `#[derive(Accounts)]` codegen, and cannot observe anything `crucible-idl-gen` gets wrong. Every real target is on a pre-1.0 Anchor and takes the other path. That gap is not hypothetical: `crucible-idl-gen` drops a `None` optional account from the account list where Anchor's derive transmits the program id, and no test in this repo could have failed. klend's 2026-08-10 run lost its entire core lending flow to it, with 375 green rows over code that never executed. `solana_vault_idl` is the same vault on `anchor-lang = "0.31.1"` — a different Cargo compatibility unit, so `crate_dep_usable` is false and the run generates its types from the IDL. `withdraw` gains an optional `fee_collector`, which is the one construct where the two paths disagree; the gate asserts the fixture actually builds it, and asserts each scenario took the path it exists for, so a version drift cannot quietly collapse the two cases into one. 0.31 rather than 0.29: it resolves to solana-program 2.x and builds with the installed platform-tools, where klend's 0.29/1.17 stack needs its own toolchain. `Cargo.lock` is committed for this scenario alone. `cargo-build-sbf` runs the platform-tools cargo (1.79), which parses neither an `edition2024` manifest nor a `rust-version` above its own, and a free resolution now picks several through `borsh-derive -> proc-macro-crate` and `solana-program -> blake3`. This is not new — `solana_vault` no longer builds from a clean lock either — but pinning the transitive set is what makes a scenario reproducible rather than dependent on the day's registry. Also fixes `build_program`: `anchor idl build -o target/idl/<p>.json` does not create its output directory and `cargo-build-sbf` only makes `target/deploy/`, so the IDL step failed on any clean checkout with a bare "No such file or directory", was swallowed by the best-effort branch, and resurfaced much later as "no IDL could be produced". Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Two failures the `solana_vault_idl` gate hit on its first two runs, both invisible to the crate path and so uncovered until there was a scenario on the other one. `warm_dirs` named only the harness crate. Warming feeds the private CARGO_HOME that the later confined, OFFLINE build reads, so whatever it misses is a build failure rather than a download. The crate path gets the program's graph by accident — its harness manifest path-depends on the program, so fetching the harness resolves the program too. The IDL path deliberately has no such dependency, so nothing warmed the program and `cargo-build-sbf` died on `no matching package named borsh-derive-internal`. The sandbox then could not exec `anchor`, which only the IDL path runs (`anchor idl build`). Granting `~/.cargo/bin` is not enough: an avm-managed install puts a symlink there into `~/.avm`, where the versioned binary it execs also lives. The bare `Permission denied` was swallowed by the best-effort IDL branch and resurfaced as "the program's anchor CLI version isn't installed", which sent the reader after a version that was in fact installed. Verified by the gate: the IDL-path vertical now passes end to end — 3 components, 19 properties, per-component LCOV, and campaign notes carrying `11/11 of the harness's actions`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`03a2562` said deleting `solana_vault_idl`'s `Cargo.lock` stops the scenario building. That overstated it, and the evidence is the crate-path gate passing on the same day with no lock at all. The failure behind the claim was a *direct* `cargo-build-sbf` on a fresh copy, which is not how the pipeline builds: `build_program` warms through `warm_cargo_cache` first, which pins the registry index protocol on both sides and uses the toolchain the sbf build will use. Skip that and the offline build reports `no matching package named anchor-lang` — a reproduction artefact, not a scenario defect. So the lock buys reproducibility against registry drift and a working by-hand build, not the gate. `solana_vault` needs no equivalent fix; it was never broken. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Port to the seam's new shape (docs/rust-applications.md §6): the check names are the author's, so `checks()` is gone and the wheel answers only where a declared check runs. * `target_for` returns the component's harness fn for every check of a component — one campaign for the whole property set, as before — and None for the preflight and the shared fixture, neither of which formalizes anything. * Attribution places a finding by the properties the author claimed for a check rather than by a single wheel-assigned one. The fixture still tags each assertion with a property *title*, so that is still what a finding names; a check claiming several properties is refuted by a finding naming any of them. * The component prompt asks for the mapping: one check per property named `c_<property title>`, with the tag prefix as what places a counterexample. One gap is left open and marked where it lives. The verdict contract says GOOD claims a check was exercised, and a campaign reports crashes rather than which tagged assertions it evaluated — so a property whose assertion was never written, or written where the fuzzer cannot reach it, still passes a clean run. Closing it needs `fuzz_assert!` to record each evaluation in the crucible repo; until then `validate` carries a KNOWN GAP note at the one place that claims more than the run established. Also shares the row-naming rule between the console rollup and the findings section as `RustFormalResult.display_name`, now that a check may carry several properties and have no single title to be named after. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The 2026-08-11 IDL-path vault gate passed but reported badly: both component authors mapped every property of their component onto a single check (`invariants`, `c_deposits_withdrawals`), so the two properties a campaign actually refuted took the other eight down with them. The wording invited it — "declare which harness function verifies which property" has one honest answer when a component has exactly one harness function. The unit the author declares has to be the thing evidence attaches to, and here that is a tagged assertion, not the fn that holds them. * The component prompt now says an invariant IS one tagged assertion, asks for exactly one per property named `c_<property title>` after its tag, and says outright why mapping several properties onto one is refused. * `validate` refuses such a declaration up front (`triage::undeclarable`), ahead of the build: a counterexample is placed by its tag, so those verdicts are unattributable however long the campaign runs, and spending the fuzz budget to produce them is waste. The complaint names the offending check, its properties, and what to declare instead. The seam itself still permits many-to-one, which stays right: a CVL rule can genuinely discharge three invariants because the Prover reports per rule. What a backend's check granularity must match is its own unit of evidence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The 2026-08-12 vault run reported 15 checks as 14 rule rows. The report identifies a rule by (file, name) — deliberately, so one definition seen through several runs collapses into a single row — and takes the file from the verdict when it names one, else from the component's artifact. Crucible named none, and its deliverable is ONE crate, so every component's checks arrived under that single file name. Both components of that run had a property titled `vault_authority_immutable`, both authors named its check `c_vault_authority_immutable`, and the two collapsed into one row: two separate campaigns, two separate verdicts, one reported. Both were GOOD there, so the output was only coincidentally right — a BAD in the second would have rendered as the first's GOOD. The hazard is not new (the key has always been (file, name) and Crucible has always had one artifact) but it is far more reachable now that check names come from authors, who — given the same property title — write the same name. So a verdict now says which section it came from: `<feature>.rs`, the file that component's tests were written into, one per component. That is what `Verdict.unit_file` was always for, and it also points the report at the file that actually holds the assertion instead of the crate root. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The verdict contract says GOOD claims a check was exercised; a Crucible campaign reports crashes, so a clean run cannot tell "held" from "never evaluated" and marks both GOOD. app.rs carries a KNOWN GAP note at the site, and author-determined-checks.md listed it as a follow-up, but neither says what the failure looks like or what would close it. This writes it down: the inference a clean run actually licenses, a guarded assertion whose guard never opens, why the two cases are byte-identical from outside, and that triage.rs already refuses the same inference one case over (UntilFirstFinding -> UNKNOWN, "a claim about a space nothing searched"). It also records what was rejected and why — an author-written counter beside the assertion (the model instruments the check the instrumentation polices), folding the guard into the condition with unwrap_or(true) (which asserts the vacuous case, turning a detectable failure into an undetectable one), and a judge-enforced ban on conditional assertions (a syntactic rule belongs in check_syntax, and neither can enforce it soundly — some guards are correct, and the goal is to measure how often they opened, not to outlaw them). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…s written One unchecked `Pubkey::find_program_address` in klend's shared fixture ended three components' campaigns and produced 84 ERROR verdicts carrying no reason. The call panics when no bump yields a valid address, which arbitrary seeds reach; the panic lands outside the fuzz target, so LibAFL records no crash, the process aborts (134), and `crucible run` reports only its own exit 1. Every property in the campaign comes back ERROR rather than a verdict — the one whose test panicked and the twenty-six that never ran. **The blast radius is what makes it a run-level defect rather than a test-level one.** The input that reached the panic is written to `./corpus`, which every component shares through `--corpus-in`/`--corpus-out`. Each later campaign loads all of it, so a component with no such call of its own dies identically — Oracle-Driven Refresh has none and failed exactly like the two that do. It spreads: one component, then three, then the run. That is also why it looked like flakiness for an hour, healthy components going bad as the corpus grew. So the rule goes to the author who can prevent it, with the mechanism attached. The cheat sheet already tells the fixture author that `false` means "could not be attempted", which is precisely what an underivable PDA is, so the guidance is `try_find_program_address` and `return false` on `None` — no new concept. It names why the panic is invisible and why it outlives the campaign, because a bare "use the checked form" reads as style advice and loses to the shorter call in the examples. `setup()` stays exempt and says so; panicking before any campaign starts is the harness failing, which is already the documented contract there. The judge gets the same defect from the other side, under C7. It reviews suites, not the fixture — `judge` returns `None` for setup, so the fixture is the one artifact with no review turn — and this would not have caught today's failure. It catches the next one: a section may derive its own PDAs (two of klend's did, six calls between them), and there it is this author's to fix. When the call is in the fixture instead, C8 already owns "a gap this author cannot fix": report it, do not reject the suite. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`judge` returns None for setup, reasoned at the call site as "scaffolding, not test evidence — the compile/dry-run gate already vets it, and there is no property to judge it against". Both halves are true and the conclusion still leaves the fixture the only authored artifact with no reviewer — the one built into every campaign rather than one. klend supplied the worked example: an unchecked `find_program_address` compiled, passed the dry-run's single iteration, and then panicked outside the fuzz target once 704 corpus inputs reached it, turning three components' campaigns into ERROR verdicts with no recorded crash. The gate proves the crate builds and runs once; this defect class survives building by construction. Records the four options rather than picking one — a host-side lint over `action_*` bodies (cheapest, narrow), a setup judge turn with its own criteria (general, expensive, and the original objection still stands against reusing the suite criteria), catching the panic in the fuzzer (bounds the blast radius, belongs in crucible, and turns a harness defect into a reachability gap), or unsharing the corpus (removes the spread, not the failure). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… does `--corpus-out ./corpus --crashes-out ./output` resolve against the invoking cwd, so every campaign wrote thousands of files into two directories at the project root — outside `RUST_FORBIDDEN_READ`, and therefore inside the surface the source tools list. A klend run put 48,675 files (10.6 MB, 348 MB on disk) there in three hours and lost 7 of 15 components: a `grep_files` during authoring inhaled the corpus and the prompts came back 1.6M–4.7M tokens against a 1M maximum. The signature was the giveaway — work completed before failing went 33 min, 20 min, 66 s, 28 s, 33 s as the directory grew, so the last components died on their first exploration call. Both directories move under `.certora_internal/crucible/`, which is what that directory is for: `309ddda` moved the sandbox scratch there on the same argument, and these are the same kind of output — generated, unbounded, not a deliverable. `crash_meta_paths` moves with them, since it looks for a finding's metadata by path. **The exclusion names the directory, not its contents.** `RUST_FORBIDDEN_READ` listed `.certora_internal/sandbox` specifically, which is why a sibling that grew to 48k files was never covered — the rule enumerated the subdirectories somebody had already been bitten by. It now withholds `.certora_internal` whole, matching `fs_forbidden_read`, which has always done that for Solidity: the Rust regex was behind its own ecosystem, not missing a Crucible-specific case. Nothing Crucible-shaped goes in the general Rust rule. `.certora_internal` was spelled as a literal in three places, so it is now `INTERNAL_DIR` in gen_types beside `CERTORA_DIR`, with the sandbox, autoProve and foundry subdirectories derived from it. The pair are what a user ignores and what a user keeps. Tested from both sides, because the halves are in different languages and nothing in either type system connects them: the wheel asserts its two directories sit under the withheld root, and the host asserts the rule covers them — plus the sandbox scratch, the logs, and a subdirectory nobody has invented yet, which is the case enumerating subdirectories kept missing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The rebase onto eric/rust picks up 23fb3b6, which renamed the callout mode's wire field primary -> deliverable_path on both sides of the seam; Crucible's declaration still constructed the old name, which strict descriptor validation rejects at load. The SDK doc comment's Crucible example also catches up with the harness crate's move under certora/crucible/ (1d99aac updated the Python docstring only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The importer now reads manual_sections + embedded_groups (1cdc1b1); the committed crucible_kb.rag.json still carried the flat sections list, so the corpus could not be ingested. Derived mechanically from the flat manifest rather than regenerated from the crucible repo, since the docs themselves have not changed (still @ 35ec899). Manual sections are the old sections verbatim — same header-path units, so keyword hits and get_section addresses are unchanged. The embedded groups recover the chunking hints the flat shape erased: markdown table runs become atomic (27 blocks that sentence-splitting would have cut mid-row), prose splits into per-paragraph blocks at blank lines, and horizontal rules are dropped — decoration with nothing to embed. Code bodies are byte-identical on both products. Validated through the real pipeline: the model validates the manifest, and BlockBuilder cuts the 126 groups into 126 chunks (max 1902 chars, under the 2000 default), with all 102 code samples held as code refs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Rewrite crucible-unexercised-checks.md around the verified fix for the unexercised-checks gap: the fuzz_assert* macros are ordinary #[macro_export] macro_rules! that authored code reaches only through wheel-generated globs, so the generated crate root can bind the name to a counting wrapper (macro_rules! __tally_fuzz_assert plus `pub(crate) use __tally_fuzz_assert as fuzz_assert` — a bare textual shadow is E0659) and every section call site expands the wrapper. Per-tag evaluation tallies land on the same captured stdout campaign.rs already parses, so the verdict can gate GOOD on a check's tag having been evaluated at all — no crucible-repo change, no authoring-surface change, and every bypass route degrades to UNKNOWN rather than a false GOOD. The former fixes 1 and 2 move to "where the increment belongs eventually" (upstream); LCOV becomes the cross-check that separates "never written" from "never reached". Also update author-determined-checks.md's follow-up bullet, which claimed the shortest fix needs the crucible repo. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Post-rebase fixups for the eric/rust master catch-up (base 1cdc1b1 -> 7f09070): - DefaultEmbedder moved to composer.rag.models (#115); repoint the three crucible gate tests. - fetch_verdicts takes the Formalized directly and is never called for gave-up/curtailed components (#90); the events/declared-findings tests drop their ReportComponentInput wrappers. - _extract_all reads run.source.content for the design-doc injection (#124); the granularity test's _Run stub grows a no-doc source. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Two clarifications to the interposition proposal. The sketch's tally line now carries the site: field (file!/line! expand to the call site), which the parser paragraph's "max per site, then summed per tag" always assumed — without it, two same-tag sites' interleaved power-of-two prints are inseparable. Alongside it, why the counter is per-site at all (each expansion mints its own static; a shared per-tag counter would need a string-keyed runtime registry, since the tag sits inside a literal the macro cannot inspect), and a new paragraph owning the count-vs-boolean question: an evaluated-once flag would satisfy the verdict gate, and the count exists for the green row's evidence weight on campaign.rs's own argument — "evaluated 2× in 67,798 executions" is a nearly-closed guard, the per-assertion analog of discovered: 44/92 — at the cost of a fetch_add over a swap and ~13 log lines over one. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Close the unexercised-checks gap without touching the crucible repo. The fuzz_assert* macros are plain #[macro_export] macro_rules! that authored code only ever reaches through globs the wheel itself writes — the fixture's `use crucible_fuzzer::*;` at crate root and section_file.j2's `use super::*;` — so the generated crate root can bind those names to counting wrappers and every call site in every section expands them. templates/tally_macros.j2 renders a __fuzz_tally helper plus a wrapper per re-exported macro, interposed via `pub(crate) use __tallied_… as fuzz_assert…` (an explicit binding shadows the glob; a macro_rules! under the original name is E0659 beside it) and delegating path-qualified, so operands are still evaluated once and messages still format only on failure. Each site counts its own evaluations in a static and prints `[FUZZ_TALLY] site: … evaluated: … tag: …` at power-of-two counts — the tag sliced from the message literal inside the print branch, so no evaluation pays a format!. tally.rs reads those lines back (max per site, summed per tag) and gates the verdict: a GOOD keeps its outcome only when a tag it claims was evaluated, and gains "evaluated at least N times"; otherwise it is UNKNOWN saying the check was never exercised. Applied in validate over whatever it concluded, so it covers both the clean-exit path (where the KNOWN GAP marker stood) and attribute_findings' GOOD-by-silence. Confirmed on real campaigns: 54 tally lines captured from a 20s vault run with an unreachable guard printing none, and validate returning two GOOD rows with the tally beside one UNKNOWN. Also repair four stalenesses that made test_crucible_formalize_gate unrunnable, none of them caused by the above — expensive tests are deselected from the routine pass, so they had rotted: * PipelineRun's _semaphore became _agent_semaphore/_cpu_semaphore (both crucible gates). * The gate never placed the crate root. Since sections moved into their own files (§17), compile/validate emit only src/<feature>.rs, so the harness dir had no Cargo.toml and every round failed to build while the author revised a spec that was never the problem. It now drives crate_root as adapter.write_crate_root does. * It asserted #[invariant_test] in the authored spec, which the cheat sheet forbids and Section::file strips; assert the section fn and the root's generated entry instead. * The preflight test asserted "fuzz_assert" absent from the crate root, which now defines the wrappers; assert the preflight body is inert. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The 6.1 escape suite collects composer.sandbox in a guest that has only pytest and annotated-types. recipes.py imported INTERNAL_DIR from composer.spec.gen_types, which imports pydantic at module top, so collection died on ModuleNotFoundError before a single kernel assertion ran. The two roots — CERTORA_DIR (keep) and INTERNAL_DIR (ignore) — move to composer.layout, a stdlib-only leaf. gen_types re-exports them. A unit test walks composer/sandbox and fails if anything there imports composer.spec or pydantic, so the next import like this fails in the regular suite instead of only in the QEMU guest.

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 5 times, most recently from f47972f to e3a5925 Compare August 10, 2026 22:35

ericeil and others added 26 commits August 13, 2026 17:35

ericeil force-pushed the eric/crucible-app branch from a9c994d to f1a194a Compare August 14, 2026 16:00

ericeil and others added 3 commits August 14, 2026 09:11

Navigation Menu

Uh oh!

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

PR 3/3: Crucible backend (capstone)#98
ericeil wants to merge 49 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