PR 2/3: Rust application framework (PyO3) by ericeil · Pull Request #97 · Certora/AutoProver

ericeil · 2026-07-23T18:42:55Z

PR 2 of 3 — Rust application framework (PyO3)

Part of the stacked split of eric/crucible.
Stack: master → ~~eric/ecosystem~~ (#96, merged) → eric/rust → eric/crucible-app.
Base: master. 79 files, +10.7k/-278.

Everything here serves one goal: **let an AutoProver application be implemented in Rust, as requested by the Solana Foundation. This PR is the host that makes that possible. It carries no verification backend; the
first one (Crucible) is PR 3.

What this adds

The generic wheel host — composer/rustapp/
A wheel supplies a declarative AppDescriptor and answers pure callouts; the host owns all control
flow, all effects, and the entire vertical an application needs — argparse, service setup, pipeline
wiring, frontend, artifact store, main().
Why: a Rust application should only have to describe itself and answer questions. Everything a
wheel would otherwise reimplement in Python lives here once.

A typed ABI on both sides — descriptor.py (load time) and wire.py (runtime)
The descriptor is pydantic-validated at load; the runtime unions are tagged (CompileOk | CompileFailed, ValidateBuildFailed | ValidateVerdicts) and the ten callouts are a Protocol checked
at import.
Why: a field renamed on the Rust side fails at the boundary, instead of reading as "" three
frames later.

The Rust workspace — rust/
autoprover-sdk — the ABI serde types, the Application / FormalizeSession traits, and the
export_app! macro that emits the PyO3 module. example-app (echoprover) — a demo wheel with zero
bespoke Python. run-confined gains a maturin bin pyproject.
Why: the Rust half of the ABI needs a home, and the framework needs something real to round-trip
against in CI.

Backend preflight — composer/pipeline/core.py
New PipelineBackend.preflight: whatever a backend can do before it knows anything about the
program, run concurrently with system analysis, awaited first, its failure cancelling the analysis.
Why: a backend that must build something can gate a broken workspace before the model is spent,
instead of surfacing it as unfixable compiler errors in the first authored draft.

StagedFormalizer replaces the Formalizer.begin hook
prepare_formalization widens to a union, and the shared setup artifact becomes a constructor
argument to the only object that uses it.
Why: no post-hoc writes into a live formalizer — the same rule as the rest of the phase chain.

PipelineBackend becomes a nominal ABC, not a structural Protocol
Each backend names its eight type arguments in its class line.
Why: conformance is checked where the backend is defined; both docstring copies of those arguments
had already drifted.

Descriptor-driven RAG — rag/import_format.py, scripts/rag_import.py, tools/rag_env.py
A producer emits a common JSON manifest, one shared importer ingests any manifest, and a wheel names
its corpus by tag. Ships corpus-free — both registries are empty here.
Why: a knowledge base should be data, not another bespoke Python builder per application.

Report / IO / UI seams
ReportBackend gains "none" with its own labels, for a pipeline that records properties without
verifying them (so the null Solana backend stops borrowing a real verifier's wording);
RuleVerdict.message carries a backend's diagnostic into report.json and the HTML (so a
counterexample is triageable from the report alone); io.context.push_custom_update (so a backend
can emit domain events between graph calls); MultiJobApp.mark_pipeline_done() (replacing seven
external writes to a private field); one outcome_label / outcome_glyph table (the console
rollup and the TUI had drifting copies).

Build and CI
A bare uv sync now builds the Rust artifacts (dev includes the apps group, cache-keys over
each crate's .rs sources); rust-toolchain.toml at the repo root; rust/Cargo.lock tracked.
pytest's CI job installs the toolchain and builds the crates; pyright's job gets --no-dev.
Why: no manual maturin develop step for contributors, and test_rustapp stops silently skipping
in CI.

Docs — application-abstraction.md, formalization-abstraction.md, rust-applications.md,
rag-import-format.md, rust/README.md.

Deliberately deferred to PR 3

The framework layer holds no Cargo shape, no chain-specific build, and no verifier's vocabulary. So
Crucible's build path (spec/solana/build.py, spec/cargo.py), its report vocabulary, and its RAG
corpus registration all land with the backend that needs them — reached here through the two empty
registry seams in rustapp/toolchain.py, and rust/Cargo.toml omits crucible-app.

Verification

pytest -m "not expensive" — 583 passed, 11 deselected.
pyright — 0 errors.
cargo build --manifest-path rust/Cargo.toml — clean.
~90 new tests across test_rustapp*, test_rust_frontend, test_rust_llm_agent,
test_pipeline_overlap, test_rag_import, test_rag_env, test_solana_component_grouping.
test_solana_gate ships here but its test_scenarios/solana_vault fixture lands in PR 3, so it is
only runnable from the tip of the stack. It is expensive-marked (real LLM + containers) and its
real-LLM run has not been executed.

🤖 Generated with Claude Code

The generic Rust-wheel host (composer/rustapp) + the rust workspace (autoprover-sdk ABI/export_app! macro, example-app/echoprover), consuming the command-sandbox seam already upstream (via the `none` passthrough; SandboxConfig.backend_spec -> {argv_prefix, timeout_s}). Includes composer/spec/solana/build.py (workspace prep), the rust prompt templates, and the report-layer support the host needs (report/{schema,render,collect}.py: the ReportBackend set incl. "crucible", the per-backend outcome_label vocabulary, and Verdict.message diagnostics). Cross-cutting intermediate forms (finalized in PR3): - rust/Cargo.toml: workspace members omit crucible-app (added in PR3). - pyproject.toml / uv.lock: the `apps` group + [tool.uv.sources] omit crucible_app (its crate lives in rust/crucible-app, which lands in PR3), so `uv sync`/`uv run` resolve here; PR3 re-adds it. - rustapp/adapter.py: RustFormalizer casts the backend tag directly; PR3 restores the validating as_report_backend. - rust/.gitignore ignores rust/Cargo.lock; the lockfile is untracked here. Gate: test_rustapp (echoprover decider round-trip; sandbox passthrough) -- 15 passed. CI pyright (composer/ analyzer sanity_analyzer certora_autosetup) -- 0 errors. test_solana_gate lives here (imports composer.rustapp.frontend), not PR1. Stacked-PR 2 of 3 (off eric/ecosystem); see docs/pr-split-plan.md. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The identity types split upstream: SourceIdentifier is now the neutral type the ecosystem seam speaks, with SolidityIdentifier and RustIdentifier as its per-language subtypes. These two sites predate the split and still claimed Solidity. Both typecheck either way, because narrow->wide assignment is legal — a SolidityIdentifier IS a SourceIdentifier. So the checker cannot catch these; they have to be retargeted by hand. - rustapp/entry.py: the generic Rust host parses --main-contract into SourceFields.contract_name, so it builds the neutral SourceIdentifier. It is descriptor-driven and not Solana-specific, so it should not claim a language at all. - tests/test_solana_gate.py: this one does know its target is a Rust program, so it builds a RustIdentifier. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Editing Rust required remembering a manual step (`maturin develop` for the app wheel, `cargo build -p run-confined --release` for the launcher, plus a one-time `maturin_import_hook site install`). Make the venv the single source of truth instead: * `dev` includes the `apps` group, so a bare `uv sync` builds the Rust artifacts. The container's UV_NO_DEV=1 still selects none of them, so its cargo-less final stage is unaffected. * `[tool.uv] cache-keys` over each project's `.rs` sources (including cross-crate, so an autoprover-sdk edit invalidates echoprover) — uv rebuilds on the next `uv run`, and the import hook becomes optional. * run-confined ships as a maturin `bin` wheel, landing the binary in `.venv/bin`; `_resolve_binary` also probes the interpreter's scripts dir, since PATH misses it when the venv is not activated. Linux-only, hence the `sys_platform` marker. * rust-toolchain.toml pins the toolchain and lets rustup install it on demand. It sits at the repo root because rustup resolves by CWD and ignores `--manifest-path`, and cargo runs both from crate dirs and from the root. * Track rust/Cargo.lock: this workspace ships artifacts, so the dependency versions are part of the build. pyright's job gets `--no-dev` — it would otherwise compile Rust it cannot see into. pytest's job now does build the crates, so tests/test_rustapp.py stops silently skipping in CI. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The Crucible work (PR3, `eric/crucible-app`) kept improving the layer beneath it, so the two branches had drifted: the framework files on `eric/rust` were stale copies of the same files on `eric/crucible-app`. This lifts the framework-layer half of that drift down to where it belongs, leaving `eric/crucible-app` to carry only crucible-specific files. What comes down, by area: * **Pipeline driver** — `PipelineBackend.preflight`, run concurrently with system analysis and joined by `_all_or_none` so either side failing cancels the other. This is what lets a backend that must *build* something gate the workspace before the model is spent, instead of surfacing a broken workspace as unfixable compiler errors in the first authored draft. `prepare_system` takes the preflight result as its third argument; a setup failure now surfaces where it happens rather than after extraction. * **Rust application framework** (`composer/rustapp`, `rust/autoprover-sdk`) — the abstract component unit mirroring EVM's, the declarative `preflight` / `idl_dest` / setup-artifact slots on the descriptor, the cached shared setup artifact, the bounded in-loop review, and IDL-driven type generation for a wheel that cannot link the program under test. * **Cargo/Solana capabilities** — `composer/spec/cargo.py` (resolve a program crate from its source path, not its name) and `composer/spec/solana/build.py` (fill in an IDL's program id when the project's build omits it; warm the cargo cache with the same cargo the sbf build uses). * **Sandbox recipes** — a private per-run `RUSTUP_HOME`, the `PATH` `cargo-build-sbf` install tree, `~/.gitconfig`, a pinned registry protocol, and `CARGO_NET_OFFLINE=true` (the spelling every cargo accepts). * **RAG seam** — `composer/tools/rag_env.py`, which `rustapp/entry.py` already imports. The corpus modules stay in PR3; an absent one degrades to no RAG, which is this module's documented contract. * Docs for the above, plus the report template rendering `Verdict.message`. Also fixes the demo wheel: `rust/example-app`'s descriptor gains `preflight: None`. It has not compiled since `preflight` was added to `AppDescriptor` on the crucible branch — that branch's `uv sync` never built the crates, so nothing noticed. Here it would break the `test_rustapp` gate the moment the wheel is rebuilt, so it is fixed in the same commit that brings the SDK change down. Verified: `cargo check --workspace` and `uv sync` clean, pyright 0 errors, and the framework/pipeline/sandbox/solana tests plus the `test_rustapp` gate pass — 422 passed vs 363 on the branch before, with no new failures. `test_solana_gate` fails here for a pre-existing reason: its `test_scenarios/solana_vault` fixture lives in PR3.

Ported from eric/ecosystem, plus the Rust-side half that branch has no backend for. `Formalizer.begin` was a defaulted no-op hook that every formalizer inherited and that the driver called unconditionally. It carried its ordering as a call-order convention and mutated the formalizer in place, contradicting `Formalizer`'s own contract ("immutable, fully constructed by prepare_formalization ... never set post-hoc") — the one thing the rest of the phase chain is built to avoid. Replace it with `StagedFormalizer`, whose abstract `begin` *returns* the `Formalizer`. `prepare_formalization` widens to the union of the two, and the driver picks the arm. On the Rust side that removes the last post-hoc write to a live formalizer: `RustFormalizer` no longer takes a `setup_author` and no longer assigns `_setup_result` / `_context_extra[context_key]` after construction. A wheel that declares a `setup` step now gets `RustStagedFormalizer`, which authors the shared artifact and calls the `build` closure `prepare_formalization` handed it; a wheel that declares none gets its formalizer straight from `build(None)`. Either way the artifact is in the context blob before any component can read it. Backends with no shared artifact (prover, foundry, null-Solana) are unchanged: their narrower `-> Formalizer[...]` return now states that positively instead of inheriting a no-op. Also brings over the CLAUDE.md testing notes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Eight fixes from the review of this branch, plus tests for the two that were behavioural. Nothing here changes the design — see REVIEW-eric-rust.md for the typing/abstraction work that is still open. * results: the console/TUI rollup read `next(iter(verdicts.values()))` on the strength of "one verdict per delivered unit", but `units()` is one unit per *property* — so a component with five properties reported one check and hid the other four. One row per verdict now, named by the property title it checks (new `RustFormalResult.unit_titles()`), falling back to the unit name. A delivered component that bakes no verdict still gets an UNKNOWN row. `report.json` was never affected; it goes through `fetch_verdicts`. * pipeline: `_all_or_none` left its tasks running when the *caller* was cancelled — `asyncio.wait` does not touch what it waits on, so a Ctrl-C left a multi-minute cargo build detached, still writing into the workdir. It now cancels them and re-raises. A task cancelled by a third party counts as a failure (and `exception()` is no longer asked of a cancelled task, which raises). * sandbox: the per-run RUSTUP_HOME's `toolchains` symlink was tested with `exists()`, which follows the link — a stale link (shared rustup home moved) read as absent and `symlink_to` would then raise FileExistsError. Check the link itself and re-point it. * pyproject: drop `console-crucible` / `tui-crucible`. They named `composer.crucible_launch`, which lands in PR3 — an entry point pointing at a missing module installs happily and fails at ImportError on first use. Same for null_backend's `:mod:`composer.crucible`` reference. * rag_env: the tag -> connection map existed twice (here and `rag/db.KNOWLEDGE_BASES`); take it from `KNOWLEDGE_BASES` and keep only the tools factory local. Split the two failure modes that were both being swallowed: an unregistered tag is a wheel bug, so `validate_rag_db` runs at descriptor load like `resolve_ecosystem` does, while an unavailable DB / embedding model still degrades to no RAG. * descriptor: `backend_tag: ReportBackend`. It feeds a closed set, so a wheel declaring a tag the report cannot render now fails in `model_validate_json` — before the run spends anything — rather than at formalizer construction. This caught the demo wheel declaring `backend_tag: "echoprover"`, which no report knows: any real echoprover run died in `RustFormalizer.__init__`. It borrows `"prover"` now, as the null Solana backend does. * adapter: `formalize` grouped its report rows as `(property, [one unit])` singletons, so two units checking one property became two rows with the same key and the store's `dict()` kept the last. Group by property as they arrive. * mark the `docs/crucible-*.md` citations that land in PR3, so a reader stops looking for files this branch doesn't carry. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The wheel's *declarative* ABI was already mirrored as pydantic models (`descriptor.py`); its *runtime* ABI was not. Python received every payload as a bare dict and destructured it by string key — `result.get("status") != "ok"`, `res.get("kind") == "build_failed"` then `res["verdicts"]`, `u.get("target") or u["unit"]`, `plan.get("files")` — while the Rust side had spelled the same things as tagged unions all along. A field renamed in autoprover-sdk read as `""` three call frames later instead of failing at the boundary. New `composer/rustapp/wire.py`, peer of `descriptor.py`: * Inbound, tagged: `CompileOk | CompileFailed` (discriminator `status`) and `ValidateBuildFailed | ValidateVerdicts` (discriminator `kind`), so `isinstance` replaces the string compare and neither variant can be asked for the other's fields. Plus `Unit` (whose `target_or_unit()` is no longer reimplemented inline), `Verdict`, `WorkspacePrep`, `SandboxGrants`, `Prompt`. * Outbound: `AuthorInput` (+ `Property`, `ProgramCrate`), `Failure`/`FailureKind` (so `{"kind": "judge"}` is a value, not a literal), and `FinalizeInput` — currently the only written definition of that payload, since the Rust `finalize` still takes an opaque `serde_json::Value`. Growing an `Outcomes` struct over there is the follow-up. * `RustAppModule` Protocol replaces `module: Any` in every signature. Members are `Callable` fields so `CALLOUTS` derives from the annotations rather than a hand-kept copy; `load_module` checks all ten at import and names the gaps, so a wheel built against an older SDK fails at load instead of with an AttributeError mid-run. The one cast sits at `import_module`, which is where the dynamism actually is. `component` and `context` stay dicts on purpose: they are opaque JSON the host only forwards, so typing them would mean inventing a schema for values it never reads. Rust side: `Verdict.outcome` becomes an `Outcome` enum (UPPERCASE serde rename, so the wire bytes don't change), with `Verdict::detailed()` for the failing case a backend almost always wants. A typo no longer compiles. Python still tolerates an unknown label (-> UNKNOWN, logged): version skew should cost one row's wording, not the component's results. Fallout worth noting: * `RustFormalResult.verdicts` is `dict[str, Verdict]`; `fetch_verdicts` and the console rollup read fields, and `results._parse_outcome` is gone. * `env: Any` -> `ServiceHost` in the authoring turn, which retired `getattr(env, "all_tools", None) or env.rag_tools`. * `_split_prompt` is gone. A wheel that sends no `instruction` now fails at the seam; it used to have its whole payload JSON-dumped into the agent's prompt. * `from_formalized` deleted — it parsed a Rust `Formalized`/`Command::Publish` that no longer exists in the SDK, and only tests called it. `as_report_backend` deleted too: pydantic validates `backend_tag` now. * The stub *wheels* in tests still return JSON strings, as real ones do. Only the host's side of the seam moved. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Two reach-throughs, one shape: a caller needed something an object owned, so it took it out of a private field instead of the object growing a way to ask. The phase enum. `RustBackend._phase: type` / `_core_phases` were dataclass *fields*, so `host.build_backend` constructed the backend with underscore-named keywords, and both callers that needed a phase member indexed the field through `cast(Any, …)` — `RustPreparedSystem` reaching across objects to do it (`cast(Any, b._phase)[setup.phase_key]`). They are now public `phase: type[enum.Enum]` / `core_phases: CorePhases` (the property is redundant — a plain attribute satisfies the protocol, as ProverBackend and the null Solana backend already show), and the indexing lives behind one accessor: def task_info(self, spec: StepSpec) -> TaskInfo[enum.Enum] Annotating the field `type[enum.Enum]` is what let the casts go: pyright resolves EnumMeta's `__getitem__`, so the member comes back typed. Both call sites were building a TaskInfo from a (phase_key, label) pair anyway, so that is what the method returns — and since PreflightSpec and SetupSpec now share a `StepSpec` base carrying `step: ClassVar[str]` (the step's kind), the task id is derived from the declaration rather than spelled `f"{name}-setup"` at the call site. ClassVar keeps `step` off the wire, so the Rust structs don't change. The TUI flag. `MultiJobApp.mark_pipeline_done()` replaces five external `app._pipeline_done = True` writes across four entry points plus two inside `ui/pipeline_app.py`; the flag is now touched only by the class that declares it. The method's docstring records why it exists at all — quitting is refused until the run ends, so a keypress can't close the app and take every panel with it mid-stream — which none of the assignments said. Both new tests assert the property the reach-through existed to provide: that a step's task carries the member of *the backend's own* enum, since the frontend looks up section labels by member identity and a member from another copy of the enum would land the task in no section at all. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`(bool, str)` carried three meanings. The string was a revise instruction when the bool was False and an aside when it was True, and `(True, "")` *also* stood for "this wheel declares no judge" — so every caller had to know which of the three it was holding, and `_budgeted`'s relent step returned `(True, rejection text)`, a verdict that read as an acceptance while carrying the opposite. Accepted(feedback="") # the gate opens; feedback is an aside Rejected(feedback=...) # the gate holds; feedback is what to revise None # no judge for this input — no verdict at all `_judge_turn` returns `Review | None`, so absence is absence: `author_and_compile` now re-authors on `isinstance(review, Rejected)`, and both "accepted" and "no judge" simply fall through. `_budgeted`'s last round produces a real `Accepted` whose feedback is the unresolved objection — the same behaviour as before, but the type now says what it does. `_make_judge_hook` narrows `None` away where it cannot happen (the hook exists only for an input that declared a judge) and says why. Two `_parse_judge` behaviours were previously implicit in the tuple: * A rejection with no feedback used to hand the next authoring turn an empty revise context — a round spent on "you were rejected" with no statement of what to fix. It now says that no reason was given. * Prose that leads with neither ACCEPT nor REJECT is taken as an acceptance. Unchanged, but now stated in the docstring and pinned by a test: the reviewer is advisory, in front of the compile/validate gates that actually decide, so an unparseable reply lets the draft through rather than burning a revise round on a verdict nobody stated. Flipping that is a policy decision — flagged, not taken. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Each of these had a value that looked like data but meant "there isn't one", so every consumer had to know the convention — and one of them silently didn't. * `cargo._dep_req` returned `""` for "no anchor-lang requirement to compare", which is what a caller comparing versions least wants to receive. It is `str | None` now, and `ProgramCrate.anchor` with it; the `""` the Rust struct's `#[serde(default)]` fields require is produced at the wire boundary (`wire_crate`) and nowhere else. * `run_llm_agent` JSON-dumped a missing result, so a turn where the agent never called the result tool handed back the literal string "null" — which went on to `compile` as if it were the authored artifact and spent an attempt on a build nobody could have fixed. It returns `str | None`; both loops treat "no artifact" as its own failure, costing an attempt but never reaching the toolchain, and the next prompt is told what actually happened. A judge turn that ends without a verdict is likewise not a rejection: it fails open, same reasoning as an unparseable reply. * `resolve_program_id` / `idl_with_program_id` took the crate as a dict and read it with `crate.get("dir", ".")` — a Python-to-Python call flattening a typed value and then papering over its absence by scanning the root as if it were the crate, matching against a set of empty names. They take `ProgramCrate | None`, and the fallback is stated once, where it happens. `run_workspace_prep` gets the resolved crate threaded in rather than reconstructing it from the wire copy, whose emptiness no longer says whether anything was resolved. * `RustFormalizer._idl` collapsed "prep placed no IDL" into `""` on the way in; it keeps `None` and flattens at `finalize`, which is the only place the payload promises a string. The fourth bullet of the review's §4 (`context_key if descriptor.setup else "setup"`, an unreachable fallback inventing a context key) went away with the typed-ABI commit, which made `build` take the key alongside the artifact. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Two places where a string was doing a type's job. The design-doc discovery task's phase was found by looking for a declared phase whose *key* was literally "discover_design_doc". The descriptor already has a mechanism for "this declared phase fills that role" — `core_slot` — so a magic key was a second, undocumented one: a convention a wheel author had to spell exactly right, with no error if they didn't, and `-> Any` at the end of it. `CoreSlot` gains `DISCOVERY`, and `CoreSlot.required()` names the four the driver itself tags and every application must map — so the new slot is optional, and unclaimed still falls back to the first declared phase. Mirrored in the Rust `CoreSlot` (additive: existing wheels don't mention it). The other: two glyph tables with identical contents, one keyed by `Outcome` (the console rollup) and one by raw strings (the TUI), because the emit payload carried `"GOOD"`/`"BAD"` as literals. They are now `render.outcome_glyph`, beside `outcome_label` — the same question, how an outcome reads to a human — and the tolerant `str -> Outcome | None` is `Outcome.parse`, used by the frontend and by `wire.Verdict`'s validator instead of each keeping its own known-values set. An outcome this host doesn't recognize loses its glyph, not its line. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Section 7 of the review: the duplication and dead code. - build_arg_parser is the only parser. rust_entry_point re-declared the same nine arguments inline, and the copy had already lost every help string. The declared-flag dests no longer ride out of _add_declared_args as a return value either: _arg_dest/_declared_args derive them, so "declared" and "collected" cannot drift apart. - build_default_env replaces build_neutral_env plus _default_env_builder's inner closure, which were the same six lines twice differing in rag_tools=. rust_entry_point binds rag_db=descriptor.rag_db_default with partial, which also keeps the corpus lookup lazy. Renamed because "neutral" described only one of the two behaviours; docs/rust-pure-app.md §5.1 records the landed name for the proposal it implements. - Deleted _before_formalize: a no-op hook with no overrider, on a branch whose thesis is that applications ship no Python. What it documented is now a comment where it matters, and the "hooks an application backend may override" banner over _context went with it. - _run_blocking has one body, guarding on nullcontext() when there is no semaphore. - Hoisted the function-local imports that had no reason to be local (io.context, diagnostics.timing, sandbox.recipes); the spec.solana.build one stays and now says why the generic host doesn't name a chain at import time. - RUST_FORBIDDEN_READ is one literal instead of being rebound four lines after it is defined. - RustLanguage.source_crate is a method: as a Callable field it advertised an injection point that source_crate_of's isinstance dispatch makes meaningless. - AppDescriptor.unit_noun(plural=) owns the component_noun fallback and the pluralization that cli.py spelled twice; cli.py's helpers take app: RustApplication. - store.py: dict comprehension -> dict(). Tests: new test_rustapp_toolchain_sem.py covers _run_blocking (serialize_toolchain had no coverage at all, so a rewrite of that guard could have gone unnoticed) — including that four concurrent callouts never overlap and a raising one releases the permit. test_rustapp.py pins the help text the duplicate parser had lost, the declared-arg threading, and unit_noun. pyright 0 errors; 463 passed, 11 deselected with the demo wheel importable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

