Crucible prototype#64
Draft
ericeil wants to merge 105 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>
…lags (parity #3) These descriptor-declared flags were parsed + validated but never threaded to `crucible run` (which hardcodes `--mode explore` and passes only `--timeout`), so they did nothing — an inert flag is worse than none. Remove them from the descriptor's `args`, keeping only `--fuzz-timeout` (the one that's actually honored). If/when the fuzz command grows `--cores` / stateful mode / a version pin, re-add the flag together with the wiring (the version pin is tracked in docs/crucible-toolchain-versioning.md). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…obal) Explores crucible-application.md §10 Q1: moving fuzzing-scenario generation from per-instruction units to a whole-program (global) context. Covers how it works today (the harness/fuzzer are already whole-program; only property selection + test + verdict are sharded per instruction), the proposed change and the per-instruction→per-component→whole-program spectrum, pros/cons, a comparison to Foundry (stateful invariant fuzzing is already whole-contract) and CVL/prover (per-rule symbolic, not scenario-based), and a staged recommendation (widen extraction context first, then per-invariant units), noting it supersedes the crate-per-component concurrency work and pairs with coverage-as-signal. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Fuzzing scenarios are now generated from a whole-program context and fanned out one harness/fuzz-run per invariant, instead of per-instruction (docs/crucible-unit-granularity.md). A coverage-guided fuzzer explores cross-instruction action sequences, so instruction- local properties were an artificial boundary; global invariants match the engine and Foundry's stateful-fuzz model, and one run per invariant avoids N× re-fuzzing the same action space. - Ecosystem gains a `global_extraction` strategy (+ `extraction_unit` / `property_unit` hooks). SOLANA opts in; EVM keeps per-component extraction. - core `_extract_all`: under global extraction, run ONE whole-program property pass, then emit one batch per resulting invariant — each its own formalize (harness + fuzz + verdict + report row). Per-component path unchanged for EVM. - solana/model: SolanaProgramInstance is now a FeatureUnit (the whole-program extraction context); new SolanaInvariantUnit (per-invariant unit; feature_json carries the whole- program instruction API so the test author can drive any action). - prompts: solana property system/user reframed from single-instruction to whole-program invariants (new program_context.j2); crucible-app per-component author prompt reframed to "whole-program property, holds after any action sequence". No adapter/store change: per-invariant units marshal through the existing formalizer (component=whole-program API, props=[invariant], slug=invariant slug). Tests (test_crucible_granularity, no toolchain/LLM): units, ecosystem wiring, and the driver fan-out. pyright clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…its) Front-half gate confirms whole-program cross-instruction invariants are extracted. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Record why per-invariant fuzzing can't be trivially parallelized: separate cargo target dirs recompile the litesvm/libafl deps N× (regression), and a shared CARGO_TARGET_DIR collides on Crucible's hardcoded `invariant_test` binary name. The only clean path is `crucible run --binary-in` (serial build, parallel fuzz), a formalize-phase redesign whose payoff only lands at production fuzz budgets — deferred. No code change; tree stays at the green per-invariant state (fd51700). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… "Rust-based" leak
The tool-enabled call_llm turn hardcoded a system prompt calling the model "an
authoring agent for a Rust-based AutoProver backend" — an odd implementation detail to
expose, and largely redundant with the decider's own instruction. Now the decider owns
it: its call_llm payload may carry a `system` prompt (backend-defined) alongside the
`instruction`; when absent, a neutral, backend-agnostic default applies (tool-using
agent + result-tool contract only — no language/domain specifics). Also extracts the
`instruction` cleanly instead of dumping the whole `{"instruction": ...}` dict as the
initial prompt. Python-only; the Crucible decider's instructions already carry the
specifics, so it uses the neutral default (no Rust change).
Test: tests/test_rust_llm_agent.py pins the split + the backend-agnostic default.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
A completed run showed only "Report ✓" with no visible results — the
per-invariant GOOD/BAD verdicts were written to report.json but never
surfaced. Two additions, following the CVL/Foundry report conventions:
Console/TUI rollup (composer/crucible/results.py):
- summarize per-invariant verdicts baked into result.outcomes into a
tally + listing, using the report's own crucible outcome labels
(render.outcome_label, now public). Wired into console-crucible's
counts block, the tui-crucible completion toast, and its post-exit
printout.
Live verdict reporting (data-driven notice events):
- EventKind gains a `notice` flag (SDK + Python descriptor). The generic
frontend routes notice-flagged events through post_notice (a persistent
callout + toast) instead of the collapsed events log.
- the Crucible decider declares a `verdict` notice kind and emits a
structured {outcome, name, line} event at each terminal publish, so
each invariant's result pops the moment its fuzz run finishes.
Also fixes a pre-existing workspace break: example-app's Formalized
literal was missing the `verdicts` field.
Tests: test_crucible_results, test_rust_frontend (wheel-independent);
test_crucible_events updated for the trailing verdict emit.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Two design notes for reshaping the Python↔Rust backend boundary: - rust-ioc-loop.md: what the current inversion-of-control effect loop (Command/Observation + resume + drive_session) does, why it exists (sync FFI/no async bridge, testability, the command-line security invariant, a backend-agnostic host), what it costs, and options to remove it. - rust-backend-api.md: the chosen shape — the backend becomes a passive service of pure callouts (descriptor, units, author_prompt, judge_prompt, finalize) plus two GIL-releasing blocking calls (compile, validate) that run the toolchain directly via a shared run-confined helper. Python owns the author→compile→judge→validate loop. No RustSession/resume, no Command/Observation protocol, no async runtime in the wheel. Decisions captured: shared autoprover_sdk::run_confined helper; compile and validate kept separate; validate is per-unit (host enumerates via units(), owns scheduling); judge_prompt present with a default no-op; wheel-owned RAG deferred (external crucible_kb stays). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Implements docs/rust-backend-api.md. The Rust wheel is no longer a driver (the resume() state machine + Command/Observation protocol + drive_session); it is a passive Backend that answers pure callouts, and Python owns the author→compile→judge→validate loop. autoprover-sdk: - New `Backend` trait: descriptor, validate_preconditions, units, author_prompt, judge_prompt (default None), compile, validate, finalize. Drops Command/ Observation/FormalizeSession/resume/RustSession and the setup/formalize session I/O types. - `compile`/`validate` run the toolchain directly via a shared `run_confined` helper (materialize files path-confined, assemble the run-confined argv from a Python-authored `Sandbox` policy, spawn + timeout + capture). Exposed as GIL-releasing #[pyfunction]s so Python calls them with asyncio.to_thread — no tokio, no pyo3-async bridge. crucible-app / example-app: implemented as `Backend`s. Crucible's prompts / api_facts / diagnostics are lifted out of the old sessions as pure functions; compile = `crucible run --dry-run`, validate = one `crucible run --mode explore` per unit. echoprover becomes a self-contained demo (compile no-op, validate GOOD). Python: - adapter.py: RustFormalizer.formalize runs the loop (run_llm_agent → compile → judge → per-unit validate), emitting build_output/verdict itself; shared `author_and_compile` helper used by the Crucible setup artifact too. Drops RealEffects/drive_session/loop.py. - SandboxConfig.backend_spec() serializes the policy (+ run-confined path, fail-closed) into the wheel's `Sandbox` JSON. - crucible/backend.py: setup fixture authored via the same loop; per-invariant feature reservation; store folds the validated feature. Tests updated to the callout API; test_sandbox_command tests run_local_command directly. Fast suite green (246); rust workspace + pyright clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…nent dry-run)
The service-API e2e ran ~2× the old loop (72 vs 37 min): each invariant did a
separate `compile` (crucible --dry-run) AND a `validate` (crucible --mode explore),
i.e. two toolchain builds per unit instead of the old loop's one. And one invariant
flipped GOOD→ERROR because validate classified is_build_error on the fuzz run's
output before checking the exit code.
Fuse (option 1): the component path drops the separate dry-run — validate's own
build IS the gate. `Backend::validate` now returns `ValidateOutcome`
(BuildFailed{errors} | Verdict): a build failure re-authors the whole spec (units
share one build), else it's a per-unit verdict. RustFormalizer.formalize runs one
fused author → judge → validate loop; author_and_compile stays for the setup
fixture (a genuine compile-only gate, one-time — not the 16× cost).
Classification fix: validate now checks [FUZZ_FINDING]→BAD and exit_code==0→GOOD
BEFORE is_build_error, so a clean fuzz run whose logs contain `error[`-looking
runtime text is no longer misread as a build failure.
Tests updated for the ValidateOutcome shape; fast suite green (49), rust + pyright
clean.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Team feedback: this import is a dead end (PEP 563 never became default, superseded by PEP 649/749 lazy eval in 3.14+ so it breaks going forward) and it doesn't solve its intended problem (stringizing all annotations breaks runtime introspection — pydantic/dataclasses/get_type_hints, and our annotation-driven graph wiring). - Removed it from the modules created/rewritten in the service-API work (rustapp/adapter, crucible/backend, crucible/results + their tests). Repo targets 3.12+, so `X | None` / `list[...]` / PEP 695 generics work eagerly; the only forward refs here were already quoted individually. - Added CLAUDE.md documenting the rule (with the why + what to do instead) so agents don't reintroduce it. ~38 pre-existing occurrences remain in older modules (not swept here). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Applies the no-future-annotations policy (CLAUDE.md) to every file this branch (eric/crucible) changed vs master — 36 modules/tests beyond the 8 already done. Verified each edited module imports at runtime (catches any latent unquoted forward reference, which pyright can't see) and pyright is clean; 246 non-expensive tests pass. Only quoted forward refs were present, so no annotations needed re-quoting. `_llm_agent.py` is untouched (its match was a docstring mention; it already has no statement). One master-only file (composer/ui/ide_content.py) still has the import and is left alone — this branch didn't change it. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The "deliberately without from __future__ import annotations" paragraph framed this module as a special case; the repo now bans the import everywhere (CLAUDE.md). Keep only the load-bearing fact — bind_standard introspects __annotations__ at runtime, so annotations must stay real objects — as one concrete reason for the policy. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The service-API refactor removed RealEffects (which consumed the RunProver/ RunFeedback effects), so the ProverHook/FeedbackHook plumbing is dead: nothing supplies a hook and nothing consumes one. Removed the type aliases (adapter.py) and the prover/feedback fields + params they threaded through BackendOptions, build_application, and run_rust_pipeline (host.py). pyright clean; 246 non-expensive tests pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The `_llm_agent` module existed to isolate eager annotations from the rest of rustapp, which used `from __future__ import annotations` (bind_standard introspects _LlmState.__annotations__ to unwrap `result: NotRequired[T]`, which stringized annotations break). That reason is gone now that the branch bans the future import everywhere, so the split no longer buys anything. Move `run_llm_agent` + `_split_prompt` + `_DEFAULT_SYS_PROMPT` + `_LlmState`/`_LlmInput` into adapter.py (right beside its only callers, `_author_turn`/`_judge_turn`), drop the two lazy imports, and keep a load-bearing comment on `_LlmState` about eager annotations (pointing at CLAUDE.md). adapter.py already pulled langgraph/graphcore transitively, so no import-time change. Test import updated. pyright clean; 246 non-expensive tests pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Backward-compatible additions to the Backend/AppDescriptor surface so an application can be defined entirely by its Rust wheel (docs/rust-pure-app.md): - AppDescriptor: `setup` (shared setup artifact), `deliverable_mode` (per_component | callout), `serialize_toolchain`, `confine_by_default`, `component_noun`. All defaulted; existing wheels load unchanged. - Backend trait: `sandbox_grants` (pure; extra ro/env unioned into the host-authored policy) and `workspace_prep` (pure; declares a plan — files to write, dirs to `cargo fetch`, a program to build — that the *host* executes with the shared warm/build helpers). Keeping prep a pure plan preserves the existing network posture: warming stays unconfined, the build stays confined + offline; the codebase never gives a confined process network. - FFI + export_app! wire the two new pure callouts; pydantic descriptor mirrored. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The command sandbox never gives a confined process network (rust_build_policy hardcodes network=False; warming runs unconfined). So the earlier draft's 'prep sandbox with network:true' would be a new capability the codebase avoids. Revised §4 to a pure workspace_prep callout (files / warm_dirs / build_program) executed by the host with the existing shared helpers — posture byte-identical to today. Updated §2/§6/§7/§8/§9/§10 to match. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The generic host now expresses everything Crucible needed a bespoke package for, gated on descriptor fields so echoprover is unaffected (docs/rust-pure-app.md): - store: `deliverable_mode=callout` writes only metadata per component; the wheel's finalize renders the whole deliverable. `deliverable_primary` gives the report link. - adapter: RustPreparedSystem now runs the wheel's workspace_prep plan (write files → cargo fetch warm_dirs → build_program, posture unchanged), authors the optional shared `setup` artifact, injects declared args + the setup result into every component's context, and serializes toolchain runs when serialize_toolchain is set. finalize's payload is enriched with artifact_text/property_units/setup. - entry: descriptor-driven env (rag_db_default → corpus search tools, via the new composer/tools/rag_env registry), confine_by_default builds the launcher policy with the wheel's sandbox_grants, and declared args are threaded to the backend. - results (moved crucible/results.py → rustapp/results.py, parametrized by backend_tag) + component_noun render a generic verdict summary in console_main/tui_main. echoprover rebuilt against the new SDK; 24 rustapp tests green, composer/crucible (still present) unchanged and importing. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…econdition (phase 3)
The wheel now fully defines the Crucible app (docs/rust-pure-app.md), no bespoke
Python needed:
- descriptor: setup (Build Harness fixture, context_key=fixture), deliverable_mode
Callout, serialize_toolchain, confine_by_default, component_noun "instruction",
deliverable_primary fuzz/{program}/src/main.rs; artifact_layout reconciled to the
values CrucibleArtifactStore actually used (certora/crucible metadata).
- crate rendering (crucible_deps / render_cargo_toml / crate_files) absorbs
CrucibleHarness + CrucibleDep — single source of truth, read $CRUCIBLE_REPO.
- workspace_prep: place deps-only manifest + warm fuzz/<program> + build the .so.
- sandbox_grants: crucible checkout + `crucible` bin dir as extra_ro.
- validate_preconditions: $CRUCIBLE_REPO / crates/crucible-fuzzer check.
- compile/validate materialize Cargo.toml per run (no shared-manifest race).
- finalize renders the whole crate from the enriched outcome set (fixture + one
section per delivered invariant, features sorted); host payload gains `program`.
Wheel built + installed; descriptor/callouts smoke-tested to match the old
CrucibleHarness output byte-for-byte.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…host (phase 4)
Crucible is now a pure-Rust app: the whole composer/crucible/ package
(backend/store/harness/pipeline/results/cli) is gone. What replaces it:
- composer/crucible_launch.py — two-line console_crucible/tui_crucible shims over
composer.rustapp.cli (console_main/tui_main "crucible_app"); pyproject repointed.
- Everything the package did is now descriptor-driven in the generic host (phase 2)
+ the crucible_app wheel (phase 3): setup fixture, workspace_prep, crate assembly
(finalize), sandbox grants, verdict summary.
Test migration (all collect; fast ones pass):
- test_crucible_results → composer.rustapp.results (backend_tag param).
- test_crucible_harness → rewritten to pin the wheel's workspace_prep/finalize crate
rendering (the cumulative-feature machinery it guarded is gone — per-run manifests
remove the race).
- test_crucible_events → build_application("crucible_app").
- setup/formalize gates → drop the manifest pre-placement (compile/validate
materialize their own crate now).
- test_crucible_gate phase2 → drive the callout-mode store + wheel finalize.
- test_crucible_e2e_gate → build_application + run_application (mirrors the entry
point: declared fuzz_timeout + launcher policy from the wheel's sandbox_grants).
No stale composer.crucible imports remain; tests/ collects (258) with no errors.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Prose-only: point the e2e/sandbox/phase-2 gate docstrings at the generic host (build_application/run_application, confine_by_default + sandbox_grants, wheel finalize) instead of the deleted run_crucible_pipeline / CrucibleArtifactStore. Verified: the two non-LLM crucible gates pass against a real build (97s, CRUCIBLE_REPO=/home/eric/src/crucible) — descriptor + $CRUCIBLE_REPO precondition, the .so build, and the wheel's finalize-rendered crate compiling + dry-running. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The fuzz budget now travels as a descriptor-declared arg injected into the component context (declared_args -> AuthorInput.context['fuzz_timeout']), so the dedicated fuzz_timeout_s field/param on BackendOptions, RustBackend, RustFormalizer, and build_application was dead. Removed. Backends read the value via the context. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…stinction explicit Audit confirmed the two axes are already cleanly separated in code — the analyzed program's language rides on the ecosystem (Ecosystem.language), and the entry point derives forbidden_read from app.ecosystem.language, never from the fact that the backend is a Rust wheel; no implementation-language notion is attached to the ecosystem or descriptor. echoprover (a Rust-implemented backend analyzing Solidity/EVM) proves the independence. This only tightens the prose so a reader can't conflate them: - Ecosystem.Language docstring + module docstring: state the facet is the language of the *code under analysis*, explicitly not the backend's implementation language. - composer/rustapp docstring: state that "Rust" there is the *backend implementation* language, orthogonal to the ecosystem, and that the host reads the analyzed-source language from app.ecosystem.language rather than assuming it. No behavioral change (docstrings only); pyright clean, imports OK. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…FeatureUnit) The shared core hardcoded ContractComponentInstance as a stand-in for "the unit", so the ecosystem-generic driver had to cast every non-EVM unit to the EVM type — a cast that was actually a lie for Solana (a SolanaInvariantUnit is not a ContractComponentInstance; it only worked because the generic path touches no EVM-specific members). Parametrize BackendJob / ComponentOutcome / _Batch / Formalizer / PreparedSystem / PipelineBackend over `U: FeatureUnit` and let each backend declare its concrete unit: CVL & Foundry → ContractComponentInstance (their finalize now reads .slugified_name / .component cast-free), Rust & null-Solana → FeatureUnit (null's to_artifact_id widened from the too-narrow SolanaInstructionInstance). CorePipelineResult stays mono in the unit (it only reads .display_name). The ecosystem is invariant in its Unit typevar and callers pass a concrete chain, so it can't be tied to the backend's U at the signature; extraction therefore yields FeatureUnit batches and run_pipeline reunites them with the backend's U via one honest widening cast. Net: two clearly-scoped boundary casts (extraction→U, outcomes→FeatureUnit for the rollup) replace the misleading per-unit ContractComponentInstance casts, and the whole core is now honestly typed. pyright clean across all 19 pipeline-type consumers; 246 non-expensive tests pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…_all The two strategies are duals — global extraction infers once over the whole program and fans each property into its own unit (one prop per batch), while per-component infers per unit (concurrently) and keeps that unit's properties grouped — but they shared context-building, inference, and batch construction with the code duplicated across both branches. Factor the shared machinery into `_unit_ctx` (derive a unit's context) and `_extract` (run inference), and reduce both strategies to a list of (unit, properties, context) triples materialized by one shared `_Batch` comprehension. The branch now expresses only the genuine difference (fan direction); no behavior change (per-component still reuses its extraction context — no redundant `.child`; global still builds a fresh per-property context). pyright clean; 246 non-expensive tests pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…up apps` Previously the crucible_app / echoprover PyO3 wheels were installed out-of-band (`maturin develop`), so every `uv sync` pruned them as extraneous and you had to rebuild by hand each time. Declare them as editable path dependencies in a dedicated `apps` group so `uv sync --group apps` builds them via maturin AND preserves them (no more pruning). The group sits outside the default groups, so the container image (final stage has no Rust toolchain; syncs with UV_NO_DEV=1 --group ragbuild) never tries to compile them — verified the image's sync line excludes the apps packages, and `uv lock --check` stays green for its --frozen build. Also add `maturin-import-hook` to the group: after a one-time `python -m maturin_import_hook site install`, editing a crate transparently recompiles it on import (with the venv activated so maturin is on PATH), so the manual `maturin develop` step is gone entirely. docs/crucible-demo.md updated: the "uv sync prunes the wheels" gotcha and the manual rebuild steps are replaced with the --group apps + import-hook flow. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Give the Crucible backend a `judge_prompt` (peer of Foundry's feedback judge),
so an authored test suite is reviewed for *meaningfulness* before it counts —
not just that it compiles. Modeled on Foundry's 8-criteria prompt but retargeted
to LiteSVM fuzzing: the load-bearing axis is reachability (can the fuzzer, via the
fixture's `action_*` methods, drive a state where the invariant could fail?).
SDK:
- `FailureKind` (Compile | Judge) on `Failure`, serde-defaulted to Compile, so a
re-author can tell a build failure from a judge rejection.
crucible-app (the wheel):
- `judge_prompt` for `kind="component"` (skipped for the shared fixture): a
reviewer persona + criteria, emitting the `{accept, feedback}` JSON the host's
`_parse_judge` consumes; a rejection re-authors with the feedback framed as
review notes, NOT compiler errors (`judge_revise_suffix` vs `revise_suffix`,
dispatched on `FailureKind`).
- `judge` event kind so the verdict surfaces in the TUI/console.
adapter (the host):
- tag judge rejections `kind="judge"`; label the judge's LLM turn distinctly
("<app> judge turn", was mislabeled "authoring turn"); emit the verdict.
Two authoring fixes found via the e2e run (solana_vault, real model):
- TEST_CHEAT_SHEET: the real raw-lamports API (`read_account`/`get_account`
return `Result<Account>` — unwrap first; there is NO `get_account_lamports`),
which the model kept mis-guessing and burning re-authors on; plus a
transaction-fee caveat (don't assert an exact lamport delta on a signer/fee
payer — the ~5000-lamport fee makes it a false oracle).
- the judge's Criterion 7 gets the same real-execution-costs principle, to catch
that false-oracle class if the author writes it anyway.
Verified: `test_crucible_e2e_gate` passes with the judge live (13/13 delivered,
judge fired + reasoned per component, reject/re-author path exercised, 0 give-ups);
unit tests in test_crucible_events cover the judge prompt, the setup skip, and the
judge-vs-compile revise framing.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…vability) A refuted property surfaced as a bare `BAD` with no clue why — `validate` classified a `[FUZZ_FINDING]` and discarded Crucible's `summary:<msg>` (the failed `fuzz_assert_*` message with the actual vs expected values). Capture it and make it durable. - SDK: `Verdict.detail` — optional explanation of a non-GOOD outcome. - crucible-app `validate`: `finding_detail()` parses `[FUZZ_FINDING] crash:<id> … summary:<msg>` into the BAD verdict; the ERROR paths carry their error text in `detail` too (and stop overloading `unit_file`, which is a report identity key). - report: thread it through as `Verdict.message` → `RuleVerdict.message`, so it persists in report.json; render it on the rule row (`.finding`) in the HTML. Additive and defaulted to None — prover/foundry are unchanged. - adapter: `fetch_verdicts` maps `detail → message`; the live `verdict` event line appends the detail. Now the `deposit_increases_balance_exactly` BAD from the e2e would read, in report.json and the rendered report, "crash <id>: deposit(...) must decrease depositor lamports by exactly that amount: expected … but got …" instead of a bare BAD. Tests: verdict `detail → report message` threading (test_crucible_events) and the finding message rendering on the row (test_autoprove_report); report suite green (prover/foundry unaffected). Co-Authored-By: Claude Opus 4.8 <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.