PR 2/3: Rust application framework (PyO3)

[ericeil]

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 — PR #96 landed, so this branch was rebased onto master directly and the last
commit reconciles it with the three APIs master moved underneath it in the meantime.

79 files, +11.8k/-149. The premise: an AutoProver application should be able to ship as a Rust
wheel and nothing else — no composer-resident Python package. This PR is the host that makes that
true, plus the framework-layer seams it needs. It carries no verification backend; the first one 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()).

• descriptor.py — the declarative ABI as pydantic models: phases + CoreSlot mapping, CLI args,
  event kinds, artifact layout, preflight / setup step specs, deliverable mode, RAG corpus tag,
  serialize_toolchain, confine_by_default, nouns. Validated at load, so a malformed wheel fails
  before the run spends anything.
• wire.py — the runtime ABI, typed to match: tagged inbound unions (CompileOk | CompileFailed,
  ValidateBuildFailed | ValidateVerdicts), outbound AuthorInput / FinalizeInput / Failure,
  and a RustAppModule Protocol whose ten callouts are checked at import — a field renamed in the
  SDK now fails at the boundary instead of reading as "" three frames later.
• adapter.py / host.py / entry.py / cli.py / frontend.py / store.py / results.py —
  the author→compile→judge→validate loop, the bounded in-loop review, the cached shared setup
  artifact, console + TUI frontends, and two-line console/TUI entry-point shims.
• toolchain.py — the two seams for the analyzed project's build system (below).

The Rust workspace — rust/

• autoprover-sdk — the ABI (serde types), the Application / FormalizeSession traits, the FFI
  helpers, and the export_app! macro that emits the PyO3 module. Verdict.outcome is a real
  Outcome enum (UPPERCASE serde rename, so the wire bytes are unchanged).
• example-app (echoprover) — a self-contained demo wheel, so the framework has something to
  round-trip against; it ships with zero bespoke Python (console_main("echoprover")).
