Ecosystem abstraction (for Solana support)#96
Open
ericeil wants to merge 19 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
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
1 participant
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