Ecosystem abstraction (for Solana support) - #96
Merged
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
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
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.
jtoman
approved these changes
Aug 3, 2026
The merge commit landed only the four conflicted files; this is the rest of the resolution, without which the tree does not typecheck. - `Ecosystem.plugin_unit`: the EVM view of a unit. Master's plugin hooks are typed on `ContractComponentInstance`, so EVM supplies the identity and Solana supplies `None` — the driver then skips its plugin phases and leaves its unit cache keys free of the plugin digest. Widening the plugin API to `FeatureUnit` retires the field. - `PropertyPrompts` replaces `PromptPair` for the property agent: a shared system template plus a per-ecosystem initial-prompt *renderer*. Only the initial prompt's params carry a unit, and each ecosystem has to name its concrete unit type so the template fuzzer can construct one — the `FeatureUnit` protocol it speaks is not constructible. - Solana templates hoisted to top-level names (the manifest scan is an AST scan, so an inlined declaration is invisible to it) and added to the manifest. - `backend_guidance` moves to Solana's system prompt, matching master's move on the EVM side; the fuzzer caught it still being read from the initial prompt. - Fuzzer: coherent-unit strategies for Solana, component shaping generalized from `ExplicitContract`/`ExternalActor` to "carries its own components list", and list draws capped so the deeply-nested Solana model fits the entropy budget under the `extended` profile. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The command named pyright as living in group `ci` and then omitted that group, so following it to restore a missing test dep uninstalled pyright and broke the other half of the same pre-commit pass it documents. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Plugin hooks were typed on `ContractComponentInstance`, so the driver narrowed its generic unit through `Ecosystem.plugin_unit` and skipped the plugin phases wholesale for any ecosystem without an EVM view. Plugins now declare which runs they apply to, and the narrowing moves to plugin *load* time. - `PipelinePlugin[U: FeatureUnit]` — hooks take `U`. Because `U` appears only in parameter position, the class is contravariant in it, so a `PipelinePlugin[FeatureUnit]` is assignable wherever a specific ecosystem's plugin is wanted and the reverse is a type error. "Agnostic plugins run everywhere, specific ones only in their own ecosystem" needs no enforcement machinery; it is what the variance already says. - `PluginScope = AnyEcosystem | ForEcosystem[U]`, declared on the *loader* so an inapplicable plugin never reaches `initialize` — where PLUGIN.md says resources get acquired. Scope and `initialize` share `U`, so a mismatch is a type error in the plugin's own package, at the declaration site. - `Ecosystem.unit_type` replaces `plugin_unit`. A runtime value because the matching happens at the entry-point boundary, and `FeatureUnit` is deliberately not `@runtime_checkable`. - `PluginManager[P, U]` carries already-narrowed plugins, so `_extract_all` loses the narrowing dance entirely: no optional unit view, no guards, no conditional digest. One cast remains, at the dynamic entry-point boundary, where the runtime scope check is the evidence the static type can't be. Cache-key semantics change: the per-component digest now covers the *applicable* manifest, not the installed one, so a plugin scoped to another ecosystem stops invalidating this one's cached work. The `cache_root` tag has to agree with that digest or `cache-autoprove` rehydrates the wrong namespaces, so the tag write moves into `cli_pipeline`'s continuation, where the ecosystem is known. Existing per-component entries invalidate once. Also documents that `cache-autoprove` reconstructs prover keys only — it advertised the foundry entries, but reads components from "ap-properties" while foundry writes "foundry-properties". Pre-existing; documented, not fixed. Backend-specific scoping is left out, with the extension points commented: the `PluginScope` union, `_applies`, and `load_plugins`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ericeil
commented
Aug 4, 2026
ericeil
commented
Aug 4, 2026
jtoman
reviewed
Aug 4, 2026
jtoman
left a comment
jtoman
left a comment
Contributor
There was a problem hiding this comment.
honestly, way less painful than I thought it would be!
master (#120) replaced the FS_FORBIDDEN_READ regex with the fs_forbidden_read predicate, which collided with this branch's SolidityIdentifier -> SourceIdentifier rename on the same two lines of the SourceFields construction in pipeline/cli.py. Took both: the neutral identifier and the predicate. The ecosystem seam merged clean but not correct — the SOLIDITY facet imported the constant master deleted. It now holds the predicate, and Language.default_forbidden_read widens from str to str | Callable[[PurePath], bool], the two shapes graphcore's GlobalExcludeArg accepts. RUST_FORBIDDEN_READ stays a pattern: nothing in a Cargo layout needs carving back out of an excluded directory, which is what forced Solidity to a predicate. graphcore moves to c8b3ae5 (master's pin), a descendant of this branch's 932cf73 that carries the forbidden_read predicate support the above depends on. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ericeil
added a commit
that referenced
this pull request
Aug 4, 2026
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>
ericeil
added a commit
that referenced
this pull request
Aug 4, 2026
Rebased onto the `eric/rust` that now sits on master, so the plugin system (#89/#96) is underneath this branch for the first time. Three seams moved: * `_extract_all` takes a `PluginPhaseManager`. `test_crucible_granularity` drives that helper directly, so it now passes one — and gets it from a new `PluginManager.without_plugins`, rather than depending on the ambient entry points happening to be empty (they are today; installing any plugin would otherwise silently change what this test measures). The granularity claim is about the unit axis; the hooks themselves are `test_plugin_scope.py`'s. * `PropertyPrompts` carries a bound `render_initial` renderer, not an `initial` template — the fake ecosystem's namespace follows. * `llm_factory` is gone from `composer.workflow.services`: an unused import in the three crucible gate modules. `RUST_FORBIDDEN_READ` keeps this branch's scratch-dir exclusions — PR 2 pushed them out of the front half precisely because they belong to the backend that creates the dirs, and that backend is this one. Only the doc comment's cross-reference changes, since master's Foundry filter is now the `fs_forbidden_read` predicate. Verified: pyright 0 errors, 653 passed / 17 deselected. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ericeil
added a commit
that referenced
this pull request
Aug 4, 2026
Rebased onto the `eric/rust` that now sits on master, so the plugin system (#89/#96) is underneath this branch for the first time. Three seams moved: * `_extract_all` takes a `PluginPhaseManager`. `test_crucible_granularity` drives that helper directly, so it now passes one — and gets it from a new `PluginManager.without_plugins`, rather than depending on the ambient entry points happening to be empty (they are today; installing any plugin would otherwise silently change what this test measures). The granularity claim is about the unit axis; the hooks themselves are `test_plugin_scope.py`'s. * `PropertyPrompts` carries a bound `render_initial` renderer, not an `initial` template — the fake ecosystem's namespace follows. * `llm_factory` is gone from `composer.workflow.services`: an unused import in the three crucible gate modules. `RUST_FORBIDDEN_READ` keeps this branch's scratch-dir exclusions — PR 2 pushed them out of the front half precisely because they belong to the backend that creates the dirs, and that backend is this one. Only the doc comment's cross-reference changes, since master's Foundry filter is now the `fs_forbidden_read` predicate. Verified: pyright 0 errors, 653 passed / 17 deselected. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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