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
120 changes: 114 additions & 6 deletions src/jacobian/checker_identity.py
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,9 @@
import importlib.util
import re
import sys
from collections.abc import Callable, Iterable
from collections.abc import Callable, Iterable, Iterator, Mapping
from contextlib import contextmanager
from contextvars import ContextVar
from dataclasses import dataclass
from functools import lru_cache
from importlib import metadata
Expand Down Expand Up @@ -52,6 +54,38 @@ class _ResolvedModule:
is_package: bool


@dataclass(slots=True)
class _ManifestMeasurementBatch:
source_modules: dict[
tuple[tuple[str, ...], frozenset[str]], tuple[CheckerSourceModule, ...]
]
distributions: dict[str, CheckerPythonDistribution]
package_owners: Mapping[str, list[str]] | None = None
python_runtime: CheckerPythonRuntime | None = None


_ACTIVE_MEASUREMENT_BATCH: ContextVar[_ManifestMeasurementBatch | None] = ContextVar(
"jacobian_checker_manifest_measurement_batch", default=None
)


@contextmanager
def batch_checker_manifest_measurement() -> Iterator[None]:
"""Share immutable identity measurements across one installation operation."""

active = _ACTIVE_MEASUREMENT_BATCH.get()
if active is not None:
yield
return
token = _ACTIVE_MEASUREMENT_BATCH.set(
_ManifestMeasurementBatch(source_modules={}, distributions={})
)
try:
yield
finally:
_ACTIVE_MEASUREMENT_BATCH.reset(token)


class _DeclaredSourceLoader(importlib.abc.Loader):
"""Load one manifest-bound module from remeasured source only."""