crucible_kb was half registered: composer.rag.db.KNOWLEDGE_BASES carried its connection and rag_env._FACTORIES carried a factory, but the module that factory imports (composer.tools.crucible_rag) lands in PR3. The tag therefore passed validate_rag_db — both halves present — and then build_rag_tools caught the ModuleNotFoundError in its degrade-on-anything path and logged "RAG unavailable", reporting a repo gap as an environment condition. That is the confusion rag_env's two failure modes exist to keep apart, and it was reachable: a wheel declaring crucible_kb would have run with no RAG and a single warning line. Both registries are empty now, so such a wheel fails at descriptor load with "not a registered RAG corpus" instead, and PR3 adds the tools module, the _FACTORIES entry and the KNOWLEDGE_BASES entry in one go. CRUCIBLE_DEFAULT_CONNECTION goes with them (nothing else read it), as does the comment naming composer.scripts.rag_import, which does not exist on this branch either. The error message now says "none is registered yet" rather than "known: []". The pyproject.toml crucible comments stay: nothing there points at a missing module (the entry points that did were deleted earlier), so they only explain why those lists look short. Tests: new tests/test_rag_env.py — the registry had no coverage at all. Includes half-registrations (either half) still refusing, which is the shape that slipped through, and a stub registration that doubles as the spec for what PR3 adds. pyright 0 errors; 470 passed, 11 deselected. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`_all_or_none` gave both of the driver's overlaps one fate, which is more than either needs. The preflight is cheap by construction, so there is nothing to save by cancelling it: await it first, and let its failure cancel the analysis agent racing it — the direction where the spend actually is. An analysis failure now waits the preflight out and reports itself. The second pair (`prepare_formalization` ∥ extraction) goes back to awaiting each in turn, no cancellation either way. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`.sandbox_cargo` / `.sandbox_rustup` / `.sandbox_tmp` were spelled out in the recipes that create them, in the forbidden-read regex that has to hide them from the source tools' file listing, and in a test's assertions. Hoist them to SANDBOX_{CARGO,RUSTUP,TMP}_DIR next to the functions that create them, and build the regex branches from those via re.escape (the joined pattern is byte-identical to the old literal). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… stuck prover run) into eric/rust Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ting them) into eric/rust Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The driver keeps the branch's preflight ∥ analysis task group and adopts #157's SYSTEM_ANALYSIS_KEY family for the analysis context key; the prover backend keeps the branch's PropertyTitle typing alongside #157's CacheKey removal. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The last derived key minted with the pre-#157 convention (inline f-string over a private hash helper, types only on the variable annotation). RUST_SETUP_KEY now pins the run-root parent, the RustSetupSpec child, and the derivation in one declaration; _setup_identity stays as the digest of what the artifact is authored from (and the subject of test_rustapp_setup_cache's identity probes). The key string is unchanged, so existing cached setups still hit. Co-Authored-By: Claude Fable 5 <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>