• run-confined gains a maturin bin pyproject so uv sync puts the launcher in .venv/bin
  (the crate itself is upstream, from Command sandbox: confine untrusted native command execution (Landlock + seccomp) #73).

Driver changes — composer/pipeline/{core,ptypes}.py

• PipelineBackend.preflight — whatever a backend can do before it knows anything about the
  program, run concurrently with system analysis. It is the cheap side of the pair, so it is
  awaited first and its failure cancels the analysis agent racing it; the result type Pre is
  opaque to the driver and threaded into prepare_system. 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.
• StagedFormalizer replaces the Formalizer.begin no-op hook: prepare_formalization widens
  to a union, and the shared artifact becomes a constructor argument to the only object that uses
  it. No post-hoc writes to a live formalizer — same rule as the rest of the phase chain.
• PipelineBackend is a nominal ABC, not a structural Protocol, so each backend names its eight
  type arguments in its class line and conformance is checked where the backend is defined.
  (Both prior docstring copies of those arguments had already drifted.)
• The second overlap (prepare_formalization ∥ extraction) simply awaits each in turn — the
  all-or-none cancellation preflight needs is not something it wanted.

Descriptor-driven RAG — composer/rag/import_format.py, composer/scripts/rag_import.py, composer/tools/rag_env.py
A corpus becomes data, not another bespoke Python builder: a producer emits a common JSON
manifest, one shared importer ingests any manifest (chunking, embedding, batching, dual-path DB
ingestion), and a wheel names its corpus by tag in the descriptor. Registration is a declarative
tag → (factory, connection) pair validated at descriptor load. The mechanism ships corpus-free —
KNOWLEDGE_BASES and rag_env._FACTORIES are both empty, and both halves of the first corpus land
with the application that declares it.

Build integration

• dev includes the apps group, so a bare uv sync builds the Rust artifacts — no manual
  maturin develop / cargo build. [tool.uv] cache-keys over each project's .rs sources
  (cross-crate, so an SDK edit invalidates the wheels) makes the import hook optional.
• rust-toolchain.toml at the repo root (rustup resolves by CWD); rust/Cargo.lock is tracked,
  since this workspace ships artifacts.
• CI: pytest's job builds the crates, so test_rustapp stops silently skipping; pyright's job gets
  --no-dev so it doesn't compile Rust it cannot see into.

Report / IO / UI seams

• ReportBackend gains "none" — a pipeline that records properties without verifying them —
  with its own labels (UNKNOWN → "Unverified", not "Unknown"). The null Solana backend reports
  under it instead of borrowing a real verifier's wording. Outcome.parse handles labels arriving
  from outside the repo, and outcome_label / outcome_glyph are the single place per-outcome
  wording lives (the console rollup and the TUI had drifting copies).
• RuleVerdict.message + its rendering: a non-GOOD row can carry the backend's diagnostic
  (a counterexample, a failed assertion) into report.json and the HTML.
• io.context.push_custom_update — the out-of-graph analogue of get_stream_writer(), for a
  backend emitting domain events between graph calls.
• MultiJobApp.mark_pipeline_done() replaces seven external writes to app._pipeline_done.

Docs — application-abstraction.md, formalization-abstraction.md, rust-applications.md,
rust-formalization-backends.md, rust-backend-api.md, rust-ioc-loop.md, rust-pure-app.md,
rag-import-format.md, rust/README.md.

What PR 3 (eric/crucible-app) does with all of this

Crucible — the Solana fuzzing backend — is the first real consumer, and because of the seams above
it lands as a pure-Rust app: rust/crucible-app (the wheel + its Askama templates + a committed
crucible_kb.rag.json), two registry entries, and a composer/crucible_launch.py holding the same
two shims echoprover uses. Concretely, per facility:

This PR's facility	How PR 3 uses it
preflight	Prepares the harness crate, compiles the program to sBPF, and gates a wheel-authored skeleton fixture through the real toolchain — all while system analysis runs. A broken dependency graph or unbuildable program surfaces before the model is spent.
WORKSPACE_TOOLCHAINS	Registers the Solana implementation (composer/spec/solana/build.py): warm the cargo cache, cargo-build-sbf the program, fill in an IDL's program id, place the IDL. The host still writes the plan's files and reports the idl context key; it never learns what a build is.
SOURCE_CRATES	Registers composer/spec/cargo.py — resolve the analyzed program's crate from its source path. Crucible's harness needs it as a path dependency; when it isn't usable, the wheel switches to IDL-generated types.
StagedFormalizer + setup slot	The shared fuzz fixture every component's harness builds on, authored once and cached.
CoreSlot.DISCOVERY	Claims its design-doc discovery phase by slot instead of by a magic "discover_design_doc" key.
Typed wire.py ABI	Its compile / validate callouts return the tagged variants directly; Verdict::detailed() carries the counterexample.
RuleVerdict.message + rendering	What makes a counterexample triageable from the report alone.
ReportBackend closed set	Adds "crucible" + its render labels, and swaps adapter.py's cast(ReportBackend, tag) for the validating as_report_backend.
RAG manifest + importer	Ships crucible_kb.rag.json as data and adds composer/tools/crucible_rag.py plus the two registry entries (rag/db.KNOWLEDGE_BASES, rag_env._FACTORIES) in one go. No new importer.
event_kinds + push_custom_update	Its domain events (harness built, section sealed, counterexample found) reach the TUI/console from between graph calls.
serialize_toolchain / confine_by_default / DeliverableMode::Callout	Declared in the descriptor: one toolchain callout at a time, sandbox default → the run-confined launcher (fail-closed), and a crate-shaped deliverable the wheel assembles.
Sandbox argv_prefix seam	Consumed here via the none passthrough provider; PR 3 flips the default to real confinement and adds the Rust build grants (private RUSTUP_HOME, cargo-build-sbf tree, offline registry).
test_scenarios/solana_vault	The Anchor sample the front-half and e2e gates drive.

Deliberately deferred to PR 3

Earlier revisions of this branch carried these; they moved forward to the backend that actually
needs them, so the framework layer holds no Cargo shape, no chain-specific build, and no verifier's
vocabulary:

• composer/spec/solana/build.py and composer/spec/cargo.py (+ the RustLanguage facet reaching
  them) — replaced by the two registry seams in rustapp/toolchain.py, which are empty here and
  unregistered in deliberately different ways: source_crate degrades to an all-empty
  ProgramCrate (indistinguishable from "nothing to resolve"), workspace_toolchain raises (a
  plan that only places files never asks, so reaching it means the wheel asked for a build nothing
  can perform). composer/sandbox/recipes.py is byte-identical to master again.
• Crucible's report vocabulary and its member of the closed ReportBackend set — hence the
  cast(ReportBackend, tag) in adapter.py, which PR 3 replaces with the validating helper.
• The crucible_kb registration (both halves) and composer/tools/crucible_rag.py. It was
  previously half-registered, which passed validation and then degraded to "RAG unavailable" —
  reporting a repo gap as an environment condition. Both registries are empty now, so such a wheel
  fails at descriptor load instead.
• rust/Cargo.toml's workspace members omit crucible-app.

(The shared Rust prompt fragment templates/rust/_failure_modes.j2 shipped in #96, alongside the
Solana front half that consumes it.)

Review-driven work on this branch

Beyond the original squash, the bulk of the commits here are the review of this branch, applied:
eight correctness fixes (a rollup hiding four of five verdicts per component; asyncio.wait
leaving a cargo build detached on Ctrl-C; a stale rustup symlink; entry points naming a PR-3
module; report rows colliding on a shared property key), then the typing/abstraction pass —
optionality instead of sentinels at four seams, Accepted | Rejected | None instead of
(bool, str), the typed runtime ABI, real APIs where callers had been reaching through private
fields, and the duplicate parser / env builder / dead hook cleanup. Each commit message states the
behaviour change, if any, and the one policy decision flagged-but-not-taken (an unparseable judge
reply fails open).

Verification

• pytest -m "not expensive" — 583 passed, 11 deselected (with the demo wheel importable).
• pyright — 0 errors.
• cargo build --manifest-path rust/Cargo.toml — clean (autoprover-sdk, example-app, run-confined).
• New coverage: 90 tests across test_rustapp* / test_rust_frontend / test_rust_llm_agent,
  plus test_pipeline_overlap, test_rag_import, test_rag_env, test_solana_component_grouping.
• test_solana_gate is in this PR (it imports composer.rustapp.frontend) but its
  test_scenarios/solana_vault fixture lands in PR 3, so it asserts out at collection-time-adjacent
  _SCENARIO.is_dir(). It is expensive-marked (real LLM + containers), so the routine pass
  deselects it; it is only runnable from the tip of the stack, and its real-LLM run has not been
  executed.

🤖 Generated with Claude Code