Crucible prototype#64
Draft
ericeil wants to merge 144 commits into
Draft
Conversation
…-pipeline-refactor
…-pipeline-refactor
Implement the framework that lets AutoProver formalization backends and whole applications be written in Rust and driven by the generic Python pipeline, per docs/rust-formalization-backends.md and docs/rust-applications.md. Rust (rust/): - autoprover-sdk: the crate new apps import — the JSON ABI (descriptor, Command/Observation IoC protocol, results, verdicts), the Application / FormalizeSession traits, sync FFI helpers, and the export_app! macro that emits the PyO3 module. - example-app: the `echoprover` demo application, built into a wheel via maturin; exercises every Command variant. - Cargo workspace + maturin build infra (abi3-py312, extension-module). Python (composer/rustapp/): - The inversion-of-control effect loop: Python owns the async event loop and every effect (LLM, prover, cache, event streaming); Rust only decides the next one. No pyo3-async bridge. - Adapter implementing the real PipelineBackend / PreparedSystem / Formalizer protocols over a Rust wheel, plus RealEffects (LangGraph stream writer, model, injectable prover/feedback hooks). - Descriptor models, cacheable FormT (RustFormalResult), artifact store, phase-enum synthesis, run_rust_pipeline, build_application. Also widen ReportBackend to `| str` so a Rust app can stamp its own report tag. Tested end-to-end (tests/test_rustapp.py, 6 passing) driving the real echoprover wheel through the loop with a fake effect handler: publish, give-up, and cache-hit paths, plus descriptor/core-phase synthesis and result round-trip. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Complete the Rust application vertical: a Rust wheel now becomes a runnable application with no bespoke Python, everything synthesized from the descriptor. composer/rustapp/entry.py — descriptor-driven async entry point (rust_entry_point): argparse built from the descriptor's declared args + standard flags, precondition validation delegated to the Rust validate_preconditions hook, a neutral RAG-free env (build_neutral_env, overridable), and build_arg_parser for introspection. Service wiring (Postgres pools, thread logger, WorkflowContext) mirrors the foundry entry point. composer/rustapp/frontend.py — GenericRustApp (Textual MultiJobApp), GenericRustTaskHandler, and GenericRustConsoleHandler, all data-driven by the descriptor's event_kinds: a Rust Command::Emit becomes a custom-stream payload the handler renders if its type is declared. No per-app subclass needed. composer/rustapp/cli.py — tui_main(module) / console_main(module); an app's CLI is two lines. Imports composer.bind first (DI/tape bootstrap), like the built-in mains. host.py — run_application builds the backend from a pre-synthesized RustApplication so the frontend's phase_labels and the backend's core_phases share ONE enum object (the identity the frontend's label lookup relies on); prevents silent label misses. Tests (10 passing): descriptor-driven argparse (declared-flag defaults + override), the shared-enum identity invariant, console-handler event rendering (declared shown, undeclared ignored), and Textual app construction. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add docs/ecosystem-abstraction.md proposing a second pipeline axis — the ecosystem (blockchain/source domain) — orthogonal to the backend axis, so the shared front half (system model, analysis + property-extraction prompts, source conventions, connectivity validation) stops being silently hardwired to Solidity. Factors an ecosystem into a language facet (solidity, rust) and a chain facet (evm, solana, soroban), composed via Jinja prompt fragments. The rust language facet — Cargo fs conventions, the code_explorer prompt, and the rust failure-mode fragment (overflow, panics) — is authored once and shared by both Solana and Soroban; only each chain's model and platform failure modes differ. Notes that the sharing is not strictly hierarchical (Soroban's contract-owns-typed-storage model is closer to EVM's than to Solana's account model), motivating composable fragments over rigid inheritance. Includes the Solidity-coupling audit, the Language/Chain seam, ecosystem selection via an application parameter (built-in apps pass EVM; the rustapp AppDescriptor gains an ecosystem: ChainTag field), the behavior-preserving EVM extraction, the Solana and Soroban chain sketches, a phased plan, open questions, and key files. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Behavior-preserving refactor introducing the ecosystem seam and capturing today's
behavior as EVM = SOLIDITY ⊕ evm (see docs/ecosystem-abstraction.md §10 phase 1).
The shared front half (system analysis + property extraction) stops being silently
hardwired to Solidity; the driver defaults to EVM, so existing apps are unchanged.
New composer/pipeline/ecosystem.py:
- PromptPair, Language (source-level facet), Ecosystem (chain facet) dataclasses.
- main_instance moved here (it is EVM's locate_main); re-exported from
composer.pipeline.core so foundry/prover/rustapp importers are unaffected.
- SOLIDITY + EVM instances wiring the existing SourceApplication, prompt template
names, _validate_connectivity, and unit enumeration — a move, not a rewrite —
plus an ECOSYSTEMS registry ({"evm": EVM}).
Threaded through, all with behavior-preserving defaults:
- run_component_analysis: keyword-only system_template / initial_template / validate.
- run_property_inference: system_template / initial_template, threaded down through
_run_bug_analysis_inner -> _run_bug_round -> _get_initial_prompt.
- run_pipeline: takes ecosystem (default EVM) and drives analysis/extraction from it
(system_model, prompts, validate, analysis_extra_input, units). The one EVM
assumption kept for now — prepare_system(analyzed: SourceApplication) — is bridged
with a documented cast, removed by phase 2's App type parameter.
Verified: EVM reproduces the prior template names, validate identity, and the
verbatim analysis front-matter; no import cycle; 115 passed / 4 skipped (the 2
tree-parsing failures and rag_db errors are pre-existing env issues — missing
certoraRun CLI and DB containers — unrelated to this change). The doc's golden-run
gate needs Docker/Postgres/LLM and should be run in CI before merge.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… param Static-typing generalization (no runtime behavior change): make the analyzed application model a first-class type parameter so the backend and the ecosystem that produces its model are paired by type, and the Phase 1 cast disappears. - Ecosystem is now generic over App (composer/pipeline/ecosystem.py): system_model: type[App], locate_main: Callable[[App, ...]]; EVM: Ecosystem[SourceApplication]; registry typed dict[ChainTag, Ecosystem[Any]]. validate_analysis stays typed over BaseApplication (it narrows the produced model internally, and this keeps it assignable to run_component_analysis's validate parameter). - PipelineBackend gains the App type parameter; prepare_system(analyzed: App). - run_pipeline is [P, FormT, H, A, App] with ecosystem: Ecosystem[App] as an explicit argument; `analyzed` flows as App straight into prepare_system — the Phase 1 cast(SourceApplication, analyzed) and the unused `cast` import are removed. - The four callers (prover, foundry, both rustapp entries) pass ecosystem=EVM. - Also fix a pre-existing pyright nit in build_phase_enum (functional enum.Enum → type[Enum]). SystemAnalysisSpec is intentionally NOT parameterized — it carries only analysis_key + extra_input, no App-typed member (the analyzed type lives on the ecosystem). Verified: pyright reports 0 errors on the touched files (the pairing type-checks with no cast; one pre-existing _batch_cache_key TypeVar warning remains). Compiles, imports cleanly, unit tests green. No end-to-end gate needed — PEP 695 generics / Protocol are erased at runtime and removing a cast is a no-op, so the Phase 1 gate result stands. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…criptor
Wire ecosystem selection into the Rust application framework, so a Rust wheel
declares which ecosystem (chain) its backend targets and the host routes the
shared front half accordingly — replacing the hardcoded EVM in rustapp.
- Rust SDK (rust/autoprover-sdk): AppDescriptor gains `ecosystem: String`
(serde default "evm", so descriptors built before the field still deserialize);
echoprover sets ecosystem="evm".
- Python mirror (composer/rustapp/descriptor.py): AppDescriptor.ecosystem:
ChainTag = "evm" (ChainTag defined locally to keep the ABI-mirror decoupled
from the pipeline).
- Host (composer/rustapp/host.py): new resolve_ecosystem(descriptor) does the
ECOSYSTEMS registry lookup with a clear error for an unregistered chain;
threaded through build_application (stored on RustApplication.ecosystem),
run_application, and run_rust_pipeline. Exported from the package.
- Tests: descriptor carries + resolves ecosystem to EVM; build_application carries
the resolved ecosystem; an unregistered chain ("solana") raises; an absent field
defaults to "evm".
Only `evm` resolves today (Solana/Soroban register in phases 4-5), so behavior is
unchanged; the plumbing is now in place. Also marks phases 1-3 done in
docs/ecosystem-abstraction.md and records the solc-provisioning finding from the
phase-1 gate run.
Verified: cargo build clean, pyright 0 errors on touched Python, 14 rustapp tests pass.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…del/ecosystem
Foundation for the Solana chain: generalize the shared driver over ecosystem-provided
Unit/Main types, add the standalone Solana system model, and register the RUST language
facet + SOLANA chain. EVM behavior is preserved (still bound to
ContractComponentInstance/ContractInstance). Solana prompts, a sample Anchor scenario,
and the live-LLM gate follow in the next commit.
Driver generalization (composer/pipeline/core.py, system_model.py, prop_inference.py):
- FeatureUnit protocol (in system_model) captures the per-unit interface the driver needs
(display_name / slug / unit_index / cache_material / context_tag). ContractComponentInstance
implements it with byte-identical cache keys/tags, so EVM behavior is unchanged.
- Thread Unit/Main type params through Ecosystem, PreparedSystem, PipelineBackend, Formalizer,
BackendJob/ComponentOutcome/_Batch/CorePipelineResult, run_pipeline, _extract_all, and
run_property_inference. The driver now uses the protocol members instead of ContractComponent
fields.
- Relax BaseApplication's type bound from SystemComponent to BaseModel so non-EVM component
unions fit.
Solana model (composer/spec/solana/model.py): SolanaApplication (programs + authorities),
SolanaProgram / SolanaInstruction / AccountConstraint (roles + program-enforced checks) /
CpiCall — accounts-passed-in, signers, PDAs, CPIs, native fields. SolanaProgramInstance /
SolanaInstructionInstance are the Main/Unit; the instruction instance satisfies FeatureUnit.
Ecosystem (composer/pipeline/ecosystem.py): Ecosystem[App, Main, Unit]; RUST language (Cargo
forbidden_read, Rust/Solana code_explorer prompt); SOLANA chain (validate/locate_main/units,
solana/*.j2 prompt names); ECOSYSTEMS = {"evm", "solana"}. Backend annotations updated to the
new param counts; a pre-existing llm_factory(args) typing nit in the rust entry cleaned up.
Verified: pyright 0 errors on all touched files (one pre-existing _batch_cache_key warning);
84 unit tests pass; a Rust wheel with ecosystem="solana" resolves end-to-end.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Complete the Solana chain: the prompt fragments/templates, a reusable null Solana backend,
a sample Anchor scenario, and the live-LLM front-half gate.
Prompts (composer/templates), with the fragment-composition convention introduced:
- rust/_failure_modes.j2 — the SHARED Rust language failure-mode fragment (overflow-panic DoS,
unwrap/panic aborts, truncating casts, unchecked results); will be reused by Soroban (phase 5).
- solana/_failure_modes.j2 — Solana platform failure modes (missing signer/owner, account
substitution/confused-deputy, unvalidated PDA/bump, arbitrary CPI, lamport/rent & close bugs,
duplicate mutable accounts, reinit, sysvar spoofing).
- solana/{analysis_system,analysis_prompt,property_system,property_prompt,instruction_context}.j2
— Solana analysis (produces SolanaApplication) + per-instruction property extraction; the
property prompt {% include %}s the shared rust/ + solana/ failure-mode fragments.
Null backend (composer/spec/solana/null_backend.py): NullSolanaBackend over the Solana
(App, Main, Unit) triple — records extracted properties without verifying (the gate's
null/echo backend, and the reference a real Solana verifier is modeled on).
Scenario (test_scenarios/solana_vault): a small Anchor lamports-vault program + design doc.
Gate (tests/test_solana_gate.py, expensive): runs real analysis + per-instruction extraction
through SOLANA + the null backend on the vault (Postgres via testcontainers, no prover/solc).
Gate result: PASSED (3 instructions, 27 properties) with sane Solana properties — signer/owner
checks, PDA/bump canonicity, System-Program substitution, reinit-once, arithmetic overflow.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Update §10: phase 4 done — driver Unit/Main generalization (deferred from phase 2),
standalone SolanaApplication model, RUST language + SOLANA chain, the {% include %}
fragment convention (a base template proved unnecessary), a null Solana backend, and
the Anchor vault scenario. Records the live-gate result (3 instructions, 27 sane
properties). Status line now reads phases 1–4 done; 5 (Soroban) and 6 (backends) remain.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Adds docs/crucible-application.md: a plan to pair the existing `solana` ecosystem front half with a new Crucible (Solana fuzzer) backend, built as a Rust application on the PyO3 framework. Key decisions captured: - Crucible is the Solana analog of Foundry (authors a source-language artifact, gates it with a local CLI, refutation-oriented verdicts). - A general RunCommand effect (Rust decides argv, LLM authors only file contents) replaces the prover-specific IoC vocabulary. - Sandboxing every RunCommand is a required, definition-of-done phase (bwrap on Linux; macOS dev mechanism TBD), because the LLM-authored harness runs as native code (verified against Crucible source: cargo build + Command::new, LiteSVM only sandboxes the program under test, no isolation in-tree). - Version compatibility (Crucible/Solana-Anchor/Rust) and a shared Solana build pipeline reused across backends (Crucible no-munge; a future Prover backend munge-and-rebuild). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Adds §7.5: how the harness author gets Crucible documentation, designed for the large-corpus future (a Certora Prover/CVLR Solana backend) rather than Crucible's small doc set. - Build tool-enabled call_llm now as a shared rustapp capability (host-assembled tool belt: backend RAG search over the descriptor's ComposerRAGDB + learned-KB + source tools), so CVLR-Solana reuses it with zero framework change. Fixes the gap that today's IoC call_llm is a tool-less single ainvoke. - Knowledge rides the backend axis (per-wheel rag_db_default), not the ecosystem axis; static injection of a harness cheat-sheet is a Crucible content shortcut layered on top. - Wire the knowledge seam into Phase 3; add open question on one-DB-vs-multiple for CVLR; add key-files rows for the RAG precedent + new crucible_kb builder. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
A backend-agnostic "run a local command over a set of files" effect, replacing
the prover-specific shape for CLI-gated backends (Crucible, cargo build-sbf,
anchor idl). The Rust decider authors program+args; only file contents may be
LLM-derived.
- SDK: Command::RunCommand { program, args, files } + Observation::CommandResult.
- composer/rustapp/command.py: run_local_command — the single command choke point
(write files into a confined workdir, exec-not-shell, timeout, optional
semaphore, capture). This is what phase-6 sandboxing (docs §7.4) will wrap.
- loop.py / adapter.py: Effects.run_command, drive_session branch, and
RealEffects.run_command with a lazily-created per-formalize workdir.
- tests/test_rustapp_command.py: round-trip, path confinement, no-shell-injection,
missing binary, non-zero exit, timeout.
No sandbox yet (network-off/clean-env/resource-caps is phase 6); run only on
trusted input for now.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The RustBackend adapter was hardwired to the EVM types (SourceApplication /
ContractInstance / ContractComponentInstance / main_instance), so a non-EVM
(e.g. solana) wheel could not run. Generalize it over the resolved ecosystem:
- FeatureUnit gains feature_json() — the generic way to marshal a unit's
semantic content across the FFI. EVM returns the component model_dump
(byte-identical to before); Solana returns {program, instruction}.
- RustBackend holds the resolved ecosystem and uses ecosystem.locate_main
instead of main_instance; prepare_system/formalize/to_artifact_id/finalize
now work through FeatureUnit (feature_json / slug / display_name) rather than
EVM-specific attrs.
- host.build_backend / build_application thread the ecosystem in.
EVM path preserved (echoprover + rustapp tests green, pyright clean).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
A new Solana verification application (ecosystem="solana") backed by the Crucible fuzzer. Phase 1 provides the declarative descriptor + a real validate_preconditions; the authoring loop is a deliberate stub (phase 1 covers preconditions + build/IDL + dry-run infra, no LLM). - rust/crucible-app: descriptor (phases incl. a UI-only Build Harness phase; args --crucible-version/--fuzz-timeout/--fuzz-cores/--stateful; rag_db_default "crucible_kb"; fuzz-flavored event kinds; provisional artifact layout) + validate_preconditions (crucible/cargo-build-sbf/anchor on PATH via a pure PATH scan, plus a buildable Cargo workspace check) + refutation-oriented backend_guidance. - Added to the rust workspace; maturin added as a dev dependency to build the wheel. Verified: cargo check clean; `maturin develop` builds+installs the wheel; the host loads the descriptor, resolves ecosystem -> solana/rust, and validate_preconditions reports the missing workspace correctly. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Completes Crucible phase 1: the build + dry-run infrastructure, gated end to end. - composer/spec/solana/build.py: build_program — the shared Solana build capability (source -> target/deploy/<program>.so [+ optional IDL]) routed through the same run_local_command choke point the RunCommand effect uses. Crucible calls it in no-munge mode; a future Prover/CVLR backend calls it in munge-and-rebuild mode. - test_scenarios/solana_vault: made a buildable Cargo workspace (Cargo.toml, programs/vault/Cargo.toml, rust-toolchain.toml) and fixed the program so it compiles against anchor-lang 1.0.1 (valid declare_id, invoke-based system transfer, renamed the #[program] module to vault_program to avoid a crate/module name clash in the harness). Build outputs + the generated fuzz harness are gitignored. - tests/test_crucible_gate.py (expensive): loads the descriptor (ecosystem -> solana), runs validate_preconditions, builds vault.so, materializes a trivial hand-written fuzz harness (crate deps resolved from CRUCIBLE_REPO), and asserts `crucible run vault invariant_vault --dry-run` exits 0. No LLM, no authoring. Gate verified green locally (cargo-build-sbf + crucible on PATH, CRUCIBLE_REPO=~/src/crucible). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Implements §7.1: a Crucible deliverable is one Cargo crate (single [[bin]] invariant_test) assembled from a shared fixture + one test fn per component, not one file per component. Phase 1 revealed crucible's CLI hardcodes the bin name, so per-component bins are a dead end; components are selected by a Cargo feature whose name equals the test fn (Crucible's #[invariant_test] macro self-gates main() by #[cfg(feature = "<fn name>")]). - composer/crucible/harness.py: CrucibleHarness assembler (renders Cargo.toml feature list + src/main.rs = shared fixture + verbatim per-component test fns) and CrucibleDep (resolves crucible/solana/anchor deps from a local checkout, §6.1). - composer/crucible/store.py: CrucibleArtifactStore — per-component write_artifact folds the test fn into the crate and re-renders it under fuzz/<program>/, while the shared base writes metadata under certora/crucible/ (the same split Foundry uses). - tests/test_crucible_gate.py: phase-2 gate — a hand-authored fixture + one test written through the store assembles a crate that `crucible run vault c_deposit --dry-run` accepts; metadata lands under certora/crucible/ and a co-located EVM certora/specs/ deliverable is untouched. Gate verified green. - docs §7.1 corrected to the verified macro-self-gating mechanism (the earlier #[cfg]-wrapped-section description was wrong; the gate caught it). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
RealEffects.call_llm now runs a bounded, tool-enabled agent turn (env.all_tools: source navigation + RAG search + learned-KB, plus a result tool) via run_to_completion, instead of a bare single ainvoke. This is the shared framework change §7.5 calls for: the harness author can pull in framework docs / read the program mid-turn, and a large-corpus backend (CVLR-Solana) reuses it by shipping only a knowledge DB — no framework change. echoprover unit tests use a fake Effects (not RealEffects) so are unaffected; real validation is the phase-3 authoring gate. (The pyright NotRequired/MessagesState warning on the new state class is the pre-existing langgraph-stub false positive that also affects composer/spec/code_explorer.py.) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The seccomp deny-list keyed on exact x86_64 syscall numbers was bypassable via the x32 ABI: an x32 call runs under the same AUDIT_ARCH_X86_64 identity (so seccompiler's arch guard passes it), but its syscall number is OR'd with __X32_SYSCALL_BIT (0x4000_0000), so it misses every exact-number rule and hits default-allow — a full bypass of the socket/io_uring/ptrace/process_vm denies. This matters most on kernels < 6.7 (the AL2023 6.1 target), where Landlock does no network filtering and seccomp is the sole network control, so the bypass is unconditional egress to the network + IMDS. Fix: mirror every deny onto its x32-tagged syscall number in apply_seccomp (x86_64 only; aarch64 has no per-syscall compat bit). Deriving the mirror from the already-built rule map means any future deny is covered automatically. Regression test records the errno of an x32 socket() attempt and asserts EPERM (seccomp caught it) rather than ENOSYS (kernel rejected it after the filter let it through) — a real guard even on x32-disabled CI kernels. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Landlock + seccomp are kernel-mediated and a container shares the host kernel, so ubuntu-latest cannot validate run-confined on the 6.1 kernel we ship on. This job boots the real Amazon Linux 2023 kernel-6.1 KVM cloud image under QEMU/KVM (SHA256-verified, UEFI/OVMF, cloud-init SSH seed) and runs tests/test_sandbox_escape.py inside it. On 6.1 the suite exercises the 6.1 contract specifically: Landlock FS enforced, network seccomp-only (no Landlock net < 6.7), scopes absent (< 6.12, so the signal / abstract-UDS vectors self-skip), and the x32 deny-mirror asserted regardless. The guest is kept dependency-light: the suite is stdlib + pytest only, so we install pytest via uv on PYTHONPATH and pass --noconftest to skip tests/conftest.py's heavy imports (its fixtures are all in-module). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The "copy repo into the VM" step tar'd the whole workspace, which by that point holds the running VM's al2023.qcow2 (QEMU actively writing it) plus seed.iso / serial.log / repo.tgz — tar aborts with "file changed as we read it". Use git archive HEAD instead: a clean snapshot of tracked source, which is all the escape suite needs and structurally cannot include the runtime artifacts. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
actions/checkout@v4 and upload-artifact@v4 run on the deprecated node20 runtime, which emits a deprecation warning now that the runner defaults to node24. Bump both to v5 (first major on node24) to clear it; our usage (plain checkout, path-list upload) is unaffected by the majors' breaking changes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ressions Negative control for the sandbox-escape (kernel 6.1) workflow. Disables the seccomp socket() network block so socket(AF_INET/AF_NETLINK/AF_VSOCK,…) succeeds, breaking the "No network" guarantee. The escape suite must go RED (inet_sock / netlink / vsock / net_ext / imds leak) — proving the CI fails when the sandbox is broken, not just when it works. REVERT THIS COMMIT before merging. Verified locally: run-confined builds and tests/test_sandbox_escape.py fails on the network probes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ches regressions" This reverts commit 6f965c1.
The base image baked the run-confined command-sandbox launcher onto PATH unconditionally (Dockerfile stage 1b + a COPY into /usr/local/bin). Not every AutoProver container needs the sandbox, so pull it out of the base image and provide it as a runtime-mounted, opt-in building block instead. - scripts/Dockerfile: drop stage 1b and the run-confined COPY; leave a pointer to the overlay. - scripts/Dockerfile.sandbox: builds run-confined in a throwaway Rust stage and publishes the binary into a mounted volume via a minimal bookworm-slim image. - scripts/docker-compose.sandbox.yml: overlay with a one-shot run-confined-build service that populates a run_confined named volume, plus the wiring onto the autoprove service (read-only mount + RUN_CONFINED_BIN, gated behind the builder via service_completed_successfully). Consumers that don't add this overlay get a sandbox-free image. - docs/command-sandbox.md: update the §9 note — the launcher is resolved via $RUN_CONFINED_BIN (overlay-mounted) rather than baked into the image. The launcher provider already resolves $RUN_CONFINED_BIN ahead of PATH (composer/sandbox/launcher.py), so no code change is needed. Verified end-to-end: the publisher lands a 0755 ELF in the volume and `run-confined --probe` reports `landlock FullyEnforced` from a read-only mount. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Bring the command-sandbox hardening + the opt-in Docker overlay from eric/sandbox onto the Crucible branch. Crucible's run-confined was the original pre-hardening baseline (its main.rs etc. were byte-identical to the sandbox PR-1 commit), so the security fixes merge cleanly as "take theirs": - run-confined: close the io_uring network bypass and the x32-ABI seccomp bypass (unconditional egress on kernels < 6.7, incl. the AL2023 6.1 target), Landlock scopes + TCP default-deny, grant only shared cargo bin/. Plus the recipes.py / command-sandbox.md / escape-suite updates that go with them. - CI: the sandbox-escape-6.1.yml workflow + provision script. Docker: the run-confined launcher is no longer baked into the base image. Consumers opt in via the new scripts/docker-compose.sandbox.yml overlay (builds scripts/Dockerfile.sandbox, mounts the binary at $RUN_CONFINED_BIN). Crucible's containerized path — whose default provider is fail-closed — must add that overlay. Conflict resolution notes: - rust/Cargo.toml: kept crucible's (workspace members autoprover-sdk / crucible-app / example-app; sandbox never changed this file from base). - rust/Cargo.lock: dropped the incoming file — crucible gitignores it and the incoming lock covers only run-confined, not the app members. - scripts/Dockerfile: applied the overlay change (dropped stage 1b + the run-confined COPY) while keeping crucible's crucible_kb.rag.json COPY. Verified: cargo build -p run-confined --release succeeds and `--probe` reports landlock FullyEnforced. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The base image no longer bundles run-confined (it moved to the scripts/docker-compose.sandbox.yml overlay). Document the binary-resolution order for the host demo (dev fallback still works unchanged) and tell containerized Crucible runs to add the overlay, since the launcher provider is fail-closed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add a Crucible toolchain image + compose overlay so `console-crucible` and the crucible test gates run entirely in-container, and make the gates container-aware. Toolchain image (Option 1 / one blessed combo — docs/crucible-toolchain-versioning.md): - scripts/Dockerfile.crucible layers on the lean base and bakes rustc 1.89.0 (the scenario's harness toolchain) + a newer CLI toolchain (anchor-cli needs rustc >= 1.91), Solana/agave platform-tools 3.1.10, anchor-cli 1.1.2, and the public crucible v0.2.0 checkout + CLI, plus the crucible_app + test dep groups. - The toolchain installs into the runtime $HOME (/opt/autoprove/home) — the exact layout the RunCommand sandbox recipe grants (RUSTUP_HOME/CARGO_HOME + ~/.local/share/solana + ~/.cache/solana), so the confined build can exec it. A build-time sBPF build of the bundled scenario pre-installs platform-tools so the offline/non-root run-time build finds them present. - scripts/docker-compose.crucible.yml swaps the autoprove service onto this image; it stacks on the sandbox overlay (Crucible is fail-closed, so run-confined is mounted from there). Wiring: - autoprove-entrypoint.sh: console-crucible/tui-crucible fail-fast if the toolchain or run-confined is missing (RAG DSN derives from PG env; no --rag-db needed). - docker-compose.sandbox.yml: drop the profile gate on run-confined-build — a depends_on a profiled service is "undefined" to `compose build`/`config` unless that profile is also passed, which broke the single-profile crucible build. Tests runnable in-container: - conftest: pg_container targets an existing postgres via $COMPOSER_TEST_PG_URL (the compose service) instead of testcontainers — no docker-in-docker. - test_crucible_e2e_gate / test_crucible_sandbox_gate: build a writable copy of the scenario (the in-image copy is read-only for the non-root user; also stops host runs polluting test_scenarios/), and the e2e provisions roles/DBs idempotently against the persistent compose postgres. - docs/crucible-demo.md §8: the full containerized run + in-container e2e recipe. Verified: base + crucible images build from scratch; the sandbox gate (cargo-build-sbf under run-confined, offline) passes in-container on the clean image and on the host. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The package-data glob `templates/*.j2` only matched the top level, so the wheel omitted composer/templates/solana/*.j2 and templates/rust/*.j2 (and the report's prism-cvl.js). Any run whose CWD isn't the source tree loaded templates from the installed wheel and hit `TemplateNotFound: 'solana/analysis_system.j2'` — which is exactly the containerized `console-crucible` (CWD=/work). The source-tree runs (pytest inserts the repo root on sys.path) masked it. Recurse into the subdirs and include the JS asset. Verified: the built wheel now contains solana/*.j2 (7), rust/*.j2, and prism-cvl.js; console-crucible in the container gets through analysis + property extraction. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The confined Rust build failed on a read-only shared RUSTUP_HOME:
error: could not create temp file /…/.rustup/tmp/…: Permission denied (os error 13)
Even with a fully pre-installed toolchain, the rustup proxy (cargo/rustc/
cargo-build-sbf) writes scratch into $RUSTUP_HOME/tmp on every invocation, and the
recipe granted RUSTUP_HOME read-only — so the containerized harness build (whose
image bakes a shared, read-only toolchain) died on every setup attempt, and Crucible
gave up "did not pass compile/judge in 7 attempts". Host dev flows masked it: there
~/.rustup is writable.
Fix mirrors the existing private per-run CARGO_HOME (sandbox_rustup_home): point
RUSTUP_HOME at <workdir>/.sandbox_rustup, symlink `toolchains` back to the shared
home (still granted read-only, so toolchain bytes are shared not copied) and keep
tmp/downloads/update-hashes as this run's writable scratch. `settings.toml` is copied
so default/override resolution still works. No new shared-writable grant, so the
untrusted-build isolation the escape suite guards is unchanged.
Also exclude `.sandbox_rustup/` from RUST_FORBIDDEN_READ — its `toolchains` symlink
would otherwise make the source tools enumerate the whole toolchain into the prompt.
Verified: the confined sbf build (a rustup proxy) passes on the host under the new
per-run home.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…s it)
The in-container e2e reached the harness setup and failed every attempt with, in
the offline confined build:
error: could not download file from '…/channel-rust-stable.toml.sha256'
to '…/.sandbox_rustup/tmp/…': dns error (offline sandbox)
Root cause: crucible-fuzz-cli pins the harness build to the `stable` toolchain — it
writes a `rust-toolchain.toml` with `channel = "stable"` into the fuzz crate and sets
`RUSTUP_TOOLCHAIN=stable` (crates/crucible-fuzz-cli/src/lib.rs). The image installed
1.89.0 (scenario) + a newer CLI toolchain but NOT `stable`, so the confined, offline
build tried to rustup-download it and failed. Host dev flows always have a `stable`
toolchain, which is why only the baked image hit this.
Fix: preinstall `stable` alongside the others so the offline build finds it present.
(The per-run RUSTUP_HOME from the previous commit remains correct defense-in-depth —
rustup needs writable scratch against the read-only baked toolchain — but installing
`stable` is what actually unblocks the harness build.)
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… codes Replace the hand-rolled argv loop with a clap derive `Cli` that lowers into the existing `Config`. `--probe` is still handled before clap (it short-circuits into a self-restricting kernel check and must not trip the required-command rule); `--allow-env`'s NAME / NAME=VALUE semantics are preserved. Exit codes now follow the `env`/`timeout` convention so the launcher's own failures stay out of the wrapped command's status range: 125 launcher failed (bad argv OR sandbox unavailable) — fail-closed 126 command found but not executable (exec != ENOENT) 127 command not found (exec == ENOENT) else the child's status passes through the execve. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- Add CommandResultObservation TypedDict for the as_observation() payload. - Drop the lexical absolute/`..` guard in _confined_target; the resolve().relative_to() check already subsumes it (and catches symlink escapes too). - Collapse the sem branch via contextlib.nullcontext(). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add a SandboxArgs TypedDict (NotRequired fields mirroring the overridable SandboxConfig fields) and type from_env(**overrides) with Unpack[SandboxArgs], so unknown/mistyped keyword overrides are caught by the type checker instead of at runtime. Return Self rather than a quoted forward reference. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…istry Declare the command-sandbox providers as composer.sandbox_providers entry points (pyproject.toml) and resolve them by name in SandboxConfig.resolve_provider, importing the selected mechanism's module lazily. This drops the in-module registry (_PROVIDERS dict, register_provider, get_provider) and the launcher's import-time self-registration, so the policy seam no longer references any concrete mechanism at all. Net: provider resolution lives in one place; the launcher module is imported only when the "launcher" provider is actually constructed (verified). Note: entry points are baked into install metadata, so environments must be (re)installed (uv pip install -e .) for the providers to resolve. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The Rust-backend handoff (`SandboxConfig.backend_spec`) used to serialize the policy field-by-field (`ro`/`rw`/`allow_env`/`network`/`rlimits`) plus the launcher `binary` path, so the backend had to reassemble a run-confined argv itself — duplicating the flag-mapping that `LauncherProvider.wrap` already owns and pinning the wire shape to one mechanism. Add `SandboxProvider.argv_prefix(policy)` — the mechanism-agnostic confinement wrapper up to the `--` separator — and express `wrap` as `[*argv_prefix, program, *args]`. `backend_spec` now ships just that opaque prefix (empty for the `none` passthrough) plus `timeout_s`, typed as the new `BackendSpec` TypedDict. The backend prepends it with no knowledge of the sandbox tool, so adding a provider is a pure-Python change on both launch paths. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`LauncherProvider.available` shelled out to `run-confined --probe` via a blocking `subprocess.run(timeout=10)` — stalling the event loop for up to 10s on the async command path (`run_local_command` → `ensure_available`). Make the probe async end-to-end: `SandboxProvider.available` (and `NoneProvider`, `ensure_available`) are now coroutines, and the launcher uses `asyncio.create_subprocess_exec` + `asyncio.wait_for`. Behavior is unchanged — OSError fails closed, a probe timeout kills the child and propagates. `SandboxConfig.backend_spec` becomes async to await the check (no production callers yet). Tests await the seam; the two collection-time `skipif` guards drive the coroutine with `asyncio.run`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`Availability(ok=bool, reason=str)` let you build the nonsensical `Availability(ok=True, reason="...")` — an available result carrying a reason. Replace it with `Availability = Literal["ok"] | Reason`, where a `Reason` holds the explanation and the `"ok"` arm has nowhere to put one, so the illegal state is unrepresentable. `ensure_available` discriminates on `avail != "ok"`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`name` is only ever read, so declare it as a read-only `@property` in the protocol (implementers still back it with a plain class attribute). Drop `@runtime_checkable`: the only isinstance check was one conformance test, and a runtime_checkable protocol only verifies member *presence*, not signatures. Rewrite that test as a static `provider: SandboxProvider = NoneProvider()` assignment so pyright is the conformance gate. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Collapse shared_cargo_ro_paths to a conditional expression (the list accumulator only ever held zero-or-one element), and use ro_candidates.extend instead of `+= list(...)`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Adopt the sandbox provider's new Rust-facing interface: backend_spec now
emits an opaque {argv_prefix, timeout_s} instead of the rich policy JSON
(run_confined/ro/rw/allow_env/network/rlimits). Python owns assembling the
run-confined argv; the Rust backend just prepends argv_prefix to its command.
- rust/autoprover-sdk: Sandbox is now {argv_prefix, timeout_s}; run_confined
launches [*argv_prefix, program, *args] (empty prefix = run directly).
Dropped the Rlimits struct and the per-flag argv assembly.
- composer/rustapp/adapter.py: await the now-async backend_spec; _sandbox_spec
is async and emits the new passthrough shape.
- composer/spec/solana/build.py: assert build_policy (now Optional) is present
on the enabled path.
- Resolve rust/Cargo.lock conflict: keep it untracked (gitignored on crucible).
- Update docs/rust-backend-api.md, pyproject entry-point comment, and tests to
the new interface.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The demo/gate validate assertions expected a stale singular
{"kind":"verdict","verdict":{…}} shape, but ValidateOutcome::Verdicts
serializes as {"kind":"verdicts","verdicts":[[unit, verdict]]}. These
assertions had never run here (the app wheels weren't built); building
them for the gate run surfaced the drift. Unrelated to the sandbox
interface change.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The gate passed the per-property unit (c_deposit) to validate(), but crucible-app puts every invariant in ONE #[invariant_test] fn named c_invariants (SINGLE_HARNESS_FN), and the macro cfg-gates main() on `feature == fn name`. Building with c_deposit left main out (E0601: main function not found). The real pipeline validates the unit's *target* (u["target"] or u["unit"]) — which units() sets to c_invariants. Mirror the pipeline: give the prop a slug, derive the target the way adapter.py does, and validate c_invariants. Also assert the correct ValidateOutcome::Verdicts shape and the target field on units. Drift against crucible-app's single-shared-harness model (docs/crucible-unit-granularity.md §3), not the sandbox interface; verified passing against a real crucible build + fuzz run. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Bring in the sandbox PR (#73, now on master) plus the other 24 master commits. The sandbox work already existed on crucible via the earlier eric/sandbox merge, so most conflicts were add/add on shared sandbox files. Conflict resolutions: - composer/pipeline/core.py: reconcile the two pipeline refactors — keep crucible's ecosystem-agnostic extraction (FeatureUnit / ecosystem seam) and adopt master's parameterized properties cache key. _extract_all now takes prop_key and uses PROPERTIES_KEY(backend.analysis_spec.properties_key); every backend already supplies a distinct properties_key. - rust/Cargo.toml: keep crucible's full workspace (sdk/example/crucible/ run-confined + [workspace.dependencies]); master had only run-confined ("later PRs re-add the framework crates"). - composer/sandbox/recipes.py: keep crucible's per-run RUSTUP_HOME handling (sandbox_rustup_home) that master lacks. - scripts/docker-compose.sandbox.yml: keep crucible's deliberately un-gated run-confined-build (4e05e25 — depends_on on a profiled service breaks `docker compose build`/`config`); newer than master's gated version. - scripts/Dockerfile: keep crucible's crucible_kb RAG COPY + launcher note. - pyproject.toml: keep crucible's more precise entry-point comment. - rust/Cargo.lock: keep untracked (gitignored on crucible). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Post-merge integration fixes surfaced by rebuilding the venv and running
the suite:
- test_crucible_granularity: pass the new `prop_key` arg to _extract_all
(the master merge parameterized the properties cache key).
- test_{crucible_setup,crucible_formalize,crucible_e2e,solana}_gate: import
the DB-bootstrap helpers (_MEMORIES_DDL/_RAG_DB/_VECTOR_DBS/_db_url) from
tests.conftest, where master moved them out of test_autoprove_integration.
Full non-expensive suite: 341 passed, 9 skipped. The 2 fake-LLM
test_autoprove_integration failures (invariant-cvl tape exhausted in
CVL_GEN) reproduce identically on clean origin/master, so they are a
pre-existing stale-tape issue, not from this merge.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The CI pyright job (uv sync --group ci; pyright composer/ analyzer sanity_analyzer certora_autosetup) flagged two reportReturnType/ reportArgumentType errors in adapter.py: `_sandbox_spec` was annotated `-> dict` and `author_and_compile` took `sandbox_dict: dict`, but the value is `config.BackendSpec` (a TypedDict, not assignable to a bare `dict`). Annotate both — and the setup-path local — as BackendSpec; the passthrough dict literals structurally satisfy it. Type-only change. CI pyright now: 0 errors. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The command sandbox shipped to master as #73 and eric/crucible merged it, so it's now an upstream dependency, not a PR in this stack. Update the plan: - 4 stacked PRs -> 3 (ecosystem -> rust framework -> crucible); former PR 3 (sandbox) becomes an "Already landed (#73)" section. - PR 2 no longer carries the sandbox seam (on master); it consumes master's backend_spec ({argv_prefix, timeout_s}, async, BackendSpec). - Fold the two residual crucible-specific sandbox deltas (recipes.py rustup home, docker-compose un-gate) into the crucible PR; update cross-cutting table + execution recipe; recompute the delta headline. - Name the branches: eric/ecosystem, eric/rust, eric/crucible-app. - Flag that PR 1's Counter-tape gate currently fails on master itself (pre-existing stale invariant-cvl tape; needs re-recording upstream). Co-Authored-By: Claude Opus 4.8 (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
2 participants
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.
No description provided.