ericeil · 2026-08-14T16:37:13Z

I've merged all of the changes from master up to yesterday, including the vfs change. I did not wire EvidenceFinder or RunBudget for Rust apps; if we want those, we should probably do them as separate PRs.

Catch-up before adopting tool families: isolate failing CEX analysis, hot fixes, and remapping contexts against the run root. The only conflict was composer/cvl/tools.py. Kept this branch's authoring-buffer extraction and restored master's parallel-edit guard in the shared edit_spec_tool so the incoming test_edit_cvl still holds — including for edit_spec.

Mechanism only: graphcore tool_family / TemplatedTool, tool_family_display, and the graphcore pin to 4c35857. No existing tools converted.

Replace _redescribe with graphcore tool_family / tool_family_display on the session tools that already used {check}/{checks} placeholders. CheckVocab.fill stays for runtime strings. MapChecks still splices a templated PropertyCheckMapping because family formatting is not transitive. PublishSpec has no placeholders, so it is a plain @tool_display class again.

Give-up, skip/unskip, and the buffer get/edit tools are tool_family classes. CVL and Foundry instantiate them with the exact wording those tools had on master; a schema-golden test pins name, description, and field text. Foundry and CVL drop their private skip copies. Descriptions are inspect.cleandoc'd at instantiate time so a {description} substitution matches a real class docstring (which Python already cleans). Buffer factories still inject the backend's state type and write-time validator — those are not nouns.

