Ecosystem abstraction (for Solana support) - #96
Open
ericeil wants to merge 42 commits into
Open
Conversation
This was referenced Jul 23, 2026
ericeil
force-pushed
the
eric/ecosystem
branch
2 times, most recently
from
July 23, 2026 19:58
4c76f66 to
833557a
Compare
Runtime Ecosystem/Language seam; the pipeline driver generalized over FeatureUnit/Main; EVM reproduces today's behavior exactly; Solana added as a second ecosystem (analysis + property extraction) proven against a null (no-verifier) backend. Built on origin/master (which already carries the command sandbox, #73). Stacked-PR 1 of 3 (eric/ecosystem -> eric/rust -> eric/crucible-app); see docs/pr-split-plan.md. Squashed from eric/crucible's final file state for this layer. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The located "main" was `Any`. It is a distinct axis from `FeatureUnit` — the per-unit protocol the extraction phase iterates — and EVM's main (`ContractInstance`) is not a FeatureUnit at all, so it can't just be typed as one. It IS the `Main` type the ecosystem seam already carries (`Ecosystem[App, Main, Unit]`). Thread that `Main` through: `PreparedSystem[FormT, U, Main]` (main: Main), `PipelineBackend[..., U, Main]` (prepare_system -> PreparedSystem[FormT, U, Main]), and `run_pipeline`. Each backend now binds it concretely — EVM foundry/prover to `ContractInstance`, the Solana null backend to `SolanaProgramInstance`. The internal `_extract_all` keeps `main: Any` on purpose: it drives the type-erased `Ecosystem[Any, Any, Any]`, so there is nothing to tie it to there. Pyright (CI paths) clean; pipeline/foundry unit tests pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
_batch_cache_key returned CacheKey[ComponentGroup, Any] because its value type isn't inferable from `props`, CacheKey/WorkflowContext are invariant (so the BackendResult bound won't assign to the caller's WorkflowContext[FormT]), and a return-only TypeVar trips reportInvalidTypeVarUse. Thread the concrete result type as a witness argument (`result_type: type[FormT]`, passed as the formalizer's `formalized_type` already in scope at the sole core-owned call site). FormT is now inferred from an argument, so the batch cache key is typed to exactly the backend's result — no Any, no warning. Pure typing change; the key value (props hash) is unchanged. Pyright (CI paths) clean; pipeline/foundry unit tests pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The `ecosystem: Ecosystem[Any, Any, Any]` param reads like an accidental weakening; it isn't. Ecosystem is invariant, the backend (and its Main) is a free var at this generic boundary so a concrete EVM/SOLANA argument can't unify with a tied param, prepare_system fixes analyzed: SourceApplication, and the backend's U isn't the ecosystem's Unit — so App/Main/Unit can't be tied without a protocol refactor, and the pairing is a runtime contract. Comment only. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The only global_extraction ecosystem (SOLANA) sets collapse_units=True, so the per-property fan-out branch — Ecosystem.property_unit, _solana_property_unit, and the `else` limb in _extract_all — was never reached. It was the prototype that finding-level attribution superseded. Remove it: global extraction now always collapses to one whole-program batch (asserted). Also drops the now-unused SolanaInvariantUnit / PropertyFormulation imports. Pyright (CI paths) clean; pipeline/foundry unit tests pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…leans After removing the per-property fan-out, global_extraction and collapse_units each carried the same single bit as `extraction_unit is not None`, and Solana's required `units` (_solana_units) was dead (never called in whole-program mode). Collapse the three signals into one invariant: an ecosystem sets exactly one of `units` (per-component) xor `extraction_unit` (whole-program), and _extract_all branches on which is present. Both callables are now Optional; drop global_extraction, collapse_units, and _solana_units; type SOLANA's Unit param as SolanaProgramInstance (the whole-program unit) and drop the now-unused SolanaInstructionInstance import. Pyright (CI paths) clean; pipeline/foundry unit tests pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
extraction_unit was equivalent to units() returning a single unit: both feed the same per-unit _extract (same cache context, task, prompts, empty-props drop). It was only distinct as a vestige of the removed fan-out. Collapse it: units is required again and returns a list; Solana returns a singleton [main] (its whole program is the one unit), EVM one per component. _extract_all is now a single gather over ecosystem.units(main) — structurally master's _one loop again, minus the ecosystem-generic bits (units(main), feat.context_tag(), ecosystem prompts). Pyright (CI paths) clean; EVM pipeline/foundry tests pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
FeatureUnit has no isinstance/issubclass call sites, so @runtime_checkable (and its import) bought nothing. Type context_tag()/feature_json() as dict[str, object] across the protocol and every impl (ContractComponentInstance, Solana program/invariant/ instruction units) — all return str-keyed, JSON-able dicts, and the sole consumer (WorkflowContext.child(tag)) accepts it. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The doc shipped in the ecosystem-abstraction commit but still described the pre-ecosystem, Solidity-only, per-component world. Update it to match: - §1/§2: reframe as smart-contract (not Solidity-only) and call out the ecosystem front-half as a second, backend-orthogonal axis of pluggability. - §3/§4: per-component -> per-unit (units() / FeatureUnit); correct the backend signature to PipelineBackend[P, FormT, H, A, U, Main] and PreparedSystem holding Main; add a new "ecosystem seam" subsection. - §4 step 1: analyzed model type is set by the ecosystem, not the backend. - §10: add the Solana front-half (model + prompts + whole-program units). Also drop the now-dangling extraction_unit reference in core.py's PreparedSystem.main comment (removed in the units() unification). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… fragment
ecosystem-abstraction.md was a proposal (title, "Status: proposal", phased
plan, open questions, future tense) and had drifted from the code. Rewrite it
as present-tense documentation of the implemented seam:
- Describe the actual Language + Ecosystem dataclasses and the ECOSYSTEMS
registry (not the earlier Language+Chain protocol sketch).
- Cover only what exists: the seam, EVM (SOLIDITY ⊕ evm), and the Solana
front half (RUST ⊕ solana, whole-program units, shared Rust fragment).
- Drop the unbuilt/off-branch material (Soroban chain, verification backends,
rustapp selection wiring) and the dead companion links.
- Refresh the ecosystem.py module docstring to match.
Also fix a real PR-split bug this surfaced: solana/property_prompt.j2 does
`{% include "rust/_failure_modes.j2" %}` and RUST.failure_modes_partial points
at it, but the file was only added on the PR2 (rust) branch — so rendering the
Solana property prompt raised TemplateNotFound on this branch. Add the file
here, alongside the Solana front half that consumes it.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
application-abstraction.md documents the (Rust) application framework, which belongs with the crucible-app PR, not this front-half ecosystem PR. Remove it here and drop the now-dangling companion link from ecosystem-abstraction.md; it is re-added on eric/crucible-app. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Pin the rendered text of the EVM + Solana analysis/property prompts so that factoring shared boilerplate into partials is provably behaviour-preserving. Renders each template with a permissive context stub (dynamic per-target bits blank out; static boilerplate renders in full) across two control-flow variants (existing-source + prior rounds, greenfield + none). Baseline captured from the current templates; EVM goldens must not change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The EVM and Solana analysis/property prompts duplicated a lot of mechanical
boilerplate (the iterative prior-rounds block, the quality-over-quantity and
adaptive-thinking guidance, the architect Behavior/Tools block, the analysis
memory-tool paragraph) — and the copies had already drifted in wording.
Extract that boilerplate into composer/templates/shared/*, carrying the EVM
canonical wording, with the one domain noun ("component"/"program")
parameterized via a `unit_noun` with-scope. Both ecosystems now `{% include %}`
the partials. Domain-specific prose (backgrounds, category examples, failure
modes, the Rust-source paragraph, the "Reasoning is load-bearing" example)
stays per-file — mechanical boilerplate unified aggressively, prose left alone.
EVM goldens are byte-identical (verified). Solana re-converges to the canonical
wording (goldens updated); nouns stay correct ("program", not "component").
Net: -135 lines across the 8 templates.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
ericeil
changed the title
ericeil
changed the title
The golden snapshot test served as a one-time guard rail to verify the shared-partial prompt refactor was behaviour-preserving (EVM byte-identical). Its job is done and we don't want the goldens/test carried into master, so remove the test module and its snapshot fixtures. The shared/ prompt partials themselves stay. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The null backend (composer/spec/solana/null_backend.py) had no focused coverage — only the expensive live-LLM gate (tests/test_solana_gate.py, on the rust/crucible branches) used it incidentally. Add a deterministic unit test (no LLM / Postgres / prover) on the branch that introduces the backend: formalize echoes properties into a NullResult, fetch_verdicts is empty, prepare_system routes through SOLANA.locate_main and yields the formalizer, to_artifact_id derives the slugged filename, and the backend declares the Solana front-half phases/keys. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
ericeil
marked this pull request as ready for review
July 24, 2026 00:15
|
similarly, files like |
jtoman
requested changes
Jul 27, 2026
Review feedback on the Solana front half: "instruction" is the wrong unit;
it should be an abstract component. The unit was a whole-program singleton,
so this is whole-program -> component, moving coarser-to-finer.
`units` lives on the ECOSYSTEM seam, so every Solana backend inherits it.
The whole-program singleton suited a fuzzer's cost model — K serialised
local builds — but a symbolic backend has the opposite one, and does not
execute action sequences at all. Choosing per-component keeps the decision
backend-neutral, which is where EVM already landed with two backends of its
own (CVL and Foundry share one ContractComponentInstance split).
Every design question here is settled by mirroring EVM: `feature_json` is
the component alone, `units` enumerates the main program only, and the
analysis prompt gives no target component count.
* Model ProgramComponent — the analog of ContractComponent, field for
field (external_entry_points -> instructions, state_variables
-> account_types). It references its instructions by name;
the program's flat list stays authoritative, so the rich
per-instruction data has one home and an instruction may
serve two capabilities.
* Units SolanaComponentInstance mirrors ContractComponentInstance.
SolanaProgramInstance is no longer a FeatureUnit — main and
unit are different axes, as on EVM — and the unused
SolanaInvariantUnit / SolanaInstructionInstance are removed.
* Validation component name/slug uniqueness and interaction resolution
mirror _validate_connectivity. One deliberate divergence: the
component<->instruction mapping must be valid and total. EVM's
external_entry_points are prose the prompt renders, but these
are references the unit wrapper resolves, so a dangling name
silently drops an instruction's account detail from the
extraction prompt, and an instruction no component claims is
an entry point no property will ever cover. It costs a dict
lookup and a set difference.
* Prompts solana/component_context.j2 mirrors application_context_new.j2
section for section, replacing the whole-program context.
property_prompt.j2 no longer describes a fuzzer: that framing
belongs in a backend's `backend_guidance`, the existing
per-backend hole, so a symbolic backend does not inherit a
prompt telling it to write fuzzer properties.
* Driver Formalizer.begin(jobs, run) — a default-no-op hook called once
with every unit's properties, between extraction and the
per-unit fan-out. It is inert for the null backend, but it is
the only point at which a backend with a SHARED artifact can
author it correctly: prepare_formalization runs concurrently
with extraction (no properties yet), and doing it lazily in
formalize lets whichever unit arrives first decide the
artifact the rest must work within.
FeatureUnit regains @runtime_checkable. It was dropped as a no-op, but it is
not one: the tests here assert isinstance against the protocol, which raises
TypeError without it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
composer.pipeline.core no longer re-exports main_instance from composer.pipeline.ecosystem; the two EVM backends (foundry, prover) now import it from ecosystem.py directly. Also tightens run_pipeline's ecosystem parameter: PipelineBackend gained an App type parameter (analyzed: App, replacing the hardcoded analyzed: SourceApplication), and ecosystem is now Ecosystem[App, Main, U] tied to the backend instead of Ecosystem[Any, Any, Any] = EVM. A mismatched backend/ecosystem pairing is now a type error instead of a silent runtime contract, and the cast that used to widen _extract_all's result back to the backend's unit type is gone since the types now line up directly. The one caller that can't tie App/Main/U statically (cli.py's cont, generic to admit both EVM backends) downcasts explicitly at that call site instead. ECOSYSTEMS becomes a TypedDict since the set of ecosystems is closed, avoiding Any there too. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…enames PromptPair.system/.initial were raw j2 filename strings threaded through run_component_analysis/run_property_inference as plain str — a template name standing in for its expected render kwargs with nothing checking they matched. Introduces AnalysisPromptParams (system_analysis.py) and PropertySystemPromptParams/PropertyInitialPromptParams (prop_inference.py) as the TypedDicts each template actually renders with, and switches the prompt fields to TypedTemplate[Params] (composer.spec.gen_types, already the pattern used by author.py/harness.py/summarizer.py/feedback.py elsewhere in this codebase). PromptPair gained a second type parameter since a pair's system and initial templates don't always share a kwargs shape (property inference's system prompt takes just sort; its initial prompt also takes context/prior_properties). Rendering now goes through TypedTemplate.bind(params).render_to(callback) instead of positional **kwargs passed straight to with_sys_prompt_template/with_initial_prompt_template, which is semantically identical (same kwargs, same call) but type-checks the kwargs against the template's declared Params instead of trusting every call site to pass the right ones by convention. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…components run_component_analysis's validate callback (and _validation_wrapper) were pinned to BaseApplication even though T was already in scope; typing them over T lets Ecosystem.validate_analysis strengthen from BaseApplication to App without a contravariance issue (verified with pyright), so the old comment justifying the wider type no longer applies. Also drops SolanaApplication's now-redundant programs/authorities cached-properties from _solana_validate in favor of filtering app.components directly, mirroring how _validate_connectivity reads BaseApplication.components, and removes the isinstance early-return that covered a case validate is never called for.
"Failure modes" undersold the content (concrete bug/vuln patterns per language/chain) and reads as inconsistent naming next to the Ecosystem/ Language split. Renames the j2 partials, the Language.failure_modes_partial field, includes, and docs to match. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Solana has no greenfield workflow — the design-doc-to-source path is natspec's, and it is Solidity-only. The four Solana prompt templates nonetheless carried `sort == "greenfield"` branches inherited from their EVM ancestors, describing a mode that could never be reached. Strip them and keep only the implementation-present content. To keep that from silently regressing, `Ecosystem` now declares whether its prompts have a greenfield branch (`supports_greenfield`: True for EVM, False for Solana) and `run_pipeline` asserts on it, so a future wiring of Solana into a greenfield run fails loudly rather than rendering a template that never mentions the mode it was asked for. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The analysis agent's design document is optional (`run_component_analysis` takes `input: SystemDoc | None` and renders with `has_doc`), so every sentence naming the inputs has to stay true when there is no document. The Solana prompts didn't: they asserted a document had been provided unconditionally. Move `input_phrase` out of the EVM-only `application_analysis_macros.j2` into `shared/analysis_macros.j2` and give it a `has_doc=false` branch plus an `impl_noun` parameter, so Solana can say "Rust implementation" while sharing the branching. All four call sites import it `with context` — a plain import leaves `has_doc`/`sort` Undefined inside the macro, which silently renders the no-document phrasing for every caller (greenfield included, where the document is the only input). That regression is what the new tests pin. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`component_context.j2` built the "other programs in the application" list inline
with a `{% set siblings = [] %}` / `{% set _ = siblings.append(p) %}` loop —
Jinja's workaround for loop-scoped mutation — and excluded the target program by
comparing `program_identifier` strings.
`SolanaComponentInstance` already exposes the neighbouring `sibling_components`
for exactly this purpose, so add `sibling_programs` beside it. It excludes by
index off the located program rather than by string match, mirroring how
`sibling_components` works, and the template collapses to a plain loop.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two cleanups to the Crucible references this stack leaves behind. The null Solana backend tagged its reports `cast(ReportBackend, "crucible")`, forward-referencing a backend that lands later. `ReportBackend` is `Literal["prover", "foundry"]`, so the cast only silenced the type checker: `AutoProverReport` is a pydantic model, so `build_report` raised a ValidationError on the tag, and `run_pipeline`'s `except Exception` swallowed it — the null backend produced no report at all, and hard-failed under `RERAISE_REPORT_FAILURES`. The tag is provenance only (it picks outcome labels, and these results are all-UNKNOWN), so borrow `"prover"` until the real backend adds its own tag to the literal. The tree also cited `docs/crucible-component-units.md` 12 times, at section granularity, for a doc that exists on neither this branch nor master. Retarget the ten covered by `docs/ecosystem-abstraction.md` at its §1/§4. The two begin-hook citations have no counterpart there, and their prose already states the whole argument, so drop the dangling cite rather than invent a section. The doc's own forward reference now says outright that the design note is not yet in the tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…narrowing test 227ba69 removed `_solana_validate`'s `if not isinstance(app, SolanaApplication): return None` guard, on the grounds that `Ecosystem.validate_analysis` is now `Callable[[App, ...]]` and the seam guarantees the model came from this ecosystem. It did not touch tests, so `test_a_non_solana_application_is_not_validated_here` — which asserts exactly the pass-through that guard provided — has been failing ever since. The test encodes a contract the PR deliberately dropped, so delete it rather than restore the guard: returning None for a foreign application silently accepts a model this function never checked. Tighten the parameter from `BaseApplication` to `SolanaApplication` so the case is unrepresentable at the type level instead of merely untested; every other call site already passes a `SolanaApplication`, and pyright over the CI scope (composer/) stays clean. Fast suite now matches master: 333 passed, 9 deselected, 0 failures. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
FormT is now return-only, inferred from the assignment context at the call site, with reportInvalidTypeVarUse suppressed on the annotation. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The identifier type had grown past its name: the ecosystem-agnostic seam (Ecosystem.validate_analysis, run_component_analysis's expected_main_id, SourceFields.contract_name) also carries Solana program identifiers, so _solana_validate was typed over a "SolidityIdentifier". Add SourceIdentifier as the language-neutral identifier and make SolidityIdentifier a phantom subclass of it. The seam now speaks SourceIdentifier; EVM-only code (natspec stubs/interfaces, harness generation, ExplicitContract.solidity_identifier) keeps the narrower type and still flows into the seam, because a Solidity identifier IS a source identifier. The reverse, and assignment to/from the sibling ContractName, stay type errors. Pyright over composer/scripts/tests is unchanged at 44 diagnostics, in one-to-one correspondence with the previous set. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
SourceIdentifier had a Solidity producer but no Rust one — Solana's program_identifier was bare str, so the neutral type was consumed at the seam without anything narrower feeding it. Add RustIdentifier as the second SourceIdentifier subclass and type SolanaProgram.program_identifier with it. The field was already documented and regex-validated as a Rust identifier, so this only makes the existing contract visible to the checker. The two language types are siblings: each widens into the seam, neither converts to the other. Also fixes the 12 bare-literal expected_main arguments in test_solana_components.py (now a VAULT_ID constant shared with the _raw() fixture that declares it, so the two cannot drift) and the constructor in test_null_solana_backend.py. Pyright over composer/scripts/tests: 44 -> 32 diagnostics, no new ones. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
SolanaProgram.name and InterComponentInteraction.program were bare str while their EVM peers (ExplicitContract.name, ComponentInteraction .contract_name) are ContractName, so the one axis the Solana model mirrors field-for-field was the one axis left untyped. Add ProgramName and use it for both. Deliberately NOT a subclass of SourceIdentifier and not sharing a base with ContractName: no ecosystem-agnostic code handles a conceptual name, so a common supertype would serve nothing, and keeping them siblings makes it a type error to name an interaction's peer with the wrong ecosystem's name — or to confuse the name a program is referred to by with the identifier it compiles under. While here, annotate the two component-name fields with the existing ecosystem-neutral ComponentName, completing the field-for-field correspondence its docstring already claims. That alias is a plain `type X = str`, so it documents without constraining. Pyright over composer/scripts/tests stays at 32 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The block had grown into rationale — why each type exists, which callers consume it, why the conceptual names get no shared base. Restore the original shape: mechanism preamble, one line per type, one note on the sibling relation. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…Unit The null backend's docstring already claims it satisfies PipelineBackend "over the Solana ecosystem's (SolanaApplication, SolanaProgramInstance, SolanaComponentInstance) triple", but its Unit slot was the bare FeatureUnit protocol. Ecosystem's Unit parameter is invariant, so that mismatch makes NullSolanaBackend and SOLANA un-composable at run_pipeline: nothing here calls that pair, so it was latent, but tests/test_solana_gate.py (the Rust-framework PR, which this backend's docstring already points at) is the caller that trips it. Narrow the four Unit slots to SolanaComponentInstance. Fixes the mismatch at the root, so the caller needs no cast. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
jtoman
requested changes
Jul 31, 2026
Comment on lines
+254
to
+283
| @@ -274,7 +275,12 @@ async def cont[FormT: BackendResult, A: ArtifactIdentifier, U: FeatureUnit, Main | |||
| run=run, | |||
| interactive=args.interactive, | |||
| max_bug_rounds=args.max_bug_rounds, | |||
| threat_model=threat_model | |||
| threat_model=threat_model, | |||
| # cli_pipeline is the EVM CLI entry point (Solidity identifiers throughout | |||
| # above); App/Main/U are only generic here to admit FoundryBackend and | |||
| # ProverBackend (same EVM triple, different FormT/A). Downcast to the | |||
| # generic ecosystem parameter rather than widening run_pipeline back to Any. | |||
| ecosystem=cast(Ecosystem[App, Main, U], EVM), | |||
Contributor
There was a problem hiding this comment.
this could be polymorphic before because we didn't need the U/App/Main types. Now that we do, fix them. I think both downstream users use this. Or, better yet, make this passed in/generated in a way that doesn't require this cast.
Comment on lines
+113
to
+115
| system_template: TypedTemplate[AnalysisPromptParams] = ANALYSIS_SYSTEM_TEMPLATE, | ||
| initial_template: TypedTemplate[AnalysisPromptParams] = ANALYSIS_INITIAL_TEMPLATE, | ||
| validate: Callable[[T, SourceIdentifier | None], str | None] = _validate_connectivity, |
Contributor
There was a problem hiding this comment.
I'm still confused why you would EVER want to allow the default prompts here or elsewhere. Ditto validate connectivity I guess.
Contributor
Author
There was a problem hiding this comment.
It turned out there was a little more plumbing needed in the natspec code. Done.
| from .types import ComponentName, SolidityIdentifier, ContractName | ||
|
|
||
|
|
||
| @runtime_checkable |
Contributor
There was a problem hiding this comment.
I don't actually see where you use this, necessary?
Contributor
Author
There was a problem hiding this comment.
At one point a test needed this, but it doesn't seem to be used now. Will drop it.
| formalized_type: type[FormT] | ||
| backend_tag: ReportBackend | ||
|
|
||
| async def begin(self, jobs: list[BackendJob[U]], run: PipelineRun) -> None: |
Contributor
There was a problem hiding this comment.
make this a Sequence which has two nice effects: 1) the caller is discouraged by the type system from mutating it, and 2) it makes it covariant, which means you don't need the cast below.
| # 4. Per-component formalization. Caching is core-owned, keyed by the backend's result type. | ||
| # 4. Any shared artifact the units build on is authored HERE — once, from every unit's | ||
| # properties — not lazily by whichever unit formalizes first (see ``Formalizer.begin``). | ||
| await formalizer.begin(cast("list[BackendJob[U]]", batches), run) |
Contributor
There was a problem hiding this comment.
super confused why your claude thinks you need to quote types here, I'm 99% certain you don't? But in any event, you shouldn't need this cast once you take my advice about Sequence.
Comment on lines
+64
to
+79
| async def begin(self, jobs: list[BackendJob[U]], run: PipelineRun) -> None: | ||
| """Called once with **every** unit's properties, after extraction and before the per-unit | ||
| fan-out. Default: nothing. | ||
|
|
||
| The hook exists for backends with a *shared* artifact that all units build on — Crucible's | ||
| fixture, and whatever setup module a CVLR backend needs. Such an artifact must be authored | ||
| from the union of every unit's properties (it is what makes them checkable), and it cannot | ||
| be authored in ``prepare_formalization`` because that runs concurrently with extraction, so | ||
| no properties exist yet. This is the only point where both are true: extraction is done, and | ||
| no unit has been formalized. Doing it inside ``formalize`` instead means the first unit to | ||
| arrive decides the shared artifact for all of them — harmless at one unit, silently wrong at | ||
| several. | ||
|
|
||
| The prover's peer (``invariants.spec``) is staged in ``prepare_formalization`` and needs | ||
| nothing here.""" | ||
| return None |
Contributor
There was a problem hiding this comment.
I would much prefer this sequencing becomes explicit in the API. a type like StagedFormalizer that is returned from prepare_formalization which you can call begin on and have it return the actual Formalizer. If you wanted, you could have the return type of formalize below be StagedFormalizer[FormT, U] | Formalizer[FormT, U] and have the pipeline driver introspect types to determine whether to begin or go straight to formalizing.
run_component_analysis and run_property_inference each defaulted their domain-specific inputs to the EVM/Solidity values. Only one caller relied on that: the natspec pipeline, which supplied neither prompt pair, no validator, and no backend guidance. It happened to want the EVM values, so the defaults were invisible rather than wrong — but they made "forgot to pass a prompt" indistinguishable from "meant the Solidity one", and a new chain that forgot would have analyzed Rust with the Solidity prompt and produced a plausible-looking run instead of an error. Drop the defaults for both prompt pairs, `validate`, and `backend_guidance`; thread an ecosystem through natspec to supply the prompts. The four *_TEMPLATE constants now have exactly one reference each, in EVM's Ecosystem binding. Two things the change surfaced: - `_validate_connectivity` is not EVM's validator, it is the Solidity model *family's* — typed over BaseApplication because it only checks the contract/actor/interaction graph that Application, SourceApplication, HarnessedApplication and FromSourceApplication all share. Renamed to validate_solidity_connectivity: three named callers across two modules (ecosystem.py was already importing the private name). - natspec cannot take `validate` from the ecosystem it now carries. Ecosystem.validate_analysis is Callable[[App, ...]] with App = SourceApplication, while natspec's model comes from mental_model.model_ty — Application or FromSourceApplication, siblings under BaseApplication, not subtypes — so contravariance rejects it. It names the family-level validator directly, and CERTORA_BACKEND_GUIDANCE likewise since it has no PipelineBackend to read backend_guidance from. Name the two concrete Ecosystem instantiations (EvmEcosystem, SolanaEcosystem) so the Ecosystems registry, the EVM/SOLANA bindings, and natspec spell each triple once; natspec takes EvmEcosystem rather than erasing to Ecosystem[Any, Any, Any], which is accurate — it authors Solidity and CVL, so EVM is the only ecosystem it can run under. pyright: 0 errors. pytest tests/: 337 passed, 5 deselected — those 5 fail identically on master here (certoraRun not installed locally, so prover validation fails and the tape lanes diverge). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
cli_pipeline held the one place the ecosystem seam still needed a cast. Its `cont` closure is generic over App/Main/U so it can admit both FoundryBackend and ProverBackend, but it named the ecosystem itself — so EVM, whose triple is concrete, had to be downcast to the caller's still-unsolved type variables. Move the ecosystem onto the Continuation protocol. Each entry point already knows its backend concretely, so foundry/entry.py and autoprove_common.py pass EVM at a point where App/Main/U are solved from the backend and the assignment checks outright. This makes the pairing enforced rather than asserted: passing SOLANA at either site is now an error on all three invariant parameters, where the cast would have accepted it silently. docs/ecosystem-abstraction.md §1 already claimed the analyzed model, main-unit, and per-unit values "flow through without casts" — that is now true. Also drops an unreachable `...` left after cont's return statement. pyright: 0 errors. pytest tests/: 337 passed, 5 deselected (the 5 fail identically without this change — certoraRun is not installed locally). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sequence is covariant, so the driver's list[_Batch[U]] passes as Sequence[BackendJob[U]] directly, and it discourages implementations from mutating the caller's list. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Nothing checked FeatureUnit at runtime — it appears only as an annotation and as the U bound on the pipeline generics. The decorator only ever enabled isinstance() (issubclass() raises on this protocol, since the @Property members are non-method), and a structural isinstance would be a weak gate anyway: it compares attribute names via getattr_static, not signatures or return types, so it can't hold the Main-is-not-a-Unit line that spec/solana/model.py documents. Leaves the type checker as the sole gate on conformance, matching SandboxProvider. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`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. The shared artifact now arrives as a constructor argument
to the only object that uses it, so no formalizer exists without it and the
ordering is a type-level dependency like every other link in the chain.
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.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Removed the number of tests from the pytest command comment.
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
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
PR 1 of 3 — Ecosystem abstraction (EVM + Solana front-half)
Part of the stacked split of the Crucible work (and preparatory for full Solana Prover support).
Stack:
master→eric/ecosystem→eric/rust→eric/crucible-app.Introduces a runtime ecosystem seam so the shared pipeline driver generalizes over the
analyzed domain instead of being hard-wired to Solidity — and lands the Solana front half
(analysis + property extraction) against it. EVM behavior is unchanged (the driver defaults
to
ecosystem=EVM); Solana is added as a second ecosystem, exercised end-to-end by a null(no-verifier) backend. The Solana verification backend (Crucible) is PR 3.
The seam
composer/pipeline/ecosystem.py(new) —Ecosystem[App, Main, Unit]+Languagefrozendataclasses, the
EVM/SOLANAbindings, and theECOSYSTEMSregistry. An ecosystem factorsinto a language facet (how the analyzed source is read — Solidity vs Rust) and a chain facet
(model + prompts + unit split).
composer/pipeline/core.py—run_pipelinetakes anecosystem(defaultEVM) and drivesthe front half through it (analyzed-model type, prompts, validation,
locate_main,units).The per-unit loop iterates
ecosystem.units(main)over anyFeatureUnit.composer/spec/system_model.py— the ecosystem-agnosticFeatureUnitprotocol; EVM staysbound to
ContractInstance/ContractComponentInstancewith byte-identical cache keys.prop_inference.py/system_analysis.py/cli.py/ptypes.py— threaded through toaccept the ecosystem's prompts/units/
Maingenerics.Typing
PreparedSystem.mainand thePipelineBackend[..., U, Main]generics carryMain/FeatureUnitinstead of
Any;_batch_cache_keyis typed via a result-type witness.run_pipeline'secosystem: Ecosystem[Any, Any, Any]) isdocumented with the invariance reasoning.
FeatureUnit.context_tag/feature_jsonreturndict[str, object]; dropped a no-op@runtime_checkable.Solana front half
composer/spec/solana/model.py(new) —SolanaApplication(the standalone analog ofSourceApplication): programs, instructions, account constraints, CPIs, signers; plus theSolanaProgramInstance/SolanaInstructionInstanceindex wrappers. Whole-program extraction(
units→ a singleton[program]).composer/spec/solana/null_backend.py(new) — a report-only backend that records extractedproperties without verifying, so the front half can be gated without a prover.
composer/templates/solana/*— Solana analysis + property prompts, and theRUSTlanguage'srust/_failure_modes.j2fragment they compose in.Shared prompt partials (EVM + Solana dedup)
The EVM and Solana prompts duplicated a lot of mechanical boilerplate (the iterative prior-rounds
block, quality-over-quantity / adaptive-thinking guidance, the architect Behavior/Tools block, the
analysis memory paragraph) — and the copies had drifted. Factored into
composer/templates/shared/*carrying the EVM canonical wording, with the one domain noun(
component/program) parameterized. Mechanical boilerplate unified; domain prose (backgrounds,examples, failure modes) left per-file. EVM prompts render byte-identical; Solana re-converges
to canonical wording.
Docs & tests
ARCHITECTURE.md(new) — high-level system map, written around the ecosystem seam.docs/ecosystem-abstraction.md— describes the implemented seam (present tense).tests/test_null_solana_backend.py(new) — deterministic unit test of the null backend(no LLM / Postgres / prover).
CLAUDE.md— repo rule againstfrom __future__ import annotations.(The Rust application framework doc
application-abstraction.mdlives with PR 3, where that codelands.)
🤖 Generated with Claude Code