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
27 changes: 22 additions & 5 deletions src/jacobian/finite_partition.py
Original file line number Diff line number Diff line change
Expand Up @@ -195,7 +195,10 @@ def __init__(
title="Partition an explicit finite domain",
description=(
"Materialize named cases over an explicit finite scope and optionally "
"replay exact coverage and disjointness with an authorized checker."
"replay exact coverage and disjointness with an authorized checker. "
"Members and case labels are opaque caller-supplied strings; the "
"checker does not establish their mathematical meaning or that the "
"supplied universe exhausts an external domain."
),
provider="jacobian.finite",
provider_runtime=known_provider_runtime(
Expand Down Expand Up @@ -372,6 +375,15 @@ def invoke(self, request: CapabilityRequest) -> CapabilityResult:
and not duplicate_case_ids
and (not require_disjoint or not overlaps)
)
verified_replay_basis = (
"authorized checker replayed equality-based coverage and required "
"disjointness within the caller-supplied universe"
if require_disjoint
else (
"authorized checker replayed equality-based coverage within the "
"caller-supplied universe; disjointness was not required"
)
)
return CapabilityResult(
capability_id=self.descriptor.capability_id,
capability_version=self.descriptor.version,
Expand All @@ -397,7 +409,10 @@ def invoke(self, request: CapabilityRequest) -> CapabilityResult:
"duplicate_case_ids": duplicate_case_ids,
},
scope=CapabilityScope(
description="the exact supplied finite universe",
description=(
"the exact caller-supplied finite universe; external-domain "
"completeness and member semantics are not checked"
),
parameters={"element_count": len(universe)},
artifact_uri=scope.artifact_uri,
),
Expand All @@ -408,7 +423,8 @@ def invoke(self, request: CapabilityRequest) -> CapabilityResult:
else CapabilityCompletenessStatus.PARTIAL
),
basis=(
"authorized checker replayed exact finite membership"
f"{verified_replay_basis}; it did not check external-domain "
"completeness or member/case semantics"
if verified
else "generator-side membership accounting; not independently checked"
),
Expand All @@ -435,7 +451,8 @@ def invoke(self, request: CapabilityRequest) -> CapabilityResult:
assurance=CapabilityAssurance(
level=assurance_level,
basis=(
"operator-authorized independent finite partition checker accepted"
f"{verified_replay_basis}; external-domain completeness and "
"member/case semantics were not checked"
if verified
else "partition was proposed and inspected by its generator only"
),
Expand Down Expand Up @@ -465,7 +482,7 @@ def _verify(
scope_digest=scope.manifest.object_digest,
)
payload: dict[str, Any] = {
"replay": "exact finite membership",
"replay": "equality-based finite coverage and conditional disjointness",
"relation_id": "case.relation.partitions",
"obligation_uri": claim_uri,
}
Expand Down
46 changes: 44 additions & 2 deletions tests/composition/runtime/test_finite_partition_capability.py
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,12 @@
from jacobian.contracts.results import Arithmetic, Conclusion, Coverage, Method


def _request(mode: CapabilityMode, *, missing_last: bool = False) -> CapabilityRequest:
def _request(
mode: CapabilityMode,
*,
missing_last: bool = False,
require_disjoint: bool = True,
) -> CapabilityRequest:
return CapabilityRequest(
capability_id="case.partition.finite",
mode=mode,
Expand All @@ -24,7 +29,7 @@ def _request(mode: CapabilityMode, *, missing_last: bool = False) -> CapabilityR
"members": ["1", "3"] if missing_last else ["1", "3", "5"],
},
],
"require_disjoint": True,
"require_disjoint": require_disjoint,
},
)

Expand Down Expand Up @@ -60,6 +65,43 @@ def test_finite_partition_verify_replays_and_discharges_obligation(
assert result.obligations[0].status is CapabilityObligationStatus.DISCHARGED


def test_finite_partition_contract_and_result_preserve_semantic_boundary(
authorized_complete_runtime,
) -> None:
runtime = authorized_complete_runtime
descriptor = next(
item
for item in runtime.core.capabilities.catalog().capabilities
if item.capability_id == "case.partition.finite"
)
result = runtime.core.capabilities.invoke(_request(CapabilityMode.VERIFY))

assert "opaque caller-supplied strings" in descriptor.description
assert "does not establish their mathematical meaning" in descriptor.description
assert "external-domain completeness" in result.scope.description
assert "member/case semantics were not checked" in result.assurance.basis
assert "member/case semantics" in result.completeness.basis


def test_finite_partition_reports_conditional_disjointness_scope(
authorized_complete_runtime,
) -> None:
runtime = authorized_complete_runtime
request = _request(CapabilityMode.VERIFY, require_disjoint=False)
request.input["cases"][1]["members"].append("0")

result = runtime.core.capabilities.invoke(request)

assert result.assurance.level is CapabilityAssuranceLevel.VERIFIED
assert result.output["overlaps"] == ["0"]
assert "disjointness was not required" in result.assurance.basis
assert "disjointness was not required" in result.completeness.basis
certificate = runtime.core.store.get(result.output["certificate_uri"])
assert certificate.payload["payload"]["replay"] == (
"equality-based finite coverage and conditional disjointness"
)


def test_finite_partition_verify_fails_closed_on_incomplete_cases(
authorized_complete_runtime,
) -> None:
Expand Down
Loading