Master's CVL and Foundry unskip texts were the same sentence with different wrapping. Collapse them to a single @tool_display class. record_skip stays a family: CVL talks about the feedback judge, Foundry about the publish-time mapping, and Foundry's reason field adds "as a foundry test".

Move the record_skip description and reason strings out of the shared family and into cvl_generation, foundry/author, and rustapp/session. The family only supplies the implementation; the LLM-facing text lives next to the backend that instantiates it.

PR #156 landed on master after we already merged the tool-family branch here. This catch-up should be the merge commit only.

ericeil · 2026-08-14T23:56:26Z

Updated the shared tools to use @jtoman's new tool family support. Verified that the text of these tools has not changed (except for some line breaks) vs. current master, for the existing uses of the tools.

ericeil · 2026-08-14T23:57:25Z

Note to self: delete this test before merging to master; this is just here to validate that we don't deviate any tools vs. the ones in master, before merging.

jtoman

Honestly, just a handful of nits at this point. Thank you for your patience on this over multiple rounds of feedback. I'm holding off my approval because I don't want anyone to think this is ready; I'm going to let Dr. Nandi review the rust bits.

jtoman · 2026-08-15T05:24:46Z

-    extra_fields: dict = {}
-    if set_did_read:
-        extra_fields["tool_call_id"] = (Annotated[str, InjectedToolCallId], ...)
+    templated = GetSpec.with_template(description=inspect.cleandoc(description))


