summarization_detector: standalone summarization-target detector - #193
Open
jar-ben wants to merge 54 commits into
Open
summarization_detector: standalone summarization-target detector#193jar-ben wants to merge 54 commits into
jar-ben wants to merge 54 commits into
Conversation
* Add AutoProver OIDC role * Add lambda_url
Uses the monitoring feature of Certora/graphcore#24 to add two monitors: 1. A prover monitor, which keeps the state of prover tool calls, and tracks whether the agent is "banging its head" against a set of rules. If so, it uses the new "reminder" channel to emit a "nag", urging the agent to either give up or try something new 2. A budget monitor, which accumulates the total cost of all LLM calls within a given "cost center". If we detect that the task is reaching a budget limit (defined as 80% of the allocated budget) we emit a "wrap it up" message. For verification tasks, we also halt any active feedback agents, and disable all feedback gating (with the idea that it's better to finish under budget with lower quality than blow the budget and return nothing). Budget cancellation is co-operative, if the agent is overbudget/under budget pressure, it throws a special exception which is interpreted as the appropriate "I give up" type (only for the verification tasks). As mentioned, there is a per cost center budget and a total "overall run" budget. The sum of cost center budgets does not necessarily have to be the overall budget, in fact, it is expected to be greater. This was chosen over a strict allocation of the total budget to different centers, with some arcane budget rebalancing for unused costs. As part of this, and as predicted by @shellygr, we have moved the pricing information out of the display subsystem into the `llm/` module. We also more accurately track 1hr vs 5m cache costs, as this matters when computing budget pressure.
Multi spec. Allow multiple spec files to gate the generated code. Adjust internal data structures to match; no CLI entry point exists as the only producer (the assistant) no longer exists.
The instruction to write "a minimal contract which simply extends the target" holds only when the target is deployable. Extending an abstract contract -- or one that leaves part of an inherited interface to a sibling that is mixed in further down the hierarchy -- produces a harness solc rejects, and even if it compiled the Prover would have no instance for it. Judging deployability also cannot be done from the target's own file: the unimplemented functions may be declared in an interface it inherits. Direct the agent to harness the concrete contract the protocol deploys in that case, and to fill in the missing functions itself only when the project has no concrete contract inheriting from the target. Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…osetup migration (#76) * solidity_ast: base node classes + vendored OZ solidity-ast schema Foundation for a full pydantic model of the solc compact AST as dumped by certoraRun --dump_asts. schema/schema.json is the OpenZeppelin solidity-ast 0.4.62 JSON Schema (MIT, see schema/NOTICE); models will be hand-authored and machine-verified against it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * solidity_ast: full typed model set, unions, loader, traversal, conformance tests, fixtures 74 hand-authored pydantic v2 models (Solidity + Yul compact AST), discriminated unions with an UnknownNode fallback per union, single-point forward-ref rebuild, a loader for the 3-level --dump_asts structure (single-parse-per-source, Vyper raw passthrough, per-source degradation), traversal utilities incl. the frozen byte-compatible legacy parent-graph builder, a 151-case schema-conformance suite against the vendored schema, and real .asts.json fixtures generated via certoraRun for solc 0.6.12 / 0.7.6 / 0.8.30. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * solidity_ast: loader/traversal/fixture-parsing tests + parent-graph golden test Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * autosetup: migrate AST consumers to the typed solidity_ast models setup_prover: declared-contracts and inheritance extraction go through a shared _iter_contract_declarations (typed find_all with a raw-scan fallback for sources the models cannot parse); generate_ast_graph delegates to the relocated byte-compatible parent-graph builder. auto_munges: .code detection iterates typed MemberAccess nodes (per-node raw salvage on unparsable sources) and decodes src offsets via parse_src. Parity with the legacy raw algorithms is pinned by tests/solidity_ast/test_consumer_migration.py on the real fixtures. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * solidity_ast: __main__ demo summarizing a dump through the typed models Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * solidity_ast: harden coverage after review — raw sweep, open version enums, cached loads Review findings addressed: iter_nodes_of_type gives typed-first iteration with a raw flat-map sweep for nodes the typed walk cannot reach (e.g. under an unknown future nodeType), used by both migrated consumers so no ContractDefinition or .code MemberAccess can be hidden; InlineAssembly.evmVersion/flags are open strings (a closed fork enum would demote whole files on the next solc release — conformance test carries the allowlisted deviation); .code patches now read and target the source file the offsets refer to (not the compilation unit's main file) and are deduplicated across units; the dump is loaded once per setup run via AstDump.load_cached; union tag sets got a drift-guard test. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * solidity_ast: round-trip fidelity diagnostics + --json validator mode roundtrip_diffs() compares a re-serialized typed tree against the exact source JSON (model_dump with exclude_unset; the internalFunctionIDs de-stamping is the one reversed normalization). Wired into the __main__ validator (with a --json machine mode for corpus sweeps) and pinned on the committed fixtures. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * solidity_ast: typed parsing for solc 0.4/0.5 dumps + legacy fixtures Corpus-driven: real certoraRun fixtures for solc 0.4.26 and 0.5.17 exposed the full legacy dialect, now handled typed (no raw-dict fallback): lenient defaults for fields that did not exist yet (mutability, virtual, tryCall, kind, abstract), string-form documentation and ElementaryTypeNameExpression.typeName, the pre-0.6 InlineAssembly shape (operations text, keyed externalReferences, no Yul AST), file-level EventDefinition (solc >= 0.8.22, missing from the vendored schema), and modeled 0.4-era FunctionDefinition flags. Every deviation from the schema is machine-tracked in the conformance test (LENIENT_REQUIRED / DELIBERATELY_OPEN / FIELD_ALLOWLIST). All five fixtures hold the same strict invariants: fully typed parse, zero unknown nodes, zero unmodeled fields, exact round-trip. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * solidity_ast: VERSION_GATES, virtual=None, derived legacy accessors When the producing solc version is known, a gated field absent at or above its introduction gate fails the source instead of silently reading as None (crash over wrong results); fixtures now always parse with their version so the gates stay exercised. virtual is None below 0.6 (everything was implicitly overridable — False would mislead). effective_mutability/effective_kind derive the pre-gate values faithfully from constant/isConstructor without touching the serialized form. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * solidity_ast: ladder-verified gates + solc 0.7.2 isLValue quirk Empirical solc ladder over every release 0.4.24-0.8.36 pinned the exact gate boundaries: FunctionCall.tryCall from 0.6.0 and InlineAssembly.evmVersion from 0.6.2 (both previously gated later, i.e. under-enforced). solc 0.7.2 alone omits isLValue on enum-member MemberAccess nodes — a bug window, present before and after, so it is lenient (None) rather than gated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * solidity_ast: stream-equivalence tests + streaming __main__ validator Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * solidity_ast: move fixtures + fixture-dependent tests to the Autosetup test repo * solidity_ast: drop inert `from __future__ import annotations` Remove the future import from the modules that have no forward references: base.py and the logic modules (loader, traversal, diagnostics, __main__). requires-python is >=3.12, so PEP 604 `X | None` evaluates natively and these modules gained nothing from postponed annotations. Kept in the six model modules (declarations, expressions, statements, types, yul, unions) where it IS load-bearing — they use unquoted cross-module forward refs (e.g. `value: YulExpression`) that only resolve as strings. 162 pure + 73 fixture tests pass. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * solidity_ast: drop 'from __future__ import annotations' everywhere PEP 563 string-annotation semantics are a dead end (Python 3.14 ships PEP 649 lazy annotations instead), so the future import is a forward-compatibility hazard. Cross-module and not-yet-defined references are explicit string annotations; everything else evaluates natively on the >=3.12 floor. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
The loop in `verify_spec` that decides whether to warn the author "this rule has failed identically 3 runs in a row" carried three defects since it landed: 1. it iterated `stuck_count.keys()` while deleting from it, raising `RuntimeError: dictionary changed size during iteration`; 2. it never decremented `history_ind` on the `run` branch, so it re-counted the *same* prover run instead of walking back through history; 3. `del stuck_count[r]` for previously-nagged rules `KeyError`s when a rule that was nagged earlier is not stuck now. 1 and 2 compound. The tally starts at 1 for the current run, the same run is counted repeatedly, and on the third pass the rule trips the threshold and is deleted mid-iteration — so *any* rule coming back TIMEOUT/ERROR/SANITY_FAILED crashed the whole CVL-generation task on its first occurrence. The detector could never have fired as intended. Lift the loop out of the closure into a module-level `stuck_rule_warnings` (it was already a pure function of the history) and fix all three: iterate a key snapshot, advance the index once per item, `pop(r, None)` for nagged rules. Behaviour is otherwise as originally intended — 3 consecutive identical failures, nag markers restart the streak, rule-scoped re-runs stay transparent to rules they did not exercise. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Compile-check generated harnesses before accepting them The harness generation prompt promises the agent that its harnesses are type-checked on delivery and that compiler errors come back for repair, but the check behind that promise never ran: it was gated on `if False`, because invoking bare `solc` on the harness files cannot resolve a project's remappings, include paths or compiler settings. A harness that does not compile is therefore only discovered by AutoSetup, one phase later, where it is misread as a compilation problem to work around rather than a source error to repair -- and the run dies with everything downstream of it discarded. Check them with the project's own build instead: write the candidates to a scratch directory at the same depth as `certora/harnesses` (so their relative imports resolve identically) and run `forge build --json` on them, which reports diagnostics with a severity field and reuses the artifacts the build phase already produced. Error-severity diagnostics are handed back to the agent against the paths it knows; the scratch directory does not outlive the check. Projects with no foundry build, or a forge that never gets as far as a report, are accepted unchecked as before. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Run the compile check over the agent's filesystem view Building the delivered files in a scratch directory inside the live project checks something subtly different from what the agent produced: the VFS may hold files it wrote but did not deliver -- a shared base contract the harnesses import, say -- and those would be missing from the build, failing harnesses that are in fact correct. It also puts a directory into the project tree for the duration of the check. Materialize the VFS instead and build there. The harnesses keep their `certora/harnesses` paths, so the diagnostics need no rewriting and the scratch directory, its depth-matching requirement and its cleanup all go away. Cost on a 353MB / 12k-file project: ~6.5s to materialize, and forge reuses the copied build cache rather than recompiling the dependency graph. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Run the compile check off the event loop, on a typed report Two review points from @jtoman: The check ran blocking work — the project copy and the forge build — inside the agent's tool call, stalling the event loop for the duration. Move the result tool to `AsyncResultTool` so the validator is a coroutine, materialize through `asyncio.to_thread` (the pattern `materializing_project` already uses for the prover's project copies), and run forge through `asyncio.create_subprocess_exec`. The forge report was read with nested `dict.get` calls. Give it a pydantic schema instead: `ForgeReport.compile_errors` is now the whole of the parsing, and output that isn't a report raises `ValidationError` where the digging used to return None from three separate places. The tool's own schema is unchanged from the model's side — `value` is all it sees, with the state injected — which a test now pins, along with acceptance storing the result and rejection returning the message. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Until now, Cache keys had to be built with loosely defined conventions; this was usually some key construction function (defined as a "private" `_` prefixed module function) that you just kinda had to know was used to define a `CacheKey[Parent, Child]`. This PR addresses that issue by introducing `KeyFamilies`, which declaratively tie the key generation to the expected types. This is done by declaring `KeyFamily(ParentType, ChildType, key_derivation)`. `KeyFamily` defines `__call__(**P)`, where `P` is the signature of `key_derivation`. Thus, you are enforced (by the type system) to pass exactly the parameters needed for each key to each derivation step. This should cut down on the proliferation of imported helper functions all over the place.
Tests surfaced broken completion gating, oops
Both CEX handlers fan their per-rule analyses out under a bare ``asyncio.gather``, so the first analysis to raise propagates out of ``analyze`` and ends the whole run — after the prover has already finished its work. The analyses call an LLM, so any transient API error on a single counterexample is enough to discard every verification result the run had earned. The client already retries 5xx (``max_retries=8`` where ``ChatAnthropic`` is built), so what reaches the gather has survived retry and is not going to clear on its own; the remaining exposure is the blast radius, not the frequency. Gather with ``return_exceptions=True`` in both handlers and drop only the failed rule's contribution: it keeps its prover-assigned status and loses its explanation (or its root causes), while every other rule reports as before and the caller still gets a rendered report. ``CancelledError`` is re-raised rather than logged, so cancellation still unwinds. The trivial handler's ``failed_count`` now counts violated rules rather than analyzed ones, so a failed analysis cannot shift the summarization threshold. Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Monitor state update broke validators (cleared channel via [], not None you dummy). Disable parallel edit tool calling for now, this has killed so many runs :(
* autosetup: express remapping contexts against the run root A remapping's two halves are matched against different things: the target is a filesystem path, while the context is a prefix solc matches against the source unit name of the importing file — i.e. the path as it appears in the conf's `files`, relative to the directory certoraRun runs from. `forge remappings` reports contexts relative to the Foundry project dir, so for a project nested under the run root the context never prefixes the source unit name, no remapping applies, and every import of that sub-project fails to resolve with `ParserError: Source "..." not found ... Searched the following locations: ""`. Re-express the context against the run root, which the three call sites already know. A context is rebased only when it names a real directory under the project dir, which is what distinguishes a project-relative context from one already written against the run root; contexts resolving outside the run root are kept as authored, with a warning. When the build config sits at the run root — every flat project — the rebasing is the identity. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Don't warn when a remapping context is the run root itself That context already covers every source unit name; it is left as authored only because promoting a scoped remapping to a global one could shadow correct global mappings. The warning belongs to the case that genuinely cannot work — a context resolving outside the run root. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Tools "polymorphic" over the nouns they work with. The vast majority of this work happens in graphcore, see that PR.
* wip: initial soroban templates * soroban ecosystem first draft * updates to tests, docs, and ecosystem
Added in a similar manner to the --threat-model flag. It supports being used multiple times, and one can provide either a path to a file or to a directory (in which case all relevant files in that directory will be collected). Also fixed a bunch of missing whitespace/newlines in some prompt snippets.
* PR2: Rust application framework (PyO3)
The generic Rust-wheel host (composer/rustapp) + the rust workspace (autoprover-sdk
ABI/export_app! macro, example-app/echoprover), consuming the command-sandbox seam
already upstream (via the `none` passthrough; SandboxConfig.backend_spec ->
{argv_prefix, timeout_s}). Includes composer/spec/solana/build.py (workspace prep),
the rust prompt templates, and the report-layer support the host needs
(report/{schema,render,collect}.py: the ReportBackend set incl. "crucible", the
per-backend outcome_label vocabulary, and Verdict.message diagnostics).
Cross-cutting intermediate forms (finalized in PR3):
- rust/Cargo.toml: workspace members omit crucible-app (added in PR3).
- pyproject.toml / uv.lock: the `apps` group + [tool.uv.sources] omit crucible_app
(its crate lives in rust/crucible-app, which lands in PR3), so `uv sync`/`uv run`
resolve here; PR3 re-adds it.
- rustapp/adapter.py: RustFormalizer casts the backend tag directly; PR3 restores the
validating as_report_backend.
- rust/.gitignore ignores rust/Cargo.lock; the lockfile is untracked here.
Gate: test_rustapp (echoprover decider round-trip; sandbox passthrough) -- 15 passed.
CI pyright (composer/ analyzer sanity_analyzer certora_autosetup) -- 0 errors.
test_solana_gate lives here (imports composer.rustapp.frontend), not PR1.
Stacked-PR 2 of 3 (off eric/ecosystem); see docs/pr-split-plan.md.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
* rust: stop typing Rust/Solana identifiers as SolidityIdentifier
The identity types split upstream: SourceIdentifier is now the neutral type
the ecosystem seam speaks, with SolidityIdentifier and RustIdentifier as its
per-language subtypes. These two sites predate the split and still claimed
Solidity.
Both typecheck either way, because narrow->wide assignment is legal — a
SolidityIdentifier IS a SourceIdentifier. So the checker cannot catch these;
they have to be retargeted by hand.
- rustapp/entry.py: the generic Rust host parses --main-contract into
SourceFields.contract_name, so it builds the neutral SourceIdentifier. It
is descriptor-driven and not Solana-specific, so it should not claim a
language at all.
- tests/test_solana_gate.py: this one does know its target is a Rust
program, so it builds a RustIdentifier.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rust: build the workspace automatically from `uv sync`
Editing Rust required remembering a manual step (`maturin develop` for the app
wheel, `cargo build -p run-confined --release` for the launcher, plus a one-time
`maturin_import_hook site install`). Make the venv the single source of truth
instead:
* `dev` includes the `apps` group, so a bare `uv sync` builds the Rust
artifacts. The container's UV_NO_DEV=1 still selects none of them, so its
cargo-less final stage is unaffected.
* `[tool.uv] cache-keys` over each project's `.rs` sources (including
cross-crate, so an autoprover-sdk edit invalidates echoprover) — uv rebuilds
on the next `uv run`, and the import hook becomes optional.
* run-confined ships as a maturin `bin` wheel, landing the binary in
`.venv/bin`; `_resolve_binary` also probes the interpreter's scripts dir,
since PATH misses it when the venv is not activated. Linux-only, hence the
`sys_platform` marker.
* rust-toolchain.toml pins the toolchain and lets rustup install it on demand.
It sits at the repo root because rustup resolves by CWD and ignores
`--manifest-path`, and cargo runs both from crate dirs and from the root.
* Track rust/Cargo.lock: this workspace ships artifacts, so the dependency
versions are part of the build.
pyright's job gets `--no-dev` — it would otherwise compile Rust it cannot see
into. pytest's job now does build the crates, so tests/test_rustapp.py stops
silently skipping in CI.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rust: pull the framework changes back from the crucible-app branch
The Crucible work (PR3, `eric/crucible-app`) kept improving the layer beneath
it, so the two branches had drifted: the framework files on `eric/rust` were
stale copies of the same files on `eric/crucible-app`. This lifts the
framework-layer half of that drift down to where it belongs, leaving
`eric/crucible-app` to carry only crucible-specific files.
What comes down, by area:
* **Pipeline driver** — `PipelineBackend.preflight`, run concurrently with
system analysis and joined by `_all_or_none` so either side failing cancels
the other. This is what lets a backend that must *build* something gate the
workspace before the model is spent, instead of surfacing a broken workspace
as unfixable compiler errors in the first authored draft. `prepare_system`
takes the preflight result as its third argument; a setup failure now
surfaces where it happens rather than after extraction.
* **Rust application framework** (`composer/rustapp`, `rust/autoprover-sdk`) —
the abstract component unit mirroring EVM's, the declarative `preflight` /
`idl_dest` / setup-artifact slots on the descriptor, the cached shared setup
artifact, the bounded in-loop review, and IDL-driven type generation for a
wheel that cannot link the program under test.
* **Cargo/Solana capabilities** — `composer/spec/cargo.py` (resolve a program
crate from its source path, not its name) and `composer/spec/solana/build.py`
(fill in an IDL's program id when the project's build omits it; warm the
cargo cache with the same cargo the sbf build uses).
* **Sandbox recipes** — a private per-run `RUSTUP_HOME`, the `PATH`
`cargo-build-sbf` install tree, `~/.gitconfig`, a pinned registry protocol,
and `CARGO_NET_OFFLINE=true` (the spelling every cargo accepts).
* **RAG seam** — `composer/tools/rag_env.py`, which `rustapp/entry.py` already
imports. The corpus modules stay in PR3; an absent one degrades to no RAG,
which is this module's documented contract.
* Docs for the above, plus the report template rendering `Verdict.message`.
Also fixes the demo wheel: `rust/example-app`'s descriptor gains
`preflight: None`. It has not compiled since `preflight` was added to
`AppDescriptor` on the crucible branch — that branch's `uv sync` never built the
crates, so nothing noticed. Here it would break the `test_rustapp` gate the
moment the wheel is rebuilt, so it is fixed in the same commit that brings the
SDK change down.
Verified: `cargo check --workspace` and `uv sync` clean, pyright 0 errors, and
the framework/pipeline/sandbox/solana tests plus the `test_rustapp` gate pass —
422 passed vs 363 on the branch before, with no new failures. `test_solana_gate`
fails here for a pre-existing reason: its `test_scenarios/solana_vault` fixture
lives in PR3.
* pipeline: make the shared-artifact step a type, not a hook
Ported from eric/ecosystem, plus the Rust-side half that branch has no backend for.
`Formalizer.begin` was a defaulted no-op hook that every formalizer inherited and
that the driver called unconditionally. It carried its ordering as a call-order
convention and mutated the formalizer in place, contradicting `Formalizer`'s own
contract ("immutable, fully constructed by prepare_formalization ... never set
post-hoc") — the one thing the rest of the phase chain is built to avoid.
Replace it with `StagedFormalizer`, whose abstract `begin` *returns* the
`Formalizer`. `prepare_formalization` widens to the union of the two, and the
driver picks the arm.
On the Rust side that removes the last post-hoc write to a live formalizer:
`RustFormalizer` no longer takes a `setup_author` and no longer assigns
`_setup_result` / `_context_extra[context_key]` after construction. A wheel that
declares a `setup` step now gets `RustStagedFormalizer`, which authors the shared
artifact and calls the `build` closure `prepare_formalization` handed it; a wheel
that declares none gets its formalizer straight from `build(None)`. Either way the
artifact is in the context blob before any component can read it.
Backends with no shared artifact (prover, foundry, null-Solana) are unchanged:
their narrower `-> Formalizer[...]` return now states that positively instead of
inheriting a no-op.
Also brings over the CLAUDE.md testing notes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rustapp: fix the review's correctness findings
Eight fixes from the review of this branch, plus tests for the two that were
behavioural. Nothing here changes the design — see REVIEW-eric-rust.md for the
typing/abstraction work that is still open.
* results: the console/TUI rollup read `next(iter(verdicts.values()))` on the
strength of "one verdict per delivered unit", but `units()` is one unit per
*property* — so a component with five properties reported one check and hid
the other four. One row per verdict now, named by the property title it
checks (new `RustFormalResult.unit_titles()`), falling back to the unit name.
A delivered component that bakes no verdict still gets an UNKNOWN row.
`report.json` was never affected; it goes through `fetch_verdicts`.
* pipeline: `_all_or_none` left its tasks running when the *caller* was
cancelled — `asyncio.wait` does not touch what it waits on, so a Ctrl-C left
a multi-minute cargo build detached, still writing into the workdir. It now
cancels them and re-raises. A task cancelled by a third party counts as a
failure (and `exception()` is no longer asked of a cancelled task, which
raises).
* sandbox: the per-run RUSTUP_HOME's `toolchains` symlink was tested with
`exists()`, which follows the link — a stale link (shared rustup home moved)
read as absent and `symlink_to` would then raise FileExistsError. Check the
link itself and re-point it.
* pyproject: drop `console-crucible` / `tui-crucible`. They named
`composer.crucible_launch`, which lands in PR3 — an entry point pointing at a
missing module installs happily and fails at ImportError on first use. Same
for null_backend's `:mod:`composer.crucible`` reference.
* rag_env: the tag -> connection map existed twice (here and
`rag/db.KNOWLEDGE_BASES`); take it from `KNOWLEDGE_BASES` and keep only the
tools factory local. Split the two failure modes that were both being
swallowed: an unregistered tag is a wheel bug, so `validate_rag_db` runs at
descriptor load like `resolve_ecosystem` does, while an unavailable DB /
embedding model still degrades to no RAG.
* descriptor: `backend_tag: ReportBackend`. It feeds a closed set, so a wheel
declaring a tag the report cannot render now fails in `model_validate_json`
— before the run spends anything — rather than at formalizer construction.
This caught the demo wheel declaring `backend_tag: "echoprover"`, which no
report knows: any real echoprover run died in `RustFormalizer.__init__`. It
borrows `"prover"` now, as the null Solana backend does.
* adapter: `formalize` grouped its report rows as `(property, [one unit])`
singletons, so two units checking one property became two rows with the same
key and the store's `dict()` kept the last. Group by property as they arrive.
* mark the `docs/crucible-*.md` citations that land in PR3, so a reader stops
looking for files this branch doesn't carry.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rustapp: type the runtime ABI, not just the descriptor
The wheel's *declarative* ABI was already mirrored as pydantic models
(`descriptor.py`); its *runtime* ABI was not. Python received every payload as a
bare dict and destructured it by string key — `result.get("status") != "ok"`,
`res.get("kind") == "build_failed"` then `res["verdicts"]`, `u.get("target") or
u["unit"]`, `plan.get("files")` — while the Rust side had spelled the same things
as tagged unions all along. A field renamed in autoprover-sdk read as `""` three
call frames later instead of failing at the boundary.
New `composer/rustapp/wire.py`, peer of `descriptor.py`:
* Inbound, tagged: `CompileOk | CompileFailed` (discriminator `status`) and
`ValidateBuildFailed | ValidateVerdicts` (discriminator `kind`), so
`isinstance` replaces the string compare and neither variant can be asked for
the other's fields. Plus `Unit` (whose `target_or_unit()` is no longer
reimplemented inline), `Verdict`, `WorkspacePrep`, `SandboxGrants`, `Prompt`.
* Outbound: `AuthorInput` (+ `Property`, `ProgramCrate`), `Failure`/`FailureKind`
(so `{"kind": "judge"}` is a value, not a literal), and `FinalizeInput` —
currently the only written definition of that payload, since the Rust
`finalize` still takes an opaque `serde_json::Value`. Growing an `Outcomes`
struct over there is the follow-up.
* `RustAppModule` Protocol replaces `module: Any` in every signature. Members
are `Callable` fields so `CALLOUTS` derives from the annotations rather than a
hand-kept copy; `load_module` checks all ten at import and names the gaps, so a
wheel built against an older SDK fails at load instead of with an
AttributeError mid-run. The one cast sits at `import_module`, which is where
the dynamism actually is.
`component` and `context` stay dicts on purpose: they are opaque JSON the host
only forwards, so typing them would mean inventing a schema for values it never
reads.
Rust side: `Verdict.outcome` becomes an `Outcome` enum (UPPERCASE serde rename,
so the wire bytes don't change), with `Verdict::detailed()` for the failing case
a backend almost always wants. A typo no longer compiles. Python still tolerates
an unknown label (-> UNKNOWN, logged): version skew should cost one row's wording,
not the component's results.
Fallout worth noting:
* `RustFormalResult.verdicts` is `dict[str, Verdict]`; `fetch_verdicts` and the
console rollup read fields, and `results._parse_outcome` is gone.
* `env: Any` -> `ServiceHost` in the authoring turn, which retired
`getattr(env, "all_tools", None) or env.rag_tools`.
* `_split_prompt` is gone. A wheel that sends no `instruction` now fails at the
seam; it used to have its whole payload JSON-dumped into the agent's prompt.
* `from_formalized` deleted — it parsed a Rust `Formalized`/`Command::Publish`
that no longer exists in the SDK, and only tests called it. `as_report_backend`
deleted too: pydantic validates `backend_tag` now.
* The stub *wheels* in tests still return JSON strings, as real ones do. Only the
host's side of the seam moved.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rustapp: give the phase enum and the TUI's done flag real APIs
Two reach-throughs, one shape: a caller needed something an object owned, so it
took it out of a private field instead of the object growing a way to ask.
The phase enum. `RustBackend._phase: type` / `_core_phases` were dataclass
*fields*, so `host.build_backend` constructed the backend with underscore-named
keywords, and both callers that needed a phase member indexed the field through
`cast(Any, …)` — `RustPreparedSystem` reaching across objects to do it
(`cast(Any, b._phase)[setup.phase_key]`). They are now public `phase:
type[enum.Enum]` / `core_phases: CorePhases` (the property is redundant — a plain
attribute satisfies the protocol, as ProverBackend and the null Solana backend
already show), and the indexing lives behind one accessor:
def task_info(self, spec: StepSpec) -> TaskInfo[enum.Enum]
Annotating the field `type[enum.Enum]` is what let the casts go: pyright resolves
EnumMeta's `__getitem__`, so the member comes back typed. Both call sites were
building a TaskInfo from a (phase_key, label) pair anyway, so that is what the
method returns — and since PreflightSpec and SetupSpec now share a `StepSpec`
base carrying `step: ClassVar[str]` (the step's kind), the task id is derived
from the declaration rather than spelled `f"{name}-setup"` at the call site.
ClassVar keeps `step` off the wire, so the Rust structs don't change.
The TUI flag. `MultiJobApp.mark_pipeline_done()` replaces five external
`app._pipeline_done = True` writes across four entry points plus two inside
`ui/pipeline_app.py`; the flag is now touched only by the class that declares it.
The method's docstring records why it exists at all — quitting is refused until
the run ends, so a keypress can't close the app and take every panel with it
mid-stream — which none of the assignments said.
Both new tests assert the property the reach-through existed to provide: that a
step's task carries the member of *the backend's own* enum, since the frontend
looks up section labels by member identity and a member from another copy of the
enum would land the task in no section at all.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rustapp: the review verdict is two types, not (bool, str)
`(bool, str)` carried three meanings. The string was a revise instruction when
the bool was False and an aside when it was True, and `(True, "")` *also* stood
for "this wheel declares no judge" — so every caller had to know which of the
three it was holding, and `_budgeted`'s relent step returned `(True, rejection
text)`, a verdict that read as an acceptance while carrying the opposite.
Accepted(feedback="") # the gate opens; feedback is an aside
Rejected(feedback=...) # the gate holds; feedback is what to revise
None # no judge for this input — no verdict at all
`_judge_turn` returns `Review | None`, so absence is absence: `author_and_compile`
now re-authors on `isinstance(review, Rejected)`, and both "accepted" and "no
judge" simply fall through. `_budgeted`'s last round produces a real `Accepted`
whose feedback is the unresolved objection — the same behaviour as before, but the
type now says what it does. `_make_judge_hook` narrows `None` away where it cannot
happen (the hook exists only for an input that declared a judge) and says why.
Two `_parse_judge` behaviours were previously implicit in the tuple:
* A rejection with no feedback used to hand the next authoring turn an empty
revise context — a round spent on "you were rejected" with no statement of
what to fix. It now says that no reason was given.
* Prose that leads with neither ACCEPT nor REJECT is taken as an acceptance.
Unchanged, but now stated in the docstring and pinned by a test: the reviewer is
advisory, in front of the compile/validate gates that actually decide, so an
unparseable reply lets the draft through rather than burning a revise round on a
verdict nobody stated. Flipping that is a policy decision — flagged, not taken.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rustapp: optionality instead of sentinels at four seams
Each of these had a value that looked like data but meant "there isn't one", so
every consumer had to know the convention — and one of them silently didn't.
* `cargo._dep_req` returned `""` for "no anchor-lang requirement to compare",
which is what a caller comparing versions least wants to receive. It is
`str | None` now, and `ProgramCrate.anchor` with it; the `""` the Rust struct's
`#[serde(default)]` fields require is produced at the wire boundary
(`wire_crate`) and nowhere else.
* `run_llm_agent` JSON-dumped a missing result, so a turn where the agent never
called the result tool handed back the literal string "null" — which went on to
`compile` as if it were the authored artifact and spent an attempt on a build
nobody could have fixed. It returns `str | None`; both loops treat "no artifact"
as its own failure, costing an attempt but never reaching the toolchain, and the
next prompt is told what actually happened. A judge turn that ends without a
verdict is likewise not a rejection: it fails open, same reasoning as an
unparseable reply.
* `resolve_program_id` / `idl_with_program_id` took the crate as a dict and read
it with `crate.get("dir", ".")` — a Python-to-Python call flattening a typed
value and then papering over its absence by scanning the root as if it were the
crate, matching against a set of empty names. They take `ProgramCrate | None`,
and the fallback is stated once, where it happens. `run_workspace_prep` gets the
resolved crate threaded in rather than reconstructing it from the wire copy,
whose emptiness no longer says whether anything was resolved.
* `RustFormalizer._idl` collapsed "prep placed no IDL" into `""` on the way in;
it keeps `None` and flattens at `finalize`, which is the only place the payload
promises a string.
The fourth bullet of the review's §4 (`context_key if descriptor.setup else
"setup"`, an unreachable fallback inventing a context key) went away with the
typed-ABI commit, which made `build` take the key alongside the artifact.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rustapp: claim the discovery phase by slot, and share one glyph table
Two places where a string was doing a type's job.
The design-doc discovery task's phase was found by looking for a declared phase
whose *key* was literally "discover_design_doc". The descriptor already has a
mechanism for "this declared phase fills that role" — `core_slot` — so a magic
key was a second, undocumented one: a convention a wheel author had to spell
exactly right, with no error if they didn't, and `-> Any` at the end of it.
`CoreSlot` gains `DISCOVERY`, and `CoreSlot.required()` names the four the driver
itself tags and every application must map — so the new slot is optional, and
unclaimed still falls back to the first declared phase. Mirrored in the Rust
`CoreSlot` (additive: existing wheels don't mention it).
The other: two glyph tables with identical contents, one keyed by `Outcome`
(the console rollup) and one by raw strings (the TUI), because the emit payload
carried `"GOOD"`/`"BAD"` as literals. They are now `render.outcome_glyph`, beside
`outcome_label` — the same question, how an outcome reads to a human — and the
tolerant `str -> Outcome | None` is `Outcome.parse`, used by the frontend and by
`wire.Verdict`'s validator instead of each keeping its own known-values set. An
outcome this host doesn't recognize loses its glyph, not its line.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rustapp: one parser, one env builder, no dead hooks
Section 7 of the review: the duplication and dead code.
- build_arg_parser is the only parser. rust_entry_point re-declared the same
nine arguments inline, and the copy had already lost every help string. The
declared-flag dests no longer ride out of _add_declared_args as a return
value either: _arg_dest/_declared_args derive them, so "declared" and
"collected" cannot drift apart.
- build_default_env replaces build_neutral_env plus _default_env_builder's
inner closure, which were the same six lines twice differing in rag_tools=.
rust_entry_point binds rag_db=descriptor.rag_db_default with partial, which
also keeps the corpus lookup lazy. Renamed because "neutral" described only
one of the two behaviours; docs/rust-pure-app.md §5.1 records the landed name
for the proposal it implements.
- Deleted _before_formalize: a no-op hook with no overrider, on a branch whose
thesis is that applications ship no Python. What it documented is now a
comment where it matters, and the "hooks an application backend may override"
banner over _context went with it.
- _run_blocking has one body, guarding on nullcontext() when there is no
semaphore.
- Hoisted the function-local imports that had no reason to be local (io.context,
diagnostics.timing, sandbox.recipes); the spec.solana.build one stays and now
says why the generic host doesn't name a chain at import time.
- RUST_FORBIDDEN_READ is one literal instead of being rebound four lines after
it is defined.
- RustLanguage.source_crate is a method: as a Callable field it advertised an
injection point that source_crate_of's isinstance dispatch makes meaningless.
- AppDescriptor.unit_noun(plural=) owns the component_noun fallback and the
pluralization that cli.py spelled twice; cli.py's helpers take
app: RustApplication.
- store.py: dict comprehension -> dict().
Tests: new test_rustapp_toolchain_sem.py covers _run_blocking (serialize_toolchain
had no coverage at all, so a rewrite of that guard could have gone unnoticed) —
including that four concurrent callouts never overlap and a raising one releases
the permit. test_rustapp.py pins the help text the duplicate parser had lost, the
declared-arg threading, and unit_noun.
pyright 0 errors; 463 passed, 11 deselected with the demo wheel importable.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rag: defer the crucible corpus registration to PR3
crucible_kb was half registered: composer.rag.db.KNOWLEDGE_BASES carried its
connection and rag_env._FACTORIES carried a factory, but the module that factory
imports (composer.tools.crucible_rag) lands in PR3. The tag therefore passed
validate_rag_db — both halves present — and then build_rag_tools caught the
ModuleNotFoundError in its degrade-on-anything path and logged "RAG unavailable",
reporting a repo gap as an environment condition. That is the confusion rag_env's
two failure modes exist to keep apart, and it was reachable: a wheel declaring
crucible_kb would have run with no RAG and a single warning line.
Both registries are empty now, so such a wheel fails at descriptor load with "not
a registered RAG corpus" instead, and PR3 adds the tools module, the _FACTORIES
entry and the KNOWLEDGE_BASES entry in one go. CRUCIBLE_DEFAULT_CONNECTION goes
with them (nothing else read it), as does the comment naming
composer.scripts.rag_import, which does not exist on this branch either. The
error message now says "none is registered yet" rather than "known: []".
The pyproject.toml crucible comments stay: nothing there points at a missing
module (the entry points that did were deleted earlier), so they only explain why
those lists look short.
Tests: new tests/test_rag_env.py — the registry had no coverage at all. Includes
half-registrations (either half) still refusing, which is the shape that slipped
through, and a stub registration that doubles as the spec for what PR3 adds.
pyright 0 errors; 470 passed, 11 deselected.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* pipeline: the preflight gates, the other overlap just awaits
`_all_or_none` gave both of the driver's overlaps one fate, which is more
than either needs.
The preflight is cheap by construction, so there is nothing to save by
cancelling it: await it first, and let its failure cancel the analysis
agent racing it — the direction where the spend actually is. An analysis
failure now waits the preflight out and reports itself.
The second pair (`prepare_formalization` ∥ extraction) goes back to
awaiting each in turn, no cancellation either way.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* sandbox: name the three private scratch dirs once
`.sandbox_cargo` / `.sandbox_rustup` / `.sandbox_tmp` were spelled out in the
recipes that create them, in the forbidden-read regex that has to hide them from
the source tools' file listing, and in a test's assertions. Hoist them to
SANDBOX_{CARGO,RUSTUP,TMP}_DIR next to the functions that create them, and build
the regex branches from those via re.escape (the joined pattern is byte-identical
to the old literal).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rust: defer the analyzed-program build path to the backend that needs it
This branch is the Rust *backend* framework (PR2) on the ecosystem seam (PR1). It
had also accumulated the code for building the program **under analysis** — which
belongs to the backend that does that, not to the framework. A Rust backend need
not build a crate to validate a program, nor depend on the analyzed crate, nor use
the sandbox at all, so none of it can sit in the layer every Rust backend shares.
It moves forward to `eric/crucible-app` (PR3).
What goes, by area:
* **The Solana build capability** — `composer/spec/solana/build.py` in full
(`build_program`, `warm_cargo_cache`, the `Anchor.toml`/`declare_id!` program-id
resolution, the IDL address fill-in), and the warm/build/place-IDL half of
`run_workspace_prep` that drove it.
* **Cargo crate resolution** — `composer/spec/cargo.py`, plus the `RustLanguage`
facet and `source_crate_of` dispatch it was reached through. `ecosystem.py` is
back to what PR1 wrote: `RUST = Language(...)`.
* **Sandbox recipes** — the private per-run `RUSTUP_HOME`, the `PATH`
`cargo-build-sbf` install tree, `~/.gitconfig`, the pinned registry protocol,
`CARGO_NET_OFFLINE=true`, and the `SANDBOX_*` scratch-dir constants.
`composer/sandbox/recipes.py` is byte-identical to master again.
* **The confined-build exclusions** in `RUST_FORBIDDEN_READ` (`.sandbox_cargo` /
`.sandbox_rustup` / `.sandbox_tmp` / nested `target/`). PR1 had already deferred
these to "the layer that introduces confined Rust builds" and PR2 took delivery;
the premise was wrong, and the NOTE now names the *backend* instead.
* **Crucible's report vocabulary** — the `"crucible"` outcome/group labels and
`ReportTerms`, and its member of the closed `ReportBackend` set.
Two seams replace the imports, both in `composer/rustapp/toolchain.py`, both empty
here and registered per chain by the application that needs them:
* `WORKSPACE_TOOLCHAINS` — executes the toolchain half of a `workspace_prep` plan.
The host still writes the plan's `files` (ecosystem-neutral) and reports the IDL
path back as the `idl` context key; it just no longer knows what a build is. It
takes the analyzed `SourceFields` rather than a resolved crate, so the framework
holds no Cargo shape. **Unregistered raises** — a plan that only places files
never asks, so reaching it means the wheel asked for a build nothing can perform,
and skipping it would resurface as a compile error the authoring agent can't fix.
* `SOURCE_CRATES` — resolves `AuthorInput.program_crate`. **Unregistered degrades**
to an all-empty `ProgramCrate`: that is already what Solidity and an unreadable
layout yield, and the SDK's `ProgramCrate::resolved` fills it from the wheel's own
convention, so "no resolver" and "nothing to resolve" are honestly the same answer.
The wheel ABI is untouched (`WorkspacePrep`, `ProgramCrate`, `AuthorInput`, the
`Sandbox` argv prefix), so PR3 re-adds no interface — only implementations.
The null Solana backend was reporting under `backend_tag="crucible"`, borrowing a
real verifier's wording for an all-UNKNOWN report. The closed `ReportBackend` set
gains **`"none"`** for it — a pipeline that records properties without verifying
them — whose `UNKNOWN` reads "Unverified" rather than "Unknown". Three framework
test fixtures that named their fake wheel `"crucible"` are now `"demoprover"`, and
the verdict-rollup / report tests assert a generic backend's words.
Generic mechanism that pointedly stays: `Verdict.message` and its rendering,
`Outcome.parse`, `outcome_label`/`outcome_glyph`, and the `argv_prefix` confinement
seam a wheel may or may not use.
Verified: `pytest -m "not expensive"` 439 passed / 11 deselected, `pyright` 0
errors. The forward half is a patch verified both ways against this tree: applied,
476 passed / 0 errors; reverse-applied, back to exactly this state.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rust: catch the framework up to master's post-merge APIs
The ecosystem PR (#96) landed on master, so this branch rebases onto master
directly instead of onto `eric/ecosystem`. Master moved three APIs underneath
the Rust framework in the meantime; this is the reconciliation.
* **The source-tool read filter is a predicate** (#120, plus the graphcore
`vfs-forbidden-predicates` bump the rebase brings in). `FS_FORBIDDEN_READ`
is gone; `build_default_env` takes `GlobalExcludeArg` — the `str |
Callable[[PurePath], bool]` union `Language.default_forbidden_read` already
declares — and defaults to `fs_forbidden_read`. `RUST_FORBIDDEN_READ` stays
a pattern: nothing in the Cargo layout needs carving back out of an excluded
directory, which is the case the predicate exists for.
* **`TieredProviders.provider_kind` is now `provider_service`.** Same rename
`composer/pipeline/cli.py` carries for the built-in entry points.
* **`llm_factory` is gone from `composer.workflow.services`** — an unused
import here and in `test_solana_gate.py`, so both just drop it.
* `InMemoryTextFile` takes a `ContentRenderer`, not a `provider` string.
Verified: pyright 0 errors, 573 passed / 11 deselected. (`hypothesis` was
missing from the local venv, not from `pyproject.toml`'s test group — a local
gap, present on master too, not something this branch introduces.)
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* pipeline: give the backends a nominal base class
`PipelineBackend` was a structural `Protocol`, so a backend's eight type
arguments were never written anywhere a checker could see them — each one
restated them in a docstring instead, and both had drifted: the null Solana
backend listed 7 of the 8 (no `Pre`), and `ProverBackend` claimed
`A = ComponentSpec` when its store is keyed by `ComponentSpec | InvariantSpec`.
Conformance was only checked where a backend reached `run_pipeline`, and a
renamed member would have silently stopped matching there rather than at the
definition.
It is now an `ABC` with the three methods abstract, and each backend names its
type arguments in its `class` line.
The four non-method members stay read-only properties — the shape the Protocol
already declared — because that is what nominal inheritance allows: a mutable
attribute override is invariant, which would reject `ProverBackend` narrowing
its store to `ProverArtifactStore` (its prepared system needs
`write_component_runs`) and `RustBackend` deriving its guidance from the wheel's
descriptor. Declaring them as attributes instead rejects the derived properties;
declaring them as properties breaks any same-named dataclass field at runtime,
since the generated `__init__` assigns through a setter-less property. So each
backend holds its store in a field and returns it from the accessor.
The driver's signature is unchanged, so `run_pipeline`, `cli.Continuation`, and
both entry points needed no edits; the partial backend stubs in the pipeline
tests still duck-type, as the driver never does an `isinstance`.
One trade: pyright cannot flag a subclass that omits an abstract property (an
inherited declaration counts as declared), so that mistake now surfaces as a
`TypeError` at construction rather than at the call site.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rag: move the generic JSON manifest importer down to the framework
The manifest format and its importer arrived with the Crucible application, but
nothing in either is Crucible's: `import_format.py` is a pydantic schema with no
RAG-stack imports at all, and `rag_import.py` reads any manifest and drives the
shared `BlockBuilder` + the dual-path DB ingestion. They belong with the
descriptor-driven RAG seam (`composer/tools/rag_env.py`, `KNOWLEDGE_BASES`) that
already lives here, so an application contributes a corpus as data rather than as
composer-resident Python.
This also settles two dangling references on this branch: `docs/rust-backend-api.md`
already pointed at `composer.scripts.rag_import` as the mechanism a wheel's corpus
arrives through, and the comment naming it in `composer/rag/db.py` had to be dropped
when the crucible registration was deferred. Both are accurate again. `KNOWLEDGE_BASES`
stays empty and `rag_env._FACTORIES` is untouched — the mechanism ships corpus-free,
and both halves of the first corpus still land with the application that declares it.
`docs/rag-import-format.md` comes along, rewritten where it assumed the Crucible app
was present: §4's registry example is empty rather than seeded, §7 lists what the
mechanism ships instead of what Crucible did with it, and the links into
`rust/crucible-app/` are gone. Crucible remains named as the first adopter, with its
own corpus documented on its own branch.
Tests: new tests/test_rag_import.py — the importer had no coverage. Pins both indexes
being fed, `part` numbering across sections and across manifests sharing a DB (the
`(headers, part)` unique key spans both), per-section code-ref tagging, the long-section
split, and the version / unresolvable-target refusals. It needs spaCy transitively via
`text_processors`, so it `importorskip`s like `test_rustapp` does for its wheel.
pyright 0 errors; 583 passed, 11 deselected.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* docs: consolidate the Rust seam into one as-built doc, and reconcile the rest
The five rust-* design notes were written as successive proposals, each
superseding the last: the IoC decider loop, the passive-service API that
replaced it, the pure-app seams that made Crucible descriptor-driven, and the
PyO3 tier survey behind all of it. What shipped is the union of the last three,
so four of the five documented code that no longer exists — `RustSession`,
`resume`, `Command`/`Observation`, `Effects`, `drive_session` — alongside a
`composer/crucible/` package and a `rust/crucible-app` crate that are no longer
in this tree at all.
Replace them with one reference for the seam as built: the ten callouts, the
descriptor, the run end to end (preflight ∥ analysis, the staged setup artifact,
the fused author→validate loop), the in-loop judge, target-shared verdicts, the
two chain seams, confinement, and what a new application actually writes. Only
current design; the proposals, tier surveys and work breakdowns are dropped.
Section numbers are stable so code comments can cite them, and every inbound
reference is repointed.
The three docs that survive on this branch had drifted against the same
refactors, so correct them too rather than leave them contradicting the new one:
- application-abstraction: the per-app `run_*_pipeline` wrapper it documents is
gone — both apps now go through the shared `cli_pipeline` and its
continuation, the ecosystem is an explicit driver argument, and both phase
enums grew a discovery phase.
- formalization-abstraction: `Formalizer`/`PreparedSystem`/`ComponentOutcome`
are all generic over the unit type, the driver's data types live in ptypes,
and `StagedFormalizer` — half of what `prepare_formalization` may return —
was missing entirely. Line-number citations had drifted; replace them with
symbol names so they can't drift again.
- command-sandbox: the mechanism is accurate, every consumer reference was not
(`RealEffects`, `warm_cargo_cache`, `build_program`, the Crucible store and
repo resolution), and it linked to a doc and two gate tests that aren't here.
Also fix two code comments that repeated a doc claim shown to be false: header
paths are neither left-packed nor truncated (`_normalize_head` maps position to
column and raises past six), and `run_local_command` no longer backs a
`RunCommand` effect.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* comments: describe the code as it is, not how it got here
A pass over the commentary this branch added, against the rule that a comment
should carry intent, constraints, trade-offs, warnings or domain context — and
that change rationale belongs in a commit message rather than in the source.
Three things came out of it.
Most of the edits are the same shape: commentary that narrated the change
instead of the code. "was the Rust sessions' SETUP/PC_MAX_ATTEMPTS", "it used to
be JSON-dumped, which handed the caller the literal string \"null\"", "the same
routing the old RealEffects.emit used", "fully expresses what Crucible used to
need a subclass for", "replacing the old per-app build_crucible_env", and the
nine test files carrying the same shape. Each is now a present-tense statement
of the invariant, which is what a reader needs and what stays true.
Two comments were also simply wrong. The example app claimed ReportBackend was
`prover | foundry | crucible` and that the null Solana backend borrows a tag —
the set is `prover | foundry | none` and that backend uses "none". And
push_custom_update named "the Rust IoC loop" as its caller, which this branch's
own SDK docs say does not exist; it is the author->compile->validate loop.
The rest is editorializing that argued for the design rather than describing it:
the Review type's case against the (bool, str) it isn't, the annotation NOTE
that litigated the repo's `from __future__` policy (kept as a warning about the
runtime introspection that actually constrains it), and program_crate_of's
parameter-shape justification.
Left alone: MAX_REVIEW_ROUNDS and _parse_judge's fail-open note. Both are long,
but both warn about behaviour the code cannot express — an unwinnable review
loop, and an advisory gate that deliberately passes what it can't parse.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* ci: install the pinned Rust toolchain before uv builds the crates
`dev` includes `apps`, so CI's `uv sync --group test --extra prover` now builds
`rust/example-app` and `rust/run-confined`. uv builds path deps concurrently and
rustup's install path is not concurrency-safe: whichever maturin -> cargo call
finishes first clears $RUSTUP_HOME/downloads, and the other dies renaming its
half-downloaded component. Deterministic on a runner, invisible locally, where
the toolchain is already installed:
error: component download failed for clippy-x86_64-unknown-linux-gnu:
could not rename 'downloaded' file from '.../<hash>.partial' to
'.../<hash>': No such file or directory (os error 2)
pytest's job wants those wheels — without them tests/test_rustapp.py and the
launcher suites skip themselves — so install the toolchain in a step of its own
first and let the concurrent builds find it present. Cargo's own locking handles
the rest. `rustup toolchain install` with no argument reads the channel, profile
and components from rust-toolchain.toml, so the pin stays in one place. The
cargo/target cache keeps each PR from recompiling pyo3 from scratch.
The nightly integration job would have broken the same way, and nothing under
`expensive` or `fuzz` touches the Rust artifacts, so it gets `--no-dev` instead —
on the `uv run` calls too, since a bare `uv run` re-syncs with the default groups
and pulls `apps` back in.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* build: declare a setuptools floor the package-data globs actually need
`requires` said `setuptools>=61.0`, which is lower than either real
constraint. The `templates/**/*.j2` package-data entry needs 62.3+ — the
release where package-data globs gained `recursive=True`. Verified by
bisecting the wheels: 62.2 and earlier expand them with a bare
`map(glob, patterns)`, where `**` collapses to a single `*`, so the entry
would match only the subdirectory templates and drop all ~92 top-level ones
without any error.
That floor turns out not to be the binding one. Every setuptools below 67.0
imports `pkgutil.ImpImporter` via `pkg_resources`, which 3.12 removed, so
none of them run on the `requires-python = ">=3.12"` this project declares —
the silent-drop build was unreachable in practice rather than latent. 67.0 is
the lowest release that both runs on 3.12 and globs recursively, confirmed by
building a fixture wheel against it and checking a top-level template, a
subdirectory template and `prism-cvl.js` all ship.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* sdk: split lib.rs into modules along its existing seams
The crate was one 1000-line file whose section banners already marked the
seams; this turns each into a module. Items move verbatim and lib.rs
re-exports every one of them, so the public API and the `$crate::…` paths
`export_app!` expands to are unchanged.
SandboxGrants moves next to WorkspacePrep rather than into sandbox.rs:
both are pure declarations the host acts on, while sandbox.rs is the half
that spawns a process.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* sdk: give the three JSON-blob callouts typed payloads
`finalize`, `validate_preconditions` and `sandbox_grants` each took a
`serde_json::Value` the backend hand-dug with string keys. The shapes were
real contracts — wire.py even noted its `FinalizeInput` was "the only written
definition" of one — so this writes them down in Rust:
* `FinalizeInput` / `FinalizeComponent`, mirroring the model the host already
sends. `delivered: bool` beside always-present fields becomes
`ComponentOutcome::{Delivered, GaveUp}`: a component that gave up has no
spec, no targets and no rows, so there is nothing to read past its name.
* `AppArgs` for the two argument-shaped callouts. `program` and `source_path`
are split from `path:Name` by the host, so no wheel re-splits it, and the
grants call now gets the same payload the precondition check does (it was
missing `program_crate` entirely).
`ProgramCrate` is resolved at the FFI boundary, so the partly-empty shape a
host that resolved nothing sends never reaches a callout. It was previously
each backend's job to remember `resolved()` — crucible calls it in five
places, and any one of them could have been forgotten.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* sdk: make AuthorInput's kind a variant that carries its own payload
`kind: String` was a discriminator the SDK documented as a closed set of
three, and every backend branched on it with string compares. Worse, it
silently changed what the neighbouring fields meant: `component` was the
analyzed model on a setup turn, the unit on a component turn, and nothing on
a preflight. It is now `Authored::{Preflight, Setup{model}, Component{unit}}`
— flattened, so the wire shape is unchanged — and neither turn can be asked
for the other's payload.
The `context` blob goes with it. Two of its keys were pure indirection
between the SDK and itself:
* `SetupSpec.context_key` — the wheel declared the key, the host echoed the
artifact back under it, and the wheel read its own string. It is now
`AuthorInput.setup`, and the field is gone from the descriptor.
* the `idl` key, whose presence meant "the file is in place" — now
`AuthorInput.idl: Option<String>`, which says that in the type.
What remains (the wheel's own declared flags) becomes `AuthorInput.args`,
the same values `AppArgs.declared` carries, read through `DeclaredArgs::get`
instead of each wheel writing its own `ctx_str`/`ctx_u64` accessors.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* sdk: hand validate the target it runs, with the rows that target covers
The trait said `unit: &str` and "check ONE unit"; the host has always passed
a *target*, which several report rows can share. So the parameter was
misnamed, and a backend's first move was to recover what the host already
knew — crucible re-derives `self.units(input)` and filters it by name.
`validate` now takes a `Target { name, units }`. `Target::all` and
`Target::verdicts` build the outcome from it, so the unit names a verdict is
keyed by come from the units the host sent rather than being spelled again
by each backend.
Adds the first test to drive the validate seam at all: one run per distinct
target, each carrying exactly its rows, and every covered row's verdict
reaching the result.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* sdk: fold the step declarations into the phase that groups them
`PreflightSpec`/`SetupSpec` were `{phase_key, label}` structs pointing at a
declared phase by string key and repeating its label — crucible writes
"preflight"/"Build Preflight" twice and "harness_fixture"/"Harness Fixture"
twice — with nothing validating that the key names a real phase (a typo was
a KeyError mid-run). `PhaseSpec.core_slot` already did this job properly for
the four driver phases, so it widens to a `role` covering all of them:
grouping (the default), the four core, discovery, preflight, setup.
A role no phase claims is a step the application doesn't have, which is what
`AppDescriptor::step(role)` returns None for. Two structs and a cross-
reference by string key go away, and a step can no longer name a phase that
does not exist.
`ArtifactLayout.deliverable_primary` — documented as "ignored PerComponent" —
moves onto `DeliverableMode::Callout`, the only mode it means anything under.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* sdk: bundle the workdir with its sandbox, and close two open sets
`compile`/`validate` took `workdir` and `sandbox` as a loose pair that every
call then handed straight back to `run_confined` — so they become one
`Workspace { dir, sandbox }` with a `run` method, and the "call this from
inside allow_threads" contract is structural rather than a doc note. `run`
also takes any `IntoIterator<Item: AsRef<OsStr>>`, which drops the
`vec!["run".to_string(), …]` ceremony from every call site.
`Property.sort` was a free string documented as a closed set of three, next
to `Outcome`, which is an enum for exactly that reason. It is now
`PropertyKind`, mirroring the host's shared `PropertyType`.
`Verdict::with_detail` covers the case a backend actually has — an
`Option<String>` parsed out of tool output — instead of forcing a mutable
struct update between two constructors.
`EventKind`'s doc pointed at a `Command::Emit` that no longer exists on the
Rust side. It now says who really emits: the host, around the callouts it
drives. A wheel has no emit channel at all, so a declared kind nothing emits
renders nothing (crucible declares two such kinds today).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* sdk: address types through the module that owns them
The crate root re-exported all ~30 items, so every type had two paths and
the modules were just filing, not namespace. Only two things stay at the
root: `Backend` (what every app names, and `backend` holds nothing else)
and the `pyo3` re-export the macro needs.
With the module as the namespace, the `ffi_` prefix was stutter, so those
ten helpers become `ffi::descriptor`, `ffi::compile` and so on. The macro
expansion is the only caller, so no wheel spells them either way.
The example app now imports per module, which is the shape a real backend
gets: authoring / descriptor / outcome / sandbox, one line each.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* sandbox: spell CARGO_NET_OFFLINE the only way cargo accepts
The offline half of the build sandbox did not work. Cargo parses this env
var as a config boolean and takes `true`/`false` only, so `=1` fails the
build with
error in environment variable `CARGO_NET_OFFLINE`:
provided string was not `true` or `false`
and — the part that matters — it fails that way *from the network path*,
having already tried to update the registry. A truthy-looking value was
worse here than no value at all: it neither forced offline nor left a
working online build.
Found while reconciling the docs with eric/crucible-app, which had already
changed the value in code but kept the `=1` wording in the docstring beside
it. The docstring and the doc now say why the spelling is load-bearing, so
nobody "simplifies" it back.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* pipeline: back to a protocol, with the members stated plainly
Review asked for `PipelineBackend` to be a `Protocol` again, as on master. Only
the base class changes: the four backends keep it in their `class` line, since
an explicit subclass of a protocol type-checks the same way and is still where
their eight type arguments are written down and tied to each other. The stubs in
the pipeline tests go back to conforming by shape alone.
This also recovers what 0119ba9 traded away — pyright reports a backend that
omits a member (`"PipelineBackend.artifact_store" is not implemented`) where the
ABC could only raise a `TypeError` at construction, because an inherited
abstract property counts as declared.
Review also asked for the members back in their pre-PR form, so the three
run-constants are plain attributes again: each backend states them as class-level
constants, and `RustBackend`'s `phase_map` field simply becomes `core_phases` —
the field is the member, with no accessor in between. Its two descriptor-derived
members are `field(init=False)` filled in `__post_init__`, a property being no
longer a legal override of an attribute member.
`artifact_store` stays a read-only property, as the one member a backend narrows:
`ProverBackend`'s store is a `ProverArtifactStore`, which `ProverPrepared` needs
for `write_component_runs`, and a mutable attribute is invariant. The
alternatives don't hold — `frozen=True` and `Final[...]` on the override are both
still rejected, and a dataclass field overriding a read-only property breaks at
runtime, the generated `__init__` assigning through the inherited descriptor.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* wire: check the mirrors, then stop letting them drift quietly
The Rust/Python seam is two hand-written mirrors — pydantic models in
composer/rustapp/{wire,descriptor}.py, serde types in rust/autoprover-sdk —
kept in step by a docstring asking for it. This replaces the asking with a
check, and then removes the tolerance that was hiding what the check finds.
The harness (tests/test_wire_roundtrip.py) round-trips every payload root
through the other language and back, under Hypothesis. The inbound generator
deliberately lives in Rust (autoprover_sdk::fuzz, behind a `fuzz` feature,
driven by the wire-echo bin over a pipe) rather than being derived from the
pydantic schema: a generator built from the host's own models cannot produce
a field only the Rust side declares, which is exactly the drift that matters
for an outbound payload. Hypothesis supplies the entropy as bytes for both
directions, so shrinking still works and there is no second RNG protocol.
Strictness. Both halves ship together, so a missing field is never version
skew — it is a mirror that drifted, and defaulting it turns a caught bug into
a silent one. The rule is now: the side that deserializes requires
everything. Rust gets deny_unknown_fields and no #[serde(default)]; the
inbound pydantic models get extra="forbid" and no defaults. Nothing carries
skip_serializing_if any more, so an empty optional has one spelling (null,
always present) rather than two that both sides must agree to treat alike.
That closed two blind spots a round trip structurally cannot see — a field
only one side declares, defaulted by the other — which now fail at the
callout naming the field instead of reading as ""/None/[] forever. The two
field-set checks kept beside the round trips no longer cover a gap; they
localize one, reporting the diverged field rather than a serde error inside a
shrunk example.
Worth knowing before adding a field: #[serde(default)] on an Option<T> does
nothing (serde defaults those regardless), so 17 of them were advertising a
compatibility decision nobody made. Requiring such a field needs
crate::required::present via deserialize_with, which serde cannot satisfy
from an absent key.
Drift the harness found on the way:
* ArgDefault was one model with `kind` beside a shared
`str | int | bool | None`, against a per-variant Rust enum — so
{"kind":"bool","value":null} was constructible here and unparseable
there. Now a discriminated union, which also drops the type narrowing at
its one consumer.
* BackendSpec.timeout_s was a bare `int` against a Rust u64, a domain
mismatch nothing enforced. Now bounded below.
* SandboxGrants.extra_env was documented as NAME=VALUE pairs; the host
feeds it to env_passthrough, which takes bare names. Doc fixed — and this
one is the reminder that a fuzzer over two `list[str]` fields sees
nothing.
Removed the unknown-outcome validator: its rationale was skew, and with none
possible an unrecognized label can only mean a variant added to one Outcome
and not the other, which UNKNOWN would hide behind a merely-inconclusive row.
Test fixtures hand-writing partial payloads no longer parse, which is the
point; conftest gains builders so a test exercising one descriptor field
needn't spell all fifteen. Six tests in test_rustapp_wire.py asserted the
removed tolerance and are inverted. An ABI change now means rebuilding the
example-app wheel in the same commit.
The root lists stay declared — a wire name and a direction are not properties
of a class — so two completeness checks discover what the ABI defines and
require the lists to account for it. The second caught a gap in this commit:
Unit is nested in the outbound Target, and since the field-set check compares
only a struct's own top level, dropping it from MIRRORS lost that coverage.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* seam: the analyzed project's build system is the chain's business
`idl` had leaked across the generic host, but it was the smallest of four leaks.
`ProgramCrate {dir, package, lib, anchor}` is Cargo plus Anchor; `warm_dirs` and
`build_program` are a Cargo cache and a lib target; and `ProgramCrate::resolved`
/ `anchor_compat_key` put the Anchor workspace layout and Cargo's 0.x-is-a-major
semver rule inside the SDK itself. rustapp is Rust because that is how a wheel is
written, not because of what it analyzes — a wheel analyzing Move has no crates,
no `cargo fetch` and no `programs/<name>` convention, and under the old shape it
could not have used this seam without an edit to the framework.
So everything project-shaped now crosses the seam opaquely, as `chain::ChainData`
— a JSON object and nothing more:
* `source_unit` replaces `ProgramCrate`.
* `WorkspacePrep {files, toolchain_request}` replaces its three Cargo fields.
* `prep_facts` replaces `idl`.
These are typed at both *ends* and nowhere in between: the chain's registered
implementation and the wheels targeting that chain share the types through the
chain's own support crate, and which type is inside follows from the declared
`ecosystem` rather than from inspecting keys. It is the treatment `model` and
`unit` already got, for the reason they got it.
Two structural consequences. The two parallel registries fold into one
`ProjectToolchain` per chain — both questions are the same knowledge, so adding
an ecosystem is now one registration — and `RustPreflight`'s two fields become
`ProjectFacts`, carried whole instead of threaded as two kwargs, which is also
what `_setup_identity` hashes.
The Anchor policy simply leaves the SDK here. Its new home is the chain's own
support crate, where the Cargo vocabulary belongs and is shared by every wheel
targeting the chain — that crate arrives with the PR that registers the chain,
since nothing in this one has a chain to register. The FFI boundary stops
normalizing anything, so an unresolved project reaches a backend empty and the
wheel applies its own convention.
Also fixes three SDK tests broken by the strict-deserialization change, and a
fourth that was passing vacuously: its parse failed, so the spy it asserted on
recorded nothing.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* authoring: one home for the loop CVL and foundry were each keeping
The CVL author and the foundry author had grown the same workflow twice: a
buffer, a skip list, a digest of both that gate tools stamp, a publish gate that
refuses a stale stamp, and a judge sub-agent with an enforced read-back. The two
copies had already started leaning on each other — foundry/state.py imported
cvl_generation's private _merge_skips — and a third copy is due for the Rust
backend, which is the point at which two copies stops being tolerable.
composer/authoring/ is that workflow with the backend-specific parts as
parameters: what makes a spec valid at write time, what the publish-time mapping
is checked against (forge names every test it ran; the prover names nothing), and
the wording each backend uses for its own units. The per-backend assembly — which
tools, which prompts, which cache — stays where it was.
Nothing the model sees moved. Tool names, descriptions and argument schemas were
diffed against HEAD; the only differences are give_up's description, which loses
an indent because it now comes from the same cleaned docstring its schema always
used, and put_test_raw's, which stops naming a state key that no longer exists.
foundry's judge prompt is declared as a TypedTemplate now, which brings it under
the template fuzzer and exposed that it never passed `sort`. Harmless in
production — jinja's default undefined makes the two `== "update"` guards false —
but fatal under COMPOSER_STRICT_TEMPLATES. It is passed "existing" now, which is
what foundry always is, and renders identically.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* rust: author in a session, and call a check a check
The Rust backend ran a Python retry loop around a stateless author: seven fresh
graphs, each remembering its predecessor only through the failing draft echoed
back in the prompt. The two Python backends run something else entirely — one
stateful agent that owns a buffer, calls its checker as a tool, and publishes
only what every gate has stamped. Every gap the reviewers listed follows from
that difference, so the loop is replaced rather than extended: composer/rustapp/
session.py assembles the shared workflow for a wheel, and adapter.py goes from
1205 lines to 700.
The seam moves with it. `Failure` and its `kind` are gone — build errors and
review feedback are tool results in a session that remembers, so there is no
revise prompt to render. `author_prompt` is asked once and supplies only the
*domain* half of the system prompt; the host owns the protocol half, because a
wheel that spelled the tool contract itself could drift from what the host
actually enforces. New: `check_syntax` to reject a draft at write time,
`skipped` on `Delivered`, and two declarations that let a wheel speak its own
language — `evidence_kinds` for what an author may cite against the judge, and
`check_noun` for what it calls a check.
Three behaviours change deliberately, all in code that has never shipped. A
counterexample now blocks publishing until it is fixed, marked with a reason, or
given up on — the CVL/foundry semantics, which is what turns a `BAD` row into a
finding somebody reasoned about. The judge returns a structured verdict, so
there is no unparseable reply to fail open on. The review budget goes with the
loop it bounded: the recursion limit and `give_up` bound the session instead.
And the thing a property's verification is called is now one word. It had four
— `Unit` on the ABI, `UnitName`/`property_units()` in the pipeline protocol,
`RuleName` in the report, `rules`/`tests` per backend — with "unit" also meaning
the component system analysis produced. A check yields a verdict; that pairing
explains itself where `Unit -> Verdict` did not. Each backend still says "rule"
or "test" to its own model, via MappingVocab. The report schema keeps its
vocabulary: those field names are in report.json, which the standalone renderer
reads back.
One trap found on the way, and documented: `@tool_display` rebinds as_tool/bind
closed over the class it decorates, so a subclass of a decorated schema silently
serves the base's fields. The rebuttal tool was already losing its declared
evidence kinds that way.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* docs: the authoring session belongs to the seam, not to one backend
formalization-abstraction.md described CVL's authoring loop as a CVL thing, and
rust-applications.md described the Rust one as a Rust thing. They are the same
workflow now, so it is documented once (§4.3.1) where the seam it belongs to is
already explained, and the Rust doc keeps only what is genuinely Rust-specific.
The new section says what the session *is* — one buffer, gates that stamp a
digest rather than return, a judge that must state a structured verdict, two
honest exits, a publish gate that checks the mapping against ground truth — and
which parts a backend supplies, including its own noun for a check. It also
records the one deliberate holdout: the report still says "rule" because those
are field names in report.json, which the standalone renderer reads back.
rust-authoring-parity.md is deleted. It argued for a change against code that
never shipped outside this branch; keeping it would leave the repo explaining a
delta no reader can see. Everything from it that outlives the argument has a
home above.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* docs: finish the rename in the prose that outran it
Five references in formalization-abstraction.md, two in rust-applications.md and
one SDK doc comment still named `property_units`. The check that was supposed to
catch this …
Allows plugins to contribute tools to the formalizers of individual backends. This accomplished in two places. First, the *formalizers* (not the backend) declares a `tool_provider_type` field. This field names a particular subclass of `PipelinePlugin` which provide tools for the formalizer to use. This information is used by the pipeline to construct a formalization cache key that includes the plugins that contributed to that formalization. The actual binding of tools is accomplished by pushing a `ToolBinder` object through to the formalizer. The `ToolBinder` takes `ToolExtension` type and the "injected parameters" and returns a sequence of `ProvidedTools`. Each `ProvidedTools` object encapsulates the Langchain tools that may be bound directly on the graph plus the system prompt blurb describing to the agent how to use said tool. ## Tool Discovery Details The ToolBinder type is a polymorphic function with (roughly) the following signature: ``` (ToolExtension[TP, U, P], **P) -> Sequence[ProvidedTool] ``` where `U` is the usual `FeatureUnit` bound type parameter for the backend. `**P` is a param spec type parameter; it defines the protocol for how the formalizer communicates with its plugins in a way that is opaque to the pipeline core. `ToolExtension` itself is defined as a class with two fields: ``` provider: type[TP] project: (TP) -> ((U, list[PropertyFormulation], PluginToolContext, **P) -> Sequence[ProvidedTools]) ``` `project` takes an instance of `TP` (the tool provider) and projects out a member function which takes, as arguments: the feature unit being formalized (represented by `U`), the list of properties being formalized, the "plugin tool context" (see below), and "whatever arguments are represented by P". The fixed argument prefix (`U`, `list[PropertyFormulation]`, and `PluginToolContext`) are all injected automatically by the tool binder implementation; all the arguments represented by `P` are passed through from the call to the `ToolBinder`. [1] Behind the scenes, the `ToolBinder` constructed by the pipeline core iterates all of the plugins loaded for a run, and finds those that are subclasses of `provider`, it injects the fixed prefix arguments alongside the formalization specific arguments represented by `P`. In addition, a special class `AnyBackend` allows a plugin to define tools used by anybackend; it only has the fixed prefix injected, formalization specific parameters are never passed through. The `PluginToolContext` type is the existing `PluginContext` type without the `runner` field; the plugin is expected to provide its functionality through tools, which should not be spawned as top-level multi-job tasks. In addition, we provide a `register` field of type `ArtifactRegistrar`. This lets plugins communicate unstructured "verification artifacts" back to the main pipeline. These artifacts are included in the main report as side information. ## Tool Usage In practice, the expected shape of communication between a plugin and the formalizer are two parameters, the actual runtime representation of the author's state type, and a projector function, which takes an instance of the state and yields a slice of the state used by the author. For example, the `CertoraProverTool` api provides the plugin tools with `type[SourceCVLGenerationState]` and `(SourceCVLGenerationState) -> AsyncContextManager[CVLAuthorState]`. `CVLAuthorState` contains, among other things: 1. The current configuration 2. A materialized copy of the VFS state of the author 3. An edit store for proposing edits to the author's VFS 4. A "prover runner" which handles provisioning and running the prover It is strongly recommended (but not enforced) that formalizers handle provisioning of abstractions for accessing the utilities they themselves access through tools (e.g., running the prover) instead of passing through the raw building blocks to access those utilities themselves. For example, in the prover runner case above, passing through the data necessary for the plugin to run the prover "from scratch" would require passing the `ProverOptions` the "config overlay" (the basic config elaboration performed by the author's prover tool), the current configuration (already passed), *and* require the plugin to know how to piece all that together. All of this together would create a far greater API surface with which to maintain BC for the plugins (e.g., don't rename the `prover_config_overlay` function because some random plugin might need it). In other words, use this projector function pattern to *push* functionality to the plugins, instead of making them pull in random pieces of code from the rest of the AP codebase. ## Parallelization To support long running tools, we've added a `TaskHost` abstraction, which can be used to launch background tasks that run in parallel with the main agent. It is expected this will be used to allow plugins to doe their work as background tasks. The main formalization agent can use the task management tools to query background task state and to wait for/retrieve results. ## Prover Tools The other "big" piece of this PR is enabling plugins for the Certora Prover tool to propose edits to the source code under verification. This could be useful to, e.g., write a plugin that addresses PTA failures due to inline assembly, or to use Concord to make verified large scale rewrites beyond what the code editor agent is empowered to do. These edits are proposed and committed using the existing edit store infrastructure. However, we extend the edit store to record the provenance of edits; the existing editor is called "MungeAgent", edits from plugins are tagged with their id (this tagging is handled automatically; the plugins cannot lie about their id). ## On Testing I have proven this code correct, but I haven't yet tested it [2]. I am sharing it here because its in its mostly final state; I plan to do a big test run in parallel with the review process. [1] There is a second form which takes an `InjectedToolExtension`, which allows the `P` part of the plugin to know about the plugin id it is requesting. Don't think too hard about it, it makes your head hurt. [2] I haven't actually proved it correct either
## Retry policies Retries happen at 2 levels: * Transient, _provider_ level errors. When these occur a retry policy will wait (with exponential backoff) and then try resuming the graph from exactly the last point at execution. * "Wedged", "bad state" errors. These indicate the graph state is likely corrupted. When this occurs; the "fresh start" policy rebuilds a fresh input from the most recent state, mints a new thread id, and then kicks off again. These policies are independent; you can have one but not the other or both at the same time. When both retry policies are installed, the transient provider exception catching is nested within the "bad state" error handler. In practice, this shouldn't matter as they are *intended* to catch different errors. Further, "transient error" retry can be (and usually is) applied to every graph execution in a run of the application. The "retry bad state" handler is, necessarily, graph specific, as it involves reconstructing an input state I from the last run S. ## Retry Policy and Subagents If there is a global, run wide retry policy installed, a subagent spawned from within a tool node will first exhaust its retry policy. Once its retries are exhausted, it will bubble that exception up to the parent graph via its `ToolNode`. The provider level exception (propagated from the subgraph) will then hit the parent graph's retry policy. At this point, the parent graph will be retried from *its* most recent checkpoint; which is the tool node that spawns the subgraph. Importantly, (by convention) subagents are spawned with fresh thread ids each time, so latest attempt at the subagent will itself start with a fresh state. NB this can have a multiplicative effect on backoffs if it turns out we are spending 2 hours retrying runs that are lost causes we can revisit. ## Policy installation As stated above, the transient retry policy is "run global", and is intended to be installed during app startup. The infrastructure is resilient to it not existing, without the context var set, all runs of the graph run without a retry policy. Individual graph runs can, optionally, install their own transient retry handler or their own "bad state", fresh retry handler, or both. It is strongly expected that only a handful of "critical" agents will opt into the fresh retry handling, and no one will ever override the run global retry policy. No one currently uses the state restart functionality but it is tested.
… rustup (#172) * build: install the pinned Rust toolchain before uv builds the crates A fresh checkout of master fails its first sync with an error that names neither rustup's on-demand install nor the concurrency that broke it: error: component download failed for cargo-x86_64-unknown-linux-gnu: could not rename downloaded file ... No such file or directory (os error 2) `dev` is one of uv's default groups and pulls in `apps`, so a plain `uv sync` -- or any `uv run`, which revalidates path deps -- builds the maturin crates under rust/. On a machine that does not yet have the toolchain rust-toolchain.toml pins, each crate's cargo call asks rustup to install it, and rustup's install path is not safe against concurrent invocations: whichever call wins clears $RUSTUP_HOME/downloads and the others die renaming a half-downloaded component. CI already installs the toolchain in a step of its own for this exact reason (.github/workflows/pytest.yml); nothing carried that over to dev machines. Two parts: * README and CLAUDE.md name rustup as a prerequisite and give the argless `rustup toolchain install`, which takes channel, profile and components from rust-toolchain.toml so the pin stays in one place. Fixing machine state is what covers every concurrent cargo caller rather than uv's builds alone -- rust-analyzer's `cargo metadata` on the workspace races identically, and no uv setting reaches it. * concurrent-builds = 1 closes the uv-driven half for whoever skips the docs. Measured on master (two maturin crates), max crates building at once: 2 with no setting, 1 with the key, 1 with UV_CONCURRENT_BUILDS=1, and 2 again under UV_CONCURRENT_BUILDS=8 -- the env var overrides the key, and the key is not merely parsed. Serializing costs next to nothing here: the crates share one cargo workspace, so their builds already contend on rust/target's build-dir lock. pytest -m "not expensive": 956 passed. pyright: 0 errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * docs: say to re-run rustup after a toolchain bump A missing toolchain is what arms the race, so it is not a fresh-checkout-only problem: the next bump to rust-toolchain.toml's `channel` re-arms it for everyone at once, and the install step reads as one-time without this. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
PR 97 (#97) landed two Solana test files that were authored against the Crucible branch's `test_scenarios/solana_vault` Anchor scenario. That scenario did not come with them, so on master they referenced a directory that is not here. `tests/` is deliberately outside pyrightconfig.json, so nothing flagged it. - test_solana_gate.py is entirely scenario-dependent (it asserts the directory exists before doing anything) and cannot run here at all. Remove it; it belongs with the scenario. - test_solana_component_grouping.py is env-gated and does exercise master's SOLANA analysis path, so keep it, but stop naming a scenario and a design doc that only exist on the Crucible branch. Both files also passed a provider *name* where standard_connections wants a resolved ProviderService; fix that in the surviving one so the probe can actually run. test_sandbox_escape.py's docstring pointed at the same scenario and at tests/test_crucible_sandbox_gate.py (a #73 leak, not #97). Describe Part B by what it is rather than by a path that is not in this tree. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Treat an unimplemented contract as a terminal compilation failure A contract that inherits functions it never implements is rejected by solc unless it is declared abstract. That is a defect in the contract's source, not in the compilation settings, so no workaround can clear it -- but the retry loop cannot tell, and its catch-all fires anyway: the run spends several more certoraRun invocations, then the import-patch pass, before reporting a generic "compilation analysis failed" that names neither the contract nor the reason. The contracts most exposed to this are the generated harnesses, written against their target's own file and so blind to what the target inherits from elsewhere. Detect the diagnostic next to the existing abstract-main-contract check and raise on it, naming the contract and the file that declares it. Like that check, it runs before any workaround is applied, so the loop stops at the compilation that reported it. Detection folds solc's hard wrap away first, as the other multi-line detectors in this module do. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Apply suggestion from @shellygr * Restore the closing quotes of _detect_unimplemented_contract's docstring Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Trim the unimplemented-contract comments to what the code does Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* tool family display update, GC bump
We kept seeing the agent say "num_instances == 1" to mean "there should just be one instance of this contract", which we were interpreting to mean "there should be one harness for this contract"-> a whole bunch of doubled up contracts during verification!
* Move code-explorer prompts onto the ecosystem as shared templates
The explorer's look-fors are chain-shaped (PDAs vs require_auth), not
language-shaped. A single Rust prompt cannot name both without lying to
Solana or Soroban. Put a TypedTemplate on Ecosystem, compose a shared
protocol plus crate navigation plus per-chain cites, and thread the
ecosystem through source-env / live-edits construction. EVM wording is
unchanged; Solana/Soroban caller guidance no longer says Solidity.
* Drop the golden EVM explorer-prompt snapshot
Keep the chain-wording checks; do not lock the EVM template to the
pre-split string.
* Defer explorer prompt rendering; name shared templates *_fragment
The explorer system prompt was rendered eagerly against the module-level
`load_jinja_template`, which bypasses whatever loader the graph builder was
configured with. `code_explorer_sys_prompt` now returns the bound
`render_to` so `with_sys_prompt` resolves it against the builder's own
loader.
Solidity's explorer prompt still carried a verbatim copy of the shared
protocol; it now includes the common fragment like the Rust ones do.
The new include-only templates used a `_` prefix to mark themselves as
fragments. The repo already had two markers for that (`_fragment` on
deliver_spec/publish_spec, `_partial` on prover_warning), so the prefix
made a third. Standardize on the `_fragment` suffix, which is both the
more common of the two and the word the ecosystem-abstraction doc already
uses for these templates.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Rename the remaining include-only templates to *_fragment
Finishes centralizing on the one convention: every template that exists
only to be pulled in by `{% include %}` now carries the `_fragment`
suffix, and nothing uses the `_` prefix or the `_partial` suffix.
rust/_vulnerability_patterns.j2 -> rust/vulnerability_patterns_fragment.j2
solana/_vulnerability_patterns.j2 -> solana/vulnerability_patterns_fragment.j2
soroban/_vulnerability_patterns.j2 -> soroban/vulnerability_patterns_fragment.j2
soroban/_platform_model.j2 -> soroban/platform_model_fragment.j2
prover_warning_partial.j2 -> prover_warning_fragment.j2
`Ecosystem.vulnerability_patterns_partial` follows the file it names; it
is declared and assigned once and read nowhere, so the rename is free.
Prose in the surrounding comments and docs moves to "fragment" too, so
the word matches the filenames.
Templates under `shared/` keep their bare names — the directory already
marks them as include-only, and unlike `code_explorer/` it holds no
entry-point templates it needs to distinguish them from.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
…135) * Detect the via-ir-required family by its remediation hint A diagnostic requires the IR pipeline when solc attaches the hint naming that pipeline or its flag (`--via-ir`, `viaIR: true`, "via-ir pipeline", "IR pipeline"), whatever the diagnostic itself is called. The hint is matched on whitespace-normalized text and tolerates a wrap inside a hyphenated token; the conf key `solc_via_ir` stays outside the family since it belongs to the error calling for the opposite fix. The affected file comes from the compiled unit's `Compiling <path>...` line when there is one, and otherwise from the first `-->` source location under the hint, so whole-project compiles are attributed too. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Require via-ir only for diagnostics that offer no other remedy The via-ir hint is read per diagnostic, delimited by solc's own labels (Warning:/<Kind>Error:/YulException:) and the Compiling progress lines. A hint counts only inside a diagnostic that offers no alternative remedy: stack-too-deep and YulException carry the same hint while also offering the optimizer and fewer locals, and stay with stack_too_deep_via_ir and the yul rungs so their ladder is climbed in order. Attribution by `-->` source location is confined to the diagnostic that asked for via-ir, so a neighbouring diagnostic's file is never enabled. The bare `IR pipeline` spelling requires a word boundary, keeping prose in quoted source lines out of the family. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…of unresolved import failed (#168) * autosetup: resolve hoisted node_modules packages, classify unresolved imports npm/yarn hoist a dependency to the highest node_modules that satisfies every consumer, so a sub-project's own node_modules/<pkg> frequently does not exist while the repo root's does. solc has no such resolver: the packages list must name a directory that exists. A bare `node_modules/...` remapping target is now looked for in base_dir first and then in each ancestor up to the run root — node's own order, bounded so the emitted path stays inside the tree certoraRun uploads. A target that resolves under base_dir always wins, so the walk can only change an entry whose target does not exist on disk. lib/ and dependencies/ targets are never walked: forge and soldeer do not hoist and a sibling project's lib/<name> is routinely a different pin. The run root now reaches the build-system managers as its own argument. It was being passed as the build-config dir, so for a monorepo sub-project — the only case where the two differ — both the remapping-context rebasing and the new walk would have been no-ops. utils/import_diagnostics.py classifies each `ParserError: Source "S" not found` against the packages the conf carried. solc names the source unit after remapping, so a target-prefix match on S decides whether a remapping fired and one is_dir() decides the rest: the package target is missing, the file inside an installed package is missing (rebuilding the list provably cannot help), the import is unmapped, or a project file is absent. The classification never gates a workaround — it names the class in the log, in the loop's giving-up message, and in the terminal compilation error. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * autosetup: keep import diagnostics tied to the failure they explain Three fixes on the unresolved-import work, all in the same seam. last_import_diagnostics was only ever written on an output that had a source-not-found error, so a run whose imports were fixed and then died of something unrelated still carried the earlier classification — which setup_prover appends verbatim to CompilationAnalysisError and the no-progress message prints. Every exit from the workaround loop now refreshes the field from the output it is returning on, clearing it when that output has no source-not-found at all. The classifier contradicted the resolver for an installed package whose remapped subdirectory is absent: it tested is_dir() on the full remapped target only, so the case resolve_node_modules_target reports as `subpath_missing` (it found the package directory) was described as "the dependency is not installed there and was not found in any ancestor node_modules". That class now has its own kind, decided by the node_modules/<pkg> root above the target. _ancestor_roots took its step count from resolved paths while composing the candidates textually. When a base_dir reaches the run root through a symlink the two disagree, and the walk either climbs above the run root — emitting a package path outside the tree certoraRun uploads — or stops short of it and misses a hoisted package. The walk is now textual end to end and terminates on the run root itself. Tests: the ancestor-beats-nearer-package case now builds a real package directory (@pkg/artifacts is two segments, so the old fixture created no package at all and never reached the branch it named), plus coverage for subpath_missing, both symlink shapes, the package-root split, and an unrelated terminal failure after an import fix. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…facts on disk (#169) * Pick the build system and artifact dir from artifacts on disk A project shipping both a foundry.toml and a Hardhat config gave no say to which one built the tree: detection always answered Foundry, so a Hardhat project whose foundry.toml only governs a forge test harness had its empty out/ read and yielded no contracts. Detection now breaks that tie on the artifacts present, with Foundry keeping it whenever it has artifacts of its own and when neither side has any. The extractor had the same shape of problem one level down: it read the build system's default artifact directory whenever that directory existed, so a project configuring out = "out/foundry" had its bare out/ read — a directory that exists only as the parent of the real one. The default now counts only while it holds artifacts, and the config's own answer decides otherwise. Both rules ask the same question, "does this directory hold artifacts", which each manager answers from its own layout, and the per-build-system artifact directory helpers in project_dir are now shared with the detector instead of copied. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Require artifact content, not an artifact directory, as build evidence Hardhat's evidence test accepted a bare `artifacts/contracts` or `artifacts/build-info` directory, which a configured-but-never-run build also leaves behind, while Foundry and Truffle both require a file. That asymmetry could hand the tie to Hardhat for a tree only Foundry had built. The unreadable-artifacts error now names the directory the config declares rather than the build system's default, and distinguishes a path that is absent from one that is present but not a directory. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Apply suggestions from code review Co-authored-by: shellygr <shellygr@users.noreply.github.com> * Name one artifacts directory, and say why the default is asked first resolve_artifacts_dir returns the directory the artifacts belong in whether or not it exists, so extract_logic_contracts tests one path and names that same path in the error instead of re-deriving the choice through a second config read. The docstring now explains why the default is asked before the config, and test_a_populated_default_out_wins_over_the_configured_one populates both directories so it actually pins that order. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* CI: give the wire round trips their own marker, out of `fuzz`
The nightly Integration Tests job failed in `run template fuzz tests` the
first night the wire round-trip suite existed. `-m 'fuzz' tests` selected
two unrelated suites: the 36 template tests the step is named for, and the
13 round trips in tests/test_wire_roundtrip.py, whose fixture builds
`wire-echo` with cargo at test time. The step runs `pytest -n 2` and that
fixture is session-scoped *per xdist worker*, so both workers asked rustup
to install the pinned 1.96 toolchain at the same moment. One rolled back
("detected conflict: 'bin/rust-gdb'") and the other found the wreckage:
"the 'cargo' binary ... is not applicable to the
'1.96-x86_64-unknown-linux-gnu' toolchain".
Installing the toolchain up front — pytest.yml already does, for exactly
this reason — would have fixed the crash but left this job paying an
uncached cargo build inside a 20-minute budget, for tests it gains nothing
by running: they pin their own max_examples, so this job's
HYPOTHESIS_PROFILE=extended never reaches them, and pytest.yml runs them at
the same depth on every push to master.
So split the marker instead. `wire` is not a statement about what those
tests do — they are fuzz tests — but about what selecting them commits a
job to: having the pinned Rust toolchain. A Rust-free job can now ask for
`fuzz` and stay Rust-free, which is what this one wants. pytest.yml selects
`-m 'not expensive'` and so keeps running all 35 tests in the file.
The `sync-deps` comment claimed the job "doesn't compile the Rust crates",
which stopped being true the moment those tests carried `fuzz`; it now says
that no toolchain gets installed and points at the step that depends on it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Remove some unneeded comments
---------
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* autosetup: keep the named main contract in the scene Two upstream steps can drop the contract the caller named. Auto-detection skips every file under a dependency directory (node_modules/, lib/, dependencies/, ...) — which is where per-address verification bundles and vendored sub-projects keep real, deployed code — and deduplication prefers the shortest path when two files declare the same contract name. The main contract then never reaches the compilation conf, and the run dies much later inside setup_prover with "'X' is not among the compiled contracts in the prover scene", a compilation message for what is really a scoping decision. with_main_contract() guarantees its presence, displacing a same-named handle from another file: the caller said which file it meant, and keeping both would put back the ambiguity dedup exists to remove. The main contract now also goes through the same artifact-backed name resolution as --contract-files-and-name, so a bare `path.sol` spec gets the contract the file really declares rather than the filename stem. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Make the scene-insertion helper generic, and call it only when it applies The helper never depended on the handle being the main contract, so it is now with_contract_handle(handles, to_add) and its docstring says what it does: append the handle if it is missing, and drop any other handle carrying the same contract_name. Why the main contract can go missing belongs at the call site, where the main contract is what we are talking about, so that reasoning moved into cli.py. The call moved into the branch that already tests for absence: the helper returns the list untouched otherwise. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
… out (#134) * autosetup: substitute a missing solc only when the pragma admits it A contract pinned to an absent compiler was rewritten to whichever compiler was default, regardless of what its pragma allows. For an exact pragma the rewrite cannot compile, so the next pass re-detects the mismatch and re-pins — the two workarounds undo each other until the retry budget or the job timeout ends it. The fallback is now a per-contract plan: each pinned contract is offered only compilers its pragma admits, and an unreadable or unparseable pragma still takes the first candidate. When a contract has no viable substitute the run raises UnsatisfiableSolcPinError naming the contract, its pragma and the binary to install, instead of retrying a substitution that cannot work. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * autosetup: stop the workaround loop when its changes start repeating The loop compares each pass against its own starting state, so it only notices a pass that changed nothing. Two workarounds that undo each other each change the conf relative to their own baseline, and alternate across passes, so the loop runs to the retry budget — one full certoraRun per pass. Record every (workaround, conf delta) applied in the run. A pass whose changes have all been made before means something is undoing them, so stop there and name them. A pass that also lands a new change is still converging and continues. missing_library_harness is exempt via progress_outside_conf: regenerating its harness covers one more library each time, which is real progress the conf does not show. Its own _harnessed_libs guard bounds it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * autosetup: tighten the solc fallback plan and the change ledger Six defects found by review of the two commits below it: - Candidate order put whatever `solc` is on PATH ahead of the project's own default, so a wide pragma could pick an unrelated compiler. The default now comes first and plain solc is the last resort. - A non-UTF-8 source (an accented byte in a header comment) raised out of read_pragma_from_source_file and killed the loop; it now reads as an unknown pragma. - parse_pragma_constraint understands `=X.Y.Z` and `~X.Y.Z`, and reports a disjunction as unknown rather than mis-parsing it. - The terminal raise is gated on a pin the conf actually carries, so a pin seeded from the default compiler no longer fails the run. - certora-fixconf reports the unsatisfiable pin and still writes back the fixes already applied, instead of exiting on a traceback. - The change ledger is scoped to one run of the loop: fixconf runs it twice on one manager, and the second run may legitimately re-apply the first's changes. An exempt workaround no longer vetoes repeat detection for the whole pass — it only keeps its own changes out of the ledger. The note on missing_library_harness now states what its guard keys on and that max_retries is what bounds it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * autosetup: stop the workaround loop on a conf it already compiled The loop now remembers every state it has compiled and gives up when one comes round again. That is what _retry_state already serializes, and it is the same criterion the no-op guard used, widened from "this pass's own start" to "any state this loop has compiled", so the two checks collapse into one. The change ledger this replaces could give up on a conf that compiles. Once compiler_version_mismatch bumps the compiler, cancun_opcode_evm_version re-adds an identical delta, the pass looks like pure repetition, and the loop stops at 3 compiles. The memo reaches the same conf and compiles it on the 4th. The ledger's cost also grew with the contract count on the case it was written for, since the fallback replaces every pinned entry at once while the mismatch re-pins one per pass: 1, 3 and 6 pinned contracts cost 4, 8 and 14 compiles, against 2, 3 and 3 for the memo. Also renames BlockedPin to BlockedSolcPin and SolcFallbackPlan.rewrites to compliant, and corrects a pragma_admits docstring example that this branch's own tilde support had already invalidated. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
… via-ir (#180) * autosetup: try the optimizer under legacy codegen before reaching for via-ir Solc's stack-too-deep advice names two things, "compile with --via-ir while enabling the optimizer", and the ladder acted on the first half only. stack_too_deep_via_ir answered CompilerError: Stack too deep by switching via-ir on for the failing contract, while the optimizer rung sat behind a YulException regex that only the via-ir pipeline ever emits. So legacy plus optimizer was unreachable, and projects that compile fine with the optimizer alone were pushed onto via-ir, which inlines internal functions and takes the CVL internal summaries with it. Three rungs now precede via-ir on a legacy stack-too-deep: enable the optimizer; then, if only the autofinder-instrumented compile is over the limit, accept the finder fallback for those files; then per-contract via-ir as before. Measured on two corpus projects, the optimizer alone compiles scenes of 171 and 43 contracts that the old ladder failed to compile at all, in 554s and 153s, with no via-ir anywhere in the final conf. Per-contract via-ir also no longer walks a large scene one compile at a time. Past ten contracts, or when the project's own build config declares via-ir, the remaining contracts are switched together. One corpus project spent 18 passes and hit a 60-minute cap doing that walk. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Say what via-ir and the autofinder fallback risk, not what they cost Both comments claimed a certainty the code does not have. Inlining can leave an internal summary with nothing to attach to, and a file that falls back during instrumentation can still yield useful finders, but neither is guaranteed either way. What decides the order is the width of the exposure, not a known loss. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Allow the author agent to get their spec stamped by "striping" the rules across different runs. This requires the AP infrastructure to get access to a list of all the rules in a spec file. The way this PR achieves that currently is ... not great, but can be easily swapped in for a "proper" certora-cli invocation whenever that comes down the pipe. This necessitated adding an exclude_rules option to the certora prover tool which maps directly onto the conf flag. While updating the prompts around the verify_spec/prover usage, I took the opportunity to point some outdated advice to the context documents and/or delete some advice that was mooted by more thorough treatment in said docs.
…aster (#184) * Initial plan * chore: advance graphcore submodule and pyproject pin to latest master (54a6852) Co-authored-by: ericeil <7407587+ericeil@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: ericeil <7407587+ericeil@users.noreply.github.com>
…iler default 20->5min
…ceHardFail off); trim comments
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.