PR 2/3: Rust application framework (PyO3) - #97
Draft
ericeil wants to merge 5 commits into
Draft
Conversation
ericeil
force-pushed
the
eric/rust
branch
3 times, most recently
from
July 23, 2026 19:58
4bbeb08 to
7ea1a77
Compare
ericeil
force-pushed
the
eric/ecosystem
branch
2 times, most recently
from
July 23, 2026 20:15
833557a to
fe84bae
Compare
ericeil
force-pushed
the
eric/rust
branch
6 times, most recently
from
July 24, 2026 00:08
0671f74 to
5361ead
Compare
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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
PR 2 of 3 — Rust application framework (PyO3)
Part of the stacked split of
eric/crucible.Stack:
master→eric/ecosystem→eric/rust→eric/crucible-app.Base:
eric/ecosystem(PR #96) — review that first.What this adds
The generic Rust-wheel host + the Rust workspace, built on the command-sandbox seam that already
landed upstream (#73), consumed here via the
nonepassthrough provider (no confinement yet):composer/rustapp/*— the PyO3 wheel host (author→compile→judge→validate loop, descriptor, IoC)rust/workspace:autoprover-sdk(the ABI +export_app!macro) andexample-app/echoprovercomposer/spec/solana/build.py— Rust/Anchor workspace prep for the Solana front halfpyproject.toml/uv.lockappsgroup + wheel path depsrust-applications.md,rust-backend-api.md,rust-formalization-backends.md,rust-ioc-loop.md,rust-pure-app.md,formalization-abstraction.mdSandboxConfig.backend_specin its master shape ({argv_prefix, timeout_s}, async,config.BackendSpec); the SDK just prependsargv_prefix(seedocs/rust-backend-api.md).(The shared Rust prompt fragment
templates/rust/_failure_modes.j2lives in PR #96 alongside theSolana front half that consumes it — it is not added here.)
Cross-cutting intermediate forms (finalized in PR 3)
rust/Cargo.toml: workspace members omitcrucible-app(added in PR 3).rustapp/adapter.py:RustFormalizercasts the backend tag directly(
cast(ReportBackend, tag)); the validatingas_report_backend+ closed literal land in PR 3,once
report/schema.pyincludes"crucible".rust/.gitignorestarts ignoringrust/Cargo.lock, and the lockfile is untracked here.Verification
cargo build(autoprover-sdk, example-app, run-confined) ✓composer.rustappimports with nocrucibleleak ✓test_rustapp— 15 passed (echoprover decider round-trip; sandbox passthrough)Notes
test_solana_gatemodule lives in this PR (it importscomposer.rustapp.frontend), but thetest_scenarios/solana_vaultsample it drives lands in PR 3 — so the gate is only runnable fromthe tip of the stack. Its real-LLM run was not executed (draft).
🤖 Generated with Claude Code