?????? Why tho? Whitespace is basically nonexistent to llms (I think) so this doesn't really matter?

This was done to help the test that checks if we've accidentally changed anything. Will remove this when I remove that test.

Pydantic can parameterize a BaseModel with a runtime type, so the create_model rewrite of `state` is unnecessary. WithGenericState copies __doc__ onto the specialized class so StructuredTool still gets the templated description.

_row_name picks a property title, a check name, or a component display name. A sibling phantom str keeps that display label out of those namespaces so it cannot be looked up as one of them.

Keep the property-to-check mapping comments on the same noun the tools already use, so a {check} is not described as a rule.

"That declaration is what gets run" reads as if map_checks itself were validation, or as if a declaration in the spec were the unit of work. Name the runner and the names it executes, and state that a check in the spec but not mapped is not run.

Doc-copying on generic subscription now lives on WithInjectedState, so GetSpec/EditSpec no longer need a local WithGenericState mixin.

jtoman

ship it! 🎉

chandrakananandi

Very sorry for the super slow review. I won't keep this PR hanging after this round.

chandrakananandi · 2026-08-10T20:30:42Z

@@ -0,0 +1,189 @@
+//! The Rust half of the wire round-trip fuzzer (`tests/test_wire_roundtrip.py`).
+//!
+//! Speaks newline-delimited JSON on stdin/stdout so the Python side drives one long-lived process


