Skip to content
Merged
Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
0ba4450
refactor(runtime): centralize capability result projection
morluto Aug 13, 2026
7a3edda
refactor(runtime): parse capability inputs before provider work (#1314)
morluto Aug 13, 2026
dca8a64
Merge live main into centralized dispatch projection
morluto Aug 13, 2026
c233311
fix(composition): preserve resolved typed value identity
morluto Aug 13, 2026
8db3872
Merge live main into centralized dispatch projection
morluto Aug 13, 2026
82dff03
fix(composition): separate typed binding from JSON accounting
morluto Aug 13, 2026
adb73d7
Merge main into centralized dispatch projection
morluto Aug 13, 2026
51bd2d3
fix(runtime): preserve typed dispatch values and outputs
morluto Aug 13, 2026
588431a
Merge current main into typed dispatch refactor
morluto Aug 13, 2026
e2e2e67
Merge remote-tracking branch 'origin/main' into HEAD
morluto Aug 13, 2026
49394a1
fix exact replay preparation and relative import ratchet
morluto Aug 13, 2026
0c71830
fix exact replay request preparation import
morluto Aug 13, 2026
e785b63
fix exact replay prepared value handoff
morluto Aug 13, 2026
3a8773e
fix exact verifier typing and relative result imports
morluto Aug 13, 2026
3fff100
test polytope adapter preparation handoff
morluto Aug 13, 2026
7f920e8
Merge current main into centralize dispatch PR
morluto Aug 13, 2026
e38bb14
test(lean): prepare typed requests in live smoke
morluto Aug 13, 2026
ea6c019
Merge current main into dispatch refactor PR
morluto Aug 13, 2026
8bb8ea3
fix(architecture): remove legacy checker mode marker
morluto Aug 13, 2026
2219b0f
Merge remote-tracking branch 'origin/main' into HEAD
morluto Aug 13, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions AGENTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -208,6 +208,13 @@ checker authorization out of plugins and search code.
validation. Exercise incompatible-but-individually-valid values through the
serialized installed-operation boundary and assert an invalid-request result
with no execution or publication.
- Parse agent-supplied JSON strictly into the owning Pydantic request model;
advertised integers must not accept numeric strings or other coercions. An
adapter prepares that typed request before provider readiness and executes
only the prepared value. Strict transport encoding is lossless: do not reduce
rationals, normalize Unicode, or otherwise repair semantic input before the
owning model validates it. At the final projection, require the published
Pydantic model to match the installed output contract before serializing it.
- Mathematical inputs are not presumed confidential. Public diagnostics should
expose a stable domain reason, path, limit, and recovery direction—not
arbitrary rejected values, which may be unbounded or user-controlled. This
Expand Down
17 changes: 11 additions & 6 deletions docs/explanation/architecture.md
Original file line number Diff line number Diff line change
Expand Up @@ -165,10 +165,15 @@ external payload
Pydantic owns complete request validation, including relationships among
otherwise valid fields. Required agreement of parents, characteristics,
presentations, axes, bases, labels, and bound identities is checked during the
single request parse, before preflight or any provider call. JSON Schema is
generated for discovery and is not executed as an additional validation pass
for built-ins. Provider and subprocess output is a separate untrusted boundary
and is parsed independently.
single strict, lossless request parse, before provider readiness, preflight, or
execution. Domain canonicalization happens only after the owning request model
has accepted the original values; transport parsing does not reduce rationals
or normalize Unicode.
JSON Schema is generated for discovery and is not executed as an additional
validation pass for built-ins. Before the single final serialization, dispatch
checks that the published Pydantic model still generates the installed output
contract. Provider and subprocess output is a separate untrusted boundary and
is parsed independently.

Preflight distinguishes supported, unsupported, provider unavailable, and
resource-limit-exceeded outcomes. Where practical it estimates work, output
Expand Down Expand Up @@ -273,8 +278,8 @@ Using a request-local carrier does not change a value or grant assurance.
## Structural JSON

The runtime retains direct bounded JSON functions rather than a codec
framework: a strict loader, deterministic serializer, Pydantic adapters, and
one explicit schema-only adapter. Generic JSON rejects duplicate keys and
framework: a strict loader, deterministic serializer, and Pydantic adapters.
Generic JSON rejects duplicate keys and
unsupported numbers, enforces depth/member/byte limits, preserves keys and
strings exactly, and performs no Unicode or mathematical normalization.

Expand Down
16 changes: 9 additions & 7 deletions docs/reference/provider-runtime.md
Original file line number Diff line number Diff line change
Expand Up @@ -86,26 +86,28 @@ SMT-LIB parser and proof APIs are checked lazily at first use. Missing or
mismatched package identity is a broken installation, while a first-use
readiness failure fails the selected invocation closed.

Source-backed adapters can construct metadata without importing their
implementation:
Source-backed checker implementations can construct metadata without importing
their implementation:

```python
from jacobian.contracts.capabilities import CapabilityInstallTier
from jacobian.provider_runtime import source_provider_runtime

runtime = source_provider_runtime(
"example.provider",
"example.checker",
version="1",
entrypoint="example_adapter:create_adapter",
entrypoint="example_checker:check",
install_tier=CapabilityInstallTier.T1,
license_id="MIT",
license_files=("LICENSE",),
features=("exact-example-operation",),
features=("exact-example-check",),
)
```

The adapter places `runtime` in its descriptor. Registration remains
fail-closed if the source identity cannot be resolved.
The checker registration binds `runtime` to its independently authorized
entrypoint. Registration remains fail-closed if the source identity cannot be
resolved. External operation packages and adapter entrypoint discovery are not
supported.

### External checker runtimes

Expand Down
6 changes: 1 addition & 5 deletions src/jacobian/adapters/mcp/tools.py
Original file line number Diff line number Diff line change
Expand Up @@ -309,11 +309,7 @@ def _bounded_run_result(
if not (result.diagnostics and result.diagnostics[0].code == "UNKNOWN_CAPABILITY"):
return result
payload = result.model_dump(mode="json")
output = {
key: value
for key, value in payload["output"].items()
if key != "available_capability_ids"
}
output = payload["output"]
output.update(_unknown_capability_context(runtime, result.capability_id))
payload["output"] = output
return CapabilityResult.model_validate(payload)
Expand Down
26 changes: 10 additions & 16 deletions src/jacobian/builtin_capabilities.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

from __future__ import annotations

from jacobian.capability_adapters import parse_capability_input
from jacobian.contracts.capabilities import (
CapabilityDescriptor,
CapabilityDiagnostic,
Expand All @@ -11,7 +12,7 @@
)
from jacobian.contracts.lean import (
LeanCheckOutput,
LeanEnvironment,
LeanCheckRequest,
)
from jacobian.contracts.results import ExecutionStatus
from jacobian.lean_frontend.service import LeanService
Expand Down Expand Up @@ -40,16 +41,7 @@ def __init__(
),
provider="jacobian.lean4",
provider_runtime=provider_runtime,
input_schema={
"type": "object",
"properties": {
"statement": {"type": "string", "minLength": 1, "maxLength": 2000},
"proof": {"type": "string", "minLength": 1, "maxLength": 20000},
"environment": {"enum": ["CORE", "MATHLIB"]},
},
"required": ["statement", "proof"],
"additionalProperties": False,
},
input_schema=LeanCheckRequest.model_json_schema(),
output_schema=LeanCheckOutput.model_json_schema(),
tags=(
"lean",
Expand Down Expand Up @@ -84,12 +76,14 @@ def __init__(
def descriptor(self) -> CapabilityDescriptor:
return self._descriptor

def invoke(self, request: CapabilityRequest) -> OperationProjection:
payload = request.input
def prepare(self, request: CapabilityRequest) -> LeanCheckRequest:
return parse_capability_input(LeanCheckRequest, request.input)

def invoke(self, payload: LeanCheckRequest) -> OperationProjection:
checked = self.lean.verify(
statement=str(payload["statement"]),
proof=str(payload["proof"]),
environment=LeanEnvironment(str(payload.get("environment", "CORE"))),
statement=payload.statement,
proof=payload.proof,
environment=payload.environment,
)
verified = checked.result.verification_record_uri is not None
evidence = (checked.certificate_uri,)
Expand Down
62 changes: 62 additions & 0 deletions src/jacobian/canonical.py
Original file line number Diff line number Diff line change
Expand Up @@ -169,6 +169,68 @@ def _normalize(value: Any, *, limits: CanonicalLimits, depth: int) -> Any:
raise CanonicalizationError("unsupported JSON value type")


def _validate_json_value(value: Any, *, limits: CanonicalLimits, depth: int) -> None:
"""Validate bounded interoperable JSON without changing semantic values."""

if depth > limits.max_depth:
raise CanonicalizationError("JSON nesting exceeds the configured depth limit")
if isinstance(value, float):
raise CanonicalizationError("JSON floating-point numbers are not allowed")
if isinstance(value, int):
_validate_json_integer(value)
return
if isinstance(value, list):
_validate_json_items(value, limits=limits, depth=depth)
return
if isinstance(value, dict):
_validate_json_object(value, limits=limits, depth=depth)
return
if value is None or isinstance(value, str):
return
raise CanonicalizationError("unsupported JSON value type")


def _validate_json_integer(value: int) -> None:
if abs(value) > _MAX_SAFE_JSON_INTEGER:
raise CanonicalizationError(
"JSON integers outside the interoperable range must be encoded as strings"
)


def _validate_json_items(
values: list[Any], *, limits: CanonicalLimits, depth: int
) -> None:
for value in values:
_validate_json_value(value, limits=limits, depth=depth + 1)


def _validate_json_object(
value: dict[Any, Any], *, limits: CanonicalLimits, depth: int
) -> None:
for key, nested in value.items():
if not isinstance(key, str):
raise CanonicalizationError("JSON object keys must be strings")
_validate_json_value(nested, limits=limits, depth=depth + 1)


def encode_strict_json(
value: Any,
*,
limits: CanonicalLimits | None = None,
) -> bytes:
"""Encode bounded JSON deterministically without semantic normalization."""

active_limits = limits or CanonicalLimits()
_validate_json_value(value, limits=active_limits, depth=0)
try:
encoded = rfc8785.dumps(value)
except (rfc8785.CanonicalizationError, RecursionError) as exc:
raise CanonicalizationError("value cannot be encoded as strict JSON") from exc
if len(encoded) > active_limits.max_output_bytes:
raise CanonicalizationError("JSON exceeds the configured size limit")
return encoded


def _normalize_object(
value: dict[str, Any], *, limits: CanonicalLimits, depth: int
) -> dict[str, Any]:
Expand Down
65 changes: 54 additions & 11 deletions src/jacobian/capability_adapters.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,29 +2,72 @@

from __future__ import annotations

from typing import Literal, Protocol, runtime_checkable
from typing import Any, Protocol, TypeVar

from pydantic import BaseModel

from jacobian.canonical import CanonicalizationError, encode_strict_json
from jacobian.capability_errors import CapabilityInvocationError
from jacobian.contracts.base import ContractModel
from jacobian.contracts.capabilities import (
CapabilityDescriptor,
CapabilityDiagnostic,
CapabilityRequest,
)
from jacobian.operation_projection import OperationProjection

PreparedT = TypeVar("PreparedT")

class CapabilityAdapter(Protocol):
"""Operator-installed adapter; registration requires no MCP changes."""

@property
def descriptor(self) -> CapabilityDescriptor: ...
def _contains_typed_value(value: Any) -> bool:
if isinstance(value, ContractModel):
return True
if isinstance(value, list):
return any(_contains_typed_value(item) for item in value)
if isinstance(value, dict):
return any(_contains_typed_value(item) for item in value.values())
return False


def parse_capability_input[ModelT: BaseModel](
model: type[ModelT], payload: dict[str, Any]
) -> ModelT:
"""Parse one bounded request into its owning model.

def invoke(self, request: CapabilityRequest) -> OperationProjection: ...
Ordinary caller input crosses the strict JSON parser exactly once. Requests
containing values resolved from typed input ports bind those already-
validated objects directly in strict Python mode; the operation adapter has
separately accounted for their canonical JSON projection before this call.
"""

if _contains_typed_value(payload):
return model.model_validate(payload, strict=True)
Comment thread
morluto marked this conversation as resolved.
Outdated
Comment thread
morluto marked this conversation as resolved.
Outdated
try:
encoded = encode_strict_json(payload)
except CanonicalizationError as exc:
raise CapabilityInvocationError(
CapabilityDiagnostic(
code="INVALID_REQUEST",
stage="capability_input_validation",
message="The capability request is not valid bounded JSON.",
hint=(
"Use only JSON objects, arrays, strings, booleans, null, "
"and supported finite numbers within the configured limits."
),
)
) from exc
return model.model_validate_json(encoded, strict=True)


class CapabilityAdapter(Protocol[PreparedT]):
"""Installed typed adapter; registration requires no MCP changes."""

@property
def descriptor(self) -> CapabilityDescriptor: ...

@runtime_checkable
class TypedInputAdapter(Protocol):
"""Adapter that owns one typed input parse and needs no schema execution."""
def prepare(self, request: CapabilityRequest) -> PreparedT: ...

typed_input: Literal[True]
def invoke(self, prepared: PreparedT) -> OperationProjection: ...


__all__ = ["CapabilityAdapter", "TypedInputAdapter"]
__all__ = ["CapabilityAdapter", "parse_capability_input"]
Loading