Expand Down Expand Up @@ -154,19 +188,19 @@ def build_checker_manifest(
first_party_packages = frozenset(
{_JACOBIAN_PACKAGE, entrypoint_module.split(".", 1)[0]}
)
checker_source_modules = _collect_source_modules(
checker_source_modules = _batched_source_modules(
(entrypoint_module,),
first_party_packages=first_party_packages,
)
worker_source_modules = _collect_source_modules(
worker_source_modules = _batched_source_modules(
(_CHECKER_WORKER_MODULE, *extra_modules),
first_party_packages=first_party_packages,
)
return CheckerManifest(
entrypoint=entrypoint,
checker_source_modules=checker_source_modules,
worker_source_modules=worker_source_modules,
python_runtime=_python_runtime(),
python_runtime=_batched_python_runtime(),
python_distributions=_collect_python_distributions(
(*checker_source_modules, *worker_source_modules),
first_party_packages=first_party_packages,
Expand Down Expand Up @@ -206,6 +240,31 @@ def require_manifest_unchanged(manifest: CheckerManifest) -> str:
return checker_implementation_digest(measured)


def require_manifest_material_unchanged(manifest: CheckerManifest) -> str:
"""Reject changes to every execution artifact already bound by a manifest.

The worker performs full dependency discovery before loading the checker. Its
post-execution check only needs to remeasure that closed set: the import guard
prevents undeclared code from entering the process, while direct remeasurement
avoids rebuilding and reparsing the complete import graph a second time.
"""

for expected in _manifest_source_modules(manifest):
resolved = _resolve_module(expected.module)
measured = _source_digest(resolved.path.read_bytes())
if measured != expected.source_digest:
raise CheckerManifestError(f"checker source changed: {expected.module}")
if _python_runtime() != manifest.python_runtime:
raise CheckerManifestError("checker Python runtime changed")
measured_distributions = tuple(
_measure_python_distribution(item.distribution)
for item in manifest.python_distributions
)
if measured_distributions != manifest.python_distributions:
raise CheckerManifestError("checker Python distribution changed")
return checker_implementation_digest(manifest)


def install_manifest_import_guard(manifest: CheckerManifest) -> None:
"""Reload the checker through the manifest and reject undeclared code imports."""

Expand Down Expand Up @@ -273,6 +332,24 @@ def _collect_source_modules(
)


def _batched_source_modules(
roots: tuple[str, ...],
*,
first_party_packages: frozenset[str],
) -> tuple[CheckerSourceModule, ...]:
batch = _ACTIVE_MEASUREMENT_BATCH.get()
if batch is None:
return _collect_source_modules(roots, first_party_packages=first_party_packages)
key = (roots, first_party_packages)
measured = batch.source_modules.get(key)
if measured is None:
measured = _collect_source_modules(
roots, first_party_packages=first_party_packages
)
batch.source_modules[key] = measured
return measured


def _manifest_source_modules(
manifest: CheckerManifest,
) -> tuple[CheckerSourceModule, ...]:
Expand Down Expand Up @@ -302,7 +379,13 @@ def _collect_python_distributions(
for bound_source in source_modules:
source = _resolve_module(bound_source.module)
import_roots.update(_third_party_import_roots(source, first_party_packages))
package_owners = metadata.packages_distributions()
batch = _ACTIVE_MEASUREMENT_BATCH.get()
if batch is not None and batch.package_owners is not None:
package_owners = batch.package_owners
else:
package_owners = metadata.packages_distributions()
if batch is not None:
batch.package_owners = package_owners
distributions = set(_WORKER_DISTRIBUTIONS)
for root in import_roots:
owners = package_owners.get(root)
Expand All @@ -317,7 +400,7 @@ def _collect_python_distributions(
distributions.add(owners[0])
measured: dict[str, CheckerPythonDistribution] = {}
for distribution in sorted(distributions, key=_distribution_key):
identity = _measure_python_distribution(distribution)
identity = _batched_python_distribution(distribution)
key = _distribution_key(identity.distribution)
existing = measured.setdefault(key, identity)
if existing != identity:
Expand Down Expand Up @@ -475,6 +558,29 @@ def _measure_python_distribution(distribution: str) -> CheckerPythonDistribution
)


def _batched_python_distribution(
distribution: str,
) -> CheckerPythonDistribution:
batch = _ACTIVE_MEASUREMENT_BATCH.get()
if batch is None:
return _measure_python_distribution(distribution)
key = _distribution_key(distribution)
measured = batch.distributions.get(key)
if measured is None:
measured = _measure_python_distribution(distribution)
batch.distributions[key] = measured
return measured


def _batched_python_runtime() -> CheckerPythonRuntime:
batch = _ACTIVE_MEASUREMENT_BATCH.get()
if batch is None:
return _python_runtime()
if batch.python_runtime is None:
batch.python_runtime = _python_runtime()
return batch.python_runtime


def _distribution_file_closure(
installed: metadata.Distribution,
) -> tuple[int, str]:
Expand Down Expand Up @@ -693,9 +799,11 @@ def _source_digest(source: bytes) -> str:
__all__ = [
"CheckerManifestError",
"UndeclaredCheckerImportError",
"batch_checker_manifest_measurement",
"build_checker_manifest",
"checker_implementation_digest",
"default_checker_sandbox_policy",
"install_manifest_import_guard",
"require_manifest_material_unchanged",
"require_manifest_unchanged",
]
3 changes: 2 additions & 1 deletion src/jacobian/checker_worker.py
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@
UndeclaredCheckerImportError,
checker_implementation_digest,
install_manifest_import_guard,
require_manifest_material_unchanged,
require_manifest_unchanged,
)
from jacobian.contracts.capabilities import (
Expand Down Expand Up @@ -159,7 +160,7 @@ def _execute(manifest_json: str, request_bytes: bytes) -> CheckerWorkerSuccess:
with contextlib.redirect_stdout(sys.stderr):
checker = _resolve(manifest.entrypoint)
response = checker(request)
measured_after = require_manifest_unchanged(manifest)
measured_after = require_manifest_material_unchanged(manifest)
if measured_after != measured_before:
raise _CheckerWorkerFailureError("SOURCE_CHANGED")
_, runtime_digest_after = _measure_runtime(runtime)
Expand Down
44 changes: 43 additions & 1 deletion src/jacobian/contracts/projective_geometry.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
from math import comb, gcd, lcm
from typing import Annotated, Literal, Self

from pydantic import Field, StringConstraints, model_validator
from pydantic import Field, StrictBool, StringConstraints, model_validator

from jacobian.canonical import format_canonical_integer, parse_canonical_integer
from jacobian.contracts.exact import CanonicalRational
Expand Down Expand Up @@ -136,6 +136,47 @@ class ProjectiveMultiplicityCount(ContractModel):
flat_count: int = Field(ge=1, le=2016, strict=True)


class ProjectiveLineArrangementPreview(ContractModel):
"""Bounded inline projection of proof-critical higher flats and accounting."""

preview_schema_version: Literal["1"] = "1"
line_count: int = Field(ge=2, le=64, strict=True)
non_double_flat_count: int = Field(ge=0, le=2016, strict=True)
non_double_flats: tuple[ProjectiveArrangementFlat, ...] = Field(max_length=32)
non_double_flats_complete: StrictBool
multiplicity_histogram: tuple[ProjectiveMultiplicityCount, ...]
pair_count_total: int = Field(ge=1, le=2016, strict=True)
artifact_completion: Literal["COMPLETE"] = "COMPLETE"
arithmetic: Literal["EXACT_INTEGER"] = "EXACT_INTEGER"

@model_validator(mode="after")
def bind_bounded_projection(self) -> Self:
if any(flat.multiplicity <= 2 for flat in self.non_double_flats):
raise ValueError(
"preview non-double flats must have multiplicity above two"
)
if self.non_double_flat_count < len(self.non_double_flats):
raise ValueError(
"preview cannot contain more flats than the reported count"
)
if self.non_double_flats_complete != (
self.non_double_flat_count == len(self.non_double_flats)
):
raise ValueError(
"preview completeness must match its bounded flat projection"
)
supplied_histogram = tuple(
(item.multiplicity, item.flat_count) for item in self.multiplicity_histogram
)
if supplied_histogram != tuple(sorted(set(supplied_histogram))):
raise ValueError("preview multiplicity histogram must be unique and sorted")
if self.pair_count_total != comb(self.line_count, 2):
raise ValueError(
"preview pair_count_total must account for every line pair"
)
return self


class ProjectiveLineArrangementResult(ContractModel):
"""Complete exact flat lattice at rank two for one labelled arrangement."""

Expand Down Expand Up @@ -197,6 +238,7 @@ def bind_complete_arrangement_accounting(self) -> Self:
"NormalizedProjectiveLine",
"PrimitiveProjectiveTriple",
"ProjectiveArrangementFlat",
"ProjectiveLineArrangementPreview",
"ProjectiveLineArrangementRequest",
"ProjectiveLineArrangementResult",
"ProjectiveMultiplicityCount",
Expand Down
Loading