Consolidate typed execution, verification, and runtime ownership (#1276)

* refactor(operations): project typed outcomes at dispatch

* refactor(verification): consolidate checker execution and identity

* refactor(runtime): remove portfolio and storage facades

* docs(architecture): codify the simplified ownership model

Author: morluto

AGENTS.md

@@ -113,6 +113,18 @@ publication binding only when inline transport is insufficient. Publication
 owns transport only; it does not own mathematical validation, applicability,
 provider selection, effects, parsing, or checker authority.
 
+Do not introduce pass-through facades to make a dependency graph look cleaner.
+An aggregate may coordinate a public lifecycle or transaction, but it must not
+mirror every collaborator method, bounce callbacks back through itself, or keep
+private forwarding methods solely for tests. Call the concrete owner directly;
+extract a shared abstraction only when two production paths replace their older
+implementations in the same change.
+
+Composition roots retain only resources needed after construction. Do not build
+or return nested installation reports, provider bags, or phase-result mirrors
+that production immediately discards. Keep an installation result only when a
+later production phase consumes that exact typed fact.
+
 Construct wire envelopes only at the final capability or protocol projection.
 Mathematical functions, typed operation executors, artifact services, and
 checker services return their owned typed values or terminal states; they do
@@ -122,6 +134,11 @@ a domain-specific durable schema or parent closure, keep that publication in a
 narrow named domain publisher and pass its typed projection to the one final
 envelope constructor.
 
+Measure expensive checker source and dependency identity at authorization and
+inside the bounded checker worker, not during catalog discovery, compatibility
+selection, or ordinary runtime startup. Registry reads validate persisted
+identity and authority; the execution boundary remeasures executable bytes.
+
 At the MCP boundary, prefer MCP Python SDK 2.0 high-level typed returns. Return
 Pydantic result models directly and let the SDK derive the output schema,
 validate results, and populate `content` and `structured_content`. Use an

docs/explanation/architecture.md

@@ -180,9 +180,10 @@ mathematical result and from verification authority.
 
 `CapabilityResult` is a wire projection, not an in-process return type. Domain
 functions, operation executors, artifact services, and checker services return
-their owned typed values or terminal states. The final capability adapter
-constructs the wire envelope once, after publication has returned the complete
-artifact closure. Artifact-producing operations must not move storage writes
+their owned typed values or terminal states. The public dispatcher constructs
+the wire envelope once, after publication has returned the complete artifact
+closure; installed adapters return a typed projection rather than constructing
+the envelope themselves. Artifact-producing operations must not move storage writes
 into `OperationSpec.execute`; a domain-specific publisher may preserve an
 established durable schema and parent closure without expanding the generic
 publication policy.
@@ -214,6 +215,19 @@ subject, candidate, evidence, protocol, semantics, scope, certificate format,
 and checker identity. Independent checker execution does not import or call the
 producer, proposal, search, or evaluation path it certifies.
 
+Checker identity comes from a versioned manifest for that checker, not from a
+digest of the whole Jacobian package. The manifest binds its exact entry point,
+separate checker and worker source closures, exact Python distributions, Python
+and provider runtime, passive contracts, and bounded-process policy. The worker
+admits only the declared first-party closure and manifest-bound third-party
+distributions, including imports requested dynamically during checker
+execution, and remeasures the complete
+manifest—including the current bytes of every indexed dependency file—around
+execution. Authorization performs the same measurement once; catalog and
+compatibility reads do not repeat that filesystem scan. A producer or unrelated
+checker edit therefore cannot change the identity, while a changed executable
+dependency cannot retain it.
+
 `VerificationResult` is the internal typed outcome of that checker execution,
 not a generic mathematical result envelope. Capability adapters project it
 once into the ordinary operation response. Ordinary producers do not use it,
@@ -299,6 +313,13 @@ and checker authority. Remote authentication, tenants, admission, leases,
 eviction, and quarantine belong to a separate remote host and do not enter the
 local mathematical server.
 
+Local artifact storage retains one concrete filesystem CAS with SQLite metadata.
+`ArtifactRepository` is its public aggregate; explicit transaction, blob, and
+metadata collaborators own the implementation. They are not interchangeable
+backend interfaces, and new storage abstractions require new workload evidence.
+The aggregate coordinates lifecycle and transactions; it does not mirror
+collaborator-private blob or recovery APIs.
+
 MCP uses SDK-derived typed schemas and structured output. Pydantic result models
 are returned directly unless a genuine `ResourceLink`, custom metadata, or
 deliberate text projection requires an explicit MCP result. The two fixed tools

docs/how-to/deploy-remote-mcp.md

@@ -397,7 +397,7 @@ is first used. This warms Lean and filesystem caches without delaying MCP
 startup.
 
 Lean results are cached only for an exact content-addressed certificate and
-the currently active checker digest. The bounded in-memory cache holds 128
+the currently active checker implementation digest. The bounded in-memory cache holds 128
 entries; a changed proof, statement, environment, checker, or authorization
 state cannot reuse an entry. `math.find` for `lean.check` reports the
 cache policy and the MATHLIB warm-up state (`RUNNING`, `HEALTHY`, or

docs/reference/evaluations/evaluation-methods.md

@@ -139,8 +139,11 @@ Representative groups include:
 - checker plan construction and bounded replay;
 - request-local and durable value transport;
 - MCP stdio and HTTP round trips; and
-- SQLite BLOB storage at 1 KiB, 100 KiB, 1 MiB, and 10 MiB with concurrency
-  1, 4, and 16, including crash/restart and backup/restore.
+- retained filesystem-CAS storage at representative payload sizes and
+  concurrency, including crash/restart, bounded reads, and backup/restore.
+
+The disposable SQLite BLOB comparison is retained only as reproducible decision
+evidence. It is not a production backend or a routine benchmark dimension.
 
 For Lean proof-state backend comparisons, run
 `benchmarks.tooling.lean_repl_backend_benchmark` as a pyperf cell for each

docs/reference/state-format.md

@@ -1,6 +1,6 @@
 # Persistent state format
 
-The current and minimum supported state format is revision 8. Older stores are
+The current and minimum supported state format is revision 10. Older stores are
 rejected before any migration code runs.
 
 To recover data from an older store, keep that directory unchanged and open it
@@ -9,7 +9,10 @@ current version; Jacobian provides no cross-revision import bridge. Do not edit
 `metadata.sqlite3` to change its revision—the migration ledger and state-format
 record are integrity boundaries.
 
-Earlier migration definitions remain in source because existing revision-8
-ledgers bind their checksums. They do not define supported runtime services or
-an in-place upgrade path. New stores apply the complete ordered schema and
-record revision 8.
+Earlier migration definitions remain in source because migration ledgers bind
+their checksums. They do not define supported runtime services or an in-place
+upgrade path. Revisions 9 and 10 replace the broad checker-package digest with
+a versioned per-checker manifest that separates checker and worker source,
+records exact Python distributions, and produces one implementation digest;
+existing checker authorization rows are deliberately not reinterpreted. New
+stores apply the complete ordered schema and record revision 10.

docs/reference/testing-strategy.md

@@ -218,10 +218,11 @@ Python identity, dependency files, native libraries/executables, and sandbox
 policy. Unrelated product changes must not alter checker identity; actual
 checker dependencies must.
 
-Storage experiments remain an independent track. Compare SQLite BLOB behavior
-at 1 KiB, 100 KiB, 1 MiB, and 10 MiB with concurrency 1, 4, and 16, including
-crash/restart, backup/restore, and bounded reads. Performance evidence never
-substitutes for correctness.
+The completed storage experiment retained the filesystem CAS. Its disposable
+SQLite comparison remains reproducible evidence rather than a selectable
+backend. Storage regression tests therefore focus on the retained CAS's
+transaction coordination, quota recovery, bounded reads, crash/restart, and
+backup/restore behavior.
 
 Run the disposable carrier comparison with:
 
@@ -230,9 +231,9 @@ uv run python tools/benchmark_storage_blobs.py --iterations 16 \
   --output storage-blob-benchmark.json
 ```
 
-The spike is decision evidence, not a selectable runtime backend. Its rollback,
-restart, bounded-read, and backup/restore checks must all pass before latency or
-throughput can justify replacing the current two-store recovery protocol.
+The spike is historical decision evidence, not a selectable runtime backend or
+a second production abstraction. Re-run it only when new workload evidence
+justifies reopening the storage decision.
 
 Hosting tests keep local and remote ownership separate. Remote authentication,
 tenants, admission, leases, eviction, and quarantine must not enter the local

pyproject.toml

@@ -5,7 +5,7 @@ build-backend = "hatchling.build"
 [project]
 name = "jacobian"
 version = "0.11.0"
-description = "A capability-first MCP workbench for executable mathematics"
+description = "Atomic mathematical tools for agents over MCP and Python"
 readme = "README.md"
 requires-python = ">=3.12,<3.14"
 license = { text = "MIT" }
@@ -184,6 +184,26 @@ forbidden_modules = [
     "jacobian.value_references",
 ]
 
+[[tool.importlinter.contracts]]
+name = "Semantic operations do not depend on installed layers"
+type = "forbidden"
+source_modules = ["jacobian.operations"]
+forbidden_modules = [
+    "jacobian.adapters",
+    "jacobian.checker_operations",
+    "jacobian.installation",
+    "jacobian.operation_bindings",
+    "jacobian.operation_installation",
+    "jacobian.operation_projection",
+    "jacobian.operation_publication",
+    "jacobian.operation_runtime",
+    "jacobian.persistence",
+    "jacobian.portfolio",
+    "jacobian.runtime",
+    "jacobian.storage",
+    "jacobian.verification",
+]
+
 [[tool.importlinter.contracts]]
 name = "Finite-field values do not import private backends"
 type = "forbidden"