"Speaks newline-delimited JSON" is a weird phrase imo. One thing I find useful is to ask a subagent (or maybe Codex if the code was written using Claude) to make the code comments and documentation as simple as possible and reduce unnecessary verbosity. It might help clean up stuff like this for example. I think later on these things can make the comments a bit tiring to read.

I've been working on getting Claude to generate better comments from the start. This was generated early in that process. :) Will clean it up.

(Actually I'm realizing this was not so early - so maybe I have work to do on my claude.md :) Will still clean this up)

chandrakananandi · 2026-08-12T20:55:41Z

+/// is closed and shared with the host, so a typo fails to compile instead of reaching a prompt.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+#[cfg_attr(feature = "fuzz", derive(arbitrary::Arbitrary))]


this is needed by Crucible right? i suspect it uses the Arbitrary trait

It's used for a similar purpose: there's a fuzz test in this PR that tests the python/rust boundary itself.

chandrakananandi · 2026-08-17T22:09:33Z

+fn workspace(workdir: &str, sandbox_json: &str) -> Workspace {
+    Workspace {
+        dir: std::path::PathBuf::from(workdir),
+        sandbox: parse(sandbox_json, "Sandbox").unwrap_or_default(),


We could return the error here instead of unwrap_or_default:

match parse(sandbox_json, "Sandbox") { Ok(s) => s Err(e) => return json::to_string(CompileResult::Failed {errors: e}) }

similar to the way you are handling author_prompt below

The big problem is that we don't have a general way to pass an error over the "wire", hence all these defaults. Will see if I can clean that up.

chandrakananandi · 2026-08-17T22:21:17Z

+/// `workspace_prep(input_json) -> str` (JSON `WorkspacePrep`). Pure.
+pub fn workspace_prep(b: &dyn Backend, input_json: &str) -> String {
+    match parse_input(input_json) {
+        Ok(input) => serde_json::to_string(&b.workspace_prep(&input)).unwrap_or_else(|_| "{}".into()),


we don't want something like .unwrap_or_else(|e| e.to_string()),? or maybe format!(" error messahe {e}")

chandrakananandi · 2026-08-17T22:21:39Z

+pub fn workspace_prep(b: &dyn Backend, input_json: &str) -> String {
+    match parse_input(input_json) {
+        Ok(input) => serde_json::to_string(&b.workspace_prep(&input)).unwrap_or_else(|_| "{}".into()),
+        Err(_) => "{}".into(),


so is it ok here to return {}? I have same question for sandbox_grants actually... should we return the error instead? So Err (e) => e?

chandrakananandi · 2026-08-17T22:37:59Z

+            if declared.contains(&c.name.as_str()) {
+                Verdict::with_outcome(Outcome::Good)
+            } else {
+                Verdict::with_outcome(Outcome::Unknown)


should this be Unknown or Error?

chandrakananandi · 2026-08-17T22:42:36Z

+    workdir: &str,
+    sandbox_json: &str,
+) -> String {
+    let target: Target = parse(target_json, "Target").unwrap_or_default();


also here maybe worth thinking if unwrap_or_default() is the right thing

chandrakananandi · 2026-08-17T22:44:32Z

+pub struct Check {
+    pub name: String,
+    pub properties: Vec<String>,
+    #[serde(deserialize_with = "crate::required::present")]


why do we want this attribute? Might be fine, just curious

chandrakananandi · 2026-08-17T22:56:27Z

+}
+
+/// The body of [`Workspace::run`], over the parts rather than the bundle.
+fn run_confined<I, S>(


pretty big function...any chance we can break it into parts?

chandrakananandi · 2026-08-17T22:58:52Z

+            Some(st) => break Some(st),
+            None => {
+                if Instant::now() >= deadline {
+                    let _ = child.kill();


i am bad at reasoning about multi-threading, so I asked Claude and Codex both to look at this part of the code and both came up with a comment which i thought i should share:

Claude:

Timeout must kill the whole process tree. Put the child in its own process group and kill the group (needs a libc dep, unix-only): use std::os::unix::process::CommandExt; cmd.process_group(0); // before spawn // on timeout, instead of child.kill(): let _ = unsafe { libc::kill(-(child.id() as i32), libc::SIGKILL) }; let _ = child.wait(); This also unblocks the reader-thread join()s, since no orphan holds the pipe open anymore.

Codex:

Timeout handling kills only the direct child, then joins stdout/stderr reader threads. If the command spawned children that inherited stdout/stderr, those pipes can stay open and join() can block indefinitely after the timeout. Use a process group/job control strategy or ensure the whole tree is terminated before joining readers.

ericeil mentioned this pull request Jul 23, 2026

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

Draft

ericeil force-pushed the eric/ecosystem branch from bd40b22 to 4c76f66 Compare July 23, 2026 18:50

ericeil force-pushed the eric/rust branch 3 times, most recently from 4bbeb08 to 7ea1a77 Compare July 23, 2026 19:58

ericeil force-pushed the eric/ecosystem branch 2 times, most recently from 833557a to fe84bae Compare July 23, 2026 20:15

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

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

ericeil and others added 15 commits August 4, 2026 11:12

ericeil and others added 5 commits August 13, 2026 17:02

Merge master (PR #153: Fix the stuck-rule nag detector crashing every…

b833ea8

… stuck prover run) into eric/rust Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Merge master (PR #129: Compile-check generated harnesses before accep…

f67b234

…ting them) into eric/rust Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Merge master (PR #161: fix codegen) into eric/rust

ca87d9b

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

ericeil requested a review from jtoman August 14, 2026 00:32

jtoman and others added 11 commits August 14, 2026 13:32

bump pointer

01994cb

heck!

d668b80

okay I updated the lockfile, happy????

1f86009

Merge branch 'master' into jtoman/tool-families

e664766

Merge PR #156 (tool family templates) into eric/rust

3de46a9

Mechanism only: graphcore tool_family / TemplatedTool, tool_family_display, and the graphcore pin to 4c35857. No existing tools converted.

Merge master (PR #156) into eric/rust

9996fac

PR #156 landed on master after we already merged the tool-family branch here. This catch-up should be the merge commit only.

ericeil commented Aug 14, 2026

View reviewed changes

jtoman reviewed Aug 15, 2026

View reviewed changes

ericeil added 5 commits August 17, 2026 10:15

rustapp: type verdict row names as a phantom RowName

cac6c04

_row_name picks a property title, a check name, or a component display name. A sibling phantom str keeps that display label out of those namespaces so it cannot be looked up as one of them.

rustapp: say check, not rule, in session mapping docs

791a912

Keep the property-to-check mapping comments on the same noun the tools already use, so a {check} is not described as a rule.

authoring: use WithInjectedState for buffer tool generics

414e6f7

Doc-copying on generic subscription now lives on WithInjectedState, so GetSpec/EditSpec no longer need a local WithGenericState mixin.

ericeil requested a review from jtoman August 17, 2026 18:21

jtoman approved these changes Aug 17, 2026

View reviewed changes

Comment thread composer/rustapp/results.py

chandrakananandi requested changes Aug 17, 2026

View reviewed changes

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 2 of 3 — Rust application framework (PyO3)

What this adds

Deliberately deferred to PR 3

Verification

Uh oh!

ericeil commented Aug 14, 2026

Uh oh!

ericeil commented Aug 14, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jtoman left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jtoman left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

chandrakananandi left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

ericeil commented Jul 23, 2026 •

edited

Loading