Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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 @@ -207,6 +207,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
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
46 changes: 35 additions & 11 deletions src/jacobian/capability_adapters.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,29 +2,53 @@

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.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 parse_capability_input[ModelT: BaseModel](
model: type[ModelT], payload: dict[str, Any]
) -> ModelT:
"""Parse one JSON capability payload strictly into its owning model."""

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)

def invoke(self, request: CapabilityRequest) -> OperationProjection: ...

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